OAI/Analysis/LipschitzHilbert/Fourier/VerticalProjectionAlgebra.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Addition and exact absorption of vertical multipliers on Schwartz functions and their continuous L2 realizations.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartzVerticalProjection_add_profile line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalL2Projection_add_profile line 21
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartzVerticalProjection_absorb line 34
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalL2Projection_absorb line 42