Estimation.Minimax­ATE.Achievability

theorem aipw_bias_identity [Nonempty C] {m : C → ℝ} {g : Bool → C → ℝ} (mhat : C → ℝ) (ghat : Bool → C → ℝ) (hmhat : ∀ x, 0 < mhat x) (hmhat1 : ∀ x, mhat x < 1) : (∑ z : Obs C, obsReal m g z * aipwScoreFin mhat ghat z) - ate g = (Fintype.card C : ℝ)⁻¹ * ∑ x : C, ((1 - m x / mhat x) * (ghat true x - g true x) - (1 - (1 - m x) / (1 - mhat x)) * (ghat false x - g false x)) := by have hm0 : ∀ x, mhat x ≠ 0 := fun x => (hmhat x).ne' have hm1 : ∀ x, (1 : ℝ) - mhat x ≠ 0 := fun x => sub_ne_zero.mpr (hmhat1 x).ne' -- collapse the sum over `(x, d, y)` to a per-cell expression have hsum : (∑ z : Obs C, obsReal m g z * aipwScoreFin mhat ghat z) = (Fintype.card C : ℝ)⁻¹ * ∑ x : C, ((ghat true x - ghat false x) + m x / mhat x * (g true x - ghat true x) - (1 - m x) / (1 - mhat x) * (g false x - ghat false x)) := by rw [Fintype.sum_prod_type, Finset.mul_sum] refine Finset.sum_congr rfl fun x _ => ?_ simp only [Fintype.sum_prod_type, Fintype.sum_bool, obsReal, aipwScoreFin, yReal, cond_true, cond_false, if_true, if_false, Bool.false_eq_true] have h0 := hm0 x; have h1 := hm1 x field_simp ring rw [hsum] unfold ate rw [← mul_sub, ← Finset.sum_sub_distrib] congr 1 refine Finset.sum_congr rfl fun x _ => ?_ have h0 := hm0 x; have h1 := hm1 x field_simp ring

theorem aipw_bias_bound [Nonempty C] {m : C → ℝ} {g : Bool → C → ℝ} (mhat : C → ℝ) (ghat : Bool → C → ℝ) {ε : ℝ} (hε : 0 < ε) (hco : ∀ x, ε ≤ mhat x ∧ ε ≤ 1 - mhat x) : |(∑ z : Obs C, obsReal m g z * aipwScoreFin mhat ghat z) - ate g| ≤ ε⁻¹ * ((sqrt (l2sq (g true) (ghat true)) + sqrt (l2sq (g false) (ghat false))) * sqrt (l2sq m mhat)) := by have hmhat : ∀ x, 0 < mhat x := fun x => lt_of_lt_of_le hε (hco x).1 have hmhat1 : ∀ x, mhat x < 1 := fun x => by linarith [(hco x).2] rw [aipw_bias_identity mhat ghat hmhat hmhat1] have hCinv : (0 : ℝ) ≤ (Fintype.card C : ℝ)⁻¹ := by positivity -- general discrete Cauchy–Schwarz over the `L²(P_X)` inner product have hCS : ∀ (a b : C → ℝ), (Fintype.card C : ℝ)⁻¹ * ∑ x, |a x| * |b x| ≤ sqrt ((Fintype.card C : ℝ)⁻¹ * ∑ x, a x ^ 2) * sqrt ((Fintype.card C : ℝ)⁻¹ * ∑ x, b x ^ 2) := by intro a b have hcs : (∑ x, |a x| * |b x|) ^ 2 ≤ (∑ x, |a x| ^ 2) * ∑ x, |b x| ^ 2 := Finset.sum_mul_sq_le_sq_mul_sq Finset.univ _ _ have hsq : ∀ (f : C → ℝ), ∑ x, |f x| ^ 2 = ∑ x, f x ^ 2 := by intro f; refine Finset.sum_congr rfl fun x _ => ?_; rw [sq_abs] rw [hsq, hsq] at hcs have hsum_nonneg : (0 : ℝ) ≤ ∑ x, |a x| * |b x| := sum_nonneg fun x _ => mul_nonneg (abs_nonneg _) (abs_nonneg _) have ha2 : (0 : ℝ) ≤ ∑ x, a x ^ 2 := sum_nonneg fun x _ => sq_nonneg _ have hb2 : (0 : ℝ) ≤ ∑ x, b x ^ 2 := sum_nonneg fun x _ => sq_nonneg _ -- `∑ |a||b| ≤ √(∑a²)·√(∑b²)` have hstep : (∑ x, |a x| * |b x|) ≤ sqrt (∑ x, a x ^ 2) * sqrt (∑ x, b x ^ 2) := by rw [← Real.sqrt_mul ha2] exact (Real.le_sqrt hsum_nonneg (mul_nonneg ha2 hb2)).mpr hcs -- multiply through by `(card C)⁻¹` and absorb into the two square roots rw [Real.sqrt_mul hCinv, Real.sqrt_mul hCinv, mul_mul_mul_comm, Real.mul_self_sqrt hCinv] exact mul_le_mul_of_nonneg_left hstep hCinv -- per-cell doubly-robust bound: `|bracket x| ≤ |Δm x|·(|Δg₁ x| + |Δg₀ x|)/ε` have hcell : ∀ x : C, |(1 - m x / mhat x) * (ghat true x - g true x) - (1 - (1 - m x) / (1 - mhat x)) * (ghat false x - g false x)| ≤ |m x - mhat x| * (|ghat true x - g true x| + |ghat false x - g false x|) * ε⁻¹ := by intro x obtain ⟨hco1, hco2⟩ := hco x have hp : 0 < mhat x := hmhat x have hq : (0:ℝ) < 1 - mhat x := by linarith [hmhat1 x] have e1 : 1 - m x / mhat x = (mhat x - m x) / mhat x := by field_simp have e2 : 1 - (1 - m x) / (1 - mhat x) = (m x - mhat x) / (1 - mhat x) := by field_simp; ring rw [e1, e2] have hpε : (mhat x)⁻¹ ≤ ε⁻¹ := by rw [inv_le_inv₀ hp hε]; exact hco1 have hqε : (1 - mhat x)⁻¹ ≤ ε⁻¹ := by rw [inv_le_inv₀ hq hε]; exact hco2 calc |(mhat x - m x) / mhat x * (ghat true x - g true x) - (m x - mhat x) / (1 - mhat x) * (ghat false x - g false x)| ≤ |(mhat x - m x) / mhat x * (ghat true x - g true x)| + |(m x - mhat x) / (1 - mhat x) * (ghat false x - g false x)| := abs_sub _ _ _ = |m x - mhat x| * (mhat x)⁻¹ * |ghat true x - g true x| + |m x - mhat x| * (1 - mhat x)⁻¹ * |ghat false x - g false x| := by rw [abs_mul, abs_mul, abs_div, abs_div, abs_of_pos hp, abs_of_pos hq, abs_sub_comm (mhat x), div_eq_mul_inv, div_eq_mul_inv] _ ≤ |m x - mhat x| * ε⁻¹ * |ghat true x - g true x| + |m x - mhat x| * ε⁻¹ * |ghat false x - g false x| := by gcongr _ = |m x - mhat x| * (|ghat true x - g true x| + |ghat false x - g false x|) * ε⁻¹ := by ring -- each Cauchy–Schwarz half, with the outcome arm aligned to `l2sq` have hhalf : ∀ d : Bool, (Fintype.card C : ℝ)⁻¹ * ∑ x, |m x - mhat x| * |ghat d x - g d x| ≤ sqrt (l2sq m mhat) * sqrt (l2sq (g d) (ghat d)) := by intro d have h := hCS (fun x => m x - mhat x) (fun x => ghat d x - g d x) refine h.trans (le_of_eq ?_) have hl2m : (Fintype.card C : ℝ)⁻¹ * ∑ x, (m x - mhat x) ^ 2 = l2sq m mhat := rfl have hl2g : (Fintype.card C : ℝ)⁻¹ * ∑ x, (ghat d x - g d x) ^ 2 = l2sq (g d) (ghat d) := by unfold l2sq congr 1 refine Finset.sum_congr rfl fun x _ => ?_ rw [← neg_sub (g d x) (ghat d x), neg_sq] rw [hl2m, hl2g] -- assemble: triangle inequality + per-cell bound + split + Cauchy–Schwarz rw [abs_mul, abs_of_nonneg hCinv] calc (Fintype.card C : ℝ)⁻¹ * |∑ x, ((1 - m x / mhat x) * (ghat true x - g true x) - (1 - (1 - m x) / (1 - mhat x)) * (ghat false x - g false x))| ≤ (Fintype.card C : ℝ)⁻¹ * ∑ x, |m x - mhat x| * (|ghat true x - g true x| + |ghat false x - g false x|) * ε⁻¹ := by apply mul_le_mul_of_nonneg_left _ hCinv exact (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum fun x _ => hcell x) _ = ε⁻¹ * (((Fintype.card C : ℝ)⁻¹ * ∑ x, |m x - mhat x| * |ghat true x - g true x|) + ((Fintype.card C : ℝ)⁻¹ * ∑ x, |m x - mhat x| * |ghat false x - g false x|)) := by rw [Finset.mul_sum, Finset.mul_sum, Finset.mul_sum, ← Finset.sum_add_distrib, Finset.mul_sum] refine Finset.sum_congr rfl fun x _ => ?_ ring _ ≤ ε⁻¹ * ((sqrt (l2sq m mhat) * sqrt (l2sq (g true) (ghat true))) + (sqrt (l2sq m mhat) * sqrt (l2sq (g false) (ghat false)))) := by apply mul_le_mul_of_nonneg_left _ (by positivity) exact add_le_add (hhalf true) (hhalf false) _ = ε⁻¹ * ((sqrt (l2sq (g true) (ghat true)) + sqrt (l2sq (g false) (ghat false))) * sqrt (l2sq m mhat)) := by ring

theorem aipw_var_bound [Nonempty C] {m : C → ℝ} {g : Bool → C → ℝ} (hv : ValidDGP m g) (mhat : C → ℝ) (ghat : Bool → C → ℝ) (hghat : ValidDGP mhat ghat) {ε : ℝ} (hε : 0 < ε) (hco : ∀ x, ε ≤ mhat x ∧ ε ≤ 1 - mhat x) (n : ℕ) : variance (estAIPW mhat ghat n) (productLaw hv n) ≤ (1 + 2 / ε) ^ 2 / n := by set B : ℝ := 1 + 2 / ε with hBdef have hB0 : (0 : ℝ) ≤ B := by rw [hBdef]; positivity -- the single-observation score and its bound set score : Obs C → ℝ := aipwScoreFin mhat ghat with hscore have hbound : ∀ z, |score z| ≤ B := fun z => aipwScore_bound mhat ghat hghat hε hco z have hmeas : Measurable score := measurable_of_finite score have haes : AEStronglyMeasurable score (obsLaw hv) := hmeas.aestronglyMeasurable have hmem : MemLp score 2 (obsLaw hv) := MemLp.of_bound haes B (Filter.Eventually.of_forall fun z => by rw [Real.norm_eq_abs]; exact hbound z) -- `Var[score] ≤ B²` have hvar_score : variance score (obsLaw hv) ≤ B ^ 2 := by refine (variance_le_expectation_sq haes).trans ?_ have hsq : ∀ z, (score ^ 2) z ≤ B ^ 2 := by intro z have := hbound z have h2 : score z ^ 2 ≤ B ^ 2 := by nlinarith [abs_nonneg (score z), sq_abs (score z)] simpa using h2 calc ∫ z, (score ^ 2) z ∂(obsLaw hv) ≤ ∫ _z, B ^ 2 ∂(obsLaw hv) := integral_mono_of_nonneg (Filter.Eventually.of_forall fun z => sq_nonneg _) (integrable_const _) (Filter.Eventually.of_forall hsq) _ = B ^ 2 := by rw [integral_const, probReal_univ, smul_eq_mul, one_mul] rcases Nat.eq_zero_or_pos n with hn | hn · subst hn have hconst : estAIPW mhat ghat 0 = (0 : (Fin 0 → Obs C) → ℝ) := by funext s; simp [estAIPW] rw [hconst, variance_zero] simp · have hne : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn.ne' -- express the estimator as a scalar multiple of the sample sum of the score have hsmul : estAIPW mhat ghat n = (n : ℝ)⁻¹ • (∑ i, fun ω : Fin n → Obs C => score (ω i)) := by funext sample simp only [estAIPW, Pi.smul_apply, Finset.sum_apply, smul_eq_mul, hscore] -- the variance of the sample sum splits over the iid coordinates have hsum_var : variance (∑ i, fun ω : Fin n → Obs C => score (ω i)) (productLaw hv n) = (n : ℝ) * variance score (obsLaw hv) := by rw [productLaw, variance_sum_pi (fun _ => hmem), Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] rw [hsmul, variance_smul, hsum_var] -- `n⁻¹² · (n · Var) ≤ n⁻¹² · (n · B²) = B²/n` have hkey : (n : ℝ)⁻¹ ^ 2 * ((n : ℝ) * variance score (obsLaw hv)) ≤ (n : ℝ)⁻¹ ^ 2 * ((n : ℝ) * B ^ 2) := by gcongr refine hkey.trans (le_of_eq ?_) field_simp