Finite Conjugate for a Bounded Isotropic Source

This is a technical endpoint for a bounded isotropic source law.

Let $E$ be finite-dimensional with its real inner-product and Borel structures, let $\mu$ be an isotropic probability measure, and let $L\in[0,\infty)$. Assume $\|y\|\le L$ for $\mu$-almost every $y$. Then there exist a potential $q:E\to\overline{\mathbb{R}}$, a point $a\in E$, real numbers $m\in\mathbb{R}$, and $\psi:E\to\mathbb{R}$ such that:

1. $q$ is convex, lower semicontinuous, and potential-integrable; its finite effective domain lies in $\overline{B}(0,L)$.
2. $a\in\overline{B}(0,L)$, $q(a)=m$, and $m\le q(y)$ for every $y$.
3. For every $x$, $q^*(x)$ is neither $+\infty$ nor $-\infty$, and

4. $\psi(x)=(q^*(x)).toReal$ and $q^*(x)=\psi(x)$ as an extended-real coercion.
5. $\operatorname{mass}_{dx}(q^*)=1$, and every potential-integrable competitor $f$ satisfies

This declaration establishes global finiteness of the conjugate and its real representative, but not convexity or Lipschitz regularity of $\psi$.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.CEK. Shown in its original module context. Proof omitted.

theorem bounded_source_finite_conjugate
    (μ : ProbabilityMeasure E) (hμ : KLS.Isotropic μ) (L : NNReal)
    (hL : ∀ᵐ y ∂(μ : Measure E), ‖y‖ ≤ (L : ℝ)) :
    ∃ (q : E → EReal) (a : E) (m : ℝ) (ψ : E → ℝ),
      ConvexPotential q ∧
      LowerSemicontinuous q ∧
      PotentialIntegrable q (μ : Measure E) ∧
      (∀ y, q y ≠ ⊤ → y ∈ closedBall (0 : E) (L : ℝ)) ∧
      a ∈ closedBall (0 : E) (L : ℝ) ∧
      q a = (m : EReal) ∧
      (∀ y, (m : EReal) ≤ q y) ∧
      (∀ x, legendre q x ≠ ⊤ ∧ legendre q x ≠ ⊥) ∧
      (∀ x, legendre q x ≤ (((L : ℝ) * ‖x‖ - m : ℝ) : EReal)) ∧
      ψ = (fun x => (legendre q x).toReal) ∧
      (∀ x, legendre q x = (ψ x : EReal)) ∧
      mass (volume : Measure E) (legendre q) = 1 ∧
      ∀ f : E → EReal, PotentialIntegrable f (μ : Measure E) →
        variationalFunctional (volume : Measure E) (μ : Measure E) f ≤
          variationalFunctional (volume : Measure E) (μ : Measure E) q

Module navigation

Module: KLS/CEK/BoundedPrimal.

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

Supporting theorems: convex_epigraph_legendre, exists_real_global_minimum_of_bounded_domain, legendre_le_of_real_lower_bound, legendre_ne_bot_iff, bounded_source_cap_lsc.

Previous: bounded_source_cap_lsc · Next: bounded_source_lipschitz_primal.

Source excerpt, lines 237–255 · Frozen source 408915f.