OAI/MathematicalPhysics/DefocusingNLS/Profile/SlowUniformGrowth.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DefocusingNLS.norm_cpow_uniform_lower_bound line 11
2. def OAI.DefocusingNLS.slowParameterMajorant line 44
3. theorem OAI.DefocusingNLS.integrable_slowParameterMajorant line 48
4. theorem OAI.DefocusingNLS.regularizedSlowKernel_uniform_spatial_bound line 56
5. theorem OAI.DefocusingNLS.exists_regularizedSlowSolution_uniform_bound line 71

   Source documentation

   Bounded parameters and a spatial distance from zero give one polynomial bound valid on the whole closed right half-plane.

   theorem exists_regularizedSlowSolution_uniform_bound (m : ℕ) (a b M δ A G : ℝ)
       (ha : -1 < a) (hab : a ≤ b) (hM : 0 ≤ M) (hδ : 0 < δ)
       (hA : 0 ≤ A) (hG : 0 ≤ G) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ q x : ℂ,
         a ≤ q.re → q.re ≤ b → ‖(m : ℂ) - 1 - q‖ ≤ M → ‖q‖ ≤ A →
         ‖(Complex.Gamma q)⁻¹‖ ≤ G → 0 ≤ x.re → δ ≤ ‖x‖ →
           ‖regularizedSlowSolution q m x‖ ≤ C * (1 + ‖x‖) ^ A := by
   …

   Mentions: OAI.DefocusingNLS.regularizedSlowSolution