Stat.Concentration.Covering.EuclideanRadialPolynomial
This barrel exports finite-trace pseudo-dimension bounds and uniform polynomial L² covering certificates for compactly supported radial monomials with a moving finite-dimensional Euclidean center.
Geometry 12 core · 4 supporting This module defines compactly supported radial monomials with a moving center and proves finite-trace VC-subgraph bounds. ★ radialMonomialClass_hasPseudoDimAtMost
Euclidean radial monomials and their finite traces
This module defines compactly supported radial monomials with a moving center and proves finite-trace VC-subgraph bounds. The bounds are intentionally non-optimized. Their important features are that they depend only on the Euclidean dimension and the finite degree cutoff, and that they are stated at the trace level, without any assumption on an ambient probability measure.
Odd and even degrees are treated uniformly. On a nonnegative radial ray, every positive integral power is monotone, so a threshold on a radial power is again a distance threshold. Squared Euclidean distance then supplies the finite-dimensional affine lift used by the trace argument.
abbrev EuclideanPoint reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, the Euclidean point space is the real Euclidean space of that dimension.
Definition (Lean source)
abbrev RadiusPoint reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, the point-radius space is the set of pairs consisting of a point in the corresponding real Euclidean space and an arbitrary real radius threshold.
Definition (Lean source)
def movingCenterClosedBallClassifier reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, a center point, and a point together with a radius threshold, the moving-center closed-ball classifier returns true exactly when the point lies at distance no greater than the threshold from the center.
Definition (Lean source)
parameters
def
def movingCenterBallExteriorClassifier reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, a center point, and a point together with a radius threshold, the moving-center exterior classifier returns true exactly when the point lies at distance strictly greater than the threshold from the center.
Definition (Lean source)
parameters
def
abbrev ClosedBallParam reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, the closed-ball parameter space is the set of pairs consisting of a point in that real Euclidean space and a nonnegative real radius.
Definition (Lean source)
def euclideanClosedBallClassifier reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, a closed-ball parameter, and a point in the corresponding Euclidean space, the closed-ball classifier returns true exactly when the point lies in the closed ball specified by that parameter.
Definition (Lean source)
parameters
def
def radialAnnulusMonomial reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, a bandwidth, two relative annulus endpoints, a natural-number degree, a center point, and an evaluation point, the radial annulus monomial equals when the distance from the evaluation point to the center lies between and , inclusive, and equals zero otherwise.
Definition (Lean source)
parameters
def
radialAnnulusMonomial d q a b k x z :
ℝ
abbrev RadialMonomialParam reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension and a maximal natural-number degree, the radial-monomial parameter space consists of a center in that Euclidean space paired with a degree from zero through .
Definition (Lean source)
def radialMonomialClass reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, a maximal degree, a bandwidth and two relative annulus endpoints, a center-and-degree parameter, and a Euclidean evaluation point, the radial-monomial class maps that parameter and point to the corresponding radial annulus monomial.
Definition (Lean source)
parameters
def
radialMonomialClass d p q a b θ z :
ℝ
given by
radialAnnulusMonomial d q a b θ.2.1 θ.1 z
def fixedRadialPseudoDimBound reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, the fixed-degree radial pseudo-dimension bound is the explicit Boolean-combination bound .
Definition (Lean source)
def radialPseudoDimBound reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension and a maximal degree, the radial pseudo-dimension bound is the explicit finite-union bound obtained by combining fixed-degree bounds.
Definition (Lean source)
parameters
d p :
ℕ
def
radialPseudoDimBound d p :
ℕ
given by
finiteUnionVCBound (p + 1) (fixedRadialPseudoDimBound d)
theorem radialMonomialClass_hasPseudoDimAtMost reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Pseudo-dimension bound for the moving-center radial-monomial class. For a positive bandwidth q, a nonnegative annulus inner radius a, and inner radius at most outer radius b, allowing both the Euclidean center and the monomial degree — ranging from zero through p — to vary gives the radial-monomial class a pseudo-dimension of at most radialPseudoDimBound d p.
Formal statement
hypotheses
d p :
ℕ
q a b :
ℝ
hq :
0 < q
ha :
0 ≤ a
hab :
a ≤ b
conclusion
Proof (Lean source)
theorem radialMonomialClass_hasPseudoDimAtMost
(d p : ℕ) {q a b : ℝ}
(hq : 0 < q) (ha : 0 ≤ a) (hab : a ≤ b) :
HasPseudoDimAtMost (radialMonomialClass d p q a b)
(radialPseudoDimBound d p) := by
let pi : (j : Fin (p + 1)) → EuclideanPoint d →
(EuclideanPoint d × ℝ) → Bool := fun j =>
subgraphClassifier
(fun x : EuclideanPoint d => radialAnnulusMonomial d q a b j.1 x)
have hpi : ∀ j, HasVCAtMost (pi j) (fixedRadialPseudoDimBound d) := by
intro j
exact radialAnnulusMonomial_hasPseudoDimAtMost d j.1 hq ha hab
have hu := finiteUnion_hasVCAtMost pi hpi
have hr := HasVCAtMost.reindex hu
(fun theta : RadialMonomialParam d p =>
(Sigma.mk theta.2 theta.1 : Sigma fun _ : Fin (p + 1) => EuclideanPoint d))
change HasVCAtMost (subgraphClassifier (radialMonomialClass d p q a b))
(radialPseudoDimBound d p)
simp only [radialPseudoDimBound, Fintype.card_fin, pi, radialMonomialClass] at hr ⊢
exact hr
4 supporting declarations (lemmas, instances)
-
movingCenterClosedBall_hasVCAtMosttheorem — Variable-radius closed-ball tests indexed by a moving Euclidean center have VC dimension at most d + 2.Proof (Lean source)
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] -
movingCenterBallExterior_hasVCAtMosttheorem — Variable-radius strict-exterior tests indexed by a moving Euclidean center have VC dimension at most d + 2.Proof (Lean source)
theorem movingCenterBallExterior_hasVCAtMost (d : ℕ) : HasVCAtMost (movingCenterBallExteriorClassifier d) (d + 2) := by exact movingCenterExterior_vc d -
euclideanClosedBall_hasVCAtMosttheorem — Closed balls in d-dimensional Euclidean space have VC dimension at most d + 2. This neutral Causalean-only statement replaces the paper-local planar ball lemma with a finite-dimensional bound.Proof (Lean source)
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] -
radialAnnulusMonomial_hasPseudoDimAtMosttheorem — For every positive bandwidth and ordered nonnegative annulus, the class of fixed-degree radial monomials with moving center has pseudo-dimension bounded solely by the Euclidean dimension.hypothesesd k :ℕq a b :ℝhq :0 < qha :0 ≤ ahab :a ≤ bconclusionHasPseudoDimAtMost (fun x : EuclideanPoint d => radialAnnulusMonomial d q a b k x) (fixedRadialPseudoDimBound d)Proof (Lean source)
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]
Cover 3 core · 14 supporting This module converts the finite-trace pseudo-dimension certificate into a uniform polynomial L²(Q) covering certificate. ★ radialMonomialOn_hasPolynomialL2Cover
Uniform polynomial covers for radial monomials
This module converts the finite-trace pseudo-dimension certificate into a
uniform polynomial L²(Q) covering certificate. The measure Q remains
arbitrary throughout, so atoms on moving annulus boundaries are included.
It also supplies two general assembly tools: pullback of a covering class along an arbitrary nonempty parameter map (using internal representatives at twice the preliminary radius), and the covering certificate for any bounded finite class. These tools let later score constructions reuse the existing sum and product closure lemmas.
def radialMonomialEnvelope reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
For an upper relative radius and a nonnegative integer , the radial-monomial envelope is .
Definition (Lean source)
def radialMonomialOn reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given an observation space , a Euclidean dimension , a maximum degree , a location map from observations to -dimensional Euclidean space, a bandwidth , annulus radii and , a radial-monomial parameter θ, and an observation , the radial monomial evaluated at that observation is the corresponding radial-monomial class function evaluated at the mapped location.
Definition (Lean source)
parameters
def
radialMonomialOn d p loc q a b θ ω :
ℝ
given by
radialMonomialClass d p q a b θ (loc ω)
theorem radialMonomialOn_hasPolynomialL2Cover reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Covering certificate transported through a location map. For a measurable map from the underlying observation space into d-dimensional Euclidean space, given a positive bandwidth q, a nonnegative annulus inner radius a, and inner radius at most outer radius b, composing the moving-center radial-monomial class of degree at most p with the location map still carries a uniform polynomial L² covering certificate at envelope radialMonomialEnvelope b p.
Formal statement
hypotheses
Ω :
Type u
d p :
ℕ
loc :
Ω → EuclideanPoint d
q a b :
ℝ
hloc :
Measurable loc
hq :
0 < q
ha :
0 ≤ a
hab :
a ≤ b
conclusion
Proof (Lean source)
theorem radialMonomialOn_hasPolynomialL2Cover
{Ω : Type u} [MeasurableSpace Ω]
(d p : ℕ) (loc : Ω → EuclideanPoint d) {q a b : ℝ}
(hloc : Measurable loc)
(hq : 0 < q) (ha : 0 ≤ a) (hab : a ≤ b) :
HasPolynomialL2Cover (radialMonomialOn d p loc q a b)
(radialMonomialEnvelope b p) := by
apply (HasPseudoDimAtMost.compDomain
(radialMonomialClass_hasPseudoDimAtMost d p hq ha hab) loc).hasPolynomialL2Cover
· 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
14 supporting declarations (lemmas, instances)
-
radialAnnulusMonomial_measurabletheorem — A compactly supported Euclidean radial monomial is Borel measurable in the observation for every fixed center and degree.hypothesesconclusionMeasurable (radialAnnulusMonomial d q a b k x)Proof (Lean source)
@[fun_prop] 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) -
abs_radialAnnulusMonomial_letheorem — Every degree k ≤ p radial monomial on an ordered nonnegative annulus is bounded in absolute value by radialMonomialEnvelope b p.hypothesesconclusion|radialAnnulusMonomial d q a b k x z| ≤ radialMonomialEnvelope b pProof (Lean source)
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 -
pullbacktheorem — Pulling a polynomial-cover class back along an arbitrary parameter map preserves a polynomial L² covering certificate when the new parameter type is nonempty. Cover centers are replaced by occupied-class representatives, which costs only a factor two in radius.hypotheses𝒳 :Type uι :Type vκ :Type wNonempty κF :ι → 𝒳 → ℝU :ℝhF :e :κ → ιconclusionHasPolynomialL2Cover (fun k => F (e k)) UProof (Lean source)
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 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] -
pullbacktheorem — Pullback preserves named entropy witnesses, with the explicit factor-two radius cost used by the ordinary pullback construction.hypotheses𝒳 :Type uι :Type vκ :Type wNonempty κF :ι → 𝒳 → ℝU A :ℝp :ℕhF :HasPolynomialL2CoverWith F U A pe :κ → ιconclusionHasPolynomialL2CoverWith (fun k => F (e k)) U (2 * A) pProof (Lean source)
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 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] -
pullbacktheorem — A parameterwise pullback preserves entropy witnesses uniformly over the outer parameter family.hypotheses𝒳 :Type uS :Type*S → Type vS → Type w(s : S) → ι s → 𝒳 → ℝS → ℝhF :hκ :∀ s, Nonempty (κ s)e :(s : S) → κ s → ι sconclusionHasUniformPolynomialL2CoverOver S (fun s k => F s (e s k)) UProof (Lean source)
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) -
monoEnvelopetheorem — Enlarging the positive envelope of a polynomial L² covering certificate preserves the certificate and its polynomial constants.hypothesesconclusionProof (Lean source)
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)⟩ -
monoEnvelopetheorem — Enlarging an envelope preserves named entropy witnesses.hypothesesconclusionHasPolynomialL2CoverWith F V A pProof (Lean source)
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)⟩ -
monoEnvelopetheorem — A parameterwise envelope enlargement preserves uniform named witnesses.hypotheses𝒳 :Type uS :Type*S → Type v(s : S) → ι s → 𝒳 → ℝS → ℝhF :hUV :∀ s, U s ≤ V sconclusionProof (Lean source)
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)⟩ -
finiteClass_hasPolynomialL2Covertheorem — Every finite family of measurable functions bounded by a positive common envelope has a uniform polynomial L² covering certificate.hypotheses𝒳 :Type uι :Type vFintype ιF :ι → 𝒳 → ℝU :ℝhU :0 < Uhmeas :∀ i, Measurable (F i)hbound :∀ i x, |F i x| ≤ UconclusionProof (Lean source)
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] -
finiteClass_hasPolynomialL2CoverWiththeorem — A finite bounded measurable class has named entropy witnesses depending only on its cardinality.hypotheses𝒳 :Type uι :Type vFintype ιF :ι → 𝒳 → ℝU :ℝhU :0 < Uhmeas :∀ i, Measurable (F i)hbound :∀ i x, |F i x| ≤ UconclusionHasPolynomialL2CoverWith F U (max 1 (Fintype.card ι : ℝ)) 1Proof (Lean source)
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] -
radialMonomialClass_hasPolynomialL2Covertheorem — Moving-center radial monomials of every degree from zero through p have a polynomial L²(Q) cover with a positive constant envelope, uniformly over every probability measure Q.hypothesesd p :ℕq a b :ℝhq :0 < qha :0 ≤ ahab :a ≤ bconclusionProof (Lean source)
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 -
radialAnnulusMonomial_hasPolynomialL2Covertheorem — A fixed degree k ≤ p of the moving-center radial class has the same uniform polynomial cover and envelope as the full degree vector.hypothesesd p k :ℕq a b :ℝhq :0 < qha :0 ≤ ahab :a ≤ bhk :k ≤ pconclusionHasPolynomialL2Cover (fun x : EuclideanPoint d => radialAnnulusMonomial d q a b k x) (radialMonomialEnvelope b p)Proof (Lean source)
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)) -
radialMonomialOn_hasPolynomialL2CoverWiththeorem — The moving-center radial class after a measurable location map has the canonical named VC-subgraph entropy witnesses.hypothesesΩ :Type ud p :ℕloc :Ω → EuclideanPoint dq a b :ℝhloc :Measurable lochq :0 < qha :0 ≤ ahab :a ≤ bconclusionHasPolynomialL2CoverWith (radialMonomialOn d p loc q a b) (radialMonomialEnvelope b p) 16 (8 * (radialPseudoDimBound d p + 1))Proof (Lean source)
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 -
finiteSignedArmRadial_hasPolynomialL2Covertheorem — Multiplying a moving-center radial monomial by any bounded measurable finite family of signed arms preserves a uniform polynomial cover. Boolean arms and the two signs are obtained by taking a finite arm type and values in {0,1} or {-1,1}.hypothesesΩ :Type uA :Type vFintype Ad p :ℕloc :Ω → EuclideanPoint darm :A → Ω → ℝq a b :ℝhloc :Measurable locharmMeas :∀ s, Measurable (arm s)harmBound :∀ s ω, |arm s ω| ≤ 1hq :0 < qha :0 ≤ ahab :a ≤ bconclusionHasPolynomialL2Cover (fun θ : RadialMonomialParam d p × A => fun ω => radialMonomialOn d p loc q a b θ.1 ω * arm θ.2 ω) (radialMonomialEnvelope b p)Proof (Lean source)
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
Score 8 core · 3 supporting This module assembles the moving-center radial basis into a bounded polynomial and then into the residual score shape used by local-polynomial empirical process arguments. ★ radialResidualScore_hasPolynomialL2Cover
Bounded radial-polynomial score classes
This module assembles the moving-center radial basis into a bounded polynomial and then into the residual score shape used by local-polynomial empirical process arguments. Coefficients range over the existing finite coefficient box, all polynomial terms share one moving center, and a finite signed arm may multiply the score.
The proofs are designed to reuse HasPolynomialL2Cover.add, .mul, .neg,
.finSum, the bounded finite-class certificate, and parameter pullback. No
measure regularity beyond measurability is imposed, so the result remains
uniform for atomic probability measures.
def boundedRadialPolynomial reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, a maximal degree, a bandwidth and two relative annulus endpoints, a coefficient bound, a center, a boxed coefficient vector, and an evaluation point, the bounded radial polynomial is the sum, over degrees zero through , of each coefficient times the corresponding radial annulus monomial about the shared center.
Definition (Lean source)
parameters
def
boundedRadialPolynomial d p q a b B x β z :
ℝ
given by
∑ k : Fin (p + 1), β.1 k * radialAnnulusMonomial d q a b k.1 x z
abbrev RadialPolynomialParam reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, a maximal degree, and a coefficient bound, the radial-polynomial parameter space consists of a Euclidean center paired with a coefficient vector whose every coordinate has absolute value at most .
Definition (Lean source)
parameters
d p :
ℕ
B :
ℝ
def
RadialPolynomialParam d p B :
Type
given by
def boundedRadialPolynomialOn reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given an observation space equipped with a σ-algebra, a natural dimension, a maximal degree, a Euclidean location map, a bandwidth and two relative annulus endpoints, a coefficient bound, a radial-polynomial parameter, and an observation, the observation-indexed bounded radial polynomial is the bounded radial polynomial evaluated at the Euclidean location of that observation.
Definition (Lean source)
parameters
def
boundedRadialPolynomialOn d p loc q a b B θ ω :
ℝ
given by
boundedRadialPolynomial d p q a b B θ.1 θ.2 (loc ω)
def radialPolynomialEnvelope reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given an outer relative radius, a maximal degree, and a coefficient bound, the radial-polynomial envelope is times the radial-monomial envelope at that outer radius and degree.
Definition (Lean source)
parameters
b :
ℝ
p :
ℕ
B :
ℝ
def
radialPolynomialEnvelope b p B :
ℝ
given by
((p + 1 : ℕ) : ℝ) * B * radialMonomialEnvelope b p
abbrev RadialResidualScoreParam reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a natural dimension, a maximal degree, a coefficient bound, and an arm index set, the radial residual-score parameter space consists of a radial-polynomial parameter paired with one arm index.
Definition (Lean source)
def radialResidualScore reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given an observation space equipped with a σ-algebra, an arm index set, a natural dimension, a maximal degree, a Euclidean location map, an arm-valued function, a response function, a bandwidth and two relative annulus endpoints, a coefficient bound, a degree index, a residual-score parameter, and an observation, the radial residual score is the product of the arm value, the selected radial annulus monomial, and the residual obtained by subtracting the shared-center boxed radial-polynomial fit from the response.
Definition (Lean source)
parameters
Ω :
Type u
A :
Type v
d p :
ℕ
loc :
Ω → EuclideanPoint d
arm :
A → Ω → ℝ
response :
Ω → ℝ
q a b B :
ℝ
j :
Fin (p + 1)
θ :
RadialResidualScoreParam d p B A
ω :
Ω
def
radialResidualScore d p loc arm response q a b B j θ ω :
ℝ
given by
arm θ.2 ω * radialAnnulusMonomial d q a b j.1 θ.1.1 (loc ω) * (response ω - boundedRadialPolynomial d p q a b B θ.1.1 θ.1.2 (loc ω))
def radialResidualScoreEnvelope reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given an outer relative radius, a maximal degree, a coefficient bound, and a response bound, the radial residual-score envelope is the radial-monomial envelope times the sum of and the radial-polynomial envelope.
Definition (Lean source)
parameters
b :
ℝ
p :
ℕ
B R :
ℝ
def
radialResidualScoreEnvelope b p B R :
ℝ
given by
radialMonomialEnvelope b p * (R + radialPolynomialEnvelope b p B)
theorem radialResidualScore_hasPolynomialL2Cover reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Covering certificate for a bounded finite-arm residual score. Given a measurable Euclidean location map, a finite family of arms, each measurable and bounded in absolute value by 1, a measurable response variable that is bounded in absolute value by R, together with a positive bandwidth q, a nonnegative annulus inner radius a, inner radius at most outer radius b, a positive polynomial-coefficient bound B, and a positive response bound R, then the score formed by multiplying a bounded arm function, a radial monomial, and the residual of the response against a boxed radial-polynomial fit carries a positive-envelope uniform polynomial L²(Q) covering certificate — with envelope radialResidualScoreEnvelope b p B R — over every probability measure Q, including atomic ones.
Formal statement
hypotheses
Ω :
Type u
A :
Type v
Fintype A
d p :
ℕ
loc :
Ω → EuclideanPoint d
arm :
A → Ω → ℝ
response :
Ω → ℝ
q a b B R :
ℝ
j :
Fin (p + 1)
hloc :
Measurable loc
harmMeas :
∀ s, Measurable (arm s)
harmBound :
∀ s ω, |arm s ω| ≤ 1
hresponseMeas :
Measurable response
hresponseBound :
∀ ω, |response ω| ≤ R
hq :
0 < q
ha :
0 ≤ a
hab :
a ≤ b
hB :
0 < B
hR :
0 < R
conclusion
HasPolynomialL2Cover (radialResidualScore d p loc arm response q a b B j) (radialResidualScoreEnvelope b p B R)
Proof (Lean source)
theorem radialResidualScore_hasPolynomialL2Cover
{Ω : Type u} [MeasurableSpace Ω]
{A : Type v} [Fintype A]
(d p : ℕ) (loc : Ω → EuclideanPoint d)
(arm : A → Ω → ℝ) (response : Ω → ℝ)
{q a b B R : ℝ} (j : Fin (p + 1))
(hloc : Measurable loc)
(harmMeas : ∀ s, Measurable (arm s))
(harmBound : ∀ s ω, |arm s ω| ≤ 1)
(hresponseMeas : Measurable response)
(hresponseBound : ∀ ω, |response ω| ≤ R)
(hq : 0 < q) (ha : 0 ≤ a) (hab : a ≤ b)
(hB : 0 < B) (hR : 0 < R) :
HasPolynomialL2Cover
(radialResidualScore d p loc arm response q a b B j)
(radialResidualScoreEnvelope b p B R) := by
classical
let M := radialMonomialEnvelope b p
let P := radialPolynomialEnvelope b p B
have hM : 0 < M := by
dsimp [M, radialMonomialEnvelope]
positivity
have hP : 0 < P := by
dsimp [P, radialPolynomialEnvelope]
have hp1 : (0 : ℝ) < (p + 1 : ℕ) := by positivity
positivity
have hU : 0 < M * (R + P) := by positivity
cases isEmpty_or_nonempty A with
| inl hA =>
letI : IsEmpty A := hA
refine ⟨?_, ?_, ?_, ?_⟩
· simpa [radialResidualScoreEnvelope, M, P] using hU
· intro θ
exact isEmptyElim θ.2
· intro θ
exact isEmptyElim θ.2
· refine ⟨1, 0, le_rfl, ?_⟩
intro Q hQ ε hε hε1
refine ⟨∅, ?_, ?_⟩
· simp
· intro θ
exact isEmptyElim θ.2
| inr hA =>
letI : Nonempty A := hA
letI : Nonempty (CoeffBox (Fin (p + 1)) B) :=
⟨⟨fun _ => 0, fun _ => by simpa using hB.le⟩⟩
have harm : HasPolynomialL2Cover arm 1 :=
finiteClass_hasPolynomialL2Cover arm (by norm_num) harmMeas harmBound
have hleading : HasPolynomialL2Cover
(fun x : EuclideanPoint d => fun ω =>
radialAnnulusMonomial d q a b j.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, j))
exact hpull
have hpoly := boundedRadialPolynomialOn_hasPolynomialL2Cover
d p loc hloc hq ha hab hB
have hresponse : HasPolynomialL2Cover
(fun _ : Unit => response) R := by
exact finiteClass_hasPolynomialL2Cover (fun _ : Unit => response)
hR (fun _ => hresponseMeas) (fun _ => hresponseBound)
have harmLeading := harm.mul hleading
have hresidual := hresponse.add hpoly.neg
have hsuper := harmLeading.mul hresidual
have hpull :=
pullback
hsuper
(fun θ : RadialResidualScoreParam d p B A =>
((θ.2, θ.1.1), ((), θ.1)))
change HasPolynomialL2Cover
(radialResidualScore d p loc arm response q a b B j)
(M * (R + P))
simp only [one_mul] at hpull
exact hpull
3 supporting declarations (lemmas, instances)
-
abs_boundedRadialPolynomial_letheorem — Every boxed shared-center radial polynomial is bounded by the number of basis functions times the coefficient bound times the monomial envelope.hypothesesd p :ℕq a b B :ℝhq :0 < qha :0 ≤ ahab :a ≤ bhB :0 ≤ Bx :z :conclusion|boundedRadialPolynomial d p q a b B x β z| ≤ radialPolynomialEnvelope b p BProof (Lean source)
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 -
boundedRadialPolynomialOn_hasPolynomialL2Covertheorem — Boxed finite radial polynomials with one moving center shared by all degrees have a uniform polynomial L² covering certificate.hypothesesΩ :Type ud p :ℕloc :Ω → EuclideanPoint dq a b B :ℝhloc :Measurable lochq :0 < qha :0 ≤ ahab :a ≤ bhB :0 < BconclusionProof (Lean source)
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 -
radialResidualScore_hasUniformPolynomialL2CoverWiththeorem — The radial residual-score construction admits entropy witnesses depending only on the Euclidean dimension, polynomial degree, and finite arm type. In particular, the witnesses precede all location maps, arm functions, responses, bandwidths, annuli, and envelope radii.hypothesesconclusion∃ 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 nProof (Lean source)
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⟩), 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
Trace 4 core · 6 supporting This module isolates the combinatorial tools used by the Euclidean radial construction. ★ booleanCombination_hasVCAtMost
Finite-trace tools for radial VC-subgraph classes
This module isolates the combinatorial tools used by the Euclidean radial construction. It gives a homogeneous linear-sign VC bound, deliberately coarse but explicit bounds for finite Boolean combinations and finite unions, and pullback lemmas for both Boolean VC dimension and pseudo-dimension.
The Boolean-combination theorem is trace-level: its combining formula may depend on the sampled point. This is important for radial subgraphs, where the formula changes according to the sign of the sampled threshold.
def booleanCombinationVCBound reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a number of Boolean component classes and a common VC-dimension bound, the Boolean-combination VC bound is the explicit natural number .
Definition (Lean source)
parameters
m d :
ℕ
def
booleanCombinationVCBound m d :
ℕ
given by
2 ^ (m * (d + 1) + 1)
def finiteUnionVCBound reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a number of component classes and a common VC-dimension bound, the finite-union VC bound is the explicit natural number .
Definition (Lean source)
parameters
m d :
ℕ
def
finiteUnionVCBound m d :
ℕ
given by
2 ^ (m * (d + 1) + 1)
def linearSignClass reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
Given a finite feature index set, a real-valued feature family, a real coefficient vector, and an evaluation point, the homogeneous linear-sign classifier returns true exactly when the coefficient-feature inner product at that point is strictly positive.
theorem booleanCombination_hasVCAtMost reviewed
⚑ flagged
Causalean.Stat.Concentration.EuclideanRadialPolynomial
VC bound for a point-dependent Boolean combination of classes. Given m independently parameterized Boolean classifier families, each of VC dimension at most d, applying to them any combining rule that may itself depend on the sampled point still yields a Boolean class of VC dimension at most booleanCombinationVCBound m d.
Formal statement
hypotheses
conclusion
HasVCAtMost (fun θ : (j : Fin m) → ι j => fun x => combine x (fun j => π j (θ j) x)) (booleanCombinationVCBound m d)
Proof (Lean source)
theorem booleanCombination_hasVCAtMost
{m d : ℕ} {ι : Fin m → Type v}
(π : (j : Fin m) → ι j → 𝒳 → Bool)
(hπ : ∀ j, HasVCAtMost (π j) d)
(combine : 𝒳 → (Fin m → Bool) → Bool) :
HasVCAtMost
(fun θ : (j : Fin m) → ι j => fun x =>
combine x (fun j => π j (θ j) x))
(booleanCombinationVCBound m d) := by
simpa only [booleanCombinationVCBound] using
hasVCAtMost_of_growth_card_le
(fun θ : (j : Fin m) → ι j => fun x =>
combine x (fun j => π j (θ j) x))
(m * (d + 1))
(fun n S => booleanCombination_growth_card_le (n := n) π hπ combine S)
6 supporting declarations (lemmas, instances)
-
reindextheorem — Reparameterizing a Boolean class by an arbitrary map cannot increase its finite-trace VC dimension.hypothesesconclusionHasVCAtMost (fun k => π (e k)) dProof (Lean source)
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⟩ -
compDomaintheorem — Precomposing the observation argument of a Boolean class cannot increase its finite-trace VC dimension.hypothesesconclusionHasVCAtMost (fun i y => π i (g y)) dProof (Lean source)
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)) -
reindextheorem — Reparameterizing a real-valued class by an arbitrary map cannot increase its pseudo-dimension.hypothesesconclusionHasPseudoDimAtMost (fun k => F (e k)) dProof (Lean source)
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⟩ -
compDomaintheorem — Precomposing every function in a real-valued class with a fixed map cannot increase its pseudo-dimension.hypothesesconclusionHasPseudoDimAtMost (fun i y => F i (g y)) dProof (Lean source)
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)) -
linearSignClass_hasVCAtMosttheorem — Homogeneous linear threshold classifiers in K real coordinates have VC dimension at most the number of coordinates.hypothesesconclusionProof (Lean source)
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 -
finiteUnion_hasVCAtMosttheorem — A finite union of m Boolean classes of VC dimension at most d has finite VC dimension bounded by finiteUnionVCBound m d.hypothesesconclusionProof (Lean source)
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)