OAI/Analysis/LipschitzHilbert/Packets/PacketDataTopEstimate.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_selected_top_estimate line 13