ComparatorChallenges/DefocusingNLS.lean

GitHub source file

40 declarations, 4 contain sorry, 0 declared as axioms

1. def OAI.DefocusingNLS.frequencyLattice line 22

   Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevWeights.lean:18 (same declaration text).

2. instance OAI.DefocusingNLS.(instance at line 25) line 25
3. instance OAI.DefocusingNLS.(instance at line 29) line 29
4. def OAI.DefocusingNLS.complexGaussian line 35

   Also declared: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/FiniteGaussian.lean:29 (same declaration text).

5. instance OAI.DefocusingNLS.complexGaussian_isProbabilityMeasure line 39

   Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/FiniteGaussian.lean:33 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.complexGaussian_isProbabilityMeasure@path.

6. def OAI.DefocusingNLS.fourierGaussianLaw line 46

   Also declared: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/GaussianFourier.lean:23 (same declaration text).

7. def OAI.DefocusingNLS.sobolevVariance line 49

   Also declared: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/GaussianFourier.lean:43 (same declaration text).

8. def OAI.DefocusingNLS.weightedGaussianCoefficient line 52

   Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/GaussianFourier.lean:70 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.weightedGaussianCoefficient@path.

9. abbrev OAI.DefocusingNLS.FourierL2 line 58

   Also declared: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/GaussianRealization.lean:22 (same declaration text).

10. instance OAI.DefocusingNLS.(instance at line 60) line 60
11. instance OAI.DefocusingNLS.(instance at line 61) line 61
12. def OAI.DefocusingNLS.weightedGaussianVector line 63

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/GaussianRealization.lean:50 (same declaration text).

13. def OAI.DefocusingNLS.sobolevFourierCoefficient line 67

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/GaussianRealization.lean:74 (same declaration text).

14. def OAI.DefocusingNLS.weightedGaussianLaw line 71

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/GaussianRealization.lean:91 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.weightedGaussianLaw@path.

15. abbrev OAI.DefocusingNLS.SchrodingerTorus line 76

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevTorus.lean:19 (same declaration text).

16. instance OAI.DefocusingNLS.(instance at line 78) line 78
17. def OAI.DefocusingNLS.frequencyCoordinates line 80

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevTorus.lean:24 (same declaration text).

18. def OAI.DefocusingNLS.torusCharacter line 83

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevTorus.lean:28 (same declaration text).

19. def OAI.DefocusingNLS.sobolevTorusTerm line 87

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevTorus.lean:45 (same declaration text).

20. def OAI.DefocusingNLS.sobolevTorusFunction line 91

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevTorus.lean:56 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.sobolevTorusFunction@path.

21. def OAI.DefocusingNLS.sobolevProductWeight line 96

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevProductWeights.lean:10 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.sobolevProductWeight@path.

22. def OAI.DefocusingNLS.sobolevProductCoefficient line 101

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevConvolution.lean:47 (same declaration text).

23. def OAI.DefocusingNLS.sobolevProduct Challenge statement: Stable blowup for the defocusing Schrödinger equation sorry line 105

    L4DEL explanation

    The formalization constructs stable self-similar finite-time blowup for defocusing nonlinear Schrödinger equations on the twelve-dimensional torus. For every prescribed lower bound on the power, it selects an odd power at least that large and a Sobolev index $k>8$ for which a nonempty open set of $H^k$ initial data has the stated classical blowup behavior. The selected quantifier gives arbitrarily large odd powers, rather than every sufficiently large odd power. For each such construction, Gaussian Fourier data with decay exponent $\alpha>k+6$ assign positive probability to the blowup set, and almost-sure global existence fails. The exponent $\alpha$ may be arbitrarily large.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.MathematicalPhysics.DefocusingNLS.MainTheorems as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevConvolution.lean:148 (different declaration text). Qualify references as OAI.DefocusingNLS.sobolevProduct@path.

    noncomputable def sobolevProduct (k : ℝ) (_hk : 6 < k) (f g : FourierL2) : FourierL2 :=
    …

    Mentions: OAI.DefocusingNLS.FourierL2

24. def OAI.DefocusingNLS.fourierConjugate line 111

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevConjugation.lean:12 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.fourierConjugate@path.

25. def OAI.DefocusingNLS.sobolevOddPower Challenge statement: Stable blowup for the defocusing Schrödinger equation line 120

    L4DEL explanation

    The formalization constructs stable self-similar finite-time blowup for defocusing nonlinear Schrödinger equations on the twelve-dimensional torus. For every prescribed lower bound on the power, it selects an odd power at least that large and a Sobolev index $k>8$ for which a nonempty open set of $H^k$ initial data has the stated classical blowup behavior. The selected quantifier gives arbitrarily large odd powers, rather than every sufficiently large odd power. For each such construction, Gaussian Fourier data with decay exponent $\alpha>k+6$ assign positive probability to the blowup set, and almost-sure global existence fails. The exponent $\alpha$ may be arbitrarily large.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.MathematicalPhysics.DefocusingNLS.MainTheorems as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Linear/SobolevNonlinearity.lean:29 (different declaration text). Qualify references as OAI.DefocusingNLS.sobolevOddPower@path.

    noncomputable def sobolevOddPower (k : ℝ) (hk : 6 < k) : ℕ → FourierL2 → FourierL2
      | 0, f => f
      | m + 1, f => sobolevProduct k hk
          (sobolevProduct k hk (sobolevOddPower k hk m f) (fourierConjugate f)) f
    
    run_cmd Lean.modifyEnv fun env => Lean.Meta.auxLemmasExt.setState env {}

    Mentions: OAI.DefocusingNLS.FourierL2

26. def OAI.DefocusingNLS.schrodingerMultiplier line 127

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/SchrodingerFlow.lean:20 (same declaration text).

27. def OAI.DefocusingNLS.schrodingerFlow Challenge statement: Stable blowup for the defocusing Schrödinger equation line 130

    L4DEL explanation

    The formalization constructs stable self-similar finite-time blowup for defocusing nonlinear Schrödinger equations on the twelve-dimensional torus. For every prescribed lower bound on the power, it selects an odd power at least that large and a Sobolev index $k>8$ for which a nonempty open set of $H^k$ initial data has the stated classical blowup behavior. The selected quantifier gives arbitrarily large odd powers, rather than every sufficiently large odd power. For each such construction, Gaussian Fourier data with decay exponent $\alpha>k+6$ assign positive probability to the blowup set, and almost-sure global existence fails. The exponent $\alpha$ may be arbitrarily large.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.MathematicalPhysics.DefocusingNLS.MainTheorems as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Linear/SchrodingerFlow.lean:48 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.schrodingerFlow@path.

    noncomputable def schrodingerFlow (t : ℝ) : FourierL2 →ₗᵢ[ℂ] FourierL2 where
    …

    Mentions: OAI.DefocusingNLS.FourierL2

28. def OAI.DefocusingNLS.fourierContraction line 163

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/SchrodingerGenerator.lean:23 (same declaration text).

29. def OAI.DefocusingNLS.lowerSobolevInclusion line 189

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Linear/SchrodingerGenerator.lean:54 (same declaration text).

30. def OAI.DefocusingNLS.lowerSobolevGenerator line 195

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Linear/SchrodingerGenerator.lean:61 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.lowerSobolevGenerator@path.

31. def OAI.DefocusingNLS.schrodingerInteractionField line 204

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Linear/SchrodingerInteraction.lean:35 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.schrodingerInteractionField@path.

32. structure OAI.DefocusingNLS.SobolevInteractionPatch line 210

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/MaximalSobolevFlow.lean:18 (same declaration text).

33. def OAI.DefocusingNLS.maximalSobolevInteractionDomain line 220

    Also declared: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/MaximalSobolevFlow.lean:34 (same declaration text).

34. def OAI.DefocusingNLS.maximalSobolevInteractionFlow line 223

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/MaximalSobolevFlow.lean:38 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.maximalSobolevInteractionFlow@path.

35. def OAI.DefocusingNLS.maximalSobolevSchrodingerFlow line 232

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/MaximalSobolevEndpoint.lean:74 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.maximalSobolevSchrodingerFlow@path.

36. def OAI.DefocusingNLS.IsClassicalDefocusingFlow line 238

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/ClassicalMaximalFlow.lean:12 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.IsClassicalDefocusingFlow@path.

37. def OAI.DefocusingNLS.HasFiniteTimeSelfSimilarBlowup line 249

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/Nonlinear/PhysicalCutoffBlowup.lean:14 (same statement text; different proof or body). Qualify references as OAI.DefocusingNLS.HasFiniteTimeSelfSimilarBlowup@path.

38. theorem OAI.DefocusingNLS.stable_blowup Challenge statement: Stable blowup for the defocusing Schrödinger equation sorry line 265

    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.

    L4DEL explanation

    The formalization constructs stable self-similar finite-time blowup for defocusing nonlinear Schrödinger equations on the twelve-dimensional torus. For every prescribed lower bound on the power, it selects an odd power at least that large and a Sobolev index $k>8$ for which a nonempty open set of $H^k$ initial data has the stated classical blowup behavior. The selected quantifier gives arbitrarily large odd powers, rather than every sufficiently large odd power. For each such construction, Gaussian Fourier data with decay exponent $\alpha>k+6$ assign positive probability to the blowup set, and almost-sure global existence fails. The exponent $\alpha$ may be arbitrarily large.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.MathematicalPhysics.DefocusingNLS.MainTheorems as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/MainTheorems.lean:20 (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 := by
    …

    Mentions: OAI.DefocusingNLS.FourierL2

39. theorem OAI.DefocusingNLS.gaussian_blowup Challenge statement: Stable blowup for the defocusing Schrödinger equation sorry line 275

    Source documentation

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

    L4DEL explanation

    The formalization constructs stable self-similar finite-time blowup for defocusing nonlinear Schrödinger equations on the twelve-dimensional torus. For every prescribed lower bound on the power, it selects an odd power at least that large and a Sobolev index $k>8$ for which a nonempty open set of $H^k$ initial data has the stated classical blowup behavior. The selected quantifier gives arbitrarily large odd powers, rather than every sufficiently large odd power. For each such construction, Gaussian Fourier data with decay exponent $\alpha>k+6$ assign positive probability to the blowup set, and almost-sure global existence fails. The exponent $\alpha$ may be arbitrarily large.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.MathematicalPhysics.DefocusingNLS.MainTheorems as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/MainTheorems.lean:30 (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 := by
    …

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

40. theorem OAI.DefocusingNLS.gaussian_not_almost_sure_global Challenge statement: Stable blowup for the defocusing Schrödinger equation sorry line 290

    Source documentation

    In particular, Gaussian data are not almost surely globally continuable.

    L4DEL explanation

    The formalization constructs stable self-similar finite-time blowup for defocusing nonlinear Schrödinger equations on the twelve-dimensional torus. For every prescribed lower bound on the power, it selects an odd power at least that large and a Sobolev index $k>8$ for which a nonempty open set of $H^k$ initial data has the stated classical blowup behavior. The selected quantifier gives arbitrarily large odd powers, rather than every sufficiently large odd power. For each such construction, Gaussian Fourier data with decay exponent $\alpha>k+6$ assign positive probability to the blowup set, and almost-sure global existence fails. The exponent $\alpha$ may be arbitrarily large.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.MathematicalPhysics.DefocusingNLS.MainTheorems as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/MathematicalPhysics/DefocusingNLS/MainTheorems.lean:45 (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 := by
    …

    Mentions: OAI.DefocusingNLS.maximalSobolevInteractionDomain