OAI.SymmetricMahler.symmetric_mahler
ProvedThe theorem states that, for every positive integer n and every subset K of ℝⁿ (functions Fin n → ℝ) that is compact, convex, centrally symmetric (x ∈ K implies −x ∈ K) and has nonempty interior, the product of the Lebesgue volume of K and the Lebesgue volume of its coordinate polar is at least 4ⁿ/n!. Here the coordinate polar of K is the set of vectors p such that the standard dot product ∑ᵢ pᵢvᵢ is at most 1 for every v in K. Volumes are taken as real numbers via the real-valued conversion of the Lebesgue measure. The result is admitted in the source without a proof.
Preamble
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/MahlerConjecture.lean; bytes 246..549
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
import Definitions.Def_MahlerConjecture
namespace OAI
namespace SymmetricMahler
variable {I : Type*} [Fintype I]
noncomputable section
open Set MeasureTheory
Formal statement
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
sorry
end
end SymmetricMahler
end OAI
Source
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.