Lean statement

Projection estimates and memory–precision bounds

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorem selected for verification: OAI.MemoryPrecision.main

Lean statement file: MemoryPrecision.leanShow on the mapFamily 140. OpenAI lists this as a main result in its Lean catalogue.

See the closest candidates Who ran the proof-verification program Report a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

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 ρ →    ∀ K : Ω → MemoryPrecision.Kernel.Policy d M T,      MemoryPrecision.Kernel.Policy.ModelAdmissible.{u} K ρ →      MemoryPrecision.Kernel.Policy.Success K ρ        (MemoryPrecision.Kernel.CubePrior (MemoryPrecision.Kernel.cubePrior_dimension hd₀ hd)) ε ≤          min 1 (ENNReal.ofReal            (D^((d/2)*(MemoryPrecision.Kernel.BlockCount T ((d/2)/4)+1)) * ε^((d/2:ℕ)/4:ℝ))) ∧      ((∀ signal : MemoryPrecision.Kernel.Sphere d,        (@OfNat.ofNat ℝ≥0∞ 2          (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance)) /        (@OfNat.ofNat ℝ≥0∞ 3          (@instOfNatAtLeastTwo ℝ≥0∞ 3 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance)) ≤          (∫⁻ observation,            MemoryPrecision.Kernel.Policy.experiment K              (MemoryPrecision.Kernel.Policy.angleTest ε) (signal, observation)            ∂ρ.prod (MemoryPrecision.Kernel.RowLaw d T))) →        c*(d:ℝ)*Real.log (1/ε) ≤ (T:ℝ))) ∧  (∃ C : ℝ, 0 < C ∧ ∃ d₀ : ℕ, 0 < d₀ ∧    ∀ d M T : ℕ, d₀ ≤ d → ∀ ε : ℝ, 0 < ε → ε ≤ 1/10 →    ∀ (Ω : Type u) [MeasurableSpace Ω] (ρ : Measure Ω), IsProbabilityMeasure ρ →    ∀ L : Ω → MemoryPrecision.Kernel.Policy d M T,      MemoryPrecision.Kernel.Policy.Admissible L ρ (MemoryPrecision.Kernel.UniformSphere d) →      MemoryPrecision.Kernel.Policy.Success L ρ (MemoryPrecision.Kernel.UniformSphere d) ε ≤ min 1 (ENNReal.ofReal        ((2*ε*Real.exp (C*(1+(M:ℝ)/(d:ℝ)^2)*(MemoryPrecision.Kernel.BlockCount T ((d-1)/8):ℝ)))^(((d:ℝ)-1)/2)))) := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

abbreviation OAI.MemoryPrecision.Kernel.Vector line 13

abbrev Vector (d : ℕ) := EuclideanSpace ℝ (Fin d)

abbreviation OAI.MemoryPrecision.Kernel.Sphere line 15

abbrev Sphere (d : ℕ) := Metric.sphere (0 : Vector d) 1

abbreviation OAI.MemoryPrecision.Kernel.State line 17
```
abbrev State (M : ℕ) := Fin (2^M)
```
abbreviation OAI.MemoryPrecision.Kernel.Action line 19
```
abbrev Action (M : ℕ) := Bool × State M
```

abbreviation OAI.MemoryPrecision.Kernel.Observations line 21

abbrev Observations (d k : ℕ) := Fin k → (Vector d × ℝ)

abbreviation OAI.MemoryPrecision.Kernel.Rows line 23
```
abbrev Rows (d k : ℕ) := Fin k → Vector d
```

definition OAI.MemoryPrecision.Kernel.UniformSphere line 25

def UniformSphere (d : ℕ) : Measure (Sphere d) :=

Show the remaining 12 lines

  let euclideanGroup : NormedAddCommGroup (Vector d) :=    PiLp.normedAddCommGroup      (@OfNat.ofNat ℝ≥0∞ 2        (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))      (fun _ : Fin d => ℝ)  let euclideanInner := PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ)  let σ := @Measure.toSphere (Vector d) euclideanGroup    (@InnerProductSpace.toNormedSpace ℝ (Vector d) _      euclideanGroup.toSeminormedAddCommGroup euclideanInner) inferInstance    (@volume (Vector d) (@measureSpaceOfInnerProductSpace (Vector d)      euclideanGroup euclideanInner inferInstance inferInstance inferInstance))  (σ Set.univ)⁻¹ • σ

definition OAI.MemoryPrecision.Kernel.RowLaw line 39

def RowLaw (d k : ℕ) : @Measure (Rows d k)    (@MeasurableSpace.pi (Fin k) (fun _ => Vector d)      (fun _ => @WithLp.measurableSpace        (@OfNat.ofNat ℝ≥0∞ 2

Show the remaining 13 lines

          (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))        (Fin d → ℝ) inferInstance)) :=  let euclideanMeasurable := @WithLp.measurableSpace    (@OfNat.ofNat ℝ≥0∞ 2      (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))    (Fin d → ℝ) inferInstance  @Measure.pi (Fin k) (fun _ => Vector d) inferInstance (fun _ => euclideanMeasurable)    (fun _ => @stdGaussian (Vector d)    (PiLp.normedAddCommGroup      (@OfNat.ofNat ℝ≥0∞ 2        (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))      (fun _ : Fin d => ℝ))    (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ)) inferInstance euclideanMeasurable)

definition OAI.MemoryPrecision.Kernel.ObservationReference line 57

def ObservationReference (d : ℕ) : Measure (Vector d × ℝ) :=  (stdGaussian (Vector d)).prod volume

structure OAI.MemoryPrecision.Kernel.Policy line 60

structure Policy (d M T : ℕ) where  initial : Action M → ℝ≥0∞  initial_sum : ∑ a, initial a = 1  transition : ℕ → State M → (Vector d × ℝ) → Action M → ℝ≥0∞  transition_sum : ∀ t j obs, ∑ a, transition t j obs a = 1  output : ℕ → State M → Measure (Sphere d)  output_probability : ∀ t j, IsProbabilityMeasure (output t j)

definition OAI.MemoryPrecision.Kernel.Policy.Completed line 70

def Completed {d M T : ℕ} (K : Policy d M T) : Prop :=  ∀ t j a, AEMeasurable (fun obs => K.transition t j obs a) (ObservationReference d)

definition OAI.MemoryPrecision.Kernel.Policy.eval line 73

def eval {d M T : ℕ} {X : Type*} (K : Policy d M T)    (w : ℕ → State M → X → ℝ≥0∞) (n : ℕ) :    (k : ℕ) → State M → X → Observations d k → ℝ≥0∞  | 0, j, s, _ => w n j s  | k+1, j, s, obs => ∑ a : Action M, K.transition (n+1) j (obs 0) a *      if a.1 then w (n+1) a.2 s else K.eval w (n+1) k a.2 s (Fin.tail obs)

definition OAI.MemoryPrecision.Kernel.Policy.pathValue line 80

def pathValue {d M T : ℕ} {X : Type*} (K : Policy d M T)    (w : ℕ → State M → X → ℝ≥0∞) (s : X) (obs : Observations d T) : ℝ≥0∞ :=  ∑ a : Action M, K.initial a * if a.1 then w 0 a.2 s else K.eval w 0 T a.2 s obs

definition OAI.MemoryPrecision.Kernel.Policy.records line 84

def records {d T : ℕ} (s : Sphere d) (A : Rows d T) : Observations d T :=  fun index => (A index, @inner ℝ (EuclideanSpace ℝ (Fin d))    (@InnerProductSpace.toInner ℝ (EuclideanSpace ℝ (Fin d)) _      (PiLp.seminormedAddCommGroup        (@OfNat.ofNat ℝ≥0∞ 2          (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))        (fun _ : Fin d => ℝ))      (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ))) s.val (A index))

definition OAI.MemoryPrecision.Kernel.Policy.outputTest line 93

def outputTest {d M T : ℕ} (K : Policy d M T) (f : Sphere d × Sphere d → ℝ≥0∞)    (t : ℕ) (j : State M) (s : Sphere d) : ℝ≥0∞ :=  ∫⁻ v, f (s,v) ∂K.output t j

definition OAI.MemoryPrecision.Kernel.Policy.angleTest line 97

def angleTest {d : ℕ} (ε : ℝ)    (point : MemoryPrecision.Kernel.Sphere d × MemoryPrecision.Kernel.Sphere d) : ℝ≥0∞ :=  @ite ℝ≥0∞ (Real.arccos (@inner ℝ (EuclideanSpace ℝ (Fin d))      (@InnerProductSpace.toInner ℝ (EuclideanSpace ℝ (Fin d)) _        (PiLp.seminormedAddCommGroup          (@OfNat.ofNat ℝ≥0∞ 2            (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))          (fun _ : Fin d => ℝ))        (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ)))      point.2.val point.1.val) ≤ ε) (Classical.propDecidable _) 1 0

definition OAI.MemoryPrecision.Kernel.Policy.chordTest line 108

def chordTest {d : ℕ} (ε : ℝ) (x : Sphere d × Sphere d) : ℝ≥0∞ :=  {x : Sphere d × Sphere d | dist x.2.val x.1.val ≤ ε}.indicator (fun _ => 1) x

definition OAI.MemoryPrecision.Kernel.Policy.experiment line 111

def experiment {d M T : ℕ} {Ω : Type u} (K : Ω → Policy d M T)    (f : Sphere d × Sphere d → ℝ≥0∞) (z : Sphere d × (Ω × Rows d T)) : ℝ≥0∞ :=  (K z.2.1).pathValue ((K z.2.1).outputTest f) z.1 (records z.1 z.2.2)

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

structure Admissible {d M T : ℕ} {Ω : Type u} [MeasurableSpace Ω]    (K : Ω → Policy d M T) (ρ : Measure Ω) (π : Measure (Sphere d)) : Prop where  completed : ∀ᵐ ω ∂ρ, (K ω).Completed  experiment : ∀ f : Sphere d × Sphere d → ℝ≥0∞, Measurable f →    (∀ x, f x ≤ 1) → AEMeasurable (experiment K f) (π.prod (ρ.prod (RowLaw d T)))

definition OAI.MemoryPrecision.Kernel.Policy.Success line 121

def Success {d M T : ℕ} {Ω : Type u} [MeasurableSpace Ω]    (K : Ω → Policy d M T) (ρ : Measure Ω) (π : Measure (Sphere d)) (ε : ℝ) : ℝ≥0∞ :=  ∫⁻ z, experiment K (angleTest ε) z ∂π.prod (ρ.prod (RowLaw d T))

definition OAI.MemoryPrecision.Kernel.Policy.ChordSuccess line 125

def ChordSuccess {d M T : ℕ} {Ω : Type u} [MeasurableSpace Ω]    (K : Ω → Policy d M T) (ρ : Measure Ω) (π : Measure (Sphere d)) (ε : ℝ) : ℝ≥0∞ :=  ∫⁻ z, experiment K (chordTest ε) z ∂π.prod (ρ.prod (RowLaw d T))

abbreviation OAI.NoiselessRegression.UnitSphere line 134

abbrev UnitSphere (d : ℕ) := Metric.sphere (0 : Vector d) 1

abbreviation OAI.MemoryPrecision.Space line 140

abbrev Space (d : ℕ) := EuclideanSpace ℝ (Fin d)

definition OAI.MemoryPrecision.J line 142

def J (β : ℝ) (m j : ℕ) : ℝ :=  let two : ℝ := @OfNat.ofNat ℝ 2 (@instOfNatAtLeastTwo ℝ 2 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let three : ℝ := @OfNat.ofNat ℝ 3 (@instOfNatAtLeastTwo ℝ 3 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 1)))  1 + three^j * two^β * (m : ℝ) / (β - (j : ℝ) - (m : ℝ))

38 more definitions are reached the same way; the full file lists them.

No confident match with a paper statement

No paper theorem is paired with this Lean statement.

Why none: no paper statement matches the Lean text clearly enough to pair, so the closest candidates are listed below.

Statements in Memory and precision in noiseless Gaussian regression come first because the Lean file and module names share words with that paper’s title.

Other possible paper matches, closest wording first

Corollary B.8 of Memory and precision in noiseless Gaussian regression. Words of the Lean statement, its names split into words, that also appear in the theorem: second, angle, step, coefficients, d/8, two and 15 more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: resulting.
Proposition A.5 of Memory and precision in noiseless Gaussian regression. Words of the Lean statement, its names split into words, that also appear in the theorem: pointwise, mixture, coordinate, vector, null, unit and ten more.
Proposition 8.3 of Memory and precision in noiseless Gaussian regression. Words of the Lean statement, its names split into words, that also appear in the theorem: min, property, cube, precision, prior, least and eight more.
Corollary 8.2 of Memory and precision in noiseless Gaussian regression. Words of the Lean statement, its names split into words, that also appear in the theorem: coordinate, paired, cube, local, real, prior and two more.
Proposition B.7 of Memory and precision in noiseless Gaussian regression. Words of the Lean statement, its names split into words, that also appear in the theorem: step, d/8, min, initial, d/2, signal and nine more.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

Accepted Their term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

Accepted Their term: “comparator-sandboxed-pass”.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Reported 8 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Classical.choice, Quot.sound

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 140’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

MathVet and cert-machine agree on how much of the advertised result the Lean statements express.

MathVet
Finds the whole advertised result stated or implied Their term: “full”.
The challenge statements imply the headline claim after unpacking definitions or one routine step. Their record
Their note: None for the headline; supporting results are in separate files. The learner model gives the learner a free shared seed at every step (a stronger model, so the lower bound is stronger).
Definitions the group asks readers to compare with the paper: Bespoke finite-memory learner model (Learner, RunStatus, Admissible bundling several AEMeasurable hypotheses, angularError := arccos ⟪ŝ, s⟫, uniformSphere via Measure.toSphere); GaussianInformation.lean also introduces local instance ambientSub/ambientInner re-defining Sub/Inner on EuclideanSpace (supporting file)
Carlos Toledo’s cert-machine
Finds the whole advertised result stated or implied Their term: “MATCHES”.
The challenge statements state the headline as OpenAI wrote it. Their record

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“The linked supporting results include inverse Gram-matrix moments, exact-projection densities, regularization bounds, and sphere- and cube-prior block estimates.”
Quoted from OpenAI’s Lean note for this family

An AI agent drafted an interpretation of that note, classifying this statement as “states a supporting result”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

812 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 348 to its own declarations, 808 to Mathlib’s documentation. 78 declared names also link to the same declaration in OpenAI’s library. 2 identifiers stay plain because they resolve to no single declaration: variables Lean binds automatically, notation, or names the scan of the pinned sources did not find. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAIopen MeasureTheory ProbabilityTheory Set Filter EuclideanGeometryopen scoped ENNReal NNReal RealInnerProductSpace Topology Pointwisenoncomputable sectionuniverse u vnamespace MemoryPrecision.Kernelabbrev Vector (d : ℕ) := EuclideanSpace ℝ (Fin d)abbrev Sphere (d : ℕ) := Metric.sphere (0 : Vector d) 1abbrev State (M : ℕ) := Fin (2^M)abbrev Action (M : ℕ) := Bool × State Mabbrev Observations (d k : ℕ) := Fin k → (Vector d × ℝ)abbrev Rows (d k : ℕ) := Fin k → Vector ddef UniformSphere (d : ℕ) : Measure (Sphere d) :=  let euclideanGroup : NormedAddCommGroup (Vector d) :=    PiLp.normedAddCommGroup      (@OfNat.ofNat ℝ≥0∞ 2        (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))      (fun _ : Fin d => ℝ)  let euclideanInner := PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ)  let σ := @Measure.toSphere (Vector d) euclideanGroup    (@InnerProductSpace.toNormedSpace ℝ (Vector d) _      euclideanGroup.toSeminormedAddCommGroup euclideanInner) inferInstance    (@volume (Vector d) (@measureSpaceOfInnerProductSpace (Vector d)      euclideanGroup euclideanInner inferInstance inferInstance inferInstance))  (σ Set.univ)⁻¹ • σdef RowLaw (d k : ℕ) : @Measure (Rows d k)    (@MeasurableSpace.pi (Fin k) (fun _ => Vector d)      (fun _ => @WithLp.measurableSpace        (@OfNat.ofNat ℝ≥0∞ 2          (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))        (Fin d → ℝ) inferInstance)) :=  let euclideanMeasurable := @WithLp.measurableSpace    (@OfNat.ofNat ℝ≥0∞ 2      (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))    (Fin d → ℝ) inferInstance  @Measure.pi (Fin k) (fun _ => Vector d) inferInstance (fun _ => euclideanMeasurable)    (fun _ => @stdGaussian (Vector d)    (PiLp.normedAddCommGroup      (@OfNat.ofNat ℝ≥0∞ 2        (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))      (fun _ : Fin d => ℝ))    (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ)) inferInstance euclideanMeasurable)def ObservationReference (d : ℕ) : Measure (Vector d × ℝ) :=  (stdGaussian (Vector d)).prod volumestructure Policy (d M T : ℕ) where  initial : Action M → ℝ≥0∞  initial_sum : ∑ a, initial a = 1  transition : ℕ → State M → (Vector d × ℝ) → Action M → ℝ≥0∞  transition_sum : ∀ t j obs, ∑ a, transition t j obs a = 1  output : ℕ → State M → Measure (Sphere d)  output_probability : ∀ t j, IsProbabilityMeasure (output t j)namespace Policydef Completed {d M T : ℕ} (K : Policy d M T) : Prop :=  ∀ t j a, AEMeasurable (fun obs => K.transition t j obs a) (ObservationReference d)def eval {d M T : ℕ} {X : Type*} (K : Policy d M T)    (w : ℕ → State M → X → ℝ≥0∞) (n : ℕ) :    (k : ℕ) → State M → X → Observations d k → ℝ≥0∞  | 0, j, s, _ => w n j s  | k+1, j, s, obs => ∑ a : Action M, K.transition (n+1) j (obs 0) a *      if a.1 then w (n+1) a.2 s else K.eval w (n+1) k a.2 s (Fin.tail obs)def pathValue {d M T : ℕ} {X : Type*} (K : Policy d M T)    (w : ℕ → State M → X → ℝ≥0∞) (s : X) (obs : Observations d T) : ℝ≥0∞ :=  ∑ a : Action M, K.initial a * if a.1 then w 0 a.2 s else K.eval w 0 T a.2 s obsdef records {d T : ℕ} (s : Sphere d) (A : Rows d T) : Observations d T :=  fun index => (A index, @inner ℝ (EuclideanSpace ℝ (Fin d))    (@InnerProductSpace.toInner ℝ (EuclideanSpace ℝ (Fin d)) _      (PiLp.seminormedAddCommGroup        (@OfNat.ofNat ℝ≥0∞ 2          (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))        (fun _ : Fin d => ℝ))      (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ))) s.val (A index))def outputTest {d M T : ℕ} (K : Policy d M T) (f : Sphere d × Sphere d → ℝ≥0∞)    (t : ℕ) (j : State M) (s : Sphere d) : ℝ≥0∞ :=  ∫⁻ v, f (s,v) ∂K.output t jdef angleTest {d : ℕ} (ε : ℝ)    (point : MemoryPrecision.Kernel.Sphere d × MemoryPrecision.Kernel.Sphere d) : ℝ≥0∞ :=  @ite ℝ≥0∞ (Real.arccos (@inner ℝ (EuclideanSpace ℝ (Fin d))      (@InnerProductSpace.toInner ℝ (EuclideanSpace ℝ (Fin d)) _        (PiLp.seminormedAddCommGroup          (@OfNat.ofNat ℝ≥0∞ 2            (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance))          (fun _ : Fin d => ℝ))        (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ)))      point.2.val point.1.val) ≤ ε) (Classical.propDecidable _) 1 0def chordTest {d : ℕ} (ε : ℝ) (x : Sphere d × Sphere d) : ℝ≥0∞ :=  {x : Sphere d × Sphere d | dist x.2.val x.1.val ≤ ε}.indicator (fun _ => 1) xdef experiment {d M T : ℕ} {Ω : Type u} (K : Ω → Policy d M T)    (f : Sphere d × Sphere d → ℝ≥0∞) (z : Sphere d × (Ω × Rows d T)) : ℝ≥0∞ :=  (K z.2.1).pathValue ((K z.2.1).outputTest f) z.1 (records z.1 z.2.2)structure Admissible {d M T : ℕ} {Ω : Type u} [MeasurableSpace Ω]    (K : Ω → Policy d M T) (ρ : Measure Ω) (π : Measure (Sphere d)) : Prop where  completed : ∀ᵐ ω ∂ρ, (K ω).Completed  experiment : ∀ f : Sphere d × Sphere d → ℝ≥0∞, Measurable f →    (∀ x, f x ≤ 1) → AEMeasurable (experiment K f) (π.prod (ρ.prod (RowLaw d T)))def Success {d M T : ℕ} {Ω : Type u} [MeasurableSpace Ω]    (K : Ω → Policy d M T) (ρ : Measure Ω) (π : Measure (Sphere d)) (ε : ℝ) : ℝ≥0∞ :=  ∫⁻ z, experiment K (angleTest ε) z ∂π.prod (ρ.prod (RowLaw d T))def ChordSuccess {d M T : ℕ} {Ω : Type u} [MeasurableSpace Ω]    (K : Ω → Policy d M T) (ρ : Measure Ω) (π : Measure (Sphere d)) (ε : ℝ) : ℝ≥0∞ :=  ∫⁻ z, experiment K (chordTest ε) z ∂π.prod (ρ.prod (RowLaw d T))end Policyend MemoryPrecision.Kernelnamespace NoiselessRegressionabbrev Vector (d : ℕ) := EuclideanSpace ℝ (Fin d)abbrev UnitSphere (d : ℕ) := Metric.sphere (0 : Vector d) 1end NoiselessRegressionnamespace MemoryPrecisionopen NoiselessRegressionabbrev Space (d : ℕ) := EuclideanSpace ℝ (Fin d)def J (β : ℝ) (m j : ℕ) : ℝ :=  let two : ℝ := @OfNat.ofNat ℝ 2 (@instOfNatAtLeastTwo ℝ 2 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let three : ℝ := @OfNat.ofNat ℝ 3 (@instOfNatAtLeastTwo ℝ 3 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 1)))  1 + three^j * two^β * (m : ℝ) / (β - (j : ℝ) - (m : ℝ))def AmbientBallBound {d : ℕ} (μ : Measure (Space d)) (H β : ℝ) : Prop :=  ∀ x : Space d, ∀ r : ℝ, 0 < r →    μ (Metric.closedBall x r) ≤ ENNReal.ofReal (H * r^β)def InverseGram {d p : ℕ} (m : ℕ) (v : Space d × (Fin (p-1) → Space d)) : ℝ≥0∞ :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  letI : AddCommGroup (Space d) := WithLp.instAddCommGroup exponent (Fin d → ℝ)  letI : Inner ℝ (Space d) := @InnerProductSpace.toInner ℝ (Space d) _    (PiLp.seminormedAddCommGroup exponent (fun _ : Fin d => ℝ))    (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ))  ENNReal.ofReal ((Real.sqrt (Matrix.gram ℝ (fun i => v.2 i - v.1)).det)⁻¹ ^ m)def MatrixLabelReference (d m : ℕ) : @Measure ((Fin m → Space d) × (Fin m → ℝ))    (@MeasurableSpace.prod (Fin m → Space d) (Fin m → ℝ)      (@MeasurableSpace.pi (Fin m) (fun _ => Space d)        (fun _ => WithLp.measurableSpace          (@OfNat.ofNat ℝ≥0∞ 2            (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast              (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))) (Fin d → ℝ)))      inferInstance) :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let euclideanMeasurable := WithLp.measurableSpace exponent (Fin d → ℝ)  let rowMeasurable := @MeasurableSpace.pi (Fin m) (fun _ => Space d)    (fun _ => euclideanMeasurable)  let rowLaw := @Measure.pi (Fin m) (fun _ => Space d) inferInstance    (fun _ => euclideanMeasurable)    (fun _ => @stdGaussian (Space d)      (PiLp.normedAddCommGroup exponent (fun _ : Fin d => ℝ))      (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ))      inferInstance euclideanMeasurable)  @Measure.prod _ _ rowMeasurable inferInstance rowLaw volumedef ProjectionLaw {d : ℕ}    (μ : @Measure (Space d)      (WithLp.measurableSpace        (@OfNat.ofNat ℝ≥0∞ 2          (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast            (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))) (Fin d → ℝ)))    (m : ℕ) : @Measure ((Fin m → Space d) × (Fin m → ℝ))      (@MeasurableSpace.prod (Fin m → Space d) (Fin m → ℝ)        (@MeasurableSpace.pi (Fin m) (fun _ => Space d)          (fun _ => WithLp.measurableSpace            (@OfNat.ofNat ℝ≥0∞ 2              (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast                (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))) (Fin d → ℝ)))        inferInstance) :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let euclideanMeasurable := WithLp.measurableSpace exponent (Fin d → ℝ)  let rowMeasurable := @MeasurableSpace.pi (Fin m) (fun _ => Space d)    (fun _ => euclideanMeasurable)  let rowLaw := @Measure.pi (Fin m) (fun _ => Space d) inferInstance    (fun _ => euclideanMeasurable)    (fun _ => @stdGaussian (Space d)      (PiLp.normedAddCommGroup exponent (fun _ : Fin d => ℝ))      (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ))      inferInstance euclideanMeasurable)  @Measure.map ((Fin m → Space d) × Space d) ((Fin m → Space d) × (Fin m → ℝ))    (@MeasurableSpace.prod _ _ rowMeasurable euclideanMeasurable)    (@MeasurableSpace.prod _ _ rowMeasurable inferInstance)    (fun pair => (pair.1, fun index => @inner ℝ (Space d)      (@InnerProductSpace.toInner ℝ (Space d) _        (PiLp.seminormedAddCommGroup exponent (fun _ : Fin d => ℝ))        (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ)))      pair.2 (pair.1 index)))    (@Measure.prod _ _ rowMeasurable euclideanMeasurable rowLaw μ)def ProjectedEllipsoid {d m : ℕ} (z : Space d) (R : ℝ) :    Set ((Fin m → Space d) × (Fin m → ℝ)) :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let euclideanInner := @InnerProductSpace.toInner ℝ (Space d) _    (PiLp.seminormedAddCommGroup exponent (fun _ : Fin d => ℝ))    (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ))  {pair | ∃ displacement ∈ @Metric.closedBall (Space d)      (PiLp.instPseudoMetricSpace (p := exponent) (β := fun _ : Fin d => ℝ))      (WithLp.toLp exponent (fun _ => (0 : ℝ))) R,    pair.2 = fun index => @inner ℝ (Space d) euclideanInner z (pair.1 index) +      @inner ℝ (Space d) euclideanInner displacement (pair.1 index)}def ProjectionNormScale (m p : ℕ) (H β R : ℝ) : ℝ :=  let two : ℝ := @OfNat.ofNat ℝ 2 (@instOfNatAtLeastTwo ℝ 2 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  (two * Real.pi) ^ (-(m : ℝ) * ((p : ℝ)-1) / (two*(p : ℝ))) * H *    R ^ (β - (m : ℝ)*(1-1/(p : ℝ))) *    (∏ j ∈ Finset.range (p-1), J β m j) ^ (1/(p : ℝ))def UniformSphere (d : ℕ) : @Measure (Space d)    (WithLp.measurableSpace      (@OfNat.ofNat ℝ≥0∞ 2        (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast          (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))) (Fin d → ℝ)) :=  let euclideanMeasurable := WithLp.measurableSpace    (@OfNat.ofNat ℝ≥0∞ 2      (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast        (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))) (Fin d → ℝ)  @Measure.map (Kernel.Sphere d) (Space d)    (MeasurableSpace.comap Subtype.val euclideanMeasurable) euclideanMeasurable    Subtype.val (Kernel.UniformSphere d)def GaussianRegularization {d : ℕ}    (μ : @Measure (Space d)      (WithLp.measurableSpace        (@OfNat.ofNat ℝ≥0∞ 2          (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast            (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))) (Fin d → ℝ)))    (m : ℕ) (δ : ℝ)    (Ay : (Fin m → Space d) × (Fin m → ℝ)) : ℝ :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  letI : MeasurableSpace (Space d) := WithLp.measurableSpace exponent (Fin d → ℝ)  ∫ signal, ∏ index, gaussianPDFReal 0 ⟨δ^2, sq_nonneg δ⟩    (Ay.2 index - @inner ℝ (Space d)      (@InnerProductSpace.toInner ℝ (Space d) _        (PiLp.seminormedAddCommGroup exponent (fun _ : Fin d => ℝ))        (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ)))      signal (Ay.1 index)) ∂μdef PointwiseDensity {d : ℕ} (μ : Measure (Space d)) (m : ℕ)    (x : (Fin m → Space d) × (Fin m → ℝ)) : ℝ := by  classical  exact if h : ∃ l : ℝ, Tendsto (fun i : ℕ => GaussianRegularization μ m (1/(i:ℝ)) x)      atTop (𝓝 l) then Classical.choose h else 0lemma space_finiteDimensional (d : ℕ) : FiniteDimensional ℝ (Space d) := by  infer_instancedef UnitBallVolume (m : ℕ) : ℝ :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let euclideanGroup := PiLp.normedAddCommGroup exponent (fun _ : Fin m => ℝ)  letI : MeasurableSpace (Space m) := WithLp.measurableSpace exponent (Fin m → ℝ)  let euclideanVolume := @volume (Space m) (@measureSpaceOfInnerProductSpace (Space m)    euclideanGroup (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin m => ℝ))    (space_finiteDimensional m) inferInstance inferInstance)  (euclideanVolume (@Metric.ball (Space m)    (PiLp.instPseudoMetricSpace (p := exponent) (β := fun _ : Fin m => ℝ))    (WithLp.toLp exponent (fun _ : Fin m => (0 : ℝ))) 1)).toRealdef CoordinateUnit (m : ℕ) : Space m :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  WithLp.toLp exponent (fun j : Fin m => if (j:ℕ) = 0 then (1:ℝ) else 0)lemma gaussianVariance_nonneg (δ : ℝ) : 0 ≤ δ^2 := sq_nonneg δdef GaussianKernel (m : ℕ) (δ : ℝ) (y : Space m) : ℝ :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  ∏ index, gaussianPDFReal 0 ⟨δ^2, gaussianVariance_nonneg δ⟩    (@WithLp.ofLp exponent (Fin m → ℝ) y index)def RadialMixture (m : ℕ) (δ r : ℝ) : ℝ :=  UnitBallVolume m * r^m * (r / δ^2) * GaussianKernel m δ (r • CoordinateUnit m)abbrev Sphere (d : ℕ) := Metric.sphere (0 : Space d) 1def SpherePrior (d : ℕ) : Measure (Sphere d) :=  MemoryPrecision.Kernel.UniformSphere ddef SphereBallBound {d : ℕ} (h : Sphere d → ℝ≥0∞) (H α : ℝ) : Prop :=  ∀ z : Space d, ∀ r : ℝ, 0 < r →    (∫⁻ s in {s : Sphere d | dist s.val z ≤ r}, h s ∂SpherePrior d) ≤      ENNReal.ofReal (H * r^α)section WeightedImagevariable {X : Type*} [MeasurableSpace X] {d m N : ℕ}def WeightedBlock (ι : X → Space d) (h : Fin N → X → ℝ≥0∞)    (g : Fin N → ((Fin m → Space d) × (Fin m → ℝ)) → ℝ≥0∞) (x : X) : ℝ≥0∞ :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let euclideanMeasurable := @WithLp.measurableSpace exponent (Fin d → ℝ) inferInstance  let rowMeasurable := @MeasurableSpace.pi (Fin m) (fun _ => Space d)    (fun _ => euclideanMeasurable)  @MeasureTheory.lintegral (Fin m → Space d) rowMeasurable    (@Measure.pi (Fin m) (fun _ => Space d) inferInstance (fun _ => euclideanMeasurable)      (fun _ => @stdGaussian (Space d)        (PiLp.normedAddCommGroup exponent (fun _ : Fin d => ℝ))        (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ))        (space_finiteDimensional d) euclideanMeasurable))    (fun rows => ∑ state, g state (rows, fun index => @inner ℝ (Space d)      (@InnerProductSpace.toInner ℝ (Space d) _        (PiLp.seminormedAddCommGroup exponent (fun _ : Fin d => ℝ))        (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ)))      (ι x) (rows index)) * h state x)end WeightedImagedef SphereBlock {d m N : ℕ} (h : Fin N → Sphere d → ℝ≥0∞)    (g : Fin N → ((Fin m → Space d) × (Fin m → ℝ)) → ℝ≥0∞)    (s : Sphere d) : ℝ≥0∞ :=  WeightedBlock Subtype.val h g sabbrev CubeSet (n : ℕ) : Set (EuclideanSpace ℝ (Fin n)) :=  fun (point : EuclideanSpace ℝ (Fin n)) => ∀ index : Fin n,    @LE.le ℝ Real.instLE      (@abs ℝ Real.lattice Real.instAddGroup        (@WithLp.ofLp          (@OfNat.ofNat ℝ≥0∞ 2            (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast              (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0))))          (Fin n → ℝ) point index))      (@HDiv.hDiv ℝ ℝ ℝ (@instHDiv ℝ Real.instDivInvMonoid.toDiv)        (@OfNat.ofNat ℝ 1 (@One.toOfNat1 ℝ Real.instOne))        (@OfNat.ofNat ℝ 2 (@instOfNatAtLeastTwo ℝ 2 Real.commRing.toNatCast          (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))))abbrev Cube (d : ℕ) := CubeSet (d/2)def CubeLaw (d : ℕ) : Measure (Cube d) :=  (volume : Measure (Space (d/2))).comap Subtype.vallemma cube_second_coordinate_lt (d : ℕ) (index : Fin d)    (lower : ¬index.val < d/2) (upper : index.val < 2*(d/2)) :    index.val - d/2 < d/2 := by omegadef cubeRaw (d : ℕ) (u : Space (d/2)) : Space d :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  @HSMul.hSMul ℝ (Space d) (Space d)    (@instHSMul ℝ (Space d) (WithLp.instSMul exponent ℝ (Fin d → ℝ)))    (Real.sqrt (d/2:ℕ))⁻¹ (WithLp.toLp exponent (fun index : Fin d =>      if lower : index.val < d/2 then        @WithLp.ofLp exponent (Fin (d/2) → ℝ) u ⟨index.val, lower⟩      else if upper : index.val < 2*(d/2) then        Real.sqrt (1-(@WithLp.ofLp exponent (Fin (d/2) → ℝ) u          ⟨index.val-d/2, cube_second_coordinate_lt d index lower upper⟩)^2)      else 0))def CubeEmbedding (d : ℕ) (u : Cube d) : Space d := cubeRaw d u.valdef CubeBall (d : ℕ) (z : Space (d/2)) (r : ℝ) : Set (Cube d) :=  {u | dist u.val z ≤ Real.sqrt (d/2:ℕ) * r}def CubeLocal {d : ℕ} (f : Cube d → ℝ≥0∞) (L : ℝ) : Prop :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let cubeMeasurable := @Subtype.instMeasurableSpace (Space (d/2)) (CubeSet (d/2))    (@WithLp.measurableSpace exponent (Fin (d/2) → ℝ) inferInstance)  ∀ z : Space (d/2), ∀ r : ℝ, 0 < r →    @MeasureTheory.lintegral (Cube d) cubeMeasurable      (@Measure.restrict (Cube d) cubeMeasurable (CubeLaw d) (CubeBall d z r)) f ≤      ENNReal.ofReal (L * r^(        (@OfNat.ofNat ℝ 3 (@instOfNatAtLeastTwo ℝ 3 Real.commRing.toNatCast          (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 1)))) * (d/2:ℕ) /        (@OfNat.ofNat ℝ 4 (@instOfNatAtLeastTwo ℝ 4 Real.commRing.toNatCast          (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 2)))) : ℝ))/-- Every coordinate of the paired cube has square at most one quarter. -/lemma cube_coordinate_square_le {d : ℕ} (u : Cube d) (i : Fin (d/2)) : u.val i^2 ≤ 1/4 := by  have hu : -(1/2 : ℝ) ≤ u.val i ∧ u.val i ≤ 1/2 := abs_le.mp (u.property i)  nlinarith [sq_nonneg (u.val i-1/2), sq_nonneg (u.val i+1/2)]lemma sum_fin_split {n d : ℕ} (hn : n ≤ d) (f : Fin d → ℝ) :    (∑ i, f i) = (∑ i : Fin n, f ⟨i.val,by omega⟩) +      ∑ i : Fin (d-n), f ⟨n+i.val,by omega⟩ := by  let e : Fin (n+(d-n)) ≃ Fin d := finCongr (Nat.add_sub_of_le hn)  calc    _ = ∑ i : Fin (n+(d-n)), f (e i) := (Equiv.sum_comp e f).symm    _ = _ := by rw [Fin.sum_univ_add]; rfldef cubeCoords (d : ℕ) (u : Space (d/2)) : Space d :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  WithLp.toLp exponent (fun index : Fin d =>    if lower : index.val < d/2 then      @WithLp.ofLp exponent (Fin (d/2) → ℝ) u ⟨index.val, lower⟩    else if upper : index.val < 2*(d/2) then      Real.sqrt (1-(@WithLp.ofLp exponent (Fin (d/2) → ℝ) u        ⟨index.val-d/2, cube_second_coordinate_lt d index lower upper⟩)^2)    else 0)lemma cubeCoords_first (d : ℕ) (u : Space (d/2)) (i : Fin (d/2)) :    cubeCoords d u ⟨i.val,by omega⟩ = u i := by  simp [cubeCoords, i.isLt]lemma cubeCoords_second (d : ℕ) (u : Space (d/2)) (i : Fin (d/2)) :    cubeCoords d u ⟨d/2+i.val,by omega⟩ = Real.sqrt (1-u i^2) := by  simp [cubeCoords, show ¬d/2+i.val < d/2 by omega, show d/2+i.val < 2*(d/2) by omega]lemma cubeCoords_tail (d : ℕ) (u : Space (d/2)) (i : Fin d) (hi : 2*(d/2) ≤ i.val) :    cubeCoords d u i = 0 := by  simp [cubeCoords, show ¬i.val < d/2 by omega, show ¬i.val < 2*(d/2) by omega]lemma cubeCoords_sum (d : ℕ) (u : Space (d/2)) (f : ℝ → ℝ) (hf : f 0 = 0) :    (∑ i : Fin d, f (cubeCoords d u i)) =      (∑ i : Fin (d/2), f (u i)) + ∑ i : Fin (d/2), f (Real.sqrt (1-u i^2)) := by  rw [sum_fin_split (show d/2 ≤ d by omega)]  simp_rw [cubeCoords_first]  rw [sum_fin_split (show d/2 ≤ d-d/2 by omega)]  congr 1  have h1 : (∑ i : Fin (d/2), f (cubeCoords d u ⟨d/2+i.val,by omega⟩)) =      ∑ i : Fin (d/2), f (Real.sqrt (1-u i^2)) := by simp_rw [cubeCoords_second]  rw [h1]  have h0 : (∑ i : Fin (d-d/2-d/2), f (cubeCoords d u ⟨d/2+(d/2+i.val),by omega⟩)) = 0 := by    apply Finset.sum_eq_zero    intro i _    rw [cubeCoords_tail d u _ (show 2*(d/2) ≤ d/2+(d/2+i.val) by omega), hf]  rw [h0, add_zero]lemma cubeEmbedding_norm {d : ℕ} (hd : 2 ≤ d) (u : Cube d) :    @Norm.norm (Space d) (PiLp.instNorm      (p := @OfNat.ofNat ℝ≥0∞ 2        (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast          (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))) (β := fun _ : Fin d => ℝ))      (CubeEmbedding d u) = (1 : ℝ) := by  have hs : ‖cubeCoords d u.val‖^2 = (d/2:ℕ) := by    rw [EuclideanSpace.real_norm_sq_eq, cubeCoords_sum d u.val (fun x => x^2) (by norm_num)]    have he (i : Fin (d/2)) : Real.sqrt (1-u.val i^2)^2 = 1-u.val i^2 :=      Real.sq_sqrt (by have := cube_coordinate_square_le u i; linarith)    simp_rw [he]    rw [← Finset.sum_add_distrib]    simp  have hn : 0 < (d/2:ℕ) := by omega  have hr : 0 < Real.sqrt (d/2:ℕ) := Real.sqrt_pos.2 (by exact_mod_cast hn)  have hnorm : ‖cubeCoords d u.val‖ = Real.sqrt (d/2:ℕ) := by    rw [← Real.sqrt_sq (norm_nonneg _), hs]  change ‖(Real.sqrt (d/2:ℕ))⁻¹ • cubeCoords d u.val‖ = 1  rw [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_pos hr, hnorm, inv_mul_cancel₀ hr.ne']def CubeSphere {d : ℕ} (hd : 2 ≤ d) (u : Cube d) : UnitSphere d :=  ⟨CubeEmbedding d u, by simpa [Metric.mem_sphere, dist_zero_right] using cubeEmbedding_norm hd u⟩def AmbientGramStatement : Prop :=  let two : ℝ := @OfNat.ofNat ℝ 2 (@instOfNatAtLeastTwo ℝ 2 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let three : ℝ := @OfNat.ofNat ℝ 3 (@instOfNatAtLeastTwo ℝ 3 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 1)))  let four : ℝ := @OfNat.ofNat ℝ 4 (@instOfNatAtLeastTwo ℝ 4 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 2)))  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  (∀ (d m p : ℕ),    letI : MeasurableSpace (Space d) := WithLp.measurableSpace exponent (Fin d → ℝ)    letI : PseudoMetricSpace (Space d) :=      PiLp.instPseudoMetricSpace (p := exponent) (β := fun _ : Fin d => ℝ)    letI : AddCommGroup (Space d) := WithLp.instAddCommGroup exponent (Fin d → ℝ)    letI : Module ℝ (Space d) := WithLp.instModule (p := exponent) (K := ℝ) (V := Fin d → ℝ)    1 ≤ d → 1 ≤ m → 2 ≤ p →    ∀ β R H : ℝ, (m : ℝ) + (p : ℝ) - two < β → 0 < R → 0 < H →    ∀ (μ : Measure (Space d)), IsFiniteMeasure μ →    ∀ z : Space d, μ.support ⊆ Metric.closedBall z R →    AmbientBallBound μ H β →    (∀ (j : ℕ), j ≤ p-2 → ∀ L : AffineSubspace ℝ (Space d),      Nonempty L → Module.finrank ℝ L.direction = j →      (∀ t : ℝ, 0 < t → t ≤ R →        μ {s | Metric.infDist s L ≤ t} ≤          ENNReal.ofReal (three^j * two^β * H * R^j * t^(β-(j:ℝ)))) ∧      (∫⁻ s, (ENNReal.ofReal (Metric.infDist s L)) ^ (-(m:ℝ)) ∂μ) ≤        ENNReal.ofReal (J β m j * H * R^(β-(m:ℝ)))) ∧    (∀ᵐ v : Space d × (Fin (p-1) → Space d)      ∂μ.prod (Measure.pi (fun _ : Fin (p-1) => μ)),      LinearIndependent ℝ (fun i => v.2 i - v.1)) ∧    (∫⁻ v : Space d × (Fin (p-1) → Space d), InverseGram m v      ∂μ.prod (Measure.pi (fun _ : Fin (p-1) => μ))) ≤      ENNReal.ofReal (H^p * R^(β*(p:ℝ)-(m:ℝ)*(p-1:ℕ)) *        ∏ j : Fin (p-1), J β m j)) ∧  (∃ C : ℝ, 1 ≤ C ∧ ∀ (d m p : ℕ), 16 ≤ d → p = d/8 →    1 ≤ m → m ≤ p → ∀ β : ℝ, ((d:ℝ)-1)/two ≤ β → β ≤ (d:ℝ)/two →    (∀ j : ℕ, j ≤ p-2 →      ((d:ℝ)-1)/two - two*(p:ℝ) + two ≤ β-(j:ℝ)-(m:ℝ) ∧      (d:ℝ)/four + three/two ≤ ((d:ℝ)-1)/two - two*(p:ℝ) + two ∧      J β m j ≤ C^d) ∧    (∀ H R : ℝ, 0 < H → 0 < R →      H^p * R^(β*(p:ℝ)-(m:ℝ)*(p-1:ℕ)) * (∏ j : Fin (p-1), J β m j) ≤        C^(d*(p-1)) * H^p * R^(β*(p:ℝ)-(m:ℝ)*(p-1:ℕ))))def FiniteDensityStatement : Prop :=  let two : ℝ := @OfNat.ofNat ℝ 2 (@instOfNatAtLeastTwo ℝ 2 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  ∀ d m p : ℕ,  letI : MeasurableSpace (Space d) := WithLp.measurableSpace exponent (Fin d → ℝ)  1 ≤ d → 1 ≤ m → 2 ≤ p →  ∀ β H R : ℝ, (m : ℝ)+(p : ℝ)-two < β → 0 < H → 0 < R →  ∀ z : Space d, ∀ μ : Measure (Space d), IsFiniteMeasure μ →    @Measure.support (Space d)      (PiLp.topologicalSpace (p := exponent) (β := fun _ : Fin d => ℝ))      (WithLp.measurableSpace exponent (Fin d → ℝ)) μ ⊆      @Metric.closedBall (Space d)        (PiLp.instPseudoMetricSpace (p := exponent) (β := fun _ : Fin d => ℝ)) z R →    AmbientBallBound μ H β →    ∃ F : ((Fin m → Space d) × (Fin m → ℝ)) → ℝ,      Measurable F ∧ (∀ x, 0 ≤ F x) ∧      (MatrixLabelReference d m).withDensity (fun x => ENNReal.ofReal (F x)) =        ProjectionLaw μ m ∧      (∀ᵐ x ∂MatrixLabelReference d m, x ∉ ProjectedEllipsoid z R → F x = 0) ∧      eLpNorm F (p : ℝ≥0∞) (MatrixLabelReference d m) ≤        ENNReal.ofReal (ProjectionNormScale m p H β R)def MeasurableTestStatement : Prop :=  let two : ℝ := @OfNat.ofNat ℝ 2 (@instOfNatAtLeastTwo ℝ 2 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  ∀ d m p : ℕ,  letI : MeasurableSpace (Space d) := WithLp.measurableSpace exponent (Fin d → ℝ)  1 ≤ d → 1 ≤ m → 2 ≤ p →  ∀ β H R : ℝ, (m : ℝ)+(p : ℝ)-two < β → 0 < H → 0 < R →  ∀ z : Space d, ∀ μ : Measure (Space d), IsFiniteMeasure μ →    @Measure.support (Space d)      (PiLp.topologicalSpace (p := exponent) (β := fun _ : Fin d => ℝ))      (WithLp.measurableSpace exponent (Fin d → ℝ)) μ ⊆      @Metric.closedBall (Space d)        (PiLp.instPseudoMetricSpace (p := exponent) (β := fun _ : Fin d => ℝ)) z R →    AmbientBallBound μ H β →    let ν := MatrixLabelReference d m    let η := ProjectionLaw μ m    let B := ENNReal.ofReal (ProjectionNormScale m p H β R)    let α := 1-1/(p:ℝ)    (∀ E, MeasurableSet E → ν E ≠ ∞ → η E ≤ B * (ν E)^α) ∧    η ≪ ν ∧    ∃ ηc : Measure (NullMeasurableSpace ((Fin m → Space d) × (Fin m → ℝ)) ν),      (∀ E, NullMeasurableSet E ν → ηc E = η E) ∧      (∀ E, NullMeasurableSet E ν → ν.completion E ≠ ∞ →        ηc E ≤ B * (ν.completion E)^α) ∧      (∀ φ : NullMeasurableSpace ((Fin m → Space d) × (Fin m → ℝ)) ν → ℝ≥0∞,        Measurable φ → (∀ x, φ x ≤ 1) →        (∫⁻ x, φ x ∂ηc) ≤ B * (∫⁻ x in ProjectedEllipsoid z R, φ x ∂ν.completion)^α)def JointL1Statement : Prop :=  let two : ℝ := @OfNat.ofNat ℝ 2 (@instOfNatAtLeastTwo ℝ 2 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  ∀ d m p : ℕ,  letI : MeasurableSpace (Space d) := WithLp.measurableSpace exponent (Fin d → ℝ)  2 ≤ d → 1 ≤ m → m < d → 2 ≤ p →  ∀ β H R : ℝ, (m : ℝ)+(p : ℝ)-two < β → 0 < H → 0 < R →  ∀ z : Space d, ∀ μ : Measure (Space d), IsFiniteMeasure μ →    @Measure.support (Space d)      (PiLp.topologicalSpace (p := exponent) (β := fun _ : Fin d => ℝ))      (WithLp.measurableSpace exponent (Fin d → ℝ)) μ ⊆      @Metric.closedBall (Space d)        (PiLp.instPseudoMetricSpace (p := exponent) (β := fun _ : Fin d => ℝ)) z R →    AmbientBallBound μ H β →    μ ≪ UniformSphere d →  ∀ F : ((Fin m → Space d) × (Fin m → ℝ)) → ℝ,    Measurable F → (∀ x, 0 ≤ F x) →    (MatrixLabelReference d m).withDensity (fun x => ENNReal.ofReal (F x)) =      ProjectionLaw μ m →    Tendsto (fun δ => eLpNorm (fun Ay => GaussianRegularization μ m δ Ay - F Ay)      1 (MatrixLabelReference d m)) (𝓝[Set.Ioi 0] 0) (𝓝 0) ∧    eLpNorm F (p : ℝ≥0∞) (MatrixLabelReference d m) ≤      ENNReal.ofReal (ProjectionNormScale m p H β R)def RadialMixtureRepresentation (m : ℕ) : Prop :=  ∀ δ : ℝ, 0 < δ →    (∀ r : ℝ, 0 < r → 0 ≤ RadialMixture m δ r) ∧    Measurable (RadialMixture m δ) ∧    (∫ r in Set.Ioi 0, RadialMixture m δ r) = 1 ∧    (∀ y : Space m, GaussianKernel m δ y =      ∫ r in Set.Ioi ‖y‖, RadialMixture m δ r / (UnitBallVolume m * r^m))def FullRankDensityFormula {d : ℕ}    (μ : @Measure (Space d)      (WithLp.measurableSpace        (@OfNat.ofNat ℝ≥0∞ 2          (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast            (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))) (Fin d → ℝ)))    (m : ℕ) : Prop :=  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  ∀ A : Fin m → Space d,    @LinearIndependent (Fin m) ℝ (Space d) A Real.commRing.toSemiring      (WithLp.instAddCommGroup exponent (Fin d → ℝ)).toAddCommMonoid      (WithLp.instModule (p := exponent) (K := ℝ) (V := Fin d → ℝ)) →    (volume : Measure (Fin m → ℝ)).withDensity      (fun y => ENNReal.ofReal (PointwiseDensity μ m (A,y))) =      @Measure.map (Space d) (Fin m → ℝ)        (WithLp.measurableSpace exponent (Fin d → ℝ)) inferInstance        (fun signal => fun index => @inner ℝ (Space d)          (@InnerProductSpace.toInner ℝ (Space d) _            (PiLp.seminormedAddCommGroup exponent (fun _ : Fin d => ℝ))            (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ)))          signal (A index)) μdef PointwiseDensityProperties {d : ℕ}    (μ : @Measure (Space d)      (WithLp.measurableSpace        (@OfNat.ofNat ℝ≥0∞ 2          (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast            (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))) (Fin d → ℝ)))    (m p : ℕ) (H β R : ℝ) : Prop :=  letI : MeasurableSpace (Space d) := WithLp.measurableSpace    (@OfNat.ofNat ℝ≥0∞ 2      (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast        (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))) (Fin d → ℝ)  let reference : Measure ((Fin m → Space d) × (Fin m → ℝ)) := MatrixLabelReference d m  RadialMixtureRepresentation m ∧  (∀ x, 0 ≤ PointwiseDensity μ m x) ∧  Measurable (PointwiseDensity μ m) ∧  FullRankDensityFormula μ m ∧  reference.withDensity (fun x => ENNReal.ofReal (PointwiseDensity μ m x)) =    ProjectionLaw μ m ∧  (∀ F : ((Fin m → Space d) × (Fin m → ℝ)) → ℝ,    Measurable F → (∀ x, 0 ≤ F x) →    reference.withDensity (fun x => ENNReal.ofReal (F x)) =      ProjectionLaw μ m → PointwiseDensity μ m =ᵐ[reference] F) ∧  (∫⁻ x, ENNReal.ofReal (PointwiseDensity μ m x)^p ∂reference) ≤    ENNReal.ofReal (ProjectionNormScale m p H β R)^pdef PointwiseDensityStatement : Prop :=  let two : ℝ := @OfNat.ofNat ℝ 2 (@instOfNatAtLeastTwo ℝ 2 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let exponent : ℝ≥0∞ := @OfNat.ofNat ℝ≥0∞ 2    (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast      (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  ∀ d m p : ℕ, 2 ≤ d → 1 ≤ m → m < d → 2 ≤ p →  ∀ β H R : ℝ, (m : ℝ)+(p : ℝ)-two < β → 0 < H → 0 < R →  ∀ z : Space d,  ∀ μ : @Measure (Space d) (WithLp.measurableSpace exponent (Fin d → ℝ)),    IsFiniteMeasure μ →    @Measure.support (Space d)      (PiLp.topologicalSpace (p := exponent) (β := fun _ : Fin d => ℝ))      (WithLp.measurableSpace exponent (Fin d → ℝ)) μ ⊆      @Metric.closedBall (Space d)        (PiLp.instPseudoMetricSpace (p := exponent) (β := fun _ : Fin d => ℝ)) z R →    AmbientBallBound μ H β →    μ ≪ UniformSphere d → PointwiseDensityProperties μ m p H β Rdef CoefficientStepStatement : Prop :=  let two : ℝ := @OfNat.ofNat ℝ 2 (@instOfNatAtLeastTwo ℝ 2 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  ∃ C : ℝ, 1 ≤ C ∧ ∀ d m N : ℕ, 16 ≤ d →    1 ≤ m → m ≤ d/8 → 1 ≤ N →    ∀ α H : ℝ, ((d:ℝ)-1)/two ≤ α → α ≤ (d:ℝ)/two → 0 < H →    ∀ h : Fin N → Sphere d → ℝ≥0∞,      (∀ w, Measurable (h w)) → (∀ w s, h w s ≤ 1) →      (∀ w, SphereBallBound (h w) H α) →    ∀ g : Fin N → ((Fin m → Space d) × (Fin m → ℝ)) → ℝ≥0∞,      (∀ w, Measurable (g w)) → (∀ x, ∑ w, g w x ≤ 1) →      SphereBallBound (SphereBlock h g) (C^d * (N:ℝ)^(1/((d/8:ℕ):ℝ)) * H) αdef CubeBlockStatement : Prop :=  ∃ C : ℝ, 1 ≤ C ∧ ∀ d k N : ℕ, 16 ≤ d → 1 ≤ k → k ≤ (d/2)/4 → 1 ≤ N →    ∀ L : ℝ, 0 ≤ L → ∀ f : Fin N → Cube d → ℝ≥0∞,      (∀ v, Measurable (f v)) → (∀ v u, f v u ≤ 1) → (∀ v, CubeLocal (f v) L) →    ∀ g : Fin N → ((Fin k → Space d) × (Fin k → ℝ)) → ℝ≥0∞,      (∀ v, Measurable (g v)) → (∀ x, ∑ v, g v x ≤ 1) →      CubeLocal (WeightedBlock (CubeEmbedding d) f g)        (C^(d/2) * (N:ℝ)^(1/(((d/2)/4:ℕ):ℝ)) * L)end MemoryPrecisionnamespace MemoryPrecision.Kernelnamespace Policydef ModelAdmissible {d M T : ℕ} {Ω : Type u} [MeasurableSpace Ω]    (K : Ω → Policy d M T) (ρ : Measure Ω) : Prop :=  ∀ π : Measure (Sphere d), IsProbabilityMeasure π → Admissible K ρ πend Policyopen MemoryPrecision NoiselessRegression Policydef CubePrior {d : ℕ} (hd : 2 ≤ d) : Measure (MemoryPrecision.Kernel.Sphere d) :=  (CubeLaw d).map (CubeSphere hd)def BlockCount (T p : ℕ) : ℕ := ⌈(T:ℝ)/(p:ℝ)⌉₊def SourceEllipsoidStatement : Prop :=  let two : ℝ := @OfNat.ofNat ℝ 2 (@instOfNatAtLeastTwo ℝ 2 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0)))  let four : ℝ := @OfNat.ofNat ℝ 4 (@instOfNatAtLeastTwo ℝ 4 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 2)))  let ten : ℝ := @OfNat.ofNat ℝ 10 (@instOfNatAtLeastTwo ℝ 10 Real.commRing.toNatCast    (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 8)))  ∃ C C₀ : ℝ, 1 ≤ C ∧ 1 ≤ C₀ ∧  ∀ d M T : ℕ, 16 ≤ d → ∀ ε : ℝ, 0 < ε → ε ≤ 1/ten →  ∀ (Ω : Type u) [MeasurableSpace Ω] (ρ : Measure Ω), IsProbabilityMeasure ρ →  ∀ K : Ω → Policy d M T, Policy.Admissible K ρ (UniformSphere d) →    Policy.Success K ρ (UniformSphere d) ε ≤ min 1 (ENNReal.ofReal      (four^d * ε^(((d:ℝ)-1)/two) *        (C^d * (((d/8+2)*2^M : ℕ):ℝ)^(1/((d/8:ℕ):ℝ)))^(BlockCount T (d/8)))) ∧    Policy.ChordSuccess K ρ (UniformSphere d) ε ≤ min 1 (ENNReal.ofReal      (C₀^d * ε^((d:ℝ)/two-1) *        (C^d * (((2*(d/8)+4)*2^M : ℕ):ℝ)^(1/((d/8:ℕ):ℝ)))^(BlockCount T (d/8)))) ∧    {x : Sphere d × Sphere d | Real.arccos (@inner ℝ (Vector d)      (@InnerProductSpace.toInner ℝ (Vector d) _        (PiLp.seminormedAddCommGroup          (@OfNat.ofNat ℝ≥0∞ 2            (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast              (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0))))          (fun _ : Fin d => ℝ))        (PiLp.innerProductSpace (𝕜 := ℝ) (fun _ : Fin d => ℝ)))      x.2.val x.1.val) ≤ ε} ⊆    {x | @Dist.dist (Vector d)      (PiLp.instDist (p := @OfNat.ofNat ℝ≥0∞ 2        (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast          (Mathlib.Meta.NormNum.instAtLeastTwo (nat_lit 0))))        (α := fun _ : Fin d => ℝ)) x.2.val x.1.val ≤ ε}lemma cubePrior_dimension {d₀ d : ℕ} (hd₀ : 16 ≤ d₀) (hd : d₀ ≤ d) : 2 ≤ d :=  Nat.le_trans (by decide : 2 ≤ 16) (Nat.le_trans hd₀ hd)end MemoryPrecision.Kernelnamespace MemoryPrecisiontheorem 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 ρ →    ∀ K : Ω → MemoryPrecision.Kernel.Policy d M T,      MemoryPrecision.Kernel.Policy.ModelAdmissible.{u} K ρ →      MemoryPrecision.Kernel.Policy.Success K ρ        (MemoryPrecision.Kernel.CubePrior (MemoryPrecision.Kernel.cubePrior_dimension hd₀ hd)) ε ≤          min 1 (ENNReal.ofReal            (D^((d/2)*(MemoryPrecision.Kernel.BlockCount T ((d/2)/4)+1)) * ε^((d/2:ℕ)/4:ℝ))) ∧      ((∀ signal : MemoryPrecision.Kernel.Sphere d,        (@OfNat.ofNat ℝ≥0∞ 2          (@instOfNatAtLeastTwo ℝ≥0∞ 2 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance)) /        (@OfNat.ofNat ℝ≥0∞ 3          (@instOfNatAtLeastTwo ℝ≥0∞ 3 ENNReal.instAddCommMonoidWithOne.toNatCast inferInstance)) ≤          (∫⁻ observation,            MemoryPrecision.Kernel.Policy.experiment K              (MemoryPrecision.Kernel.Policy.angleTest ε) (signal, observation)            ∂ρ.prod (MemoryPrecision.Kernel.RowLaw d T))) →        c*(d:ℝ)*Real.log (1/ε) ≤ (T:ℝ))) ∧  (∃ C : ℝ, 0 < C ∧ ∃ d₀ : ℕ, 0 < d₀ ∧    ∀ d M T : ℕ, d₀ ≤ d → ∀ ε : ℝ, 0 < ε → ε ≤ 1/10 →    ∀ (Ω : Type u) [MeasurableSpace Ω] (ρ : Measure Ω), IsProbabilityMeasure ρ →    ∀ L : Ω → MemoryPrecision.Kernel.Policy d M T,      MemoryPrecision.Kernel.Policy.Admissible L ρ (MemoryPrecision.Kernel.UniformSphere d) →      MemoryPrecision.Kernel.Policy.Success L ρ (MemoryPrecision.Kernel.UniformSphere d) ε ≤ min 1 (ENNReal.ofReal        ((2*ε*Real.exp (C*(1+(M:ℝ)/(d:ℝ)^2)*(MemoryPrecision.Kernel.BlockCount T ((d-1)/8):ℝ)))^(((d:ℝ)-1)/2)))) := by  sorryend MemoryPrecisionendend OAI

Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

Memory and precision in noiseless Gaussian regression

Theorem (Memory and precision)

For every fixed finite A>0, there are constants c_A>0 and d_A such that the following holds. Let d\ge d_A, let 0\le M\le Ad^2 be an integer, and let 0<\epsilon\le1/10. For any learner in Definition h:model, draw S\sim\sigma_d independently of the rows and the learner’s data-independent randomness. If

\Prob\{\arccos\ip{\widehat s}{S}\le\epsilon\}\ge\frac23,

then its prescribed horizon satisfies

T\ge c_A\,d\log(1/\epsilon).

Section 1, Exact observations and finite memory Read it in the paper TeX source, line 59

Show the TeX

For every fixed finite \(A>0\), there are constants \(c_A>0\) and
\(d_A\) such that the following holds. Let \(d\ge d_A\), let
\(0\le M\le Ad^2\) be an integer, and let \(0<\epsilon\le1/10\).
For any learner in Definition~\ref{h:model}, draw
\(S\sim\sigma_d\) independently of the rows and the learner's
data-independent randomness. If
\[
 \Prob\{\arccos\ip{\widehat s}{S}\le\epsilon\}\ge\frac23,
\]
then its prescribed horizon satisfies
\[
 T\ge c_A\,d\log(1/\epsilon).
\]

Corollary (Subquadratic memory)

Let M(d)\ge0 be integer-valued with M(d)=o(d^2), and let 0<\epsilon(d)\le1/10 be any accuracy sequence. A family of learners in Definition h:model with uniform-sphere average success at least 2/3 satisfies

T(d)\ge c\,d\log(1/\epsilon(d))

for all sufficiently large d, where c>0 is absolute. The dimension threshold may depend on the memory sequence.

Section 1, Exact observations and finite memory Read it in the paper TeX source, line 81

Show the TeX

Let \(M(d)\ge0\) be integer-valued with \(M(d)=o(d^2)\), and let
\(0<\epsilon(d)\le1/10\) be any accuracy sequence. A family of learners
in Definition~\ref{h:model} with uniform-sphere average success at
least \(2/3\) satisfies
\[
 T(d)\ge c\,d\log(1/\epsilon(d))
\]
for all sufficiently large \(d\), where \(c>0\) is absolute. The
dimension threshold may depend on the memory sequence.

Corollary (A guarantee for every signal)

The conclusions of Theorem h:main and Corollary h:subquadratic also hold when their average-success assumption is replaced by

\Prob\{\arccos\ip{\widehat s}{s}\le\epsilon\}\ge\frac23 \qquad\text{for every }s\in S^{d-1},

where this probability is over the rows and the learner’s randomness.

Section 1, Exact observations and finite memory Read it in the paper TeX source, line 93

Show the TeX

The conclusions of Theorem~\ref{h:main} and
Corollary~\ref{h:subquadratic} also hold when their average-success
assumption is replaced by
\[
 \Prob\{\arccos\ip{\widehat s}{s}\le\epsilon\}\ge\frac23
 \qquad\text{for every }s\in S^{d-1},
\]
where this probability is over the rows and the learner's randomness.

Posterior replicas and conditional information in Gaussian regression

Theorem (Gaussian replica block bound)

For all sufficiently large d, set

k=2\lfloor d/16\rfloor,\qquad m=k,\qquad t=m+1,\qquad \ell=4k.

Suppose p=f\sigma_d is a probability with 0\le f\le L<\infty. In the block experiment above, let A have k rows and let B have \ell rows. There is an absolute constant C such that

I(S;W\mid B,BS) \le \frac{H(W)}{t}+Cd+C\log(2+\log L).

The bound is uniform over the prior, the density bound L, and the message kernel. The labels used to produce W are the exact values AS.

Section 1, Introduction Read it in the paper TeX source, line 81

Show the TeX

For all sufficiently large $d$, set
\[
 k=2\lfloor d/16\rfloor,\qquad m=k,\qquad t=m+1,\qquad \ell=4k.
\]
Suppose $p=f\sigma_d$ is a probability with $0\le f\le L<\infty$.
In the block experiment above, let $A$ have $k$ rows and let $B$ have
$\ell$ rows. There is an absolute constant $C$ such that
\begin{equation}
 I(S;W\mid B,BS)
 \le \frac{H(W)}{t}+Cd+C\log(2+\log L).
\end{equation}
The bound is uniform over the prior, the density bound $L$, and the message
kernel. The labels used to produce $W$ are the exact values $AS$.

Theorem (Uniform-prior sample lower bound)

Let M(d)=o(d^2) be nonnegative integer-valued, and let 0<\epsilon(d)\le1/10. Suppose a family of learners in Definition def:streaming-model satisfies

\Prob\{\arccos\langle\widehat S,S\rangle\le\epsilon(d)\}\ge\frac23 \qquad\text{when }S\sim\sigma_d,

where the probability includes the signal, samples, and learner randomness. Then there is an absolute c>0 such that

T(d)\ge c\,d\log\frac1{\epsilon(d)}

for all sufficiently large d. The eventual threshold may depend on the memory sequence.

Section 1, Introduction Read it in the paper TeX source, line 147

Show the TeX

Let $M(d)=o(d^2)$ be nonnegative integer-valued, and let
$0<\epsilon(d)\le1/10$. Suppose a family of learners in
Definition~\ref{def:streaming-model} satisfies
\[
 \Prob\{\arccos\langle\widehat S,S\rangle\le\epsilon(d)\}\ge\frac23
 \qquad\text{when }S\sim\sigma_d,
\]
where the probability includes the signal, samples, and learner randomness.
Then there is an absolute $c>0$ such that
\[
 T(d)\ge c\,d\log\frac1{\epsilon(d)}
\]
for all sufficiently large $d$. The eventual threshold may depend on the
memory sequence.

Localization costs and information growth for exact Gaussian observations

Theorem (Repeated localization)

There is an absolute constant c>0 with the following property. For any fixed C_0>0, consider the experiment above with t\ge0 blocks and N\ge1 possible message values, and suppose

\bigl(2/m+e^{-ck}\bigr)\log N\le C_0d.

One can reveal nested dyadic cells Q_0\supset Q_1\supset\cdots\supset Q_t containing Z, where Q_i is a finite-valued measurable function of Z, the preceding revelations, and W_1,\ldots,W_i, so that the augmented transcript

\Pi_t=(W_1,Q_1,\ldots,W_t,Q_t)

satisfies

I(Z;\Pi_t)\le Cdt.

Here C is a constant depending only on C_0. If J_t is the level of Q_t, the construction also gives \E J_t\le Ct.

Section 3, Dyadic localization and its information cost Read it in the paper TeX source, line 54

Show the TeX

There is an absolute constant $c>0$ with the following property.
For any fixed $C_0>0$, consider the experiment above with $t\ge0$
blocks and $N\ge1$ possible message values, and suppose
\begin{equation}
 \bigl(2/m+e^{-ck}\bigr)\log N\le C_0d.
\end{equation}
One can reveal nested dyadic cells
$Q_0\supset Q_1\supset\cdots\supset Q_t$ containing $Z$, where $Q_i$
is a finite-valued measurable function of $Z$, the preceding revelations,
and $W_1,\ldots,W_i$, so that the augmented transcript
\[
 \Pi_t=(W_1,Q_1,\ldots,W_t,Q_t)
\]
satisfies
\begin{equation}
 I(Z;\Pi_t)\le Cdt.
\end{equation}
Here $C$ is a constant depending only on $C_0$. If $J_t$ is the level of $Q_t$, the
construction also gives $\E J_t\le Ct$.

Theorem (Precision lower bound from likelihood truncation)

Let M(d)=o(d^2) be a nonnegative integer-valued memory bound, and let 0<\epsilon(d)\le1/10. Suppose a family of learners in the model above satisfies

\mathbb P\!\left\{\arccos\langle\widehat s,s\rangle \le\epsilon(d)\right\}\ge\frac23 \qquad\text{for every }s\in S^{d-1}.

There is an absolute c>0 such that, for all sufficiently large d,

T(d)\ge c\,d\log_2\frac1{\epsilon(d)}.

The eventual dimension threshold may depend on the memory sequence.

Section 7, Likelihood truncation and selected dyadic cells Read it in the paper TeX source, line 34

Show the TeX

Let $M(d)=o(d^2)$ be a nonnegative integer-valued memory bound, and let
$0<\epsilon(d)\le1/10$.  Suppose a family of learners in the model
above satisfies
\[
 \mathbb P\!\left\{\arccos\langle\widehat s,s\rangle
              \le\epsilon(d)\right\}\ge\frac23
 \qquad\text{for every }s\in S^{d-1}.
\]
There is an absolute $c>0$ such that, for all sufficiently large $d$,
\[
 T(d)\ge c\,d\log_2\frac1{\epsilon(d)}.
\]
The eventual dimension threshold may depend on the memory sequence.

Theorem (The sample bound by separated-tuple localization)

Let M(d)=o(d^2) be integer-valued and let 0<\epsilon(d)\le1/10. Every learner of Section l:model with uniform-sphere angular success probability at least 2/3 must satisfy

T(d)\ge c\,d\log(1/\epsilon(d))

for all sufficiently large d, with an absolute c>0. The eventual dimension threshold may depend on the memory sequence. Success at least 2/3 for every fixed signal implies the same conclusion by averaging.

Section 10, Localization by separated tuples Read it in the paper TeX source, line 727

Show the TeX

Let \(M(d)=o(d^2)\) be integer-valued and let
\(0<\epsilon(d)\le1/10\).  Every learner of
Section~\ref{l:model} with uniform-sphere angular success probability
at least \(2/3\) must satisfy
\[
 T(d)\ge c\,d\log(1/\epsilon(d))
\]
for all sufficiently large \(d\), with an absolute \(c>0\).
The eventual dimension threshold may depend on the memory sequence.
Success at least \(2/3\) for every fixed signal implies the same
conclusion by averaging.

Projection moments, positive cap domination, and Riesz estimates on the sphere

Theorem (Finite-memory precision bound)

Let M(d)=o(d^2) be a sequence of nonnegative integers and let 0<\epsilon(d)\le1/10. There is an absolute c>0 such that, for all sufficiently large d, every learner in the experiment above whose uniform-sphere average success satisfies

\Prob\{\arccos\inner{\widehat S}{S}\le\epsilon(d)\}\ge\frac23

must use

T(d)\ge c\,d\log\frac1{\epsilon(d)}.

The dimension threshold may depend on the memory sequence. In particular, the conclusion holds when the same success probability is required separately for every s\in S^{d-1}.

Section 2, Spherical probabilities and exact observations Read it in the paper TeX source, line 175

Show the TeX

Let \(M(d)=o(d^2)\) be a sequence of nonnegative integers and let
\(0<\epsilon(d)\le1/10\). There is an absolute \(c>0\) such that, for
all sufficiently large \(d\), every learner in the experiment above whose
uniform-sphere average success satisfies
\[
 \Prob\{\arccos\inner{\widehat S}{S}\le\epsilon(d)\}\ge\frac23
\]
must use
\[
 T(d)\ge c\,d\log\frac1{\epsilon(d)}.
\]
The dimension threshold may depend on the memory sequence. In particular,
the conclusion holds when the same success probability is required
separately for every \(s\in S^{d-1}\).

Theorem (Integrated orthonormal-projection moment)

Let d,k,q be integers and \beta a real number with k\ge1, q\ge2, and

k+q\le d,\qquad 0<\beta\le d,\qquad \beta-k-(q-2)\ge1.

Let \nu be a finite positive Borel measure supported in B(z,R), R>0, satisfying (p:all-ball-mass) for some K\ge0. Assume that P_\#\nu is absolutely continuous with respect to Lebesgue measure for \vartheta_{d,k}-almost every P. There is a jointly measurable version g(P,u) of its density such that

\left(\int_{\mathcal V_{d,k}}\int_{\R^k}g(P,u)^q\,du\, d\vartheta_{d,k}(P)\right)^{1/q} \le C^d(C\sqrt d)^{k(1-1/q)} K R^{\beta-k(1-1/q)}.

For every P, this version vanishes when \norm{u-Pz}>R.

Section 3, Integrated moments of orthonormal projections Read it in the paper TeX source, line 168

Show the TeX

Let \(d,k,q\) be integers and \(\beta\) a real number with
\(k\ge1\), \(q\ge2\), and
\begin{equation}
 k+q\le d,\qquad 0<\beta\le d,\qquad
 \beta-k-(q-2)\ge1.
\end{equation}
Let \(\nu\) be a finite positive Borel measure supported in
\(B(z,R)\), \(R>0\), satisfying \eqref{p:all-ball-mass} for some
\(K\ge0\). Assume that \(P_\#\nu\) is absolutely continuous with
respect to Lebesgue measure for \(\vartheta_{d,k}\)-almost every \(P\).
There is a jointly measurable version \(g(P,u)\) of its density such that
\begin{equation}
 \left(\int_{\mathcal V_{d,k}}\int_{\R^k}g(P,u)^q\,du\,
 d\vartheta_{d,k}(P)\right)^{1/q}
 \le C^d(C\sqrt d)^{k(1-1/q)}
 K R^{\beta-k(1-1/q)}.
\end{equation}
For every \(P\), this version vanishes when \(\norm{u-Pz}>R\).

Theorem (Normalized moment for unit-ball measures)

For sufficiently large d, put

k=p=\lfloor d/16\rfloor,\qquad \lambda=(d-1)/2.

Let X be a k-by-d standard Gaussian matrix and define

H=(XX^{\mathsf T})^{1/2},\qquad P=H^{-1}X

on its probability-one full-row-rank event, and set P to a fixed frame on the null complement. Let m_k be uniform probability on the unit ball of \R^k. Suppose \nu is a finite positive Borel measure fixed independently of X, of mass at most one, supported in the unit ball of \R^d, such that for a fixed D>0,

\nu(B(b,t))\le D^d t^\lambda \qquad(b\in\R^d,\ t>0).

Assume P_\#\nu is absolutely continuous for almost every X. There is a jointly measurable nonnegative g_X(z) such that, for almost every X, P_\#\nu(dz)=g_X(z)\,dz/v_k. This version vanishes when \norm z>1 and satisfies

\E_X\int g_X(z)^p\,dm_k(z)\le \exp(C_Ddp).

Section 3, Integrated moments of orthonormal projections Read it in the paper TeX source, line 288

Show the TeX

For sufficiently large \(d\), put
\[
 k=p=\lfloor d/16\rfloor,\qquad \lambda=(d-1)/2.
\]
Let \(X\) be a \(k\)-by-\(d\) standard Gaussian matrix and define
\[
 H=(XX^{\mathsf T})^{1/2},\qquad P=H^{-1}X
\]
on its probability-one full-row-rank event, and set \(P\) to a fixed frame
on the null complement. Let \(m_k\) be uniform
probability on the unit ball of \(\R^k\). Suppose \(\nu\) is a finite
positive Borel measure fixed independently of \(X\), of mass at most one, supported in the unit ball
of \(\R^d\), such that for a fixed \(D>0\),
\[
 \nu(B(b,t))\le D^d t^\lambda
 \qquad(b\in\R^d,\ t>0).
\]
Assume \(P_\#\nu\) is absolutely continuous for almost every \(X\).
There is a jointly measurable nonnegative \(g_X(z)\) such that, for almost
every \(X\), \(P_\#\nu(dz)=g_X(z)\,dz/v_k\). This version vanishes when
\(\norm z>1\) and satisfies
\begin{equation}
 \E_X\int g_X(z)^p\,dm_k(z)\le \exp(C_Ddp).
\end{equation}

Replacing Gaussian observations in memory-constrained inference

Theorem (Mixed projection moment and exact density version)

Let n=d-1, let m,r,q\ge1 be integers, and put \ell=m+r. Suppose

\ell<n,\qquad \ell-m-(q-1)\ge1.

Let \rho be a finite nonnegative Borel measure on S^{d-1}. Suppose that B,D>0 and, for every z\in\R^d and t>0,

\rho(B(z,t))\le Bt^\ell,\qquad \rho(B(z,t))\le Dt^n.

Let X\sim\gamma_m and Z\sim\gamma_r be independent, and set G=(X;Z). For \delta>0, define the cube average

p_{\rho,\delta}(g,y) =(2\delta)^{-\ell}\int \ind_{\{\norm{gu-y}_\infty\le\delta\}}\,d\rho(u).

There is an absolute C such that, for every fixed s\in S^{d-1} and every \delta>0,

\left[\E_X \left(\E_Z p_{\rho,\delta}((X;Z),(X;Z)s)\right)^q \right]^{1/q} \le e^{Cd}B\bigl(1+\log^+(D/B)\bigr).

If in addition \rho\ll\sigma, use the jointly Borel density p_\rho in (eq:r-density-version). There is a measurable set E_\rho\subset S^{d-1}, with \rho(E_\rho)=0, such that for every s\notin E_\rho the cube averages converge to p_\rho(G,Gs) for \gamma_\ell-almost every G, and

\left[\E_X \left(\E_Zp_\rho((X;Z),(X;Z)s)\right)^q \right]^{1/q} \le e^{Cd}B\bigl(1+\log^+(D/B)\bigr).

When \rho\ne0, E_\rho may also be chosen so that 0<p_\rho(G,Gs)<\infty for \gamma_\ell-almost every G and every s\notin E_\rho.

Section 3, A projection moment with shared and fresh rows Read it in the paper TeX source, line 23

Show the TeX

Let \(n=d-1\), let \(m,r,q\ge1\) be integers, and put
\(\ell=m+r\).  Suppose
\begin{equation}
 \ell<n,\qquad \ell-m-(q-1)\ge1.
\end{equation}
Let \(\rho\) be a finite nonnegative Borel measure on \(S^{d-1}\).
Suppose that \(B,D>0\) and, for every \(z\in\R^d\) and \(t>0\),
\begin{equation}
 \rho(B(z,t))\le Bt^\ell,\qquad
 \rho(B(z,t))\le Dt^n.
\end{equation}
Let \(X\sim\gamma_m\) and \(Z\sim\gamma_r\) be independent, and set
\(G=(X;Z)\).  For \(\delta>0\), define the cube average
\[
 p_{\rho,\delta}(g,y)
   =(2\delta)^{-\ell}\int
       \ind_{\{\norm{gu-y}_\infty\le\delta\}}\,d\rho(u).
\]
There is an absolute \(C\) such that, for every fixed
\(s\in S^{d-1}\) and every \(\delta>0\),
\begin{equation}
 \left[\E_X
       \left(\E_Z p_{\rho,\delta}((X;Z),(X;Z)s)\right)^q
 \right]^{1/q}
 \le e^{Cd}B\bigl(1+\log^+(D/B)\bigr).
\end{equation}

If in addition \(\rho\ll\sigma\), use the jointly Borel density
\(p_\rho\) in \eqref{eq:r-density-version}.  There is a measurable
set \(E_\rho\subset S^{d-1}\), with \(\rho(E_\rho)=0\), such that
for every \(s\notin E_\rho\) the cube averages converge to
\(p_\rho(G,Gs)\) for \(\gamma_\ell\)-almost every \(G\), and
\begin{equation}
 \left[\E_X
       \left(\E_Zp_\rho((X;Z),(X;Z)s)\right)^q
 \right]^{1/q}
 \le e^{Cd}B\bigl(1+\log^+(D/B)\bigr).
\end{equation}
When \(\rho\ne0\), \(E_\rho\) may also be chosen so that
\(0<p_\rho(G,Gs)<\infty\) for \(\gamma_\ell\)-almost every \(G\)
and every \(s\notin E_\rho\).

Theorem (Critical-radius comparison)

In the two experiments of Subsection subsec:r-two-experiments, use the dimensions (eq:r-critical-parameters). Thus S\sim\sigma, A\sim\gamma_m is independent of S, and W is countable with an arbitrary joint dependence on (S,A). The aligned law retains (S,A,W) and appends independent r-row C, whereas the independent law retains (S,W) and draws an independent \ell-row matrix G. If H(W)\le d^2, then, for an absolute constant K,

I_0(S;W\mid G,GS)\le I_1(S;W\mid G,GS)+Kd.

Section 4, A critical radius makes the density terms cancel Read it in the paper TeX source, line 22

Show the TeX

In the two experiments of Subsection~\ref{subsec:r-two-experiments},
use the dimensions \eqref{eq:r-critical-parameters}.  Thus
\(S\sim\sigma\), \(A\sim\gamma_m\) is independent of \(S\), and
\(W\) is countable with an arbitrary joint dependence on \((S,A)\).
The aligned law retains \((S,A,W)\) and appends independent
\(r\)-row \(C\), whereas the independent law retains \((S,W)\)
and draws an independent \(\ell\)-row matrix \(G\).
If \(H(W)\le d^2\), then, for an absolute constant \(K\),
\begin{equation}
 I_0(S;W\mid G,GS)\le I_1(S;W\mid G,GS)+Kd.
\end{equation}

Theorem (Streaming consequence of the critical radius)

Let M(d) be a nonnegative integer sequence with M(d)=o(d^2), and let 0<\epsilon(d)\le1/10. For each d, consider a learner in Definition def:r-streaming-model with deterministic finite horizon T(d). If its uniform-sphere angular success probability, including all learner randomness, is at least 3/5, then

T(d)\ge c\,d\log\frac1{\epsilon(d)}

for an absolute c>0 and all sufficiently large d. The eventual dimension threshold may depend on the memory sequence.

Section 8, From row comparisons to streaming lower bounds Read it in the paper TeX source, line 284

Show the TeX

Let \(M(d)\) be a nonnegative integer sequence with \(M(d)=o(d^2)\),
and let \(0<\epsilon(d)\le1/10\).  For each \(d\), consider a learner
in Definition~\ref{def:r-streaming-model} with deterministic finite
horizon \(T(d)\).  If its uniform-sphere angular success probability,
including all learner randomness, is at least \(3/5\), then
\[
 T(d)\ge c\,d\log\frac1{\epsilon(d)}
\]
for an absolute \(c>0\) and all sufficiently large \(d\).  The
eventual dimension threshold may depend on the memory sequence.

Subsphere methods for memory-sample lower bounds in noiseless Gaussian regression

Theorem (Explicit noiseless precision bound)

Let M:\mathbb N\to\mathbb Z_{\ge0} satisfy M(d)=o(d^2). There is a dimension threshold depending only on this memory sequence such that, for every larger d, every 0<\epsilon\le1/10, and every learner in Definition s:model, the following implication holds. If S is uniform on S^{d-1}, independently of the Gaussian rows and learner randomness, and

\Prob\{\arccos\ip{\widehat s}{S}\le\epsilon\}\ge\frac23,

then

T\ge 2^{-16}d\log_2(1/\epsilon).

Section 1, Introduction Read it in the paper TeX source, line 53

Show the TeX

Let \(M:\mathbb N\to\mathbb Z_{\ge0}\) satisfy \(M(d)=o(d^2)\).
There is a dimension threshold depending only on this memory sequence
such that, for every larger \(d\), every \(0<\epsilon\le1/10\), and
every learner in Definition~\ref{s:model}, the following implication
holds. If \(S\) is uniform on \(S^{d-1}\), independently of the
Gaussian rows and learner randomness, and
\[
 \Prob\{\arccos\ip{\widehat s}{S}\le\epsilon\}\ge\frac23,
\]
then
\begin{equation}
 T\ge 2^{-16}d\log_2(1/\epsilon).
\end{equation}

Corollary (Guarantees for every signal)

Under the memory assumption of Theorem s:main, suppose a learner satisfies

\Prob_s\{\arccos\ip{\widehat s}{s}\le\epsilon\}\ge\frac23 \qquad\text{for every }s\in S^{d-1},

where \Prob_s averages its observations and randomness at the fixed signal s. Then (s:main-bound) holds at the same dimension threshold.

Section 1, Introduction Read it in the paper TeX source, line 69

Show the TeX

Under the memory assumption of Theorem~\ref{s:main}, suppose a learner
satisfies
\[
 \Prob_s\{\arccos\ip{\widehat s}{s}\le\epsilon\}\ge\frac23
 \qquad\text{for every }s\in S^{d-1},
\]
where \(\Prob_s\) averages its observations and randomness at the fixed
signal \(s\). Then \eqref{s:main-bound} holds at the same dimension
threshold.

Configuration and file facts

File: lean/ComparatorChallenges/MemoryPrecision.lean
OpenAI’s Lean catalogue: OpenAI lists this as a main result in its Lean catalogue.
Solution module: OAI/Probability/MemoryPrecision/Main.lean
Allowed axioms: propext, Classical.choice, Quot.soundThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports: Mathlib
Imports from outside Mathlib: None
Local vocabulary: 66 local vocabulary declarations
Lines of Lean, without comments or blank lines: 688
Second proof-verification program (nanoda): Off in OpenAI's configuration.

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas