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: true means the true position is treated, and false means the false position is treated.

Definition (Lean source)
noncomputable def pairCoinDesign : FiniteDesign Bool := 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

The matched-pair design: each pair p independently treats one of its two positions by a fair coin. The assignment z p : Bool is the treated position in pair p; the other position is control. This is a size-two stratified design with one treated unit per stratum, represented in the smaller assignment space of treated positions rather than as independent unit-level assignments.

Definition (Lean source)
noncomputable def matchedPairDesign : FiniteDesign (P → Bool) := prodDesign (fun _ : P => pairCoinDesign)
Causalean.Experimentation.MatchedPairDesign.matchedPairDesign · Causalean/Experimentation/MatchedPairDesign/MatchedPair.lean:53 · uses FiniteDesign
def mpTreatInd reviewed
Causalean.Experimentation.MatchedPairDesign

The treatment indicator of the unit at position b of pair p under assignment z: 1 if the coin selected position b, else 0.

Definition (Lean source)
def mpTreatInd (p : P) (b : Bool) (z : P → Bool) : ℝ := if z p = b then 1 else 0
Causalean.Experimentation.MatchedPairDesign.mpTreatInd · Causalean/Experimentation/MatchedPairDesign/MatchedPair.lean:64
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 :
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:76 · 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 :
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:88 · 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 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:100 · 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

The sample average treatment effect over the 2|P| units (both positions of every pair).

Definition (Lean source)
noncomputable def sate (y1 y0 : P → Bool → ℝ) : ℝ := (∑ 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

The observed treated-minus-control contribution of pair p under assignment z: the treated position is z p (outcome y1 p (z p)), the control position is ¬ z p (outcome y0 p (¬ z p)).

Definition (Lean source)
noncomputable def pairContribution (y1 y0 : P → Bool → ℝ) (p : P) (z : P → Bool) : ℝ := y1 p (z p) - y0 p (!z p)
Causalean.Experimentation.MatchedPairDesign.pairContribution · Causalean/Experimentation/MatchedPairDesign/Estimator.lean:50
def matchedPairEstimator reviewed
Causalean.Experimentation.MatchedPairDesign

The matched-pair difference-in-means estimator: the average over pairs of the per-pair treated-minus-control contributions.

Definition (Lean source)
noncomputable def matchedPairEstimator (y1 y0 : P → Bool → ℝ) (z : P → Bool) : ℝ := (∑ p, pairContribution y1 y0 p z) / (Fintype.card P : ℝ)
Causalean.Experimentation.MatchedPairDesign.matchedPairEstimator · Causalean/Experimentation/MatchedPairDesign/Estimator.lean:56
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
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:80 · 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
    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:61
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

The within-pair imbalance of pair p: the difference, between its two positions, of the unit totals y1 + y0. Good matching makes this small.

Definition (Lean source)
noncomputable def pairImbalance (y1 y0 : P → Bool → ℝ) (p : P) : ℝ := (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
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:73 · uses Var , matchedPairDesign , matchedPairEstimator , pairImbalance
1 supporting declaration (lemmas, instances)