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

77 declarations, 1 contain sorry, 0 declared as axioms

  1. abbrev OAI.PosteriorReplicas.Vec line 14

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:15 (same declaration text).

  2. abbrev OAI.PosteriorReplicas.Rows line 15

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:16 (same declaration text).

  3. abbrev OAI.PosteriorReplicas.Labels line 16

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:17 (same declaration text).

  4. abbrev OAI.PosteriorReplicas.Data line 17

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:18 (same declaration text).

  5. abbrev OAI.PosteriorReplicas.Tuple line 18

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:19 (same declaration text).

  6. def OAI.PosteriorReplicas.sphereLaw line 20

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:21 (same declaration text).

  7. def OAI.PosteriorReplicas.gaussianRows line 24

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:25 (same declaration text).

  8. instance OAI.PosteriorReplicas.(instance at line 27) line 27
  9. def OAI.PosteriorReplicas.labels line 31

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:32 (same declaration text).

  10. lemma OAI.PosteriorReplicas.measurable_labels line 34

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:35 (same declaration text).

  11. def OAI.PosteriorReplicas.messageKernel line 39

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:40 (same declaration text).

  12. instance OAI.PosteriorReplicas.(instance at line 45) line 45
  13. def OAI.PosteriorReplicas.signalMessageLaw line 50

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:51 (same declaration text).

  14. instance OAI.PosteriorReplicas.(instance at line 55) line 55
  15. def OAI.PosteriorReplicas.sideLaw line 61

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:62 (same declaration text).

  16. instance OAI.PosteriorReplicas.(instance at line 66) line 66
  17. def OAI.PosteriorReplicas.messageEntropy line 71

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:72 (same declaration text).

  18. def OAI.PosteriorReplicas.conditionalInformation line 74

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:75 (same declaration text).

  19. def OAI.PosteriorReplicas.GaussianReplicaBlock line 78

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:79 (same declaration text).

  20. inductive OAI.PosteriorReplicas.BaseLaw line 92

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:93 (same declaration text).

  21. def OAI.PosteriorReplicas.BaseLaw.measure line 97

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:98 (same declaration text).

  22. def OAI.PosteriorReplicas.rowGram line 102

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:103 (same declaration text).

  23. def OAI.PosteriorReplicas.liftLabel line 105

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:106 (same declaration text).

  24. def OAI.PosteriorReplicas.kernelComponent line 108

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:109 (same declaration text).

  25. def OAI.PosteriorReplicas.baseFiber line 111

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:112 (same declaration text).

  26. def OAI.PosteriorReplicas.baseDensity line 121

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:122 (same declaration text).

  27. def OAI.PosteriorReplicas.tiltMass line 134

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:135 (same declaration text).

  28. def OAI.PosteriorReplicas.projectedDensity line 138

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:139 (same declaration text).

  29. def OAI.PosteriorReplicas.tiltedFiber line 142

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:143 (same declaration text).

  30. def OAI.PosteriorReplicas.differences line 147

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:148 (same declaration text).

  31. def OAI.PosteriorReplicas.differenceSpan line 150

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:151 (same declaration text).

  32. def OAI.PosteriorReplicas.affineVolume line 153

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:154 (same declaration text).

  33. def OAI.PosteriorReplicas.constrainedRows line 156

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:157 (same declaration text).

  34. def OAI.PosteriorReplicas.equalLabelLeft line 160

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:161 (same declaration text).

  35. def OAI.PosteriorReplicas.equalLabelRight line 166

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:167 (same declaration text).

  36. def OAI.PosteriorReplicas.EqualLabelMeasureIdentity line 173

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:174 (same declaration text).

  37. def OAI.PosteriorReplicas.DistanceReplicaBlock line 181

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:182 (same declaration text).

  38. def OAI.PosteriorReplicas.SyntheticReplicaBlock line 192

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:193 (same declaration text).

  39. def OAI.PosteriorReplicas.IncidenceReplicaBlock line 204

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:205 (same declaration text).

  40. def OAI.PosteriorReplicas.labelNorm line 215

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:216 (same declaration text).

  41. def OAI.PosteriorReplicas.ballDensityVersion line 217

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:218 (same declaration text).

  42. def OAI.PosteriorReplicas.gaussianDensityVersion line 223

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:224 (same declaration text).

  43. def OAI.PosteriorReplicas.EqualLabelVersions line 230

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:231 (same declaration text).

  44. def OAI.PosteriorReplicas.haarRows line 255

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:256 (same declaration text).

  45. def OAI.PosteriorReplicas.cmi line 258

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:259 (same declaration text).

  46. def OAI.PosteriorReplicas.finiteEntropy line 263

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:264 (same declaration text).

  47. def OAI.PosteriorReplicas.stateMessageKernel line 266

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:267 (same declaration text).

  48. instance OAI.PosteriorReplicas.(instance at line 270) line 270
  49. def OAI.PosteriorReplicas.stateMessageLaw line 275

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:276 (same declaration text).

  50. instance OAI.PosteriorReplicas.(instance at line 280) line 280
  51. def OAI.PosteriorReplicas.stateHaarSideLaw line 286

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:287 (same declaration text).

  52. instance OAI.PosteriorReplicas.(instance at line 292) line 292
  53. def OAI.PosteriorReplicas.terminalConditionalEntropy line 298

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:299 (same declaration text).

  54. def OAI.PosteriorReplicas.HaarReplicaBlock line 302

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:303 (same declaration text).

  55. abbrev OAI.PosteriorRegression.Vector line 327

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:328 (same declaration text).

  56. abbrev OAI.PosteriorRegression.UnitSphere line 328

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:329 (same declaration text).

  57. abbrev OAI.PosteriorRegression.State line 329

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:330 (same declaration text).

  58. abbrev OAI.PosteriorRegression.Samples line 330

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:331 (same declaration text).

  59. def OAI.PosteriorRegression.uniformSphere line 332

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:333 (same declaration text).

  60. def OAI.PosteriorRegression.sampleLaw line 336

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:337 (same declaration text).

  61. def OAI.PosteriorRegression.observationReference line 339

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:340 (same declaration text).

  62. abbrev OAI.PosteriorRegression.Learner.RunStatus line 344

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:345 (same declaration text).

  63. def OAI.PosteriorRegression.Learner.angularError line 346

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:347 (same declaration text).

  64. abbrev OAI.PosteriorRegression.CompletedObservation line 359

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:360 (same declaration text).

  65. abbrev OAI.PosteriorRegression.Destination line 360

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:361 (same declaration text).

  66. structure OAI.PosteriorRegression.CompletedKernelLearner line 362

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:363 (same declaration text).

  67. def OAI.PosteriorRegression.CompletedKernelLearner.destStatus line 375

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:376 (same declaration text).

  68. def OAI.PosteriorRegression.CompletedKernelLearner.finishState line 378

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:379 (same declaration text).

  69. def OAI.PosteriorRegression.CompletedKernelLearner.stepMeasure line 382

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:383 (same declaration text).

  70. def OAI.PosteriorRegression.CompletedKernelLearner.runMeasure line 387

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:388 (same declaration text).

  71. def OAI.PosteriorRegression.CompletedKernelLearner.terminalLaw line 393

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:394 (same declaration text).

  72. def OAI.PosteriorRegression.CompletedKernelLearner.estimateLaw line 397

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:398 (same declaration text).

  73. structure OAI.PosteriorRegression.JointKernelExperiment line 403

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:404 (same declaration text).

  74. def OAI.PosteriorRegression.JointKernelExperiment.law line 415

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:416 (same declaration text).

  75. def OAI.PosteriorRegression.JointKernelExperiment.uniformSuccess line 419

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:420 (same declaration text).

  76. def OAI.PosteriorRegression.KernelSubquadraticMemory line 425

    Also declared: OAI/Probability/PosteriorReplicas/Model.lean:426 (same declaration text).

  77. theorem OAI.PosteriorReplicas.source_main Challenge statement: Posterior-replica comparisons and sample lower bound sorry line 447

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

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

    theorem source_main : EqualLabelMeasureIdentity ∧ EqualLabelVersions ∧
    GaussianReplicaBlock ∧ DistanceReplicaBlock ∧ HaarReplicaBlock ∧
    SyntheticReplicaBlock ∧ IncidenceReplicaBlock ∧
    PosteriorRegression.KernelSubquadraticMemory.{u} := by
…

    Mentions: OAI.PosteriorReplicas.EqualLabelMeasureIdentity, OAI.PosteriorReplicas.EqualLabelVersions, OAI.PosteriorReplicas.GaussianReplicaBlock, OAI.PosteriorReplicas.DistanceReplicaBlock, OAI.PosteriorReplicas.HaarReplicaBlock, OAI.PosteriorReplicas.SyntheticReplicaBlock, OAI.PosteriorReplicas.IncidenceReplicaBlock