OAI/Analysis/LipschitzHilbert/Trees/UnaryRunVariation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One common residual variation controls segments from every unary run.

  1. theorem OAI.LipschitzHilbert.unaryRunSegment_intervals_disjoint line 18
  2. theorem OAI.LipschitzHilbert.unary_runs_oscillation_cube_sum line 39

    Source documentation

    The actual block-to-angular-level map preserves disjointness. Hence all unary segments, including different runs, use a single variation bound.

    theorem unary_runs_oscillation_cube_sum {E : Type*} [NormedAddCommGroup E]
    (F : ℕ → E) (level : ℕ → ℕ) (hlevel : StrictMono level) (N : ℕ)
    (hend : level finish ≤ N) :
    (∑ i : UnaryRunSegment R P,
      intervalOscillation F N (level i.2.val.1) (level i.2.val.2) ^ 3) ≤
      finiteCubicVariation (fun k => F (min k N)) (2 * N) := by
…

    Mentions: OAI.LipschitzHilbert.UnaryRunSegment, OAI.LipschitzHilbert.intervalOscillation, OAI.LipschitzHilbert.finiteCubicVariation