OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedSelectorControlledGoodSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Concentration and mask removal use the auxiliary jet bound belonging only to the smaller dilation. The larger central normalization does not enter the mask exponent choice. All physical coefficients are preserved.

  1. theorem OAI.LipschitzHilbert.PacketLatticeData.source_assigned_selector_mask_good_set_with_jet_control line 15