Stat.Nonparametric.Local­Poly.Rate

Explicit Θ(Nh) leverage-rate bounds for the local-polynomial design inverse, derived from entrywise design-matrix concentration and population scaling.

Rate 2 core · 1 supporting Explicit Θ(Nh) leverage-rate bounds for the local-polynomial design inverse, derived from entrywise design-matrix concentration and population scaling. ★ localPoly_inv00_rate★ localPoly_leverage_bound

Explicit Θ(Nh) rate for the local-polynomial leverage (M⁻¹)₀₀

Explicit Θ(Nh) leverage-rate bounds for the local-polynomial design inverse, derived from entrywise design-matrix concentration and population scaling.

This module converts the entrywise design-matrix concentration of Concentration.DesignInverse into the explicit interior local-polynomial leverage rate:

* localPoly_inv00_rate — on the good design event (empirical moment matrix M entrywise within η of the population matrix S), the leverage (M⁻¹)₀₀ ≤ 2·cInv/(Nh), i.e. the variance scale is Θ(1/(Nh)). * localPoly_leverage_bound — the leverage product √(M₀₀·(M⁻¹)₀₀) ≤ √(2·cInv·(cTop+1)), a bandwidth-free constant, controlling the ℓ¹ bias leverage.

The population matrix is supplied with its Θ(Nh) scale via the diagonal-conjugation factorization S = (Nh)·D·T·D (D = diagonal (h^j)): population_scaling_of_conj turns a bandwidth-free shape matrix T (invertible with bounded (T⁻¹)₀₀ and T₀₀, supplied by the integral-moment positive-definiteness of LocalPoly.Rate.IntegralMoment) into the leverage scaling hypotheses (S⁻¹)₀₀ ≤ cInv/(Nh) and S₀₀ ≤ cTop·(Nh). The entrywise-closeness hypothesis is the good event whose probability is bounded by designMatrix_inv_concentration.

theorem localPoly_inv00_rate reviewed
Causalean.Stat.Nonparametric

Explicit Θ(1/(Nh)) rate for the local-polynomial leverage. On a good design event with positive scale Nh where the population moment matrix S is invertible, its inverse row sums are bounded by a nonnegative constant c, the empirical moment matrix M lies entrywise within a nonnegative perturbation scale η of S, the perturbation is small relative to the dimension: c·(p+1)·η ≤ 1/2, and the population intercept leverage sits at the Θ(Nh) scale: (S⁻¹)₀₀ ≤ cInv/(Nh) and 2c²(p+1)η ≤ cInv/(Nh), then the empirical moment matrix M is invertible and its intercept leverage obeys the explicit interior rate (M⁻¹)₀₀ ≤ 2·cInv/(Nh). This is the variance-rate capstone for the local-polynomial upper bound: combined with localPoly_intercept_variance_le it yields the O((Nh)^{-1/2}) stochastic error.

Formal statement
hypotheses
N :
ℕ
h c cInv η :
ℝ
S M :
Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ
_hNh :
0 < (N : ℝ) * h
hS :
IsUnit S.det
_hc :
0 ≤ c
_hη :
0 ≤ η
hSrow :
∀ i, (∑ j, |S⁻¹ i j|) ≤ c
hclose :
∀ j k, |M j k - S j k| ≤ η
hsmall :
c * ((p + 1 : ℕ) * η) ≤ 1 / 2
hSinv00 :
S⁻¹ 0 0 ≤ cInv / ((N : ℝ) * h)
hpert :
2 * c ^ 2 * ((p + 1 : ℕ) * η) ≤ cInv / ((N : ℝ) * h)
conclusion
IsUnit M.det ∧ M⁻¹ 0 0 ≤ 2 * (cInv / ((N : ℝ) * h))
Proof (Lean source)
theorem localPoly_inv00_rate {N : ℕ} {h c cInv η : ℝ} {S M : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ} (_hNh : 0 < (N : ℝ) * h) (hS : IsUnit S.det) (_hc : 0 ≤ c) (_hη : 0 ≤ η) (hSrow : ∀ i, (∑ j, |S⁻¹ i j|) ≤ c) (hclose : ∀ j k, |M j k - S j k| ≤ η) (hsmall : c * ((p + 1 : ℕ) * η) ≤ 1 / 2) (hSinv00 : S⁻¹ 0 0 ≤ cInv / ((N : ℝ) * h)) (hpert : 2 * c ^ 2 * ((p + 1 : ℕ) * η) ≤ cInv / ((N : ℝ) * h)) : IsUnit M.det ∧ M⁻¹ 0 0 ≤ 2 * (cInv / ((N : ℝ) * h)) := by obtain ⟨hMdet, hΔ⟩ := designInv00_perturb S M hS hSrow hclose hsmall refine ⟨hMdet, ?_⟩ have hub := (abs_le.mp hΔ).2 linarith [hub, hSinv00, hpert]
Causalean.Stat.Nonparametric.localPoly_inv00_rate · Causalean/Stat/Nonparametric/LocalPoly/Rate.lean:77
theorem localPoly_leverage_bound reviewed
Causalean.Stat.Nonparametric

Bandwidth-free bound on the local-polynomial leverage product. On the same good design event with positive scale Nh, where the population moment matrix S is invertible, its inverse row sums are bounded by a nonnegative constant c, the empirical moment matrix M lies entrywise within a nonnegative perturbation scale η that is small relative to the dimension (c·(p+1)·η ≤ 1/2) and at most Nh, with nonnegative density constants cInv and cTop such that the population intercept leverage and perturbation obey (S⁻¹)₀₀ ≤ cInv/(Nh) and 2c²(p+1)η ≤ cInv/(Nh), the population top weight obeys S₀₀ ≤ cTop·(Nh), and the empirical top weight M₀₀ and inverse leverage (M⁻¹)₀₀ are both nonnegative, the geometric mean of the total weight and the inverse leverage is bounded by the bandwidth-free constant √(M₀₀·(M⁻¹)₀₀) ≤ √(2·cInv·(cTop+1)). The Θ(Nh) growth of M₀₀ ≤ (cTop+1)·(Nh) exactly cancels the Θ(1/(Nh)) decay of (M⁻¹)₀₀. Via equivKernelWeight_abs_sum_sq_le ((∑ᵢ|Sᵢ|)² ≤ M₀₀·(M⁻¹)₀₀) this controls the ℓ¹ bias leverage ∑ᵢ|Sᵢ| by a bandwidth-free constant, the second leverage capstone used by the upper-bound analysis.

Formal statement
hypotheses
N :
ℕ
h c cInv cTop η :
ℝ
S M :
Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ
hNh :
0 < (N : ℝ) * h
hS :
IsUnit S.det
hc :
0 ≤ c
hη :
0 ≤ η
_hcInv :
0 ≤ cInv
_hcTop :
0 ≤ cTop
hSrow :
∀ i, (∑ j, |S⁻¹ i j|) ≤ c
hclose :
∀ j k, |M j k - S j k| ≤ η
hsmall :
c * ((p + 1 : ℕ) * η) ≤ 1 / 2
hSinv00 :
S⁻¹ 0 0 ≤ cInv / ((N : ℝ) * h)
hpert :
2 * c ^ 2 * ((p + 1 : ℕ) * η) ≤ cInv / ((N : ℝ) * h)
hS00 :
S 0 0 ≤ cTop * ((N : ℝ) * h)
hηle :
η ≤ (N : ℝ) * h
hM00 :
0 ≤ M 0 0
hMinv00 :
0 ≤ M⁻¹ 0 0
conclusion
sqrt (M 0 0 * M⁻¹ 0 0) ≤ sqrt (2 * cInv * (cTop + 1))
Proof (Lean source)
theorem localPoly_leverage_bound {N : ℕ} {h c cInv cTop η : ℝ} {S M : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ} (hNh : 0 < (N : ℝ) * h) (hS : IsUnit S.det) (hc : 0 ≤ c) (hη : 0 ≤ η) (_hcInv : 0 ≤ cInv) (_hcTop : 0 ≤ cTop) (hSrow : ∀ i, (∑ j, |S⁻¹ i j|) ≤ c) (hclose : ∀ j k, |M j k - S j k| ≤ η) (hsmall : c * ((p + 1 : ℕ) * η) ≤ 1 / 2) (hSinv00 : S⁻¹ 0 0 ≤ cInv / ((N : ℝ) * h)) (hpert : 2 * c ^ 2 * ((p + 1 : ℕ) * η) ≤ cInv / ((N : ℝ) * h)) (hS00 : S 0 0 ≤ cTop * ((N : ℝ) * h)) (hηle : η ≤ (N : ℝ) * h) (hM00 : 0 ≤ M 0 0) (hMinv00 : 0 ≤ M⁻¹ 0 0) : sqrt (M 0 0 * M⁻¹ 0 0) ≤ sqrt (2 * cInv * (cTop + 1)) := by obtain ⟨_, hrate⟩ := localPoly_inv00_rate hNh hS hc hη hSrow hclose hsmall hSinv00 hpert have hcl := (abs_le.mp (hclose 0 0)).2 have hM00bd : M 0 0 ≤ (cTop + 1) * ((N : ℝ) * h) := by nlinarith [hS00, hcl, hηle] have hb0 : 0 ≤ (cTop + 1) * ((N : ℝ) * h) := by nlinarith [_hcTop, hNh.le] have hprod : M 0 0 * M⁻¹ 0 0 ≤ 2 * cInv * (cTop + 1) := by have hmul := mul_le_mul hM00bd hrate hMinv00 hb0 have hne : ((N : ℝ) * h) ≠ 0 := hNh.ne' calc M 0 0 * M⁻¹ 0 0 ≤ ((cTop + 1) * ((N : ℝ) * h)) * (2 * (cInv / ((N : ℝ) * h))) := hmul _ = 2 * cInv * (cTop + 1) := by rw [div_eq_mul_inv] calc ((cTop + 1) * ((N : ℝ) * h)) * (2 * (cInv * (((N : ℝ) * h)⁻¹))) = (2 * cInv * (cTop + 1)) * (((N : ℝ) * h) * (((N : ℝ) * h)⁻¹)) := by ring _ = 2 * cInv * (cTop + 1) := by rw [mul_inv_cancel₀ hne] ring exact Real.sqrt_le_sqrt hprod
Causalean.Stat.Nonparametric.localPoly_leverage_bound · Causalean/Stat/Nonparametric/LocalPoly/Rate.lean:102
1 supporting declaration (lemmas, instances)
  • population_scaling_of_conj theorem — Θ(Nh) leverage scaling from the change-of-variables factorization. If the population moment matrix factors as S = (Nh)·D·T·D with D = diagonal (fun j => h^j) (so D₀₀ = 1) and a bandwidth-free shape matrix T that is invertible with (T⁻¹)₀₀ ≤ cInv and T₀₀ ≤ cTop, then S is invertible and its intercept leverage scales as (S⁻¹)₀₀ ≤ cInv/(Nh) while its top weight scales as S₀₀ ≤ cTop·(Nh). This discharges the leverage-scaling hypotheses of the rate capstones from the bandwidth-free shape matrix T.
    hypotheses
    N :
    ℕ
    h cInv cTop :
    ℝ
    hh :
    0 < h
    hN :
    0 < (N : ℝ)
    T S :
    Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ
    hT :
    IsUnit T.det
    hTinv00 :
    T⁻¹ 0 0 ≤ cInv
    hT00 :
    T 0 0 ≤ cTop
    hS :
    S
    = ((N : ℝ) * h) • (diagonal (fun j : Fin (p + 1) => h ^ (j : ℕ)) * T * diagonal (fun j : Fin (p + 1) => h ^ (j : ℕ)))
    conclusion
    IsUnit S.det ∧ S⁻¹ 0 0 ≤ cInv / ((N : ℝ) * h) ∧ S 0 0 ≤ cTop * ((N : ℝ) * h)
    Proof (Lean source)
    theorem population_scaling_of_conj {N : ℕ} {h cInv cTop : ℝ} (hh : 0 < h) (hN : 0 < (N : ℝ)) {T S : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ} (hT : IsUnit T.det) (hTinv00 : T⁻¹ 0 0 ≤ cInv) (hT00 : T 0 0 ≤ cTop) (hS : S = ((N : ℝ) * h) • (diagonal (fun j : Fin (p + 1) => h ^ (j : ℕ)) * T * diagonal (fun j : Fin (p + 1) => h ^ (j : ℕ)))) : IsUnit S.det ∧ S⁻¹ 0 0 ≤ cInv / ((N : ℝ) * h) ∧ S 0 0 ≤ cTop * ((N : ℝ) * h) := by let κ : ℝ := (N : ℝ) * h have hκ : κ ≠ 0 := (mul_pos hN hh).ne' have hd : ∀ i : Fin (p + 1), h ^ (i : ℕ) ≠ 0 := fun i => pow_ne_zero _ hh.ne' have hd0 : (fun j : Fin (p + 1) => h ^ (j : ℕ)) 0 = 1 := by simp obtain ⟨hdet, hinv00⟩ := inv00_diag_conj (κ := κ) hκ hd hd0 hT hS have htop := top00_diag_conj (κ := κ) hd0 hS refine ⟨hdet, ?_, ?_⟩ · rw [hinv00] have hκnonneg : 0 ≤ κ⁻¹ := inv_nonneg.mpr (mul_pos hN hh).le calc κ⁻¹ * T⁻¹ 0 0 ≤ κ⁻¹ * cInv := mul_le_mul_of_nonneg_left hTinv00 hκnonneg _ = cInv / ((N : ℝ) * h) := by simp [κ, div_eq_mul_inv, mul_comm] · rw [htop] have hκnonneg : 0 ≤ κ := (mul_pos hN hh).le calc κ * T 0 0 ≤ κ * cTop := mul_le_mul_of_nonneg_left hT00 hκnonneg _ = cTop * ((N : ℝ) * h) := by simp [κ, mul_comm]
    Causalean.Stat.Nonparametric.population_scaling_of_conj · Causalean/Stat/Nonparametric/LocalPoly/Rate.lean:41
Conjugation 1 core · 2 supporting The interior local-polynomial leverage (M⁻¹)₀₀ lives on the population moment matrix S at the scale Θ(Nh). ★ inv00_diag_conj

Diagonal-conjugation scaling of the design moment matrix inverse

The interior local-polynomial leverage (M⁻¹)₀₀ lives on the population moment matrix S at the scale Θ(Nh). The change of variables u = (a−t)/h factors the population matrix as a diagonal conjugation of a bandwidth-free shape matrix T:

S = (N·h) • (D · T · D), with D = diagonal (fun j => h^j),

so that D₀₀ = h⁰ = 1. This file isolates the pure linear algebra of that factorization: if S = κ • (D · T · D) with D an invertible diagonal matrix whose (0,0) entry is 1, T invertible, and κ ≠ 0, then S is invertible and its leverage entry collapses to

(S⁻¹)₀₀ = κ⁻¹ · (T⁻¹)₀₀.

The D₀₀ = 1 cancellation is exactly why the bandwidth powers drop out of the (0,0) entry, leaving the clean Θ(1/(Nh)) rate (the off-diagonal h^j factors never touch the intercept). The companion top-entry identity S₀₀ = κ · T₀₀ is recorded for the leverage product M₀₀·(M⁻¹)₀₀.

theorem inv00_diag_conj reviewed
Causalean.Stat.Nonparametric

Leverage entry under diagonal-conjugation scaling. If S factors as κ • (D · T · D) for a nonzero scalar κ with D = diagonal d an invertible diagonal matrix (every d i nonzero) whose first entry is 1, and T invertible, then S is invertible and its (0,0) inverse entry collapses to (S⁻¹)₀₀ = κ⁻¹ · (T⁻¹)₀₀: the diagonal bandwidth powers cancel at the intercept because D₀₀ = 1.

Formal statement
hypotheses
κ :
ℝ
hκ :
κ ≠ 0
d :
Fin (p + 1) → ℝ
hd :
∀ i, d i ≠ 0
hd0 :
d 0 = 1
T S :
Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ
hT :
IsUnit T.det
hS :
S = κ • (diagonal d * T * diagonal d)
conclusion
IsUnit S.det ∧ S⁻¹ 0 0 = κ⁻¹ * T⁻¹ 0 0
Proof (Lean source)
theorem inv00_diag_conj {κ : ℝ} (hκ : κ ≠ 0) {d : Fin (p + 1) → ℝ} (hd : ∀ i, d i ≠ 0) (hd0 : d 0 = 1) {T S : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ} (hT : IsUnit T.det) (hS : S = κ • (diagonal d * T * diagonal d)) : IsUnit S.det ∧ S⁻¹ 0 0 = κ⁻¹ * T⁻¹ 0 0 := by obtain ⟨hdet, hform⟩ := inv_diag_conj hκ hd hT hS refine ⟨hdet, ?_⟩ rw [hform] simp [Matrix.smul_apply, Matrix.diagonal_mul, Matrix.mul_diagonal, hd0]
Causalean.Stat.Nonparametric.inv00_diag_conj · Causalean/Stat/Nonparametric/LocalPoly/Rate/Conjugation.lean:80
2 supporting declarations (lemmas, instances)
  • inv_diag_conj theorem — Diagonal-conjugation inverse formula. If S = κ • (D · T · D) with κ ≠ 0 and D = diagonal d an invertible diagonal matrix (d i ≠ 0), T invertible, then S is invertible with S⁻¹ = κ⁻¹ • (D⁻¹ · T⁻¹ · D⁻¹) where D⁻¹ = diagonal (fun i => (d i)⁻¹).
    hypotheses
    κ :
    ℝ
    hκ :
    κ ≠ 0
    d :
    Fin (p + 1) → ℝ
    hd :
    ∀ i, d i ≠ 0
    T S :
    Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ
    hT :
    IsUnit T.det
    hS :
    S = κ • (diagonal d * T * diagonal d)
    conclusion
    IsUnit S.det ∧
    S⁻¹
    = κ⁻¹ • (diagonal (fun i => (d i)⁻¹) * T⁻¹ * diagonal (fun i => (d i)⁻¹))
    Proof (Lean source)
    theorem inv_diag_conj {κ : ℝ} (hκ : κ ≠ 0) {d : Fin (p + 1) → ℝ} (hd : ∀ i, d i ≠ 0) {T S : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ} (hT : IsUnit T.det) (hS : S = κ • (Matrix.diagonal d * T * Matrix.diagonal d)) : IsUnit S.det ∧ S⁻¹ = κ⁻¹ • (Matrix.diagonal (fun i => (d i)⁻¹) * T⁻¹ * Matrix.diagonal (fun i => (d i)⁻¹)) := by let D : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ := Matrix.diagonal d let D' : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ := Matrix.diagonal (fun i => (d i)⁻¹) let X : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ := κ⁻¹ • (D' * T⁻¹ * D') have hDD' : D * D' = 1 := by dsimp [D, D'] rw [Matrix.diagonal_mul_diagonal] simp [Matrix.diagonal_one, fun i => mul_inv_cancel₀ (hd i)] have hcore : (D * T * D) * (D' * T⁻¹ * D') = 1 := by calc (D * T * D) * (D' * T⁻¹ * D') = D * T * (D * D') * T⁻¹ * D' := by simp [mul_assoc] _ = D * (T * T⁻¹) * D' := by rw [hDD'] simp [mul_assoc] _ = D * 1 * D' := by rw [Matrix.mul_nonsing_inv T hT] _ = D * D' := by simp _ = 1 := hDD' have hSX : S * X = 1 := by rw [hS] dsimp [X] change (κ • (D * T * D)) * (κ⁻¹ • (D' * T⁻¹ * D')) = 1 calc (κ • (D * T * D)) * (κ⁻¹ • (D' * T⁻¹ * D')) = (κ⁻¹ * κ) • ((D * T * D) * (D' * T⁻¹ * D')) := by simp [smul_smul] _ = 1 := by rw [inv_mul_cancel₀ hκ] simp [hcore] exact ⟨Matrix.isUnit_det_of_right_inverse hSX, Matrix.inv_eq_right_inv hSX⟩
    Causalean.Stat.Nonparametric.inv_diag_conj · Causalean/Stat/Nonparametric/LocalPoly/Rate/Conjugation.lean:36
  • top00_diag_conj theorem — Top entry under diagonal-conjugation scaling. Under the same factorization S = κ • (D · T · D) with d 0 = 1, the (0,0) entry of S itself is S₀₀ = κ · T₀₀.
    hypotheses
    κ :
    ℝ
    d :
    Fin (p + 1) → ℝ
    hd0 :
    d 0 = 1
    T S :
    Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ
    hS :
    S = κ • (diagonal d * T * diagonal d)
    conclusion
    S 0 0 = κ * T 0 0
    Proof (Lean source)
    theorem top00_diag_conj {κ : ℝ} {d : Fin (p + 1) → ℝ} (hd0 : d 0 = 1) {T S : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ} (hS : S = κ • (diagonal d * T * diagonal d)) : S 0 0 = κ * T 0 0 := by rw [hS] simp [Matrix.smul_apply, Matrix.diagonal_mul, Matrix.mul_diagonal, hd0]
    Causalean.Stat.Nonparametric.top00_diag_conj · Causalean/Stat/Nonparametric/LocalPoly/Rate/Conjugation.lean:95
Integral­Moment 2 core · 4 supporting Positive-definiteness criteria for integral Gram matrices of centered monomials, supplying invertibility of local-polynomial population moment matrices. ★ intMomentMatrix_posDef

Positive-definiteness of the integral (population) moment matrix

Positive-definiteness criteria for integral Gram matrices of centered monomials, supplying invertibility of local-polynomial population moment matrices.

The population analogue of the empirical design moment matrix is the integral Gram matrix of the centered monomials φ_j(a) = (a − t)^j against a positive measure ν (for the local-polynomial fit, ν is the kernel-weighted design law K((·−t)/h)·μ_A):

S_{jk} = ∫ (a − t)^j · (a − t)^k dν.

Its quadratic form is vᵀ S v = ∫ (∑ⱼ vⱼ (a−t)^j)² dν ≥ 0, so with a finite second moment it is positive semidefinite, and positive definite — hence invertible — exactly when the design law ν is non-degenerate (no nonzero degree-p polynomial of the centered argument vanishes ν-almost everywhere; e.g. ν is not supported on ≤ p points). This is the integral transport of designMatrix_posDef and discharges the IsUnit S.det hypothesis for the bandwidth-free shape matrix T feeding the Θ(Nh) leverage rate.

def intMomentMatrix reviewed
Causalean.Stat.Nonparametric

The integral (population) moment matrix S_{jk} = ∫ (a − t)^j (a − t)^k dν of the centered monomials against a measure ν.

Definition (Lean source)
noncomputable def intMomentMatrix (p : ℕ) (ν : Measure ℝ) (t : ℝ) : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ := of (fun j k => ∫ a, (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ) ∂ν)
Causalean.Stat.Nonparametric.intMomentMatrix · Causalean/Stat/Nonparametric/LocalPoly/Rate/IntegralMoment.lean:36
theorem intMomentMatrix_posDef reviewed
Causalean.Stat.Nonparametric

The integral moment matrix is positive definite whenever every centered-monomial product (a−t)^j·(a−t)^k is integrable against the design measure ν and the design law is non-degenerate: no nonzero coefficient vector v makes the centered polynomial ∑ⱼ vⱼ (a−t)^j vanish ν-almost everywhere. Then the integral moment matrix intMomentMatrix p ν t is positive definite.

Formal statement
hypotheses
p :
ℕ
ν :
Measure ℝ
t :
ℝ
hint :
∀ j k : Fin (p + 1), Integrable (fun a => (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ)) ν
hnd :
∀ v : Fin (p + 1) → ℝ
if
v ≠ 0
then
¬ (∀ᵐ a ∂ν, (∑ j, v j * (a - t) ^ (j : ℕ)) = 0)
conclusion
(intMomentMatrix p ν t).PosDef
Proof (Lean source)
theorem intMomentMatrix_posDef {p : ℕ} {ν : Measure ℝ} {t : ℝ} (hint : ∀ j k : Fin (p + 1), Integrable (fun a => (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ)) ν) (hnd : ∀ v : Fin (p + 1) → ℝ, v ≠ 0 → ¬ (∀ᵐ a ∂ν, (∑ j, v j * (a - t) ^ (j : ℕ)) = 0)) : (intMomentMatrix p ν t).PosDef := by refine Matrix.PosDef.of_dotProduct_mulVec_pos intMomentMatrix_isHermitian (fun v hv => ?_) have hstar : star v = v := funext (fun i => star_trivial _) rw [hstar, intMomentMatrix_quadForm hint] have hnn : 0 ≤ ∫ a, (∑ j : Fin (p + 1), v j * (a - t) ^ (j : ℕ)) ^ 2 ∂ν := integral_nonneg (fun a => sq_nonneg _) have hq2 : Integrable (fun a => (∑ j : Fin (p + 1), v j * (a - t) ^ (j : ℕ)) ^ 2) ν := by have e : (fun a => (∑ j : Fin (p + 1), v j * (a - t) ^ (j : ℕ)) ^ 2) = (fun a => ∑ j : Fin (p + 1), ∑ k : Fin (p + 1), (v j * v k) * ((a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ))) := by funext a rw [pow_two, Finset.sum_mul_sum] refine Finset.sum_congr rfl ?_ intro j _ refine Finset.sum_congr rfl ?_ intro k _ ring rw [e] exact integrable_finset_sum _ (fun j _ => integrable_finset_sum _ (fun k _ => (hint j k).const_mul (v j * v k))) cases lt_or_eq_of_le hnn with | inl h => exact h | inr h => exfalso have hz := (MeasureTheory.integral_eq_zero_iff_of_nonneg (fun a => sq_nonneg ((∑ j : Fin (p + 1), v j * (a - t) ^ (j : ℕ)))) hq2).mp h.symm apply hnd v hv filter_upwards [hz] with a ha exact sq_eq_zero_iff.mp ha
Causalean.Stat.Nonparametric.intMomentMatrix_posDef · Causalean/Stat/Nonparametric/LocalPoly/Rate/IntegralMoment.lean:115 · uses intMomentMatrix
4 supporting declarations (lemmas, instances)
  • intMomentMatrix_quadForm theorem — Gram quadratic form of the integral moment matrix. vᵀ S v = ∫ (∑ⱼ vⱼ (a−t)^j)² dν — the population moment matrix is the integral Gram matrix of the centered monomial features.
    hypotheses
    p :
    ℕ
    ν :
    Measure ℝ
    t :
    ℝ
    hint :
    ∀ j k : Fin (p + 1), Integrable (fun a => (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ)) ν
    v :
    Fin (p + 1) → ℝ
    conclusion
    v ⬝ᵥ (intMomentMatrix p ν t *ᵥ v) = ∫ a, (∑ j, v j * (a - t) ^ (j : ℕ)) ^ 2 ∂ν
    Proof (Lean source)
    theorem intMomentMatrix_quadForm {p : ℕ} {ν : Measure ℝ} {t : ℝ} (hint : ∀ j k : Fin (p + 1), Integrable (fun a => (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ)) ν) (v : Fin (p + 1) → ℝ) : v ⬝ᵥ (intMomentMatrix p ν t *ᵥ v) = ∫ a, (∑ j, v j * (a - t) ^ (j : ℕ)) ^ 2 ∂ν := by simp only [dotProduct, mulVec, intMomentMatrix, Matrix.of_apply] calc ∑ j : Fin (p + 1), v j * ∑ k : Fin (p + 1), (∫ a, (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ) ∂ν) * v k = ∑ j : Fin (p + 1), ∑ k : Fin (p + 1), (v j * v k) * ∫ a, (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ) ∂ν := by refine Finset.sum_congr rfl ?_ intro j _ rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro k _ ring _ = ∑ j : Fin (p + 1), ∑ k : Fin (p + 1), ∫ a, (v j * v k) * ((a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ)) ∂ν := by refine Finset.sum_congr rfl ?_ intro j _ refine Finset.sum_congr rfl ?_ intro k _ exact (MeasureTheory.integral_const_mul (v j * v k) (fun a => (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ))).symm _ = ∑ j : Fin (p + 1), ∫ a, ∑ k : Fin (p + 1), (v j * v k) * ((a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ)) ∂ν := by refine Finset.sum_congr rfl ?_ intro j _ symm rw [MeasureTheory.integral_finset_sum] intro k _ exact (hint j k).const_mul (v j * v k) _ = ∫ a, ∑ j : Fin (p + 1), ∑ k : Fin (p + 1), (v j * v k) * ((a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ)) ∂ν := by symm rw [MeasureTheory.integral_finset_sum] intro j _ exact integrable_finset_sum _ (fun k _ => (hint j k).const_mul (v j * v k)) _ = ∫ a, (∑ j, v j * (a - t) ^ (j : ℕ)) ^ 2 ∂ν := by exact MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall (fun a => by change (∑ j : Fin (p + 1), ∑ k : Fin (p + 1), (v j * v k) * ((a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ))) = (∑ j : Fin (p + 1), v j * (a - t) ^ (j : ℕ)) ^ 2 rw [pow_two, Finset.sum_mul_sum] refine Finset.sum_congr rfl ?_ intro j _ refine Finset.sum_congr rfl ?_ intro k _ ring))
    Causalean.Stat.Nonparametric.intMomentMatrix_quadForm · Causalean/Stat/Nonparametric/LocalPoly/Rate/IntegralMoment.lean:42
  • intMomentMatrix_isHermitian theorem — The integral moment matrix is symmetric.
    hypotheses
    p :
    ℕ
    ν :
    Measure ℝ
    t :
    ℝ
    conclusion
    (intMomentMatrix p ν t).IsHermitian
    Proof (Lean source)
    theorem intMomentMatrix_isHermitian {p : ℕ} {ν : Measure ℝ} {t : ℝ} : (intMomentMatrix p ν t).IsHermitian := by ext j k simp only [Matrix.conjTranspose_apply, intMomentMatrix, Matrix.of_apply, star_trivial] exact MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall (fun a => by ring))
    Causalean.Stat.Nonparametric.intMomentMatrix_isHermitian · Causalean/Stat/Nonparametric/LocalPoly/Rate/IntegralMoment.lean:98
  • intMomentMatrix_posSemidef theorem — The integral moment matrix is positive semidefinite (a Gram matrix of an L² family).
    hypotheses
    p :
    ℕ
    ν :
    Measure ℝ
    t :
    ℝ
    hint :
    ∀ j k : Fin (p + 1), Integrable (fun a => (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ)) ν
    conclusion
    (intMomentMatrix p ν t).PosSemidef
    Proof (Lean source)
    theorem intMomentMatrix_posSemidef {p : ℕ} {ν : Measure ℝ} {t : ℝ} (hint : ∀ j k : Fin (p + 1), Integrable (fun a => (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ)) ν) : (intMomentMatrix p ν t).PosSemidef := by refine Matrix.PosSemidef.of_dotProduct_mulVec_nonneg intMomentMatrix_isHermitian (fun v => ?_) have hstar : star v = v := funext (fun i => star_trivial _) rw [hstar, intMomentMatrix_quadForm hint] exact integral_nonneg (fun a => sq_nonneg _)
    Causalean.Stat.Nonparametric.intMomentMatrix_posSemidef · Causalean/Stat/Nonparametric/LocalPoly/Rate/IntegralMoment.lean:105
  • intMomentMatrix_isUnit_det theorem — Invertibility of the integral moment matrix from design non-degeneracy: a positive definite matrix has a unit determinant, discharging the IsUnit S.det hypothesis for the population shape matrix.
    hypotheses
    p :
    ℕ
    ν :
    Measure ℝ
    t :
    ℝ
    hint :
    ∀ j k : Fin (p + 1), Integrable (fun a => (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ)) ν
    hnd :
    ∀ v : Fin (p + 1) → ℝ
    if
    v ≠ 0
    then
    ¬ (∀ᵐ a ∂ν, (∑ j, v j * (a - t) ^ (j : ℕ)) = 0)
    conclusion
    IsUnit (intMomentMatrix p ν t).det
    Proof (Lean source)
    theorem intMomentMatrix_isUnit_det {p : ℕ} {ν : Measure ℝ} {t : ℝ} (hint : ∀ j k : Fin (p + 1), Integrable (fun a => (a - t) ^ (j : ℕ) * (a - t) ^ (k : ℕ)) ν) (hnd : ∀ v : Fin (p + 1) → ℝ, v ≠ 0 → ¬ (∀ᵐ a ∂ν, (∑ j, v j * (a - t) ^ (j : ℕ)) = 0)) : IsUnit (intMomentMatrix p ν t).det := (Matrix.isUnit_iff_isUnit_det _).mp (intMomentMatrix_posDef hint hnd).isUnit
    Causalean.Stat.Nonparametric.intMomentMatrix_isUnit_det · Causalean/Stat/Nonparametric/LocalPoly/Rate/IntegralMoment.lean:157