Formal statistical learning · Lean 4
FormalSLT develops reusable Lean foundations for the mathematics behind data and ML systems: VC and Rademacher theory, metric entropy and chaining, PAC-Bayes bounds, anytime-valid e-processes, and learning from dependent data.
Interactive proof map
Select a regime. The mechanism changes, but the library keeps the same question in view: what may be chosen from the observed data without invalidating the conclusion?
Classical learning theory
Sauer–Shelah bounds the realized label patterns; Rademacher complexity turns that growth control into uniform deviation and ERM excess risk.
Overview film
Fixed-time guarantees can fail under repeated monitoring; one checked event can cover repeated looks. This repo-wide film starts there, then maps reusable interfaces from VC and Rademacher theory through chaining, PAC-Bayes, and dependent trajectories. It establishes a broader proof stack; the controlled queue appears only as one worked application.
Inspect the Manim source and fact receiptpropext, Classical.choice, and Quot.sound.REPRODUCTION, SPECIALIZATION, and DERIVED VARIANT are an independent axis recorded in the literature ledger.A connected research program
The project develops reusable foundations first, then composes them into sequential and dependent-data results.
Checked foundations · classical learning theory
The library includes Sauer–Shelah growth bounds, VC-based uniform-deviation and ERM excess-risk bounds, symmetrization, contraction, linear-predictor bounds, and finite and total-bounded chaining interfaces.
Proved composition · IID endpoint
The IID endpoint gives one all-sample-size event for continuous posterior measures. The forward route supports post-data finite model and predictable-strategy posteriors with separate KL costs, and a countable fixed scalar-tilt master over arbitrary measurable hypotheses and eligible continuous posteriors. Exact finite and countable sleeping-expert masters provide executable wealth competition over declared strategies.
Proved compositions · two state-space regimes
The growing-prefix oracle supports continuous posterior measures on arbitrary measurable state and hypothesis spaces. It selects the exact observable boundary over the reporting-time geometric prefix, retains ordinary monitored conditional-risk semantics, and proves vanishing width under an explicit pathwise posterior-KL rate.
Proved compositions · finite-state stationary layer
Finite-depth Poisson corrections connect trajectory risk to stationary risk. A selected empirical catalog adds transition confidence, contraction transfer, and the exact branch under which the invariant law is unique.
Six highlighted endpoints
Each row gives the usable theorem and the nearest boundary it does not cross.
Proved composition · IID · continuous posterior measures
exists_continuousInfiniteEmpiricalBernstein_eventOne prior-dependent event works for every n ≥ 2 and every admissible posterior measure on an arbitrary measurable hypothesis space, for bounded losses over a finite IID observation type.
Boundary. This is an offline simultaneous event built by reverse stitching. It is not itself a forward e-process, an optional-stopping result, or an all-real-tilt optimization.
Proved composition · adaptive finite-state dynamics
exists_trajectoryCountableEmpiricalBernsteinPACBayes_allTime_vanishing_eventFor finite states, arbitrary prefix-dependent kernels, and bounded predeclared trajectory scores, the common event covers every declared tilt atom and path- and time-dependent posterior PMFs. The capstone substitutes the explicit n-dependent geometric atom and proves that selected width vanishes.
Boundary. The endpoint starts from a fixed state and does not allow new score-catalog members learned after observing outcomes. Countable confidence allocation is not itself a master e-process.
Proved composition · arbitrary measurable spaces
exists_continuousMeasurableTrajectoryGrowingPrefixForwardBesselPACBayesOracle_eventOne outer event supports every reporting time, an eligible continuous posterior selected from the path, and exact minimization over the growing geometric tilt prefix for prefix-dependent kernels on arbitrary measurable state and hypothesis spaces.
Boundary. The endpoint starts from a fixed state and requires a jointly strongly measurable bounded score family. The exact argmin is noncomputable, and vanishing width requires the displayed pathwise posterior-KL rate.
Proved composition · conditional inputs · known finite-state kernel
exists_stationaryPoissonDepthSelection_allTime_vanishing_eventGiven an invariant PMF, a nonnegative D bounding each centered row-risk oscillation, and explicit oscillation contraction, logarithmic finite-depth Poisson potentials and geometric tilt selection yield an all-time stationary boundary that tends to zero.
Boundary. The theorem is finite-state and assumes the kernel, invariant PMF, contraction, and oscillation bound are supplied. It is not a continuous-state mixing-time result or a learned-nuisance guarantee.
Proved composition · empirical transitions · finite catalog
exists_selectedCanonicalEmpiricalStationaryCatalog_eventA finite predeclared candidate and depth catalog combines same-path risk and transition confidence, post-path selection, contraction transfer, a canonical invariant PMF, and a conditional uniqueness conclusion.
Boundary. Every state row must be visited, candidates must be predeclared, and uniqueness only follows on the selected strict-contraction branch. Arbitrary path-fitted candidates are outside the theorem.
Proved composition · current main · observable adaptive oracle
exists_trajectoryGrowingPrefixForwardBesselPACBayesOracle_eventFor finite hypotheses and finite-state prefix-dependent trajectories, one event permits path- and time-selected posteriors and exact minimization over the reporting-time prefix of a geometric tilt catalog. It controls posterior-averaged monitored conditional loss by empirical prequential loss plus an observable boundary, bounds that boundary by an explicit LIL-order envelope, and proves the width tends to zero.
Underlying generic result: exists_growingPrefixForwardBesselPACBayesOracle_event.
Boundary. Scores and the countable tilt catalog are fixed before the path. The minimizer is over a finite declared prefix, not all real tilts; the selected boundary is not itself an e-process. This endpoint is on current main and is not part of the tagged v0.2 compatibility allowlist.
Four ways in
Inspect the artifact