OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousConjugation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.homogeneousSchwartzConjugation line 14
2. theorem OAI.DefocusingNLS.homogeneousSchwartzConjugation_apply line 18
3. theorem OAI.DefocusingNLS.homogeneousSchwartzConjugation_involutive line 21
4. theorem OAI.DefocusingNLS.homogeneousSchwartzConjugation_energy line 27
5. theorem OAI.DefocusingNLS.homogeneousSchwartzConjugation_norm line 35
6. def OAI.DefocusingNLS.homogeneousConjugation line 46
7. theorem OAI.DefocusingNLS.homogeneousConjugation_on_Schwartz line 52
8. theorem OAI.DefocusingNLS.homogeneousConjugation_norm_le line 67
9. theorem OAI.DefocusingNLS.homogeneousConjugation_involutive line 82
10. theorem OAI.DefocusingNLS.homogeneousConjugation_norm line 96
11. theorem OAI.DefocusingNLS.inverseRadianFourier_conjugate_reflect line 103
12. theorem OAI.DefocusingNLS.homogeneousConjugation_physical line 120

    Source documentation

    The real-linear isometry is ordinary pointwise complex conjugation.

    theorem homogeneousConjugation_physical (a k : ℝ)
        (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (f : HomogeneousY a k) (y : E) :
        homogeneousPhysicalCLM a k ha ha1 hk (homogeneousConjugation a k ha ha1 hk f) y =
          conj (homogeneousPhysicalCLM a k ha ha1 hk f y) := by
    …

    Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousPhysicalCLM, OAI.DefocusingNLS.homogeneousConjugation