Experimentation.DesignBased.Designs
Canonical, paper-agnostic randomization designs with their inclusion probabilities computed once, ready to plug into the design-based estimation and optimality layers.
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
⚑ flagged
Causalean.Experimentation.DesignBased
The single-unit coin design on Bool: treatment (true) with probability p, control (false) with probability 1 − p.
Definition (Lean source)
def coinDesign (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : FiniteDesign Bool where
p := fun b => cond b p (1 - p)
p_nonneg := by
intro b
cases b
· exact sub_nonneg.mpr hp1
· exact hp0
p_sum := by
rw [Fintype.sum_bool]
change p + (1 - p) = 1
ring
lemma coinDesign_E reviewed
⚑ flagged
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
conclusion
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]
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
⚑ flagged
Causalean.Experimentation.DesignBased
The Bernoulli randomization design: each unit i is independently assigned treatment with probability p i. Built as the product of the per-unit coin designs.
Definition (Lean source)
noncomputable def bernoulliDesign (p : U → ℝ) (hp0 : ∀ i, 0 ≤ p i) (hp1 : ∀ i, p i ≤ 1) :
FiniteDesign (U → Bool) :=
prodDesign (fun i => coinDesign (p i) (hp0 i) (hp1 i))
def treatInd reviewed
⚑ flagged
Causalean.Experimentation.DesignBased
The treatment indicator of unit i under an assignment z: 1 if i is treated, else 0.
lemma bernoulliDesign_E_treatInd_pair reviewed
⚑ flagged
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
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]
5 supporting declarations (lemmas, instances)
-
coinDesign_E_treatlemma — The treatment indicator of a single coin, 1(true), has expectation p.hypothesesp :ℝhp0 :0 ≤ php1 :p ≤ 1conclusion(coinDesign p hp0 hp1).E (fun b => if b then (1 : ℝ) else 0) = pProof (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 -
coinDesign_Var_treatlemma — The treatment indicator of a single coin has variance p(1 − p).hypothesesp :ℝhp0 :0 ≤ php1 :p ≤ 1conclusion(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 -
bernoulliDesign_E_treatIndlemma — 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.hypothesesProof (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] -
bernoulliDesign_Var_treatIndlemma — The treatment indicator of unit i has variance p i (1 − p i) under the Bernoulli design.hypothesesp :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1i :UProof (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] -
bernoulliDesign_Cov_treatIndlemma — For distinct units i ≠ j, the two treatment indicators are uncorrelated under the Bernoulli design.hypothesesp :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1i j :Uh :i ≠ jProof (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)]
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
⚑ flagged
Causalean.Experimentation.DesignBased
The centered monomial attached to a finite set of units S: the product over j ∈ S of unit j's treatment indicator minus its treatment probability. These are the Walsh/Fourier basis functions of the biased Boolean cube; the empty set gives the constant 1.
Definition (Lean source)
noncomputable def centeredMonomial (p : U → ℝ) (S : Finset U) : (U → Bool) → ℝ :=
fun z => ∏ j ∈ S, (treatInd j z - p j)
theorem bernoulliDesign_E_centeredMonomial_mul reviewed
⚑ flagged
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
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
def DependsOnBlock reviewed
⚑ flagged
Causalean.Experimentation.DesignBased
A statistic depends only on the coordinate block N if changing the assignment of any unit outside N leaves its value unchanged.
Definition (Lean source)
def DependsOnBlock (N : Finset U) (F : (U → Bool) → ℝ) : Prop :=
∀ z z', (∀ j ∈ N, z j = z' j) → F z = F z'
15 supporting declarations (lemmas, instances)
-
bernoulliDesign_E_prodlemma — 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).hypothesesProof (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) -
bernoulliDesign_E_prod_finsetlemma — 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.hypothesesProof (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] -
bernoulliDesign_E_treatInd_prodtheorem — 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.hypothesesconclusion(bernoulliDesign p hp0 hp1).E (fun z => ∏ j ∈ S, treatInd j z) = ∏ j ∈ S, p jProof (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 -
bernoulliDesign_E_ctrlInd_prodtheorem — 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.hypothesesconclusion(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 -
treatInd_prod_mul_prodlemma — 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.hypothesesProof (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] -
ctrlInd_prod_mul_prodlemma — 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.hypothesesProof (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] -
bernoulliDesign_E_treatInd_prod_mul_prodtheorem — Two overlapping sets of units are simultaneously treated with probability ∏_{j ∈ S ∪ T} p j: the shared units are counted once, not twice.hypothesesProof (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) -
bernoulliDesign_E_ctrlInd_prod_mul_prodtheorem — 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.hypothesesProof (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) -
centeredMonomial_emptylemma — The centered monomial of the empty set of units is the constant function 1.Proof (Lean source)
@[simp] lemma centeredMonomial_empty (p : U → ℝ) : centeredMonomial p (∅ : Finset U) = fun _ => 1 := rfl -
bernoulliDesign_E_centeredMonomialtheorem — 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.hypothesesconclusion(bernoulliDesign p hp0 hp1).E (centeredMonomial p S) = if S = ∅ then 1 else 0Proof (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 -
bernoulliDesign_E_centeredMonomial_mul_treatInd_prodtheorem — 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.hypothesesconclusion(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 0Proof (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]) -
exists_centeredMonomial_expansionlemma — 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.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 -
bernoulliDesign_E_sq_of_expansiontheorem — 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.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 -
centeredMonomial_coef_empty_eq_zerotheorem — A statistic with design mean zero has no constant term: the coefficient of the empty subset in any centered-monomial expansion of it vanishes.hypothesesp :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1F :(U → Bool) → ℝa :Finset U → ℝha :hmean :(bernoulliDesign p hp0 hp1).E F = 0conclusiona ∅ = 0Proof (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 -
centeredMonomial_coef_eq_zero_of_not_subsettheorem — 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.)hypothesesp :U → ℝhp0 :∀ i, 0 ≤ p ihp1 :∀ i, p i ≤ 1N :Finset UF :(U → Bool) → ℝhF :DependsOnBlock N Fa :Finset U → ℝha :S :Finset UhSN :¬ S ⊆ Nhp0S :∀ i ∈ S, 0 < p ihp1S :∀ i ∈ S, p i < 1conclusiona S = 0Proof (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
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
⚑ flagged
Causalean.Experimentation.DesignBased
The cluster-randomization design: each cluster c is independently assigned treatment with probability p c (a Bernoulli design over the cluster labels). A unit is treated iff its cluster is.
Definition (Lean source)
noncomputable def clusterDesign (p : C → ℝ) (hp0 : ∀ c, 0 ≤ p c) (hp1 : ∀ c, p c ≤ 1) :
FiniteDesign (C → Bool) :=
bernoulliDesign p hp0 hp1
def unitTreatInd reviewed
⚑ flagged
Causalean.Experimentation.DesignBased
The treatment indicator of unit i under cluster assignment z: 1 if i's cluster is treated, else 0.
Definition (Lean source)
lemma clusterDesign_E_unitTreatInd_pair_same reviewed
⚑ flagged
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
p :
C → ℝ
hp0 :
∀ c, 0 ≤ p c
hp1 :
∀ c, p c ≤ 1
clus :
U → C
i j :
U
h :
clus i = clus j
conclusion
= 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))
2 supporting declarations (lemmas, instances)
-
clusterDesign_E_unitTreatIndlemma — First-order inclusion probability. A unit i is treated with probability p (clus i), the treatment rate of its own cluster.hypothesesp :C → ℝhp0 :∀ c, 0 ≤ p chp1 :∀ c, p c ≤ 1clus :U → Ci :Uconclusion(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 -
clusterDesign_E_unitTreatInd_pair_difflemma — Different-cluster joint treatment. Two units in distinct clusters are jointly treated with the product of their cluster rates — distinct clusters are randomized independently.hypothesesp :C → ℝhp0 :∀ c, 0 ≤ p chp1 :∀ c, p c ≤ 1clus :U → Ci j :Uh :clus i ≠ clus jconclusion= 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
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
⚑ flagged
Causalean.Experimentation.DesignBased
The complete-randomization design: the uniform law on size-n₁ subsets of the population, i.e. exactly n₁ of the N = card U units are treated, with every such treated set equally likely. Requires n₁ ≤ N so that the design space is nonempty.
Definition (Lean source)
noncomputable def completeRandomization {V : Type*} [Fintype V] (n₁ : ℕ)
(hn : n₁ ≤ card V) : FiniteDesign {S : Finset V // S.card = n₁} := 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
-- The equally likely treated sets have total mass one; `hn` makes their count positive.
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] }
lemma completeRandomization_incl_pair reviewed
⚑ flagged
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
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
6 supporting declarations (lemmas, instances)
-
completeRandomization_cardlemma — The number of possible treated sets in complete randomization is the binomial coefficient (Fintype.card U).choose n₁.hypothesesV :Type*Fintype Vn₁ :ℕProof (Lean source)
-
card_powersetCard_filter_mem_succlemma — 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.hypothesesconclusion((s.powersetCard (k + 1)).filter (fun t => i ∈ t)).card= ((s.erase i).powersetCard k).cardProof (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) -
card_design_mem_succlemma — 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.hypothesesi :Uk :ℕ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] -
card_powersetCard_filter_mem_pairlemma — 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.hypothesesconclusion((s.powersetCard (k + 2)).filter (fun t => i ∈ t ∧ j ∈ t)).card= (((s.erase i).erase j).powersetCard k).cardProof (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] -
card_design_mem_pairlemma — 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.hypothesesi j :Uhij :i ≠ jk :ℕ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] -
completeRandomization_incllemma — First-order inclusion probability. Under complete randomization, a unit is treated with probability n₁ / N.hypothesesn₁ :ℕhn :n₁ ≤ Fintype.card Ui :Uconclusion(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
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
⚑ flagged
Causalean.Experimentation.DesignBased
The stratified randomization design: an independent complete randomization within each stratum k, treating exactly n₁ k of that stratum's units. Built as the product of the per-stratum complete-randomization designs.
Definition (Lean source)
noncomputable def stratifiedDesign (n₁ : K → ℕ) (hn : ∀ k, n₁ k ≤ card (V k)) :
FiniteDesign (∀ k, {S : Finset (V k) // S.card = n₁ k}) :=
prodDesign (fun k => completeRandomization (n₁ k) (hn k))
lemma stratifiedDesign_incl_pair_across reviewed
⚑ flagged
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
conclusion
(stratifiedDesign n₁ hn).Pr (fun z => i ∈ (z k).val ∧ i' ∈ (z k').val)
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']
2 supporting declarations (lemmas, instances)
-
stratifiedDesign_incllemma — 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.hypothesesconclusion(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 -
stratifiedDesign_incl_pair_withinlemma — 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.hypothesesconclusion(stratifiedDesign n₁ hn).Pr (fun z => i ∈ (z k).val ∧ j ∈ (z k).val)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