OAI/Analysis/LipschitzHilbert/Geometry/DyadicProjectionPacking.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite collections of the actual dyadic projection cell energies satisfy the Carleson packing condition.

  1. theorem OAI.LipschitzHilbert.DyadicLineGrid.cell_level_le_of_subset line 13
  2. theorem OAI.LipschitzHilbert.DyadicLineGrid.sum_cell_integral_le line 21
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadic_projection_carleson_packing line 42