DisjointIntervalVariation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Reorder an actual finite family of disjoint residual intervals before applying the common cubic variation bound.

theorem OAI.LipschitzHilbert.disjoint_intervalOscillation_cube_sum line 17

Source documentation

Positive-length disjoint intervals can be sorted by their actual starting indices. Their number is bounded by the finite horizon.

theorem disjoint_intervalOscillation_cube_sum {ι E : Type*} [Fintype ι]
    [NormedAddCommGroup E] (F : ℕ → E) (N : ℕ) (a b : ι → ℕ)
    (hab : ∀ i, a i < b i) (hb : ∀ i, b i ≤ N)
    (hdisjoint : ∀ i j, i ≠ j → b i ≤ a j ∨ b j ≤ a i) :
    (∑ i, intervalOscillation F N (a i) (b i) ^ 3) ≤
      finiteCubicVariation (fun n => F (min n N)) (2 * N) := by
…

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