PerturbedLepingle.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Lépingle plus the actual square-summable smooth/dyadic error.

theorem OAI.LipschitzHilbert.lintegral_finiteCubicVariation_comparison line 16
theorem OAI.LipschitzHilbert.measurable_complex_martingale line 50

theorem OAI.LipschitzHilbert.lepingle_complex_comparison line 68

Source documentation

Only the scalar published input is assumed. The error term is the sum of the actual squared smooth/dyadic differences.

theorem lepingle_complex_comparison (hL : LepingleInput) :
    ∃ C : ℝ≥0, 0 < C ∧
      ∀ (Ω : Type) (m : MeasurableSpace Ω) (μ : Measure Ω),
        IsProbabilityMeasure μ → ∀ (κ : Type) [Fintype κ]
          (ℱ : Filtration ℕ m) (P M : ℕ → Ω → EuclideanSpace ℂ κ),
          (∀ n, Measurable (P n)) →
          (∀ k, Martingale (fun n x => (M n x k).re) ℱ μ) →
          (∀ k, Martingale (fun n x => (M n x k).im) ℱ μ) →
          (∀ k n, MemLp (fun x => (M n x k).re) 2 μ) →
          (∀ k n, MemLp (fun x => (M n x k).im) 2 μ) → ∀ N : ℕ,
            (∫⁻ x, ENNReal.ofReal (finiteCubicVariation (fun n => P n x) N) ^ (2 / 3 : ℝ) ∂μ) ≤
              2 * (C : ℝ≥0∞) ^ 2 * (∫⁻ x, ‖M N x‖ₑ ^ 2 ∂μ) +
…

Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.finiteCubicVariation