Estimation.Minimax­ATE.Varying­Center­Case1

theorem validDGP_hatV : ValidDGP (C := Fin K × Bool) P.mhatV P.ghatV := by refine ⟨fun x => ?_, fun d x => ?_⟩ · simp only [mhatV]; exact ⟨(P.hm₀0 x.1).le, (P.hm₀1 x.1).le⟩ · simp only [ghatV]; cases d · exact ⟨(P.hg₀0 x.1).le, (P.hg₀1 x.1).le⟩ · exact ⟨(P.hg₁0 x.1).le, (P.hg₁1 x.1).le⟩

theorem validDGP_pertV (lam : Fin K → Bool) : ValidDGP (P.mPertV lam) (P.gPertV lam) := by refine ⟨fun x => ?_, fun d x => ?_⟩ · -- propensity `m₀·(1 − (β/g₁)·Δ) ∈ [0,1]` have hr := P.ratio_nonneg x.1 have hr1 := P.ratio_lt_one x.1 have hmU := P.hmU x.1 have hm0 := P.hm₀0 x.1 simp only [mPertV] rcases Δ_mem lam x with h | h · rw [h]; constructor · nlinarith · nlinarith · rw [h]; constructor · nlinarith · nlinarith · -- outcome `gλ(d,·) ∈ [0,1]` have hd := P.denomV_pos lam x rcases d with _ | _ · simp only [gPertV, Bool.false_eq_true, if_false]; exact ⟨(P.hg₀0 x.1).le, (P.hg₀1 x.1).le⟩ · simp only [gPertV, if_true] have hr := P.ratio_nonneg x.1 have hgU := P.hgU x.1 have hαg₁ := P.hαg₁ x.1 have hg₁0 := P.hg₁0 x.1 have hg₁1 := P.hg₁1 x.1 have hα := P.hα rcases Δ_mem lam x with h | h · rw [h] at hd ⊢ refine ⟨div_nonneg (by nlinarith) hd.le, ?_⟩ rw [div_le_one hd]; nlinarith · rw [h] at hd ⊢ refine ⟨div_nonneg (by nlinarith) hd.le, ?_⟩ rw [div_le_one hd]; nlinarith

theorem chiSqOverlap_eqV [NeZero K] (lam lam' : Fin K → Bool) : P.chiSqOverlapV lam lam' = 1 + ∑ j, (P.ΓV j / (K : ℝ)) * (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 as a per-pair sum. have hsum : P.chiSqOverlapV lam lam' = ∑ j : Fin K, (1 / (K : ℝ)) * (1 + P.ΓV j * (signOf (lam j) * signOf (lam' j))) := by unfold chiSqOverlapV rw [Fintype.sum_prod_type, Fintype.sum_prod_type] refine Finset.sum_congr rfl fun j _ => ?_ simp only [Fintype.sum_prod_type, Fintype.sum_bool] simp only [obsReal_pertV_eq] simp only [obsReal, mhatV, ghatV, 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 hg₁ne : P.g₁ j ≠ 0 := ne_of_gt (P.hg₁0 j) have hm₀ne : P.m₀ j ≠ 0 := ne_of_gt (P.hm₀0 j) have hg₀ne : P.g₀ j ≠ 0 := ne_of_gt (P.hg₀0 j) have h1g₁ : (1 : ℝ) - P.g₁ j ≠ 0 := by have := P.hg₁1 j; intro hc; linarith have h1m₀ : (1 : ℝ) - P.m₀ j ≠ 0 := by have := P.hm₀1 j; intro hc; linarith have h1g₀ : (1 : ℝ) - P.g₀ j ≠ 0 := by have := P.hg₀1 j; intro hc; linarith rcases signOf_mem (lam j) with h | h <;> rcases signOf_mem (lam' j) with h' | h' <;> rw [h, h'] <;> · simp only [ΓV] field_simp ring rw [hsum] have hsplit : ∀ j : Fin K, (1 / (K : ℝ)) * (1 + P.ΓV j * (signOf (lam j) * signOf (lam' j))) = 1 / (K : ℝ) + P.ΓV j / (K : ℝ) * (signOf (lam j) * signOf (lam' j)) := by intro j; ring 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] field_simp

theorem ate_gPertV [NeZero K] (lam : Fin K → Bool) : ate (P.gPertV lam) = (card (Fin K × Bool) : ℝ)⁻¹ * ∑ j : Fin K, (2 * P.g₁ j * (P.g₁ j ^ 2 + P.α * P.β) / (P.g₁ j ^ 2 - P.β ^ 2) - 2 * P.g₀ j) := by rw [ate, Fintype.sum_prod_type] congr 1 refine Finset.sum_congr rfl fun j _ => ?_ rw [Fintype.sum_bool] have := P.perPairV lam j linarith [this]

theorem ate_gapV [NeZero K] (lam : Fin K → Bool) : ate (P.gPertV lam) - ate (P.ghatV (K := K)) = (card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β * (P.α + P.β)) * ∑ j : Fin K, P.g₁ j / (P.g₁ j ^ 2 - P.β ^ 2) := by rw [P.ate_gPertV lam, P.ate_ghatV, ← mul_sub, ← Finset.sum_sub_distrib, mul_assoc] congr 1 rw [Finset.mul_sum] refine Finset.sum_congr rfl fun j _ => ?_ have hg₁ne : P.g₁ j ≠ 0 := ne_of_gt (P.hg₁0 j) have d3 : P.g₁ j ^ 2 - P.β ^ 2 ≠ 0 := ne_of_gt (P.g1sq_sub_betasq_pos j) field_simp ring

theorem ingster_bound_general (K n : ℕ) [NeZero K] {d : Fin K → ℝ} (hd0 : ∀ j, 0 ≤ d j) (hdsum : ∑ j, d j ≤ 1) (hreg : (n : ℝ) ^ 2 / 2 * ∑ j, (d j) ^ 2 ≤ log 2) : ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, ((2 : ℝ) ^ K)⁻¹ * ((2 : ℝ) ^ K)⁻¹ * (1 + ∑ j, d j * (signOf (lam j) * signOf (lam' j))) ^ n ≤ 2 := by -- abbreviations set w : ℝ := ((2 : ℝ) ^ K)⁻¹ with hw_def have hw0 : 0 ≤ w := by rw [hw_def]; positivity -- Per-term: `(1 + S)^n ≤ exp (n S)` where `S = ∑ j, d j*(signOf (lam j)*signOf (lam' j))`. have step1 : ∀ lam lam' : Fin K → Bool, (1 + ∑ j, d j * (signOf (lam j) * signOf (lam' j))) ^ n ≤ exp ((n : ℝ) * ∑ j, d j * (signOf (lam j) * signOf (lam' j))) := by intro lam lam' set S : ℝ := ∑ j, d j * (signOf (lam j) * signOf (lam' j)) with hS_def -- Each summand `d j * (signOf (lam j)*signOf (lam' j)) ≥ d j * (-1) = -(d j)`. have hSlow : -(1 : ℝ) ≤ S := by rw [hS_def] have hterm : ∀ j ∈ univ, -(d j) ≤ d j * (signOf (lam j) * signOf (lam' j)) := by intro j _ have hmem : -1 ≤ signOf (lam j) * signOf (lam' j) := by rcases signOf_mem (lam j) with h1 | h1 <;> rcases signOf_mem (lam' j) with h2 | h2 <;> simp [h1, h2] have := mul_le_mul_of_nonneg_left hmem (hd0 j) simpa using this calc -(1 : ℝ) ≤ -(∑ j, d j) := by linarith _ = ∑ j, -(d j) := by rw [Finset.sum_neg_distrib] _ ≤ ∑ j, d j * (signOf (lam j) * signOf (lam' j)) := Finset.sum_le_sum hterm have h0 : (0 : ℝ) ≤ 1 + S := by linarith -- `1 + S ≤ exp (S)` have hexp : 1 + S ≤ exp S := by have := Real.add_one_le_exp S linarith calc (1 + S) ^ n ≤ (exp S) ^ n := pow_le_pow_left₀ h0 hexp n _ = exp ((n : ℝ) * 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 + ∑ j, d j * (signOf (lam j) * signOf (lam' j))) ^ n ≤ ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, w * w * exp ((n : ℝ) * ∑ j, d 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 `∏ j, cosh (n * d j)`. have step3 : ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, w * w * exp ((n : ℝ) * ∑ j, d j * (signOf (lam j) * signOf (lam' j))) = ∏ j, Real.cosh ((n : ℝ) * d j) := by -- Define the per-coordinate factor. set h : Fin K → Bool × Bool → ℝ := fun j p => (1 / 4 : ℝ) * exp ((n : ℝ) * d j * (signOf p.1 * signOf p.2)) with hh_def -- The single-coordinate sum is cosh. have hsum_h : ∀ j, (∑ p : Bool × Bool, h j p) = Real.cosh ((n : ℝ) * d j) := by intro j rw [Fintype.sum_prod_type] simp only [hh_def, Fintype.sum_bool, signOf_true, signOf_false] rw [show (n : ℝ) * d j * (1 * 1) = (n : ℝ) * d j by ring, show (n : ℝ) * d j * (1 * -1) = -((n : ℝ) * d j) by ring, show (n : ℝ) * d j * (-1 * 1) = -((n : ℝ) * d j) by ring, show (n : ℝ) * d j * (-1 * -1) = (n : ℝ) * d j by ring] rw [Real.cosh_eq] ring -- Rewrite the RHS product as a product of single-coordinate sums. have hprod_eq : ∏ j, Real.cosh ((n : ℝ) * d j) = ∏ j, ∑ p : Bool × Bool, h j p := by apply Finset.prod_congr rfl intro j _ rw [hsum_h j] rw [hprod_eq] -- `∏ j, ∑ p, h j p = ∑ ρ : Fin K → Bool×Bool, ∏ j, h j (ρ j)` (distribute product of sums). rw [Finset.prod_univ_sum, Fintype.piFinset_univ] -- 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 : ℝ) * ∑ j, d j * (signOf (p.1 j) * signOf (p.2 j))))] 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)*∑ j, d j*(signOf (ρ j).1 * signOf (ρ j).2)) = ∏ j, h j (ρ j) rw [hh_def] -- ∏ j, (1/4)*exp(n*d j*(signOf (ρ j).1 * signOf (ρ j).2)) rw [Finset.prod_mul_distrib] -- = (∏ j, 1/4) * (∏ j, exp(...)) rw [← Real.exp_sum] rw [Finset.prod_const, Finset.card_univ, Fintype.card_fin] -- 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)*∑ j ...) = (1/4)^K * exp(∑ j, n*d j*(...)) congr 1 congr 1 rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j _ ring -- Step 4: `∏ j, cosh (n * d j) ≤ 2`. have step4 : ∏ j, Real.cosh ((n : ℝ) * d j) ≤ 2 := by calc ∏ j, Real.cosh ((n : ℝ) * d j) ≤ ∏ j, exp (((n : ℝ) * d j) ^ 2 / 2) := by apply Finset.prod_le_prod · intro j _; exact le_of_lt (Real.cosh_pos _) · intro j _; exact Real.cosh_le_exp_half_sq _ _ = exp (∑ j, ((n : ℝ) * d j) ^ 2 / 2) := by rw [← Real.exp_sum] _ ≤ exp (log 2) := by apply Real.exp_le_exp.mpr have hsum_eq : (∑ j, ((n : ℝ) * d j) ^ 2 / 2) = (n : ℝ) ^ 2 / 2 * ∑ j, (d j) ^ 2 := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j _ ring rw [hsum_eq] exact hreg _ = 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 + ∑ j, d j * (signOf (lam j) * signOf (lam' j))) ^ n ≤ ∑ lam : Fin K → Bool, ∑ lam' : Fin K → Bool, w * w * exp ((n : ℝ) * ∑ j, d j * (signOf (lam j) * signOf (lam' j))) := step2 _ = ∏ j, Real.cosh ((n : ℝ) * d j) := step3 _ ≤ 2 := step4

theorem minimax_lower_bound_var (P : VarConstr K) {n : ℕ} [NeZero K] {εg εm : ℝ} (hm : ∀ j, (P.m₀ j * (P.β / P.g₁ j)) ^ 2 ≤ εm) (hg : ∀ j, P.g₁ j ^ 2 * (P.α + P.β) ^ 2 / (P.g₁ j - P.β) ^ 2 ≤ εg) (hεg : 0 ≤ εg) (hεm : 0 ≤ εm) (hΓsum : ∑ j, P.ΓV j / (K : ℝ) ≤ 1) (hreg : (n : ℝ) ^ 2 / 2 * ∑ j, (P.ΓV j / (K : ℝ)) ^ 2 ≤ log 2) {est : (Fin n → Obs (Fin K × Bool)) → ℝ} (hest : Measurable est) : 1 / 4 ≤ minimaxMiss P.mhatV P.ghatV εg εm n est ((card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β * (P.α + P.β)) * (∑ j : Fin K, P.g₁ j / (P.g₁ j ^ 2 - P.β ^ 2)) / 2) := by set gap := (card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β * (P.α + P.β)) * ∑ j : Fin K, P.g₁ j / (P.g₁ j ^ 2 - P.β ^ 2) with hgap have hgap0 : 0 ≤ gap := by have h := P.ate_gap_nonneg (fun _ => true) rwa [P.ate_gapV (fun _ => true)] at h set s := gap / 2 with hs set θ0 := ate (P.ghatV (K := K)) with hθ0 -- the two-point witness let W : TwoPointWitness (Fin K × Bool) n P.mhatV P.ghatV εg εm := { s := s c := 1 / 2 Q := fun j => cond j (QtrueV P n) (QfalseV P n) prob := by intro j; cases j · exact QfalseV_isProb P n · exact QtrueV_isProb P n θ := fun j => cond j (θ0 + gap) θ0 sep := by change 2 * s ≤ |(θ0 + gap) - θ0| rw [add_sub_cancel_left, abs_of_nonneg hgap0, hs]; linarith tvBound := by simpa using P.tvDist_QfalseV_QtrueV_le_half (n := n) hΓsum hreg dominated := by intro est' j cases j · -- null branch change (QfalseV P n).real {x | s ≤ |est' x - θ0|} ≤ minimaxMiss P.mhatV P.ghatV εg εm n est' s have hb := P.realV_le_minimaxMiss (n := n) (inClass_nullV P hεg hεm) est' s rw [hθ0] exact hb · -- mixture branch change (QtrueV P n).real {x | s ≤ |est' x - (θ0 + gap)|} ≤ minimaxMiss P.mhatV P.ghatV εg εm n est' s haveI : ∀ lam : Fin K → Bool, IsProbabilityMeasure (QpertV P n lam) := fun lam => QpertV_isProb P n lam unfold QtrueV refine mixtureReal_le (signWeight K) (signWeight_sum K) (fun lam => QpertV P n lam) _ _ ?_ intro lam have hb := P.realV_le_minimaxMiss (n := n) (P.inClassV hm hg hεg lam) est' s have hkey : ate (P.gPertV lam) = θ0 + gap := by have := P.ate_gapV lam rw [hθ0, hgap]; linarith [this] rw [hkey] at hb exact hb } exact twoPointWitness_quarter W (le_refl _) hest

theorem inClassV [NeZero K] {εg εm : ℝ} (hm : ∀ j, (P.m₀ j * (P.β / P.g₁ j)) ^ 2 ≤ εm) (hg : ∀ j, P.g₁ j ^ 2 * (P.α + P.β) ^ 2 / (P.g₁ j - P.β) ^ 2 ≤ εg) (hεg : 0 ≤ εg) (lam : Fin K → Bool) : InClass (P.mhatV (K := K)) P.ghatV εg εm (P.mPertV lam) (P.gPertV lam) := by refine ⟨P.validDGP_pertV lam, ?_, ?_⟩ · intro d cases d with | false => rw [P.l2sq_gPertV_false lam]; exact hεg | true => exact P.l2sq_gPertV_true_le hg lam · exact P.l2sq_mPertV_le hm lam