OAI/Analysis/LipschitzHilbert/Trees/SourceLatticeScaleEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The fixed-length energy estimate for the original physical source packets. The profile and lattice assumptions already present in the source family discharge every envelope and overlap hypothesis.

  1. theorem OAI.LipschitzHilbert.physicalPlanarPacket_profile_envelope line 15
  2. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalPacket_lattice_envelope line 34
  3. theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalPacket_scale_energy line 57