Estimation.MinimaxATE.ConstCenterGeneral
General constant-center least-favourable construction for MinimaxATE: mixture laws, class membership, χ² overlap, gap, MSE, and lower-bound assembly.
Construction 7 core · 3 supporting This file generalizes the structure-agnostic ATE lower-bound construction from the centered half-probability nuisance estimates to arbitrary constant nuisance centers bounded away from zero and one. ★ validDGP_hatG★ validDGP_pertG
General Constant-Center Lower-Bound Construction
This file generalizes the structure-agnostic ATE lower-bound construction from the centered half-probability nuisance estimates to arbitrary constant nuisance centers bounded away from zero and one. It defines the perturbed data-generating process and proves that the resulting propensity and outcome functions are valid probability functions.
The record GenConstr stores the bump sizes α, β, the constant center
(m₀, g₀, g₁), and the inequalities that keep the perturbation in [0,1].
The public definitions mhatG, ghatG, mPertG, and gPertG give the null
and sign-indexed perturbed DGPs, while validDGP_hatG and validDGP_pertG
establish their finite-model validity.
General-constant-center construction data. This record packages two nonnegative Rademacher-bump magnitudes together with a constant nuisance center (m₀, g₀, g₁) with each coordinate strictly between zero and one, and four further inequalities — the propensity bump smaller than the treated center, the outcome bump at most the treated center, and two worst-case upper bounds keeping the perturbed propensity and treated-arm regression at most one — that together certify the perturbed propensity and outcome-regression functions built from this data stay in the unit interval.
Definition (Lean source)
The constant propensity center as a function of the covariate.
The constant outcome-regression center: g₁ on the treated arm, g₀ on control.
The perturbed propensity mλ = m₀·(1 − (β/g₁)·Δ).
The perturbed outcome regression: control arm = g₀, treated arm gλ(1,·) = (g₁ + α·Δ)/(1 − (β/g₁)·Δ).
The null constant-center data-generating process, with propensity m₀ and outcome regressions (g₀, g₁), is a valid finite observed-data model, i.e. all its component probabilities lie in [0,1].
For any Rademacher sign vector lam indexing the perturbation, the perturbed propensity and outcome-regression functions define a valid finite observed-data model, i.e. take values in [0,1].
Proof (Lean source)
3 supporting declarations (lemmas, instances)
-
ratio_nonnegtheorem — 0 < β/g₁ is false in general (β may be 0); but 0 ≤ β/g₁ always.conclusion0 ≤ P.β / P.g₁Proof (Lean source)
theorem ratio_nonneg : 0 ≤ P.β / P.g₁ := div_nonneg P.hβ P.hg₁0.le -
ratio_lt_onetheorem — β/g₁ < 1 since β < g₁.conclusionP.β / P.g₁ < 1Proof (Lean source)
theorem ratio_lt_one : P.β / P.g₁ < 1 := (div_lt_one P.hg₁0).mpr P.hβg₁ -
denomG_postheorem — The denominator 1 − (β/g₁)·Δ is positive: Δ ≤ 1 gives 1 − (β/g₁)·Δ ≥ 1 − β/g₁ > 0.
ChiSqOverlap 3 core · 1 supporting This file derives the closed-form single-observation chi-squared overlap for two general constant-center Rademacher perturbations relative to the null law. ★ chiSqOverlap_eqG
General-Center Chi-Squared Second-Moment Overlap
This file derives the closed-form single-observation chi-squared overlap for two general constant-center Rademacher perturbations relative to the null law. The formula isolates the per-cell overlap coefficient that feeds the Ingster second-moment argument, with the linear perturbation terms canceling by construction. "Overlap" here is the χ² second-moment overlap of two likelihood ratios, not the causal positivity/overlap condition.
The definition Γ is the per-cell coefficient, chiSqOverlapG is the raw
single-observation overlap, obsReal_pertG_eq gives the denominator-free
observed-mass formula for the four treatment/outcome cells, and
chiSqOverlap_eqG proves the closed form
1 + (Γ / K) * ∑ j, signOf (lam j) * signOf (lam' j).
The per-cell χ²-overlap coefficient.
Definition (Lean source)
The single-observation χ² second-moment overlap of two perturbed laws relative to the null.
For any two Rademacher sign vectors lam and lam' indexing perturbed data-generating processes, the single-observation χ² overlap between them equals one plus the per-cell coefficient Γ/K times the sum of pairwise sign agreements between lam and lam'.
Formal statement
Proof (Lean source)
1 supporting declaration (lemmas, instances)
-
obsReal_pertG_eqtheorem — Denominator-free value of the perturbed observed mass obsReal mλ gλ at the four (d, y) combinations. The treated arm's denominator 1 − (β/g₁)Δ cancels against mλ = m₀·(1 − (β/g₁)Δ).hypothesesconclusionobsReal (P.mPertG lam) (P.gPertG lam) (x, d, y)= (card (Fin K × Bool) : ℝ)⁻¹ * (match d, y with | true, true => P.m₀ * (P.g₁ + P.α * Δ lam x) | true, false => P.m₀ * ((1 - P.g₁) - (P.α + P.β / P.g₁) * Δ lam x) | false, true => (1 - P.m₀ + P.m₀ * (P.β / P.g₁) * Δ lam x) * P.g₀ | false, false => (1 - P.m₀ + P.m₀ * (P.β / P.g₁) * Δ lam x) * (1 - P.g₀))Proof (Lean source)
theorem obsReal_pertG_eq (lam : Fin K → Bool) (x : Fin K × Bool) (d y : Bool) : obsReal (P.mPertG lam) (P.gPertG lam) (x, d, y) = (card (Fin K × Bool) : ℝ)⁻¹ * (match d, y with | true, true => P.m₀ * (P.g₁ + P.α * Δ lam x) | true, false => P.m₀ * ((1 - P.g₁) - (P.α + P.β / P.g₁) * Δ lam x) | false, true => (1 - P.m₀ + P.m₀ * (P.β / P.g₁) * Δ lam x) * P.g₀ | false, false => (1 - P.m₀ + P.m₀ * (P.β / P.g₁) * Δ lam x) * (1 - P.g₀)) := by have hd : (1 - (P.β / P.g₁) * Δ lam x) ≠ 0 := (P.denomG_pos lam x).ne' have hg₁ne : P.g₁ ≠ 0 := ne_of_gt P.hg₁0 have hden : P.g₁ - P.β * Δ lam x ≠ 0 := by rcases Δ_mem lam x with h | h <;> rw [h] <;> · have := P.hβg₁; have := P.hβ; intro hc; nlinarith unfold obsReal mPertG gPertG cases d <;> cases y <;> simp only [Bool.false_eq_true, if_false, if_true] <;> rw [mul_assoc] <;> refine congrArg _ ?_ <;> field_simp <;> ring
LowerBound 4 core · 12 supporting This file assembles the general constant-center construction for structure-agnostic ATE estimation into a two-point minimax lower bound. ★ minimax_lower_bound_gen
General-Center Lower Bound
This file assembles the general constant-center construction for structure-agnostic ATE
estimation into a two-point minimax lower bound. It defines the null sample law QfalseG, the
sign-indexed perturbed sample laws QpertG, and the Rademacher-mixture alternative QtrueG,
then proves their probability-measure facts.
The main calculations are one_add_chiSqDiv_QtrueG_QfalseG, which expresses the mixture
second moment through the general-center overlap coefficient, chiSqDiv_QtrueG_QfalseG_le_one,
which applies the Ingster bound under the Γ sample-size regime, and
tvDist_QfalseG_QtrueG_le_half, which converts chi-squared control to total variation. The
capstone minimax_lower_bound_gen shows that every measurable estimator misses by the
general-center product-rate scale somewhere in the structure-agnostic nuisance class.
The null n-sample law P̂^⊗n.
The perturbed n-sample law Qλ^⊗n.
The alternative n-sample law: the uniform Rademacher mixture of the perturbed laws.
Structure-agnostic minimax lower bound (general constant center). Fix a constant nuisance center (m₀, g₀, g₁) ∈ (0,1)³ and Rademacher bump magnitudes (α, β). Suppose the squared propensity-perturbation size (m₀·β/g₁)² is within the budget εm and the squared outcome-regression perturbation size g₁²(α+β)²/(g₁−β)² is within the budget εg, with both budgets nonnegative. If further the per-cell overlap coefficient Γ is at most 1 and the sample size obeys the regime 2n²(Γ/2)² ≤ K·log 2, then for every measurable estimator, there is a data-generating process in the structure-agnostic class around this center on which the estimator misses the true ATE by s = g₁β(α+β)/(2(g₁²−β²)) with probability at least 1/4.
Formal statement
Proof (Lean source)
12 supporting declarations (lemmas, instances)
-
Γ_nonnegtheorem — The per-cell overlap coefficient is nonnegative.Proof (Lean source)
theorem Γ_nonneg (P : GenConstr) : 0 ≤ P.Γ := by have h1 := P.hm₀0; have h2 := P.hm₀1; have h3 := P.hg₁0; have h4 := P.hg₁1 unfold Γ have t1 : 0 ≤ P.m₀ * P.α ^ 2 / P.g₁ := by positivity have t2 : 0 ≤ P.m₀ * (P.α + P.β / P.g₁) ^ 2 / (1 - P.g₁) := by apply div_nonneg (by positivity); linarith have t3 : 0 ≤ P.m₀ ^ 2 * P.β ^ 2 / (P.g₁ ^ 2 * (1 - P.m₀)) := by apply div_nonneg (by positivity) have : 0 < 1 - P.m₀ := by linarith positivity linarith -
inClass_nullGtheorem — The null estimate is itself in the class (zero nuisance error).hypothesesconclusionInClass (P.mhatG (K := K)) P.ghatG εg εm P.mhatG P.ghatG where validProof (Lean source)
theorem inClass_nullG (P : GenConstr) {K : ℕ} {εg εm : ℝ} (hεg : 0 ≤ εg) (hεm : 0 ≤ εm) : InClass (P.mhatG (K := K)) P.ghatG εg εm P.mhatG P.ghatG where valid := P.validDGP_hatG err_g d := by rw [l2sq_self]; exact hεg err_m := by rw [l2sq_self]; exact hεm -
QfalseG_isProbtheorem — The null sample law is a probability measure.Proof (Lean source)
theorem QfalseG_isProb (P : GenConstr) (K n : ℕ) [NeZero K] : IsProbabilityMeasure (QfalseG P K n) := by unfold QfalseG; infer_instance -
QpertG_isProbtheorem — Each perturbed sample law is a probability measure.hypothesesconclusionIsProbabilityMeasure (QpertG P K n lam)Proof (Lean source)
theorem QpertG_isProb (P : GenConstr) (K n : ℕ) [NeZero K] (lam : Fin K → Bool) : IsProbabilityMeasure (QpertG P K n lam) := by unfold QpertG; infer_instance -
QtrueG_isProbtheorem — The Rademacher mixture of perturbed sample laws is a probability measure.Proof (Lean source)
theorem QtrueG_isProb (P : GenConstr) (K n : ℕ) [NeZero K] : IsProbabilityMeasure (QtrueG P K n) := by haveI : ∀ lam : Fin K → Bool, IsProbabilityMeasure (QpertG P K n lam) := fun lam => QpertG_isProb P K n lam unfold QtrueG exact mixture_isProbabilityMeasure _ (signWeight_sum K) _ -
realG_le_minimaxMisstheorem — An in-class DGP's n-sample miss probability at its own ATE is dominated by the minimax miss probability.hypothesesconclusion(productLaw hin.valid n).real {x | s ≤ |est x - ate g|}≤ minimaxMiss P.mhatG P.ghatG εg εm n est sProof (Lean source)
theorem realG_le_minimaxMiss (P : GenConstr) {K n : ℕ} [NeZero K] {εg εm : ℝ} {m : Fin K × Bool → ℝ} {g : Bool → Fin K × Bool → ℝ} (hin : InClass (P.mhatG (K := K)) P.ghatG εg εm m g) (est : (Fin n → Obs (Fin K × Bool)) → ℝ) (s : ℝ) : (productLaw hin.valid n).real {x | s ≤ |est x - ate g|} ≤ minimaxMiss P.mhatG P.ghatG εg εm n est s := by simpa [nMiss] using nMiss_le_minimaxMiss (⟨(m, g), hin⟩ : InClassDGP (P.mhatG (K := K)) P.ghatG εg εm) (est := est) (s := s) -
QfalseG_singleton_ne_zerotheorem — The null n-sample law charges every point.hypothesesconclusionQfalseG P K n {ω} ≠ 0Proof (Lean source)
theorem QfalseG_singleton_ne_zero (P : GenConstr) {K n : ℕ} [NeZero K] (ω : Fin n → Obs (Fin K × Bool)) : QfalseG P K n {ω} ≠ 0 := by have hm0 := P.hm₀0; have h1m0 : (0:ℝ) < 1 - P.m₀ := by have := P.hm₀1; linarith have hg00 := P.hg₀0; have h1g0 : (0:ℝ) < 1 - P.g₀ := by have := P.hg₀1; linarith have hg10 := P.hg₁0; have h1g1 : (0:ℝ) < 1 - P.g₁ := by have := P.hg₁1; linarith have hpos : 0 < (QfalseG P K n).real {ω} := by rw [QfalseG, productLaw_real_singleton] apply Finset.prod_pos intro i _ have hC : (0 : ℝ) < (card (Fin K × Bool) : ℝ) := by have := Fintype.card_pos (α := Fin K × Bool); exact_mod_cast this simp only [obsReal, mhatG, ghatG] rcases (ω i).2.1 with _ | _ <;> rcases (ω i).2.2 with _ | _ <;> · simp only [Bool.false_eq_true, if_false, if_true]; positivity intro h rw [Measure.real, h, ENNReal.toReal_zero] at hpos exact lt_irrefl _ hpos -
QtrueG_real_singletontheorem — The alternative law's .real point mass: a uniform mixture over sign vectors.hypothesesProof (Lean source)
theorem QtrueG_real_singleton (P : GenConstr) {K n : ℕ} [NeZero K] (ω : Fin n → Obs (Fin K × Bool)) : (QtrueG P K n).real {ω} = ∑ lam : Fin K → Bool, ((2 : ℝ) ^ K)⁻¹ * ∏ i, obsReal (P.mPertG lam) (P.gPertG lam) (ω i) := by haveI : ∀ lam : Fin K → Bool, IsProbabilityMeasure (QpertG P K n lam) := fun lam => QpertG_isProb P K n lam rw [QtrueG, Measure.real, mixture_apply] rw [ENNReal.toReal_sum (fun lam _ => ENNReal.mul_ne_top (by rw [signWeight]; exact ENNReal.inv_ne_top.2 (by simp)) (measure_ne_top _ _))] refine Finset.sum_congr rfl fun lam _ => ?_ rw [ENNReal.toReal_mul, signWeight_toReal] congr 1 rw [QpertG] exact productLaw_real_singleton (P.validDGP_pertG lam) ω -
one_add_chiSqDiv_QtrueG_QfalseGtheorem — Mixture second-moment identity (general center).hypothesesProof (Lean source)
theorem one_add_chiSqDiv_QtrueG_QfalseG (P : GenConstr) {K n : ℕ} [NeZero K] : 1 + chiSqDiv (QtrueG P K n) (QfalseG P K n) = ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, ((2 : ℝ) ^ K)⁻¹ * ((2 : ℝ) ^ K)⁻¹ * (P.chiSqOverlapG lam lam') ^ n := by haveI : IsProbabilityMeasure (QtrueG P K n) := QtrueG_isProb P K n haveI : IsProbabilityMeasure (QfalseG P K n) := QfalseG_isProb P K n have hac : QtrueG P K n ≪ QfalseG P K n := absolutelyContinuous_of_singleton_pos _ _ (QfalseG_singleton_ne_zero P) rw [finite_one_add_chiSqDiv (QtrueG P K n) (QfalseG P K n) hac] have hstep : ∀ ω : Fin n → Obs (Fin K × Bool), ((QtrueG P K n).real {ω}) ^ 2 / (QfalseG P K n).real {ω} = ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, ((2 : ℝ) ^ K)⁻¹ * ((2 : ℝ) ^ K)⁻¹ * ∏ i, (obsReal (P.mPertG lam) (P.gPertG lam) (ω i) * obsReal (P.mPertG lam') (P.gPertG lam') (ω i) / obsReal P.mhatG P.ghatG (ω i)) := by intro ω rw [QtrueG_real_singleton P ω, QfalseG, productLaw_real_singleton (P.validDGP_hatG (K := K)) ω, sq, Finset.sum_mul_sum] rw [Finset.sum_div] refine Finset.sum_congr rfl fun lam _ => ?_ rw [Finset.sum_div] refine Finset.sum_congr rfl fun lam' _ => ?_ rw [Finset.prod_div_distrib, Finset.prod_mul_distrib] ring rw [Finset.sum_congr rfl fun ω _ => hstep ω] rw [Finset.sum_comm] refine Finset.sum_congr rfl fun lam _ => ?_ rw [Finset.sum_comm] refine Finset.sum_congr rfl fun lam' _ => ?_ rw [← Finset.mul_sum] congr 1 unfold chiSqOverlapG rw [Fintype.sum_pow] -
chiSqDiv_QtrueG_QfalseG_le_onetheorem — The χ² indistinguishability bound (general center): Γ ≤ 1, 2n²(Γ/2)² ≤ K·log 2 imply χ²(QtrueG‖QfalseG) ≤ 1.hypothesesProof (Lean source)
theorem chiSqDiv_QtrueG_QfalseG_le_one (P : GenConstr) {K n : ℕ} [NeZero K] (hΓ : P.Γ ≤ 1) (hreg : 2 * (n : ℝ) ^ 2 * (P.Γ / 2) ^ 2 ≤ (K : ℝ) * log 2) : chiSqDiv (QtrueG P K n) (QfalseG P K n) ≤ 1 := by have hΓ0 := P.Γ_nonneg have hid := P.one_add_chiSqDiv_QtrueG_QfalseG (K := K) (n := n) have hov : ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, ((2 : ℝ) ^ K)⁻¹ * ((2 : ℝ) ^ K)⁻¹ * (P.chiSqOverlapG lam lam') ^ n = ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, ((2 : ℝ) ^ K)⁻¹ * ((2 : ℝ) ^ K)⁻¹ * (1 + (2 * (P.Γ / 2) / (K : ℝ)) * ∑ j, signOf (lam j) * signOf (lam' j)) ^ n := by refine Finset.sum_congr rfl fun lam _ => Finset.sum_congr rfl fun lam' _ => ?_ rw [P.chiSqOverlap_eqG lam lam', show P.Γ / (K : ℝ) = 2 * (P.Γ / 2) / (K : ℝ) from by ring] have hbound := ingster_bound K n (by linarith : (0:ℝ) ≤ P.Γ / 2) (by linarith : 2 * (P.Γ / 2) ≤ 1) hreg rw [← hov] at hbound rw [← hid] at hbound linarith -
tvDist_QfalseG_QtrueG_le_halftheorem — Total-variation indistinguishability (general center).hypothesesProof (Lean source)
theorem tvDist_QfalseG_QtrueG_le_half (P : GenConstr) {K n : ℕ} [NeZero K] (hΓ : P.Γ ≤ 1) (hreg : 2 * (n : ℝ) ^ 2 * (P.Γ / 2) ^ 2 ≤ (K : ℝ) * log 2) : tvDist (QfalseG P K n) (QtrueG P K n) ≤ 1 / 2 := by haveI : IsProbabilityMeasure (QtrueG P K n) := QtrueG_isProb P K n haveI : IsProbabilityMeasure (QfalseG P K n) := QfalseG_isProb P K n have hac : QtrueG P K n ≪ QfalseG P K n := absolutelyContinuous_of_singleton_pos _ _ (QfalseG_singleton_ne_zero P) have hchi := P.chiSqDiv_QtrueG_QfalseG_le_one (K := K) (n := n) hΓ hreg rw [tvDist_symm] calc tvDist (QtrueG P K n) (QfalseG P K n) ≤ (1 / 2) * sqrt (chiSqDiv (QtrueG P K n) (QfalseG P K n)) := tvDist_le_half_sqrt_chiSqDiv _ _ hac Integrable.of_finite _ ≤ (1 / 2) * sqrt 1 := by apply mul_le_mul_of_nonneg_left _ (by norm_num); exact Real.sqrt_le_sqrt hchi _ = 1 / 2 := by rw [Real.sqrt_one]; ring
Gap 2 core · 3 supporting This file computes the exact average-treatment-effect gap for the general constant-center Rademacher construction. ★ ate_gPertG★ ate_gapG
General-Center ATE Gap
This file computes the exact average-treatment-effect gap for the general constant-center Rademacher construction. The calculation shows that every sign vector produces the same ATE shift from the null center, giving the separation used by the general-center lower bound.
The main public results are ate_ghatG, the null-center ATE calculation;
gPertG_true_eq, which clears the treated-arm denominator for algebraic use;
ate_gPertG, the exact perturbed ATE formula; and ate_gapG, the resulting
constant ATE separation between the perturbation and the null.
Exact ATE of the perturbed construction. For any Rademacher sign vector lam, the average treatment effect of the perturbed outcome regression equals (g₁ − g₀) + g₁β(α+β)/(g₁² − β²), independent of lam.
Formal statement
Proof (Lean source)
For any Rademacher sign vector lam, the gap between the perturbed construction's ATE and the null estimate's ATE equals g₁β(α+β)/(g₁² − β²).
Formal statement
3 supporting declarations (lemmas, instances)
-
g1sq_sub_betasq_postheorem — g₁² − β² > 0 since 0 ≤ β < g₁.conclusion0 < P.g₁ ^ 2 - P.β ^ 2Proof (Lean source)
theorem g1sq_sub_betasq_pos : 0 < P.g₁ ^ 2 - P.β ^ 2 := by have := P.hβg₁; have := P.hβ; have := P.hg₁0; nlinarith -
gPertG_true_eqtheorem — Cleared treated arm. Multiplying numerator and denominator by g₁ turns the inner fraction β/g₁ into the polynomial denominator g₁ − β·Δ: gλ(1,x) = (g₁² + α·g₁·Δ)/(g₁ − β·Δ).hypothesesconclusionP.gPertG lam true x = (P.g₁ ^ 2 + P.α * P.g₁ * Δ lam x) / (P.g₁ - P.β * Δ lam x)Proof (Lean source)
theorem gPertG_true_eq (lam : Fin K → Bool) (x : Fin K × Bool) : P.gPertG lam true x = (P.g₁ ^ 2 + P.α * P.g₁ * Δ lam x) / (P.g₁ - P.β * Δ lam x) := by have hg₁ne : P.g₁ ≠ 0 := ne_of_gt P.hg₁0 have hden0 := P.denomG_pos lam x have hden : P.g₁ - P.β * Δ lam x ≠ 0 := by rcases Δ_mem lam x with h | h <;> rw [h] <;> · have := P.hβg₁; have := P.hβ; intro hc; nlinarith simp only [gPertG, if_true] rw [div_eq_div_iff hden0.ne' hden] field_simp -
ate_ghatGtheorem — The null estimate ĝ has ATE g₁ − g₀: every cell contributes g₁ − g₀.Proof (Lean source)
theorem ate_ghatG [NeZero K] : ate (P.ghatG (K := K)) = P.g₁ - P.g₀ := by rw [ate] have : ∀ x : Fin K × Bool, P.ghatG true x - P.ghatG false x = P.g₁ - P.g₀ := by intro x; simp [ghatG] rw [Finset.sum_congr rfl (fun x _ => this x), Finset.sum_const, Finset.card_univ, nsmul_eq_mul] have hcard : (card (Fin K × Bool) : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr Fintype.card_ne_zero field_simp
Membership 1 core · 4 supporting This file proves that the general constant-center Rademacher perturbations belong to the structure-agnostic nuisance class when the propensity and outcome error budgets are large enough. ★ inClassG
General-Center Membership
This file proves that the general constant-center Rademacher perturbations belong to the
structure-agnostic nuisance class when the propensity and outcome error budgets are large enough.
The supporting estimates are l2sq_mPertG for the exact propensity error,
l2sq_gPertG_false for the unchanged control arm, gPertG_true_sub for the treated-arm
pointwise deviation, and l2sq_gPertG_true_le for the uniform treated-arm error bound.
The capstone inClassG packages these estimates into the realizability input required by the
general-center minimax lower bound.
Class membership. Given the squared propensity-perturbation size (m₀·(β/g₁))² within the budget εm and the squared treated-arm outcome-regression perturbation bound g₁²(α+β)²/(g₁ − β)² within the budget εg, the Rademacher-perturbed data-generating process (mλ, gλ) lies in the structure-agnostic nuisance class ℱ(εg, εm) around the constant center (m̂, ĝ).
Formal statement
Proof (Lean source)
4 supporting declarations (lemmas, instances)
-
l2sq_mPertGtheorem — The propensity perturbation has exact squared L² size (m₀·(β/g₁))²: it is a Rademacher bump of magnitude m₀·(β/g₁) on Δ.hypothesesconclusionl2sq (P.mPertG lam) (P.mhatG (K := K)) = (P.m₀ * (P.β / P.g₁)) ^ 2Proof (Lean source)
theorem l2sq_mPertG [NeZero K] (lam : Fin K → Bool) : l2sq (P.mPertG lam) (P.mhatG (K := K)) = (P.m₀ * (P.β / P.g₁)) ^ 2 := by have hbump : (P.mPertG lam) = (fun x => P.mhatG x + (-(P.m₀ * (P.β / P.g₁))) * Δ lam x) := by funext x simp only [mPertG, mhatG] ring rw [hbump] have hb := l2sq_bump (P.mhatG (K := K)) (-(P.m₀ * (P.β / P.g₁))) (fun x => Δ lam x) (fun x => Δ_sq lam x) rw [hb] ring -
l2sq_gPertG_falsetheorem — The control outcome arm is unchanged (gλ(0,·) = g₀ = ĝ(0,·)), so its L² error is 0. -
gPertG_true_subtheorem — The treated outcome arm: its pointwise deviation from ĝ(1) = g₁ is g₁(α+β)·Δ/(g₁ − β·Δ).hypothesesconclusionP.gPertG lam true x - P.g₁ = P.g₁ * (P.α + P.β) * Δ lam x / (P.g₁ - P.β * Δ lam x)Proof (Lean source)
theorem gPertG_true_sub (lam : Fin K → Bool) (x : Fin K × Bool) : P.gPertG lam true x - P.g₁ = P.g₁ * (P.α + P.β) * Δ lam x / (P.g₁ - P.β * Δ lam x) := by have hden : P.g₁ - P.β * Δ lam x ≠ 0 := by rcases Δ_mem lam x with h | h <;> rw [h] <;> · have := P.hβg₁; have := P.hβ; intro hc; nlinarith rw [gPertG_true_eq, eq_div_iff hden, sub_mul, div_mul_cancel₀ _ hden] ring -
l2sq_gPertG_true_letheorem — Uniform bound on the treated arm's squared L² error: every pointwise term is ≤ g₁²(α+β)²/(g₁ − β)², so the average is too.hypothesesProof (Lean source)
theorem l2sq_gPertG_true_le [NeZero K] (lam : Fin K → Bool) : l2sq (P.gPertG lam true) (P.ghatG true) ≤ P.g₁ ^ 2 * (P.α + P.β) ^ 2 / (P.g₁ - P.β) ^ 2 := by set C := Fin K × Bool have hC : (Fintype.card C : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr Fintype.card_ne_zero -- denominator `g₁ − β` is positive have hden : (0 : ℝ) < P.g₁ - P.β := by have := P.hβg₁; linarith have hden2 : (0 : ℝ) < (P.g₁ - P.β) ^ 2 := by positivity -- each summand is `g₁²(α+β)²/(g₁ − β·Δ)²` and is bounded by `g₁²(α+β)²/(g₁ − β)²` have hterm : ∀ x : C, (P.gPertG lam true x - P.ghatG true x) ^ 2 ≤ P.g₁ ^ 2 * (P.α + P.β) ^ 2 / (P.g₁ - P.β) ^ 2 := by intro x have hghat : P.ghatG true x = P.g₁ := by simp [ghatG] rw [hghat, P.gPertG_true_sub lam x] -- the cleared denominator `g₁ − β·Δ` is nonzero (in fact positive squared) have hdne : P.g₁ - P.β * Δ lam x ≠ 0 := by rcases Δ_mem lam x with h | h <;> rw [h] <;> · have := P.hβg₁; have := P.hβ; intro hc; nlinarith have hdenΔ : (0 : ℝ) < (P.g₁ - P.β * Δ lam x) ^ 2 := by positivity -- rewrite the squared term using `Δ² = 1` have hsq : (P.g₁ * (P.α + P.β) * Δ lam x / (P.g₁ - P.β * Δ lam x)) ^ 2 = P.g₁ ^ 2 * (P.α + P.β) ^ 2 / (P.g₁ - P.β * Δ lam x) ^ 2 := by rw [div_pow, mul_pow, mul_pow, Δ_sq, mul_one] rw [hsq] -- compare denominators: `(g₁ − β)² ≤ (g₁ − β·Δ)²` have hcmp : (P.g₁ - P.β) ^ 2 ≤ (P.g₁ - P.β * Δ lam x) ^ 2 := by have hβ := P.hβ have hβg₁ := P.hβg₁ have hg₁0 := P.hg₁0 rcases Δ_mem lam x with h | h · rw [h]; nlinarith · rw [h]; nlinarith apply div_le_div_of_nonneg_left (by positivity) hden2 hcmp -- average of bounded terms is bounded rw [l2sq] have hsum : ∑ x : C, (P.gPertG lam true x - P.ghatG true x) ^ 2 ≤ ∑ _x : C, P.g₁ ^ 2 * (P.α + P.β) ^ 2 / (P.g₁ - P.β) ^ 2 := Finset.sum_le_sum (fun x _ => hterm x) rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] at hsum calc (Fintype.card C : ℝ)⁻¹ * ∑ x : C, (P.gPertG lam true x - P.ghatG true x) ^ 2 ≤ (Fintype.card C : ℝ)⁻¹ * ((Fintype.card C : ℝ) * (P.g₁ ^ 2 * (P.α + P.β) ^ 2 / (P.g₁ - P.β) ^ 2)) := by apply mul_le_mul_of_nonneg_left hsum positivity _ = P.g₁ ^ 2 * (P.α + P.β) ^ 2 / (P.g₁ - P.β) ^ 2 := by field_simp
MSE 1 core · 0 supporting This file converts the general constant-center quantile lower bound into an expected mean-squared-error lower bound. ★ minimax_lower_bound_mse_gen
General-Center MSE Bound
This file converts the general constant-center quantile lower bound into an expected
mean-squared-error lower bound. The theorem minimax_lower_bound_mse_gen uses
minimax_lower_bound_gen together with the Chebyshev bridge nMiss_sq_le_nMSE to extract an
in-class data-generating process on which any measurable estimator has squared-error risk at
least one quarter of the squared general-center separation.
The proof keeps the two possible witnesses explicit: the null law QfalseG with ATE g₁ - g₀,
or one perturbed law QpertG selected from the uniform mixture QtrueG.
Structure-agnostic minimax lower bound, expected-risk (MSE) form (general center). Under the same budget and regularity hypotheses as minimax_lower_bound_gen — the squared propensity-perturbation size within the budget εm, the squared outcome-regression perturbation size within the budget εg, both budgets nonnegative, the per-cell overlap coefficient Γ at most 1, and the sample size in the regime 2n²(Γ/2)² ≤ K·log 2 — every measurable estimator has the weaker expected-risk consequence: there is a data-generating process in the class on which the estimator's mean-squared error is at least s²/4, where s = g₁β(α+β)/(2(g₁²−β²)) ≍ √(εg·εm), obtained from the quantile bound by a Chebyshev (1−γ)-factor conversion at γ = 3/4.