HilbertVariation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional Hilbert consequence of the published scalar input.

theorem OAI.LipschitzHilbert.measurable_variationCube line 15

theorem OAI.LipschitzHilbert.lepingle_euclidean_bound line 37

Source documentation

No extra Hilbert-valued input is assumed: coordinatewise scalar martingales and finite Minkowski give the same squared Lépingle constant.

theorem lepingle_euclidean_bound (hL : LepingleInput) :
    ∃ C : ℝ≥0, 0 < C ∧
      ∀ (Ω : Type) (m : MeasurableSpace Ω) (μ : Measure Ω),
        IsProbabilityMeasure μ → ∀ (κ : Type) [Fintype κ]
          (ℱ : Filtration ℕ m) (F : ℕ → Ω → EuclideanSpace ℝ κ),
          (∀ k, Martingale (fun n x => F n x k) ℱ μ) →
          (∀ k n, MemLp (fun x => F n x k) 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