OAI/Analysis/LipschitzHilbert/Packets/PacketDataScaleRestrictionSums.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Dropping an initial scale segment is an exact reindexing of finite packet sums. Original coefficients and physical packets are retained.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.dropIndex_injective line 15
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.dropIndex_surjective_tail line 22
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.sum_dropIndex line 29
  4. theorem OAI.LipschitzHilbert.PacketLatticeData.sum_dropScales line 43