Welford’s streaming variance
Update a mean and sum of squared deviations one value at a time. Proves the result equals the full-data calculation.
Old papers → Lean
I’m taking small results from old math papers, explaining them, and writing proofs that Lean can check. The source and assumptions are included. Work in progress.
Papers (19)
Clenshaw’s backward summation
Evaluate a whole Chebyshev series by running a recurrence backwards. Checked for any finite number of coefficients.
Frisch–Waugh residualization
Remove one nuisance variable before regression. Proves the same coefficient and an exact loss decomposition.
Schulz’s inverse iteration
Improve an approximate inverse by squaring its error. Proves exact formulas after any number of steps.
Halley’s cubic square-root step
A square-root update with a cubed error ratio. Includes exact formulas for every iterate.
Steffensen’s derivative-free step
Find a square root without evaluating a derivative. Proves a safe bracket and a quadratic error bound.
Newman’s Kantorovich inequality
Bound the product of a weighted average and a weighted reciprocal average. Includes an equality example.
Samuelson’s outlier bound
How far can one observation sit from its own sample mean? Proves the sharp squared-deviation bound.
Grüss’s finite covariance bound
Bound covariance using only the ranges of two lists. Allows arbitrary nonnegative normalized weights.
Jury’s quadratic stability test
Three coefficient inequalities put every root of a quadratic inside the unit disk. Handles complex and repeated roots.
Richardson’s extrapolation
Cancel a finite set of known error powers. An exact result for geometrically refined grids.
Kaczmarz’s row projections
Solve one equation at a time. Proves exactly how each projection changes the error, including relaxed steps.
Hildreth’s quadratic procedure
Update one nonnegative variable at a time. Each step minimizes its coordinate; every finite sweep preserves feasibility and never increases the objective.
Fletcher–Powell’s DFP update
A matrix update that keeps positive curvature. Proves symmetry, the secant relation, and strict positive definiteness.
Broyden’s least-change update
Fit a new secant equation while changing the matrix as little as possible. Proves an exact distance decomposition and uniqueness.
Aitken’s Δ² acceleration
Proves that Aitken’s three-sample transform accelerates convergence under an error-ratio condition, with exact error formulas.
Shanks’s two-mode transformation
Five samples recover the target exactly from two geometric error modes. The proof also identifies every singular case in the local model.
Cantor’s diagonal argument
Try to list every infinite sequence of zeros and ones. A small diagonal trick always finds one you missed.
Peirce’s law
An unusual rule about “if … then” becomes a short proof, with its classical assumption made explicit.
Paper map
drag to rotate · click a paper
Grouped by subject for now. Distances don’t measure similarity; this isn’t t-SNE yet.