ML.Linear

theorem ols_is_squaredLoss_ERM_of_normalEq (X : Matrix Obs Param ℝ) (y : Obs → ℝ) (βhat : Param → ℝ) (hNE : (Xᵀ * X) *ᵥ βhat = Xᵀ *ᵥ y) : ∀ β : Param → ℝ, olsObjective X y βhat ≤ olsObjective X y β := by intro β let δ : Param → ℝ := β - βhat let r : Obs → ℝ := fun i => y i - (X *ᵥ βhat) i let z : Obs → ℝ := X *ᵥ δ have hr : Xᵀ *ᵥ r = 0 := by have hNE' : Xᵀ *ᵥ (X *ᵥ βhat) = Xᵀ *ᵥ y := by simpa only [Matrix.mulVec_mulVec] using hNE change Xᵀ *ᵥ (y - X *ᵥ βhat) = 0 rw [Matrix.mulVec_sub, hNE'.symm] simp have hβ : β = βhat + δ := by ext k simp [δ] have hres : ∀ i, y i - (X *ᵥ β) i = r i - z i := by intro i have hx : X *ᵥ β = X *ᵥ βhat + z := by rw [hβ, Matrix.mulVec_add] rw [hx] simp [r, z] ring have hcross : r ⬝ᵥ z = 0 := by calc r ⬝ᵥ z = r ⬝ᵥ X *ᵥ δ := rfl _ = r ᵥ* X ⬝ᵥ δ := Matrix.dotProduct_mulVec r X δ _ = (Xᵀ *ᵥ r) ⬝ᵥ δ := by rw [Matrix.mulVec_transpose] _ = 0 := by simp [hr] have hobj : olsObjective X y β = olsObjective X y βhat - 2 * (r ⬝ᵥ z) + ∑ i, z i ^ 2 := by unfold olsObjective simp_rw [hres] change (∑ i, (r i - z i) ^ 2) = (∑ i, r i ^ 2) - 2 * (r ⬝ᵥ z) + ∑ i, z i ^ 2 calc (∑ i, (r i - z i) ^ 2) = ∑ i, (r i ^ 2 - 2 * (r i * z i) + z i ^ 2) := by apply Finset.sum_congr rfl intro i _hi ring _ = (∑ i, r i ^ 2) - 2 * (r ⬝ᵥ z) + ∑ i, z i ^ 2 := by simp [dotProduct, Finset.sum_sub_distrib, Finset.sum_add_distrib, Finset.mul_sum] have hnonneg : 0 ≤ ∑ i, z i ^ 2 := Finset.sum_nonneg fun i _hi => sq_nonneg (z i) nlinarith

theorem olsCoef_normalEq [DecidableEq Param] (X : Matrix Obs Param ℝ) (y : Obs → ℝ) (hX : IsUnit (Xᵀ * X).det) : (Xᵀ * X) *ᵥ olsCoef X y = Xᵀ *ᵥ y := by unfold olsCoef rw [Matrix.mulVec_mulVec, Matrix.mul_nonsing_inv _ hX, Matrix.one_mulVec]

theorem rademacherComplexity_l2_ball_le {d n : ℕ} {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xb W : ℝ} (hXb : 0 ≤ Xb) (hW : 0 ≤ W) (X : Ω → EuclideanSpace ℝ (Fin d)) (hXbound : ∀ ω, ‖X ω‖ ≤ Xb) : rademacherComplexity n (fun w : closedBall (0 : EuclideanSpace ℝ (Fin d)) W => fun a : EuclideanSpace ℝ (Fin d) => inner ℝ (w : EuclideanSpace ℝ (Fin d)) a) μ X ≤ Xb * W / sqrt (n : ℝ) := by classical haveI : Nonempty (closedBall (0 : EuclideanSpace ℝ (Fin d)) W) := ⟨⟨0, by simpa [Metric.mem_closedBall, dist_self] using hW⟩⟩ have hpoint : ∀ ω : Fin n → Ω, empiricalRademacherComplexity n (fun w : closedBall (0 : EuclideanSpace ℝ (Fin d)) W => fun a : EuclideanSpace ℝ (Fin d) => inner ℝ (w : EuclideanSpace ℝ (Fin d)) a) (X ∘ ω) ≤ Xb * W / sqrt (n : ℝ) := by intro ω let Y' : Fin n → closedBall (0 : EuclideanSpace ℝ (Fin d)) Xb := fun k => ⟨X (ω k), mem_closedBall_zero_iff.mpr (hXbound (ω k))⟩ simpa [Y', Function.comp_def] using (linear_predictor_l2_bound' (d := d) (n := n) (W := W) (X := Xb) hXb hW Y' id) have hnonneg : ∀ ω : Fin n → Ω, 0 ≤ empiricalRademacherComplexity n (fun w : closedBall (0 : EuclideanSpace ℝ (Fin d)) W => fun a : EuclideanSpace ℝ (Fin d) => inner ℝ (w : EuclideanSpace ℝ (Fin d)) a) (X ∘ ω) := by intro ω unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine Finset.sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro w exact abs_nonneg _ unfold rademacherComplexity calc ∫ ω : Fin n → Ω, empiricalRademacherComplexity n (fun w : closedBall (0 : EuclideanSpace ℝ (Fin d)) W => fun a : EuclideanSpace ℝ (Fin d) => inner ℝ (w : EuclideanSpace ℝ (Fin d)) a) (X ∘ ω) ∂(Measure.pi fun _ : Fin n => μ) ≤ ∫ _ω : Fin n → Ω, Xb * W / sqrt (n : ℝ) ∂(Measure.pi fun _ : Fin n => μ) := by apply MeasureTheory.integral_mono_of_nonneg · exact Filter.Eventually.of_forall hnonneg · exact integrable_const _ · exact Filter.Eventually.of_forall hpoint _ = Xb * W / sqrt (n : ℝ) := by simp

theorem l2Ball_erm_squaredLoss_excess_rate {d n : ℕ} {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xb Yb W : ℝ} (hXb : 0 ≤ Xb) (hYb : 0 ≤ Yb) (hW : 0 ≤ W) (X : Ω → L2BallFeat d Xb Yb) (hX : Measurable X) {t : ℝ} (ht' : t * ((Xb * W) ^ 2 + 2 * Yb * (Xb * W)) ^ 2 ≤ 1 / 2) {ε : ℝ} (hε : 0 ≤ ε) (ŵ : (Fin n → Ω) → L2BallWeight d W) (wstar : L2BallWeight d W) (hERM : ∀ ω : Fin n → Ω, (n : ℝ)⁻¹ * ∑ k, (inner ℝ ((ŵ ω) : EuclideanSpace ℝ (Fin d)) ((X (ω k)).1 : EuclideanSpace ℝ (Fin d)) - ((X (ω k)).2 : ℝ)) ^ 2 ≤ (n : ℝ)⁻¹ * ∑ k, (inner ℝ (wstar : EuclideanSpace ℝ (Fin d)) ((X (ω k)).1 : EuclideanSpace ℝ (Fin d)) - ((X (ω k)).2 : ℝ)) ^ 2) : (Measure.pi (fun _ : Fin n => μ) (fun ω => 4 * ((4 * (Xb * W) ^ 2 + 2 * Yb * Xb * W) / sqrt (n : ℝ)) + 2 * ε < μ[fun ω' => (inner ℝ ((ŵ ω) : EuclideanSpace ℝ (Fin d)) ((X ω').1 : EuclideanSpace ℝ (Fin d)) - ((X ω').2 : ℝ)) ^ 2] - μ[fun ω' => (inner ℝ (wstar : EuclideanSpace ℝ (Fin d)) ((X ω').1 : EuclideanSpace ℝ (Fin d)) - ((X ω').2 : ℝ)) ^ 2])).toReal ≤ (- ε ^ 2 * t * n).exp := by classical haveI : Nonempty (L2BallFeat d Xb Yb) := ⟨(⟨0, by simpa using hXb⟩, ⟨0, by simpa using hYb⟩)⟩ haveI : Nonempty (L2BallWeight d W) := ⟨⟨0, by simpa using hW⟩⟩ -- linear predictor and squared/centered losses set p : L2BallWeight d W → L2BallFeat d Xb Yb → ℝ := fun w a => inner ℝ (w : EuclideanSpace ℝ (Fin d)) (a.1 : EuclideanSpace ℝ (Fin d)) with hp set φ : ℝ → ℝ := clampedSq (Xb * W) with hφdef set f : L2BallWeight d W → L2BallFeat d Xb Yb → ℝ := fun w a => φ (p w a) - 2 * (a.2 : ℝ) * p w a with hf set sqLoss : L2BallWeight d W → L2BallFeat d Xb Yb → ℝ := fun w a => (p w a - (a.2 : ℝ)) ^ 2 with hsq have hXbW : 0 ≤ Xb * W := mul_nonneg hXb hW -- pointwise bounds on the predictor have hpbound : ∀ (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb), |p w a| ≤ Xb * W := by intro w a have hw : ‖(w : EuclideanSpace ℝ (Fin d))‖ ≤ W := by simpa using (mem_closedBall_zero_iff.mp w.2) have ha : ‖(a.1 : EuclideanSpace ℝ (Fin d))‖ ≤ Xb := by simpa using (mem_closedBall_zero_iff.mp a.1.2) calc |p w a| ≤ ‖(w : EuclideanSpace ℝ (Fin d))‖ * ‖(a.1 : EuclideanSpace ℝ (Fin d))‖ := abs_real_inner_le_norm _ _ _ ≤ W * Xb := mul_le_mul hw ha (norm_nonneg _) hW _ = Xb * W := by ring have hybound : ∀ a : L2BallFeat d Xb Yb, |(a.2 : ℝ)| ≤ Yb := by intro a simpa using (mem_closedBall_zero_iff.mp a.2.2) -- `f` is the centered squared loss: `sqLoss = f + y²` have hsqf : ∀ (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb), sqLoss w a = f w a + ((a.2 : ℝ)) ^ 2 := by intro w a have hclamp : φ (p w a) = (p w a) ^ 2 := by rw [hφdef]; exact clampedSq_eq_sq (hpbound w a) simp only [hsq, hf, hclamp] ring -- uniform bound on `f` have hb0 : (0 : ℝ) ≤ (Xb * W) ^ 2 + 2 * Yb * (Xb * W) := by positivity have hfbound : ∀ (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb), |f w a| ≤ (Xb * W) ^ 2 + 2 * Yb * (Xb * W) := by intro w a have h1 : |φ (p w a)| ≤ (Xb * W) ^ 2 := by rw [hφdef, abs_of_nonneg (clampedSq_nonneg _ _)] exact clampedSq_le_sq hXbW _ have h2 : |2 * (a.2 : ℝ) * p w a| ≤ 2 * Yb * (Xb * W) := by rw [abs_mul, abs_mul, show |(2 : ℝ)| = 2 from by norm_num] nlinarith [hybound a, hpbound w a, abs_nonneg ((a.2 : ℝ)), abs_nonneg (p w a), hYb, hXbW] calc |f w a| = |φ (p w a) - 2 * (a.2 : ℝ) * p w a| := by rw [hf] _ ≤ |φ (p w a)| + |2 * (a.2 : ℝ) * p w a| := abs_sub _ _ _ ≤ (Xb * W) ^ 2 + 2 * Yb * (Xb * W) := add_le_add h1 h2 -- continuity of the predictor and losses have hcont_x1 : Continuous (fun a : L2BallFeat d Xb Yb => (a.1 : EuclideanSpace ℝ (Fin d))) := continuous_subtype_val.comp continuous_fst have hcont_x2 : Continuous (fun a : L2BallFeat d Xb Yb => (a.2 : ℝ)) := continuous_subtype_val.comp continuous_snd have hpcont_a : ∀ w : L2BallWeight d W, Continuous (fun a : L2BallFeat d Xb Yb => p w a) := by intro w exact continuous_const.inner hcont_x1 have hpcont_w : ∀ a : L2BallFeat d Xb Yb, Continuous (fun w : L2BallWeight d W => p w a) := by intro a exact continuous_subtype_val.inner continuous_const have hfcont_a : ∀ w : L2BallWeight d W, Continuous (fun a : L2BallFeat d Xb Yb => f w a) := by intro w exact ((continuous_clampedSq _).comp (hpcont_a w)).sub ((continuous_const.mul hcont_x2).mul (hpcont_a w)) have hfcont_w : ∀ a : L2BallFeat d Xb Yb, Continuous (fun w : L2BallWeight d W => f w a) := by intro a exact ((continuous_clampedSq _).comp (hpcont_w a)).sub (continuous_const.mul (hpcont_w a)) have hfmeas : ∀ w : L2BallWeight d W, Measurable (f w) := fun w => (hfcont_a w).measurable -- Rademacher-complexity bound for the centered squared-loss class set Cf : ℝ := 4 * (Xb * W) ^ 2 + 2 * Yb * Xb * W with hCf have hRC : rademacherComplexity n f μ X ≤ Cf / sqrt (n : ℝ) := by -- uniform empirical bound, over every sample have hemp : ∀ S : Fin n → L2BallFeat d Xb Yb, empiricalRademacherComplexity n f S ≤ Cf / sqrt (n : ℝ) := by intro S -- (1) predictor complexity from the linear L²-ball bound have hpS : empiricalRademacherComplexity n p S ≤ Xb * W / sqrt (n : ℝ) := by have h := linear_predictor_l2_bound' (d := d) (n := n) (ι := L2BallWeight d W) (W := W) (X := Xb) hXb hW (fun k => (S k).1) (fun w => w) rw [hp] exact h -- (2) quadratic part via contraction with the clamped square have hquadbd : ∀ (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb), |φ (p w a)| ≤ (Xb * W) ^ 2 := by intro w a rw [hφdef, abs_of_nonneg (clampedSq_nonneg _ _)] exact clampedSq_le_sq hXbW _ have hcontr := empiricalRademacherComplexity_contraction_abs_of_bddAbove (ι := L2BallWeight d W) φ (L := 2 * (Xb * W)) (by rw [hφdef]; exact lipschitzAt0_clampedSq hXbW) p (M := Xb * W) hXbW hpbound n S have hquad : empiricalRademacherComplexity n (fun (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb) => φ (p w a)) S ≤ 4 * (Xb * W) ^ 2 / sqrt (n : ℝ) := by calc empiricalRademacherComplexity n (fun (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb) => φ (p w a)) S ≤ 2 * (2 * (Xb * W)) * empiricalRademacherComplexity n p S := hcontr _ ≤ 2 * (2 * (Xb * W)) * (Xb * W / sqrt (n : ℝ)) := mul_le_mul_of_nonneg_left hpS (by positivity) _ = 4 * (Xb * W) ^ 2 / sqrt (n : ℝ) := by ring -- (3) cross part: a linear class over rescaled features `2y·x` set featCross : L2BallFeat d Xb Yb → EuclideanSpace ℝ (Fin d) := fun a => (2 * (a.2 : ℝ)) • (a.1 : EuclideanSpace ℝ (Fin d)) with hfeat have hmem : ∀ a : L2BallFeat d Xb Yb, featCross a ∈ closedBall (0 : EuclideanSpace ℝ (Fin d)) (2 * Yb * Xb) := by intro a rw [mem_closedBall_zero_iff, hfeat, norm_smul, Real.norm_eq_abs, abs_mul, show |(2 : ℝ)| = 2 from by norm_num] have hx : ‖(a.1 : EuclideanSpace ℝ (Fin d))‖ ≤ Xb := by simpa using mem_closedBall_zero_iff.mp a.1.2 nlinarith [hybound a, hx, abs_nonneg ((a.2 : ℝ)), norm_nonneg (a.1 : EuclideanSpace ℝ (Fin d)), hYb, hXb] have hcrossfun : (fun (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb) => 2 * (a.2 : ℝ) * p w a) = (fun (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb) => inner ℝ (w : EuclideanSpace ℝ (Fin d)) (featCross a)) := by funext w a rw [hfeat, real_inner_smul_right, hp] have hcrossS : empiricalRademacherComplexity n (fun (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb) => 2 * (a.2 : ℝ) * p w a) S ≤ 2 * Yb * Xb * W / sqrt (n : ℝ) := by rw [hcrossfun] have h := linear_predictor_l2_bound' (d := d) (n := n) (ι := L2BallWeight d W) (W := W) (X := 2 * Yb * Xb) (by positivity) hW (fun k => ⟨featCross (S k), hmem (S k)⟩) (fun w => w) exact h -- (4) combine the two parts via sub-additivity have hcrossbd : ∀ (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb), |2 * (a.2 : ℝ) * p w a| ≤ 2 * Yb * (Xb * W) := by intro w a rw [abs_mul, abs_mul, show |(2 : ℝ)| = 2 from by norm_num] nlinarith [hybound a, hpbound w a, abs_nonneg ((a.2 : ℝ)), abs_nonneg (p w a), hYb, hXbW] have hsub := empiricalRademacherComplexity_sub_le (ι := L2BallWeight d W) (fun (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb) => φ (p w a)) (fun (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb) => 2 * (a.2 : ℝ) * p w a) (MF := (Xb * W) ^ 2) (MG := 2 * Yb * (Xb * W)) (by positivity) (by positivity) hquadbd hcrossbd n S have hfeq : empiricalRademacherComplexity n f S = empiricalRademacherComplexity n (fun (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb) => φ (p w a) - 2 * (a.2 : ℝ) * p w a) S := rfl rw [hfeq] calc empiricalRademacherComplexity n (fun (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb) => φ (p w a) - 2 * (a.2 : ℝ) * p w a) S ≤ empiricalRademacherComplexity n (fun (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb) => φ (p w a)) S + empiricalRademacherComplexity n (fun (w : L2BallWeight d W) (a : L2BallFeat d Xb Yb) => 2 * (a.2 : ℝ) * p w a) S := hsub _ ≤ 4 * (Xb * W) ^ 2 / sqrt (n : ℝ) + 2 * Yb * Xb * W / sqrt (n : ℝ) := add_le_add hquad hcrossS _ = Cf / sqrt (n : ℝ) := by rw [← add_div] -- integrate the uniform empirical bound have hnn : ∀ ω : Fin n → Ω, 0 ≤ empiricalRademacherComplexity n f (X ∘ ω) := by intro ω unfold empiricalRademacherComplexity refine mul_nonneg (by positivity) (Finset.sum_nonneg fun σ _ => ?_) exact Real.iSup_nonneg fun i => abs_nonneg _ unfold rademacherComplexity calc ∫ ω, empiricalRademacherComplexity n f (X ∘ ω) ∂(Measure.pi fun _ : Fin n => μ) ≤ ∫ _ω, Cf / sqrt (n : ℝ) ∂(Measure.pi fun _ : Fin n => μ) := by apply integral_mono_of_nonneg (Filter.Eventually.of_forall hnn) (integrable_const _) exact Filter.Eventually.of_forall (fun ω => hemp (X ∘ ω)) _ = Cf / sqrt (n : ℝ) := by simp -- the `f`-ERM hypothesis follows from the squared-loss ERM hypothesis have hERMf : ∀ ω : Fin n → Ω, (n : ℝ)⁻¹ * ∑ k, f (ŵ ω) (X (ω k)) ≤ (n : ℝ)⁻¹ * ∑ k, f wstar (X (ω k)) := by intro ω have hrw : ∀ w : L2BallWeight d W, (n : ℝ)⁻¹ * ∑ k, f w (X (ω k)) = (n : ℝ)⁻¹ * ∑ k, sqLoss w (X (ω k)) - (n : ℝ)⁻¹ * ∑ k, ((X (ω k)).2 : ℝ) ^ 2 := by intro w rw [← mul_sub, ← Finset.sum_sub_distrib] refine congrArg _ (Finset.sum_congr rfl fun k _ => ?_) have := hsqf w (X (ω k)) linarith rw [hrw (ŵ ω), hrw wstar] have hE := hERM ω simp only [hsq, hp] linarith [hE] have key := erm_oracle_inequality_separable (μ := μ) (n := n) (f := f) hfmeas X hX (b := (Xb * W) ^ 2 + 2 * Yb * (Xb * W)) hb0 hfbound hfcont_w ht' hε ŵ wstar hERMf -- transport from `f`-excess to genuine squared-loss excess refine le_trans ?_ key refine ENNReal.toReal_mono (measure_ne_top _ _) (measure_mono ?_) intro ω hω -- population split: `∫ f w = ∫ sqLoss w − ∫ y²` have hsqcont_a : ∀ w : L2BallWeight d W, Continuous (fun a : L2BallFeat d Xb Yb => sqLoss w a) := by intro w exact ((hpcont_a w).sub hcont_x2).pow 2 have hpop : ∀ w : L2BallWeight d W, μ[fun ω' => f w (X ω')] = μ[fun ω' => sqLoss w (X ω')] - μ[fun ω' => ((X ω').2 : ℝ) ^ 2] := by intro w have hInt_sq : Integrable (fun ω' => sqLoss w (X ω')) μ := by refine Integrable.of_bound (((hsqcont_a w).measurable.comp hX).aestronglyMeasurable) ((Xb * W + Yb) ^ 2) ?_ filter_upwards with ω' have hpy : |p w (X ω') - ((X ω').2 : ℝ)| ≤ Xb * W + Yb := (abs_sub _ _).trans (add_le_add (hpbound w (X ω')) (hybound (X ω'))) rw [Real.norm_eq_abs, abs_of_nonneg (by positivity : (0 : ℝ) ≤ sqLoss w (X ω'))] have heq : sqLoss w (X ω') = |p w (X ω') - ((X ω').2 : ℝ)| ^ 2 := by rw [hsq, sq_abs] rw [heq] nlinarith [hpy, abs_nonneg (p w (X ω') - ((X ω').2 : ℝ))] have hInt_y : Integrable (fun ω' => ((X ω').2 : ℝ) ^ 2) μ := by refine Integrable.of_bound ((hcont_x2.pow 2).measurable.comp hX).aestronglyMeasurable (Yb ^ 2) ?_ filter_upwards with ω' rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] nlinarith [hybound (X ω'), sq_abs ((X ω').2 : ℝ), abs_nonneg ((X ω').2 : ℝ)] have hpt : (fun ω' => f w (X ω')) = (fun ω' => sqLoss w (X ω') - ((X ω').2 : ℝ) ^ 2) := by funext ω'; have := hsqf w (X ω'); linarith rw [hpt, integral_sub hInt_sq hInt_y] -- f-excess equals squared-loss excess (the `y²` term cancels) have hexc : μ[fun ω' => f (ŵ ω) (X ω')] - μ[fun ω' => f wstar (X ω')] = μ[fun ω' => sqLoss (ŵ ω) (X ω')] - μ[fun ω' => sqLoss wstar (X ω')] := by rw [hpop (ŵ ω), hpop wstar]; ring have hgoal_eq : μ[fun ω' => (inner ℝ ((ŵ ω) : EuclideanSpace ℝ (Fin d)) ((X ω').1 : EuclideanSpace ℝ (Fin d)) - ((X ω').2 : ℝ)) ^ 2] - μ[fun ω' => (inner ℝ (wstar : EuclideanSpace ℝ (Fin d)) ((X ω').1 : EuclideanSpace ℝ (Fin d)) - ((X ω').2 : ℝ)) ^ 2] = μ[fun ω' => sqLoss (ŵ ω) (X ω')] - μ[fun ω' => sqLoss wstar (X ω')] := by simp only [hsq, hp] have hthr : 4 • rademacherComplexity n f μ X + 2 * ε ≤ 4 * (Cf / sqrt (n : ℝ)) + 2 * ε := by have he : 4 • rademacherComplexity n f μ X = 4 * rademacherComplexity n f μ X := by -- … truncated; follow the source link for the rest …

theorem bestLinearPredictor_minimizes_populationRisk (P : Measure (X' × ℝ)) (φ : FeatureMap X' K) {βstar : K → ℝ} (hortho : IsPopulationOLS P φ βstar) (β : K → ℝ) (hint_star : HasFinitePopulationRisk squaredLoss P (fun x => ∑ k, βstar k * φ.φ x k)) (hint_β : HasFinitePopulationRisk squaredLoss P (fun x => ∑ k, β k * φ.φ x k)) (hcross : ∀ k, Integrable (fun z => (z.2 - ∑ j, βstar j * φ.φ z.1 j) * φ.φ z.1 k) P) : populationRisk squaredLoss P (fun x => ∑ k, βstar k * φ.φ x k) ≤ populationRisk squaredLoss P (fun x => ∑ k, β k * φ.φ x k) := by let m : X' → ℝ := fun x => ∑ k, βstar k * φ.φ x k let h : X' → ℝ := fun x => ∑ k, β k * φ.φ x k have hint_m' : Integrable (fun z : X' × ℝ => (z.2 - m z.1) ^ 2) P := by simpa [HasFinitePopulationRisk, squaredLoss, m] using hint_star have hint_h' : Integrable (fun z : X' × ℝ => (z.2 - h z.1) ^ 2) P := by simpa [HasFinitePopulationRisk, squaredLoss, h] using hint_β have hdiff : Integrable (fun z : X' × ℝ => (z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) P := hint_h'.sub hint_m' have hmh_expand : ∀ z : X' × ℝ, m z.1 - h z.1 = ∑ k, (βstar k - β k) * φ.φ z.1 k := by intro z calc m z.1 - h z.1 = (∑ k, βstar k * φ.φ z.1 k) - ∑ k, β k * φ.φ z.1 k := rfl _ = ∑ k, (βstar k * φ.φ z.1 k - β k * φ.φ z.1 k) := by rw [Finset.sum_sub_distrib] _ = ∑ k, (βstar k - β k) * φ.φ z.1 k := by exact Finset.sum_congr rfl (fun k _ => by ring) have hcross_mh : Integrable (fun z : X' × ℝ => (z.2 - m z.1) * (m z.1 - h z.1)) P := by have hsum_int : Integrable (fun z : X' × ℝ => ∑ k, (βstar k - β k) * ((z.2 - m z.1) * φ.φ z.1 k)) P := by exact integrable_finset_sum (s := univ) (fun k _ => (hcross k).const_mul (βstar k - β k)) refine hsum_int.congr ?_ filter_upwards with z rw [hmh_expand z] rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro k _ ring have horth : ∫ z, (z.2 - m z.1) * (m z.1 - h z.1) ∂P = 0 := by calc ∫ z, (z.2 - m z.1) * (m z.1 - h z.1) ∂P = ∫ z, ∑ k, (βstar k - β k) * ((z.2 - m z.1) * φ.φ z.1 k) ∂P := by apply integral_congr_ae filter_upwards with z rw [hmh_expand z] rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro k _ ring _ = ∑ k, ∫ z, (βstar k - β k) * ((z.2 - m z.1) * φ.φ z.1 k) ∂P := by rw [integral_finset_sum] intro k _ exact (hcross k).const_mul (βstar k - β k) _ = ∑ k, (βstar k - β k) * ∫ z, (z.2 - m z.1) * φ.φ z.1 k ∂P := by refine Finset.sum_congr rfl ?_ intro k _ rw [integral_const_mul] _ = 0 := by rw [Finset.sum_eq_zero] intro k _ rw [hortho k] ring have hsq_int : Integrable (fun z : X' × ℝ => (m z.1 - h z.1) ^ 2) P := by have htmp : Integrable (fun z : X' × ℝ => ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) - 2 * ((z.2 - m z.1) * (m z.1 - h z.1))) P := hdiff.sub (hcross_mh.const_mul 2) convert htmp using 1 funext z ring have hdiff_nonneg : 0 ≤ ∫ z, ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) ∂P := by calc 0 ≤ ∫ z, (m z.1 - h z.1) ^ 2 ∂P := by exact integral_nonneg (fun z => sq_nonneg _) _ = 2 * ∫ z, (z.2 - m z.1) * (m z.1 - h z.1) ∂P + ∫ z, (m z.1 - h z.1) ^ 2 ∂P := by simp [horth] _ = ∫ z, 2 * ((z.2 - m z.1) * (m z.1 - h z.1)) + (m z.1 - h z.1) ^ 2 ∂P := by rw [integral_add] · rw [integral_const_mul] · exact hcross_mh.const_mul 2 · exact hsq_int _ = ∫ z, ((z.2 - h z.1) ^ 2 - (z.2 - m z.1) ^ 2) ∂P := by apply integral_congr_ae filter_upwards with z ring have hle : ∫ z, (z.2 - m z.1) ^ 2 ∂P ≤ ∫ z, (z.2 - h z.1) ^ 2 ∂P := by have hnonneg_sub : 0 ≤ ∫ z, (z.2 - h z.1) ^ 2 ∂P - ∫ z, (z.2 - m z.1) ^ 2 ∂P := by rw [← integral_sub hint_h' hint_m'] exact hdiff_nonneg linarith simpa [populationRisk, squaredLoss, m, h] using hle