Regular Moment Potential With Weak Hessian Tensor

This formalizes a partial regularity package related to Lemmas 2.2 and Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Assume $n\ge1$, $\kappa>0$, $K$ is compact and convex with nonempty interior, $W$ is smooth, $W-\frac\kappa2\|\cdot\|^2$ is convex, and an isotropic probability measure $\mu$ has density $\mathbf{1}_K e^{-W}$ with respect to Lebesgue measure. Then there exist $u$, $L$, $L_F$, and a tensor $T$ such that:

1. $u$ is convex, $L$-Lipschitz, $C^1$, normalized by $\int e^{-u}=1$, and its tilted measure maps under $\nabla u$ to $\mu$.
2. $\nabla u$ is $(16/\kappa)$-Lipschitz.
3. $-u+W\circ\nabla u$ is $L_F$-Lipschitz and

4. Almost everywhere, $H_u\succ0$, $\log\det H_u=-u+W(\nabla u)$, and $(16/\kappa)I-H_u\succeq0$.
5. $T$ is the weak directional derivative tensor of $H_u$, with every component locally in $L^2$ on compact sets.

No further classical Hessian regularity is included.

Original Lean declaration header

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

theorem exists_regular_moment_weak_tensor :
    ∃ (u : EuclideanSpace ℝ (Fin n) → ℝ) (L LF : NNReal)
        (T : EuclideanSpace ℝ (Fin n) → Fin n → Fin n → Fin n → ℝ),
      ConvexOn ℝ univ u ∧ LipschitzWith L u ∧
      (∫ x, Real.exp (-u x) ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) = 1 ∧
      ((volume : Measure (EuclideanSpace ℝ (Fin n))).tilted (-u)).map (gradient u) =
        (μ : Measure (EuclideanSpace ℝ (Fin n))) ∧
      ContDiff ℝ 1 u ∧ LipschitzWith (Real.toNNReal (16 / κ)) (gradient u) ∧
      LipschitzWith LF (fun x => -u x + W (gradient u x)) ∧
      (∀ x h, u (x + h) + u (x - h) - 2 * u x ≤ (4 / κ) * ‖h‖ ^ 2) ∧
      (∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
        (hessianMatrix u x).PosDef ∧
        Real.log (hessianMatrix u x).det = -u x + W (gradient u x) ∧
        ((16 / κ) • (1 : Matrix (Fin n) (Fin n) ℝ) - hessianMatrix u x).PosSemidef) ∧
      ∀ k i j,
        HasWeakDerivAlong (fun x => hessianMatrix u x i j) (fun x => T x k i j)
            (EuclideanSpace.basisFun (Fin n) ℝ k) ∧
          ∀ S : Set (EuclideanSpace ℝ (Fin n)), IsCompact S →
            MemLp (fun x => T x k i j) 2 ((volume : Measure (EuclideanSpace ℝ (Fin n))).restrict S)

Module navigation

Module: KLS/CEK/MomentRegularity/WeakDerivative.

Definition modules: Analysis/BakryEmery/HessianOperator, Analysis/Operator/Coordinates, KLS/Isotropic, Analysis/WeakDerivative/Basic.

Supporting theorems: exists_lipschitzWith_neg_add_comp_gradient, exists_regular_moment_potential, exists_weak_third_derivative, secondDifference_le_of_map_gradient.

Next: exists_regular_moment_weak_first_derivative.

Source excerpt, lines 48–66 · Frozen source 408915f.