OAI/Analysis/LipschitzHilbert/Estimates/VariationDifference.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Perturbing finite variation by a short-scale sequence.

  1. theorem OAI.LipschitzHilbert.cubicVariation_neg line 12
  2. theorem OAI.LipschitzHilbert.cubicVariation_add_le line 18
  3. theorem OAI.LipschitzHilbert.abs_cubicVariation_sub_le line 22
  4. theorem OAI.LipschitzHilbert.abs_cubicVariation_add_sub_le line 34