OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousDuhamel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.homogeneousDuhamel line 15
2. theorem OAI.DefocusingNLS.continuousOn_homogeneousDuhamelIntegrand line 20
3. theorem OAI.DefocusingNLS.homogeneousDuhamel_norm_le line 28
4. theorem OAI.DefocusingNLS.homogeneousDuhamel_sub line 43
5. theorem OAI.DefocusingNLS.homogeneousDuhamel_norm_le_mul line 57
6. theorem OAI.DefocusingNLS.homogeneousDuhamel_eq_unitIntegral line 78

   Source documentation

   Unit-interval rescaling keeps continuity valid for positive and negative time.

   theorem homogeneousDuhamel_eq_unitIntegral (a b k : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k)
       (t : ℝ) (r : ℝ → HomogeneousY a k) :
       homogeneousDuhamel a b k ha ha1 hk t r =
         t • ∫ u in Icc (0 : ℝ) 1,
           homogeneousFreeOperator a b k (t - t * u) ha ha1 hk (r (t * u)) := by
   …

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

7. theorem OAI.DefocusingNLS.continuous_homogeneousDuhamel line 90