Stat.Concentration.Covering.Euclidean­Radial­Polynomial

theorem movingCenterClosedBall_hasVCAtMost (d : ℕ) : HasVCAtMost (movingCenterClosedBallClassifier d) (d + 2) := by have h := HasVCAtMost.boolNot (movingCenterExterior_vc d) convert h using 1 funext x zr by_cases hlt : zr.2 < dist zr.1 x · simp [movingCenterClosedBallClassifier, movingCenterBallExteriorClassifier, hlt, not_le_of_gt hlt] · simp [movingCenterClosedBallClassifier, movingCenterBallExteriorClassifier, hlt, le_of_not_gt hlt]

theorem euclideanClosedBall_hasVCAtMost (d : ℕ) : HasVCAtMost (euclideanClosedBallClassifier d) (d + 2) := by have hext : HasVCAtMost (fun cr : ClosedBallParam d => fun z => decide ((cr.2 : ℝ) < dist z cr.1)) (d + 2) := by have h := HasVCAtMost.reindex (linearSignClass_hasVCAtMost (ballLift d)) (ballLiftParameter d) simpa only [Fintype.card_option, Fintype.card_fin, ballExterior_eq_linearSign] using h have h := HasVCAtMost.boolNot hext convert h using 1 funext cr z by_cases hlt : (cr.2 : ℝ) < dist z cr.1 · simp [euclideanClosedBallClassifier, hlt, not_le_of_gt hlt] · simp [euclideanClosedBallClassifier, hlt, le_of_not_gt hlt]

theorem radialAnnulusMonomial_hasPseudoDimAtMost (d k : ℕ) {q a b : ℝ} (hq : 0 < q) (ha : 0 ≤ a) (hab : a ≤ b) : HasPseudoDimAtMost (fun x : EuclideanPoint d => radialAnnulusMonomial d q a b k x) (fixedRadialPseudoDimBound d) := by let f0 : EuclideanPoint d → (EuclideanPoint d × ℝ) → Bool := fun x zt => movingCenterNonstrictExteriorClassifier d x (zt.1, a * q) let f1 : EuclideanPoint d → (EuclideanPoint d × ℝ) → Bool := fun x zt => movingCenterClosedBallClassifier d x (zt.1, b * q) let f2 : EuclideanPoint d → (EuclideanPoint d × ℝ) → Bool := fun x zt => movingCenterBallExteriorClassifier d x (zt.1, radialPowerRadius q k zt.2) let pi : (j : Fin 3) → EuclideanPoint d → (EuclideanPoint d × ℝ) → Bool := fun j => ![f0, f1, f2] j let combine : (EuclideanPoint d × ℝ) → (Fin 3 → Bool) → Bool := fun zt labels => if zt.2 < 0 then true else labels 0 && labels 1 && (if k = 0 then decide (zt.2 < 1) else labels 2) have h0 : HasVCAtMost f0 (d + 2) := by exact HasVCAtMost.compDomain (movingCenterNonstrictExterior_vc d) (fun zt : EuclideanPoint d × ℝ => (zt.1, a * q)) have h1 : HasVCAtMost f1 (d + 2) := by exact HasVCAtMost.compDomain (movingCenterClosedBall_hasVCAtMost d) (fun zt : EuclideanPoint d × ℝ => (zt.1, b * q)) have h2 : HasVCAtMost f2 (d + 2) := by exact HasVCAtMost.compDomain (movingCenterBallExterior_hasVCAtMost d) (fun zt : EuclideanPoint d × ℝ => (zt.1, radialPowerRadius q k zt.2)) have hpi : ∀ j, HasVCAtMost (pi j) (d + 2) := by intro j fin_cases j <;> simp only [pi, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two] <;> assumption have hind := booleanCombination_hasVCAtMost pi hpi combine have hdiag := HasVCAtMost.reindex hind (fun x : EuclideanPoint d => fun _ => x) change HasVCAtMost (subgraphClassifier (fun x : EuclideanPoint d => radialAnnulusMonomial d q a b k x)) (fixedRadialPseudoDimBound d) convert hdiag using 1 case e'_4 => rfl funext x zt by_cases ht : zt.2 < 0 · by_cases hann : a * q ≤ dist zt.1 x ∧ dist zt.1 x ≤ b * q · have hp : 0 ≤ (dist zt.1 x / q) ^ k := pow_nonneg (div_nonneg dist_nonneg hq.le) k have htp : zt.2 < (dist zt.1 x / q) ^ k := lt_of_lt_of_le ht hp simp [subgraphClassifier, radialAnnulusMonomial, combine, pi, f0, f1, f2, movingCenterNonstrictExteriorClassifier, movingCenterClosedBallClassifier, movingCenterBallExteriorClassifier, hann, ht, hp, htp] · simp [subgraphClassifier, radialAnnulusMonomial, combine, pi, f0, f1, f2, movingCenterNonstrictExteriorClassifier, movingCenterClosedBallClassifier, movingCenterBallExteriorClassifier, hann, ht] · have ht0 : 0 ≤ zt.2 := le_of_not_gt ht by_cases hann : a * q ≤ dist zt.1 x ∧ dist zt.1 x ≤ b * q · by_cases hk : k = 0 · subst k simp [subgraphClassifier, radialAnnulusMonomial, combine, pi, f0, f1, f2, movingCenterNonstrictExteriorClassifier, movingCenterClosedBallClassifier, movingCenterBallExteriorClassifier, hann, ht] · have hpow := radialPower_threshold_iff k hq ht0 (dist_nonneg : 0 ≤ dist zt.1 x) hk simp [subgraphClassifier, radialAnnulusMonomial, combine, pi, f0, f1, f2, movingCenterNonstrictExteriorClassifier, movingCenterClosedBallClassifier, movingCenterBallExteriorClassifier, hann, ht, hk, hpow] · have hnot : ¬ zt.2 < 0 := ht simp [subgraphClassifier, radialAnnulusMonomial, combine, pi, f0, f1, f2, movingCenterNonstrictExteriorClassifier, movingCenterClosedBallClassifier, movingCenterBallExteriorClassifier, hann, ht, hnot]

theorem radialAnnulusMonomial_measurable (d k : ℕ) (q a b : ℝ) (x : EuclideanPoint d) : Measurable (radialAnnulusMonomial d q a b k x) := by unfold radialAnnulusMonomial have hd : Measurable (fun z : EuclideanPoint d => dist z x) := measurable_id.dist measurable_const refine Measurable.ite ?_ ((hd.div measurable_const).pow_const k) measurable_const simpa only [Set.setOf_and] using (measurableSet_le measurable_const hd).inter (measurableSet_le hd measurable_const)

theorem abs_radialAnnulusMonomial_le (d p k : ℕ) {q a b : ℝ} (hq : 0 < q) (ha : 0 ≤ a) (hab : a ≤ b) (hk : k ≤ p) (x z : EuclideanPoint d) : |radialAnnulusMonomial d q a b k x z| ≤ radialMonomialEnvelope b p := by rw [radialAnnulusMonomial] split_ifs with h · rw [abs_of_nonneg (pow_nonneg (div_nonneg dist_nonneg hq.le) _)] have hrb : dist z x / q ≤ b := (div_le_iff₀ hq).2 h.2 have hrM : dist z x / q ≤ max 1 b := hrb.trans (le_max_right _ _) have hM : 1 ≤ max 1 b := le_max_left _ _ exact (pow_le_pow_left₀ (div_nonneg dist_nonneg hq.le) hrM k).trans (pow_le_pow_right₀ hM hk) · rw [abs_zero] exact pow_nonneg (le_trans (by norm_num) (le_max_left 1 b)) p

theorem HasPolynomialL2Cover.pullback {𝒳 : Type u} [MeasurableSpace 𝒳] {ι : Type v} {κ : Type w} [Nonempty κ] {F : ι → 𝒳 → ℝ} {U : ℝ} (hF : HasPolynomialL2Cover F U) (e : κ → ι) : HasPolynomialL2Cover (fun k => F (e k)) U := by refine ⟨hF.envelope_pos, fun k => hF.measurable (e k), fun k => hF.envelope (e k), ?_⟩ obtain ⟨A, p, hA, hent⟩ := hF.entropy refine ⟨2 * A, p, by nlinarith, ?_⟩ intro Q hQ ε hε hε1 have hhalf : 0 < ε / 2 := by positivity have hhalf1 : ε / 2 ≤ 1 := by linarith obtain ⟨C, hCcard, hCcover⟩ := hent Q hQ (ε / 2) hhalf hhalf1 classical choose center hcenter_mem hcenter_dist using fun k => hCcover (e k) let occupied : Finset ι := C.filter fun i => ∃ k, center k = i let representative : ι → κ := fun i => if hi : ∃ k, center k = i then choose hi else Classical.choice inferInstance refine ⟨occupied.image representative, ?_, ?_⟩ · calc (occupied.image representative).card ≤ occupied.card := Finset.card_image_le _ ≤ C.card := Finset.card_filter_le _ _ _ ≤ ceil ((A / (ε / 2)) ^ p) := hCcard _ = ceil (((2 * A) / ε) ^ p) := by congr 2 field_simp · intro k have hocc : center k ∈ occupied := by simp only [occupied, mem_filter] exact ⟨hcenter_mem k, ⟨k, rfl⟩⟩ have hrep_center : center (representative (center k)) = center k := by dsimp only [representative] split · next h => exact Classical.choose_spec h · next h => exact (h ⟨k, rfl⟩).elim refine ⟨representative (center k), Finset.mem_image.mpr ⟨center k, hocc, rfl⟩, ?_⟩ letI : IsProbabilityMeasure Q := hQ calc measureL2Dist Q (F (e k)) (F (e (representative (center k)))) ≤ measureL2Dist Q (F (e k)) (F (center k)) + measureL2Dist Q (F (center k)) (F (e (representative (center k)))) := measureL2Dist_triangle' _ _ _ (hF.measurable _) (hF.measurable _) (hF.measurable _) (hF.envelope _) (hF.envelope _) _ = measureL2Dist Q (F (e k)) (F (center k)) + measureL2Dist Q (F (e (representative (center k)))) (F (center k)) := by congr 1 simp only [measureL2Dist] congr 2 funext x ring _ < ε * U := by have hrep_dist : measureL2Dist Q (F (e (representative (center k)))) (F (center k)) < ε / 2 * U := by simpa only [hrep_center] using hcenter_dist (representative (center k)) nlinarith [hcenter_dist k, hrep_dist]

theorem HasPolynomialL2CoverWith.pullback {𝒳 : Type u} [MeasurableSpace 𝒳] {ι : Type v} {κ : Type w} [Nonempty κ] {F : ι → 𝒳 → ℝ} {U A : ℝ} {p : ℕ} (hF : HasPolynomialL2CoverWith F U A p) (e : κ → ι) : HasPolynomialL2CoverWith (fun k => F (e k)) U (2 * A) p := by refine ⟨HasPolynomialL2Cover.pullback hF.forget e, by linarith [hF.one_le_base], ?_⟩ intro Q hQ ε hε hε1 have hhalf : 0 < ε / 2 := by positivity have hhalf1 : ε / 2 ≤ 1 := by linarith obtain ⟨C, hCcard, hCcover⟩ := hF.entropy Q hQ (ε / 2) hhalf hhalf1 classical choose center hcenter_mem hcenter_dist using fun k => hCcover (e k) let occupied : Finset ι := C.filter fun i => ∃ k, center k = i let representative : ι → κ := fun i => if hi : ∃ k, center k = i then choose hi else Classical.choice inferInstance refine ⟨occupied.image representative, ?_, ?_⟩ · calc (occupied.image representative).card ≤ occupied.card := Finset.card_image_le _ ≤ C.card := Finset.card_filter_le _ _ _ ≤ ceil ((A / (ε / 2)) ^ p) := hCcard _ = ceil (((2 * A) / ε) ^ p) := by congr 2 field_simp · intro k have hocc : center k ∈ occupied := by simp only [occupied, mem_filter] exact ⟨hcenter_mem k, ⟨k, rfl⟩⟩ have hrep_center : center (representative (center k)) = center k := by dsimp only [representative] split · next h => exact Classical.choose_spec h · next h => exact (h ⟨k, rfl⟩).elim refine ⟨representative (center k), Finset.mem_image.mpr ⟨center k, hocc, rfl⟩, ?_⟩ letI : IsProbabilityMeasure Q := hQ calc measureL2Dist Q (F (e k)) (F (e (representative (center k)))) ≤ measureL2Dist Q (F (e k)) (F (center k)) + measureL2Dist Q (F (center k)) (F (e (representative (center k)))) := measureL2Dist_triangle' _ _ _ (hF.forget.measurable _) (hF.forget.measurable _) (hF.forget.measurable _) (hF.forget.envelope _) (hF.forget.envelope _) _ = measureL2Dist Q (F (e k)) (F (center k)) + measureL2Dist Q (F (e (representative (center k)))) (F (center k)) := by congr 1 simp only [measureL2Dist] congr 2 funext x ring _ < ε * U := by have hrep_dist : measureL2Dist Q (F (e (representative (center k)))) (F (center k)) < ε / 2 * U := by simpa only [hrep_center] using hcenter_dist (representative (center k)) nlinarith [hcenter_dist k, hrep_dist]

theorem HasUniformPolynomialL2CoverOver.pullback {𝒳 : Type u} [MeasurableSpace 𝒳] {S : Type*} {ι : S → Type v} {κ : S → Type w} {F : (s : S) → ι s → 𝒳 → ℝ} {U : S → ℝ} (hF : HasUniformPolynomialL2CoverOver S F U) (hκ : ∀ s, Nonempty (κ s)) (e : (s : S) → κ s → ι s) : HasUniformPolynomialL2CoverOver S (fun s k => F s (e s k)) U := by obtain ⟨A, p, hF⟩ := hF refine ⟨2 * A, p, fun s => ?_⟩ letI : Nonempty (κ s) := hκ s exact HasPolynomialL2CoverWith.pullback (hF s) (e s)

theorem HasPolynomialL2Cover.monoEnvelope {𝒳 : Type u} [MeasurableSpace 𝒳] {ι : Type v} {F : ι → 𝒳 → ℝ} {U V : ℝ} (hF : HasPolynomialL2Cover F U) (hUV : U ≤ V) : HasPolynomialL2Cover F V := by refine ⟨hF.envelope_pos.trans_le hUV, hF.measurable, fun i x => (hF.envelope i x).trans hUV, ?_⟩ 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 exact ⟨j, hjC, hij.trans_le (mul_le_mul_of_nonneg_left hUV hε.le)⟩

theorem HasPolynomialL2CoverWith.monoEnvelope {𝒳 : Type u} [MeasurableSpace 𝒳] {ι : Type v} {F : ι → 𝒳 → ℝ} {U V A : ℝ} {p : ℕ} (hF : HasPolynomialL2CoverWith F U A p) (hUV : U ≤ V) : HasPolynomialL2CoverWith F V A p := by refine ⟨Causalean.Stat.Concentration.EuclideanRadialPolynomial.HasPolynomialL2Cover.monoEnvelope hF.forget hUV, 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 exact ⟨j, hjC, hij.trans_le (mul_le_mul_of_nonneg_left hUV hε.le)⟩

theorem HasUniformPolynomialL2CoverOver.monoEnvelope {𝒳 : Type u} [MeasurableSpace 𝒳] {S : Type*} {ι : S → Type v} {F : (s : S) → ι s → 𝒳 → ℝ} {U V : S → ℝ} (hF : HasUniformPolynomialL2CoverOver S F U) (hUV : ∀ s, U s ≤ V s) : HasUniformPolynomialL2CoverOver S F V := by obtain ⟨A, p, hF⟩ := hF exact ⟨A, p, fun s => monoEnvelope (hF s) (hUV s)⟩

theorem finiteClass_hasPolynomialL2Cover {𝒳 : Type u} [MeasurableSpace 𝒳] {ι : Type v} [Fintype ι] (F : ι → 𝒳 → ℝ) {U : ℝ} (hU : 0 < U) (hmeas : ∀ i, Measurable (F i)) (hbound : ∀ i x, |F i x| ≤ U) : HasPolynomialL2Cover F U := by refine ⟨hU, hmeas, hbound, max 1 (Fintype.card ι : ℝ), 1, le_max_left _ _, ?_⟩ intro Q hQ ε hε hε1 classical refine ⟨Finset.univ, ?_, ?_⟩ · rw [Finset.card_univ] have hA0 : 0 ≤ max 1 (Fintype.card ι : ℝ) := (by norm_num : (0 : ℝ) ≤ 1).trans (le_max_left _ _) have hreal : (Fintype.card ι : ℝ) ≤ max 1 (Fintype.card ι : ℝ) / ε := by calc (Fintype.card ι : ℝ) ≤ max 1 (Fintype.card ι : ℝ) := le_max_right _ _ _ ≤ max 1 (Fintype.card ι : ℝ) / ε := by apply (le_div_iff₀ hε).2 nlinarith [mul_nonneg hA0 (sub_nonneg.mpr hε1)] have hnat : Fintype.card ι ≤ ceil (max 1 (Fintype.card ι : ℝ) / ε) := by exact_mod_cast hreal.trans (Nat.le_ceil (max 1 (Fintype.card ι : ℝ) / ε)) simpa using hnat · intro i refine ⟨i, Finset.mem_univ _, ?_⟩ simp [measureL2Dist, mul_pos hε hU]

theorem finiteClass_hasPolynomialL2CoverWith {𝒳 : Type u} [MeasurableSpace 𝒳] {ι : Type v} [Fintype ι] (F : ι → 𝒳 → ℝ) {U : ℝ} (hU : 0 < U) (hmeas : ∀ i, Measurable (F i)) (hbound : ∀ i x, |F i x| ≤ U) : HasPolynomialL2CoverWith F U (max 1 (Fintype.card ι : ℝ)) 1 := by refine ⟨finiteClass_hasPolynomialL2Cover F hU hmeas hbound, le_max_left _ _, ?_⟩ intro Q hQ ε hε hε1 classical refine ⟨Finset.univ, ?_, ?_⟩ · rw [Finset.card_univ] have hA0 : 0 ≤ max 1 (Fintype.card ι : ℝ) := (by norm_num : (0 : ℝ) ≤ 1).trans (le_max_left _ _) have hreal : (Fintype.card ι : ℝ) ≤ max 1 (Fintype.card ι : ℝ) / ε := by calc (Fintype.card ι : ℝ) ≤ max 1 (Fintype.card ι : ℝ) := le_max_right _ _ _ ≤ max 1 (Fintype.card ι : ℝ) / ε := by apply (le_div_iff₀ hε).2 nlinarith [mul_nonneg hA0 (sub_nonneg.mpr hε1)] have hnat : Fintype.card ι ≤ ceil (max 1 (Fintype.card ι : ℝ) / ε) := by exact_mod_cast hreal.trans (Nat.le_ceil (max 1 (Fintype.card ι : ℝ) / ε)) simpa using hnat · intro i refine ⟨i, Finset.mem_univ _, ?_⟩ simp [measureL2Dist, mul_pos hε hU]

theorem radialMonomialClass_hasPolynomialL2Cover (d p : ℕ) {q a b : ℝ} (hq : 0 < q) (ha : 0 ≤ a) (hab : a ≤ b) : HasPolynomialL2Cover (radialMonomialClass d p q a b) (radialMonomialEnvelope b p) := by apply (radialMonomialClass_hasPseudoDimAtMost d p hq ha hab).hasPolynomialL2Cover · intro θ exact radialAnnulusMonomial_measurable d θ.2.1 q a b θ.1 · unfold radialMonomialEnvelope positivity · intro θ z apply abs_radialAnnulusMonomial_le d p θ.2.1 hq ha hab exact Nat.le_of_lt_succ θ.2.2

theorem radialAnnulusMonomial_hasPolynomialL2Cover (d p k : ℕ) {q a b : ℝ} (hq : 0 < q) (ha : 0 ≤ a) (hab : a ≤ b) (hk : k ≤ p) : HasPolynomialL2Cover (fun x : EuclideanPoint d => radialAnnulusMonomial d q a b k x) (radialMonomialEnvelope b p) := by let degree : Fin (p + 1) := ⟨k, Nat.lt_succ_iff.mpr hk⟩ exact HasPolynomialL2Cover.pullback (radialMonomialClass_hasPolynomialL2Cover d p hq ha hab) (fun x : EuclideanPoint d => (x, degree))

theorem radialMonomialOn_hasPolynomialL2CoverWith {Ω : Type u} [MeasurableSpace Ω] (d p : ℕ) (loc : Ω → EuclideanPoint d) {q a b : ℝ} (hloc : Measurable loc) (hq : 0 < q) (ha : 0 ≤ a) (hab : a ≤ b) : HasPolynomialL2CoverWith (radialMonomialOn d p loc q a b) (radialMonomialEnvelope b p) 16 (8 * (radialPseudoDimBound d p + 1)) := by apply (HasPseudoDimAtMost.compDomain (radialMonomialClass_hasPseudoDimAtMost d p hq ha hab) loc).hasPolynomialL2CoverWith · intro θ exact (radialAnnulusMonomial_measurable d θ.2.1 q a b θ.1).comp hloc · unfold radialMonomialEnvelope positivity · intro θ ω apply abs_radialAnnulusMonomial_le d p θ.2.1 hq ha hab exact Nat.le_of_lt_succ θ.2.2

theorem finiteSignedArmRadial_hasPolynomialL2Cover {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [Fintype A] (d p : ℕ) (loc : Ω → EuclideanPoint d) (arm : A → Ω → ℝ) {q a b : ℝ} (hloc : Measurable loc) (harmMeas : ∀ s, Measurable (arm s)) (harmBound : ∀ s ω, |arm s ω| ≤ 1) (hq : 0 < q) (ha : 0 ≤ a) (hab : a ≤ b) : HasPolynomialL2Cover (fun θ : RadialMonomialParam d p × A => fun ω => radialMonomialOn d p loc q a b θ.1 ω * arm θ.2 ω) (radialMonomialEnvelope b p) := by classical have hU : 0 < radialMonomialEnvelope b p := by unfold radialMonomialEnvelope positivity cases isEmpty_or_nonempty A with | inl hA => letI : IsEmpty A := hA refine ⟨hU, ?_, ?_, ?_⟩ · intro θ exact isEmptyElim θ.2 · intro θ exact isEmptyElim θ.2 · refine ⟨1, 0, le_rfl, ?_⟩ intro Q hQ ε hε hε1 refine ⟨∅, by simp, ?_⟩ intro θ exact isEmptyElim θ.2 | inr hA => letI : Nonempty A := hA have hrad := radialMonomialOn_hasPolynomialL2Cover d p loc hloc hq ha hab have harm : HasPolynomialL2Cover arm 1 := finiteClass_hasPolynomialL2Cover arm (by norm_num) harmMeas harmBound simpa using hrad.mul harm

theorem abs_boundedRadialPolynomial_le (d p : ℕ) {q a b B : ℝ} (hq : 0 < q) (ha : 0 ≤ a) (hab : a ≤ b) (hB : 0 ≤ B) (x : EuclideanPoint d) (β : CoeffBox (Fin (p + 1)) B) (z : EuclideanPoint d) : |boundedRadialPolynomial d p q a b B x β z| ≤ radialPolynomialEnvelope b p B := by classical calc |boundedRadialPolynomial d p q a b B x β z| ≤ ∑ k : Fin (p + 1), |β.1 k * radialAnnulusMonomial d q a b k.1 x z| := by exact Finset.abs_sum_le_sum_abs _ _ _ = ∑ k : Fin (p + 1), |β.1 k| * |radialAnnulusMonomial d q a b k.1 x z| := by apply Finset.sum_congr rfl intro k _ rw [abs_mul] _ ≤ ∑ _k : Fin (p + 1), B * radialMonomialEnvelope b p := by exact Finset.sum_le_sum fun k _ => mul_le_mul (β.2 k) (abs_radialAnnulusMonomial_le d p k.1 hq ha hab (Nat.le_of_lt_succ k.2) x z) (abs_nonneg _) hB _ = radialPolynomialEnvelope b p B := by simp [radialPolynomialEnvelope] ring

theorem boundedRadialPolynomialOn_hasPolynomialL2Cover {Ω : Type u} [MeasurableSpace Ω] (d p : ℕ) (loc : Ω → EuclideanPoint d) {q a b B : ℝ} (hloc : Measurable loc) (hq : 0 < q) (ha : 0 ≤ a) (hab : a ≤ b) (hB : 0 < B) : HasPolynomialL2Cover (boundedRadialPolynomialOn d p loc q a b B) (radialPolynomialEnvelope b p B) := by classical let M := radialMonomialEnvelope b p have hM : 0 < M := by dsimp [M, radialMonomialEnvelope] positivity letI : Nonempty (CoeffBox (Fin (p + 1)) B) := ⟨⟨fun _ => 0, fun _ => by simpa using hB.le⟩⟩ have hcoeff (k : Fin (p + 1)) : HasPolynomialL2Cover (fun β : CoeffBox (Fin (p + 1)) B => fun _ω : Ω => β.1 k) B := by have hbase := linearParameterClass_hasPolynomialL2Cover (𝒳 := Ω) (K := Fin 1) (B := B) (M := 1) (fun _ _ => (1 : ℝ)) hB (by norm_num) (fun _ => measurable_const) (fun _ _ => by norm_num) have hpull := pullback hbase (fun β : CoeffBox (Fin (p + 1)) B => (⟨fun _ : Fin 1 => β.1 k, fun _ => β.2 k⟩ : CoeffBox (Fin 1) B)) convert hpull using 1 · funext β ω simp [linearParameterClass] · simp have hradial (k : Fin (p + 1)) : HasPolynomialL2Cover (fun x : EuclideanPoint d => fun ω => radialAnnulusMonomial d q a b k.1 x (loc ω)) M := by have hfull := radialMonomialOn_hasPolynomialL2Cover d p loc hloc hq ha hab have hpull := pullback hfull (fun x : EuclideanPoint d => (x, k)) exact hpull have hterm (k : Fin (p + 1)) : HasPolynomialL2Cover (fun t : CoeffBox (Fin (p + 1)) B × EuclideanPoint d => fun ω => t.1.1 k * radialAnnulusMonomial d q a b k.1 t.2 (loc ω)) (B * M) := by exact (hcoeff k).mul (hradial k) have hsum := HasPolynomialL2Cover.finSum hterm have hpull := pullback hsum (fun θ : RadialPolynomialParam d p B => fun k => (θ.2, θ.1)) change HasPolynomialL2Cover (fun θ : RadialPolynomialParam d p B => fun ω => ∑ k : Fin (p + 1), θ.2.1 k * radialAnnulusMonomial d q a b k.1 θ.1 (loc ω)) (((p + 1 : ℕ) : ℝ) * B * M) simpa only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, Nat.cast_add, cast_one, mul_assoc] using hpull

theorem radialResidualScore_hasUniformPolynomialL2CoverWith {Ω : Type u} [MeasurableSpace Ω] {A : Type v} [Fintype A] [Nonempty A] (d p : ℕ) : ∃ C : ℝ, ∃ n : ℕ, ∀ (loc : Ω → EuclideanPoint d) (arm : A → Ω → ℝ) (response : Ω → ℝ) {q a b B R : ℝ}, Measurable loc → (∀ s, Measurable (arm s)) → (∀ s ω, |arm s ω| ≤ 1) → Measurable response → (∀ ω, |response ω| ≤ R) → 0 < q → 0 ≤ a → a ≤ b → 0 < B → 0 < R → HasPolynomialL2CoverWith (fun θ : RadialResidualScoreParam d p B A × Fin (p + 1) => radialResidualScore d p loc arm response q a b B θ.2 θ.1) (radialResidualScoreEnvelope b p B R) C n := by classical let S := RadialResidualCoverData Ω A d p let M : S → ℝ := fun s => radialMonomialEnvelope s.b p let P : S → ℝ := fun s => radialPolynomialEnvelope s.b p s.B have hcoeff (k : Fin (p + 1)) : HasUniformPolynomialL2CoverOver S (fun s (β : CoeffBox (Fin (p + 1)) s.B) (_ω : Ω) => β.1 k) (fun s => s.B) := by refine ⟨32, 24, fun s => ?_⟩ letI : Nonempty (CoeffBox (Fin 1) s.B) := ⟨⟨fun _ => 0, fun _ => by simpa using s.B_pos.le⟩⟩ letI : Nonempty (CoeffBox (Fin (p + 1)) s.B) := ⟨⟨fun _ => 0, fun _ => by simpa using s.B_pos.le⟩⟩ have hbase := (linearParameterClass_hasPseudoDimAtMost (𝒳 := Ω) (K := Fin 1) (fun _ _ => (1 : ℝ)) s.B).hasPolynomialL2CoverWith (fun _ => measurable_const) (by simpa using s.B_pos) (fun θ ω => by simp [linearParameterClass] exact θ.2 0) have hpull := HasPolynomialL2CoverWith.pullback hbase (fun β : CoeffBox (Fin (p + 1)) s.B => (⟨fun _ : Fin 1 => β.1 k, fun _ => β.2 k⟩ : CoeffBox (Fin 1) s.B)) convert hpull using 1 · funext β ω simp [linearParameterClass] · norm_num · simp have hradial : HasUniformPolynomialL2CoverOver S (fun s (x : EuclideanPoint d × Fin (p + 1)) ω => radialAnnulusMonomial d s.q s.a s.b x.2.1 x.1 (s.loc ω)) M := by refine ⟨16, 8 * (radialPseudoDimBound d p + 1), fun s => ?_⟩ exact radialMonomialOn_hasPolynomialL2CoverWith d p s.loc s.loc_measurable s.q_pos s.a_nonneg s.ab have hradialDegree (k : Fin (p + 1)) : HasUniformPolynomialL2CoverOver S (fun s (x : EuclideanPoint d) ω => radialAnnulusMonomial d s.q s.a s.b k.1 x (s.loc ω)) M := by exact pullback hradial (fun _ => inferInstance) (fun _ x => (x, k)) have hterm (k : Fin (p + 1)) : HasUniformPolynomialL2CoverOver S (fun s (t : CoeffBox (Fin (p + 1)) s.B × EuclideanPoint d) ω => t.1.1 k * radialAnnulusMonomial d s.q s.a s.b k.1 t.2 (s.loc ω)) (fun s => s.B * M s) := (hcoeff k).mul (hradialDegree k) have hsum := HasUniformPolynomialL2CoverOver.finSum hterm have hpoly : HasUniformPolynomialL2CoverOver S (fun s (θ : RadialPolynomialParam d p s.B) ω => boundedRadialPolynomial d p s.q s.a s.b s.B θ.1 θ.2 (s.loc ω)) P := by have hpull := pullback hsum (fun s => ⟨(0, ⟨fun _ => 0, fun _ => by simpa using s.B_pos.le⟩)⟩) (fun s (θ : RadialPolynomialParam d p s.B) k => (θ.2, θ.1)) simpa only [boundedRadialPolynomial, P, M, radialPolynomialEnvelope, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, Nat.cast_add, cast_one, mul_assoc] using hpull have harm : HasUniformPolynomialL2CoverOver S (fun s => s.arm) (fun _ => 1) := by refine ⟨max 1 (Fintype.card A : ℝ), 1, fun s => ?_⟩ exact finiteClass_hasPolynomialL2CoverWith s.arm (by norm_num) s.arm_measurable s.arm_bound have hresponse : HasUniformPolynomialL2CoverOver S (fun s (_ : Unit) => s.response) (fun s => s.R) := by refine ⟨1, 1, fun s => ?_⟩ simpa using finiteClass_hasPolynomialL2CoverWith (fun _ : Unit => s.response) s.R_pos (fun _ => s.response_measurable) (fun _ => s.response_bound) have harmLeading := harm.mul hradial have hresidual := hresponse.add hpoly.neg have hsuper := harmLeading.mul hresidual have hpull := pullback hsuper (fun s => ⟨((0, ⟨fun _ => 0, fun _ => by simpa using s.B_pos.le⟩), Classical.choice inferInstance), 0⟩) (fun s (θ : RadialResidualScoreParam d p s.B A × Fin (p + 1)) => ((θ.1.2, (θ.1.1.1, θ.2)), ((), θ.1.1))) obtain ⟨C, n, hpull⟩ := hpull refine ⟨C, n, ?_⟩ intro loc arm response q a b B R hloc harmMeas harmBound hresponseMeas hresponseBound hq ha hab hB hR let s : S := { loc := loc arm := arm response := response q := q a := a b := b B := B R := R loc_measurable := hloc arm_measurable := harmMeas arm_bound := harmBound response_measurable := hresponseMeas response_bound := hresponseBound q_pos := hq a_nonneg := ha ab := hab B_pos := hB R_pos := hR } have hs := hpull s simp only [one_mul] at hs exact hs

theorem HasVCAtMost.reindex {ι : Type v} {κ : Type w} {π : ι → 𝒳 → Bool} {d : ℕ} (hπ : HasVCAtMost π d) (e : κ → ι) : HasVCAtMost (fun k => π (e k)) d := by intro n S apply (Finset.vcDim_mono (ℬ := growthFamily π S) ?_).trans (hπ n S) intro A hA rw [mem_growthFamily_iff] at hA ⊢ obtain ⟨k, rfl⟩ := hA exact ⟨e k, rfl⟩

theorem HasVCAtMost.compDomain {ι : Type v} {𝒴 : Type w} {π : ι → 𝒳 → Bool} {d : ℕ} (hπ : HasVCAtMost π d) (g : 𝒴 → 𝒳) : HasVCAtMost (fun i y => π i (g y)) d := by intro n S exact hπ n (fun j => g (S j))

theorem HasPseudoDimAtMost.reindex {ι : Type v} {κ : Type w} {F : ι → 𝒳 → ℝ} {d : ℕ} (hF : HasPseudoDimAtMost F d) (e : κ → ι) : HasPseudoDimAtMost (fun k => F (e k)) d := by intro n T apply (Finset.vcDim_mono (ℬ := growthFamily (subgraphClassifier F) T) ?_).trans (hF n T) intro A hA rw [mem_growthFamily_iff] at hA ⊢ obtain ⟨k, rfl⟩ := hA exact ⟨e k, rfl⟩

theorem HasPseudoDimAtMost.compDomain {ι : Type v} {𝒴 : Type w} {F : ι → 𝒳 → ℝ} {d : ℕ} (hF : HasPseudoDimAtMost F d) (g : 𝒴 → 𝒳) : HasPseudoDimAtMost (fun i y => F i (g y)) d := by intro n T exact hF n (fun j => (g (T j).1, (T j).2))

theorem linearSignClass_hasVCAtMost {K : Type v} [Fintype K] (φ : K → 𝒳 → ℝ) : HasVCAtMost (linearSignClass φ) (card K) := by classical intro n S unfold vcDim refine Finset.sup_le fun s hs => ?_ rw [Finset.mem_shatterer] at hs by_contra hcard have hcard_lt : card K < s.card := by omega let v : {i // i ∈ s} → K → ℝ := fun i k => φ k (S i.1) have hvdep : ¬ LinearIndependent ℝ v := by intro hv have hle := hv.fintype_card_le_finrank rw [Module.finrank_pi, 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 · 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}) : linearSignClass φ θ (S i.1) = true ↔ 0 < g i := by rw [← restrictionPattern_mem_iff (p := linearSignClass φ θ) (S := S) (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 => ∑ k, θ k * φ k (S i.1) have he_pos (i : {i // i ∈ s}) (hi : 0 < g i) : 0 < e i := by simpa [linearSignClass, e] using (hlabel i).2 hi have he_nonpos (i : {i // i ∈ s}) (hi : ¬ 0 < g i) : e i ≤ 0 := by have hfalse : linearSignClass φ θ (S i.1) ≠ true := (hlabel i).not.mpr hi simpa [linearSignClass, e] using hfalse 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 · exact mul_nonneg_of_nonpos_of_nonpos (le_of_not_gt hi) (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 := 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 (k : K) : ∑ i, g i * v i k = 0 := by have := congrFun hg0 k simpa [Pi.smul_apply, smul_eq_mul] using this simp_rw [e, Finset.mul_sum] rw [Finset.sum_comm] apply Finset.sum_eq_zero intro k _ rw [show (∑ i, g i * (θ k * φ k (S i.1))) = θ k * ∑ i, g i * v i k by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i _ dsimp [v] ring] rw [hcoord, mul_zero] linarith

theorem finiteUnion_hasVCAtMost {K : Type v} [Fintype K] {ι : K → Type w} {d : ℕ} (π : (k : K) → ι k → 𝒳 → Bool) (hπ : ∀ k, HasVCAtMost (π k) d) : HasVCAtMost (fun θ : Sigma ι => π θ.1 θ.2) (finiteUnionVCBound (card K) d) := by simpa only [finiteUnionVCBound] using hasVCAtMost_of_growth_card_le (fun θ : Sigma ι => π θ.1 θ.2) (card K * (d + 1)) (fun n S => finiteUnion_growth_card_le (n := n) π hπ S)