HomogeneousFastTail.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The fast radial exponent cannot satisfy the top-derivative condition

Only the elementary power comparison is used here. Applying it to an actual slow/fast decomposition still requires the normalized asymptotic formula for that solution; no decomposition is postulated as an input.

theorem OAI.DefocusingNLS.radial_weighted_not_integrable_of_power_lower line 19

Source documentation

Any nonzero tail bounded below by r^beta with beta >= -6 fails the 12-dimensional radial square-integrability condition.

theorem radial_weighted_not_integrable_of_power_lower
    (f : ℝ → ℂ) (R beta c : ℝ) (hc : 0 < c) (hb : -6 ≤ beta)
    (hlower : ∀ᶠ r in atTop, c * r ^ beta ≤ ‖f r‖) :
    ¬ IntegrableOn (fun r => r ^ (11 : ℕ) * ‖f r‖ ^ 2) (Ioi R) := by
…

theorem OAI.DefocusingNLS.radial_weighted_limit_eq_zero line 54

Source documentation

A nonzero normalized limiting amplitude is incompatible with the radial L² condition whenever its power is at least the threshold -6.

theorem radial_weighted_limit_eq_zero
    (f : ℝ → ℂ) (R beta c : ℝ) (hb : -6 ≤ beta) (hc : 0 ≤ c)
    (hf : IntegrableOn (fun r => r ^ (11 : ℕ) * ‖f r‖ ^ 2) (Ioi R))
    (hlim : Tendsto (fun r => ‖f r‖ / r ^ beta) atTop (𝓝 c)) : c = 0 := by
…

theorem OAI.DefocusingNLS.fast_derivative_exponent line 69
Source documentation
The exponent in the manuscript's fast kth derivative is above the radial L² threshold throughout the counting half-plane.
```
theorem fast_derivative_exponent (a reLam : ℝ) (k : ℕ)
    (ha : 0 ≤ a) (hLam : -(1 / 32 : ℝ) ≤ reLam) (hk : 7 ≤ k) :
    -6 < (k : ℝ) - 12 + 2 * (a + reLam) := by
…
```