ComparatorChallenges/GeneralMahler.lean

GitHub source file

4 declarations, 1 contain sorry, 0 declared as axioms

1. abbrev OAI.GeneralMahler.Rn line 12

   Also declared: OAI/Geometry/Convex/GeneralMahler/Cone.lean:22 (same declaration text).

2. def OAI.GeneralMahler.polarAt The polar of a convex body translated by an interior center line 15

   Source documentation

   The polar of a convex body translated by an interior center.

   L4DEL explanation

   The polar of a convex body translated by an interior center.

   1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

   Distinct definitions of this name: OAI/Geometry/Convex/GeneralMahler/Polar.lean:12 (different declaration text). Qualify references as OAI.GeneralMahler.polarAt@path.

   def polarAt {n : ℕ} (K : Set (Rn n)) (z : Rn n) : Set (Rn n) :=
   …

   Mentions: OAI.GeneralMahler.Rn

3. def OAI.GeneralMahler.volumeProduct The volume product minimized over the interior centers of the body line 19

   Source documentation

   The volume product minimized over the interior centers of the body.

   L4DEL explanation

   The volume product minimized over the interior centers of the body.

   1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

   Also declared: OAI/Geometry/Convex/GeneralMahler/Theorem.lean:12 (same declaration text).

   def volumeProduct {n : ℕ} (K : Set (EuclideanSpace ℝ (Fin n))) : ℝ :=
   …

4. theorem OAI.GeneralMahler.general_mahler Challenge statement: The general Mahler bound, with equality exactly for simplices sorry line 24

   Source documentation

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

   L4DEL explanation

   with Santaló point s(K), |K| |(K − s(K))◦ | ≥ (n + 1)n+1 /(n!)2 , with equality exactly for simplices

   The symmetric Mahler conjecture asks for the different, stronger constant 4n /n! on the restricted class of centrally symmetric bodies

   Among all compact convex bodies with interior in $\mathbb R^n$, the smallest possible product of the body's volume and the volume of an optimally centered polar is $(n+1)^{n+1}/(n!)^2$. Exactly the simplices attain it.

   1. polarAt K z contains the vectors $y$ whose pairing with every displacement $x-z$ from the chosen interior center is at most one. volumeProduct K is the infimum of $|K|\,|(K-z)^\circ|$ over all interior centers $z$.
   2. The hypotheses require positive dimension, compactness, convexity, and nonempty interior. No central symmetry, smooth boundary, or strict convexity is assumed.
   3. The conclusion is a conjunction: the sharp lower bound holds, and equality is equivalent to the existence of $n+1$ affinely independent vertices whose convex hull is exactly $K$.
   4. This is the nonsymmetric theorem. The stronger constant $4^n/n!$ for centrally symmetric bodies is a different statement, already exposed separately on the symmetric-Mahler page. The manuscript's functional inequality is outside this comparator target. The body is sorry, paired with OAI.Geometry.Convex.GeneralMahler.Theorem.

   Sources and attribution: Pinned Lean source (fd4aeeb2ee4f), OpenAI general-Mahler manuscript (abstract), Pinned OpenAI formalization note 087, Kurt Mahler, original polygon paper bibliographic record

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

   Checked implications (found by the pipeline and checked by Lean's kernel when it ran; a recorded result, not checked again in this build: what these are)

   1 more checked entries are routine (the same statement, a restatement, a generated lemma, one challenge file, a field of a structure, a route the released proof already takes, a duplicate): in the catalogue.

   Santaló point: the unique interior center that minimizes the volume of the translated polar body

   volume product: the volume of a convex body multiplied by the volume of its polar at an optimizing interior center

   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