Skip to content

Latent causal variable model

22 fully proved

Latent Causal Variable

StructureLatent causal variable model#✓fully proved

The latent causal variable model of O'Connor and Price (2018, Equation 3) on a probability space: α_k = q_k π + γ_k with π independent of (γ₁, γ₂), the law of (γ₁, γ₂) invariant under each sign flip, π of mean zero and unit variance, and both α_k of unit second moment. Fourth moments are assumed finite.

MathlibExt.Biology.StatisticalGenetics.LatentCausalVariable.Model · 24 lines 
structure Model (P : Measure Ω) where
  /-- The normalized effect of the latent variable on trait 1. -/
  q1 : ℝ
  /-- The normalized effect of the latent variable on trait 2. -/
  q2 : ℝ
  /-- The effect of a SNP on the latent causal variable. -/
  pi : Ω → ℝ
  /-- The non-mediated effect of a SNP on trait 1. -/
  g1 : Ω → ℝ
  /-- The non-mediated effect of a SNP on trait 2. -/
  g2 : Ω → ℝ
  memLp_pi : MemLp pi 4 P
  memLp_g1 : MemLp g1 4 P
  memLp_g2 : MemLp g2 4 P
  /-- `π` is independent of `(γ₁, γ₂)`. -/
  indep : IndepFun pi (fun ω => (g1 ω, g2 ω)) P
  /-- `(γ₁, γ₂) ~ (-γ₁, γ₂)`. -/
  symm_left : IdentDistrib (fun ω => (g1 ω, g2 ω)) (fun ω => (-g1 ω, g2 ω)) P P
  /-- `(γ₁, γ₂) ~ (γ₁, -γ₂)`. -/
  symm_right : IdentDistrib (fun ω => (g1 ω, g2 ω)) (fun ω => (g1 ω, -g2 ω)) P P
  integral_pi : ∫ ω, pi ω ∂P = 0
  integral_pi_sq : ∫ ω, pi ω ^ 2 ∂P = 1
  integral_alpha1_sq : ∫ ω, (q1 * pi ω + g1 ω) ^ 2 ∂P = 1
  integral_alpha2_sq : ∫ ω, (q2 * pi ω + g2 ω) ^ 2 ∂P = 1
Used by 16
Used byThe centred moments order q₁² and q₂² · The uncentred comparison is reversed when κ_π < 0 · The paper's uncentred comparison, under its sign condition · Marginal effect on the first trait in the latent causal variable model · Marginal effect on the second trait in the latent causal variable model · Centred mixed fourth moment \(E(\alpha_1^3 \alpha_2)\) · Centred mixed fourth moment \(E(\alpha_1 \alpha_2^3)\) · The paper's criterion for gcp ≥ 0 · Genetic correlation in the latent causal variable model · Mixed fourth moment \(E(\alpha_1 \alpha_2^3)\) · Mixed fourth moment · Excess kurtosis of the latent effect · Excess kurtosis of the latent effect is at least −2 · Fourth moment of the latent effect is at least one · Mediated coefficient of the first trait is at most one in size · Mediated coefficient of the second trait is at most one in size

Model

DefinitionMarginal effect on the first trait in the latent causal variable model#✓fully proved

The marginal effect α₁ = q₁ π + γ₁ on trait 1.

def alpha1 (ω : Ω) : ℝ := D.q1 * D.pi ω + D.g1 ω
Uses 1 · Used by 9
Statement usesLatent causal variable model
Used byThe centred moments order q₁² and q₂² · The uncentred comparison is reversed when κ_π < 0 · The paper's uncentred comparison, under its sign condition · Centred mixed fourth moment \(E(\alpha_1^3 \alpha_2)\) · Centred mixed fourth moment \(E(\alpha_1 \alpha_2^3)\) · The paper's criterion for gcp ≥ 0 · Genetic correlation in the latent causal variable model · Mixed fourth moment \(E(\alpha_1 \alpha_2^3)\) · Mixed fourth moment

DefinitionMarginal effect on the second trait in the latent causal variable model#✓fully proved

The marginal effect α₂ = q₂ π + γ₂ on trait 2.

def alpha2 (ω : Ω) : ℝ := D.q2 * D.pi ω + D.g2 ω
Uses 1 · Used by 9
Statement usesLatent causal variable model
Used byThe centred moments order q₁² and q₂² · The uncentred comparison is reversed when κ_π < 0 · The paper's uncentred comparison, under its sign condition · Centred mixed fourth moment \(E(\alpha_1^3 \alpha_2)\) · Centred mixed fourth moment \(E(\alpha_1 \alpha_2^3)\) · The paper's criterion for gcp ≥ 0 · Genetic correlation in the latent causal variable model · Mixed fourth moment \(E(\alpha_1 \alpha_2^3)\) · Mixed fourth moment

DefinitionExcess kurtosis of the latent effect#✓fully proved

The excess kurtosis κ_π = E(π⁴) - 3 of the effect on the latent variable.

noncomputable def kurtosis : ℝ := ∫ ω, D.pi ω ^ 4 ∂P - 3
Uses 1 · Used by 9
Statement usesLatent causal variable model
Used byThe centred moments order q₁² and q₂² · The uncentred comparison is reversed when κ_π < 0 · The paper's uncentred comparison, under its sign condition · Centred mixed fourth moment \(E(\alpha_1^3 \alpha_2)\) · Centred mixed fourth moment \(E(\alpha_1 \alpha_2^3)\) · The paper's criterion for gcp ≥ 0 · Mixed fourth moment \(E(\alpha_1 \alpha_2^3)\) · Mixed fourth moment · Excess kurtosis of the latent effect is at least −2

TheoremGenetic correlation in the latent causal variable model#✓fully proved

The genetic correlation is E(α₁ α₂) = q₁ q₂ (O'Connor and Price 2018, after Equation 1).

theorem integral_alpha1_mul_alpha2 : ∫ ω, D.alpha1 ω * D.alpha2 ω ∂P = D.q1 * D.q2
Uses 3
Statement usesLatent causal variable model · Marginal effect on the first trait in the latent causal variable model · Marginal effect on the second trait in the latent causal variable model

TheoremMixed fourth moment#✓fully proved

Mixed fourth moment (O'Connor and Price 2018, Equation 2): E(α₁³ α₂) = κ_π q₁³ q₂ + 3 q₁ q₂.

theorem integral_alpha1_pow_three_mul_alpha2 :
    ∫ ω, D.alpha1 ω ^ 3 * D.alpha2 ω ∂P = D.kurtosis * D.q1 ^ 3 * D.q2 + 3 * (D.q1 * D.q2)
Uses 4 · Used by 4
Statement usesLatent causal variable model · Marginal effect on the first trait in the latent causal variable model · Marginal effect on the second trait in the latent causal variable model · Excess kurtosis of the latent effect
Used byThe uncentred comparison is reversed when κ_π < 0 · The paper's uncentred comparison, under its sign condition · Centred mixed fourth moment \(E(\alpha_1^3 \alpha_2)\) · Mixed fourth moment \(E(\alpha_1 \alpha_2^3)\)

TheoremMixed fourth moment \(E(\alpha_1 \alpha_2^3)\)#✓fully proved

The mirror image of Equation 2: E(α₁ α₂³) = κ_π q₁ q₂³ + 3 q₁ q₂.

theorem integral_alpha1_mul_alpha2_pow_three :
    ∫ ω, D.alpha1 ω * D.alpha2 ω ^ 3 ∂P = D.kurtosis * D.q1 * D.q2 ^ 3 + 3 * (D.q1 * D.q2)
Uses 5 · Used by 3
Statement usesLatent causal variable model · Marginal effect on the first trait in the latent causal variable model · Marginal effect on the second trait in the latent causal variable model · Excess kurtosis of the latent effect
Proof usesMixed fourth moment
Used byThe uncentred comparison is reversed when κ_π < 0 · The paper's uncentred comparison, under its sign condition · Centred mixed fourth moment \(E(\alpha_1 \alpha_2^3)\)

TheoremMediated coefficient of the first trait is at most one in size#✓fully proved

Unit variance of α₁ forces q₁² ≤ 1 (the non-mediated part has variance 1 - q₁²).

theorem q1_sq_le_one : D.q1 ^ 2 ≤ 1
Uses 1 · Used by 2
Statement usesLatent causal variable model
Used byThe uncentred comparison is reversed when κ_π < 0 · The paper's uncentred comparison, under its sign condition

TheoremMediated coefficient of the second trait is at most one in size#✓fully proved

Unit variance of α₂ forces q₂² ≤ 1.

theorem q2_sq_le_one : D.q2 ^ 2 ≤ 1
Uses 1 · Used by 2
Statement usesLatent causal variable model
Used byThe uncentred comparison is reversed when κ_π < 0 · The paper's uncentred comparison, under its sign condition

TheoremFourth moment of the latent effect is at least one#✓fully proved

E(π⁴) ≥ (E π²)² = 1, so the excess kurtosis is at least -2.

theorem one_le_integral_pi_pow_four : 1 ≤ ∫ ω, D.pi ω ^ 4 ∂P
Uses 1 · Used by 1
Statement usesLatent causal variable model
Used byExcess kurtosis of the latent effect is at least −2

TheoremCentred mixed fourth moment \(E(\alpha_1^3 \alpha_2)\)#✓fully proved

The centred mixed fourth moment: E(α₁³ α₂) - 3 ρ_g = κ_π q₁³ q₂.

theorem centred_moment_left :
    ∫ ω, D.alpha1 ω ^ 3 * D.alpha2 ω ∂P - 3 * (D.q1 * D.q2) = D.kurtosis * D.q1 ^ 3 * D.q2
Uses 5 · Used by 1
Statement usesLatent causal variable model · Marginal effect on the first trait in the latent causal variable model · Marginal effect on the second trait in the latent causal variable model · Excess kurtosis of the latent effect
Proof usesMixed fourth moment
Used byThe centred moments order q₁² and q₂²

TheoremCentred mixed fourth moment \(E(\alpha_1 \alpha_2^3)\)#✓fully proved

The centred mixed fourth moment: E(α₁ α₂³) - 3 ρ_g = κ_π q₁ q₂³.

theorem centred_moment_right :
    ∫ ω, D.alpha1 ω * D.alpha2 ω ^ 3 ∂P - 3 * (D.q1 * D.q2) = D.kurtosis * D.q1 * D.q2 ^ 3
Uses 5 · Used by 1
Statement usesLatent causal variable model · Marginal effect on the first trait in the latent causal variable model · Marginal effect on the second trait in the latent causal variable model · Excess kurtosis of the latent effect
Proof usesMixed fourth moment \(E(\alpha_1 \alpha_2^3)\)
Used byThe centred moments order q₁² and q₂²

TheoremThe centred moments order q₁² and q₂²#✓fully proved

If κ_π ≠ 0 and ρ_g = q₁ q₂ ≠ 0, then |E(α₁ α₂³) - 3 ρ_g| ≤ |E(α₁³ α₂) - 3 ρ_g| iff q₂² ≤ q₁².

theorem abs_centredMoment_le_iff (hκ : D.kurtosis ≠ 0) (hρ : D.q1 * D.q2 ≠ 0) :
    |∫ ω, D.alpha1 ω * D.alpha2 ω ^ 3 ∂P - 3 * (D.q1 * D.q2)| ≤
        |∫ ω, D.alpha1 ω ^ 3 * D.alpha2 ω ∂P - 3 * (D.q1 * D.q2)| ↔ D.q2 ^ 2 ≤ D.q1 ^ 2
Uses 6
Statement usesLatent causal variable model · Marginal effect on the first trait in the latent causal variable model · Marginal effect on the second trait in the latent causal variable model · Excess kurtosis of the latent effect
Proof usesCentred mixed fourth moment \(E(\alpha_1^3 \alpha_2)\) · Centred mixed fourth moment \(E(\alpha_1 \alpha_2^3)\)

TheoremExcess kurtosis of the latent effect is at least −2#✓fully proved

κ_π ≥ -2.

theorem neg_two_le_kurtosis : -2 ≤ D.kurtosis
Uses 3 · Used by 2
Statement usesLatent causal variable model · Excess kurtosis of the latent effect
Proof usesFourth moment of the latent effect is at least one
Used byThe uncentred comparison is reversed when κ_π < 0 · The paper's uncentred comparison, under its sign condition

TheoremThe paper's uncentred comparison, under its sign condition#✓fully proved

If κ_π > 0 and ρ_g ≠ 0, then |E(α₁ α₂³)| ≤ |E(α₁³ α₂)| iff q₂² ≤ q₁² (O'Connor and Price 2018, after Equation 2, which states the forward implication).

theorem abs_moment_le_iff_of_kurtosis_pos (hκ : 0 < D.kurtosis) (hρ : D.q1 * D.q2 ≠ 0) :
    |∫ ω, D.alpha1 ω * D.alpha2 ω ^ 3 ∂P| ≤ |∫ ω, D.alpha1 ω ^ 3 * D.alpha2 ω ∂P| ↔
      D.q2 ^ 2 ≤ D.q1 ^ 2
Uses 9 · Used by 1
Statement usesLatent causal variable model · Marginal effect on the first trait in the latent causal variable model · Marginal effect on the second trait in the latent causal variable model · Excess kurtosis of the latent effect
Proof usesMixed fourth moment \(E(\alpha_1 \alpha_2^3)\) · Mixed fourth moment · Excess kurtosis of the latent effect is at least −2 · Mediated coefficient of the first trait is at most one in size · Mediated coefficient of the second trait is at most one in size
Used byThe paper's criterion for gcp ≥ 0

TheoremThe uncentred comparison is reversed when κ_π < 0#✓fully proved

If κ_π < 0 and ρ_g ≠ 0, then |E(α₁ α₂³)| ≤ |E(α₁³ α₂)| iff q₁² ≤ q₂². So the paper's uncentred criterion needs κ_π > 0; the centred criterion abs_centredMoment_le_iff does not.

theorem abs_moment_le_iff_of_kurtosis_neg (hκ : D.kurtosis < 0) (hρ : D.q1 * D.q2 ≠ 0) :
    |∫ ω, D.alpha1 ω * D.alpha2 ω ^ 3 ∂P| ≤ |∫ ω, D.alpha1 ω ^ 3 * D.alpha2 ω ∂P| ↔
      D.q1 ^ 2 ≤ D.q2 ^ 2
Uses 9
Statement usesLatent causal variable model · Marginal effect on the first trait in the latent causal variable model · Marginal effect on the second trait in the latent causal variable model · Excess kurtosis of the latent effect
Proof usesMixed fourth moment \(E(\alpha_1 \alpha_2^3)\) · Mixed fourth moment · Excess kurtosis of the latent effect is at least −2 · Mediated coefficient of the first trait is at most one in size · Mediated coefficient of the second trait is at most one in size

Latent Causal Variable

DefinitionGenetic causality proportion#✓fully proved

The genetic causality proportion gcp = (log|q₂| - log|q₁|) / (log|q₂| + log|q₁|) (O'Connor and Price 2018, Equation 4). Meaningful for 0 < |q₁|, |q₂| ≤ 1 and ρ_g² < 1; for |q₁| = |q₂| = 1 the denominator vanishes and the value is 0 by the convention x / 0 = 0.

noncomputable def gcp (q1 q2 : ℝ) : ℝ :=
  (Real.log |q2| - Real.log |q1|) / (Real.log |q2| + Real.log |q1|)
Used by 5
Used byGenetic causality proportion is at most 1 · Sign of the genetic causality proportion · The paper's criterion for gcp ≥ 0 · Genetic causality proportion is at least −1 · Genetic causality proportion solves the defining equation

TheoremSign of the genetic causality proportion#✓fully proved

gcp ≥ 0 iff q₂² ≤ q₁², for nonzero q₁, q₂ with ρ_g² = (q₁ q₂)² < 1.

theorem gcp_nonneg_iff {q1 q2 : ℝ} (h1 : q1 ≠ 0) (h2 : q2 ≠ 0) (hρ : (q1 * q2) ^ 2 < 1) :
    0 ≤ gcp q1 q2 ↔ q2 ^ 2 ≤ q1 ^ 2
Uses 1 · Used by 1
Statement usesGenetic causality proportion
Used byThe paper's criterion for gcp ≥ 0

TheoremGenetic causality proportion solves the defining equation#✓fully proved

The genetic causality proportion solves the paper's Equation 1: q₂² / q₁² = (ρ_g²) ^ gcp with ρ_g = q₁ q₂, for nonzero q₁, q₂ with ρ_g² < 1.

theorem rpow_gcp {q1 q2 : ℝ} (h1 : q1 ≠ 0) (h2 : q2 ≠ 0) (hρ : (q1 * q2) ^ 2 < 1) :
    ((q1 * q2) ^ 2) ^ gcp q1 q2 = q2 ^ 2 / q1 ^ 2
Uses 1
Statement usesGenetic causality proportion

TheoremGenetic causality proportion is at most 1#✓fully proved

gcp ≤ 1 when q₁² ≤ 1 (for nonzero q₁, q₂ with ρ_g² < 1).

theorem gcp_le_one {q1 q2 : ℝ} (h1 : q1 ≠ 0) (h2 : q2 ≠ 0) (hρ : (q1 * q2) ^ 2 < 1)
    (hq1 : q1 ^ 2 ≤ 1) : gcp q1 q2 ≤ 1
Uses 1
Statement usesGenetic causality proportion

TheoremGenetic causality proportion is at least −1#✓fully proved

-1 ≤ gcp when q₂² ≤ 1 (for nonzero q₁, q₂ with ρ_g² < 1).

theorem neg_one_le_gcp {q1 q2 : ℝ} (h1 : q1 ≠ 0) (h2 : q2 ≠ 0) (hρ : (q1 * q2) ^ 2 < 1)
    (hq2 : q2 ^ 2 ≤ 1) : -1 ≤ gcp q1 q2
Uses 1
Statement usesGenetic causality proportion

TheoremThe paper's criterion for gcp ≥ 0#✓fully proved

The paper's criterion for gcp ≥ 0 (O'Connor and Price 2018, after Equation 2), under the sign condition κ_π > 0 that it needs: if ρ_g ≠ 0, ρ_g² < 1 and |E(α₁ α₂³)| ≤ |E(α₁³ α₂)|, then gcp ≥ 0.

theorem Model.gcp_nonneg_of_abs_moment_le {P : Measure Ω} [IsProbabilityMeasure P] (D : Model P)
    (hκ : 0 < D.kurtosis) (hρ : D.q1 * D.q2 ≠ 0) (hρ1 : (D.q1 * D.q2) ^ 2 < 1)
    (h : |∫ ω, D.alpha1 ω * D.alpha2 ω ^ 3 ∂P| ≤ |∫ ω, D.alpha1 ω ^ 3 * D.alpha2 ω ∂P|) :
    0 ≤ gcp D.q1 D.q2
Uses 7
Statement usesLatent causal variable model · Marginal effect on the first trait in the latent causal variable model · Marginal effect on the second trait in the latent causal variable model · Excess kurtosis of the latent effect · Genetic causality proportion
Proof usesThe paper's uncentred comparison, under its sign condition · Sign of the genetic causality proportion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.