ComparatorChallenges/AtomicGaussian.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.

Project sources: Pinned openai/math documentation, Pinned formalization catalogue

69 declarations, 1 contain sorry, 0 declared as axioms

  1. abbrev OAI.AtomicTriangular.Plane line 11

    Also declared: ComparatorChallenges/TriangularEnergy.lean:42 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:18 (same declaration text), OAI/Analysis/Triangular/Basic.lean:11 (same declaration text).

  2. def OAI.AtomicTriangular.b line 13

    Also declared: ComparatorChallenges/TriangularEnergy.lean:44 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:20 (same declaration text), OAI/Analysis/Triangular/Basic.lean:13 (same declaration text).

  3. def OAI.AtomicTriangular.triangularPoint line 15

    Also declared: ComparatorChallenges/TriangularEnergy.lean:46 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:22 (same declaration text), OAI/Analysis/Triangular/Basic.lean:15 (same declaration text).

  4. def OAI.AtomicTriangular.A line 20

    Also declared: ComparatorChallenges/TriangularEnergy.lean:51 (same declaration text), ComparatorChallenges/TriangularGaussian.lean:27 (same declaration text), OAI/Analysis/Triangular/Basic.lean:20 (same declaration text).

  5. def OAI.AtomicTriangular.dualA line 22

    Also declared: ComparatorChallenges/TriangularGaussian.lean:29 (same declaration text), OAI/Analysis/Triangular/Basic.lean:22 (same declaration text).

  6. def OAI.AtomicTriangular.gaussian line 24

    Also declared: ComparatorChallenges/TriangularGaussian.lean:31 (same declaration text), OAI/Analysis/Triangular/Basic.lean:24 (same declaration text).

  7. def OAI.AtomicTriangular.Radial line 26

    Also declared: ComparatorChallenges/TriangularGaussian.lean:33 (same declaration text), OAI/Analysis/Triangular/Basic.lean:26 (same declaration text).

  8. def OAI.AtomicTriangular.realFourier line 28

    Also declared: ComparatorChallenges/TriangularGaussian.lean:35 (same declaration text), OAI/Analysis/Triangular/Basic.lean:28 (same declaration text).

  9. def OAI.AtomicTriangular.Construction.b line 34

    Also declared: ComparatorChallenges/TriangularGaussian.lean:41 (same declaration text), OAI/Analysis/Triangular/Basic.lean:34 (same declaration text).

  10. def OAI.AtomicTriangular.Construction.h line 36

    Also declared: ComparatorChallenges/TriangularGaussian.lean:43 (same declaration text), OAI/Analysis/Triangular/Basic.lean:36 (same declaration text).

  11. def OAI.AtomicTriangular.Construction.H line 38

    Also declared: ComparatorChallenges/TriangularGaussian.lean:45 (same declaration text), OAI/Analysis/Triangular/Basic.lean:38 (same declaration text).

  12. def OAI.AtomicTriangular.Construction.eta line 40

    Also declared: ComparatorChallenges/TriangularGaussian.lean:47 (same declaration text), OAI/Analysis/Triangular/Basic.lean:40 (same declaration text).

  13. def OAI.AtomicTriangular.Construction.kappa line 42

    Also declared: ComparatorChallenges/TriangularGaussian.lean:49 (same declaration text), OAI/Analysis/Triangular/Basic.lean:42 (same declaration text).

  14. def OAI.AtomicTriangular.Construction.residues line 44

    Also declared: ComparatorChallenges/TriangularGaussian.lean:51 (same declaration text), OAI/Analysis/Triangular/Basic.lean:44 (same declaration text).

  15. def OAI.AtomicTriangular.Construction.residue line 46

    Also declared: ComparatorChallenges/TriangularGaussian.lean:53 (same declaration text), OAI/Analysis/Triangular/Basic.lean:46 (same declaration text).

  16. def OAI.AtomicTriangular.Construction.Node line 48

    Also declared: ComparatorChallenges/TriangularGaussian.lean:55 (same declaration text), OAI/Analysis/Triangular/Basic.lean:48 (same declaration text).

  17. def OAI.AtomicTriangular.Construction.FiniteNodes line 50

    Also declared: ComparatorChallenges/TriangularGaussian.lean:57 (same declaration text), OAI/Analysis/Triangular/Basic.lean:50 (same declaration text).

  18. def OAI.AtomicTriangular.Construction.sineFactor line 52

    Also declared: ComparatorChallenges/TriangularGaussian.lean:59 (same declaration text), OAI/Analysis/Triangular/Basic.lean:52 (same declaration text).

  19. def OAI.AtomicTriangular.Construction.P line 55

    Also declared: ComparatorChallenges/TriangularGaussian.lean:62 (same declaration text), OAI/Analysis/Triangular/Basic.lean:55 (same declaration text).

  20. def OAI.AtomicTriangular.Construction.dBasis line 57

    Also declared: ComparatorChallenges/TriangularGaussian.lean:64 (same declaration text), OAI/Analysis/Triangular/Basic.lean:57 (same declaration text).

  21. def OAI.AtomicTriangular.Construction.cBasis line 59

    Also declared: ComparatorChallenges/TriangularGaussian.lean:66 (same declaration text), OAI/Analysis/Triangular/Basic.lean:59 (same declaration text).

  22. def OAI.AtomicTriangular.Construction.finiteC line 61

    Also declared: ComparatorChallenges/TriangularGaussian.lean:68 (same declaration text), OAI/Analysis/Triangular/Basic.lean:61 (same declaration text).

  23. def OAI.AtomicTriangular.Construction.finiteD line 64

    Also declared: ComparatorChallenges/TriangularGaussian.lean:71 (same declaration text), OAI/Analysis/Triangular/Basic.lean:64 (same declaration text).

  24. def OAI.AtomicTriangular.Construction.phase line 69

    Also declared: ComparatorChallenges/TriangularGaussian.lean:76 (same declaration text), OAI/Analysis/Triangular/Basic.lean:69 (same declaration text).

  25. def OAI.AtomicTriangular.Construction.atomFactor line 71

    Also declared: ComparatorChallenges/TriangularGaussian.lean:78 (same declaration text), OAI/Analysis/Triangular/Basic.lean:71 (same declaration text).

  26. def OAI.AtomicTriangular.Construction.atomPolynomial line 74

    Also declared: ComparatorChallenges/TriangularGaussian.lean:81 (same declaration text), OAI/Analysis/Triangular/Basic.lean:74 (same declaration text).

  27. def OAI.AtomicTriangular.Construction.cAtomPolynomial line 76

    Also declared: ComparatorChallenges/TriangularGaussian.lean:83 (same declaration text), OAI/Analysis/Triangular/Basic.lean:76 (same declaration text).

  28. def OAI.AtomicTriangular.Construction.dAtomPolynomial line 79

    Also declared: ComparatorChallenges/TriangularGaussian.lean:86 (same declaration text), OAI/Analysis/Triangular/Basic.lean:79 (same declaration text).

  29. def OAI.AtomicTriangular.Construction.fourierCoeff line 84

    Also declared: ComparatorChallenges/TriangularGaussian.lean:91 (same declaration text), OAI/Analysis/Triangular/Basic.lean:84 (same declaration text).

  30. def OAI.AtomicTriangular.Construction.frequency line 86

    Also declared: ComparatorChallenges/TriangularGaussian.lean:93 (same declaration text), OAI/Analysis/Triangular/Basic.lean:86 (same declaration text).

  31. def OAI.AtomicTriangular.Construction.waveDerivative line 88

    Also declared: ComparatorChallenges/TriangularGaussian.lean:95 (same declaration text), OAI/Analysis/Triangular/Basic.lean:88 (same declaration text).

  32. def OAI.AtomicTriangular.Construction.Q line 92

    Also declared: ComparatorChallenges/TriangularGaussian.lean:99 (same declaration text), OAI/Analysis/Triangular/Basic.lean:92 (same declaration text).

  33. def OAI.AtomicTriangular.Construction.D line 94

    Also declared: ComparatorChallenges/TriangularGaussian.lean:101 (same declaration text), OAI/Analysis/Triangular/Basic.lean:94 (same declaration text).

  34. def OAI.AtomicTriangular.FiniteCertificate.cShiftPolynomial line 101

    Also declared: ComparatorChallenges/TriangularGaussian.lean:108 (same declaration text), OAI/Analysis/Triangular/Basic.lean:101 (same declaration text).

  35. def OAI.AtomicTriangular.FiniteCertificate.cCoefficient line 103

    Also declared: ComparatorChallenges/TriangularGaussian.lean:110 (same declaration text), OAI/Analysis/Triangular/Basic.lean:103 (same declaration text).

  36. def OAI.AtomicTriangular.FiniteCertificate.dCoefficient line 105

    Also declared: ComparatorChallenges/TriangularGaussian.lean:112 (same declaration text), OAI/Analysis/Triangular/Basic.lean:105 (same declaration text).

  37. abbrev OAI.AtomicTriangular.Construction.Plane line 111

    Also declared: ComparatorChallenges/TriangularGaussian.lean:118 (same declaration text), OAI/Analysis/Triangular/Basic.lean:111 (same declaration text).

  38. def OAI.AtomicTriangular.Construction.radial line 113

    Also declared: ComparatorChallenges/TriangularGaussian.lean:120 (same declaration text), OAI/Analysis/Triangular/Basic.lean:113 (same declaration text).

  39. def OAI.AtomicTriangular.Construction.waveDen line 115

    Also declared: ComparatorChallenges/TriangularGaussian.lean:122 (same declaration text), OAI/Analysis/Triangular/Basic.lean:115 (same declaration text).

  40. def OAI.AtomicTriangular.Construction.Xwave line 117

    Also declared: ComparatorChallenges/TriangularGaussian.lean:124 (same declaration text), OAI/Analysis/Triangular/Basic.lean:117 (same declaration text).

  41. def OAI.AtomicTriangular.Construction.lambda line 119

    Also declared: ComparatorChallenges/TriangularGaussian.lean:126 (same declaration text), OAI/Analysis/Triangular/Basic.lean:119 (same declaration text).

  42. def OAI.AtomicTriangular.Construction.zeta line 121

    Also declared: ComparatorChallenges/TriangularGaussian.lean:128 (same declaration text), OAI/Analysis/Triangular/Basic.lean:121 (same declaration text).

  43. def OAI.AtomicTriangular.Construction.transformedWave line 123

    Also declared: ComparatorChallenges/TriangularGaussian.lean:130 (same declaration text), OAI/Analysis/Triangular/Basic.lean:123 (same declaration text).

  44. def OAI.AtomicTriangular.Construction.finiteColumn line 125

    Also declared: ComparatorChallenges/TriangularGaussian.lean:132 (same declaration text), OAI/Analysis/Triangular/Basic.lean:125 (same declaration text).

  45. def OAI.AtomicTriangular.Construction.finiteNode line 131

    Also declared: ComparatorChallenges/TriangularGaussian.lean:138 (same declaration text), OAI/Analysis/Triangular/Basic.lean:131 (same declaration text).

  46. def OAI.AtomicTriangular.Construction.jetMultiplier line 133

    Also declared: ComparatorChallenges/TriangularGaussian.lean:140 (same declaration text), OAI/Analysis/Triangular/Basic.lean:133 (same declaration text).

  47. def OAI.AtomicTriangular.Construction.jet line 137

    Also declared: ComparatorChallenges/TriangularGaussian.lean:144 (same declaration text), OAI/Analysis/Triangular/Basic.lean:137 (same declaration text).

  48. def OAI.AtomicTriangular.Construction.fullJetMatrix line 140

    Also declared: ComparatorChallenges/TriangularGaussian.lean:147 (same declaration text), OAI/Analysis/Triangular/Basic.lean:140 (same declaration text).

  49. def OAI.AtomicTriangular.Construction.R line 144

    Also declared: ComparatorChallenges/TriangularGaussian.lean:151 (same declaration text), OAI/Analysis/Triangular/Basic.lean:144 (same declaration text).

  50. def OAI.AtomicTriangular.Construction.R0 line 146

    Also declared: ComparatorChallenges/TriangularGaussian.lean:153 (same declaration text), OAI/Analysis/Triangular/Basic.lean:146 (same declaration text).

  51. abbrev OAI.AtomicTriangular.Construction.TailNode line 149

    Also declared: ComparatorChallenges/TriangularGaussian.lean:156 (same declaration text), OAI/Analysis/Triangular/Basic.lean:149 (same declaration text).

  52. structure OAI.AtomicTriangular.Construction.InputCoefficients line 151

    Also declared: ComparatorChallenges/TriangularGaussian.lean:158 (same declaration text), OAI/Analysis/Triangular/Basic.lean:151 (same declaration text).

  53. def OAI.AtomicTriangular.Construction.tailInput line 159

    Also declared: ComparatorChallenges/TriangularGaussian.lean:166 (same declaration text), OAI/Analysis/Triangular/Basic.lean:159 (same declaration text).

  54. def OAI.AtomicTriangular.Construction.finiteInput line 162

    Also declared: ComparatorChallenges/TriangularGaussian.lean:169 (same declaration text), OAI/Analysis/Triangular/Basic.lean:162 (same declaration text).

  55. def OAI.AtomicTriangular.Construction.inputComplex line 166

    Also declared: ComparatorChallenges/TriangularGaussian.lean:173 (same declaration text), OAI/Analysis/Triangular/Basic.lean:166 (same declaration text).

  56. def OAI.AtomicTriangular.Construction.Z line 170

    Also declared: OAI/Analysis/Triangular/Basic.lean:170 (same declaration text).

  57. def OAI.AtomicTriangular.Construction.targetCoefficient line 172

    Also declared: ComparatorChallenges/TriangularGaussian.lean:177 (same declaration text), OAI/Analysis/Triangular/Basic.lean:172 (same declaration text).

  58. def OAI.AtomicTriangular.Construction.Yf line 174

    Also declared: ComparatorChallenges/TriangularGaussian.lean:179 (same declaration text), OAI/Analysis/Triangular/Basic.lean:174 (same declaration text).

  59. def OAI.AtomicTriangular.Construction.gamma line 181

    Also declared: ComparatorChallenges/TriangularGaussian.lean:186 (same declaration text), OAI/Analysis/Triangular/Basic.lean:181 (same declaration text).

  60. def OAI.AtomicTriangular.Construction.Uplus line 184

    Also declared: ComparatorChallenges/TriangularGaussian.lean:189 (same declaration text), OAI/Analysis/Triangular/Basic.lean:184 (same declaration text).

  61. def OAI.AtomicTriangular.Construction.Uminus line 187

    Also declared: ComparatorChallenges/TriangularGaussian.lean:192 (same declaration text), OAI/Analysis/Triangular/Basic.lean:187 (same declaration text).

  62. def OAI.AtomicTriangular.Construction.finiteSolution line 190

    Also declared: ComparatorChallenges/TriangularGaussian.lean:195 (same declaration text), OAI/Analysis/Triangular/Basic.lean:190 (same declaration text).

  63. def OAI.AtomicTriangular.Construction.Acoefficient line 193

    Also declared: ComparatorChallenges/TriangularGaussian.lean:198 (same declaration text), OAI/Analysis/Triangular/Basic.lean:193 (same declaration text).

  64. def OAI.AtomicTriangular.Construction.gaussianZ line 198

    Also declared: ComparatorChallenges/TriangularGaussian.lean:203 (same declaration text), OAI/Analysis/Triangular/Basic.lean:198 (same declaration text).

  65. def OAI.AtomicTriangular.Construction.actualParameter line 200

    Also declared: ComparatorChallenges/TriangularGaussian.lean:205 (same declaration text), OAI/Analysis/Triangular/Basic.lean:200 (same declaration text).

  66. def OAI.AtomicTriangular.Construction.normalizingDen line 204

    Also declared: ComparatorChallenges/TriangularGaussian.lean:209 (same declaration text), OAI/Analysis/Triangular/Basic.lean:204 (same declaration text).

  67. def OAI.AtomicTriangular.Construction.finiteCoordinates line 210

    Also declared: OAI/Analysis/Triangular/Basic.lean:210 (same declaration text).

  68. def OAI.AtomicTriangular.Construction.HasAtomicConstruction line 214

    Also declared: OAI/Analysis/Triangular/Basic.lean:214 (same declaration text).

  69. theorem OAI.AtomicTriangular.sharp_gaussian_minorants_atomic Challenge statement: Sharp Gaussian minorants from an atomic certificate sorry line 239

    L4DEL explanation

    This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content.

    1. The linked formalization note covers 4 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.Analysis.Triangular.Main as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Analysis/Triangular/Main.lean:75 (same statement text; different proof or body). Qualify references as OAI.AtomicTriangular.sharp_gaussian_minorants_atomic@path.

    theorem sharp_gaussian_minorants_atomic (α : ℝ) (hα : 0 < α) :
    ∃ f : SchwartzMap Plane ℝ,
      Radial f ∧ (∀ x, f x ≤ gaussian α x) ∧
      (∀ w, (realFourier f w).im = 0 ∧ 0 ≤ (realFourier f w).re) ∧
      (∀ a ∈ A, a ≠ 0 → f a = gaussian α a) ∧
      (∀ w ∈ dualA, w ≠ 0 → realFourier f w = 0) ∧
      (1 ≤ α → Construction.HasAtomicConstruction α f) := by
…

    Mentions: OAI.AtomicTriangular.Plane, OAI.AtomicTriangular.Radial, OAI.AtomicTriangular.gaussian, OAI.AtomicTriangular.realFourier, OAI.AtomicTriangular.A, OAI.AtomicTriangular.dualA, OAI.AtomicTriangular.Construction.HasAtomicConstruction