Almost-Everywhere Congruence Of Compensated Poisson Integrals

This is an auxiliary locality theorem for compensated Poisson integration. Let $(\Omega,P)$ be a probability space, let $E$ carry a sigma-finite measure $\nu$, let $N$ be a Poisson random measure with filtration $\mathcal F$, and let $\varphi_1,\varphi_2:\Omega\times\mathbb R\times E\to\mathbb R$ be jointly measurable and marked-progressively measurable. Assume that for every $T>0$ their squared integrals are finite:

If $t>0$ and $\varphi_1(\omega,s,\cdot)=\varphi_2(\omega,s,\cdot)$ for $P$-almost every $\omega$ and volume-almost every $s\in[0,t]$, then

The statement formalizes the time-locality of the compensated-Poisson integral.

Original Lean declaration header

Within namespace LevyStochCalc.Ito.Picard. Shown in its original module context. Proof omitted.

theorem compensatedIntegral_congr_ae {ν : Measure E} [SigmaFinite ν]
    (N : LevyStochCalc.Poisson.PoissonRandomMeasure P ν)
    (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›)
    (hℱN : LevyStochCalc.Poisson.IsPoissonFiltration N ℱ)
    (φ₁ φ₂ : Ω → ℝ → E → ℝ)
    (hm₁ : Measurable fun p : Ω × ℝ × E => φ₁ p.1 p.2.1 p.2.2)
    (hp₁ : Probability.MarkedProgressivelyMeasurable ℱ φ₁)
    (hs₁ : ∀ T : ℝ, 0 < T →
      ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T, ∫⁻ e, (‖φ₁ ω s e‖₊ : ℝ≥0∞) ^ 2 ∂ν ∂volume ∂P < ⊤)
    (hm₂ : Measurable fun p : Ω × ℝ × E => φ₂ p.1 p.2.1 p.2.2)
    (hp₂ : Probability.MarkedProgressivelyMeasurable ℱ φ₂)
    (hs₂ : ∀ T : ℝ, 0 < T →
      ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T, ∫⁻ e, (‖φ₂ ω s e‖₊ : ℝ≥0∞) ^ 2 ∂ν ∂volume ∂P < ⊤)
    {t : ℝ} (ht : 0 < t)
    (h : ∀ᵐ ω ∂P, ∀ᵐ s ∂(volume.restrict (Set.Icc (0 : ℝ) t)), φ₁ ω s = φ₂ ω s) :
    ∀ᵐ ω ∂P,
      LevyStochCalc.Poisson.Compensated.stochasticIntegral N ℱ hℱN φ₁ hm₁ hp₁ hs₁ t ω
        = LevyStochCalc.Poisson.Compensated.stochasticIntegral N ℱ hℱN φ₂ hm₂ hp₂ hs₂ t ω

Module navigation

Module: LevyStochCalc/Ito/PicardLocality.

Definition modules: LevyStochCalc/Poisson/Filtered, LevyStochCalc/Poisson/Compensated, LevyStochCalc/Poisson/RandomMeasure, LevyStochCalc/Probability/Progressive.

Previous: itoIntegral_congr_ae · Next: picardStep_diffusion_congr_ae.

Source excerpt, lines 127–144 · Frozen source 408915f.