OAI.CAT0Fillings.sharp_integral_filling
OpenThe theorem states that, for a proper metric space X with its Borel σ-algebra that is CAT(0), meaning there is a choice of geodesic parametrization segment(x,y,t) from x to y (with segment(x,y,0)=x, segment(x,y,1)=y, and dist(segment(x,y,s),segment(x,y,t))=|s−t|·dist(x,y) for s,t in [0,1]) satisfying the comparison inequality dist(segment(o,x,s),segment(o,y,t))² ≤ (s·d(o,x) − t·d(o,y))² + s·t·(d(x,y)² − (d(o,x) − d(o,y))²), the following filling property holds for every integer n ≥ 2. Let T be an integral n-current on X, that is, a metric current (a multilinear functional on a bounded Lipschitz function and n Lipschitz functions, with locality, continuity and finite mass) that is a countable sum of disjointly supported integer-multiplicity bi-Lipschitz chart pieces and whose boundary has the same properties, and suppose T is compactly supported and a cycle, meaning its boundary is zero. Then there exists a compactly supported integral (n+1)-current S on X whose boundary is T and whose mass satisfies mass(S) ≤ c_n · mass(T)^((n+1)/n), where c_n = 1/((n+1)·(σ_n)^(1/n)), σ_n = (n+1)·ω_{n+1} is the area of the unit n-sphere and ω_{n+1} is the volume of the unit ball in Euclidean (n+1)-space. This is an admitted theorem statement, not a verified proof.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/SharpCAT0Filling.lean; bytes 5363..5802 -- 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_SharpCAT0Filling namespace OAI open Set Filter MeasureTheory open scoped Topology ENNReal NNReal namespace CAT0Fillings attribute [local instance] Classical.propDecidable universe u
theorem sharp_integral_filling
(X : Type u) [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [ProperSpace X]
(hX : IsCAT0 X) (n : ℕ) (hn : 2 ≤ n) (T : IntegralCurrent X n)
(hTc : CompactlySupported T.val) (hTz : IsCycle T.val) :
∃ S : IntegralCurrent X (n + 1), CompactlySupported S.val ∧
boundarySucc S.val = T.val ∧
mass S.val ≤ fillingCoefficient n * (mass T.val) ^ fillingPower n := by
sorry
end CAT0Fillings
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.