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)
For a randomization design on a finite assignment space and a real-valued statistic of the realized assignment, the design expectation is the probability-weighted sum of that statistic over all assignments.
Definition (Lean source)
For a randomization design on a finite assignment space and a real-valued statistic of the realized assignment, the design variance is the design expectation of the statistic's squared deviation from its design expectation.
Definition (Lean source)
For a randomization design on a finite assignment space and two real-valued statistics of the realized assignment, the design covariance is the design expectation of the product of their deviations from their respective design expectations.
Definition (Lean source)
For an event with decidable membership on an assignment space, its indicator statistic assigns one to assignments in the event and zero to all other assignments.
Definition (Lean source)
For a randomization design on a finite assignment space and an event with decidable membership, the design probability of the event is the design expectation of its indicator statistic.
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
For a randomization design on a finite assignment space and a transformation from that space to another finite assignment space, the pushforward randomization design is the law of the transformed assignment: each transformed assignment receives the total probability of all original assignments mapped to it.
Definition (Lean source)
32 supporting declarations (lemmas, instances)
-
E_constlemma — The expectation of a constant random variable is that constant.Proof (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.hypothesesconclusionD.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.hypothesesconclusionD.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.hypothesesconclusionD.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.hypothesesconclusionD.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.hypothesesconclusionD.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.hypothesesconclusionD.E X = D.E Y -
Var_congrlemma — Congruence: pointwise-equal random variables have equal variance.hypothesesconclusionD.Var X = D.Var Y -
Cov_congrlemma — Congruence: pointwise-equal random variables have equal covariance.hypothesesΩ :sharedType u_1X Y X' Y' :Ω → ℝhX :∀ z, X z = X' zhY :∀ z, Y z = Y' zconclusionD.Cov X Y = D.Cov X' Y' -
Cov_selflemma — The covariance of a random variable with itself is its variance. -
Cov_commlemma — Covariance is symmetric in its two arguments.hypothesesconclusionD.Cov X Y = D.Cov Y X -
Cov_const_mul_leftlemma — Multiplying the left random variable by a constant multiplies covariance by that constant.hypothesesconclusionD.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.hypothesesconclusionD.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.hypothesesconclusionD.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.hypothesesconclusionD.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).hypothesesconclusionD.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.hypothesesconclusionD.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.hypothesesΩ :sharedType u_1A :Ω → Prop -
E_nonneglemma — Expectation of a nonnegative random variable is nonnegative.hypothesesconclusion0 ≤ 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.hypothesesconclusionD.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.hypothesesconclusion0 ≤ D.Pr AProof (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.hypothesesconclusionD.Pr A ≤ 1Proof (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.hypothesesΩ :sharedType u_1A 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.hypothesesΩ :sharedType u_1A 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.hypothesesconclusionD.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]
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.
For a randomization design on a finite assignment space equipped with a σ-algebra, the induced probability measure assigns to each assignment a point mass equal to that assignment's design probability, and sums these point masses over all assignments.
Definition (Lean source)
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.hypothesesconclusionD.toMeasure s = ∑ z, ofReal (D.p z) * Measure.dirac z sProof (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 — For every randomization design on a finite assignment space equipped with a σ-algebra, the measure induced by that design is a probability measure: its total mass is one.parametersΩ :sharedType u_1instancegiven byby refine ⟨?_⟩ rw [toMeasure_apply] have h : ∀ z ∈ (Finset.univ : Finset Ω), ofReal (D.p z) * Measure.dirac z univ
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.
For a finite, equality-comparable index set whose coordinate assignment spaces are finite, a family of coordinate-specific randomization designs defines the product design, which randomizes all coordinates independently: the probability of an assignment vector is the product of the probabilities assigned to its coordinate values by their respective designs.
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)
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.
For an assignment-to-exposure rule, a map assigning each unit its traits, a unit, and an assignment, the unit's exposure is the exposure assigned by that rule to the assignment and the unit's traits.
Definition (Lean source)
For an assignment-to-exposure rule, a map assigning each unit its traits, a unit, and an exposure condition from a set whose elements can be compared for equality, the exposure indicator maps each assignment to one when that unit receives that condition and to zero otherwise.
Definition (Lean source)
On a finite assignment space, for a finite randomization design, an assignment-to-exposure rule, a map assigning each unit its traits, a unit, and an exposure condition from a set whose elements can be compared for equality, the generalized probability of exposure is the design probability that the unit receives that condition.
Definition (Lean source)
On a finite assignment space, for a finite randomization design, an assignment-to-exposure rule, a map assigning each unit its traits, two units, and an exposure condition from a set whose elements can be compared for equality, the same-condition joint exposure probability is the design expectation of the product of the two units' indicators for that condition.
Definition (Lean source)
On a finite assignment space, for a finite randomization design, an assignment-to-exposure rule, a map assigning each unit its traits, two units, and two exposure conditions from a set whose elements can be compared for equality, the cross-condition joint exposure probability is the design expectation of the product of the first unit's indicator for the first condition and the second unit's indicator for the second condition.
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.hypothesesΩ :sharedType u_1ι :sharedType u_2Θ :sharedType u_3Δ :sharedType u_4f :Ω → Θ → Δθ :ι → Θ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.hypothesesΩ :sharedType u_1ι :sharedType u_2Θ :sharedType u_3Δ :sharedType u_4D :f :Ω → Θ → Δθ :ι → Θi :ιd d' :Δhne :d ≠ d'conclusionpropPairCross 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.
For a randomization design, a real-valued estimator of the realized assignment, and a real-valued target, the estimator's design bias is its design expectation minus the target.
Definition (Lean source)
For a randomization design, a real-valued estimator of the realized assignment, and a real-valued target, the estimator's design mean squared error is the design expectation of the squared difference between the estimator and the target.
Definition (Lean source)
For a randomization design, a real-valued estimator of the realized assignment, and a real-valued target, the assertion that the estimator is unbiased means that its design expectation equals the target.
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.hypothesesconclusionD.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.hypothesesconclusionD.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.hypothesesconclusion0 ≤ 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).Proof (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.hypothesesconclusionD.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.hypothesesconclusionD.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])
InProb 5 core · 8 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.
For a sequence of finite assignment spaces, a sequence of finite randomization designs, a sequence of real-valued statistics, and a sequence of real-valued targets, the assertion of convergence in probability means that, for every positive , the probability that the statistic differs from its target by at least tends to zero as the sequence index tends to infinity.
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)
For a sequence of finite assignment spaces, a sequence of finite randomization designs, and a sequence of real-valued statistics, the assertion that the statistics are bounded in probability means that, for every positive tolerance, there is a real threshold such that, from some index onward, the probability that the statistic's absolute value is at least that threshold is at most the tolerance. This is the counterpart of convergence in probability.
Definition (Lean source)
8 supporting declarations (lemmas, instances)
-
deterministic_tendstoInProbtheorem — Under a sequence of finite-design laws, if a deterministic real sequence converges to a constant, then the corresponding constant-on-assignment statistics converge in finite-design probability.hypothesesconclusionTendstoInProb D (fun n _ => a n) (fun _ => c)Proof (Lean source)
theorem deterministic_tendstoInProb (D : ∀ n, FiniteDesign (Ω n)) (a : ℕ → ℝ) (c : ℝ) (ha : Tendsto a atTop (𝓝 c)) : TendstoInProb D (fun n _ => a n) (fun _ => c) := by intro ε hε have hev : ∀ᶠ n in atTop, |a n - c| < ε := by simpa [Real.dist_eq] using (Metric.tendsto_atTop.1 ha ε hε) apply tendsto_order.2 constructor · intro u hu filter_upwards [] with n exact hu.trans_le ((D n).Pr_nonneg _) · intro u hu filter_upwards [hev] with n hn have hz : (D n).Pr (fun _ => ε ≤ |a n - c|) = 0 := by unfold FiniteDesign.Pr FiniteDesign.E FiniteDesign.ind simp [not_le.mpr hn] rw [hz] exact hu -
tendstoInProb_continuousMaptheorem — Under a sequence of finite-design laws, if a statistic converges in probability to a constant and a real map is continuous at that constant, then applying the map preserves convergence in probability.hypothesesΩ :sharedℕ → Type u_1D :∀ n, FiniteDesign (Ω n)X :∀ nifΩ nthenℝc :ℝf :ℝ → ℝhX :TendstoInProb D X (fun _ => c)hf :ContinuousAt f cconclusionTendstoInProb D (fun n z => f (X n z)) (fun _ => f c)Proof (Lean source)
theorem tendstoInProb_continuousMap (D : ∀ n, FiniteDesign (Ω n)) (X : ∀ n, Ω n → ℝ) (c : ℝ) (f : ℝ → ℝ) (hX : TendstoInProb D X (fun _ => c)) (hf : ContinuousAt f c) : TendstoInProb D (fun n z => f (X n z)) (fun _ => f c) := by intro ε hε obtain ⟨δ, hδ, hmap⟩ := (Metric.continuousAt_iff.1 hf) ε hε have htail := hX δ hδ refine squeeze_zero (fun n => (D n).Pr_nonneg _) (fun n => ?_) htail apply (D n).Pr_mono intro z hz by_contra hfar rw [not_le] at hfar have := hmap (show dist (X n z) c < δ by simpa [Real.dist_eq] using hfar) exact (not_lt_of_ge hz) (by simpa [Real.dist_eq] using this) -
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.hypothesesconclusionTendstoInProb 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.hypothesesΩ :sharedℕ → Type u_1D :∀ m, FiniteDesign (Ω m)X :∀ mifΩ mthenℝV c :ℝhc :∀ᶠ m in atTop, |(D m).E (X m)| ≤ cconclusionBoundedInProb 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.hypothesesconclusionTendstoInProb 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]
GaussianCDF 3 core · 5 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.
For a real threshold, the standard normal cumulative distribution function is the probability that a standard normal random variable is no greater than that threshold.
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)
5 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 -
boundedInProb_of_stdNormalCDFtheorem — For a sequence of finite-design laws and real-valued statistics, if their CDFs converge pointwise to the standard normal CDF, then the statistics are bounded in probability.hypothesesconclusionBoundedInProb D TProof (Lean source)
theorem boundedInProb_of_stdNormalCDF (D : ∀ n, FiniteDesign (Ω n)) (T : ∀ n, Ω n → ℝ) (hT : ∀ x : ℝ, Tendsto (fun n => (D n).Pr (fun z => T n z ≤ x)) atTop (𝓝 (stdNormalCdf x))) : BoundedInProb D T := by intro η hη have htop : Tendsto stdNormalCdf atTop (𝓝 1) := by rw [show stdNormalCdf = stdNormalCDF by funext x; exact stdNormalCdf_eq x] exact Causalean.Mathlib.stdNormalCDF_tendsto_atTop have hevent : ∀ᶠ x : ℝ in atTop, 1 - stdNormalCdf x < η / 4 := by have h := (Metric.tendsto_nhds.1 htop) (η / 4) (by linarith) filter_upwards [h] with x hx rw [Real.dist_eq] at hx linarith [(abs_lt.1 hx).1] obtain ⟨R, hRtail, hRpos⟩ := (hevent.and (eventually_gt_atTop (0 : ℝ))).exists refine ⟨2 * R, ?_⟩ have hneg := hT (-R) have hpos := hT R have hsum : Tendsto (fun n => (D n).Pr (fun z => T n z ≤ -R) + (1 - (D n).Pr (fun z => T n z ≤ R))) atTop (𝓝 (2 * (1 - stdNormalCdf R))) := by convert hneg.add (tendsto_const_nhds.sub hpos) using 1 · rw [stdNormalCdf_neg] ring have hsumSmall : ∀ᶠ n in atTop, (D n).Pr (fun z => T n z ≤ -R) + (1 - (D n).Pr (fun z => T n z ≤ R)) < η := by have hlimlt : 2 * (1 - stdNormalCdf R) < η := by linarith exact hsum.eventually (eventually_lt_nhds hlimlt) filter_upwards [hsumSmall] with n hn have hcompl : (D n).Pr (fun z => ¬ T n z ≤ R) = 1 - (D n).Pr (fun z => T n z ≤ R) := by have hs := (D n).Pr_split (fun _ => True) (fun z => T n z ≤ R) have htrue : (D n).Pr (fun _ => True) = 1 := by unfold FiniteDesign.Pr FiniteDesign.E FiniteDesign.ind simp [(D n).p_sum] rw [htrue] at hs simp only [true_and] at hs linarith calc (D n).Pr (fun z => 2 * R ≤ |T n z|) ≤ (D n).Pr (fun z => T n z ≤ -R ∨ ¬ T n z ≤ R) := by apply (D n).Pr_mono intro z hz rcases le_total (T n z) 0 with hnonpos | hnonneg · left rw [abs_of_nonpos hnonpos] at hz linarith · right rw [abs_of_nonneg hnonneg] at hz linarith _ ≤ (D n).Pr (fun z => T n z ≤ -R) + (D n).Pr (fun z => ¬ T n z ≤ R) := Pr_or_le _ _ _ _ ≤ η := by rw [hcompl]; exact hn.le
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.
For a finite space of first-stage outcomes, a finite space of second-stage outcomes, a probability design for the first stage, and a rule assigning a probability design for the second stage after each first-stage outcome, the compound two-stage design assigns a pair of outcomes the product of its first-stage probability and its conditional second-stage probability.
Definition (Lean source)
For a finite space of first-stage outcomes, a finite index set for second-stage coordinates, a finite outcome space for each coordinate, a probability design for the first stage, and a rule assigning, after each first-stage outcome, a design to each coordinate, the compound two-stage design first draws the first-stage outcome and then independently draws every coordinate from its conditional design.
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.hypothesesconclusionD.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, ·)]].hypothesesΩ₁ :sharedType u_1ι :sharedType u_2ι → Type u_3D₁ :FiniteDesign Ω₁D₂ :Ω₁ → ∀ i, FiniteDesign (α i)F :(Ω₁ × ∀ i, α i) → ℝconclusion(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.hypothesesΩ :sharedType u_1X :Ω → ℝ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.hypothesesΩ :sharedType u_1X :Ω → ℝ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.hypothesesconclusion|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.hypothesesΩ :sharedType u_1X 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.hypothesesconclusionD.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
HeydeBrown 14 core · 6 supporting This module turns a finite product randomization design into the product probability space and reveal filtration needed by a supplied Heyde--Brown fourth-moment inequality. ★ finiteDesign_heydeBrown_fourthMoment
Finite-design Heyde--Brown bridge
This module turns a finite product randomization design into the product probability space and reveal filtration needed by a supplied Heyde--Brown fourth-moment inequality. It identifies the finite and measure-theoretic conditional expectations, predictable variations, moments, and CDF expressions, then specializes the supplied inequality without postulating or proving it.
A reveal permutation and coordinate determine that coordinate's reveal rank, namely the step at which the permutation reveals it.
A reveal permutation, prefix length, and two assignments determine agreement through the reveal prefix: the assignments have the same values on every coordinate already revealed by this equality condition.
Definition (Lean source)
A reveal permutation and prefix length determine the σ-algebra generated by the revealed coordinates, which records exactly the information available after that many reveal steps by generating from those coordinate evaluations.
Definition (Lean source)
A reveal permutation determines the reveal filtration, whose time-k σ-algebra is the prefix σ-algebra, is monotone in reveal time, and lies inside the full product σ-algebra.
Definition (Lean source)
A family of coordinate designs, reveal permutation, prefix length, and statistic determine the explicit prefix conditional expectation, obtained by averaging over unrevealed coordinates while holding revealed coordinates fixed by the stated finite sum.
Definition (Lean source)
A family of coordinate designs, reveal permutation, and increment family satisfy the prefix martingale-difference condition when each increment has zero conditional mean immediately before its reveal and is visible after that reveal.
Definition (Lean source)
A family of coordinate designs, reveal permutation, and increment family determine the finite-design predictable variation, the sum of conditional second moments just before each reveal step by the displayed finite sum.
Definition (Lean source)
A measure (in intended use a probability measure; none is required), filtration, and increment family determine the measure-theoretic predictable variation, the sum of conditional second moments at the preceding filtration times by the displayed finite sum.
Definition (Lean source)
A family of coordinate designs, reveal permutation, and increment family determine the finite fourth-moment error: the sum of fourth moments plus the second moment of predictable variation minus one by the displayed sum of two terms.
Definition (Lean source)
A measure (in intended use a probability measure; none is required), filtration, and increment family determine the measure-theoretic fourth-moment error: the sum of fourth moments plus the second moment of predictable variation minus one by the displayed sum of two terms.
Definition (Lean source)
A finite randomization design and real statistic determine its finite-design Kolmogorov expression, the largest absolute gap between its CDF and the standard-normal CDF by taking the supremum over thresholds.
Definition (Lean source)
A measure and real random variable determine its measure-theoretic Kolmogorov expression, the largest absolute gap between its CDF and the standard-normal CDF by taking the supremum over thresholds. No probability-measure assumption is made: the CDF term is the real-valued measure of the lower set (zero where that measure is infinite), and an unbounded family of gaps has supremum zero by convention; for a probability measure the gaps are bounded and this is the usual Kolmogorov distance.
Definition (Lean source)
A measure (in intended use a probability measure; the premise itself does not require one), filtration, increment family, and constant define the supplied Heyde--Brown fourth-moment premise: adapted, centered, normalized increments with finite fourth moments obey the stated one-fifth-power Kolmogorov bound by the four displayed assumptions and conclusion.
Definition (Lean source)
Given coordinate designs, a reveal permutation, an increment family, and a bound constant, if the increments are prefix martingale differences, their total second moment is one, and the supplied Heyde--Brown premise holds, then their sum satisfies the finite-design one-fifth-power Kolmogorov bound.
Formal statement
Proof (Lean source)
6 supporting declarations (lemmas, instances)
-
prefixCondExp_ae_eq_condExptheorem — A family of coordinate designs, reveal permutation, prefix length, and statistic give an almost-everywhere identification of the explicit prefix average with conditional expectation under the product-design measure and its reveal σ-algebra.hypothesesconclusionprefixCondExp D pi k fProof (Lean source)
theorem prefixCondExp_ae_eq_condExp (D : ∀ i, FiniteDesign (alpha i)) (pi : Perm (Fin N)) (k : Fin (N + 1)) (f : (∀ i, alpha i) → ℝ) : prefixCondExp D pi k f =ᵐ[(prodDesign D).toMeasure] (prodDesign D).toMeasure[f | (revealFiltration pi) k] := by classical let m0 : MeasurableSpace (∀ i, alpha i) := inferInstance let m : MeasurableSpace (∀ i, alpha i) := (revealFiltration pi) k let mInv : MeasurableSpace (∀ i, alpha i) := by exact { MeasurableSet' := fun s ↦ ∀ w w', AgreeOnPrefix pi k w w' → (w ∈ s ↔ w' ∈ s) measurableSet_empty := by simp measurableSet_compl := by intro s hs w w' hww' simpa only [Set.mem_compl_iff] using not_congr (hs w w' hww') measurableSet_iUnion := by intro s hs w w' hww' constructor <;> intro hw · simp only [Set.mem_iUnion] at hw ⊢ obtain ⟨i, hi⟩ := hw exact ⟨i, (hs i w w' hww').1 hi⟩ · simp only [Set.mem_iUnion] at hw ⊢ obtain ⟨i, hi⟩ := hw exact ⟨i, (hs i w w' hww').2 hi⟩ } have hm : m ≤ m0 := by simpa only [m, m0] using (revealFiltration pi).le k have hmInv : m ≤ mInv := by unfold m revealFiltration revealMeasurableSpace refine iSup_le fun i ↦ ?_ by_cases hi : (prefixRank pi i).val < k.val · simp only [hi, if_true] intro s hs rw [MeasurableSpace.measurableSet_comap] at hs obtain ⟨t, ht, rfl⟩ := hs change ∀ w w', AgreeOnPrefix pi k w w' → (w i ∈ t ↔ w' i ∈ t) intro w w' hww' rw [hww' i hi] · simp [hi] have hmem_of_agree {s : Set (∀ i, alpha i)} (hs : MeasurableSet[m] s) {w w' : ∀ i, alpha i} (hww' : AgreeOnPrefix pi k w w') : w ∈ s ↔ w' ∈ s := by exact hmInv s hs w w' hww' have hcell (w' : ∀ i, alpha i) : MeasurableSet[m] {w | AgreeOnPrefix pi k w w'} := by have hset : {w | AgreeOnPrefix pi k w w'} = ⋂ i, if (prefixRank pi i).val < k.val then {w | w i = w' i} else univ := by ext w simp only [Set.mem_ofPred_eq, Set.mem_iInter] constructor · intro h i by_cases hi : (prefixRank pi i).val < k.val · simp [hi, (h i hi).symm] · simp [hi] · intro h i hi have h' : w i = w' i := by simpa [hi] using h i exact h'.symm rw [hset] refine MeasurableSet.iInter fun i ↦ ?_ by_cases hi : (prefixRank pi i).val < k.val · simp only [hi, if_true] have hbase : MeasurableSet[ comap (fun w : ∀ q, alpha q => w i) (inferInstance)] {w | w i = w' i} := (measurableSet_singleton (w' i)).preimage (comap_measurable (fun w : ∀ q, alpha q => w i)) have hcomponent : MeasurableSet[ if (prefixRank pi i).val < k.val then comap (fun w : ∀ q, alpha q => w i) inferInstance else ⊥] {w | w i = w' i} := by rw [if_pos hi] exact hbase exact (le_iSup (fun j : Fin N ↦ if (prefixRank pi j).val < k.val then comap (fun w : ∀ q, alpha q => w j) inferInstance else ⊥) i) _ hcomponent · simp [hi] have hmeas : Measurable[m] (prefixCondExp D pi k f) := by unfold prefixCondExp exact measurable_sum univ fun w' _ ↦ Measurable.ite (hcell w') measurable_const measurable_const let _ : MeasurableSpace (∀ i, alpha i) := m0 have hf : Integrable f (prodDesign D).toMeasure := Integrable.of_finite refine ae_eq_condExp_of_forall_setIntegral_eq hm hf ?_ ?_ hmeas.stronglyMeasurable.aestronglyMeasurable · intro s _ _ exact (show Integrable (prefixCondExp D pi k f) (prodDesign D).toMeasure from Integrable.of_finite).integrableOn · intro s hs _ have hs0 : MeasurableSet[m0] s := hm s hs rw [← integral_indicator hs0, ← integral_indicator hs0, FiniteDesign.integral_toMeasure, FiniteDesign.integral_toMeasure] have hmass (w' : ∀ i, alpha i) : (∑ z : ∀ i, alpha i, if AgreeOnPrefix pi k z w' then ∏ i, (D i).p (z i) else 0) = ∏ i, if (prefixRank pi i).val < k.val then (D i).p (w' i) else 1 := by have hterm (z : ∀ i, alpha i) : (if AgreeOnPrefix pi k z w' then ∏ i, (D i).p (z i) else 0) = ∏ i, if (prefixRank pi i).val < k.val then if z i = w' i then (D i).p (z i) else 0 else (D i).p (z i) := by by_cases hz : AgreeOnPrefix pi k z w' · rw [if_pos hz] apply Finset.prod_congr rfl intro i _ by_cases hi : (prefixRank pi i).val < k.val · simp [hi, (hz i hi).symm] · simp [hi] · rw [if_neg hz] simp only [AgreeOnPrefix] at hz push Not at hz obtain ⟨i, hi, hne⟩ := hz exact (Finset.prod_eq_zero (Finset.mem_univ i) (by simp [hi, hne.symm])).symm calc (∑ z : ∀ i, alpha i, if AgreeOnPrefix pi k z w' then ∏ i, (D i).p (z i) else 0) = ∑ z : ∀ i, alpha i, ∏ i, if (prefixRank pi i).val < k.val then if z i = w' i then (D i).p (z i) else 0 else (D i).p (z i) := Finset.sum_congr rfl fun z _ ↦ hterm z _ = ∏ i, ∑ a : alpha i, if (prefixRank pi i).val < k.val then if a = w' i then (D i).p a else 0 else (D i).p a := (Fintype.prod_sum (fun i (a : alpha i) ↦ if (prefixRank pi i).val < k.val then if a = w' i then (D i).p a else 0 else (D i).p a)).symm _ = ∏ i, if (prefixRank pi i).val < k.val then (D i).p (w' i) else 1 := by apply Finset.prod_congr rfl intro i _ by_cases hi : (prefixRank pi i).val < k.val · simp [hi] · simp [hi, (D i).p_sum] have hsplit (w' : ∀ i, alpha i) : (∏ i, if k.val ≤ (prefixRank pi i).val then (D i).p (w' i) else 1) * (∏ i, if (prefixRank pi i).val < k.val then (D i).p (w' i) else 1) = ∏ i, (D i).p (w' i) := by rw [← Finset.prod_mul_distrib] apply Finset.prod_congr rfl intro i _ by_cases hi : (prefixRank pi i).val < k.val · have hnle : ¬k.val ≤ (prefixRank pi i).val := Nat.not_le_of_gt hi simp [hi, hnle] · have hle : k.val ≤ (prefixRank pi i).val := Nat.le_of_not_gt hi simp [hi, hle] have hswap (z : ∀ i, alpha i) : (∏ i, (D i).p (z i)) * (if z ∈ s then ∑ w' : ∀ i, alpha i, if AgreeOnPrefix pi k z w' then (∏ i, if k.val ≤ (prefixRank pi i).val then (D i).p (w' i) else 1) * f w' else 0 else 0) = ∑ w' : ∀ i, alpha i, if w' ∈ s then (∏ i, if k.val ≤ (prefixRank pi i).val then (D i).p (w' i) else 1) * f w' * (if AgreeOnPrefix pi k z w' then ∏ i, (D i).p (z i) else 0) else 0 := by by_cases hz : z ∈ s · rw [if_pos hz, Finset.mul_sum] apply Finset.sum_congr rfl intro w' _ by_cases ha : AgreeOnPrefix pi k z w' · have hw' : w' ∈ s := (hmem_of_agree hs ha).1 hz simp only [ha, if_true, hw'] ring · simp [ha] · rw [if_neg hz] simp only [mul_zero] symm apply Finset.sum_eq_zero intro w' _ by_cases ha : AgreeOnPrefix pi k z w' · have hw' : w' ∉ s := fun hw' ↦ hz ((hmem_of_agree hs ha).2 hw') simp [hw'] · simp [ha] simp only [FiniteDesign.E, prodDesign_p, indicator, prefixCondExp] calc (∑ z, (∏ i, (D i).p (z i)) * if z ∈ s then ∑ w', if AgreeOnPrefix pi k z w' then (∏ i, if k.val ≤ (prefixRank pi i).val then (D i).p (w' i) else 1) * f w' else 0 else 0) = ∑ z, ∑ w', if w' ∈ s then (∏ i, if k.val ≤ (prefixRank pi i).val then (D i).p (w' i) else 1) * f w' * (if AgreeOnPrefix pi k z w' then ∏ i, (D i).p (z i) else 0) else 0 := Finset.sum_congr rfl fun z _ ↦ hswap z _ = ∑ w', ∑ z, if w' ∈ s then (∏ i, if k.val ≤ (prefixRank pi i).val then (D i).p (w' i) else 1) * f w' * (if AgreeOnPrefix pi k z w' then ∏ i, (D i).p (z i) else 0) else 0 := Finset.sum_comm _ = ∑ w', (∏ i, (D i).p (w' i)) * if w' ∈ s then f w' else 0 := by apply Finset.sum_congr rfl intro w' _ by_cases hw' : w' ∈ s · simp only [hw', if_true] rw [← Finset.mul_sum, hmass] rw [← hsplit w'] ring · simp [hw'] -
aestronglyMeasurable_reveal_of_prefixCondExp_eqtheorem — A family of coordinate designs, reveal permutation, prefix length, statistic, and pointwise equality to its prefix conditional expectation imply that the statistic is almost-everywhere strongly measurable for the reveal σ-algebra.hypothesesD :∀ i, FiniteDesign (alpha i)k :Fin (N + 1)f :(∀ i, alpha i) → ℝhf :prefixCondExp D pi k f = fconclusionProof (Lean source)
theorem aestronglyMeasurable_reveal_of_prefixCondExp_eq (D : ∀ i, FiniteDesign (alpha i)) (pi : Perm (Fin N)) (k : Fin (N + 1)) (f : (∀ i, alpha i) → ℝ) (hf : prefixCondExp D pi k f = f) : AEStronglyMeasurable[(revealFiltration pi) k] f (prodDesign D).toMeasure := by rw [← hf] exact stronglyMeasurable_condExp.aestronglyMeasurable.congr (prefixCondExp_ae_eq_condExp D pi k f).symm -
condExp_ae_eq_zero_of_prefixCondExp_eq_zerotheorem — A family of coordinate designs, reveal permutation, prefix length, statistic, and zero explicit prefix conditional expectation imply the measure-theoretic conditional expectation is almost everywhere zero.hypothesesD :∀ i, FiniteDesign (alpha i)k :Fin (N + 1)f :(∀ i, alpha i) → ℝhf :prefixCondExp D pi k f = 0conclusionProof (Lean source)
theorem condExp_ae_eq_zero_of_prefixCondExp_eq_zero (D : ∀ i, FiniteDesign (alpha i)) (pi : Perm (Fin N)) (k : Fin (N + 1)) (f : (∀ i, alpha i) → ℝ) (hf : prefixCondExp D pi k f = 0) : (prodDesign D).toMeasure[f | (revealFiltration pi) k] =ᵐ[(prodDesign D).toMeasure] 0 := by simpa only [hf] using (prefixCondExp_ae_eq_condExp D pi k f).symm -
finitePredictableVariation_ae_eq_measurePredictableVariationtheorem — A family of coordinate designs, reveal permutation, and increment family give an almost-everywhere equality between finite-design and measure-theoretic predictable variations under the product-design measure.hypothesesD :∀ i, FiniteDesign (alpha i)X :Fin N → (∀ i, alpha i) → ℝconclusionfinitePredictableVariation D pi X=ᵐ[(prodDesign D).toMeasure] measurePredictableVariation (prodDesign D).toMeasure (revealFiltration pi) XProof (Lean source)
theorem finitePredictableVariation_ae_eq_measurePredictableVariation (D : ∀ i, FiniteDesign (alpha i)) (pi : Perm (Fin N)) (X : Fin N → (∀ i, alpha i) → ℝ) : finitePredictableVariation D pi X =ᵐ[(prodDesign D).toMeasure] measurePredictableVariation (prodDesign D).toMeasure (revealFiltration pi) X := by unfold finitePredictableVariation measurePredictableVariation filter_upwards [ae_all_iff.2 (fun s ↦ prefixCondExp_ae_eq_condExp D pi (castSucc s) (fun z ↦ (X s z) ^ 2))] with w hw exact Finset.sum_congr rfl fun s _ ↦ hw s -
finiteKolmogorovExpr_eq_measureKolmogorovExprtheorem — A family of coordinate designs and real statistic give an exact identification between the finite-design and measure-theoretic Kolmogorov expressions under the induced product-design measure.hypothesesconclusionProof (Lean source)
theorem finiteKolmogorovExpr_eq_measureKolmogorovExpr (D : ∀ i, FiniteDesign (alpha i)) (Y : (∀ i, alpha i) → ℝ) : finiteKolmogorovExpr (prodDesign D) Y = measureKolmogorovExpr (prodDesign D).toMeasure Y := by classical unfold finiteKolmogorovExpr measureKolmogorovExpr apply congrArg sSup congr 1 funext t rw [FiniteDesign.Pr_eq_measureReal] -
finiteFourthMomentError_eq_measureFourthMomentErrortheorem — A family of coordinate designs, reveal permutation, and increment family give an exact identification between finite-design and measure-theoretic fourth-moment errors, including the predictable-variation term.hypothesesD :∀ i, FiniteDesign (alpha i)X :Fin N → (∀ i, alpha i) → ℝconclusionfiniteFourthMomentError D pi XProof (Lean source)
theorem finiteFourthMomentError_eq_measureFourthMomentError (D : ∀ i, FiniteDesign (alpha i)) (pi : Perm (Fin N)) (X : Fin N → (∀ i, alpha i) → ℝ) : finiteFourthMomentError D pi X = measureFourthMomentError (prodDesign D).toMeasure (revealFiltration pi) X := by unfold finiteFourthMomentError measureFourthMomentError congr 1 · apply Finset.sum_congr rfl intro s _ exact ((prodDesign D).integral_toMeasure (fun w ↦ |X s w| ^ 4)).symm · rw [← (prodDesign D).integral_toMeasure (fun w ↦ |finitePredictableVariation D pi X w - 1| ^ 2)] apply integral_congr_ae filter_upwards [finitePredictableVariation_ae_eq_measurePredictableVariation D pi X] with w hw rw [hw]
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.
At each stage suppose the coordinate index set and every coordinate assignment space are finite, coordinate equality is decidable, and every singleton in every coordinate assignment space is measurable. For a family of coordinate-specific randomization designs, indexed by stage and coordinate, a family of real-valued coordinate summands, and a stage, the diagonal dependency graph is the dependency graph of the coordinate summands under the corresponding product design, in which two coordinates are adjacent exactly when they are the same coordinate.
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)
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.
For a finite population of units, a dependence block assigned to each unit, and a nonnegative integer bound, the assertion that the block family has degree at most means that, for every unit, at most blocks contain that unit. When the blocks are the in-neighbourhoods of a dependency graph, this is the out-degree bound.
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).
Formal statement
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)
@[fun_prop] 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.hypothesesconclusionAEMeasurable g D.toMeasureProof (Lean source)
@[fun_prop] 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.hypothesesconclusionD.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.hypothesesconclusionD.Var g = variance g D.toMeasureProof (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.hypothesesconclusionD.Pr A = D.toMeasure.real {z | A z}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.hypothesesconclusionD.Cov X Y = covariance X Y D.toMeasureProof (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 This file represents a unit's outcome under an assignment by evaluating its potential outcome at the exposure induced by that assignment. ★ Yobs_eq_sum
Potential outcomes under exposure mappings
This file represents a unit's outcome under an assignment by evaluating its potential outcome at the exposure induced by that assignment. It supplies the properly specified exposure condition and the observed-outcome construction used by the design-based interference results.
For potential outcomes indexed by unit and exposure level, randomization potential outcomes indexed by unit and assignment, an assignment-to-exposure mapping, and unit-level attributes used by that mapping, the properly specified exposure condition states that, for every unit and every assignment, the randomization potential outcome equals the potential outcome at the exposure induced for that unit by the assignment.
Definition (Lean source)
For potential outcomes indexed by unit and exposure level, an assignment-to-exposure mapping, unit-level attributes used by that mapping, a unit, and an assignment, the observed outcome is that unit's potential outcome at the exposure induced by the assignment.
Definition (Lean source)
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.hypothesesΩ :sharedType u_1ι :sharedType u_2Θ :sharedType u_3Δ :sharedType u_4y :ι → Δ → ℝ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)².hypothesesΩ :sharedType u_1ι :sharedType u_2Θ :sharedType u_3Δ :sharedType u_4y :ι → Δ → ℝ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.hypothesesΩ :sharedType u_1ι :sharedType u_2Θ :sharedType u_3Δ :sharedType u_4y :ι → Δ → ℝ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.hypothesesconclusionNonempty (α i)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.)hypothesesι :sharedType u_1ι → Type u_2D :∀ 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.hypothesesι :sharedType u_1ι → Type u_2D :∀ 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ι :sharedType u_1ι → Type u_2β γ :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.hypothesesι :sharedType u_1ι → Type u_2D :∀ i, FiniteDesign (α i)i j :ιh :i ≠ jg :α i → ℝhfun :α j → ℝconclusion(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.hypothesesι :sharedType u_1ι → Type u_2D :∀ i, FiniteDesign (α i)i j :ιh :i ≠ jg :α i → ℝhfun :α j → ℝconclusion(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.hypothesesconclusionD.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.hypothesesΩ :sharedType u_1X 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 · 1 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)
1 supporting declaration (lemmas, instances)
-
finiteDesign_symmetricBand_tendstolemma — For a sequence of finite-design laws and real-valued statistics, if their CDFs converge pointwise to a limit CDF, the limit CDF is continuous, and the symmetric-band radius is nonnegative, then the closed symmetric-band probabilities converge to the difference of the limiting CDF at the two endpoints.hypothesesΩ :sharedℕ → Type u_1D :∀ n, FiniteDesign (Ω n)T :∀ nifΩ nthenℝF :ℝ → ℝhF :c :ℝhc :0 ≤ cProof (Lean source)
lemma finiteDesign_symmetricBand_tendsto (D : ∀ n, FiniteDesign (Ω n)) (T : ∀ n, Ω n → ℝ) (F : ℝ → ℝ) (hT : ∀ x : ℝ, Tendsto (fun n => (D n).Pr (fun z => T n z ≤ x)) atTop (𝓝 (F x))) (hF : Continuous F) (c : ℝ) (hc : 0 ≤ c) : Tendsto (fun n => (D n).Pr (fun z => -c ≤ T n z ∧ T n z ≤ c)) atTop (𝓝 (F c - F (-c))) := by classical rw [Metric.tendsto_atTop] intro ε hε have hε8 : 0 < ε / 8 := by linarith obtain ⟨δ, hδ, hcont⟩ := (Metric.continuousAt_iff.1 hF.continuousAt) (ε / 8) hε8 let d : ℝ := δ / 2 have hd : 0 < d := by dsimp [d]; linarith have hdlt : dist (-c - d) (-c) < δ := by rw [Real.dist_eq] dsimp [d] rw [show -c - δ / 2 - -c = -(δ / 2) by ring, abs_neg, abs_of_pos (by linarith : 0 < δ / 2)] linarith have hFd : |F (-c - d) - F (-c)| < ε / 8 := by simpa [Real.dist_eq] using hcont hdlt let S : ℕ → ℝ := fun n => (D n).Pr (fun z => T n z ≤ c) let L : ℕ → ℝ := fun n => (D n).Pr (fun z => T n z ≤ -c) let Ld : ℕ → ℝ := fun n => (D n).Pr (fun z => T n z ≤ -c - d) let J : ℕ → ℝ := fun n => (D n).Pr (fun z => -c ≤ T n z ∧ T n z ≤ c) have hS := hT c have hL := hT (-c) have hLd := hT (-c - d) have hevS : ∀ᶠ n in atTop, |S n - F c| < ε / 8 := by simpa [S, Real.dist_eq] using (Metric.tendsto_nhds.1 hS) (ε / 8) hε8 have hevL : ∀ᶠ n in atTop, |L n - F (-c)| < ε / 8 := by simpa [L, Real.dist_eq] using (Metric.tendsto_nhds.1 hL) (ε / 8) hε8 have hevLd : ∀ᶠ n in atTop, |Ld n - F (-c - d)| < ε / 8 := by simpa [Ld, Real.dist_eq] using (Metric.tendsto_nhds.1 hLd) (ε / 8) hε8 have hbounds : ∀ n, S n - L n ≤ J n ∧ J n ≤ S n - Ld n := by intro n have hlo := (D n).Pr_split (fun z => T n z ≤ c) (fun z => T n z ≤ -c) have hld := (D n).Pr_split (fun z => T n z ≤ c) (fun z => T n z ≤ -c - d) have hlofirst : (D n).Pr (fun z => T n z ≤ c ∧ T n z ≤ -c) = L n := by apply (D n).Pr_congr intro z constructor · exact fun h => h.2 · intro h exact ⟨h.trans (by linarith), h⟩ have hldfirst : (D n).Pr (fun z => T n z ≤ c ∧ T n z ≤ -c - d) = Ld n := by apply (D n).Pr_congr intro z constructor · exact fun h => h.2 · intro h exact ⟨h.trans (by linarith), h⟩ have hloeq : S n - L n = (D n).Pr (fun z => T n z ≤ c ∧ ¬ T n z ≤ -c) := by have : S n = (D n).Pr (fun z => T n z ≤ c ∧ T n z ≤ -c) + (D n).Pr (fun z => T n z ≤ c ∧ ¬ T n z ≤ -c) := by simpa [S, L] using hlo rw [this, hlofirst] ring have hldeq : S n - Ld n = (D n).Pr (fun z => T n z ≤ c ∧ ¬ T n z ≤ -c - d) := by have : S n = (D n).Pr (fun z => T n z ≤ c ∧ T n z ≤ -c - d) + (D n).Pr (fun z => T n z ≤ c ∧ ¬ T n z ≤ -c - d) := by simpa [S, Ld] using hld rw [this, hldfirst] ring constructor · rw [hloeq] apply (D n).Pr_mono intro z hz exact ⟨le_of_not_ge hz.2, hz.1⟩ · rw [hldeq] apply (D n).Pr_mono intro z hz constructor · exact hz.2 · rw [not_le] linarith apply Filter.eventually_atTop.1 filter_upwards [hevS, hevL, hevLd] with n hnS hnL hnLd rw [Real.dist_eq, abs_lt] rcases hbounds n with ⟨hlower, hupper⟩ rcases abs_lt.1 hnS with ⟨hnSlo, hnShi⟩ rcases abs_lt.1 hnL with ⟨hnLlo, hnLhi⟩ rcases abs_lt.1 hnLd with ⟨hnLdlo, hnLdhi⟩ rcases abs_lt.1 hFd with ⟨hFdlo, hFdhi⟩ constructor <;> linarith
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 − α.