OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedSelectorJointGoodSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A common fixed set for the actual original selector coefficients, mask removal and the simultaneous direction count at the larger dilation. All numerical choices precede the finite packet and top families.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.source_assigned_selector_joint_good_set line 16