Stratified LD-score regression

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

The random-effects model of stratified LD-score regression at the level of raw second moments: marker k has effect variance sigma2 k, the noise has variance sigmaE2, and effects and noise are orthogonal in L². As in LDScore.Model, the measure is arbitrary, no means are assumed, and all statements are conditional on the genotype matrix.

MathlibExt.Biology.StatisticalGenetics.StratifiedLDScore.Model · 19 lines

structure Model (μ : Measure Ω) (N M : ℕ) where
  /-- The per-marker effect variance `σ²_k`. -/
  sigma2 : Fin M → ℝ
  /-- The noise variance `σ²_e`. -/
  sigmaE2 : ℝ
  /-- 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: `∫ β βᵀ = diag σ²`. -/
  integral_beta_mul : ∀ k l, ∫ ω, beta k ω * beta l ω ∂μ = if k = l then sigma2 k else 0
  /-- Raw second moments of the noise: `∫ ε εᵀ = σ²_e I`. -/
  integral_eps_mul : ∀ i i', ∫ ω, eps i ω * eps i' ω ∂μ = if i = i' then sigmaE2 else 0
  /-- Effects and noise are orthogonal in `L²`. -/
  integral_beta_mul_eps : ∀ k i, ∫ ω, beta k ω * eps i ω ∂μ = 0

Used by 9

Used byNormalized marker score in stratified LD-score regression · Association chi-squared statistic in stratified LD-score regression · Expected statistic with per-marker variances · Expected statistics are the design matrix times the parameters · Frequency-dependent architecture · Stratified LD-score regression · Expected chi-squared statistic of a standardized marker · LD-score regression model as a stratified model · 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 usesRandom-effects model of stratified LD-score regression

Used byNormalized marker score in stratified LD-score regression · Expected statistic with per-marker variances

DefinitionNormalized marker score in stratified LD-score regression#✓fully proved

The N-normalized score β̂ j = X_jᵀ y / N of marker j (as in LDScore.Model.betaHat).

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

Uses 2 · Used by 2

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

Used byAssociation chi-squared statistic in stratified LD-score regression · Expected statistic with per-marker variances

DefinitionAssociation chi-squared statistic in stratified LD-score regression#✓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 6

Statement usesRandom-effects model of stratified LD-score regression · Normalized marker score in stratified LD-score regression

Used byStratified statistic agrees with the LD-score statistic · Expected statistic with per-marker variances · Expected statistics are the design matrix times the parameters · Frequency-dependent architecture · Stratified LD-score regression · Expected chi-squared statistic of a standardized marker

DefinitionLD-score regression model as a stratified model#✓fully proved

The LD-score regression model of LDScore is the stratified model with equal per-marker variances h² / M and noise variance 1 - h².

noncomputable def ofLDScore (D : LDScore.Model μ N M) : Model μ N M where
  sigma2 := fun _ => D.h2 / M
  sigmaE2 := 1 - D.h2
  beta := D.beta
  eps := D.eps
  memLp_beta := D.memLp_beta
  memLp_eps := D.memLp_eps
  integral_beta_mul := D.integral_beta_mul
  integral_eps_mul := D.integral_eps_mul
  integral_beta_mul_eps := D.integral_beta_mul_eps

Uses 2 · Used by 1

Statement usesRandom-effects model of LD-score regression · Random-effects model of stratified LD-score regression

Used byStratified statistic agrees with the LD-score statistic

TheoremStratified statistic agrees with the LD-score statistic#✓fully proved

The stratified statistic of ofLDScore D is the statistic of LDScore.

theorem chiSq_ofLDScore (D : LDScore.Model μ N M) : (ofLDScore D).chiSq X = D.chiSq X

Uses 4

Statement usesRandom-effects model of LD-score regression · Association statistic in the LD-score model · Association chi-squared statistic in stratified LD-score regression · LD-score regression model as a stratified model

TheoremExpected statistic with per-marker variances#✓fully proved

Expected statistic with per-marker variances, for an arbitrary genotype matrix: 𝔼[χ² j] = N ∑_k r_jk² σ²_k + σ²_e (∑_i X_ij²) / N. (For N = 0 both sides are 0.)

theorem integral_chiSq (j : Fin M) :
    ∫ ω, D.chiSq X j ω ∂μ =
      N * ∑ k, ldCorr X j k ^ 2 * D.sigma2 k + D.sigmaE2 * (∑ i, X i j ^ 2) / N

Uses 5 · Used by 1

Statement usesNormalized cross product of genotype markers · Random-effects model of stratified LD-score regression · Association chi-squared statistic in stratified LD-score regression

Proof usesNormalized marker score in stratified LD-score regression · Phenotype in the stratified LD-score model

Used byExpected chi-squared statistic of a standardized marker

TheoremExpected chi-squared statistic of a standardized marker#✓fully proved

For a column with sum of squares N (a standardized marker) and N ≠ 0: 𝔼[χ² j] = N ∑_k r_jk² σ²_k + σ²_e.

theorem integral_chiSq_of_standardized (hN : N ≠ 0) (j : Fin M) (hX : IsStandardized X) :
    ∫ ω, D.chiSq X j ω ∂μ = N * ∑ k, ldCorr X j k ^ 2 * D.sigma2 k + D.sigmaE2

Uses 5 · Used by 1

Statement usesStandardized genotype matrix · Normalized cross product of genotype markers · Random-effects model of stratified LD-score regression · Association chi-squared statistic in stratified LD-score regression

Proof usesExpected statistic with per-marker variances

Used byStratified LD-score regression

DefinitionAnnotation LD score of a marker#✓fully proved

The LD score of marker j with respect to annotation C: ℓ(j, C) = ∑_k a_{kC} r_jk² (Finucane et al. 2015 for binary annotations; Gazal et al. 2017 for continuous ones).

noncomputable def annotLDScore {ι : Type*} (X : Matrix (Fin N) (Fin M) ℝ) (a : Fin M → ι → ℝ)
    (j : Fin M) (C : ι) : ℝ :=
  ∑ k, a k C * ldCorr X j k ^ 2

Uses 1 · Used by 4

Statement usesNormalized cross product of genotype markers

Used byDesign matrix of stratified LD-score regression · Expected statistics are the design matrix times the parameters · Frequency-dependent architecture · Stratified LD-score regression

TheoremStratified LD-score regression#✓fully proved

Stratified LD-score regression (Finucane et al. 2015; continuous annotations, Gazal et al. 2017): if the per-marker variances are linear in the annotations, σ²_k = ∑_C τ_C a_{kC}, then for a standardized genotype matrix and N ≠ 0, 𝔼[χ² j] = N ∑_C τ_C ℓ(j, C) + σ²_e.

theorem integral_chiSq_of_annot {ι : Type*} [Fintype ι] (a : Fin M → ι → ℝ) (τ : ι → ℝ)
    (hσ : ∀ k, D.sigma2 k = ∑ C, τ C * a k C) (hN : N ≠ 0) (j : Fin M)
    (hX : IsStandardized X) :
    ∫ ω, D.chiSq X j ω ∂μ = N * ∑ C, τ C * annotLDScore X a j C + D.sigmaE2

Uses 6 · Used by 2

Statement usesStandardized genotype matrix · Random-effects model of stratified LD-score regression · Association chi-squared statistic in stratified LD-score regression · Annotation LD score of a marker

Proof usesNormalized cross product of genotype markers · Expected chi-squared statistic of a standardized marker

Used byExpected statistics are the design matrix times the parameters · Frequency-dependent architecture

TheoremFrequency-dependent architecture#✓fully proved

Frequency-dependent architecture (the α model of Schoech et al. 2019): if the per-allele effect variance of marker k with allele frequency p_k is proportional to [p_k (1 - p_k)]^α, the variance of the effect of the standardized genotype is σ²_k = c [p_k (1 - p_k)]^(1 + α), and then, for a standardized genotype matrix and N ≠ 0, 𝔼[χ² j] = N c ∑_k [p_k (1 - p_k)]^(1 + α) r_jk² + σ²_e. (The real power is meaningful for 0 < p_k < 1.)

theorem integral_chiSq_of_alpha (p : Fin M → ℝ) (α c : ℝ)
    (hσ : ∀ k, D.sigma2 k = c * (p k * (1 - p k)) ^ (1 + α)) (hN : N ≠ 0) (j : Fin M)
    (hX : IsStandardized X) :
    ∫ ω, D.chiSq X j ω ∂μ =
      N * c * ∑ k, (p k * (1 - p k)) ^ (1 + α) * ldCorr X j k ^ 2 + D.sigmaE2

Uses 6

Statement usesStandardized genotype matrix · Normalized cross product of genotype markers · Random-effects model of stratified LD-score regression · Association chi-squared statistic in stratified LD-score regression

Proof usesStratified LD-score regression · Annotation LD score of a marker

19 fully proved

Category heritability and enrichment

DefinitionHeritability of a marker category#✓fully proved

The heritability h²(C) = ∑_{k ∈ C} σ²_k of category C, for a labeling cat of the markers by categories.

noncomputable def catH2 {ι : Type*} [DecidableEq ι] (σ2 : Fin M → ℝ) (cat : Fin M → ι)
    (C : ι) : ℝ :=
  ∑ k ∈ Finset.univ.filter (fun k => cat k = C), σ2 k

Used by 2

Used byHeritability enrichment of a category · Marker-proportion-weighted enrichments sum to one

DefinitionNumber of markers in a category#✓fully proved

The number M_C of markers in category C.

def catSize {ι : Type*} [DecidableEq ι] (cat : Fin M → ι) (C : ι) : ℕ :=
  (Finset.univ.filter (fun k => cat k = C)).card

Used by 2

Used byHeritability enrichment of a category · Marker-proportion-weighted enrichments sum to one

DefinitionHeritability enrichment of a category#✓fully proved

The enrichment of category C: its proportion of heritability divided by its proportion of markers, (h²(C) / h²) / (M_C / M) with h² = ∑_k σ²_k (Finucane et al. 2015).

noncomputable def enrichment {ι : Type*} [DecidableEq ι] (σ2 : Fin M → ℝ) (cat : Fin M → ι)
    (C : ι) : ℝ :=
  (catH2 σ2 cat C / ∑ k, σ2 k) / ((catSize cat C : ℝ) / M)

Uses 2 · Used by 1

Statement usesHeritability of a marker category · Number of markers in a category

Used byMarker-proportion-weighted enrichments sum to one

TheoremMarker-proportion-weighted enrichments sum to one#✓fully proved

For a partition of the markers into categories (a labeling cat) and nonzero total heritability, the marker-proportion-weighted enrichments sum to one: ∑_C (M_C / M) * Enrichment(C) = 1. Empty categories contribute 0 on both sides of each term.

theorem sum_size_mul_enrichment {ι : Type*} [Fintype ι] [DecidableEq ι] (σ2 : Fin M → ℝ)
    (cat : Fin M → ι) (hh : ∑ k, σ2 k ≠ 0) :
    ∑ C, ((catSize cat C : ℝ) / M) * enrichment σ2 cat C = 1

Uses 3

Statement usesNumber of markers in a category · Heritability enrichment of a category

Proof usesHeritability of a marker category

Identifiability with a free intercept

DefinitionDesign matrix of stratified LD-score regression#✓fully proved

The design matrix [1 | N ℓ(·, C)] of stratified LD-score regression with a free intercept; column none is the intercept and column some C the scaled annotation LD score.

noncomputable def design {ι : Type*} (X : Matrix (Fin N) (Fin M) ℝ) (a : Fin M → ι → ℝ) :
    Matrix (Fin M) (Option ι) ℝ :=
  fun j c => Option.elim c 1 fun C => N * annotLDScore X a j C

Uses 1 · Used by 1

Statement usesAnnotation LD score of a marker

Used byExpected statistics are the design matrix times the parameters

TheoremInjective matrix action iff full column rank#✓fully proved

A real matrix has injective mulVec iff it has full column rank.

theorem injective_mulVec_iff_rank_eq_card {m n : Type*} [Fintype n]
    (A : Matrix m n ℝ) : Function.Injective A.mulVec ↔ A.rank = Fintype.card n

TheoremExpected statistics are the design matrix times the parameters#✓fully proved

Under the annotation model, the vector of expected statistics is the design matrix applied to the parameter vector (σ²_e, τ) (intercept first). Hence the parameters are determined by the expected statistics of all markers, whatever their values, iff (design X a).rank = Fintype.card (Option ι) (injective_mulVec_iff_rank_eq_card).

theorem integral_chiSq_eq_design_mulVec {ι : Type*} [Fintype ι] (a : Fin M → ι → ℝ)
    (τ : ι → ℝ) (hσ : ∀ k, D.sigma2 k = ∑ C, τ C * a k C) (hN : N ≠ 0)
    (hX : IsStandardized X) (j : Fin M) :
    ∫ ω, D.chiSq X j ω ∂μ = (design X a *ᵥ fun c => Option.elim c D.sigmaE2 τ) j

Uses 6

Statement usesStandardized genotype matrix · Random-effects model of stratified LD-score regression · Association chi-squared statistic in stratified LD-score regression · Design matrix of stratified LD-score regression

Proof usesStratified LD-score regression · Annotation LD score of a marker

LDSC-SEG: the gene-set coefficient as a per-SNP contrast

TheoremLDSC-SEG contrast#✓fully proved

LDSC-SEG contrast (Finucane et al. 2018): for per-SNP variances σ²_k = ∑_C τ_C a_{kC}, two SNPs k, k' whose annotations agree except on annotation cS differ in per-SNP variance by τ_{cS} (a_{k cS} - a_{k' cS}). With cS the indicator of a gene set S contained in the control gene set G (whose indicator is one of the other annotations), k ∈ S and k' ∈ G ∖ S with equal values of all other annotations give σ²_k - σ²_{k'} = τ_S.

theorem sigma2_sub_sigma2_eq {ι : Type*} [Fintype ι] (a : Fin M → ι → ℝ) (τ : ι → ℝ)
    (cS : ι) (k k' : Fin M) (hagree : ∀ C, C ≠ cS → a k C = a k' C) :
    ∑ C, τ C * a k C - ∑ C, τ C * a k' C = τ cS * (a k cS - a k' cS)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.