OAI/Analysis/RieszRectifiability/Packing/LatticeMassPacking.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Mass bounds for lattice descendants

Each descendant cell is contained in a ball with controlled radius. Global upper growth therefore bounds its mass by a constant times the corresponding power of its radius, both in extended and real-valued form.

  1. theorem OAI.RieszRectifiability.SupportCellDescendant.measure_upper line 21
  2. theorem OAI.RieszRectifiability.SupportCellDescendant.real_measure_upper line 32
  3. theorem OAI.RieszRectifiability.cleanSupportCell_real_measure_bounds line 42
  4. def OAI.RieszRectifiability.latticeMassPackingConstant line 61
  5. theorem OAI.RieszRectifiability.latticeMassPackingConstant_pos line 64
  6. theorem OAI.RieszRectifiability.cell_mass_packing_of_radius_packing line 69