ConditionalMain.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The paper's main statements conditional on the published rectangle Rouché input

The sole explicit published input is RectangleRouche, the rectangle specialization of the corollary after Ahlfors, Complex Analysis, third edition, Chapter 4, §5.2, Theorem 18, p.153. The conclusions combine the profile, spectral, nonlinear, physical-openness and probabilistic arguments.

theorem OAI.DefocusingNLS.stable_blowup_conditional line 22

Source documentation

Theorem 1.1, with an arbitrary lower bound on the odd power.

theorem stable_blowup_conditional (hRou : RectangleRouche) (p₀ : ℕ) :
    ∃ p k : ℕ, p₀ ≤ p ∧ Odd p ∧ 3 ≤ p ∧ ∃ hk : 8 < (k : ℝ),
      ∃ U : Set FourierL2, U.Nonempty ∧ IsOpen U ∧ ∀ f ∈ U,
        IsClassicalDefocusingFlow k (by linarith) ((p - 1) / 2) f ∧
        HasFiniteTimeSelfSimilarBlowup k (by linarith) ((p - 1) / 2)
          (1 / ((p : ℝ) - 1)) f := by
…

Mentions: OAI.DefocusingNLS.RectangleRouche, OAI.DefocusingNLS.FourierL2

theorem OAI.DefocusingNLS.gaussian_blowup_conditional line 50

Source documentation

Corollary 1.2: the same fixed power and Sobolev order work for every allowed Gaussian decay exponent. The charged event is an actual open measurable set.

theorem gaussian_blowup_conditional (hRou : RectangleRouche) (p₀ : ℕ) :
    ∃ p k : ℕ, p₀ ≤ p ∧ Odd p ∧ 3 ≤ p ∧ ∃ hk : 8 < (k : ℝ),
      ∃ U : Set FourierL2, U.Nonempty ∧ IsOpen U ∧
      (∀ f ∈ U, IsClassicalDefocusingFlow k (by linarith) ((p - 1) / 2) f ∧
        HasFiniteTimeSelfSimilarBlowup k (by linarith) ((p - 1) / 2)
          (1 / ((p : ℝ) - 1)) f) ∧
      ∀ α : ℝ, (k : ℝ) + 6 < α →
        (∀ᵐ g ∂fourierGaussianLaw, Memℓp (weightedGaussianCoefficient k α g) 2) ∧
        (∀ᵐ g ∂fourierGaussianLaw, ∀ n,
          sobolevFourierCoefficient k (weightedGaussianVector k α g) n =
            (1 + ‖n‖ ^ 2) ^ (-α / 2) • g n) ∧
        0 < weightedGaussianLaw k α U := by
…

Mentions: OAI.DefocusingNLS.RectangleRouche, OAI.DefocusingNLS.FourierL2, OAI.DefocusingNLS.fourierGaussianLaw, OAI.DefocusingNLS.sobolevFourierCoefficient, OAI.DefocusingNLS.weightedGaussianVector