OAI/Analysis/LipschitzHilbert/Fourier/SharpBandMeasurableRestricted.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual sharp band logarithmic estimate for bounded measurable L2 tests. The slight strip margin is used only for smooth approximation.

  1. def OAI.LipschitzHilbert.PacketRepresentation.sharpBandL2Pairing line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.support_into_open_strip line 21
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartz_open_strip_zero line 30
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.actual_sharp_band_measurable_restricted_log line 38