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.
Definition (Lean source)
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. -
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
AIPW Optimality
This file combines the cell-varying minimax converse with the finite-sample AIPW upper bound. It records that the structure-agnostic ATE minimax rate is of product-bias order and that the AIPW estimator attains this order up to constants.
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
MinimaxRateThreshold and assembles the lower and upper bounds in aipw_attains_minimax_rate,
showing that the cell-varying lower-bound construction and the AIPW upper bound have matching
sqrt(εg * εm) separation order.
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)
Minimax rate threshold (reusable vocabulary). An estimation problem over the finite model exhibits a rate threshold when a single estimator's worst-case miss is bounded above at one separation (sepUpper), while every estimator's worst-case miss is bounded below at a (smaller) separation (sepLower). When sepLower and sepUpper are of the same order, this certifies the minimax rate and that estimator attains it.
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 minimax-rate threshold certificate specifies 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