Potential outcomes and causal identification

26 fully proved

Finite-population randomization inference (Neyman 1923)

DefinitionSample mean over a set of units#✓fully proved

The mean of y over a set of units S, (1/|S|) ∑_{i ∈ S} yᵢ (the junk value 0 for S = ∅).

noncomputable def sampleMean (y : ι → ℝ) (S : Finset ι) : ℝ :=
  (∑ i ∈ S, y i) / S.card

Used by 5

Used byDifference-in-means estimator · Neyman (1923) · Expectation of Neyman's variance estimator under complete randomization · Neyman (1923) · Sample variance over a set of units

DefinitionSample variance over a set of units#✓fully proved

The sample variance of y over S with divisor |S| - 1; meaningful for |S| ≥ 2 (for |S| ≤ 1 it is the junk value 0).

noncomputable def sampleVar (y : ι → ℝ) (S : Finset ι) : ℝ :=
  (∑ i ∈ S, (y i - sampleMean y S) ^ 2) / ((S.card : ℝ) - 1)

Uses 1 · Used by 2

Statement usesSample mean over a set of units

Used byNeyman's variance estimator · Expectation of Neyman's variance estimator under complete randomization

DefinitionMean of a finite population#✓fully proved

The mean of a finite population of N = Fintype.card ι units, (1/N) ∑ᵢ yᵢ.

noncomputable def popMean (y : ι → ℝ) : ℝ :=
  (∑ i, y i) / Fintype.card ι

Used by 6

Used byFinite-population average treatment effect · Variance of a finite population · Neyman (1923) · Expectation of Neyman's variance estimator under complete randomization · Neyman (1923) · Neyman's variance estimator is conservative

DefinitionVariance of a finite population#✓fully proved

The variance of a finite population with divisor N - 1, S² = ∑ᵢ (yᵢ - ȳ)² / (N - 1); meaningful for N ≥ 2.

noncomputable def popVar (y : ι → ℝ) : ℝ :=
  (∑ i, (y i - popMean y) ^ 2) / ((Fintype.card ι : ℝ) - 1)

Uses 1 · Used by 3

Statement usesMean of a finite population

Used byExpectation of Neyman's variance estimator under complete randomization · Neyman (1923) · Neyman's variance estimator is conservative

DefinitionFinite-population average treatment effect#✓fully proved

The finite-population average treatment effect (1/N) ∑ᵢ (y₁ᵢ - y₀ᵢ).

noncomputable def ate (y₀ y₁ : ι → ℝ) : ℝ :=
  popMean fun i => y₁ i - y₀ i

Uses 1 · Used by 3

Statement usesMean of a finite population

Used byNeyman (1923) · Neyman (1923) · Neyman's variance estimator is conservative

DefinitionDifference-in-means estimator#✓fully proved

The difference in means for the treated set S: the mean of the treated outcomes y₁ over S minus the mean of the control outcomes y₀ over the complement.

noncomputable def diffInMeans [DecidableEq ι] (y₀ y₁ : ι → ℝ) (S : Finset ι) : ℝ :=
  sampleMean y₁ S - sampleMean y₀ Sᶜ

Uses 1 · Used by 3

Statement usesSample mean over a set of units

Used byNeyman (1923) · Neyman (1923) · Neyman's variance estimator is conservative

DefinitionNeyman's variance estimator#✓fully proved

Neyman's variance estimator s₁² / n₁ + s₀² / n₀ for the treated set S.

noncomputable def neymanVar [DecidableEq ι] (y₀ y₁ : ι → ℝ) (S : Finset ι) : ℝ :=
  sampleVar y₁ S / S.card + sampleVar y₀ Sᶜ / (Sᶜ).card

Uses 1 · Used by 2

Statement usesSample variance over a set of units

Used byExpectation of Neyman's variance estimator under complete randomization · Neyman's variance estimator is conservative

DefinitionExpectation of a statistic under complete randomization#✓fully proved

The expectation of a statistic f of the treated set under complete randomization: the treated set is uniform among the (N choose n₁) sets of n₁ units (n₁ ≤ N; for n₁ > N there is no such set and the value is 0).

noncomputable def randExp (n₁ : ℕ) (f : Finset ι → ℝ) : ℝ :=
  (∑ S ∈ univ.powersetCard n₁, f S) / (Fintype.card ι).choose n₁

Used by 4

Used byNeyman (1923) · Expectation of Neyman's variance estimator under complete randomization · Neyman (1923) · Neyman's variance estimator is conservative

TheoremNeyman (1923)#✓fully proved

Under complete randomization with n₁ ≥ 1 treated and n₀ ≥ 1 control units, the difference in means is unbiased for the finite-population average treatment effect.

theorem randExp_diffInMeans [DecidableEq ι] (y₀ y₁ : ι → ℝ) {n₁ : ℕ} (h₁ : 1 ≤ n₁)
    (h₀ : n₁ + 1 ≤ Fintype.card ι) :
    randExp n₁ (diffInMeans y₀ y₁) = ate y₀ y₁

Uses 5

Statement usesFinite-population average treatment effect · Difference-in-means estimator · Expectation of a statistic under complete randomization

Proof usesMean of a finite population · Sample mean over a set of units

TheoremNeyman (1923)#✓fully proved

The variance of the difference in means under complete randomization is S₁²/n₁ + S₀²/n₀ - S_τ²/N, where S_τ² is the population variance of the unit-level effects τᵢ = y₁ᵢ - y₀ᵢ and n₀ = N - n₁.

theorem randExp_sq_diffInMeans_sub_ate [DecidableEq ι] (y₀ y₁ : ι → ℝ) {n₁ : ℕ} (h₁ : 1 ≤ n₁)
    (h₀ : n₁ + 1 ≤ Fintype.card ι) :
    randExp n₁ (fun S => (diffInMeans y₀ y₁ S - ate y₀ y₁) ^ 2) =
      popVar y₁ / n₁ + popVar y₀ / ((Fintype.card ι : ℝ) - n₁) -
        popVar (fun i => y₁ i - y₀ i) / Fintype.card ι

Uses 6 · Used by 1

Statement usesFinite-population average treatment effect · Difference-in-means estimator · Variance of a finite population · Expectation of a statistic under complete randomization

Proof usesMean of a finite population · Sample mean over a set of units

Used byNeyman's variance estimator is conservative

TheoremExpectation of Neyman's variance estimator under complete randomization#✓fully proved

The expectation of Neyman's variance estimator under complete randomization with at least two treated and two control units is S₁²/n₁ + S₀²/n₀ (the sample variances are unbiased for the population variances under sampling without replacement).

theorem randExp_neymanVar [DecidableEq ι] (y₀ y₁ : ι → ℝ) {n₁ : ℕ} (h₁ : 2 ≤ n₁)
    (h₀ : n₁ + 2 ≤ Fintype.card ι) :
    randExp n₁ (neymanVar y₀ y₁) =
      popVar y₁ / n₁ + popVar y₀ / ((Fintype.card ι : ℝ) - n₁)

Uses 6 · Used by 1

Statement usesNeyman's variance estimator · Variance of a finite population · Expectation of a statistic under complete randomization

Proof usesMean of a finite population · Sample mean over a set of units · Sample variance over a set of units

Used byNeyman's variance estimator is conservative

TheoremNeyman's variance estimator is conservative#✓fully proved

Its expectation under complete randomization is at least the variance of the difference in means, with equality exactly when the treatment effect y₁ᵢ - y₀ᵢ is the same for all units.

theorem randVar_le_randExp_neymanVar [DecidableEq ι] (y₀ y₁ : ι → ℝ) {n₁ : ℕ} (h₁ : 2 ≤ n₁)
    (h₀ : n₁ + 2 ≤ Fintype.card ι) :
    randExp n₁ (fun S => (diffInMeans y₀ y₁ S - ate y₀ y₁) ^ 2) ≤
        randExp n₁ (neymanVar y₀ y₁) ∧
      (randExp n₁ (fun S => (diffInMeans y₀ y₁ S - ate y₀ y₁) ^ 2) =
          randExp n₁ (neymanVar y₀ y₁) ↔ ∃ c, ∀ i, y₁ i - y₀ i = c)

Uses 8

Statement usesFinite-population average treatment effect · Difference-in-means estimator · Neyman's variance estimator · Expectation of a statistic under complete randomization

Proof usesMean of a finite population · Variance of a finite population · Expectation of Neyman's variance estimator under complete randomization · Neyman (1923)

Observed outcomes, propensity score and strong ignorability

DefinitionObserved outcome from potential outcomes#✓fully proved

The observed outcome: Y₁ on the treated event T, Y₀ off it (consistency).

noncomputable def observed (T : Set Ω) (Y₀ Y₁ : Ω → ℝ) : Ω → ℝ :=
  T.indicator Y₁ + Tᶜ.indicator Y₀

Used by 4

Used byIdentification of the average treatment effect by inverse probability weighting · Inverse probability weighting · Inverse probability weighting · Inverse probability weighting with a general covariate

DefinitionPropensity score#✓fully proved

The propensity of the event T given W = w, P(T ∩ {W = w}) / P(W = w). Meaningful for P(W = w) > 0; it is 0 (a junk value) when P(W = w) = 0.

noncomputable def propensity (μ : Measure Ω) (T : Set Ω) (W : Ω → β) (w : β) : ℝ :=
  μ.real (T ∩ W ⁻¹' {w}) / μ.real (W ⁻¹' {w})

Used by 10

Used byStrong ignorability passes to functions of the potential outcomes · Rosenbaum & Rubin (1983), Theorem 3 · Rosenbaum & Rubin (1983), Theorem 2 · Rosenbaum & Rubin (1983), Theorem 1 · Identification of the average treatment effect by inverse probability weighting · Inverse probability weighting · Inverse probability weighting · Calibration of the propensity score · Strong ignorability · Rosenbaum & Rubin (1983), Theorem 3

DefinitionConditional independence given a discrete variable#✓fully proved

The event T is conditionally independent of V given W, stated through the values of W: P(T, V ∈ B, W = w) P(W = w) = P(T, W = w) P(V ∈ B, W = w) for all measurable B and all w. For a W with countably many values this is the conditional independence of the indicator of T and V given W.

def CondIndepDiscrete [MeasurableSpace β] (μ : Measure Ω) (T : Set Ω) (V : Ω → β) (W : Ω → γ) :
    Prop :=
  ∀ B : Set β, MeasurableSet B → ∀ w : γ,
    μ.real (T ∩ V ⁻¹' B ∩ W ⁻¹' {w}) * μ.real (W ⁻¹' {w}) =
      μ.real (T ∩ W ⁻¹' {w}) * μ.real (V ⁻¹' B ∩ W ⁻¹' {w})

Used by 8

Used byStrong ignorability passes to functions of the potential outcomes · Rosenbaum & Rubin (1983), Theorem 3 · Rosenbaum & Rubin (1983), Theorem 2 · Rosenbaum & Rubin (1983), Theorem 1 · Identification of the average treatment effect by inverse probability weighting · Inverse probability weighting · Inverse probability weighting · Strong ignorability

DefinitionStrong ignorability#✓fully proved

Strong ignorability of the treatment T given W for the potential outcomes V (Rosenbaum & Rubin 1983): T ⊥ V | W and overlap, 0 < P(T | W = w) < 1 for every value w of positive probability.

def StronglyIgnorable [MeasurableSpace β] (μ : Measure Ω) (T : Set Ω) (V : Ω → β) (W : Ω → γ) :
    Prop :=
  CondIndepDiscrete μ T V W ∧
    ∀ w, μ (W ⁻¹' {w}) ≠ 0 → 0 < propensity μ T W w ∧ propensity μ T W w < 1

Uses 2 · Used by 6

Statement usesConditional independence given a discrete variable · Propensity score

Used byStrong ignorability passes to functions of the potential outcomes · Rosenbaum & Rubin (1983), Theorem 3 · Identification of the average treatment effect by inverse probability weighting · Inverse probability weighting · Inverse probability weighting · Rosenbaum & Rubin (1983), Theorem 3

TheoremStrong ignorability passes to functions of the potential outcomes#✓fully proved

Strong ignorability is inherited by measurable functions of the potential outcomes.

theorem StronglyIgnorable.comp [MeasurableSpace β] [MeasurableSpace γ] {T : Set Ω}
    {V : Ω → β} {δ : Type*} {W : Ω → δ} (h : StronglyIgnorable μ T V W) {g : β → γ}
    (hg : Measurable g) :
    StronglyIgnorable μ T (g ∘ V) W

Uses 3 · Used by 1

Statement usesStrong ignorability

Proof usesConditional independence given a discrete variable · Propensity score

Used byIdentification of the average treatment effect by inverse probability weighting

TheoremRosenbaum & Rubin (1983), Theorem 1#✓fully proved

The propensity score e(X) = P(T | X) is a balancing score: given e(X), the treatment is conditionally independent of the covariate X.

theorem condIndepDiscrete_propensity [IsFiniteMeasure μ] {T : Set Ω} (hT : MeasurableSet T)
    {X : Ω → 𝒳} (hX : Measurable X) :
    CondIndepDiscrete μ T X (fun ω => propensity μ T X (X ω))

Uses 2 · Used by 1

Statement usesConditional independence given a discrete variable · Propensity score

Used byRosenbaum & Rubin (1983), Theorem 3

TheoremCalibration of the propensity score#✓fully proved

The propensity score is calibrated: among units with score c (an event of positive probability), the proportion treated is c.

theorem propensity_propensity [IsFiniteMeasure μ] {T : Set Ω} (hT : MeasurableSet T)
    {X : Ω → 𝒳} (hX : Measurable X) {c : ℝ}
    (hc : μ ((fun ω => propensity μ T X (X ω)) ⁻¹' {c}) ≠ 0) :
    propensity μ T (fun ω => propensity μ T X (X ω)) c = c

Uses 1

Statement usesPropensity score

TheoremRosenbaum & Rubin (1983), Theorem 2#✓fully proved

A function b(X) of the covariate is a balancing score (T ⊥ X | b(X)) if and only if it is finer than the propensity score: covariate values of positive probability with the same b have the same propensity. (Theorem 1 is the case b = e.)

theorem condIndepDiscrete_comp_iff [IsFiniteMeasure μ] {T : Set Ω} (hT : MeasurableSet T)
    {X : Ω → 𝒳} (hX : Measurable X) {δ : Type*} (b : 𝒳 → δ) :
    CondIndepDiscrete μ T X (fun ω => b (X ω)) ↔
      ∀ x x', μ (X ⁻¹' {x}) ≠ 0 → μ (X ⁻¹' {x'}) ≠ 0 → b x = b x' →
        propensity μ T X x = propensity μ T X x'

Uses 2 · Used by 1

Statement usesConditional independence given a discrete variable · Propensity score

Used byRosenbaum & Rubin (1983), Theorem 3

TheoremRosenbaum & Rubin (1983), Theorem 3#✓fully proved

If treatment assignment is strongly ignorable given the covariate X, it is strongly ignorable given any balancing score b(X).

theorem StronglyIgnorable.comp_of_balancing [IsFiniteMeasure μ] [MeasurableSpace β] {T : Set Ω}
    (hT : MeasurableSet T) {V : Ω → β} (hV : Measurable V) {X : Ω → 𝒳} (hX : Measurable X)
    {δ : Type*} (b : 𝒳 → δ) (hb : CondIndepDiscrete μ T X (fun ω => b (X ω)))
    (h : StronglyIgnorable μ T V X) :
    StronglyIgnorable μ T V (fun ω => b (X ω))

Uses 4 · Used by 1

Statement usesConditional independence given a discrete variable · Strong ignorability

Proof usesRosenbaum & Rubin (1983), Theorem 2 · Propensity score

Used byRosenbaum & Rubin (1983), Theorem 3

TheoremRosenbaum & Rubin (1983), Theorem 3#✓fully proved

Rosenbaum & Rubin (1983), Theorem 3 for the propensity score: if treatment assignment is strongly ignorable given the covariate X, it is strongly ignorable given e(X).

theorem stronglyIgnorable_propensity [IsFiniteMeasure μ] [MeasurableSpace β] {T : Set Ω}
    (hT : MeasurableSet T) {V : Ω → β} (hV : Measurable V) {X : Ω → 𝒳} (hX : Measurable X)
    (h : StronglyIgnorable μ T V X) :
    StronglyIgnorable μ T V (fun ω => propensity μ T X (X ω))

Uses 4

Statement usesStrong ignorability · Propensity score

Proof usesRosenbaum & Rubin (1983), Theorem 3 · Rosenbaum & Rubin (1983), Theorem 1

TheoremInverse probability weighting#✓fully proved

Inverse probability weighting (Horvitz & Thompson 1952; Rosenbaum 1987): under strong ignorability of T given a finitely-valued covariate X for the treated potential outcome Y₁, E[1_T Y / e(X)] = E[Y₁], where Y is the observed outcome.

theorem integral_ipw_treated [IsProbabilityMeasure μ] {T : Set Ω} (hT : MeasurableSet T)
    {X : Ω → 𝒳} (hX : Measurable X) {Y₀ Y₁ : Ω → ℝ} (hY₁ : Measurable Y₁)
    (hY₁i : Integrable Y₁ μ) (h : StronglyIgnorable μ T Y₁ X) :
    ∫ ω, T.indicator (fun ω => observed T Y₀ Y₁ ω / propensity μ T X (X ω)) ω ∂μ =
      ∫ ω, Y₁ ω ∂μ

Uses 4

Statement usesStrong ignorability · Observed outcome from potential outcomes · Propensity score

Proof usesConditional independence given a discrete variable

TheoremInverse probability weighting#✓fully proved

Inverse probability weighting, control arm: under strong ignorability of T given X for Y₀, E[1_{Tᶜ} Y / (1 - e(X))] = E[Y₀].

theorem integral_ipw_control [IsProbabilityMeasure μ] {T : Set Ω} (hT : MeasurableSet T)
    {X : Ω → 𝒳} (hX : Measurable X) {Y₀ Y₁ : Ω → ℝ} (hY₀ : Measurable Y₀)
    (hY₀i : Integrable Y₀ μ) (h : StronglyIgnorable μ T Y₀ X) :
    ∫ ω, Tᶜ.indicator (fun ω => observed T Y₀ Y₁ ω / (1 - propensity μ T X (X ω))) ω ∂μ =
      ∫ ω, Y₀ ω ∂μ

Uses 4

Statement usesStrong ignorability · Observed outcome from potential outcomes · Propensity score

Proof usesConditional independence given a discrete variable

TheoremIdentification of the average treatment effect by inverse probability weighting#✓fully proved

Under strong ignorability of T given a finitely-valued X for the pair (Y₀, Y₁), E[1_T Y / e(X) - 1_{Tᶜ} Y / (1 - e(X))] = E[Y₁ - Y₀].

theorem integral_ipw_ate [IsProbabilityMeasure μ] {T : Set Ω} (hT : MeasurableSet T)
    {X : Ω → 𝒳} (hX : Measurable X) {Y₀ Y₁ : Ω → ℝ} (hY₀ : Measurable Y₀) (hY₁ : Measurable Y₁)
    (hY₀i : Integrable Y₀ μ) (hY₁i : Integrable Y₁ μ)
    (h : StronglyIgnorable μ T (fun ω => (Y₀ ω, Y₁ ω)) X) :
    ∫ ω, (T.indicator (fun ω => observed T Y₀ Y₁ ω / propensity μ T X (X ω)) ω -
        Tᶜ.indicator (fun ω => observed T Y₀ Y₁ ω / (1 - propensity μ T X (X ω))) ω) ∂μ =
      ∫ ω, (Y₁ ω - Y₀ ω) ∂μ

Uses 5

Statement usesStrong ignorability · Observed outcome from potential outcomes · Propensity score

Proof usesConditional independence given a discrete variable · Strong ignorability passes to functions of the potential outcomes

Inverse probability weighting with a general covariate

TheoremInverse probability weighting with a general covariate#✓fully proved

Let the covariate information be a sub-σ-algebra m (for example the one generated by X), and e = P(T | m) the propensity score. If Y₁ is integrable, the treatment is mean-ignorable for Y₁, E[1_T Y₁ | m] = e E[Y₁ | m] (implied by Y₁ ⊥ T | m), and overlap holds in the strong form e ≥ ε > 0, then E[1_T Y / e] = E[Y₁] for the observed outcome Y.

theorem integral_ipw_treated_condExp {m : MeasurableSpace Ω} (hm : m ≤ mΩ)
    [IsProbabilityMeasure μ] {T : Set Ω} (hT : MeasurableSet[mΩ] T) {Y₀ Y₁ : Ω → ℝ}
    (hY₁ : Integrable Y₁ μ)
    (hign : μ[T.indicator Y₁ | m] =ᵐ[μ] fun ω => μ[T.indicator 1 | m] ω * μ[Y₁ | m] ω)
    {ε : ℝ} (hε : 0 < ε) (hov : ∀ᵐ ω ∂μ, ε ≤ μ[T.indicator 1 | m] ω) :
    ∫ ω, T.indicator (fun ω => observed T Y₀ Y₁ ω / μ[T.indicator 1 | m] ω) ω ∂μ =
      ∫ ω, Y₁ ω ∂μ

Uses 1

Statement usesObserved outcome from potential outcomes

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.