ForwardConeMonotonicity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Positive forward cone growth to the right of the counting region

theorem OAI.DefocusingNLS.normalizedForwardJet_cone_monotone line 9
theorem OAI.DefocusingNLS.normalizedForwardJet_first_strict line 24

theorem OAI.DefocusingNLS.normalizedForwardJet_sum_cone_pos line 46

Source documentation

Opposite initial cross terms cancel. Strict growth in one channel covers initial vectors whose first coordinate vanishes.

theorem normalizedForwardJet_sum_cone_pos (M : ℝ) (s q₁ q₂ : ℂ)
    (w : Fin 2 → ℂ) (N : ℕ) (hM : 0 < M) (hs : s.re = 0) (hs0 : s ≠ 0)
    (hq₁ : M / 2 < q₁.re) (hq₂ : M / 2 < q₂.re)
    (hd₁ : ∀ n : ℕ, q₁ + n - (M : ℂ) ≠ 0)
    (hd₂ : ∀ n : ℕ, q₂ + n - (M : ℂ) ≠ 0) (hN : 1 ≤ N) (hw : w ≠ 0) :
    0 < coneForm M s (normalizedForwardJet M s q₁ w N 0)
        (normalizedForwardJet M s q₁ w N 1) +
      coneForm M (-s) (normalizedForwardJet M (-s) q₂ w N 0)
        (normalizedForwardJet M (-s) q₂ w N 1) := by
…

Mentions: OAI.DefocusingNLS.coneForm, OAI.DefocusingNLS.normalizedForwardJet