OAI/Analysis/LipschitzHilbert/Fourier/ProductPVVerticalDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Along every vertical sequence escaping to infinity the actual short principal value tends to zero. Only boundedness of the direction is used.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.bounded_sample_tendsto_cocompact line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.productPV_vertical_decay line 35