OAI/Analysis/LipschitzHilbert/Estimates/VariationScalar.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact behavior of finite interval-sum variation under a common scalar. This keeps polynomial localization independent of the number of scales.

  1. theorem OAI.LipschitzHilbert.finiteCubicVariation_smul line 13
  2. theorem OAI.LipschitzHilbert.finiteCubicVariation_smul_square line 25
  3. theorem OAI.LipschitzHilbert.ennreal_finiteCubicVariation_smul_square line 35