OAI/Analysis/LipschitzHilbert/Phase/PacketAngularPartition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact reconstruction after the three-grid split. The selector for each piece agrees with the original one on every retained packet.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.sum_angularPackets line 15
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.crossPacketValue_congr_selector line 26
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.crossPacketValue_angularSelector line 36
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.sum_crossPacketValue_angularPartition line 49