Vanishing Weighted Noise Sum
ProvedFunctionalInequalities.Probability.Diffusion.weighted_noise_zero_readableThis auxiliary statement concerns a finite family of Brownian integrands. Let be a probability space, let be an -dimensional Brownian motion with Brownian filtration , and let for be jointly measurable, progressively measurable, and of finite squared ENNReal energy on every positive time interval. Let satisfy
for every . Then, for every ,
It records the consequence of pointwise cancellation of the weighted integrands and is reused in the diffusion argument.
Original Lean declaration header
Within namespace FunctionalInequalities.Probability.Diffusion. Shown in its original module context. Proof omitted.
private theorem weighted_noise_zero
(W : BrownianMotion P) (ℱ : Filtration ℝ ‹MeasurableSpace Ω›)
(hW : IsBrownianFiltration W ℱ)
(H : Fin N → Ω → ℝ → ℝ)
(hm : ∀ p, Measurable (Function.uncurry (H p)))
(hp : ∀ p, Probability.ProgressivelyMeasurable ℱ (H p))
(hq : ∀ p (T : ℝ), 0 < T →
∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T, (‖H p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
(c : Fin N → ℝ) (hz : ∀ ω s, ∑ p, c p * H p ω s = 0)
{T : ℝ} (hT : 0 < T) :
∀ᵐ ω ∂P, ∑ p, c p * stochasticIntegralBrownian W ℱ hW
(H p) (hm p) (hp p) (hq p) T ω = 0
Module navigation
Module: Probability/Diffusion/Dynkin.
Definition modules: LevyStochCalc/Brownian/ItoL2CompletionMaster, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Construction, LevyStochCalc/Probability/Progressive.
Supporting theorems: exists_stochasticIntegralBrownian_finsetSum, lintegral_sq_bounded_mul_lt_top, stochasticIntegralBrownian_ae_zero, stochasticIntegralBrownian_const_mul.
Previous: IsDiffusion.dynkin · Next: IsDiffusion.ae_linear_eq_integral.
Source excerpt, lines 273–284 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Diffusion_Dynkin
open MeasureTheory ProbabilityTheory Filter Topology
open scoped NNReal ENNReal
open LevyStochCalc LevyStochCalc.Brownian LevyStochCalc.Brownian.Multidim
LevyStochCalc.Brownian.Ito
variable {Ω : Type*} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P] {N d : ℕ}
theorem FunctionalInequalities.Probability.Diffusion.weighted_noise_zero_readable
(W : BrownianMotion P) (ℱ : Filtration ℝ ‹MeasurableSpace Ω›)
(hW : IsBrownianFiltration W ℱ)
(H : Fin N → Ω → ℝ → ℝ)
(hm : ∀ p, Measurable (Function.uncurry (H p)))
(hp : ∀ p, Probability.ProgressivelyMeasurable ℱ (H p))
(hq : ∀ p (T : ℝ), 0 < T →
∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T, (‖H p ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
(c : Fin N → ℝ) (hz : ∀ ω s, ∑ p, c p * H p ω s = 0)
{T : ℝ} (hT : 0 < T) :
∀ᵐ ω ∂P, ∑ p, c p * stochasticIntegralBrownian W ℱ hW
(H p) (hm p) (hp p) (hq p) T ω = 0 := by sorry