OAI/Analysis/LipschitzHilbert/Packets/PacketIntervalNeighborhood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A common exceptional set for all actual packet intervals. The regularity and both domination hypotheses are proved by finite synthesis; only the geometric packet bounds and their local budgets remain as data.

  1. theorem OAI.LipschitzHilbert.packet_interval_neighborhood line 16