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 := 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 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