OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousWeightedDuhamel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.homogeneous_integral_exp_Icc line 14
2. theorem OAI.DefocusingNLS.homogeneousDuhamel_weighted_norm_le line 21

   Source documentation

   An exponentially bounded forcing gives the Bielecki contraction estimate.

   theorem homogeneousDuhamel_weighted_norm_le (a b k η t C : ℝ)
       (ha : 0 < a) (ha1 : a < 1) (hk : 8 < k) (hη : 0 < η) (ht : 0 ≤ t) (hC : 0 ≤ C)
       (r : ℝ → HomogeneousY a k) (hbound : ∀ τ ∈ Icc 0 t, ‖r τ‖ ≤ C * Real.exp (η * τ)) :
       Real.exp (-η * t) * ‖homogeneousDuhamel a b k ha ha1 hk t r‖ ≤ C / η := by
   …

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