LD-score regression

DefinitionNormalized cross product of genotype markers#✓fully proved

The normalized cross product r j k = X_jᵀ X_k / N of markers j and k. For a standardized genotype matrix (IsStandardized) it is the sample correlation of the two markers; for other matrices it is only a scale-dependent dot product.

noncomputable def ldCorr (X : Matrix (Fin N) (Fin M) ℝ) (j k : Fin M) : ℝ :=
  (∑ i, X i j * X i k) / N

Used by 18

Used byThe mean of the marginal estimates · The raw residual-product second moment of the marginal estimates · Expected association statistic in the stratified LD-score model · One causal variant · Stratified LD score · Expected association statistic for an arbitrary genotype matrix · A standardized marker has correlation one with itself · Correlations of standardized markers lie in (-1, 1) · LD score of a marker · First-moment identity, exact in-sample form · Unbiasedness of the weighted least-squares estimator · Unbiasedness with covariates · In-sample LD matrix · Annotation LD score of a marker · Expected statistic with per-marker variances · Frequency-dependent architecture · Stratified LD-score regression · Expected chi-squared statistic of a standardized marker

DefinitionLD score of a marker#✓fully proved

The LD score ℓ j = ∑ k, r j k ^ 2 of marker j (an LD score in the sense of the cited paper for a standardized genotype matrix).

noncomputable def ldScore (X : Matrix (Fin N) (Fin M) ℝ) (j : Fin M) : ℝ :=
  ∑ k, ldCorr X j k ^ 2

Uses 1 · Used by 8

Statement usesNormalized cross product of genotype markers

Used byExpected association statistic for an arbitrary genotype matrix · LD-score regression · Expected association statistic under stratification · LD-score regression with constant stratification · Expected statistic under stratification for standardized genotypes · Polygenic inflation of the mean association statistic · Mean association statistic with constant stratification · Mean LD score

DefinitionStandardized genotype matrix#✓fully proved

The genotype matrix is standardized: every marker column has mean 0 and sum of squares N (unit sample variance).

def IsStandardized (X : Matrix (Fin N) (Fin M) ℝ) : Prop :=
  ∀ k, ∑ i, X i k = 0 ∧ ∑ i, X i k ^ 2 = N

Used by 15

Used byStratified LD-score regression · One causal variant · Attenuation ratio under constant stratification · Confounding share of inflation under constant stratification · LD-score regression · LD-score regression with constant stratification · Expected statistic under stratification for standardized genotypes · A standardized marker has correlation one with itself · Correlations of standardized markers lie in (-1, 1) · Polygenic inflation of the mean association statistic · Mean association statistic with constant stratification · Expected statistics are the design matrix times the parameters · Frequency-dependent architecture · Stratified LD-score regression · Expected chi-squared statistic of a standardized marker

TheoremA standardized marker has correlation one with itself#✓fully proved

For a standardized matrix each marker has correlation 1 with itself.

theorem IsStandardized.ldCorr_self {X : Matrix (Fin N) (Fin M) ℝ} (hX : IsStandardized X)
    (hN : N ≠ 0) (k : Fin M) : ldCorr X k k = 1

Uses 2

Statement usesStandardized genotype matrix · Normalized cross product of genotype markers

TheoremCorrelations of standardized markers lie in (-1, 1)#✓fully proved

For a standardized matrix the correlations lie in [-1, 1] (Cauchy–Schwarz).

theorem IsStandardized.ldCorr_sq_le_one {X : Matrix (Fin N) (Fin M) ℝ} (hX : IsStandardized X)
    (j k : Fin M) : ldCorr X j k ^ 2 ≤ 1

Uses 2

Statement usesStandardized genotype matrix · Normalized cross product of genotype markers

StructureRandom-effects model of LD-score regression#✓fully proved

The random-effects model of LD-score regression (Bulik-Sullivan et al. 2015), stated at the level of raw second moments, for N individuals and M markers with heritability h2.

• beta k is the (random) effect of marker k, with ∫ β k * β l = h2 / M * [k = l];
• eps i is the environmental noise of individual i, with ∫ ε i * ε i' = (1 - h2) * [i = i'];
• effects and noise are orthogonal in L².

The measure is arbitrary and no means are assumed; for a probability measure and mean-zero effects and noise these are the covariance conditions of the cited model. The genotype matrix is not part of the model: all expectations are conditional on it.

MathlibExt.Biology.StatisticalGenetics.LDScore.Model · 17 lines

structure Model (μ : Measure Ω) (N M : ℕ) where
  /-- The SNP heritability `h²`. -/
  h2 : ℝ
  /-- Random per-marker effect sizes. -/
  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 μ
  /-- Raw second moments of the effects: `∫ β βᵀ = (h² / M) I`. -/
  integral_beta_mul : ∀ k l, ∫ ω, beta k ω * beta l ω ∂μ = if k = l then h2 / M else 0
  /-- Raw second moments of the noise: `∫ ε εᵀ = (1 - h²) I`. -/
  integral_eps_mul : ∀ i i', ∫ ω, eps i ω * eps i' ω ∂μ = if i = i' then 1 - h2 else 0
  /-- Effects and noise are orthogonal in `L²`: `∫ β εᵀ = 0`. -/
  integral_beta_mul_eps : ∀ k i, ∫ ω, beta k ω * eps i ω ∂μ = 0

Used by 22

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 · Attenuation ratio under constant stratification · Normalized marginal score in the LD-score model · Normalized score under stratification · Association statistic in the LD-score model · Association statistic under stratification · Confounding share of inflation under constant stratification · Heritability is at most one in the LD-score model · Nonnegativity of heritability in the LD-score model · Expected association statistic for an arbitrary genotype matrix · LD-score regression · Expected association statistic under stratification · LD-score regression with constant stratification · Expected statistic under stratification for standardized genotypes · Polygenic inflation of the mean association statistic · Mean association statistic with constant stratification · Phenotype in the LD-score model · Phenotype with population stratification · Stratified statistic agrees with the LD-score statistic · LD-score regression model as a stratified model

TheoremNonnegativity of heritability in the LD-score model#✓fully proved

The heritability is nonnegative when there is at least one marker.

theorem h2_nonneg (hM : 0 < M) : 0 ≤ D.h2

Uses 1

Statement usesRandom-effects model of LD-score regression

TheoremHeritability is at most one in the LD-score model#✓fully proved

The heritability is at most 1 when there is at least one individual.

theorem h2_le_one (hN : 0 < N) : D.h2 ≤ 1

Uses 1

Statement usesRandom-effects model of LD-score regression

DefinitionPhenotype in the 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 5

Statement usesRandom-effects model of LD-score regression

Used byEstimates of the derived model are normalized scores · Normalized marginal score in the LD-score model · Expected association statistic for an arbitrary genotype matrix · Expected association statistic under stratification · Phenotype with population stratification

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

The N-normalized score β̂ j = X_jᵀ y / N of marker j. For a standardized column (∑ i, X i j ^ 2 = N) it is the marginal least-squares estimate of the effect of marker j; in general that estimate has denominator ∑ i, X i j ^ 2 instead of N.

noncomputable def betaHat (j : Fin M) (ω : Ω) : ℝ := (∑ i, X i j * D.pheno X i ω) / N

Uses 2 · Used by 4

Statement usesRandom-effects model of LD-score regression · Phenotype in the LD-score model

Used byEstimates of the derived model are normalized scores · Association statistic in the LD-score model · Expected association statistic for an arbitrary genotype matrix · Expected association statistic under stratification

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

The association statistic χ² j = N * β̂ j ^ 2 of marker j.

noncomputable def chiSq (j : Fin M) (ω : Ω) : ℝ := N * D.betaHat X j ω ^ 2

Uses 2 · Used by 5

Statement usesRandom-effects model of LD-score regression · Normalized marginal score in the LD-score model

Used byExpected association statistic for an arbitrary genotype matrix · LD-score regression · Expected association statistic under stratification · Polygenic inflation of the mean association statistic · Stratified statistic agrees with the LD-score statistic

TheoremExpected association statistic for an arbitrary genotype matrix#✓fully proved

The exact expectation of the association statistic built from the N-normalized score, for an arbitrary genotype matrix: 𝔼[χ² j] = N h² / M * ℓ j + (1 - h²) * (∑ i, X i j ^ 2) / N. (For N = 0 both sides are 0 by the convention x / 0 = 0.)

theorem integral_chiSq (j : Fin M) :
    ∫ ω, D.chiSq X j ω ∂μ =
      N * D.h2 / M * ldScore X j + (1 - D.h2) * (∑ i, X i j ^ 2) / N

Uses 6 · Used by 2

Statement usesRandom-effects model of LD-score regression · Association statistic in the LD-score model · LD score of a marker

Proof usesNormalized marginal score in the LD-score model · Phenotype in the LD-score model · Normalized cross product of genotype markers

Used byLD-score regression · Expected association statistic under stratification

TheoremLD-score regression#✓fully proved

LD-score regression (Bulik-Sullivan et al. 2015): for a standardized genotype matrix (IsStandardized, so that ldCorr is the sample correlation and ldScore the LD score) and N ≠ 0, 𝔼[χ² j] = N h² / M * ℓ j + (1 - h²). The expected association statistic is affine in the LD score, with slope N h² / M and intercept 1 - h². The proof uses only that column j has sum of squares N; the rest of the standardization is what makes ℓ j an LD score.

theorem integral_chiSq_of_standardized (hN : N ≠ 0) (j : Fin M) (hX : IsStandardized X) :
    ∫ ω, D.chiSq X j ω ∂μ = N * D.h2 / M * ldScore X j + (1 - D.h2)

Uses 5 · Used by 1

Statement usesStandardized genotype matrix · Random-effects model of LD-score regression · Association statistic in the LD-score model · LD score of a marker

Proof usesExpected association statistic for an arbitrary genotype matrix

Used byPolygenic inflation of the mean association statistic

DefinitionMean LD score#✓fully proved

The mean LD score ℓ̄ = (1 / M) ∑ j, ℓ j.

noncomputable def meanLDScore (X : Matrix (Fin N) (Fin M) ℝ) : ℝ := (∑ j, ldScore X j) / M

Uses 1 · Used by 4

Statement usesLD score of a marker

Used byAttenuation ratio under constant stratification · Confounding share of inflation under constant stratification · Polygenic inflation of the mean association statistic · Mean association statistic with constant stratification

TheoremPolygenic inflation of the mean association statistic#✓fully proved

Polygenic inflation: for a standardized genotype matrix with N, M ≠ 0, the mean expected association statistic is 1 - h² + N h² ℓ̄ / M.

theorem mean_integral_chiSq (D : Model μ N M) (X : Matrix (Fin N) (Fin M) ℝ) (hN : N ≠ 0)
    (hM : M ≠ 0) (hX : IsStandardized X) :
    (∑ j, ∫ ω, D.chiSq X j ω ∂μ) / M = 1 - D.h2 + N * D.h2 / M * meanLDScore X

Uses 6

Statement usesStandardized genotype matrix · Random-effects model of LD-score regression · Association statistic in the LD-score model · Mean LD score

Proof usesLD-score regression · LD score of a marker

DefinitionPhenotype with population stratification#✓fully proved

The phenotype with a stratification shift: y i = (X β) i + ε i + s * c i.

def phenoStrat (D : Model μ N M) (X : Matrix (Fin N) (Fin M) ℝ) (s : ℝ) (c : Fin N → ℝ)
    (i : Fin N) (ω : Ω) : ℝ := D.pheno X i ω + s * c i

Uses 2 · Used by 2

Statement usesRandom-effects model of LD-score regression · Phenotype in the LD-score model

Used byNormalized score under stratification · Expected association statistic under stratification

DefinitionNormalized score under stratification#✓fully proved

The N-normalized score of marker j under stratification, X_jᵀ y / N.

noncomputable def betaHatStrat (D : Model μ N M) (X : Matrix (Fin N) (Fin M) ℝ) (s : ℝ)
    (c : Fin N → ℝ) (j : Fin M) (ω : Ω) : ℝ := (∑ i, X i j * phenoStrat D X s c i ω) / N

Uses 2 · Used by 2

Statement usesRandom-effects model of LD-score regression · Phenotype with population stratification

Used byAssociation statistic under stratification · Expected association statistic under stratification

DefinitionAssociation statistic under stratification#✓fully proved

The association statistic N * β̂ j ^ 2 under stratification.

noncomputable def chiSqStrat (D : Model μ N M) (X : Matrix (Fin N) (Fin M) ℝ) (s : ℝ)
    (c : Fin N → ℝ) (j : Fin M) (ω : Ω) : ℝ := N * betaHatStrat D X s c j ω ^ 2

Uses 2 · Used by 6

Statement usesRandom-effects model of LD-score regression · Normalized score under stratification

Used byAttenuation ratio under constant stratification · Confounding share of inflation under constant stratification · Expected association statistic under stratification · LD-score regression with constant stratification · Expected statistic under stratification for standardized genotypes · Mean association statistic with constant stratification

TheoremExpected association statistic under stratification#✓fully proved

Stratification inflation: for a probability measure and mean-zero effects and noise, 𝔼[χ² j] = N h² / M * ℓ j + (1 - h²) (∑ i, X i j ^ 2) / N + N s² (X_jᵀ c / N)².

theorem integral_chiSqStrat [IsProbabilityMeasure μ] (D : Model μ N M)
    (X : Matrix (Fin N) (Fin M) ℝ) (hβ : ∀ k, ∫ ω, D.beta k ω ∂μ = 0)
    (hε : ∀ i, ∫ ω, D.eps i ω ∂μ = 0) (s : ℝ) (c : Fin N → ℝ) (j : Fin M) :
    ∫ ω, chiSqStrat D X s c j ω ∂μ =
      N * D.h2 / M * ldScore X j + (1 - D.h2) * (∑ i, X i j ^ 2) / N +
        N * s ^ 2 * ((∑ i, X i j * c i) / N) ^ 2

Uses 9 · Used by 1

Statement usesRandom-effects model of LD-score regression · LD score of a marker · Association statistic under stratification

Proof usesNormalized marginal score in the LD-score model · Association statistic in the LD-score model · Expected association statistic for an arbitrary genotype matrix · Phenotype in the LD-score model · Normalized score under stratification · Phenotype with population stratification

Used byExpected statistic under stratification for standardized genotypes

TheoremExpected statistic under stratification for standardized genotypes#✓fully proved

Stratification inflation for a standardized genotype matrix and N ≠ 0: 𝔼[χ² j] = N h² / M * ℓ j + (1 - h²) + N s² (X_jᵀ c / N)².

theorem integral_chiSqStrat_of_standardized [IsProbabilityMeasure μ] (D : Model μ N M)
    (X : Matrix (Fin N) (Fin M) ℝ) (hN : N ≠ 0) (hX : IsStandardized X)
    (hβ : ∀ k, ∫ ω, D.beta k ω ∂μ = 0) (hε : ∀ i, ∫ ω, D.eps i ω ∂μ = 0) (s : ℝ)
    (c : Fin N → ℝ) (j : Fin M) :
    ∫ ω, chiSqStrat D X s c j ω ∂μ =
      N * D.h2 / M * ldScore X j + (1 - D.h2) + N * s ^ 2 * ((∑ i, X i j * c i) / N) ^ 2

Uses 5 · Used by 1

Statement usesStandardized genotype matrix · Random-effects model of LD-score regression · LD score of a marker · Association statistic under stratification

Proof usesExpected association statistic under stratification

Used byLD-score regression with constant stratification

TheoremLD-score regression with constant stratification#✓fully proved

With a constant stratification term (s² (X_jᵀ c / N)² = a for every marker), the expected statistic is exactly affine in the LD score, with slope N h² / M and intercept 1 - h² + N a.

theorem integral_chiSqStrat_of_const [IsProbabilityMeasure μ] (D : Model μ N M)
    (X : Matrix (Fin N) (Fin M) ℝ) (hN : N ≠ 0) (hX : IsStandardized X)
    (hβ : ∀ k, ∫ ω, D.beta k ω ∂μ = 0) (hε : ∀ i, ∫ ω, D.eps i ω ∂μ = 0) (s : ℝ)
    (c : Fin N → ℝ) {a : ℝ} (ha : ∀ j, s ^ 2 * ((∑ i, X i j * c i) / N) ^ 2 = a) (j : Fin M) :
    ∫ ω, chiSqStrat D X s c j ω ∂μ = N * D.h2 / M * ldScore X j + (1 - D.h2 + N * a)

Uses 5 · Used by 1

Statement usesStandardized genotype matrix · Random-effects model of LD-score regression · LD score of a marker · Association statistic under stratification

Proof usesExpected statistic under stratification for standardized genotypes

Used byMean association statistic with constant stratification

TheoremMean association statistic with constant stratification#✓fully proved

With a constant stratification term N a, the mean expected statistic is N h² ℓ̄ / M + (1 - h² + N a).

theorem mean_integral_chiSqStrat_of_const [IsProbabilityMeasure μ] (D : Model μ N M)
    (X : Matrix (Fin N) (Fin M) ℝ) (hN : N ≠ 0) (hM : M ≠ 0) (hX : IsStandardized X)
    (hβ : ∀ k, ∫ ω, D.beta k ω ∂μ = 0) (hε : ∀ i, ∫ ω, D.eps i ω ∂μ = 0) (s : ℝ)
    (c : Fin N → ℝ) {a : ℝ} (ha : ∀ j, s ^ 2 * ((∑ i, X i j * c i) / N) ^ 2 = a) :
    (∑ j, ∫ ω, chiSqStrat D X s c j ω ∂μ) / M =
      N * D.h2 / M * meanLDScore X + (1 - D.h2 + N * a)

Uses 6 · Used by 2

Statement usesStandardized genotype matrix · Random-effects model of LD-score regression · Association statistic under stratification · Mean LD score

Proof usesLD score of a marker · LD-score regression with constant stratification

Used byAttenuation ratio under constant stratification · Confounding share of inflation under constant stratification

DefinitionAttenuation ratio#✓fully proved

The attenuation ratio (intercept - 1) / (mean χ² - 1) of Loh et al. (2018).

noncomputable def attenuationRatio (intercept meanChiSq : ℝ) : ℝ :=
  (intercept - 1) / (meanChiSq - 1)

Used by 1

Used byAttenuation ratio under constant stratification

TheoremAttenuation ratio under constant stratification#✓fully proved

With a constant stratification term N a, the attenuation ratio of the exact intercept 1 - h² + N a and the mean expected statistic is (N a - h²) / (N h² ℓ̄ / M + N a - h²).

theorem attenuationRatio_of_const [IsProbabilityMeasure μ] (D : Model μ N M)
    (X : Matrix (Fin N) (Fin M) ℝ) (hN : N ≠ 0) (hM : M ≠ 0) (hX : IsStandardized X)
    (hβ : ∀ k, ∫ ω, D.beta k ω ∂μ = 0) (hε : ∀ i, ∫ ω, D.eps i ω ∂μ = 0) (s : ℝ)
    (c : Fin N → ℝ) {a : ℝ} (ha : ∀ j, s ^ 2 * ((∑ i, X i j * c i) / N) ^ 2 = a) :
    attenuationRatio (1 - D.h2 + N * a) ((∑ j, ∫ ω, chiSqStrat D X s c j ω ∂μ) / M) =
      (N * a - D.h2) / (N * D.h2 / M * meanLDScore X + N * a - D.h2)

Uses 6

Statement usesStandardized genotype matrix · Random-effects model of LD-score regression · Attenuation ratio · Association statistic under stratification · Mean LD score

Proof usesMean association statistic with constant stratification

TheoremConfounding share of inflation under constant stratification#✓fully proved

With a constant stratification term N a, the share of the mean inflation above the exact null level 1 - h² that is due to stratification is N a / (N a + N h² ℓ̄ / M).

theorem confoundingShare_of_const [IsProbabilityMeasure μ] (D : Model μ N M)
    (X : Matrix (Fin N) (Fin M) ℝ) (hN : N ≠ 0) (hM : M ≠ 0) (hX : IsStandardized X)
    (hβ : ∀ k, ∫ ω, D.beta k ω ∂μ = 0) (hε : ∀ i, ∫ ω, D.eps i ω ∂μ = 0) (s : ℝ)
    (c : Fin N → ℝ) {a : ℝ} (ha : ∀ j, s ^ 2 * ((∑ i, X i j * c i) / N) ^ 2 = a) :
    ((1 - D.h2 + N * a) - (1 - D.h2)) /
        ((∑ j, ∫ ω, chiSqStrat D X s c j ω ∂μ) / M - (1 - D.h2)) =
      N * a / (N * a + N * D.h2 / M * meanLDScore X)

Uses 5

Statement usesStandardized genotype matrix · Random-effects model of LD-score regression · Association statistic under stratification · Mean LD score

Proof usesMean association statistic with constant stratification

TheoremConfounding share lies between 0 and 1#✓fully proved

The confounding share N a / (N a + N h² ℓ̄ / M) lies in [0, 1] when a, h² and ℓ̄ are nonnegative (as they are in the model: a is a square, h² ≥ 0 by Model.h2_nonneg, LD scores are sums of squares).

theorem confoundingShare_mem_Icc {a h2 lbar : ℝ} (ha : 0 ≤ a) (hh : 0 ≤ h2) (hl : 0 ≤ lbar) :
    N * a / (N * a + N * h2 / M * lbar) ∈ Set.Icc 0 1

26 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.