Main.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The general Mahler inequality, equality characterization, and Santaló minimum.

lemma OAI.GeneralMahler.Complete_profile_input line 14

theorem OAI.GeneralMahler.mahal line 19

Source documentation

The sharp volume-product bound and its simplex equality case.

theorem mahal {n : ℕ} (K : Body n) :
    ((n : ℝ) + 1) ^ (n + 1) / (n.factorial : ℝ) ^ 2 ≤ K.P ∧
      (K.P = ((n : ℝ) + 1) ^ (n + 1) / (n.factorial : ℝ) ^ 2 ↔
        IsSimplex (K : Set (Rn n))) :=
…

Mentions: OAI.GeneralMahler.Body, OAI.GeneralMahler.IsSimplex, OAI.GeneralMahler.Rn

theorem OAI.GeneralMahler.all_centers line 26

Source documentation

The sharp lower bound also holds at every interior center.

theorem all_centers {n : ℕ} (K : Body n) {x : Rn n}
    (hx : x ∈ interior (K : Set (Rn n))) :
    ((n : ℝ) + 1) ^ (n + 1) / (n.factorial : ℝ) ^ 2 ≤ K.productAt x :=
…

Mentions: OAI.GeneralMahler.Body, OAI.GeneralMahler.Rn

def OAI.GeneralMahler.ofSet line 31
theorem OAI.GeneralMahler.general_geometric line 40
Source documentation
The Santaló minimum is attained uniquely and satisfies the sharp Mahler inequality.
```
theorem general_geometric {n : ℕ} (_hn : 1 ≤ n) (K : Set (Rn n))
    (hK : IsCompact K) (hc : Convex ℝ K) (hi : (interior K).Nonempty) :
    let D := ofSet K hK hc hi
…
```
Mentions: OAI.GeneralMahler.Rn, OAI.GeneralMahler.ofSet