Experimentation.DesignBased.Designs

Coin 2 core · 0 supporting This file defines the canonical two-point Bernoulli design and its expectation formula. ★ coinDesign_E

Single-coin randomization design

This file defines the canonical two-point Bernoulli design and its expectation formula. Product Bernoulli designs and paper-specific experimentation developments reuse this common one-coordinate layer.

def coinDesign reviewed

Causalean.Experimentation.DesignBased

For a probability between zero and one, the single-unit coin randomization design assigns treatment with probability $p$ and control with probability $1-p$ .

Definition (Lean source)

parameters

p :

ℝ

hp0 :

0 ≤ p

hp1 :

p ≤ 1

def

coinDesign p hp0 hp1 :

FiniteDesign Bool

given by

clause 1

p := fun b => cond b p (1 - p)

clause 2

p_nonneg := by intro b cases b · exact sub_nonneg.mpr hp1 · exact hp0

clause 3

p_sum := by rw [Fintype.sum_bool] change p + (1 - p) = 1 ring

Causalean.Experimentation.DesignBased.coinDesign · Causalean/Experimentation/DesignBased/Designs/Coin.lean:23 · uses FiniteDesign

lemma coinDesign_E reviewed

Causalean.Experimentation.DesignBased

For a probability p lying in [0,1], the expectation of a real-valued function g of a single coin flip that lands heads with probability p equals the probability-weighted two-point sum p · g(true) + (1 − p) · g(false).

Formal statement

hypotheses

p :

ℝ

hp0 :

0 ≤ p

hp1 :

p ≤ 1

g :

Bool → ℝ

conclusion

(coinDesign p hp0 hp1).E g = p * g true + (1 - p) * g false

Proof (Lean source)

lemma coinDesign_E (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (g : Bool → ℝ) : (coinDesign p hp0 hp1).E g = p * g true + (1 - p) * g false := by simp only [FiniteDesign.E, coinDesign, Fintype.sum_bool, cond_true, cond_false]

Causalean.Experimentation.DesignBased.coinDesign_E · Causalean/Experimentation/DesignBased/Designs/Coin.lean:38 · uses E , coinDesign

Bernoulli 3 core · 5 supporting Bernoulli designs assign each unit independently with unit-specific treatment probabilities. ★ bernoulliDesign★ bernoulliDesign_E_treatInd_pair

Bernoulli randomization designs

Bernoulli designs assign each unit independently with unit-specific treatment probabilities.

This file builds the product Bernoulli design from the canonical single-coin design, then records the first- and second-order inclusion facts used by estimator bias and variance calculations.

def bernoulliDesign reviewed

Causalean.Experimentation.DesignBased

For a finite population of units, unit-specific treatment probabilities that are each between zero and one, the Bernoulli randomization design independently assigns every unit to treatment with its own specified probability.

Definition (Lean source)

parameters

U :

Type u_1

shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

def

bernoulliDesign p hp0 hp1 :

FiniteDesign (U → Bool)

given by

prodDesign (fun i => coinDesign (p i) (hp0 i) (hp1 i))

Causalean.Experimentation.DesignBased.bernoulliDesign · Causalean/Experimentation/DesignBased/Designs/Bernoulli.lean:57 · uses FiniteDesign

def treatInd reviewed

Causalean.Experimentation.DesignBased

For a finite population of units, a unit, and a treatment assignment for that population, the treatment indicator for that unit equals one when the unit is assigned treatment and zero otherwise.

Definition (Lean source)

parameters

U :

Type u_1

shared

i :

U

z :

U → Bool

def

treatInd i z :

ℝ

given by

if z i then 1 else 0

Causalean.Experimentation.DesignBased.treatInd · Causalean/Experimentation/DesignBased/Designs/Bernoulli.lean:66

lemma bernoulliDesign_E_treatInd_pair reviewed

Causalean.Experimentation.DesignBased

Second-order inclusion probability. Under the Bernoulli randomization design with per-unit treatment probabilities p i lying between 0 and 1, for two distinct units i ≠ j, the joint expectation of their treatment indicators factors as p i · p j — the units are independently assigned.

Formal statement

hypotheses

U :

Type u_1

shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

i j :

U

h :

i ≠ j

conclusion

(bernoulliDesign p hp0 hp1).E (fun z => treatInd i z * treatInd j z) = p i * p j

Proof (Lean source)

lemma bernoulliDesign_E_treatInd_pair (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) {i j : U} (h : i ≠ j) : (bernoulliDesign p hp0 hp1).E (fun z => treatInd i z * treatInd j z) = p i * p j := by change (prodDesign (fun k => coinDesign (p k) (hp0 k) (hp1 k))).E (fun z => (fun b => if b then (1 : ℝ) else 0) (z i) * (fun b => if b then (1 : ℝ) else 0) (z j)) = p i * p j rw [FiniteDesign.E_prod_apply₂ (fun k => coinDesign (p k) (hp0 k) (hp1 k)) h (fun b => if b then (1 : ℝ) else 0) (fun b => if b then (1 : ℝ) else 0), coinDesign_E_treat, coinDesign_E_treat]

Causalean.Experimentation.DesignBased.bernoulliDesign_E_treatInd_pair · Causalean/Experimentation/DesignBased/Designs/Bernoulli.lean:89 · uses E , bernoulliDesign , treatInd

5 supporting declarations (lemmas, instances)

coinDesign_E_treat lemma — The treatment indicator of a single coin, 1(true), has expectation p.

hypotheses

p :

ℝ

hp0 :

0 ≤ p

hp1 :

p ≤ 1

conclusion

(coinDesign p hp0 hp1).E (fun b => if b then (1 : ℝ) else 0) = p

Proof (Lean source)

lemma coinDesign_E_treat (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : (coinDesign p hp0 hp1).E (fun b => if b then (1 : ℝ) else 0) = p := by rw [coinDesign_E]; simp

Causalean.Experimentation.DesignBased.coinDesign_E_treat · Causalean/Experimentation/DesignBased/Designs/Bernoulli.lean:40
coinDesign_Var_treat lemma — The treatment indicator of a single coin has variance p(1 − p).

hypotheses

p :

ℝ

hp0 :

0 ≤ p

hp1 :

p ≤ 1

conclusion

(coinDesign p hp0 hp1).Var (fun b => if b then (1 : ℝ) else 0) = p * (1 - p)

Proof (Lean source)

lemma coinDesign_Var_treat (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : (coinDesign p hp0 hp1).Var (fun b => if b then (1 : ℝ) else 0) = p * (1 - p) := by rw [FiniteDesign.Var_eq, coinDesign_E_treat] have hsq : (fun b : Bool => ((if b then (1 : ℝ) else 0) : ℝ) ^ 2) = (fun b : Bool => if b then (1 : ℝ) else 0) := by funext b cases b <;> simp rw [hsq, coinDesign_E_treat] ring

Causalean.Experimentation.DesignBased.coinDesign_Var_treat · Causalean/Experimentation/DesignBased/Designs/Bernoulli.lean:45
bernoulliDesign_E_treatInd lemma — A quantity depending only on unit i's treatment coin has expectation equal to its value under treatment weighted by p i plus its value under control weighted by 1 - p i.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

i :

U

g :

Bool → ℝ

conclusion

(bernoulliDesign p hp0 hp1).E (fun z => g (z i)) = p i * g true + (1 - p i) * g false

Proof (Lean source)

lemma bernoulliDesign_E_treatInd (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (i : U) (g : Bool → ℝ) : (bernoulliDesign p hp0 hp1).E (fun z => g (z i)) = p i * g true + (1 - p i) * g false := by change (prodDesign (fun k => coinDesign (p k) (hp0 k) (hp1 k))).E (fun z => g (z i)) = p i * g true + (1 - p i) * g false rw [FiniteDesign.E_prod_apply (fun k => coinDesign (p k) (hp0 k) (hp1 k)) i g, coinDesign_E]

Causalean.Experimentation.DesignBased.bernoulliDesign_E_treatInd · Causalean/Experimentation/DesignBased/Designs/Bernoulli.lean:71
bernoulliDesign_Var_treatInd lemma — The treatment indicator of unit i has variance p i (1 − p i) under the Bernoulli design.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

i :

U

conclusion

(bernoulliDesign p hp0 hp1).Var (treatInd i) = p i * (1 - p i)

Proof (Lean source)

lemma bernoulliDesign_Var_treatInd (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (i : U) : (bernoulliDesign p hp0 hp1).Var (treatInd i) = p i * (1 - p i) := by change (prodDesign (fun k => coinDesign (p k) (hp0 k) (hp1 k))).Var (fun z => (fun b => if b then (1 : ℝ) else 0) (z i)) = p i * (1 - p i) rw [FiniteDesign.Var_prod_apply (fun k => coinDesign (p k) (hp0 k) (hp1 k)) i (fun b => if b then (1 : ℝ) else 0), coinDesign_Var_treat]

Causalean.Experimentation.DesignBased.bernoulliDesign_Var_treatInd · Causalean/Experimentation/DesignBased/Designs/Bernoulli.lean:81
bernoulliDesign_Cov_treatInd lemma — For distinct units i ≠ j, the two treatment indicators are uncorrelated under the Bernoulli design.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

i j :

U

h :

i ≠ j

conclusion

(bernoulliDesign p hp0 hp1).Cov (treatInd i) (treatInd j) = 0

Proof (Lean source)

lemma bernoulliDesign_Cov_treatInd (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) {i j : U} (h : i ≠ j) : (bernoulliDesign p hp0 hp1).Cov (treatInd i) (treatInd j) = 0 := by change (prodDesign (fun k => coinDesign (p k) (hp0 k) (hp1 k))).Cov (fun z => (fun b => if b then (1 : ℝ) else 0) (z i)) (fun z => (fun b => if b then (1 : ℝ) else 0) (z j)) = 0 rw [FiniteDesign.Cov_prod_apply_of_ne (fun k => coinDesign (p k) (hp0 k) (hp1 k)) h (fun b => if b then (1 : ℝ) else 0) (fun b => if b then (1 : ℝ) else 0)]

Causalean.Experimentation.DesignBased.bernoulliDesign_Cov_treatInd · Causalean/Experimentation/DesignBased/Designs/Bernoulli.lean:104

BernoulliMoments 3 core · 15 supporting This file provides the arbitrary-arity product-expectation identities for bernoulliDesign (bernoulliDesign_E_prod and its Finset-restricted form bernoulliDesign_E_prod_finset), the raw-monomial expectation bernoulliDesig ★ bernoulliDesign_E_centeredMonomial_mul

Product moments and centered monomials of the Bernoulli design

This file provides the arbitrary-arity product-expectation identities for bernoulliDesign (bernoulliDesign_E_prod and its Finset-restricted form bernoulliDesign_E_prod_finset), the raw-monomial expectation bernoulliDesign_E_treatInd_prod, and the centered monomial basis centeredMonomial with its orthogonality theorem bernoulliDesign_E_centeredMonomial_mul and its pairing against a raw monomial bernoulliDesign_E_centeredMonomial_mul_treatInd_prod.

It then develops the centered-monomial (Walsh/Fourier) expansion of an arbitrary statistic: exists_centeredMonomial_expansion (completeness), bernoulliDesign_E_sq_of_expansion (Parseval), and the coefficient-support facts centeredMonomial_coef_empty_eq_zero and centeredMonomial_coef_eq_zero_of_not_subset for statistics satisfying DependsOnBlock.

def centeredMonomial reviewed

Causalean.Experimentation.DesignBased

For a population of units, unit-specific treatment probabilities, and a finite set of units, the centered monomial maps each assignment to the product, over the selected units, of that unit's treatment indicator minus its treatment probability. The empty selected set gives the constant one.

Definition (Lean source)

parameters

U :

Type u_1

shared

p :

U → ℝ

S :

Finset U

def

centeredMonomial p S :

(U → Bool) → ℝ

given by

fun z => ∏ j ∈ S, (treatInd j z - p j)

Causalean.Experimentation.DesignBased.centeredMonomial · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:165

theorem bernoulliDesign_E_centeredMonomial_mul reviewed

Causalean.Experimentation.DesignBased

Orthogonality of the centered monomials. Under a Bernoulli randomization in which every unit's treatment probability p i lies in [0,1], the centered monomials attached to two finite sets of units S and T are uncorrelated whenever S ≠ T, while the monomial attached to S itself has second moment ∏_{j ∈ S} p j · (1 − p j) — the product of the per-unit assignment variances — when S = T. This is the design-based analogue of the orthonormality of a Fourier basis.

Formal statement

hypotheses

U :

Type u_1

shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

S T :

Finset U

conclusion

(bernoulliDesign p hp0 hp1).E (fun z => centeredMonomial p S z * centeredMonomial p T z)

= if S = T then ∏ j ∈ S, p j * (1 - p j) else 0

Proof (Lean source)

theorem bernoulliDesign_E_centeredMonomial_mul (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (S T : Finset U) : (bernoulliDesign p hp0 hp1).E (fun z => centeredMonomial p S z * centeredMonomial p T z) = if S = T then ∏ j ∈ S, p j * (1 - p j) else 0 := by set x : U → Bool → ℝ := fun j b => (if b then (1 : ℝ) else 0) - p j with hx rw [show (fun z : U → Bool => centeredMonomial p S z * centeredMonomial p T z) = (fun z => ∏ j, ((if j ∈ S then x j (z j) else 1) * (if j ∈ T then x j (z j) else 1))) by funext z rw [Finset.prod_mul_distrib] simp [centeredMonomial, treatInd, hx]] rw [bernoulliDesign_E_prod p hp0 hp1 (fun j b => (if j ∈ S then x j b else 1) * (if j ∈ T then x j b else 1))] by_cases hST : S = T · subst hST rw [if_pos rfl] have hfactor (j : U) : p j * ((if j ∈ S then x j true else 1) * (if j ∈ S then x j true else 1)) + (1 - p j) * ((if j ∈ S then x j false else 1) * (if j ∈ S then x j false else 1)) = if j ∈ S then p j * (1 - p j) else 1 := by by_cases hj : j ∈ S <;> simp [hj, hx] ring simp_rw [hfactor] rw [Finset.prod_ite_mem, Finset.univ_inter] · rw [if_neg hST] have hdiff : ∃ j, (j ∈ S ∧ j ∉ T) ∨ (j ∈ T ∧ j ∉ S) := by by_contra h exact hST (Finset.ext fun j => ⟨fun hjS => by by_contra hjT; exact h ⟨j, inl ⟨hjS, hjT⟩⟩, fun hjT => by by_contra hjS; exact h ⟨j, inr ⟨hjT, hjS⟩⟩⟩) obtain ⟨j, hj⟩ := hdiff refine Finset.prod_eq_zero (Finset.mem_univ j) ?_ rcases hj with hj | hj · simp [hj.1, hj.2, hx]; ring · simp [hj.1, hj.2, hx]; ring

Causalean.Experimentation.DesignBased.bernoulliDesign_E_centeredMonomial_mul · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:177 · uses E , bernoulliDesign , centeredMonomial

def DependsOnBlock reviewed

Causalean.Experimentation.DesignBased

For a population of units, a finite block of units, and a real-valued statistic of the assignment, the assertion that the statistic depends only on the block means that any two assignments agreeing on every unit in the block have the same statistic value.

Definition (Lean source)

parameters

U :

Type u_1

shared

N :

Finset U

F :

(U → Bool) → ℝ

z z' :

(∀ j ∈ N, z j = z' j)

def

DependsOnBlock N F :

Prop

given by

F z = F z'

Causalean.Experimentation.DesignBased.DependsOnBlock · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:374

15 supporting declarations (lemmas, instances)

bernoulliDesign_E_prod lemma — Independence across units turns the expectation of a product into a product of expectations: if every unit contributes a factor that depends only on its own coin, the design expectation of the whole product is the product over units of p i · g i (treated) + (1 − p i) · g i (control).

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

g :

U → Bool → ℝ

conclusion

(bernoulliDesign p hp0 hp1).E (fun z => ∏ i, g i (z i))
= ∏ i, (p i * g i true + (1 - p i) * g i false)

Proof (Lean source)

lemma bernoulliDesign_E_prod (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (g : U → Bool → ℝ) : (bernoulliDesign p hp0 hp1).E (fun z => ∏ i, g i (z i)) = ∏ i, (p i * g i true + (1 - p i) * g i false) := by unfold bernoulliDesign rw [FiniteDesign.E_prod_prod] exact Finset.prod_congr rfl fun i _ => coinDesign_E (p i) (hp0 i) (hp1 i) (g i)

Causalean.Experimentation.DesignBased.bernoulliDesign_E_prod · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:51
bernoulliDesign_E_prod_finset lemma — The same factorization when only the units in a finite set S contribute a factor: the units outside S are simply averaged out and leave no trace.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

S :

Finset U

g :

U → Bool → ℝ

conclusion

(bernoulliDesign p hp0 hp1).E (fun z => ∏ k ∈ S, g k (z k))
= ∏ k ∈ S, (p k * g k true + (1 - p k) * g k false)

Proof (Lean source)

lemma bernoulliDesign_E_prod_finset (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (S : Finset U) (g : U → Bool → ℝ) : (bernoulliDesign p hp0 hp1).E (fun z => ∏ k ∈ S, g k (z k)) = ∏ k ∈ S, (p k * g k true + (1 - p k) * g k false) := by rw [show (fun z : U → Bool => ∏ k ∈ S, g k (z k)) = (fun z => ∏ k, (fun i b => if i ∈ S then g i b else 1) k (z k)) by funext z rw [Finset.prod_ite_mem, Finset.univ_inter]] rw [bernoulliDesign_E_prod p hp0 hp1 (fun i b => if i ∈ S then g i b else 1)] rw [show (fun k => p k * (if k ∈ S then g k true else 1) + (1 - p k) * (if k ∈ S then g k false else 1)) = (fun k => if k ∈ S then p k * g k true + (1 - p k) * g k false else 1) by funext k by_cases hk : k ∈ S <;> simp [hk]] rw [Finset.prod_ite_mem, Finset.univ_inter]

Causalean.Experimentation.DesignBased.bernoulliDesign_E_prod_finset · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:62
bernoulliDesign_E_treatInd_prod theorem — Higher-order inclusion probability. The units in a finite set S are all treated together with probability ∏_{j ∈ S} p j; equivalently, the expectation of the product of their treatment indicators is the product of their treatment probabilities.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

S :

Finset U

conclusion

(bernoulliDesign p hp0 hp1).E (fun z => ∏ j ∈ S, treatInd j z) = ∏ j ∈ S, p j

Proof (Lean source)

theorem bernoulliDesign_E_treatInd_prod (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (S : Finset U) : (bernoulliDesign p hp0 hp1).E (fun z => ∏ j ∈ S, treatInd j z) = ∏ j ∈ S, p j := by rw [show (fun z : U → Bool => ∏ j ∈ S, treatInd j z) = (fun z => ∏ j ∈ S, (fun _ : U => fun b : Bool => if b then (1 : ℝ) else 0) j (z j)) from rfl] rw [bernoulliDesign_E_prod_finset p hp0 hp1 S (fun _ b => if b then (1 : ℝ) else 0)] simp

Causalean.Experimentation.DesignBased.bernoulliDesign_E_treatInd_prod · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:80
bernoulliDesign_E_ctrlInd_prod theorem — The units in a finite set S are all left untreated together with probability ∏_{j ∈ S} (1 − p j): the expectation of the product of their control indicators is the product of their control probabilities.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

S :

Finset U

conclusion

(bernoulliDesign p hp0 hp1).E (fun z => ∏ j ∈ S, (1 - treatInd j z)) = ∏ j ∈ S, (1 - p j)

Proof (Lean source)

theorem bernoulliDesign_E_ctrlInd_prod (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (S : Finset U) : (bernoulliDesign p hp0 hp1).E (fun z => ∏ j ∈ S, (1 - treatInd j z)) = ∏ j ∈ S, (1 - p j) := by rw [show (fun z : U → Bool => ∏ j ∈ S, (1 - treatInd j z)) = (fun z => ∏ j ∈ S, (fun _ : U => fun b : Bool => 1 - if b then (1 : ℝ) else 0) j (z j)) from rfl] rw [bernoulliDesign_E_prod_finset p hp0 hp1 S (fun _ b => 1 - if b then (1 : ℝ) else 0)] exact Finset.prod_congr rfl fun j _ => by simp

Causalean.Experimentation.DesignBased.bernoulliDesign_E_ctrlInd_prod · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:91
treatInd_prod_mul_prod lemma — Treatment indicators take only the values zero and one, so two overlapping products of them collapse into a single product over the union of the two sets of units.

hypotheses

U :

Type u_1
shared

S T :

Finset U

z :

U → Bool

conclusion

(∏ j ∈ S, treatInd j z) * (∏ j ∈ T, treatInd j z) = ∏ j ∈ S ∪ T, treatInd j z

Proof (Lean source)

lemma treatInd_prod_mul_prod (S T : Finset U) (z : U → Bool) : (∏ j ∈ S, treatInd j z) * (∏ j ∈ T, treatInd j z) = ∏ j ∈ S ∪ T, treatInd j z := by by_cases h : ∀ j ∈ S ∪ T, z j = true · have hone : ∀ A : Finset U, A ⊆ S ∪ T → ∏ j ∈ A, treatInd j z = 1 := fun A hA => Finset.prod_eq_one fun j hj => by simp [treatInd, h j (hA hj)] rw [hone S subset_union_left, hone T subset_union_right, hone (S ∪ T) Finset.Subset.rfl, one_mul] · push_neg at h obtain ⟨j, hj, hzj⟩ := h have hzero : treatInd j z = 0 := by simp [treatInd, Bool.eq_false_iff.mpr hzj] rw [Finset.prod_eq_zero hj hzero] rcases Finset.mem_union.mp hj with hjS | hjT · rw [Finset.prod_eq_zero hjS hzero, zero_mul] · rw [Finset.prod_eq_zero hjT hzero, mul_zero]

Causalean.Experimentation.DesignBased.treatInd_prod_mul_prod · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:105
ctrlInd_prod_mul_prod lemma — Control indicators take only the values zero and one, so two overlapping products of them collapse into a single product over the union of the two sets of units.

hypotheses

U :

Type u_1
shared

S T :

Finset U

z :

U → Bool

conclusion

(∏ j ∈ S, (1 - treatInd j z)) * (∏ j ∈ T, (1 - treatInd j z))
= ∏ j ∈ S ∪ T, (1 - treatInd j z)

Proof (Lean source)

lemma ctrlInd_prod_mul_prod (S T : Finset U) (z : U → Bool) : (∏ j ∈ S, (1 - treatInd j z)) * (∏ j ∈ T, (1 - treatInd j z)) = ∏ j ∈ S ∪ T, (1 - treatInd j z) := by by_cases h : ∀ j ∈ S ∪ T, z j = false · have hone : ∀ A : Finset U, A ⊆ S ∪ T → ∏ j ∈ A, (1 - treatInd j z) = 1 := fun A hA => Finset.prod_eq_one fun j hj => by simp [treatInd, h j (hA hj)] rw [hone S subset_union_left, hone T subset_union_right, hone (S ∪ T) Finset.Subset.rfl, one_mul] · push_neg at h obtain ⟨j, hj, hzj⟩ := h have hzj' : z j = true := by cases hzj' : z j <;> simp_all have hzero : 1 - treatInd j z = 0 := by simp [treatInd, hzj'] rw [Finset.prod_eq_zero hj hzero] rcases Finset.mem_union.mp hj with hjS | hjT · rw [Finset.prod_eq_zero hjS hzero, zero_mul] · rw [Finset.prod_eq_zero hjT hzero, mul_zero]

Causalean.Experimentation.DesignBased.ctrlInd_prod_mul_prod · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:123
bernoulliDesign_E_treatInd_prod_mul_prod theorem — Two overlapping sets of units are simultaneously treated with probability ∏_{j ∈ S ∪ T} p j: the shared units are counted once, not twice.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

S T :

Finset U

conclusion

(bernoulliDesign p hp0 hp1).E (fun z => (∏ j ∈ S, treatInd j z) * ∏ j ∈ T, treatInd j z)
= ∏ j ∈ S ∪ T, p j

Proof (Lean source)

theorem bernoulliDesign_E_treatInd_prod_mul_prod (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (S T : Finset U) : (bernoulliDesign p hp0 hp1).E (fun z => (∏ j ∈ S, treatInd j z) * ∏ j ∈ T, treatInd j z) = ∏ j ∈ S ∪ T, p j := by rw [show (fun z : U → Bool => (∏ j ∈ S, treatInd j z) * ∏ j ∈ T, treatInd j z) = (fun z => ∏ j ∈ S ∪ T, treatInd j z) from funext fun z => treatInd_prod_mul_prod S T z] exact bernoulliDesign_E_treatInd_prod p hp0 hp1 (S ∪ T)

Causalean.Experimentation.DesignBased.bernoulliDesign_E_treatInd_prod_mul_prod · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:142
bernoulliDesign_E_ctrlInd_prod_mul_prod theorem — Two overlapping sets of units are simultaneously left untreated with probability ∏_{j ∈ S ∪ T} (1 − p j): the shared units are counted once, not twice.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

S T :

Finset U

conclusion

(bernoulliDesign p hp0 hp1).E (fun z => (∏ j ∈ S, (1 - treatInd j z)) * ∏ j ∈ T, (1 - treatInd j z))
= ∏ j ∈ S ∪ T, (1 - p j)

Proof (Lean source)

theorem bernoulliDesign_E_ctrlInd_prod_mul_prod (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (S T : Finset U) : (bernoulliDesign p hp0 hp1).E (fun z => (∏ j ∈ S, (1 - treatInd j z)) * ∏ j ∈ T, (1 - treatInd j z)) = ∏ j ∈ S ∪ T, (1 - p j) := by rw [show (fun z : U → Bool => (∏ j ∈ S, (1 - treatInd j z)) * ∏ j ∈ T, (1 - treatInd j z)) = (fun z => ∏ j ∈ S ∪ T, (1 - treatInd j z)) from funext fun z => ctrlInd_prod_mul_prod S T z] exact bernoulliDesign_E_ctrlInd_prod p hp0 hp1 (S ∪ T)

Causalean.Experimentation.DesignBased.bernoulliDesign_E_ctrlInd_prod_mul_prod · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:152
centeredMonomial_empty lemma — The centered monomial of the empty set of units is the constant function 1.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

conclusion

centeredMonomial p (∅ : Finset U) = fun _ => 1

Proof (Lean source)

@[simp] lemma centeredMonomial_empty (p : U → ℝ) : centeredMonomial p (∅ : Finset U) = fun _ => 1 := rfl

Causalean.Experimentation.DesignBased.centeredMonomial_empty · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:173
bernoulliDesign_E_centeredMonomial theorem — A centered monomial has mean zero unless it is the constant one: the design expectation of the S-centered monomial is 1 when S is empty and 0 otherwise.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

S :

Finset U

conclusion

(bernoulliDesign p hp0 hp1).E (centeredMonomial p S) = if S = ∅ then 1 else 0

Proof (Lean source)

theorem bernoulliDesign_E_centeredMonomial (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (S : Finset U) : (bernoulliDesign p hp0 hp1).E (centeredMonomial p S) = if S = ∅ then 1 else 0 := by rcases eq_or_ne S ∅ with hS | hS · subst hS simp · have h := bernoulliDesign_E_centeredMonomial_mul p hp0 hp1 S ∅ have hfun : (fun z => centeredMonomial p S z * centeredMonomial p (∅ : Finset U) z) = centeredMonomial p S := by funext z simp rw [hfun, if_neg hS] at h rw [if_neg hS] exact h

Causalean.Experimentation.DesignBased.bernoulliDesign_E_centeredMonomial · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:218
bernoulliDesign_E_centeredMonomial_mul_treatInd_prod theorem — Pairing a centered monomial with a raw monomial. The expectation of the S-centered monomial times the product of the treatment indicators of a set T vanishes unless every unit of S also lies in T; when it does, it equals the product of the assignment variances p j (1 − p j) over S times the treatment probabilities of the units of T outside S.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

S T :

Finset U

conclusion

(bernoulliDesign p hp0 hp1).E (fun z => centeredMonomial p S z * ∏ j ∈ T, treatInd j z)
= if S ⊆ T then (∏ j ∈ S, p j * (1 - p j)) * ∏ j ∈ T \ S, p j else 0

Proof (Lean source)

theorem bernoulliDesign_E_centeredMonomial_mul_treatInd_prod (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (S T : Finset U) : (bernoulliDesign p hp0 hp1).E (fun z => centeredMonomial p S z * ∏ j ∈ T, treatInd j z) = if S ⊆ T then (∏ j ∈ S, p j * (1 - p j)) * ∏ j ∈ T \ S, p j else 0 := by set x : U → Bool → ℝ := fun j b => (if b then (1 : ℝ) else 0) - p j with hx set y : Bool → ℝ := fun b => if b then (1 : ℝ) else 0 with hy rw [show (fun z : U → Bool => centeredMonomial p S z * ∏ j ∈ T, treatInd j z) = (fun z => ∏ j, ((if j ∈ S then x j (z j) else 1) * (if j ∈ T then y (z j) else 1))) by funext z rw [Finset.prod_mul_distrib] simp [centeredMonomial, treatInd, hx, hy]] rw [bernoulliDesign_E_prod p hp0 hp1 (fun j b => (if j ∈ S then x j b else 1) * (if j ∈ T then y b else 1))] have hfactor (j : U) : p j * ((if j ∈ S then x j true else 1) * (if j ∈ T then y true else 1)) + (1 - p j) * ((if j ∈ S then x j false else 1) * (if j ∈ T then y false else 1)) = if j ∈ S then (if j ∈ T then p j * (1 - p j) else 0) else if j ∈ T then p j else 1 := by by_cases hjS : j ∈ S <;> by_cases hjT : j ∈ T <;> simp [hjS, hjT, hx, hy] ring simp_rw [hfactor] by_cases hsub : S ⊆ T · rw [if_pos hsub] have hsplit (j : U) : (if j ∈ S then (if j ∈ T then p j * (1 - p j) else 0) else if j ∈ T then p j else 1) = (if j ∈ S then p j * (1 - p j) else 1) * (if j ∈ T \ S then p j else 1) := by by_cases hjS : j ∈ S · simp [hjS, hsub hjS] · by_cases hjT : j ∈ T <;> simp [hjS, hjT] simp_rw [hsplit] rw [Finset.prod_mul_distrib, Finset.prod_ite_mem, Finset.univ_inter, Finset.prod_ite_mem, Finset.univ_inter] · rw [if_neg hsub] obtain ⟨j, hjS, hjT⟩ : ∃ j, j ∈ S ∧ j ∉ T := by simpa only [Finset.not_subset] using hsub exact Finset.prod_eq_zero (Finset.mem_univ j) (by simp [hjS, hjT])

Causalean.Experimentation.DesignBased.bernoulliDesign_E_centeredMonomial_mul_treatInd_prod · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:235
exists_centeredMonomial_expansion lemma — Completeness of the centered-monomial basis. Every real-valued statistic of a Bernoulli assignment can be written as a linear combination of the centered monomials indexed by the subsets of the population — the design-based Fourier (Walsh) expansion of the statistic.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

F :

(U → Bool) → ℝ

conclusion

∃ a : Finset U → ℝ,
∀ z, F z = ∑ S ∈ (Finset.univ : Finset U).powerset, a S * centeredMonomial p S z

Proof (Lean source)

lemma exists_centeredMonomial_expansion (p : U → ℝ) (F : (U → Bool) → ℝ) : ∃ a : Finset U → ℝ, ∀ z, F z = ∑ S ∈ (Finset.univ : Finset U).powerset, a S * centeredMonomial p S z := by classical set sgn : Bool → ℝ := fun b => if b then 1 else -1 with hsgn set base : U → Bool → ℝ := fun j b => if b then p j else 1 - p j with hbase refine ⟨fun S => ∑ w : U → Bool, F w * (∏ j ∈ S, sgn (w j)) * ∏ j ∈ (Finset.univ : Finset U) \ S, base j (w j), fun z => ?_⟩ have hdelta (w : U → Bool) : (if z = w then (1 : ℝ) else 0) = ∑ S ∈ (Finset.univ : Finset U).powerset, ((∏ j ∈ S, sgn (w j)) * ∏ j ∈ (Finset.univ : Finset U) \ S, base j (w j)) * centeredMonomial p S z := by rw [show (if z = w then (1 : ℝ) else 0) = ∏ j : U, if z j = w j then (1 : ℝ) else 0 by by_cases hzw : z = w · subst hzw; simp · rw [if_neg hzw] obtain ⟨j, hj⟩ : ∃ j, z j ≠ w j := by simpa [funext_iff] using hzw exact (Finset.prod_eq_zero (Finset.mem_univ j) (by simp [hj])).symm] rw [show (∏ j : U, if z j = w j then (1 : ℝ) else 0) = ∏ j : U, (sgn (w j) * (treatInd j z - p j) + base j (w j)) by refine Finset.prod_congr rfl fun j _ => ?_ cases hz : z j <;> cases hw : w j <;> simp [hz, hsgn, hbase, treatInd]] rw [Finset.prod_add] refine Finset.sum_congr rfl fun S _ => ?_ rw [show (∏ i ∈ S, sgn (w i) * (treatInd i z - p i)) = (∏ i ∈ S, sgn (w i)) * centeredMonomial p S z by rw [Finset.prod_mul_distrib]; rfl] ring calc F z = ∑ w : U → Bool, F w * (if z = w then (1 : ℝ) else 0) := by rw [Finset.sum_eq_single z] · simp · intro w _ hwz; simp [Ne.symm hwz] · simp _ = ∑ w : U → Bool, F w * ∑ S ∈ (Finset.univ : Finset U).powerset, ((∏ j ∈ S, sgn (w j)) * ∏ j ∈ (Finset.univ : Finset U) \ S, base j (w j)) * centeredMonomial p S z := Finset.sum_congr rfl fun w _ => by rw [hdelta w] _ = _ := by simp only [Finset.mul_sum] rw [Finset.sum_comm] refine Finset.sum_congr rfl fun S _ => ?_ rw [Finset.sum_mul] exact Finset.sum_congr rfl fun w _ => by ring

Causalean.Experimentation.DesignBased.exists_centeredMonomial_expansion · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:279
bernoulliDesign_E_sq_of_expansion theorem — Parseval's identity for the Bernoulli design. Once a statistic is written in the centered-monomial basis, its second moment is the sum over subsets of the squared coefficient times the product of the per-unit assignment variances on that subset — the basis is orthogonal, so no cross terms survive.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

F :

(U → Bool) → ℝ

a :

Finset U → ℝ

ha :

∀ z, F z = ∑ S ∈ (Finset.univ : Finset U).powerset, a S * centeredMonomial p S z

conclusion

(bernoulliDesign p hp0 hp1).E (fun z => F z ^ 2)
= ∑ S ∈ (Finset.univ : Finset U).powerset, a S ^ 2 * ∏ j ∈ S, p j * (1 - p j)

Proof (Lean source)

theorem bernoulliDesign_E_sq_of_expansion (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (F : (U → Bool) → ℝ) (a : Finset U → ℝ) (ha : ∀ z, F z = ∑ S ∈ (Finset.univ : Finset U).powerset, a S * centeredMonomial p S z) : (bernoulliDesign p hp0 hp1).E (fun z => F z ^ 2) = ∑ S ∈ (Finset.univ : Finset U).powerset, a S ^ 2 * ∏ j ∈ S, p j * (1 - p j) := by rw [show (fun z => F z ^ 2) = (fun z => (∑ S ∈ (Finset.univ : Finset U).powerset, a S * centeredMonomial p S z) * ∑ T ∈ (Finset.univ : Finset U).powerset, a T * centeredMonomial p T z) by funext z; rw [ha z]; ring] simp only [Finset.sum_mul, Finset.mul_sum, FiniteDesign.E_sum] have hterm (S T : Finset U) : (bernoulliDesign p hp0 hp1).E (fun z => (a S * centeredMonomial p S z) * (a T * centeredMonomial p T z)) = a S * a T * (if S = T then ∏ j ∈ S, p j * (1 - p j) else 0) := by rw [show (fun z => (a S * centeredMonomial p S z) * (a T * centeredMonomial p T z)) = (fun z => (a S * a T) * (centeredMonomial p S z * centeredMonomial p T z)) by funext z; ring] rw [FiniteDesign.E_const_mul, bernoulliDesign_E_centeredMonomial_mul p hp0 hp1 S T] simp_rw [hterm] refine Finset.sum_congr rfl fun S hS => ?_ rw [Finset.sum_eq_single S] · rw [if_pos rfl]; ring · intro T _ hTS; rw [if_neg hTS]; ring · exact fun hS' => (hS' hS).elim

Causalean.Experimentation.DesignBased.bernoulliDesign_E_sq_of_expansion · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:328
centeredMonomial_coef_empty_eq_zero theorem — A statistic with design mean zero has no constant term: the coefficient of the empty subset in any centered-monomial expansion of it vanishes.

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

F :

(U → Bool) → ℝ

a :

Finset U → ℝ

ha :

∀ z, F z = ∑ S ∈ (Finset.univ : Finset U).powerset, a S * centeredMonomial p S z

hmean :

(bernoulliDesign p hp0 hp1).E F = 0

conclusion

a ∅ = 0

Proof (Lean source)

theorem centeredMonomial_coef_empty_eq_zero (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (F : (U → Bool) → ℝ) (a : Finset U → ℝ) (ha : ∀ z, F z = ∑ S ∈ (Finset.univ : Finset U).powerset, a S * centeredMonomial p S z) (hmean : (bernoulliDesign p hp0 hp1).E F = 0) : a ∅ = 0 := by rw [show F = fun z => ∑ S ∈ (Finset.univ : Finset U).powerset, a S * centeredMonomial p S z from funext ha, FiniteDesign.E_sum] at hmean have hterm (S : Finset U) : (bernoulliDesign p hp0 hp1).E (fun z => a S * centeredMonomial p S z) = if S = ∅ then a S else 0 := by rw [FiniteDesign.E_const_mul, bernoulliDesign_E_centeredMonomial p hp0 hp1 S] by_cases hS : S = ∅ <;> simp [hS] simp_rw [hterm] at hmean simpa using hmean

Causalean.Experimentation.DesignBased.centeredMonomial_coef_empty_eq_zero · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:357
centeredMonomial_coef_eq_zero_of_not_subset theorem — Locality of the Fourier support. If a statistic depends only on the units of a block N, every centered-monomial coefficient attached to a subset that is not contained in N is zero, so its expansion is supported on the subsets of N. (Only treatment probabilities on S must be strictly between zero and one, so those selected coordinates are nondegenerate.)

hypotheses

U :

Type u_1
shared

p :

U → ℝ

hp0 :

∀ i, 0 ≤ p i

hp1 :

∀ i, p i ≤ 1

N :

Finset U

F :

(U → Bool) → ℝ

hF :

DependsOnBlock N F

a :

Finset U → ℝ

ha :

∀ z, F z = ∑ S ∈ (Finset.univ : Finset U).powerset, a S * centeredMonomial p S z

S :

Finset U

hSN :

¬ S ⊆ N

hp0S :

∀ i ∈ S, 0 < p i

hp1S :

∀ i ∈ S, p i < 1

conclusion

a S = 0

Proof (Lean source)

theorem centeredMonomial_coef_eq_zero_of_not_subset (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) (N : Finset U) (F : (U → Bool) → ℝ) (hF : DependsOnBlock N F) (a : Finset U → ℝ) (ha : ∀ z, F z = ∑ S ∈ (Finset.univ : Finset U).powerset, a S * centeredMonomial p S z) (S : Finset U) (hSN : ¬ S ⊆ N) (hp0S : ∀ i ∈ S, 0 < p i) (hp1S : ∀ i ∈ S, p i < 1) : a S = 0 := by classical have hS : S ∈ (Finset.univ : Finset U).powerset := Finset.mem_powerset.mpr (Finset.subset_univ S) obtain ⟨j, hjS, hjN⟩ : ∃ j, j ∈ S ∧ j ∉ N := by simpa only [Finset.not_subset] using hSN have hp0' : ∀ i, 0 ≤ p i := hp0 have hp1' : ∀ i, p i ≤ 1 := hp1 set Dcoin : U → FiniteDesign Bool := fun i => coinDesign (p i) (hp0' i) (hp1' i) with hDcoin set R : (U → Bool) → ℝ := fun z => F z * centeredMonomial p (S.erase j) z with hR have hzero : (bernoulliDesign p hp0' hp1').E (fun z => F z * centeredMonomial p S z) = 0 := by unfold bernoulliDesign rw [show (fun z => F z * centeredMonomial p S z) = (fun z => (treatInd j z - p j) * R z) by funext z rw [hR] simp only [centeredMonomial] rw [← Finset.mul_prod_erase S (fun k => treatInd k z - p k) hjS] ring] rw [FiniteDesign.E_prod_block_mul Dcoin {j} (fun z => treatInd j z - p j) R] · have hx : (prodDesign Dcoin).E (fun z => treatInd j z - p j) = 0 := by have hE := bernoulliDesign_E_centeredMonomial p hp0' hp1' ({j} : Finset U) rw [if_neg (Finset.singleton_ne_empty j), show centeredMonomial p ({j} : Finset U) = fun z => treatInd j z - p j from funext fun z => by simp [centeredMonomial]] at hE simpa [bernoulliDesign, hDcoin] using hE rw [hx, zero_mul] · intro z z' hzz simp only [treatInd, hzz j (mem_singleton_self j)] · intro z z' hzz rw [hR] refine congrArg₂ (· * ·) (hF z z' fun k hkN => hzz k ?_) ?_ · exact fun hkj => hjN (by rw [Finset.mem_singleton.mp hkj] at hkN; exact hkN) · simp only [centeredMonomial] refine Finset.prod_congr rfl fun k hk => ?_ simp only [treatInd, hzz k (by simpa using Finset.ne_of_mem_erase hk)] have hcoef : (bernoulliDesign p hp0' hp1').E (fun z => F z * centeredMonomial p S z) = a S * ∏ i ∈ S, p i * (1 - p i) := by rw [show (fun z => F z * centeredMonomial p S z) = (fun z => ∑ T ∈ (Finset.univ : Finset U).powerset, a T * (centeredMonomial p T z * centeredMonomial p S z)) by funext z rw [ha z, Finset.sum_mul] exact Finset.sum_congr rfl fun T _ => by ring] rw [FiniteDesign.E_sum] simp_rw [FiniteDesign.E_const_mul, bernoulliDesign_E_centeredMonomial_mul p hp0' hp1'] rw [Finset.sum_eq_single S] · simp · intro T _ hTS; simp [hTS] · exact fun h => (h hS).elim rw [hzero] at hcoef have hv : (∏ i ∈ S, p i * (1 - p i)) ≠ 0 := Finset.prod_ne_zero_iff.mpr fun i hi => (mul_pos (hp0S i hi) (sub_pos.mpr (hp1S i hi))).ne' exact (mul_eq_zero.mp hcoef.symm).resolve_right hv

Causalean.Experimentation.DesignBased.centeredMonomial_coef_eq_zero_of_not_subset · Causalean/Experimentation/DesignBased/Designs/BernoulliMoments.lean:382

ClusterRandomization 3 core · 2 supporting Cluster randomization treats all units in a cluster according to one cluster-level coin flip. ★ clusterDesign_E_unitTreatInd_pair_same

Cluster randomization designs

Cluster randomization treats all units in a cluster according to one cluster-level coin flip.

This file packages cluster-level Bernoulli assignment and proves the resulting unit-level inclusion probabilities for same-cluster and cross-cluster pairs.

def clusterDesign reviewed

Causalean.Experimentation.DesignBased

For a finite population of clusters, cluster-specific treatment probabilities that are each between zero and one, the cluster-randomization design independently assigns each cluster to treatment with its specified probability.

Definition (Lean source)

parameters

C :

Type u_2

shared

p :

C → ℝ

hp0 :

∀ c, 0 ≤ p c

hp1 :

∀ c, p c ≤ 1

def

clusterDesign p hp0 hp1 :

FiniteDesign (C → Bool)

given by

bernoulliDesign p hp0 hp1

Causalean.Experimentation.DesignBased.clusterDesign · Causalean/Experimentation/DesignBased/Designs/ClusterRandomization.lean:35 · uses FiniteDesign

def unitTreatInd reviewed

Causalean.Experimentation.DesignBased

For a finite population of units, a finite population of clusters, a map assigning every unit to a cluster, a unit, and a treatment assignment for the clusters, the unit-level treatment indicator equals one if that unit's cluster is treated and zero otherwise.

Definition (Lean source)

parameters

U :

Type u_1

shared

C :

Type u_2

shared

clus :

U → C

i :

U

z :

C → Bool

def

unitTreatInd clus i z :

ℝ

given by

treatInd (clus i) z

Causalean.Experimentation.DesignBased.unitTreatInd · Causalean/Experimentation/DesignBased/Designs/ClusterRandomization.lean:44

lemma clusterDesign_E_unitTreatInd_pair_same reviewed

Causalean.Experimentation.DesignBased

Same-cluster joint treatment. For a cluster-randomization design in which each cluster's treatment probability p c lies in [0,1], if two units i and j belong to the same cluster, then they are jointly treated with probability exactly their shared cluster's rate p (clus i) — because being in the same cluster makes their treatment indicators identical.

Formal statement

hypotheses

U :

Type u_1

shared

C :

Type u_2

shared

p :

C → ℝ

hp0 :

∀ c, 0 ≤ p c

hp1 :

∀ c, p c ≤ 1

clus :

U → C

i j :

U

h :

clus i = clus j

conclusion

(clusterDesign p hp0 hp1).E (fun z => unitTreatInd clus i z * unitTreatInd clus j z)

= p (clus i)

Proof (Lean source)

lemma clusterDesign_E_unitTreatInd_pair_same (p : C → ℝ) (hp0 : ∀ c, 0 ≤ p c) (hp1 : ∀ c, p c ≤ 1) (clus : U → C) {i j : U} (h : clus i = clus j) : (clusterDesign p hp0 hp1).E (fun z => unitTreatInd clus i z * unitTreatInd clus j z) = p (clus i) := by simp only [clusterDesign, unitTreatInd] rw [← h] rw [show (fun z => treatInd (clus i) z * treatInd (clus i) z) = (fun z => treatInd (clus i) z) by funext z by_cases hz : z (clus i) <;> simp [treatInd, hz]] simpa [treatInd] using (bernoulliDesign_E_treatInd p hp0 hp1 (clus i) (fun b => if b then (1 : ℝ) else 0))

Causalean.Experimentation.DesignBased.clusterDesign_E_unitTreatInd_pair_same · Causalean/Experimentation/DesignBased/Designs/ClusterRandomization.lean:60 · uses E , clusterDesign , unitTreatInd

2 supporting declarations (lemmas, instances)

clusterDesign_E_unitTreatInd lemma — First-order inclusion probability. A unit i is treated with probability p (clus i), the treatment rate of its own cluster.

hypotheses

U :

Type u_1
shared

C :

Type u_2
shared

p :

C → ℝ

hp0 :

∀ c, 0 ≤ p c

hp1 :

∀ c, p c ≤ 1

clus :

U → C

i :

U

conclusion

(clusterDesign p hp0 hp1).E (unitTreatInd clus i) = p (clus i)

Proof (Lean source)

lemma clusterDesign_E_unitTreatInd (p : C → ℝ) (hp0 : ∀ c, 0 ≤ p c) (hp1 : ∀ c, p c ≤ 1) (clus : U → C) (i : U) : (clusterDesign p hp0 hp1).E (unitTreatInd clus i) = p (clus i) := by simp only [clusterDesign] have h := bernoulliDesign_E_treatInd p hp0 hp1 (clus i) (fun b => if b then (1 : ℝ) else 0) simp only [if_true, mul_one, Bool.false_eq_true, if_false, mul_zero, add_zero] at h exact h

Causalean.Experimentation.DesignBased.clusterDesign_E_unitTreatInd · Causalean/Experimentation/DesignBased/Designs/ClusterRandomization.lean:50
clusterDesign_E_unitTreatInd_pair_diff lemma — Different-cluster joint treatment. Two units in distinct clusters are jointly treated with the product of their cluster rates — distinct clusters are randomized independently.

hypotheses

U :

Type u_1
shared

C :

Type u_2
shared

p :

C → ℝ

hp0 :

∀ c, 0 ≤ p c

hp1 :

∀ c, p c ≤ 1

clus :

U → C

i j :

U

h :

clus i ≠ clus j

conclusion

(clusterDesign p hp0 hp1).E (fun z => unitTreatInd clus i z * unitTreatInd clus j z)
= p (clus i) * p (clus j)

Proof (Lean source)

lemma clusterDesign_E_unitTreatInd_pair_diff (p : C → ℝ) (hp0 : ∀ c, 0 ≤ p c) (hp1 : ∀ c, p c ≤ 1) (clus : U → C) {i j : U} (h : clus i ≠ clus j) : (clusterDesign p hp0 hp1).E (fun z => unitTreatInd clus i z * unitTreatInd clus j z) = p (clus i) * p (clus j) := by simp only [clusterDesign, unitTreatInd] exact bernoulliDesign_E_treatInd_pair p hp0 hp1 h

Causalean.Experimentation.DesignBased.clusterDesign_E_unitTreatInd_pair_diff · Causalean/Experimentation/DesignBased/Designs/ClusterRandomization.lean:78

CompleteRandomization 2 core · 6 supporting This file defines the fixed-treated-count randomization design completeRandomization, the uniform law on treated subsets of size n₁. ★ completeRandomization★ completeRandomization_incl_pair

Complete randomization designs

This file defines the fixed-treated-count randomization design completeRandomization, the uniform law on treated subsets of size n₁. It also proves the design-space count completeRandomization_card, the first-order inclusion probability completeRandomization_incl, and the second-order inclusion probability completeRandomization_incl_pair for two distinct units. These are the finite-population facts used by Horvitz-Thompson and difference-in-means bias and variance calculations under complete randomization.

def completeRandomization reviewed

Causalean.Experimentation.DesignBased

For a finite population of units, a nonnegative number of treated units that does not exceed the population size, the complete-randomization design assigns equal probability to every treatment allocation that treats exactly that many units.

Definition (Lean source)

parameters

V :

Type*

Fintype V

n₁ :

ℕ

hn :

n₁ ≤ card V

def

completeRandomization n₁ hn :

FiniteDesign {S : Finset V // S.card = n₁}

given by

by classical exact { p := fun _ => 1 / (card {S : Finset V // S.card = n₁} : ℝ) p_nonneg := fun _ => one_div_nonneg.mpr (Nat.cast_nonneg _) p_sum := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] have hcard_nat : card {S : Finset V // S.card = n₁} ≠ 0 := by rw [completeRandomization_card] exact Nat.choose_ne_zero hn have hcard_real : (card {S : Finset V // S.card = n₁} : ℝ) ≠ 0 := by exact_mod_cast hcard_nat field_simp [hcard_real] }

Causalean.Experimentation.DesignBased.completeRandomization · Causalean/Experimentation/DesignBased/Designs/CompleteRandomization.lean:54 · uses FiniteDesign

lemma completeRandomization_incl_pair reviewed

Causalean.Experimentation.DesignBased

Second-order inclusion probability. Under complete randomization treating exactly n₁ of the N units, where the treated count n₁ does not exceed the population size N, two distinct units are jointly treated with probability n₁(n₁−1) / (N(N−1)).

Formal statement

hypotheses

U :

Type u_1

shared

n₁ :

ℕ

hn :

n₁ ≤ Fintype.card U

i j :

U

h :

i ≠ j

conclusion

(completeRandomization n₁ hn).Pr (fun S => i ∈ S.val ∧ j ∈ S.val)

= ((n₁ : ℝ) * ((n₁ : ℝ) - 1)) / ((Fintype.card U : ℝ) * ((Fintype.card U : ℝ) - 1))

Proof (Lean source)

lemma completeRandomization_incl_pair (n₁ : ℕ) (hn : n₁ ≤ Fintype.card U) {i j : U} (h : i ≠ j) : (completeRandomization n₁ hn).Pr (fun S => i ∈ S.val ∧ j ∈ S.val) = ((n₁ : ℝ) * ((n₁ : ℝ) - 1)) / ((Fintype.card U : ℝ) * ((Fintype.card U : ℝ) - 1)) := by -- Pr = C(N−2,n₁−2)/C(N,n₁); size-n₁ subsets containing both i,j ↔ size-(n₁−2) subsets of U∖{i,j}. cases n₁ with | zero => unfold FiniteDesign.Pr FiniteDesign.E FiniteDesign.ind completeRandomization simp | succ m => cases m with | zero => unfold FiniteDesign.Pr FiniteDesign.E FiniteDesign.ind completeRandomization have hfalse : ∀ S : {S : Finset U // S.card = 1}, ¬(i ∈ S.val ∧ j ∈ S.val) := by intro S hmem have hpair_sub : ({i, j} : Finset U) ⊆ S.val := by intro x hx simp only [Finset.mem_insert, mem_singleton] at hx rcases hx with rfl | rfl · exact hmem.1 · exact hmem.2 have hpair_card : ({i, j} : Finset U).card = 2 := by simp [h] have hle : 2 ≤ S.val.card := by rw [← hpair_card] exact Finset.card_le_card hpair_sub omega simp [hfalse] | succ k => unfold FiniteDesign.Pr FiniteDesign.E FiniteDesign.ind completeRandomization rw [← Finset.mul_sum] have hsum : (∑ S : {S : Finset U // S.card = k + 2}, if i ∈ S.val ∧ j ∈ S.val then (1 : ℝ) else 0) = (Fintype.card {S : {S : Finset U // S.card = k + 2} // i ∈ S.val ∧ j ∈ S.val} : ℝ) := by rw [Fintype.card_subtype] exact Finset.sum_boole (R := ℝ) (fun S : {S : Finset U // S.card = k + 2} => i ∈ S.val ∧ j ∈ S.val) Finset.univ rw [hsum, card_design_mem_pair i j h k] rw [completeRandomization_card] have hpair_sub : ({i, j} : Finset U) ⊆ (Finset.univ : Finset U) := by intro x _hx exact Finset.mem_univ x have hpair_card : ({i, j} : Finset U).card = 2 := by simp [h] have hN2 : 2 ≤ Fintype.card U := by rw [← Finset.card_univ, ← hpair_card] exact Finset.card_le_card hpair_sub have hNpos : 0 < Fintype.card U := by omega have h1 : (Fintype.card U - 1) * (Fintype.card U - 2).choose k = (Fintype.card U - 1).choose (k + 1) * (k + 1) := by have hchoose := Nat.add_one_mul_choose_eq (Fintype.card U - 2) k have hsub : Fintype.card U - 2 + 1 = Fintype.card U - 1 := by omega rwa [hsub] at hchoose have h2 : Fintype.card U * (Fintype.card U - 1).choose (k + 1) = (Fintype.card U).choose (k + 2) * (k + 2) := by have hchoose := Nat.add_one_mul_choose_eq (Fintype.card U - 1) (k + 1) rwa [Nat.sub_add_cancel (Nat.succ_le_of_lt hNpos)] at hchoose have hchoose_nat : Fintype.card U * (Fintype.card U - 1) * (Fintype.card U - 2).choose k = (Fintype.card U).choose (k + 2) * ((k + 2) * (k + 1)) := by calc Fintype.card U * (Fintype.card U - 1) * (Fintype.card U - 2).choose k = Fintype.card U * ((Fintype.card U - 1) * (Fintype.card U - 2).choose k) := by ring _ = Fintype.card U * ((Fintype.card U - 1).choose (k + 1) * (k + 1)) := by rw [h1] _ = (Fintype.card U * (Fintype.card U - 1).choose (k + 1)) * (k + 1) := by ring _ = ((Fintype.card U).choose (k + 2) * (k + 2)) * (k + 1) := by rw [h2] _ = (Fintype.card U).choose (k + 2) * ((k + 2) * (k + 1)) := by ring have hchoose_real0 : (Fintype.card U : ℝ) * ((Fintype.card U - 1 : ℕ) : ℝ) * ((Fintype.card U - 2).choose k : ℝ) = ((Fintype.card U).choose (k + 2) : ℝ) * (((k + 2 : ℕ) : ℝ) * ((k + 1 : ℕ) : ℝ)) := by exact_mod_cast hchoose_nat have hchoose_real : (Fintype.card U : ℝ) * ((Fintype.card U : ℝ) - 1) * ((Fintype.card U - 2).choose k : ℝ) = ((Fintype.card U).choose (k + 2) : ℝ) * (((k : ℝ) + 2) * ((k : ℝ) + 1)) := by simpa [Nat.cast_sub (by omega : 1 ≤ Fintype.card U)] using hchoose_real0 have hden_real : (((Fintype.card U).choose (k + 2) : ℝ) ≠ 0) := by exact_mod_cast Nat.choose_ne_zero hn have hN_real : (Fintype.card U : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hNpos) have hNm1_real : (Fintype.card U : ℝ) - 1 ≠ 0 := by have hNgt1 : (1 : ℝ) < Fintype.card U := by exact_mod_cast (by omega : 1 < Fintype.card U) exact ne_of_gt (sub_pos.mpr hNgt1) field_simp [hden_real, hN_real, hNm1_real] ring_nf at hchoose_real ⊢ rw [hchoose_real] norm_num [Nat.cast_add, Nat.cast_ofNat] ring

Causalean.Experimentation.DesignBased.completeRandomization_incl_pair · Causalean/Experimentation/DesignBased/Designs/CompleteRandomization.lean:284 · uses Pr , completeRandomization

6 supporting declarations (lemmas, instances)

completeRandomization_card lemma — The number of possible treated sets in complete randomization is the binomial coefficient (Fintype.card U).choose n₁.

hypotheses

V :

Type*
Fintype V

n₁ :

ℕ

conclusion

card {S : Finset V // S.card = n₁} = (card V).choose n₁

Proof (Lean source)

lemma completeRandomization_card {V : Type*} [Fintype V] (n₁ : ℕ) : card {S : Finset V // S.card = n₁} = (card V).choose n₁ := by classical rw [Fintype.card_subtype] rw [← Finset.card_univ] rw [← Finset.card_powersetCard n₁ (Finset.univ : Finset V)] congr ext S simp [Finset.mem_powersetCard]

Causalean.Experimentation.DesignBased.completeRandomization_card · Causalean/Experimentation/DesignBased/Designs/CompleteRandomization.lean:42
card_powersetCard_filter_mem_succ lemma — Among subsets containing a specified unit and of size k + 1, there are exactly as many as there are size-k subsets after that unit is removed.

hypotheses

α :

Type*
DecidableEq α

s :

Finset α

i :

α

hi :

i ∈ s

k :

ℕ

conclusion

((s.powersetCard (k + 1)).filter (fun t => i ∈ t)).card
= ((s.erase i).powersetCard k).card

Proof (Lean source)

lemma card_powersetCard_filter_mem_succ {α : Type*} [DecidableEq α] (s : Finset α) (i : α) (hi : i ∈ s) (k : ℕ) : ((s.powersetCard (k + 1)).filter (fun t => i ∈ t)).card = ((s.erase i).powersetCard k).card := by have hps0 := Finset.powersetCard_succ_insert (notMem_erase i s) k have hps : s.powersetCard (k + 1) = (s.erase i).powersetCard (k + 1) ∪ ((s.erase i).powersetCard k).image (insert i) := by simpa [Nat.succ_eq_add_one, show insert i (s.erase i) = s by exact Finset.insert_erase hi] using hps0 rw [hps, Finset.filter_union] have hleft : (((s.erase i).powersetCard (k + 1)).filter (fun S => i ∈ S)) = ∅ := by apply Finset.filter_false_of_mem intro S hSpow hi exact (Finset.notMem_erase i s) ((Finset.mem_powersetCard.mp hSpow).1 hi) have hright : ((((s.erase i).powersetCard k).image (insert i)).filter (fun S => i ∈ S)) = ((s.erase i).powersetCard k).image (insert i) := by ext S simp only [mem_filter] constructor · exact fun h => h.1 · intro hS refine ⟨hS, ?_⟩ rcases Finset.mem_image.mp hS with ⟨T, _hT, rfl⟩ exact mem_insert_self _ _ rw [hleft, hright, Finset.empty_union] exact Finset.card_image_of_injOn (by intro A hA B hB hEq exact insert_erase_invOn.2.injOn (by intro hi exact (Finset.notMem_erase i s) ((Finset.mem_powersetCard.mp hA).1 hi)) (by intro hi exact (Finset.notMem_erase i s) ((Finset.mem_powersetCard.mp hB).1 hi)) hEq)

Causalean.Experimentation.DesignBased.card_powersetCard_filter_mem_succ · Causalean/Experimentation/DesignBased/Designs/CompleteRandomization.lean:74
card_design_mem_succ lemma — The number of subsets of a finite population with k + 1 units that contain one specified unit equals the number of ways to choose k units from the remaining population.

hypotheses

U :

Type u_1
shared

i :

U

k :

ℕ

conclusion

card {S : {S : Finset U // S.card = k + 1} // i ∈ S.val}
= (card U - 1).choose k

Proof (Lean source)

lemma card_design_mem_succ (i : U) (k : ℕ) : card {S : {S : Finset U // S.card = k + 1} // i ∈ S.val} = (card U - 1).choose k := by let e : {S : {S : Finset U // S.card = k + 1} // i ∈ S.val} ≃ {S : Finset U // S.card = k + 1 ∧ i ∈ S} := { toFun := fun S => ⟨S.val.val, S.val.property, S.property⟩ invFun := fun S => ⟨⟨S.val, S.property.1⟩, S.property.2⟩ left_inv := by intro S; cases S; rfl right_inv := by intro S; cases S; rfl } rw [Fintype.card_congr e] rw [Fintype.card_subtype] have hfilter : ((Finset.univ : Finset (Finset U)).filter (fun S => S.card = k + 1 ∧ i ∈ S)) = (((Finset.univ : Finset U).powersetCard (k + 1)).filter (fun S => i ∈ S)) := by ext S simp [Finset.mem_powersetCard, and_comm] rw [hfilter, card_powersetCard_filter_mem_succ (Finset.univ : Finset U) i (Finset.mem_univ i)] rw [Finset.card_powersetCard, Finset.card_erase_of_mem (Finset.mem_univ i), Finset.card_univ]

Causalean.Experimentation.DesignBased.card_design_mem_succ · Causalean/Experimentation/DesignBased/Designs/CompleteRandomization.lean:116
card_powersetCard_filter_mem_pair lemma — Among the fixed-size subsets of a finite set that contain two distinct specified elements, the count equals the number of subsets of the remaining set after those two elements are removed. This is the finite-population counting identity behind pairwise inclusion probabilities.

hypotheses

α :

Type*
DecidableEq α

s :

Finset α

i j :

α

hi :

i ∈ s

hj :

j ∈ s

hij :

i ≠ j

k :

ℕ

conclusion

((s.powersetCard (k + 2)).filter (fun t => i ∈ t ∧ j ∈ t)).card
= (((s.erase i).erase j).powersetCard k).card

Proof (Lean source)

lemma card_powersetCard_filter_mem_pair {α : Type*} [DecidableEq α] (s : Finset α) (i j : α) (hi : i ∈ s) (hj : j ∈ s) (hij : i ≠ j) (k : ℕ) : ((s.powersetCard (k + 2)).filter (fun t => i ∈ t ∧ j ∈ t)).card = (((s.erase i).erase j).powersetCard k).card := by refine Finset.card_bij' (fun t _ => (t.erase i).erase j) (fun t _ => insert i (insert j t)) ?_ ?_ ?_ ?_ · intro t ht rcases Finset.mem_filter.mp ht with ⟨htpow, hti, htj⟩ rw [Finset.mem_powersetCard] constructor · intro x hx rcases Finset.mem_erase.mp hx with ⟨hxj, hx⟩ rcases Finset.mem_erase.mp hx with ⟨hxi, hxt⟩ exact Finset.mem_erase.mpr ⟨hxj, Finset.mem_erase.mpr ⟨hxi, (Finset.mem_powersetCard.mp htpow).1 hxt⟩⟩ · have htcard : t.card = k + 2 := (Finset.mem_powersetCard.mp htpow).2 have hterase_i : (t.erase i).card = k + 1 := by rw [Finset.card_erase_of_mem hti, htcard] omega have htj_erase_i : j ∈ t.erase i := by simp [htj, hij.symm] rw [Finset.card_erase_of_mem htj_erase_i, hterase_i] omega · intro t ht rcases Finset.mem_powersetCard.mp ht with ⟨htsub, htcard⟩ rw [mem_filter] constructor · rw [Finset.mem_powersetCard] constructor · intro x hx rcases Finset.mem_insert.mp hx with rfl | hx · exact hi rcases Finset.mem_insert.mp hx with rfl | hx · exact hj exact (Finset.mem_erase.mp (Finset.mem_erase.mp (htsub hx)).2).2 · have hti : i ∉ t := by intro hti have := htsub hti simp at this have htj : j ∉ t := by intro htj have := htsub htj simp at this have hti_insert_j : i ∉ insert j t := by simp [hti, hij] rw [Finset.card_insert_of_notMem hti_insert_j, Finset.card_insert_of_notMem htj, htcard] · simp · intro t ht rcases Finset.mem_filter.mp ht with ⟨_htpow, hti, htj⟩ ext x by_cases hxi : x = i · subst x simp [hti] · by_cases hxj : x = j · subst x simp [htj] · simp [hxi, hxj] · intro t ht have hti : i ∉ t := by intro hti have := (Finset.mem_powersetCard.mp ht).1 hti simp at this have htj : j ∉ t := by intro htj have := (Finset.mem_powersetCard.mp ht).1 htj simp at this ext x by_cases hxi : x = i · subst x simp [hti] · by_cases hxj : x = j · subst x simp [htj] · simp [hxi, hxj]

Causalean.Experimentation.DesignBased.card_powersetCard_filter_mem_pair · Causalean/Experimentation/DesignBased/Designs/CompleteRandomization.lean:138
card_design_mem_pair lemma — The number of subsets of a finite population with k + 2 units that contain two distinct specified units equals the number of ways to choose k units from the remaining population.

hypotheses

U :

Type u_1
shared

i j :

U

hij :

i ≠ j

k :

ℕ

conclusion

card {S : {S : Finset U // S.card = k + 2} // i ∈ S.val ∧ j ∈ S.val}
= (card U - 2).choose k

Proof (Lean source)

lemma card_design_mem_pair (i j : U) (hij : i ≠ j) (k : ℕ) : card {S : {S : Finset U // S.card = k + 2} // i ∈ S.val ∧ j ∈ S.val} = (card U - 2).choose k := by let e : {S : {S : Finset U // S.card = k + 2} // i ∈ S.val ∧ j ∈ S.val} ≃ {S : Finset U // S.card = k + 2 ∧ i ∈ S ∧ j ∈ S} := { toFun := fun S => ⟨S.val.val, S.val.property, S.property⟩ invFun := fun S => ⟨⟨S.val, S.property.1⟩, S.property.2⟩ left_inv := by intro S; cases S; rfl right_inv := by intro S; cases S; rfl } rw [Fintype.card_congr e] rw [Fintype.card_subtype] have hfilter : ((Finset.univ : Finset (Finset U)).filter (fun S => S.card = k + 2 ∧ i ∈ S ∧ j ∈ S)) = (((Finset.univ : Finset U).powersetCard (k + 2)).filter (fun S => i ∈ S ∧ j ∈ S)) := by ext S simp [Finset.mem_powersetCard] rw [hfilter, card_powersetCard_filter_mem_pair (Finset.univ : Finset U) i j (Finset.mem_univ i) (Finset.mem_univ j) hij k] rw [Finset.card_powersetCard] have hcard : ((Finset.univ.erase i).erase j).card = card U - 2 := by rw [Finset.card_erase_of_mem (by simp [hij.symm] : j ∈ (Finset.univ : Finset U).erase i), Finset.card_erase_of_mem (Finset.mem_univ i), Finset.card_univ] omega rw [hcard]

Causalean.Experimentation.DesignBased.card_design_mem_pair · Causalean/Experimentation/DesignBased/Designs/CompleteRandomization.lean:215
completeRandomization_incl lemma — First-order inclusion probability. Under complete randomization, a unit is treated with probability n₁ / N.

hypotheses

U :

Type u_1
shared

n₁ :

ℕ

hn :

n₁ ≤ Fintype.card U

i :

U

conclusion

(completeRandomization n₁ hn).Pr (fun S => i ∈ S.val) = (n₁ : ℝ) / (Fintype.card U : ℝ)

Proof (Lean source)

lemma completeRandomization_incl (n₁ : ℕ) (hn : n₁ ≤ Fintype.card U) (i : U) : (completeRandomization n₁ hn).Pr (fun S => i ∈ S.val) = (n₁ : ℝ) / (Fintype.card U : ℝ) := by -- Pr = (#{size-n₁ sets containing i}) / C(N,n₁) = C(N−1,n₁−1)/C(N,n₁) = n₁/N. -- Key counting: size-n₁ subsets containing i ↔ size-(n₁−1) subsets of U∖{i}; and the choose -- identity n₁ · C(N,n₁) = N · C(N−1,n₁−1) (`Nat.succ_mul_choose_eq` family). cases n₁ with | zero => unfold FiniteDesign.Pr FiniteDesign.E FiniteDesign.ind completeRandomization simp | succ k => unfold FiniteDesign.Pr FiniteDesign.E FiniteDesign.ind completeRandomization rw [← Finset.mul_sum] have hsum : (∑ S : {S : Finset U // S.card = k + 1}, if i ∈ S.val then (1 : ℝ) else 0) = (Fintype.card {S : {S : Finset U // S.card = k + 1} // i ∈ S.val} : ℝ) := by rw [Fintype.card_subtype] exact Finset.sum_boole (R := ℝ) (fun S : {S : Finset U // S.card = k + 1} => i ∈ S.val) univ rw [hsum, card_design_mem_succ] rw [completeRandomization_card] have hNpos : 0 < Fintype.card U := Fintype.card_pos_iff.mpr ⟨i⟩ have hchoose_nat : Fintype.card U * (Fintype.card U - 1).choose k = (Fintype.card U).choose (k + 1) * (k + 1) := by have h := Nat.add_one_mul_choose_eq (Fintype.card U - 1) k rwa [Nat.sub_add_cancel (Nat.succ_le_of_lt hNpos)] at h have hchoose_real : (Fintype.card U : ℝ) * ((Fintype.card U - 1).choose k : ℝ) = ((Fintype.card U).choose (k + 1) : ℝ) * ((k : ℝ) + 1) := by exact_mod_cast hchoose_nat have hden_real : ((Fintype.card U).choose (k + 1) : ℝ) ≠ 0 := by exact_mod_cast Nat.choose_ne_zero hn have hN_real : (Fintype.card U : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hNpos) field_simp [hden_real, hN_real] rw [mul_comm] simpa using hchoose_real

Causalean.Experimentation.DesignBased.completeRandomization_incl · Causalean/Experimentation/DesignBased/Designs/CompleteRandomization.lean:244

Stratified 2 core · 2 supporting This file builds stratifiedDesign, the product of stratum-level complete-randomization designs. ★ stratifiedDesign_incl_pair_across

Stratified randomization designs

This file builds stratifiedDesign, the product of stratum-level complete-randomization designs. It proves the first-order inclusion probability stratifiedDesign_incl, the within-stratum second-order inclusion probability stratifiedDesign_incl_pair_within, and the across-strata factorization stratifiedDesign_incl_pair_across. These lemmas expose the design facts needed by estimators whose bias or variance depends on stratified treatment inclusion probabilities.

def stratifiedDesign reviewed

Causalean.Experimentation.DesignBased

For a finite collection of strata, each with a finite population of units, and a specified number of treated units in every stratum that does not exceed that stratum's population size, the stratified randomization design independently selects exactly the specified number of units in each stratum.

Definition (Lean source)

parameters

K :

Type u_1

K → Type u_2

shared

n₁ :

K → ℕ

hn :

∀ k, n₁ k ≤ card (V k)

def

stratifiedDesign n₁ hn :

FiniteDesign (∀ k, {S : Finset (V k) // S.card = n₁ k})

given by

prodDesign (fun k => completeRandomization (n₁ k) (hn k))

Causalean.Experimentation.DesignBased.stratifiedDesign · Causalean/Experimentation/DesignBased/Designs/Stratified.lean:39 · uses FiniteDesign

lemma stratifiedDesign_incl_pair_across reviewed

Causalean.Experimentation.DesignBased

Second-order inclusion probability across strata. For a stratified design in which each stratum k treats exactly n₁ k of its N k units, with n₁ k never exceeding N k, if k and k' are distinct strata, then a unit i in stratum k and a unit i' in stratum k' are jointly treated with probability the product of their two strata's treatment rates, (n₁ k / N k) · (n₁ k' / N k') — the strata are randomized independently.

Formal statement

hypotheses

K :

Type u_1

K → Type u_2

shared

n₁ :

K → ℕ

hn :

∀ k, n₁ k ≤ card (V k)

k k' :

K

hk :

k ≠ k'

i :

V k

i' :

V k'

conclusion

(stratifiedDesign n₁ hn).Pr (fun z => i ∈ (z k).val ∧ i' ∈ (z k').val)

= ((n₁ k : ℝ) / (card (V k) : ℝ)) * ((n₁ k' : ℝ) / (card (V k') : ℝ))

Proof (Lean source)

lemma stratifiedDesign_incl_pair_across (n₁ : K → ℕ) (hn : ∀ k, n₁ k ≤ card (V k)) {k k' : K} (hk : k ≠ k') (i : V k) (i' : V k') : (stratifiedDesign n₁ hn).Pr (fun z => i ∈ (z k).val ∧ i' ∈ (z k').val) = ((n₁ k : ℝ) / (card (V k) : ℝ)) * ((n₁ k' : ℝ) / (card (V k') : ℝ)) := by unfold FiniteDesign.Pr FiniteDesign.ind simp only [stratifiedDesign] have hpoint : (fun z : ∀ k, {S : Finset (V k) // S.card = n₁ k} => if i ∈ (z k).val ∧ i' ∈ (z k').val then (1 : ℝ) else 0) = (fun z => (fun S => if i ∈ S.val then (1 : ℝ) else 0) (z k) * (fun S => if i' ∈ S.val then (1 : ℝ) else 0) (z k')) := by funext z by_cases hi : i ∈ (z k).val · by_cases hi' : i' ∈ (z k').val · simp [hi, hi'] · simp [hi, hi'] · simp [hi] rw [hpoint] rw [FiniteDesign.E_prod_apply₂ (fun k => completeRandomization (n₁ k) (hn k)) hk (fun S => if i ∈ S.val then (1 : ℝ) else 0) (fun S => if i' ∈ S.val then (1 : ℝ) else 0)] rw [show (completeRandomization (n₁ k) (hn k)).E (fun S => if i ∈ S.val then (1 : ℝ) else 0) = (n₁ k : ℝ) / (card (V k) : ℝ) from by change (completeRandomization (n₁ k) (hn k)).Pr (fun S => i ∈ S.val) = (n₁ k : ℝ) / (card (V k) : ℝ) exact completeRandomization_incl (n₁ k) (hn k) i] rw [show (completeRandomization (n₁ k') (hn k')).E (fun S => if i' ∈ S.val then (1 : ℝ) else 0) = (n₁ k' : ℝ) / (card (V k') : ℝ) from by change (completeRandomization (n₁ k') (hn k')).Pr (fun S => i' ∈ S.val) = (n₁ k' : ℝ) / (card (V k') : ℝ) exact completeRandomization_incl (n₁ k') (hn k') i']

Causalean.Experimentation.DesignBased.stratifiedDesign_incl_pair_across · Causalean/Experimentation/DesignBased/Designs/Stratified.lean:89 · uses Pr , stratifiedDesign

2 supporting declarations (lemmas, instances)

stratifiedDesign_incl lemma — First-order inclusion probability. A unit i in stratum k is treated with probability n₁ k / N k, the complete-randomization rate of its own stratum.

hypotheses

K :

Type u_1
K → Type u_2
shared

n₁ :

K → ℕ

hn :

∀ k, n₁ k ≤ card (V k)

k :

K

i :

V k

conclusion

(stratifiedDesign n₁ hn).Pr (fun z => i ∈ (z k).val)
= (n₁ k : ℝ) / (card (V k) : ℝ)

Proof (Lean source)

lemma stratifiedDesign_incl (n₁ : K → ℕ) (hn : ∀ k, n₁ k ≤ card (V k)) (k : K) (i : V k) : (stratifiedDesign n₁ hn).Pr (fun z => i ∈ (z k).val) = (n₁ k : ℝ) / (card (V k) : ℝ) := by unfold FiniteDesign.Pr FiniteDesign.ind simp only [stratifiedDesign] change (prodDesign (fun k => completeRandomization (n₁ k) (hn k))).E (fun z => (fun S => if i ∈ S.val then (1 : ℝ) else 0) (z k)) = (n₁ k : ℝ) / (card (V k) : ℝ) rw [FiniteDesign.E_prod_apply (fun k => completeRandomization (n₁ k) (hn k)) k (fun S => if i ∈ S.val then (1 : ℝ) else 0)] change (completeRandomization (n₁ k) (hn k)).Pr (fun S => i ∈ S.val) = (n₁ k : ℝ) / (card (V k) : ℝ) exact completeRandomization_incl (n₁ k) (hn k) i

Causalean.Experimentation.DesignBased.stratifiedDesign_incl · Causalean/Experimentation/DesignBased/Designs/Stratified.lean:49
stratifiedDesign_incl_pair_within lemma — Second-order inclusion probability within one stratum. Two distinct units in the same stratum k are jointly treated with the complete-randomization second-order inclusion probability for that stratum.

hypotheses

K :

Type u_1
K → Type u_2
shared

n₁ :

K → ℕ

hn :

∀ k, n₁ k ≤ card (V k)

k :

K
V k

hij :

i ≠ j

conclusion

(stratifiedDesign n₁ hn).Pr (fun z => i ∈ (z k).val ∧ j ∈ (z k).val)
= ((n₁ k : ℝ) * ((n₁ k : ℝ) - 1)) / ((card (V k) : ℝ) * ((card (V k) : ℝ) - 1))

Proof (Lean source)

lemma stratifiedDesign_incl_pair_within (n₁ : K → ℕ) (hn : ∀ k, n₁ k ≤ card (V k)) (k : K) {i j : V k} (hij : i ≠ j) : (stratifiedDesign n₁ hn).Pr (fun z => i ∈ (z k).val ∧ j ∈ (z k).val) = ((n₁ k : ℝ) * ((n₁ k : ℝ) - 1)) / ((card (V k) : ℝ) * ((card (V k) : ℝ) - 1)) := by unfold FiniteDesign.Pr FiniteDesign.ind simp only [stratifiedDesign] change (prodDesign (fun k => completeRandomization (n₁ k) (hn k))).E (fun z => (fun S => if i ∈ S.val ∧ j ∈ S.val then (1 : ℝ) else 0) (z k)) = ((n₁ k : ℝ) * ((n₁ k : ℝ) - 1)) / ((card (V k) : ℝ) * ((card (V k) : ℝ) - 1)) rw [FiniteDesign.E_prod_apply (fun k => completeRandomization (n₁ k) (hn k)) k (fun S => if i ∈ S.val ∧ j ∈ S.val then (1 : ℝ) else 0)] change (completeRandomization (n₁ k) (hn k)).Pr (fun S => i ∈ S.val ∧ j ∈ S.val) = ((n₁ k : ℝ) * ((n₁ k : ℝ) - 1)) / ((card (V k) : ℝ) * ((card (V k) : ℝ) - 1)) exact completeRandomization_incl_pair (n₁ k) (hn k) hij

Causalean.Experimentation.DesignBased.stratifiedDesign_incl_pair_within · Causalean/Experimentation/DesignBased/Designs/Stratified.lean:67

Experimentation.Design­Based.Designs

Single-coin randomization design

Bernoulli randomization designs

Product moments and centered monomials of the Bernoulli design

Cluster randomization designs

Complete randomization designs

Stratified randomization designs