OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedTopAlternate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The common-type assigned top families have exactly the original physical bands, including original selector coefficients and top masks.

  1. def OAI.LipschitzHilbert.PacketLatticeData.assignedTopAlternate line 19
  2. theorem OAI.LipschitzHilbert.PacketLatticeData.assignedTopAlternate_bound line 25
  3. theorem OAI.LipschitzHilbert.PacketLatticeData.sum_assignedTopPackets_filter line 32