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 Bai's fixed matched-pair design organizes units into pairs and treats exactly one of each pair's two positions, selected by an independent fair coin. ★ matchedPairDesign_E_mpTreatInd★ matchedPairDesign_E_mpTreatInd_within★ matchedPairDesign_E_mpTreatInd_cross

Matched-pair designs

Bai's fixed matched-pair design organizes units into pairs and treats exactly one of each pair's two positions, selected by an independent fair coin. It is therefore a product across pairs, not independent assignment across all units.

This file defines the pair-level coin, the product design, and its treatment indicator. The main inclusion results give treatment probability 1/2, perfect negative dependence within a pair, and independence across pairs with joint treatment probability 1/4. The file fixes the pairing; it does not compare pairings or prove an optimal matching theorem.

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:35 · 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:41 · 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:53
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:66 · 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:78 · 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:90 · uses E , matchedPairDesign , mpTreatInd
2 supporting declarations (lemmas, instances)
Estimator 4 core · 1 supporting For Bai's fixed matched-pair randomization design, a fair coin selects the treated position in each pair. ★ sate★ matchedPairEstimator★ E_matchedPairEstimator

Matched-pair estimators

For Bai's fixed matched-pair randomization design, a fair coin selects the treated position in each pair. The difference-in-means estimator averages the observed treated-minus-control contrast over pairs, while the sample average treatment effect averages both potential-outcome contrasts over all units.

This file defines those two averages and proves that the estimator is unbiased for the sample average treatment effect. The proof reduces to the one-pair marginal of the product design: each pair's observed contrast has expectation equal to that pair's average treatment effect.

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:35
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:42
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:49
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:76 · 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:57
Variance 2 core · 1 supporting For a fixed set of pairs, the matched-pair estimator's randomization variance is Var(τ̂) = (1 / 4N²) ∑ₚ ((y1 p true + y0 p true) − (y1 p false + y0 p false))². ★ Var_matchedPairEstimator

Matched-pair estimator variance

For a fixed set of pairs, the matched-pair estimator's randomization variance is

Var(τ̂) = (1 / 4N²) ∑ₚ ((y1 p true + y0 p true) − (y1 p false + y0 p false))².

The quantity inside each square is the within-pair imbalance in the units' treated-plus-control outcome totals. This file computes the fair-coin variance of one pair and sums the independent pair contributions through product-design independence. It treats the pairing as fixed and does not prove that one pairing is optimal among alternatives.

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:35
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:64 · uses Var , matchedPairDesign , matchedPairEstimator , pairImbalance
1 supporting declaration (lemmas, instances)