OAI/Analysis/Mahler/LowDimensionalBodies.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SymmetricMahler.symmetric_mahler_dimension_one line 14

   Source documentation

   The symmetric Mahler body inequality in dimension one.

   theorem symmetric_mahler_dimension_one
       {K : Set (Fin 1 → ℝ)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (hsym : ∀ x ∈ K, -x ∈ K) (hint : (interior K).Nonempty) :
       4 ≤ (volume K).toReal*(volume (coordinatePolar K)).toReal := by
   …

   Mentions: OAI.SymmetricMahler.coordinatePolar

2. theorem OAI.SymmetricMahler.symmetric_mahler_dimension_two line 28

   Source documentation

   The symmetric Mahler body inequality in dimension two, using the coordinate/radius identity and the dimension-two homogeneous flux value; no flux, mass, regularity or approximation conclusion is an extra premise.

   theorem symmetric_mahler_dimension_two
       {K : Set (Fin 2 → ℝ)} (hK : IsCompact K) (hconv : Convex ℝ K)
       (hsym : ∀ x ∈ K, -x ∈ K) (hint : (interior K).Nonempty) :
       8 ≤ (volume K).toReal*(volume (coordinatePolar K)).toReal := by
   …

   Mentions: OAI.SymmetricMahler.coordinatePolar