Experimentation.Matched­Pair­Design

Worked application of the design-based randomization substrate to the fixed-pair matched-pair design from Bai (2022), "Optimality of Matched-Pair Designs in Randomized Controlled Trials" (American Economic Review).

Matched­Pair 6 core · 2 supporting Matched-pair designs organize units into pairs indexed by P, with the two members of each pair represented by positions Bool. ★ matchedPairDesign★ matchedPairDesign_E_mpTreatInd★ matchedPairDesign_E_mpTreatInd_within★ matchedPairDesign_E_mpTreatInd_cross

Matched-pair designs

Matched-pair designs organize units into pairs indexed by P, with the two members of each pair represented by positions Bool. The assignment z p is a pair-level fair coin selecting the treated position, so this is not independent assignment over the 2|P| units: each size-two stratum treats exactly one unit.

This file defines the fair coin pairCoinDesign, the product design matchedPairDesign, and the treatment indicator mpTreatInd. The main inclusion results prove within-pair exclusivity, first-order inclusion probability 1/2, perfect within-pair negative dependence, and cross-pair independence with joint probability 1/4.

def pairCoinDesign reviewed
Causalean.Experimentation.MatchedPairDesign

The per-pair fair-coin randomization design assigns probability one half to each of the two positions: one outcome selects the first position for treatment and the other selects the second position.

Definition (Lean source)
def
pairCoinDesign :
FiniteDesign Bool
given by
coinDesign ((1 : ℝ) / 2) (by norm_num) (by norm_num)
Causalean.Experimentation.MatchedPairDesign.pairCoinDesign · Causalean/Experimentation/MatchedPairDesign/MatchedPair.lean:48 · uses FiniteDesign
def matchedPairDesign reviewed
Causalean.Experimentation.MatchedPairDesign

For a finite collection of pair labels with decidable identity, the matched-pair randomization design independently draws a fair coin for every pair and treats the position selected by that coin, leaving the other position as control. This is a size-two stratified design with one treated unit in each pair rather than independent assignment over all units.

Definition (Lean source)
parameters
P :
Type u_1
shared
def
matchedPairDesign :
FiniteDesign (P → Bool)
given by
prodDesign (fun _ : P => pairCoinDesign)
Causalean.Experimentation.MatchedPairDesign.matchedPairDesign · Causalean/Experimentation/MatchedPairDesign/MatchedPair.lean:54 · uses FiniteDesign
def mpTreatInd reviewed
Causalean.Experimentation.MatchedPairDesign

For a pair label, one of its two positions, and an assignment selecting a treated position in every pair, the treatment indicator for that unit equals one when the assignment selects that position and zero otherwise.

Definition (Lean source)
parameters
P :
Type u_1
shared
p :
P
b :
Bool
z :
P → Bool
def
mpTreatInd p b z :
ℝ
given by
if z p = b then 1 else 0
Causalean.Experimentation.MatchedPairDesign.mpTreatInd · Causalean/Experimentation/MatchedPairDesign/MatchedPair.lean:66
lemma matchedPairDesign_E_mpTreatInd reviewed
Causalean.Experimentation.MatchedPairDesign

First-order inclusion probability. Under the matched-pair design, the unit occupying position b of pair p is treated with probability 1/2.

Formal statement
hypotheses
P :
Type u_1
shared
p :
P
b :
Bool
conclusion
(matchedPairDesign (P := P)).E (mpTreatInd p b) = 1 / 2
Proof (Lean source)
lemma matchedPairDesign_E_mpTreatInd (p : P) (b : Bool) : (matchedPairDesign (P := P)).E (mpTreatInd p b) = 1 / 2 := by change (prodDesign (fun _ : P => pairCoinDesign)).E (fun z => (fun c : Bool => if c = b then (1 : ℝ) else 0) (z p)) = 1 / 2 rw [FiniteDesign.E_prod_apply (fun _ : P => pairCoinDesign) p (fun c : Bool => if c = b then (1 : ℝ) else 0)] unfold pairCoinDesign rw [coinDesign_E] cases b <;> norm_num
Causalean.Experimentation.MatchedPairDesign.matchedPairDesign_E_mpTreatInd · Causalean/Experimentation/MatchedPairDesign/MatchedPair.lean:79 · uses E , matchedPairDesign , mpTreatInd
lemma matchedPairDesign_E_mpTreatInd_within reviewed
Causalean.Experimentation.MatchedPairDesign

Within-pair negative dependence. Under the matched-pair design, the two units of pair p are never treated together, so the expectation of the product of their treatment indicators is zero — perfect negative dependence.

Formal statement
hypotheses
P :
Type u_1
shared
p :
P
conclusion
(matchedPairDesign (P := P)).E (fun z => mpTreatInd p true z * mpTreatInd p false z) = 0
Proof (Lean source)
lemma matchedPairDesign_E_mpTreatInd_within (p : P) : (matchedPairDesign (P := P)).E (fun z => mpTreatInd p true z * mpTreatInd p false z) = 0 := by have hzero : ∀ z : P → Bool, mpTreatInd p true z * mpTreatInd p false z = 0 := by intro z unfold mpTreatInd cases z p <;> simp rw [(matchedPairDesign (P := P)).E_congr hzero] exact (matchedPairDesign (P := P)).E_const 0
Causalean.Experimentation.MatchedPairDesign.matchedPairDesign_E_mpTreatInd_within · Causalean/Experimentation/MatchedPairDesign/MatchedPair.lean:91 · uses E , matchedPairDesign , mpTreatInd
lemma matchedPairDesign_E_mpTreatInd_cross reviewed
Causalean.Experimentation.MatchedPairDesign

Cross-pair independence. For pairs p and p' that are distinct, the probability that position b of p and position b' of p' are treated simultaneously equals ¼ — units in distinct pairs are treated independently, and each position is treated with probability ½, so the joint probability factors as ½ · ½.

Formal statement
hypotheses
P :
Type u_1
shared
p p' :
P
h :
p ≠ p'
b b' :
Bool
conclusion
(matchedPairDesign (P := P)).E (fun z => mpTreatInd p b z * mpTreatInd p' b' z) = 1 / 4
Proof (Lean source)
lemma matchedPairDesign_E_mpTreatInd_cross (p p' : P) (h : p ≠ p') (b b' : Bool) : (matchedPairDesign (P := P)).E (fun z => mpTreatInd p b z * mpTreatInd p' b' z) = 1 / 4 := by change (prodDesign (fun _ : P => pairCoinDesign)).E (fun z => (fun c : Bool => if c = b then (1 : ℝ) else 0) (z p) * (fun c : Bool => if c = b' then (1 : ℝ) else 0) (z p')) = 1 / 4 rw [FiniteDesign.E_prod_apply₂ (fun _ : P => pairCoinDesign) h (fun c : Bool => if c = b then (1 : ℝ) else 0) (fun c : Bool => if c = b' then (1 : ℝ) else 0)] unfold pairCoinDesign rw [coinDesign_E, coinDesign_E] cases b <;> cases b' <;> norm_num
Causalean.Experimentation.MatchedPairDesign.matchedPairDesign_E_mpTreatInd_cross · Causalean/Experimentation/MatchedPairDesign/MatchedPair.lean:103 · uses E , matchedPairDesign , mpTreatInd
2 supporting declarations (lemmas, instances)
Estimator 4 core · 1 supporting For a fixed matched-pair randomization design, each unit is the position b : Bool of a pair p : P, with treated/control potential outcomes y1 p b and y0 p b. ★ sate★ matchedPairEstimator★ E_matchedPairEstimator

Matched-pair estimators

For a fixed matched-pair randomization design, each unit is the position b : Bool of a pair p : P, with treated/control potential outcomes y1 p b and y0 p b. Under the matched-pair design the coin z p selects the treated position in pair p; pairContribution records that pair's observed treated-minus-control contrast y1 p (z p) - y0 p (!z p).

This file defines the sample average treatment effect sate, the matched-pair difference-in-means estimator matchedPairEstimator, the per-pair expectation identity E_pairContribution, and the unbiasedness theorem E_matchedPairEstimator for Bai's matched-pair design.

def sate reviewed
Causalean.Experimentation.MatchedPairDesign

For a finite collection of pairs and the treated and control potential outcomes of every position in every pair, the sample average treatment effect is the sum, over both positions of all pairs, of the treated potential outcome minus the control potential outcome, divided by twice the number of pairs, with a zero denominator understood to yield zero.

Definition (Lean source)
parameters
P :
Type u_1
shared
y1 y0 :
P → Bool → ℝ
def
sate y1 y0 :
ℝ
given by
(∑ p, ∑ b, (y1 p b - y0 p b)) / (2 * (Fintype.card P : ℝ))
Causalean.Experimentation.MatchedPairDesign.sate · Causalean/Experimentation/MatchedPairDesign/Estimator.lean:46
def pairContribution reviewed
Causalean.Experimentation.MatchedPairDesign

For the treated and control potential outcomes of every position in every pair, a particular pair, and an assignment selecting a treated position in every pair, the observed treated-minus-control contribution of that pair is its treated potential outcome at the selected position minus its control potential outcome at the other position.

Definition (Lean source)
parameters
P :
Type u_1
shared
y1 y0 :
P → Bool → ℝ
p :
P
z :
P → Bool
def
pairContribution y1 y0 p z :
ℝ
given by
y1 p (z p) - y0 p (!z p)
Causalean.Experimentation.MatchedPairDesign.pairContribution · Causalean/Experimentation/MatchedPairDesign/Estimator.lean:53
def matchedPairEstimator reviewed
Causalean.Experimentation.MatchedPairDesign

For a finite collection of pairs, the treated and control potential outcomes of every position in every pair, and an assignment selecting a treated position in every pair, the matched-pair difference-in-means estimator is the sum of the observed treated-minus-control contributions across pairs divided by the number of pairs, with a zero denominator understood to yield zero.

Definition (Lean source)
parameters
P :
Type u_1
shared
y1 y0 :
P → Bool → ℝ
z :
P → Bool
def
matchedPairEstimator y1 y0 z :
ℝ
given by
(∑ p, pairContribution y1 y0 p z) / (Fintype.card P : ℝ)
Causalean.Experimentation.MatchedPairDesign.matchedPairEstimator · Causalean/Experimentation/MatchedPairDesign/Estimator.lean:60
theorem E_matchedPairEstimator reviewed
Causalean.Experimentation.MatchedPairDesign

Unbiasedness of the matched-pair estimator. Provided there is at least one pair, under the matched-pair design the difference-in-means estimator is unbiased for the sample average treatment effect.

Formal statement
hypotheses
P :
Type u_1
shared
y1 y0 :
P → Bool → ℝ
hP :
0 < card P
conclusion
(matchedPairDesign (P := P)).E (matchedPairEstimator y1 y0) = sate y1 y0
Proof (Lean source)
theorem E_matchedPairEstimator (y1 y0 : P → Bool → ℝ) (hP : 0 < Fintype.card P) : (matchedPairDesign (P := P)).E (matchedPairEstimator y1 y0) = sate y1 y0 := by unfold matchedPairEstimator sate change (matchedPairDesign (P := P)).E (fun z => (∑ p, pairContribution y1 y0 p z) * ((Fintype.card P : ℝ)⁻¹)) = (∑ p, ∑ b, (y1 p b - y0 p b)) / (2 * (Fintype.card P : ℝ)) rw [FiniteDesign.E_mul_const] rw [show (matchedPairDesign (P := P)).E (fun z => ∑ p, pairContribution y1 y0 p z) = ∑ p, (matchedPairDesign (P := P)).E (pairContribution y1 y0 p) by simpa using (FiniteDesign.E_sum (matchedPairDesign (P := P)) (univ) (fun p z => pairContribution y1 y0 p z))] simp_rw [E_pairContribution] have hN : (Fintype.card P : ℝ) ≠ 0 := by exact_mod_cast Nat.ne_of_gt hP field_simp [hN] rw [Finset.mul_sum] apply Finset.sum_congr rfl intro p hp ring
Causalean.Experimentation.MatchedPairDesign.E_matchedPairEstimator · Causalean/Experimentation/MatchedPairDesign/Estimator.lean:87 · uses E , matchedPairDesign , matchedPairEstimator , sate
1 supporting declaration (lemmas, instances)
  • E_pairContribution lemma — The expected per-pair contribution is pair p's average treatment effect ½ ∑_b (y1 p b − y0 p b) — the fair coin gives each position probability ½ of being treated.
    hypotheses
    P :
    Type u_1
    shared
    y1 y0 :
    P → Bool → ℝ
    p :
    P
    conclusion
    (matchedPairDesign (P := P)).E (pairContribution y1 y0 p) = (∑ b, (y1 p b - y0 p b)) / 2
    Proof (Lean source)
    lemma E_pairContribution (y1 y0 : P → Bool → ℝ) (p : P) : (matchedPairDesign (P := P)).E (pairContribution y1 y0 p) = (∑ b, (y1 p b - y0 p b)) / 2 := by change (prodDesign (fun k : P => coinDesign ((fun _ : P => (1 : ℝ) / 2) k) (by norm_num) (by norm_num))).E (fun z => (fun c : Bool => y1 p c - y0 p (!c)) (z p)) = (∑ b, (y1 p b - y0 p b)) / 2 rw [FiniteDesign.E_prod_apply (fun k : P => coinDesign ((fun _ : P => (1 : ℝ) / 2) k) (by norm_num) (by norm_num)) p (fun c : Bool => y1 p c - y0 p (!c)), coinDesign_E] rw [Fintype.sum_bool] norm_num ring
    Causalean.Experimentation.MatchedPairDesign.E_pairContribution · Causalean/Experimentation/MatchedPairDesign/Estimator.lean:68
Variance 2 core · 1 supporting For a fixed set of pairs, the matched-pair estimator's randomization variance equals the sum of squared within-pair imbalances, scaled by 1/(4N²). ★ Var_matchedPairEstimator

Matched-pair estimator variance

For a fixed set of pairs, the matched-pair estimator's randomization variance equals the sum of squared within-pair imbalances, scaled by 1/(4N²).

The main definition is pairImbalance, the difference across the two units in a pair of the unit totals y1 + y0. The lemma Var_pairContribution computes the variance contribution of one pair, and Var_matchedPairEstimator sums these independent pair contributions using product-design independence. The file does not compare alternative pairings or prove an optimal matching theorem.

def pairImbalance reviewed
Causalean.Experimentation.MatchedPairDesign

For the treated and control potential outcomes of every position in every pair and a particular pair, the within-pair imbalance is the difference between the two positions in the sum of their treated and control potential outcomes.

Definition (Lean source)
parameters
P :
Type u_1
shared
y1 y0 :
P → Bool → ℝ
p :
P
def
pairImbalance y1 y0 p :
ℝ
given by
(y1 p true + y0 p true) - (y1 p false + y0 p false)
Causalean.Experimentation.MatchedPairDesign.pairImbalance · Causalean/Experimentation/MatchedPairDesign/Variance.lean:47
theorem Var_matchedPairEstimator reviewed
Causalean.Experimentation.MatchedPairDesign

Variance of the matched-pair estimator. Under the matched-pair design, the difference-in-means estimator built from potential outcomes y1 and y0 has randomization variance equal to 1/(4N²) times the sum of squared within-pair imbalances.

Formal statement
hypotheses
P :
Type u_1
shared
y1 y0 :
P → Bool → ℝ
conclusion
(matchedPairDesign (P := P)).Var (matchedPairEstimator y1 y0)
= (∑ p, (pairImbalance y1 y0 p) ^ 2) / (4 * (Fintype.card P : ℝ) ^ 2)
Proof (Lean source)
theorem Var_matchedPairEstimator (y1 y0 : P → Bool → ℝ) : (matchedPairDesign (P := P)).Var (matchedPairEstimator y1 y0) = (∑ p, (pairImbalance y1 y0 p) ^ 2) / (4 * (Fintype.card P : ℝ) ^ 2) := by let D : P → FiniteDesign Bool := fun _ => coinDesign ((1 : ℝ) / 2) (by norm_num) (by norm_num) have hcongr : ∀ z : P → Bool, matchedPairEstimator y1 y0 z = ∑ p, ((Fintype.card P : ℝ)⁻¹) * (fun c : Bool => y1 p c - y0 p (!c)) (z p) := by intro z unfold matchedPairEstimator pairContribution rw [div_eq_mul_inv, Finset.sum_mul] apply Finset.sum_congr rfl intro p hp ring rw [(matchedPairDesign (P := P)).Var_congr hcongr] change (prodDesign D).Var (fun z => ∑ p, ((Fintype.card P : ℝ)⁻¹) * (fun c : Bool => y1 p c - y0 p (!c)) (z p)) = (∑ p, (pairImbalance y1 y0 p) ^ 2) / (4 * (Fintype.card P : ℝ) ^ 2) rw [FiniteDesign.Var_prod_linear_comb D (fun _ : P => (Fintype.card P : ℝ)⁻¹) (fun p c => y1 p c - y0 p (!c))] have hVar : ∀ p : P, (D p).Var (fun c : Bool => y1 p c - y0 p (!c)) = (pairImbalance y1 y0 p) ^ 2 / 4 := by intro p rw [FiniteDesign.Var_eq, coinDesign_E, coinDesign_E] unfold pairImbalance norm_num ring simp_rw [hVar] rw [show (∑ x, (Fintype.card P : ℝ)⁻¹ ^ 2 * ((pairImbalance y1 y0 x) ^ 2 / 4)) = ∑ x, (pairImbalance y1 y0 x) ^ 2 * ((Fintype.card P : ℝ)⁻¹ ^ 2 / 4) by apply Finset.sum_congr rfl intro p hp ring] rw [← Finset.sum_mul] ring_nf
Causalean.Experimentation.MatchedPairDesign.Var_matchedPairEstimator · Causalean/Experimentation/MatchedPairDesign/Variance.lean:76 · uses Var , matchedPairDesign , matchedPairEstimator , pairImbalance
1 supporting declaration (lemmas, instances)