LepingleIntervals.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Lépingle for disjoint intervals selected separately at each point.

theorem OAI.LipschitzHilbert.martingale_freeze line 17

Source documentation

Freezing a scalar martingale at a deterministic horizon preserves the original filtration and the terminal value.

theorem martingale_freeze {Ω : Type*} [m : MeasurableSpace Ω] {μ : Measure Ω}
    [IsFiniteMeasure μ]
    {ℱ : Filtration ℕ m} {F : ℕ → Ω → ℝ} (hF : Martingale F ℱ μ) (N : ℕ) :
    Martingale (fun n => F (min n N)) ℱ μ := by
…

theorem OAI.LipschitzHilbert.lepingle_ordered_intervals line 37

Source documentation

The intervals may depend arbitrarily on the point. A single uniform published scalar constant controls their Euclidean cubic sum.

theorem lepingle_ordered_intervals (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 S : ℕ) (a b : Ω → Fin S → ℕ), S ≤ N →
          (∀ x i, a x i ≤ b x i) → (∀ x i, b x i ≤ N) →
          (∀ x i j, i < j → b x i ≤ a x j) →
            (∫⁻ x, ENNReal.ofReal (∑ i, ‖F (b x i) x - F (a x i) x‖ ^ 3) ^
              (2 / 3 : ℝ) ∂μ) ≤
…

Mentions: OAI.LipschitzHilbert.LepingleInput