ML.Kernel

lemma effectiveDimension_le_trace_div {μ : ι → ℝ} {lam : ℝ} (hμ : ∀ i, 0 ≤ μ i) (hlam : 0 < lam) (hsum : Summable μ) : effectiveDimension μ lam ≤ (∑' i, μ i) / lam := by have hle : effectiveDimension μ lam ≤ ∑' i, μ i / lam := Summable.tsum_le_tsum (fun i => effectiveDimension_term_le_div hμ hlam i) (summable_effectiveDimension_term hμ hlam hsum) (hsum.div_const lam) rwa [tsum_div_const] at hle

lemma effectiveDimension_antitone {μ : ι → ℝ} {lam₁ lam₂ : ℝ} (hμ : ∀ i, 0 ≤ μ i) (hlam₁ : 0 < lam₁) (hle : lam₁ ≤ lam₂) (hsum : Summable μ) : effectiveDimension μ lam₂ ≤ effectiveDimension μ lam₁ := by have hlam₂ : 0 < lam₂ := lt_of_lt_of_le hlam₁ hle refine Summable.tsum_le_tsum (fun i => ?_) (summable_effectiveDimension_term hμ hlam₂ hsum) (summable_effectiveDimension_term hμ hlam₁ hsum) gcongr <;> linarith [hμ i, hlam₁, hle]

theorem representer_theorem {X H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {feval : H → X → ℝ} {representer : X → H} (hrkhs : HasReproducingRepresenters X H feval representer) {n : ℕ} (x : Fin n → X) (y : Fin n → ℝ) {lam : ℝ} (hlam : 0 < lam) {fhat : H} (hmin : ∀ g : H, krrRisk feval x y lam fhat ≤ krrRisk feval x y lam g) : ∃ α : Fin n → ℝ, fhat = ∑ i, α i • representer (x i) := by classical let M : Submodule ℝ H := span ℝ (Set.range fun i : Fin n => representer (x i)) have : FiniteDimensional ℝ M := FiniteDimensional.span_of_finite ℝ (Set.finite_range _) have : CompleteSpace M := by infer_instance let p : H := M.starProjection fhat have hp_mem : p ∈ M := M.starProjection_apply_mem fhat have hrep_mem : ∀ i : Fin n, representer (x i) ∈ M := by intro i exact Submodule.subset_span ⟨i, rfl⟩ have heval_eq : ∀ i : Fin n, feval fhat (x i) = feval p (x i) := by intro i have horth : inner ℝ (fhat - p) (representer (x i)) = 0 := by exact Submodule.starProjection_inner_eq_zero (K := M) fhat (representer (x i)) (hrep_mem i) rw [hrkhs.reproducing fhat (x i), hrkhs.reproducing p (x i)] calc inner ℝ fhat (representer (x i)) = inner ℝ ((fhat - p) + p) (representer (x i)) := by rw [sub_add_cancel] _ = inner ℝ (fhat - p) (representer (x i)) + inner ℝ p (representer (x i)) := by rw [inner_add_left] _ = inner ℝ p (representer (x i)) := by rw [horth, zero_add] have hdata_eq : (∑ i, (feval fhat (x i) - y i) ^ 2) = ∑ i, (feval p (x i) - y i) ^ 2 := by refine Finset.sum_congr rfl ?_ intro i _ rw [heval_eq i] have hmin_p : krrRisk feval x y lam fhat ≤ krrRisk feval x y lam p := hmin p have hnorm_le : ‖fhat‖ ^ 2 ≤ ‖p‖ ^ 2 := by have hmul_le : lam * ‖fhat‖ ^ 2 ≤ lam * ‖p‖ ^ 2 := by unfold krrRisk at hmin_p rw [hdata_eq] at hmin_p linarith nlinarith have hnorm_decomp : ‖fhat‖ ^ 2 = ‖p‖ ^ 2 + ‖(Mᗮ).starProjection fhat‖ ^ 2 := Submodule.norm_sq_eq_add_norm_sq_starProjection fhat M have hperp_sq : ‖(Mᗮ).starProjection fhat‖ ^ 2 = 0 := by have hnonneg : 0 ≤ ‖(Mᗮ).starProjection fhat‖ ^ 2 := sq_nonneg _ nlinarith have hperp_zero : (Mᗮ).starProjection fhat = 0 := by apply norm_eq_zero.mp have hnonneg : 0 ≤ ‖(Mᗮ).starProjection fhat‖ := norm_nonneg _ nlinarith have hfhat_eq_p : fhat = p := by have hsplit := Submodule.starProjection_add_starProjection_orthogonal (K := M) fhat calc fhat = M.starProjection fhat + (Mᗮ).starProjection fhat := hsplit.symm _ = M.starProjection fhat + 0 := by rw [hperp_zero] _ = p := by rw [add_zero] have hfhat_mem : fhat ∈ M := by simpa [hfhat_eq_p] using hp_mem rcases (Submodule.mem_span_range_iff_exists_fun (R := ℝ) (v := fun i : Fin n => representer (x i)) (x := fhat)).mp hfhat_mem with ⟨α, hα⟩ exact ⟨α, hα.symm⟩

theorem rkhs_ball_empiricalRademacher_le {X H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {feval : H → X → ℝ} {representer : X → H} (hK : HasReproducingRepresenters X H feval representer) {n : ℕ} {κ r : ℝ} (hκ : 0 ≤ κ) (hr : 0 ≤ r) (xs : Fin n → X) (hbound : ∀ k, ‖representer (xs k)‖ ≤ κ) : empiricalRademacherComplexity n (fun (f : {f : H // ‖f‖ ≤ r}) (x : X) => feval (f : H) x) xs ≤ κ * r / sqrt n := by classical let ball := {f : H // ‖f‖ ≤ r} let Y : Fin n → H := fun k => representer (xs k) let w : ball → H := fun f => (f : H) have hw : ∀ f : ball, ‖w f‖ ≤ r := by intro f exact f.2 have hlinear : empiricalRademacherComplexity n (fun (f : ball) (a : H) => inner ℝ (w f) a) Y ≤ κ * r / sqrt n := by exact empiricalRademacherComplexity_innerBall_le κ r hκ hr Y hbound w hw -- Rewrite evaluation into the inner product with the representer; the two -- complexity terms then agree by beta reduction, so close by `exact`. have heval : (fun (f : ball) (x : X) => feval (f : H) x) = fun (f : ball) (x : X) => inner ℝ (w f) (representer x) := by funext f x exact hK.reproducing (f : H) x rw [heval] exact hlinear