OAI/Analysis/LipschitzHilbert/Geometry/SourceSelectedPacketPacking.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded overlap for actual selected packets with slopes close to a fixed longer tree. Both temporal order and spatial lattice counts have been proved; no overlap premise is assumed.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.SizeStoppingRun.selected_packet_box_packing line 22