OAI/Analysis/LipschitzHilbert/Estimates/VariationIntervals.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Disjoint interval selections, including selections depending on a point, are controlled by one finite cubic variation.

  1. def OAI.LipschitzHilbert.intervalPoint line 14
  2. theorem OAI.LipschitzHilbert.intervalPoint_le line 17
  3. theorem OAI.LipschitzHilbert.intervalPoint_mono line 25
  4. theorem OAI.LipschitzHilbert.ordered_intervals_le_variation line 64

    Source documentation

    Padding with the terminal endpoint embeds all selected intervals into a monotone partition of the stopped sequence. There is no measurability assumption on how the intervals were selected.

    theorem ordered_intervals_le_variation {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, ‖F (b i) - F (a i)‖ ^ 3) ≤
      finiteCubicVariation (fun n => F (min n N)) (2 * N) := by
…

    Mentions: OAI.LipschitzHilbert.finiteCubicVariation