MassPotentialCompensator.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A remaining-mass potential determines the predictable mass increments.

theorem OAI.SLEExactGauge.remainingPotential_increment line 17

Source documentation

The difference of the current potential and the one-step averaged future potential is the conditional expectation of the mass increment.

theorem remainingPotential_increment
    (ℱ : Filtration ℕ mΩ) (A V : ℕ → Ω → ℝ) (L : Ω → ℝ)
    (hA : StronglyAdapted ℱ A) (hAI : ∀ i, Integrable (A i) P) (hLI : Integrable L P)
    (hV : ∀ i, V i =ᵐ[P] P[L-A i|ℱ i]) (i : ℕ) :
    V i-P[V (i+1)|ℱ i] =ᵐ[P] P[A (i+1)-A i|ℱ i] := by
…

lemma OAI.SLEExactGauge.predictable_mass_sum_eq line 34

Source documentation

Pathwise telescoping after identifying each predictable increment.

lemma predictable_mass_sum_eq
    (ℱ : Filtration ℕ mΩ) (A : ℕ → Ω → ℝ)
    (q : ℕ → Ω → ℝ)
    (hq : ∀ i, q i =ᵐ[P] P[A (i+1)-A i|ℱ i]) (N : ℕ) :
    (fun ω => ∑ i ∈ Finset.range N, q i ω) =ᵐ[P]
      fun ω => A N ω-A 0 ω-centeredMassPartialSum P ℱ
        (fun i => A (i+1)-A i) N ω := by
…

Mentions: OAI.SLEExactGauge.centeredMassPartialSum