Hadwiger's theorem on valuations

AbbreviationModel space for convex bodies#✓fully proved

For a natural number \(n\), \(E_n\) is the real Euclidean space \(\mathbb{R}^n\) with its standard inner product and Euclidean norm.

abbrev E (n : ℕ) := EuclideanSpace ℝ (Fin n)

Used by 3

Used byHadwiger's theorem · Continuous invariant valuation · The space of continuous invariant valuations

DefinitionContinuous invariant valuation#✓fully proved

For a natural number \(n\), a real-valued function \(f\) on the convex bodies (nonempty compact convex subsets) of the Euclidean space \(\mathbb{R}^n\) is a continuous invariant valuation if: \(f\) is continuous for the Hausdorff metric; \(f(A) + f(B) = f(C) + f(D)\) for all convex bodies \(A, B, C, D\) with \(A = C \cup D\) and \(B = C \cap D\); \(f(e(A)) = f(A)\) for every convex body \(A\) and every linear isometry \(e\) of \(\mathbb{R}^n\); and \(f(A + t) = f(A)\) for every convex body \(A\) and every \(t \in \mathbb{R}^n\).

def IsValuation {n : ℕ} (f : ConvexBody (E n) → ℝ) : Prop :=
  Continuous f ∧
  (∀ A B C D : ConvexBody (E n),
      (A : Set (E n)) = (C : Set (E n)) ∪ (D : Set (E n)) →
      (B : Set (E n)) = (C : Set (E n)) ∩ (D : Set (E n)) →
      f A + f B = f C + f D) ∧
  (∀ A B : ConvexBody (E n), ∀ e : E n ≃ₗᵢ[ℝ] E n,
      (B : Set (E n)) = e '' (A : Set (E n)) → f B = f A) ∧
  (∀ A B : ConvexBody (E n), ∀ t : E n,
      (B : Set (E n)) = (· + t) '' (A : Set (E n)) → f A = f B)

Uses 1 · Used by 1

Statement usesModel space for convex bodies

Used byThe space of continuous invariant valuations

DefinitionThe space of continuous invariant valuations#✓fully proved

For a natural number \(n\), the continuous invariant valuations on the convex bodies of \(\mathbb{R}^n\) form a real linear subspace of the vector space of all functions from the convex bodies of \(\mathbb{R}^n\) to \(\mathbb{R}\).

MathlibExt.Geometry.HadwigerWanted.ConvexGeometry.valuations · 21 lines

noncomputable def valuations (n : ℕ) : Submodule ℝ (ConvexBody (E n) → ℝ) where
  carrier := {f | IsValuation f}
  add_mem' := by
    rintro f g ⟨hfc, hfa, hfi, hft⟩ ⟨hgc, hga, hgi, hgt⟩
    refine ⟨hfc.add hgc, fun A B C D hU hI => ?_, fun A B e hB => ?_, fun A B t hB => ?_⟩
    · have h₁ := hfa A B C D hU hI
      have h₂ := hga A B C D hU hI
      simp only [Pi.add_apply]
      linarith
    · simp only [Pi.add_apply, hfi A B e hB, hgi A B e hB]
    · simp only [Pi.add_apply, hft A B t hB, hgt A B t hB]
  zero_mem' :=
    ⟨continuous_zero, fun _ _ _ _ _ _ => rfl, fun _ _ _ _ => rfl, fun _ _ _ _ => rfl⟩
  smul_mem' := by
    rintro c f ⟨hfc, hfa, hfi, hft⟩
    refine ⟨hfc.const_smul c, fun A B C D hU hI => ?_, fun A B e hB => ?_, fun A B t hB => ?_⟩
    · have h := hfa A B C D hU hI
      simp only [Pi.smul_apply]
      rw [← smul_add, ← smul_add, h]
    · simp only [Pi.smul_apply, hfi A B e hB]
    · simp only [Pi.smul_apply, hft A B t hB]

Uses 2 · Used by 1

Statement usesModel space for convex bodies · Continuous invariant valuation

Used byHadwiger's theorem

TheoremHadwiger's theorem#●ready to prove

For every natural number \(n\), the real vector space of continuous invariant valuations on the convex bodies of \(\mathbb{R}^n\) (continuous, additive, and invariant under linear isometries and translations) is finite-dimensional of dimension \(n + 1\).

public theorem_wanted hadwiger (n : ℕ) : Module.finrank ℝ (valuations n) = n + 1

Sources

• H. Hadwiger (1937). Listed as §31 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem hadwiger of the lean-eval benchmark.

Uses 2

Statement usesModel space for convex bodies · The space of continuous invariant valuations

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.