Trace Integral Bound from Almost-Everywhere Quadratic Expansions

This is a technical trace inequality for a convex function with almost-everywhere quadratic expansions.

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

1. $F(y)\leq\log\det B$;
2. $u$ admits the local quadratic expansion represented by quadraticAt B y g (u y) with error at most $\varepsilon\|z-y\|^2$ for every $\varepsilon>0$;
3. $\chi$ is $C^2$, compactly supported, and nonnegative.

Let $H$ be a real matrix satisfying, for every $v\in\mathbb R^n$,

$$\langle v,Hv\rangle=\int u(y)D^2\chi(y)[v,v] \,dy.$$

Then every positive-definite matrix $J$ satisfies

$$\int\bigl(F(y)+\log\det J+n\bigr)\chi(y)\,dy \leq \operatorname{tr}(JH).$$

The lemma packages the spectral trace comparison needed for the mollified log-determinant estimate.

Original Lean declaration header

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

set_option maxHeartbeats 800000 in
private lemma trace_integral_bound {n : ℕ}
    {u F χ : EuclideanSpace ℝ (Fin n) → ℝ}
    (hconv : ConvexOn ℝ univ u) (hF : Continuous F)
    (hae : ∀ᵐ y ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      ∃ B : Matrix (Fin n) (Fin n) ℝ, B.IsHermitian ∧ B.PosDef ∧
        F y ≤ Real.log B.det ∧ ∃ g : EuclideanSpace ℝ (Fin n),
          ∀ ε > 0, ∀ᶠ z in 𝓝 y,
            |u z - quadraticAt B y g (u y) z| ≤ ε * ‖z - y‖ ^ 2)
    (hχ : ContDiff ℝ 2 χ) (hχc : HasCompactSupport χ) (hχ0 : ∀ y, 0 ≤ χ y)
    (H : Matrix (Fin n) (Fin n) ℝ)
    (hH : ∀ v : EuclideanSpace ℝ (Fin n),
      ⟪v, Matrix.toEuclideanLin H v⟫ =
        ∫ y, u y * iteratedFDeriv ℝ 2 χ y (fun _ => v))
    (J : Matrix (Fin n) (Fin n) ℝ) (hJ : J.PosDef) :
    (∫ y, (F y + Real.log J.det + n) * χ y) ≤ (J * H).trace

Module navigation

Module: Analysis/Convex/Viscosity.

Definition modules: Analysis/Convex/Alexandrov.

Supporting theorems: forall_posDef_add_log_det_le_trace_iff, integral_mul_le_integral_mul_sum_iteratedFDeriv, expansion_secondDifference.

Previous: convolution_hessian_integral · Next: posDef_and_convolution_le_log_det_hessianMatrix.

Source excerpt, lines 1254–1269 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_Viscosity

open MeasureTheory Set Metric Filter
open scoped RealInnerProductSpace ENNReal Topology
set_option maxHeartbeats 800000

 lemma FunctionalInequalities.Analysis.trace_integral_bound_readable {n : ℕ}
    {u F χ : EuclideanSpace ℝ (Fin n) → ℝ}
    (hconv : ConvexOn ℝ univ u) (hF : Continuous F)
    (hae : ∀ᵐ y ∂(volume : Measure (EuclideanSpace ℝ (Fin n))),
      ∃ B : Matrix (Fin n) (Fin n) ℝ, B.IsHermitian ∧ B.PosDef ∧
        F y ≤ Real.log B.det ∧ ∃ g : EuclideanSpace ℝ (Fin n),
          ∀ ε > 0, ∀ᶠ z in 𝓝 y,
            |u z - quadraticAt B y g (u y) z| ≤ ε * ‖z - y‖ ^ 2)
    (hχ : ContDiff ℝ 2 χ) (hχc : HasCompactSupport χ) (hχ0 : ∀ y, 0 ≤ χ y)
    (H : Matrix (Fin n) (Fin n) ℝ)
    (hH : ∀ v : EuclideanSpace ℝ (Fin n),
      ⟪v, Matrix.toEuclideanLin H v⟫ =
        ∫ y, u y * iteratedFDeriv ℝ 2 χ y (fun _ => v))
    (J : Matrix (Fin n) (Fin n) ℝ) (hJ : J.PosDef) :
    (∫ y, (F y + Real.log J.det + n) * χ y) ≤ (J * H).trace := by sorry