OAI/Analysis/LipschitzHilbert/Estimates/TopDyadicDomination.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Dyadic dilation domination for the actual decaying top weights. The base dilation may be larger than the weight radius, as required when the popular-rectangle argument first clips to the localization strip.

  1. def OAI.LipschitzHilbert.SlopeBox.radialDilation line 18
  2. theorem OAI.LipschitzHilbert.SlopeBox.measurableSet_radialDilation line 20
  3. theorem OAI.LipschitzHilbert.SlopeBox.exists_dyadic_weight_bound line 26
  4. theorem OAI.LipschitzHilbert.SlopeBox.weight_le_dyadic_sum line 74