Stat.Concentration.Rademacher

lemma zero_mem_starHull {ι 𝒳 : Type*} [Nonempty ι] (F : ι → 𝒳 → ℝ) : (fun _ : 𝒳 => (0 : ℝ)) ∈ starHull F := by refine ⟨Classical.arbitrary ι, 0, le_refl 0, by norm_num, ?_⟩ ext x simp

lemma starHull_congr {ι 𝒳 : Type*} {F G : ι → 𝒳 → ℝ} (h : ∀ i x, F i x = G i x) : starHull F = starHull G := by have hFG : F = G := by funext i x exact h i x rw [hFG]

lemma starHullEval_mem_starHull {ι 𝒳 : Type*} (F : ι → 𝒳 → ℝ) (p : starHullParam ι) : starHullEval F p ∈ starHull F := by refine ⟨p.2, p.1.val, p.1.property.1, p.1.property.2, ?_⟩ funext x simp [starHullEval, smul_eq_mul]

lemma finite_iSup_eq_value {α : Type*} [Nonempty α] [Finite α] (f : α → ℝ) : ∃ a : α, (⨆ x, f x) = f a ∧ ∀ x, f x ≤ f a := by classical rcases Finite.exists_max f with ⟨a, ha⟩ refine ⟨a, ?_, ha⟩ exact le_antisymm (ciSup_le ha) (le_ciSup (Finite.bddAbove_range f) a)

lemma sup_pair_lipschitz_scaled {ι : Type*} [Nonempty ι] [Finite ι] (φ : ℝ → ℝ) {L c : ℝ} (hc : 0 ≤ c) (hφ : ∀ x y, |φ x - φ y| ≤ L * |x - y|) (a : ι → ℝ) (b : ι → ℝ) : (⨆ i, a i + c * φ (b i)) + (⨆ i, a i - c * φ (b i)) ≤ (⨆ i, a i + c * (L * b i)) + (⨆ i, a i - c * (L * b i)) := by classical rcases finite_iSup_eq_value (fun i : ι => a i + c * φ (b i)) with ⟨i₁, hi₁eq, _hi₁max⟩ rcases finite_iSup_eq_value (fun i : ι => a i - c * φ (b i)) with ⟨i₂, hi₂eq, _hi₂max⟩ rw [hi₁eq, hi₂eq] have hdiff : φ (b i₁) - φ (b i₂) ≤ L * |b i₁ - b i₂| := by exact (le_abs_self _).trans (hφ (b i₁) (b i₂)) have hcdiff : c * (φ (b i₁) - φ (b i₂)) ≤ c * (L * |b i₁ - b i₂|) := by exact mul_le_mul_of_nonneg_left hdiff hc by_cases hcase : b i₂ ≤ b i₁ · have habs : |b i₁ - b i₂| = b i₁ - b i₂ := abs_of_nonneg (sub_nonneg.mpr hcase) have hmain : a i₁ + c * φ (b i₁) + (a i₂ - c * φ (b i₂)) ≤ (a i₁ + c * (L * b i₁)) + (a i₂ - c * (L * b i₂)) := by rw [habs] at hcdiff linarith refine hmain.trans ?_ exact add_le_add (le_ciSup (Finite.bddAbove_range (fun i : ι => a i + c * (L * b i))) i₁) (le_ciSup (Finite.bddAbove_range (fun i : ι => a i - c * (L * b i))) i₂) · have hcase' : b i₁ ≤ b i₂ := le_of_not_ge hcase have habs : |b i₁ - b i₂| = b i₂ - b i₁ := by rw [abs_sub_comm] exact abs_of_nonneg (sub_nonneg.mpr hcase') have hmain : a i₁ + c * φ (b i₁) + (a i₂ - c * φ (b i₂)) ≤ (a i₂ + c * (L * b i₂)) + (a i₁ - c * (L * b i₁)) := by rw [habs] at hcdiff linarith refine hmain.trans ?_ have hp := le_ciSup (Finite.bddAbove_range (fun i : ι => a i + c * (L * b i))) i₂ have hm := le_ciSup (Finite.bddAbove_range (fun i : ι => a i - c * (L * b i))) i₁ linarith

theorem empiricalRademacherComplexity_without_abs_smul_class (F : ι → 𝒳 → ℝ) (c : ℝ) (hc : 0 ≤ c) (n : ℕ) (S : Fin n → 𝒳) : empiricalRademacherComplexity_without_abs n (fun i x => c * F i x) S = c * empiricalRademacherComplexity_without_abs n F S := by unfold empiricalRademacherComplexity_without_abs have hsum : (∑ σ : Signs n, ⨆ i, (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (c * F i (S k))) = c * ∑ σ : Signs n, ⨆ i, (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k) := by rw [Finset.mul_sum] refine Finset.sum_congr rfl fun σ _ => ?_ calc (⨆ i, (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (c * F i (S k))) = ⨆ i, c * ((n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)) := by refine iSup_congr fun i => ?_ calc (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (c * F i (S k)) = (n : ℝ)⁻¹ * (c * ∑ k : Fin n, (σ k : ℝ) * F i (S k)) := by congr 1 rw [Finset.mul_sum] refine Finset.sum_congr rfl fun k _ => by ring _ = c * ((n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)) := by ring _ = c * ⨆ i, (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k) := by exact (Real.mul_iSup_of_nonneg hc (fun i => (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k))).symm rw [hsum] ring

lemma lipschitzAt0_neg (φ : ℝ → ℝ) {L : ℝ} (hφ : LipschitzAt0 φ L) : LipschitzAt0 (fun x => -φ x) L := by refine ⟨by simp [hφ.1], ?_⟩ intro x y rw [show -φ x - -φ y = -(φ x - φ y) from by ring, abs_neg] exact hφ.2 x y

lemma iSup_abs_le_iSup_add_iSup_neg_of_exists_zero {α : Type*} [Finite α] (x : α → ℝ) (h0 : ∃ a : α, x a = 0) : (⨆ a, |x a|) ≤ (⨆ a, x a) + (⨆ a, -x a) := by classical letI := ofFinite α rcases h0 with ⟨a0, ha0⟩ letI : Nonempty α := ⟨a0⟩ have hsup_nonneg : 0 ≤ ⨆ a, x a := by rw [← ha0] exact le_ciSup (Finite.bddAbove_range x) a0 have hsup_neg_nonneg : 0 ≤ ⨆ a, -x a := by rw [← show -x a0 = 0 by rw [ha0]; simp] exact le_ciSup (Finite.bddAbove_range fun a => -x a) a0 refine ciSup_le ?_ intro a by_cases hx : 0 ≤ x a · rw [abs_of_nonneg hx] have hxle : x a ≤ ⨆ a, x a := le_ciSup (Finite.bddAbove_range x) a linarith · have hxle : -x a ≤ ⨆ a, -x a := le_ciSup (Finite.bddAbove_range fun a => -x a) a rw [abs_of_neg (lt_of_not_ge hx)] linarith

lemma empirical_abs_withZero_le_no_abs_plus_neg [Finite ι] (F : Option ι → 𝒳 → ℝ) (hzero : ∀ x, F none x = 0) (n : ℕ) (S : Fin n → 𝒳) : empiricalRademacherComplexity n F S ≤ empiricalRademacherComplexity_without_abs n F S + empiricalRademacherComplexity_without_abs n (fun i x => -F i x) S := by classical letI := ofFinite ι unfold empiricalRademacherComplexity empiricalRademacherComplexity_without_abs rw [← mul_add] refine mul_le_mul_of_nonneg_left ?_ (by positivity) rw [← Finset.sum_add_distrib] refine Finset.sum_le_sum ?_ intro σ _ have hzero_inner : (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F none (S k) = 0 := by simp [hzero] have hpoint := iSup_abs_le_iSup_add_iSup_neg_of_exists_zero (fun i : Option ι => (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)) ⟨none, hzero_inner⟩ have hneg : (⨆ i : Option ι, -((n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k))) = (⨆ i : Option ι, (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (-F i (S k))) := by refine iSup_congr fun i => ?_ calc -((n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)) = (n : ℝ)⁻¹ * (-(∑ k : Fin n, (σ k : ℝ) * F i (S k))) := by ring _ = (n : ℝ)⁻¹ * (∑ k : Fin n, -((σ k : ℝ) * F i (S k))) := by rw [Finset.sum_neg_distrib] _ = (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (-F i (S k)) := by congr 1 refine Finset.sum_congr rfl fun k _ => by ring simpa [hneg] using hpoint

theorem empiricalRademacherComplexity_smul_class (F : ι → 𝒳 → ℝ) (c : ℝ) (n : ℕ) (S : Fin n → 𝒳) : empiricalRademacherComplexity n (fun i x => c * F i x) S = |c| * empiricalRademacherComplexity n F S := by unfold empiricalRademacherComplexity have hsum : (∑ σ : Signs n, ⨆ i, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (c * F i (S k))|) = |c| * ∑ σ : Signs n, ⨆ i, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)| := by rw [Finset.mul_sum] refine Finset.sum_congr rfl fun σ _ => ?_ calc (⨆ i, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (c * F i (S k))|) = ⨆ i, |c| * |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)| := by refine iSup_congr fun i => ?_ have hlin : (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (c * F i (S k)) = c * ((n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)) := by calc (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (c * F i (S k)) = (n : ℝ)⁻¹ * (c * ∑ k : Fin n, (σ k : ℝ) * F i (S k)) := by congr 1 rw [Finset.mul_sum] refine Finset.sum_congr rfl fun k _ => by ring _ = c * ((n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)) := by ring rw [hlin, abs_mul] _ = |c| * ⨆ i, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)| := by exact (Real.mul_iSup_of_nonneg (abs_nonneg c) (fun i => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)|)).symm rw [hsum] ring

lemma absInner_le_of_bound (H : ι → 𝒳 → ℝ) {M : ℝ} (hM0 : 0 ≤ M) (hH : ∀ i x, |H i x| ≤ M) (n : ℕ) (S : Fin n → 𝒳) (σ : Signs n) (i : ι) : |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * H i (S k)| ≤ M := by by_cases hn : n = 0 · subst hn; simpa using hM0 · have hn_pos : 0 < (n : ℝ) := by positivity rw [abs_mul, abs_of_nonneg (by positivity : (0:ℝ) ≤ (n:ℝ)⁻¹)] calc (n : ℝ)⁻¹ * |∑ k : Fin n, (σ k : ℝ) * H i (S k)| ≤ (n : ℝ)⁻¹ * ∑ k : Fin n, M := by refine mul_le_mul_of_nonneg_left ?_ (by positivity) refine (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum ?_) intro k _ rw [abs_mul] rcases signAtom_coe_real_eq_neg_one_or_one (σ k) with h | h · rw [h]; simpa using hH i (S k) · rw [h]; simpa using hH i (S k) _ = M := by rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] field_simp

lemma absInner_bddAbove (H : ι → 𝒳 → ℝ) {M : ℝ} (hM0 : 0 ≤ M) (hH : ∀ i x, |H i x| ≤ M) (n : ℕ) (S : Fin n → 𝒳) (σ : Signs n) : BddAbove (range (fun i => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * H i (S k)|)) := by refine ⟨M, ?_⟩ rintro _ ⟨i, rfl⟩ exact absInner_le_of_bound H hM0 hH n S σ i

theorem empiricalRademacherComplexity_sub_le [Nonempty ι] (F G : ι → 𝒳 → ℝ) {MF MG : ℝ} (hMF0 : 0 ≤ MF) (hMG0 : 0 ≤ MG) (hF : ∀ i x, |F i x| ≤ MF) (hG : ∀ i x, |G i x| ≤ MG) (n : ℕ) (S : Fin n → 𝒳) : empiricalRademacherComplexity n (fun i x => F i x - G i x) S ≤ empiricalRademacherComplexity n F S + empiricalRademacherComplexity n G S := by classical unfold empiricalRademacherComplexity rw [← mul_add, ← Finset.sum_add_distrib] refine mul_le_mul_of_nonneg_left (Finset.sum_le_sum ?_) (by positivity) intro σ _ have hbddF := absInner_bddAbove F hMF0 hF n S σ have hbddG := absInner_bddAbove G hMG0 hG n S σ refine ciSup_le (fun i => ?_) have hsplit : (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (F i (S k) - G i (S k)) = ((n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)) - ((n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * G i (S k)) := by rw [← mul_sub, ← Finset.sum_sub_distrib] refine congrArg _ (Finset.sum_congr rfl fun k _ => by ring) rw [hsplit] refine (abs_sub _ _).trans ?_ exact add_le_add (le_ciSup hbddF i) (le_ciSup hbddG i)

theorem empiricalRademacherComplexity_contraction_abs_of_bddAbove [Nonempty ι] (φ : ℝ → ℝ) {L : ℝ} (hφ : LipschitzAt0 φ L) (F : ι → 𝒳 → ℝ) {M : ℝ} (hM0 : 0 ≤ M) (hM : ∀ i x, |F i x| ≤ M) (n : ℕ) (S : Fin n → 𝒳) : empiricalRademacherComplexity n (fun i x => φ (F i x)) S ≤ 2 * L * empiricalRademacherComplexity n F S := by classical have hL : 0 ≤ L := by have h := hφ.2 0 1 norm_num [hφ.1] at h exact (abs_nonneg _).trans h haveI hSigns : Nonempty (Signs n) := ⟨fun _ => ⟨1, by decide⟩⟩ -- uniform bound for the composed class `φ ∘ F` have hLM0 : 0 ≤ L * M := mul_nonneg hL hM0 have hφM : ∀ i x, |φ (F i x)| ≤ L * M := by intro i x have h := hφ.2 (F i x) 0 rw [hφ.1, sub_zero, sub_zero] at h exact h.trans (mul_le_mul_of_nonneg_left (hM i x) hL) have hcard : (0 : ℝ) < (card (Signs n) : ℝ) := by exact_mod_cast Fintype.card_pos (α := Signs n) refine le_of_forall_pos_le_add (fun ε hε => ?_) -- per-sign ε-approximate maximizers (explicit supremand form) have hex : ∀ σ : Signs n, ∃ i, (⨆ j, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * φ (F j (S k))|) - ε < |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * φ (F i (S k))| := by intro σ exact exists_lt_of_lt_ciSup (sub_lt_self _ hε) choose iσ hiσ using hex -- the finite subindex collecting all per-sign maximizers set T : Finset ι := Finset.image iσ Finset.univ with hT haveI : Nonempty {x // x ∈ T} := ⟨⟨iσ (Classical.arbitrary (Signs n)), Finset.mem_image.mpr ⟨_, Finset.mem_univ _, rfl⟩⟩⟩ -- Fintype contraction on the subindex `↥T` have hcontr := rademacher_contraction_abs (ι := {x // x ∈ T}) φ hφ (fun j => F j.val) n S -- (b) restricting the index only lowers the (with-abs) complexity have hb : empiricalRademacherComplexity n (fun j : {x // x ∈ T} => F j.val) S ≤ empiricalRademacherComplexity n F S := by unfold empiricalRademacherComplexity refine mul_le_mul_of_nonneg_left (Finset.sum_le_sum ?_) (by positivity) intro σ _ exact ciSup_le (fun j => le_ciSup (absInner_bddAbove F hM0 hM n S σ) j.val) -- (a) the ε-maximizers recover the full supremum up to ε have ha : empiricalRademacherComplexity n (fun i x => φ (F i x)) S ≤ empiricalRademacherComplexity n (fun (j : {x // x ∈ T}) x => φ (F j.val x)) S + ε := by unfold empiricalRademacherComplexity have hpt : ∀ σ : Signs n, (⨆ i, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * φ (F i (S k))|) ≤ (⨆ j : {x // x ∈ T}, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * φ (F j.val (S k))|) + ε := by intro σ have hmem : iσ σ ∈ T := Finset.mem_image.mpr ⟨σ, Finset.mem_univ _, rfl⟩ have hbddT : BddAbove (range (fun j : {x // x ∈ T} => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * φ (F j.val (S k))|)) := Finite.bddAbove_range _ have hle := le_ciSup hbddT (⟨iσ σ, hmem⟩ : {x // x ∈ T}) have := hiσ σ linarith calc (card (Signs n) : ℝ)⁻¹ * ∑ σ : Signs n, ⨆ i, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * φ (F i (S k))| ≤ (card (Signs n) : ℝ)⁻¹ * ∑ σ : Signs n, ((⨆ j : {x // x ∈ T}, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * φ (F j.val (S k))|) + ε) := by refine mul_le_mul_of_nonneg_left (Finset.sum_le_sum fun σ _ => hpt σ) (by positivity) _ = (card (Signs n) : ℝ)⁻¹ * ∑ σ : Signs n, (⨆ j : {x // x ∈ T}, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * φ (F j.val (S k))|) + (card (Signs n) : ℝ)⁻¹ * (card (Signs n) : ℝ) * ε := by rw [Finset.sum_add_distrib, Finset.sum_const, Finset.card_univ, nsmul_eq_mul] ring _ = (card (Signs n) : ℝ)⁻¹ * ∑ σ : Signs n, (⨆ j : {x // x ∈ T}, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * φ (F j.val (S k))|) + ε := by rw [inv_mul_cancel₀ (ne_of_gt hcard)]; ring calc empiricalRademacherComplexity n (fun i x => φ (F i x)) S ≤ empiricalRademacherComplexity n (fun (j : {x // x ∈ T}) x => φ (F j.val x)) S + ε := ha _ ≤ 2 * L * empiricalRademacherComplexity n (fun j : {x // x ∈ T} => F j.val) S + ε := by linarith [hcontr] _ ≤ 2 * L * empiricalRademacherComplexity n F S + ε := by nlinarith [mul_le_mul_of_nonneg_left hb (by linarith : (0:ℝ) ≤ 2 * L)]

lemma localRademacherComplexity_nonneg (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) (n : ℕ) (r : ℝ) : 0 ≤ localRademacherComplexity F norm μ X n r := by unfold localRademacherComplexity rademacherComplexity apply MeasureTheory.integral_nonneg intro ω unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro p exact abs_nonneg _

lemma empiricalRademacherComplexity_mono_of_inner {ι' : Type*} {n : ℕ} (f g : ι' → 𝒳 → ℝ) (S : Fin n → 𝒳) (hbdd_g : ∀ σ : Signs n, BddAbove (range fun i => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * g i (S k)|)) (h : ∀ σ : Signs n, ∀ i : ι', |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * f i (S k)| ≤ |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * g i (S k)|) : empiricalRademacherComplexity n f S ≤ empiricalRademacherComplexity n g S := by unfold empiricalRademacherComplexity refine mul_le_mul_of_nonneg_left ?_ (by positivity) refine Finset.sum_le_sum ?_ intro σ _ refine Real.iSup_le ?_ ?_ · intro i exact le_trans (h σ i) (le_ciSup (hbdd_g σ) i) · refine Real.iSup_nonneg ?_ intro i exact abs_nonneg _

lemma abs_inner_starHullZeroOut_mono (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) {r₁ r₂ : ℝ} (hr : r₁ ≤ r₂) {n : ℕ} (S : Fin n → 𝒳) (σ : Signs n) (p : starHullParam ι) : |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₁ p (S k)| ≤ |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₂ p (S k)| := by -- Three-way case split on `norm (starHullEval F p)` vs `r₁, r₂`. -- Cases (A) `≤ r₁` and (C) `> r₂`: both inner sums are equal pointwise -- (either both zero, or both `α • F i`). Case (B) `r₁ < · ≤ r₂`: LHS -- inner sum is `0` (every k is zeroed), so |LHS| = 0 ≤ |RHS|. by_cases h₁ : norm (starHullEval F p) ≤ r₁ · have h₂ : norm (starHullEval F p) ≤ r₂ := le_trans h₁ hr apply le_of_eq have hsum : ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₁ p (S k) = ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₂ p (S k) := by refine Finset.sum_congr rfl fun k _ => ?_ simp [starHullZeroOut, h₁, h₂] rw [hsum] · -- LHS evaluates to 0 since every coordinate is zeroed out have hlhs : (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₁ p (S k) = 0 := by have : ∀ k ∈ (Finset.univ : Finset (Fin n)), (σ k : ℝ) * starHullZeroOut F norm r₁ p (S k) = 0 := by intro k _ simp [starHullZeroOut, h₁] rw [Finset.sum_eq_zero this] ring rw [hlhs] simp only [abs_zero, Int.reduceNeg, abs_mul, abs_inv, Nat.abs_cast, ge_iff_le] positivity

lemma abs_starHullZeroOut_mono (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) {r₁ r₂ : ℝ} (h : r₁ ≤ r₂) (p : starHullParam ι) (x : 𝒳) : |starHullZeroOut F norm r₁ p x| ≤ |starHullZeroOut F norm r₂ p x| := by unfold starHullZeroOut by_cases h₁ : norm (starHullEval F p) ≤ r₁ · -- both branches active and equal have h₂ : norm (starHullEval F p) ≤ r₂ := le_trans h₁ h simp [h₁, h₂] · -- LHS is 0 in absolute value; RHS is non-negative simp [h₁]

lemma abs_starHullZeroOut_le_starHullEval (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (r : ℝ) (p : starHullParam ι) (x : 𝒳) : |starHullZeroOut F norm r p x| ≤ |starHullEval F p x| := by unfold starHullZeroOut by_cases h : norm (starHullEval F p) ≤ r · simp [h] · simp [h]

lemma localRademacherComplexity_mono_r (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) (n : ℕ) {r₁ r₂ : ℝ} (h : r₁ ≤ r₂) (hbdd : ∀ S : Fin n → 𝒳, ∀ σ : Signs n, BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₂ p (S k)|)) (hint : Integrable (fun ω : Fin n → Ω => empiricalRademacherComplexity n (starHullZeroOut F norm r₂) (X ∘ ω)) (Measure.pi (fun _ => μ))) : localRademacherComplexity F norm μ X n r₁ ≤ localRademacherComplexity F norm μ X n r₂ := by unfold localRademacherComplexity rademacherComplexity apply MeasureTheory.integral_mono_of_nonneg · exact Filter.Eventually.of_forall fun ω => by unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro p exact abs_nonneg _ · exact hint · exact Filter.Eventually.of_forall fun ω => empiricalRademacherComplexity_mono_of_inner (starHullZeroOut F norm r₁) (starHullZeroOut F norm r₂) (X ∘ ω) (fun σ => hbdd (X ∘ ω) σ) (fun σ p => abs_inner_starHullZeroOut_mono F norm h (X ∘ ω) σ p)

lemma localRademacherComplexity_le_upperBound {F : ι → 𝒳 → ℝ} {norm : (𝒳 → ℝ) → ℝ} {μ : Measure Ω} {X : Ω → 𝒳} {n : ℕ} {ψ : ℝ → ℝ} (hub : RademacherUpperBound F norm μ X n ψ) {r : ℝ} (hr : 0 ≤ r) : localRademacherComplexity F norm μ X n r ≤ ψ r := by unfold localRademacherComplexity exact hub r hr

lemma rademacherComplexity_zeroOut_le_starHullZeroOut (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) (n : ℕ) {r : ℝ} (hbdd : ∀ S : Fin n → 𝒳, ∀ σ : Signs n, BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p (S k)|)) (hint : Integrable (fun ω : Fin n → Ω => empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)) (Measure.pi (fun _ => μ))) : rademacherComplexity n (fun i ω => if norm (F i) ≤ r then F i (X ω) else 0) μ id ≤ rademacherComplexity n (starHullZeroOut F norm r) μ X := by -- The LHS integrand is `empiricalRademacherComplexity n f (id ∘ ω)` where -- `f i x = if norm (F i) ≤ r then F i x else 0`. For any sample path -- `S = X ∘ ω`, the function `f i (S k) = starHullZeroOut F norm r (⟨1, _⟩, i) (S k)`, -- so the sup over `i : ι` is dominated by the sup over `p : starHullParam ι`. -- The integral inequality then follows from pointwise dominance plus integrability. unfold rademacherComplexity apply MeasureTheory.integral_mono_of_nonneg · exact Filter.Eventually.of_forall fun ω => by unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro i exact abs_nonneg _ · exact hint · exact Filter.Eventually.of_forall fun ω => by unfold empiricalRademacherComplexity refine mul_le_mul_of_nonneg_left ?_ (by positivity) refine Finset.sum_le_sum ?_ intro σ _ refine Real.iSup_le ?_ ?_ · intro i let p : starHullParam ι := (⟨(1 : ℝ), by simp [Set.mem_Icc]⟩, i) have hsum : ∑ k : Fin n, (σ k : ℝ) * (if norm (F i) ≤ r then F i (X ((id ∘ ω) k)) else 0) = ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p ((X ∘ ω) k) := by refine Finset.sum_congr rfl ?_ intro k _ have hp : starHullZeroOut F norm r p ((X ∘ ω) k) = if norm (F i) ≤ r then F i (X ((id ∘ ω) k)) else 0 := by unfold starHullZeroOut rw [starHullEval_one] rfl rw [hp] rw [hsum] exact le_ciSup (hbdd (X ∘ ω) σ) p · refine Real.iSup_nonneg ?_ intro i exact abs_nonneg _

@[causal_defs_simps] lemma empiricalRademacherComplexity_eq {𝒳 ι : Type*} (n : ℕ) (f : ι → 𝒳 → ℝ) (S : Fin n → 𝒳) : empiricalRademacherComplexity n f S = (card (Signs n) : ℝ)⁻¹ * ∑ σ : Signs n, ⨆ i, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * f i (S k)| := rfl

@[causal_defs_simps] lemma rademacherComplexity_eq {Ω 𝒳 ι : Type*} [MeasurableSpace Ω] (n : ℕ) (f : ι → 𝒳 → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) : rademacherComplexity n f μ X = ∫ ω : Fin n → Ω, empiricalRademacherComplexity n f (X ∘ ω) ∂(pi fun _ => μ) := rfl

lemma empiricalRademacherComplexity_congr_sample {𝒳 ι : Type*} (n : ℕ) (f f' : ι → 𝒳 → ℝ) (sample : Fin n → 𝒳) (h : ∀ i k, f i (sample k) = f' i (sample k)) : empiricalRademacherComplexity n f sample = empiricalRademacherComplexity n f' sample := by simp only [causal_defs_simps] congr 1 apply Finset.sum_congr rfl intro σ _hσ congr 1 ext i congr 2 apply Finset.sum_congr rfl intro k _hk rw [h i k]

lemma rademacherComplexity_congr_ae_all {Ω 𝒳 ι : Type*} [MeasurableSpace Ω] (n : ℕ) (f f' : ι → 𝒳 → ℝ) (μ : Measure Ω) [SigmaFinite μ] (sample : Ω → 𝒳) (h : ∀ᵐ ω ∂μ, ∀ i : ι, f i (sample ω) = f' i (sample ω)) : rademacherComplexity n f μ sample = rademacherComplexity n f' μ sample := by simp only [causal_defs_simps] apply integral_congr_ae have hprod : ∀ᵐ s : Fin n → Ω ∂Measure.pi (fun _ : Fin n => μ), ∀ i : ι, ∀ k : Fin n, f i (sample (s k)) = f' i (sample (s k)) := by filter_upwards [Filter.eventually_all.2 fun k : Fin n => Measure.tendsto_eval_ae_ae.eventually h] with s hs i k exact hs k i filter_upwards [hprod] with s hs exact empiricalRademacherComplexity_congr_sample n f f' (sample ∘ s) (fun i k => hs i k)