OAI/Analysis/LipschitzHilbert/Fourier/DyadicSmoothCutoff.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A genuine binary low-pass difference for the dyadic commutator proof, with its scale-independent Fourier square bound.

  1. def OAI.LipschitzHilbert.PacketRepresentation.dyadicDifference line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicDifference_apply line 14
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicDifference_small line 20
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicDifference_large line 24
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicDifference_norm line 29
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicDifference_separated line 33
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicDifference_nonzero_count line 51
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicDifference_square_sum line 74
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicDifference_inverse_square_sum line 99