OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingMultiplication.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DefocusingNLS.expandingFourierCoefficient_add line 11
2. lemma OAI.DefocusingNLS.expandingFourierCoefficient_smul line 16
3. lemma OAI.DefocusingNLS.summable_expandingProductTerms line 22
4. theorem OAI.DefocusingNLS.expandingProduct_comm line 28
5. theorem OAI.DefocusingNLS.expandingProduct_add_left line 39
6. theorem OAI.DefocusingNLS.expandingProduct_smul_left line 51
7. theorem OAI.DefocusingNLS.expandingProduct_add_right line 60
8. theorem OAI.DefocusingNLS.expandingProduct_smul_right line 65
9. def OAI.DefocusingNLS.expandingBilinearProduct line 70

   Source documentation

   The exact Y_L product is continuous bilinear, with norm bounded independently of L.

   noncomputable def expandingBilinearProduct (a k L : ℝ) (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) :
       FourierL2 →L[ℂ] FourierL2 →L[ℂ] FourierL2 :=
   …

   Mentions: OAI.DefocusingNLS.FourierL2

10. theorem OAI.DefocusingNLS.expandingBilinearProduct_apply line 77
11. theorem OAI.DefocusingNLS.expandingTorusFunction_product line 81

    Source documentation

    The uniform algebra product agrees with the product of represented functions.

    theorem expandingTorusFunction_product (a k L : ℝ)
        (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hL : 1 ≤ L) (f g : FourierL2) :
        expandingTorusFunction a k L (expandingProduct a k L ha ha1 hk hL f g) =
          expandingTorusFunction a k L f * expandingTorusFunction a k L g := by
    …

    Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingTorusFunction, OAI.DefocusingNLS.expandingProduct