Skip to content

Genomic prediction from summary statistics

49 fully proved

Polygenic-score accuracy

TheoremCross moment of two polygenic scores#✓fully proved

In a target population whose marker genotypes x j have raw second moments ∫ x j * x k = [j = k] (standardized, uncorrelated markers), the scores xᵀ a and xᵀ b of two effect vectors have raw cross moment aᵀ b. With mean-zero genotypes and a probability measure this is the covariance of the genetic value xᵀ β and the polygenic score xᵀ β̂.

theorem integral_score_mul_score {Ξ : Type*} {mΞ : MeasurableSpace Ξ} {ν : Measure Ξ}
    (x : Fin M → Ξ → ℝ) (hx : ∀ j, MemLp (x j) 2 ν)
    (hxx : ∀ j k, ∫ ξ, x j ξ * x k ξ ∂ν = if j = k then 1 else 0) (a b : Fin M → ℝ) :
    ∫ ξ, (∑ j, a j * x j ξ) * (∑ k, b k * x k ξ) ∂ν = ∑ j, a j * b j

StructureEffect-estimate model for polygenic score accuracy#✓fully proved

The effect-estimate model behind polygenic-score accuracy (Daetwyler et al. 2008; Dudbridge 2013), at the level of raw second moments, for M independent markers: true effects beta k with ∫ β k β l = (h² / M) [k = l], estimation errors err k with ∫ e k e l = s² [k = l], orthogonal to the effects. The estimates are β̂ = β + e (betaHat). For a probability measure and mean-zero effects and errors these are the covariance conditions of the cited model; s² is the sampling variance of each estimate (1 / N in the cited papers, (1 - h²) / N in ofLDScore).

MathlibExt.Biology.StatisticalGenetics.GenomicPrediction.PRSModel · 19 lines 
structure PRSModel (μ : Measure Ω) (M : ℕ) where
  /-- The SNP heritability `h²`. -/
  h2 : ℝ
  /-- The sampling variance `s²` of each effect estimate. -/
  s2 : ℝ
  /-- Random per-marker effects. -/
  beta : Fin M → Ω → ℝ
  /-- Random estimation errors. -/
  err : Fin M → Ω → ℝ
  /-- Effects are square integrable. -/
  memLp_beta : ∀ k, MemLp (beta k) 2 μ
  /-- Errors are square integrable. -/
  memLp_err : ∀ k, MemLp (err k) 2 μ
  /-- `∫ β βᵀ = (h² / M) I`. -/
  integral_beta_mul : ∀ k l, ∫ ω, beta k ω * beta l ω ∂μ = if k = l then h2 / M else 0
  /-- `∫ e eᵀ = s² I`. -/
  integral_err_mul : ∀ k l, ∫ ω, err k ω * err l ω ∂μ = if k = l then s2 else 0
  /-- Effects and errors are orthogonal: `∫ β eᵀ = 0`. -/
  integral_beta_mul_err : ∀ k l, ∫ ω, beta k ω * err l ω ∂μ = 0
Used by 11
Used bySquared accuracy of a polygenic score · Polygenic-score accuracy · Daetwyler–Dudbridge formula · Polygenic-score accuracy in the LD-score model · Estimated marker effects · Nonnegativity of heritability in the effect-estimate model · Expected squared norm of the estimated effects · Expected cross product of true and estimated effects · Expected squared norm of the true effects · Effect-estimate model derived from the LD-score model · Nonnegativity of the sampling error variance of effect estimates

TheoremNonnegativity of heritability in the effect-estimate model#✓fully proved

The model forces h² ≥ 0 when there is at least one marker.

theorem h2_nonneg (hM : 0 < M) : 0 ≤ D.h2
Uses 1
Statement usesEffect-estimate model for polygenic score accuracy

TheoremNonnegativity of the sampling error variance of effect estimates#✓fully proved

The model forces s² ≥ 0 when there is at least one marker.

theorem s2_nonneg (hM : 0 < M) : 0 ≤ D.s2
Uses 1
Statement usesEffect-estimate model for polygenic score accuracy

DefinitionEstimated marker effects#✓fully proved

The estimated effects β̂ = β + e.

def betaHat (k : Fin M) (ω : Ω) : ℝ := D.beta k ω + D.err k ω
Uses 1 · Used by 5
Statement usesEffect-estimate model for polygenic score accuracy
Used bySquared accuracy of a polygenic score · Polygenic-score accuracy · Expected squared norm of the estimated effects · Expected cross product of true and estimated effects · Estimates of the derived model are normalized scores

DefinitionSquared accuracy of a polygenic score#✓fully proved

The squared correlation of the genetic value and the polygenic score as a ratio of expectations, 𝔼[βᵀβ̂]² / (𝔼[βᵀβ] 𝔼[β̂ᵀβ̂]): by integral_score_mul_score, βᵀβ̂, βᵀβ and β̂ᵀβ̂ are the covariance and variances of xᵀβ and xᵀβ̂ over a target population of standardized uncorrelated markers. It is not the expectation of a squared correlation.

noncomputable def accuracySq : ℝ :=
  (∫ ω, ∑ k, D.beta k ω * D.betaHat k ω ∂μ) ^ 2 /
    ((∫ ω, ∑ k, D.beta k ω ^ 2 ∂μ) * ∫ ω, ∑ k, D.betaHat k ω ^ 2 ∂μ)
Uses 2 · Used by 3
Statement usesEffect-estimate model for polygenic score accuracy · Estimated marker effects
Used byPolygenic-score accuracy · Daetwyler–Dudbridge formula · Polygenic-score accuracy in the LD-score model

TheoremExpected cross product of true and estimated effects#✓fully proved

𝔼[βᵀβ̂] = h² (for at least one marker).

theorem integral_beta_mul_betaHat (hM : M ≠ 0) :
    ∫ ω, ∑ k, D.beta k ω * D.betaHat k ω ∂μ = D.h2
Uses 2 · Used by 1
Statement usesEffect-estimate model for polygenic score accuracy · Estimated marker effects
Used byPolygenic-score accuracy

TheoremExpected squared norm of the true effects#✓fully proved

𝔼[βᵀβ] = h² (for at least one marker).

theorem integral_beta_sq (hM : M ≠ 0) : ∫ ω, ∑ k, D.beta k ω ^ 2 ∂μ = D.h2
Uses 1 · Used by 1
Statement usesEffect-estimate model for polygenic score accuracy
Used byPolygenic-score accuracy

TheoremExpected squared norm of the estimated effects#✓fully proved

𝔼[β̂ᵀβ̂] = h² + M s² (for at least one marker).

theorem integral_betaHat_sq (hM : M ≠ 0) :
    ∫ ω, ∑ k, D.betaHat k ω ^ 2 ∂μ = D.h2 + M * D.s2
Uses 2 · Used by 1
Statement usesEffect-estimate model for polygenic score accuracy · Estimated marker effects
Used byPolygenic-score accuracy

TheoremPolygenic-score accuracy#✓fully proved

Polygenic-score accuracy as a ratio of expectations: r²_g = h² / (h² + M s²). (If h² = 0 both sides are 0.)

theorem accuracySq_eq (hM : M ≠ 0) : D.accuracySq = D.h2 / (D.h2 + M * D.s2)
Uses 6 · Used by 2
Statement usesEffect-estimate model for polygenic score accuracy · Squared accuracy of a polygenic score
Proof usesEstimated marker effects · Expected squared norm of the estimated effects · Expected cross product of true and estimated effects · Expected squared norm of the true effects
Used byDaetwyler–Dudbridge formula · Polygenic-score accuracy in the LD-score model

TheoremDaetwyler–Dudbridge formula#✓fully proved

With sampling variance s² = 1 / N, r²_g = N h² / (N h² + M).

theorem accuracySq_eq_of_s2 {N : ℕ} (hM : M ≠ 0) (hN : N ≠ 0) (hs : D.s2 = 1 / N) :
    D.accuracySq = N * D.h2 / (N * D.h2 + M)
Uses 3
Statement usesEffect-estimate model for polygenic score accuracy · Squared accuracy of a polygenic score
Proof usesPolygenic-score accuracy

DefinitionTraining genotype matrix with orthogonal standardized columns#✓fully proved

The training genotype matrix has orthogonal columns with sum of squares N, ∑ i, X i k * X i l = N [k = l]; for centered columns this says that the markers are uncorrelated, with unit sample variance, in the training sample.

def HasOrthogonalColumns {N : ℕ} (X : Matrix (Fin N) (Fin M) ℝ) : Prop :=
  ∀ k l, ∑ i, X i k * X i l = if k = l then (N : ℝ) else 0
Used by 3
Used byPolygenic-score accuracy in the LD-score model · Effect-estimate model derived from the LD-score model · Estimates of the derived model are normalized scores

DefinitionEffect-estimate model derived from the LD-score model#✓fully proved

The effect-estimate model obtained from the LD-score model when the effects are estimated by the normalized scores β̂ = Xᵀ y / N on a training matrix with orthogonal standardized columns: the error is e k = ∑ i, X i k ε i / N and its sampling variance is (1 - h²) / N.

MathlibExt.Biology.StatisticalGenetics.GenomicPrediction.PRSModel.ofLDScore · 35 lines 
noncomputable def ofLDScore (D : LDScore.Model μ N M) (X : Matrix (Fin N) (Fin M) ℝ)
    (hX : HasOrthogonalColumns X) : PRSModel μ M where
  h2 := D.h2
  s2 := (1 - D.h2) / N
  beta := D.beta
  err k ω := ∑ i, X i k / N * D.eps i ω
  memLp_beta := D.memLp_beta
  memLp_err k := by
    have h := memLp_finsetSum Finset.univ fun i _ => (D.memLp_eps i).const_mul (X i k / N)
    convert h using 1
  integral_beta_mul := D.integral_beta_mul
  integral_err_mul k l := by
    rw [integral_sum_mul_sum _ _ _ _ D.memLp_eps D.memLp_eps]
    simp_rw [D.integral_eps_mul, mul_ite, mul_zero, Finset.sum_ite_eq, Finset.mem_univ,
      ite_true]
    have h : ∑ i, X i k / N * (X i l / N) * (1 - D.h2) =
        (∑ i, X i k * X i l) * ((1 - D.h2) / N ^ 2) := by
      rw [Finset.sum_mul]
      exact Finset.sum_congr rfl fun i _ => by ring
    rw [h, hX k l]
    rcases eq_or_ne (N : ℝ) 0 with hN | hN
    · simp [hN]
    · split_ifs
      · field_simp
      · simp
  integral_beta_mul_err k l := by
    have h (i : Fin N) : ∫ ω, D.beta k ω * (X i l / N * D.eps i ω) ∂μ = 0 := by
      have he : (fun ω => D.beta k ω * (X i l / N * D.eps i ω)) =
          fun ω => X i l / N * (D.beta k ω * D.eps i ω) := funext fun ω => by ring
      rw [he, integral_const_mul, D.integral_beta_mul_eps, mul_zero]
    have hi (i : Fin N) : Integrable (fun ω => D.beta k ω * (X i l / N * D.eps i ω)) μ :=
      (D.memLp_beta k).integrable_mul ((D.memLp_eps i).const_mul (X i l / N))
    simp_rw [Finset.mul_sum]
    rw [integral_finsetSum _ fun i _ => hi i]
    simp [h]
Uses 3 · Used by 2
Statement usesTraining genotype matrix with orthogonal standardized columns · Effect-estimate model for polygenic score accuracy · Random-effects model of LD-score regression
Used byPolygenic-score accuracy in the LD-score model · Estimates of the derived model are normalized scores

TheoremEstimates of the derived model are normalized scores#✓fully proved

The estimates of ofLDScore are the normalized scores Xᵀ y / N of the LD-score model.

theorem ofLDScore_betaHat (D : LDScore.Model μ N M) (X : Matrix (Fin N) (Fin M) ℝ)
    (hX : HasOrthogonalColumns X) (hN : N ≠ 0) (k : Fin M) (ω : Ω) :
    (ofLDScore D X hX).betaHat k ω = D.betaHat X k ω
Uses 6
Statement usesTraining genotype matrix with orthogonal standardized columns · Estimated marker effects · Effect-estimate model derived from the LD-score model · Random-effects model of LD-score regression · Normalized marginal score in the LD-score model
Proof usesPhenotype in the LD-score model

TheoremPolygenic-score accuracy in the LD-score model#✓fully proved

With orthogonal standardized training columns, β̂ = Xᵀ y / N and residual variance 1 - h², r²_g = N h² / (N h² + M (1 - h²)). The cited N h² / (N h² + M) takes the residual variance to be 1.

theorem accuracySq_ofLDScore (D : LDScore.Model μ N M) (X : Matrix (Fin N) (Fin M) ℝ)
    (hX : HasOrthogonalColumns X) (hN : N ≠ 0) (hM : M ≠ 0) :
    (ofLDScore D X hX).accuracySq = N * D.h2 / (N * D.h2 + M * (1 - D.h2))
Uses 6
Statement usesTraining genotype matrix with orthogonal standardized columns · Squared accuracy of a polygenic score · Effect-estimate model derived from the LD-score model · Random-effects model of LD-score regression
Proof usesEffect-estimate model for polygenic score accuracy · Polygenic-score accuracy

COJO: joint and conditional estimates from marginal statistics

DefinitionMarginal least-squares estimate of a marker effect#✓fully proved

The marginal least-squares estimate x_jᵀ y / x_jᵀ x_j of marker j (single-marker regression without intercept, on centered genotypes and phenotype as in Yang et al. 2012).

noncomputable def marginalEstimate (X : Matrix (Fin n) ι ℝ) (y : Fin n → ℝ) (j : ι) : ℝ :=
  (Xᵀ *ᵥ y) j / (Xᵀ * X) j j
Used by 4
Used byCOJO joint estimate · Joint estimate equals marginal estimates for uncorrelated markers · COJO conditional algebraic formula from summary statistics · Genotype-phenotype cross products from marginal estimates

DefinitionDiagonal of the genotype Gram matrix#✓fully proved

The diagonal D = diag(XᵀX) of the Gram matrix.

noncomputable def gramDiag (X : Matrix (Fin n) ι ℝ) : Matrix ι ι ℝ :=
  diagonal fun j => (Xᵀ * X) j j
Used by 4
Used byCOJO joint estimate · Joint estimate equals marginal estimates for uncorrelated markers · COJO conditional algebraic formula from summary statistics · Genotype-phenotype cross products from marginal estimates

TheoremGenotype-phenotype cross products from marginal estimates#✓fully proved

Xᵀ y = D β̂ for the marginal estimates β̂ (Yang et al. 2012). This holds for every genotype matrix: a column with x_jᵀ x_j = 0 is zero, so both sides vanish there.

theorem transpose_mulVec_eq_gramDiag_mulVec (X : Matrix (Fin n) ι ℝ) (y : Fin n → ℝ) :
    Xᵀ *ᵥ y = gramDiag X *ᵥ marginalEstimate X y
Uses 2 · Used by 2
Statement usesDiagonal of the genotype Gram matrix · Marginal least-squares estimate of a marker effect
Used byCOJO joint estimate · COJO conditional algebraic formula from summary statistics

TheoremCOJO joint estimate#✓fully proved

COJO joint estimate (Yang et al. 2012, eq. (5)): the joint least-squares estimate (XᵀX)⁻¹ Xᵀ y equals (XᵀX)⁻¹ D β̂ in terms of the marginal estimates β̂, so it can be computed from summary statistics and XᵀX. (Stated for every X; it is the least-squares estimate when XᵀX is invertible.)

theorem cojo_joint (X : Matrix (Fin n) ι ℝ) (y : Fin n → ℝ) :
    (Xᵀ * X)⁻¹ *ᵥ (Xᵀ *ᵥ y) = (Xᵀ * X)⁻¹ *ᵥ (gramDiag X *ᵥ marginalEstimate X y)
Uses 3 · Used by 1
Statement usesDiagonal of the genotype Gram matrix · Marginal least-squares estimate of a marker effect
Proof usesGenotype-phenotype cross products from marginal estimates
Used byJoint estimate equals marginal estimates for uncorrelated markers

TheoremJoint estimate equals marginal estimates for uncorrelated markers#✓fully proved

For markers uncorrelated in the sample (XᵀX diagonal) without zero columns, the joint estimate is the vector of marginal estimates.

theorem cojo_joint_of_diagonal (X : Matrix (Fin n) ι ℝ) (y : Fin n → ℝ)
    (hX : Xᵀ * X = gramDiag X) (hD : ∀ j, (Xᵀ * X) j j ≠ 0) :
    (Xᵀ * X)⁻¹ *ᵥ (Xᵀ *ᵥ y) = marginalEstimate X y
Uses 3
Statement usesDiagonal of the genotype Gram matrix · Marginal least-squares estimate of a marker effect
Proof usesCOJO joint estimate

DefinitionConditional estimate of second-block effects (COJO)#✓fully proved

The unconditional algebraic formula from Yang et al. 2012, eq. (15): (X₂ᵀX₂)⁻¹ X₂ᵀ y - (X₂ᵀX₂)⁻¹ X₂ᵀX₁ (X₁ᵀX₁)⁻¹ X₁ᵀ y. When both Gram determinants are units, this has the usual interpretation as the block-2 fit conditional on the block-1 fit. For a singular Gram matrix, Mathlib's nonsingular inverse is zero and the value can be a junk value.

noncomputable def conditionalEstimate (X₁ : Matrix (Fin n) ι₁ ℝ) (X₂ : Matrix (Fin n) ι₂ ℝ)
    (y : Fin n → ℝ) : ι₂ → ℝ :=
  (X₂ᵀ * X₂)⁻¹ *ᵥ (X₂ᵀ *ᵥ y) - ((X₂ᵀ * X₂)⁻¹ * X₂ᵀ * X₁ * (X₁ᵀ * X₁)⁻¹) *ᵥ (X₁ᵀ *ᵥ y)
Used by 2
Used byConditional estimate as a fit to the first-block residual · COJO conditional algebraic formula from summary statistics

TheoremCOJO conditional algebraic formula from summary statistics#✓fully proved

COJO conditional algebraic formula from summary statistics (Yang et al. 2012, eq. (17)): b̂₂|b̂₁ = (X₂ᵀX₂)⁻¹ D₂ β̂₂ - (X₂ᵀX₂)⁻¹ X₂ᵀX₁ (X₁ᵀX₁)⁻¹ D₁ β̂₁.

theorem conditionalEstimate_eq_summary (X₁ : Matrix (Fin n) ι₁ ℝ) (X₂ : Matrix (Fin n) ι₂ ℝ)
    (y : Fin n → ℝ) :
    conditionalEstimate X₁ X₂ y =
      (X₂ᵀ * X₂)⁻¹ *ᵥ (gramDiag X₂ *ᵥ marginalEstimate X₂ y) -
        ((X₂ᵀ * X₂)⁻¹ * X₂ᵀ * X₁ * (X₁ᵀ * X₁)⁻¹) *ᵥ (gramDiag X₁ *ᵥ marginalEstimate X₁ y)
Uses 4
Statement usesConditional estimate of second-block effects (COJO) · Diagonal of the genotype Gram matrix · Marginal least-squares estimate of a marker effect
Proof usesGenotype-phenotype cross products from marginal estimates

TheoremConditional estimate as a fit to the first-block residual#✓fully proved

Unconditionally, the conditional formula equals the nonsingular-inverse formula applied to the algebraic residual y - X₁ ((X₁ᵀX₁)⁻¹ X₁ᵀ y). If both Gram determinants are units, these are the successive least-squares fits on blocks 1 and 2. With a singular Gram matrix they need not minimize residual error. This is in general not the block-2 part of the joint formula on both blocks (the formulas agree when X₂ᵀX₁ = 0).

theorem conditionalEstimate_eq_residual (X₁ : Matrix (Fin n) ι₁ ℝ) (X₂ : Matrix (Fin n) ι₂ ℝ)
    (y : Fin n → ℝ) :
    conditionalEstimate X₁ X₂ y =
      (X₂ᵀ * X₂)⁻¹ *ᵥ (X₂ᵀ *ᵥ (y - X₁ *ᵥ ((X₁ᵀ * X₁)⁻¹ *ᵥ (X₁ᵀ *ᵥ y))))
Uses 1
Statement usesConditional estimate of second-block effects (COJO)

Stratified and cross-trait LD-score regression

DefinitionStratified LD score#✓fully proved

The stratified normalized-cross-product score ℓ(j, C) = ∑_{k ∈ C} (X_jᵀ X_k / N)². For a standardized genotype matrix this is the stratified LD score of marker j with respect to annotation category C (Finucane et al. 2015).

noncomputable def stratLDScore (X : Matrix (Fin N) (Fin M) ℝ) (C : Finset (Fin M)) (j : Fin M) :
    ℝ :=
  ∑ k ∈ C, ldCorr X j k ^ 2
Uses 1 · Used by 3
Statement usesNormalized cross product of genotype markers
Used byExpected association statistic in the stratified LD-score model · Stratified LD-score regression · One causal variant

StructureStratified LD-score model#✓fully proved

The stratified LD-score model (Finucane et al. 2015), at the level of raw second moments: annotation categories cat c ⊆ {markers} (possibly overlapping), per-category contributions tau c, effects with ∫ β k β l = [k = l] ∑_c τ_c [k ∈ cat c], noise with ∫ ε i ε i' = σ²_e [i = i'], effects orthogonal to noise. The cited model normalizes the phenotypic variance so that σ²_e ≈ 1; the confounding term N a is not modeled.

MathlibExt.Biology.StatisticalGenetics.GenomicPrediction.StratifiedModel · 22 lines 
structure StratifiedModel (μ : Measure Ω) (N M : ℕ) (C : Type*) [Fintype C] where
  /-- The markers in each annotation category. -/
  cat : C → Finset (Fin M)
  /-- The per-marker heritability contribution `τ_C` of each category. -/
  tau : C → ℝ
  /-- The noise variance `σ²_e`. -/
  sigma2e : ℝ
  /-- Random per-marker effects. -/
  beta : Fin M → Ω → ℝ
  /-- Random environmental noise. -/
  eps : Fin N → Ω → ℝ
  /-- Effects are square integrable. -/
  memLp_beta : ∀ k, MemLp (beta k) 2 μ
  /-- Noise terms are square integrable. -/
  memLp_eps : ∀ i, MemLp (eps i) 2 μ
  /-- `∫ β k β l = [k = l] ∑_c τ_c [k ∈ cat c]`. -/
  integral_beta_mul : ∀ k l, ∫ ω, beta k ω * beta l ω ∂μ =
    if k = l then ∑ c, (if k ∈ cat c then tau c else 0) else 0
  /-- `∫ ε εᵀ = σ²_e I`. -/
  integral_eps_mul : ∀ i i', ∫ ω, eps i ω * eps i' ω ∂μ = if i = i' then sigma2e else 0
  /-- Effects and noise are orthogonal. -/
  integral_beta_mul_eps : ∀ k i, ∫ ω, beta k ω * eps i ω ∂μ = 0
Used by 6
Used byNormalized score in the stratified LD-score model · Association statistic in the stratified LD-score model · Expected association statistic in the stratified LD-score model · Stratified LD-score regression · One causal variant · Phenotype in the stratified LD-score model

DefinitionPhenotype in the stratified LD-score model#✓fully proved

The phenotype y = X β + ε.

def pheno (i : Fin N) (ω : Ω) : ℝ := ∑ k, X i k * D.beta k ω + D.eps i ω
Uses 1 · Used by 2
Statement usesStratified LD-score model
Used byNormalized score in the stratified LD-score model · Expected association statistic in the stratified LD-score model

DefinitionNormalized score in the stratified LD-score model#✓fully proved

The N-normalized score β̂ j = X_jᵀ y / N.

noncomputable def betaHat (j : Fin M) (ω : Ω) : ℝ := (∑ i, X i j * D.pheno X i ω) / N
Uses 2 · Used by 2
Statement usesStratified LD-score model · Phenotype in the stratified LD-score model
Used byAssociation statistic in the stratified LD-score model · Expected association statistic in the stratified LD-score model

DefinitionAssociation statistic in the stratified LD-score model#✓fully proved

The association statistic χ² j = N β̂ j ².

noncomputable def chiSq (j : Fin M) (ω : Ω) : ℝ := N * D.betaHat X j ω ^ 2
Uses 2 · Used by 3
Statement usesStratified LD-score model · Normalized score in the stratified LD-score model
Used byExpected association statistic in the stratified LD-score model · Stratified LD-score regression · One causal variant

TheoremExpected association statistic in the stratified LD-score model#✓fully proved

The exact expectation of the association statistic in the stratified model, for any genotype matrix: 𝔼[χ² j] = N ∑_c τ_c ℓ(j, cat c) + σ²_e (∑ i, X i j ²) / N.

theorem integral_chiSq (j : Fin M) :
    ∫ ω, D.chiSq X j ω ∂μ =
      N * ∑ c, D.tau c * stratLDScore X (D.cat c) j + D.sigma2e * (∑ i, X i j ^ 2) / N
Uses 6 · Used by 1
Statement usesStratified LD-score model · Association statistic in the stratified LD-score model · Stratified LD score
Proof usesNormalized score in the stratified LD-score model · Phenotype in the stratified LD-score model · Normalized cross product of genotype markers
Used byStratified LD-score regression

TheoremStratified LD-score regression#✓fully proved

Stratified LD-score regression (Finucane et al. 2015): for a standardized genotype matrix and N ≠ 0, 𝔼[χ² j] = N ∑_c τ_c ℓ(j, cat c) + σ²_e. Full-matrix standardization makes every normalized cross product in stratLDScore a sample correlation.

theorem integral_chiSq_of_standardized (hN : N ≠ 0) (j : Fin M) (hX : IsStandardized X) :
    ∫ ω, D.chiSq X j ω ∂μ = N * ∑ c, D.tau c * stratLDScore X (D.cat c) j + D.sigma2e
Uses 5 · Used by 1
Statement usesStratified LD-score model · Association statistic in the stratified LD-score model · Stratified LD score · Standardized genotype matrix
Proof usesExpected association statistic in the stratified LD-score model
Used byOne causal variant

TheoremOne causal variant#✓fully proved

One causal variant (the LD-proxy noncentrality; Pritchard & Przeworski 2001): if the genotype matrix is standardized and the only category is the single causal marker c with variance τ, then for a marker m and N ≠ 0, 𝔼[χ² m] = N τ r m c ² + σ²_e.

theorem integral_chiSq_single_causal (D : StratifiedModel μ N M Unit) (c : Fin M)
    (hcat : D.cat () = {c}) (hN : N ≠ 0) (j : Fin M) (hX : IsStandardized X) :
    ∫ ω, D.chiSq X j ω ∂μ = N * D.tau () * ldCorr X j c ^ 2 + D.sigma2e
Uses 6
Statement usesStratified LD-score model · Association statistic in the stratified LD-score model · Standardized genotype matrix · Normalized cross product of genotype markers
Proof usesStratified LD-score regression · Stratified LD score

DefinitionIn-sample LD correlation#✓fully proved

The in-sample normalized cross product ∑_{i ∈ S} X i j X i k / |S| of markers j, k in the sample S of a pool of individuals (the sample LD correlation for a matrix standardized within S).

noncomputable def sampleCorr (X : Matrix (Fin n) (Fin M) ℝ) (S : Finset (Fin n)) (j k : Fin M) :
    ℝ :=
  (∑ i ∈ S, X i j * X i k) / S.card
Used by 2
Used byCross-trait scaled-score identity, exact form · Equal normalized-cross-product specialization of the residual cross-moment identity

StructureBivariate LD-score model#✓fully proved

The bivariate LD-score model (Bulik-Sullivan et al. 2015b), at the level of the cross second moments that enter 𝔼[z₁ z₂]: a pool of n genotyped individuals with genotype matrix X, two GWAS samples S₁, S₂ of the pool (possibly overlapping), effects β₁, β₂ with ∫ β₁ k β₂ l = (ρ_g / M) [k = l] (genetic covariance ρ_g), noises ε₁, ε₂ with ∫ ε₁ i ε₂ i' = ρ_e [i = i'] (residual cross-moment ρ_e within an individual), effects of each trait orthogonal to the noise of the other. The structure intentionally does not impose within-trait moments or phenotype normalization, so it does not identify ρ_e with phenotypic correlation or establish that the scaled scores below are standardized z-scores.

MathlibExt.Biology.StatisticalGenetics.GenomicPrediction.CrossTraitModel · 34 lines 
structure CrossTraitModel (μ : Measure Ω) (n M : ℕ) where
  /-- The sample of trait 1. -/
  S1 : Finset (Fin n)
  /-- The sample of trait 2. -/
  S2 : Finset (Fin n)
  /-- The genetic covariance `ρ_g`. -/
  rhoG : ℝ
  /-- The environmental covariance `ρ_e`. -/
  rhoE : ℝ
  /-- Effects on trait 1. -/
  beta1 : Fin M → Ω → ℝ
  /-- Effects on trait 2. -/
  beta2 : Fin M → Ω → ℝ
  /-- Noise of trait 1. -/
  eps1 : Fin n → Ω → ℝ
  /-- Noise of trait 2. -/
  eps2 : Fin n → Ω → ℝ
  /-- Square integrability. -/
  memLp_beta1 : ∀ k, MemLp (beta1 k) 2 μ
  /-- Square integrability. -/
  memLp_beta2 : ∀ k, MemLp (beta2 k) 2 μ
  /-- Square integrability. -/
  memLp_eps1 : ∀ i, MemLp (eps1 i) 2 μ
  /-- Square integrability. -/
  memLp_eps2 : ∀ i, MemLp (eps2 i) 2 μ
  /-- `∫ β₁ β₂ᵀ = (ρ_g / M) I`. -/
  integral_beta1_mul_beta2 : ∀ k l, ∫ ω, beta1 k ω * beta2 l ω ∂μ =
    if k = l then rhoG / M else 0
  /-- `∫ ε₁ ε₂ᵀ = ρ_e I`. -/
  integral_eps1_mul_eps2 : ∀ i i', ∫ ω, eps1 i ω * eps2 i' ω ∂μ = if i = i' then rhoE else 0
  /-- `∫ β₁ ε₂ᵀ = 0`. -/
  integral_beta1_mul_eps2 : ∀ k i, ∫ ω, beta1 k ω * eps2 i ω ∂μ = 0
  /-- `∫ ε₁ β₂ᵀ = 0`. -/
  integral_eps1_mul_beta2 : ∀ i k, ∫ ω, eps1 i ω * beta2 k ω ∂μ = 0
Used by 4
Used byCross-trait scaled-score identity, exact form · Equal normalized-cross-product specialization of the residual cross-moment identity · Scaled marginal score for the first trait · Scaled marginal score for the second trait

DefinitionScaled marginal score for the first trait#✓fully proved

The scaled marginal score z₁ j = √N₁ X_jᵀ y₁ / N₁ of marker j for trait 1, computed on S₁ with y₁ = X β₁ + ε₁. The model does not assert the normalization needed for a z-score.

noncomputable def z1 (j : Fin M) (ω : Ω) : ℝ :=
  √(D.S1.card : ℝ) * ((∑ i ∈ D.S1, X i j * (∑ k, X i k * D.beta1 k ω + D.eps1 i ω)) / D.S1.card)
Uses 1 · Used by 2
Statement usesBivariate LD-score model
Used byCross-trait scaled-score identity, exact form · Equal normalized-cross-product specialization of the residual cross-moment identity

DefinitionScaled marginal score for the second trait#✓fully proved

The analogous scaled marginal score z₂ j of marker j for trait 2, computed on S₂.

noncomputable def z2 (j : Fin M) (ω : Ω) : ℝ :=
  √(D.S2.card : ℝ) * ((∑ i ∈ D.S2, X i j * (∑ k, X i k * D.beta2 k ω + D.eps2 i ω)) / D.S2.card)
Uses 1 · Used by 2
Statement usesBivariate LD-score model
Used byCross-trait scaled-score identity, exact form · Equal normalized-cross-product specialization of the residual cross-moment identity

TheoremCross-trait scaled-score identity, exact form#✓fully proved

With N₁ = |S₁|, N₂ = |S₂|, 𝔼[z₁ j z₂ j] = √(N₁ N₂) (ρ_g / M) ∑_k r¹ j k r² j k + ρ_e (∑_{i ∈ S₁ ∩ S₂} X i j ²) / √(N₁ N₂), with the in-sample normalized cross products r¹, r² (sampleCorr).

theorem integral_z_mul_z (j : Fin M) :
    ∫ ω, D.z1 X j ω * D.z2 X j ω ∂μ =
      √((D.S1.card : ℝ) * D.S2.card) * (D.rhoG / M) *
          ∑ k, sampleCorr X D.S1 j k * sampleCorr X D.S2 j k +
        D.rhoE * (∑ i ∈ D.S1 ∩ D.S2, X i j ^ 2) / √((D.S1.card : ℝ) * D.S2.card)
Uses 4 · Used by 1
Statement usesBivariate LD-score model · Scaled marginal score for the first trait · Scaled marginal score for the second trait · In-sample LD correlation
Used byEqual normalized-cross-product specialization of the residual cross-moment identity

TheoremEqual normalized-cross-product specialization of the residual cross-moment identity#✓fully proved

If the two samples have the same normalized cross products with marker j and the overlap marker is standardized at j (∑_{i ∈ S₁ ∩ S₂} X i j ² = N_s), then 𝔼[z₁ j z₂ j] = √(N₁ N₂) ρ_g ℓ_j / M + ρ_e N_s / √(N₁ N₂). Here ρ_e is only the residual cross-moment specified by CrossTraitModel; this theorem does not state the Bulik-Sullivan phenotypic-correlation overlap formula or establish z-score normalization.

theorem integral_z_mul_z_of_sameLD (j : Fin M)
    (hLD : ∀ k, sampleCorr X D.S1 j k = sampleCorr X D.S2 j k)
    (hs : ∑ i ∈ D.S1 ∩ D.S2, X i j ^ 2 = (D.S1 ∩ D.S2).card) :
    ∫ ω, D.z1 X j ω * D.z2 X j ω ∂μ =
      √((D.S1.card : ℝ) * D.S2.card) * D.rhoG * (∑ k, sampleCorr X D.S1 j k ^ 2) / M +
        D.rhoE * (D.S1 ∩ D.S2).card / √((D.S1.card : ℝ) * D.S2.card)
Uses 5
Statement usesBivariate LD-score model · Scaled marginal score for the first trait · Scaled marginal score for the second trait · In-sample LD correlation
Proof usesCross-trait scaled-score identity, exact form

The Cochran–Armitage trend test

DefinitionNumber of individuals in a case-control genotype table#✓fully proved

The number of individuals N = ∑ (r i + s i).

def total : ℝ := ∑ i, (r i + s i)
Used by 8
Used byPooled allele frequency · The allelic test equals the trend test iff the pooled sample is in Hardy–Weinberg proportions · Allelic versus trend test · Squared correlation of case status and genotype score · Pooled genotype-score variance · Departure of the genotype-score variance from Hardy–Weinberg · Cochran–Armitage trend statistic · The trend test is N r²

DefinitionNumerator of the Cochran–Armitage trend statistic#✓fully proved

The trend numerator U = ∑ i, i (r i S - s i R) with R = ∑ r, S = ∑ s.

def numer : ℝ := ∑ i : Fin 3, ((i : ℕ) : ℝ) * (r i * ∑ j, s j - s i * ∑ j, r j)
Used by 4
Used byThe allelic test equals the trend test iff the pooled sample is in Hardy–Weinberg proportions · Allelic versus trend test · Cochran–Armitage trend statistic · The trend test is N r²

DefinitionPooled genotype-score variance#✓fully proved

The pooled genotype-score variance ∑ i² n_i / N - (∑ i n_i / N)², n_i = r i + s i.

noncomputable def scoreVar : ℝ :=
  (∑ i : Fin 3, ((i : ℕ) : ℝ) ^ 2 * (r i + s i)) / total r s -
    ((∑ i : Fin 3, ((i : ℕ) : ℝ) * (r i + s i)) / total r s) ^ 2
Uses 1 · Used by 5
Statement usesNumber of individuals in a case-control genotype table
Used byThe allelic test equals the trend test iff the pooled sample is in Hardy–Weinberg proportions · Allelic versus trend test · Squared correlation of case status and genotype score · Departure of the genotype-score variance from Hardy–Weinberg · The trend test is N r²

DefinitionCochran–Armitage trend statistic#✓fully proved

The Cochran–Armitage trend statistic with scores 0, 1, 2 (Armitage 1955): N U² / (R S (N ∑ i² n_i - (∑ i n_i)²)).

noncomputable def trendStat : ℝ :=
  total r s * numer r s ^ 2 / ((∑ i, r i) * (∑ i, s i) *
    (total r s * ∑ i : Fin 3, ((i : ℕ) : ℝ) ^ 2 * (r i + s i) -
      (∑ i : Fin 3, ((i : ℕ) : ℝ) * (r i + s i)) ^ 2))
Uses 2 · Used by 3
Statement usesNumerator of the Cochran–Armitage trend statistic · Number of individuals in a case-control genotype table
Used byThe allelic test equals the trend test iff the pooled sample is in Hardy–Weinberg proportions · Allelic versus trend test · The trend test is N r²

DefinitionSquared correlation of case status and genotype score#✓fully proved

The squared sample correlation of case status (1 for cases, 0 for controls) and the genotype score over the N individuals of the table.

noncomputable def corrSq : ℝ :=
  ((∑ i : Fin 3, ((i : ℕ) : ℝ) * r i) / total r s -
      (∑ i, r i) / total r s * ((∑ i : Fin 3, ((i : ℕ) : ℝ) * (r i + s i)) / total r s)) ^ 2 /
    (((∑ i, r i) / total r s - ((∑ i, r i) / total r s) ^ 2) * scoreVar r s)
Uses 2 · Used by 1
Statement usesPooled genotype-score variance · Number of individuals in a case-control genotype table
Used byThe trend test is N r²

DefinitionPooled allele frequency#✓fully proved

The pooled frequency p = ∑ i n_i / (2 N) of the counted allele.

noncomputable def alleleFreq : ℝ :=
  (∑ i : Fin 3, ((i : ℕ) : ℝ) * (r i + s i)) / (2 * total r s)
Uses 1 · Used by 3
Statement usesNumber of individuals in a case-control genotype table
Used byThe allelic test equals the trend test iff the pooled sample is in Hardy–Weinberg proportions · Allelic versus trend test · Departure of the genotype-score variance from Hardy–Weinberg

DefinitionPearson's chi-squared statistic of a 2 × 2 table#✓fully proved

Pearson's statistic n (a d - b c)² / ((a + b)(c + d)(a + c)(b + d)) of a 2 × 2 table [[a, b], [c, d]] with n = a + b + c + d.

noncomputable def pearson2x2 (a b c d : ℝ) : ℝ :=
  (a + b + c + d) * (a * d - b * c) ^ 2 / ((a + b) * (c + d) * (a + c) * (b + d))
Used by 2
Used byAllelic test statistic · Allelic versus trend test

DefinitionAllelic test statistic#✓fully proved

The allelic test: Pearson's statistic of the 2 × 2 table of case and control allele counts (2N alleles).

noncomputable def allelicStat : ℝ :=
  pearson2x2 (∑ i : Fin 3, ((i : ℕ) : ℝ) * r i) (2 * ∑ i, r i - ∑ i : Fin 3, ((i : ℕ) : ℝ) * r i)
    (∑ i : Fin 3, ((i : ℕ) : ℝ) * s i) (2 * ∑ i, s i - ∑ i : Fin 3, ((i : ℕ) : ℝ) * s i)
Uses 1 · Used by 2
Statement usesPearson's chi-squared statistic of a 2 × 2 table
Used byThe allelic test equals the trend test iff the pooled sample is in Hardy–Weinberg proportions · Allelic versus trend test

TheoremThe trend test is N r²#✓fully proved

The trend test is N r² (Armitage 1955): the Cochran–Armitage statistic is N times the squared sample correlation of case status and genotype score. (In degenerate tables, where a denominator vanishes, both sides are 0 by the convention x / 0 = 0.)

theorem trendStat_eq_total_mul_corrSq : trendStat r s = total r s * corrSq r s
Uses 5
Statement usesSquared correlation of case status and genotype score · Number of individuals in a case-control genotype table · Cochran–Armitage trend statistic
Proof usesNumerator of the Cochran–Armitage trend statistic · Pooled genotype-score variance

TheoremDeparture of the genotype-score variance from Hardy–Weinberg#✓fully proved

The observed score variance minus the Hardy–Weinberg score variance 2 p q: Var - 2 p (1 - p) = (4 n₀ n₂ - n₁²) / (2 N²).

theorem scoreVar_sub_hweVar (hN : total r s ≠ 0) :
    scoreVar r s - 2 * alleleFreq r s * (1 - alleleFreq r s) =
      (4 * (r 0 + s 0) * (r 2 + s 2) - (r 1 + s 1) ^ 2) / (2 * total r s ^ 2)
Uses 3 · Used by 1
Statement usesPooled allele frequency · Pooled genotype-score variance · Number of individuals in a case-control genotype table
Used byThe allelic test equals the trend test iff the pooled sample is in Hardy–Weinberg proportions

TheoremAllelic versus trend test#✓fully proved

Allelic versus trend test (Sasieni 1997): with cases and controls present, a pooled allele frequency strictly between 0 and 1 and a positive score variance, allelic · 2 p q = trend · Var.

theorem allelicStat_mul_hweVar (hR : 0 < ∑ i, r i) (hS : 0 < ∑ i, s i)
    (hp0 : 0 < alleleFreq r s) (hp1 : alleleFreq r s < 1) (hV : 0 < scoreVar r s) :
    allelicStat r s * (2 * alleleFreq r s * (1 - alleleFreq r s)) =
      trendStat r s * scoreVar r s
Uses 7 · Used by 1
Statement usesPooled allele frequency · Allelic test statistic · Pooled genotype-score variance · Cochran–Armitage trend statistic
Proof usesNumerator of the Cochran–Armitage trend statistic · Pearson's chi-squared statistic of a 2 × 2 table · Number of individuals in a case-control genotype table
Used byThe allelic test equals the trend test iff the pooled sample is in Hardy–Weinberg proportions

TheoremThe allelic test equals the trend test iff the pooled sample is in Hardy–Weinberg proportions#✓fully proved

The allelic test equals the trend test iff the pooled sample is in Hardy–Weinberg proportions (n₁² = 4 n₀ n₂; Sasieni 1997), whenever the trend numerator is nonzero.

theorem allelicStat_eq_trendStat_iff (hR : 0 < ∑ i, r i) (hS : 0 < ∑ i, s i)
    (hp0 : 0 < alleleFreq r s) (hp1 : alleleFreq r s < 1) (hV : 0 < scoreVar r s)
    (hU : numer r s ≠ 0) :
    allelicStat r s = trendStat r s ↔
      (r 1 + s 1) ^ 2 = 4 * (r 0 + s 0) * (r 2 + s 2)
Uses 8
Statement usesPooled allele frequency · Allelic test statistic · Numerator of the Cochran–Armitage trend statistic · Pooled genotype-score variance · Cochran–Armitage trend statistic
Proof usesAllelic versus trend test · Departure of the genotype-score variance from Hardy–Weinberg · Number of individuals in a case-control genotype table

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.