OAI/Analysis/LipschitzHilbert/Fourier/VerticalBinAdjoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Self-adjointness of the real vertical bin cutoffs, first on Schwartz functions and then on the full L2 quotient.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBin_schwartz_adjoint line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinLp_adjoint line 26