OAI/Analysis/LipschitzHilbert/Estimates/IntervalOscillation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual maxima of subinterval sums on residual segments.

  1. def OAI.LipschitzHilbert.intervalOscillation line 13
  2. theorem OAI.LipschitzHilbert.intervalOscillation_nonneg line 21
  3. theorem OAI.LipschitzHilbert.exists_intervalOscillation_eq line 30
  4. theorem OAI.LipschitzHilbert.increment_le_intervalOscillation line 45
  5. theorem OAI.LipschitzHilbert.intervalOscillation_cube_sum line 61

    Source documentation

    Choose an actual maximizing subinterval in every disjoint segment, then use one common variation bound for all segments together.

    theorem intervalOscillation_cube_sum {E : Type*} [NormedAddCommGroup E]
    (F : ℕ → E) (N S : ℕ) (a b : Fin S → ℕ) (hS : S ≤ N)
    (hab : ∀ i, a i ≤ b i) (hb : ∀ i, b i ≤ N)
    (horder : ∀ i j, i < j → b i ≤ a j) :
    (∑ 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