MassCompensatorSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The compensator error at a selected grid endpoint. The endpoint may depend on the whole path; the maximal bound does not require it to be a discrete stopping time.

lemma OAI.SLEExactGauge.centeredMassPartialSum_selected_bound line 18

theorem OAI.SLEExactGauge.centeredMassPartialSum_selected_tendstoInMeasure line 46

Source documentation

Vanishing expected quadratic increments imply that the centered compensator vanishes in probability at every bounded selected index.

theorem centeredMassPartialSum_selected_tendstoInMeasure
    (ℱ : ℕ → Filtration ℕ mΩ) (D : ℕ → ℕ → Ω → ℝ)
    (hD : ∀ n i, MemLp (D n i) 2 P)
    (hDm : ∀ n i, StronglyMeasurable[ℱ n (i+1)] (D n i))
    (N : ℕ → ℕ) (J : ℕ → Ω → ℕ) (hJ : ∀ n ω, J n ω ≤ N n)
    (hE : Tendsto (fun n => ∫ ω, ∑ i ∈ Finset.range (N n), D n i ω^2 ∂P)
      atTop (𝓝 0)) :
    TendstoInMeasure P (fun n ω => centeredMassPartialSum P (ℱ n) (D n) (J n ω) ω)
      atTop 0 := by
…

Mentions: OAI.SLEExactGauge.centeredMassPartialSum