OAI/Analysis/LipschitzHilbert/Estimates/VariationPerturbation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The square-summable error in the smooth/dyadic comparison controls its entire cubic variation, uniformly in the number of scales.

  1. theorem OAI.LipschitzHilbert.cubic_sum_rpow_le_square_sum line 14
  2. theorem OAI.LipschitzHilbert.monotone_partition_square_sum line 26
  3. theorem OAI.LipschitzHilbert.finiteCubicVariation_le_square_energy line 83
  4. theorem OAI.LipschitzHilbert.finiteCubicVariation_add_rpow line 100
  5. theorem OAI.LipschitzHilbert.finiteCubicVariation_add_square line 139
  6. theorem OAI.LipschitzHilbert.finiteCubicVariation_comparison line 160

    Source documentation

    The manuscript's smooth partial sums are a dyadic martingale plus the square-summable comparison error. No scale-count factor occurs.

    theorem finiteCubicVariation_comparison {E : Type*} [NormedAddCommGroup E]
    (P M : ℕ → E) (N : ℕ) :
    (finiteCubicVariation P N) ^ (2 / 3 : ℝ) ≤
      2 * (finiteCubicVariation M N) ^ (2 / 3 : ℝ) +
        8 * ∑ k : Fin (N + 1), ‖P k - M k‖ ^ 2 := by
…

    Mentions: OAI.LipschitzHilbert.finiteCubicVariation