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

79 declarations, 11 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentProjection.Vector line 12

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:10 (same declaration text).

  2. abbrev OAI.CurrentProjection.Sphere line 14

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:11 (same declaration text).

  3. abbrev OAI.CurrentProjection.Rows line 16

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:12 (same declaration text).

  4. def OAI.CurrentProjection.uniformSphere line 18

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:15 (same declaration text).

  5. def OAI.CurrentProjection.gaussianRows line 22

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:20 (same declaration text).

  6. def OAI.CurrentProjection.label line 25

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:23 (same declaration text).

  7. def OAI.CurrentProjection.LocalGrowth line 28

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:27 (same declaration text).

  8. def OAI.CurrentProjection.cubeAverage line 32

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:32 (same declaration text).

  9. def OAI.CurrentProjection.exactDensity line 37

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:38 (same declaration text).

  10. def OAI.CurrentProjection.AdmissibleDimensions line 43

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:45 (same declaration text).

  11. def OAI.CurrentProjection.momentConstant line 46

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:48 (same declaration text).

  12. def OAI.CurrentProjection.MixedMomentMain line 49

    Also declared: OAI/Probability/GaussianReplacement/Basic.lean:53 (same declaration text).

  13. instance OAI.CurrentProjection.gaussianRows_isProbabilityMeasure line 69

    Also declared: OAI/Probability/GaussianReplacement/Density.lean:351 (same declaration text).

  14. lemma OAI.CurrentProjection.measurable_own_label line 73

    Also declared: OAI/Probability/GaussianReplacement/Density.lean:355 (same declaration text).

  15. def OAI.CurrentProjection.swapLast line 80

    Also declared: OAI/Probability/GaussianReplacement/Entropy.lean:183 (same declaration text).

  16. def OAI.CurrentProjection.rowInformation line 89

    Also declared: OAI/Probability/GaussianReplacement/Entropy.lean:211 (same declaration text).

  17. def OAI.CurrentProjection.shannonEntropy line 93

    Also declared: OAI/Probability/GaussianReplacement/Entropy.lean:133 (same declaration text).

  18. def OAI.CurrentProjection.conditionalMutualInformation line 96

    Also declared: OAI/Probability/GaussianReplacement/ConditionalInfo.lean:15 (same declaration text).

  19. def OAI.CurrentProjection.actualExperiment line 105

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:13 (same declaration text).

  20. instance OAI.CurrentProjection.actualExperiment_isProbabilityMeasure line 109

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:17 (same declaration text).

  21. def OAI.CurrentProjection.actualObservation line 114

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:26 (same declaration text).

  22. instance OAI.CurrentProjection.actualObservation_isProbabilityMeasure line 119

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:42 (same declaration text).

  23. def OAI.CurrentProjection.selectedCube line 124

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:126 (same declaration text).

  24. def OAI.CurrentProjection.selectedExact line 127

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:129 (same declaration text).

  25. def OAI.CurrentProjection.momentBound line 130

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:196 (same declaration text).

  26. def OAI.CurrentProjection.logPositive line 133

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:262 (same declaration text).

  27. def OAI.CurrentProjection.logNegative line 135

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:264 (same declaration text).

  28. def OAI.CurrentProjection.extendedLogExpectation line 137

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:267 (same declaration text).

  29. def OAI.CurrentProjection.PositiveMessage line 142

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:308 (same declaration text).

  30. def OAI.CurrentProjection.completeFamily line 144

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:310 (same declaration text).

  31. structure OAI.CurrentProjection.ActualRowConclusion line 148

    Also declared: OAI/Probability/GaussianReplacement/ActualRow.lean:341 (same declaration text).

  32. def OAI.CurrentProjection.actualConditionalRowInformation line 181

    Also declared: OAI/Probability/GaussianReplacement/ConditionalInfo.lean:290 (same declaration text).

  33. structure OAI.CurrentProjection.ActualRowSourceConclusion line 186

    Also declared: OAI/Probability/GaussianReplacement/ConditionalInfo.lean:295 (same declaration text).

  34. def OAI.CurrentProjection.alignedExperiment line 220

    Also declared: OAI/Probability/GaussianReplacement/ConditionalInfo.lean:400 (same declaration text).

  35. instance OAI.CurrentProjection.alignedExperiment_probability line 224

    Also declared: OAI/Probability/GaussianReplacement/ConditionalInfo.lean:408 (same declaration text).

  36. def OAI.CurrentProjection.exposedJointMap line 230

    Also declared: OAI/Probability/GaussianReplacement/ConditionalInfo.lean:414 (same declaration text).

  37. def OAI.CurrentProjection.exposedInformation line 233

    Also declared: OAI/Probability/GaussianReplacement/ConditionalInfo.lean:423 (same declaration text).

  38. def OAI.CurrentProjection.CriticalComparisonMain line 237

    Also declared: OAI/Probability/GaussianReplacement/CriticalGeometry.lean:12 (same declaration text).

  39. def OAI.CurrentProjection.OneLevelComparisonMain line 246

    Also declared: OAI/Probability/GaussianReplacement/Comparison.lean:233 (same declaration text).

  40. def OAI.CurrentProjection.TwoLabelComparisonMain line 256

    Also declared: OAI/Probability/GaussianReplacement/Comparison.lean:243 (same declaration text).

  41. def OAI.CurrentProjection.blockInput line 265

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:16 (same declaration text).

  42. lemma OAI.CurrentProjection.measurable_blockInput line 269

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:20 (same declaration text).

  43. def OAI.CurrentProjection.blockLaw line 275

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:26 (same declaration text).

  44. instance OAI.CurrentProjection.blockLaw_probability line 281

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:32 (same declaration text).

  45. def OAI.CurrentProjection.endingSignalLaw line 289

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:40 (same declaration text).

  46. instance OAI.CurrentProjection.endingSignalLaw_probability line 295

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:46 (same declaration text).

  47. def OAI.CurrentProjection.freshInformation line 303

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:54 (same declaration text).

  48. def OAI.CurrentProjection.hybridFirst line 307

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:58 (same declaration text).

  49. def OAI.CurrentProjection.hybridLast line 309

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:60 (same declaration text).

  50. def OAI.CurrentProjection.hybridCount line 311

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:62 (same declaration text).

  51. def OAI.CurrentProjection.averagedFreshInformation line 313

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:64 (same declaration text).

  52. def OAI.CurrentProjection.HybridBlockMain line 319

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:71 (same declaration text).

  53. def OAI.CurrentProjection.FiberBlockMain line 335

    Also declared: OAI/Probability/GaussianReplacement/HybridModel.lean:87 (same declaration text).

  54. def OAI.CurrentProjection.dependentMapKernel line 346

    Also declared: OAI/Probability/GaussianReplacement/ConditionalLaw.lean:13 (same declaration text).

  55. def OAI.CurrentProjection.fiberObservationLaw line 350

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:16 (same declaration text).

  56. instance OAI.CurrentProjection.uniformSphere_finite line 354

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:24 (same declaration text).

  57. instance OAI.CurrentProjection.fiberObservationLaw_finite line 360

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:30 (same declaration text).

  58. lemma OAI.CurrentProjection.sphere_standardBorel line 364

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:34 (same declaration text).

  59. def OAI.CurrentProjection.sphericalFiberKernel line 367

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:37 (same declaration text).

  60. instance OAI.CurrentProjection.sphericalFiberKernel_markov line 373

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:43 (same declaration text).

  61. def OAI.CurrentProjection.fiberTwoPointLeft line 378

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:49 (same declaration text).

  62. def OAI.CurrentProjection.perpendicularRow line 385

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:57 (same declaration text).

  63. def OAI.CurrentProjection.perpendicularRowsKernel line 390

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:67 (same declaration text).

  64. def OAI.CurrentProjection.fiberTwoPointConstant line 394

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:72 (same declaration text).

  65. def OAI.CurrentProjection.fiberDistanceWeight line 401

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:79 (same declaration text).

  66. def OAI.CurrentProjection.fiberTwoPointRight line 404

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:83 (same declaration text).

  67. lemma OAI.CurrentProjection.uniformSphere_probability_of_pos line 413

    Also declared: OAI/Probability/GaussianReplacement/Comparison.lean:185 (same declaration text).

  68. def OAI.CurrentProjection.FiberTwoPointMain line 425

    Also declared: OAI/Probability/GaussianReplacement/FiberModel.lean:93 (same declaration text).

  69. theorem OAI.CurrentProjection.mixedMomentMain Challenge statement: Gaussian replacement and information bounds sorry line 433

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/GaussianReplacement/Density.lean:484 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.mixedMomentMain@path.

    theorem mixedMomentMain : MixedMomentMain := by
…

    Mentions: OAI.CurrentProjection.MixedMomentMain

  70. theorem OAI.CurrentProjection.actualRowMain Challenge statement: Gaussian replacement and information bounds sorry line 436

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/GaussianReplacement/ActualRow.lean:375 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.actualRowMain@path.

    theorem actualRowMain {d m r q : ℕ} {W : Type*} [MeasurableSpace W]
    [Countable W] [MeasurableSingletonClass W]
    (hdim : AdmissibleDimensions d m r q)
    (P : Measure ((Sphere d×W)×Rows m d)) [IsProbabilityMeasure P]
    (ν : Measure (Sphere d)) [IsProbabilityMeasure ν]
    (hInd : (P.map swapLast).fst = ν.prod (gaussianRows m d))
    (H : ℝ) (hν : ν ≤ ENNReal.ofReal H • uniformSphere d)
    (hEntropy : shannonEntropy (P.map swapLast).snd ≠ ∞)
    (ρ : PositiveMessage (P.map swapLast).snd → Measure (Sphere d))
    [∀ w, IsFiniteMeasure (ρ w)]
    (_hρac : ∀ w, ρ w ≪ uniformSphere d)
    (B D : PositiveMessage (P.map swapLast).snd → ℝ)
…

    Mentions: OAI.CurrentProjection.AdmissibleDimensions, OAI.CurrentProjection.Sphere, OAI.CurrentProjection.Rows, OAI.CurrentProjection.swapLast, OAI.CurrentProjection.gaussianRows, OAI.CurrentProjection.uniformSphere, OAI.CurrentProjection.shannonEntropy, OAI.CurrentProjection.PositiveMessage

  71. theorem OAI.CurrentProjection.actualRowRefinement Challenge statement: Gaussian replacement and information bounds sorry line 457

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/GaussianReplacement/ActualRow.lean:433 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.actualRowRefinement@path.

    theorem actualRowRefinement {d m : ℕ} {W E : Type*} [MeasurableSpace W]
    [MeasurableSpace E] [Countable W] [MeasurableSingletonClass W]
    [Countable E] [MeasurableSingletonClass E]
    (P : Measure ((Sphere d×W)×Rows m d)) [IsProbabilityMeasure P]
    (e : Sphere d×W → E) (he : Measurable e)
    (_hEntropy : shannonEntropy
      ((P.map (fun p => ((p.1.1,(p.1.2,e p.1)),p.2))).map swapLast).snd ≠ ∞) :
    rowInformation (P.map (fun p => ((p.1.1,(p.1.2,e p.1)),p.2))) (gaussianRows m d) =
      rowInformation P (gaussianRows m d) := by
…

    Mentions: OAI.CurrentProjection.Sphere, OAI.CurrentProjection.Rows, OAI.CurrentProjection.shannonEntropy, OAI.CurrentProjection.swapLast, OAI.CurrentProjection.rowInformation, OAI.CurrentProjection.gaussianRows

  72. theorem OAI.CurrentProjection.actualRowSourceMain Challenge statement: Gaussian replacement and information bounds sorry line 468

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/GaussianReplacement/ConditionalInfo.lean:329 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.actualRowSourceMain@path.

    theorem actualRowSourceMain {d m r q : ℕ} {W : Type*} [MeasurableSpace W]
    [Countable W] [MeasurableSingletonClass W]
    (hdim : AdmissibleDimensions d m r q)
    (P : Measure ((Sphere d×W)×Rows m d)) [IsProbabilityMeasure P]
    (ν : Measure (Sphere d)) [IsProbabilityMeasure ν]
    (hInd : (P.map swapLast).fst = ν.prod (gaussianRows m d))
    (H : ℝ) (hν : ν ≤ ENNReal.ofReal H • uniformSphere d)
    (hEntropy : shannonEntropy (P.map swapLast).snd ≠ ∞)
    (ρ : PositiveMessage (P.map swapLast).snd → Measure (Sphere d))
    [∀ w, IsFiniteMeasure (ρ w)]
    (_hρac : ∀ w, ρ w ≪ uniformSphere d)
    (B D : PositiveMessage (P.map swapLast).snd → ℝ)
…

    Mentions: OAI.CurrentProjection.AdmissibleDimensions, OAI.CurrentProjection.Sphere, OAI.CurrentProjection.Rows, OAI.CurrentProjection.swapLast, OAI.CurrentProjection.gaussianRows, OAI.CurrentProjection.uniformSphere, OAI.CurrentProjection.shannonEntropy, OAI.CurrentProjection.PositiveMessage

  73. theorem OAI.CurrentProjection.actualRowSourceRefinement Challenge statement: Gaussian replacement and information bounds sorry line 489

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/GaussianReplacement/ConditionalInfo.lean:365 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.actualRowSourceRefinement@path.

    theorem actualRowSourceRefinement {d m : ℕ} {W E : Type*} [MeasurableSpace W]
    [MeasurableSpace E] [Countable W] [MeasurableSingletonClass W]
    [Countable E] [MeasurableSingletonClass E]
    (P : Measure ((Sphere d×W)×Rows m d)) [IsProbabilityMeasure P]
    (ν : Measure (Sphere d)) [IsProbabilityMeasure ν]
    (hInd : (P.map swapLast).fst = ν.prod (gaussianRows m d))
    (e : Sphere d×W → E) (he : Measurable e)
    (hEntropy : shannonEntropy
      ((P.map (fun p => ((p.1.1,(p.1.2,e p.1)),p.2))).map swapLast).snd ≠ ∞) :
    actualConditionalRowInformation (P.map (fun p => ((p.1.1,(p.1.2,e p.1)),p.2))) =
      actualConditionalRowInformation P := by
…

    Mentions: OAI.CurrentProjection.Sphere, OAI.CurrentProjection.Rows, OAI.CurrentProjection.swapLast, OAI.CurrentProjection.gaussianRows, OAI.CurrentProjection.shannonEntropy, OAI.CurrentProjection.actualConditionalRowInformation

  74. theorem OAI.CurrentProjection.criticalComparisonMain Challenge statement: Gaussian replacement and information bounds sorry line 502

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/GaussianReplacement/Comparison.lean:197 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.criticalComparisonMain@path.

    theorem criticalComparisonMain : CriticalComparisonMain := by
…

    Mentions: OAI.CurrentProjection.CriticalComparisonMain

  75. theorem OAI.CurrentProjection.oneLevelComparisonMain Challenge statement: Gaussian replacement and information bounds sorry line 505

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/GaussianReplacement/Comparison.lean:286 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.oneLevelComparisonMain@path.

    theorem oneLevelComparisonMain : OneLevelComparisonMain := by
…

    Mentions: OAI.CurrentProjection.OneLevelComparisonMain

  76. theorem OAI.CurrentProjection.twoLabelComparisonMain Challenge statement: Gaussian replacement and information bounds sorry line 508

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/GaussianReplacement/Comparison.lean:325 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.twoLabelComparisonMain@path.

    theorem twoLabelComparisonMain : TwoLabelComparisonMain := by
…

    Mentions: OAI.CurrentProjection.TwoLabelComparisonMain

  77. theorem OAI.CurrentProjection.hybridBlockMain Challenge statement: Gaussian replacement and information bounds sorry line 511

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/GaussianReplacement/Hybrid.lean:97 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.hybridBlockMain@path.

    theorem hybridBlockMain : HybridBlockMain := by
…

    Mentions: OAI.CurrentProjection.HybridBlockMain

  78. theorem OAI.CurrentProjection.fiberTwoPointMain Challenge statement: Gaussian replacement and information bounds sorry line 514

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/GaussianReplacement/FiberEquality.lean:141 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.fiberTwoPointMain@path.

    theorem fiberTwoPointMain : FiberTwoPointMain := by
…

    Mentions: OAI.CurrentProjection.FiberTwoPointMain

  79. theorem OAI.CurrentProjection.fiberBlockMain Challenge statement: Gaussian replacement and information bounds sorry line 517

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

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/GaussianReplacement/FiberBlock.lean:74 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.fiberBlockMain@path.

    theorem fiberBlockMain : FiberBlockMain := by
…

    Mentions: OAI.CurrentProjection.FiberBlockMain