Experimentation.Design­Based.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

For a randomization design, a real-valued variance estimator, and a real-valued statistic of the realized assignment, the assertion that the estimator is conservative means that its design expectation is at least the design variance of the statistic.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
D :
FiniteDesign Ω
shared
Vhat X :
Ω → ℝ
def
IsConservativeVarEst D Vhat X :
Prop
given by
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
Ω :
Type u_1
shared
D :
FiniteDesign Ω
shared
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:58 · uses FiniteDesign , E , IsConservativeVarEst , Pr
2 supporting declarations (lemmas, instances)