OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFreePhysical.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.homogeneousPhysicalAmplitude line 15
2. theorem OAI.DefocusingNLS.homogeneousPhysicalAmplitude_eq line 18
3. theorem OAI.DefocusingNLS.homogeneousPhysicalAmplitude_norm line 26
4. theorem OAI.DefocusingNLS.homogeneousPhysicalCLM_rawSchwartz line 30
5. theorem OAI.DefocusingNLS.inverseRadianFourier_dilation line 39
6. theorem OAI.DefocusingNLS.homogeneousFreePhase_scaled line 50
7. theorem OAI.DefocusingNLS.homogeneousFreeAmplitude_dilation line 63
8. theorem OAI.DefocusingNLS.inverseRadianFourier_homogeneousFree line 78
9. theorem OAI.DefocusingNLS.homogeneousFreeOperator_physical line 105

   Source documentation

   Formula (lin:free-flow) on every element of the actual homogeneous completion.

   theorem homogeneousFreeOperator_physical (a b k s : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (f : HomogeneousY a k) (y : E) :
       homogeneousPhysicalCLM a k ha ha1 hk (homogeneousFreeOperator a b k s ha ha1 hk f) y =
         homogeneousPhysicalAmplitude a b s *
           homogeneousPhysicalCLM a k ha ha1 hk
             (homogeneousSchrodingerOperator a k (1 - Real.exp (-s)) f)
             (Real.exp (-s / 2) • y) := by
   …

   Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousPhysicalCLM, OAI.DefocusingNLS.homogeneousFreeOperator, OAI.DefocusingNLS.homogeneousPhysicalAmplitude, OAI.DefocusingNLS.homogeneousSchrodingerOperator