Machine-checked algebraic identities underlying an empirical study of ridge regression with random Fourier features for exchange-rate forecasting.
Every result in this repository is finite-dimensional vector and matrix algebra. Nothing here depends on data, on any particular implementation, or on any statistical assumption: there are no limits, no measure theory, no asymptotics, and no probability. The point of formalising them is that a reader who cannot re-run the empirical work can still have the algebra checked by Lean's kernel.
Identity A — a test statistic that is a performance statistic. When the restricted forecast is identically zero (a driftless random walk), the timing return is defined as forecast times realised return, and both statistics are computed under the same dispersion convention, the Clark–West MSPE-adjusted statistic and the timing-strategy Sharpe t-statistic are the same number.
The result is stated for an arbitrary absolutely homogeneous dispersion functional rather than a fixed standard-error formula. Both the i.i.d. sample standard deviation (for any degrees-of-freedom convention) and the Newey–West/HAC estimator (for any lag truncation and any kernel weights) are proved to have that property, so the identity covers the standard-error conventions actually used in the forecast-evaluation literature.
The requirement that the same convention be used on both sides is not cosmetic, and is enforced structurally: a single dispersion functional appears on both sides of the equation.
Identity B — the ridge penalty parameterisation.
A ridge objective may penalise the mean squared error or the summed squared
error. ridge_mean_eq_sum_form shows the two agree exactly when the nominal
penalties are related by the sample size. sum_form_penalty_not_invariant
shows, by explicit witness, that at a shared nominal value they are different
estimators. The two together are the content of the claim that a nominal
penalty value ported across loss conventions changes what a comparison
measures.
Identity C — the dual-weight representation.
For more features than observations, the ridge forecast is an exact linear
functional of the training-window realisations. This is the measurement
instrument used in the empirical work: the weight vector is available in closed
form, so what the estimator computes is measurable rather than inferred. The
invertibility side conditions are discharged from a strictly positive penalty in
forecast_eq_dual_weights_of_pos.
Identity D — the closed-form decomposition of the Clark–West statistic. The statistic decomposes into a correlation term (correlation times the two standard deviations) plus a product of means, over the standard error. The degrees-of-freedom convention is not free here, and the definitions are arranged so that the alignment with Identity A is structural rather than documentary.
Requires elan. The toolchain is pinned in
lean-toolchain and the Mathlib revision in lake-manifest.json.
lake exe cache get
lake build
lake env lean AxiomAudit.lean
Every theorem must report exactly Lean's three standard foundational axioms:
[propext, Classical.choice, Quot.sound]
Any other entry — in particular sorryAx, or any user-declared axiom —
constitutes a failure of the audit. The repository contains no sorry and
declares no axioms of its own.
Apache License 2.0 — see LICENSE. This matches Mathlib's licence.