OAI/Analysis/LipschitzHilbert/Packets/PacketDataActualPacketRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original packet sum is recovered from a reference exception for every common grid translation. Central and averaged boundary budgets follow from the energy, fixed-set, mask, and geometric/concentration hypotheses on the popular collection.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.eventually_actual_packet_recovery line 18