OAI/Analysis/LipschitzHilbert/Packets/PacketDataHighDensityEnergyRecovery.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Popular recovery for the actual high-density sum. The energy bound follows from ordinary model estimates. The hypotheses concern explicit packet geometry and a bounded supported input.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.source_high_density_energy_recovery line 15