OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorCoefficientNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform coefficient normalization for the original smooth selectors. It uses the physical analyzing packet, with no replacement of its selector by a sharp cutoff and no dependence on the number of coordinates.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMultiplierCoefficient_norm line 18