OAI/Probability/SLE/Mass/MassCompensatorVariance.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Orthogonality and variance bounds for the discrete potential compensator used in the prescribed moment coefficients.

  1. lemma OAI.SLEExactGauge.centered_mass_increment_condExp line 23
  2. lemma OAI.SLEExactGauge.integral_mul_centered_mass_increment line 31
  3. lemma OAI.SLEExactGauge.centered_mass_increment_variance_le line 48
  4. lemma OAI.SLEExactGauge.martingale_square_submartingale line 62
  5. lemma OAI.SLEExactGauge.martingale_square_maximal_ineq line 78
  6. def OAI.SLEExactGauge.centeredMassPartialSum line 90
  7. lemma OAI.SLEExactGauge.centeredMassPartialSum_memLp line 94
  8. lemma OAI.SLEExactGauge.centeredMassPartialSum_stronglyMeasurable line 100
  9. lemma OAI.SLEExactGauge.centeredMassPartialSum_variance line 110
  10. lemma OAI.SLEExactGauge.centeredMassPartialSum_variance_le line 138
  11. lemma OAI.SLEExactGauge.centeredMassPartialSum_martingale line 148
  12. theorem OAI.SLEExactGauge.centeredMassPartialSum_maximal_error line 176

    Source documentation

    A maximal estimate valid at every selected grid index, without requiring that the selected index itself be a stopping time.

    theorem centeredMassPartialSum_maximal_error
    (ℱ : Filtration ℕ mΩ) (D : ℕ → Ω → ℝ)
    (hD : ∀ i, MemLp (D i) 2 P)
    (hDm : ∀ i, StronglyMeasurable[ℱ (i+1)] (D i)) (ε : ℝ≥0) (N : ℕ) :
    (ε:ℝ≥0∞)*P {ω | (ε:ℝ) ≤ (Finset.range (N+1)).sup'
      Finset.nonempty_range_add_one (fun j => centeredMassPartialSum P ℱ D j ω^2)} ≤
        ENNReal.ofReal (∫ ω, ∑ i ∈ Finset.range N, D i ω^2 ∂P) := by
…

    Mentions: OAI.SLEExactGauge.centeredMassPartialSum