Experimentation.DesignBased
The shared, paper-agnostic substrate for design-based / randomization inference under interference: the finite-population, fixed-potential-outcome flavor of the potential-outcomes framework, where probability comes from
DesignCore 14 core · 32 supporting A FiniteDesign Ω is a probability mass function on a finite assignment space Ω. ★ FiniteDesign★ E_sum★ Var_eq★ Cov_eq★ Cov_linear_comb★ Var_linear_comb★ E_ind★ Var_ind
Finite randomization design
A FiniteDesign Ω is a probability mass function on a finite assignment space Ω.
All estimators below are real-valued functions of the realized assignment z : Ω,
and E, Var, Cov are their finite-sum moments under the design.
A randomization design: a probability mass function p on a finite assignment space Ω whose values are nonnegative and sum to one.
Definition (Lean source)
Expectation of a random variable X : Ω → ℝ under the design.
Definition (Lean source)
Variance of X under the design.
Definition (Lean source)
Covariance of X and Y under the design.
Definition (Lean source)
Indicator of an event A, as a {0,1}-valued random variable.
Definition (Lean source)
Probability of an event A under the design.
Definition (Lean source)
Linearity of expectation over a finite sum. For a finite index set s over an index type ι and a family of random variables f, the design expectation of the finite sum ∑ᵢ∈s fᵢ equals the finite sum of the design expectations ∑ᵢ∈s E[fᵢ].
Formal statement
Variance identity. For any statistic X, its design variance equals the design expectation of X² minus the square of its design expectation.
Formal statement
Covariance identity. For any two statistics X and Y under the design, their design covariance equals the design expectation of X·Y minus the product of their design expectations.
Formal statement
Proof (Lean source)
Bilinear expansion of covariance for linear combinations. For finite weighted sums ∑ᵢ∈s cᵢXᵢ and ∑ⱼ∈t eⱼYⱼ, built from index sets s ⊆ ι, t ⊆ κ, weights c, e, and random-variable families X, Y, their design covariance equals the double sum over s×t of the weighted covariances cᵢeⱼ·Cov(Xᵢ,Yⱼ).
Formal statement
Proof (Lean source)
Variance of a finite linear combination. For a finite weighted sum ∑ᵢ∈s cᵢXᵢ, built from an index set s ⊆ ι, weights c, and a random-variable family X, its design variance equals the double sum of weighted covariances ∑ᵢ∈s∑ⱼ∈s cᵢcⱼ·Cov(Xᵢ,Xⱼ).
Formal statement
Proof (Lean source)
Expectation of an indicator. For any event A, the design expectation of its indicator equals the design probability of A.
Formal statement
Proof (Lean source)
Variance of an indicator. For any event A, the design variance of its indicator equals the design probability of A times one minus that probability.
Formal statement
The pushforward design f_* D of D along f : Ω → Ω': the law of the transformed assignment f z when z is drawn from D. Its weight on y is the total design weight of the fiber f⁻¹{y}.
Definition (Lean source)
32 supporting declarations (lemmas, instances)
-
E_constlemma — The expectation of a constant random variable is that constant.hypothesesc :ℝconclusionD.E (fun _ => c) = cProof (Lean source)
@[simp] lemma E_const (c : ℝ) : D.E (fun _ => c) = c := by simp only [E, ← Finset.sum_mul, D.p_sum, one_mul] -
E_addlemma — The expectation of a sum is the sum of expectations.hypothesesX Y :Ω → ℝconclusionD.E (fun z => X z + Y z) = D.E X + D.E YProof (Lean source)
lemma E_add (X Y : Ω → ℝ) : D.E (fun z => X z + Y z) = D.E X + D.E Y := by simp only [E, mul_add, Finset.sum_add_distrib] -
E_sublemma — The expectation of a difference is the difference of expectations.hypothesesX Y :Ω → ℝconclusionD.E (fun z => X z - Y z) = D.E X - D.E YProof (Lean source)
lemma E_sub (X Y : Ω → ℝ) : D.E (fun z => X z - Y z) = D.E X - D.E Y := by simp only [E, mul_sub, Finset.sum_sub_distrib] -
E_const_mullemma — Multiplying a random variable by a constant on the left multiplies its expectation by that constant.hypothesesc :ℝX :Ω → ℝconclusionD.E (fun z => c * X z) = c * D.E XProof (Lean source)
lemma E_const_mul (c : ℝ) (X : Ω → ℝ) : D.E (fun z => c * X z) = c * D.E X := by simp only [E, Finset.mul_sum]; congr 1; funext z; ring -
E_mul_constlemma — Multiplying a random variable by a constant on the right multiplies its expectation by that constant.hypothesesX :Ω → ℝc :ℝconclusionD.E (fun z => X z * c) = D.E X * cProof (Lean source)
lemma E_mul_const (X : Ω → ℝ) (c : ℝ) : D.E (fun z => X z * c) = D.E X * c := by simp only [E, Finset.sum_mul]; congr 1; funext z; ring -
E_neglemma — The expectation of a negated random variable is the negated expectation.hypothesesX :Ω → ℝconclusionD.E (fun z => -X z) = -D.E XProof (Lean source)
lemma E_neg (X : Ω → ℝ) : D.E (fun z => -X z) = -D.E X := by simp only [E, mul_neg, Finset.sum_neg_distrib] -
E_congrlemma — Congruence: pointwise-equal random variables have equal expectation.hypothesesX Y :Ω → ℝh :∀ z, X z = Y zconclusionD.E X = D.E Y -
Var_congrlemma — Congruence: pointwise-equal random variables have equal variance.hypothesesX Y :Ω → ℝh :∀ z, X z = Y zconclusionD.Var X = D.Var Y -
Cov_congrlemma — Congruence: pointwise-equal random variables have equal covariance.hypothesesX Y X' Y' :Ω → ℝhX :∀ z, X z = X' zhY :∀ z, Y z = Y' zconclusionD.Cov X Y = D.Cov X' Y' -
Cov_const_mul_leftlemma — Multiplying the left random variable by a constant multiplies covariance by that constant.hypothesesc :ℝX Y :Ω → ℝconclusionD.Cov (fun z => c * X z) Y = c * D.Cov X YProof (Lean source)
lemma Cov_const_mul_left (c : ℝ) (X Y : Ω → ℝ) : D.Cov (fun z => c * X z) Y = c * D.Cov X Y := by rw [Cov_eq, Cov_eq, E_const_mul] have : D.E (fun z => c * X z * Y z) = c * D.E (fun z => X z * Y z) := by rw [← E_const_mul]; exact D.E_congr (fun z => by ring) rw [this]; ring -
Cov_sum_leftlemma — Covariance with a finite sum in the left argument is the finite sum of covariances.hypothesesconclusionD.Cov (fun z => ∑ i ∈ s, f i z) Y = ∑ i ∈ s, D.Cov (f i) YProof (Lean source)
lemma Cov_sum_left {ι : Type*} (s : Finset ι) (f : ι → Ω → ℝ) (Y : Ω → ℝ) : D.Cov (fun z => ∑ i ∈ s, f i z) Y = ∑ i ∈ s, D.Cov (f i) Y := by have hEY : D.E (fun z => (∑ i ∈ s, f i z) * Y z) = ∑ i ∈ s, D.E (fun z => f i z * Y z) := by rw [← E_sum]; exact D.E_congr (fun z => by rw [Finset.sum_mul]) simp only [Cov_eq] rw [hEY, E_sum, Finset.sum_mul, ← Finset.sum_sub_distrib] -
Cov_sum_rightlemma — Covariance with a finite sum in the right argument is the finite sum of covariances.hypothesesconclusionD.Cov X (fun z => ∑ i ∈ s, g i z) = ∑ i ∈ s, D.Cov X (g i)Proof (Lean source)
lemma Cov_sum_right {ι : Type*} (s : Finset ι) (X : Ω → ℝ) (g : ι → Ω → ℝ) : D.Cov X (fun z => ∑ i ∈ s, g i z) = ∑ i ∈ s, D.Cov X (g i) := by rw [Cov_comm, Cov_sum_left] exact Finset.sum_congr rfl (fun i _ => D.Cov_comm _ _) -
Cov_const_mul_rightlemma — Multiplying the right random variable by a constant multiplies covariance by that constant.hypothesesc :ℝX Y :Ω → ℝconclusionD.Cov X (fun z => c * Y z) = c * D.Cov X YProof (Lean source)
lemma Cov_const_mul_right (c : ℝ) (X Y : Ω → ℝ) : D.Cov X (fun z => c * Y z) = c * D.Cov X Y := by rw [Cov_comm, Cov_const_mul_left, Cov_comm] -
Cov_sub_leftlemma — Covariance is linear over differences in its left argument.hypothesesX Y Z :Ω → ℝconclusionD.Cov (fun z => X z - Y z) Z = D.Cov X Z - D.Cov Y ZProof (Lean source)
-
Cov_sub_rightlemma — Covariance is linear over differences in its right argument.hypothesesX Y Z :Ω → ℝconclusionD.Cov X (fun z => Y z - Z z) = D.Cov X Y - D.Cov X ZProof (Lean source)
lemma Cov_sub_right (X Y Z : Ω → ℝ) : D.Cov X (fun z => Y z - Z z) = D.Cov X Y - D.Cov X Z := by rw [Cov_comm, Cov_sub_left, D.Cov_comm Y X, D.Cov_comm Z X] -
Var_sublemma — Variance of a difference: Var(X−Y) = Var X + Var Y − 2 Cov(X,Y).hypothesesX Y :Ω → ℝconclusionD.Var (fun z => X z - Y z) = D.Var X + D.Var Y - 2 * D.Cov X YProof (Lean source)
lemma Var_sub (X Y : Ω → ℝ) : D.Var (fun z => X z - Y z) = D.Var X + D.Var Y - 2 * D.Cov X Y := by rw [← Cov_self, Cov_sub_left, Cov_sub_right, Cov_sub_right, Cov_self, Cov_self, D.Cov_comm Y X] ring -
Var_const_mullemma — Variance scales by the square of a constant: Var(c·X) = c²·Var X.hypothesesc :ℝX :Ω → ℝconclusionD.Var (fun z => c * X z) = c ^ 2 * D.Var XProof (Lean source)
lemma Var_const_mul (c : ℝ) (X : Ω → ℝ) : D.Var (fun z => c * X z) = c ^ 2 * D.Var X := by rw [← Cov_self, Cov_const_mul_left, Cov_const_mul_right, Cov_self]; ring -
ind_sqlemma — 1_A ^ 2 = 1_A, the idempotence of an indicator. -
E_nonneglemma — Expectation of a nonnegative random variable is nonnegative.hypothesesX :Ω → ℝh :∀ z, 0 ≤ X zconclusion0 ≤ D.E XProof (Lean source)
lemma E_nonneg {X : Ω → ℝ} (h : ∀ z, 0 ≤ X z) : 0 ≤ D.E X := sum_nonneg (fun z _ => mul_nonneg (D.p_nonneg z) (h z)) -
E_le_onelemma — Expectation of a random variable bounded above by one is at most one.hypothesesX :Ω → ℝh1 :∀ z, X z ≤ 1conclusionD.E X ≤ 1 -
ind_nonneglemma — An event indicator is always nonnegative.Proof (Lean source)
lemma ind_nonneg (A : Ω → Prop) [DecidablePred A] (z : Ω) : 0 ≤ ind A z := by unfold ind; by_cases h : A z <;> simp [h] -
ind_le_onelemma — An event indicator is always at most one.Proof (Lean source)
lemma ind_le_one (A : Ω → Prop) [DecidablePred A] (z : Ω) : ind A z ≤ 1 := by unfold ind; by_cases h : A z <;> simp [h] -
Pr_nonneglemma — A probability lies in [0,1]: nonnegativity.Proof (Lean source)
lemma Pr_nonneg (A : Ω → Prop) [DecidablePred A] : 0 ≤ D.Pr A := D.E_nonneg (fun z => ind_nonneg A z) -
Pr_le_onelemma — A probability lies in [0,1]: at most one.Proof (Lean source)
lemma Pr_le_one (A : Ω → Prop) [DecidablePred A] : D.Pr A ≤ 1 := D.E_le_one (fun z => ind_le_one A z) -
Pr_congrlemma — Probability respects pointwise-equivalent events.hypothesesA B :h :∀ z, A z ↔ B zconclusionD.Pr A = D.Pr BProof (Lean source)
lemma Pr_congr (A B : Ω → Prop) [DecidablePred A] [DecidablePred B] (h : ∀ z, A z ↔ B z) : D.Pr A = D.Pr B := by unfold Pr; exact D.E_congr (fun z => by unfold ind; simp only [h z]) -
Pr_monolemma — Monotonicity of probability: a smaller event has smaller probability.hypothesesA B :h :∀ zifA zthenB zconclusionD.Pr A ≤ D.Pr BProof (Lean source)
lemma Pr_mono (A B : Ω → Prop) [DecidablePred A] [DecidablePred B] (h : ∀ z, A z → B z) : D.Pr A ≤ D.Pr B := by unfold Pr E ind apply Finset.sum_le_sum intro z _ apply mul_le_mul_of_nonneg_left _ (D.p_nonneg z) by_cases hA : A z · simp [hA, h z hA] · by_cases hB : B z <;> simp [hA, hB] -
Pr_splitlemma — Finite additivity: splitting an event by a second event.hypothesesB A :conclusionD.Pr B = D.Pr (fun z => B z ∧ A z) + D.Pr (fun z => B z ∧ ¬ A z)Proof (Lean source)
lemma Pr_split (B A : Ω → Prop) [DecidablePred A] [DecidablePred B] : D.Pr B = D.Pr (fun z => B z ∧ A z) + D.Pr (fun z => B z ∧ ¬ A z) := by unfold Pr E ind rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro z _ by_cases hB : B z <;> by_cases hA : A z <;> simp [hB, hA] -
map_plemma — The pushforward weight of y is the fiber sum ∑_{z} 1[f z = y] · D.p z.hypothesesconclusion(D.map f).p y = ∑ z, @ite ℝ (f z = y) (propDecidable _) (D.p z) 0Proof (Lean source)
@[simp] lemma map_p {Ω' : Type*} [Fintype Ω'] (f : Ω → Ω') (y : Ω') : (D.map f).p y = ∑ z, @ite ℝ (f z = y) (propDecidable _) (D.p z) 0 := by classical rfl -
E_maplemma — Transfer of expectation across a pushforward. The expectation of g under the pushforward f_* D equals the expectation of the composite g ∘ f under D.hypothesesconclusion(D.map f).E g = D.E (fun z => g (f z))Proof (Lean source)
lemma E_map {Ω' : Type*} [Fintype Ω'] (f : Ω → Ω') (g : Ω' → ℝ) : (D.map f).E g = D.E (fun z => g (f z)) := by classical unfold E map simp only [Finset.sum_mul] rw [Finset.sum_comm] refine Finset.sum_congr rfl fun z _ => ?_ have hpt : ∀ y, (if f z = y then D.p z else 0) * g y = if f z = y then D.p z * g y else 0 := fun y => by by_cases h : f z = y <;> simp [h] simp only [hpt, Finset.sum_ite_eq, Finset.mem_univ, if_true] -
Pr_maplemma — Transfer of probability across a pushforward. The probability of an event A under the pushforward f_* D equals the probability of its preimage under D.hypothesesconclusion(D.map f).Pr A = D.Pr (fun z => A (f z))
FiniteDesignMeasure 4 core · 2 supporting Finite randomization designs can be viewed as ordinary probability measures, enabling reuse of measure-theoretic probability results. ★ integral_toMeasure★ toMeasure_real_setOf★ variance_toMeasure
Finite designs as probability measures
Finite randomization designs can be viewed as ordinary probability measures, enabling reuse of measure-theoretic probability results.
For a design D, FiniteDesign.toMeasure places mass D.p z at each assignment z. The induced
measure is registered as an IsProbabilityMeasure, and the bridge theorems
integral_toMeasure, toMeasure_real_setOf, and variance_toMeasure identify integrals, event
probabilities, and variances under D.toMeasure with the finite-design operations D.E, D.Pr,
and D.Var.
The probability measure on Ω induced by the design: ∑_z (p z)·δ_z.
Integral against the induced measure is the design expectation. For any statistic g, the measure-theoretic integral of g against the design's induced probability measure equals its design expectation.
Formal statement
Proof (Lean source)
Induced measure matches the design probability. For any event A, the induced measure's probability of A equals the design probability of A.
Formal statement
Proof (Lean source)
Measure-theoretic variance equals the design variance. For any statistic g, the measure-theoretic variance of g under the design's induced measure equals its design variance.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
toMeasure_applylemma — The measure induced by a finite randomization design assigns each set the sum, over assignments, of each assignment's probability times the point mass of that assignment on the set.Proof (Lean source)
lemma toMeasure_apply (s : Set Ω) : D.toMeasure s = ∑ z, ofReal (D.p z) * Measure.dirac z s := by rw [toMeasure, Measure.finset_sum_apply] refine Finset.sum_congr rfl (fun z _ => ?_) rw [Measure.smul_apply, smul_eq_mul] -
instIsProbabilityMeasureToMeasureinstance — The measure induced by a finite randomization design has total mass one.instance : IsProbabilityMeasure D.toMeasure := by refine ⟨?_⟩ rw [toMeasure_apply] have h : ∀ z ∈ (Finset.univ : Finset Ω), ofReal (D.p z) * Measure.dirac z univ = ofReal (D.p z) := by intro z _; rw [Measure.dirac_apply' z MeasurableSet.univ]; simp rw [Finset.sum_congr rfl h, ← ENNReal.ofReal_sum_of_nonneg (fun z _ => D.p_nonneg z), D.p_sum, ENNReal.ofReal_one]
Product 4 core · 0 supporting This file constructs prodDesign, the finite product of a family of independent randomization designs. ★ prodDesign★ prodDesign_p★ E_prod_prod★ E_prod_apply
Product finite randomization designs
This file constructs prodDesign, the finite product of a family of independent randomization
designs. Its probability mass function is the product of the coordinate probabilities, recorded by
prodDesign_p.
The main expectation identities are FiniteDesign.E_prod_prod, which factors expectations of
products of coordinate functions, and FiniteDesign.E_prod_apply, which says a statistic depending
on one coordinate has the expectation induced by that coordinate's marginal design.
The product design of a finite family D i : FiniteDesign (α i): each coordinate is randomized independently, with joint pmf w ↦ ∏ i, (D i).p (w i).
Definition (Lean source)
For a family of independent coordinate designs D and an assignment w, the product-design probability of w equals the product of the coordinate probabilities ∏ᵢ (D i).p (w i).
Formal statement
Proof (Lean source)
For a family of independent coordinate designs D and single-coordinate functions g, the expectation under the product design of the product ∏ᵢ g i (w i) factors into the product of the individual coordinate expectations ∏ᵢ (D i).E (g i).
Formal statement
Proof (Lean source)
For a family of independent coordinate designs D, the expectation under the product design of a function of a single coordinate j equals the expectation of that same function under coordinate j's own marginal design.
Formal statement
Proof (Lean source)
GaussianCDF 3 core · 4 supporting The design-based standard-normal CDF is a namespace-local presentation of the canonical Mathlib-facing CDF. ★ stdNormalCdf_neg★ continuous_stdNormalCdf
Standard normal CDF adapter
The design-based standard-normal CDF is a namespace-local presentation of the canonical Mathlib-facing CDF.
The definition stdNormalCdf uses the .real (Iic t) probability-measure presentation needed by
design-based interval and CLT statements, while stdNormalCdf_eq identifies it with
Causalean.Mathlib.stdNormalCDF. The remaining lemmas forward the reusable facts needed
downstream: nonnegativity, the upper bound by one, monotonicity, symmetry
stdNormalCdf_neg, and continuity continuous_stdNormalCdf.
Standard normal cumulative distribution function Φ(t) = P[Z ≤ t], Z ∼ 𝒩(0,1), in the (gaussianReal 0 1).real (Iic t) presentation used by the design-based interval theorems. Definitionally the canonical Causalean.Mathlib.stdNormalCDF (see stdNormalCdf_eq).
Definition (Lean source)
Symmetry of the standard normal CDF. For any threshold t, the standard normal CDF satisfies Φ(−t) = 1 − Φ(t).
Formal statement
Proof (Lean source)
Continuity of the standard normal CDF. The standard normal cumulative distribution function Φ is continuous.
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
stdNormalCdf_eqlemma — The design-based .real (Iic) presentation agrees with the canonical stdNormalCDF.Proof (Lean source)
@[simp] lemma stdNormalCdf_eq (t : ℝ) : stdNormalCdf t = stdNormalCDF t := by rw [stdNormalCDF_def]; exact (ProbabilityTheory.cdf_eq_real _ t).symm -
stdNormalCdf_nonneglemma — The standard-normal cumulative probability is nonnegative.Proof (Lean source)
lemma stdNormalCdf_nonneg (t : ℝ) : 0 ≤ stdNormalCdf t := by rw [stdNormalCdf_eq]; exact stdNormalCDF_nonneg t -
stdNormalCdf_le_onelemma — The standard-normal cumulative probability is at most one.Proof (Lean source)
lemma stdNormalCdf_le_one (t : ℝ) : stdNormalCdf t ≤ 1 := by rw [stdNormalCdf_eq]; exact stdNormalCDF_le_one t -
monotone_stdNormalCdflemma — The standard-normal cumulative distribution function is monotone in its threshold.conclusionProof (Lean source)
lemma monotone_stdNormalCdf : Monotone stdNormalCdf := by rw [show stdNormalCdf = stdNormalCDF from funext stdNormalCdf_eq] exact stdNormalCDF_monotone
Exposure 9 core · 2 supporting Exposure mappings turn assignments and unit traits into treatment conditions, and generalized exposure probabilities are the design probabilities of those conditions. ★ prop★ E_expoInd★ Cov_expoInd_same★ Cov_expoInd_cross★ sum_prop_eq_one
Exposure mappings and generalized exposure probabilities
Exposure mappings turn assignments and unit traits into treatment conditions, and generalized exposure probabilities are the design probabilities of those conditions.
The basic declarations are expo, the indicator expoInd, the marginal probability prop, and
the joint probabilities propPairSame and propPairCross. The covariance lemmas
Cov_expoInd_same and Cov_expoInd_cross rewrite indicator covariances into those probabilities,
while expoInd_mul_self_of_ne and propPairCross_self_of_ne record that one unit cannot occupy two
distinct exposures in the same assignment. For finite exposure spaces, sum_prop_eq_one shows that
each unit's exposure probabilities sum to one.
The exposure unit i receives under assignment z: f z (θ i).
Definition (Lean source)
Indicator that unit i is in exposure condition d under assignment z.
Generalized probability of exposure: π_i(d) = Pr[expo i = d].
Definition (Lean source)
Joint exposure probability π_{ij}(d) = E[1(expo i = d)·1(expo j = d)].
Definition (Lean source)
Cross joint exposure probability π_{ij}(d,d') = E[1(expo i = d)·1(expo j = d')].
Definition (Lean source)
Exposure probability as an expectation. For a design, an exposure mapping, unit traits, a unit i, and an exposure level d, the design expectation of the exposure indicator equals the generalized probability of exposure π_i(d).
Formal statement
Proof (Lean source)
Covariance of same-exposure indicators. For a design, an exposure mapping, unit traits, units i and j, and an exposure level d, the design covariance of the two units' d-exposure indicators equals the joint exposure probability π_ij(d) minus the product of their marginal exposure probabilities.
Formal statement
Proof (Lean source)
Covariance of cross-exposure indicators. For a design, an exposure mapping, unit traits, units i and j, and exposure levels d and d', the design covariance of unit i's d-exposure indicator and unit j's d'-exposure indicator equals the cross joint exposure probability π_ij(d,d') minus the product of their marginal exposure probabilities.
Formal statement
Proof (Lean source)
Exposure probabilities sum to one. For a design, an exposure mapping, unit traits, and a unit i, the generalized exposure probabilities of unit i, summed over all exposure levels, equal one.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
expoInd_mul_self_of_nelemma — A unit cannot be in two distinct exposures at once: the indicators are pointwise disjoint.hypothesesf :Ω → Θ → Δθ :ι → Θi :ιd d' :Δhne :d ≠ d'z :ΩProof (Lean source)
lemma expoInd_mul_self_of_ne (f : Ω → Θ → Δ) (θ : ι → Θ) (i : ι) {d d' : Δ} (hne : d ≠ d') (z : Ω) : expoInd f θ i d z * expoInd f θ i d' z = 0 := by unfold expoInd FiniteDesign.ind by_cases h : expo f θ i z = d · simp [h, hne] · simp [h] -
propPairCross_self_of_nelemma — The self cross-exposure joint probability vanishes for distinct exposures.hypothesesconclusionpropPairCross D f θ i i d d' = 0Proof (Lean source)
lemma propPairCross_self_of_ne (D : FiniteDesign Ω) (f : Ω → Θ → Δ) (θ : ι → Θ) (i : ι) {d d' : Δ} (hne : d ≠ d') : propPairCross D f θ i i d d' = 0 := by unfold propPairCross rw [show (fun z => expoInd f θ i d z * expoInd f θ i d' z) = (fun _ => (0 : ℝ)) from funext (fun z => expoInd_mul_self_of_ne f θ i hne z)] exact D.E_const 0
Risk 4 core · 6 supporting Bias and mean squared error summarize fixed-target estimation error under a finite design. ★ mse_eq_var_add_bias_sq
Design-based risk summaries
Bias and mean squared error summarize fixed-target estimation error under a finite design.
The definitions FiniteDesign.bias, FiniteDesign.mse, and FiniteDesign.Unbiased describe
estimation error for a fixed target under a finite randomization design. The central theorem
FiniteDesign.mse_eq_var_add_bias_sq proves the bias-variance decomposition, with supporting
lemmas for unbiased estimators, nonnegativity, the lower bound FiniteDesign.var_le_mse, and
congruence under pointwise-equal estimators.
Bias of an estimator est for the target μ under the design: E[est] − μ.
Definition (Lean source)
Mean squared error of est for the target μ under the design: E[(est − μ)²].
Definition (Lean source)
An estimator is unbiased for μ under the design when its expectation equals μ.
Definition (Lean source)
Bias–variance decomposition. The mean squared error mse of estimator est for target μ equals its randomization variance plus the square of its bias: mse = Var + bias².
Formal statement
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
mse_eq_var_of_unbiasedlemma — For an unbiased estimator the mean squared error equals the variance.hypothesesest :Ω → ℝμ :ℝh :D.Unbiased est μconclusionD.mse est μ = D.Var estProof (Lean source)
lemma mse_eq_var_of_unbiased {est : Ω → ℝ} {μ : ℝ} (h : D.Unbiased est μ) : D.mse est μ = D.Var est := by rw [mse_eq_var_add_bias_sq] unfold bias Unbiased at * rw [h]; ring -
bias_of_unbiasedlemma — The bias of an unbiased estimator is zero.hypothesesest :Ω → ℝμ :ℝh :D.Unbiased est μconclusionD.bias est μ = 0Proof (Lean source)
@[simp] lemma bias_of_unbiased {est : Ω → ℝ} {μ : ℝ} (h : D.Unbiased est μ) : D.bias est μ = 0 := by unfold bias Unbiased at *; rw [h]; ring -
mse_nonneglemma — Mean squared error is nonnegative.hypothesesest :Ω → ℝμ :ℝconclusion0 ≤ D.mse est μProof (Lean source)
lemma mse_nonneg (est : Ω → ℝ) (μ : ℝ) : 0 ≤ D.mse est μ := D.E_nonneg (fun _ => sq_nonneg _) -
Var_nonneglemma — Variance is nonnegative (it is the mean squared error of the centered estimator).hypothesesX :Ω → ℝconclusion0 ≤ D.Var XProof (Lean source)
lemma Var_nonneg (X : Ω → ℝ) : 0 ≤ D.Var X := by have : D.Var X = D.mse X (D.E X) := by unfold mse Var; rfl rw [this]; exact D.mse_nonneg _ _ -
var_le_mselemma — Mean squared error is bounded below by the variance.hypothesesest :Ω → ℝμ :ℝconclusionD.Var est ≤ D.mse est μProof (Lean source)
lemma var_le_mse (est : Ω → ℝ) (μ : ℝ) : D.Var est ≤ D.mse est μ := by rw [mse_eq_var_add_bias_sq] exact le_add_of_nonneg_right (sq_nonneg _) -
mse_congrlemma — Congruence: pointwise-equal estimators have equal mean squared error.hypothesesest est' :Ω → ℝμ :ℝh :∀ z, est z = est' zconclusionD.mse est μ = D.mse est' μProof (Lean source)
lemma mse_congr {est est' : Ω → ℝ} {μ : ℝ} (h : ∀ z, est z = est' z) : D.mse est μ = D.mse est' μ := D.E_congr (fun z => by rw [h z])
TwoStage 4 core · 0 supporting Compound designs combine a stage-one design with conditionally independent stage-two designs. ★ compound★ E_compound★ E_compound_factor
Two-stage compound randomization designs
Compound designs combine a stage-one design with conditionally independent stage-two designs.
The definition compound builds the joint finite design on (stage_one, stage_two_assignments)
from a first-stage design and conditionally independent coordinate designs. Lemma
FiniteDesign.E_compound expands expectations as an iterated finite sum, and
FiniteDesign.E_compound_factor collapses the stage-two expectation of a statistic that depends on
one coordinate to that coordinate's conditional marginal expectation.
Generic conditional composition of a first-stage finite design with a finite second-stage design chosen after observing the first-stage outcome.
Definition (Lean source)
The compound (two-stage) design: stage-1 design D₁ on Ω₁, then, conditionally on the stage-1 outcome s, the independent within-coordinate designs D₂ s i.
Definition (Lean source)
For the stage-2 design map assigning each stage-1 outcome s a per-coordinate design D₂ s and any real-valued function X of the joint outcome, built on top of a stage-1 design D₁, the expectation of X under the compound (two-stage) design equals the double sum over stage-1 outcomes s and stage-2 profiles w of the compound probability D₁.p(s)·∏ᵢ(D₂ s i).p(wᵢ) times X(s,w).
Formal statement
Proof (Lean source)
Stage-2 collapse. For the stage-2 design map assigning each stage-1 outcome s a per-coordinate design D₂ s, the compound-design expectation of the product of a stage-1 quantity h(s) and a function g of a single group j's within-assignment wⱼ factors through the marginal expectation of group j's conditional design: E[h(s)·g(wⱼ)] = E_s[h(s)·E_{D₂ s j}[g]].
Formal statement
Proof (Lean source)
Chebyshev 1 core · 1 supporting This file proves FiniteDesign.chebyshev, the finite-design Chebyshev inequality Pr[ε ≤ |X - E X|] ≤ Var X / ε ^ 2 for a statistic on a finite assignment space. ★ chebyshev
Finite Chebyshev inequality
This file proves FiniteDesign.chebyshev, the finite-design Chebyshev inequality
Pr[ε ≤ |X - E X|] ≤ Var X / ε ^ 2 for a statistic on a finite assignment space.
The proof works directly from FiniteDesign.Pr, FiniteDesign.E, and FiniteDesign.Var, so it
can be used in design-based consistency arguments without moving through the measure-theoretic
probability layer.
Finite-design Chebyshev inequality. In a finite design, for any statistic X and a strictly positive threshold ε, the design probability that X differs from its design mean by at least ε is at most the design variance of X divided by ε².
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
Pr_eq_zero_lelemma — Zero-hitting bound for a nonzero-mean statistic. In a finite design, a statistic whose design mean is nonzero equals zero with probability at most its design variance divided by the square of its mean. This is the Chebyshev corollary that controls degeneracy of a random Horvitz–Thompson / Hájek denominator: a zero value is exactly a deviation from the mean of size equal to the mean, so it is Var / mean²-rare.hypothesesX :Ω → ℝh :D.E X ≠ 0conclusionD.Pr (fun z => X z = 0) ≤ D.Var X / (D.E X) ^ 2Proof (Lean source)
lemma Pr_eq_zero_le (X : Ω → ℝ) (h : D.E X ≠ 0) : D.Pr (fun z => X z = 0) ≤ D.Var X / (D.E X) ^ 2 := by have hpos : (0 : ℝ) < |D.E X| := abs_pos.mpr h have hmono : D.Pr (fun z => X z = 0) ≤ D.Pr (fun z => |D.E X| ≤ |X z - D.E X|) := by apply D.Pr_mono intro z hz have habs : |X z - D.E X| = |D.E X| := by rw [hz, zero_sub, abs_neg] exact le_of_eq habs.symm have hcheb : D.Pr (fun z => |D.E X| ≤ |X z - D.E X|) ≤ D.Var X / |D.E X| ^ 2 := D.chebyshev X hpos rw [sq_abs] at hcheb exact hmono.trans hcheb
CompoundVariance 1 core · 1 supporting This file proves the expectation tower property FiniteDesign.E_compound_tower for the two-stage compound design and the corresponding law of total variance FiniteDesign.Var_compound_eq_tower. ★ Var_compound_eq_tower
Compound-design variance decomposition
This file proves the expectation tower property FiniteDesign.E_compound_tower for the two-stage
compound design and the corresponding law of total variance
FiniteDesign.Var_compound_eq_tower. The decomposition writes total variance as expected
within-stage variance plus the stage-1 variance of the stage-2 conditional mean, the algebraic form
used by partial-interference between-group and within-group variance decompositions.
Law of total variance for the two-stage compound design. For a stage-1 design D₁ paired with a stage-2 design D₂ s at every stage-1 outcome s, applied to any statistic X on the joint outcome space, the total variance of X under the compound design decomposes as the stage-1 expectation of the stage-2 conditional variance of X, plus the stage-1 variance of the stage-2 conditional mean of X:
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
E_compound_towerlemma — Tower property of expectation for the compound design. The compound expectation iterates as the stage-1 expectation of the stage-2 product-design conditional expectation, E[F] = E_s[E_{D₂ s}[F(s, ·)]].hypothesesconclusion(compound D₁ D₂).E F = D₁.E (fun s => (prodDesign (D₂ s)).E (fun w => F (s, w)))Proof (Lean source)
lemma E_compound_tower (D₁ : FiniteDesign Ω₁) (D₂ : Ω₁ → ∀ i, FiniteDesign (α i)) (F : (Ω₁ × ∀ i, α i) → ℝ) : (compound D₁ D₂).E F = D₁.E (fun s => (prodDesign (D₂ s)).E (fun w => F (s, w))) := by rw [E_compound] simp only [FiniteDesign.E, prodDesign_p] apply Finset.sum_congr rfl intro s _ rw [Finset.mul_sum] apply Finset.sum_congr rfl intro w _ ring
Concentration 1 core · 2 supporting For a finite design D and a statistic X bounded by c, with design mean 0 and design variance at most v, bernstein_ge gives the one-sided tail bound Pr[ε ≤ X] ≤ exp(−ε² / (2(2v + cε))) and bernstein_abs_ge the two-sided b ★ bernstein_abs_ge
Bernstein concentration for a bounded design statistic
For a finite design D and a statistic X bounded by c, with design mean 0 and design
variance at most v, bernstein_ge gives the one-sided tail bound
Pr[ε ≤ X] ≤ exp(−ε² / (2(2v + cε))) and bernstein_abs_ge the two-sided bound
Pr[ε ≤ |X|] ≤ 2·exp(−ε² / (2(2v + cε))). These are exponentially sharper than the Chebyshev
bound Var/ε², and are obtained from the measure-theoretic sub-exponential Chernoff bound through
the design-to-measure bridge.
Bernstein tail for a bounded design statistic (two-sided). For a statistic X on a finite design, suppose the bound c is nonnegative, X has design mean 0 , X is bounded in absolute value by c everywhere, the design variance of X is at most v, and the threshold ε is nonnegative. Then the design probability that X deviates from 0 by at least ε in absolute value is at most 2·exp(−ε²/(2(2v + cε))), twice the corresponding one-sided Bernstein bound.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
hasSubexponentialMGF_of_boundedlemma — A bounded, mean-zero statistic on a finite design is sub-exponential under the design measure, with variance-proxy 2v and scale c. This is the finite-design instance of the Bernstein sub-exponential lemma, obtained through the measure bridge.hypothesesX :Ω → ℝc v :ℝhc :0 ≤ chmean :D.E X = 0hbound :∀ z, |X z| ≤ chvar :D.Var X ≤ vconclusionHasSubexponentialMGF X ⟨2 * v, by exact mul_nonneg (by norm_num) (le_trans (D.E_nonneg fun _ => sq_nonneg _) hvar)⟩ ⟨c, hc⟩ D.toMeasureProof (Lean source)
lemma hasSubexponentialMGF_of_bounded (X : Ω → ℝ) {c v : ℝ} (hc : 0 ≤ c) (hmean : D.E X = 0) (hbound : ∀ z, |X z| ≤ c) (hvar : D.Var X ≤ v) : HasSubexponentialMGF X ⟨2 * v, by exact mul_nonneg (by norm_num) (le_trans (D.E_nonneg fun _ => sq_nonneg _) hvar)⟩ ⟨c, hc⟩ D.toMeasure := by have hmean' : D.toMeasure[X] = 0 := (D.integral_toMeasure X).trans hmean have hvar' : D.toMeasure[fun ω => X ω ^ 2] ≤ v := by rw [D.integral_toMeasure (fun z => X z ^ 2)] have : D.E (fun z => X z ^ 2) = D.Var X := by rw [D.Var_eq X, hmean]; ring rw [this]; exact hvar have hv : 0 ≤ v := le_trans (D.E_nonneg fun _ => sq_nonneg _) hvar simpa only [Real.sq_sqrt hv] using bounded_hasSubexponentialMGF (σ := sqrt v) hc (D.aemeasurable_toMeasure X) hmean' (Filter.Eventually.of_forall hbound) (by simpa only [Real.sq_sqrt hv] using hvar') -
bernstein_getheorem — Bernstein tail for a bounded design statistic (one-sided). If a statistic is bounded by c, has design mean 0, and has design variance at most v, then it exceeds a nonnegative threshold ε with probability at most exp(−ε² / (2(2v + cε))), far sharper than Chebyshev.hypothesesX :Ω → ℝc v ε :ℝhc :0 ≤ chmean :D.E X = 0hbound :∀ z, |X z| ≤ chvar :D.Var X ≤ vhε :0 ≤ εconclusionD.Pr (fun z => ε ≤ X z) ≤ exp (-ε ^ 2 / (2 * (2 * v + c * ε)))Proof (Lean source)
theorem bernstein_ge (X : Ω → ℝ) {c v ε : ℝ} (hc : 0 ≤ c) (hmean : D.E X = 0) (hbound : ∀ z, |X z| ≤ c) (hvar : D.Var X ≤ v) (hε : 0 ≤ ε) : D.Pr (fun z => ε ≤ X z) ≤ exp (-ε ^ 2 / (2 * (2 * v + c * ε))) := by have hsub := D.hasSubexponentialMGF_of_bounded X hc hmean hbound hvar have h := hsub.measure_ge_le hε rw [D.toMeasure_real_setOf (fun z => ε ≤ X z)] at h -- `((⟨_, _⟩ : ℝ≥0) : ℝ)` is definitionally the underlying real, so `exact` closes this -- at default transparency (`simpa`'s final check no longer unfolds it). exact h
DependencyCLT 1 core · 0 supporting dependency_studentized_cdf transports the bounded-degree dependency-graph CLT to the finite-design layer: for a sequence of designs whose unit contributions X n are uniformly bounded, mean-zero, and dependent only across ★ dependency_studentized_cdf
Design-based dependency-graph CLT
dependency_studentized_cdf transports the bounded-degree dependency-graph CLT to the finite-design
layer: for a sequence of designs whose unit contributions X n are uniformly bounded, mean-zero,
and dependent only across a bounded-degree graph, with the standardizing variance v n bounded
below by a constant multiple of the number of units, the studentized statistic
depSum(X n)/√(v n) has standard-normal limiting CDF under D n. It is stated in the
FiniteDesign.Pr form so it plugs directly into conservative_wald_liminf_of_studentized_cdf.
Design-based dependency-graph CLT (studentized CDF form). Consider a sequence of finite designs D n together with a triangular array of unit contributions X n i and, for each n, a dependency-graph structure Dep n on the units. Suppose every neighbourhood in the dependency graph has size at most Dmax, the contributions are uniformly bounded by a nonnegative constant M, each contribution has design mean 0, the design second moment v n of the aggregate depSum(X n) is recorded exactly, a positive constant c eventually lower-bounds v n by c times the number of units, and the number of units diverges to infinity. Then, at every point s, the studentized aggregate depSum(X n)/√(v n) has, under the design D n, a limiting CDF equal to the standard normal CDF at s.
Formal statement
Proof (Lean source)
EdgeVarianceBound 1 core · 3 supporting This file proves bounded-expectation and bounded-covariance helpers for FiniteDesign (abs_E_le, abs_Cov_le_two_sq, and Cov_zero_left) and the main dependency-graph edge-sum variance inequality var_edge_sum_le. ★ var_edge_sum_le
Edge-sum variance bound for finite designs
This file proves bounded-expectation and bounded-covariance helpers for FiniteDesign
(abs_E_le, abs_Cov_le_two_sq, and Cov_zero_left) and the main dependency-graph edge-sum
variance inequality var_edge_sum_le. The final theorem controls the variance of a sum of bounded
edge-indexed statistics by 8 * M ^ 2 * (m ^ 3 * N) when the edge variables vanish off a symmetric
bounded-degree graph and are uncorrelated across graph-separated edges.
Variance of an edge-sum over a bounded-degree dependency graph. Consider real-valued statistics b i j attached to ordered pairs of units, all defined on the same finite design. Suppose every statistic attached to an edge of a graph G is bounded in absolute value by a nonnegative constant M, G is symmetric, every unit has at most m neighbours in G, every statistic attached to a pair that is not an edge of G is identically zero, and two statistics are uncorrelated whenever no edge of G connects an endpoint of one pair to an endpoint of the other. Then the variance of the double sum ∑ᵢ∑ⱼ b i j is at most 8·M²·m³·N, where N is the number of units.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
abs_E_lelemma — The expectation of a random variable whose absolute value is bounded by M pointwise is itself bounded by M in absolute value.hypothesesX :Ω → ℝM :ℝh :∀ z, |X z| ≤ Mconclusion|D.E X| ≤ MProof (Lean source)
lemma abs_E_le {X : Ω → ℝ} {M : ℝ} (h : ∀ z, |X z| ≤ M) : |D.E X| ≤ M := by apply abs_le.mpr constructor · -- -M ≤ D.E X have hptw : ∀ z, 0 ≤ X z + M := by intro z; have := abs_le.mp (h z); linarith have hpos : 0 ≤ D.E (fun z => X z + M) := D.E_nonneg hptw have heq : D.E (fun z => X z + M) = D.E X + M := by rw [D.E_add]; simp [D.E_const] rw [heq] at hpos; linarith · -- D.E X ≤ M have hptw : ∀ z, 0 ≤ M - X z := by intro z; have := abs_le.mp (h z); linarith have hpos : 0 ≤ D.E (fun z => M - X z) := D.E_nonneg hptw have heq : D.E (fun z => M - X z) = M - D.E X := by rw [D.E_sub]; simp [D.E_const] rw [heq] at hpos; linarith -
abs_Cov_le_two_sqlemma — The design covariance of random variables bounded by MX and MY in absolute value pointwise is bounded by 2·MX·MY in absolute value.hypothesesX Y :Ω → ℝMX MY :ℝhMX :0 ≤ MXhX :∀ z, |X z| ≤ MXhY :∀ z, |Y z| ≤ MYconclusion|D.Cov X Y| ≤ 2 * MX * MYProof (Lean source)
lemma abs_Cov_le_two_sq {X Y : Ω → ℝ} {MX MY : ℝ} (hMX : 0 ≤ MX) (hX : ∀ z, |X z| ≤ MX) (hY : ∀ z, |Y z| ≤ MY) : |D.Cov X Y| ≤ 2 * MX * MY := by rw [D.Cov_eq] have hExy : |D.E (fun z => X z * Y z)| ≤ MX * MY := by apply D.abs_E_le (X := fun z => X z * Y z) (M := MX * MY) intro z rw [abs_mul] exact mul_le_mul (hX z) (hY z) (abs_nonneg _) hMX have hEX : |D.E X| ≤ MX := D.abs_E_le hX have hEY : |D.E Y| ≤ MY := D.abs_E_le hY have hprod : |D.E X * D.E Y| ≤ MX * MY := by rw [abs_mul] exact mul_le_mul hEX hEY (abs_nonneg _) hMX calc |D.E (fun z => X z * Y z) - D.E X * D.E Y| ≤ |D.E (fun z => X z * Y z)| + |D.E X * D.E Y| := abs_sub _ _ _ ≤ MX * MY + MX * MY := by linarith _ = 2 * MX * MY := by ring -
Cov_zero_leftlemma — The covariance of the identically-zero random variable with anything is zero.hypothesesY :Ω → ℝconclusionD.Cov (fun _ => 0) Y = 0Proof (Lean source)
lemma Cov_zero_left (Y : Ω → ℝ) : D.Cov (fun _ => 0) Y = 0 := by rw [D.Cov_eq] have h1 : D.E (fun z => (0 : ℝ) * Y z) = 0 := by rw [D.E_congr (fun z => zero_mul (Y z)), D.E_const] have h2 : D.E (fun _ : Ω => (0 : ℝ)) = 0 := D.E_const 0 rw [h1, h2]; ring
IndepSummandsCLT 2 core · 0 supporting Product-design sums of independent bounded mean-zero summands satisfy a standard-normal limit. ★ prodDesign_clt
Independent-summands CLT for product designs
Product-design sums of independent bounded mean-zero summands satisfy a standard-normal limit.
The construction diagDepGraph supplies the dependency graph whose only edges are self-edges, with
independence coming from finite product designs. The theorem prodDesign_clt then specializes the
dependency-graph Stein CLT: uniformly bounded, mean-zero coordinate summands with vanishing
third-moment envelope and unit total design variance have standard-normal distributional limits
under the product design.
The diagonal dependency graph for the per-coordinate summands X n i = fun w => g n i (w i) under the product-design measure: each coordinate depends only on itself (G a b := a = b). The independence field is the product-measure block independence indepFun_prodDesign_apply_blocks, since distinct coordinate-index sets are disjoint.
Definition (Lean source)
Independent-summands CLT over product designs. Fix a family of coordinate designs D n i and real-valued per-coordinate summands g n i, one pair per stage n and coordinate i. Suppose there is a sequence of nonnegative bounds B n tending to zero, every summand g n i a is bounded in absolute value by B n, the number of coordinates at stage n times B n cubed tends to zero, each summand has mean zero under its own coordinate design, and the total sum ∑ᵢ g n i (w i) has design variance exactly one under the product design at every stage n. Then the design probability that the sum is at most any fixed threshold s converges, as n → ∞, to the standard normal cumulative distribution function Φ(s).
Formal statement
Proof (Lean source)
InProb 5 core · 6 supporting Finite-design convergence in probability tracks vanishing assignment-tail probabilities along a sequence of randomization designs. ★ tendstoInProb_of_var★ sub★ tendstoInProb_div_one
Convergence in probability for finite designs
Finite-design convergence in probability tracks vanishing assignment-tail probabilities along a sequence of randomization designs.
The predicate FiniteDesign.TendstoInProb states convergence of statistics X m to targets c m
using the design probabilities of absolute-deviation events. The theorem tendstoInProb_of_var
turns vanishing randomization variance into convergence to the design mean via Chebyshev's
inequality. The closure result TendstoInProb.sub handles differences, and
tendstoInProb_div_one is the Hájek/Slutsky ratio step for denominators converging in probability
to one.
Convergence in probability along a sequence of finite designs: X m converges in probability to the target c m if Pr(|X m − c m| ≥ ε) → 0 for every ε > 0.
Definition (Lean source)
Chebyshev consistency engine. Along a sequence of finite designs D, for statistics X, if the design variance of X m tends to zero as m → ∞, then X m converges in probability to its design mean E[X m].
Formal statement
Proof (Lean source)
Along a sequence of finite designs, if the statistics X m converge in probability to a m and the statistics Y m converge in probability to b m, then the difference X m − Y m converges in probability to a m − b m: convergence in probability is closed under differences.
Formal statement
Proof (Lean source)
Slutsky ratio step. Along a sequence of finite designs D, fix statistics X and Y. If X m converges in probability to a m, the denominator Y m converges in probability to 1, and the limit sequence a m is uniformly bounded by a constant M, then the ratio X m / Y m converges in probability to a m. (The realized normalizer tends to one, so dividing by it does not change the probability limit.)
Formal statement
Proof (Lean source)
Uniform tightness (bounded in probability). The statistics X m are uniformly tight if, for every tolerance η, there is a single threshold M past which the deviation probability Pr(M ≤ |X m|) is at most η for every index m. This is the O_p(1) counterpart of TendstoInProb, satisfied by a bounded (non-vanishing) factor of a delta-method remainder.
Definition (Lean source)
6 supporting declarations (lemmas, instances)
-
Pr_or_lelemma — Union bound for two events: Pr(P ∨ Q) ≤ Pr P + Pr Q.hypothesesconclusionD.Pr (fun z => P z ∨ Q z) ≤ D.Pr P + D.Pr QProof (Lean source)
lemma Pr_or_le {Ω' : Type*} [Fintype Ω'] (D : FiniteDesign Ω') (P Q : Ω' → Prop) [DecidablePred P] [DecidablePred Q] : D.Pr (fun z => P z ∨ Q z) ≤ D.Pr P + D.Pr Q := by unfold FiniteDesign.Pr FiniteDesign.E FiniteDesign.ind rw [← Finset.sum_add_distrib] apply Finset.sum_le_sum intro z _ rw [← mul_add] apply mul_le_mul_of_nonneg_left _ (D.p_nonneg z) by_cases hP : P z <;> by_cases hQ : Q z <;> simp [hP, hQ] -
addtheorem — Convergence in probability is closed under sums.hypothesesD :∀ m, FiniteDesign (Ω m)X Y :∀ mifΩ mthenℝa b :ℕ → ℝhX :TendstoInProb D X ahY :TendstoInProb D Y bconclusionTendstoInProb D (fun m z => X m z + Y m z) (fun m => a m + b m)Proof (Lean source)
theorem TendstoInProb.add {D : ∀ m, FiniteDesign (Ω m)} {X Y : ∀ m, Ω m → ℝ} {a b : ℕ → ℝ} (hX : TendstoInProb D X a) (hY : TendstoInProb D Y b) : TendstoInProb D (fun m z => X m z + Y m z) (fun m => a m + b m) := by intro ε hε have hε2 : (0 : ℝ) < ε / 2 := by linarith have hbound : ∀ m, (D m).Pr (fun z => ε ≤ |(X m z + Y m z) - (a m + b m)|) ≤ (D m).Pr (fun z => ε / 2 ≤ |X m z - a m|) + (D m).Pr (fun z => ε / 2 ≤ |Y m z - b m|) := by intro m have hmono : (D m).Pr (fun z => ε ≤ |(X m z + Y m z) - (a m + b m)|) ≤ (D m).Pr (fun z => (ε / 2 ≤ |X m z - a m|) ∨ (ε / 2 ≤ |Y m z - b m|)) := by apply (D m).Pr_mono intro z hz by_contra hcon push_neg at hcon obtain ⟨h1, h2⟩ := hcon have htri : |(X m z + Y m z) - (a m + b m)| ≤ |X m z - a m| + |Y m z - b m| := by have : (X m z + Y m z) - (a m + b m) = (X m z - a m) + (Y m z - b m) := by ring rw [this] exact abs_add_le _ _ linarith exact le_trans hmono (Pr_or_le (D m) _ _) have hupper : Tendsto (fun m => (D m).Pr (fun z => ε / 2 ≤ |X m z - a m|) + (D m).Pr (fun z => ε / 2 ≤ |Y m z - b m|)) atTop (𝓝 0) := by have := (hX (ε / 2) hε2).add (hY (ε / 2) hε2) simpa using this refine squeeze_zero (fun m => (D m).Pr_nonneg _) hbound hupper -
abstheorem — If X m → 0 in probability then |X m| → 0 in probability.hypothesesconclusionTendstoInProb D (fun m z => |X m z|) (fun _ => 0)Proof (Lean source)
theorem TendstoInProb.abs {D : ∀ m, FiniteDesign (Ω m)} {X : ∀ m, Ω m → ℝ} (h : TendstoInProb D X (fun _ => 0)) : TendstoInProb D (fun m z => |X m z|) (fun _ => 0) := by intro ε hε simpa only [sub_zero, abs_abs] using h ε hε -
boundedInProb_of_var_boundtheorem — An eventual variance bound together with an eventual mean bound makes a sequence bounded in probability: if the design variances Var(X m) are eventually at most V and the means E(X m) eventually lie within c of zero, then X is uniformly tight.hypothesesconclusionBoundedInProb D XProof (Lean source)
theorem boundedInProb_of_var_bound (D : ∀ m, FiniteDesign (Ω m)) (X : ∀ m, Ω m → ℝ) {V c : ℝ} (hV : ∀ᶠ m in atTop, (D m).Var (X m) ≤ V) (hc : ∀ᶠ m in atTop, |(D m).E (X m)| ≤ c) : BoundedInProb D X := by intro η hη obtain ⟨m0, hm0⟩ := hV.exists have hVnn : 0 ≤ V := le_trans ((D m0).Var_nonneg (X m0)) hm0 set r : ℝ := V / η + 1 with hrdef have hr_pos : 0 < r := by rw [hrdef]; positivity have hr2_pos : 0 < r ^ 2 := pow_pos hr_pos 2 refine ⟨c + r, ?_⟩ filter_upwards [hV, hc] with m hVm hcm have hsub : (D m).Pr (fun z => c + r ≤ |X m z|) ≤ (D m).Pr (fun z => r ≤ |X m z - (D m).E (X m)|) := by apply (D m).Pr_mono intro z hz have h1 : |X m z| - |(D m).E (X m)| ≤ |X m z - (D m).E (X m)| := abs_sub_abs_le_abs_sub _ _ linarith refine le_trans hsub (le_trans ((D m).chebyshev (X m) hr_pos) ?_) rw [div_le_iff₀ hr2_pos] have hkey : η * r = V + η := by rw [hrdef]; field_simp have hexp : η * r ^ 2 = (V + η) * r := by rw [pow_two, ← mul_assoc, hkey] rw [hexp] have hr1 : (1 : ℝ) ≤ r := by rw [hrdef]; have : (0 : ℝ) ≤ V / η := by positivity linarith have hVle : V ≤ (V + η) * r := by calc V = V * 1 := (mul_one V).symm _ ≤ (V + η) * r := by apply mul_le_mul (by linarith) hr1 (by norm_num) (by linarith) linarith [hVm] -
const_multheorem — Scaling a convergent sequence by a constant scales its probability limit: if X m → a m in probability then c · X m → c · a m in probability.hypothesesconclusionTendstoInProb D (fun m z => c * X m z) (fun m => c * a m)Proof (Lean source)
theorem TendstoInProb.const_mul {D : ∀ m, FiniteDesign (Ω m)} {X : ∀ m, Ω m → ℝ} {a : ℕ → ℝ} (c : ℝ) (h : TendstoInProb D X a) : TendstoInProb D (fun m z => c * X m z) (fun m => c * a m) := by intro ε hε have hc1 : 0 < |c| + 1 := by positivity have hεc : 0 < ε / (|c| + 1) := by positivity have hsub : ∀ m, (D m).Pr (fun z => ε ≤ |c * X m z - c * a m|) ≤ (D m).Pr (fun z => ε / (|c| + 1) ≤ |X m z - a m|) := by intro m apply (D m).Pr_mono intro z hz rw [← mul_sub, abs_mul] at hz rw [div_le_iff₀ hc1] nlinarith [hz, abs_nonneg (X m z), abs_nonneg c] refine squeeze_zero (fun m => (D m).Pr_nonneg _) hsub ?_ simpa using h (ε / (|c| + 1)) hεc -
mul_boundedInProbtheorem — Product-tightness (o_p × O_p = o_p). If U m converges to zero in probability and V m is uniformly tight (bounded in probability), then the product U m · V m converges to zero in probability. This is the engine that turns a delta-method remainder — a vanishing factor times a bounded factor — into an o_p(1) term.hypothesesD :∀ m, FiniteDesign (Ω m)U V :∀ mifΩ mthenℝhU :TendstoInProb D U (fun _ => 0)hV :BoundedInProb D VconclusionTendstoInProb D (fun m z => U m z * V m z) (fun _ => 0)Proof (Lean source)
theorem TendstoInProb.mul_boundedInProb {D : ∀ m, FiniteDesign (Ω m)} {U V : ∀ m, Ω m → ℝ} (hU : TendstoInProb D U (fun _ => 0)) (hV : BoundedInProb D V) : TendstoInProb D (fun m z => U m z * V m z) (fun _ => 0) := by intro ε hε simp only [sub_zero] apply tendsto_order.2 constructor · intro a ha filter_upwards [] with m exact lt_of_lt_of_le ha ((D m).Pr_nonneg _) · intro a ha have ha2 : (0 : ℝ) < a / 2 := by linarith obtain ⟨M, hM⟩ := hV (a / 2) ha2 set M' : ℝ := |M| + 1 with hM'def have hM' : 0 < M' := by rw [hM'def] positivity have hMle : M ≤ M' := by rw [hM'def] linarith [le_abs_self M] have hMbound : ∀ᶠ m in atTop, (D m).Pr (fun z => M' ≤ |V m z|) ≤ a / 2 := by filter_upwards [hM] with m hmm refine le_trans ?_ hmm apply (D m).Pr_mono intro z hz exact le_trans hMle hz have hbound : ∀ m, (D m).Pr (fun z => ε ≤ |U m z * V m z|) ≤ (D m).Pr (fun z => M' ≤ |V m z|) + (D m).Pr (fun z => ε / M' ≤ |U m z|) := by intro m refine le_trans ?_ (Pr_or_le (D m) _ _) apply (D m).Pr_mono intro z hz by_cases hVlarge : M' ≤ |V m z| · exact inl hVlarge · right push_neg at hVlarge rw [div_le_iff₀ hM'] rw [abs_mul] at hz have hUpos : 0 < |U m z| := by by_contra hUpos have hUzero : |U m z| = 0 := le_antisymm (le_of_not_gt hUpos) (abs_nonneg _) rw [hUzero, zero_mul] at hz linarith exact le_of_lt (lt_of_le_of_lt hz (mul_lt_mul_of_pos_left hVlarge hUpos)) have hU' : Tendsto (fun m => (D m).Pr (fun z => ε / M' ≤ |U m z|)) atTop (𝓝 0) := by have hεM' : (0 : ℝ) < ε / M' := by positivity simpa using hU (ε / M') hεM' have htail : ∀ᶠ m in atTop, (D m).Pr (fun z => ε / M' ≤ |U m z|) < a / 2 := (tendsto_order.mp hU').2 (a / 2) ha2 filter_upwards [htail, hMbound] with m hm hmb calc (D m).Pr (fun z => ε ≤ |U m z * V m z|) ≤ (D m).Pr (fun z => M' ≤ |V m z|) + (D m).Pr (fun z => ε / M' ≤ |U m z|) := hbound m _ < a := by linarith [hmb]
LocalDependenceVariance 2 core · 0 supporting This file provides BlockDegreeLE, the condition that no unit lies in more than d of the dependence blocks, and bernoulliDesign_E_sum_sq_le_blockDegree_mul_sum_sq, the resulting bound E[(∑ᵢ Fᵢ)²] ≤ d · ∑ᵢ E[Fᵢ²] for mean- ★ bernoulliDesign_E_sum_sq_le_blockDegree_mul_sum_sq
Local-dependence variance bound on a Bernoulli design
This file provides BlockDegreeLE, the condition that no unit lies in more than d of the
dependence blocks, and bernoulliDesign_E_sum_sq_le_blockDegree_mul_sum_sq, the resulting bound
E[(∑ᵢ Fᵢ)²] ≤ d · ∑ᵢ E[Fᵢ²] for mean-zero, block-dependent summands.
A family of dependence blocks has degree at most d if no single unit's treatment is read by more than d of the blocks. When the blocks are the in-neighbourhoods of a dependency graph this is the bound on out-degree.
Definition (Lean source)
Local-dependence variance bound. Under a Bernoulli design in which every unit's treatment probability lies strictly between 0 and 1, suppose each unit i contributes a term F i — attached to a dependence block N i — such that no unit's treatment is read by more than d of these blocks, every term has mean zero under the Bernoulli design, and each term F i depends only on the treatments of its own block N i. Then the second moment of the total ∑ᵢ F i is at most d times the total of the individual second moments, d · ∑ᵢ E[(F i)²]. The bound is scale free: it needs no uniform bound on the terms, no explicit decorrelation assumption, and no dependence on the population size.
Formal statement
Proof (Lean source)
MeasureBridge 1 core · 7 supporting For a finite design D, FiniteDesign.E, FiniteDesign.Var, and FiniteDesign.Pr are the design expectation, variance, and event probability. ★ abs_Cov_le
Descent bundle: design operations as measure-theoretic operations
For a finite design D, FiniteDesign.E, FiniteDesign.Var, and FiniteDesign.Pr are the design
expectation, variance, and event probability. This file exposes them as the integral, variance, and
event measure of D.toMeasure, and proves that every statistic is Lᵖ under D.toMeasure
(memLp_toMeasure) and strongly measurable (aestronglyMeasurable_toMeasure). These are the
obligations that gate the reuse of measure-theoretic inference results, so discharging them once
lets those results transfer to the design layer directly.
Cauchy–Schwarz for the design covariance. In any finite design, the absolute covariance of two statistics X and Y is at most the product of their design standard deviations, |Cov(X,Y)| ≤ √(Var X) · √(Var Y).
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
aestronglyMeasurable_toMeasurelemma — On a finite assignment space every statistic is strongly measurable, because singletons — hence all sets — are measurable.Proof (Lean source)
lemma aestronglyMeasurable_toMeasure {β : Type*} [MeasurableSpace β] [TopologicalSpace β] [PseudoMetrizableSpace β] [SecondCountableTopology β] [OpensMeasurableSpace β] (g : Ω → β) : AEStronglyMeasurable g D.toMeasure := (measurable_of_finite g).aestronglyMeasurable -
aemeasurable_toMeasurelemma — On a finite assignment space every statistic with a measurable codomain is a.e.-measurable under the design measure.Proof (Lean source)
lemma aemeasurable_toMeasure {β : Type*} [MeasurableSpace β] (g : Ω → β) : AEMeasurable g D.toMeasure := (measurable_of_finite g).aemeasurable -
memLp_toMeasurelemma — Every normed-additive statistic with a suitable measurable second-countable codomain on a finite assignment space is Lᵖ under the design measure: the space is finite so every statistic is bounded, and the design measure is a probability measure, so every power is integrable.Proof (Lean source)
lemma memLp_toMeasure {β : Type*} [NormedAddCommGroup β] [MeasurableSpace β] [SecondCountableTopology β] [OpensMeasurableSpace β] (g : Ω → β) (p : ℝ≥0∞) : MemLp g p D.toMeasure := by refine MemLp.of_bound (D.aestronglyMeasurable_toMeasure g) (∑ z, ‖g z‖) ?_ filter_upwards with x exact Finset.single_le_sum (f := fun z => ‖g z‖) (fun z _ => norm_nonneg _) (Finset.mem_univ x) -
E_eq_integrallemma — Reverse rewrite. The design expectation is the integral against the design measure.hypothesesg :Ω → ℝconclusionD.E g = ∫ x, g x ∂D.toMeasureProof (Lean source)
lemma E_eq_integral (g : Ω → ℝ) : D.E g = ∫ x, g x ∂D.toMeasure := (D.integral_toMeasure g).symm -
Var_eq_variancelemma — Reverse rewrite. The design variance is the measure-theoretic variance under the design measure.Proof (Lean source)
lemma Var_eq_variance (g : Ω → ℝ) : D.Var g = variance g D.toMeasure := (D.variance_toMeasure g).symm -
Pr_eq_measureReallemma — Reverse rewrite. The design probability of an event is the real-valued measure of the event under the design measure.Proof (Lean source)
lemma Pr_eq_measureReal (A : Ω → Prop) [DecidablePred A] : D.Pr A = D.toMeasure.real {z | A z} := (D.toMeasure_real_setOf A).symm -
Cov_eq_covariancelemma — Reverse rewrite. The design covariance is the measure-theoretic covariance under the design measure.Proof (Lean source)
lemma Cov_eq_covariance (X Y : Ω → ℝ) : D.Cov X Y = covariance X Y D.toMeasure := by rw [covariance, D.integral_toMeasure X, D.integral_toMeasure Y, D.integral_toMeasure (fun z => (X z - D.E X) * (Y z - D.E Y))] rfl
PotentialOutcome 3 core · 3 supporting Exposure-indexed potential outcomes factor observed outcomes through a finite assignment's exposure. ★ Yobs_eq_sum
Potential outcomes under exposure mappings
Exposure-indexed potential outcomes factor observed outcomes through a finite assignment's exposure.
ProperlySpecified states that randomization potential outcomes factor through the exposure
mapping, while Yobs evaluates the exposure-indexed potential outcome at the realized exposure.
The lemmas Yobs_eq_sum, expoInd_mul_Yobs, expoInd_mul_Yobs_sq, and
expoInd₂_mul_Yobs provide the consistency and on-event substitution identities used by
Horvitz-Thompson and variance calculations.
A properly specified exposure mapping: the randomization potential outcome yr factors through the exposure via exposure-indexed potential outcomes y.
Definition (Lean source)
Observed outcome of unit i under assignment z: y i (expo i z).
Condition 2 (consistency). The observed outcome of unit i under assignment z equals the sum, over every exposure level, of the exposure indicator times the exposure-indexed potential outcome.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
expoInd_mul_Yobslemma — On the event expo i = d, the observed outcome agrees with the potential outcome y i d; hence 1(expo i = d)·Yobs i = 1(expo i = d)·y i d.hypothesesy :ι → Δ → ℝf :Ω → Θ → Δθ :ι → Θi :ιd :Δz :ΩProof (Lean source)
lemma expoInd_mul_Yobs (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (i : ι) (d : Δ) (z : Ω) : expoInd f θ i d z * Yobs y f θ i z = expoInd f θ i d z * y i d := by unfold expoInd FiniteDesign.ind Yobs by_cases h : expo f θ i z = d <;> simp [h] -
expoInd_mul_Yobs_sqlemma — Squared on-event substitution: 1(expo i = d)·(Yobs i)² = 1(expo i = d)·(y i d)².hypothesesy :ι → Δ → ℝf :Ω → Θ → Δθ :ι → Θi :ιd :Δz :ΩProof (Lean source)
lemma expoInd_mul_Yobs_sq (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (i : ι) (d : Δ) (z : Ω) : expoInd f θ i d z * (Yobs y f θ i z) ^ 2 = expoInd f θ i d z * (y i d) ^ 2 := by unfold expoInd FiniteDesign.ind Yobs by_cases h : expo f θ i z = d <;> simp [h] -
expoInd₂_mul_Yobslemma — On the event expo i = di, multiplying the observed outcome for unit i by any real quantity leaves it valid to replace that outcome by potential outcome y i di.hypothesesy :ι → Δ → ℝf :Ω → Θ → Δθ :ι → Θi :ιdi :Δq :Ω → ℝz :ΩProof (Lean source)
lemma expoInd₂_mul_Yobs (y : ι → Δ → ℝ) (f : Ω → Θ → Δ) (θ : ι → Θ) (i : ι) (di : Δ) (q : Ω → ℝ) (z : Ω) : expoInd f θ i di z * q z * Yobs y f θ i z = expoInd f θ i di z * q z * y i di := by unfold expoInd FiniteDesign.ind Yobs by_cases h : expo f θ i z = di <;> simp [h]
ProductBlock 3 core · 1 supporting Functions of disjoint coordinate blocks factor under a finite product design. ★ E_prod_block_mul★ Cov_prod_block_zero★ Cov_prod_disjoint_zero
Disjoint-block independence for product designs
Functions of disjoint coordinate blocks factor under a finite product design.
The theorem FiniteDesign.E_prod_block_mul factors the expectation of f * g when f depends
only on coordinates in a block A and g depends only on the complement. The covariance
corollaries FiniteDesign.Cov_prod_block_zero and FiniteDesign.Cov_prod_disjoint_zero package
that independence for complement blocks and for arbitrary disjoint blocks.
Disjoint-block factorization of expectation. For a family of independent coordinate designs D and real-valued functions f and g on the joint assignment space, suppose f is invariant under any change to the coordinates outside a block A — it depends only on the coordinates in A, and g depends only on the coordinates outside A. Then under the product design, the expectation of the product f·g factors as E[f·g] = E[f]·E[g]. The general (block-level) form of E_prod_apply₂.
Formal statement
Proof (Lean source)
Disjoint-block covariance vanishing (complement form). For a family of independent coordinate designs D and real-valued functions f and g, suppose f depends only on the coordinates in a block A and g depends only on the coordinates outside A. Then their covariance under the product design is zero.
Formal statement
Proof (Lean source)
Disjoint-block covariance vanishing (two-block form). For a family of independent coordinate designs D and real-valued functions f and g, suppose the index sets S and T are disjoint, f depends only on the coordinates in S, and g depends only on the coordinates in T. Then their covariance under the product design is zero.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
nonempty_of_designtheorem — Every coordinate type carrying a finite design is nonempty.Proof (Lean source)
theorem nonempty_of_design (D : ∀ i, FiniteDesign (α i)) : ∀ i, Nonempty (α i) := by intro i by_contra h rw [not_nonempty_iff] at h have := (D i).p_sum rw [Finset.univ_eq_empty, Finset.sum_empty] at this exact one_ne_zero this.symm
ProductMeasure 2 core · 5 supporting The measure induced by a finite product design is Mathlib's product measure. ★ prodDesign_toMeasure_eq_pi★ indepFun_prodDesign_blocks
Product-design measures
The measure induced by a finite product design is Mathlib's product measure.
prodDesign_toMeasure_eq_pi identifies (prodDesign D).toMeasure with
Measure.pi (fun i => (D i).toMeasure), using FiniteDesign.toMeasure_singleton to compare
singleton masses. The independence results iIndepFun_prodDesign_eval,
indepFun_prodDesign_eval, indepFun_prodDesign_blocks, and
indepFun_prodDesign_apply_blocks then expose Mathlib's product-measure independence for
coordinate projections and disjoint coordinate blocks.
The product design IS Mathlib's product measure. For a family of independent coordinate designs D, the probability measure induced by the product design prodDesign D coincides exactly with Mathlib's product measure of the coordinate design measures. Both are finite measures on the Fintype ∀ i, α i, so they agree iff they agree on every singleton {w}; on a singleton both sides evaluate to ∏ i, (D i).p (w i).
Formal statement
Proof (Lean source)
Disjoint-block independence. For a family of independent coordinate designs D, suppose the finite index sets A and B are disjoint. Then the tuple of coordinates indexed by A is probabilistically independent of the tuple of coordinates indexed by B, under the measure induced by the product design. This is the form a diagonal dependency graph G a b := a = b consumes.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
toMeasure_singletonlemma — The design measure of a singleton equals that singleton's design probability: (D i).toMeasure {a} = (D i).p a. (The dirac sum collapses to the single term z = a.)hypothesesconclusionD.toMeasure {a} = ofReal (D.p a)Proof (Lean source)
lemma toMeasure_singleton {β : Type*} [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] (D : FiniteDesign β) (a : β) : D.toMeasure {a} = ofReal (D.p a) := by rw [toMeasure, Measure.finset_sum_apply] rw [Finset.sum_eq_single a] · rw [Measure.smul_apply, smul_eq_mul, Measure.dirac_apply' a (measurableSet_singleton a)] simp · intro z _ hz rw [Measure.smul_apply, smul_eq_mul, Measure.dirac_apply' z (measurableSet_singleton a), Set.indicator_of_notMem (by simpa using hz)] simp · intro h; exact absurd (Finset.mem_univ a) h -
iIndepFun_prodDesign_evallemma — Coordinate evaluations are mutually independent under the product-design measure: viewing fun (i) (w) => w i as the family of coordinate projections, this family is iIndepFun under (prodDesign D).toMeasure. (The push-forward of iIndepFun_pi along prodDesign_toMeasure_eq_pi.)hypothesesD :∀ i, FiniteDesign (α i)conclusioniIndepFun (fun (i : ι) (w : ∀ j, α j) => w i) (prodDesign D).toMeasureProof (Lean source)
lemma iIndepFun_prodDesign_eval (D : ∀ i, FiniteDesign (α i)) : iIndepFun (fun (i : ι) (w : ∀ j, α j) => w i) (prodDesign D).toMeasure := by rw [prodDesign_toMeasure_eq_pi] exact iIndepFun_pi (X := fun _ => id) (fun i => aemeasurable_id) -
indepFun_prodDesign_evaltheorem — For i ≠ j, the two coordinate evaluations w ↦ w i and w ↦ w j are independent under the product-design measure.hypothesesconclusionProof (Lean source)
theorem indepFun_prodDesign_eval (D : ∀ i, FiniteDesign (α i)) {i j : ι} (hij : i ≠ j) : IndepFun (fun w : ∀ k, α k => w i) (fun w => w j) (prodDesign D).toMeasure := (iIndepFun_prodDesign_eval D).indepFun hij -
indepFun_prodDesign_apply_blockstheorem — Functions of disjoint coordinate blocks are independent. Applying separate measurable function families to the coordinates in two disjoint blocks preserves their independence, even when the two blocks have different coordinatewise output spaces.hypothesesD :∀ i, FiniteDesign (α i)β γ :g :∀ iifα ithenβ ih :∀ iifα ithenγ ihg :∀ i, Measurable (g i)hh :∀ i, Measurable (h i)A B :Finset ιhAB :Disjoint A BconclusionIndepFun (fun (w : ∀ k, α k) (k : A) => g k (w k)) (fun w (k : B) => h k (w k)) (prodDesign D).toMeasureProof (Lean source)
theorem indepFun_prodDesign_apply_blocks (D : ∀ i, FiniteDesign (α i)) {β γ : ι → Type*} [∀ i, MeasurableSpace (β i)] [∀ i, MeasurableSpace (γ i)] {g : ∀ i, α i → β i} {h : ∀ i, α i → γ i} (hg : ∀ i, Measurable (g i)) (hh : ∀ i, Measurable (h i)) {A B : Finset ι} (hAB : Disjoint A B) : IndepFun (fun (w : ∀ k, α k) (k : A) => g k (w k)) (fun w (k : B) => h k (w k)) (prodDesign D).toMeasure := (indepFun_prodDesign_blocks D hAB).comp (φ := fun (v : ∀ k : A, α k) (k : A) => g k (v k)) (ψ := fun (v : ∀ k : B, α k) (k : B) => h k (v k)) (by fun_prop) (by fun_prop) -
indepFun_prodDesign_of_depends_on_disjoint_blockstheorem — General functions of disjoint coordinate blocks are independent. The strict generalization of indepFun_prodDesign_apply_blocks from coordinatewise-separable maps (g k (w k))_k to *arbitrary* measurable functions that each depend only on a block: if F is unchanged by any assignment that agrees on S, and G is unchanged by any assignment that agrees on the disjoint set T, then F and G are independent under the product-design measure. This is the hypothesis a dependency-graph construction actually consumes, where each summand depends jointly (not coordinatewise) on a neighbourhood block.hypothesesβ γ :D :∀ i, FiniteDesign (α i)S T :Finset ιhST :Disjoint S TF :(∀ i, α i) → βG :(∀ i, α i) → γhF :∀ w w' : ∀ iifα i, (∀ i ∈ S, w i = w' i)thenF w = F w'hG :∀ w w' : ∀ iifα i, (∀ i ∈ T, w i = w' i)thenG w = G w'conclusionProof (Lean source)
theorem indepFun_prodDesign_of_depends_on_disjoint_blocks {β γ : Type*} [MeasurableSpace β] [MeasurableSpace γ] (D : ∀ i, FiniteDesign (α i)) {S T : Finset ι} (hST : Disjoint S T) (F : (∀ i, α i) → β) (G : (∀ i, α i) → γ) (hF : ∀ w w' : ∀ i, α i, (∀ i ∈ S, w i = w' i) → F w = F w') (hG : ∀ w w' : ∀ i, α i, (∀ i ∈ T, w i = w' i) → G w = G w') : IndepFun F G (prodDesign D).toMeasure := by classical have hne : ∀ i, Nonempty (α i) := by intro i by_contra h rw [not_nonempty_iff] at h have := (D i).p_sum rw [Finset.univ_eq_empty, Finset.sum_empty] at this exact one_ne_zero this.symm let x₀ : ∀ i, α i := fun i => (hne i).some let F₀ : (∀ k : (S : Finset ι), α k) → β := fun a => F (fun i => if h : i ∈ S then a ⟨i, h⟩ else x₀ i) let G₀ : (∀ k : (T : Finset ι), α k) → γ := fun b => G (fun i => if h : i ∈ T then b ⟨i, h⟩ else x₀ i) have hF₀ : ∀ w, F w = F₀ (fun k : (S : Finset ι) => w k) := by intro w refine hF _ _ (fun i hi => ?_) simp [hi] have hG₀ : ∀ w, G w = G₀ (fun k : (T : Finset ι) => w k) := by intro w refine hG _ _ (fun i hi => ?_) simp [hi] have hblk := (indepFun_prodDesign_blocks D hST).comp (φ := F₀) (ψ := G₀) (measurable_of_finite F₀) (measurable_of_finite G₀) exact hblk.congr (Filter.Eventually.of_forall fun w => (hF₀ w).symm) (Filter.Eventually.of_forall fun w => (hG₀ w).symm)
ProductReindex 1 core · 0 supporting Permuting coordinate labels only relabels probabilities under a product design. ★ prodDesign_Pr_reindex
Reindexing product designs
Permuting coordinate labels only relabels probabilities under a product design.
The theorem FiniteDesign.prodDesign_Pr_reindex is a finite-sum reindexing identity: for a
coordinate permutation sigma, the probability of a permuted predicate under prodDesign D
equals the probability of the original predicate under the correspondingly permuted product
design. It is used to express selection symmetry in identical-group two-stage arguments without
invoking measure theory.
Relabeling a product design by a coordinate permutation. For a family of designs D over a common coordinate space W, indexed by ι, and a permutation σ : ι ≃ ι, the probability under prodDesign D of the predicate w ↦ P (w ∘ σ) equals the probability under the permuted product prodDesign (D ∘ σ) of P.
Formal statement
Proof (Lean source)
ProductVariance 1 core · 3 supporting Distinct coordinates of a finite product design are uncorrelated. ★ Var_prod_linear_comb
Product-design variance identities
Distinct coordinates of a finite product design are uncorrelated.
FiniteDesign.E_prod_apply₂ factors expectations of products of statistics on two distinct
coordinates, yielding FiniteDesign.Var_prod_apply for one-coordinate variances and
FiniteDesign.Cov_prod_apply_of_ne for zero cross-coordinate covariance. The payload
FiniteDesign.Var_prod_linear_comb states that the variance of a linear combination of
single-coordinate statistics is the sum of squared coefficients times the marginal variances.
The payload. Under the product design formed from a family of per-coordinate finite designs, the variance of a linear combination ∑ᵢ cᵢ·gᵢ(wᵢ) of single-coordinate functions gᵢ, with coefficients c, equals the sum over coordinates of the squared coefficient times the coordinate's own variance — cross-coordinate covariances vanish.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
E_prod_apply₂lemma — Two-coordinate factorization: under the product design, the expectation of a product of a function of one coordinate and a function of a distinct coordinate factors into the product of the two marginal expectations.hypothesesconclusion(prodDesign D).E (fun w => g (w i) * hfun (w j)) = (D i).E g * (D j).E hfunProof (Lean source)
lemma E_prod_apply₂ (D : ∀ i, FiniteDesign (α i)) {i j : ι} (h : i ≠ j) (g : α i → ℝ) (hfun : α j → ℝ) : (prodDesign D).E (fun w => g (w i) * hfun (w j)) = (D i).E g * (D j).E hfun := by rw [E_prod_block_mul D {i} (fun w => g (w i)) (fun w => hfun (w j))] · rw [E_prod_apply D i g, E_prod_apply D j hfun] · intro w w' hw exact congrArg g (hw i (by simp)) · intro w w' hw exact congrArg hfun (hw j (by simpa using h.symm)) -
Var_prod_applylemma — Single-coordinate variance: under the product design, the variance of a function of one coordinate equals the variance of that function under the coordinate's own design.hypothesesconclusionProof (Lean source)
lemma Var_prod_apply (D : ∀ i, FiniteDesign (α i)) (j : ι) (g : α j → ℝ) : (prodDesign D).Var (fun w => g (w j)) = (D j).Var g := by rw [Var_eq, Var_eq] congr 1 · -- E[(g (w j))^2] = (D j).E (fun a => g a ^ 2) have : (fun w : ∀ i, α i => g (w j) ^ 2) = (fun w => (fun a => g a ^ 2) (w j)) := rfl rw [this, E_prod_apply D j (fun a => g a ^ 2)] · -- (prodDesign D).E (fun w => g (w j)) = (D j).E g rw [E_prod_apply D j g] -
Cov_prod_apply_of_nelemma — Cross-coordinate independence: under the product design, functions of two distinct coordinates have zero covariance.hypothesesconclusion(prodDesign D).Cov (fun w => g (w i)) (fun w => hfun (w j)) = 0Proof (Lean source)
lemma Cov_prod_apply_of_ne (D : ∀ i, FiniteDesign (α i)) {i j : ι} (h : i ≠ j) (g : α i → ℝ) (hfun : α j → ℝ) : (prodDesign D).Cov (fun w => g (w i)) (fun w => hfun (w j)) = 0 := by rw [Cov_eq] rw [show (fun w : ∀ i, α i => g (w i) * hfun (w j)) = (fun w => g (w i) * hfun (w j)) from rfl, E_prod_apply₂ D h g hfun, E_prod_apply D i g, E_prod_apply D j hfun] ring
RatioLinearization 1 core · 3 supporting Exact design-mean identities for mean-normalized (Horvitz–Thompson / Hájek) ratio statistics and their products, computed directly from FiniteDesign.E. ★ E_lin_expand
Finite-sample delta-method identities for the design-based layer
Exact design-mean identities for mean-normalized (Horvitz–Thompson / Hájek) ratio statistics
and their products, computed directly from FiniteDesign.E.
These are the finite-design counterpart of the measure-theoretic ratio delta method
(Causalean.Stat's deltaMethod_ratio): rather than a limiting distributional statement, they
give the exact finite-n linearization kernel of a ratio estimator, so a design-based variance
computation never has to leave the FiniteDesign world.
* E_centered_ratio — a plug-in ratio X / E[X] is exactly centered.
* E_centered_ratio_mul — the exact covariance of two normalized ratios; the linearization
kernel for any ratio / Hájek variance.
* E_lin_expand — distributes the design mean over a product of two two-term linear forms, the
bilinear bookkeeping step for a two-arm linearized variance.
* ratio_remainder_capped_bound — the capped second-order remainder of a single scaled ratio
estimator, the per-arm building block of a ratio/Hájek CLT's asymptotic-linearity argument.
Bilinear expansion of a design mean. In a finite design, suppose the mean of A·C equals AA, the mean of A·F equals AB, the mean of B·C equals BA, and the mean of B·F equals BB — the four pairwise cross-moments of the two-term linear forms (A·ai − B·bi) and (C·aj − F·bj). Then the mean of the product (A·ai − B·bi)(C·aj − F·bj) equals AA·ai·aj − AB·ai·bj − BA·bi·aj + BB·bi·bj. This is the generic bookkeeping step assembling a two-arm (e.g. treated/control) linearized variance from its component moments.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
ratio_remainder_capped_boundlemma — Capped ratio-remainder bound. Consider a ratio estimator A / D of a target μ, scaled by √n (here sn with sn² = n), and let G = A − μ·D be the centered numerator. The scaled second-order remainder √n·(A/D − μ) − √n⁻¹·G equals √n⁻¹·G·(n/D − 1), and on the event where the denominator is at least half its target (equivalently n/D ≤ 2) it is bounded by 2·|√n⁻¹·G|·|n⁻¹·D − 1|. This is the per-arm remainder control a design-based ratio / Hájek CLT uses to reduce the studentized estimator to its linear score.hypothesesn sn A D μ G :ℝhn :0 < nhsn_sq :sn ^ 2 = nhD :0 < Dhcap :n / D ≤ 2hG :G = A - μ * Dconclusion|sn * (A / D - μ) - sn⁻¹ * G| ≤ 2 * |sn⁻¹ * G| * |n⁻¹ * D - 1|Proof (Lean source)
lemma ratio_remainder_capped_bound {n sn A D μ G : ℝ} (hn : 0 < n) (hsn_sq : sn ^ 2 = n) (hD : 0 < D) (hcap : n / D ≤ 2) (hG : G = A - μ * D) : |sn * (A / D - μ) - sn⁻¹ * G| ≤ 2 * |sn⁻¹ * G| * |n⁻¹ * D - 1| := by have hsn0 : sn ≠ 0 := by intro h rw [h, pow_two, mul_zero] at hsn_sq exact absurd hsn_sq.symm (ne_of_gt hn) have hD0 : D ≠ 0 := ne_of_gt hD have hrem : sn * (A / D - μ) - sn⁻¹ * G = sn⁻¹ * G * (n / D - 1) := by have hquot : A / D - μ = G / D := by rw [hG]; field_simp rw [hquot] field_simp rw [hsn_sq] have hbound : |sn⁻¹ * G * (n / D - 1)| ≤ 2 * |sn⁻¹ * G| * |n⁻¹ * D - 1| := by have hid : n / D - 1 = -((n / D) * (n⁻¹ * D - 1)) := by field_simp; ring have hnonneg : 0 ≤ n / D := le_of_lt (div_pos hn hD) have hratio : |n / D - 1| ≤ 2 * |n⁻¹ * D - 1| := by rw [hid, abs_neg, abs_mul, abs_of_nonneg hnonneg] exact mul_le_mul_of_nonneg_right hcap (abs_nonneg _) rw [abs_mul] calc |sn⁻¹ * G| * |n / D - 1| ≤ |sn⁻¹ * G| * (2 * |n⁻¹ * D - 1|) := mul_le_mul_of_nonneg_left hratio (abs_nonneg _) _ = 2 * |sn⁻¹ * G| * |n⁻¹ * D - 1| := by ring rw [hrem] exact hbound -
E_centered_ratiolemma — Centering of a plug-in ratio. In a finite design, the mean-normalized ratio X / E[X] − 1 has design mean zero whenever the mean E[X] is nonzero — the first-order (linearization) fact that a ratio statistic is exactly centered at its plug-in point.hypothesesX :Ω → ℝa :ℝha :a ≠ 0hEX :D.E X = aconclusionD.E (fun z => X z / a - 1) = 0Proof (Lean source)
lemma E_centered_ratio (X : Ω → ℝ) (a : ℝ) (ha : a ≠ 0) (hEX : D.E X = a) : D.E (fun z => X z / a - 1) = 0 := by have hpoint : (fun z => X z / a - 1) = (fun z => (1 / a) * X z - 1) := by funext z ring rw [D.E_congr (by intro z; exact congrFun hpoint z)] rw [D.E_sub, D.E_const_mul, D.E_const, hEX] field_simp [ha] ring -
E_centered_ratio_mullemma — Covariance of two normalized ratios (the ratio linearization kernel). In a finite design, the mean of the product of two mean-normalized ratios (X/E[X] − 1)(Y/E[Y] − 1) equals E[XY] / (E[X]·E[Y]) − 1. This is the exact second cross-moment at the heart of every Horvitz–Thompson / Hájek ratio-variance linearization.hypothesesX Y :Ω → ℝa b c :ℝha :a ≠ 0hb :b ≠ 0hEX :D.E X = ahEY :D.E Y = bhEXY :D.E (fun z => X z * Y z) = cconclusionD.E (fun z => (X z / a - 1) * (Y z / b - 1)) = c / (a * b) - 1Proof (Lean source)
lemma E_centered_ratio_mul (X Y : Ω → ℝ) (a b c : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) (hEX : D.E X = a) (hEY : D.E Y = b) (hEXY : D.E (fun z => X z * Y z) = c) : D.E (fun z => (X z / a - 1) * (Y z / b - 1)) = c / (a * b) - 1 := by have hpoint : (fun z => (X z / a - 1) * (Y z / b - 1)) = (fun z => ((1 / (a * b)) * (X z * Y z) - (1 / a) * X z) - (1 / b) * Y z + 1) := by funext z field_simp [ha, hb] ring rw [D.E_congr (by intro z; exact congrFun hpoint z)] rw [D.E_add, D.E_sub, D.E_sub, D.E_const_mul, D.E_const_mul, D.E_const_mul, D.E_const] rw [hEX, hEY, hEXY] field_simp [ha, hb] ring
Slutsky 1 core · 0 supporting The finite-design counterpart of the classical converging-together / Slutsky theorem, stated directly on FiniteDesign.Pr at the level of pointwise CDF convergence. ★ finiteDesign_cdf_converging_together
Design-based converging-together (CDF-level Slutsky)
The finite-design counterpart of the classical converging-together / Slutsky theorem, stated
directly on FiniteDesign.Pr at the level of pointwise CDF convergence. If Sₙ and Tₙ are
asymptotically indistinguishable in probability and the CDFs of Tₙ converge to a continuous limit
CDF Φ, then the CDFs of Sₙ converge to the same Φ. It transfers a limiting CDF across an
in-probability-negligible perturbation — the exact step a studentized design-based estimator needs
to pass from an oracle statistic to its feasible (plug-in standard error) version — without leaving
the finite-design layer for the measure-theoretic weak-convergence API.
Finite-design CDF converging-together. Along a sequence of finite designs on two sequences of real-valued statistics Sₙ and Tₙ, suppose Sₙ is asymptotically indistinguishable from Tₙ in probability: for every η > 0, Pr(η ≤ |Sₙ − Tₙ|) → 0, the CDFs of Tₙ converge pointwise to a limit function Φ, and Φ is continuous. Then the CDFs of Sₙ converge pointwise to the same Φ.
Formal statement
Proof (Lean source)
WaldCoverage 1 core · 0 supporting A paper-agnostic asymptotic-coverage transfer for two-sided Wald intervals built from a *deterministic conservative* standard error. ★ conservative_wald_liminf_of_studentized_cdf
Design-based conservative Wald-interval coverage
A paper-agnostic asymptotic-coverage transfer for two-sided Wald intervals built from a
deterministic conservative standard error. It is stated over abstract per-stage sequences — a
design D n, an estimator est n, a target θ n, the true variance scale v n, a conservative
(dominating) variance v̂ n, and the normalization size m n — so every design-based paper with a
studentized CLT and a conservative variance estimator can instantiate it in one line instead of
re-cloning the liminf/Pr_split/coverage argument (as the exposure-mapping, two-stage, and
bipartite-interference formalizations each previously did).
Conservative Wald-interval liminf coverage. Consider a sequence of finite designs with an estimator est n of a target θ n. Suppose the normalization size m n is eventually positive, the true variance scale v n is eventually positive, and a deterministic conservative variance v̂ n eventually dominates v n. Suppose further that the studentized statistic √(m n)·(est n − θ n)/√(v n) has design-probability CDF converging to the standard-normal CDF at z and at −z, where z is nonnegative and satisfies Φ(z) = 1 − α/2. Then the two-sided interval |θ n − est n| ≤ z·√(v̂ n / m n) has asymptotic (liminf) coverage at least 1 − α.
Formal statement
Proof (Lean source)
WaldPipeline 1 core · 0 supporting dependency_wald_coverage chains the design-based dependency CLT (dependency_studentized_cdf) into the conservative Wald-coverage transfer (conservative_wald_liminf_of_studentized_cdf). ★ dependency_wald_coverage
Design-based Wald-interval pipeline
dependency_wald_coverage chains the design-based dependency CLT (dependency_studentized_cdf)
into the conservative Wald-coverage transfer (conservative_wald_liminf_of_studentized_cdf). Given
unit
contributions X n whose standardized sum depSum(X n) eventually equals the scaled centered
estimator √(m n)·(est n − θ n), and a deterministic variance vhat n that eventually dominates
v n, the Wald interval
|θ n − est n| ≤ z·√(vhat n / m n) has liminf coverage at least 1 − α.
Design-based Wald-interval coverage from dependency-graph primitives. Consider a sequence of finite designs together with per-unit contributions X n i governed by a dependency graph Dep n on those contributions whose neighbourhoods have cardinality at most Dmax, where the contributions are uniformly bounded by a nonnegative constant M and have design mean zero. Suppose the standardizing quantity v n equals the design second moment of the contributions' sum depSum(X n), is bounded below by a positive constant c times the number of units eventually, and the number of units diverges. Suppose further that the standardized sum eventually equals √(m n)·(est n − θ n) for an estimator est n of a target θ n, the normalization m n is eventually positive, and a deterministic conservative variance v̂ n eventually dominates v n, with z the nonnegative quantile satisfying Φ(z) = 1 − α/2. Then the two-sided Wald interval |θ n − est n| ≤ z·√(v̂ n / m n) has asymptotic (liminf) coverage at least 1 − α.