RadialLimitFreeEquation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The C¹ limit solves the free amplitude equation wherever it stays strictly below one.

theorem OAI.DefocusingNLS.radial_inner_limit_free_equation_on line 14

theorem OAI.DefocusingNLS.radial_inner_limit_free_equation line 88

Source documentation

No pressure remains at any interior point of the limiting nonunit region.

theorem radial_inner_limit_free_equation (R : ℝ) (P : ℕ → RadialInnerData)
    (hR : ∀ n, (P n).R=R) (H : ℕ → ℝ → ℝ)
    (hH : ∀ n, RadialInnerOutputSpec (P n).p R (P n).lo (P n).c (P n).b (H n) (H n))
    (hp : Tendsto (fun n => (P n).p) atTop atTop)
    (c b : ℝ) (hc : c ∈ Icc (599/100 : ℝ) 6)
    (hcT : Tendsto (fun n => (P n).c) atTop (𝓝 c))
    (hbT : Tendsto (fun n => (P n).b) atTop (𝓝 b))
    (A D : ℝ → ℝ) (hA : Continuous A) (hD : Continuous D)
    (hAI : ∀ r ∈ Icc 0 R, A r ∈ Icc (999/1000 : ℝ) 1)
    (hTA : TendstoUniformlyOn H A atTop (Icc 0 R))
    (hTD : TendstoUniformlyOn (fun n => deriv (H n)) D atTop (Icc 0 R)) :
    ∀ r ∈ Ioo 0 R, A r < 1 → HasDerivAt A (D r) r ∧ HasDerivAt D
…

Mentions: OAI.DefocusingNLS.RadialInnerData, OAI.DefocusingNLS.RadialInnerOutputSpec