OAI/Analysis/LipschitzHilbert/Estimates/ThresholdSynthesis.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A monotone threshold selects one terminal interval of dyadic scales. Its synthesis is controlled by the actual partial-sum variation.

  1. theorem OAI.LipschitzHilbert.increment_cube_le_finiteCubicVariation line 13
  2. theorem OAI.LipschitzHilbert.increment_le_cubicVariation line 45
  3. theorem OAI.LipschitzHilbert.monotone_threshold_suffix line 56
  4. theorem OAI.LipschitzHilbert.threshold_sum_eq_partial_difference line 79
  5. theorem OAI.LipschitzHilbert.threshold_sum_le_variation line 96