OAI/Analysis/LipschitzHilbert/Packets/SourcePacketStoppedBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original stopped packet product has the source's uniform path bound once its two reference residual norms have polynomial control.

  1. theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_packet_stopped_bound line 16