OAI/MathematicalPhysics/DefocusingNLS/Linear/TorusL2Product.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Multiplication of torus L² functions by continuous coefficients

  1. theorem OAI.DefocusingNLS.torusL2Product_memLp line 17
  2. def OAI.DefocusingNLS.torusL2ProductValue line 26
  3. theorem OAI.DefocusingNLS.torusL2ProductValue_ae line 29
  4. theorem OAI.DefocusingNLS.torusL2ProductValue_norm_le line 32
  5. def OAI.DefocusingNLS.torusL2Product line 39
  6. theorem OAI.DefocusingNLS.torusL2Product_ae line 64
  7. theorem OAI.DefocusingNLS.torusL2Product_continuous line 68
  8. theorem OAI.DefocusingNLS.torusL2Product_mFourier line 81