OAI/Analysis/LipschitzHilbert/Packets/PacketDataPacketScaleCount.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Reindex the actual packets at one scale into their original labels and spatial sites, then apply the uniform lattice count.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.filter_card_sum line 17
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.scale_card_eq_labels line 24
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.direction_packets_count line 45