Lower-Semicontinuous Capped Optimizer

This is a normalized capped-source construction for a bounded isotropic probability law.

Let $E$ be a finite-dimensional real inner-product space with Borel measurable structure, let $\mu$ be a probability measure on $E$, and let $L\in[0,\infty)$. Assume $\mu$ is isotropic and

$$\|y\|\le L\quad\text{for $\mu$-almost every }y.$$

Then there exists $q:E\to\overline{\mathbb{R}}$ such that:

1. $q$ is a convex lower-semicontinuous potential and is potential-integrable under $\mu$.
2. If $q(y)<\infty$, then $y\in\overline{B}(0,L)$.
3. Its conjugate mass with respect to Lebesgue measure is one:

$$\operatorname{mass}_{dx}(q^*)=1.$$

4. Every potential-integrable competitor $f$ satisfies

$$I_{dx,\mu}(f)\le I_{dx,\mu}(q).$$

The declaration is a reusable capped optimizer interface retaining convexity, lower semicontinuity, integrability, normalization, and maximality.

Original Lean declaration header

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

theorem bounded_source_cap_lsc
    (μ : ProbabilityMeasure E) (hμ : KLS.Isotropic μ) (L : NNReal)
    (hL : ∀ᵐ y ∂(μ : Measure E), ‖y‖ ≤ (L : ℝ)) :
    ∃ q : E → EReal,
      ConvexPotential q ∧
      LowerSemicontinuous q ∧
      PotentialIntegrable q (μ : Measure E) ∧
      (∀ y, q y ≠ ⊤ → y ∈ closedBall (0 : E) (L : ℝ)) ∧
      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: closedBallCap_lowerSemicontinuous, exists_variational_maximum.

Next: bounded_source_finite_conjugate.

Source excerpt, lines 45–56 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_CEK_BoundedPrimal

open MeasureTheory Set Metric
open FunctionalInequalities.Analysis
open FunctionalInequalities.Probability.MomentMeasure
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

theorem FunctionalInequalities.KLS.CEK.bounded_source_cap_lsc_readable
    (μ : ProbabilityMeasure E) (hμ : KLS.Isotropic μ) (L : NNReal)
    (hL : ∀ᵐ y ∂(μ : Measure E), ‖y‖ ≤ (L : ℝ)) :
    ∃ q : E → EReal,
      ConvexPotential q ∧
      LowerSemicontinuous q ∧
      PotentialIntegrable q (μ : Measure E) ∧
      (∀ y, q y ≠ ⊤ → y ∈ closedBall (0 : E) (L : ℝ)) ∧
      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 := by sorry