Dynkin Identity for the Cutoff Eldan Process

This formalizes the Dynkin identity associated with Equation (67), p. 19, of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), at the compact-support cutoff stage.

Let $n\in\mathbb N$, let $\mu$ be an isotropic probability measure on $\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin}(n))$ with compact support, and let $P$ be a probability measure on a measurable sample space $\Omega$. Let $W$ be an $n$-dimensional multidimensional Brownian motion whose coordinates are Brownian with respect to a filtration $\mathcal F$. Let $\gamma$ be a cutoff on the parameter space and let $p_t(\omega)$ be an IsEldanCutoff process. Assume:

1. The filtration is decreasing from time $0$ toward nonpositive times: $\mathcal F_0\leq\mathcal F_t$ whenever $t\leq 0$.
2. Every $P$-null measurable set is measurable with respect to $\mathcal F_0$.
3. The cutoff and process satisfy the stated cutoff Eldan process conditions.
4. $F$ is a $C^2$ function on the parameter space, and $T\geq 0$.

Then $F(p_T)$ is $P$-integrable and its expectation satisfies

This is a reusable expectation identity for twice continuously differentiable observables of the cutoff localization process.

Formalization Note. The integrals are Lebesgue integrals over $(0,T]$ and $P$; the generator is the uncut generator, multiplied by the squared cutoff coefficient.

Original Lean declaration header

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

theorem IsEldanCutoff.dynkin (hiso : KLS.Isotropic μ) (hγ : IsCutoff γ)
    (hℱ0 : ∀ t : ℝ, t ≤ 0 → ℱ 0 ≤ ℱ t)
    (hnull : ∀ s : Set Ω, MeasurableSet s → P s = 0 → MeasurableSet[ℱ 0] s)
    (h : IsEldanCutoff μ hc W ℱ hW γ p) {F : Param n → ℝ} (hF : ContDiff ℝ 2 F)
    {T : ℝ} (hT : 0 ≤ T) :
    Integrable (fun ω => F (p T ω)) P ∧
      ∫ ω, F (p T ω) ∂P - F 0 =
        ∫ ω, ∫ s in Set.Ioc (0 : ℝ) T, γ (p s ω) ^ 2 * generator μ hc F (p s ω) ∂volume ∂P

Module navigation

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

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

Supporting theorems: cutoffCoefficients_admissible, IsDiffusion.dynkin_transport.

Previous: IsEldanCutoff.continuous · Next: IsEldanCutoff.ae_inner_Q_eq_integral.

Source excerpt, lines 180–187 · Frozen source 408915f.