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_lt_top_of_totallyBounded {X : Type*} [PseudoMetricSpace X] {A : Set X} (ha : TotallyBounded A) {ε : ℝ} (hε : ε > 0) : coveringNumber A ε < ⊤ := by rw [coveringNumber_eq ha hε] exact ENat.natCast_lt_top _

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'_eq_zero_of_nonpos {X : Type*} [PseudoMetricSpace X] {A : Set X} (ha : TotallyBounded A) {ε : ℝ} (hε : ε ≤ 0) : coveringNumber' ha ε = 0 := by rw [coveringNumber', ENat.toNat_eq_zero] by_cases hA : A.Nonempty · right rw [coveringNumber] rw [show {n : ℕ∞ | ∃ t : Finset X, (t.card : ℕ∞) = n ∧ A ⊆ ⋃ y ∈ t, ball y ε} = ∅ by apply Set.eq_empty_iff_forall_notMem.mpr intro n hn obtain ⟨t, _htcard, htcover⟩ := hn obtain ⟨x, hx⟩ := hA have hxcover := htcover hx simp only [Set.mem_iUnion] at hxcover obtain ⟨y, _hy, hxy⟩ := hxcover have hdist : ε ≤ dist x y := hε.trans dist_nonneg exact (not_lt_of_ge hdist) (Metric.mem_ball.mp hxy)] exact sInf_empty · left rw [coveringNumber, ENat.sInf_eq_zero] refine ⟨∅, ?_, ?_⟩ · simp · simpa [Set.not_nonempty_iff_eq_empty.mp hA]

@[fun_prop] 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] exact coveringNumber'_eq_zero_of_nonpos ha (le_of_not_gt 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 Finset.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 := 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 False.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 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 Finset.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, Nat.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, Nat.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 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

lemma criticalRadius_linear_eq {C : ℝ} (hC : 0 < C) : criticalRadius (fun r : ℝ => C * r) = C := by apply le_antisymm · exact criticalRadius_linear_le hC · rw [criticalRadius] apply le_csInf · exact ⟨C, hC, by rw [pow_two]⟩ · rintro δ ⟨hδ_pos, hδ⟩ have hδ' : C * δ ≤ δ * δ := by simpa [pow_two] using hδ nlinarith [hδ', hδ_pos]

lemma vcLocalizedPsi_criticalRadius_fp {K : ℝ} {d n : ℕ} (hK : 0 ≤ K) (hn : 0 < n) : vcLocalizedPsi K d n (criticalRadius (vcLocalizedPsi K d n)) ≤ (criticalRadius (vcLocalizedPsi K d n)) ^ 2 := by let ρ := vcLocalizedSlope K d n have hρ_pos : 0 < ρ := vcLocalizedSlope_pos hK hn have hcrit_eq : criticalRadius (vcLocalizedPsi K d n) = ρ := by unfold vcLocalizedPsi exact criticalRadius_linear_eq hρ_pos rw [hcrit_eq] unfold vcLocalizedPsi ρ rw [pow_two]

lemma ciSup_prod_eq_of_bddAbove {A B : Type*} [Nonempty A] [Nonempty B] (f : A → B → ℝ) (hb : BddAbove (Set.range fun p : A × B => f p.1 p.2)) : (⨆ p : A × B, f p.1 p.2) = ⨆ b : B, ⨆ a : A, f a b := by classical have hinner_bdd : ∀ b : B, BddAbove (Set.range fun a : A => f a b) := by intro b rcases hb with ⟨M, hM⟩ refine ⟨M, ?_⟩ rintro _ ⟨a, rfl⟩ exact hM ⟨(a, b), rfl⟩ have houter_bdd : BddAbove (Set.range fun b : B => ⨆ a : A, f a b) := by rcases hb with ⟨M, hM⟩ refine ⟨M, ?_⟩ rintro _ ⟨b, rfl⟩ exact ciSup_le fun a => hM ⟨(a, b), rfl⟩ apply le_antisymm · refine ciSup_le ?_ intro p exact le_trans (le_ciSup (hinner_bdd p.2) p.1) (le_ciSup houter_bdd p.2) · refine ciSup_le ?_ intro b refine ciSup_le ?_ intro a exact le_ciSup hb (a, b)

lemma vc_starHullZeroOut_empirical_rademacher_aemeasurable [MeasurableSpace 𝒳] [Nonempty ι] [Countable ι] (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (hF_meas : ∀ i, Measurable (F i)) (μ : Measure 𝒳) (b r : ℝ) (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (n : ℕ) : AEMeasurable (fun ω : Fin n → 𝒳 => empiricalRademacherComplexity n (starHullZeroOut F norm r) (id ∘ ω)) (Measure.pi (fun _ => μ)) := by classical apply Measurable.aemeasurable unfold empiricalRademacherComplexity apply measurable_const.mul apply Finset.univ.measurable_sum intro σ _ have hsup_eq : (fun ω : Fin n → 𝒳 => ⨆ p : starHullParam ι, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p ((id ∘ ω) k)|) = fun ω : Fin n → 𝒳 => ⨆ i : ι, starHullZeroOutScaleCoeff F norm r i * |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (ω k)| := by funext ω have hbdd : BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p ((id ∘ ω) k)|) := by simpa using starHullZeroOut_bddAbove_of_bound F norm hb n r (id ∘ ω) (fun i k => hbound i _) σ calc (⨆ p : starHullParam ι, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p ((id ∘ ω) k)|) = ⨆ i : ι, ⨆ a : Icc (0 : ℝ) 1, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r (a, i) (ω k)| := by unfold starHullParam simpa [Function.comp_def] using ciSup_prod_eq_of_bddAbove (fun a : Icc (0 : ℝ) 1 => fun i : ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r (a, i) (ω k)|) hbdd _ = ⨆ i : ι, starHullZeroOutScaleCoeff F norm r i * |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (ω k)| := by congr ext i exact starHullZeroOut_inner_sup_eq F norm r ω σ i rw [hsup_eq] apply Measurable.iSup intro i apply measurable_const.mul apply Measurable.abs apply measurable_const.mul apply Finset.univ.measurable_sum intro k _ apply measurable_const.mul exact (hF_meas i).comp (measurable_pi_apply k)

lemma vc_starHullZeroOut_empirical_rademacher_integrable [MeasurableSpace 𝒳] [Nonempty ι] [Countable ι] (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure 𝒳) [IsProbabilityMeasure μ] (hF_meas : ∀ i, Measurable (F i)) (b : ℝ) (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (K : ℝ) (d n : ℕ) (hK : (1 : ℝ) ≤ K) (hn : 0 < n) (Hvc : BinaryFactoredVCClass F d) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) : ∀ r : ℝ, vcLocalizedSlope K d n ≤ r → Integrable (fun ω : Fin n → 𝒳 => empiricalRademacherComplexity n (starHullZeroOut F norm r) (id ∘ ω)) (Measure.pi (fun _ => μ)) := by intro r hr let g : (Fin n → 𝒳) → ℝ := fun ω => empiricalRademacherComplexity n (starHullZeroOut F norm r) (id ∘ ω) have hr_nonneg : 0 ≤ r := le_trans (vcLocalizedSlope_nonneg K d n) hr have hg_meas : AEMeasurable g (Measure.pi (fun _ : Fin n => μ)) := by simpa [g] using vc_starHullZeroOut_empirical_rademacher_aemeasurable F norm hF_meas μ b r hb hbound n have hg_nonneg : ∀ᵐ ω : Fin n → 𝒳 ∂(Measure.pi (fun _ : Fin n => μ)), 0 ≤ g ω := by exact Filter.Eventually.of_forall fun ω => by dsimp [g] unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine Finset.sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro p exact abs_nonneg _ have hg_upper : ∀ᵐ ω : Fin n → 𝒳 ∂(Measure.pi (fun _ : Fin n => μ)), g ω ≤ vcLocalizedPsi K d n r := by exact Filter.Eventually.of_forall fun ω => by dsimp [g] simpa using vc_starHullZeroOut_empirical_rademacher_le_linear F norm K d n hK Hvc Hloc (id ∘ ω) r hr_nonneg have hg_Icc : ∀ᵐ ω : Fin n → 𝒳 ∂(Measure.pi (fun _ : Fin n => μ)), g ω ∈ Icc 0 (vcLocalizedPsi K d n r) := by filter_upwards [hg_nonneg, hg_upper] with ω h0 h1 exact ⟨h0, h1⟩ exact integrable_bounded 0 (vcLocalizedPsi K d n r) hg_meas hg_Icc

lemma vc_starHullZeroOut_empirical_rademacher_integrable_of_card [MeasurableSpace 𝒳] [Nonempty ι] [Countable ι] (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (μ : Measure 𝒳) [IsProbabilityMeasure μ] (hF_meas : ∀ i, Measurable (F i)) (b : ℝ) (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) (K : ℝ) (dPi n : ℕ) (hK : (1 : ℝ) ≤ K) (hn : 0 < n) (hcard : ∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ dPi) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) : ∀ r : ℝ, vcLocalizedSlope K dPi n ≤ r → Integrable (fun ω : Fin n → 𝒳 => empiricalRademacherComplexity n (starHullZeroOut F norm r) (id ∘ ω)) (Measure.pi (fun _ => μ)) := by intro r hr let g : (Fin n → 𝒳) → ℝ := fun ω => empiricalRademacherComplexity n (starHullZeroOut F norm r) (id ∘ ω) have hr_nonneg : 0 ≤ r := le_trans (vcLocalizedSlope_nonneg K dPi n) hr have hg_meas : AEMeasurable g (Measure.pi (fun _ : Fin n => μ)) := by simpa [g] using vc_starHullZeroOut_empirical_rademacher_aemeasurable F norm hF_meas μ b r hb hbound n have hg_nonneg : ∀ᵐ ω : Fin n → 𝒳 ∂(Measure.pi (fun _ : Fin n => μ)), 0 ≤ g ω := by exact Filter.Eventually.of_forall fun ω => by dsimp [g] unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine Finset.sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro p exact abs_nonneg _ have hg_upper : ∀ᵐ ω : Fin n → 𝒳 ∂(Measure.pi (fun _ : Fin n => μ)), g ω ≤ vcLocalizedPsi K dPi n r := by exact Filter.Eventually.of_forall fun ω => by dsimp [g] simpa using vc_starHullZeroOut_empirical_rademacher_le_linear_of_card F norm π hfactor K dPi n hK hcard Hloc (id ∘ ω) r hr_nonneg have hg_Icc : ∀ᵐ ω : Fin n → 𝒳 ∂(Measure.pi (fun _ : Fin n => μ)), g ω ∈ Icc 0 (vcLocalizedPsi K dPi n r) := by filter_upwards [hg_nonneg, hg_upper] with ω h0 h1 exact ⟨h0, h1⟩ exact integrable_bounded 0 (vcLocalizedPsi K dPi n r) hg_meas hg_Icc

theorem vc_localized_deviation_event_eventually (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure 𝒳) [IsProbabilityMeasure μ] (hF_meas : ∀ i, Measurable (F i)) (b : ℝ) (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (hnorm_nonneg : ∀ i, 0 ≤ norm (F i)) (hvariance : ∀ i, variance (F i) μ ≤ norm (F i) ^ 2) (K : ℝ) (d : ℕ) (hK : (1 : ℝ) ≤ K) (hd : 0 < d) (Hvc : BinaryFactoredVCClass F d) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) {δ : ℝ} (hδ : 0 < δ) (hδ' : δ ≤ 1) : ∃ n₀ : ℕ, ∀ n ≥ n₀, ∀ L : ℕ, (L : ℝ) ≤ log ((n : ℝ) + 1) → b ≤ vcLocalizedSlope K d n * (2 : ℝ) ^ L → vcLocalizedSlope K d n ≤ b → ∃ E : Set (Fin n → 𝒳), MeasurableSet E ∧ Measure.pi (fun _ => μ) E ≥ 1 - ofReal δ ∧ ∀ ω ∈ E, ∀ i : ι, 0 ≤ norm (F i) → norm (F i) ≤ b → |(n : ℝ)⁻¹ * (Finset.univ.sum fun k : Fin n => F i (ω k)) - μ[fun x => F i x]| ≤ 10 * vcLocalizedSlope K d n * norm (F i) + 5 * (vcLocalizedSlope K d n) ^ 2 := by obtain ⟨n₀, hn₀⟩ := vcLocalizedSlope_peelingCondition_eventually hb hδ hδ' hK hd refine ⟨max n₀ 1, ?_⟩ intro n hn L hL hcover hρ_le_b have hn₀n : n₀ ≤ n := (Nat.le_max_left n₀ 1).trans hn have hnpos : 0 < n := Nat.zero_lt_one.trans_le ((Nat.le_max_right n₀ 1).trans hn) exact vc_localized_deviation_event F norm μ hF_meas b hb hbound hnorm_nonneg hvariance K d n hK hnpos Hvc Hloc hδ hδ' hρ_le_b (hn₀ n hn₀n L hL hcover)