Proximal contamination in mixed-model association

DefinitionMixed-model association chi-squared statistic#✓fully proved

The mixed-model (generalized-least-squares score) statistic χ²(V) = (xᵀ V⁻¹ y)² / (xᵀ V⁻¹ x) of the marker x for the phenotype y under the phenotypic covariance V. For positive definite V and x ≠ 0 the denominator is positive.

noncomputable def mmChiSq (V : Matrix n n ℝ) (x y : n → ℝ) : ℝ :=
  (x ⬝ᵥ (V⁻¹ *ᵥ y)) ^ 2 / (x ⬝ᵥ (V⁻¹ *ᵥ x))

Used by 2

Used byProximal contamination · Including the marker in the covariance never increases the statistic

TheoremSherman–Morrison applied to the candidate marker#✓fully proved

For positive definite V₀ and c ≥ 0, (V₀ + c x xᵀ)⁻¹ x = (1 + c xᵀ V₀⁻¹ x)⁻¹ • V₀⁻¹ x.

theorem inv_add_smul_vecMulVec_mulVec {V₀ : Matrix n n ℝ} (hV₀ : V₀.PosDef) {c : ℝ}
    (hc : 0 ≤ c) (x : n → ℝ) :
    (V₀ + c • vecMulVec x x)⁻¹ *ᵥ x =
      (1 + c * (x ⬝ᵥ (V₀⁻¹ *ᵥ x)))⁻¹ • (V₀⁻¹ *ᵥ x)

Used by 1

Used byProximal contamination

TheoremProximal contamination#✓fully proved

Including the candidate marker x in the covariance, V = V₀ + c x xᵀ with V₀ positive definite and c ≥ 0, divides the mixed-model statistic by 1 + c xᵀ V₀⁻¹ x, for every phenotype vector y: χ²(V₀ + c x xᵀ) = χ²(V₀) / (1 + c xᵀ V₀⁻¹ x).

theorem mmChiSq_add_smul_vecMulVec {V₀ : Matrix n n ℝ} (hV₀ : V₀.PosDef) {c : ℝ} (hc : 0 ≤ c)
    (x y : n → ℝ) :
    mmChiSq (V₀ + c • vecMulVec x x) x y =
      mmChiSq V₀ x y / (1 + c * (x ⬝ᵥ (V₀⁻¹ *ᵥ x)))

Uses 2 · Used by 1

Statement usesMixed-model association chi-squared statistic

Proof usesSherman–Morrison applied to the candidate marker

Used byIncluding the marker in the covariance never increases the statistic

TheoremIncluding the marker in the covariance never increases the statistic#✓fully proved

Including the candidate marker in the covariance never increases the mixed-model statistic: χ²(V₀ + c x xᵀ) ≤ χ²(V₀) for positive definite V₀ and c ≥ 0.

theorem mmChiSq_add_smul_vecMulVec_le {V₀ : Matrix n n ℝ} (hV₀ : V₀.PosDef) {c : ℝ}
    (hc : 0 ≤ c) (x y : n → ℝ) : mmChiSq (V₀ + c • vecMulVec x x) x y ≤ mmChiSq V₀ x y

Uses 2

Statement usesMixed-model association chi-squared statistic

Proof usesProximal contamination

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.