Stat.Concentration.Covering.Real­Valued­VCSubgraph

theorem hasPseudoDimAtMost_iff_growthFamily (F : ι → 𝒳 → ℝ) (d : ℕ) : HasPseudoDimAtMost F d ↔ ∀ (n : ℕ) (T : Fin n → 𝒳 × ℝ), (growthFamily (subgraphClassifier F) T).vcDim ≤ d := by rfl

theorem sharp_vc_weightedHamming_packing_card_le {n : ℕ} (d : ℕ) (w : Fin n → ℝ) (hw : ∀ j, 0 ≤ w j) (r ε : ℝ) (hε : 0 < ε) (hεr : ε ≤ r) (hwsum : ∑ j, w j ≤ r ^ 2) (P : Finset (Fin n → Bool)) (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) : P.card ≤ ceil ((16 * r ^ 2 / ε ^ 2) ^ (2 * (d + 1))) := by classical let B : ℝ := 16 * r ^ 2 / ε ^ 2 have hr : 0 < r := hε.trans_le hεr have hx : 1 ≤ r ^ 2 / ε ^ 2 := by have hdiv : 1 ≤ r / ε := (one_le_div hε).2 hεr rw [← div_pow] nlinarith [sq_nonneg (r / ε)] have hB : 16 ≤ B := by dsimp [B] calc 16 ≤ 16 * (r ^ 2 / ε ^ 2) := by nlinarith _ = 16 * r ^ 2 / ε ^ 2 := by ring have hBpos : 0 < B := lt_of_lt_of_le (by norm_num) hB have hpow_one : 1 ≤ B ^ (2 * (d + 1)) := by exact one_le_pow₀ (by linarith) by_cases hsmall : P.card ≤ 1 · apply (Nat.cast_le (α := ℝ)).mp have hsmall' : (P.card : ℝ) ≤ 1 := by exact_mod_cast hsmall exact hsmall'.trans (hpow_one.trans (Nat.le_ceil _)) have hPcard : 2 ≤ P.card := by omega obtain ⟨m, J, hm, hvcJ, hinj⟩ := exists_separating_subsample d w hw r ε hr hε hwsum P hPcard hvc hsep have hcard_image : (P.image (subsamplePattern J)).card = P.card := Finset.card_image_of_injOn hinj have hcard_sum : P.card ≤ ∑ k ∈ Iic d, m.choose k := by rw [← hcard_image] exact card_growthFamily_le_sum_choose (P.image (subsamplePattern J)) hvcJ by_cases hd0 : d = 0 · have : P.card ≤ 1 := by rw [hd0, show Iic 0 = {0} by ext k; simp] at hcard_sum simpa using hcard_sum omega have hd : 0 < d := Nat.pos_of_ne_zero hd0 have hreal_goal : (P.card : ℝ) ≤ B ^ (2 * (d + 1)) := by by_cases hdm : d ≤ m · have hcard_scaled : (P.card : ℝ) ≤ (4 * (m : ℝ) / (d : ℝ)) ^ d := by have hc : (P.card : ℝ) ≤ ((∑ k ∈ Iic d, m.choose k : ℕ) : ℝ) := by exact_mod_cast hcard_sum exact hc.trans (sum_choose_le_four_mul_div_pow hd hdm) let L : ℝ := log (P.card) have hPpos : 0 < (P.card : ℝ) := by positivity have hmpos : 0 < m := lt_of_lt_of_le hd hdm have hbase_pos : 0 < 4 * (m : ℝ) / (d : ℝ) := by positivity have hlog_card : L ≤ (d : ℝ) * log (4 * (m : ℝ) / (d : ℝ)) := by calc L ≤ log ((4 * (m : ℝ) / (d : ℝ)) ^ d) := Real.log_le_log hPpos hcard_scaled _ = (d : ℝ) * log (4 * (m : ℝ) / (d : ℝ)) := Real.log_pow _ _ have htangent : log (4 * (m : ℝ) / (d : ℝ)) ≤ (4 * (m : ℝ) / (d : ℝ)) / B + log B - 1 := by have hratio : 0 < (4 * (m : ℝ) / (d : ℝ)) / B := by positivity have h := Real.log_le_sub_one_of_pos hratio rw [Real.log_div (ne_of_gt hbase_pos) (ne_of_gt hBpos)] at h linarith have hm' : (m : ℝ) ≤ 1 + (2 * r ^ 2 / ε ^ 2) * L := by simpa [L] using hm have hratio_bound : (4 * (m : ℝ) / (d : ℝ)) / B ≤ 1 / (4 * (d : ℝ)) + L / (2 * (d : ℝ)) := by dsimp [B] have hdreal : 0 < (d : ℝ) := by positivity have hscale : 0 < 4 / ((d : ℝ) * (16 * r ^ 2 / ε ^ 2)) := by positivity have := mul_le_mul_of_nonneg_left hm' hscale.le calc (4 * (m : ℝ) / (d : ℝ)) / (16 * r ^ 2 / ε ^ 2) = (4 / ((d : ℝ) * (16 * r ^ 2 / ε ^ 2))) * (m : ℝ) := by field_simp _ ≤ (4 / ((d : ℝ) * (16 * r ^ 2 / ε ^ 2))) * (1 + (2 * r ^ 2 / ε ^ 2) * L) := this _ = 1 / (4 * (d : ℝ)) * (ε ^ 2 / r ^ 2) + L / (2 * (d : ℝ)) := by field_simp; ring _ ≤ 1 / (4 * (d : ℝ)) + L / (2 * (d : ℝ)) := by have heps : ε ^ 2 / r ^ 2 ≤ 1 := by rw [div_le_one (sq_pos_of_pos hr)] nlinarith [sq_nonneg (r - ε)] have hcoef : 0 ≤ 1 / (4 * (d : ℝ)) := by positivity nlinarith [mul_le_mul_of_nonneg_left heps hcoef] have hL : L ≤ 2 * (d : ℝ) * log B := by have hdreal : 0 < (d : ℝ) := by positivity have hstep := hlog_card.trans (mul_le_mul_of_nonneg_left htangent (by positivity : 0 ≤ (d : ℝ))) have hstep' : L ≤ (d : ℝ) * (1 / (4 * (d : ℝ)) + L / (2 * (d : ℝ)) + log B - 1) := hstep.trans (mul_le_mul_of_nonneg_left (by linarith [hratio_bound]) (by positivity)) have hd_one : (1 : ℝ) ≤ d := by exact_mod_cast Nat.succ_le_iff.mpr hd have hstep'' : L ≤ 1 / 4 + L / 2 + (d : ℝ) * log B - (d : ℝ) := by convert hstep' using 1 <;> field_simp nlinarith have hlog_pow : log (B ^ (2 * (d + 1))) = (2 * (d + 1) : ℕ) * log B := Real.log_pow _ _ have hlog_le : L ≤ log (B ^ (2 * (d + 1))) := by rw [hlog_pow] have hlogB : 0 ≤ log B := Real.log_nonneg (by linarith) exact hL.trans (by norm_num [Nat.cast_mul, Nat.cast_add] nlinarith) change log (P.card : ℝ) ≤ log (B ^ (2 * (d + 1))) at hlog_le rw [← Real.exp_log hPpos, ← Real.exp_log (pow_pos hBpos _)] exact Real.exp_le_exp.mpr hlog_le · have hmd : m < d := Nat.lt_of_not_ge hdm have hcard_univ : (P.image (subsamplePattern J)).card ≤ (Finset.univ : Finset (Finset (Fin m))).card := Finset.card_le_univ _ have hcard_two : P.card ≤ 2 ^ m := by rw [hcard_image] at hcard_univ simpa using hcard_univ have htwoB : (2 : ℝ) ≤ B := by linarith calc (P.card : ℝ) ≤ (2 : ℝ) ^ m := by exact_mod_cast hcard_two _ ≤ B ^ m := pow_le_pow_left₀ (by norm_num) htwoB m _ ≤ B ^ (2 * (d + 1)) := by exact pow_le_pow_right₀ (by linarith) (by omega) apply (Nat.cast_le (α := ℝ)).mp exact hreal_goal.trans (Nat.le_ceil _)

theorem HasPolynomialL2Cover.neg {ι : Type v} {F : ι → 𝒳 → ℝ} {U : ℝ} (hF : HasPolynomialL2Cover F U) : HasPolynomialL2Cover (fun i x => -F i x) U := by refine ⟨hF.envelope_pos, fun i => (hF.measurable i).neg, ?_, ?_⟩ · intro i x simpa using hF.envelope i x · obtain ⟨A, p, hA, hent⟩ := hF.entropy refine ⟨A, p, hA, ?_⟩ intro Q hQ ε hε hε1 obtain ⟨C, hCcard, hCcover⟩ := hent Q hQ ε hε hε1 refine ⟨C, hCcard, ?_⟩ intro i obtain ⟨j, hjC, hij⟩ := hCcover i refine ⟨j, hjC, ?_⟩ have heq : measureL2Dist Q (fun x => -F i x) (fun x => -F j x) = measureL2Dist Q (F i) (F j) := by rw [measureL2Dist_eq_lpNorm Q _ _ (hF.measurable i).fun_neg (hF.measurable j).fun_neg, measureL2Dist_eq_lpNorm Q _ _ (hF.measurable i) (hF.measurable j)] have hfun : (fun x => -F i x - -F j x) = -(fun x => F i x - F j x) := by funext x simp only [Pi.neg_apply] ring rw [hfun, lpNorm_neg] rwa [heq]

theorem HasPolynomialL2Cover.add {ι : Type v} {κ : Type w} {F : ι → 𝒳 → ℝ} {G : κ → 𝒳 → ℝ} {U V : ℝ} (hF : HasPolynomialL2Cover F U) (hG : HasPolynomialL2Cover G V) : HasPolynomialL2Cover (fun p : ι × κ => fun x => F p.1 x + G p.2 x) (U + V) := by have hU : 0 < U := hF.envelope_pos have hV : 0 < V := hG.envelope_pos refine ⟨by positivity, fun p => (hF.measurable p.1).add (hG.measurable p.2), ?_, ?_⟩ · intro p x exact (abs_add_le _ _).trans (add_le_add (hF.envelope p.1 x) (hG.envelope p.2 x)) · obtain ⟨A, p, hA, hentF⟩ := hF.entropy obtain ⟨B, q, hB, hentG⟩ := hG.entropy refine ⟨8 * A * B, p + q + 2, by nlinarith [mul_nonneg (sub_nonneg.mpr hA) (sub_nonneg.mpr hB)], ?_⟩ intro Q hQ ε hε hε1 have hhalf : 0 < ε / 2 := by positivity have hhalf1 : ε / 2 ≤ 1 := by linarith obtain ⟨CF, hCFcard, hCFcover⟩ := hentF Q hQ (ε / 2) hhalf hhalf1 obtain ⟨CG, hCGcard, hCGcover⟩ := hentG Q hQ (ε / 2) hhalf hhalf1 rw [show A / (ε / 2) = 2 * A / ε by field_simp] at hCFcard rw [show B / (ε / 2) = 2 * B / ε by field_simp] at hCGcard classical refine ⟨CF ×ˢ CG, ?_, ?_⟩ · rw [Finset.card_product] exact (Nat.mul_le_mul hCFcard hCGcard).trans (ceil_mul_le_ceil_poly hA hB hε hε1) · intro a obtain ⟨i, hiC, hi⟩ := hCFcover a.1 obtain ⟨j, hjC, hj⟩ := hCGcover a.2 refine ⟨(i, j), Finset.mem_product.mpr ⟨hiC, hjC⟩, ?_⟩ haveI : IsProbabilityMeasure Q := hQ calc measureL2Dist Q (fun x => F a.1 x + G a.2 x) (fun x => F i x + G j x) ≤ measureL2Dist Q (F a.1) (F i) + measureL2Dist Q (G a.2) (G j) := measureL2Dist_add_le _ _ _ _ (hF.measurable a.1) (hF.measurable i) (hG.measurable a.2) (hG.measurable j) (hF.envelope a.1) (hF.envelope i) _ < ε * (U + V) := by nlinarith

theorem HasPolynomialL2Cover.mul {ι : Type v} {κ : Type w} {F : ι → 𝒳 → ℝ} {G : κ → 𝒳 → ℝ} {U V : ℝ} (hF : HasPolynomialL2Cover F U) (hG : HasPolynomialL2Cover G V) : HasPolynomialL2Cover (fun p : ι × κ => fun x => F p.1 x * G p.2 x) (U * V) := by have hU : 0 < U := hF.envelope_pos have hV : 0 < V := hG.envelope_pos refine ⟨mul_pos hU hV, fun p => (hF.measurable p.1).mul (hG.measurable p.2), ?_, ?_⟩ · intro p x rw [abs_mul] exact mul_le_mul (hF.envelope p.1 x) (hG.envelope p.2 x) (abs_nonneg _) hU.le · obtain ⟨A, p, hA, hentF⟩ := hF.entropy obtain ⟨B, q, hB, hentG⟩ := hG.entropy refine ⟨8 * A * B, p + q + 2, by nlinarith [mul_nonneg (sub_nonneg.mpr hA) (sub_nonneg.mpr hB)], ?_⟩ intro Q hQ ε hε hε1 have hhalf : 0 < ε / 2 := by positivity have hhalf1 : ε / 2 ≤ 1 := by linarith obtain ⟨CF, hCFcard, hCFcover⟩ := hentF Q hQ (ε / 2) hhalf hhalf1 obtain ⟨CG, hCGcard, hCGcover⟩ := hentG Q hQ (ε / 2) hhalf hhalf1 rw [show A / (ε / 2) = 2 * A / ε by field_simp] at hCFcard rw [show B / (ε / 2) = 2 * B / ε by field_simp] at hCGcard classical refine ⟨CF ×ˢ CG, ?_, ?_⟩ · rw [Finset.card_product] exact (Nat.mul_le_mul hCFcard hCGcard).trans (ceil_mul_le_ceil_poly hA hB hε hε1) · intro z obtain ⟨i, hiC, hi⟩ := hCFcover z.1 obtain ⟨j, hjC, hj⟩ := hCGcover z.2 refine ⟨(i, j), Finset.mem_product.mpr ⟨hiC, hjC⟩, ?_⟩ haveI : IsProbabilityMeasure Q := hQ calc measureL2Dist Q (fun x => F z.1 x * G z.2 x) (fun x => F i x * G j x) ≤ V * measureL2Dist Q (F z.1) (F i) + U * measureL2Dist Q (G z.2) (G j) := measureL2Dist_mul_le _ _ _ _ (hF.measurable z.1) (hF.measurable i) (hG.measurable z.2) (hG.measurable j) hU.le hV.le (hF.envelope z.1) (hF.envelope i) (hG.envelope z.2) (hG.envelope j) _ < ε * (U * V) := by nlinarith

theorem HasPolynomialL2Cover.finSum {K : Type w} [Fintype K] [Nonempty K] {ι : K → Type v} {F : (k : K) → ι k → 𝒳 → ℝ} {U : K → ℝ} (hF : ∀ k, HasPolynomialL2Cover (F k) (U k)) : HasPolynomialL2Cover (fun θ : (k : K) → ι k => fun x => ∑ k, F k (θ k) x) (∑ k, U k) := by classical let P : ∀ (K : Type w) [Fintype K], Prop := fun K _ => Nonempty K → ∀ (ι : K → Type v) (F : (k : K) → ι k → 𝒳 → ℝ) (U : K → ℝ), (∀ k, HasPolynomialL2Cover (F k) (U k)) → HasPolynomialL2Cover (fun θ : (k : K) → ι k => fun x => ∑ k, F k (θ k) x) (∑ k, U k) refine Fintype.induction_empty_option (P := P) ?_ ?_ ?_ K (inferInstance : Nonempty K) ι F U hF · intro α β _ e ih hβ ι F U hF letI : Fintype α := Fintype.ofEquiv β e.symm let hα : Nonempty α := ⟨e.symm (choice hβ)⟩ have hc := ih hα (fun a => ι (e a)) (fun a => F (e a)) (fun a => U (e a)) (fun a => hF (e a)) let eθ : ((b : β) → ι b) ≃ ((a : α) → ι (e a)) := (Equiv.piCongrLeft ι e).symm have hclass : (fun θ : (b : β) → ι b => fun x => ∑ b, F b (θ b) x) = (fun θ : (b : β) → ι b => fun x => ∑ a, F (e a) (θ (e a)) x) := by funext θ x exact (e.sum_comp (fun b => F b (θ b) x)).symm have hUeq : (∑ b, U b) = ∑ a, U (e a) := (e.sum_comp U).symm rw [hclass, hUeq] simpa [eθ] using hc.reindex eθ · intro h exact isEmptyElim (choice h) · intro α _ ih _ ι F U hF by_cases hα : Nonempty α · have htail := ih hα (fun a => ι (some a)) (fun a => F (some a)) (fun a => U (some a)) (fun a => hF (some a)) have hadd := (hF none).add htail let split : ((k : Option α) → ι k) ≃ (ι none × ((a : α) → ι (some a))) := { toFun := fun θ => (θ none, fun a => θ (some a)) invFun := fun p k => Option.rec p.1 p.2 k left_inv := fun θ => by funext k; cases k <;> rfl right_inv := fun p => by cases p; rfl } simp only [Fintype.sum_option] exact hadd.reindex split · letI : IsEmpty α := not_nonempty_iff.mp hα let single : ((k : Option α) → ι k) ≃ ι none := { toFun := fun θ => θ none invFun := fun i k => Option.rec i (fun a => isEmptyElim a) k left_inv := fun θ => by funext k; cases k with | none => rfl | some a => exact isEmptyElim a right_inv := fun i => rfl } simp only [Fintype.sum_option, Finset.univ_eq_empty, Finset.sum_empty, add_zero] exact (hF none).reindex single

theorem HasPolynomialL2Cover.finProd {K : Type w} [Fintype K] [Nonempty K] {ι : K → Type v} {F : (k : K) → ι k → 𝒳 → ℝ} {U : K → ℝ} (hF : ∀ k, HasPolynomialL2Cover (F k) (U k)) : HasPolynomialL2Cover (fun θ : (k : K) → ι k => fun x => ∏ k, F k (θ k) x) (∏ k, U k) := by classical let P : ∀ (K : Type w) [Fintype K], Prop := fun K _ => Nonempty K → ∀ (ι : K → Type v) (F : (k : K) → ι k → 𝒳 → ℝ) (U : K → ℝ), (∀ k, HasPolynomialL2Cover (F k) (U k)) → HasPolynomialL2Cover (fun θ : (k : K) → ι k => fun x => ∏ k, F k (θ k) x) (∏ k, U k) refine Fintype.induction_empty_option (P := P) ?_ ?_ ?_ K (inferInstance : Nonempty K) ι F U hF · intro α β _ e ih hβ ι F U hF letI : Fintype α := Fintype.ofEquiv β e.symm let hα : Nonempty α := ⟨e.symm (choice hβ)⟩ have hc := ih hα (fun a => ι (e a)) (fun a => F (e a)) (fun a => U (e a)) (fun a => hF (e a)) let eθ : ((b : β) → ι b) ≃ ((a : α) → ι (e a)) := (Equiv.piCongrLeft ι e).symm have hclass : (fun θ : (b : β) → ι b => fun x => ∏ b, F b (θ b) x) = (fun θ : (b : β) → ι b => fun x => ∏ a, F (e a) (θ (e a)) x) := by funext θ x exact (e.prod_comp (fun b => F b (θ b) x)).symm have hUeq : (∏ b, U b) = ∏ a, U (e a) := (e.prod_comp U).symm rw [hclass, hUeq] simpa [eθ] using hc.reindex eθ · intro h exact isEmptyElim (choice h) · intro α _ ih _ ι F U hF by_cases hα : Nonempty α · have htail := ih hα (fun a => ι (some a)) (fun a => F (some a)) (fun a => U (some a)) (fun a => hF (some a)) have hmul := (hF none).mul htail let split : ((k : Option α) → ι k) ≃ (ι none × ((a : α) → ι (some a))) := { toFun := fun θ => (θ none, fun a => θ (some a)) invFun := fun p k => Option.rec p.1 p.2 k left_inv := fun θ => by funext k; cases k <;> rfl right_inv := fun p => by cases p; rfl } simp only [Fintype.prod_option] exact hmul.reindex split · letI : IsEmpty α := not_nonempty_iff.mp hα let single : ((k : Option α) → ι k) ≃ ι none := { toFun := fun θ => θ none invFun := fun i k => Option.rec i (fun a => isEmptyElim a) k left_inv := fun θ => by funext k; cases k with | none => rfl | some a => exact isEmptyElim a right_inv := fun i => rfl } simp only [Fintype.prod_option, Finset.univ_eq_empty, Finset.prod_empty, mul_one] exact (hF none).reindex single

theorem HasPolynomialL2CoverWith.forget {ι : Type v} {F : ι → 𝒳 → ℝ} {U A : ℝ} {p : ℕ} (hF : HasPolynomialL2CoverWith F U A p) : HasPolynomialL2Cover F U := hF.toHasPolynomialL2Cover

-- @node: HasPolynomialL2CoverWith.enlargeEnvelope theorem HasPolynomialL2CoverWith.enlargeEnvelope {ι : Type v} {F : ι → 𝒳 → ℝ} {U V A : ℝ} {p : ℕ} (hF : HasPolynomialL2CoverWith F U A p) (hUV : U ≤ V) : HasPolynomialL2CoverWith F V A p := by have hV : 0 < V := hF.forget.envelope_pos.trans_le hUV refine ⟨⟨hV, hF.forget.measurable, fun i x => (hF.forget.envelope i x).trans hUV, A, p, hF.one_le_base, ?_⟩, hF.one_le_base, ?_⟩ <;> intro Q hQ ε hε hε1 · obtain ⟨C, hCcard, hCcover⟩ := hF.entropy Q hQ ε hε hε1 refine ⟨C, hCcard, fun i => ?_⟩ obtain ⟨j, hjC, hij⟩ := hCcover i exact ⟨j, hjC, hij.trans_le (mul_le_mul_of_nonneg_left hUV hε.le)⟩ · obtain ⟨C, hCcard, hCcover⟩ := hF.entropy Q hQ ε hε hε1 refine ⟨C, hCcard, fun i => ?_⟩ obtain ⟨j, hjC, hij⟩ := hCcover i exact ⟨j, hjC, hij.trans_le (mul_le_mul_of_nonneg_left hUV hε.le)⟩

theorem HasPseudoDimAtMost.hasPolynomialL2CoverWith {ι : Type v} [Nonempty ι] {F : ι → 𝒳 → ℝ} {d : ℕ} {U : ℝ} (hpdim : HasPseudoDimAtMost F d) (hmeas : ∀ i, Measurable (F i)) (hU : 0 < U) (henvelope : ∀ i x, |F i x| ≤ U) : HasPolynomialL2CoverWith F U 16 (8 * (d + 1)) := by refine ⟨hpdim.hasPolynomialL2Cover hmeas hU henvelope, by norm_num, ?_⟩ intro Q hQ ε hε hε1 letI : IsProbabilityMeasure Q := hQ simpa only [vcSubgraphCoverBound] using (real_vcSubgraph_l2_covering F d hmeas hpdim hU hε hε1 henvelope Q)

theorem HasPolynomialL2CoverWith.neg {ι : Type v} {F : ι → 𝒳 → ℝ} {U A : ℝ} {p : ℕ} (hF : HasPolynomialL2CoverWith F U A p) : HasPolynomialL2CoverWith (fun i x => -F i x) U A p := by refine ⟨hF.forget.neg, hF.one_le_base, ?_⟩ intro Q hQ ε hε hε1 obtain ⟨C, hCcard, hCcover⟩ := hF.entropy Q hQ ε hε hε1 refine ⟨C, hCcard, ?_⟩ intro i obtain ⟨j, hjC, hij⟩ := hCcover i refine ⟨j, hjC, ?_⟩ have heq : measureL2Dist Q (fun x => -F i x) (fun x => -F j x) = measureL2Dist Q (F i) (F j) := by rw [measureL2Dist_eq_lpNorm Q _ _ (hF.forget.measurable i).fun_neg (hF.forget.measurable j).fun_neg, measureL2Dist_eq_lpNorm Q _ _ (hF.forget.measurable i) (hF.forget.measurable j)] have hfun : (fun x => -F i x - -F j x) = -(fun x => F i x - F j x) := by funext x simp only [Pi.neg_apply] ring rw [hfun, lpNorm_neg] rwa [heq]

theorem HasPolynomialL2CoverWith.add {ι : Type v} {κ : Type w} {F : ι → 𝒳 → ℝ} {G : κ → 𝒳 → ℝ} {U V A B : ℝ} {p q : ℕ} (hF : HasPolynomialL2CoverWith F U A p) (hG : HasPolynomialL2CoverWith G V B q) : HasPolynomialL2CoverWith (fun z : ι × κ => fun x => F z.1 x + G z.2 x) (U + V) (8 * A * B) (p + q + 2) := by have hA := hF.one_le_base have hB := hG.one_le_base have hU := hF.forget.envelope_pos have hV := hG.forget.envelope_pos refine ⟨hF.forget.add hG.forget, by nlinarith [mul_nonneg (sub_nonneg.mpr hA) (sub_nonneg.mpr hB)], ?_⟩ intro Q hQ ε hε hε1 have hhalf : 0 < ε / 2 := by positivity have hhalf1 : ε / 2 ≤ 1 := by linarith obtain ⟨CF, hCFcard, hCFcover⟩ := hF.entropy Q hQ (ε / 2) hhalf hhalf1 obtain ⟨CG, hCGcard, hCGcover⟩ := hG.entropy Q hQ (ε / 2) hhalf hhalf1 rw [show A / (ε / 2) = 2 * A / ε by field_simp] at hCFcard rw [show B / (ε / 2) = 2 * B / ε by field_simp] at hCGcard classical refine ⟨CF ×ˢ CG, ?_, ?_⟩ · rw [Finset.card_product] exact (Nat.mul_le_mul hCFcard hCGcard).trans (ceil_mul_le_ceil_poly hA hB hε hε1) · intro z obtain ⟨i, hiC, hi⟩ := hCFcover z.1 obtain ⟨j, hjC, hj⟩ := hCGcover z.2 refine ⟨(i, j), Finset.mem_product.mpr ⟨hiC, hjC⟩, ?_⟩ haveI : IsProbabilityMeasure Q := hQ calc measureL2Dist Q (fun x => F z.1 x + G z.2 x) (fun x => F i x + G j x) ≤ measureL2Dist Q (F z.1) (F i) + measureL2Dist Q (G z.2) (G j) := measureL2Dist_add_le _ _ _ _ (hF.forget.measurable z.1) (hF.forget.measurable i) (hG.forget.measurable z.2) (hG.forget.measurable j) (hF.forget.envelope z.1) (hF.forget.envelope i) _ < ε * (U + V) := by nlinarith

theorem HasPolynomialL2CoverWith.mul {ι : Type v} {κ : Type w} {F : ι → 𝒳 → ℝ} {G : κ → 𝒳 → ℝ} {U V A B : ℝ} {p q : ℕ} (hF : HasPolynomialL2CoverWith F U A p) (hG : HasPolynomialL2CoverWith G V B q) : HasPolynomialL2CoverWith (fun z : ι × κ => fun x => F z.1 x * G z.2 x) (U * V) (8 * A * B) (p + q + 2) := by have hA := hF.one_le_base have hB := hG.one_le_base have hU := hF.forget.envelope_pos have hV := hG.forget.envelope_pos refine ⟨hF.forget.mul hG.forget, by nlinarith [mul_nonneg (sub_nonneg.mpr hA) (sub_nonneg.mpr hB)], ?_⟩ intro Q hQ ε hε hε1 have hhalf : 0 < ε / 2 := by positivity have hhalf1 : ε / 2 ≤ 1 := by linarith obtain ⟨CF, hCFcard, hCFcover⟩ := hF.entropy Q hQ (ε / 2) hhalf hhalf1 obtain ⟨CG, hCGcard, hCGcover⟩ := hG.entropy Q hQ (ε / 2) hhalf hhalf1 rw [show A / (ε / 2) = 2 * A / ε by field_simp] at hCFcard rw [show B / (ε / 2) = 2 * B / ε by field_simp] at hCGcard classical refine ⟨CF ×ˢ CG, ?_, ?_⟩ · rw [Finset.card_product] exact (Nat.mul_le_mul hCFcard hCGcard).trans (ceil_mul_le_ceil_poly hA hB hε hε1) · intro z obtain ⟨i, hiC, hi⟩ := hCFcover z.1 obtain ⟨j, hjC, hj⟩ := hCGcover z.2 refine ⟨(i, j), Finset.mem_product.mpr ⟨hiC, hjC⟩, ?_⟩ haveI : IsProbabilityMeasure Q := hQ calc measureL2Dist Q (fun x => F z.1 x * G z.2 x) (fun x => F i x * G j x) ≤ V * measureL2Dist Q (F z.1) (F i) + U * measureL2Dist Q (G z.2) (G j) := measureL2Dist_mul_le _ _ _ _ (hF.forget.measurable z.1) (hF.forget.measurable i) (hG.forget.measurable z.2) (hG.forget.measurable j) hF.forget.envelope_pos.le hG.forget.envelope_pos.le (hF.forget.envelope z.1) (hF.forget.envelope i) (hG.forget.envelope z.2) (hG.forget.envelope j) _ < ε * (U * V) := by nlinarith

theorem HasPolynomialL2CoverWith.tightenEnvelopeBy {ι : Type v} {F : ι → 𝒳 → ℝ} {V A c : ℝ} {p : ℕ} (hF : HasPolynomialL2CoverWith F (c * V) A p) (hc : 1 ≤ c) (hV : 0 < V) (hbound : ∀ i x, |F i x| ≤ V) : HasPolynomialL2CoverWith F V (c * A) p := by have hc0 : 0 < c := lt_of_lt_of_le zero_lt_one hc have hbaseOne : 1 ≤ c * A := by simpa only [one_mul] using (mul_le_mul hc hF.one_le_base (by norm_num : (0 : ℝ) ≤ 1) hc0.le) refine ⟨⟨hV, hF.forget.measurable, hbound, c * A, p, hbaseOne, ?_⟩, hbaseOne, ?_⟩ · intro Q hQ ε hε hε1 have hec : 0 < ε / c := div_pos hε hc0 have hec1 : ε / c ≤ 1 := by apply (div_le_one hc0).2 exact hε1.trans hc have hradius : (ε / c) * (c * V) = ε * V := by field_simp have hbase : A / (ε / c) = (c * A) / ε := by field_simp simpa only [hradius, hbase] using hF.entropy Q hQ (ε / c) hec hec1 · intro Q hQ ε hε hε1 have hec : 0 < ε / c := div_pos hε hc0 have hec1 : ε / c ≤ 1 := by apply (div_le_one hc0).2 exact hε1.trans hc have hradius : (ε / c) * (c * V) = ε * V := by field_simp have hbase : A / (ε / c) = (c * A) / ε := by field_simp simpa only [hradius, hbase] using hF.entropy Q hQ (ε / c) hec hec1

theorem HasUniformPolynomialL2CoverOver.neg {S : Type*} {ι : S → Type v} {F : (s : S) → ι s → 𝒳 → ℝ} {U : S → ℝ} (hF : HasUniformPolynomialL2CoverOver S F U) : HasUniformPolynomialL2CoverOver S (fun s i x => -F s i x) U := by obtain ⟨A, p, hF⟩ := hF exact ⟨A, p, fun s => (hF s).neg⟩

theorem HasUniformPolynomialL2CoverOver.add {S : Type*} {ι : S → Type v} {κ : S → Type w} {F : (s : S) → ι s → 𝒳 → ℝ} {G : (s : S) → κ s → 𝒳 → ℝ} {U V : S → ℝ} (hF : HasUniformPolynomialL2CoverOver S F U) (hG : HasUniformPolynomialL2CoverOver S G V) : HasUniformPolynomialL2CoverOver S (fun s (z : ι s × κ s) x => F s z.1 x + G s z.2 x) (fun s => U s + V s) := by obtain ⟨A, p, hF⟩ := hF obtain ⟨B, q, hG⟩ := hG exact ⟨8 * A * B, p + q + 2, fun s => (hF s).add (hG s)⟩

theorem HasUniformPolynomialL2CoverOver.mul {S : Type*} {ι : S → Type v} {κ : S → Type w} {F : (s : S) → ι s → 𝒳 → ℝ} {G : (s : S) → κ s → 𝒳 → ℝ} {U V : S → ℝ} (hF : HasUniformPolynomialL2CoverOver S F U) (hG : HasUniformPolynomialL2CoverOver S G V) : HasUniformPolynomialL2CoverOver S (fun s (z : ι s × κ s) x => F s z.1 x * G s z.2 x) (fun s => U s * V s) := by obtain ⟨A, p, hF⟩ := hF obtain ⟨B, q, hG⟩ := hG exact ⟨8 * A * B, p + q + 2, fun s => (hF s).mul (hG s)⟩

theorem HasUniformPolynomialL2CoverOver.finSum {S : Type*} {K : Type w} [Fintype K] [Nonempty K] {ι : (s : S) → K → Type v} {F : (s : S) → (k : K) → ι s k → 𝒳 → ℝ} {U : S → K → ℝ} (hF : ∀ k, HasUniformPolynomialL2CoverOver S (fun s => F s k) (fun s => U s k)) : HasUniformPolynomialL2CoverOver S (fun s (θ : (k : K) → ι s k) x => ∑ k, F s k (θ k) x) (fun s => ∑ k, U s k) := by classical let P : ∀ (K : Type w) [Fintype K], Prop := fun K _ => Nonempty K → ∀ (ι : (s : S) → K → Type v) (F : (s : S) → (k : K) → ι s k → 𝒳 → ℝ) (U : S → K → ℝ), (∀ k, HasUniformPolynomialL2CoverOver S (fun s => F s k) (fun s => U s k)) → HasUniformPolynomialL2CoverOver S (fun s (θ : (k : K) → ι s k) x => ∑ k, F s k (θ k) x) (fun s => ∑ k, U s k) refine Fintype.induction_empty_option (P := P) ?_ ?_ ?_ K (inferInstance : Nonempty K) ι F U hF · intro α β _ e ih hβ ι F U hF letI : Fintype α := Fintype.ofEquiv β e.symm let hα : Nonempty α := ⟨e.symm (choice hβ)⟩ have hc := ih hα (fun s a => ι s (e a)) (fun s a => F s (e a)) (fun s a => U s (e a)) (fun a => hF (e a)) obtain ⟨A, p, hc⟩ := hc refine ⟨A, p, fun s => ?_⟩ let eθ : ((b : β) → ι s b) ≃ ((a : α) → ι s (e a)) := (Equiv.piCongrLeft (ι s) e).symm have hclass : (fun θ : (b : β) → ι s b => fun x => ∑ b, F s b (θ b) x) = (fun θ : (b : β) → ι s b => fun x => ∑ a, F s (e a) (θ (e a)) x) := by funext θ x exact (e.sum_comp (fun b => F s b (θ b) x)).symm have hUeq : (∑ b, U s b) = ∑ a, U s (e a) := (e.sum_comp (U s)).symm change HasPolynomialL2CoverWith (fun θ : (b : β) → ι s b => fun x => ∑ b, F s b (θ b) x) (∑ b, U s b) A p rw [hclass, hUeq] simpa [eθ] using (hc s).reindex eθ · intro h exact isEmptyElim (choice h) · intro α _ ih _ ι F U hF by_cases hα : Nonempty α · have htail := ih hα (fun s a => ι s (some a)) (fun s a => F s (some a)) (fun s a => U s (some a)) (fun a => hF (some a)) have hadd := (hF none).add htail obtain ⟨A, p, hadd⟩ := hadd refine ⟨A, p, fun s => ?_⟩ let split : ((k : Option α) → ι s k) ≃ (ι s none × ((a : α) → ι s (some a))) := { toFun := fun θ => (θ none, fun a => θ (some a)) invFun := fun z k => Option.rec z.1 z.2 k left_inv := fun θ => by funext k; cases k <;> rfl right_inv := fun z => by cases z; rfl } simp only [Fintype.sum_option] exact (hadd s).reindex split · letI : IsEmpty α := not_nonempty_iff.mp hα obtain ⟨A, p, hone⟩ := hF none refine ⟨A, p, fun s => ?_⟩ let single : ((k : Option α) → ι s k) ≃ ι s none := { toFun := fun θ => θ none invFun := fun i k => Option.rec i (fun a => isEmptyElim a) k left_inv := fun θ => by funext k; cases k with | none => rfl | some a => exact isEmptyElim a right_inv := fun i => rfl } simp only [Fintype.sum_option, Finset.univ_eq_empty, Finset.sum_empty, add_zero] exact (hone s).reindex single

theorem finiteSampleMeasure_isProbabilityMeasure {n : ℕ} (S : Fin n → 𝒳) (hn : 0 < n) : IsProbabilityMeasure (finiteSampleMeasure S) := by refine ⟨?_⟩ simp only [finiteSampleMeasure, Measure.smul_apply, Measure.finset_sum_apply, Measure.dirac_apply_of_mem (Set.mem_univ _), Finset.sum_const, Finset.card_univ, Fintype.card_fin] rw [ENNReal.ofReal_natCast] simpa [nsmul_eq_mul] using ENNReal.inv_mul_cancel (Nat.cast_ne_zero.mpr (Nat.ne_of_gt hn)) (ENNReal.natCast_ne_top n)

theorem integral_finiteSampleMeasure {n : ℕ} (S : Fin n → 𝒳) (hn : 0 < n) {f : 𝒳 → ℝ} (hf : Measurable f) : ∫ x, f x ∂finiteSampleMeasure S = (1 / (n : ℝ)) * ∑ i : Fin n, f (S i) := by rw [finiteSampleMeasure, integral_smul_measure] rw [integral_finset_sum_measure] · simp only [integral_dirac' f _ hf.stronglyMeasurable, ENNReal.toReal_inv, ENNReal.ofReal_natCast, ENNReal.toReal_natCast, smul_eq_mul] rw [one_div] · intro i hi exact integrable_dirac' hf.stronglyMeasurable (by simp)

theorem measureL2Dist_finiteSampleMeasure_eq_empiricalDist {n : ℕ} (S : Fin n → 𝒳) (hn : 0 < n) {f g : 𝒳 → ℝ} (hf : Measurable f) (hg : Measurable g) : measureL2Dist (finiteSampleMeasure S) f g = empiricalDist S f g := by rw [measureL2Dist, empiricalDist, empiricalNorm, integral_finiteSampleMeasure S hn ((hf.fun_sub hg).pow_const 2)] simp only [Pi.sub_apply, one_div]

theorem real_vcSubgraph_empirical_l2_covering [Nonempty ι] {F : ι → 𝒳 → ℝ} {d n : ℕ} (hmeas : ∀ i, Measurable (F i)) (hpdim : HasPseudoDimAtMost F d) {U ε : ℝ} (hU : 0 < U) (hε : 0 < ε) (hε1 : ε ≤ 1) (henvelope : ∀ i x, |F i x| ≤ U) (S : Fin n → 𝒳) (hn : 0 < n) : L2CoveringNumberLe (finiteSampleMeasure S) F (ε * U) (vcSubgraphCoverBound d ε) := by letI : IsProbabilityMeasure (finiteSampleMeasure S) := finiteSampleMeasure_isProbabilityMeasure S hn exact real_vcSubgraph_l2_covering F d hmeas hpdim hU hε hε1 henvelope (finiteSampleMeasure S)

theorem real_vcSubgraph_empirical_totallyBounded [Nonempty ι] {F : ι → 𝒳 → ℝ} {d n : ℕ} (hmeas : ∀ i, Measurable (F i)) (hpdim : HasPseudoDimAtMost F d) {U : ℝ} (hU : 0 < U) (henvelope : ∀ i x, |F i x| ≤ U) (S : Fin n → 𝒳) (hn : 0 < n) : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S)) := by classical rw [Metric.totallyBounded_iff] intro r hr let ε : ℝ := min 1 (r / U) have hε : 0 < ε := lt_min (by norm_num) (div_pos hr hU) have hε1 : ε ≤ 1 := min_le_left _ _ obtain ⟨C, hCcard, hCcover⟩ := real_vcSubgraph_empirical_l2_covering hmeas hpdim hU hε hε1 henvelope S hn let T : Finset (EmpiricalFunctionSpace F S) := C.image fun j => ⟨j⟩ refine ⟨(T : Set (EmpiricalFunctionSpace F S)), T.finite_toSet, ?_⟩ intro q hq obtain ⟨j, hjC, hj⟩ := hCcover q.index have hεU : ε * U ≤ r := by calc ε * U ≤ (r / U) * U := mul_le_mul_of_nonneg_right (min_le_right _ _) (le_of_lt hU) _ = r := by field_simp have hj' : empiricalDist S (F q.index) (F j) < r := by rw [← measureL2Dist_finiteSampleMeasure_eq_empiricalDist S hn (hmeas q.index) (hmeas j)] exact lt_of_lt_of_le hj hεU refine Set.mem_iUnion_of_mem (⟨j⟩ : EmpiricalFunctionSpace F S) ?_ refine Set.mem_iUnion_of_mem ?_ ?_ · exact Finset.mem_coe.mpr (Finset.mem_image.mpr ⟨j, hjC, rfl⟩) · exact hj'

theorem real_vcSubgraph_empirical_coveringNumber_le [Nonempty ι] {F : ι → 𝒳 → ℝ} {d n : ℕ} (hmeas : ∀ i, Measurable (F i)) (hpdim : HasPseudoDimAtMost F d) {U ε : ℝ} (hU : 0 < U) (hε : 0 < ε) (hε1 : ε ≤ 1) (henvelope : ∀ i x, |F i x| ≤ U) (S : Fin n → 𝒳) (hn : 0 < n) : let htot := real_vcSubgraph_empirical_totallyBounded hmeas hpdim hU henvelope S hn coveringNumber htot (ε * U) ≤ vcSubgraphCoverBound d ε := by classical dsimp only let htot := real_vcSubgraph_empirical_totallyBounded hmeas hpdim hU henvelope S hn let r := ε * U have hr : 0 < r := mul_pos hε hU obtain ⟨C, hCcard, hCcover⟩ := real_vcSubgraph_empirical_l2_covering hmeas hpdim hU hε hε1 henvelope S hn let T : Finset (EmpiricalFunctionSpace F S) := C.image fun j => ⟨j⟩ have hTcover : (Set.univ : Set (EmpiricalFunctionSpace F S)) ⊆ ⋃ y ∈ T, ball y r := by intro q hq obtain ⟨j, hjC, hj⟩ := hCcover q.index have hj' : empiricalDist S (F q.index) (F j) < r := by rw [← measureL2Dist_finiteSampleMeasure_eq_empiricalDist S hn (hmeas q.index) (hmeas j)] exact hj refine Set.mem_iUnion_of_mem (⟨j⟩ : EmpiricalFunctionSpace F S) ?_ refine Set.mem_iUnion_of_mem ?_ ?_ · exact Finset.mem_coe.mpr (Finset.mem_image.mpr ⟨j, hjC, rfl⟩) · exact hj' rw [coveringNumber_eq htot hr] calc find (coveringNumber_exists htot hr) ≤ T.card := Nat.find_min' (coveringNumber_exists htot hr) ⟨T, rfl, hTcover⟩ _ ≤ C.card := Finset.card_image_le _ ≤ vcSubgraphCoverBound d ε := hCcard

theorem linearParameterClass_hasPseudoDimAtMost {K : Type w} [Fintype K] (φ : K → 𝒳 → ℝ) (B : ℝ) : HasPseudoDimAtMost (linearParameterClass φ B) (card K + 1) := by classical intro n T unfold vcDim refine Finset.sup_le fun s hs => ?_ rw [Finset.mem_shatterer] at hs by_contra hcard have hcard_lt : card K + 1 < s.card := by omega let v : {i // i ∈ s} → Option K → ℝ := fun i q => match q with | none => -(T i.1).2 | some k => φ k (T i.1).1 have hvdep : ¬ LinearIndependent ℝ v := by intro hv have hle := hv.fintype_card_le_finrank rw [Module.finrank_pi, Fintype.card_option, Fintype.card_coe] at hle omega obtain ⟨a, ha0, i0, hi0⟩ := Fintype.not_linearIndependent_iff.mp hvdep let g : {i // i ∈ s} → ℝ := if 0 < a i0 then a else fun i => -a i have hg0 : ∑ i, g i • v i = 0 := by dsimp [g] split_ifs · exact ha0 · calc ∑ i, (-a i) • v i = ∑ i, -(a i • v i) := by apply Finset.sum_congr rfl intro i _ exact neg_smul (a i) (v i) _ = -(∑ i, a i • v i) := by rw [Finset.sum_neg_distrib] _ = 0 := by rw [ha0, neg_zero] have hgi0 : 0 < g i0 := by dsimp [g] split_ifs with h · exact h · dsimp exact neg_pos.mpr (lt_of_le_of_ne (le_of_not_gt h) hi0) let g0 : Fin n → ℝ := fun i => if hi : i ∈ s then g ⟨i, hi⟩ else 0 let t : Finset (Fin n) := s.filter fun i => 0 < g0 i have hts : t ⊆ s := filter_subset _ _ obtain ⟨u, hu_growth, hsu⟩ := hs hts obtain ⟨θ, hθ⟩ := (mem_growthFamily_iff.mp hu_growth) have hlabel (i : {i // i ∈ s}) : subgraphClassifier (linearParameterClass φ B) θ (T i.1) = true ↔ 0 < g i := by rw [← restrictionPattern_mem_iff (p := subgraphClassifier (linearParameterClass φ B) θ) (S := T) (j := i.1), hθ] have hi_mem : i.1 ∈ u ↔ i.1 ∈ t := by constructor · intro hiu have : i.1 ∈ s ∩ u := Finset.mem_inter.mpr ⟨i.2, hiu⟩ rwa [hsu] at this · intro hit have : i.1 ∈ s ∩ u := by rwa [hsu] exact (Finset.mem_inter.mp this).2 rw [hi_mem] simp only [t, mem_filter, i.2, true_and] simp [g0, i.2] let e : {i // i ∈ s} → ℝ := fun i => linearParameterClass φ B θ (T i.1).1 - (T i.1).2 have he_pos (i : {i // i ∈ s}) (hi : 0 < g i) : 0 < e i := by have hlt : (T i.1).2 < linearParameterClass φ B θ (T i.1).1 := by simpa [subgraphClassifier] using (hlabel i).2 hi dsimp [e] linarith have he_nonpos (i : {i // i ∈ s}) (hi : ¬ 0 < g i) : e i ≤ 0 := by have hnot : ¬ (T i.1).2 < linearParameterClass φ B θ (T i.1).1 := by simpa [subgraphClassifier] using (hlabel i).not.mpr hi dsimp [e] linarith have hprod_nonneg (i : {i // i ∈ s}) : 0 ≤ g i * e i := by by_cases hi : 0 < g i · exact (mul_pos hi (he_pos i hi)).le · have hgle : g i ≤ 0 := le_of_not_gt hi exact mul_nonneg_of_nonpos_of_nonpos hgle (he_nonpos i hi) have hprod_pos : 0 < g i0 * e i0 := mul_pos hgi0 (he_pos i0 hgi0) have hsum_pos : 0 < ∑ i, g i * e i := by exact Finset.sum_pos' (fun i _ => hprod_nonneg i) ⟨i0, Finset.mem_univ _, hprod_pos⟩ have hsum_zero : ∑ i, g i * e i = 0 := by have hcoord (q : Option K) : ∑ i, g i * v i q = 0 := by have := congrFun hg0 q simpa [Pi.smul_apply, smul_eq_mul] using this rw [show (∑ i, g i * e i) = ∑ q : Option K, (match q with | none => 1 | some k => θ.1 k) * ∑ i, g i * v i q by simp_rw [Finset.mul_sum] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro i _ change g i * ((∑ k, θ.1 k * φ k (T i.1).1) - (T i.1).2) = _ rw [mul_sub, Finset.mul_sum] simp only [Fintype.sum_option, v] ring] simp only [hcoord, mul_zero, Finset.sum_const_zero] linarith

-- @node: HasVCAtMost.indicatorClass_hasPseudoDimAtMost theorem HasVCAtMost.indicatorClass_hasPseudoDimAtMost {κ : Type w} (π : κ → 𝒳 → Bool) (d : ℕ) (hπvc : HasVCAtMost π d) : HasPseudoDimAtMost (fun j x => if π j x then 1 else 0) d := by classical intro n T unfold vcDim refine Finset.sup_le fun s hs => ?_ rw [Finset.mem_shatterer] at hs obtain ⟨uTop, huTop, hTop⟩ := hs (Finset.Subset.rfl) obtain ⟨jTop, hjTop⟩ := mem_growthFamily_iff.mp huTop obtain ⟨uBot, huBot, hBot⟩ := hs (empty_subset s) obtain ⟨jBot, hjBot⟩ := mem_growthFamily_iff.mp huBot have hupper (i : Fin n) (hi : i ∈ s) : (T i).2 < 1 := by have hiTop : i ∈ uTop := by have : i ∈ s ∩ uTop := by rwa [hTop] exact (Finset.mem_inter.mp this).2 have htrue : subgraphClassifier (fun j x => if π j x then 1 else 0) jTop (T i) = true := by rw [← restrictionPattern_mem_iff (p := subgraphClassifier (fun j x => if π j x then 1 else 0) jTop) (S := T) (j := i), hjTop] exact hiTop have hlt : (T i).2 < if π jTop (T i).1 then 1 else 0 := by simpa [subgraphClassifier] using htrue cases hπi : π jTop (T i).1 <;> simp [hπi] at hlt ⊢ <;> linarith have hlower (i : Fin n) (hi : i ∈ s) : 0 ≤ (T i).2 := by have hiBot : i ∉ uBot := by intro hiu have : i ∈ s ∩ uBot := Finset.mem_inter.mpr ⟨hi, hiu⟩ rw [hBot] at this exact Finset.notMem_empty i this have hfalse : subgraphClassifier (fun j x => if π j x then 1 else 0) jBot (T i) ≠ true := by intro htrue apply hiBot rw [← hjBot, restrictionPattern_mem_iff] exact htrue have hnot : ¬ (T i).2 < if π jBot (T i).1 then 1 else 0 := by simpa [subgraphClassifier] using hfalse cases hπi : π jBot (T i).1 <;> simp [hπi] at hnot ⊢ <;> linarith have hmiddle (j : κ) (i : Fin n) (hi : i ∈ s) : subgraphClassifier (fun j x => if π j x then 1 else 0) j (T i) = true ↔ π j (T i).1 = true := by cases hπi : π j (T i).1 · simp [subgraphClassifier, hπi, hlower i hi] · simp [subgraphClassifier, hπi, hupper i hi] have hshπ : (growthFamily π (fun i => (T i).1)).Shatters s := by intro t ht obtain ⟨u, hu, hsu⟩ := hs ht obtain ⟨j, hj⟩ := mem_growthFamily_iff.mp hu refine ⟨restrictionPattern (π j) (fun i => (T i).1), ?_, ?_⟩ · rw [mem_growthFamily_iff] exact ⟨j, rfl⟩ · ext i by_cases hi : i ∈ s · have hpiu : i ∈ restrictionPattern (π j) (fun i => (T i).1) ↔ i ∈ u := by rw [restrictionPattern_mem_iff, ← hmiddle j i hi, ← restrictionPattern_mem_iff, hj] have hut : i ∈ u ↔ i ∈ t := by constructor · intro hiu have : i ∈ s ∩ u := Finset.mem_inter.mpr ⟨hi, hiu⟩ rwa [hsu] at this · intro hit have : i ∈ s ∩ u := by rwa [hsu] exact (Finset.mem_inter.mp this).2 simp only [mem_inter, hi, true_and] exact hpiu.trans hut · simp only [mem_inter, hi, false_and] exact (iff_false_intro fun hit => hi (ht hit)).symm exact hshπ.card_le_vcDim.trans (hπvc n fun i => (T i).1)

theorem HasPolynomialL2Cover.mulIndicator {ι : Type v} {κ : Type w} {F : ι → 𝒳 → ℝ} {π : κ → 𝒳 → Bool} {U : ℝ} {d : ℕ} (hF : HasPolynomialL2Cover F U) (hπmeas : ∀ j, MeasurableSet {x | π j x = true}) (hπvc : HasVCAtMost π d) : HasPolynomialL2Cover (fun p : ι × κ => fun x => F p.1 x * if π p.2 x then 1 else 0) U := by rcases isEmpty_or_nonempty κ with hκ | hκ · letI : IsEmpty κ := hκ refine ⟨hF.envelope_pos, ?_, ?_, ?_⟩ · intro p exact isEmptyElim p.2 · intro p exact isEmptyElim p.2 · refine ⟨1, 0, le_rfl, ?_⟩ intro Q hQ ε hε hε1 classical refine ⟨∅, by simp, ?_⟩ intro p exact isEmptyElim p.2 · letI : Nonempty κ := hκ have hindicator : HasPolynomialL2Cover (fun j x => if π j x then 1 else 0) 1 := (HasVCAtMost.indicatorClass_hasPseudoDimAtMost π d hπvc).hasPolynomialL2Cover (fun j => Measurable.ite (hπmeas j) measurable_const measurable_const) (by norm_num) (by intro j x cases π j x <;> simp) simpa using hF.mul hindicator