OAI/Analysis/LipschitzHilbert/Packets/PacketDataActualReferenceArea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal parent-square and continuing-path reference events have one common weighted bad-mass and area bound. Only original physical packet spectra, selectors, and assigned-top geometry enter the hypotheses.

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