Linear Functionals Annihilating Noise Follow the Drift

This statement concerns a finite-dimensional diffusion. Let $N,d∈ℕ$, let $W$ be a $d$-dimensional Brownian motion with Brownian filtration $ℱ$, and let $Y_t:Ω→ℝ^N$ be an IsDiffusion with continuous drift $b:ℝ^N→ℝ^N$, diffusion coefficient $σ$, and initial point $x₀$. Assume that $b$ is bounded in norm by some $B∈ℝ$. Let $ℓ:(ℝ^N)→ℝ$ be a continuous linear map satisfying

for every state $x$ and noise coordinate $k$.

Then, $P$-almost surely, for every $t≥0$,

The integral is over Set.Ioc (0 : ℝ) t. This is a pathwise drift identity for linear observables that annihilate every noise direction, and it is used in the localization-process analysis.

Original Lean declaration header

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

set_option maxHeartbeats 1200000 in
theorem IsDiffusion.ae_linear_eq_integral {W : MultidimBrownianMotion P d}
    {ℱ : Filtration ℝ ‹MeasurableSpace Ω›} {hW : ∀ k, IsBrownianFiltration (W.W k) ℱ}
    {b : (Fin N → ℝ) → Fin N → ℝ} {σ : (Fin N → ℝ) → Fin d → Fin N → ℝ} {x₀ : Fin N → ℝ}
    (hbc : Continuous b) {B : ℝ} (hbB : ∀ x, ‖b x‖ ≤ B)
    {Y : ℝ → Ω → Fin N → ℝ} (h : IsDiffusion W ℱ hW b σ x₀ Y)
    (ℓ : (Fin N → ℝ) →L[ℝ] ℝ) (hℓ : ∀ x k, ℓ (σ x k) = 0) :
    ∀ᵐ ω ∂P, ∀ t : ℝ, 0 ≤ t →
      ℓ (Y t ω) = ℓ x₀ + ∫ s in Set.Ioc (0 : ℝ) t, ℓ (b (Y s ω))

Module navigation

Module: Probability/Diffusion/Dynkin.

Definition modules: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, Probability/Diffusion/Setup.

Supporting theorems: version_ae_eq_zero, weighted_noise_zero.

Previous: weighted_noise_zero.

Source excerpt, lines 327–335 · Frozen source 408915f.