OAI/Analysis/OperatorAlgebra/LpFourierCoefficients.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fourier transform commutes with fixed vector coefficients, relating the scalar inclusion to the vector regular representation.

  1. lemma OAI.WeakPureInfiniteness.fourier_schwartz_postcomp line 18
  2. lemma OAI.WeakPureInfiniteness.compLp_schwartz line 31
  3. lemma OAI.WeakPureInfiniteness.fourier_compLp line 38
  4. lemma OAI.WeakPureInfiniteness.fourierInv_compLp line 51