OAI.Problem356.coulomb_counterexample_and_equal_infima
OpenThe theorem states, without a proof being verified here, that there exists a function ρ on three-dimensional Euclidean space ℝ³ satisfying a full Coulomb conclusion. This means ρ is a nonnegative C^∞ function with compact support, whose square root is also C^∞ with compact support, and with integral 1 over ℝ³; its density measure μ (Lebesgue measure weighted by ρ) is a probability measure. Consider three-marginal couplings of μ, namely probability measures on triples (x,y,z) of points of ℝ³ all of whose three coordinate marginals equal μ, with cost 1/|x−y| + 1/|x−z| + 1/|y−z| valued in [0,∞] (the inverse of distance zero is ∞). The Kantorovich value of μ is the infimum of the expected cost over all such couplings, and the theorem asserts it is finite and attained by some coupling. Further, no pair of measurable maps T₂,T₃ each preserving μ (pushing μ forward to itself) is a Monge optimizer: for every such pair, the expected cost of the triple (x,T₂x,T₃x) under μ is strictly larger than the Kantorovich value. Nevertheless, the Monge value, the infimum of this graph cost over all such pairs of μ-preserving maps, equals the Kantorovich value, and for every ε>0 there are μ-preserving maps T₂,T₃ with finite graph cost at most the Kantorovich value plus ε.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/CoulombCounterexample.lean; bytes 3010..3128 -- 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_CoulombCounterexample namespace OAI noncomputable section open MeasureTheory open scoped ENNReal namespace Problem356
theorem coulomb_counterexample_and_equal_infima :
∃ rho : E3 → ℝ, HasFullCoulombConclusion rho := by
sorry
end Problem356
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.