Pathwise Integral Formula for the Q Component

This formalizes the $Q$-component identity associated with Equation (67), p. 19 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), partially formalizing the localization posterior and parameter evolution. Let $μ$ be an isotropic probability measure on $\operatorname{EuclideanSpace}(ℝ,Fin\,n)$ with compact support, let $γ$ be an admissible cutoff, and let $p_t=(c_t,Q_t)$ be an IsEldanCutoff process driven by a multidimensional Brownian motion.

For $P$-almost every sample $ω$, every $t≥0$, and all $x,y∈\operatorname{EuclideanSpace}(ℝ,Fin\,n)$,

In the Lean statement the covariance is represented by cov μ hc, its inverse by Ring.inverse, and the parameter space is Param n. The conclusion is almost sure but uniform over all times and vectors, and the integral is a Lebesgue integral over Set.Ioc.

Original Lean declaration header

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

theorem IsEldanCutoff.ae_inner_Q_eq_integral (hiso : KLS.Isotropic μ) (hγ : IsCutoff γ)
    (h : IsEldanCutoff μ hc W ℱ hW γ p) :
    ∀ᵐ ω ∂P, ∀ t : ℝ, 0 ≤ t → ∀ x y : EuclideanSpace ℝ (Fin n),
      ⟪(p t ω).2 x, y⟫ =
        ∫ s in Set.Ioc (0 : ℝ) t, γ (p s ω) ^ 2 * ⟪Ring.inverse (cov μ hc (p s ω)) x, y⟫

Module navigation

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

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

Supporting theorems: Covariance.inner_operator_self_pos_of_affineSupport_eq_top, cutoffCoefficients_admissible, IsDiffusion.ae_linear_eq_integral, contDiff_posteriorCovariance_joint.

Previous: IsEldanCutoff.dynkin · Next: IsEldanCutoff.ae_Q_posSemidef.

Source excerpt, lines 247–251 · Frozen source 408915f.