OAI/Analysis/LipschitzHilbert/Packets/SourceBoundaryPacketRegroup.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-packet regrouping for the expected boundary error. The only prefix bound is on the original packet values.

  1. theorem OAI.LipschitzHilbert.packet_stopping_prefix_bound line 17
  2. theorem OAI.LipschitzHilbert.sum_weighted_stopping_fibers line 35
  3. theorem OAI.LipschitzHilbert.AngularGrid.source_boundary_expected_finite_packet_error line 54