Estimation.Minimax­ATE.Const­Center­Half

theorem validDGP_perturbed (hα : 0 ≤ α) (hβ : 0 ≤ β) (hαβ : α + 2 * β ≤ 1 / 2) (lam : Fin K → Bool) : ValidDGP (mPerturbed β lam) (gPerturbed α β lam) := by have hβ4 : β ≤ 1 / 4 := by linarith refine ⟨fun x => ?_, fun d x => ?_⟩ · -- propensity `1/2 − β·Δ ∈ [0,1]` constructor <;> simp only [mPerturbed] · rcases Δ_mem lam x with h | h <;> · rw [h]; nlinarith · rcases Δ_mem lam x with h | h <;> · rw [h]; nlinarith · -- outcome `gλ(d,·) ∈ [0,1]` have hd := denom_pos hβ hαβ hα lam x rcases d with _ | _ · -- control arm `= 1/2` simp only [gPerturbed, Bool.false_eq_true, if_false]; norm_num · -- treated arm `(1/2 + α·Δ)/(1 − 2β·Δ) ∈ [0,1]` simp only [gPerturbed, if_true] rcases Δ_mem lam x with h | h · rw [h] at hd ⊢ constructor · apply div_nonneg <;> nlinarith · rw [div_le_one hd]; nlinarith · rw [h] at hd ⊢ constructor · apply div_nonneg <;> nlinarith · rw [div_le_one hd]; nlinarith

theorem chiSqOverlap_eq [NeZero K] (hα : 0 ≤ α) (hβ : 0 ≤ β) (hαβ : α + 2 * β ≤ 1 / 2) (lam lam' : Fin K → Bool) : chiSqOverlap α β lam lam' = 1 + (2 * (α ^ 2 + 2 * α * β + 3 * β ^ 2) / (K : ℝ)) * ∑ j, signOf (lam j) * signOf (lam' j) := by have hK : (K : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne K) have hcard : (card (Fin K × Bool) : ℝ) = 2 * K := by rw [Fintype.card_prod, Fintype.card_fin, Fintype.card_bool]; push_cast; ring -- Rewrite the overlap sum as a sum over cells `j : Fin K` of an explicit -- per-cell value, by collapsing the inner `Bool × Bool` sum over `(d, y)`. have hsum : chiSqOverlap α β lam lam' = ∑ j : Fin K, 2 / (K : ℝ) * (1 / 2 + (α ^ 2 + 2 * α * β + 3 * β ^ 2) * (signOf (lam j) * signOf (lam' j))) := by unfold chiSqOverlap -- peel `Obs = (Fin K × Bool) × (Bool × Bool)` into `∑ (j,pos), ∑ (d,y)`, -- then split the covariate `Fin K × Bool` into `∑ j, ∑ pos`. rw [Fintype.sum_prod_type, Fintype.sum_prod_type] refine Finset.sum_congr rfl fun j _ => ?_ -- collapse the position sum `∑ pos : Bool` and the `(d, y) : Bool × Bool` sum; -- replace every perturbed mass by its denominator-free closed form, and the -- null mass `obsReal mhat ghat = (2K)⁻¹·(1/2)·(1/2)`. simp only [Fintype.sum_prod_type, Fintype.sum_bool] -- perturbed masses → denominator-free closed forms; null mass → its constant simp only [obsReal_perturbed_eq hα hβ hαβ] simp only [obsReal, mhat, ghat, Bool.false_eq_true, if_false, if_true] have e1 : Δ lam (j, true) = signOf (lam j) := by simp [Δ] have e2 : Δ lam (j, false) = -signOf (lam j) := by simp [Δ] have e3 : Δ lam' (j, true) = signOf (lam' j) := by simp [Δ] have e4 : Δ lam' (j, false) = -signOf (lam' j) := by simp [Δ] simp only [e1, e2, e3, e4] rw [hcard] have hs : (signOf (lam j)) ^ 2 = 1 := signOf_sq _ have hs' : (signOf (lam' j)) ^ 2 = 1 := signOf_sq _ field_simp nlinarith [hs, hs', mul_self_nonneg (signOf (lam j) * signOf (lam' j))] rw [hsum] have hsplit : ∀ j : Fin K, 2 / (K : ℝ) * (1 / 2 + (α ^ 2 + 2 * α * β + 3 * β ^ 2) * (signOf (lam j) * signOf (lam' j))) = 1 / (K : ℝ) + 2 * (α ^ 2 + 2 * α * β + 3 * β ^ 2) / (K : ℝ) * (signOf (lam j) * signOf (lam' j)) := by intro j; field_simp rw [Finset.sum_congr rfl (fun j _ => hsplit j), Finset.sum_add_distrib, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, ← Finset.mul_sum] field_simp

theorem explicit_minimax_lower_bound [NeZero K] (hα : 0 ≤ α) (hβ : 0 ≤ β) (hαβ : α + 2 * β ≤ 1 / 2) (hm : β ^ 2 ≤ εm) (hg : (α + β) ^ 2 / (1 - 2 * β) ^ 2 ≤ εg) (hεg : 0 ≤ εg) (hεm : 0 ≤ εm) (htv : tvDist (Qfalse K n) (Qtrue hα hβ hαβ n) ≤ 1 / 2) {est : (Fin n → Obs (Fin K × Bool)) → ℝ} (hest : Measurable est) : 1 / 4 ≤ minimaxMiss mhat ghat εg εm n est (β * (α + β) / (1 - 4 * β ^ 2)) := twoPointWitness_quarter (explicitWitness hα hβ hαβ hm hg hεg hεm htv) (le_refl _) hest

theorem minimax_lower_bound [NeZero K] (hα : 0 ≤ α) (hβ : 0 ≤ β) (hαβ : α + 2 * β ≤ 1 / 2) (hm : β ^ 2 ≤ εm) (hg : (α + β) ^ 2 / (1 - 2 * β) ^ 2 ≤ εg) (hεg : 0 ≤ εg) (hεm : 0 ≤ εm) (hγ : 2 * (α ^ 2 + 2 * α * β + 3 * β ^ 2) ≤ 1) (hreg : 2 * (n : ℝ) ^ 2 * (α ^ 2 + 2 * α * β + 3 * β ^ 2) ^ 2 ≤ (K : ℝ) * log 2) {est : (Fin n → Obs (Fin K × Bool)) → ℝ} (hest : Measurable est) : 1 / 4 ≤ minimaxMiss mhat ghat εg εm n est (β * (α + β) / (1 - 4 * β ^ 2)) := explicit_minimax_lower_bound hα hβ hαβ hm hg hεg hεm (tvDist_Qfalse_Qtrue_le_half hα hβ hαβ hγ hreg) hest

theorem two_point_lower_bound_continuous [NeZero K] (ρ : Measure W) [IsProbabilityMeasure ρ] (hα : 0 ≤ α) (hβ : 0 ≤ β) (hαβ : α + 2 * β ≤ 1 / 2) (hγ : 2 * (α ^ 2 + 2 * α * β + 3 * β ^ 2) ≤ 1) (hreg : 2 * (n : ℝ) ^ 2 * (α ^ 2 + 2 * α * β + 3 * β ^ 2) ^ 2 ≤ (K : ℝ) * log 2) {est : ((Fin n → Obs (Fin K × Bool)) × (Fin n → W)) → ℝ} (hest : Measurable est) : 1 / 4 ≤ max ((QtrueCont hα hβ hαβ n ρ).real {x | β * (α + β) / (1 - 4 * β ^ 2) ≤ |est x - 2 * β * (α + β) / (1 - 4 * β ^ 2)|}) ((QfalseCont K n ρ).real {x | β * (α + β) / (1 - 4 * β ^ 2) ≤ |est x - 0|}) := by haveI : IsProbabilityMeasure (QtrueCont (K := K) hα hβ hαβ n ρ) := QtrueCont_isProb (K := K) hα hβ hαβ ρ haveI : IsProbabilityMeasure (QfalseCont K n ρ) := QfalseCont_isProb ρ have hac : QtrueCont hα hβ hαβ n ρ ≪ QfalseCont K n ρ := by unfold QtrueCont QfalseCont exact (absolutelyContinuous_of_singleton_pos _ _ Qfalse_singleton_ne_zero).prod (Measure.AbsolutelyContinuous.refl _) have hint := integrable_sq_rnDeriv_QtrueCont_QfalseCont (K := K) (n := n) ρ hα hβ hαβ have hchi := chiSqDiv_QtrueCont_QfalseCont_le_one (K := K) (n := n) ρ hα hβ hαβ hγ hreg -- Separation `2s ≤ |θ₀ − θ₁|` with `θ₁ = 0`. have hsep : 2 * (β * (α + β) / (1 - 4 * β ^ 2)) ≤ |2 * β * (α + β) / (1 - 4 * β ^ 2) - 0| := by have hβ4 : β ≤ 1 / 4 := by linarith have hden : (0 : ℝ) < 1 - 4 * β ^ 2 := by nlinarith have hnum : (0 : ℝ) ≤ 2 * β * (α + β) := by have : (0 : ℝ) ≤ α + β := by linarith positivity rw [sub_zero, abs_of_nonneg (div_nonneg hnum hden.le)] apply le_of_eq; ring have hkey := two_point_lower_bound_of_chiSqDiv_le (P₀ := QtrueCont hα hβ hαβ n ρ) (P₁ := QfalseCont K n ρ) hest (θ₀ := 2 * β * (α + β) / (1 - 4 * β ^ 2)) (θ₁ := 0) (s := β * (α + β) / (1 - 4 * β ^ 2)) hsep hac hint (c := 1) hchi -- `(1 - (1/2)·√1)/2 = 1/4`. have hval : (1 - (1 / 2) * sqrt 1) / 2 = 1 / 4 := by rw [Real.sqrt_one]; norm_num rwa [hval] at hkey

theorem ate_gPerturbed [NeZero K] (hα : 0 ≤ α) (hβ : 0 ≤ β) (hαβ : α + 2 * β ≤ 1 / 2) (lam : Fin K → Bool) : ate (gPerturbed α β lam) = 2 * β * (α + β) / (1 - 4 * β ^ 2) := by have hβ4 : β ≤ 1 / 4 := by linarith have h3 : (1 : ℝ) - 4 * β ^ 2 > 0 := by nlinarith have hK : (K : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne K) rw [ate] -- Split the sum over `Fin K × Bool` into pairs, collapse each pair via `perPair`. rw [Fintype.sum_prod_type] have hpair : ∀ j : Fin K, (∑ b : Bool, (gPerturbed α β lam true (j, b) - gPerturbed α β lam false (j, b))) = 4 * β * (α + β) / (1 - 4 * β ^ 2) := by intro j rw [Fintype.sum_bool] have := perPair hα hβ hαβ lam j linarith [this] rw [Finset.sum_congr rfl (fun j _ => hpair j)] rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] rw [Fintype.card_prod, Fintype.card_fin, Fintype.card_bool] push_cast field_simp ring

theorem ate_gap [NeZero K] (hα : 0 ≤ α) (hβ : 0 ≤ β) (hαβ : α + 2 * β ≤ 1 / 2) (lam : Fin K → Bool) : ate (gPerturbed α β lam) - ate (ghat : Bool → (Fin K × Bool) → ℝ) = 2 * β * (α + β) / (1 - 4 * β ^ 2) := by rw [ate_ghat, sub_zero] exact ate_gPerturbed hα hβ hαβ lam

theorem ingster_bound (K n : ℕ) [NeZero K] {γ : ℝ} (hγ0 : 0 ≤ γ) (hγ : 2 * γ ≤ 1) (hreg : 2 * (n : ℝ) ^ 2 * γ ^ 2 ≤ (K : ℝ) * log 2) : ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, ((2 : ℝ) ^ K)⁻¹ * ((2 : ℝ) ^ K)⁻¹ * (1 + (2 * γ / (K : ℝ)) * ∑ j, signOf (lam j) * signOf (lam' j)) ^ n ≤ 2 := by -- Basic facts about `K`. have hKpos : 0 < (K : ℝ) := by have := NeZero.ne K exact_mod_cast Nat.pos_of_ne_zero this have hKne : (K : ℝ) ≠ 0 := ne_of_gt hKpos set c : ℝ := 2 * γ / (K : ℝ) with hc_def have hc0 : 0 ≤ c := by rw [hc_def]; positivity -- abbreviations set w : ℝ := ((2 : ℝ) ^ K)⁻¹ with hw_def have hw0 : 0 ≤ w := by rw [hw_def]; positivity -- Per-term: `(1 + c S)^n ≤ exp (n c S)` where `S = ∑ j, signOf (lam j) * signOf (lam' j)`. have step1 : ∀ lam lam' : Fin K → Bool, (1 + c * ∑ j, signOf (lam j) * signOf (lam' j)) ^ n ≤ exp ((n : ℝ) * (c * ∑ j, signOf (lam j) * signOf (lam' j))) := by intro lam lam' set S : ℝ := ∑ j, signOf (lam j) * signOf (lam' j) with hS_def -- `-K ≤ S ≤ K` have hScard : ∀ j : Fin K, -1 ≤ signOf (lam j) * signOf (lam' j) ∧ signOf (lam j) * signOf (lam' j) ≤ 1 := by intro j rcases signOf_mem (lam j) with h1 | h1 <;> rcases signOf_mem (lam' j) with h2 | h2 <;> simp [h1, h2] have hSlow : -(K : ℝ) ≤ S := by rw [hS_def] have : ∀ j ∈ univ, (-1 : ℝ) ≤ signOf (lam j) * signOf (lam' j) := fun j _ => (hScard j).1 calc -(K : ℝ) = ∑ _j : Fin K, (-1 : ℝ) := by rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin]; simp _ ≤ _ := Finset.sum_le_sum this -- `c * S ≥ -1` have hcS_ge : -1 ≤ c * S := by have : c * (-(K : ℝ)) ≤ c * S := mul_le_mul_of_nonneg_left hSlow hc0 have hcK : c * (K : ℝ) = 2 * γ := by rw [hc_def]; field_simp calc (-1 : ℝ) ≤ -(2 * γ) := by linarith _ = c * (-(K : ℝ)) := by rw [mul_neg, hcK] _ ≤ c * S := this have h0 : (0 : ℝ) ≤ 1 + c * S := by linarith -- `1 + cS ≤ exp (cS)` have hexp : 1 + c * S ≤ exp (c * S) := by have := Real.add_one_le_exp (c * S) linarith calc (1 + c * S) ^ n ≤ (exp (c * S)) ^ n := pow_le_pow_left₀ h0 hexp n _ = exp ((n : ℝ) * (c * S)) := by rw [Real.exp_nat_mul] -- Step 2: bound the whole double sum by the exp double sum. have step2 : ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, w * w * (1 + c * ∑ j, signOf (lam j) * signOf (lam' j)) ^ n ≤ ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, w * w * exp ((n : ℝ) * (c * ∑ j, signOf (lam j) * signOf (lam' j))) := by apply Finset.sum_le_sum intro lam _ apply Finset.sum_le_sum intro lam' _ apply mul_le_mul_of_nonneg_left (step1 lam lam') positivity -- Step 3: the exp double sum equals `(cosh (n c))^K`. have step3 : ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, w * w * exp ((n : ℝ) * (c * ∑ j, signOf (lam j) * signOf (lam' j))) = (Real.cosh ((n : ℝ) * c)) ^ K := by -- Define the per-coordinate factor. set h : Bool × Bool → ℝ := fun p => (1 / 4 : ℝ) * exp ((n : ℝ) * c * (signOf p.1 * signOf p.2)) with hh_def -- The single-coordinate sum is cosh. have hsum_h : (∑ p : Bool × Bool, h p) = Real.cosh ((n : ℝ) * c) := by rw [Fintype.sum_prod_type] simp only [hh_def, Fintype.sum_bool, signOf_true, signOf_false] rw [show (n : ℝ) * c * (1 * 1) = (n : ℝ) * c by ring, show (n : ℝ) * c * (1 * -1) = -((n : ℝ) * c) by ring, show (n : ℝ) * c * (-1 * 1) = -((n : ℝ) * c) by ring, show (n : ℝ) * c * (-1 * -1) = (n : ℝ) * c by ring] rw [Real.cosh_eq] ring -- Now the double sum equals `(∑ p, h p)^K`. rw [← hsum_h] rw [Fintype.sum_pow] -- RHS is now `∑ ρ : Fin K → Bool × Bool, ∏ j, h (ρ j)`. -- LHS: convert the double sum into a sum over the product, then reindex by the equiv. rw [← Fintype.sum_prod_type (f := fun p : (Fin K → Bool) × (Fin K → Bool) => w * w * exp ((n : ℝ) * (c * ∑ j, signOf (p.1 j) * signOf (p.2 j))))] -- LHS : `∑ p : (Fin K → Bool) × (Fin K → Bool), w*w*exp(...)` rw [← Equiv.sum_comp (Equiv.arrowProdEquivProdArrow (Fin K) (fun _ => Bool) (fun _ => Bool)).symm] apply Finset.sum_congr rfl intro ρ _ -- For a fixed `ρ : Fin K → Bool × Bool`. simp only [Equiv.arrowProdEquivProdArrow_symm_apply] -- Goal: w*w*exp((n)*(c*∑ j, signOf (ρ j).1 * signOf (ρ j).2)) = ∏ j, h (ρ j) rw [hh_def] -- ∏ j, (1/4)*exp(nc*(signOf (ρ j).1 * signOf (ρ j).2)) rw [Finset.prod_mul_distrib] -- = (∏ j, 1/4) * (∏ j, exp(...)) rw [← Real.exp_sum] -- ∏ j, exp = exp (∑ j ...) rw [Finset.prod_const, Finset.card_univ, Fintype.card_fin] -- (1/4)^K * exp(∑ j, nc*(...)) -- w*w = (1/4)^K have hww : w * w = (1 / 4 : ℝ) ^ K := by rw [hw_def] rw [← mul_inv] rw [show (2 : ℝ) ^ K * 2 ^ K = 4 ^ K by rw [← mul_pow]; norm_num] rw [show (1 / 4 : ℝ) = (4 : ℝ)⁻¹ by norm_num] rw [inv_pow] rw [hww] -- now goal: (1/4)^K * exp((n)*(c*∑ j ...)) = (1/4)^K * exp(∑ j, nc*(...)) congr 1 congr 1 rw [Finset.mul_sum, Finset.mul_sum] apply Finset.sum_congr rfl intro j _ ring -- Step 4: `(cosh (n c))^K ≤ 2`. have step4 : (Real.cosh ((n : ℝ) * c)) ^ K ≤ 2 := by have hcosh_pos : 0 ≤ Real.cosh ((n : ℝ) * c) := le_of_lt (Real.cosh_pos _) have hcosh_le : Real.cosh ((n : ℝ) * c) ≤ exp (((n : ℝ) * c) ^ 2 / 2) := Real.cosh_le_exp_half_sq _ calc (Real.cosh ((n : ℝ) * c)) ^ K ≤ (exp (((n : ℝ) * c) ^ 2 / 2)) ^ K := pow_le_pow_left₀ hcosh_pos hcosh_le K _ = exp ((K : ℝ) * (((n : ℝ) * c) ^ 2 / 2)) := by rw [Real.exp_nat_mul] _ ≤ exp (log 2) := by apply Real.exp_le_exp.mpr -- (K) * ((n c)^2/2) = 2 n^2 γ^2 / K ≤ log 2 have hexp_eq : (K : ℝ) * (((n : ℝ) * c) ^ 2 / 2) = 2 * (n : ℝ) ^ 2 * γ ^ 2 / (K : ℝ) := by rw [hc_def] field_simp rw [hexp_eq] rw [div_le_iff₀ hKpos] calc 2 * (n : ℝ) ^ 2 * γ ^ 2 ≤ (K : ℝ) * log 2 := hreg _ = log 2 * (K : ℝ) := by ring _ = 2 := by rw [Real.exp_log]; norm_num -- Chain everything. The LHS of the goal matches step2's LHS. calc ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, w * w * (1 + c * ∑ j, signOf (lam j) * signOf (lam' j)) ^ n ≤ ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, w * w * exp ((n : ℝ) * (c * ∑ j, signOf (lam j) * signOf (lam' j))) := step2 _ = (Real.cosh ((n : ℝ) * c)) ^ K := step3 _ ≤ 2 := step4

theorem inClass_perturbed [NeZero K] {εg εm : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β) (hαβ : α + 2 * β ≤ 1 / 2) (hm : β ^ 2 ≤ εm) (hg : (α + β) ^ 2 / (1 - 2 * β) ^ 2 ≤ εg) (lam : Fin K → Bool) : InClass mhat ghat εg εm (mPerturbed β lam) (gPerturbed α β lam) := by refine ⟨validDGP_perturbed hα hβ hαβ lam, ?_, ?_⟩ · intro d cases d with | false => rw [l2sq_gPerturbed_false lam] -- `0 ≤ εg` from `hg` (LHS is nonneg) have hnn : (0 : ℝ) ≤ (α + β) ^ 2 / (1 - 2 * β) ^ 2 := by positivity linarith | true => exact le_trans (l2sq_gPerturbed_true_le hα hβ hαβ lam) hg · rw [l2sq_mPerturbed lam] exact hm

theorem minimax_lower_bound_mse [NeZero K] (hα : 0 ≤ α) (hβ : 0 ≤ β) (hαβ : α + 2 * β ≤ 1 / 2) (hm : β ^ 2 ≤ εm) (hg : (α + β) ^ 2 / (1 - 2 * β) ^ 2 ≤ εg) (hεg : 0 ≤ εg) (hεm : 0 ≤ εm) (hγ : 2 * (α ^ 2 + 2 * α * β + 3 * β ^ 2) ≤ 1) (hreg : 2 * (n : ℝ) ^ 2 * (α ^ 2 + 2 * α * β + 3 * β ^ 2) ^ 2 ≤ (K : ℝ) * log 2) {est : (Fin n → Obs (Fin K × Bool)) → ℝ} (hest : Measurable est) : ∃ p : InClassDGP mhat ghat εg εm, (β * (α + β) / (1 - 4 * β ^ 2)) ^ 2 / 4 ≤ nMSE p.2.valid n est := by set s := β * (α + β) / (1 - 4 * β ^ 2) with hs_def have hβ4 : β ≤ 1 / 4 := by linarith have hden : (0 : ℝ) < 1 - 4 * β ^ 2 := by nlinarith have hαβ0 : (0 : ℝ) ≤ α + β := by linarith have hs0 : 0 ≤ s := by rw [hs_def]; positivity haveI : IsProbabilityMeasure (Qfalse K n) := Qfalse_isProb K n haveI : IsProbabilityMeasure (Qtrue (K := K) hα hβ hαβ n) := Qtrue_isProb hα hβ hαβ n haveI : ∀ lam : Fin K → Bool, IsProbabilityMeasure (Qpert hα hβ hαβ n lam) := fun lam => Qpert_isProb hα hβ hαβ n lam -- From `1/4 ≤ nMiss` on an in-class DGP (at its own ATE `θ`), Chebyshev gives MSE `≥ s²/4`. have hkey : ∀ {m : Fin K × Bool → ℝ} {g : Bool → Fin K × Bool → ℝ} (hin : InClass mhat ghat εg εm m g) (θ : ℝ), ate g = θ → 1 / 4 ≤ (productLaw hin.valid n).real {x | s ≤ |est x - θ|} → ∃ p : InClassDGP mhat ghat εg εm, s ^ 2 / 4 ≤ nMSE p.2.valid n est := by intro m g hin θ hθ h14 refine ⟨⟨(m, g), hin⟩, ?_⟩ have hcheb : s ^ 2 * (productLaw hin.valid n).real {x | s ≤ |est x - θ|} ≤ nMSE hin.valid n est := by have h := nMiss_sq_le_nMSE hin.valid n (est := est) hs0 unfold nMiss at h rwa [hθ] at h have h1 := mul_le_mul_of_nonneg_left h14 (sq_nonneg s) change s ^ 2 / 4 ≤ nMSE hin.valid n est calc s ^ 2 / 4 = s ^ 2 * (1 / 4) := by ring _ ≤ s ^ 2 * (productLaw hin.valid n).real {x | s ≤ |est x - θ|} := h1 _ ≤ nMSE hin.valid n est := hcheb -- Two-point bound: `1/4 ≤ max(null miss, mixture miss)`. have htv := tvDist_Qfalse_Qtrue_le_half (K := K) (n := n) hα hβ hαβ hγ hreg have hsep : 2 * s ≤ |(0 : ℝ) - 2 * β * (α + β) / (1 - 4 * β ^ 2)| := by rw [zero_sub, abs_neg, abs_of_nonneg (by positivity)] rw [hs_def]; apply le_of_eq; ring have hmax := two_point_lower_bound_of_tvDist_le (P₀ := Qfalse K n) (P₁ := Qtrue hα hβ hαβ n) hest hsep htv rw [show (1 - (1 : ℝ) / 2) / 2 = 1 / 4 by norm_num] at hmax rcases le_max_iff.mp hmax with hleft | hright · -- null branch: `(m̂, ĝ)` is in class, `ate ĝ = 0` exact hkey (inClass_null hεg hεm) 0 ate_ghat hleft · -- mixture branch: extract a single Rademacher-perturbed DGP obtain ⟨lam, hlam⟩ := exists_real_ge_mixture (signWeight K) (signWeight_sum K) (fun l => Qpert hα hβ hαβ n l) {x | s ≤ |est x - 2 * β * (α + β) / (1 - 4 * β ^ 2)|} exact hkey (inClass_perturbed hα hβ hαβ hm hg lam) (2 * β * (α + β) / (1 - 4 * β ^ 2)) (ate_gPerturbed hα hβ hαβ lam) (le_trans hright hlam)

theorem parametric_lower_bound {C : Type*} [Fintype C] [Nonempty C] [MeasurableSpace C] [MeasurableSingletonClass C] {n : ℕ} {m₀ g₀ g₁ δ εg εm : ℝ} (hm0 : 0 < m₀) (hm1 : m₀ < 1) (hg0 : 0 < g₀) (hg0' : g₀ < 1) (hg1 : 0 < g₁) (hg1' : g₁ < 1) (hδ : 0 ≤ δ) (hδU : g₁ + δ ≤ 1) (hbudget : δ ^ 2 ≤ εg) (hεm : 0 ≤ εm) (hreg : (n : ℝ) * (m₀ * δ ^ 2 / (g₁ * (1 - g₁))) ≤ log 2) {est : (Fin n → Obs C) → ℝ} (hest : Measurable est) : 1 / 4 ≤ minimaxMiss (fun _ => m₀) (fun d _ => if d then g₁ else g₀) εg εm n est (δ / 2) := by have hvN : ValidDGP (C := C) (mC m₀) (gNull g₀ g₁) := validDGP_null hm0 hm1 hg0 hg0' hg1 hg1' have hvP : ValidDGP (C := C) (mC m₀) (gPert g₀ g₁ δ) := validDGP_pert hm0 hm1 hg0 hg0' hg1 hδ hδU have hεg : 0 ≤ εg := le_trans (sq_nonneg δ) hbudget -- the two-point witness: null vs perturbed let W : TwoPointWitness C n (mC m₀) (gNull g₀ g₁) εg εm := { s := δ / 2 c := 1 / 2 Q := fun j => cond j (productLaw hvP n) (productLaw hvN n) prob := by intro j; cases j · exact productLaw_isProb hvN n · exact productLaw_isProb hvP n θ := fun j => cond j ((g₁ + δ) - g₀) (g₁ - g₀) sep := by change 2 * (δ / 2) ≤ |((g₁ + δ) - g₀) - (g₁ - g₀)| have : ((g₁ + δ) - g₀) - (g₁ - g₀) = δ := by ring rw [this, abs_of_nonneg hδ]; linarith tvBound := by simpa using tvDist_productLaw_le_half hvN hvP hm0 hm1 hg0 hg0' hg1 hg1' hreg dominated := by intro est' j cases j · -- null branch change (productLaw hvN n).real {x | (δ / 2) ≤ |est' x - (g₁ - g₀)|} ≤ minimaxMiss (mC m₀) (gNull g₀ g₁) εg εm n est' (δ / 2) have hb := nMiss_le_minimaxMiss (mhat := mC m₀) (ghat := gNull g₀ g₁) (εg := εg) (εm := εm) (⟨(mC m₀, gNull g₀ g₁), inClass_null hvN hεg hεm⟩) (est := est') (s := δ / 2) simp only [nMiss, ate_gNull] at hb exact hb · -- perturbed branch change (productLaw hvP n).real {x | (δ / 2) ≤ |est' x - ((g₁ + δ) - g₀)|} ≤ minimaxMiss (mC m₀) (gNull g₀ g₁) εg εm n est' (δ / 2) have hb := nMiss_le_minimaxMiss (mhat := mC m₀) (ghat := gNull g₀ g₁) (εg := εg) (εm := εm) (⟨(mC m₀, gPert g₀ g₁ δ), inClass_pert hvP hbudget hεm⟩) (est := est') (s := δ / 2) simp only [nMiss, ate_gPert] at hb exact hb } exact twoPointWitness_quarter W (le_refl _) hest