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 defines the finite observed-data experiment used for structure-agnostic ATE estimation. ★ nMiss_sq_le_nMSE
Finite Observed-Data Model
This file defines the finite observed-data experiment used for structure-agnostic ATE estimation.
The covariate space is an arbitrary finite type C, treatment and outcome are binary, and one
observation is Obs C = C × Bool × Bool.
Main declarations:
* ValidDGP, obsReal, obsPMF, and obsLaw build a valid data-generating process and its
single-observation law, with obsReal_sum, obsReal_nonneg, and obsLaw_isProb recording the
finite probability facts.
* ate and l2sq define the average treatment effect and squared L²(P_X) nuisance distance.
* InClass and InClassDGP package the structure-agnostic nuisance class around fixed estimates.
* productLaw, nMiss, nMSE, and minimaxMiss define the sample law, miss probability,
expected squared error, and worst-case-over-class miss probability.
* nMiss_sq_le_nMSE connects probability-of-miss lower bounds to mean-squared-error lower
bounds, and nMiss_le_minimaxMiss embeds an in-class DGP's miss probability into the minimax
supremum.
One observation: covariate X : C, treatment D : Bool, outcome Y : Bool.
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].
The real-valued mass the DGP (m, g) assigns to the observation z = (x, d, y): (1/card C) · P(D = d | x) · P(Y = y | d, x).
The single-observation law of the DGP (m, g) as a probability PMF.
Definition (Lean source)
The single-observation law of the DGP (m, g) as a probability Measure.
The average treatment effect (1/card C) Σ_x (g true x − g false x). Depends only on the outcome regression g.
The squared L²(P_X) distance (1/card C) Σ_x (a x − b x)² between two functions of the covariate.
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.
A DGP packaged with a proof that it lies in the class ℱ(εg, εm).
Definition (Lean source)
The n-sample data law: the product Measure.pi of n independent copies of the single-observation law.
The probability that the estimator est, run on n samples from the DGP (m, g), misses the true ATE ate g by at least s.
The mean-squared error of est on n samples from the DGP (m, g): the expected squared deviation from the true ATE ate g. This is the expected-risk functional whose minimax lower bound the paper (Jin–Syrgkanis 2024, eq. for 𝔐ⁿ,γ) deduces — as the weaker (1−γ)-factor consequence — from the quantile (probability-of-miss) form.
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)
Minimax (worst-case-over-class) miss probability. The supremum over all in-class DGPs of the probability that est misses that DGP's true ATE by s. A lower bound on this quantity is a minimax lower bound: no estimator can be within s of the truth with high probability uniformly over the class.
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.Proof (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.Proof (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 — The single-observation law of any valid data-generating process is a probability measure.instance obsLaw_isProb [Nonempty C] {m : C → ℝ} {g : Bool → C → ℝ} (hv : ValidDGP m g) : IsProbabilityMeasure (obsLaw hv) := by unfold obsLaw; infer_instance -
productLaw_isProbinstance — The independent sample law of any valid data-generating process is a probability measure.instance productLaw_isProb [Nonempty C] {m : C → ℝ} {g : Bool → C → ℝ} (hv : ValidDGP m g) (n : ℕ) : IsProbabilityMeasure (productLaw hv n) := by 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.hypothesesconclusionnMiss p.2.valid n est s ≤ minimaxMiss mhat ghat εg εm n est sProof (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)
Capstone — DR/AIPW attains the structure-agnostic minimax rate. For the cell-varying construction P with the per-pair budgets and regularity conditions of the lower bound, the problem exhibits a MinimaxRateThreshold:
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