OAI/Analysis/LipschitzHilbert/Packets/PacketDataSpatialTree.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The ordinary tree estimate for an actual selected packet set. Local angular multiplicity supplies the row count; empty ambient rows disappear.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.exists_spatial_selected_tree_estimate line 14