FiniteMeasureLepingle.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Normalize a finite line cell, apply the published probability-space inequality, then restore its unnormalized measure without loss.

theorem OAI.LipschitzHilbert.martingale_smul_measure line 15

theorem OAI.LipschitzHilbert.lepingle_complex_finite_measure line 30

Source documentation

The scalar probability-space theorem gives the same constant on every finite measure. This is the normalization used on coarsest line cells.

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

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