OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousFreeContinuity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.schwartz_polynomial_bound line 15
2. theorem OAI.DefocusingNLS.schwartz_dilation_polynomial_bound line 26
3. theorem OAI.DefocusingNLS.free_difference_polynomial_bound line 40
4. theorem OAI.DefocusingNLS.polynomial_bound_square line 61
5. theorem OAI.DefocusingNLS.continuous_homogeneousFreeFourier_coordinate line 78
6. theorem OAI.DefocusingNLS.tendsto_free_Schwartz_at_zero line 91
7. theorem OAI.DefocusingNLS.continuous_homogeneousFreeBound line 143
8. theorem OAI.DefocusingNLS.tendsto_homogeneousFreeOperator_at_zero line 148

   Source documentation

   Strong continuity at zero follows from the dense Schwartz core and a local uniform bound.

   theorem tendsto_homogeneousFreeOperator_at_zero (a b k : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (f : HomogeneousY a k) :
       Tendsto (fun s : ℝ => homogeneousFreeOperator a b k s ha ha1 hk f) (𝓝 0) (𝓝 f) := by
   …

   Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousFreeOperator

9. theorem OAI.DefocusingNLS.continuous_homogeneousFreeOperator line 180

   Source documentation

   The exact whole-space free group is strongly continuous at every real time.

   theorem continuous_homogeneousFreeOperator (a b k : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (f : HomogeneousY a k) :
       Continuous (fun s : ℝ => homogeneousFreeOperator a b k s ha ha1 hk f) := by
   …

   Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousFreeOperator