OAI/Analysis/LipschitzHilbert/Packets/PacketDataSelectedPartial.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The selected reference lattice preserves every scale partial sum, its interval maximum, and its exact coefficient energy.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.selectedReference_partial line 19
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.selectedReference_maximal line 51
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.selectedReference_energy line 61