OAI/Analysis/LipschitzHilbert/Estimates/VariationSum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Summing localized packet variations with summable box weights.

  1. def OAI.LipschitzHilbert.cubicVariation line 15
  2. theorem OAI.LipschitzHilbert.cubicVariation_nonneg line 18
  3. theorem OAI.LipschitzHilbert.cubicVariation_sq line 21
  4. theorem OAI.LipschitzHilbert.cubicVariation_finset_sum line 27
  5. theorem OAI.LipschitzHilbert.weighted_cubicVariation_sum line 38
  6. theorem OAI.LipschitzHilbert.lintegral_weighted_cubicVariation_sum line 49
  7. theorem OAI.LipschitzHilbert.lintegral_cubicVariation_sum_of_weighted_energy line 87