Estimation.MinimaxATE
Structure-agnostic lower bounds for treatment-effect estimation: the oracle-vs-black-box reduction, least-favourable constructions, and variance calculations.
Model 14 core · 6 supporting This file supplies the finite observed-data experiment used for structure-agnostic estimation of the average treatment effect: a finite covariate, binary treatment, and binary outcome. ★ nMiss_sq_le_nMSE
Finite observed-data model for ATE estimation
This file supplies the finite observed-data experiment used for structure-agnostic estimation of the average treatment effect: a finite covariate, binary treatment, and binary outcome. It defines the data laws, nuisance class, sample risks, and minimax miss probability used by the lower-bound construction.
For a covariate space, one observed data record consists of a covariate value, a binary treatment indicator, and a binary outcome indicator.
A data-generating process (m, g) is valid when the propensity m takes values in the unit interval [0,1] and each outcome-regression arm g d also takes values in [0,1].
For a finite covariate space, a propensity function, an outcome-regression function for binary treatment, and an observed record, the record’s real-valued probability mass is the uniform covariate mass times the conditional treatment probability times the conditional outcome probability.
For a finite nonempty covariate space, a propensity function, an outcome-regression function, and evidence that these functions define valid probabilities, the single-observation probability mass function assigns each record its nonnegative real-valued mass.
Definition (Lean source)
For a finite nonempty covariate space with a measurable structure, a propensity function, an outcome-regression function, and evidence that these functions define valid probabilities, the single-observation probability measure is the measure associated with the corresponding finite probability mass function.
For a finite covariate space and an outcome-regression function for binary treatment, the average treatment effect is the uniform average over covariate values of the treated-arm regression minus the control-arm regression.
For a finite covariate space, a first real-valued covariate function, and a second real-valued covariate function, the squared uniform distance is the uniform average of their squared pointwise difference.
Definition (Lean source)
Structure-agnostic nuisance class. A candidate data-generating process (m, g) belongs to the class ℱ(εg, εm) around fixed nuisance estimates (mhat, ghat) when it is a valid DGP, with propensity and both outcome-regression arms taking values in [0,1], each outcome-regression arm lies within squared L²(P_X) distance εg of the corresponding estimated arm, and the propensity lies within squared L²(P_X) distance εm of the estimated propensity.
For a finite covariate space, a reference propensity function, a reference outcome-regression function, an outcome-regression error budget, and a propensity error budget, an in-class data-generating process is a pair of propensity and outcome-regression functions together with evidence that the pair belongs to the corresponding nuisance class.
For a finite nonempty covariate space with a measurable structure, a propensity function, an outcome-regression function, evidence that the functions define valid probabilities, and a nonnegative sample size, the sample probability law is the joint law of that many independent observations from the single-observation law.
For a finite nonempty covariate space with a measurable structure, a propensity function, an outcome-regression function, evidence that the functions define valid probabilities, a nonnegative sample size, an estimator based on that sample, and a real-valued threshold, the miss probability is the probability that the estimator differs from the true average treatment effect by at least the threshold.
For a finite nonempty covariate space with a measurable structure, a propensity function, an outcome-regression function, evidence that the functions define valid probabilities, a nonnegative sample size, and an estimator based on that sample, the mean-squared error is the expected squared deviation of the estimator from the true average treatment effect.
Chebyshev/Markov bridge. For a valid data-generating process (m, g) and a nonnegative separation threshold s, the squared threshold times the probability that an estimator misses the true average treatment effect by at least s, on n i.i.d. draws, is at most the estimator's mean-squared error. This is the quantitative form of the paper's observation that the quantile risk lower bound implies the expected-risk one (𝔐ₙ,γ ≥ ρ ⟹ minimax 𝔼-risk ≥ (1−γ)ρ`).
Formal statement
Proof (Lean source)
For a finite nonempty covariate space with a measurable structure, a reference propensity function, a reference outcome-regression function, an outcome-regression error budget, a propensity error budget, a nonnegative sample size, an estimator based on that sample, and a real-valued threshold, the minimax miss probability is the supremum, over all data-generating processes in the specified nuisance class, of the probability that the estimator differs from that process’s true average treatment effect by at least the threshold.
Definition (Lean source)
6 supporting declarations (lemmas, instances)
-
obsReal_sumtheorem — The total mass of obsReal is 1 (for nonempty C): summing over Y gives 1, then over D gives 1, then over X gives card C · (1/card C) = 1.hypothesesProof (Lean source)
theorem obsReal_sum [Nonempty C] (m : C → ℝ) (g : Bool → C → ℝ) : ∑ z : Obs C, obsReal m g z = 1 := by have hC : (Fintype.card C : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr Fintype.card_ne_zero -- summing over `Y` then `D` collapses each cell to its mass `1/card C` have key : ∑ z : Obs C, obsReal m g z = ∑ _x : C, (Fintype.card C : ℝ)⁻¹ := by rw [Fintype.sum_prod_type] refine Finset.sum_congr rfl fun x _ => ?_ rw [Fintype.sum_prod_type] simp only [obsReal, Fintype.sum_bool, Bool.false_eq_true, if_false, if_true] ring rw [key, Finset.sum_const, Finset.card_univ, nsmul_eq_mul] field_simp -
obsReal_nonnegtheorem — Nonnegativity of obsReal for a valid DGP.hypothesesconclusion0 ≤ obsReal m g zProof (Lean source)
theorem obsReal_nonneg {m : C → ℝ} {g : Bool → C → ℝ} (hv : ValidDGP m g) (z : Obs C) : 0 ≤ obsReal m g z := by have hCinv : (0 : ℝ) ≤ (Fintype.card C : ℝ)⁻¹ := by positivity obtain ⟨hm0, hm1⟩ := hv.m_mem z.1 refine mul_nonneg (mul_nonneg hCinv ?_) ?_ · rcases z.2.1 with _ | _ <;> simp <;> linarith · obtain ⟨hg0, hg1⟩ := hv.g_mem z.2.1 z.1 rcases z.2.2 with _ | _ <;> simp <;> linarith -
obsLaw_isProbinstance — For every finite, nonempty covariate space equipped with a $\sigma$-algebra, propensity function $m$, binary-treatment outcome-regression function $g$, and evidence that these functions constitute a valid data-generating process, the corresponding single-observation law is a probability measure. -
productLaw_isProbinstance — For every finite, nonempty covariate space equipped with a $\sigma$-algebra, propensity function $m$, binary-treatment outcome-regression function $g$, evidence that these functions constitute a valid data-generating process, and sample size $n$, the corresponding independent-sample law is a probability measure.parametersinstancegiven byby unfold productLaw; infer_instance -
bddAbove_nMiss_rangetheorem — Each in-class miss probability is bounded above by 1 (it is a probability), so the range of nMiss over the class is bounded above.hypothesesconclusionProof (Lean source)
theorem bddAbove_nMiss_range [Nonempty C] (mhat : C → ℝ) (ghat : Bool → C → ℝ) (εg εm : ℝ) (n : ℕ) (est : (Fin n → Obs C) → ℝ) (s : ℝ) : BddAbove (Set.range fun p : InClassDGP mhat ghat εg εm => nMiss p.2.valid n est s) := by refine ⟨1, ?_⟩ rintro y ⟨p, rfl⟩ unfold nMiss calc (productLaw p.2.valid n).real {x | s ≤ |est x - ate p.1.2|} ≤ (productLaw p.2.valid n).real univ := measureReal_mono (Set.subset_univ _) (measure_ne_top _ _) _ = 1 := by rw [probReal_univ] -
nMiss_le_minimaxMisstheorem — A specific in-class DGP's miss probability is ≤ minimaxMiss.hypothesesεg εm :ℝs :ℝp :conclusionProof (Lean source)
theorem nMiss_le_minimaxMiss [Nonempty C] {mhat : C → ℝ} {ghat : Bool → C → ℝ} {εg εm : ℝ} {n : ℕ} {est : (Fin n → Obs C) → ℝ} {s : ℝ} (p : InClassDGP mhat ghat εg εm) : nMiss p.2.valid n est s ≤ minimaxMiss mhat ghat εg εm n est s := le_ciSup (bddAbove_nMiss_range mhat ghat εg εm n est s) p
Optimality 4 core · 2 supporting This file combines the cell-varying minimax converse with the finite-sample AIPW upper bound. ★ aipw_inclass_bias_bound★ aipw_minimaxMiss_le
Finite-Sample AIPW Lower and Upper Bounds
This file combines the cell-varying minimax converse with the finite-sample AIPW upper bound.
The file first proves finite-sample facts for the fixed-center AIPW estimator: aipw_mean_eq
identifies its mean, aipw_nMiss_le turns a bias and variance bound into a miss-probability
bound, aipw_inclass_bias_bound supplies the uniform product-bias estimate over InClass, and
aipw_minimaxMiss_le lifts these bounds to the minimax miss probability. It then defines
FiniteSampleTwoThresholdBounds and assembles the two finite-sample inequalities in
aipw_finiteSample_twoThreshold_bounds. No comparison between the lower and upper separation,
positivity of the lower separation, or asymptotic rate claim is included.
In-class bias bound. For a positive overlap threshold ε such that the fixed propensity estimate mhat stays at least ε away from both 0 and 1 at every covariate value, and for any data-generating process (m, g) lying in the structure-agnostic nuisance class around the fixed estimates (mhat, ghat) with error budgets εg, εm, the plug-in bias of the fixed-center AIPW estimator's population score is at most ε⁻¹·2·√εg·√εm.
Formal statement
Proof (Lean source)
Worst-case (minimax) miss bound for AIPW. Suppose the fixed nuisance estimates (mhat, ghat) are themselves valid, for a positive overlap threshold ε such that mhat stays at least ε away from 0 and 1 everywhere, nonnegative error budgets εg, εm, a positive sample size n, and a separation s exceeding the uniform bias bound b = ε⁻¹·2·√εg·√εm. Then the worst-case-over-class miss probability of the fixed-center AIPW estimator at separation s is at most ((1+2/ε)²/n)/(s−b)².
Formal statement
Proof (Lean source)
For fixed nuisance centers, error budgets, and a sample size, the finite-sample two-threshold bounds package a lower miss bound for every measurable estimator at one separation and an upper miss bound for one estimator at another. They do not assert that the separations are positive, ordered, or comparable in rate.
Definition (Lean source)
For a cell-varying construction over a nonzero finite number of paired covariate cells, a positive sample size, and nonnegative outcome-regression and propensity-error budgets, suppose for every pair , the squared propensity perturbation is at most , for every pair , the squared treated-arm outcome-regression perturbation is at most , the normalized overlap coefficients satisfy , and their normalized squared sum satisfies . For a positive overlap constant such that the fitted propensity is between and in every covariate cell, and a separation strictly larger than , the finite-sample two-threshold bounds specify the fixed-center augmented inverse-probability-weighted estimator, its upper miss-probability bound at , and the construction-induced lower miss-probability bound for every measurable estimator.
Definition (Lean source)
2 supporting declarations (lemmas, instances)
-
aipw_mean_eqtheorem — The mean of the AIPW estimator equals the single-observation population mean of the score (mean of an i.i.d. average), for n > 0.hypothesesconclusion∫ sample, estAIPW mhat ghat n sample ∂(productLaw hv n)Proof (Lean source)
theorem aipw_mean_eq {m : C → ℝ} {g : Bool → C → ℝ} (hv : ValidDGP m g) (mhat : C → ℝ) (ghat : Bool → C → ℝ) {n : ℕ} (hn : 0 < n) : ∫ sample, estAIPW mhat ghat n sample ∂(productLaw hv n) = ∑ z : Obs C, obsReal m g z * aipwScoreFin mhat ghat z := by have hne : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne' have hper : ∀ i : Fin n, ∫ sample, aipwScoreFin mhat ghat (sample i) ∂(productLaw hv n) = ∑ z : Obs C, obsReal m g z * aipwScoreFin mhat ghat z := by intro i have hmap : (productLaw hv n).map (fun s : Fin n → Obs C => s i) = obsLaw hv := by rw [productLaw]; exact (measurePreserving_eval (fun _ : Fin n => obsLaw hv) i).map_eq rw [← aipw_pop_mean hv mhat ghat, ← integral_map (φ := fun s : Fin n → Obs C => s i) (measurable_pi_apply i).aemeasurable (measurable_of_finite _).aestronglyMeasurable, hmap] unfold estAIPW rw [integral_const_mul, integral_finset_sum _ (fun i _ => Integrable.of_finite)] simp_rw [hper] rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, ← mul_assoc, inv_mul_cancel₀ hne, one_mul] -
aipw_nMiss_letheorem — Per-DGP Chebyshev miss bound. If the plug-in bias is ≤ b and the variance is ≤ V, then for any separation s > b the miss probability is ≤ V / (s − b)².hypothesesProof (Lean source)
theorem aipw_nMiss_le {m : C → ℝ} {g : Bool → C → ℝ} (hv : ValidDGP m g) (mhat : C → ℝ) (ghat : Bool → C → ℝ) {n : ℕ} (hn : 0 < n) {b V s : ℝ} (hbias : |(∑ z : Obs C, obsReal m g z * aipwScoreFin mhat ghat z) - ate g| ≤ b) (hvar : variance (estAIPW mhat ghat n) (productLaw hv n) ≤ V) (hsb : b < s) : nMiss hv n (estAIPW mhat ghat n) s ≤ V / (s - b) ^ 2 := by have hsub0 : 0 < s - b := by linarith set μ' := productLaw hv n with hμ' set X := estAIPW mhat ghat n with hX have hmem : MemLp X 2 μ' := ⟨(measurable_of_finite _).aestronglyMeasurable, eLpNorm_lt_top_of_finite⟩ have hmean : ∫ a, X a ∂μ' = ∑ z : Obs C, obsReal m g z * aipwScoreFin mhat ghat z := aipw_mean_eq hv mhat ghat hn have hEbias : |(∫ a, X a ∂μ') - ate g| ≤ b := by rw [hmean]; exact hbias have hsubset : {sample | s ≤ |X sample - ate g|} ⊆ {sample | s - b ≤ |X sample - ∫ a, X a ∂μ'|} := by intro sample hsample simp only [Set.mem_setOf_eq] at hsample ⊢ have htri : |X sample - ate g| ≤ |X sample - ∫ a, X a ∂μ'| + |(∫ a, X a ∂μ') - ate g| := abs_sub_le _ _ _ linarith have hvar0 : 0 ≤ variance X μ' := variance_nonneg _ _ calc nMiss hv n X s = μ'.real {sample | s ≤ |X sample - ate g|} := rfl _ ≤ μ'.real {sample | s - b ≤ |X sample - ∫ a, X a ∂μ'|} := measureReal_mono hsubset (measure_ne_top _ _) _ ≤ variance X μ' / (s - b) ^ 2 := by rw [Measure.real] refine (ENNReal.toReal_mono ENNReal.ofReal_ne_top (meas_ge_le_variance_div_sq hmem hsub0)).trans ?_ rw [ENNReal.toReal_ofReal (by positivity)] _ ≤ V / (s - b) ^ 2 := by gcongr