ComparatorChallenges/TriangularGaussian.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

68 declarations, 1 contain sorry, 0 declared as axioms

Sharp Gaussian minorants with atomic interpolation

The sharp Gaussian minorants of the atomic certificate for triangular-lattice universal optimality, including the construction for parameters at least one.

  1. abbrev OAI.AtomicTriangular.Plane line 18

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

  2. def OAI.AtomicTriangular.b line 20

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

  3. def OAI.AtomicTriangular.triangularPoint line 22

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

  4. def OAI.AtomicTriangular.A line 27

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

  5. def OAI.AtomicTriangular.dualA line 29

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

  6. def OAI.AtomicTriangular.gaussian line 31

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

  7. def OAI.AtomicTriangular.Radial line 33

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

  8. def OAI.AtomicTriangular.realFourier line 35

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  56. def OAI.AtomicTriangular.Construction.targetCoefficient line 177

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

  57. def OAI.AtomicTriangular.Construction.Yf line 179

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

  58. def OAI.AtomicTriangular.Construction.gamma line 186

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

  59. def OAI.AtomicTriangular.Construction.Uplus line 189

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

  60. def OAI.AtomicTriangular.Construction.Uminus line 192

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

  61. def OAI.AtomicTriangular.Construction.finiteSolution line 195

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

  62. def OAI.AtomicTriangular.Construction.Acoefficient line 198

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

  63. def OAI.AtomicTriangular.Construction.gaussianZ line 203

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

  64. def OAI.AtomicTriangular.Construction.actualParameter line 205

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

  65. def OAI.AtomicTriangular.Construction.normalizingDen line 209

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

  66. def OAI.AtomicTriangular.Construction.correctedFinite line 220

    Also declared: OAI/Analysis/Triangular/GaussianMinorants.lean:21 (same declaration text).

  67. def OAI.AtomicTriangular.AtomicConstruction line 236

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

  68. theorem OAI.AtomicTriangular.sharp_gaussian_minorants_with_construction Challenge statement: Gaussian Fourier minorants with their construction sorry line 263

    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.GaussianMinorants as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

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

    theorem sharp_gaussian_minorants_with_construction (α : ℝ) (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 ≤ α → AtomicConstruction α f) := by
…

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