OAI.MemoryPrecision.Kernel.source_cube_success: intermediate lemma from OpenAI, Memory and precision in noiseless Gaussian regression

Proved

OAI.MemoryPrecision.Kernel.source_cube_success

by dbenbenn · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

openai-math

An intermediate lemma of the split of OpenAI's proof of OAI.MemoryPrecision.main, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, Memory and precision in noiseless Gaussian regression, OpenAI Math Release, September 27, 2026, result family 140, github.com/openai/math, Apache License 2.0); in Lean it is the declaration OAI.MemoryPrecision.Kernel.source_cube_success of lean/OAI/Probability/MemoryPrecision/CubeSuccess.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.MemoryPrecision.Kernel, with open MeasureTheory ProbabilityTheory Set Filter EuclideanGeometry, open scoped ENNReal NNReal RealInnerProductSpace Topology Pointwise, open MeasureTheory ProbabilityTheory Set Filter, open scoped ENNReal NNReal RealInnerProductSpace Topology Pointwise, open MemoryPrecision NoiselessRegression Policy):

theorem source_cube_success : SourceCubeStatement

Definitions. The statement is written with OAI.MemoryPrecision.Kernel.SourceCubeStatement (definitions bundle OAIQ1Mp000 of this split).

Used by. The proof of OAI.MemoryPrecision.main of this split imports it.

Preamble

import Mathlib
import Definitions.Def_OAIQ1Mp000

Formal statement

section

set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

open MeasureTheory ProbabilityTheory Set Filter EuclideanGeometry
open scoped ENNReal NNReal RealInnerProductSpace Topology Pointwise

noncomputable section
universe u v

open MeasureTheory ProbabilityTheory Set Filter
open scoped ENNReal NNReal RealInnerProductSpace Topology Pointwise
namespace MemoryPrecision.Kernel
open MemoryPrecision NoiselessRegression Policy

theorem source_cube_success : SourceCubeStatement := by
  sorry
end MemoryPrecision.Kernel

end

end OAI
end

Source

OpenAI, Memory and precision in noiseless Gaussian regression, OpenAI Math Release, September 27, 2026, https://github.com/openai/math (result family 140; paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Memory-and-precision-in-noiseless-Gaussian-regression-September-27-2026/paper.pdf; Apache License 2.0); Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Probability/MemoryPrecision/CubeSuccess.lean (declaration OAI.MemoryPrecision.Kernel.source_cube_success)

View graph