Stat.FiniteDesign
FiniteDesign — DesignCore, FiniteDesignMeasure, Product, ProductMeasure.
DesignCore 9 core · 37 supporting This file defines FiniteDesign, its finite-sum expectation, variance, covariance, event probability, and pushforward, together with their elementary algebraic identities. ★ FiniteDesign★ E_sum★ E_ind
Finite probability distributions and moments
This file defines FiniteDesign, its finite-sum expectation, variance, covariance, event
probability, and pushforward, together with their elementary algebraic identities. Because the
sample space is finite, none of these results needs measure-theoretic integrability assumptions.
structure FiniteDesign reviewed
⚑ flagged
Causalean.Experimentation.DesignBased
A probability distribution on a finite type: a probability mass function p on a finite type Ω whose values are nonnegative and sum to one.
Definition (Lean source)
parameters
Ω :
Type*
Fintype Ω
fields
Probability mass at the outcome `z`.
p :
Ω → ℝ
Design probabilities are nonnegative.
p_nonneg :
∀ z, 0 ≤ p z
Design probabilities sum to one.
p_sum :
∑ z, p z = 1
def E reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
For a finite probability distribution and a real-valued statistic of the realized outcome, the expectation is the probability-weighted sum of that statistic over all assignments.
Definition (Lean source)
parameters
def
E D X :
ℝ
given by
∑ z, D.p z * X z
def Var reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
For a finite probability distribution and a real-valued statistic of the realized outcome, the variance is the design expectation of the statistic's squared deviation from its expectation.
Definition (Lean source)
parameters
def
Var D X :
ℝ
given by
D.E (fun z => (X z - D.E X) ^ 2)
def Cov reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
For a finite probability distribution and two real-valued statistics of the realized outcome, the covariance is the design expectation of the product of their deviations from their respective expectations.
Definition (Lean source)
parameters
def
Cov D X Y :
ℝ
given by
D.E (fun z => (X z - D.E X) * (Y z - D.E Y))
def ind reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
For an event with decidable membership, its indicator statistic assigns one to assignments in the event and zero to all other assignments.
Definition (Lean source)
parameters
Ω :
Type u_1
A :
Ω → Prop
def
ind A :
Ω → ℝ
given by
fun z => if A z then 1 else 0
def Pr reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
For a finite probability distribution and an event with decidable membership, the design probability of the event is the design expectation of its indicator statistic.
Definition (Lean source)
lemma E_sum reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
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 expectations ∑ᵢ∈s E[fᵢ].
Formal statement
hypotheses
conclusion
D.E (fun z => ∑ i ∈ s, f i z) = ∑ i ∈ s, D.E (f i)
lemma E_ind reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
Expectation of an indicator. For any event A, the expectation of its indicator equals the design probability of A.
Formal statement
hypotheses
conclusion
D.E (ind A) = D.Pr A
Proof (Lean source)
def map reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
For a finite probability distribution and a transformation from that space to another finite type, the pushforward distribution is the law of the transformed assignment: each transformed assignment receives the total probability of all original assignments mapped to it.
Definition (Lean source)
parameters
def
given by
by classical exact { p := fun y => ∑ z, if f z = y then D.p z else 0 p_nonneg := fun y => Finset.sum_nonneg fun z _ => by by_cases h : f z = y <;> simp [h, D.p_nonneg z] p_sum := by rw [Finset.sum_comm] simp only [Finset.sum_ite_eq, Finset.mem_univ, if_true] exact D.p_sum }
37 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' -
Var_eqlemma — Variance identity. For any statistic X, its variance equals the expectation of X² minus the square of its expectation.hypothesesconclusionD.Var X = D.E (fun z => (X z) ^ 2) - (D.E X) ^ 2 -
Cov_eqlemma — Covariance identity. For any two statistics X and Y under the design, their covariance equals the expectation of X·Y minus the product of their expectations.hypothesesconclusionD.Cov X Y = D.E (fun z => X z * Y z) - D.E X * D.E YProof (Lean source)
lemma Cov_eq (X Y : Ω → ℝ) : D.Cov X Y = D.E (fun z => X z * Y z) - D.E X * D.E Y := by have h : (fun z => (X z - D.E X) * (Y z - D.E Y)) = (fun z => X z * Y z + ((-(D.E Y)) * X z + ((-(D.E X)) * Y z + D.E X * D.E Y))) := by funext z; ring rw [Cov, h, E_add, E_add, E_add, E_const_mul, E_const_mul, E_const]; ring -
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 -
Cov_linear_comblemma — 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 covariance equals the double sum over s×t of the weighted covariances cᵢeⱼ·Cov(Xᵢ,Yⱼ).hypothesesΩ :sharedType u_1ι κ :Type*s :Finset ιt :Finset κc :ι → ℝe :κ → ℝX :ι → Ω → ℝY :κ → Ω → ℝconclusionD.Cov (fun z => ∑ i ∈ s, c i * X i z) (fun z => ∑ j ∈ t, e j * Y j z)= ∑ i ∈ s, ∑ j ∈ t, c i * e j * D.Cov (X i) (Y j)Proof (Lean source)
lemma Cov_linear_comb {ι κ : Type*} (s : Finset ι) (t : Finset κ) (c : ι → ℝ) (e : κ → ℝ) (X : ι → Ω → ℝ) (Y : κ → Ω → ℝ) : D.Cov (fun z => ∑ i ∈ s, c i * X i z) (fun z => ∑ j ∈ t, e j * Y j z) = ∑ i ∈ s, ∑ j ∈ t, c i * e j * D.Cov (X i) (Y j) := by rw [Cov_sum_left] apply Finset.sum_congr rfl; intro i _ rw [Cov_const_mul_left, Cov_sum_right, Finset.mul_sum] apply Finset.sum_congr rfl; intro j _ rw [Cov_const_mul_right]; ring -
Var_linear_comblemma — 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 variance equals the double sum of weighted covariances ∑ᵢ∈s∑ⱼ∈s cᵢcⱼ·Cov(Xᵢ,Xⱼ).hypothesesconclusionD.Var (fun z => ∑ i ∈ s, c i * X i z) = ∑ i ∈ s, ∑ j ∈ s, c i * c j * D.Cov (X i) (X j)Proof (Lean source)
lemma Var_linear_comb {ι : Type*} (s : Finset ι) (c : ι → ℝ) (X : ι → Ω → ℝ) : D.Var (fun z => ∑ i ∈ s, c i * X i z) = ∑ i ∈ s, ∑ j ∈ s, c i * c j * D.Cov (X i) (X j) := by rw [← Cov_self]; exact D.Cov_linear_comb s s c c X X -
ind_sqlemma — 1_A ^ 2 = 1_A, the idempotence of an indicator.hypothesesΩ :sharedType u_1A :Ω → PropProof (Lean source)
lemma ind_sq (A : Ω → Prop) [DecidablePred A] : (fun z => (ind A z) ^ 2) = ind A := by funext z; unfold ind; by_cases h : A z <;> simp [h] -
Var_indlemma — Variance of an indicator. For any event A, the variance of its indicator equals the design probability of A times one minus that probability.hypothesesconclusionD.Var (ind A) = D.Pr A * (1 - D.Pr A) -
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 := Finset.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 probability distributions 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 probability distributions 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.
def toMeasure reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
For a finite probability distribution on a finite type 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)
theorem integral_toMeasure reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
Integral against the induced measure is the expectation. For any statistic g, the measure-theoretic integral of g against the design's induced probability measure equals its expectation.
Formal statement
hypotheses
conclusion
∫ x, g x ∂D.toMeasure = D.E g
Proof (Lean source)
theorem integral_toMeasure (g : Ω → ℝ) : ∫ x, g x ∂D.toMeasure = D.E g := by
rw [toMeasure, integral_finset_sum_measure]
· have h : ∀ z ∈ (Finset.univ : Finset Ω),
∫ x, g x ∂(ofReal (D.p z) • Measure.dirac z) = D.p z * g z := by
intro z _
rw [integral_smul_measure, integral_dirac, smul_eq_mul,
ENNReal.toReal_ofReal (D.p_nonneg z)]
rw [Finset.sum_congr rfl h]
rfl
· intro z _
exact (integrable_dirac (by simp)).smul_measure (by simp)
theorem toMeasure_real_setOf reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
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
hypotheses
conclusion
D.toMeasure.real {z | A z} = D.Pr A
Proof (Lean source)
theorem toMeasure_real_setOf (A : Ω → Prop) [DecidablePred A] :
D.toMeasure.real {z | A z} = D.Pr A := by
rw [← integral_indicator_one (Set.toFinite {z | A z}).measurableSet,
Pr, ← integral_toMeasure]
refine integral_congr_ae (Filter.Eventually.of_forall (fun z => ?_))
unfold ind
by_cases h : A z <;> simp [indicator, h]
theorem variance_toMeasure reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
Measure-theoretic variance equals the variance. For any statistic g, the measure-theoretic variance of g under the design's induced measure equals its design variance.
Formal statement
hypotheses
conclusion
variance g D.toMeasure = D.Var g
Proof (Lean source)
theorem variance_toMeasure (g : Ω → ℝ) : variance g D.toMeasure = D.Var g := by
rw [variance_eq_integral (measurable_of_finite g).aemeasurable, integral_toMeasure,
integral_toMeasure]
rfl
2 supporting declarations (lemmas, instances)
-
toMeasure_applylemma — The measure induced by a finite probability distribution 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 finite probability distribution on a finite type 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 3 core · 1 supporting This file constructs prodDesign, the finite product of a family of independent randomization designs. ★ prodDesign★ prodDesign_p★ E_prod_apply
Products of finite probability distributions
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.
def prodDesign reviewed
⚑ flagged
Causalean.Experimentation.DesignBased
For a finite, equality-comparable index set whose coordinate finite types are finite, a family of coordinate-specific finite probability distributions 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)
parameters
ι :
Type u_1
ι → Type u_2
D :
∀ i, FiniteDesign (α i)
def
given by
clause 1
p w := ∏ i, (D i).p (w i)
clause 2
p_nonneg w := Finset.prod_nonneg (fun i _ => (D i).p_nonneg (w i))
clause 3
p_sum := by rw [show (∑ w : ∀ i, α i, ∏ i, (D i).p (w i)) = ∏ i, ∑ a : α i, (D i).p a from by rw [Finset.prod_univ_sum]; rw [Fintype.piFinset_univ]] simp only [FiniteDesign.p_sum, Finset.prod_const_one]
lemma prodDesign_p reviewed
⚑ flagged
Causalean.Experimentation.DesignBased
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
hypotheses
conclusion
(prodDesign D).p w = ∏ i, (D i).p (w i)
Proof (Lean source)
@[simp] lemma prodDesign_p (D : ∀ i, FiniteDesign (α i)) (w : ∀ i, α i) :
(prodDesign D).p w = ∏ i, (D i).p (w i) := rfl
lemma E_prod_apply reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
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
hypotheses
conclusion
(prodDesign D).E (fun w => g (w j)) = (D j).E g
Proof (Lean source)
lemma E_prod_apply (D : ∀ i, FiniteDesign (α i)) (j : ι) (g : α j → ℝ) :
(prodDesign D).E (fun w => g (w j)) = (D j).E g := by
have hg : (fun w : ∀ i, α i => g (w j))
= (fun w => ∏ i, (fun (i : ι) (a : α i) => if h : i = j then g (h ▸ a) else 1) i (w i)) := by
funext w
simp only
rw [Finset.prod_dite_eq' univ j (fun i h => g (h ▸ w i))]
simp
rw [hg, E_prod_prod D (fun (i : ι) (a : α i) => if h : i = j then g (h ▸ a) else 1)]
rw [Finset.prod_eq_single j]
· congr 1
funext a
simp
· intro i _ hij
have hF : (fun a : α i => (if h : i = j then g (h ▸ a) else (1 : ℝ))) = (fun _ => 1) := by
funext a; rw [dif_neg hij]
rw [hF, (D i).E_const]
· intro h; exact absurd (Finset.mem_univ j) h
1 supporting declaration (lemmas, instances)
-
E_prod_prodlemma — 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).hypothesesconclusion(prodDesign D).E (fun w => ∏ i, g i (w i)) = ∏ i, (D i).E (g i)Proof (Lean source)
lemma E_prod_prod (D : ∀ i, FiniteDesign (α i)) (g : ∀ i, α i → ℝ) : (prodDesign D).E (fun w => ∏ i, g i (w i)) = ∏ i, (D i).E (g i) := by simp only [FiniteDesign.E, prodDesign_p] rw [show (∑ w : ∀ i, α i, (∏ i, (D i).p (w i)) * ∏ i, g i (w i)) = ∑ w : ∀ i, α i, ∏ i, ((D i).p (w i) * g i (w i)) from Finset.sum_congr rfl (fun w _ => by rw [Finset.prod_mul_distrib])] rw [Finset.prod_univ_sum, Fintype.piFinset_univ]
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.
theorem chebyshev reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
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
hypotheses
conclusion
D.Pr (fun z => ε ≤ |X z - D.E X|) ≤ D.Var X / ε ^ 2
Proof (Lean source)
theorem chebyshev (X : Ω → ℝ) {ε : ℝ} (hε : 0 < ε) :
D.Pr (fun z => ε ≤ |X z - D.E X|) ≤ D.Var X / ε ^ 2 := by
have hε2 : (0 : ℝ) < ε ^ 2 := pow_pos hε 2
-- Monotonicity of a finite sum (proved from scratch: the ordered-`BigOperators`
-- module is not in scope here, only the basic algebraic one).
have hmono : ∀ (s : Finset Ω) (a b : Ω → ℝ), (∀ i ∈ s, a i ≤ b i) →
∑ i ∈ s, a i ≤ ∑ i ∈ s, b i := by
intro s
induction s using Finset.induction with
| empty => intro a b _; simp
| insert x t hx ih =>
intro a b h
rw [Finset.sum_insert hx, Finset.sum_insert hx]
exact add_le_add (h x (Finset.mem_insert_self x t))
(ih a b (fun i hi => h i (Finset.mem_insert_of_mem hi)))
-- Core inequality: `ε² * Pr(event) ≤ Var X`.
have hcore : ε ^ 2 * D.Pr (fun z => ε ≤ |X z - D.E X|) ≤ D.Var X := by
-- Write both sides as `∑ z, D.p z * (…)`, then compare term by term.
have hlhs : ε ^ 2 * D.Pr (fun z => ε ≤ |X z - D.E X|)
= ∑ z, D.p z * (ε ^ 2 * (if ε ≤ |X z - D.E X| then (1 : ℝ) else 0)) := by
unfold FiniteDesign.Pr FiniteDesign.E FiniteDesign.ind
rw [Finset.mul_sum]
exact Finset.sum_congr rfl (fun z _ => by ring)
have hrhs : D.Var X = ∑ z, D.p z * (X z - D.E X) ^ 2 := rfl
rw [hlhs, hrhs]
refine hmono univ _ _ (fun z _ => ?_)
refine mul_le_mul_of_nonneg_left ?_ (D.p_nonneg z)
by_cases hz' : ε ≤ |X z - D.E X|
· simp only [hz', if_true, mul_one]
rw [← sq_abs (X z - D.E X)]
exact pow_le_pow_left₀ hε.le hz' 2
· simp only [hz', if_false, mul_zero]
exact sq_nonneg _
rw [le_div_iff₀ hε2, mul_comm]
exact hcore
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
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
Measure-theoretic bridges for finite-design 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
standard side conditions needed to reuse measure-theoretic results with finite designs.
lemma abs_Cov_le reviewed
⚑ flagged
Causalean.Experimentation.DesignBased.FiniteDesign
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
hypotheses
Proof (Lean source)
lemma abs_Cov_le (X Y : Ω → ℝ) :
|D.Cov X Y| ≤ sqrt (D.Var X) * sqrt (D.Var Y) := by
rw [D.Cov_eq_covariance X Y, D.Var_eq_variance X, D.Var_eq_variance Y]
exact abs_covariance_le_sqrt_mul (D.memLp_toMeasure X 2) (D.memLp_toMeasure Y 2)
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
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.
theorem prodDesign_toMeasure_eq_pi reviewed
⚑ flagged
Causalean.Experimentation.DesignBased
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
hypotheses
ι :
Type u_1
ι → Type u_2
D :
∀ i, FiniteDesign (α i)
conclusion
(prodDesign D).toMeasure = Measure.pi (fun i => (D i).toMeasure)
Proof (Lean source)
theorem prodDesign_toMeasure_eq_pi (D : ∀ i, FiniteDesign (α i)) :
(prodDesign D).toMeasure = Measure.pi (fun i => (D i).toMeasure) := by
refine Measure.ext_of_singleton (fun w => ?_)
-- LHS: the product-design measure of `{w}` is `∏ i, (D i).p (w i)`.
rw [FiniteDesign.toMeasure_singleton (prodDesign D) w, prodDesign_p,
ENNReal.ofReal_prod_of_nonneg (fun i _ => (D i).p_nonneg (w i))]
-- RHS: `{w} = Set.univ.pi (fun i => {w i})`, so `Measure.pi … {w} = ∏ i, (D i).toMeasure {w i}`.
have hsingleton : ({w} : Set (∀ i, α i)) = Set.univ.pi (fun i => {w i}) := by
ext x; simp [funext_iff]
rw [hsingleton, Measure.pi_pi]
exact Finset.prod_congr rfl (fun i _ => (FiniteDesign.toMeasure_singleton (D i) (w i)).symm)
theorem indepFun_prodDesign_blocks reviewed
⚑ flagged
Causalean.Experimentation.DesignBased
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
hypotheses
conclusion
IndepFun (fun (w : ∀ k, α k) (k : A) => w k) (fun w (k : B) => w k) (prodDesign D).toMeasure
Proof (Lean source)
theorem indepFun_prodDesign_blocks (D : ∀ i, FiniteDesign (α i)) {A B : Finset ι}
(hAB : Disjoint A B) :
IndepFun (fun (w : ∀ k, α k) (k : A) => w k) (fun w (k : B) => w k)
(prodDesign D).toMeasure :=
(iIndepFun_prodDesign_eval D).indepFun_finset A B hAB
(fun i => measurable_pi_apply i)
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.hypothesesconclusionIndepFun (fun w : ∀ k, α k => w i) (fun w => w j) (prodDesign D).toMeasureProof (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'conclusionIndepFun F G (prodDesign D).toMeasureProof (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)