OAI/Analysis/LipschitzHilbert/Fourier/LineSamplingEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual one-dimensional composition operators with uniform L2 bounds from the inverse Lipschitz estimate.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.line_map_le_two line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.line_memLp_comp line 21
  3. def OAI.LipschitzHilbert.PacketRepresentation.lineCompositionToL2 line 34
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.lineCompositionToL2_bound line 41
  5. def OAI.LipschitzHilbert.PacketRepresentation.lineCompositionL2 line 53
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.lineCompositionL2_onSchwartz line 57
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.lineCompositionL2_bound line 64