OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedBoundaryError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The integrated boundary error for the original selected physical packets. Raw assigned-reference concentration supplies the prefix bounds; the top cutoff and every packet cutoff are their actual last eligible levels.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.assigned_boundary_integrated_error line 19