Stat.Concentration.Rademacher.Contraction

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

lemma signAtom_coe_real_eq_neg_one_or_one (s : SignAtom) : (s : ℝ) = -1 ∨ (s : ℝ) = 1 := by rcases s with ⟨z, hz⟩ simp only [Finset.mem_insert, Int.reduceNeg, Finset.mem_singleton, Int.cast_eq_one] at hz ⊢ rcases hz with rfl | rfl · left norm_num · right norm_num

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)]