Import statistical learning theory formalization - #400
Open
Vilin97 wants to merge 4 commits into
Open
Conversation
Greptile SummaryThe PR imports an endpoint-focused statistical-learning-theory formalization and integrates its project module into the Lean Pool catalog and root import surface.
|
| Filename | Overview |
|---|---|
| LeanPool/StatisticalLearningTheory.lean | Adds the project umbrella module and imports the four retained endpoint branches. |
| LeanPool/StatisticalLearningTheory/HansonWright.lean | Defines a source-shaped compatibility layer that delegates the live tail-bound proof to the existing pooled Hanson–Wright theorem. |
| LeanPool/StatisticalLearningTheory/RMT/Basic.lean | Adds the random-matrix infrastructure and two-sided sub-Gaussian singular-value concentration endpoint. |
| LeanPool/StatisticalLearningTheory/TDudley.lean | Adds the truncated Dudley entropy-bound development. |
| LeanPool/StatisticalLearningTheory/LeastSquares/L1Regression/L1CoveringBound.lean | Adds the Maurey-method covering argument and localized l1-design covering endpoint. |
| LeanPool/StatisticalLearningTheory/SmallBallProb.lean | Adds the small-ball probability inequality and supporting measure-theoretic development. |
| LeanPool/projects.yml | Registers the imported statistical-learning-theory project and its retained results. |
Reviews (3): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Contributor
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 861 maxHeartbeats units across 13 files (6,654 added LOC). Sum of Count-heartbeats wall-clock total: 120.12 s. Repeated import cost inside Heartbeat values come from Mathlib's LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.StatisticalLearningTheory.RMT.Basic |
44.00 s |
LeanPool.StatisticalLearningTheory.TDudley |
37.00 s |
LeanPool.StatisticalLearningTheory.LeastSquares.L1Regression.L1CoveringBound |
16.00 s |
LeanPool.StatisticalLearningTheory.CoveringNumber |
12.00 s |
LeanPool.StatisticalLearningTheory.SmallBallProb |
10.00 s |
LeanPool.StatisticalLearningTheory.LeastSquares.Defs |
9.60 s |
LeanPool.StatisticalLearningTheory.SubGaussian |
8.30 s |
LeanPool.StatisticalLearningTheory.HansonWright |
4.60 s |
LeanPool.StatisticalLearningTheory.LeastSquares.Localization |
3.60 s |
LeanPool.StatisticalLearningTheory.MetricEntropy |
3.30 s |
LeanPool.StatisticalLearningTheory.LeastSquares.LinearRegression.DesignMatrix |
2.90 s |
LeanPool.StatisticalLearningTheory.LeastSquares.L1Regression.L1DesignMatrix |
2.60 s |
Per-file `lean --profile` output
LeanPool/StatisticalLearningTheory.lean
import took 1.71s
cumulative profiling times:
elaboration 0.19ms
import 1.71s
initialization 29.4ms
interpretation 204ms
linting 0.316ms
module linting 0.00101ms
overlappingInstancesLinter 0.302ms
parsing 0.0313ms
tacticAnalysis 1.08ms
real 2.63
user 1.45
sys 1.18
LeanPool/StatisticalLearningTheory/CoveringNumber.lean
import took 1.55s
cumulative profiling times:
attribute application 0.389ms
compilation (IR) 0.0963ms
compilation (LCNF base) 2.22ms
compilation (LCNF impure) 0.455ms
compilation (LCNF mono) 0.994ms
congr simp thm 7.63ms
elaboration 145ms
fix level params 4.06ms
import 1.55s
initialization 39ms
instantiate metavars 6.41ms
interpretation 852ms
let-to-have transformation 0.53ms
linting 68.6ms
module linting 0.00164ms
norm_num 82.6ms
overlappingInstancesLinter 16.8ms
parsing 41.9ms
process pre-definitions 24ms
ring 40.7ms
share common exprs 17.8ms
simp 145ms
tactic execution 503ms
tacticAnalysis 104ms
type checking 208ms
typeclass inference 1.19s
real 3.57
user 4.49
sys 1.15
LeanPool/StatisticalLearningTheory/HansonWright.lean
import took 1.7s
cumulative profiling times:
attribute application 0.0891ms
blocked (unaccounted) 1.3ms
compilation (IR) 0.177ms
compilation (LCNF base) 2.93ms
compilation (LCNF impure) 1.05ms
compilation (LCNF mono) 1.8ms
congr simp thm 1.59ms
elaboration 59ms
fix level params 0.23ms
import 1.7s
initialization 29.5ms
instantiate metavars 0.265ms
interpretation 297ms
let-to-have transformation 0.13ms
linting 8.09ms
module linting 0.00141ms
overlappingInstancesLinter 5.84ms
parsing 7.12ms
process pre-definitions 5.24ms
share common exprs 0.9ms
simp 16ms
tactic execution 18.2ms
tacticAnalysis 20.2ms
type checking 35.9ms
typeclass inference 140ms
real 2.84
user 1.81
sys 1.20
LeanPool/StatisticalLearningTheory/LeastSquares/Defs.lean
import took 1.47s
cumulative profiling times:
attribute application 0.991ms
compilation (IR) 0.119ms
compilation (LCNF base) 1.27ms
compilation (LCNF impure) 0.641ms
compilation (LCNF mono) 1.02ms
congr simp thm 1.7ms
elaboration 40.6ms
fix level params 0.374ms
import 1.47s
initialization 33.7ms
instantiate metavars 0.68ms
interpretation 287ms
let-to-have transformation 0.0961ms
linting 11.4ms
module linting 0.00133ms
norm_num 0.216ms
overlappingInstancesLinter 3.26ms
parsing 11.2ms
process pre-definitions 6.21ms
ring 3.9ms
share common exprs 2.49ms
simp 61.7ms
tactic execution 148ms
tacticAnalysis 26ms
type checking 24.1ms
typeclass inference 269ms
real 2.71
user 1.99
sys 1.04
LeanPool/StatisticalLearningTheory/LeastSquares/L1Regression/L1CoveringBound.lean
import took 1.66s
typeclass inference of Nonempty took 106ms
typeclass inference of Nonempty took 104ms
typeclass inference of Nonempty took 109ms
typeclass inference of Nonempty took 107ms
typeclass inference of Nonempty took 109ms
typeclass inference of Nonempty took 108ms
tactic execution of Mathlib.Tactic.nlinarith took 481ms
tactic execution of Mathlib.Tactic.nlinarith took 142ms
tactic execution of Mathlib.Tactic.nlinarith took 190ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 210ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 134ms
cumulative profiling times:
attribute application 1.48ms
compilation (IR) 0.0336ms
compilation (LCNF base) 0.558ms
compilation (LCNF impure) 0.177ms
compilation (LCNF mono) 0.255ms
congr simp thm 24.7ms
elaboration 217ms
fix level params 4.26ms
import 1.66s
initialization 29.5ms
instantiate metavars 12ms
interpretation 1.8s
let-to-have transformation 0.515ms
linting 121ms
module linting 0.00161ms
norm_num 84ms
overlappingInstancesLinter 13ms
parsing 73.6ms
process pre-definitions 50ms
ring 119ms
share common exprs 49.8ms
simp 727ms
tactic execution 2.32s
tacticAnalysis 181ms
type checking 309ms
typeclass inference 4.45s
real 6.27
user 11.74
sys 1.17
LeanPool/StatisticalLearningTheory/LeastSquares/L1Regression/L1DesignMatrix.lean
import took 1.57s
cumulative profiling times:
attribute application 0.528ms
congr simp thm 1.37ms
elaboration 42ms
fix level params 0.378ms
import 1.57s
initialization 29.1ms
instantiate metavars 0.479ms
interpretation 316ms
let-to-have transformation 0.124ms
linting 7.67ms
module linting 0.00131ms
norm_num 0.167ms
overlappingInstancesLinter 2.72ms
parsing 7.36ms
process pre-definitions 3.32ms
ring 3.88ms
share common exprs 2.36ms
simp 65.3ms
tactic execution 81.9ms
tacticAnalysis 20.6ms
type checking 29.2ms
typeclass inference 171ms
real 2.63
user 1.91
sys 1.08
LeanPool/StatisticalLearningTheory/LeastSquares/LinearRegression/DesignMatrix.lean
import took 1.44s
cumulative profiling times:
attribute application 0.494ms
congr simp thm 0.502ms
elaboration 19ms
fix level params 0.143ms
import 1.44s
initialization 29.1ms
instantiate metavars 0.173ms
interpretation 219ms
let-to-have transformation 0.0718ms
linting 4.15ms
module linting 0.00161ms
overlappingInstancesLinter 2.15ms
parsing 3.62ms
process pre-definitions 1.52ms
share common exprs 0.95ms
simp 4.03ms
tactic execution 39.2ms
tacticAnalysis 13.8ms
type checking 15ms
typeclass inference 52.6ms
real 2.37
user 1.46
sys 1.02
LeanPool/StatisticalLearningTheory/LeastSquares/Localization.lean
import took 1.45s
cumulative profiling times:
attribute application 0.013ms
congr simp thm 0.598ms
elaboration 6.1ms
fix level params 0.106ms
import 1.45s
initialization 28.6ms
instantiate metavars 0.169ms
interpretation 212ms
let-to-have transformation 0.0197ms
linting 3.23ms
module linting 0.0015ms
norm_num 0.605ms
overlappingInstancesLinter 1.49ms
parsing 1.95ms
process pre-definitions 0.882ms
ring 6.21ms
share common exprs 1.29ms
simp 7.6ms
tactic execution 19.4ms
tacticAnalysis 8.12ms
type checking 6.47ms
typeclass inference 40.5ms
real 2.39
user 1.40
sys 1.03
LeanPool/StatisticalLearningTheory/MetricEntropy.lean
import took 1.54s
cumulative profiling times:
attribute application 0.0791ms
compilation (IR) 0.0548ms
compilation (LCNF base) 0.548ms
compilation (LCNF impure) 0.325ms
compilation (LCNF mono) 0.529ms
congr simp thm 1.2ms
elaboration 30.7ms
fix level params 0.389ms
import 1.54s
initialization 28.7ms
instantiate metavars 0.984ms
interpretation 314ms
let-to-have transformation 0.0699ms
linting 9.58ms
module linting 0.00164ms
norm_num 0.554ms
overlappingInstancesLinter 5.05ms
parsing 7.22ms
process pre-definitions 2.84ms
ring 3.12ms
share common exprs 1.57ms
simp 29.6ms
tactic execution 67.5ms
tacticAnalysis 21.4ms
type checking 35.5ms
typeclass inference 100ms
real 2.62
user 1.77
sys 1.07
LeanPool/StatisticalLearningTheory/RMT/Basic.lean
import took 1.7s
tactic execution of Lean.Parser.Tactic.simpa took 109ms
type checking took 112ms
tactic execution of Lean.Parser.Tactic.change took 414ms
simp took 157ms
tactic execution of Lean.Parser.Tactic.refine took 127ms
interpretation of Lean.Elab.Tactic._aux_Mathlib_Tactic_Widget_Calc___elabRules_Lean_calcTactic_1._boxed took 132ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 560ms
tactic execution of Mathlib.Tactic.nlinarith took 506ms
tactic execution of Mathlib.Tactic.nlinarith took 707ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 509ms
tactic execution of Mathlib.Tactic.nlinarith took 694ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 610ms
tactic execution of Mathlib.Tactic.nlinarith took 851ms
simp took 100ms
simp took 145ms
interpretation of Mathlib.Meta.FunProp.funPropTac._boxed took 112ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 100ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 108ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 130ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 149ms
simp took 111ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 227ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 234ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 264ms
tactic execution of Mathlib.Tactic.nlinarith took 506ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 511ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 287ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 370ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 398ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.13s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.43s
tactic execution of Mathlib.Tactic.nlinarith took 1.06s
simp took 110ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 158ms
simp took 120ms
cumulative profiling times:
attribute application 1.36ms
blocked (unaccounted) 11.3s
compilation (IR) 0.143ms
compilation (LCNF base) 1.4ms
compilation (LCNF impure) 0.681ms
compilation (LCNF mono) 1.11ms
congr simp thm 51ms
dsimp 90.2ms
elaboration 918ms
fix level params 13.5ms
import 1.7s
initialization 32.1ms
instantiate metavars 25.8ms
interpretation 11.3s
let-to-have transformation 2.92ms
linting 263ms
module linting 0.00159ms
norm_num 469ms
overlappingInstancesLinter 36ms
parsing 167ms
process pre-definitions 156ms
ring 353ms
share common exprs 162ms
simp 3.38s
tactic execution 9.07s
tacticAnalysis 415ms
type checking 1.34s
typeclass inference 18.7s
real 25.59
user 47.85
sys 1.37
LeanPool/StatisticalLearningTheory/SmallBallProb.lean
import took 1.64s
cumulative profiling times:
aesop 43.1ms
attribute application 0.058ms
compilation (IR) 0.11ms
compilation (LCNF base) 1.31ms
compilation (LCNF impure) 0.566ms
compilation (LCNF mono) 0.953ms
congr simp thm 7.19ms
dsimp 12.1ms
elaboration 49.9ms
fix level params 1.06ms
import 1.64s
initialization 35.6ms
instantiate metavars 1.12ms
interpretation 594ms
let-to-have transformation 0.111ms
linting 28.1ms
module linting 0.00142ms
norm_num 7.22ms
overlappingInstancesLinter 4.41ms
parsing 17ms
process pre-definitions 13.2ms
ring 18.9ms
share common exprs 7.43ms
simp 136ms
tactic execution 333ms
tacticAnalysis 45ms
type checking 70.6ms
typeclass inference 496ms
real 3.22
user 3.06
sys 1.11
LeanPool/StatisticalLearningTheory/SubGaussian.lean
import took 1.68s
cumulative profiling times:
attribute application 0.101ms
elaboration 22.5ms
fix level params 0.106ms
import 1.68s
initialization 29.4ms
instantiate metavars 0.0861ms
interpretation 249ms
let-to-have transformation 0.0527ms
linting 3.86ms
module linting 0.00133ms
overlappingInstancesLinter 3.09ms
parsing 3.58ms
process pre-definitions 0.748ms
share common exprs 0.284ms
tacticAnalysis 11.9ms
type checking 2.46ms
typeclass inference 17.9ms
real 2.61
user 1.53
sys 1.15
LeanPool/StatisticalLearningTheory/TDudley.lean
import took 1.73s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 162ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 146ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 148ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 145ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 172ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 757ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 303ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 157ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 162ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 150ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 173ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 1.26s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 1.16s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 835ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 102ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 120ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 155ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 162ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 191ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 1.11s
interpretation of Mathlib.Tactic.RingNF._aux_Mathlib_Tactic_Ring_RingNF___elabRules_Mathlib_Tactic_RingNF_ringNF_1._boxed took 132ms
typeclass inference of Nonempty took 103ms
typeclass inference of Nonempty took 103ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 205ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 323ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 480ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 158ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_NormNum_Core___elabRules_Mathlib_Tactic_normNum_1._boxed took 103ms
typeclass inference of MulRightMono took 118ms
simp took 103ms
simp took 132ms
simp took 131ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 185ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 235ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 189ms
simp took 194ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 672ms
cumulative profiling times:
aesop 42.8ms
attribute application 0.698ms
compilation (IR) 0.153ms
compilation (LCNF base) 1.52ms
compilation (LCNF impure) 0.807ms
compilation (LCNF mono) 1.08ms
congr simp thm 139ms
dsimp 19.2ms
elaboration 727ms
fix level params 21.7ms
import 1.73s
initialization 36.6ms
instantiate metavars 60.7ms
interpretation 18s
let-to-have transformation 1.49ms
linting 409ms
module linting 0.00151ms
norm_num 3.35s
overlappingInstancesLinter 34.9ms
parsing 175ms
process pre-definitions 190ms
ring 788ms
share common exprs 267ms
simp 2.8s
tactic execution 5.39s
tacticAnalysis 514ms
type checking 1.12s
typeclass inference 14.6s
real 19.84
user 49.65
sys 1.38
Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.
Contributor
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | 🛑 block |
The Dudley headline uses a totalized supremum that collapses unbounded oscillations to zero, and the localized covering headline hides an additional empirical-metric normalization. |
| Novelty | ✅ pass |
The searches ran for all four headlines and found no Mathlib or pooled declaration that already proves any of them. |
| Significance | ✅ pass |
This is a substantial theory-building project with several recognizable graduate-level results in statistical learning and high-dimensional probability. |
| Sources | ✅ pass |
The diff consistently credits the pinned upstream formalization and labels the high-dimensional-probability material as later development, but the exact contents of the arXiv paper and GitHub commit are not verifiable from the diff. |
| Code quality (advisory) | 🤔 discuss |
The development carries substantial generated debt: a long proof duplicates an immediately preceding result, exact theorem and proof duplicates remain, and the compatibility and RMT APIs retain unused assumptions and fields. |
| Aspect | Value |
|---|---|
| Proves the claim | 🛑 mismatch |
| Assumed, not proved | The Dudley diameter, sub-Gaussian increment, total-boundedness, nonemptiness, and integrability hypotheses; the RMT bundled measurable/independent/mean-zero/isotropic/finite-scale row hypotheses; the small-ball measurability, independence, nonnegativity, and density hypotheses; and the covering bound's column normalization are all explicit and disclosed. |
| Matches cited source | 🟡 unverifiable |
| Fit | ✅ good_fit |
| Level | graduate |
| Branch | statistical learning theory and high-dimensional probability |
| Mode | theory_building |
| Code quality | 2 / 5 |
Statement check: The RMT and small-ball endpoints match their informals, but truncated_dudley_entropy_bound bounds totalized ℝ-valued sSups and l1LocalizedImage_coveringNumber_le covers Xθ/√n in a metric that divides distances by another √n.
The contribution develops covering and metric entropy machinery through a truncated Dudley bound, Maurey covering bounds, a small-ball inequality, and two-sided singular-value concentration for isotropic sub-Gaussian random matrices.
Faithfulness findings (2)
- overclaimed-headline —
LeanPool/StatisticalLearningTheory/TDudley.lean:55
globalOscandlocalOscare real-valued totalized suprema, with no pathwiseBddAbovehypothesis. An unbounded increment set therefore produces value zero underReal.sSup_of_not_bddAbove; the proof explicitly handles this branch. Consequently, integrability of these functions does not assert that the mathematical oscillations are finite or integrable. Add pathwise boundedness of the global increment set, or revise the card to state that it concerns these zero-on-unbounded totalized definitions.
Evidence: The definitions aredef globalOsc (X : α → ℝ) (T : Set α) : ℝ := sSup {X x - X y | (x ∈ T) (y ∈ T)}anddef localOsc (X : α → ℝ) (T : Set α) (δ : ℝ) : ℝ := sSup {X x - X y | (x ∈ T) (y ∈ T) (_ : dist x y ≤ δ)}. The headline assumes only(h_integrable_global : Integrable (fun ω => globalOsc (X ω) T) P)and(h_integrable_local : Integrable (fun ω => localOsc (X ω) T δ) P). Its supporting proof containsrw [Real.sSup_of_not_bddAbove] at h_contrafor the unbounded case. - surrogate-object —
LeanPool/StatisticalLearningTheory/LeastSquares/L1Regression/L1CoveringBound.lean:878
The image already dividesXθby√n, but its ambientEmpiricalSpacedistance applies the empirical norm and divides Euclidean distances by another√n. For positiven, the effective distance between represented predictors is the Euclidean norm ofX(θ−θ′)divided byn, not the Euclidean distance on the card's normalized imageXθ/√n. This is a contracted covering problem. Either remove the extra scaling from the represented image while retaining the empirical metric, or disclose the ambient empirical metric and the resulting second normalization in the informal.
Evidence: The metric is defined bynoncomputable def empiricalNorm (n : ℕ) (f : Fin n → ℝ) : ℝ := Real.sqrt ((n : ℝ)⁻¹ * ∑ k : Fin n, f k ^ 2)andnoncomputable instance instDist (n : ℕ) : Dist (EmpiricalSpace n) where dist a b := empiricalNorm n (a - b). The set is defined withv = fun i => (1 / Real.sqrt n) * @inner ℝ _ _ θ (x i), and the theorem concludescoveringNumber ε (l1LocalizedImage x R δ) ≤ (2 * d + 1) ^ ⌈R ^ 2 / ε ^ 2⌉₊.
Code quality findings (7)
- agent-slop —
LeanPool/StatisticalLearningTheory/LeastSquares/L1Regression/L1CoveringBound.lean:690
exists_maureyAvg_closerebuilds a finite-minimum argument and special-cases zero parameters aftermaurey_exists_good_samplehas already established the required squared-distance estimate for every positivek. Obtain that sample directly, boundR * l1norm θ / kbyR ^ 2 / kand then byε ^ 2, and conclude from nonnegativity. The current detour also leaveshk_pos_realandhvar_boundunused.
Evidence:maurey_exists_good_sampleconcludesdist (maureyAvg x R k f) (fun i => (1 / Real.sqrt n) * @inner ℝ _ _ θ (x i)) ^ 2 ≤ R * l1norm θ / k. The next proof nevertheless introduceslet distSq : α → ℝ := fun f => dist (maureyAvg x R k f) target ^ 2,obtain ⟨f₀, hf₀_min⟩ := Finite.exists_min distSq, andby_cases hk1 : k = 1, before later callingobtain ⟨f_good, hf_good⟩ := maurey_exists_good_sample x θ hR hθ hcol hn k hkpos. It also declareshave hk_pos_real : (0 : ℝ) < k := Nat.cast_pos.mpr hkposandhave hvar_bound : R * l1norm θ ≤ R ^ 2 := bywithout using either binding. - duplicate-definition —
LeanPool/StatisticalLearningTheory/TDudley.lean:1250
dudley_sum_bound_tightrestatesdudley_sum_boundwith the same arguments and conclusion and only forwards to it. Remove the alias and havedudley_step_sum_le_entropycalldudley_sum_bounddirectly.
Evidence:lemma dudley_sum_bound_tight {f : ℝ → ℝ} {D : ℝ} (hD : 0 < D) (hf_antitone : AntitoneOn f (Set.Icc 0 D)) (L : ℕ) (hL : 1 ≤ L) : ∑ k ∈ Finset.range (L - 1), 4 * (D * 2 ^ (-(k + 1 : ℝ))) * f (D * 2 ^ (-(k + 2 : ℝ))) ≤ 16 * ∫ x in Set.Icc (D * 2 ^ (-(L + 1 : ℝ))) (D * 2 ^ (-2 : ℝ)), f x := by convert dudley_sum_bound hD hf_antitone L hL using 1. - duplicate-definition —
LeanPool/StatisticalLearningTheory/RMT/Basic.lean:900
operatorNorm_one_pos_of_posandone_le_operatorNorm_one_of_posrepeat the same witness, norm computation, operator application, and lower-bound proof. Proveone_le_operatorNorm_one_of_posonce and derive positivity from it.
Evidence: Both declarations begin with the same body:unfold HansonWright.operatorNorm,let i : Fin n := ⟨0, hn⟩,let e : EuclideanSpace ℝ (Fin n) := EuclideanSpace.single i (1 : ℝ), the identicalhave he,have happly, andhave hle. The first ends withexact lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) hle, while the second ends withexact hle. - unused-structure-field —
LeanPool/StatisticalLearningTheory/RMT/Basic.lean:530
The codomain half ofMatrixBilinearNethas no consumer in the retained development: all net reductions usedomainNet, and the sole endpoint path explicitly discards the codomain bound. Replace this rectangular two-net structure with the single centered sphere net actually used.
Evidence:structure MatrixBilinearNet (m n : ℕ) (ε : ℝ) wherecontainscodomainNet : Finset (EuclideanSpace ℝ (Fin m))andcodomain_isNet : IsENet codomainNet ε (euclideanUnitSphere m);CenteredMatrixBilinearNetaddscodomain_subset_unitBall. There is onlylemma MatrixBilinearNet.exists_domain_near, and the tail proof usesobtain ⟨N, hN_domain, _hN_codomain⟩ := exists_quarter_centeredMatrixBilinearNet n n. - unused-hypothesis —
LeanPool/StatisticalLearningTheory/RMT/Basic.lean:1000
The endpoint proof never selects themeasurableormean_zerofields ofHasIndependentMeanZeroIsotropicSubGaussianRows; downstream arguments use only row independence, isotropy, and finite row ψ₂ bounds. Split or weaken this assumption structure so the theorem does not require unused data.
Evidence: The structure declaresmeasurable : ∀ i j, Measurable (A i j)andmean_zero : ∀ i (x : EuclideanSpace ℝ (Fin n)), ∫ ω, inner ℝ (randomMatrixRowVector A i ω) x ∂μ = 0. Subsequent projections shown in the diff arehA.independent_rows.comp,hA.isotropic i x, andhA.finite_row_psi2; there is no use ofhA.measurableorhA.mean_zero. - unused-hypothesis —
LeanPool/StatisticalLearningTheory/HansonWright.lean:84
The compatibility theorem asks for four constant conditions that its proof discards. Expose the leaner adapter theorem matching the pooled Hanson–Wright result; otherwise downstream constant lemmas exist only to satisfy ceremonial arguments.
Evidence:hanson_wright_inequalitytakes(_hC : 0 < C),(_hC_domain : 4 * exp 1 ≤ C),(_hC_diag_quad : 8 * exp 1 ^ 3 ≤ C), and(_hC_offdiag_domain : 16 * exp 1 ≤ C ^ 2), but the delegated call is_root_.LeanPool.HansonWright.hanson_wright_inequality hK hC_offdiag_quad hF hOp h_indep hX_subG ht. - unused-hypothesis —
LeanPool/StatisticalLearningTheory/CoveringNumber.lean:264
Nonnegativity ofepsis threaded through the half-ball disjointness and volume lemmas but never used. Remove these suppressed hypotheses and the corresponding arguments at their callers.
Evidence:closedBall_half_disjointtakes(_heps : 0 ≤ eps)but proves the result solely fromhsep;volume_disjoint_union_closedBallslikewise takes{eps : ℝ} (_heps : 0 ≤ eps)and its body is onlyhave hmeas ...; exact measure_biUnion_finset hpwd hmeas.packing_halfBalls_pairwiseDisjointuses itshepsonly asclosedBall_half_disjoint heps hsep.
Tokens: 609,757 in / 33,666 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $2.0294
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
request_changes is an ask, not a close: of the reviewer's past request_changes verdicts, 39% were merged after a human looked. Read the findings before acting on the verdict.
# Conflicts: # LeanPool/projects.yml
Owner
Author
Changes requested by automated reviewReviewed exact head |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Imports the endpoint closure of Yuanhe Zhang, Jason D. Lee, and Fanghui Liu's Apache-2.0 statistical-learning formalization at commit
d0f506f0a695018265dccb33bcb05e2f5ca1c876, ported from Lean 4.32 to the pool's Lean 4.34 toolchain.The retained development covers four source endpoints:
LeanPool.StatisticalLearningTheory.truncated_dudley_entropy_boundLeanPool.StatisticalLearningTheory.RMT.two_sided_subgaussian_matrices_hdp_of_posLeanPool.StatisticalLearningTheory.SmallBallProbability.small_ball_probLeanPool.StatisticalLearningTheory.LeastSquares.l1LocalizedImage_coveringNumber_leTogether they preserve a truncated Dudley entropy bound, two-sided singular-value concentration for isotropic sub-Gaussian random matrices, a small-ball probability inequality, and a localized l1-design covering bound. The registry records mixed provenance because the source proofs and the Lean Pool port/optimization both contribute substantially.
Closure and dead-code elimination
SLTmodules. Exact module dependency closure from the four endpoints first selected 18 modules (15,278 physical lines after the initial port/reuse pass).simp/rflsource-elaboration dependencies. Each was separately removed and rebuilt to verify that elaboration fails without it; they are intentionally private rather than public API.set_optionoverrides. The two formerly oversized Dudley proofs and the Maurey proof were decomposed into ordinary live helpers; every proof is below 200 code lines and every file below 10,000.Source/final size (comments included / non-comment code):
SLT/Relative to upstream
SLT/, the final implementation removes 49,362 physical lines (88.4%) and 39,367 code lines (87.6%). The generated 21-line project card is separate from those implementation figures.Lean Pool reuse
The source's 4,583-line Hanson-Wright file shares ancestry with
LeanPool.HansonWright, but its later API is not wholesale type-compatible. I kernel-checked a 15-name compatibility surface, delegated exact matches to the pooled implementation, and let endpoint DCE discard four adapter declarations that were not needed. The final live adapter has 11 declarations in 111 physical / 69 code lines, saving 4,472 physical lines (97.6%) and 4,245 code lines (98.4%) versus the source file.The scalar sub-Gaussian layer likewise delegates to
LeanPool.HansonWright.Probability.Process.SubGaussian: 1,039 physical / 834 code source lines become a 60 physical / 32 code-line compatibility module.Build cost
Both measurements used cached dependency artifacts and no pre-existing project artifacts; every project module was compiled.
The endpoint closure reduces wall time by 73.3%, peak RSS by 46.0%, and the build graph by 63.0% in this comparison.
Verification
LeanPool.leanaggregate import compilation against a complete base artifact setrunLinteron the aggregate and every project modulelint-styleon the aggregate and every project modulemk_all --checkQuality checks passed.)#print axiomsfor each endpoint: onlypropext,Classical.choice, andQuot.sound