OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialPressureDecay.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.radial_pressure_uniform_decay line 11
2. theorem OAI.DefocusingNLS.radial_pressure_decay_on_compact line 39

   Source documentation

   This is the locally uniform pressure limit required away from the limiting plateau.

   theorem radial_pressure_decay_on_compact (p : ℕ → ℕ)
       (hp : Tendsto p atTop atTop) (H : ℕ → ℝ → ℝ) (A : ℝ → ℝ) (s K : Set ℝ)
       (hH : ∀ n r, r ∈ s → 0 ≤ H n r) (hT : TendstoUniformlyOn H A atTop s)
       (hA : ContinuousOn A s) (hK : IsCompact K) (hKs : K ⊆ s)
       (hK1 : ∀ r ∈ K, A r < 1) :
       TendstoUniformlyOn (fun n r => (H n r)^(p n-1)) (fun _ => 0) atTop K := by
   …