hadwiger.toml

id = "hadwiger"
title = "Hadwiger's theorem"
test = false
module = "LeanEval.ConvexGeometry.Hadwiger"
holes = ["hadwiger"]
submitter = "Kim Morrison"
notes = "§31 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. The real vector space of continuous, rigid-motion-invariant valuations on convex bodies in ℝⁿ has dimension n + 1. The problem defines the IsValuation predicate (continuity in the Hausdorff metric, inclusion-exclusion additivity, invariance under linear isometries and translations) and the valuations submodule. mathlib has ConvexBody with its Hausdorff MetricSpace but no valuations, intrinsic volumes, or Hadwiger's theorem; no formalization was found in any other proof assistant. The Submodule membership-closure fields of `valuations` are shipped as sorry (routine: valuations are closed under sum and scalar multiple)."
source = "H. Hadwiger (1937). Listed as §31 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf)."
informal_solution = "Hadwiger's classification: every continuous rigid-motion-invariant valuation on convex bodies in ℝⁿ is a linear combination of the n + 1 intrinsic volumes V₀, …, Vₙ (equivalently the coefficients of the Steiner polynomial Vol(K + tB) = ∑ⱼ aⱼ tʲ). The intrinsic volumes are linearly independent valuations, so they form a basis and the space has dimension exactly n + 1. The hard direction (every such valuation is a combination of intrinsic volumes) is Hadwiger's characterization theorem, proved by reduction to the one-dimensional case via the behaviour of valuations on simple convex bodies."