OAI/Analysis/Mahler/ConvexMassReduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SymmetricMahler.symmetric_mahler_of_special_gram_mass line 13

   Source documentation

   Reduction of the full symmetric convex-body theorem to the exact complex mass inequality. The remaining analytic premise is displayed explicitly.

   theorem symmetric_mahler_of_special_gram_mass {n : ℕ} (hn : 1 ≤ n)
       (hmass : ∀ N (A : Matrix (Fin N) (Fin n) ℝ), Function.Injective (measurement A) →
         ∀ m : ℕ, 2 ≤ m →
           ENNReal.ofReal ((Real.pi * (m : ℝ)) ^ n) ≤
             ∫⁻ z in specialSublevel A m,
               ENNReal.ofReal ((Nat.factorial n : ℝ) * specialGramDet A m z))
       {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.measurement, OAI.SymmetricMahler.specialSublevel, OAI.SymmetricMahler.specialGramDet, OAI.SymmetricMahler.coordinatePolar