OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedSelectorGoodSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One fixed testing subset for the original selector coefficients. The mask exponent is chosen before the larger counting dilation. Actual concentration, smooth-count cutoff and mask removal all hold on this set.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.source_assigned_selector_mask_good_set line 17