BrunnMinkowski.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PettyProjection.BrunnMinkowskiRoot line 18
Source documentation
The dimension-induction predicate, used only with a proved lower-dimensional case. It is not an extra hypothesis on the projection-volume main theorem.
```
def BrunnMinkowskiRoot (E : Type uE) [NormedAddCommGroup E] [NormedSpace ℝ E]
    [MeasureSpace E] (m : ℕ) : Prop :=
…
```
lemma OAI.PettyProjection.sliceDensity_root_concave line 27
lemma OAI.PettyProjection.sliceDensity_continuous line 44

theorem OAI.PettyProjection.brunnMinkowski_product_unit line 56

Source documentation

The actual convex-body product step, not a replacement by abstract densities.

theorem brunnMinkowski_product_unit {m : ℕ} (hm0 : 0 < m) (hm : BrunnMinkowskiRoot E m)
    {K M : Set (E × ℝ)} (hK : IsCompact K) (hcK : Convex ℝ K)
    (hiK : (interior K).Nonempty) (hM : IsCompact M) (hcM : Convex ℝ M)
    (hiM : (interior M).Nonempty) (hvK : volume.real K=1) (hvM : volume.real M=1)
    {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a+b=1) :
    1 ≤ volume.real (a • K+b • M) := by
…

Mentions: OAI.PettyProjection.BrunnMinkowskiRoot

lemma OAI.PettyProjection.volumeReal_smul_nonneg line 113
lemma OAI.PettyProjection.volumeReal_pos_of_body line 120

theorem OAI.PettyProjection.brunnMinkowski_of_unit line 127

Source documentation

Usual normalization from the unit-volume form. The exponent is the actual finite dimension of the Haar space, and the bodies remain arbitrary.

theorem brunnMinkowski_of_unit {d : ℕ} (hd : 0 < d) (hDim : Module.finrank ℝ E=d)
    (hunit : ∀ K M : Set E, IsCompact K → Convex ℝ K → (interior K).Nonempty →
      IsCompact M → Convex ℝ M → (interior M).Nonempty →
      volume.real K=1 → volume.real M=1 → ∀ a b : ℝ, 0 < a → 0 < b → a+b=1 →
      1 ≤ volume.real (a • K+b • M)) : BrunnMinkowskiRoot E d := by
…

Mentions: OAI.PettyProjection.BrunnMinkowskiRoot

lemma OAI.PettyProjection.linearEquiv_preimage_combo line 187
lemma OAI.PettyProjection.BrunnMinkowskiRoot.equiv line 200
lemma OAI.PettyProjection.brunnMinkowski_real line 224
Source documentation
The one-dimensional base case, with no symmetry or origin condition.
```
lemma brunnMinkowski_real : BrunnMinkowskiRoot ℝ 1 := by
…
```
Mentions: OAI.PettyProjection.BrunnMinkowskiRoot
def OAI.PettyProjection.finSplitLinear line 247
Source documentation
Standard coordinate splitting, with explicit measure evidence.
```
def finSplitLinear (n : ℕ) : (Fin (n+1) → ℝ) ≃ₗ[ℝ] ((Fin n → ℝ) × ℝ) where
…
```
def OAI.PettyProjection.finSplit line 253
lemma OAI.PettyProjection.finSplit_measurePreserving line 256
def OAI.PettyProjection.finOneLinear line 262
def OAI.PettyProjection.finOne line 264
lemma OAI.PettyProjection.finOne_measurePreserving line 266
theorem OAI.PettyProjection.brunnMinkowski_fin line 271
Source documentation
Brunn--Minkowski in all positive Cartesian dimensions, obtained by the actual convex-body slice induction.
```
theorem brunnMinkowski_fin (n : ℕ) : BrunnMinkowskiRoot (Fin (n+1) → ℝ) (n+1) := by
…
```
Mentions: OAI.PettyProjection.BrunnMinkowskiRoot
theorem OAI.PettyProjection.brunnMinkowski_space line 290
Source documentation
Standard Euclidean volume version used for the projection-body theorem.
```
theorem brunnMinkowski_space {n : ℕ} (hn : 0 < n) : BrunnMinkowskiRoot (Space n) n := by
…
```
Mentions: OAI.PettyProjection.BrunnMinkowskiRoot, OAI.PettyProjection.Space

theorem OAI.PettyProjection.brunnMinkowski_innerProduct line 305

Source documentation

Brunn--Minkowski for the canonical Euclidean volume on any finite-dimensional real inner-product space.

theorem brunnMinkowski_innerProduct {E : Type uE} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (hE : 0 < Module.finrank ℝ E) : BrunnMinkowskiRoot E (Module.finrank ℝ E) := by
…

Mentions: OAI.PettyProjection.BrunnMinkowskiRoot