Theorem.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GeneralMahler.volumeProduct line 12
Source documentation
The volume product minimized over the interior centers of the body.
Also declared: ComparatorChallenges/GeneralMahler.lean:19 (same declaration text).
```
def volumeProduct {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) : ℝ :=
…
```

theorem OAI.GeneralMahler.general_mahler line 17

Source documentation

The sharp general Mahler inequality, with equality exactly for simplices.

Distinct definitions of this name: ComparatorChallenges/GeneralMahler.lean:24 (same statement text; different proof or body). Qualify references as OAI.GeneralMahler.general_mahler@path.

theorem general_mahler {n : ℕ} (hn : 1 ≤ n)
    (K : Set (EuclideanSpace ℝ (Fin n)))
    (hcompact : IsCompact K) (hconvex : Convex ℝ K)
    (hinterior : (interior K).Nonempty) :
    ((n : ℝ) + 1) ^ (n + 1) / (Nat.factorial n : ℝ) ^ 2 ≤ volumeProduct K ∧
      (volumeProduct K = ((n : ℝ) + 1) ^ (n + 1) / (Nat.factorial n : ℝ) ^ 2 ↔
        ∃ vertices : Fin (n + 1) → EuclideanSpace ℝ (Fin n),
          AffineIndependent ℝ vertices ∧ K = convexHull ℝ (range vertices)) := by
…

Mentions: OAI.GeneralMahler.volumeProduct