Penalized Maximum and Density Comparison

This is a weak-route supporting theorem for Letwin’s second-difference argument.

Let $u,F:\mathbb R^n\to\mathbb R$. Assume: $u$ is convex, globally Lipschitz, and has compact sublevel sets; $F$ is continuous; and for every open $G$, the Alexandrov identity

holds. Let $u_k\in C^2$ and $F_k$ satisfy uniform approximation $|u_k-u|\le\delta_k$ with $\delta_k\to0$, local uniform convergence $F_k\to F$, positive-definite $\nabla^2u_k$, and $F_k\le\log\det\nabla^2u_k$. For every $h\in\mathbb R^n$ and $\eta>0$, there exists $x_0$ such that $\Delta_h^2u(x_0)-\eta u(x_0)$ is maximal and

This is an auxiliary existence and comparison result, not a dimension-free bound.

Original Lean declaration header

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

theorem exists_penalized_maximum_with_comparison {n : ℕ} {u F : EuclideanSpace ℝ (Fin n) → ℝ}
    (hconv : ConvexOn ℝ univ u) {L : NNReal} (hLip : LipschitzWith L u)
    (hcoer : ∀ R : ℝ, IsCompact {x | u x ≤ R}) (hF : Continuous F)
    (hMA : ∀ G : Set (EuclideanSpace ℝ (Fin n)), IsOpen G →
      (volume : Measure (EuclideanSpace ℝ (Fin n))) (subgradientImage u G) =
        ∫⁻ x in G, ENNReal.ofReal (Real.exp (F x)) ∂(volume : Measure (EuclideanSpace ℝ (Fin n))))
    {uk Fk : ℕ → EuclideanSpace ℝ (Fin n) → ℝ} (huk : ∀ k, ContDiff ℝ 2 (uk k))
    {δ : ℕ → ℝ} (hδ : Tendsto δ atTop (𝓝 0)) (hclose : ∀ k x, |uk k x - u x| ≤ δ k)
    (hFk : TendstoLocallyUniformly Fk F atTop)
    (hpos : ∀ k x, (hessianMatrix (uk k) x).PosDef)
    (hlog : ∀ k x, Fk k x ≤ Real.log (hessianMatrix (uk k) x).det)
    (h : EuclideanSpace ℝ (Fin n)) {η : ℝ} (hη : 0 < η) :
    ∃ x₀ : EuclideanSpace ℝ (Fin n),
      (∀ y, u (y + h) + u (y - h) - 2 * u y - η * u y ≤
        u (x₀ + h) + u (x₀ - h) - 2 * u x₀ - η * u x₀) ∧
      F (x₀ + h) + F (x₀ - h) - 2 * F x₀ ≤ η * n

Module navigation

Module: Analysis/Convex/Viscosity.

Definition modules: Analysis/BakryEmery/HessianOperator, Analysis/Convex/Subgradient.

Supporting theorems: det_hessianMatrix_le_of_lower_touch, forall_posDef_add_log_det_le_trace_iff.

Previous: ae_exists_quadraticAt_expansion · Next: ae_hessian_increment_le_generator.

Source excerpt, lines 1707–1722 · Frozen source 408915f.