Testing LD consistency of association statistics

DefinitionDENTIST-S statistic#✓fully proved

The DENTIST-S statistic (z_i - r z_c) ^ 2 / (1 - r ^ 2) of a variant with z-score zi, given the z-score zc of the lead (putative causal) variant and the reference correlation r between them (Kanai et al. 2022, Equation 1). Meaningful for r ^ 2 < 1; for r ^ 2 = 1 it is 0 by the convention x / 0 = 0.

noncomputable def dentistS (r zi zc : ℝ) : ℝ := (zi - r * zc) ^ 2 / (1 - r ^ 2)

Used by 2

Used byDENTIST-S is exactly χ²₁ when the reference LD is right · DENTIST-S is chi-squared with one degree of freedom under correct LD

DefinitionMean of the standardized DENTIST difference#✓fully proved

The mean (ρ - r) λ / √(1 - r²) of the standardized DENTIST difference when the true correlation is ρ, the reference correlation is r and the lead variant has mean λ.

noncomputable def dentistMean (ρ r lam : ℝ) : ℝ := (ρ - r) * lam / Real.sqrt (1 - r ^ 2)

Used by 3

Used byZero-mean criterion for the DENTIST difference · DENTIST-S is chi-squared with one degree of freedom under correct LD · Exact law of the standardized DENTIST difference

DefinitionVariance of the standardized DENTIST difference#✓fully proved

The variance (1 - 2 r ρ + r²) / (1 - r²) of the standardized DENTIST difference when the true correlation is ρ and the reference correlation is r.

noncomputable def dentistVariance (ρ r : ℝ) : ℝ := (1 - 2 * r * ρ + r ^ 2) / (1 - r ^ 2)

Used by 3

Used byUnit-variance criterion for the DENTIST difference · DENTIST-S is chi-squared with one degree of freedom under correct LD · Exact law of the standardized DENTIST difference

TheoremExact law of the standardized DENTIST difference#✓fully proved

Let (z_i, z_c) be jointly Gaussian with unit variances, correlation ρ (the covariance, as the variances are 1), and means ρ λ and λ. For a reference correlation r with r ^ 2 < 1, the standardized difference (z_i - r z_c) / √(1 - r²) is Gaussian with mean dentistMean ρ r λ and variance dentistVariance ρ r.

theorem map_standardized_eq_gaussianReal {zi zc : Ω → ℝ}
    (hz : HasGaussianLaw (fun ω => (zi ω, zc ω)) P) {ρ r lam : ℝ}
    (hvi : Var[zi; P] = 1) (hvc : Var[zc; P] = 1) (hcov : cov[zi, zc; P] = ρ)
    (hmi : P[zi] = ρ * lam) (hmc : P[zc] = lam) (hr : r ^ 2 < 1) :
    P.map (fun ω => (zi ω - r * zc ω) / Real.sqrt (1 - r ^ 2)) =
      gaussianReal (dentistMean ρ r lam) (dentistVariance ρ r).toNNReal

Uses 2 · Used by 1

Statement usesMean of the standardized DENTIST difference · Variance of the standardized DENTIST difference

Used byDENTIST-S is chi-squared with one degree of freedom under correct LD

TheoremDENTIST-S is chi-squared with one degree of freedom under correct LD#✓fully proved

When the reference correlation equals the true correlation ρ (ρ ^ 2 < 1), the DENTIST-S statistic has the law of the square of a standard normal variable.

theorem map_dentistS_eq_map_sq {zi zc : Ω → ℝ}
    (hz : HasGaussianLaw (fun ω => (zi ω, zc ω)) P) {ρ lam : ℝ}
    (hvi : Var[zi; P] = 1) (hvc : Var[zc; P] = 1) (hcov : cov[zi, zc; P] = ρ)
    (hmi : P[zi] = ρ * lam) (hmc : P[zc] = lam) (hρ : ρ ^ 2 < 1) :
    P.map (fun ω => dentistS ρ (zi ω) (zc ω)) = (gaussianReal 0 1).map (fun x : ℝ => x ^ 2)

Uses 4 · Used by 1

Statement usesDENTIST-S statistic

Proof usesMean of the standardized DENTIST difference · Variance of the standardized DENTIST difference · Exact law of the standardized DENTIST difference

Used byDENTIST-S is exactly χ²₁ when the reference LD is right

TheoremDENTIST-S is exactly χ²₁ when the reference LD is right#✓fully proved

Under the model of map_standardized_eq_gaussianReal with reference correlation equal to the true correlation ρ (ρ ^ 2 < 1), the DENTIST-S statistic has the chiSquareMeasure 1 law, for every value λ of the lead variant's mean.

theorem map_dentistS_eq_chiSquare {zi zc : Ω → ℝ}
    (hz : HasGaussianLaw (fun ω => (zi ω, zc ω)) P) {ρ lam : ℝ}
    (hvi : Var[zi; P] = 1) (hvc : Var[zc; P] = 1) (hcov : cov[zi, zc; P] = ρ)
    (hmi : P[zi] = ρ * lam) (hmc : P[zc] = lam) (hρ : ρ ^ 2 < 1) :
    P.map (fun ω => dentistS ρ (zi ω) (zc ω)) = chiSquareMeasure 1

Uses 4

Statement usesDENTIST-S statistic · Chi-square distribution

Proof usesDENTIST-S is chi-squared with one degree of freedom under correct LD · The square of a standard normal variable is chi-square with one degree of freedom

TheoremUnit-variance criterion for the DENTIST difference#✓fully proved

The standardized DENTIST difference has unit variance iff the reference correlation is 0 or equals the true correlation (for r ^ 2 < 1).

theorem dentistVariance_eq_one_iff {ρ r : ℝ} (hr : r ^ 2 < 1) :
    dentistVariance ρ r = 1 ↔ r = 0 ∨ r = ρ

Uses 1

Statement usesVariance of the standardized DENTIST difference

TheoremZero-mean criterion for the DENTIST difference#✓fully proved

The standardized DENTIST difference has mean zero iff the reference correlation equals the true correlation or the lead variant has mean zero (for r ^ 2 < 1).

theorem dentistMean_eq_zero_iff {ρ r lam : ℝ} (hr : r ^ 2 < 1) :
    dentistMean ρ r lam = 0 ↔ r = ρ ∨ lam = 0

Uses 1

Statement usesMean of the standardized DENTIST difference

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.