OAI/Analysis/LipschitzHilbert/Packets/PacketDataPacketRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recovery for the literal original packet sum. Integrability of the original, masked, and translated boundary sums follows from their actual Schwartz packets; the hypotheses here are the quantitative local budgets.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.eventually_physical_packet_recovery line 17