MainTheorems.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Stable defocusing Schrödinger blowup

Theorem 1.1 and Corollary 1.2 of OpenAI, Stable self-similar blowup for a supercritical defocusing Schrödinger equation on the torus (September 2026).

theorem OAI.DefocusingNLS.stable_blowup line 20
Source documentation
Theorem 1.1: arbitrarily large odd powers admit a nonempty open family of classical solutions with finite-time self-similar blowup on the twelve-torus.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:265 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.stable_blowup@path.
```
theorem stable_blowup (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 :=
…
```
Mentions: OAI.DefocusingNLS.FourierL2

theorem OAI.DefocusingNLS.gaussian_blowup line 30

Source documentation

Corollary 1.2: for every permitted Gaussian Fourier decay exponent, the same open blowup family has positive Gaussian probability.

Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:275 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.gaussian_blowup@path.

theorem gaussian_blowup (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 :=
…

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

theorem OAI.DefocusingNLS.gaussian_not_almost_sure_global line 45
Source documentation
In particular, Gaussian data are not almost surely globally continuable.
Distinct definitions of this name: ComparatorChallenges/DefocusingNLS.lean:290 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.gaussian_not_almost_sure_global@path.
```
theorem gaussian_not_almost_sure_global (p₀ : ℕ) :
    ∃ p k : ℕ, p₀ ≤ p ∧ Odd p ∧ 3 ≤ p ∧ ∃ hk : 8 < (k : ℝ),
      ∀ α : ℝ, (k : ℝ) + 6 < α →
        ¬ ∀ᵐ f ∂weightedGaussianLaw k α,
          maximalSobolevInteractionDomain k (by linarith) ((p - 1) / 2) f = univ :=
…
```
Mentions: OAI.DefocusingNLS.maximalSobolevInteractionDomain