OAI/Analysis/LipschitzHilbert/Fourier/DyadicResolutionSymbol.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact telescoping and strong pointwise resolution for the binary low-pass differences used in the commutator decomposition.

  1. def OAI.LipschitzHilbert.PacketRepresentation.dyadicResolutionScale line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicResolutionScale_pos line 15
  3. def OAI.LipschitzHilbert.PacketRepresentation.dyadicResolutionSymbol line 19
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicDifference_telescope line 22
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicResolutionSymbol_eq line 33
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicResolutionSymbol_norm line 51
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicResolutionSymbol_tendsto line 58