MassMartingaleUniqueness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of a continuous mass process from its integrable increasing variation and martingale difference. No second moment is imposed on a competing mass construction.

theorem OAI.SLEExactGauge.increasing_mass_martingale_eq_at line 23

Source documentation

A continuous martingale which is the difference of two increasing processes starting at zero vanishes, using only integrability of the two endpoint masses.

theorem increasing_mass_martingale_eq_at
    (hM : Martingale (fun t ω => A t ω-B t ω) ℱ P)
    (hA : ∀ᵐ ω ∂P, Monotone (fun t => A t ω))
    (hB : ∀ᵐ ω ∂P, Monotone (fun t => B t ω))
    (hA0 : A 0 =ᵐ[P] 0) (hB0 : B 0 =ᵐ[P] 0)
    (T : ℝ≥0) (hAI : Integrable (A T) P) (hBI : Integrable (B T) P)
    (hcont : ∀ᵐ ω ∂P, ContinuousOn (fun t => A t ω-B t ω) (Icc 0 T)) :
    A T =ᵐ[P] B T := by
…

theorem OAI.SLEExactGauge.increasing_mass_martingale_indistinguishable line 98

Source documentation

The fixed-time result holds simultaneously at every time by continuity and a countable dense family of deterministic times.

theorem increasing_mass_martingale_indistinguishable
    (hM : Martingale (fun t ω => A t ω-B t ω) ℱ P)
    (hA : ∀ᵐ ω ∂P, Monotone (fun t => A t ω))
    (hB : ∀ᵐ ω ∂P, Monotone (fun t => B t ω))
    (hA0 : A 0 =ᵐ[P] 0) (hB0 : B 0 =ᵐ[P] 0)
    (hAI : ∀ T, Integrable (A T) P) (hBI : ∀ T, Integrable (B T) P)
    (hcont : ∀ᵐ ω ∂P, Continuous (fun t => A t ω-B t ω)) :
    ∀ᵐ ω ∂P, ∀ t, A t ω = B t ω := by
…