OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousDilation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.homogeneousFourierDilation line 14
2. theorem OAI.DefocusingNLS.homogeneousFourierDilation_apply line 20
3. theorem OAI.DefocusingNLS.homogeneousFourierDilation_energy line 25
4. theorem OAI.DefocusingNLS.homogeneousFourierDilation_norm_le line 52
5. def OAI.DefocusingNLS.homogeneousDilation line 84
6. theorem OAI.DefocusingNLS.homogeneousDilation_on_Schwartz line 91
7. theorem OAI.DefocusingNLS.homogeneousDilation_norm_le line 98
8. theorem OAI.DefocusingNLS.inverseRadianFourier_homogeneousDilation line 104
9. theorem OAI.DefocusingNLS.homogeneousDilation_physical line 123

   Source documentation

   The operator is exactly the physical scaling R^(-2a) f(y/R).

   theorem homogeneousDilation_physical (a k R : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hR : 1 ≤ R)
       (f : HomogeneousY a k) (y : E) :
       homogeneousPhysicalCLM a k ha ha1 hk (homogeneousDilation a k R ha ha1 hk hR f) y =
         (R ^ (-2 * a) : ℝ) * homogeneousPhysicalCLM a k ha ha1 hk f (R⁻¹ • y) := by
   …

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