SlowAsymptoticBound.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A uniform first-order bound for the outgoing slow asymptotic

theorem OAI.DefocusingNLS.one_add_real_div_bounds_large line 12
theorem OAI.DefocusingNLS.hasDerivAt_regularizingBracket_real line 29
theorem OAI.DefocusingNLS.regularizingBracket_uniform_bound line 39
theorem OAI.DefocusingNLS.regularizedSlowKernel_uniform_bound line 71

theorem OAI.DefocusingNLS.regularizedSlowSolution_first_remainder line 111

Source documentation

The first outgoing asymptotic is uniform up to both imaginary rays.

theorem regularizedSlowSolution_first_remainder (q : ℂ) (m : ℕ) (hq : -1 < q.re) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ x : ℂ, 0 ≤ x.re → 1 ≤ ‖x‖ →
      ‖x ^ q * regularizedSlowSolution q m x - 1‖ ≤ C / ‖x‖ := by
…

Mentions: OAI.DefocusingNLS.regularizedSlowSolution

theorem OAI.DefocusingNLS.regularizedSlowSolution_nonzero_at_large_norm line 152
Source documentation
The outgoing solution cannot vanish at any sufficiently large point of the closed right half-plane.
```
theorem regularizedSlowSolution_nonzero_at_large_norm (q : ℂ) (m : ℕ)
    (hq : -1 < q.re) :
    ∃ R : ℝ, 0 < R ∧ ∀ x : ℂ, 0 ≤ x.re → R ≤ ‖x‖ →
      regularizedSlowSolution q m x ≠ 0 := by
…
```
Mentions: OAI.DefocusingNLS.regularizedSlowSolution