OAI/Analysis/LipschitzHilbert/Estimates/ComplexVariation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Realification preserves the cubic variation and the terminal L² norm of the complex Hilbert-valued packet sums.

  1. def OAI.LipschitzHilbert.complexRealify line 15
  2. theorem OAI.LipschitzHilbert.complexRealify_sub line 19
  3. theorem OAI.LipschitzHilbert.norm_complexRealify line 24
  4. theorem OAI.LipschitzHilbert.finiteCubicVariation_complexRealify line 33
  5. theorem OAI.LipschitzHilbert.lepingle_complex_bound line 43

    Source documentation

    Apply the scalar published input to real and imaginary coordinates. Realification preserves both norms exactly, so there is no dimension loss.

    theorem lepingle_complex_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).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