OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousSchrodingerMultiplier.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.homogeneousSchrodingerPhase line 15
2. theorem OAI.DefocusingNLS.homogeneousSchrodingerPhase_norm line 18
3. theorem OAI.DefocusingNLS.homogeneousSchrodingerPhase_continuous line 21
4. theorem OAI.DefocusingNLS.homogeneousSchrodingerPhase_temperate line 26
5. theorem OAI.DefocusingNLS.memLp_homogeneousSchrodingerPhase_mul line 31
6. def OAI.DefocusingNLS.homogeneousSchrodingerVector line 40
7. theorem OAI.DefocusingNLS.homogeneousSchrodingerVector_ae line 45
8. theorem OAI.DefocusingNLS.homogeneousSchrodingerVector_norm line 50
9. def OAI.DefocusingNLS.homogeneousSchrodingerLinearMap line 61
10. def OAI.DefocusingNLS.homogeneousSchrodingerOperator line 83
11. theorem OAI.DefocusingNLS.homogeneousSchrodingerOperator_norm line 90
12. theorem OAI.DefocusingNLS.homogeneousSchrodingerOperator_Schwartz line 93
13. theorem OAI.DefocusingNLS.homogeneousSchrodingerOperator_physical line 115

    Source documentation

    The physical representative of the usual free Schrödinger evolution.

    theorem homogeneousSchrodingerOperator_physical (a k t : ℝ)
        (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (f : HomogeneousY a k) (y : E) :
        homogeneousPhysicalCLM a k ha ha1 hk (homogeneousSchrodingerOperator a k t f) y =
          inverseRadianFourier (fun ξ => homogeneousSchrodingerPhase t ξ * f ξ) y := by
    …

    Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousPhysicalCLM, OAI.DefocusingNLS.homogeneousSchrodingerOperator, OAI.DefocusingNLS.inverseRadianFourier, OAI.DefocusingNLS.homogeneousSchrodingerPhase