Mollified Log-Determinant Lower Bound

This is the mollified log-det lower bound from the weak Letwin route.

Let $u,F:\mathbb R^n\to\mathbb R$, with $u$ convex and $F$ continuous. Assume that, almost everywhere in $x$, there exist a Hermitian positive-definite matrix $B$ and a vector $g$ such that

1. $F(x)\leq\log\det B$;
2. for every $\varepsilon>0$, $u$ has at $x$ the quadratic expansion represented by quadraticAt B x g (u x), with error bounded by $\varepsilon\|y-x\|^2$ near $x$.

For every $C^2$ compactly supported bump $\phi$ normalized with respect to volume, and every $x\in\mathbb R^n$, the convolution $u_\phi=\phi.\mathrm{normed}*u$ has positive-definite Hessian and

This is the formalized mollified determinant inequality and can be reused as the regularized convexity input in moment-map arguments.

Original Lean declaration header

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

theorem posDef_and_convolution_le_log_det_hessianMatrix {n : ℕ}
    {u F : EuclideanSpace ℝ (Fin n) → ℝ} (hconv : ConvexOn ℝ univ u) (hF : Continuous F)
    (hae : ∀ᵐ x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      ∃ B : Matrix (Fin n) (Fin n) ℝ, B.IsHermitian ∧ B.PosDef ∧ F x ≤ Real.log B.det ∧
        ∃ g : EuclideanSpace ℝ (Fin n),
          ∀ ε > 0, ∀ᶠ y in 𝓝 x, |u y - quadraticAt B x g (u x) y| ≤ ε * ‖y - x‖ ^ 2)
    (φ : ContDiffBump (0 : EuclideanSpace ℝ (Fin n))) (x : EuclideanSpace ℝ (Fin n)) :
    (hessianMatrix (convolution (φ.normed volume) u (ContinuousLinearMap.lsmul ℝ ℝ) volume) x).PosDef ∧
      convolution (φ.normed volume) F (ContinuousLinearMap.lsmul ℝ ℝ) volume x ≤
        Real.log (hessianMatrix
          (convolution (φ.normed volume) u (ContinuousLinearMap.lsmul ℝ ℝ) volume) x).det

Module navigation

Module: Analysis/Convex/Viscosity.

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

Supporting theorems: forall_posDef_add_log_det_le_trace_iff, posSemidef_hessianMatrix_of_upper_touch, convolution_hessian_integral, trace_integral_bound.

Previous: trace_integral_bound · Next: ae_exists_quadraticAt_expansion.

Source excerpt, lines 1327–1337 · Frozen source 408915f.