OAI/Analysis/RieszRectifiability/Packing/ADCellHaarPairs.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Haar tests on AD-regular lattice cells

Admissible core radii remain admissible at later lattice levels. Global upper growth makes the clean cells finite, while the lower AD estimate gives positive inner-cell mass. These facts yield mean-zero, L²-normalized Haar tests and the exact pairing formula in terms of the inner and outer cell means.

  1. theorem OAI.RieszRectifiability.lattice_core_admissible_at_later_level line 23
  2. theorem OAI.RieszRectifiability.cleanSupportCell_finite_of_growth line 31
  3. theorem OAI.RieszRectifiability.CellHaarPair.cells_finite line 38
  4. theorem OAI.RieszRectifiability.CellHaarPair.inner_real_pos line 45
  5. theorem OAI.RieszRectifiability.CellHaarPair.test_properties line 58