Experimentation.DesignBased.Variance

This namespace collects variance-estimation tools for finite design-based experiments.

Conservative 2 core · 2 supporting Conservative variance estimators have expectation at least the true finite-design variance. ★ chebyshev_conservative

Conservative variance estimators

Conservative variance estimators have expectation at least the true finite-design variance.

FiniteDesign.IsConservativeVarEst states the comparison Var X <= E[Vhat]. The lemmas FiniteDesign.isConservativeVarEst_of_E_eq_add and FiniteDesign.isConservativeVarEst_of_unbiased give common certification patterns, and FiniteDesign.chebyshev_conservative turns conservativeness into a valid Chebyshev tail bound with E[Vhat] in place of the unknown variance.

def IsConservativeVarEst reviewed

Causalean.Experimentation.DesignBased.FiniteDesign

A variance estimator Vhat is conservative for X when its expectation is at least the randomization variance of X.

Definition (Lean source)

def IsConservativeVarEst (Vhat X : Ω → ℝ) : Prop := D.Var X ≤ D.E Vhat

Causalean.Experimentation.DesignBased.FiniteDesign.IsConservativeVarEst · Causalean/Experimentation/DesignBased/Variance/Conservative.lean:41 · uses FiniteDesign

theorem chebyshev_conservative reviewed

Causalean.Experimentation.DesignBased.FiniteDesign

Conservative Chebyshev bound. If the design expectation of a proposed variance estimator V̂ is at least the randomization variance of X, then for any positive threshold ε, the probability that X deviates from its mean by at least ε is bounded by that expected estimator divided by ε².

Formal statement

hypotheses

Vhat X :

Ω → ℝ

hcons :

D.IsConservativeVarEst Vhat X

ε :

ℝ

hε :

0 < ε

conclusion

D.Pr (fun z => ε ≤ |X z - D.E X|) ≤ D.E Vhat / ε ^ 2

Proof (Lean source)

theorem chebyshev_conservative {Vhat X : Ω → ℝ} (hcons : D.IsConservativeVarEst Vhat X) {ε : ℝ} (hε : 0 < ε) : D.Pr (fun z => ε ≤ |X z - D.E X|) ≤ D.E Vhat / ε ^ 2 := by have hε2 : (0 : ℝ) < ε ^ 2 := pow_pos hε 2 have hc : D.Var X ≤ D.E Vhat := hcons calc D.Pr (fun z => ε ≤ |X z - D.E X|) ≤ D.Var X / ε ^ 2 := D.chebyshev X hε _ ≤ D.E Vhat / ε ^ 2 := by gcongr

Causalean.Experimentation.DesignBased.FiniteDesign.chebyshev_conservative · Causalean/Experimentation/DesignBased/Variance/Conservative.lean:56 · uses FiniteDesign , E , IsConservativeVarEst , Pr

2 supporting declarations (lemmas, instances)

isConservativeVarEst_of_E_eq_add lemma — A variance estimator whose expectation equals the variance plus a nonnegative bias is conservative.

hypotheses

Vhat X :

Ω → ℝ

B :

ℝ

hB :

0 ≤ B

h :

D.E Vhat = D.Var X + B

conclusion

D.IsConservativeVarEst Vhat X

Proof (Lean source)

lemma isConservativeVarEst_of_E_eq_add {Vhat X : Ω → ℝ} {B : ℝ} (hB : 0 ≤ B) (h : D.E Vhat = D.Var X + B) : D.IsConservativeVarEst Vhat X := by rw [IsConservativeVarEst, h]; exact le_add_of_nonneg_right hB

Causalean.Experimentation.DesignBased.FiniteDesign.isConservativeVarEst_of_E_eq_add · Causalean/Experimentation/DesignBased/Variance/Conservative.lean:45
isConservativeVarEst_of_unbiased lemma — An unbiased variance estimator (its expectation equals the variance) is conservative.

hypotheses

Vhat X :

Ω → ℝ

h :

D.E Vhat = D.Var X

conclusion

D.IsConservativeVarEst Vhat X

Proof (Lean source)

lemma isConservativeVarEst_of_unbiased {Vhat X : Ω → ℝ} (h : D.E Vhat = D.Var X) : D.IsConservativeVarEst Vhat X := by rw [IsConservativeVarEst, h]

Causalean.Experimentation.DesignBased.FiniteDesign.isConservativeVarEst_of_unbiased · Causalean/Experimentation/DesignBased/Variance/Conservative.lean:51

Experimentation.Design­Based.Variance

Conservative variance estimators

Experimentation.DesignBased.Variance