Mendelian randomization

45 fully proved

Wald covariance identities in an observational linear moment model

StructureLinear moment model for instrumental variables#✓fully proved

An observational linear moment model: variables Z, X, Y and U on a probability space, all square integrable, with the algebraic decomposition Y = α + β X + U. The residual U is an arbitrary observed-variable function. Consequently outcome_eq does not exclude direct effects of Z under interventions, and β is only the coefficient in this decomposition. Orthogonality (Cov(Z, U) = 0) and nonzero first stage (Cov(Z, X) ≠ 0) are hypotheses of the covariance identities that use them.

MathlibExt.Biology.StatisticalGenetics.MendelianRandomization.LinearMomentModel · 21 lines

structure LinearMomentModel (μ : Measure Ω) where
  /-- The instrument `Z` (in Mendelian randomization, a genotype). -/
  instrument : Ω → ℝ
  /-- The exposure `X`. -/
  exposure : Ω → ℝ
  /-- The outcome `Y`. -/
  outcome : Ω → ℝ
  /-- The observational residual `U`. It may contain direct dependence on the instrument. -/
  residual : Ω → ℝ
  /-- The intercept `α`. -/
  intercept : ℝ
  /-- The coefficient `β` in the observational decomposition. -/
  coefficient : ℝ
  /-- The instrument is square integrable. -/
  memLp_instrument : MemLp instrument 2 μ
  /-- The exposure is square integrable. -/
  memLp_exposure : MemLp exposure 2 μ
  /-- The residual is square integrable. -/
  memLp_residual : MemLp residual 2 μ
  /-- The observational decomposition `Y = α + β X + U`. -/
  outcome_eq : ∀ ω, outcome ω = intercept + coefficient * exposure ω + residual ω

Used by 5

Used byWald ratio identity · Wald ratio identity for an instrument independent of the residual · Bias of the ordinary least-squares coefficient under confounding · Wald ratio as a ratio of regression slopes · Covariance with the outcome in a linear moment model

TheoremCovariance with the outcome in a linear moment model#✓fully proved

The covariance of any square-integrable variable with the outcome splits along the observational decomposition: Cov(V, Y) = β Cov(V, X) + Cov(V, U).

theorem covariance_outcome {V : Ω → ℝ} (hV : MemLp V 2 μ) :
    cov[V, M.outcome; μ] =
      M.coefficient * cov[V, M.exposure; μ] + cov[V, M.residual; μ]

Uses 1 · Used by 2

Statement usesLinear moment model for instrumental variables

Used byWald ratio identity · Bias of the ordinary least-squares coefficient under confounding

TheoremWald ratio identity#✓fully proved

The Wald covariance identity: if Cov(Z, U) = 0 and Cov(Z, X) ≠ 0, then Cov(Z, Y) / Cov(Z, X) = β. For a two-valued Z the ratio is the grouping estimator of Wald (1940), the difference of the group means of Y over that of X. This is a moment-condition identity, not a formal causal-identification result.

theorem covariance_div_covariance (hZU : cov[M.instrument, M.residual; μ] = 0)
    (hZX : cov[M.instrument, M.exposure; μ] ≠ 0) :
    cov[M.instrument, M.outcome; μ] / cov[M.instrument, M.exposure; μ] =
      M.coefficient

Uses 2 · Used by 2

Statement usesLinear moment model for instrumental variables

Proof usesCovariance with the outcome in a linear moment model

Used byWald ratio identity for an instrument independent of the residual · Wald ratio as a ratio of regression slopes

TheoremWald ratio identity for an instrument independent of the residual#✓fully proved

The Wald covariance identity when the instrument is independent of the residual.

theorem covariance_div_covariance_of_indepFun (hZU : IndepFun M.instrument M.residual μ)
    (hZX : cov[M.instrument, M.exposure; μ] ≠ 0) :
    cov[M.instrument, M.outcome; μ] / cov[M.instrument, M.exposure; μ] =
      M.coefficient

Uses 2

Statement usesLinear moment model for instrumental variables

Proof usesWald ratio identity

TheoremWald ratio as a ratio of regression slopes#✓fully proved

The Wald ratio as a ratio of regression slopes: the slope of Y on Z divided by the slope of X on Z (the form used with SNP–outcome and SNP–exposure associations) is β. This is again an observational moment identity.

theorem covariance_div_variance_div (hZU : cov[M.instrument, M.residual; μ] = 0)
    (hZX : cov[M.instrument, M.exposure; μ] ≠ 0) :
    (cov[M.instrument, M.outcome; μ] / Var[M.instrument; μ]) /
      (cov[M.instrument, M.exposure; μ] / Var[M.instrument; μ]) = M.coefficient

Uses 2

Statement usesLinear moment model for instrumental variables

Proof usesWald ratio identity

TheoremBias of the ordinary least-squares coefficient under confounding#✓fully proved

The ordinary least-squares coefficient identity for Y on X is β + Cov(X, U) / Var(X), which differs from β exactly when Cov(X, U) ≠ 0.

theorem covariance_div_variance (hX : Var[M.exposure; μ] ≠ 0) :
    cov[M.exposure, M.outcome; μ] / Var[M.exposure; μ] =
      M.coefficient + cov[M.exposure, M.residual; μ] / Var[M.exposure; μ]

Uses 2

Statement usesLinear moment model for instrumental variables

Proof usesCovariance with the outcome in a linear moment model

Summary-data estimators: inverse-variance weighting

DefinitionRatio estimate of a single SNP#✓fully proved

The ratio estimate β̂_{Yj} / β̂_{Xj} of SNP j (Lean's x / 0 = 0 gives 0 when β̂_{Xj} = 0; such SNPs carry weight 0 in ivwWeight).

noncomputable def ratioEstimate (bX bY : ι → ℝ) (j : ι) : ℝ := bY j / bX j

Used by 1

Used byIVW estimator as a weighted mean of ratio estimates

DefinitionInverse-variance weight of a ratio estimate#✓fully proved

The first-order inverse-variance weight w_j = β̂_{Xj}² / σ_j² of the ratio estimate of SNP j, where σ_j is the standard error of β̂_{Yj} (Burgess, Butterworth & Thompson 2013).

noncomputable def ivwWeight (bX se : ι → ℝ) (j : ι) : ℝ := bX j ^ 2 / se j ^ 2

Used by 8

Used byUnbiasedness of the IVW estimator · Inverse-variance-weighted estimator · IVW estimator as a weighted mean of ratio estimates · IVW estimator minimizes the weighted residual sum of squares · Directional pleiotropy biases the IVW estimator · IVW recovers an exact proportionality coefficient · Positivity of the total IVW weight · Variance of the IVW estimator

DefinitionInverse-variance-weighted estimator#✓fully proved

The inverse-variance-weighted (IVW) estimator ∑ β̂_{Xj} β̂_{Yj} σ_j⁻² / ∑ β̂_{Xj}² σ_j⁻² (Burgess, Butterworth & Thompson 2013). The standard errors are positive in the model; it is the junk value 0 if every β̂_{Xj} = 0.

noncomputable def ivw (bX bY se : ι → ℝ) : ℝ :=
  (∑ j, bX j * bY j / se j ^ 2) / ∑ j, ivwWeight bX se j

Uses 1 · Used by 6

Statement usesInverse-variance weight of a ratio estimate

Used byUnbiasedness of the IVW estimator · IVW estimator as a weighted mean of ratio estimates · IVW estimator minimizes the weighted residual sum of squares · Directional pleiotropy biases the IVW estimator · IVW recovers an exact proportionality coefficient · Variance of the IVW estimator

DefinitionWeighted residual sum of squares through the origin#✓fully proved

The weighted residual sum of squares ∑ (β̂_{Yj} - b β̂_{Xj})² / σ_j² of the regression through the origin with slope b.

noncomputable def weightedSSR (bX bY se : ι → ℝ) (b : ℝ) : ℝ :=
  ∑ j, (bY j - b * bX j) ^ 2 / se j ^ 2

Used by 1

Used byIVW estimator minimizes the weighted residual sum of squares

TheoremIVW estimator as a weighted mean of ratio estimates#✓fully proved

The IVW estimator is the weighted mean of the ratio estimates with weights w_j = β̂_{Xj}² / σ_j². This holds for all data: a SNP with β̂_{Xj} = 0 has weight 0 and contributes nothing to either side.

theorem ivw_eq_weightedMean (bX bY se : ι → ℝ) :
    ivw bX bY se =
      (∑ j, ivwWeight bX se j * ratioEstimate bX bY j) / ∑ j, ivwWeight bX se j

Uses 3

Statement usesInverse-variance-weighted estimator · Inverse-variance weight of a ratio estimate · Ratio estimate of a single SNP

TheoremIVW estimator minimizes the weighted residual sum of squares#✓fully proved

The IVW estimator is the weighted least-squares slope through the origin: it minimizes the weighted residual sum of squares. This holds for all data: if every β̂_{Xj} = 0 the sum does not depend on the slope (and ivw is the junk value 0), and a SNP with σ_j = 0 has weight 0 on both sides by Lean's x / 0 = 0.

theorem ivw_le_weightedSSR (bX bY se : ι → ℝ) (b : ℝ) :
    weightedSSR bX bY se (ivw bX bY se) ≤ weightedSSR bX bY se b

Uses 3

Statement usesInverse-variance-weighted estimator · Weighted residual sum of squares through the origin

Proof usesInverse-variance weight of a ratio estimate

TheoremPositivity of the total IVW weight#✓fully proved

The total weight is positive as soon as some SNP has β̂_{Xj} ≠ 0.

theorem sum_ivwWeight_pos {bX se : ι → ℝ} (hse : ∀ j, 0 < se j) (hX : ∃ j, bX j ≠ 0) :
    0 < ∑ j, ivwWeight bX se j

Uses 1 · Used by 4

Statement usesInverse-variance weight of a ratio estimate

Used byUnbiasedness of the IVW estimator · Directional pleiotropy biases the IVW estimator · IVW recovers an exact proportionality coefficient · Variance of the IVW estimator

TheoremIVW recovers an exact proportionality coefficient#✓fully proved

Without error, IVW recovers the proportionality coefficient: if β̂_{Yj} = β β̂_{Xj} for all j and some β̂_{Xj} ≠ 0, then the IVW estimate is β. This algebraic statement does not itself give β a causal interpretation.

theorem ivw_of_proportional {bX se : ι → ℝ} (hse : ∀ j, 0 < se j) (hX : ∃ j, bX j ≠ 0)
    (β : ℝ) : ivw bX (fun j => β * bX j) se = β

Uses 3

Statement usesInverse-variance-weighted estimator

Proof usesInverse-variance weight of a ratio estimate · Positivity of the total IVW weight

TheoremUnbiasedness of the IVW estimator#✓fully proved

Unbiasedness of IVW (Burgess, Butterworth & Thompson 2013), with the SNP–exposure associations β̂_{Xj} treated as fixed: if β̂_{Yj} = β β̂_{Xj} + ε_j with integrable mean-zero errors, the IVW estimator has mean β.

theorem integral_ivw {bX se : ι → ℝ} (hse : ∀ j, 0 < se j) (hX : ∃ j, bX j ≠ 0) (β : ℝ)
    {ε : ι → Ω → ℝ} (hint : ∀ j, Integrable (ε j) μ) (hmean : ∀ j, ∫ ω, ε j ω ∂μ = 0) :
    ∫ ω, ivw bX (fun j => β * bX j + ε j ω) se ∂μ = β

Uses 3

Statement usesInverse-variance-weighted estimator

Proof usesInverse-variance weight of a ratio estimate · Positivity of the total IVW weight

TheoremVariance of the IVW estimator#✓fully proved

The first-order variance of IVW (Burgess, Butterworth & Thompson 2013): with the β̂_{Xj} fixed and β̂_{Yj} = β β̂_{Xj} + ε_j, where the errors are square integrable, pairwise uncorrelated (for instance independent) and Var(ε_j) = σ_j², the IVW estimator has variance (∑ w_j)⁻¹ = (∑ β̂_{Xj}² / σ_j²)⁻¹.

theorem variance_ivw {bX se : ι → ℝ} (hse : ∀ j, 0 < se j) (hX : ∃ j, bX j ≠ 0) (β : ℝ)
    {ε : ι → Ω → ℝ} (hL2 : ∀ j, MemLp (ε j) 2 μ)
    (hcov : ∀ i j, i ≠ j → cov[ε i, ε j; μ] = 0) (hvar : ∀ j, Var[ε j; μ] = se j ^ 2) :
    Var[fun ω => ivw bX (fun j => β * bX j + ε j ω) se; μ] = (∑ j, ivwWeight bX se j)⁻¹

Uses 3

Statement usesInverse-variance-weighted estimator · Inverse-variance weight of a ratio estimate

Proof usesPositivity of the total IVW weight

MR-Egger regression and InSIDE

DefinitionWeighted mean#✓fully proved

The weighted mean ∑ v_j a_j / ∑ v_j.

noncomputable def weightedMean (v a : ι → ℝ) : ℝ := (∑ j, v j * a j) / ∑ j, v j

Used by 6

Used byMR-Egger intercept · MR-Egger intercept under pleiotropy · MR-Egger slope under pleiotropy · InSIDE identity for MR-Egger · MR-Egger line is the weighted least-squares line · Weighted covariance

DefinitionWeighted covariance#✓fully proved

The weighted covariance ∑ v_j (a_j - ā_v)(b_j - b̄_v) / ∑ v_j, where ā_v and b̄_v are weighted means.

noncomputable def weightedCov (v a b : ι → ℝ) : ℝ :=
  (∑ j, v j * (a j - weightedMean v a) * (b j - weightedMean v b)) / ∑ j, v j

Uses 1 · Used by 5

Statement usesWeighted mean

Used byMR-Egger intercept under pleiotropy · MR-Egger slope · MR-Egger slope under pleiotropy · InSIDE identity for MR-Egger · MR-Egger line is the weighted least-squares line

DefinitionMR-Egger slope#✓fully proved

The MR-Egger slope (Bowden, Davey Smith & Burgess 2015): the slope of the weighted linear regression of β̂_{Yj} on β̂_{Xj} with an intercept, Cov_v(β̂_X, β̂_Y) / Var_v(β̂_X). The paper's weights are v_j = σ_j⁻².

noncomputable def eggerSlope (v bX bY : ι → ℝ) : ℝ := weightedCov v bX bY / weightedCov v bX bX

Uses 1 · Used by 5

Statement usesWeighted covariance

Used byMR-Egger intercept · MR-Egger intercept under pleiotropy · MR-Egger slope under pleiotropy · InSIDE identity for MR-Egger · MR-Egger line is the weighted least-squares line

DefinitionMR-Egger intercept#✓fully proved

The MR-Egger intercept β̂̄_Y - slope · β̂̄_X (weighted means).

noncomputable def eggerIntercept (v bX bY : ι → ℝ) : ℝ :=
  weightedMean v bY - eggerSlope v bX bY * weightedMean v bX

Uses 2 · Used by 3

Statement usesMR-Egger slope · Weighted mean

Used byMR-Egger intercept under pleiotropy · InSIDE identity for MR-Egger · MR-Egger line is the weighted least-squares line

DefinitionWeighted residual sum of squares of a line#✓fully proved

The weighted residual sum of squares ∑ v_j (β̂_{Yj} - a - b β̂_{Xj})² of the line with intercept a and slope b.

noncomputable def eggerSSR (v bX bY : ι → ℝ) (a b : ℝ) : ℝ :=
  ∑ j, v j * (bY j - a - b * bX j) ^ 2

Used by 1

Used byMR-Egger line is the weighted least-squares line

TheoremMR-Egger line is the weighted least-squares line#✓fully proved

The MR-Egger line is the weighted least-squares line: for nonnegative weights and β̂_X of nonzero weighted variance (so the total weight is positive and β̂_X is not constant on the support of the weights), it minimizes the weighted residual sum of squares.

theorem eggerSSR_le {v bX : ι → ℝ} (bY : ι → ℝ) (hv : ∀ j, 0 ≤ v j)
    (hX : weightedCov v bX bX ≠ 0) (a b : ℝ) :
    eggerSSR v bX bY (eggerIntercept v bX bY) (eggerSlope v bX bY) ≤ eggerSSR v bX bY a b

Uses 5

Statement usesMR-Egger intercept · Weighted residual sum of squares of a line · MR-Egger slope · Weighted covariance

Proof usesWeighted mean

TheoremMR-Egger slope under pleiotropy#✓fully proved

The MR-Egger slope under pleiotropy (Bowden, Davey Smith & Burgess 2015): if the SNP–outcome associations are Γ_j = α_j + β γ_j, with pleiotropic terms α_j and SNP–exposure associations γ_j, the Egger slope of Γ on γ is β + Cov_v(γ, α) / Var_v(γ).

theorem eggerSlope_eq {v γ : ι → ℝ} (hγ : weightedCov v γ γ ≠ 0)
    (α : ι → ℝ) (β : ℝ) :
    eggerSlope v γ (fun j => α j + β * γ j) = β + weightedCov v γ α / weightedCov v γ γ

Uses 3 · Used by 2

Statement usesMR-Egger slope · Weighted covariance

Proof usesWeighted mean

Used byMR-Egger intercept under pleiotropy · InSIDE identity for MR-Egger

TheoremMR-Egger intercept under pleiotropy#✓fully proved

The MR-Egger intercept under pleiotropy: it is the weighted mean pleiotropic effect ᾱ_v minus Cov_v(γ, α) / Var_v(γ) · γ̄_v.

theorem eggerIntercept_eq {v γ : ι → ℝ} (hγ : weightedCov v γ γ ≠ 0)
    (α : ι → ℝ) (β : ℝ) :
    eggerIntercept v γ (fun j => α j + β * γ j) =
      weightedMean v α - weightedCov v γ α / weightedCov v γ γ * weightedMean v γ

Uses 5 · Used by 1

Statement usesMR-Egger intercept · Weighted covariance · Weighted mean

Proof usesMR-Egger slope · MR-Egger slope under pleiotropy

Used byInSIDE identity for MR-Egger

TheoremInSIDE identity for MR-Egger#✓fully proved

The finite-sample InSIDE identity (Bowden, Davey Smith & Burgess 2015): if the pleiotropic terms are uncorrelated with the instrument strengths in the weighted sense, Cov_v(α, γ) = 0, the MR-Egger slope is the coefficient β and the intercept is the weighted mean pleiotropic term ᾱ_v. This identity alone does not encode a causal interpretation.

theorem eggerSlope_eq_of_inside {v γ α : ι → ℝ} (hγ : weightedCov v γ γ ≠ 0)
    (hinside : weightedCov v α γ = 0) (β : ℝ) :
    eggerSlope v γ (fun j => α j + β * γ j) = β ∧
      eggerIntercept v γ (fun j => α j + β * γ j) = weightedMean v α

Uses 6

Statement usesMR-Egger intercept · MR-Egger slope · Weighted covariance · Weighted mean

Proof usesMR-Egger intercept under pleiotropy · MR-Egger slope under pleiotropy

TheoremDirectional pleiotropy biases the IVW estimator#✓fully proved

Directional pleiotropy biases IVW: if Γ_j = α_j + β γ_j, the IVW estimate is β + ∑ γ_j α_j σ_j⁻² / ∑ γ_j² σ_j⁻². For example a common pleiotropic term α_j = α ≠ 0 biases IVW whenever ∑ γ_j σ_j⁻² ≠ 0, whereas a constant α satisfies InSIDE, so eggerSlope_eq_of_inside gives MR-Egger slope β and intercept α.

theorem ivw_of_pleiotropy {γ se : ι → ℝ} (hse : ∀ j, 0 < se j) (hγ : ∃ j, γ j ≠ 0)
    (α : ι → ℝ) (β : ℝ) :
    ivw γ (fun j => α j + β * γ j) se =
      β + (∑ j, γ j * α j / se j ^ 2) / ∑ j, ivwWeight γ se j

Uses 3

Statement usesInverse-variance-weighted estimator · Inverse-variance weight of a ratio estimate

Proof usesPositivity of the total IVW weight

Weak instruments: the ratio estimator has no mean

TheoremRatio with a Gaussian denominator has infinite first moment#✓fully proved

A ratio with a Gaussian denominator has no first moment (a classical fact, recalled in the weak-instrument analysis of Burgess & Thompson 2011): if D ~ N(m, v) with v > 0 and N is independent of D and not almost surely 0, then 𝔼|N / D| = ∞. Applied to the ratio estimator β̂_Y / β̂_X with a normally distributed SNP–exposure estimate β̂_X.

theorem lintegral_enorm_div_eq_top {μ : Measure Ω} [IsProbabilityMeasure μ] {N D : Ω → ℝ}
    {m : ℝ} {v : ℝ≥0} (hv : v ≠ 0) (hD : HasLaw D (gaussianReal m v) μ)
    (hN : AEMeasurable N μ) (hind : IndepFun N D μ) (hN0 : ¬ N =ᵐ[μ] 0) :
    ∫⁻ ω, ‖N ω / D ω‖ₑ ∂μ = ∞

Used by 1

Used byRatio of independent normal variables is not integrable

TheoremRatio of independent normal variables is not integrable#✓fully proved

The ratio of two independent normal variables, the denominator with positive variance and the numerator not almost surely zero ((mN, vN) ≠ (0, 0)), is not integrable.

theorem not_integrable_div_gaussian {μ : Measure Ω} [IsProbabilityMeasure μ] {N D : Ω → ℝ}
    {mN mD : ℝ} {vN vD : ℝ≥0} (hvD : vD ≠ 0) (hN : HasLaw N (gaussianReal mN vN) μ)
    (hD : HasLaw D (gaussianReal mD vD) μ) (hind : IndepFun N D μ) (hN0 : mN ≠ 0 ∨ vN ≠ 0) :
    ¬ Integrable (fun ω => N ω / D ω) μ

Uses 1

Proof usesRatio with a Gaussian denominator has infinite first moment

Potential outcomes and the local average treatment effect

InductiveCompliance types of Angrist, Imbens and Rubin#✓fully proved

The four compliance types of Angrist, Imbens & Rubin (1996), determined by the pair of potential treatments (D(0), D(1)).

inductive ComplianceType
  /-- `D(0) = 0`, `D(1) = 1`: takes the treatment exactly when encouraged. -/
  | complier
  /-- `D(0) = D(1) = 1`. -/
  | alwaysTaker
  /-- `D(0) = D(1) = 0`. -/
  | neverTaker
  /-- `D(0) = 1`, `D(1) = 0`: takes the treatment exactly when not encouraged. -/
  | defier
  deriving DecidableEq

Used by 5

Used byReduced form: outcome difference is the complier-weighted effect · First stage: treatment-rate difference equals complier share · Compliance type of a pair of potential treatments · Compliers in a potential-outcomes model · Compliance type of a unit

DefinitionCompliance type of a pair of potential treatments#✓fully proved

The compliance type of the potential treatments (D(0), D(1)) = (d₀, d₁).

def complianceType : Bool → Bool → ComplianceType
  | false, true => .complier
  | true, true => .alwaysTaker
  | false, false => .neverTaker
  | true, false => .defier

Uses 1 · Used by 3

Statement usesCompliance types of Angrist, Imbens and Rubin

Used byReduced form: outcome difference is the complier-weighted effect · First stage: treatment-rate difference equals complier share · Compliance type of a unit

StructurePotential-outcomes model with binary instrument and treatment#✓fully proved

A potential-outcomes model with a binary instrument and a binary treatment (Imbens & Angrist 1994; Angrist, Imbens & Rubin 1996): the assigned instrument Z, the potential treatments D(z) and the potential outcomes Y(z, d), all measurable. The observed treatment is D(Z) and the observed outcome Y(Z, D(Z)). The identifying assumptions (independence, exclusion, monotonicity, relevance) are separate predicates.

structure PotentialOutcomes (Ω : Type*) [MeasurableSpace Ω] where
  /-- The assigned instrument `Z`. -/
  instrument : Ω → Bool
  /-- The potential treatment `D(z)` under assignment `z`. -/
  treatment : Bool → Ω → Bool
  /-- The potential outcome `Y(z, d)` under assignment `z` and treatment `d`. -/
  outcome : Bool → Bool → Ω → ℝ
  /-- The instrument is measurable. -/
  measurable_instrument : Measurable instrument
  /-- The potential treatments are measurable. -/
  measurable_treatment : ∀ z, Measurable (treatment z)
  /-- The potential outcomes are measurable. -/
  measurable_outcome : ∀ z d, Measurable (outcome z d)

Used by 14

Used byMean of a variable within an instrument arm · Reduced form: outcome difference is the complier-weighted effect · First stage: treatment-rate difference equals complier share · Compliers in a potential-outcomes model · Exclusion restriction for an instrument · Independence assumption for an instrument · Monotonicity assumption (no defiers) · Observed outcome in a potential-outcomes model · Observed treatment in a potential-outcomes model · Observed treatment as a 0-1 real variable · Compliance type of a unit · Wald instrumental-variable estimand · Local average treatment effect theorem · Unrestricted algebraic identity behind the LATE theorem

DefinitionObserved treatment in a potential-outcomes model#✓fully proved

The observed treatment D = D(Z).

def observedTreatment (ω : Ω) : Bool := P.treatment (P.instrument ω) ω

Uses 1 · Used by 4

Statement usesPotential-outcomes model with binary instrument and treatment

Used byReduced form: outcome difference is the complier-weighted effect · First stage: treatment-rate difference equals complier share · Observed outcome in a potential-outcomes model · Observed treatment as a 0-1 real variable

DefinitionObserved outcome in a potential-outcomes model#✓fully proved

The observed outcome Y = Y(Z, D(Z)).

def observedOutcome (ω : Ω) : ℝ := P.outcome (P.instrument ω) (P.observedTreatment ω) ω

Uses 2 · Used by 3

Statement usesPotential-outcomes model with binary instrument and treatment · Observed treatment in a potential-outcomes model

Used byReduced form: outcome difference is the complier-weighted effect · Wald instrumental-variable estimand · Unrestricted algebraic identity behind the LATE theorem

DefinitionCompliance type of a unit#✓fully proved

The compliance type of a unit.

def type (ω : Ω) : ComplianceType := complianceType (P.treatment false ω) (P.treatment true ω)

Uses 3 · Used by 1

Statement usesCompliance types of Angrist, Imbens and Rubin · Potential-outcomes model with binary instrument and treatment · Compliance type of a pair of potential treatments

Used byCompliers in a potential-outcomes model

DefinitionCompliers in a potential-outcomes model#✓fully proved

The compliers, D(0) = 0 and D(1) = 1.

def compliers : Set Ω := {ω | P.type ω = .complier}

Uses 3 · Used by 4

Statement usesCompliance types of Angrist, Imbens and Rubin · Potential-outcomes model with binary instrument and treatment · Compliance type of a unit

Used byReduced form: outcome difference is the complier-weighted effect · First stage: treatment-rate difference equals complier share · Local average treatment effect theorem · Unrestricted algebraic identity behind the LATE theorem

DefinitionIndependence assumption for an instrument#✓fully proved

Independence (random assignment): the instrument is independent of the vector of all potential treatments and potential outcomes.

def Independence (μ : Measure Ω) : Prop :=
  IndepFun P.instrument (fun ω => (fun z => P.treatment z ω, fun z d => P.outcome z d ω)) μ

Uses 1 · Used by 4

Statement usesPotential-outcomes model with binary instrument and treatment

Used byReduced form: outcome difference is the complier-weighted effect · First stage: treatment-rate difference equals complier share · Local average treatment effect theorem · Unrestricted algebraic identity behind the LATE theorem

DefinitionExclusion restriction for an instrument#✓fully proved

Exclusion: the instrument affects the outcome only through the treatment, Y(0, d) = Y(1, d).

def Exclusion : Prop := ∀ d ω, P.outcome false d ω = P.outcome true d ω

Uses 1 · Used by 3

Statement usesPotential-outcomes model with binary instrument and treatment

Used byReduced form: outcome difference is the complier-weighted effect · Local average treatment effect theorem · Unrestricted algebraic identity behind the LATE theorem

DefinitionMonotonicity assumption (no defiers)#✓fully proved

Monotonicity: assignment never decreases the treatment, D(0) ≤ D(1); there are no defiers.

def Monotonicity : Prop := ∀ ω, P.treatment false ω ≤ P.treatment true ω

Uses 1 · Used by 4

Statement usesPotential-outcomes model with binary instrument and treatment

Used byReduced form: outcome difference is the complier-weighted effect · First stage: treatment-rate difference equals complier share · Local average treatment effect theorem · Unrestricted algebraic identity behind the LATE theorem

DefinitionMean of a variable within an instrument arm#✓fully proved

The mean of f in the arm Z = z, 𝔼[f | Z = z], the expectation under the conditional measure. It is the junk value 0 when P(Z = z) = 0.

noncomputable def armMean (μ : Measure Ω) (f : Ω → ℝ) (z : Bool) : ℝ :=
  ∫ ω, f ω ∂μ[|P.instrument ⁻¹' {z}]

Uses 1 · Used by 4

Statement usesPotential-outcomes model with binary instrument and treatment

Used byReduced form: outcome difference is the complier-weighted effect · First stage: treatment-rate difference equals complier share · Wald instrumental-variable estimand · Unrestricted algebraic identity behind the LATE theorem

DefinitionObserved treatment as a 0-1 real variable#✓fully proved

The observed treatment as a 0/1 real variable.

def treated (ω : Ω) : ℝ := if P.observedTreatment ω then 1 else 0

Uses 2 · Used by 3

Statement usesPotential-outcomes model with binary instrument and treatment · Observed treatment in a potential-outcomes model

Used byFirst stage: treatment-rate difference equals complier share · Wald instrumental-variable estimand · Unrestricted algebraic identity behind the LATE theorem

DefinitionWald instrumental-variable estimand#✓fully proved

The Wald (instrumental-variable) estimand (𝔼[Y | Z = 1] - 𝔼[Y | Z = 0]) / (𝔼[D | Z = 1] - 𝔼[D | Z = 0]).

noncomputable def waldEstimand (μ : Measure Ω) : ℝ :=
  (P.armMean μ P.observedOutcome true - P.armMean μ P.observedOutcome false) /
    (P.armMean μ P.treated true - P.armMean μ P.treated false)

Uses 4 · Used by 2

Statement usesPotential-outcomes model with binary instrument and treatment · Mean of a variable within an instrument arm · Observed outcome in a potential-outcomes model · Observed treatment as a 0-1 real variable

Used byLocal average treatment effect theorem · Unrestricted algebraic identity behind the LATE theorem

TheoremFirst stage: treatment-rate difference equals complier share#✓fully proved

The first stage (Imbens & Angrist 1994): under independence and monotonicity, with both arms of positive probability, the difference in treatment rates between the arms is the proportion of compliers.

theorem armMean_treated_sub {μ : Measure Ω} [IsProbabilityMeasure μ]
    (hind : P.Independence μ) (hmono : P.Monotonicity)
    (hZ : ∀ z, μ (P.instrument ⁻¹' {z}) ≠ 0) :
    P.armMean μ P.treated true - P.armMean μ P.treated false = μ.real P.compliers

Uses 9 · Used by 1

Statement usesPotential-outcomes model with binary instrument and treatment · Independence assumption for an instrument · Monotonicity assumption (no defiers) · Mean of a variable within an instrument arm · Compliers in a potential-outcomes model · Observed treatment as a 0-1 real variable

Proof usesCompliance types of Angrist, Imbens and Rubin · Observed treatment in a potential-outcomes model · Compliance type of a pair of potential treatments

Used byUnrestricted algebraic identity behind the LATE theorem

TheoremReduced form: outcome difference is the complier-weighted effect#✓fully proved

The reduced form (Imbens & Angrist 1994): under independence, exclusion and monotonicity, with integrable potential outcomes and both arms of positive probability, the difference in mean outcomes between the arms is 𝔼[(Y(z, 1) - Y(z, 0)) 1_complier], for either z.

theorem armMean_outcome_sub {μ : Measure Ω} [IsProbabilityMeasure μ]
    (hind : P.Independence μ) (hexcl : P.Exclusion) (hmono : P.Monotonicity)
    (hY : ∀ z d, Integrable (P.outcome z d) μ) (hZ : ∀ z, μ (P.instrument ⁻¹' {z}) ≠ 0)
    (z : Bool) :
    P.armMean μ P.observedOutcome true - P.armMean μ P.observedOutcome false =
      ∫ ω in P.compliers, P.outcome z true ω - P.outcome z false ω ∂μ

Uses 10 · Used by 1

Statement usesPotential-outcomes model with binary instrument and treatment · Exclusion restriction for an instrument · Independence assumption for an instrument · Monotonicity assumption (no defiers) · Mean of a variable within an instrument arm · Compliers in a potential-outcomes model · Observed outcome in a potential-outcomes model

Proof usesCompliance types of Angrist, Imbens and Rubin · Observed treatment in a potential-outcomes model · Compliance type of a pair of potential treatments

Used byUnrestricted algebraic identity behind the LATE theorem

TheoremUnrestricted algebraic identity behind the LATE theorem#✓fully proved

The unrestricted algebraic identity behind LATE. If the complier set has measure zero, both sides totalize to 0; therefore this theorem is not an identification or complier-average claim at that boundary. Use waldEstimand_eq_late for the source-faithful result with relevance.

theorem waldEstimand_eq_late_totalized {μ : Measure Ω} [IsProbabilityMeasure μ]
    (hind : P.Independence μ) (hexcl : P.Exclusion) (hmono : P.Monotonicity)
    (hY : ∀ z d, Integrable (P.outcome z d) μ)
    (hZ : ∀ z, μ (P.instrument ⁻¹' {z}) ≠ 0) (z : Bool) :
    P.waldEstimand μ = ∫ ω, P.outcome z true ω - P.outcome z false ω ∂μ[|P.compliers]

Uses 11 · Used by 1

Statement usesPotential-outcomes model with binary instrument and treatment · Exclusion restriction for an instrument · Independence assumption for an instrument · Monotonicity assumption (no defiers) · Compliers in a potential-outcomes model · Wald instrumental-variable estimand

Proof usesMean of a variable within an instrument arm · Reduced form: outcome difference is the complier-weighted effect · First stage: treatment-rate difference equals complier share · Observed outcome in a potential-outcomes model · Observed treatment as a 0-1 real variable

Used byLocal average treatment effect theorem

TheoremLocal average treatment effect theorem#✓fully proved

The local average treatment effect theorem (Imbens & Angrist 1994, Theorem 1; Angrist, Imbens & Rubin 1996): under independence, exclusion, monotonicity and relevance, with integrable potential outcomes and both arms of positive probability, the Wald estimand is the average treatment effect among compliers, 𝔼[Y(1) - Y(0) | complier] (read at either instrument value z, which exclusion makes irrelevant). Relevance is the nonzero complier mass hypothesis; by armMean_treated_sub, it is equivalent here to a nonzero Wald denominator.

theorem waldEstimand_eq_late {μ : Measure Ω} [IsProbabilityMeasure μ]
    (hind : P.Independence μ) (hexcl : P.Exclusion) (hmono : P.Monotonicity)
    (hY : ∀ z d, Integrable (P.outcome z d) μ)
    (hZ : ∀ z, μ (P.instrument ⁻¹' {z}) ≠ 0) (hC : μ P.compliers ≠ 0) (z : Bool) :
    P.waldEstimand μ = ∫ ω, P.outcome z true ω - P.outcome z false ω ∂μ[|P.compliers]

Uses 7

Statement usesPotential-outcomes model with binary instrument and treatment · Exclusion restriction for an instrument · Independence assumption for an instrument · Monotonicity assumption (no defiers) · Compliers in a potential-outcomes model · Wald instrumental-variable estimand

Proof usesUnrestricted algebraic identity behind the LATE theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.