Positive Semidefiniteness of the Q Component

This formalizes the positivity property of the localization parameter in Equation (67), p. 19 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1). Let $μ$ be isotropic with compact support, let $γ$ satisfy the cutoff assumptions, and let $p$ be an IsEldanCutoff process driven by a multidimensional Brownian motion with Brownian filtration.

For $P$-almost every $ω$, every $t≥0$, the operator $Q_t(ω)$ is self-adjoint and positive semidefinite:

The declaration uses IsSelfAdjoint and the quadratic-form inequality directly. It is a structural consequence used to express positivity of the evolving localization covariance correction.

Original Lean declaration header

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

theorem IsEldanCutoff.ae_Q_posSemidef (hiso : KLS.Isotropic μ) (hγ : IsCutoff γ)
    (h : IsEldanCutoff μ hc W ℱ hW γ p) :
    ∀ᵐ ω ∂P, ∀ t : ℝ, 0 ≤ t →
      IsSelfAdjoint (p t ω).2 ∧ ∀ x, 0 ≤ ⟪(p t ω).2 x, x⟫

Module navigation

Module: KLS/BKL/Localization/Process/Basic.

Definition modules: KLS/BKL/Localization/Coefficients, LevyStochCalc/Brownian/Filtered, KLS/Isotropic, LevyStochCalc/Brownian/Multidim.

Supporting theorems: inner_self_pos_of_comp_eq_id, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, IsEldanCutoff.ae_inner_Q_eq_integral.

Previous: IsEldanCutoff.ae_inner_Q_eq_integral.

Source excerpt, lines 429–432 · Frozen source 408915f.