TailCone.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Strict cone for a decaying recurrent tail

Decay of the two tail sums, the Laguerre recurrence, and nontriviality beyond the cutoff give the strict cone inequality in Lemma free:cone.

theorem OAI.DefocusingNLS.hasSum_cone_increments line 19

Source documentation

Summing the nonnegative cone increments recovers the negative initial cone. In particular the infinite sum needs no additional summability input.

theorem hasSum_cone_increments (p a : ℕ → ℝ) (K : ℕ)
    (hlimit : Tendsto p atTop (𝓝 0))
    (hinc : ∀ n, p (n + 1) - p n = a n)
    (hnonneg : ∀ n, K ≤ n → 0 ≤ a n) :
    HasSum (fun n => a (n + K)) (-p K) := by
…

theorem OAI.DefocusingNLS.coneForm_tendsto_zero line 34

Source documentation

Decay of both tail sums makes the cone form tend to zero.

theorem coneForm_tendsto_zero (M : ℝ) (s : ℂ) (B C : ℕ → ℂ)
    (hB : Tendsto B atTop (𝓝 0)) (hC : Tendsto C atTop (𝓝 0)) :
    Tendsto (fun n => coneForm M s (B n) (C n)) atTop (𝓝 0) := by
…

Mentions: OAI.DefocusingNLS.coneForm

theorem OAI.DefocusingNLS.recurrent_tail_cone_negative line 45

Source documentation

A nontrivial decaying tail satisfying the Laguerre recurrence lies in the strict cone once the cutoff is at least three.

theorem recurrent_tail_cone_negative (σ : ℝ) (ℓ K : ℕ)
    (s : ℂ) (t B C g : ℕ → ℂ)
    (hσ : -(1 / 32 : ℝ) ≤ σ) (hK : 3 ≤ K) (hs : s.re = 0)
    (ht : ∀ n, (t n).re = σ + (ℓ : ℝ) / 2 + n)
    (hrec : ∀ n, t n * g n = -((ℓ : ℝ) + 5 : ℂ) * (B n - g n) - s * C n)
    (hBrec : ∀ n, B (n + 1) = B n - g n)
    (hCrec : ∀ n, C (n + 1) = C n - B (n + 1))
    (hB : Tendsto B atTop (𝓝 0)) (hC : Tendsto C atTop (𝓝 0))
    (hnonzero : ∃ n, K ≤ n ∧ g n ≠ 0) :
    coneForm ((ℓ : ℝ) + 5) s (B K) (C K) < 0 := by
…

Mentions: OAI.DefocusingNLS.coneForm