MainTheorem.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SymmetricMahler.symmetric_mahler line 12
Source documentation
The symmetric Mahler inequality in every positive dimension, for ordinary Lebesgue volume and the coordinate polar.
Distinct definitions of this name: ComparatorChallenges/MahlerConjecture.lean:15 (same statement text; different proof or body). Qualify references as OAI.SymmetricMahler.symmetric_mahler@path.
```
theorem symmetric_mahler {n : ℕ} (hn : 1 ≤ n)
    {K : Set (Fin n → ℝ)} (hK : IsCompact K) (hconv : Convex ℝ K)
    (hsym : ∀ x ∈ K, -x ∈ K) (hint : (interior K).Nonempty) :
    (4:ℝ)^n/(Nat.factorial n:ℝ) ≤
      (volume K).toReal*(volume (coordinatePolar K)).toReal := by
…
```
Mentions: OAI.SymmetricMahler.coordinatePolar