OAI/Analysis/LipschitzHilbert/Fourier/LineCommutatorCoefficientLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform Lipschitz approximation of the coefficient identifies the limit of the actual smoothed commutators in L2.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.scale_neg_nat_tendsto line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineCommutator_lowpass_tendsto line 20