Stat.Nonparametric.SeriesSieve
Tools for regression on a finite set of basis functions.
LeastSquares 4 core · 2 supporting This module supplies the finite-dimensional algebra used by the series prediction-rate theorem. ★ seriesHatMatrix_frobenius_sq
Closed-form series least squares and its hat matrix
This module supplies the finite-dimensional algebra used by the series prediction-rate theorem.
For a design matrix Φ, it defines the unweighted Gram matrix ΦᵀΦ, its inverse-Gram
least-squares coefficient map, and the projection hat matrix H = Φ(ΦᵀΦ)⁻¹Φᵀ. When the Gram
matrix is invertible, the coefficient map satisfies the normal equations, fitted-value differences
are exactly linear in outcome differences, and ∑ᵢₖ Hᵢₖ² equals the number of columns.
Given a finite series design matrix, the series Gram matrix is the column cross-product ΦᵀΦ.
Given a finite series design matrix and a vector of responses, the closed-form series least-squares coefficient vector is (ΦᵀΦ)⁻¹Φᵀy.
Definition (Lean source)
Given a finite series design matrix, the series hat matrix is the fitted-value projection Φ(ΦᵀΦ)⁻¹Φᵀ.
Hat-matrix Frobenius identity. If the series Gram matrix is invertible, then the sum of squares of all entries of the least-squares hat matrix equals the number of series columns.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
seriesLSCoeff_normal_equationstheorem — Normal equations for the closed-form series fit. If the series Gram matrix is invertible, then the residual from the closed-form coefficient vector is orthogonal to every design column.hypothesesconclusion∑ i, lstsqResidual Φ y (seriesLSCoeff Φ y) i * Φ i k = 0Proof (Lean source)
theorem seriesLSCoeff_normal_equations (Φ : Matrix (Fin N) ι ℝ) (y : Fin N → ℝ) (hGram : IsUnit (seriesGram Φ).det) : ∀ k : ι, ∑ i, lstsqResidual Φ y (seriesLSCoeff Φ y) i * Φ i k = 0 := by intro k let b : ι → ℝ := Φᵀ *ᵥ y have hnormal : Φᵀ *ᵥ (y - Φ *ᵥ seriesLSCoeff Φ y) = 0 := by calc Φᵀ *ᵥ (y - Φ *ᵥ seriesLSCoeff Φ y) = b - (seriesGram Φ) *ᵥ seriesLSCoeff Φ y := by rw [Matrix.mulVec_sub, Matrix.mulVec_mulVec] rfl _ = b - (seriesGram Φ) *ᵥ ((seriesGram Φ)⁻¹ *ᵥ b) := by rfl _ = b - ((seriesGram Φ) * (seriesGram Φ)⁻¹) *ᵥ b := by rw [Matrix.mulVec_mulVec] _ = 0 := by rw [Matrix.mul_nonsing_inv _ hGram, Matrix.one_mulVec, sub_self] have hk := congrFun hnormal k simpa [lstsqResidual, mulVec, Matrix.transpose_apply, dotProduct, sub_eq_add_neg, Finset.sum_add_distrib, Finset.sum_neg_distrib, mul_comm, mul_left_comm, mul_assoc] using hk -
seriesLS_fitted_sub_eq_neg_hattheorem — Least-squares fitted-value linearity. For a design matrix Φ, a baseline response vector f, and an additive error vector ε, the fitted-value difference between the baseline fit and the fit to f+ε is -Hε, where H is the series hat matrix.hypothesesconclusionProof (Lean source)
theorem seriesLS_fitted_sub_eq_neg_hat (Φ : Matrix (Fin N) ι ℝ) (f ε : Fin N → ℝ) : Φ *ᵥ (seriesLSCoeff Φ f - seriesLSCoeff Φ (f + ε)) = -(seriesHatMatrix Φ *ᵥ ε) := by simp only [seriesLSCoeff, Matrix.mulVec_add, Matrix.mulVec_sub] rw [sub_add_eq_sub_sub, sub_self, zero_sub] rw [seriesHatMatrix, Matrix.mulVec_mulVec, Matrix.mulVec_mulVec]
Jackson 5 core · 4 supporting Jackson-type approximation bounds for a piecewise-Taylor construction on one-dimensional Hölder classes. ★ piecewiseTaylor_sup_approx_rate
Jackson-type approximation by a piecewise-Taylor function
Jackson-type approximation bounds for a piecewise-Taylor construction on one-dimensional Hölder classes.
This file proves a from-scratch Jackson-type approximation bound for the piecewise-Taylor
approximant on a uniform J-cell partition of a window [lo, hi].
Splitting [lo, hi] into J cells of width δ = (hi − lo)/J and replacing f on each cell
by its degree-p Taylor polynomial, where p = holderDerivOrder β, expanded at
the cell's left endpoint yields a
piecewise polynomial whose uniform (sup-norm) approximation error obeys
sup_{x ∈ [lo,hi]} |f x − g x| ≤ (M / p!) · ((hi − lo)/J)^β = C · J^{−β}
under the standard Hölder convention used here: f has p continuous
derivatives and its p-th derivative satisfies the displayed Hölder-type bound
with exponent β − p. For positive integer β = m, this means p = m - 1
and exponent 1.
The result controls this function-valued approximant only. This file does not define a finite
basis, represent the approximant by a coefficient vector, or relate J to a basis dimension.
Using the bound in SeriesSieve/Prediction.lean therefore requires a separate representation
theorem that supplies the comparator coefficients expected by seriesApprox_le_of_sup.
For a real left endpoint, a real right endpoint, and a nonnegative integer number of cells, the width of each cell in the uniform partition is .
Definition (Lean source)
For a real left endpoint, a real right endpoint, a nonnegative integer number of cells, and a real point, the uniform-partition cell index is the nonnegative floor of the point's displacement from the left endpoint divided by the cell width, capped at so that the right endpoint belongs to the final cell.
For a real left endpoint, a real right endpoint, a nonnegative integer number of cells, and a real point, the base point of the point's cell is the left endpoint plus the cell index times the uniform cell width. The piecewise-Taylor approximant expands its function around this point.
Definition (Lean source)
For a nonnegative Taylor degree, a real-valued function, a real left endpoint, a real right endpoint, a nonnegative integer number of cells, and a real evaluation point, the piecewise-Taylor sieve approximant is the degree- Taylor polynomial of the function, expanded at the left endpoint of the uniform-partition cell containing the evaluation point and evaluated at that point.
Definition (Lean source)
Jackson rate, J^{−β} form. Fix a Hölder exponent β > 0, a nonnegative Hölder constant M, and a nondegenerate window [lo, hi] with lo < hi subdivided into a positive number J of uniform cells. If f has p = holderDerivOrder β continuous derivatives on the window and its p-th derivative obeys the Hölder bound |f^(p) x − f^(p) y| ≤ M · |x − y|^(β − p) for all x, y in the window, then at any evaluation point x in the window, the piecewise-Taylor approximant on the uniform J-cell partition has pointwise error |f x − g x| ≤ C · J^{−β}, with constant C = (M / p!) · (hi − lo)^β independent of J.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
cellWidth_poslemma — The cell width is positive on a nondegenerate window.Proof (Lean source)
lemma cellWidth_pos {lo hi : ℝ} {J : ℕ} (hlohi : lo < hi) (hJ : 0 < J) : 0 < cellWidth lo hi J := by unfold cellWidth have h1 : 0 < hi - lo := by linarith have h2 : (0 : ℝ) < (J : ℝ) := by exact_mod_cast hJ exact div_pos h1 h2 -
cellBase_memlemma — The cell base point lies inside the window [lo, hi].hypotheseslo hi :ℝJ :ℕhlohi :lo < hihJ :0 < Jx :ℝProof (Lean source)
lemma cellBase_mem {lo hi : ℝ} {J : ℕ} (hlohi : lo < hi) (hJ : 0 < J) {x : ℝ} : cellBase lo hi J x ∈ Icc lo hi := by let δ := cellWidth lo hi J have hδ : 0 < δ := cellWidth_pos hlohi hJ constructor · unfold cellBase have hnonneg : 0 ≤ (cellIdx lo hi J x : ℝ) * δ := mul_nonneg (Nat.cast_nonneg _) hδ.le dsimp [δ] at hnonneg ⊢ linarith · unfold cellBase change lo + (cellIdx lo hi J x : ℝ) * δ ≤ hi have hJone : 1 ≤ J := Nat.succ_le_of_lt hJ have hidx_nat : cellIdx lo hi J x ≤ J - 1 := by unfold cellIdx exact min_le_left _ _ have hidx_cast : (cellIdx lo hi J x : ℝ) ≤ (J : ℝ) - 1 := by have hcast : (cellIdx lo hi J x : ℝ) ≤ (J - 1 : ℕ) := by exact_mod_cast hidx_nat have hsub : ((J - 1 : ℕ) : ℝ) = (J : ℝ) - 1 := by rw [Nat.cast_sub hJone, Nat.cast_one] linarith have hmul : (cellIdx lo hi J x : ℝ) * δ ≤ ((J : ℝ) - 1) * δ := mul_le_mul_of_nonneg_right hidx_cast hδ.le have hJnz : (J : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hJ) have hJδ : (J : ℝ) * δ = hi - lo := by dsimp [δ] unfold cellWidth field_simp [hJnz] nlinarith [hmul, hδ] -
cellBase_distlemma — x is within one cell width to the right of its base point: 0 ≤ x − base ≤ δ.hypothesesProof (Lean source)
lemma cellBase_dist {lo hi : ℝ} {J : ℕ} (hlohi : lo < hi) (hJ : 0 < J) {x : ℝ} (hx : x ∈ Icc lo hi) : 0 ≤ x - cellBase lo hi J x ∧ x - cellBase lo hi J x ≤ cellWidth lo hi J := by let δ := cellWidth lo hi J have hδ : 0 < δ := cellWidth_pos hlohi hJ let q := (x - lo) / δ let m : ℕ := ⌊q⌋₊ let i : ℕ := min (J - 1) m have hq0 : 0 ≤ q := by dsimp [q] exact div_nonneg (by linarith [hx.1]) hδ.le have hJnz : (J : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hJ) have hJδ : (J : ℝ) * δ = hi - lo := by dsimp [δ] unfold cellWidth field_simp [hJnz] have hqJ : q ≤ (J : ℝ) := by have hxq' : q * δ = x - lo := by dsimp [q] field_simp [hδ.ne'] have hmul : q * δ ≤ (J : ℝ) * δ := by linarith [hx.2, hJδ, hxq'] exact le_of_mul_le_mul_right hmul hδ have hmq : (m : ℝ) ≤ q := by exact Nat.floor_le hq0 have hqm : q < (m : ℝ) + 1 := by exact Nat.lt_floor_add_one q have him : (i : ℝ) ≤ (m : ℝ) := by exact_mod_cast (min_le_right (J - 1) m) have hcellidx : cellIdx lo hi J x = i := by unfold cellIdx dsimp [δ, q, m, i] have hxq : δ * q = x - lo := by dsimp [q] field_simp [hδ.ne'] have hrepr : x - cellBase lo hi J x = δ * (q - (i : ℝ)) := by unfold cellBase rw [hcellidx] nlinarith [hxq] constructor · rw [hrepr] exact mul_nonneg hδ.le (by linarith [him, hmq]) · rw [hrepr] have hqi : q ≤ (i : ℝ) + 1 := by by_cases hmle : m ≤ J - 1 · have hi_eq_m : i = m := by dsimp [i] exact min_eq_right hmle rw [hi_eq_m] linarith [hqm] · have hlt : J - 1 < m := Nat.lt_of_not_ge hmle have hle : J - 1 ≤ m := le_of_lt hlt have hi_eq_j : i = J - 1 := by dsimp [i] exact min_eq_left hle rw [hi_eq_j] have hJone : 1 ≤ J := Nat.succ_le_of_lt hJ have hcast : ((J - 1 : ℕ) : ℝ) + 1 = (J : ℝ) := by rw [Nat.cast_sub hJone, Nat.cast_one] linarith rw [hcast] exact hqJ have hle1 : q - (i : ℝ) ≤ 1 := by linarith calc δ * (q - (i : ℝ)) ≤ δ * 1 := mul_le_mul_of_nonneg_left hle1 hδ.le _ = cellWidth lo hi J := by simp [δ] -
piecewiseTaylor_sup_approxtheorem — Piecewise-Taylor approximation bound under the standard Hölder convention. If f has p = holderDerivOrder β continuous derivatives and its p-th derivative obeys a Hölder bound with exponent β - p on the window, then the corresponding piecewise-Taylor approximant on a uniform J-cell partition has pointwise error at most (M / p!)·((hi − lo)/J)^β. For positive integer β = m, this uses derivative order m - 1 and Hölder exponent 1.hypothesesf :ℝ → ℝM β lo hi :ℝJ :ℕhβ :0 < βhM :0 ≤ Mhlohi :lo < hihJ :0 < Jhf :ContDiff ℝ ((holderDerivOrder β)) fhb :x :ℝhx :x ∈ Icc lo hiconclusion|f x - piecewiseTaylorApprox (holderDerivOrder β) f lo hi J x|≤ M / ((holderDerivOrder β)).factorial * ((hi - lo) / (J : ℝ)) ^ βProof (Lean source)
theorem piecewiseTaylor_sup_approx {f : ℝ → ℝ} {M β lo hi : ℝ} {J : ℕ} (hβ : 0 < β) (hM : 0 ≤ M) (hlohi : lo < hi) (hJ : 0 < J) (hf : ContDiff ℝ ((holderDerivOrder β)) f) (hb : ∀ x ∈ Icc lo hi, ∀ y ∈ Icc lo hi, |iteratedDeriv (holderDerivOrder β) f x - iteratedDeriv (holderDerivOrder β) f y| ≤ M * |x - y| ^ (β - ((holderDerivOrder β) : ℝ))) {x : ℝ} (hx : x ∈ Icc lo hi) : |f x - piecewiseTaylorApprox (holderDerivOrder β) f lo hi J x| ≤ M / ((holderDerivOrder β)).factorial * ((hi - lo) / (J : ℝ)) ^ β := by have hbase_mem := cellBase_mem (x := x) hlohi hJ have hdist := cellBase_dist hlohi hJ hx have hwpos := cellWidth_pos hlohi hJ -- Hölder–Taylor remainder at base point `cellBase`. have hrem := holder_taylor_remainder (f := f) (M := M) (β := β) (lo := lo) (hi := hi) (t := cellBase lo hi J x) (a := x) hβ hM hbase_mem hx hf hb refine hrem.trans ?_ -- `|x − base|^β ≤ δ^β` since `0 ≤ x − base ≤ δ`. have habs : |x - cellBase lo hi J x| = x - cellBase lo hi J x := abs_of_nonneg hdist.1 have hpow : |x - cellBase lo hi J x| ^ β ≤ (cellWidth lo hi J) ^ β := by rw [habs] exact Real.rpow_le_rpow hdist.1 hdist.2 hβ.le have hcoef : 0 ≤ M / (((holderDerivOrder β)).factorial : ℝ) := div_nonneg hM (by positivity) calc M / (((holderDerivOrder β)).factorial : ℝ) * |x - cellBase lo hi J x| ^ β ≤ M / (((holderDerivOrder β)).factorial : ℝ) * (cellWidth lo hi J) ^ β := mul_le_mul_of_nonneg_left hpow hcoef _ = M / (((holderDerivOrder β)).factorial : ℝ) * ((hi - lo) / (J : ℝ)) ^ β := by rw [cellWidth]
Prediction 1 core · 3 supporting Prediction-error decompositions for series least squares, combining deterministic approximation error with the heteroskedastic-noise variance bound for the projected fit. ★ seriesLS_expected_prediction_le
Series / sieve least-squares prediction error
Prediction-error decompositions for series least squares, combining deterministic approximation error with the heteroskedastic-noise variance bound for the projected fit.
This file proves a conditional oracle inequality for series least-squares prediction from two reusable substrate pieces:
* approximation (deterministic, bias side): the empirical best-approximation error of the
least-squares fit is controlled by the sup-norm error of any comparator, so an externally supplied
approximation bound can transfer to the weighted empirical objective;
* stochastic (variance side): the exact orthogonal (Pythagorean) decomposition of the
prediction error splits off the projected noise, whose expected weighted quadratic form is
σ² · (effective degrees of freedom).
Conditioning on the design, the data fit Φ ĉ and the noise-free projection Φ ĉ⁰ differ by a
deterministic linear image of the noise (the hat matrix), so the stochastic term's expectation
reduces, via the uncorrelated bounded-variance inequality (linearSmoother_variance_le),
to at most σbar²·∑ᵢ wᵢ ∑ₖ aᵢₖ². If a separate design argument bounds that
effective-degree-of-freedom sum by V, and if a separate approximation argument bounds the
noise-free projection error by A, the main theorem gives the oracle inequality A + σ² V.
All results are generic in the design matrix Φ. They do not connect a concrete smoothness
approximant to a finite series basis or prove a J-dependent prediction rate.
Conditional oracle inequality for series least-squares prediction. Suppose the noise-free projection coefficients c0 have residual orthogonal to every design column, so that the noise-free least-squares objective is bounded by A, and suppose the data fit chat ω differs from c0, at every design row i, by a deterministic linear image ∑ₖ a i k · ε k ω of a noise family ε that is square-integrable, mean zero, and uncorrelated with coordinate variances bounded by σbar², with nonnegative weights and the weighted trace sum ∑ᵢ wᵢ ∑ₖ aᵢₖ² bounded by V. Then the expected weighted quadratic prediction error of the fitted series coefficients against the target values f is at most A + σ² V:
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
seriesApprox_le_of_suptheorem — Empirical approximation error is controlled by the best uniform approximant. If the least-squares fit c to target values f has residual orthogonal to every design column (lstsq_normal_equations) and some comparator cstar approximates f uniformly within δ at the design points (|fᵢ − ∑ⱼ cstarⱼ Φᵢⱼ| ≤ δ), then the empirical fit error is at most (∑ᵢ wᵢ)·δ². Applying this to a Jackson approximant requires separately supplying coefficients cstar that represent that approximant in the chosen finite design.hypothesesN :ℕw f :Fin N → ℝc cstar :ι → ℝδ :ℝhw :∀ i, 0 ≤ w ihortho :∀ k : ι, ∑ i, w i * lstsqResidual Φ f c i * Φ i k = 0hsup :∀ i, |f i - ∑ j, cstar j * Φ i j| ≤ δconclusionlstsqObjective Φ w f c ≤ (∑ i, w i) * δ ^ 2Proof (Lean source)
theorem seriesApprox_le_of_sup {N : ℕ} {ι : Type*} [Fintype ι] {Φ : Fin N → ι → ℝ} {w f : Fin N → ℝ} {c cstar : ι → ℝ} {δ : ℝ} (hw : ∀ i, 0 ≤ w i) (hortho : ∀ k : ι, ∑ i, w i * lstsqResidual Φ f c i * Φ i k = 0) (hsup : ∀ i, |f i - ∑ j, cstar j * Φ i j| ≤ δ) : lstsqObjective Φ w f c ≤ (∑ i, w i) * δ ^ 2 := by have hopt := lstsq_objective_le_of_orthogonal hw hortho cstar refine hopt.trans ?_ unfold lstsqObjective calc ∑ i, w i * lstsqResidual Φ f cstar i ^ 2 ≤ ∑ i, w i * δ ^ 2 := by apply Finset.sum_le_sum intro i _ apply mul_le_mul_of_nonneg_left _ (hw i) have hres : |lstsqResidual Φ f cstar i| ≤ δ := by simpa [lstsqResidual] using hsup i calc lstsqResidual Φ f cstar i ^ 2 = |lstsqResidual Φ f cstar i| ^ 2 := (sq_abs _).symm _ ≤ δ ^ 2 := by apply pow_le_pow_left₀ (abs_nonneg _) hres _ = (∑ i, w i) * δ ^ 2 := by rw [← Finset.sum_mul] -
seriesLS_prediction_decomptheorem — Pythagorean decomposition of the series prediction error. If the noise-free projection coefficient c0 (least-squares fit to the true values f) has residual orthogonal to every design column, then for *any* coefficient vector chat the prediction error of Φ·chat against the truth f splits exactly into the approximation error of the projection plus the squared fitted-value gap:hypothesesN :ℕw f :Fin N → ℝc0 chat :ι → ℝhortho :∀ k : ι, ∑ i, w i * lstsqResidual Φ f c0 i * Φ i k = 0conclusionlstsqObjective Φ w f chat= lstsqObjective Φ w f c0 + ∑ i, w i * (∑ j, (c0 j - chat j) * Φ i j) ^ 2Proof (Lean source)
theorem seriesLS_prediction_decomp {N : ℕ} {ι : Type*} [Fintype ι] {Φ : Fin N → ι → ℝ} {w f : Fin N → ℝ} {c0 chat : ι → ℝ} (hortho : ∀ k : ι, ∑ i, w i * lstsqResidual Φ f c0 i * Φ i k = 0) : lstsqObjective Φ w f chat = lstsqObjective Φ w f c0 + ∑ i, w i * (∑ j, (c0 j - chat j) * Φ i j) ^ 2 := lstsq_pythagoras hortho chat -
expected_weighted_sq_image_letheorem — Expected weighted quadratic form of a deterministic linear image of heteroskedastic noise. If the weights are nonnegative, ε is a mean-zero square-integrable family whose coordinates are uncorrelated and have variances bounded by σbar², then the linear image Dᵢ(ω) = ∑ₖ aᵢₖ εₖ(ω) has expected weighted sum of squares bounded by σbar² · ∑ᵢ wᵢ ∑ₖ aᵢₖ².hypothesesΩ :Type*N :ℕμ :ε :Fin N → Ω → ℝw :Fin N → ℝσbar :ℝhw :∀ i, 0 ≤ w ihε :∀ k, MemLp (ε k) 2 μhmean :∀ k, ∫ ω, ε k ω ∂μ = 0hnoise :UncorrelatedVarianceFamily ε μ σbarconclusion∫ ω, ∑ i, w i * (∑ k, a i k * ε k ω) ^ 2 ∂μ ≤ σbar ^ 2 * ∑ i, w i * ∑ k, a i k ^ 2Proof (Lean source)
theorem expected_weighted_sq_image_le {Ω : Type*} {N : ℕ} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {ε : Fin N → Ω → ℝ} {a : Fin N → Fin N → ℝ} {w : Fin N → ℝ} {σbar : ℝ} (hw : ∀ i, 0 ≤ w i) (hε : ∀ k, MemLp (ε k) 2 μ) (hmean : ∀ k, ∫ ω, ε k ω ∂μ = 0) (hnoise : UncorrelatedVarianceFamily ε μ σbar) : ∫ ω, ∑ i, w i * (∑ k, a i k * ε k ω) ^ 2 ∂μ ≤ σbar ^ 2 * ∑ i, w i * ∑ k, a i k ^ 2 := by -- RECIPE (codex): -- Let `D i ω = ∑ k, a i k * ε k ω`. -- (1) Pull the finite sum out of the integral: `integral_finset_sum`, with each summand -- `fun ω => w i * (D i ω)^2` integrable. Integrability: `(D i)` is `MemLp _ 2` as a finite -- sum of `L²` functions (`MemLp.const_mul`, `memLp_finset_sum'`), so `(D i)^2` is `L¹` -- (`MemLp.integrable_sq` / `MemLp.integrable (le_refl)` after `.pow`); the `w i *` is a -- constant multiple (`Integrable.const_mul`). -- (2) Constant `w i` out of each integral (`integral_const_mul`). -- (3) `∫ (D i)^2 = Var[D i; μ]`: because `∫ D i = ∑ k a i k * ∫ ε k = 0` (linearity of the -- integral over the finite sum + `hmean`). Use `ProbabilityTheory.variance_eq` -- (`Var[X] = ∫ X^2 - (∫ X)^2`, valid for `MemLp X 2`) and simplify the `(∫ D i)^2 = 0` term. -- The variance form: `Var[fun ω => ∑ k, a i k * ε k ω; μ]`. -- (4) `Var[fun ω => ∑ k, a i k * ε k ω; μ] = σ^2 * ∑ k, (a i k)^2` by -- `linearSmoother_variance_le (S := a i) hε hnoise`. -- (5) Assemble: `∑ i, w i * (σ^2 * ∑ k, (a i k)^2) = σ^2 * ∑ i, w i * ∑ k, (a i k)^2` -- via `Finset.mul_sum`/`ring`-style sum manipulation (reduce with -- `Finset.sum_congr rfl (fun _ _ => ?_)` then `ring` at the scalar leaf). let D : Fin N → Ω → ℝ := fun i ω => ∑ k, a i k * ε k ω have hDmemlp : ∀ i, MemLp (D i) 2 μ := by intro i dsimp [D] convert memLp_finset_sum' univ (fun k _ => (hε k).const_mul (a i k)) using 1 ext ω simp have hDint : ∀ i, ∫ ω, D i ω ∂μ = 0 := by intro i calc ∫ ω, D i ω ∂μ = ∫ ω, ∑ k, a i k * ε k ω ∂μ := rfl _ = ∑ k, ∫ ω, a i k * ε k ω ∂μ := by simpa using (integral_finset_sum univ (fun k _ => ((hε k).const_mul (a i k)).integrable (by norm_num))) _ = 0 := by simp [integral_const_mul, hmean] have hDsq : ∀ i, ∫ ω, (D i ω) ^ 2 ∂μ ≤ σbar ^ 2 * ∑ k, a i k ^ 2 := by intro i have hvarint : Var[D i; μ] = ∫ ω, (D i ω) ^ 2 ∂μ := by rw [variance_eq_integral (hDmemlp i).aemeasurable] rw [hDint i] simp calc ∫ ω, (D i ω) ^ 2 ∂μ = Var[D i; μ] := hvarint.symm _ ≤ σbar ^ 2 * ∑ k, a i k ^ 2 := by simpa [D] using (linearSmoother_variance_le (Y := ε) (S := a i) hε hnoise (le_refl _)) have hterm_int : ∀ i, Integrable (fun ω => w i * (D i ω) ^ 2) μ := by intro i exact (hDmemlp i).integrable_sq.const_mul (w i) calc ∫ ω, ∑ i, w i * (∑ k, a i k * ε k ω) ^ 2 ∂μ = ∫ ω, ∑ i, w i * (D i ω) ^ 2 ∂μ := by simp [D] _ = ∑ i, ∫ ω, w i * (D i ω) ^ 2 ∂μ := by simpa using (integral_finset_sum univ (fun i _ => hterm_int i)) _ = ∑ i, w i * ∫ ω, (D i ω) ^ 2 ∂μ := by refine Finset.sum_congr rfl (fun i _ => ?_) rw [integral_const_mul] _ ≤ ∑ i, w i * (σbar ^ 2 * ∑ k, a i k ^ 2) := by refine Finset.sum_le_sum (fun i _ => ?_) exact mul_le_mul_of_nonneg_left (hDsq i) (hw i) _ = σbar ^ 2 * ∑ i, w i * ∑ k, a i k ^ 2 := by rw [Finset.mul_sum] refine Finset.sum_congr rfl (fun i _ => ?_) ring
PredictionRate 3 core · 0 supporting The Causalean file Causalean.Stat.Nonparametric.SeriesSieve.Prediction proves a *conditional* oracle inequality seriesLS_expected_prediction_le: 𝔼[‖f − Φ·ĉ‖²_w] ≤ A + σ² · V, where A is any bound on the noise-free least ★ seriesBiasRate_of_jackson_bound★ seriesEffectiveDoF_le★ seriesLS_prediction_rate_of_jackson_bound
Conditional series least-squares prediction bound under an assumed Jackson objective bound
The Causalean file Causalean.Stat.Nonparametric.SeriesSieve.Prediction proves a conditional
oracle inequality seriesLS_expected_prediction_le:
𝔼[‖f − Φ·ĉ‖²_w] ≤ A + σ² · V,
where A is any bound on the noise-free least-squares objective (bias side) and V is any bound
on the effective-degrees-of-freedom sum ∑ᵢ wᵢ ∑ₖ aᵢₖ² (variance side). This module rewrites an
explicitly assumed Jackson-shaped objective bound and derives the finite-dimensional hat-matrix
term. It does not prove that the piecewise-Taylor approximant belongs to a chosen series span.
Main results
* seriesBiasRate_of_jackson_bound — rewrites the assumed Jackson objective bound
A ≤ (∑ᵢ wᵢ)·(C_J·J^{−s/d})² into the explicit bias rate A ≤ ((∑ᵢ wᵢ)·C_J²)·J^{−2s/d}.
The Jackson approximation power of the sieve is taken as an explicit hypothesis (no attempt to
prove Jackson's theorem for a concrete basis).
* seriesEffectiveDoF_le — converts a Frobenius bound into the normalized J/N scale.
* seriesLS_prediction_rate_of_jackson_bound — constructs the least-squares coefficients and hat
matrix from Φ, conditional on the Jackson objective bound. Gram invertibility supplies the
normal equations, fitted-value linearity, and the exact identity ∑ᵢₖ Hᵢₖ² = J, so neither
linearity nor a trace bound is assumed.
Here J^{−s/d} is the real power (J : ℝ) ^ (-(s/d)) (Real.rpow), keeping s, d, J, N, σ as
free parameters. A caller must separately justify the assumed objective bound for its basis and
dimension; the classical series-estimator and Jackson literature is motivation, not a result
formalized by this module.
Bias-rate rewrite from an assumed Jackson objective bound. If the noise-free least-squares objective A := lstsqObjective Φ w f c0 obeys the squared Jackson best-approximation bound A ≤ (∑ᵢ wᵢ)·(C_J·J^{−s/d})² — the shape produced by seriesApprox_le_of_sup with sup-error δ = C_J·J^{−s/d} — then the same objective satisfies the explicit doubled-exponent bias rate A ≤ ((∑ᵢ wᵢ)·C_J²) · J^{−2s/d}:
Formal statement
Proof (Lean source)
Effective degrees of freedom is controlled by J/N. If the sample size N is positive, the least-squares weights are normalized as wᵢ = 1/N, and the hat map a obeys the Frobenius/trace bound ∑ᵢ ∑ₖ aᵢₖ² ≤ Cvar·J, then the weighted coefficient sum — the effective degrees of freedom V of the oracle inequality — obeys the bound Cvar · J / N:
Formal statement
Proof (Lean source)
Series least-squares prediction bound under an assumed Jackson objective bound. Assume a positive sample size, an invertible series Gram matrix, and an error family that is square-integrable, mean zero, and uncorrelated with coordinate variances bounded by σbar². If the noise-free closed-form least-squares fit obeys the squared Jackson approximation bound, then the expected normalized prediction error of the closed-form fit to f+ε is at most the doubled-exponent Jackson term plus σbar² · card(ι)/N. The normal equations, least-squares linearity, and exact hat-matrix Frobenius identity are conclusions of Gram invertibility, not assumptions.