Estimation.Minimax­ATE.Varying­Center­Case2

theorem mPert2_eq (lam : Fin K → Bool) (x : Fin K × Bool) : P.mPert2 lam x = P.m₀ x.1 * (1 + P.κ x.1 * Δ lam x) := by have hg₁ne : P.g₁ x.1 ≠ 0 := ne_of_gt (P.hg₁0 x.1) unfold mPert2 D2 κ -- expand and use Δ² = 1 have hsq : Δ lam x * Δ lam x = 1 := by have := Δ_sq lam x; nlinarith [this] field_simp linear_combination (P.m₀ x.1 * P.α * P.g₁ x.1 * P.β) * hsq

theorem validDGP_pert2 (lam : Fin K → Bool) : ValidDGP (P.mPert2 lam) (P.gPert2 lam) := by refine ⟨fun x => ?_, fun d x => ?_⟩ · -- propensity `m₀·(1 + κ·Δ) ∈ [0,1]` rw [P.mPert2_eq lam x] have hm0 := P.hm₀0 x.1 have hm1 := P.hm₀1 x.1 have hκ0 := P.κ_nonneg x.1 have hκ1 := P.hκ x.1 have hmU := P.hmU x.1 have hκeq : P.κ x.1 = P.β / P.g₁ x.1 + P.α * P.g₁ x.1 - P.α ^ 2 * P.β * P.g₁ x.1 := rfl rw [← hκeq] at hκ1 hmU constructor · rcases Δ_mem lam x with h | h · rw [h]; nlinarith · rw [h]; nlinarith · rcases Δ_mem lam x with h | h · rw [h]; nlinarith · rw [h]; nlinarith · -- outcome `gλ(d,·) ∈ [0,1]` have hd := P.D2_pos lam x rcases d with _ | _ · simp only [gPert2, Bool.false_eq_true, if_false]; exact ⟨(P.hg₀0 x.1).le, (P.hg₀1 x.1).le⟩ · simp only [gPert2, if_true] have hg10 := P.hg₁0 x.1 have hgU := P.hgU x.1 have hr := P.ratio_nonneg x.1 refine ⟨div_nonneg hg10.le hd.le, ?_⟩ rw [div_le_one hd] -- need g₁ ≤ D = 1 + (β/g₁)Δ − αβ; worst case Δ = −1 covered by hgU unfold D2 rcases Δ_mem lam x with h | h · rw [h]; nlinarith · rw [h]; nlinarith

theorem chiSqOverlap_eq2 [NeZero K] (lam lam' : Fin K → Bool) : P.chiSqOverlapV2 lam lam' = 1 + ∑ j, (P.ΓV2 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.chiSqOverlapV2 lam lam' = ∑ j : Fin K, (1 / (K : ℝ)) * (1 + P.ΓV2 j * (signOf (lam j) * signOf (lam' j))) := by unfold chiSqOverlapV2 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_pert2_eq, D2] simp only [obsReal, mhat2, ghat2, 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 [ΓV2, κ] field_simp ring rw [hsum] have hsplit : ∀ j : Fin K, (1 / (K : ℝ)) * (1 + P.ΓV2 j * (signOf (lam j) * signOf (lam' j))) = 1 / (K : ℝ) + P.ΓV2 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_gPert2 [NeZero K] (lam : Fin K → Bool) : ate (P.gPert2 lam) = (card (Fin K × Bool) : ℝ)⁻¹ * ∑ j : Fin K, (2 * P.g₁ j ^ 3 * (1 - P.α * P.β) / (P.g₁ j ^ 2 * (1 - P.α * P.β) ^ 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.perPair2 lam j linarith [this]

theorem ate_gap2 [NeZero K] (lam : Fin K → Bool) : ate (P.gPert2 lam) - ate (P.ghat2 (K := K)) = (card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β) * ∑ j : Fin K, P.g₁ j * (P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) + P.β) / (P.g₁ j ^ 2 * (1 - P.α * P.β) ^ 2 - P.β ^ 2) := by rw [P.ate_gPert2 lam, P.ate_ghat2, ← 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 hE := P.denomE_pos j have hEne : P.g₁ j ^ 2 * (1 - P.α * P.β) ^ 2 - P.β ^ 2 ≠ 0 := ne_of_gt hE field_simp ring

theorem minimax_lower_bound_var2 (P : VarConstr2 K) {n : ℕ} [NeZero K] {εg εm : ℝ} (hβpos : 0 < P.β) (hm : ∀ j, (P.m₀ j * P.κ j) ^ 2 ≤ εm) (hg : ∀ j, P.β ^ 2 * (P.α * P.g₁ j + 1) ^ 2 / (1 - P.β / P.g₁ j - P.α * P.β) ^ 2 ≤ εg) (hεg : 0 ≤ εg) (hεm : 0 ≤ εm) (hΓsum : ∑ j, P.ΓV2 j / (K : ℝ) ≤ 1) (hreg : (n : ℝ) ^ 2 / 2 * ∑ j, (P.ΓV2 j / (K : ℝ)) ^ 2 ≤ log 2) {est : (Fin n → Obs (Fin K × Bool)) → ℝ} (hest : Measurable est) : 1 / 4 ≤ minimaxMiss P.mhat2 P.ghat2 εg εm n est ((card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β) * (∑ j : Fin K, P.g₁ j * (P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) + P.β) / (P.g₁ j ^ 2 * (1 - P.α * P.β) ^ 2 - P.β ^ 2)) / 2) := by set gap := (card (Fin K × Bool) : ℝ)⁻¹ * (2 * P.β) * ∑ j : Fin K, P.g₁ j * (P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) + P.β) / (P.g₁ j ^ 2 * (1 - P.α * P.β) ^ 2 - P.β ^ 2) with hgap have hgap_pos : 0 < gap := by have hcard : 0 < (card (Fin K × Bool) : ℝ)⁻¹ := by have hcard_nat : 0 < card (Fin K × Bool) := Fintype.card_pos exact inv_pos.mpr (by exact_mod_cast hcard_nat) have h2β : 0 < 2 * P.β := by positivity have hsum_pos : 0 < ∑ j : Fin K, P.g₁ j * (P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) + P.β) / (P.g₁ j ^ 2 * (1 - P.α * P.β) ^ 2 - P.β ^ 2) := by apply Finset.sum_pos · intro j _ have hg1 := P.hg₁0 j have hE := P.denomE_pos j have hab := P.alphabeta_le_one j have hinner : 0 < P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) + P.β := by have hnonneg : 0 ≤ P.α * P.g₁ j ^ 2 * (1 - P.α * P.β) := by apply mul_nonneg (mul_nonneg P.hα (sq_nonneg _)) linarith linarith exact div_pos (mul_pos hg1 hinner) hE · exact Finset.univ_nonempty rw [hgap] exact mul_pos (mul_pos hcard h2β) hsum_pos set s := gap / 2 with hs set θ0 := ate (P.ghat2 (K := K)) with hθ0 -- the two-point witness let W : TwoPointWitness (Fin K × Bool) n P.mhat2 P.ghat2 εg εm := { s := s c := 1 / 2 Q := fun j => cond j (Qtrue2 P n) (Qfalse2 P n) prob := by intro j; cases j · exact Qfalse2_isProb P n · exact Qtrue2_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_pos hgap_pos, hs]; linarith tvBound := by simpa using P.tvDist_Qfalse2_Qtrue2_le_half (n := n) hΓsum hreg dominated := by intro est' j cases j · -- null branch change (Qfalse2 P n).real {x | s ≤ |est' x - θ0|} ≤ minimaxMiss P.mhat2 P.ghat2 εg εm n est' s have hb := P.real2_le_minimaxMiss (n := n) (inClass_null2 P hεg hεm) est' s rw [hθ0] exact hb · -- mixture branch change (Qtrue2 P n).real {x | s ≤ |est' x - (θ0 + gap)|} ≤ minimaxMiss P.mhat2 P.ghat2 εg εm n est' s haveI : ∀ lam : Fin K → Bool, IsProbabilityMeasure (Qpert2 P n lam) := fun lam => Qpert2_isProb P n lam unfold Qtrue2 refine mixtureReal_le (signWeight K) (signWeight_sum K) (fun lam => Qpert2 P n lam) _ _ ?_ intro lam have hb := P.real2_le_minimaxMiss (n := n) (P.inClass2 hm hg hεg lam) est' s have hkey : ate (P.gPert2 lam) = θ0 + gap := by have := P.ate_gap2 lam rw [hθ0, hgap]; linarith [this] rw [hkey] at hb exact hb } exact twoPointWitness_quarter W (le_refl _) hest

theorem inClass2 [NeZero K] {εg εm : ℝ} (hm : ∀ j, (P.m₀ j * P.κ j) ^ 2 ≤ εm) (hg : ∀ j, P.β ^ 2 * (P.α * P.g₁ j + 1) ^ 2 / (1 - P.β / P.g₁ j - P.α * P.β) ^ 2 ≤ εg) (hεg : 0 ≤ εg) (lam : Fin K → Bool) : InClass (P.mhat2 (K := K)) P.ghat2 εg εm (P.mPert2 lam) (P.gPert2 lam) := by refine ⟨P.validDGP_pert2 lam, ?_, ?_⟩ · intro d cases d with | false => rw [P.l2sq_gPert2_false lam]; exact hεg | true => exact P.l2sq_gPert2_true_le hg lam · exact P.l2sq_mPert2_le hm lam