Signed LD profile regression

8 fully proved

Signed LD profiles

DefinitionIn-sample LD matrix#✓fully proved

The in-sample LD matrix R̂ = Xᵀ X / N, with entries ldCorr X j k.

noncomputable def ldMatrix (X : Matrix (Fin N) (Fin M) ℝ) : Matrix (Fin M) (Fin M) ℝ :=
  Matrix.of (ldCorr X)

Uses 1 · Used by 4

Statement usesNormalized cross product of genotype markers

Used byFirst-moment identity, exact in-sample form · SLDP first-moment identity · Unbiasedness of the weighted least-squares estimator · Unbiasedness with covariates

StructureFirst-moment phenotype model of SLDP regression#✓fully proved

The linear phenotype model of SLDP regression at the level of first moments: integrable random effects β with means meanBeta and integrable noise ε of mean zero. (SLDP's model takes meanBeta = μ v for a signed annotation v; second moments are not needed for the first-moment identity.)

MathlibExt.Biology.StatisticalGenetics.SignedLDProfile.Model · 15 lines

structure Model (P : Measure Ω) (N M : ℕ) where
  /-- The mean `𝔼 β` of the true effects. -/
  meanBeta : Fin M → ℝ
  /-- Random per-marker effects. -/
  beta : Fin M → Ω → ℝ
  /-- Random environmental noise. -/
  eps : Fin N → Ω → ℝ
  /-- Effects are integrable. -/
  integrable_beta : ∀ k, Integrable (beta k) P
  /-- Noise terms are integrable. -/
  integrable_eps : ∀ i, Integrable (eps i) P
  /-- The effects have mean `meanBeta`. -/
  integral_beta : ∀ k, ∫ ω, beta k ω ∂P = meanBeta k
  /-- The noise has mean zero. -/
  integral_eps : ∀ i, ∫ ω, eps i ω ∂P = 0

Used by 6

Used byMarginal marker-phenotype correlations in SLDP regression · First-moment identity, exact in-sample form · SLDP first-moment identity · Unbiasedness of the weighted least-squares estimator · Unbiasedness with covariates · Phenotype in the SLDP regression model

Model

DefinitionPhenotype in the SLDP regression 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 4

Statement usesFirst-moment phenotype model of SLDP regression

Used byMarginal marker-phenotype correlations in SLDP regression · First-moment identity, exact in-sample form · Unbiasedness of the weighted least-squares estimator · Unbiasedness with covariates

DefinitionMarginal marker-phenotype correlations in SLDP regression#✓fully proved

The vector α̂ = Xᵀ y / N of marginal correlations between the (standardized) markers and the phenotype.

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

Uses 2 · Used by 4

Statement usesFirst-moment phenotype model of SLDP regression · Phenotype in the SLDP regression model

Used byFirst-moment identity, exact in-sample form · SLDP first-moment identity · Unbiasedness of the weighted least-squares estimator · Unbiasedness with covariates

TheoremFirst-moment identity, exact in-sample form#✓fully proved

Conditional on the genotype matrix, 𝔼 α̂ = R̂ 𝔼 β with R̂ = Xᵀ X / N.

theorem integral_alphaHat (j : Fin M) :
    ∫ ω, D.alphaHat X ω j ∂P = (ldMatrix X *ᵥ D.meanBeta) j

Uses 5 · Used by 3

Statement usesFirst-moment phenotype model of SLDP regression · Marginal marker-phenotype correlations in SLDP regression · In-sample LD matrix

Proof usesNormalized cross product of genotype markers · Phenotype in the SLDP regression model

Used bySLDP first-moment identity · Unbiasedness of the weighted least-squares estimator · Unbiasedness with covariates

TheoremSLDP first-moment identity#✓fully proved

SLDP first-moment identity (Reshef et al. 2018, Methods, Equation 5): if the true effects have mean μ v, then 𝔼 α̂ = μ R̂ v, a multiple of the signed LD profile R̂ v of v.

theorem integral_alphaHat_of_mean {mu : ℝ} {v : Fin M → ℝ}
    (hmean : D.meanBeta = mu • v) (j : Fin M) :
    ∫ ω, D.alphaHat X ω j ∂P = mu * (ldMatrix X *ᵥ v) j

Uses 4

Statement usesFirst-moment phenotype model of SLDP regression · Marginal marker-phenotype correlations in SLDP regression · In-sample LD matrix

Proof usesFirst-moment identity, exact in-sample form

TheoremUnbiasedness of the weighted least-squares estimator#✓fully proved

For any weight matrix W and signed LD profile s = R̂ v with ⟪s, s⟫_W = sᵀ W s ≠ 0, if 𝔼 β = μ v then 𝔼 [⟪s, α̂⟫_W / ⟪s, s⟫_W] = μ, where ⟪a, b⟫_W = aᵀ W b. SLDP uses the inverse of Ω = σ² R² + R / N as W.

theorem integral_gls_estimator {mu : ℝ} {v : Fin M → ℝ} (hmean : D.meanBeta = mu • v)
    (W : Matrix (Fin M) (Fin M) ℝ)
    (hne : (ldMatrix X *ᵥ v) ⬝ᵥ (W *ᵥ (ldMatrix X *ᵥ v)) ≠ 0) :
    ∫ ω, (ldMatrix X *ᵥ v) ⬝ᵥ (W *ᵥ D.alphaHat X ω) /
        ((ldMatrix X *ᵥ v) ⬝ᵥ (W *ᵥ (ldMatrix X *ᵥ v))) ∂P = mu

Uses 6

Statement usesFirst-moment phenotype model of SLDP regression · Marginal marker-phenotype correlations in SLDP regression · In-sample LD matrix

Proof usesNormalized cross product of genotype markers · First-moment identity, exact in-sample form · Phenotype in the SLDP regression model

TheoremUnbiasedness with covariates#✓fully proved

Unbiasedness with covariates (the signed background model): suppose the true effects have mean μ v + U γ for background annotations U (columns u_b) with arbitrary coefficients γ, let A = R̂ U be their signed LD profiles, and let z⊥ = R̂ v - A w be the weighted residual of the signed LD profile of v on A (Aᵀ W z⊥ = 0) for a symmetric weight matrix W. If ⟪z⊥, z⊥⟫_W ≠ 0, then 𝔼 [⟪z⊥, α̂⟫_W / ⟪z⊥, z⊥⟫_W] = μ. By Matrix.frischWaughLovell this estimator equals the coefficient of R̂ v in the joint weighted regression of α̂ on [A | R̂ v], and the same as regressing the residualized α̂ on z⊥.

theorem integral_gls_estimator_of_background {κ : Type*} [Fintype κ] {mu : ℝ} {v : Fin M → ℝ}
    (U : Matrix (Fin M) κ ℝ) (γ : κ → ℝ) (hmean : D.meanBeta = mu • v + U *ᵥ γ)
    {W : Matrix (Fin M) (Fin M) ℝ} (hW : Wᵀ = W) (w : κ → ℝ)
    (hres : (ldMatrix X * U)ᵀ *ᵥ (W *ᵥ (ldMatrix X *ᵥ v - (ldMatrix X * U) *ᵥ w)) = 0)
    (hne : (ldMatrix X *ᵥ v - (ldMatrix X * U) *ᵥ w) ⬝ᵥ
      (W *ᵥ (ldMatrix X *ᵥ v - (ldMatrix X * U) *ᵥ w)) ≠ 0) :
    ∫ ω, (ldMatrix X *ᵥ v - (ldMatrix X * U) *ᵥ w) ⬝ᵥ (W *ᵥ D.alphaHat X ω) /
        ((ldMatrix X *ᵥ v - (ldMatrix X * U) *ᵥ w) ⬝ᵥ
          (W *ᵥ (ldMatrix X *ᵥ v - (ldMatrix X * U) *ᵥ w))) ∂P = mu

Uses 6

Statement usesFirst-moment phenotype model of SLDP regression · Marginal marker-phenotype correlations in SLDP regression · In-sample LD matrix

Proof usesNormalized cross product of genotype markers · First-moment identity, exact in-sample form · Phenotype in the SLDP regression model

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.