OAI/Analysis/LipschitzHilbert/Trees/HierarchyVariation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The full-root logarithmic variation bound for shifted angular blocks.

  1. theorem OAI.LipschitzHilbert.sliding_window_sum_le line 15
  2. theorem OAI.LipschitzHilbert.sum_log_ratios line 42
  3. theorem OAI.LipschitzHilbert.sum_log_ratios_Ico line 51
  4. theorem OAI.LipschitzHilbert.full_root_log_variation line 61