FiniteAnnularCarleson.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite annular witness packing

Annular witnesses with bounded lattice depth give Haar mean gaps at one common positive truncation scale. Applying top-ball Haar packing to those gaps bounds the total mass of the selected descendant cells by the original top-cell mass.

theorem OAI.RieszRectifiability.finite_annular_witness_mass_packing line 23