OAI/Analysis/LipschitzHilbert/Packets/SourcePacketScaleCount.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.SourceLabeledLattice.filter_card_sum line 16
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.scale_card_eq_labels line 23
  3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.direction_packets_count line 44