OAI/Analysis/LipschitzHilbert/Estimates/LocalizedSelectorDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The separated selector has a derivative bound uniform in the Fourier parameter. The fixed polynomial weight absorbs its linear growth.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.selectorCharacter_hasDerivAt line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.weightedSelector_hasDerivAt line 23
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolWeight_le_one line 33
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.weightedSelector_norm_le line 36
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.weightedSelector_deriv_bound line 43
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedSelector_deriv_bound line 59