Estimation.CATE.Kennedy

theorem cate_linear_smoother_bias_bound (S : CATEEstimationSystem P γ) {ε : ℝ} (h_overlap : S.toBackdoorEstimationSystem.StrictOverlap ε) (op : LinearSmootherOp P.Ω P.μ γ) (η_hat : ℕ → P.Ω → NuisanceVec γ) (n : ℕ) (ω : P.Ω) (x : γ) {ι : Type*} (B : Finset ι) (w : ι → ℝ) (xs : ι → γ × Bool × ℝ) (c_n p q : ℝ) (h_overlap_η_hat : η_hat n ω ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε) (hLin : LinearSmootherOp.IsLinearSmoother op n ω x B w xs) (hWeights : ∑ i ∈ B, |w i| ≤ c_n) (hConj : HolderConjugate p q) : |op.evalAt n ω (fun z => condBias (η_hat n ω) S.toBackdoorEstimationSystem.η₀ z.1) x| ≤ BackdoorEstimationSystem.aipw_rem_const ε * c_n * WeightedNorm B w (fun i => (η_hat n ω).e_fn (xs i).1 - S.e_val (xs i).1) p * (∑ a : Bool, WeightedNorm B w (fun i => (η_hat n ω).μ_fn a (xs i).1 - S.μ_val a (xs i).1) q) := by classical let η : NuisanceVec γ := η_hat n ω let C : ℝ := BackdoorEstimationSystem.aipw_rem_const ε let de : γ → ℝ := fun y => η.e_fn y - S.e_val y let dμ : Bool → γ → ℝ := fun a y => η.μ_fn a y - S.μ_val a y have hC_ge_inv : ε⁻¹ ≤ C := by unfold C BackdoorEstimationSystem.aipw_rem_const have hpos : 0 < ε := h_overlap.1 have hone : 0 < 1 - ε := by linarith [h_overlap.2.1] have hden : 0 < ε * (1 - ε) := mul_pos hpos hone rw [div_eq_mul_inv] field_simp [hpos.ne', hden.ne'] nlinarith [h_overlap.2.1] have hC_nonneg : 0 ≤ C := (inv_nonneg.mpr h_overlap.1.le).trans hC_ge_inv have hη_lower : ∀ y, ε ≤ η.e_fn y := fun y => (h_overlap_η_hat y).1 have hη_upper : ∀ y, η.e_fn y ≤ 1 - ε := fun y => (h_overlap_η_hat y).2 have hη_pos : ∀ y, 0 < η.e_fn y := fun y => lt_of_lt_of_le h_overlap.1 (hη_lower y) have hη_false_pos : ∀ y, 0 < 1 - η.e_fn y := by intro y have : ε ≤ 1 - η.e_fn y := by linarith [hη_upper y] exact lt_of_lt_of_le h_overlap.1 this have hpoint : ∀ y, |condBias η S.toBackdoorEstimationSystem.η₀ y| ≤ C * ∑ a : Bool, |de y| * |dμ a y| := by intro y have hdenT : η.e_fn y ≠ 0 := (hη_pos y).ne' have hdenF : 1 - η.e_fn y ≠ 0 := (hη_false_pos y).ne' have hinvT : |(η.e_fn y)⁻¹| ≤ C := by have hle : (η.e_fn y)⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ (hη_pos y) h_overlap.1).2 (hη_lower y) rw [abs_of_pos (inv_pos.mpr (hη_pos y))] exact hle.trans hC_ge_inv have hinvF : |(1 - η.e_fn y)⁻¹| ≤ C := by have hden : ε ≤ 1 - η.e_fn y := by linarith [hη_upper y] have hle : (1 - η.e_fn y)⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ (hη_false_pos y) h_overlap.1).2 hden rw [abs_of_pos (inv_pos.mpr (hη_false_pos y))] exact hle.trans hC_ge_inv have hT : |(de y * dμ true y) / η.e_fn y| ≤ C * (|de y| * |dμ true y|) := by calc |(de y * dμ true y) / η.e_fn y| = |de y| * |dμ true y| * |(η.e_fn y)⁻¹| := by rw [div_eq_mul_inv] simp [abs_mul, mul_assoc, mul_comm] _ ≤ |de y| * |dμ true y| * C := mul_le_mul_of_nonneg_left hinvT (mul_nonneg (abs_nonneg _) (abs_nonneg _)) _ = C * (|de y| * |dμ true y|) := by ring have hF : |(de y * dμ false y) / (1 - η.e_fn y)| ≤ C * (|de y| * |dμ false y|) := by calc |(de y * dμ false y) / (1 - η.e_fn y)| = |de y| * |dμ false y| * |(1 - η.e_fn y)⁻¹| := by rw [div_eq_mul_inv] simp [abs_mul, mul_assoc, mul_comm] _ ≤ |de y| * |dμ false y| * C := mul_le_mul_of_nonneg_left hinvF (mul_nonneg (abs_nonneg _) (abs_nonneg _)) _ = C * (|de y| * |dμ false y|) := by ring calc |condBias η S.toBackdoorEstimationSystem.η₀ y| = |(de y * dμ true y) / η.e_fn y + (de y * dμ false y) / (1 - η.e_fn y)| := by simp [condBias, BackdoorEstimationSystem.η₀, de, dμ] _ ≤ |(de y * dμ true y) / η.e_fn y| + |(de y * dμ false y) / (1 - η.e_fn y)| := abs_add_le _ _ _ ≤ C * (|de y| * |dμ true y|) + C * (|de y| * |dμ false y|) := add_le_add hT hF _ = C * ∑ a : Bool, |de y| * |dμ a y| := by simp ring let absOp : LinearSmootherOp P.Ω P.μ γ := { evalAt := fun _ _ f _ => ∑ i ∈ B, |w i| * f (xs i) meas_evalAt_const := by intro _ c simpa using (measurable_const : Measurable (fun _ : P.Ω × γ => ∑ i ∈ B, |w i| * c)) weights := fun _ _ _ _ => 0 } have hAbsLin : LinearSmootherOp.IsLinearSmoother absOp n ω x B (fun i => |w i|) xs := by intro f rfl have hAbsWeights : ∑ i ∈ B, |(|w i|)| ≤ c_n := by simpa [abs_of_nonneg] using hWeights have hProd : ∀ a : Bool, ∑ i ∈ B, |w i| * (|de (xs i).1| * |dμ a (xs i).1|) ≤ c_n * WeightedNorm B w (fun i => de (xs i).1) p * WeightedNorm B w (fun i => dμ a (xs i).1) q := by intro a have h := smoother_bias_product_holder absOp n ω x (fun y => |de y|) (fun y => |dμ a y|) B (fun i => |w i|) xs c_n p q hAbsLin hAbsWeights hConj have hsum_nonneg : 0 ≤ ∑ i ∈ B, |w i| * (|de (xs i).1| * |dμ a (xs i).1|) := by refine sum_nonneg ?_ intro i hi positivity simpa [absOp, WeightedNorm, abs_of_nonneg, hsum_nonneg, de, dμ, mul_assoc] using h have hEval : op.evalAt n ω (fun z => condBias (η_hat n ω) S.toBackdoorEstimationSystem.η₀ z.1) x = ∑ i ∈ B, w i * condBias η S.toBackdoorEstimationSystem.η₀ (xs i).1 := by simpa [η] using hLin (fun z => condBias (η_hat n ω) S.toBackdoorEstimationSystem.η₀ z.1) have hMain : |∑ i ∈ B, w i * condBias η S.toBackdoorEstimationSystem.η₀ (xs i).1| ≤ C * c_n * WeightedNorm B w (fun i => de (xs i).1) p * (∑ a : Bool, WeightedNorm B w (fun i => dμ a (xs i).1) q) := by calc |∑ i ∈ B, w i * condBias η S.toBackdoorEstimationSystem.η₀ (xs i).1| ≤ ∑ i ∈ B, |w i * condBias η S.toBackdoorEstimationSystem.η₀ (xs i).1| := Finset.abs_sum_le_sum_abs _ _ _ = ∑ i ∈ B, |w i| * |condBias η S.toBackdoorEstimationSystem.η₀ (xs i).1| := by simp [abs_mul] _ ≤ ∑ i ∈ B, |w i| * (C * ∑ a : Bool, |de (xs i).1| * |dμ a (xs i).1|) := by refine Finset.sum_le_sum ?_ intro i hi exact mul_le_mul_of_nonneg_left (hpoint (xs i).1) (abs_nonneg _) _ = C * ∑ a : Bool, ∑ i ∈ B, |w i| * (|de (xs i).1| * |dμ a (xs i).1|) := by simp only [Fintype.sum_bool, Finset.mul_sum, mul_add, Finset.sum_add_distrib] congr 1 <;> (refine Finset.sum_congr rfl ?_; intro i _; ring) _ ≤ C * ∑ a : Bool, (c_n * WeightedNorm B w (fun i => de (xs i).1) p * WeightedNorm B w (fun i => dμ a (xs i).1) q) := by exact mul_le_mul_of_nonneg_left (Finset.sum_le_sum (fun a _ => hProd a)) hC_nonneg _ = C * c_n * WeightedNorm B w (fun i => de (xs i).1) p * (∑ a : Bool, WeightedNorm B w (fun i => dμ a (xs i).1) q) := by simp only [Fintype.sum_bool] ring simpa [hEval, C, de, dμ, η] using hMain

theorem cate_dr_oracle_efficient_linear (S : CATEEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) {ε : ℝ} (_h_overlap : S.toBackdoorEstimationSystem.StrictOverlap ε) (op : LinearSmootherOp P.Ω P.μ γ) (η_hat : ℕ → P.Ω → NuisanceVec γ) (x : γ) (d_n : ℕ → P.Ω → ℝ) (BiasIdent : (ℕ → P.Ω → γ × Bool × ℝ → ℝ) → (γ × Bool × ℝ → ℝ) → (ℕ → P.Ω → γ → ℝ) → Prop) (hStab : Stable op.toSecondStageOperator S.τ_val d_n x BiasIdent) (hCons : Tendsto_inProb d_n (fun _ => 0) P.μ) (hBias : BiasIdent (fun n ω z => phi_eta z (η_hat n ω)) (fun z => phi₀ S z) (fun n ω u => condBias (η_hat n ω) S.toBackdoorEstimationSystem.η₀ u)) (hSmoothedBias : IsLittleOp (fun n ω => op.evalAt n ω (fun z => condBias (η_hat n ω) S.toBackdoorEstimationSystem.η₀ z.1) x) (fun n => drOracleRiskScale S op.toSecondStageOperator x n) P.μ) : IsLittleOp (fun n ω => drLearnerEstimator S op.toSecondStageOperator η_hat n ω x - drOracleEstimator S op.toSecondStageOperator n ω x) (fun n => drOracleRiskScale S op.toSecondStageOperator x n) P.μ := dr_oracle_efficient S hA op.toSecondStageOperator η_hat x d_n BiasIdent hStab hCons hBias hSmoothedBias

theorem dr_oracle_expansion (S : CATEEstimationSystem P γ) (_hA : S.toPOBackdoorSystem.Assumptions) (op : SecondStageOperator P.Ω P.μ γ) (η_hat : ℕ → P.Ω → NuisanceVec γ) (x : γ) (d_n : ℕ → P.Ω → ℝ) (BiasIdent : (ℕ → P.Ω → γ × Bool × ℝ → ℝ) → (γ × Bool × ℝ → ℝ) → (ℕ → P.Ω → γ → ℝ) → Prop) (hStab : Stable op S.τ_val d_n x BiasIdent) (hCons : Tendsto_inProb d_n (fun _ => 0) P.μ) (hBias : BiasIdent (fun n ω z => phi_eta z (η_hat n ω)) (fun z => phi₀ S z) (fun n ω u => condBias (η_hat n ω) S.toBackdoorEstimationSystem.η₀ u)) : IsLittleOp (fun n ω => drLearnerEstimator S op η_hat n ω x - drOracleEstimator S op n ω x - op.evalAt n ω (fun z => condBias (η_hat n ω) S.toBackdoorEstimationSystem.η₀ z.1) x) (fun n => drOracleRiskScale S op x n) P.μ := by unfold drLearnerEstimator drOracleEstimator drOracleRiskScale exact oracle_expansion op S.τ_val x d_n (fun n ω z => phi_eta z (η_hat n ω)) (fun z => phi₀ S z) (fun n ω u => condBias (η_hat n ω) S.toBackdoorEstimationSystem.η₀ u) BiasIdent hStab hCons hBias

theorem dr_oracle_efficient (S : CATEEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (op : SecondStageOperator P.Ω P.μ γ) (η_hat : ℕ → P.Ω → NuisanceVec γ) (x : γ) (d_n : ℕ → P.Ω → ℝ) (BiasIdent : (ℕ → P.Ω → γ × Bool × ℝ → ℝ) → (γ × Bool × ℝ → ℝ) → (ℕ → P.Ω → γ → ℝ) → Prop) (hStab : Stable op S.τ_val d_n x BiasIdent) (hCons : Tendsto_inProb d_n (fun _ => 0) P.μ) (hBias : BiasIdent (fun n ω z => phi_eta z (η_hat n ω)) (fun z => phi₀ S z) (fun n ω u => condBias (η_hat n ω) S.toBackdoorEstimationSystem.η₀ u)) (hSmoothedBias : IsLittleOp (fun n ω => op.evalAt n ω (fun z => condBias (η_hat n ω) S.toBackdoorEstimationSystem.η₀ z.1) x) (fun n => drOracleRiskScale S op x n) P.μ) : IsLittleOp (fun n ω => drLearnerEstimator S op η_hat n ω x - drOracleEstimator S op n ω x) (fun n => drOracleRiskScale S op x n) P.μ := by have hExp := dr_oracle_expansion S hA op η_hat x d_n BiasIdent hStab hCons hBias have hrn_nonneg : ∀ᶠ n : ℕ in atTop, 0 ≤ drOracleRiskScale S op x n := Filter.Eventually.of_forall (fun n => by unfold drOracleRiskScale SecondStageOperator.oracleRiskScale exact Real.sqrt_nonneg _) have hSum := IsLittleOp.add_eventually_nonneg_rate (μ := P.μ) hrn_nonneg hExp hSmoothedBias convert hSum using 1 funext n ω ring