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

78 declarations, 1 contain sorry, 0 declared as axioms

  1. abbrev OAI.MemoryPrecision.Kernel.Vector line 13

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:15 (same declaration text).

  2. abbrev OAI.MemoryPrecision.Kernel.Sphere line 15

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:16 (same declaration text).

  3. abbrev OAI.MemoryPrecision.Kernel.State line 17

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:17 (same declaration text).

  4. abbrev OAI.MemoryPrecision.Kernel.Action line 19

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:18 (same declaration text).

  5. abbrev OAI.MemoryPrecision.Kernel.Observations line 21

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:19 (same declaration text).

  6. abbrev OAI.MemoryPrecision.Kernel.Rows line 23

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:20 (same declaration text).

  7. def OAI.MemoryPrecision.Kernel.UniformSphere line 25

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:22 (same declaration text).

  8. def OAI.MemoryPrecision.Kernel.RowLaw line 39

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:36 (same declaration text).

  9. def OAI.MemoryPrecision.Kernel.ObservationReference line 57

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:53 (same declaration text).

  10. structure OAI.MemoryPrecision.Kernel.Policy line 60

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:56 (same declaration text).

  11. def OAI.MemoryPrecision.Kernel.Policy.Completed line 70

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:68 (same declaration text).

  12. def OAI.MemoryPrecision.Kernel.Policy.eval line 73

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:73 (same declaration text).

  13. def OAI.MemoryPrecision.Kernel.Policy.pathValue line 80

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:80 (same declaration text).

  14. def OAI.MemoryPrecision.Kernel.Policy.records line 84

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:84 (same declaration text).

  15. def OAI.MemoryPrecision.Kernel.Policy.outputTest line 93

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:93 (same declaration text).

  16. def OAI.MemoryPrecision.Kernel.Policy.angleTest line 97

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:97 (same declaration text).

  17. def OAI.MemoryPrecision.Kernel.Policy.chordTest line 108

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:108 (same declaration text).

  18. def OAI.MemoryPrecision.Kernel.Policy.experiment line 111

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:111 (same declaration text).

  19. structure OAI.MemoryPrecision.Kernel.Policy.Admissible line 115

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:115 (same declaration text).

  20. def OAI.MemoryPrecision.Kernel.Policy.Success line 121

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:121 (same declaration text).

  21. def OAI.MemoryPrecision.Kernel.Policy.ChordSuccess line 125

    Also declared: OAI/Probability/MemoryPrecision/KernelModel.lean:124 (same declaration text).

  22. abbrev OAI.NoiselessRegression.Vector line 133

    Also declared: ComparatorChallenges/NoiselessRegression.lean:18 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:17 (same declaration text), OAI/Probability/ProjectionMoments/Model.lean:17 (same declaration text).

  23. abbrev OAI.NoiselessRegression.UnitSphere line 134

    Also declared: ComparatorChallenges/NoiselessRegression.lean:19 (same declaration text), ComparatorChallenges/ProjectionMoments.lean:19 (same declaration text), OAI/Probability/ProjectionMoments/Model.lean:19 (same declaration text).

  24. abbrev OAI.MemoryPrecision.Space line 140

    Also declared: OAI/Probability/MemoryPrecision/AmbientGram.lean:18 (same declaration text).

  25. def OAI.MemoryPrecision.J line 142

    Also declared: OAI/Probability/MemoryPrecision/AmbientGram.lean:20 (same declaration text).

  26. def OAI.MemoryPrecision.AmbientBallBound line 149

    Also declared: OAI/Probability/MemoryPrecision/AmbientGram.lean:27 (same declaration text).

  27. def OAI.MemoryPrecision.InverseGram line 153

    Also declared: OAI/Probability/MemoryPrecision/AmbientGram.lean:31 (same declaration text).

  28. def OAI.MemoryPrecision.MatrixLabelReference line 163

    Also declared: OAI/Probability/MemoryPrecision/FiniteDensity.lean:20 (same declaration text).

  29. def OAI.MemoryPrecision.ProjectionLaw line 185

    Also declared: OAI/Probability/MemoryPrecision/FiniteDensity.lean:42 (same declaration text).

  30. def OAI.MemoryPrecision.ProjectedEllipsoid line 221

    Also declared: OAI/Probability/MemoryPrecision/FiniteDensity.lean:77 (same declaration text).

  31. def OAI.MemoryPrecision.ProjectionNormScale line 235

    Also declared: OAI/Probability/MemoryPrecision/FiniteDensity.lean:90 (same declaration text).

  32. def OAI.MemoryPrecision.UniformSphere line 242

    Also declared: OAI/Probability/MemoryPrecision/JointL1.lean:19 (same declaration text).

  33. def OAI.MemoryPrecision.GaussianRegularization line 255

    Also declared: OAI/Probability/MemoryPrecision/JointL1.lean:32 (same declaration text).

  34. def OAI.MemoryPrecision.PointwiseDensity line 274

    Also declared: OAI/Probability/MemoryPrecision/PointwiseDensity.lean:18 (same declaration text).

  35. lemma OAI.MemoryPrecision.space_finiteDimensional line 280

    Also declared: OAI/Probability/MemoryPrecision/WeightedImage.lean:19 (same declaration text).

  36. def OAI.MemoryPrecision.UnitBallVolume line 283

    Also declared: OAI/Probability/MemoryPrecision/RadialMixture.lean:18 (same declaration text).

  37. def OAI.MemoryPrecision.CoordinateUnit line 296

    Also declared: OAI/Probability/MemoryPrecision/RadialMixture.lean:31 (same declaration text).

  38. lemma OAI.MemoryPrecision.gaussianVariance_nonneg line 302

    Also declared: OAI/Probability/MemoryPrecision/RadialMixture.lean:37 (same declaration text).

  39. def OAI.MemoryPrecision.GaussianKernel line 304

    Also declared: OAI/Probability/MemoryPrecision/RadialMixture.lean:39 (same declaration text).

  40. def OAI.MemoryPrecision.RadialMixture line 311

    Also declared: OAI/Probability/MemoryPrecision/RadialMixture.lean:46 (same declaration text).

  41. abbrev OAI.MemoryPrecision.Sphere line 314

    Also declared: OAI/Probability/MemoryPrecision/CoefficientStep.lean:19 (same declaration text).

  42. def OAI.MemoryPrecision.SpherePrior line 316

    Also declared: OAI/Probability/MemoryPrecision/CoefficientStep.lean:20 (same declaration text).

  43. def OAI.MemoryPrecision.SphereBallBound line 319

    Also declared: OAI/Probability/MemoryPrecision/CoefficientStep.lean:23 (same declaration text).

  44. def OAI.MemoryPrecision.WeightedBlock line 327

    Also declared: OAI/Probability/MemoryPrecision/WeightedImage.lean:25 (same declaration text).

  45. def OAI.MemoryPrecision.SphereBlock line 349

    Also declared: OAI/Probability/MemoryPrecision/CoefficientStep.lean:27 (same declaration text).

  46. abbrev OAI.MemoryPrecision.CubeSet line 354

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:18 (same declaration text).

  47. abbrev OAI.MemoryPrecision.Cube line 368

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:31 (same declaration text).

  48. def OAI.MemoryPrecision.CubeLaw line 370

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:32 (same declaration text).

  49. lemma OAI.MemoryPrecision.cube_second_coordinate_lt line 373

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:34 (same declaration text).

  50. def OAI.MemoryPrecision.cubeRaw line 377

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:38 (same declaration text).

  51. def OAI.MemoryPrecision.CubeEmbedding line 391

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:51 (same declaration text).

  52. def OAI.MemoryPrecision.CubeBall line 393

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:52 (same declaration text).

  53. def OAI.MemoryPrecision.CubeLocal line 396

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:54 (same declaration text).

  54. lemma OAI.MemoryPrecision.cube_coordinate_square_le Every coordinate of the paired cube has square at most one quarter line 413

    Source documentation

    Every coordinate of the paired cube has square at most one quarter.

    L4DEL explanation

    Every coordinate of the paired cube has square at most one quarter.

    1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:158 (same declaration text).

    lemma cube_coordinate_square_le {d : ℕ} (u : Cube d) (i : Fin (d/2)) : u.val i^2 ≤ 1/4 := by
…

    Mentions: OAI.MemoryPrecision.Cube

  55. lemma OAI.MemoryPrecision.sum_fin_split line 417

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:110 (same declaration text).

  56. def OAI.MemoryPrecision.cubeCoords line 425

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:118 (same declaration text).

  57. lemma OAI.MemoryPrecision.cubeCoords_first line 437

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:130 (same declaration text).

  58. lemma OAI.MemoryPrecision.cubeCoords_second line 441

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:134 (same declaration text).

  59. lemma OAI.MemoryPrecision.cubeCoords_tail line 445

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:138 (same declaration text).

  60. lemma OAI.MemoryPrecision.cubeCoords_sum line 449

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:142 (same declaration text).

  61. lemma OAI.MemoryPrecision.cubeEmbedding_norm line 465

    Also declared: OAI/Probability/MemoryPrecision/CubeGeometry.lean:162 (same declaration text).

  62. def OAI.MemoryPrecision.CubeSphere line 485

    Also declared: OAI/Probability/MemoryPrecision/CubeExperiment.lean:20 (same declaration text).

  63. def OAI.MemoryPrecision.AmbientGramStatement line 488

    Also declared: OAI/Probability/MemoryPrecision/AmbientGram.lean:585 (same declaration text).

  64. def OAI.MemoryPrecision.FiniteDensityStatement line 533

    Also declared: OAI/Probability/MemoryPrecision/FiniteDensity.lean:247 (same declaration text).

  65. def OAI.MemoryPrecision.MeasurableTestStatement line 558

    Also declared: OAI/Probability/MemoryPrecision/MeasurableTests.lean:109 (same declaration text).

  66. def OAI.MemoryPrecision.JointL1Statement line 589

    Also declared: OAI/Probability/MemoryPrecision/JointL1.lean:132 (same declaration text).

  67. def OAI.MemoryPrecision.RadialMixtureRepresentation line 616

    Also declared: OAI/Probability/MemoryPrecision/PointwiseMain.lean:18 (same declaration text).

  68. def OAI.MemoryPrecision.FullRankDensityFormula line 624

    Also declared: OAI/Probability/MemoryPrecision/PointwiseMain.lean:26 (same declaration text).

  69. def OAI.MemoryPrecision.PointwiseDensityProperties line 648

    Also declared: OAI/Probability/MemoryPrecision/PointwiseMain.lean:50 (same declaration text).

  70. def OAI.MemoryPrecision.PointwiseDensityStatement line 673

    Also declared: OAI/Probability/MemoryPrecision/PointwiseMain.lean:75 (same declaration text).

  71. def OAI.MemoryPrecision.CoefficientStepStatement line 692

    Also declared: OAI/Probability/MemoryPrecision/CoefficientStep.lean:31 (same declaration text).

  72. def OAI.MemoryPrecision.CubeBlockStatement line 705

    Also declared: OAI/Probability/MemoryPrecision/CubeBlock.lean:111 (same declaration text).

  73. def OAI.MemoryPrecision.Kernel.Policy.ModelAdmissible line 719

    Also declared: OAI/Probability/MemoryPrecision/KernelAdmissibility.lean:19 (same declaration text).

  74. def OAI.MemoryPrecision.Kernel.CubePrior line 727

    Also declared: OAI/Probability/MemoryPrecision/KernelCube.lean:23 (same declaration text).

  75. def OAI.MemoryPrecision.Kernel.BlockCount line 730

    Also declared: OAI/Probability/MemoryPrecision/KernelEllipsoid.lean:84 (same declaration text).

  76. def OAI.MemoryPrecision.Kernel.SourceEllipsoidStatement line 732

    Also declared: OAI/Probability/MemoryPrecision/KernelEllipsoid.lean:85 (same declaration text).

  77. lemma OAI.MemoryPrecision.Kernel.cubePrior_dimension line 764

    Also declared: OAI/Probability/MemoryPrecision/CubeSuccess.lean:44 (same declaration text).

  78. theorem OAI.MemoryPrecision.main Challenge statement: Projection estimates and memory–precision bounds sorry line 771

    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 8 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.Probability.MemoryPrecision.Main as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/MemoryPrecision/Main.lean:59 (same statement text; different proof or body). Qualify references as OAI.MemoryPrecision.main@path.

    theorem main :
  AmbientGramStatement ∧
  FiniteDensityStatement ∧
  MeasurableTestStatement ∧
  JointL1Statement ∧
  PointwiseDensityStatement ∧
  CoefficientStepStatement ∧
  Kernel.SourceEllipsoidStatement.{u} ∧
  CubeBlockStatement ∧
  (∃ D : ℝ, Real.exp 1 ≤ D ∧ ∃ d₀ : ℕ, ∃ hd₀ : 16 ≤ d₀, ∃ c : ℝ, 0 < c ∧
    ∀ d M T : ℕ, ∀ hd : d₀ ≤ d, M ≤ d^2 → ∀ ε : ℝ, 0 < ε → ε ≤ 1/10 →
    ∀ (Ω : Type u) [MeasurableSpace Ω] (ρ : Measure Ω), IsProbabilityMeasure ρ →
…

    Mentions: OAI.MemoryPrecision.AmbientGramStatement, OAI.MemoryPrecision.FiniteDensityStatement, OAI.MemoryPrecision.MeasurableTestStatement, OAI.MemoryPrecision.JointL1Statement, OAI.MemoryPrecision.PointwiseDensityStatement, OAI.MemoryPrecision.CoefficientStepStatement, OAI.MemoryPrecision.CubeBlockStatement