OAI/Analysis/LipschitzHilbert/Estimates/VariationDisjointExact.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Disjoint intervals fit into a partition of the original finite horizon. Each interval is collapsed to one jump at its right endpoint; the gaps contribute additional nonnegative variation.

  1. def OAI.LipschitzHilbert.intervalCollapse line 13
  2. theorem OAI.LipschitzHilbert.intervalCollapse_mono line 16
  3. def OAI.LipschitzHilbert.disjointCollapse line 25
  4. theorem OAI.LipschitzHilbert.disjointCollapse_mono line 29
  5. theorem OAI.LipschitzHilbert.disjointCollapse_le line 42
  6. theorem OAI.LipschitzHilbert.disjointCollapse_endpoints line 48
  7. theorem OAI.LipschitzHilbert.disjoint_increment_cube_sum_exact line 99

    Source documentation

    No padding or multiplicative loss is needed for disjoint intervals inside the original finite horizon.

    theorem disjoint_increment_cube_sum_exact {ι 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, ‖F (b i)-F (a i)‖^3) ≤ finiteCubicVariation F N := by
…

    Mentions: OAI.LipschitzHilbert.finiteCubicVariation