Estimation.MinimaxATE.Reduction
The reduction from estimation risk to testing between mixture alternatives, including witness-mixture constructions.
Bump 1 core · 3 supporting This file provides finite squared-distance identities for functions on a covariate space. ★ l2sq_bump
Squared-Distance Bump Algebra
This file provides finite squared-distance identities for functions on a covariate
space. It proves the basic algebraic facts l2sq_self, l2sq_comm, and l2sq_nonneg, then
records the Rademacher-bump identity l2sq_bump: if a x = b x + δ * σ x and every sign satisfies
(σ x)^2 = 1, then the squared distance from a to b is exactly δ^2 on a nonempty finite
space. This is the reusable membership calculation for lower-bound perturbations that are placed
on the boundary of an InClass budget.
Constant-magnitude (Rademacher) bump. If a sign function σ satisfies (σ x)² = 1 at every covariate value, then on a nonempty finite covariate space, the squared L²(P_X) distance between b shifted by δ·σ and b itself equals δ². This is exactly what makes a Rademacher-bump perturbation land on the boundary of the nuisance class ℱ(ε,·) when δ = √ε.
Formal statement
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
l2sq_nonnegtheorem — l2sq is nonnegative.Proof (Lean source)
theorem l2sq_nonneg (a b : C → ℝ) : 0 ≤ l2sq a b := by rw [l2sq] refine mul_nonneg ?_ ?_ · exact inv_nonneg.mpr (Nat.cast_nonneg _) · exact sum_nonneg fun x _ => sq_nonneg _
Witness 2 core · 1 supporting This file defines the abstract two-point witness used in structure-agnostic ATE lower bounds. ★ twoPointWitness_lower_bound
Two-Point Reduction
This file defines the abstract two-point witness used in structure-agnostic ATE lower bounds. It turns a pair of statistically close sample laws with separated ATEs and in-class realizability into a minimax lower bound for the worst-case probability of estimator error.
The structure TwoPointWitness packages the two sample laws, their ATE labels, a separation
half-scale, a total-variation budget, and the domination condition connecting each witness law to
minimaxMiss. The theorem twoPointWitness_lower_bound gives the Le Cam lower bound
(1 - c) / 2, and twoPointWitness_quarter specializes it to the common c ≤ 1/2 case used by
the explicit minimax constructions.
Two-point (Le Cam) witness for the structure-agnostic ATE lower bound: it bundles two n-sample data laws, indexed by a hypothesis label j : Bool, together with the data needed to run Le Cam's two-point method. For each hypothesis, Q j is a probability measure with true average treatment effect θ j; the two hypotheses' ATE values are separated by at least twice the half-scale s, while the total-variation distance between the two laws is bounded by c, and for every estimator the probability under Q j of missing θ j by s is dominated by the in-class minimax miss probability — the realizability condition that a mixture-of-in-class-DGPs construction discharges.
Definition (Lean source)
Structure-agnostic two-point lower bound. Given a two-point (Le Cam) witness W packaging two statistically close n-sample laws with separated true average-treatment-effect values, for any measurable estimator, the worst-case-over-class probability that it misses the true ATE by W.s is at least (1 − W.c)/2. The proof is two_point_lower_bound_of_tvDist_le applied to the two witness laws, followed by the realizability domination.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
twoPointWitness_quartertheorem — A witness with total-variation budget c ≤ 1/2 forces every estimator to miss the true ATE by W.s with probability at least 1/4 somewhere in the class.Proof (Lean source)
theorem twoPointWitness_quarter (W : TwoPointWitness C n mhat ghat εg εm) (hc : W.c ≤ 1 / 2) {est : (Fin n → Obs C) → ℝ} (hest : Measurable est) : 1 / 4 ≤ minimaxMiss mhat ghat εg εm n est W.s := by refine le_trans ?_ (twoPointWitness_lower_bound W hest) linarith
WitnessMixture 1 core · 0 supporting This file proves a mixture version of the two-point lower-bound argument for structure-agnostic average-treatment-effect estimation. ★ mixture_two_point_lower_bound
Mixture Two-Point Reduction
This file proves a mixture version of the two-point lower-bound argument for structure-agnostic average-treatment-effect estimation. It handles a null in-class DGP and a finite weighted family of in-class alternatives whose treatment effects are each separated from the null, without requiring the alternatives to share one common ATE.
The main theorem mixture_two_point_lower_bound combines the total-variation testing inequality
with mixtureReal_le and nMiss_le_minimaxMiss: the null miss event is dominated directly, while
the complement of the null miss event is contained in each alternative's own miss event by the
per-component separation.
Mixture two-point lower bound (one-sided separation). Suppose a null data-generating process (m₀, g₀) lies in the structure-agnostic nuisance class and a finite family of alternative data-generating processes (mlam i, glam i) also lie in the class, with nonnegative mixture weights w summing to 1, where every alternative's average treatment effect is at least 2s away from the null's, and the null's n-sample law and the weighted mixture of the alternatives' n-sample laws are at total-variation distance at most c. Then for any measurable estimator of the average treatment effect, the worst-case-over-class probability that it misses the true ATE by s is at least (1 − c)/2. Unlike TwoPointWitness, the alternatives need not share a common ATE — only 2 s ≤ |ate g₀ − ate (glam i)| per component.