Convexified Competitor Within Epsilon

This formalizes the epsilon reduction underlying Proposition 12 of Cordero–Erausquin–Klartag (arXiv:1304.0630v1).

Let $dx$ be a measure and let $\mu$ be a nonzero finite Borel measure on a real inner-product space. If $f$ is potential-integrable and $\varepsilon>0$, then there exists an integer $n>0$ such that, with

$c$ is a convex lower-semicontinuous potential, is potential-integrable with respect to $\mu$, and

The variational functional and the epsilon are interpreted in EReal, so zero and infinite exponential masses remain part of the statement.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.MomentMeasure. Shown in its original module context. Proof omitted.

theorem exists_convexified_lowerTruncate_variational_le_add [IsFiniteMeasure μ]
    (dx : Measure E) (f : E → EReal) (hμ : μ ≠ 0) (hf : PotentialIntegrable f μ)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ n : ℕ, 0 < n ∧
      let c := legendre (legendre (lowerTruncate f (n : ℝ)))
      ConvexPotential c ∧ LowerSemicontinuous c ∧ PotentialIntegrable c μ ∧
        variationalFunctional dx μ f ≤ variationalFunctional dx μ c + (ε : EReal)

Module navigation

Module: Probability/MomentMeasure/Truncation.

Definition modules: Probability/MomentMeasure/Basic, Analysis/Convex/Legendre.

Supporting theorems: lowerTruncate_convexification, biconjugate_lowerTruncate_potentialIntegrable.

Source excerpt, lines 188–194 · Frozen source 408915f.