A Time with Controlled Weighted Cumulant Energy

This formalizes an interval-averaging component related to the cumulant bounds cited as Theorem 4.1, p. 18, of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $\mu$ be isotropic with compact support, let $p_t$ be an IsEldanCutoff process with cutoff $\gamma$, and fix $d\in\mathbb N$ and $u\in\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))$. Assume:

1. $C\geq 0$.
2. For every parameter $q=(c,Q)$ with $Q$ self-adjoint and positive semidefinite, the cumulant energy $E_d(q)$ is at most $C$.
3. The map $q\mapsto E_d(q)$ is continuous.
4. $T_0>0$.

Then there is $t\in[T_0,2T_0]$ such that

$$\int_\Omega \gamma(p_t(\omega))^2 E_d(p_t(\omega))\,dP(\omega) \leq \frac{I_d(2T_0)}{T_0},$$

where $I_d(2T_0)$ is the weightedEnergyIntegral up to time $2T_0$.

This provides a finite-horizon replacement for selecting a subsequence with horizon tending to infinity.

Formalization Note. The cumulant energy is evaluated using compactPosterior; the displayed quantities are real-valued integrals.

Original Lean declaration header

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

theorem IsEldanCutoff.exists_weighted_energy_le (hiso : KLS.Isotropic μ) {γ : Param n → ℝ} (hγ : IsCutoff γ)
    (h : IsEldanCutoff μ hc W ℱ hW γ p) (d : ℕ) (u : EuclideanSpace ℝ (Fin n))
    {C : ℝ} (hC0 : 0 ≤ C)
    (hC : ∀ q : Param n, IsSelfAdjoint q.2 → (∀ x, 0 ≤ ⟪q.2 x, x⟫) →
      cumulantEnergy (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) d u ≤ C)
    (hcont : Continuous fun q : Param n =>
      cumulantEnergy (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) d u)
    {T₀ : ℝ} (hT₀ : 0 < T₀) :
    ∃ t ∈ Set.Icc T₀ (2 * T₀),
      (∫ w, γ (p t w) ^ 2 *
        cumulantEnergy (compactPosterior μ hc (p t w).1 (p t w).2 : Measure (EuclideanSpace ℝ (Fin n))) d u ∂P) ≤
        weightedEnergyIntegral μ hc P γ p d u (2 * T₀) / T₀

Module navigation

Module: KLS/BKL/Localization/CutoffEnergy/Boundary.

Definition modules: KLS/BKL/CumulantEnergy/Basic, KLS/BKL/Localization/Process/Basic, KLS/BKL/Localization/Coefficients, LevyStochCalc/Brownian/Filtered, KLS/Isotropic, LevyStochCalc/Brownian/Multidim, Probability/Posterior/CompactDomain, KLS/BKL/Localization/CutoffEnergy/Basic.

Supporting theorems: IsEldanCutoff.ae_Q_posSemidef, IsEldanCutoff.continuous, IsEldanCutoff.integrable_integral_of_ae_bound, exists_le_setIntegral_div.

Previous: IsEldanCutoff.integral_energy_le_weighted_add.

Source excerpt, lines 225–236 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_CutoffEnergy_Boundary

open MeasureTheory ProbabilityTheory Filter Topology
open scoped NNReal ENNReal RealInnerProductSpace
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Analysis.BakryEmery FunctionalInequalities.Probability.Diffusion
variable {n : ℕ} {μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n))}
  {hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support}
  {Ω : Type*} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P n} {ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›}
  {hW : ∀ k, LevyStochCalc.Brownian.IsBrownianFiltration (W.W k) ℱ} {p : ℝ → Ω → FunctionalInequalities.KLS.BKL.Localization.Param n}

theorem FunctionalInequalities.KLS.BKL.Localization.IsEldanCutoff.exists_weighted_energy_le_readable (hiso : KLS.Isotropic μ) {γ : Param n → ℝ} (hγ : IsCutoff γ)
    (h : IsEldanCutoff μ hc W ℱ hW γ p) (d : ℕ) (u : EuclideanSpace ℝ (Fin n))
    {C : ℝ} (hC0 : 0 ≤ C)
    (hC : ∀ q : Param n, IsSelfAdjoint q.2 → (∀ x, 0 ≤ ⟪q.2 x, x⟫) →
      cumulantEnergy (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) d u ≤ C)
    (hcont : Continuous fun q : Param n =>
      cumulantEnergy (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) d u)
    {T₀ : ℝ} (hT₀ : 0 < T₀) :
    ∃ t ∈ Set.Icc T₀ (2 * T₀),
      (∫ w, γ (p t w) ^ 2 *
        cumulantEnergy (compactPosterior μ hc (p t w).1 (p t w).2 : Measure (EuclideanSpace ℝ (Fin n))) d u ∂P) ≤
        weightedEnergyIntegral μ hc P γ p d u (2 * T₀) / T₀ := by sorry