OAI/Analysis/RieszRectifiability/Packing/RieszOscillationPacking.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Packing for Riesz oscillations

The packing constant combines finitely many coarse levels with the small-scale Riesz packing estimate. Its positivity yields a packing bound whose constant is chosen uniformly before the measure.

  1. def OAI.RieszRectifiability.rieszOscillationPackingConstant line 22
  2. theorem OAI.RieszRectifiability.rieszOscillationPackingConstant_pos line 27
  3. theorem OAI.RieszRectifiability.DyadicOscillationTests.riesz_oscillation_packing line 33
  4. theorem OAI.RieszRectifiability.exists_uniform_riesz_oscillation_packing_constant line 76