OAI/MathematicalPhysics/DefocusingNLS/Linear/ExpandingWeightedDuhamel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exponentially weighted inhomogeneous estimates

The Bielecki weight gives a contraction on any finite time slab. The constant depends on the reaction bound, while the starting radius drops out.

  1. theorem OAI.DefocusingNLS.integral_exp_mul_Icc line 16
  2. theorem OAI.DefocusingNLS.expandingDuhamel_weighted_norm_le line 23

    Source documentation

    A forcing bounded by C exp(η t) has weighted response at most C/η.

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

    Mentions: OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.expandingDuhamel