Stat.Concentration.Covering

lemma empiricalDist_proj (S : Fin n → 𝒳) (f : 𝒳 → ℝ) (i : Fin n) : |f (S i)|/√n ≤ empiricalNorm S f := by calc _ = √(f (S i)^2)/√n := by have : √(f (S i)^2) = |f (S i)| := by exact Real.sqrt_sq_eq_abs (f (S i)) rw [this] _ = √((f (S i)^2)/n) := by simp _ ≤ _ := by dsimp [empiricalNorm] apply Real.sqrt_le_sqrt rw [one_div_mul_eq_div] refine div_le_div_of_nonneg_right ?_ ?_ · have hnonneg : ∀ j ∈ univ, 0 ≤ (f (S j))^2 := by intro j hj; exact sq_nonneg _ have hi : i ∈ univ := by simp simpa using (Finset.single_le_sum (s := univ) (f := fun j => (f (S j))^2) hnonneg hi) · simp

lemma coveringNumber_exists {X : Type*} {A : Set X} [PseudoMetricSpace X] (ha : TotallyBounded A) {ε : ℝ} (εpos : ε > 0) : ∃ n : Nat, ∃ t : Finset X, t.card = n ∧ A ⊆ ⋃ y ∈ t, ball y ε := by have hball := Metric.finite_approx_of_totallyBounded ha ε εpos have ⟨t, ⟨_ht, tfin, tball⟩⟩ := hball have : Fintype t := tfin.fintype let n : Nat := this.card exists n exists t.toFinset constructor · exact Set.toFinset_card t · convert tball simp only [Set.mem_toFinset]

theorem coveringNumber_antitone {X : Type*} [PseudoMetricSpace X] {A : Set X} (ha : TotallyBounded A) : AntitoneOn (coveringNumber ha) (Ioi 0) := by intro ε₁ hε₁ ε₂ hε₂ hε₁ε₂ rw [coveringNumber_eq ha hε₁, coveringNumber_eq ha hε₂] apply Nat.find_mono intro n ⟨t, ht₁, ht₂⟩ exists t, ht₁ apply ht₂.trans apply Set.iUnion_mono intro _ apply Set.iUnion_mono intro _ exact Metric.ball_subset_ball hε₁ε₂

theorem coveringNumber_nonzero {X : Type*} [PseudoMetricSpace X] {A : Set X} (hs : A.Nonempty) (ha : TotallyBounded A) {ε : ℝ} (hε : ε > 0) : 0 < coveringNumber ha ε := by rw [coveringNumber_eq ha hε] rw [Nat.find_pos] simpa using Set.nonempty_iff_ne_empty.mp hs

theorem coveringNumber_aemeasurable {X : Type*} [PseudoMetricSpace X] {A : Set X} (ha : TotallyBounded A) (μ : Measure ℝ) : AEMeasurable (coveringNumber ha) μ := by have h₀ : AEMeasurable (coveringNumber ha) (μ.restrict (Ioi 0)) := aemeasurable_restrict_of_antitoneOn measurableSet_Ioi (coveringNumber_antitone ha) convert (aemeasurable_indicator_iff measurableSet_Ioi).mpr h₀ ext ε if h : ε ∈ Ioi 0 then rw [Set.indicator_of_mem h] else rw [Set.indicator_of_notMem h] rw [coveringNumber, dif_neg (by exact h)]

lemma coveringFinset_cover {X : Type*} [PseudoMetricSpace X] {A : Set X} (ha : TotallyBounded A) {ε : ℝ} (hε : ε > 0) : A ⊆ ⋃ y ∈ coveringFinset ha hε, ball y ε := by simpa [coveringFinset, coveringNumber_exists] using (Classical.choose_spec (Nat.find_spec (coveringNumber_exists (X := X) (A := A) ha hε))).2

lemma coveringFinset_card {X : Type*} [PseudoMetricSpace X] {A : Set X} (ha : TotallyBounded A) {ε : ℝ} (hε : ε > 0) : (coveringFinset ha hε).card = coveringNumber ha ε := by have h := (Classical.choose_spec (Nat.find_spec (coveringNumber_exists (X := X) (A := A) ha hε))).1 simpa [coveringFinset, coveringNumber_eq (X := X) (A := A) ha hε, coveringNumber_exists] using h

lemma mem_growthFamily_iff {π : ι → 𝒳 → Bool} {S : Fin n → 𝒳} {A : Finset (Fin n)} : A ∈ growthFamily π S ↔ ∃ i : ι, restrictionPattern (π i) S = A := by classical simp [growthFamily]

lemma restrictionPattern_mem_iff {p : 𝒳 → Bool} {S : Fin n → 𝒳} {j : Fin n} : j ∈ restrictionPattern p S ↔ p (S j) = true := by classical simp [restrictionPattern]

theorem card_growthFamily_le_sum_choose (𝒜 : Finset (Finset (Fin n))) (hvd : 𝒜.vcDim ≤ d) : 𝒜.card ≤ ∑ k ∈ Iic d, n.choose k := by classical calc 𝒜.card ≤ 𝒜.shatterer.card := Finset.card_le_card_shatterer 𝒜 _ ≤ ∑ k ∈ Iic 𝒜.vcDim, (card (Fin n)).choose k := Finset.card_shatterer_le_sum_vcDim _ = ∑ k ∈ Iic 𝒜.vcDim, n.choose k := by simp _ ≤ ∑ k ∈ Iic d, n.choose k := by refine Finset.sum_le_sum_of_subset_of_nonneg ?_ ?_ · simpa [Finset.Iic_subset_Iic] using hvd · intro _ _ _ exact zero_le _

lemma empirical_dist_eq_zero_of_factor_pattern {F : ι → 𝒳 → ℝ} {S : Fin n → 𝒳} {π : ι → 𝒳 → Bool} {φ : Fin n → Bool → ℝ} (hfactor : ∀ i j, F i (S j) = φ j (π i (S j))) {i i' : ι} (hpat : restrictionPattern (π i') S = restrictionPattern (π i) S) : dist (EmpiricalFunctionSpace.mk (F := F) (S := S) i) (EmpiricalFunctionSpace.mk (F := F) (S := S) i') = 0 := by have hpoint : ∀ j : Fin n, F i (S j) = F i' (S j) := by intro j rw [hfactor i j, hfactor i' j] apply congrArg (φ j) apply Bool.eq_iff_iff.mpr rw [← restrictionPattern_mem_iff (p := π i') (S := S) (j := j), hpat, restrictionPattern_mem_iff (p := π i) (S := S) (j := j)] simp [empiricalNorm, hpoint]

lemma patternCover_card_le {F : ι → 𝒳 → ℝ} (π : ι → 𝒳 → Bool) (S : Fin n → 𝒳) : (patternCover (F := F) π S).card ≤ (growthFamily π S).card := by classical let f : (growthFamily π S) → EmpiricalFunctionSpace F S := fun A => EmpiricalFunctionSpace.mk (F := F) (S := S) (choose ((mem_growthFamily_iff (π := π) (S := S) (A := A.1)).mp A.2)) calc (patternCover (F := F) π S).card = ((growthFamily π S).attach.image f).card := by rfl _ ≤ (growthFamily π S).attach.card := Finset.card_image_le _ = (growthFamily π S).card := Finset.card_attach

lemma patternCover_covers {F : ι → 𝒳 → ℝ} {S : Fin n → 𝒳} {π : ι → 𝒳 → Bool} {φ : Fin n → Bool → ℝ} (hfactor : ∀ i j, F i (S j) = φ j (π i (S j))) {ε : ℝ} (hε : 0 < ε) : (Set.univ : Set (EmpiricalFunctionSpace F S)) ⊆ ⋃ y ∈ patternCover (F := F) π S, ball y ε := by classical intro q _ let A : Finset (Fin n) := restrictionPattern (π q.index) S have hA : A ∈ growthFamily π S := by rw [mem_growthFamily_iff] exact ⟨q.index, rfl⟩ let a : (growthFamily π S) := ⟨A, hA⟩ let repIndex : ι := choose ((mem_growthFamily_iff (π := π) (S := S) (A := a.1)).mp a.2) let rep : EmpiricalFunctionSpace F S := ⟨repIndex⟩ have hrep_mem : rep ∈ patternCover (F := F) π S := by rw [patternCover] exact Finset.mem_image.mpr ⟨a, Finset.mem_attach _ _, rfl⟩ refine Set.mem_iUnion.mpr ⟨rep, Set.mem_iUnion.mpr ⟨hrep_mem, ?_⟩⟩ rw [Metric.mem_ball] have hrep_pattern : restrictionPattern (π rep.index) S = restrictionPattern (π q.index) S := by dsimp [rep, repIndex] exact Classical.choose_spec ((mem_growthFamily_iff (π := π) (S := S) (A := a.1)).mp a.2) calc dist q rep = 0 := by cases q exact empirical_dist_eq_zero_of_factor_pattern (F := F) (S := S) (π := π) (φ := φ) hfactor hrep_pattern _ < ε := hε

theorem vc_coveringNumber_le_growth {F : ι → 𝒳 → ℝ} {S : Fin n → 𝒳} {π : ι → 𝒳 → Bool} {φ : Fin n → Bool → ℝ} (hfactor : ∀ i j, F i (S j) = φ j (π i (S j))) (h' : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) {ε : ℝ} (hε : 0 < ε) : coveringNumber h' ε ≤ (growthFamily π S).card := by classical rw [coveringNumber_eq h' hε] let t : Finset (EmpiricalFunctionSpace F S) := patternCover (F := F) π S have hfind : find (coveringNumber_exists h' hε) ≤ t.card := Nat.find_min' (coveringNumber_exists h' hε) (m := t.card) ⟨t, rfl, patternCover_covers hfactor hε⟩ exact le_trans hfind (patternCover_card_le (F := F) π S)

theorem log_coveringNumber_le_of_card_bound [Nonempty ι] {F : ι → 𝒳 → ℝ} {S : Fin n → 𝒳} {π : ι → 𝒳 → Bool} {φ : Fin n → Bool → ℝ} (hfactor : ∀ i j, F i (S j) = φ j (π i (S j))) (h' : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) {ε : ℝ} (hε : 0 < ε) {N : ℕ} (hcard : (growthFamily π S).card ≤ N) : log (coveringNumber h' ε) ≤ log N := by classical have hcov_card : coveringNumber h' ε ≤ (growthFamily π S).card := vc_coveringNumber_le_growth hfactor h' hε have hcov_N : coveringNumber h' ε ≤ N := le_trans hcov_card hcard have hcov_pos : 0 < coveringNumber h' ε := by have hnonempty : (Set.univ : Set (EmpiricalFunctionSpace F S)).Nonempty := by obtain ⟨i⟩ := (inferInstance : Nonempty ι) exact ⟨⟨i⟩, by simp⟩ exact coveringNumber_nonzero hnonempty h' hε have hcovN_real : ((coveringNumber h' ε : ℕ) : ℝ) ≤ (N : ℝ) := by exact_mod_cast hcov_N exact Real.log_le_log (Nat.cast_pos.mpr hcov_pos) hcovN_real

lemma sum_choose_le_succ_mul_pow (hn_pos : 0 < n) : ((∑ k ∈ Iic d, n.choose k : ℕ) : ℝ) ≤ ((d + 1 : ℕ) : ℝ) * (n : ℝ) ^ d := by have hsum_nat : (∑ k ∈ Iic d, n.choose k) ≤ (d + 1) * n ^ d := by calc (∑ k ∈ Iic d, n.choose k) ≤ ∑ k ∈ Iic d, n ^ d := by refine Finset.sum_le_sum ?_ intro k hk have hk_le : k ≤ d := by simpa using hk exact le_trans (Nat.choose_le_pow n k) (Nat.pow_le_pow_right hn_pos hk_le) _ = (d + 1) * n ^ d := by simp [Nat.card_Iic, Finset.sum_const] exact_mod_cast hsum_nat

lemma weightedHammingSq_nonneg {n : ℕ} (w : Fin n → ℝ) (hw : ∀ j, 0 ≤ w j) (a b : Fin n → Bool) : 0 ≤ weightedHammingSq w a b := by classical unfold weightedHammingSq exact sum_nonneg fun j _ => by by_cases h : a j = b j · simp [h] · simp [h, hw j]

lemma subsamplePattern_mem_iff {n m : ℕ} {J : Fin m → Fin n} {a : Fin n → Bool} {i : Fin m} : i ∈ subsamplePattern J a ↔ a (J i) = true := by classical simp [subsamplePattern]

lemma sum_choose_le_succ_pow (n d : ℕ) : (∑ k ∈ Iic d, n.choose k) ≤ (n + 1) ^ d := by calc (∑ k ∈ Iic d, n.choose k) ≤ ∑ k ∈ Iic d, n ^ k := by refine Finset.sum_le_sum ?_ intro k _hk exact Nat.choose_le_pow n k _ ≤ ∑ k ∈ Iic d, d.choose k * n ^ k := by refine Finset.sum_le_sum ?_ intro k hk have hk' : k ≤ d := by simpa using hk have hchoose_pos : 1 ≤ d.choose k := Nat.succ_le_of_lt (Nat.choose_pos hk') simpa [one_mul] using Nat.mul_le_mul_right (n ^ k) hchoose_pos _ = (n + 1) ^ d := by rw [add_pow] simp only [one_pow, mul_one, Nat.cast_id] apply Finset.sum_congr · ext k simp · intro k _hk rw [Nat.mul_comm]

lemma subsamplePattern_eq_iff {n m : ℕ} {J : Fin m → Fin n} {a b : Fin n → Bool} : subsamplePattern J a = subsamplePattern J b ↔ ∀ t : Fin m, a (J t) = b (J t) := by classical constructor · intro h t by_cases ha : a (J t) = true · have ht : t ∈ subsamplePattern J b := by rw [← h, subsamplePattern_mem_iff] exact ha rw [subsamplePattern_mem_iff] at ht rw [ha, ht] · have ha_false : a (J t) = false := by exact Bool.eq_false_of_not_eq_true ha by_cases hb : b (J t) = true · have ht : t ∈ subsamplePattern J a := by rw [h, subsamplePattern_mem_iff] exact hb rw [subsamplePattern_mem_iff] at ht exact elim (ha ht) · have hb_false : b (J t) = false := by exact Bool.eq_false_of_not_eq_true hb rw [ha_false, hb_false] · intro h ext t simp [subsamplePattern_mem_iff, h t]

lemma per_pair_collision_sum {n m : ℕ} (w : Fin n → ℝ) (a b : Fin n → Bool) : (∑ J : Fin m → Fin n, (∏ t : Fin m, w (J t)) * (if (∀ t : Fin m, a (J t) = b (J t)) then (1 : ℝ) else 0)) = (∑ j ∈ Finset.univ.filter (fun j : Fin n => a j = b j), w j) ^ m := by classical let g : Fin n → ℝ := fun j => w j * (if a j = b j then (1 : ℝ) else 0) have hpoint : ∀ J : Fin m → Fin n, (∏ t : Fin m, w (J t)) * (if (∀ t : Fin m, a (J t) = b (J t)) then (1 : ℝ) else 0) = ∏ t : Fin m, g (J t) := by intro J by_cases h : ∀ t : Fin m, a (J t) = b (J t) · simp [g, h] · have hprod_zero : ∏ t : Fin m, (if a (J t) = b (J t) then (1 : ℝ) else 0) = 0 := by rw [Finset.prod_eq_zero_iff] push_neg at h rcases h with ⟨t, ht⟩ exact ⟨t, Finset.mem_univ t, by simp [ht]⟩ have hgprod_zero : (∏ t : Fin m, g (J t)) = 0 := by rw [Finset.prod_eq_zero_iff] push_neg at h rcases h with ⟨t, ht⟩ exact ⟨t, Finset.mem_univ t, by simp [g, ht]⟩ simp [h, hgprod_zero] calc (∑ J : Fin m → Fin n, (∏ t : Fin m, w (J t)) * (if (∀ t : Fin m, a (J t) = b (J t)) then (1 : ℝ) else 0)) = ∑ J : Fin m → Fin n, ∏ t : Fin m, g (J t) := by exact Finset.sum_congr rfl fun J _ => hpoint J _ = (∑ j : Fin n, g j) ^ m := product_sum_normalization g _ = (∑ j ∈ Finset.univ.filter (fun j : Fin n => a j = b j), w j) ^ m := by congr 1 simp [g, Finset.sum_filter]

lemma averaging_exists_zero_count {ι : Type*} [Fintype ι] (μ : ι → ℝ) (cnt : ι → ℕ) (hμsum : ∑ i : ι, μ i = 1) (hμnonneg : ∀ i, 0 ≤ μ i) (hmean : ∑ i : ι, μ i * (cnt i : ℝ) < 1) : ∃ i, cnt i = 0 := by classical by_contra hnone push_neg at hnone have hge : 1 ≤ ∑ i : ι, μ i * (cnt i : ℝ) := by calc 1 = ∑ i : ι, μ i := by rw [hμsum] _ = ∑ i : ι, μ i * (1 : ℝ) := by simp _ ≤ ∑ i : ι, μ i * (cnt i : ℝ) := by refine Finset.sum_le_sum ?_ intro i _hi exact mul_le_mul_of_nonneg_left (by exact_mod_cast Nat.succ_le_of_lt (Nat.pos_of_ne_zero (hnone i))) (hμnonneg i) exact not_lt_of_ge hge hmean

lemma collision_bound {n m : ℕ} (w : Fin n → ℝ) (hw : ∀ j, 0 ≤ w j) (r ε W : ℝ) (hr : 0 < r) (hW : W = ∑ j : Fin n, w j) (hWpos : 0 < W) (hwsum : W ≤ r ^ 2) (a b : Fin n → Bool) (hsep : ε ^ 2 ≤ weightedHammingSq w a b) : (∑ j ∈ Finset.univ.filter (fun j : Fin n => a j = b j), w j / W) ^ m ≤ exp (-(m : ℝ) * ε ^ 2 / r ^ 2) := by classical -- The agreeing-coordinate weight is the total minus the weighted Hamming gap. have hagree : (∑ j ∈ Finset.univ.filter (fun j : Fin n => a j = b j), w j) = W - weightedHammingSq w a b := by rw [hW] unfold weightedHammingSq rw [← Finset.sum_sub_distrib, Finset.sum_filter] apply Finset.sum_congr rfl intro j _ by_cases h : a j = b j <;> simp [h] have hr2pos : 0 < r ^ 2 := by positivity have hWH_nonneg : 0 ≤ weightedHammingSq w a b := weightedHammingSq_nonneg w hw a b -- Normalize: the collision factor `s = (W - WH)/W` lies in `[0, 1 - ε²/r²]`. rw [← Finset.sum_div, hagree] set s : ℝ := (W - weightedHammingSq w a b) / W with hs_def have hs_nonneg : 0 ≤ s := by rw [hs_def] refine div_nonneg ?_ (le_of_lt hWpos) rw [← hagree] exact sum_nonneg (fun j _ => hw j) have hs_le1 : s ≤ 1 - ε ^ 2 / r ^ 2 := by rw [hs_def, sub_div, div_self (ne_of_gt hWpos)] have hratio : ε ^ 2 / r ^ 2 ≤ weightedHammingSq w a b / W := by rw [div_le_div_iff₀ hr2pos hWpos] nlinarith [hsep, hwsum, hWH_nonneg, sq_nonneg ε] linarith have hexp : 1 - ε ^ 2 / r ^ 2 ≤ exp (-(ε ^ 2 / r ^ 2)) := by have h := Real.add_one_le_exp (-(ε ^ 2 / r ^ 2)) linarith have hs_le_exp : s ≤ exp (-(ε ^ 2 / r ^ 2)) := le_trans hs_le1 hexp calc s ^ m ≤ (exp (-(ε ^ 2 / r ^ 2))) ^ m := pow_le_pow_left₀ hs_nonneg hs_le_exp m _ = exp (-(m : ℝ) * ε ^ 2 / r ^ 2) := by rw [← Real.exp_nat_mul] congr 1 ring

lemma card_subsample_family_le_succ_pow {n m d : ℕ} (J : Fin m → Fin n) (P : Finset (Fin n → Bool)) (hvcJ : (P.image (subsamplePattern J)).vcDim ≤ d) : (P.image (subsamplePattern J)).card ≤ (m + 1) ^ d := by exact le_trans (card_growthFamily_le_sum_choose (P.image (subsamplePattern J)) hvcJ) (sum_choose_le_succ_pow m d)

lemma subsample_image_vcDim_le {n m : ℕ} (d : ℕ) (J : Fin m → Fin n) (P : Finset (Fin n → Bool)) (hvc : (P.image (fun a => Finset.univ.filter (fun j => a j = true))).vcDim ≤ d) : (P.image (subsamplePattern J)).vcDim ≤ d := by classical let A : Finset (Finset (Fin n)) := P.image (fun a => Finset.univ.filter (fun j => a j = true)) let B : Finset (Finset (Fin m)) := P.image (subsamplePattern J) have hB_le_A : B.vcDim ≤ A.vcDim := by unfold vcDim refine Finset.sup_le ?_ intro T hTmem have hT : B.Shatters T := Finset.mem_shatterer.mp hTmem let U : Finset (Fin n) := T.image J have hinj : InjOn J (↑T) := by intro i hi k hk hJ by_contra hik have hsingle : ({i} : Finset (Fin m)) ⊆ T := Finset.singleton_subset_iff.mpr hi obtain ⟨u, huB, hTu⟩ := hT hsingle rcases Finset.mem_image.mp huB with ⟨a, _haP, rfl⟩ have hi_inter : i ∈ T ∩ subsamplePattern J a := by rw [hTu] simp have hi_pat : i ∈ subsamplePattern J a := (Finset.mem_inter.mp hi_inter).2 have hk_pat : k ∈ subsamplePattern J a := by rw [subsamplePattern_mem_iff] at hi_pat ⊢ simpa [hJ] using hi_pat have hk_inter : k ∈ T ∩ subsamplePattern J a := Finset.mem_inter.mpr ⟨hk, hk_pat⟩ have hk_single : k ∈ ({i} : Finset (Fin m)) := by rw [← hTu] exact hk_inter have hki : k = i := by simpa using hk_single exact hik hki.symm have hAshat : A.Shatters U := by intro S hS let S' : Finset (Fin m) := T.filter fun i => J i ∈ S have hS'T : S' ⊆ T := by intro i hi exact (Finset.mem_filter.mp hi).1 obtain ⟨u, huB, hTu⟩ := hT hS'T rcases Finset.mem_image.mp huB with ⟨a, haP, rfl⟩ refine ⟨Finset.univ.filter (fun j => a j = true), ?_, ?_⟩ · exact Finset.mem_image.mpr ⟨a, haP, rfl⟩ · ext x constructor · intro hx rcases Finset.mem_inter.mp hx with ⟨hxU, hxtrue⟩ rcases Finset.mem_image.mp hxU with ⟨i, hiT, rfl⟩ have hi_pat : i ∈ subsamplePattern J a := by rw [subsamplePattern_mem_iff] simpa using (Finset.mem_filter.mp hxtrue).2 have hiS' : i ∈ S' := by rw [← hTu] exact Finset.mem_inter.mpr ⟨hiT, hi_pat⟩ exact (Finset.mem_filter.mp hiS').2 · intro hxS have hxU : x ∈ U := hS hxS rcases Finset.mem_image.mp hxU with ⟨i, hiT, hJi⟩ have hiS' : i ∈ S' := Finset.mem_filter.mpr ⟨hiT, by simpa [hJi] using hxS⟩ have hi_inter : i ∈ T ∩ subsamplePattern J a := by rw [hTu] exact hiS' have hi_pat : i ∈ subsamplePattern J a := (Finset.mem_inter.mp hi_inter).2 refine Finset.mem_inter.mpr ⟨hxU, ?_⟩ rw [mem_filter] constructor · simp · rw [subsamplePattern_mem_iff] at hi_pat simpa [hJi] using hi_pat have hU_le : U.card ≤ A.vcDim := Finset.Shatters.card_le_vcDim hAshat have hcard : U.card = T.card := Finset.card_image_of_injOn hinj exact hcard.ge.trans hU_le exact hB_le_A.trans hvc

lemma finite_averaging_exists_separating_subsample {n : ℕ} (w : Fin n → ℝ) (hw : ∀ j, 0 ≤ w j) (r ε : ℝ) (hr : 0 < r) (hε : 0 < ε) (hwsum : ∑ j, w j ≤ r ^ 2) (P : Finset (Fin n → Bool)) (hPcard : 2 ≤ P.card) (hsep : ∀ a ∈ P, ∀ b ∈ P, a ≠ b → ε ^ 2 ≤ weightedHammingSq w a b) : ∃ (m : ℕ) (J : Fin m → Fin n), (m : ℝ) ≤ 1 + (2 * r ^ 2 / ε ^ 2) * log (P.card) ∧ InjOn (subsamplePattern J) ↑P := by classical let W : ℝ := ∑ j : Fin n, w j have hWdef : W = ∑ j : Fin n, w j := rfl have hWpos : 0 < W := by have htwo : 1 < P.card := by omega rcases Finset.one_lt_card.mp htwo with ⟨a, haP, b, hbP, hab⟩ have hdist_le_W : weightedHammingSq w a b ≤ W := by dsimp [W] unfold weightedHammingSq refine Finset.sum_le_sum ?_ intro j _hj by_cases h : a j = b j · simp [h, hw j] · simp [h] have hdist_pos : 0 < weightedHammingSq w a b := by have hεsq : 0 < ε ^ 2 := sq_pos_of_ne_zero (ne_of_gt hε) exact lt_of_lt_of_le hεsq (hsep a haP b hbP hab) exact lt_of_lt_of_le hdist_pos hdist_le_W have hwsumW : W ≤ r ^ 2 := by simpa [W] using hwsum let L : ℝ := (2 * r ^ 2 / ε ^ 2) * log (P.card) let m : ℕ := ⌊L⌋₊ + 1 have hPpos_nat : 0 < P.card := by omega have hPone_nat : 1 ≤ P.card := by omega have hPpos_real : 0 < (P.card : ℝ) := by exact_mod_cast hPpos_nat have hLnonneg : 0 ≤ L := by have hcoef_nonneg : 0 ≤ 2 * r ^ 2 / ε ^ 2 := by positivity have hlog_nonneg : 0 ≤ log (P.card) := Real.log_nonneg (by exact_mod_cast hPone_nat) exact mul_nonneg hcoef_nonneg hlog_nonneg have hm_bound : (m : ℝ) ≤ 1 + (2 * r ^ 2 / ε ^ 2) * log (P.card) := by have hfloor : ((⌊L⌋₊ : ℕ) : ℝ) ≤ L := Nat.floor_le hLnonneg dsimp [m, L] norm_num [Nat.cast_add, cast_one] linarith let μ : (Fin m → Fin n) → ℝ := fun J => ∏ t : Fin m, (w (J t) / W) let cnt : (Fin m → Fin n) → ℕ := fun J => (P.offDiag.filter fun ab => subsamplePattern J ab.1 = subsamplePattern J ab.2).card have hμsum : ∑ J : Fin m → Fin n, μ J = 1 := by dsimp [μ] rw [product_sum_normalization (n := n) (m := m) (fun j : Fin n => w j / W)] have hsum : (∑ j : Fin n, w j / W) = 1 := by rw [← Finset.sum_div] rw [← hWdef] exact div_self (ne_of_gt hWpos) rw [hsum, one_pow] have hμnonneg : ∀ J : Fin m → Fin n, 0 ≤ μ J := by intro J dsimp [μ] exact Finset.prod_nonneg fun t _ht => div_nonneg (hw (J t)) (le_of_lt hWpos) have hcnt_cast : ∀ J : Fin m → Fin n, (cnt J : ℝ) = ∑ ab ∈ P.offDiag, if subsamplePattern J ab.1 = subsamplePattern J ab.2 then (1 : ℝ) else 0 := by intro J dsimp [cnt] simp have hinner : ∀ ab ∈ P.offDiag, (∑ J : Fin m → Fin n, μ J * (if subsamplePattern J ab.1 = subsamplePattern J ab.2 then (1 : ℝ) else 0)) = (∑ j ∈ Finset.univ.filter (fun j : Fin n => ab.1 j = ab.2 j), w j / W) ^ m := by intro ab _hab calc (∑ J : Fin m → Fin n, μ J * (if subsamplePattern J ab.1 = subsamplePattern J ab.2 then (1 : ℝ) else 0)) = ∑ J : Fin m → Fin n, (∏ t : Fin m, (w (J t) / W)) * (if (∀ t : Fin m, ab.1 (J t) = ab.2 (J t)) then (1 : ℝ) else 0) := by refine Finset.sum_congr rfl ?_ intro J _hJ dsimp [μ] by_cases h : subsamplePattern J ab.1 = subsamplePattern J ab.2 · have hforall : ∀ t : Fin m, ab.1 (J t) = ab.2 (J t) := subsamplePattern_eq_iff.mp h simp [h, hforall] · have hforall : ¬ ∀ t : Fin m, ab.1 (J t) = ab.2 (J t) := by intro hall exact h (subsamplePattern_eq_iff.mpr hall) simp [h, hforall] _ = (∑ j ∈ Finset.univ.filter (fun j : Fin n => ab.1 j = ab.2 j), w j / W) ^ m := by exact per_pair_collision_sum (fun j : Fin n => w j / W) ab.1 ab.2 have hmean_le : (∑ J : Fin m → Fin n, μ J * (cnt J : ℝ)) ≤ (P.offDiag.card : ℝ) * exp (-(m : ℝ) * ε ^ 2 / r ^ 2) := by calc (∑ J : Fin m → Fin n, μ J * (cnt J : ℝ)) = ∑ J : Fin m → Fin n, μ J * (∑ ab ∈ P.offDiag, if subsamplePattern J ab.1 = subsamplePattern J ab.2 then (1 : ℝ) else 0) := by refine Finset.sum_congr rfl ?_ intro J _hJ rw [hcnt_cast J] _ = ∑ J : Fin m → Fin n, ∑ ab ∈ P.offDiag, μ J * (if subsamplePattern J ab.1 = subsamplePattern J ab.2 then (1 : ℝ) else 0) := by refine Finset.sum_congr rfl ?_ intro J _hJ rw [Finset.mul_sum] _ = ∑ ab ∈ P.offDiag, ∑ J : Fin m → Fin n, μ J * (if subsamplePattern J ab.1 = subsamplePattern J ab.2 then (1 : ℝ) else 0) := by rw [Finset.sum_comm] _ ≤ ∑ ab ∈ P.offDiag, exp (-(m : ℝ) * ε ^ 2 / r ^ 2) := by refine Finset.sum_le_sum ?_ intro ab hab rw [hinner ab hab] rcases Finset.mem_offDiag.mp hab with ⟨haP, hbP, habne⟩ exact collision_bound w hw r ε W hr hWdef hWpos hwsumW ab.1 ab.2 (hsep ab.1 haP ab.2 hbP habne) _ = (P.offDiag.card : ℝ) * exp (-(m : ℝ) * ε ^ 2 / r ^ 2) := by simp have hmean_lt_one : (∑ J : Fin m → Fin n, μ J * (cnt J : ℝ)) < 1 := by have hm_gt_L : L < (m : ℝ) := by dsimp [m] simpa [Nat.cast_add, cast_one] using (Nat.lt_floor_add_one L) have hscale_pos : 0 < ε ^ 2 / r ^ 2 := by positivity have hscaled : L * (ε ^ 2 / r ^ 2) < (m : ℝ) * (ε ^ 2 / r ^ 2) := mul_lt_mul_of_pos_right hm_gt_L hscale_pos have hLscale : L * (ε ^ 2 / r ^ 2) = 2 * log (P.card) := by dsimp [L] field_simp [ne_of_gt hε, ne_of_gt hr] have hmexp : 2 * log (P.card) < (m : ℝ) * ε ^ 2 / r ^ 2 := by rw [hLscale] at hscaled convert hscaled using 1 ring have hneg : -((m : ℝ) * ε ^ 2 / r ^ 2) < -(2 * log (P.card)) := by linarith have hexp_lt : exp (-((m : ℝ) * ε ^ 2 / r ^ 2)) < exp (-(2 * log (P.card))) := Real.exp_lt_exp.mpr hneg have hoff_card : (P.offDiag.card : ℝ) ≤ (P.card : ℝ) ^ 2 := by have hn : P.offDiag.card ≤ P.card * P.card := by rw [Finset.offDiag_card] omega have hnreal : (P.offDiag.card : ℝ) ≤ (P.card * P.card : ℕ) := by exact_mod_cast hn simpa [sq] using hnreal have hN2pos : 0 < (P.card : ℝ) ^ 2 := sq_pos_of_ne_zero (ne_of_gt hPpos_real) have hprod_lt : (P.card : ℝ) ^ 2 * exp (-((m : ℝ) * ε ^ 2 / r ^ 2)) < (P.card : ℝ) ^ 2 * exp (-(2 * log (P.card))) := mul_lt_mul_of_pos_left hexp_lt hN2pos have hexp_neg_eq : exp (-(2 * log (P.card))) = ((P.card : ℝ) ^ 2)⁻¹ := by rw [Real.exp_neg] have htwice : exp (2 * log (P.card)) = (P.card : ℝ) ^ 2 := by have hrewrite : 2 * log (P.card) = log (P.card) + log (P.card) := by ring rw [hrewrite, Real.exp_add, Real.exp_log hPpos_real] ring rw [htwice] have hprod_eq : (P.card : ℝ) ^ 2 * exp (-(2 * log (P.card))) = 1 := by rw [hexp_neg_eq] exact mul_inv_cancel₀ (ne_of_gt hN2pos) have hcardexp_le : (P.offDiag.card : ℝ) * exp (-(m : ℝ) * ε ^ 2 / r ^ 2) ≤ (P.card : ℝ) ^ 2 * exp (-(m : ℝ) * ε ^ 2 / r ^ 2) := by exact mul_le_mul_of_nonneg_right hoff_card (le_of_lt (Real.exp_pos _)) have hprod_lt_one : (P.card : ℝ) ^ 2 * exp (-(m : ℝ) * ε ^ 2 / r ^ 2) < 1 := by convert (by simpa [hprod_eq] using hprod_lt) using 2 ring_nf exact lt_of_le_of_lt (hmean_le.trans hcardexp_le) hprod_lt_one obtain ⟨J, hcnt_zero⟩ := averaging_exists_zero_count μ cnt hμsum hμnonneg hmean_lt_one refine ⟨m, J, hm_bound, ?_⟩ intro a haP b hbP hpat by_contra hab have hbad_mem : (a, b) ∈ P.offDiag.filter (fun ab => subsamplePattern J ab.1 = subsamplePattern J ab.2) := by rw [mem_filter] exact ⟨Finset.mem_offDiag.mpr ⟨haP, hbP, hab⟩, hpat⟩ have hcnt_pos : 0 < cnt J := by dsimp [cnt] exact Finset.card_pos.mpr ⟨(a, b), hbad_mem⟩ exact (Nat.ne_of_gt hcnt_pos) hcnt_zero

lemma exists_separating_subsample {n : ℕ} (d : ℕ) (w : Fin n → ℝ) (hw : ∀ j, 0 ≤ w j) (r ε : ℝ) (hr : 0 < r) (hε : 0 < ε) (hwsum : ∑ j, w j ≤ r ^ 2) (P : Finset (Fin n → Bool)) (hPcard : 2 ≤ P.card) (hvc : (P.image (fun a => (Finset.univ.filter (fun j => a j = true)))).vcDim ≤ d) (hsep : ∀ a ∈ P, ∀ b ∈ P, a ≠ b → ε ^ 2 ≤ weightedHammingSq w a b) : ∃ (m : ℕ) (J : Fin m → Fin n), (m : ℝ) ≤ 1 + (2 * r ^ 2 / ε ^ 2) * log (P.card) ∧ (P.image (subsamplePattern J)).vcDim ≤ d ∧ InjOn (subsamplePattern J) ↑P := by obtain ⟨m, J, hm, hinj⟩ := finite_averaging_exists_separating_subsample w hw r ε hr hε hwsum P hPcard hsep exact ⟨m, J, hm, subsample_image_vcDim_le d J P hvc, hinj⟩

lemma self_log_solve {a L : ℝ} {d : ℕ} (hd : 1 ≤ d) (ha : 2 ≤ a) (hL : 0 ≤ L) (hbound : L ≤ (d : ℝ) * log (2 + a * L)) : L ≤ 1 + 2 * (d : ℝ) * log (2 * a * (d : ℝ)) := by have hd_pos_nat : 0 < d := lt_of_lt_of_le Nat.zero_lt_one hd have hd_pos : 0 < (d : ℝ) := by exact_mod_cast hd_pos_nat have hd_nonneg : 0 ≤ (d : ℝ) := le_of_lt hd_pos have ha_pos : 0 < a := by linarith have ha_nonneg : 0 ≤ a := le_of_lt ha_pos have hy_pos : 0 < 2 + a * L := by have hmul_nonneg : 0 ≤ a * L := mul_nonneg ha_nonneg hL linarith have ht_pos : 0 < 2 * a * (d : ℝ) := by positivity have hlog_tangent : log (2 + a * L) ≤ (2 + a * L) / (2 * a * (d : ℝ)) + log (2 * a * (d : ℝ)) - 1 := by have hratio_pos : 0 < (2 + a * L) / (2 * a * (d : ℝ)) := div_pos hy_pos ht_pos have h0 := Real.log_le_sub_one_of_pos hratio_pos have hlog_div : log ((2 + a * L) / (2 * a * (d : ℝ))) = log (2 + a * L) - log (2 * a * (d : ℝ)) := by exact Real.log_div (ne_of_gt hy_pos) (ne_of_gt ht_pos) rw [hlog_div] at h0 linarith have hstep : L ≤ (d : ℝ) * ((2 + a * L) / (2 * a * (d : ℝ)) + log (2 * a * (d : ℝ)) - 1) := by exact le_trans hbound (mul_le_mul_of_nonneg_left hlog_tangent hd_nonneg) have hrewrite : (d : ℝ) * ((2 + a * L) / (2 * a * (d : ℝ)) + log (2 * a * (d : ℝ)) - 1) = 1 / a + L / 2 + (d : ℝ) * log (2 * a * (d : ℝ)) - (d : ℝ) := by field_simp [ne_of_gt ha_pos, ne_of_gt hd_pos] have hstep' : L ≤ 1 / a + L / 2 + (d : ℝ) * log (2 * a * (d : ℝ)) - (d : ℝ) := by rwa [hrewrite] at hstep have hdrop : L ≤ 1 / a + L / 2 + (d : ℝ) * log (2 * a * (d : ℝ)) := by linarith have hhalf' : L ≤ 2 * (1 / a + (d : ℝ) * log (2 * a * (d : ℝ))) := by linarith have hhalf : L ≤ 2 / a + 2 * (d : ℝ) * log (2 * a * (d : ℝ)) := by convert hhalf' using 1 ring have htwo_div_le_one : 2 / a ≤ 1 := (div_le_one ha_pos).2 ha linarith

lemma abs_starHullZeroOut_le_of_bound {F : ι → 𝒳 → ℝ} {norm : (𝒳 → ℝ) → ℝ} {B r : ℝ} (hbound : ∀ i x, |F i x| ≤ B) (p : starHullParam ι) (x : 𝒳) : |starHullZeroOut F norm r p x| ≤ B := by rcases p with ⟨a, i⟩ by_cases hactive : norm (starHullEval F (a, i)) ≤ r · calc |starHullZeroOut F norm r (a, i) x| = |(a : ℝ) * F i x| := by simp [starHullZeroOut, hactive, starHullEval] _ = (a : ℝ) * |F i x| := by rw [abs_mul, abs_of_nonneg a.property.1] _ ≤ 1 * |F i x| := mul_le_mul_of_nonneg_right a.property.2 (abs_nonneg _) _ ≤ B := by simpa using hbound i x · have hB : 0 ≤ B := (abs_nonneg (F i x)).trans (hbound i x) simpa [starHullZeroOut, hactive] using hB

lemma empiricalNorm_le_of_forall_abs_le {n : ℕ} (S : Fin n → 𝒳) {f : 𝒳 → ℝ} {η : ℝ} (hη : 0 ≤ η) (hf : ∀ j : Fin n, |f (S j)| ≤ η) : empiricalNorm S f ≤ η := by classical by_cases hn : n = 0 · simp [empiricalNorm, hn, hη] · have hnpos : 0 < n := Nat.pos_of_ne_zero hn have hnR : 0 < (n : ℝ) := by exact_mod_cast hnpos have hsum : (∑ j : Fin n, (f (S j)) ^ 2) ≤ ∑ _j : Fin n, η ^ 2 := by refine Finset.sum_le_sum ?_ intro j _ calc (f (S j)) ^ 2 = |f (S j)| ^ 2 := by rw [sq_abs] _ ≤ η ^ 2 := sq_le_sq.mpr (by simpa [abs_of_nonneg hη] using hf j) have harg : (1 / (n : ℝ)) * ∑ j : Fin n, (f (S j)) ^ 2 ≤ η ^ 2 := by calc (1 / (n : ℝ)) * ∑ j : Fin n, (f (S j)) ^ 2 ≤ (1 / (n : ℝ)) * ∑ _j : Fin n, η ^ 2 := mul_le_mul_of_nonneg_left hsum (by positivity) _ = (1 / (n : ℝ)) * ((n : ℝ) * η ^ 2) := by simp _ = η ^ 2 := by field_simp [Finset.card_fin, hnR.ne'] calc empiricalNorm S f = sqrt ((1 / (n : ℝ)) * ∑ j : Fin n, (f (S j)) ^ 2) := rfl _ ≤ sqrt (η ^ 2) := Real.sqrt_le_sqrt harg _ = η := by rw [Real.sqrt_sq_eq_abs, abs_of_nonneg hη]

lemma empiricalFunctionSpace_dist_le_of_forall_abs_sub_le {G : starHullParam ι → 𝒳 → ℝ} {n : ℕ} {S : Fin n → 𝒳} (q q' : EmpiricalFunctionSpace G S) {η : ℝ} (hη : 0 ≤ η) (hcoord : ∀ j : Fin n, |G q.index (S j) - G q'.index (S j)| ≤ η) : dist q q' ≤ η := by have hnorm : empiricalNorm S ((q : 𝒳 → ℝ) - (q' : 𝒳 → ℝ)) ≤ η := empiricalNorm_le_of_forall_abs_le S hη (by intro j simpa [Pi.sub_apply] using hcoord j) simpa [instDistEmpiricalFunctionSpace, empiricalDist] using hnorm

lemma starHullZeroOut_totallyBounded_of_bounded {F : ι → 𝒳 → ℝ} {norm : (𝒳 → ℝ) → ℝ} {B : ℝ} (hbound : ∀ i x, |F i x| ≤ B) {n : ℕ} (S : Fin n → 𝒳) {r : ℝ} : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace (starHullZeroOut F norm r) S)) := by classical let sampleVector : EmpiricalFunctionSpace (starHullZeroOut F norm r) S → Fin n → ℝ := fun q j => starHullZeroOut F norm r q.index (S j) have hcube : TotallyBounded (Icc (fun _ : Fin n => -B) (fun _ : Fin n => B) : Set (Fin n → ℝ)) := isCompact_Icc.totallyBounded refine Metric.totallyBounded_of_finite_discretization (s := (Set.univ : Set (EmpiricalFunctionSpace (starHullZeroOut F norm r) S))) ?_ intro ε hε let δ : ℝ := ε / 4 have hδ : 0 < δ := by positivity rcases Metric.finite_approx_of_totallyBounded hcube δ hδ with ⟨t, ht_subset, ht_finite, ht_cover⟩ have hmem_cube : ∀ q : (Set.univ : Set (EmpiricalFunctionSpace (starHullZeroOut F norm r) S)), sampleVector q.1 ∈ (Icc (fun _ : Fin n => -B) (fun _ : Fin n => B) : Set (Fin n → ℝ)) := by intro q constructor · intro j exact neg_le_of_abs_le (abs_starHullZeroOut_le_of_bound hbound q.1.index (S j)) · intro j exact le_of_abs_le (abs_starHullZeroOut_le_of_bound hbound q.1.index (S j)) have hnear : ∀ q : (Set.univ : Set (EmpiricalFunctionSpace (starHullZeroOut F norm r) S)), ∃ y : (t : Set (Fin n → ℝ)), dist (sampleVector q.1) y.1 < δ := by intro q have hq := ht_cover (hmem_cube q) simp only [Set.mem_iUnion, Metric.mem_ball] at hq rcases hq with ⟨y, hy_t, hy_dist⟩ exact ⟨⟨y, hy_t⟩, hy_dist⟩ let domain : Set (EmpiricalFunctionSpace (starHullZeroOut F norm r) S) := Set.univ let center0 : domain → (t : Set (Fin n → ℝ)) := fun q => choose (hnear q) let center : domain → ULift.{u} (t : Set (Fin n → ℝ)) := fun q => ULift.up (center0 q) haveI : Fintype (t : Set (Fin n → ℝ)) := ht_finite.fintype refine ⟨ULift.{u} (t : Set (Fin n → ℝ)), inferInstance, center, ?_⟩ intro q q' hcenter have hcenter0 : center0 q = center0 q' := by simpa [center] using congrArg ULift.down hcenter have hq_near : dist (sampleVector q.1) (center0 q).1 < δ := Classical.choose_spec (hnear q) have hq'_near : dist (sampleVector q'.1) (center0 q').1 < δ := Classical.choose_spec (hnear q') have hcoord : ∀ j : Fin n, |starHullZeroOut F norm r q.1.index (S j) - starHullZeroOut F norm r q'.1.index (S j)| ≤ ε / 2 := by intro j have hjq : dist (sampleVector q.1 j) ((center0 q).1 j) < δ := (dist_le_pi_dist (sampleVector q.1) (center0 q).1 j).trans_lt hq_near have hjq' : dist ((center0 q).1 j) (sampleVector q'.1 j) < δ := by rw [← hcenter0] at hq'_near simpa [dist_comm] using (dist_le_pi_dist (sampleVector q'.1) (center0 q).1 j).trans_lt hq'_near have hsum : dist (sampleVector q.1 j) (sampleVector q'.1 j) < ε / 2 := by calc dist (sampleVector q.1 j) (sampleVector q'.1 j) ≤ dist (sampleVector q.1 j) ((center0 q).1 j) + dist ((center0 q).1 j) (sampleVector q'.1 j) := dist_triangle _ _ _ _ < δ + δ := add_lt_add hjq hjq' _ = ε / 2 := by ring simpa [Real.dist_eq] using le_of_lt hsum have hdist_le : dist q.1 q'.1 ≤ ε / 2 := empiricalFunctionSpace_dist_le_of_forall_abs_sub_le q.1 q'.1 (by positivity) hcoord exact lt_of_le_of_lt hdist_le (by linarith)

theorem localizedVCDudleyHypotheses_of_empiricalRadius {F : ι → 𝒳 → ℝ} {norm : (𝒳 → ℝ) → ℝ} {B : ℝ} (hbound : ∀ i x, |F i x| ≤ B) (empirical_radius : ∀ {n : ℕ} (S : Fin n → 𝒳) {r : ℝ}, 0 ≤ r → ∀ p : starHullParam ι, empiricalNorm S (starHullZeroOut F norm r p) ≤ r) : LocalizedVCDudleyHypotheses F norm where empirical_radius := empirical_radius totallyBounded := fun {_} S {_} _ => starHullZeroOut_totallyBounded_of_bounded hbound S

lemma vcLocalizedRate_nonneg {K : ℝ} {d n : ℕ} (hK : 0 ≤ K) : 0 ≤ (K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ) := by by_cases hn : n = 0 · simp [hn] · have hn_pos : 0 < n := Nat.pos_of_ne_zero hn have hnR : 0 < (n : ℝ) := by exact_mod_cast hn_pos have hone_le : (1 : ℝ) ≤ (n : ℝ) + 1 := by linarith [le_of_lt hnR] have hlog : 0 ≤ log ((n : ℝ) + 1) := Real.log_nonneg hone_le have hterm : 0 ≤ K * (d : ℝ) * log ((n : ℝ) + 1) := by exact mul_nonneg (mul_nonneg hK (Nat.cast_nonneg d)) hlog have hnum : 0 ≤ K * (d : ℝ) * log ((n : ℝ) + 1) + 1 := by linarith exact div_nonneg hnum (le_of_lt hnR)

lemma vcLocalizedSlope_pos {K : ℝ} {d n : ℕ} (hK : 0 ≤ K) (hn : 0 < n) : 0 < vcLocalizedSlope K d n := by unfold vcLocalizedSlope have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hone_le : (1 : ℝ) ≤ (n : ℝ) + 1 := by linarith [le_of_lt hnR] have hlog : 0 ≤ log ((n : ℝ) + 1) := Real.log_nonneg hone_le have hterm : 0 ≤ K * (d : ℝ) * log ((n : ℝ) + 1) := by exact mul_nonneg (mul_nonneg hK (Nat.cast_nonneg d)) hlog have hnum : 0 < K * (d : ℝ) * log ((n : ℝ) + 1) + 1 := by linarith have hfrac : 0 < (K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ) := div_pos hnum hnR have hsqrt : 0 < sqrt ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ)) := Real.sqrt_pos.mpr hfrac nlinarith

lemma vcLocalizedSlope_sq {K : ℝ} {d n : ℕ} (hK : 0 ≤ K) : vcLocalizedSlope K d n ^ 2 = 36 * ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ)) := by unfold vcLocalizedSlope rw [mul_pow, Real.sq_sqrt (vcLocalizedRate_nonneg (K := K) (d := d) (n := n) hK)] ring

lemma linear_subRoot {C : ℝ} (hC : 0 ≤ C) : SubRoot (fun r : ℝ => C * r) := by refine ⟨?_, ?_, ?_⟩ · intro r hr exact mul_nonneg hC hr · intro r₁ r₂ _ hr₁₂ exact mul_le_mul_of_nonneg_left hr₁₂ hC · intro r₁ r₂ hr₁ hr₁₂ have hr₂ : 0 < r₂ := lt_of_lt_of_le hr₁ hr₁₂ have h₁ : C * r₁ / r₁ = C := by field_simp [ne_of_gt hr₁] have h₂ : C * r₂ / r₂ = C := by field_simp [ne_of_gt hr₂] rw [h₁, h₂]

lemma criticalRadius_linear_sq_le {C : ℝ} (hC : 0 < C) : (criticalRadius (fun r : ℝ => C * r)) ^ 2 ≤ C ^ 2 := by have hle : criticalRadius (fun r : ℝ => C * r) ≤ C := criticalRadius_linear_le hC have hnonneg : 0 ≤ criticalRadius (fun r : ℝ => C * r) := criticalRadius_nonneg _ nlinarith

lemma criticalRadius_vcLocalizedPsi_le {K : ℝ} {d n : ℕ} (hK : 0 ≤ K) (hn : 0 < n) : criticalRadius (vcLocalizedPsi K d n) ≤ vcLocalizedSlope K d n := by unfold vcLocalizedPsi exact criticalRadius_linear_le (vcLocalizedSlope_pos hK hn)

lemma criticalRadius_vcLocalizedPsi_sq_le {K : ℝ} {d n : ℕ} (hK : 0 ≤ K) (hn : 0 < n) : (criticalRadius (vcLocalizedPsi K d n)) ^ 2 ≤ (vcLocalizedSlope K d n) ^ 2 := by unfold vcLocalizedPsi exact criticalRadius_linear_sq_le (vcLocalizedSlope_pos hK hn)

lemma growthFamily_card_le_succ_pow_of_trace (π : ι → 𝒳 → Bool) (d n : ℕ) (Htrace : BinaryTraceEntropyControl π d) (S : Fin n → 𝒳) : (growthFamily π S).card ≤ (n + 1) ^ d := by rcases Htrace with hvc | hcard · exact le_trans (card_growthFamily_le_sum_choose (growthFamily π S) (hvc S)) (sum_choose_le_succ_pow n d) · exact hcard n S

lemma log_two_growth_card_le (π : ι → 𝒳 → Bool) (d n : ℕ) (S : Fin n → 𝒳) (hcard_pos : 0 < (growthFamily π S).card) (hcard : (growthFamily π S).card ≤ (n + 1) ^ d) : 2 * log (2 * ((growthFamily π S).card : ℝ)) ≤ 2 * (d : ℝ) * log ((n : ℝ) + 1) + 2 := by let N : ℕ := (growthFamily π S).card let M : ℕ := (n + 1) ^ d have hleR : (2 : ℝ) * N ≤ 2 * M := by exact_mod_cast (Nat.mul_le_mul_left 2 hcard) have hlog_le : log (2 * (N : ℝ)) ≤ log (2 * (M : ℝ)) := by exact Real.log_le_log (by positivity) hleR have hlogM : log (2 * (M : ℝ)) = log 2 + (d : ℝ) * log ((n : ℝ) + 1) := by dsimp [M] norm_num only [Nat.cast_pow, Nat.cast_add, cast_one] rw [Real.log_mul] · rw [Real.log_pow] · norm_num · positivity have hlog2 : log 2 ≤ (1 : ℝ) := by have h := Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 2) linarith dsimp [N] at hlog_le nlinarith

lemma empiricalRademacher_withAbs_finiteClass_le {ι' Z : Type*} {m : ℕ} (hm : 0 < m) (H : ι' → Z → ℝ) (S' : Fin m → Z) (f : Finset ι') (hf : f.Nonempty) (ρ : ℝ) (hradius : ∀ i ∈ f, sqrt (∑ k : Fin m, ((m : ℝ)⁻¹ * |H i (S' k)|) ^ 2) ≤ ρ) : empiricalRademacherComplexity m (F_on H f) S' ≤ ρ * sqrt (2 * log (2 * (f.card : ℝ))) := by classical let Hd : ι' × Bool → Z → ℝ := fun jb z => if jb.2 then H jb.1 z else -H jb.1 z let fd : Finset (ι' × Bool) := f.product (Finset.univ : Finset Bool) have hfd_nonempty : fd.Nonempty := by rcases hf with ⟨i, hi⟩ refine ⟨(i, true), ?_⟩ simp [fd, hi] have hpoint : empiricalRademacherComplexity m (F_on H f) S' ≤ empiricalRademacherComplexity_without_abs m (F_on Hd fd) S' := by haveI : Nonempty {j // j ∈ f} := by rcases hf with ⟨i, hi⟩ exact ⟨⟨i, hi⟩⟩ unfold empiricalRademacherComplexity empiricalRademacherComplexity_without_abs refine mul_le_mul_of_nonneg_left ?_ (by positivity) refine Finset.sum_le_sum ?_ intro σ _ refine ciSup_le ?_ intro j let x : ℝ := (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on H f j (S' k) have htrue : x = (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd ⟨(j.1, true), by simp [fd, j.2]⟩ (S' k) := by simp [x, Hd, F_on] have hfalse : -x = (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd ⟨(j.1, false), by simp [fd, j.2]⟩ (S' k) := by simp [x, Hd, F_on, Finset.mul_sum] have hle_true : x ≤ ⨆ jb : {jb // jb ∈ fd}, (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd jb (S' k) := by rw [htrue] exact le_ciSup (Finite.bddAbove_range fun jb : {jb // jb ∈ fd} => (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd jb (S' k)) ⟨(j.1, true), by simp [fd, j.2]⟩ have hle_false : -x ≤ ⨆ jb : {jb // jb ∈ fd}, (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd jb (S' k) := by rw [hfalse] exact le_ciSup (Finite.bddAbove_range fun jb : {jb // jb ∈ fd} => (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd jb (S' k)) ⟨(j.1, false), by simp [fd, j.2]⟩ have hlower : -(⨆ jb : {jb // jb ∈ fd}, (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd jb (S' k)) ≤ x := by linarith simpa [x] using abs_le.mpr ⟨hlower, hle_true⟩ have hpointwise : ∀ i ∈ fd, ∀ j : Fin m, |Hd i (S' j)| ≤ (m : ℝ) * ρ := by intro i hi j rcases i with ⟨i, b⟩ have hi_f : i ∈ f := by simpa [fd] using (Finset.mem_product.mp hi).1 have hterm : ((m : ℝ)⁻¹ * |H i (S' j)|) ^ 2 ≤ ∑ k : Fin m, ((m : ℝ)⁻¹ * |H i (S' k)|) ^ 2 := by exact Finset.single_le_sum (s := (Finset.univ : Finset (Fin m))) (f := fun k : Fin m => ((m : ℝ)⁻¹ * |H i (S' k)|) ^ 2) (by intro k _; exact sq_nonneg _) (by simp) have hscaled : (m : ℝ)⁻¹ * |H i (S' j)| ≤ ρ := by have hsqrt := (Real.sqrt_le_sqrt hterm).trans (hradius i hi_f) have hnonneg : 0 ≤ (m : ℝ)⁻¹ * |H i (S' j)| := by exact mul_nonneg (inv_nonneg.mpr (Nat.cast_nonneg m)) (abs_nonneg _) simpa [Real.sqrt_sq_eq_abs, abs_of_nonneg hnonneg] using hsqrt have hmR : 0 < (m : ℝ) := by exact_mod_cast hm have hmul := mul_le_mul_of_nonneg_left hscaled (le_of_lt hmR) have hcancel : (m : ℝ) * ((m : ℝ)⁻¹ * |H i (S' j)|) = |H i (S' j)| := by field_simp [ne_of_gt hmR] have hH : |H i (S' j)| ≤ (m : ℝ) * ρ := by simpa [hcancel, mul_assoc] using hmul by_cases hb : b = true · simp [Hd, hb, hH] · have hbfalse : b = false := by cases b <;> simp at hb ⊢ simpa [Hd, hbfalse, abs_neg] using hH have hmass : empiricalRademacherComplexity_without_abs m (F_on Hd fd) S' ≤ (sup' fd hfd_nonempty fun j => sqrt (∑ i : Fin m, ((m : ℝ)⁻¹ * |Hd j (S' i)|) ^ 2)) * sqrt (2 * log fd.card) := by rw [empiricalRademacherComplexity_without_abs_eq_empiricalRademacherComplexity_pmf_without_abs] exact massart_lemma_pmf (F := Hd) (S := S') fd hfd_nonempty have hsup : (sup' fd hfd_nonempty fun j => sqrt (∑ i : Fin m, ((m : ℝ)⁻¹ * |Hd j (S' i)|) ^ 2)) ≤ ρ := by refine Finset.sup'_le _ _ ?_ intro jb hjb rcases jb with ⟨i, b⟩ have hi_f : i ∈ f := by simpa [fd] using (Finset.mem_product.mp hjb).1 by_cases hb : b = true · simpa [Hd, hb] using hradius i hi_f · have hbfalse : b = false := by cases b <;> simp at hb ⊢ simpa [Hd, hbfalse, abs_neg] using hradius i hi_f have hcard : (fd.card : ℝ) = 2 * (f.card : ℝ) := by simp [fd, Nat.cast_mul, mul_comm] calc empiricalRademacherComplexity m (F_on H f) S' ≤ empiricalRademacherComplexity_without_abs m (F_on Hd fd) S' := hpoint _ ≤ (sup' fd hfd_nonempty fun j => sqrt (∑ i : Fin m, ((m : ℝ)⁻¹ * |Hd j (S' i)|) ^ 2)) * sqrt (2 * log fd.card) := hmass _ ≤ ρ * sqrt (2 * log fd.card) := mul_le_mul_of_nonneg_right hsup (Real.sqrt_nonneg _) _ = ρ * sqrt (2 * log (2 * (f.card : ℝ))) := by rw [hcard]

lemma empiricalRademacherComplexity_F_on_univ_eq {ι' Z : Type*} [Fintype ι'] {m : ℕ} (H : ι' → Z → ℝ) (S' : Fin m → Z) : empiricalRademacherComplexity m (F_on H (Finset.univ : Finset ι')) S' = empiricalRademacherComplexity m H S' := by classical cases isEmpty_or_nonempty ι' with | inl _ => simp [empiricalRademacherComplexity] | inr _ => unfold empiricalRademacherComplexity apply congrArg refine Finset.sum_congr rfl ?_ intro σ _ haveI : Nonempty {j // j ∈ (Finset.univ : Finset ι')} := by rcases (inferInstance : Nonempty ι') with ⟨i⟩ exact ⟨⟨i, by simp⟩⟩ apply le_antisymm · refine ciSup_le ?_ intro i exact le_ciSup (Finite.bddAbove_range fun j : ι' => |(m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * H j (S' k)|) i.1 · refine ciSup_le ?_ intro i have hidx : i ∈ (Finset.univ : Finset ι') := by simp exact le_ciSup (Finite.bddAbove_range fun j : {j // j ∈ (Finset.univ : Finset ι')} => |(m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on H (Finset.univ : Finset ι') j (S' k)|) ⟨i, hidx⟩

lemma empiricalNorm_const_mul {𝒳 : Type*} {n : ℕ} (S : Fin n → 𝒳) (c : ℝ) (f : 𝒳 → ℝ) : empiricalNorm S (fun x => c * f x) = |c| * empiricalNorm S f := by classical unfold empiricalNorm have hsum : (∑ i : Fin n, (c * f (S i)) ^ 2) = c ^ 2 * ∑ i : Fin n, (f (S i)) ^ 2 := by rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro i _ ring_nf have hnonneg : 0 ≤ (1 / (n : ℝ)) * ∑ i : Fin n, (f (S i)) ^ 2 := by exact mul_nonneg (by positivity) (sum_nonneg fun i _ => sq_nonneg _) calc sqrt ((1 / (n : ℝ)) * ∑ i : Fin n, (c * f (S i)) ^ 2) = sqrt (c ^ 2 * ((1 / (n : ℝ)) * ∑ i : Fin n, (f (S i)) ^ 2)) := by rw [hsum] ring_nf _ = sqrt (c ^ 2) * sqrt ((1 / (n : ℝ)) * ∑ i : Fin n, (f (S i)) ^ 2) := by rw [Real.sqrt_mul (sq_nonneg c)] _ = |c| * sqrt ((1 / (n : ℝ)) * ∑ i : Fin n, (f (S i)) ^ 2) := by rw [Real.sqrt_sq_eq_abs]

lemma growthFamilyRep_spec {ι 𝒳 : Type*} {n : ℕ} (π : ι → 𝒳 → Bool) (S : Fin n → 𝒳) (A : {A // A ∈ growthFamily π S}) : restrictionPattern (π (growthFamilyRep π S A)) S = A.1 := Classical.choose_spec ((mem_growthFamily_iff (π := π) (S := S) (A := A.1)).mp A.2)

lemma starHullZeroOutScaleCoeff_nonneg {ι 𝒳 : Type*} (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (r : ℝ) (i : ι) : 0 ≤ starHullZeroOutScaleCoeff F norm r i := by classical let c : Icc (0 : ℝ) 1 → ℝ := fun a => if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0 have hc_bdd : BddAbove (range c) := by refine ⟨1, ?_⟩ rintro _ ⟨a, rfl⟩ dsimp [c] split_ifs · exact a.property.2 · norm_num let a0 : Icc (0 : ℝ) 1 := ⟨0, by simp [Set.mem_Icc]⟩ have hval : c a0 = 0 := by simp [c, a0] rw [starHullZeroOutScaleCoeff] change 0 ≤ ⨆ a : Icc (0 : ℝ) 1, c a simpa [hval] using le_ciSup hc_bdd a0

lemma starHullPatternCoeff_nonneg {ι 𝒳 : Type*} {n : ℕ} (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (S : Fin n → 𝒳) (r : ℝ) (A : {A // A ∈ growthFamily π S}) : 0 ≤ starHullPatternCoeff F norm π S r A := by classical let rep : {i : ι // restrictionPattern (π i) S = A.1} := ⟨growthFamilyRep π S A, growthFamilyRep_spec π S A⟩ have hcoeff_le : BddAbove (Set.range fun i : {i : ι // restrictionPattern (π i) S = A.1} => starHullZeroOutScaleCoeff F norm r i.1) := by refine ⟨1, ?_⟩ rintro _ ⟨i, rfl⟩ exact starHullZeroOutScaleCoeff_le_one F norm r i.1 have hrep_le : starHullZeroOutScaleCoeff F norm r rep.1 ≤ starHullPatternCoeff F norm π S r A := by rw [starHullPatternCoeff] exact le_ciSup hcoeff_le rep exact (starHullZeroOutScaleCoeff_nonneg F norm r rep.1).trans hrep_le

lemma sample_eq_growthFamilyRep_of_pattern {ι 𝒳 : Type*} {n : ℕ} {F : ι → 𝒳 → ℝ} {π : ι → 𝒳 → Bool} {S : Fin n → 𝒳} {φ : Fin n → Bool → ℝ} (hfactorS : ∀ i j, F i (S j) = φ j (π i (S j))) (A : {A // A ∈ growthFamily π S}) {i : ι} (hiA : restrictionPattern (π i) S = A.1) (k : Fin n) : F i (S k) = F (growthFamilyRep π S A) (S k) := by rw [hfactorS i k, hfactorS (growthFamilyRep π S A) k] apply congrArg (φ k) apply Bool.eq_iff_iff.mpr rw [← restrictionPattern_mem_iff (p := π i) (S := S) (j := k), hiA, ← growthFamilyRep_spec π S A, restrictionPattern_mem_iff (p := π (growthFamilyRep π S A)) (S := S) (j := k)]

lemma starHullZeroOut_empirical_rademacher_le_patternClass {ι 𝒳 : Type*} [Nonempty ι] {n : ℕ} (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) (S : Fin n → 𝒳) (r : ℝ) : empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ empiricalRademacherComplexity n (starHullPatternClass F norm π S r) S := by classical rcases hfactor S with ⟨φ, hφ⟩ haveI : Nonempty {A // A ∈ growthFamily π S} := by let i0 : ι := Classical.arbitrary ι have hmem : restrictionPattern (π i0) S ∈ growthFamily π S := by rw [mem_growthFamily_iff] exact ⟨i0, rfl⟩ exact ⟨⟨restrictionPattern (π i0) S, hmem⟩⟩ unfold empiricalRademacherComplexity refine mul_le_mul_of_nonneg_left ?_ (by positivity) refine Finset.sum_le_sum ?_ intro σ _ refine ciSup_le ?_ intro p rcases p with ⟨a, i⟩ let A0 : Finset (Fin n) := restrictionPattern (π i) S have hA0 : A0 ∈ growthFamily π S := by rw [mem_growthFamily_iff] exact ⟨i, rfl⟩ let A : {A // A ∈ growthFamily π S} := ⟨A0, hA0⟩ have hiA : restrictionPattern (π i) S = A.1 := rfl let active : ℝ := if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0 let innerI : ℝ := (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k) let innerRep : ℝ := (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F (growthFamilyRep π S A) (S k) have hstar : |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r (a, i) (S k)| = active * |innerI| := by simpa [active, innerI] using starHullZeroOut_inner_term_eq F norm r S σ a i have hinner : innerI = innerRep := by simp [innerI, innerRep, sample_eq_growthFamilyRep_of_pattern (F := F) (π := π) (S := S) (φ := φ) hφ A hiA] have hactive_nonneg : 0 ≤ active := by dsimp [active] split_ifs · exact a.property.1 · norm_num have hscale_le : active ≤ starHullZeroOutScaleCoeff F norm r i := by simpa [active] using activeCoeff_le_starHullZeroOutScaleCoeff F norm r a i have hcoeff_le : starHullZeroOutScaleCoeff F norm r i ≤ starHullPatternCoeff F norm π S r A := starHullZeroOutScaleCoeff_le_patternCoeff F norm π S r A i hiA have hterm_le : active * |innerI| ≤ starHullPatternCoeff F norm π S r A * |innerRep| := by calc active * |innerI| ≤ starHullZeroOutScaleCoeff F norm r i * |innerI| := mul_le_mul_of_nonneg_right hscale_le (abs_nonneg _) _ ≤ starHullPatternCoeff F norm π S r A * |innerI| := mul_le_mul_of_nonneg_right hcoeff_le (abs_nonneg _) _ = starHullPatternCoeff F norm π S r A * |innerRep| := by rw [hinner] have hpattern : starHullPatternCoeff F norm π S r A * |innerRep| = |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullPatternClass F norm π S r A (S k)| := by have hcoeff_nonneg := starHullPatternCoeff_nonneg F norm π S r A have hlin : (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullPatternClass F norm π S r A (S k) = starHullPatternCoeff F norm π S r A * innerRep := by dsimp [starHullPatternClass, innerRep] calc (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * (starHullPatternCoeff F norm π S r A * F (growthFamilyRep π S A) (S k)) = (n : ℝ)⁻¹ * (starHullPatternCoeff F norm π S r A * ∑ k : Fin n, (σ k : ℝ) * F (growthFamilyRep π S A) (S k)) := by congr 1 rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro k _ ring _ = starHullPatternCoeff F norm π S r A * ((n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F (growthFamilyRep π S A) (S k)) := by ring symm calc |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullPatternClass F norm π S r A (S k)| = |starHullPatternCoeff F norm π S r A * innerRep| := by rw [hlin] _ = starHullPatternCoeff F norm π S r A * |innerRep| := by rw [abs_mul, abs_of_nonneg hcoeff_nonneg] calc |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r (a, i) (S k)| = active * |innerI| := hstar _ ≤ starHullPatternCoeff F norm π S r A * |innerRep| := hterm_le _ = |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullPatternClass F norm π S r A (S k)| := hpattern _ ≤ ⨆ A : {A // A ∈ growthFamily π S}, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullPatternClass F norm π S r A (S k)| := by exact le_ciSup (Finite.bddAbove_range fun A : {A // A ∈ growthFamily π S} => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullPatternClass F norm π S r A (S k)|) A

lemma sqrt_sum_inv_abs_sq_eq_empiricalNorm_div_sqrt {𝒳 : Type*} {n : ℕ} (hn : 0 < n) (S : Fin n → 𝒳) (g : 𝒳 → ℝ) : sqrt (∑ k : Fin n, ((n : ℝ)⁻¹ * |g (S k)|) ^ 2) = empiricalNorm S g / sqrt (n : ℝ) := by classical have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hsum : (∑ k : Fin n, ((n : ℝ)⁻¹ * |g (S k)|) ^ 2) = (n : ℝ)⁻¹ * ((n : ℝ)⁻¹ * ∑ k : Fin n, (g (S k)) ^ 2) := by calc (∑ k : Fin n, ((n : ℝ)⁻¹ * |g (S k)|) ^ 2) = ∑ k : Fin n, ((n : ℝ)⁻¹) ^ 2 * (g (S k)) ^ 2 := by refine Finset.sum_congr rfl ?_ intro k _ rw [mul_pow, sq_abs] _ = ((n : ℝ)⁻¹) ^ 2 * ∑ k : Fin n, (g (S k)) ^ 2 := by rw [Finset.mul_sum] _ = (n : ℝ)⁻¹ * ((n : ℝ)⁻¹ * ∑ k : Fin n, (g (S k)) ^ 2) := by ring calc sqrt (∑ k : Fin n, ((n : ℝ)⁻¹ * |g (S k)|) ^ 2) = sqrt ((n : ℝ)⁻¹ * ((n : ℝ)⁻¹ * ∑ k : Fin n, (g (S k)) ^ 2)) := by rw [hsum] _ = sqrt ((n : ℝ)⁻¹) * sqrt ((n : ℝ)⁻¹ * ∑ k : Fin n, (g (S k)) ^ 2) := by rw [Real.sqrt_mul (inv_nonneg.mpr (le_of_lt hnR))] _ = (sqrt (n : ℝ))⁻¹ * sqrt ((n : ℝ)⁻¹ * ∑ k : Fin n, (g (S k)) ^ 2) := by rw [Real.sqrt_inv] _ = empiricalNorm S g / sqrt (n : ℝ) := by unfold empiricalNorm ring

lemma starHullZeroOutScaleCoeff_mul_empiricalNorm_le {ι 𝒳 : Type*} {n : ℕ} (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (Hloc : LocalizedVCDudleyHypotheses F norm) (S : Fin n → 𝒳) {r : ℝ} (hr : 0 ≤ r) (i : ι) : starHullZeroOutScaleCoeff F norm r i * empiricalNorm S (F i) ≤ r := by classical have hnorm_nonneg : 0 ≤ empiricalNorm S (F i) := by unfold empiricalNorm positivity have hmul : (⨆ a : Icc (0 : ℝ) 1, (if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0) * empiricalNorm S (F i)) = starHullZeroOutScaleCoeff F norm r i * empiricalNorm S (F i) := by rw [ciSup_mul_const_of_le_one (fun a : Icc (0 : ℝ) 1 => if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0) (empiricalNorm S (F i)) hnorm_nonneg] rfl rw [← hmul] refine ciSup_le ?_ intro a by_cases hactive : norm (starHullEval F (a, i)) ≤ r · have hnorm := Hloc.empirical_radius S hr (a, i) have heq : empiricalNorm S (starHullZeroOut F norm r (a, i)) = (a : ℝ) * empiricalNorm S (F i) := by calc empiricalNorm S (starHullZeroOut F norm r (a, i)) = empiricalNorm S (fun x => (a : ℝ) * F i x) := by congr funext x simp [starHullZeroOut, hactive, starHullEval] _ = (a : ℝ) * empiricalNorm S (F i) := by simpa [abs_of_nonneg a.property.1] using empiricalNorm_const_mul S (a : ℝ) (F i) simpa [hactive, heq] using hnorm · calc (if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0) * empiricalNorm S (F i) = 0 := by simp [hactive] _ ≤ r := hr

lemma starHullZeroOut_empirical_rademacher_le_growthFamily [Nonempty ι] (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) {n : ℕ} (hn : 0 < n) (Hloc : LocalizedVCDudleyHypotheses F norm) (S : Fin n → 𝒳) (r : ℝ) (hr : 0 ≤ r) : empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ r * sqrt ((2 * log (2 * ((growthFamily π S).card : ℝ))) / (n : ℝ)) := by classical let W : {A // A ∈ growthFamily π S} → 𝒳 → ℝ := starHullPatternClass F norm π S r have hgf_nonempty : (growthFamily π S).Nonempty := by let i0 : ι := Classical.arbitrary ι refine ⟨restrictionPattern (π i0) S, ?_⟩ rw [mem_growthFamily_iff] exact ⟨i0, rfl⟩ haveI : Nonempty {A // A ∈ growthFamily π S} := by rcases hgf_nonempty with ⟨A, hA⟩ exact ⟨⟨A, hA⟩⟩ have hcollapse : empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ empiricalRademacherComplexity n W S := by simpa [W] using starHullZeroOut_empirical_rademacher_le_patternClass F norm π hfactor S r have hfinite_on : empiricalRademacherComplexity n (F_on W (Finset.univ : Finset {A // A ∈ growthFamily π S})) S ≤ (r / sqrt (n : ℝ)) * sqrt (2 * log (2 * (((Finset.univ : Finset {A // A ∈ growthFamily π S}).card : ℝ)))) := by refine empiricalRademacher_withAbs_finiteClass_le (ι' := {A // A ∈ growthFamily π S}) (Z := 𝒳) hn W S (Finset.univ : Finset {A // A ∈ growthFamily π S}) ?_ (r / sqrt (n : ℝ)) ?_ · simpa using (Finset.univ_nonempty : (Finset.univ : Finset {A // A ∈ growthFamily π S}).Nonempty) · intro A _hA simpa [W] using starHullPatternClass_radius_le hn F norm π hfactor Hloc S hr A have hfinite : empiricalRademacherComplexity n W S ≤ (r / sqrt (n : ℝ)) * sqrt (2 * log (2 * ((growthFamily π S).card : ℝ))) := by have hcard : (((Finset.univ : Finset {A // A ∈ growthFamily π S}).card : ℝ)) = ((growthFamily π S).card : ℝ) := by simp have hfinite_univ := hfinite_on rw [empiricalRademacherComplexity_F_on_univ_eq W S] at hfinite_univ simpa [hcard] using hfinite_univ let L : ℝ := 2 * log (2 * ((growthFamily π S).card : ℝ)) have hcard_pos : 0 < (growthFamily π S).card := Finset.card_pos.mpr hgf_nonempty have hlog_nonneg : 0 ≤ log (2 * ((growthFamily π S).card : ℝ)) := by have hcard_one : (1 : ℝ) ≤ ((growthFamily π S).card : ℝ) := by exact_mod_cast (Nat.succ_le_of_lt hcard_pos) have hone_le : (1 : ℝ) ≤ 2 * ((growthFamily π S).card : ℝ) := by nlinarith exact Real.log_nonneg hone_le have hL_nonneg : 0 ≤ L := by dsimp [L] exact mul_nonneg (by norm_num) hlog_nonneg calc empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ empiricalRademacherComplexity n W S := hcollapse _ ≤ (r / sqrt (n : ℝ)) * sqrt L := by simpa [L] using hfinite _ = r * sqrt (L / (n : ℝ)) := by rw [Real.sqrt_div hL_nonneg] ring _ = r * sqrt ((2 * log (2 * ((growthFamily π S).card : ℝ))) / (n : ℝ)) := by rfl

lemma starHullZeroOut_empirical_rademacher_massart_vc (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) (d n : ℕ) (Htrace : BinaryTraceEntropyControl π d) (Hloc : LocalizedVCDudleyHypotheses F norm) : ∀ (S : Fin n → 𝒳) (r : ℝ), 0 ≤ r → empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ r * sqrt ((2 * (d : ℝ) * log ((n : ℝ) + 1) + 2) / (n : ℝ)) := by intro S r hr by_cases hn0 : n = 0 · subst n simp [empiricalRademacherComplexity] · have hn : 0 < n := Nat.pos_of_ne_zero hn0 by_cases hι : Nonempty ι · haveI : Nonempty ι := hι have hcard_pos : 0 < (growthFamily π S).card := by let i0 : ι := Classical.choice hι have hmem : restrictionPattern (π i0) S ∈ growthFamily π S := by rw [mem_growthFamily_iff] exact ⟨i0, rfl⟩ exact Finset.card_pos.mpr ⟨_, hmem⟩ have hcard : (growthFamily π S).card ≤ (n + 1) ^ d := growthFamily_card_le_succ_pow_of_trace π d n Htrace S have hmass := starHullZeroOut_empirical_rademacher_le_growthFamily F norm π hfactor hn Hloc S r hr have hlog := log_two_growth_card_le π d n S hcard_pos hcard have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hsqrt : sqrt ((2 * log (2 * ((growthFamily π S).card : ℝ))) / (n : ℝ)) ≤ sqrt ((2 * (d : ℝ) * log ((n : ℝ) + 1) + 2) / (n : ℝ)) := by exact Real.sqrt_le_sqrt (div_le_div_of_nonneg_right hlog (le_of_lt hnR)) exact hmass.trans (mul_le_mul_of_nonneg_left hsqrt hr) · letI : IsEmpty ι := ⟨fun i => hι ⟨i⟩⟩ have hzero : empiricalRademacherComplexity n (starHullZeroOut F norm r) S = 0 := by simp [empiricalRademacherComplexity, starHullParam] rw [hzero] exact mul_nonneg hr (Real.sqrt_nonneg _)

lemma absolute_dudley_vc_starHullZeroOut_linear_residual_shared (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) (K : ℝ) (d n : ℕ) (hK : (1 : ℝ) ≤ K) (Htrace : BinaryTraceEntropyControl π d) (Hloc : LocalizedVCDudleyHypotheses F norm) : ∀ (S : Fin n → 𝒳) (r : ℝ), 0 ≤ r → empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ vcLocalizedPsi K d n r := by intro S r hr have hmass := starHullZeroOut_empirical_rademacher_massart_vc F norm π hfactor d n Htrace Hloc S r hr by_cases hn0 : n = 0 · simpa [vcLocalizedPsi, vcLocalizedSlope, hn0] using hmass · have hn : 0 < n := Nat.pos_of_ne_zero hn0 have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hK0 : 0 ≤ K := le_trans zero_le_one hK have hlog : 0 ≤ log ((n : ℝ) + 1) := by have hone_le : (1 : ℝ) ≤ (n : ℝ) + 1 := by linarith [le_of_lt hnR] exact Real.log_nonneg hone_le have hD_nonneg : 0 ≤ (d : ℝ) * log ((n : ℝ) + 1) := mul_nonneg (Nat.cast_nonneg d) hlog have hKD : (d : ℝ) * log ((n : ℝ) + 1) ≤ K * (d : ℝ) * log ((n : ℝ) + 1) := by calc (d : ℝ) * log ((n : ℝ) + 1) = 1 * ((d : ℝ) * log ((n : ℝ) + 1)) := by ring _ ≤ K * ((d : ℝ) * log ((n : ℝ) + 1)) := mul_le_mul_of_nonneg_right hK hD_nonneg _ = K * (d : ℝ) * log ((n : ℝ) + 1) := by ring have hnum : 2 * (d : ℝ) * log ((n : ℝ) + 1) + 2 ≤ 36 * (K * (d : ℝ) * log ((n : ℝ) + 1) + 1) := by nlinarith have hfrac : (2 * (d : ℝ) * log ((n : ℝ) + 1) + 2) / (n : ℝ) ≤ 36 * ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ)) := by have hdiv := div_le_div_of_nonneg_right hnum (le_of_lt hnR) simpa [mul_div_assoc, mul_assoc] using hdiv have hsqrt : sqrt ((2 * (d : ℝ) * log ((n : ℝ) + 1) + 2) / (n : ℝ)) ≤ 6 * sqrt ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ)) := by calc sqrt ((2 * (d : ℝ) * log ((n : ℝ) + 1) + 2) / (n : ℝ)) ≤ sqrt (36 * ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ))) := Real.sqrt_le_sqrt hfrac _ = 6 * sqrt ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ)) := by have hsqrt36 : sqrt (36 : ℝ) = 6 := by have hsq : (sqrt (36 : ℝ)) ^ 2 = (6 : ℝ) ^ 2 := by rw [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 36)] norm_num rcases (sq_eq_sq_iff_eq_or_eq_neg.mp hsq) with h | h · exact h · nlinarith [Real.sqrt_nonneg (36 : ℝ)] rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 36)] rw [hsqrt36] calc empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ r * sqrt ((2 * (d : ℝ) * log ((n : ℝ) + 1) + 2) / (n : ℝ)) := hmass _ ≤ r * (6 * sqrt ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ))) := mul_le_mul_of_nonneg_left hsqrt hr _ = vcLocalizedPsi K d n r := by simp [vcLocalizedPsi, vcLocalizedSlope] ring

lemma vc_starHullZeroOut_empirical_rademacher_le_linear (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (K : ℝ) (d n : ℕ) (hK : (1 : ℝ) ≤ K) (Hvc : BinaryFactoredVCClass F d) (Hloc : LocalizedVCDudleyHypotheses F norm) : ∀ (S : Fin n → 𝒳) (r : ℝ), 0 ≤ r → empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ vcLocalizedPsi K d n r := absolute_dudley_vc_starHullZeroOut_linear_residual_shared F norm Hvc.π Hvc.factor K d n hK (inl Hvc.vcDim_le) Hloc

lemma vc_starHullZeroOut_empirical_rademacher_le_linear_of_card (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) (K : ℝ) (dPi n : ℕ) (hK : (1 : ℝ) ≤ K) (hcard : ∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ dPi) (Hloc : LocalizedVCDudleyHypotheses F norm) : ∀ (S : Fin n → 𝒳) (r : ℝ), 0 ≤ r → empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ vcLocalizedPsi K dPi n r := absolute_dudley_vc_starHullZeroOut_linear_residual_shared F norm π hfactor K dPi n hK (inr hcard) Hloc

lemma vc_starHullZeroOut_population_rademacher_le_linear (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) [IsProbabilityMeasure μ] (K : ℝ) (d n : ℕ) (hK : (1 : ℝ) ≤ K) (Hvc : BinaryFactoredVCClass F d) (Hloc : LocalizedVCDudleyHypotheses F norm) : ∀ r : ℝ, 0 ≤ r → rademacherComplexity n (starHullZeroOut F norm r) μ X ≤ vcLocalizedPsi K d n r := by intro r hr let C := vcLocalizedPsi K d n r have hpoint : ∀ S : Fin n → 𝒳, empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ C := by intro S exact vc_starHullZeroOut_empirical_rademacher_le_linear F norm K d n hK Hvc Hloc S r hr have h_abs : ∀ᵐ ω : Fin n → Ω ∂(Measure.pi fun _ : Fin n => μ), |empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)| ≤ C := by exact Filter.Eventually.of_forall fun ω => by have hnonneg : 0 ≤ empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω) := by unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro p exact abs_nonneg _ rw [abs_of_nonneg hnonneg] exact hpoint (X ∘ ω) unfold rademacherComplexity change ∫ ω : Fin n → Ω, empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω) ∂(Measure.pi fun _ : Fin n => μ) ≤ C exact le_trans (le_abs_self _) (abs_expectation_le_of_abs_le_const h_abs)

lemma vc_starHullZeroOut_population_rademacher_le_linear_of_card (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (μ : Measure Ω) (X : Ω → 𝒳) [IsProbabilityMeasure μ] (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) (K : ℝ) (dPi n : ℕ) (hK : (1 : ℝ) ≤ K) (hcard : ∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ dPi) (Hloc : LocalizedVCDudleyHypotheses F norm) : ∀ r : ℝ, 0 ≤ r → rademacherComplexity n (starHullZeroOut F norm r) μ X ≤ vcLocalizedPsi K dPi n r := by intro r hr let C := vcLocalizedPsi K dPi n r have hpoint : ∀ S : Fin n → 𝒳, empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ C := by intro S exact vc_starHullZeroOut_empirical_rademacher_le_linear_of_card F norm π hfactor K dPi n hK hcard Hloc S r hr have h_abs : ∀ᵐ ω : Fin n → Ω ∂(Measure.pi fun _ : Fin n => μ), |empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)| ≤ C := by exact Filter.Eventually.of_forall fun ω => by have hnonneg : 0 ≤ empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω) := by unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro p exact abs_nonneg _ rw [abs_of_nonneg hnonneg] exact hpoint (X ∘ ω) unfold rademacherComplexity change ∫ ω : Fin n → Ω, empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω) ∂(Measure.pi fun _ : Fin n => μ) ≤ C exact le_trans (le_abs_self _) (abs_expectation_le_of_abs_le_const h_abs)

theorem vcLocalizedRademacherUpperBound (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) [IsProbabilityMeasure μ] (K : ℝ) (d n : ℕ) (hK : (1 : ℝ) ≤ K) (Hvc : BinaryFactoredVCClass F d) (Hloc : LocalizedVCDudleyHypotheses F norm) : RademacherUpperBound F norm μ X n (vcLocalizedPsi K d n) := by intro r hr exact vc_starHullZeroOut_population_rademacher_le_linear F norm μ X K d n hK Hvc Hloc r hr

theorem vcLocalizedRademacherUpperBound_of_card (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (μ : Measure Ω) (X : Ω → 𝒳) [IsProbabilityMeasure μ] (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) (K : ℝ) (dPi n : ℕ) (hK : (1 : ℝ) ≤ K) (hcard : ∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ dPi) (Hloc : LocalizedVCDudleyHypotheses F norm) : RademacherUpperBound F norm μ X n (vcLocalizedPsi K dPi n) := by intro r hr exact vc_starHullZeroOut_population_rademacher_le_linear_of_card F norm π μ X hfactor K dPi n hK hcard Hloc r hr

theorem vcLocalizedEnvelope (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) [IsProbabilityMeasure μ] (K : ℝ) (d n : ℕ) (hK : (1 : ℝ) ≤ K) (hn : 0 < n) (Hvc : BinaryFactoredVCClass F d) (Hloc : LocalizedVCDudleyHypotheses F norm) : SubRoot (vcLocalizedPsi K d n) ∧ RademacherUpperBound F norm μ X n (vcLocalizedPsi K d n) ∧ criticalRadius (vcLocalizedPsi K d n) ≤ vcLocalizedSlope K d n ∧ (criticalRadius (vcLocalizedPsi K d n)) ^ 2 ≤ 36 * ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ)) := by refine ⟨vcLocalizedPsi_subRoot K d n, ?_, ?_, ?_⟩ · exact vcLocalizedRademacherUpperBound F norm μ X K d n hK Hvc Hloc · exact criticalRadius_vcLocalizedPsi_le (le_trans zero_le_one hK) hn · exact criticalRadius_vcLocalizedPsi_sq_le_rate (le_trans zero_le_one hK) hn

theorem term_le_total_sum_of_nonneg {α : Type u} [Fintype α] {M : Type*} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] (j : α) (f : α → M) (h0 : ∀ j, 0 ≤ f j) : f j ≤ ∑ i : α, f i := by classical have hj : j ∈ (Finset.univ : Finset α) := by simp have hsum : (Finset.univ.erase j).sum (fun i : α => f i) + f j = ∑ i : α, f i := by exact Finset.sum_erase_add _ _ hj have h_nonneg : 0 ≤ (Finset.univ.erase j).sum (fun i : α => f i) := by refine sum_nonneg ?_ intro i hi exact h0 i have h_le : f j ≤ (Finset.univ.erase j).sum (fun i : α => f i) + f j := by simpa [add_comm] using add_le_add_left h_nonneg (f j) exact h_le.trans_eq hsum

lemma pointwise_bound_from_empirical_norm (cs : ∀ f : ι, empiricalNorm S (F f) ≤ c) (i : Fin m) (hm_pos : 0 < m) : ∀ (f : ι), |F f (S i)| ≤ √↑m * c := by intro f dsimp [empiricalNorm] at cs have fcs := cs f -- from a finite-sample ℓ₂ bound to a pointwise bound via the coordinate projection inequality have hm_pos : 0 < (m : ℝ) := by norm_cast have hm_sqrt_pos : 0 < sqrt (m : ℝ) := Real.sqrt_pos.2 hm_pos have hproj := empiricalDist_proj (S := S) (f := F f) (i := i) have hcancel : sqrt (m : ℝ) ≠ 0 := ne_of_gt hm_sqrt_pos have h1 : |F f (S i)| ≤ √↑m * empiricalNorm S (F f) := by have hproj' := mul_le_mul_of_nonneg_left hproj (le_of_lt hm_sqrt_pos) -- simplify the left side using positivity of √m have hleft : √↑m * (|F f (S i)| / √↑m) = |F f (S i)| := by field_simp [hcancel] simpa [hleft] using hproj' calc |F f (S i)| ≤ √↑m * empiricalNorm S (F f) := h1 _ ≤ √↑m * c := by apply mul_le_mul_of_nonneg_left fcs exact le_of_lt hm_sqrt_pos

theorem splitBound.bddAbove_main_term {c_pos : 0 < c} (cs : ∀ (f : ι), empiricalNorm S (F f) ≤ c) (h : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (n : ℕ) (m_pos : ¬m = 0) (i : Signs m) : BddAbove (range fun fh ↦ ∑ i_1, ↑↑(i i_1) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1))) := by rw [bddAbove_def] classical refine ⟨m * (2 * (sqrt (m : ℝ) * c)), ?_⟩ intro y hy rcases hy with ⟨fh, rfl⟩ have hmpos : 0 < m := Nat.pos_of_ne_zero m_pos calc (∑ i_1, (i i_1 : ℝ) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1))) ≤ ∑ i_1, |(i i_1 : ℝ) * (F fh (S i_1) - chainApprox c_pos h fh n (S i_1))| := by refine Finset.sum_le_sum ?_ intro _ _ exact le_abs_self _ _ = ∑ i_1, |F fh (S i_1) - chainApprox c_pos h fh n (S i_1)| := by apply Finset.sum_congr rfl intro _ _ simp [abs_mul] _ ≤ ∑ i_1, (|F fh (S i_1)| + |chainApprox c_pos h fh n (S i_1)|) := by refine Finset.sum_le_sum ?_ intro i_1 _ have htri : |F fh (S i_1) - chainApprox c_pos h fh n (S i_1)| ≤ |F fh (S i_1)| + |chainApprox c_pos h fh n (S i_1)| := by exact abs_sub (F fh (S i_1)) (chainApprox c_pos h fh n (S i_1)) exact htri _ ≤ ∑ i_1, (sqrt (m : ℝ) * c + sqrt (m : ℝ) * c) := by refine Finset.sum_le_sum ?_ intro i_1 _ have hF : |F fh (S i_1)| ≤ sqrt (m : ℝ) * c := pointwise_bound_from_empirical_norm cs i_1 hmpos fh have hG : |chainApprox c_pos h fh n (S i_1)| ≤ sqrt (m : ℝ) * c := chainApprox_pointwise_bound c_pos hmpos cs n h i_1 fh have : |F fh (S i_1)| + |chainApprox c_pos h fh n (S i_1)| ≤ sqrt (m : ℝ) * c + sqrt (m : ℝ) * c := by nlinarith exact this _ = m * (2 * (sqrt (m : ℝ) * c)) := by simp grind

theorem splitBound.bddAbove_increment_term {c_pos : 0 < c} (cs : ∀ (f : ι), empiricalNorm S (F f) ≤ c) (h : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (n : ℕ) (m_pos : ¬m = 0) (i : Signs m) : BddAbove (Set.range fun fh ↦ ∑ x_1 : Fin n, ∑ i_1, ↑↑(i i_1) * (chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1))) := by rw [bddAbove_def] classical refine ⟨(n : ℝ) * m * (2 * (sqrt (m : ℝ) * c)), ?_⟩ intro y hy rcases hy with ⟨fh, rfl⟩ have hmpos : 0 < m := Nat.pos_of_ne_zero m_pos calc (∑ x_1 : Fin n, ∑ i_1, (i i_1 : ℝ) * (chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1))) ≤ ∑ x_1 : Fin n, ∑ i_1, |(i i_1 : ℝ) * (chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1))| := by refine Finset.sum_le_sum ?_ intro _ _ refine Finset.sum_le_sum ?_ intro _ _ exact le_abs_self _ _ = ∑ x_1 : Fin n, ∑ i_1, |chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1)| := by apply Finset.sum_congr rfl intro _ _ apply Finset.sum_congr rfl intro i_1 _ obtain ⟨v, hv⟩ := i i_1 simp at hv cases hv with | inl hv => simp [hv]; rw [<- abs_neg]; apply congrArg; linarith | inr hv => simp [hv] _ ≤ ∑ x_1 : Fin n, ∑ i_1, 2 * (sqrt (m : ℝ) * c) := by refine Finset.sum_le_sum ?_ intro x_1 _ refine Finset.sum_le_sum ?_ intro i_1 _ have hdiff : |chainApprox c_pos h fh (↑x_1 + 1) (S i_1) - chainApprox c_pos h fh (↑x_1) (S i_1)| ≤ 2 * (sqrt (m : ℝ) * c) := chainApprox_increment_bound c_pos hmpos cs (↑x_1) h i_1 fh nlinarith _ = (n : ℝ) * m * (2 * (sqrt (m : ℝ) * c)) := by simp [Finset.sum_const, Finset.card_univ, mul_assoc, mul_left_comm, mul_comm]

lemma signed_sum_le_empiricalDist (f g : Z → ℝ) (σ : Signs m) : ∑ i : Fin m, (σ i : ℝ) * (f (S i) - g (S i)) ≤ m * empiricalDist S f g := by calc _ = @inner ℝ (EuclideanSpace ℝ (Fin m)) _ (toLp 2 fun i ↦ (σ i : ℝ)) (toLp 2 fun i ↦ f (S i) - g (S i)) := by simp [inner] apply Finset.sum_congr rfl intro i hi exact (RCLike.inner_apply' (↑↑(σ i) : ℝ) (f (S i) - g (S i))).symm -- Use Cauchy-Schwarz inequality _ ≤ (@norm (EuclideanSpace ℝ (Fin m)) _ (toLp 2 fun i ↦ (σ i : ℝ))) * (@norm (EuclideanSpace ℝ (Fin m)) _ (toLp 2 fun i ↦ f (S i) - g (S i))) := @real_inner_le_norm (EuclideanSpace ℝ (Fin m)) _ _ (toLp 2 fun i ↦ (σ i : ℝ)) (toLp 2 fun i ↦ f (S i) - g (S i)) _ = m * empiricalDist S f g := by simp [norm, empiricalNorm] have : (∑ i, (σ i : ℝ) ^ 2) = m := by have : (∑ i, (σ i : ℝ) ^ 2) = (∑ i : Fin m, 1) := by congr ext i obtain ⟨σi, hσi⟩ := σ i simp at hσi simp cases hσi with | inl h1 => right; rw [h1]; norm_num | inr h2 => left; rw [h2] rw [this] apply (Finset.sum_const 1).trans simp rw [Real.sqrt_eq_rpow, Real.sqrt_eq_rpow, ←mul_assoc] congr · rw [←Real.rpow_neg (by simp), ←Real.rpow_one_add' (by simp) (by norm_num)] congr norm_num · norm_num

theorem partB.mem_incrementPairFinset_repr (c_pos : 0 < c) (h' : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))) (n : ℕ) (j : Fin n) (hk : (Z → ℝ) × (Z → ℝ)) (hk0 : hk ∈ incrementPairFinset c_pos h' n j) : ∃ fh, (chainApprox c_pos h' fh ((j : ℕ) + 1), chainApprox c_pos h' fh (j : ℕ)) = hk := by dsimp [incrementPairFinset] at hk0 simp at hk0 dsimp [incrementPairSet] at hk0 exact hk0

theorem MonotoneOn.leftRiemann_sum_le_integral_antitoneOn (n : ℕ) (f : ℕ → ℝ) (g : ℝ → ℝ) (hf : Monotone f) (hg : AntitoneOn g (Icc (f 0) (f n))) (j : Fin n): (f (j+1) - f j) * g (f (j+1)) ≤ ∫ (x : ℝ) in (f j)..(f (j+1)), g x := by calc _ = ∫ (x : ℝ) in (f j)..(f (j+1)), g (f (j+1)) := by simp _ ≤ _ := by apply intervalIntegral.integral_mono_on · apply hf simp · apply AntitoneOn.intervalIntegrable exact antitoneOn_const · apply AntitoneOn.intervalIntegrable refine antitoneOn_iff_forall_lt.mpr ?_ intro a ha b hb hab apply hg · suffices uIcc (f (j : ℕ)) (f ((j : ℕ) + 1)) ⊆ Icc (f 0) (f n) from by grind refine Set.uIcc_subset_Icc ?_ ?_ · constructor · apply hf simp · apply hf simp · constructor · apply hf simp · apply hf refine Order.add_one_le_of_lt ?_; simp · suffices uIcc (f (j : ℕ)) (f ((j : ℕ) + 1)) ⊆ Icc (f 0) (f n) from by grind refine Set.uIcc_subset_Icc ?_ ?_ · constructor · apply hf simp · apply hf simp · constructor · apply hf simp · apply hf refine Order.add_one_le_of_lt ?_; simp exact le_of_lt hab intro x hx simp at hx apply hg · constructor · have : f 0 ≤ f (j : ℕ) := by apply hf; simp linarith · have : f ((j : ℕ) + 1) ≤ f n := by apply hf; refine Order.add_one_le_of_lt ?_; simp linarith · constructor · apply hf simp · apply hf refine Order.add_one_le_of_lt ?_; simp exact hx.2

theorem AntitoneOn.leftRiemann_sum_le_integral (n : ℕ) (f : ℕ → ℝ) (g : ℝ → ℝ) (hf : Antitone f) (hg : AntitoneOn g (Icc (f n) (f 0))): ∑ j : Fin n, (f j - f (j+1)) * g (f j) ≤ ∫ (x : ℝ) in (f n)..(f 0), g x := by by_cases hnpos : 0 < n · let h (p : ℕ) := f (n-p) have s0 : f n = h 0 := by dsimp [h] have s1 : f 0 = h n := by dsimp [h]; simp have hh' : Monotone h := by dsimp [h] change Monotone (f ∘ (fun p ↦ (n - p))) apply Antitone.comp exact hf exact antitone_const_tsub rw [s0, s1] rw [<- intervalIntegral.sum_integral_adjacent_intervals] have t : ∑ j : Fin n, (f (j : ℕ) - f ((j : ℕ) + 1)) * g (f (j : ℕ)) = ∑ j : Fin n, (h ((j : ℕ) + 1) - h (j : ℕ)) * g (h ((j : ℕ) + 1)) := by let φ : Fin n ≃ Fin n := { toFun := fun j => ⟨n - 1 - j, by have hlt : n - 1 < n := Nat.pred_lt (Nat.ne_of_gt hnpos) exact lt_of_le_of_lt (Nat.sub_le _ _) hlt⟩ invFun := fun j => ⟨n - 1 - j, by have hlt : n - 1 < n := Nat.pred_lt (Nat.ne_of_gt hnpos) exact lt_of_le_of_lt (Nat.sub_le _ _) hlt⟩ left_inv := by intro j apply Fin.ext have hjle : (j : ℕ) ≤ n - 1 := Nat.le_pred_of_lt j.is_lt have : n - 1 - (n - 1 - j) = j := by grind simp [this] right_inv := by intro j apply Fin.ext have hjle : (j : ℕ) ≤ n - 1 := Nat.le_pred_of_lt j.is_lt have : n - 1 - (n - 1 - j) = j := by grind simp [this] } have tsum := (Equiv.sum_comp φ (fun j : Fin n => (f j - f (j + 1)) * g (f j))) -- simp the rewritten sum to expose `h` refine tsum.symm.trans ?_ refine Finset.sum_congr rfl ?_ intro j _ -- unpack φ and h change (f (φ j) - f (φ j + 1)) * g (f (φ j)) = (h (j + 1) - h j) * g (h (j + 1)) dsimp [φ, h] -- arithmetic on naturals have hjle : (j : ℕ) ≤ n - 1 := Nat.le_pred_of_lt j.is_lt simp [Nat.sub_sub, Nat.add_comm] left apply congrArg grind rw [t] have u : ∑ k ∈ range n, ∫ (x : ℝ) in h k..h (k + 1), g x = ∑ k : Fin n, ∫ (x : ℝ) in h k..h (k + 1), g x := by exact Finset.sum_range fun i ↦ ∫ (x : ℝ) in h i..h (i + 1), g x rw [u] apply Finset.sum_le_sum intro i yi apply MonotoneOn.leftRiemann_sum_le_integral_antitoneOn · exact hh' · rw [<-s0] rw [<-s1] exact hg intro k kn apply AntitoneOn.intervalIntegrable rw [s0] at hg rw [s1] at hg apply hg.mono refine Set.uIcc_subset_Icc ?_ ?_ constructor · apply hh' simp · apply hh' linarith constructor · apply hh' simp · apply hh' linarith · have n_zero : n = 0 := by linarith rw [n_zero] simp

lemma sqrt_le_add_one_div_two {t : ℝ} (ht : 0 ≤ t) : sqrt t ≤ (t + 1) / 2 := by have hsq : 0 ≤ (sqrt t - 1) ^ 2 := sq_nonneg _ have hsqrt_sq : (sqrt t) ^ 2 = t := by rw [Real.sq_sqrt ht] nlinarith [hsq, Real.sqrt_nonneg t, hsqrt_sq]

lemma log_div_nonneg_of_mem_Icc {δ ε x : ℝ} (hε : 0 < ε) (hx : x ∈ Icc ε δ) : 0 ≤ log (δ / x) := by have hxpos : 0 < x := lt_of_lt_of_le hε hx.1 have hratio : 1 ≤ δ / x := by rw [le_div_iff₀ hxpos] simpa using hx.2 exact Real.log_nonneg hratio

lemma intervalIntegrable_sqrt_log_div {δ ε : ℝ} (hε : 0 < ε) (hεδ : ε ≤ δ) : IntervalIntegrable (fun x : ℝ => sqrt (log (δ / x))) volume ε δ := by have hcont : ContinuousOn (fun x : ℝ => sqrt (log (δ / x))) [[ε, δ]] := by simpa [Set.uIcc_of_le hεδ] using continuousOn_sqrt_log_div_Icc hε hεδ exact hcont.intervalIntegrable

lemma intervalIntegrable_log_div {δ ε : ℝ} (hε : 0 < ε) (hεδ : ε ≤ δ) : IntervalIntegrable (fun x : ℝ => log (δ / x)) volume ε δ := by have hδ : 0 < δ := lt_of_lt_of_le hε hεδ have hcont : ContinuousOn (fun x : ℝ => log (δ / x)) (Icc ε δ) := by refine ContinuousOn.log ?_ ?_ · exact (continuousOn_const (c := δ)).div continuousOn_id (fun x hx => by linarith [hx.1]) · intro x hx exact div_ne_zero (ne_of_gt hδ) (by linarith [hx.1]) have hcont' : ContinuousOn (fun x : ℝ => log (δ / x)) [[ε, δ]] := by simpa [Set.uIcc_of_le hεδ] using hcont exact hcont'.intervalIntegrable

lemma integral_log_div_eq {δ ε : ℝ} (hε : 0 < ε) (hεδ : ε ≤ δ) : (∫ x in ε..δ, log (δ / x)) = δ - ε - ε * log (δ / ε) := by have hδ : 0 < δ := lt_of_lt_of_le hε hεδ calc (∫ x in ε..δ, log (δ / x)) = ∫ x in ε..δ, (log δ - log x) := by refine intervalIntegral.integral_congr ?_ intro x hx have hxIcc : x ∈ Icc ε δ := by simpa [Set.uIcc_of_le hεδ] using hx have hxpos : 0 < x := lt_of_lt_of_le hε hxIcc.1 simpa using Real.log_div (ne_of_gt hδ) (ne_of_gt hxpos) _ = (δ - ε) * log δ - (δ * log δ - ε * log ε - δ + ε) := by rw [intervalIntegral.integral_sub] · rw [intervalIntegral.integral_const] rw [integral_log] simp [smul_eq_mul] · exact intervalIntegrable_const · exact intervalIntegral.intervalIntegrable_log' _ = δ - ε - ε * log (δ / ε) := by rw [Real.log_div (ne_of_gt hδ) (ne_of_gt hε)] ring

lemma integral_log_div_le {δ ε : ℝ} (hε : 0 < ε) (hεδ : ε ≤ δ) : (∫ x in ε..δ, log (δ / x)) ≤ δ - ε := by have hratio : 1 ≤ δ / ε := by rw [le_div_iff₀ hε] simpa using hεδ have hnonneg : 0 ≤ ε * log (δ / ε) := mul_nonneg (le_of_lt hε) (Real.log_nonneg hratio) rw [integral_log_div_eq hε hεδ] linarith