Estimation.NPIV.DR

lemma trae_dr_estimator_eq_avg_phi {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} (S : InverseProblemSystem Ω μ) {P_W : Measure S.𝒲} (sample : IIDSample Ω S.𝒲 μ P_W) (split : OneShotSplit sample) (h_hat : ℕ → Ω → (S.𝒳 → ℝ)) (q_hat : ℕ → Ω → (S.𝒵 → ℝ)) (n : ℕ) (ω : Ω) : trae_dr_estimator S sample split h_hat q_hat n ω = ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, S.phiVal (h_hat n ω) (q_hat n ω) (sample.Z i ω) := rfl

theorem trae_dr_isAsymLinear {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] (S : InverseProblemSystem Ω μ) {q₀ : S.𝒵 → ℝ} (hq₀ : S.DualSolution q₀) {P_W : Measure S.𝒲} [IsProbabilityMeasure P_W] (sample : IIDSample Ω S.𝒲 μ P_W) (split : OneShotSplit sample) (h_hat : ℕ → Ω → (S.𝒳 → ℝ)) (q_hat : ℕ → Ω → (S.𝒵 → ℝ)) (_hyps : TRAEDRRemainderHyps S hq₀ sample split h_hat q_hat) (h_law_W : μ.map S.W = P_W) (hρ₀_meas : Measurable (ρ₀ S q₀)) : IsAsymLinear (trae_dr_estimator S sample split h_hat q_hat) S.θ₀ (ρ₀ S q₀) sample split.foldB := by refine ⟨mean_zero_of_DualSolution S hq₀ h_law_W hρ₀_meas, _hyps.finite_var, ?_⟩ have h_add_one : ∀ {Xn Yn : ℕ → Ω → ℝ}, IsLittleOp Xn (fun _ => (1 : ℝ)) μ → IsLittleOp Yn (fun _ => (1 : ℝ)) μ → IsLittleOp (fun n ω => Xn n ω + Yn n ω) (fun _ => (1 : ℝ)) μ := by intro Xn Yn hX hY ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ by_cases hδtop : δ = ⊤ · filter_upwards with n simp [hδtop] have hδpos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop let α : ℝ := δ.toReal / 4 have hαpos : 0 < α := by dsimp [α] linarith let A : ℕ → Set Ω := fun n => {ω | (ε / 2) * (1 : ℝ) < |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | (ε / 2) * (1 : ℝ) < |Yn n ω|} let C : ℕ → Set Ω := fun n => {ω | ε * (1 : ℝ) < |Xn n ω + Yn n ω|} have hXevent_le := (ENNReal.tendsto_nhds_zero.mp (hX (ε / 2) (by linarith))) (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) have hYevent_le := (ENNReal.tendsto_nhds_zero.mp (hY (ε / 2) (by linarith))) (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) have htwo_alpha_lt_delta : ofReal (2 * α) < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [α] linarith · dsimp [α] linarith [le_of_lt hδpos] · exact hδtop filter_upwards [hXevent_le, hYevent_le] with n hXA hYB have hsubset : C n ⊆ A n ∪ B n := by intro ω hω by_contra hnot have hnotA : ¬ ε / 2 < |Xn n ω| := by intro hx exact hnot (inl (by simpa [A] using hx)) have hnotB : ¬ ε / 2 < |Yn n ω| := by intro hy exact hnot (inr (by simpa [B] using hy)) have hXle : |Xn n ω| ≤ ε / 2 := le_of_not_gt hnotA have hYle : |Yn n ω| ≤ ε / 2 := le_of_not_gt hnotB have hsum : |Xn n ω + Yn n ω| ≤ ε := by calc |Xn n ω + Yn n ω| ≤ |Xn n ω| + |Yn n ω| := abs_add_le _ _ _ ≤ ε / 2 + ε / 2 := add_le_add hXle hYle _ = ε := by ring exact not_lt_of_ge hsum (by simpa [C] using hω) exact le_of_lt <| calc μ {ω | ε * (fun _ => (1 : ℝ)) n < |Xn n ω + Yn n ω|} = μ (C n) := by simp [C] _ ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) _ ≤ ofReal α + ofReal α := add_le_add hXA hYB _ = ofReal (2 * α) := by rw [← ENNReal.ofReal_add] · congr 1 ring · linarith · linarith _ < δ := htwo_alpha_lt_delta let EP : ℕ → Ω → ℝ := fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, (S.phiVal (h_hat n ω) (q_hat n ω) (sample.Z i ω) - S.phiVal S.h₀ q₀ (sample.Z i ω)) - sqrt ((split.foldB n).card : ℝ) * ∫ ω', (S.phiVal (h_hat n ω) (q_hat n ω) (S.W ω') - S.phiVal S.h₀ q₀ (S.W ω')) ∂μ let MB : ℕ → Ω → ℝ := fun n ω => sqrt ((split.foldB n).card : ℝ) * ∫ ω', (q₀ (S.zOf (S.W ω')) - q_hat n ω (S.zOf (S.W ω'))) * (h_hat n ω (S.xOf (S.W ω')) - S.h₀ (S.xOf (S.W ω'))) ∂μ have hsum : IsLittleOp (fun n ω => EP n ω + MB n ω) (fun _ => (1 : ℝ)) μ := by exact h_add_one _hyps.ep_remainder _hyps.mixed_bias have h_eq : ∀ n ω, sqrt ((split.foldB n).card : ℝ) * (trae_dr_estimator S sample split h_hat q_hat n ω - S.θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, ρ₀ S q₀ (sample.Z i ω) = EP n ω + MB n ω := by intro n ω have hrange := _hyps.candidate_mem n ω have hphi_hat_int : Integrable (fun ω' => S.phiVal (h_hat n ω) (q_hat n ω) (S.W ω')) μ := by unfold InverseProblemSystem.phiVal exact ((S.integrable_m_e (h_hat n ω) hrange.1).add (S.integrable_m (q_hat n ω) hrange.2)).sub (S.integrable_qh (h_hat n ω) hrange.1 (q_hat n ω) hrange.2) have hphi_zero_int : Integrable (fun ω' => S.phiVal S.h₀ q₀ (S.W ω')) μ := by unfold InverseProblemSystem.phiVal exact ((S.integrable_m_e S.h₀ S.h₀_mem).add (S.integrable_m q₀ hq₀.mem)).sub (S.integrable_qh S.h₀ S.h₀_mem q₀ hq₀.mem) have h_int_eq : (∫ ω', (S.phiVal (h_hat n ω) (q_hat n ω) (S.W ω') - S.phiVal S.h₀ q₀ (S.W ω')) ∂μ) = ∫ ω', (q₀ (S.zOf (S.W ω')) - q_hat n ω (S.zOf (S.W ω'))) * (h_hat n ω (S.xOf (S.W ω')) - S.h₀ (S.xOf (S.W ω'))) ∂μ := by rw [integral_sub hphi_hat_int hphi_zero_int] have hmb := mixed_bias_identity S hq₀ hrange.1 hrange.2 have hzero := Θ_q₀_eq_θ₀ S hq₀ S.h₀_mem unfold InverseProblemSystem.Θ InverseProblemSystem.phi at hmb hzero rw [hzero] simpa [InverseProblemSystem.X, InverseProblemSystem.Z] using hmb by_cases hcard : (split.foldB n).card = 0 · have hempty : split.foldB n = ∅ := Finset.card_eq_zero.mp hcard simp [EP, MB, h_int_eq, trae_dr_estimator, ρ₀, hempty] · have hcard_pos_nat : 0 < (split.foldB n).card := Nat.pos_of_ne_zero hcard have hcard_pos_real : 0 < ((split.foldB n).card : ℝ) := by exact_mod_cast hcard_pos_nat have hsqrt_ne : sqrt ((split.foldB n).card : ℝ) ≠ 0 := by intro hsqrt_zero have hzero_real : ((split.foldB n).card : ℝ) = 0 := by rw [← Real.mul_self_sqrt (le_of_lt hcard_pos_real), hsqrt_zero, zero_mul] exact (ne_of_gt hcard_pos_real) hzero_real have hsqrt_sq : sqrt ((split.foldB n).card : ℝ) * sqrt ((split.foldB n).card : ℝ) = ((split.foldB n).card : ℝ) := Real.mul_self_sqrt (by positivity) have h_sqrt_mul_inv_card : sqrt ((split.foldB n).card : ℝ) * (((split.foldB n).card : ℝ)⁻¹) = (sqrt ((split.foldB n).card : ℝ))⁻¹ := by let r : ℝ := sqrt ((split.foldB n).card : ℝ) let c : ℝ := ((split.foldB n).card : ℝ) have hr : r ≠ 0 := by simpa [r] using hsqrt_ne have hsq : r * r = c := by simp [r, c, hsqrt_sq] change r * c⁻¹ = r⁻¹ rw [← hsq] field_simp [hr] have h_inv_sqrt_mul_card : (sqrt ((split.foldB n).card : ℝ))⁻¹ * ((split.foldB n).card : ℝ) = sqrt ((split.foldB n).card : ℝ) := by let r : ℝ := sqrt ((split.foldB n).card : ℝ) let c : ℝ := ((split.foldB n).card : ℝ) have hr : r ≠ 0 := by simpa [r] using hsqrt_ne have hsq : r * r = c := by simp [r, c, hsqrt_sq] change r⁻¹ * c = r rw [← hsq] field_simp [hr] simp [EP, MB, h_int_eq, trae_dr_estimator, ρ₀, Finset.sum_sub_distrib] rw [mul_sub] rw [← mul_assoc (sqrt ((split.foldB n).card : ℝ)) (((split.foldB n).card : ℝ)⁻¹) (∑ i ∈ split.foldB n, S.phiVal (h_hat n ω) (q_hat n ω) (sample.Z i ω))] rw [h_sqrt_mul_inv_card] rw [mul_sub] rw [← mul_assoc (sqrt ((split.foldB n).card : ℝ))⁻¹ ((split.foldB n).card : ℝ) S.θ₀] rw [h_inv_sqrt_mul_card] ring convert hsum using 1 ext n ω exact h_eq n ω

theorem trae_dr_asymp_normal {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] (S : InverseProblemSystem Ω μ) {q₀ : S.𝒵 → ℝ} (hq₀ : S.DualSolution q₀) {P_W : Measure S.𝒲} [IsProbabilityMeasure P_W] (sample : IIDSample Ω S.𝒲 μ P_W) (split : OneShotSplit sample) (h_hat : ℕ → Ω → (S.𝒳 → ℝ)) (q_hat : ℕ → Ω → (S.𝒵 → ℝ)) (_hyps : TRAEDRRemainderHyps S hq₀ sample split h_hat q_hat) (h_law_W : μ.map S.W = P_W) (_h_ρ₀_meas : Measurable (ρ₀ S q₀)) (h_meas_θ : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (trae_dr_estimator S sample split h_hat q_hat) S.θ₀ split.foldB n) μ) (_h_meas_sum : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum sample (ρ₀ S q₀) split.foldB n) μ) : Tendsto_dist (IsAsymLinear.rescaledEstimator (trae_dr_estimator S sample split h_hat q_hat) S.θ₀ split.foldB) (gaussianMeasure 0 (∫ w, (ρ₀ S q₀ w) ^ 2 ∂P_W)) μ h_meas_θ := by have hAL : IsAsymLinear (trae_dr_estimator S sample split h_hat q_hat) S.θ₀ (ρ₀ S q₀) sample split.foldB := by exact trae_dr_isAsymLinear S hq₀ sample split h_hat q_hat _hyps h_law_W _h_ρ₀_meas exact hAL.tendsto_normal_foldB split _h_ρ₀_meas h_meas_θ _h_meas_sum

theorem trae_dr_studentized {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] (S : InverseProblemSystem Ω μ) {q₀ : S.𝒵 → ℝ} (hq₀ : S.DualSolution q₀) {P_W : Measure S.𝒲} [IsProbabilityMeasure P_W] (sample : IIDSample Ω S.𝒲 μ P_W) (split : OneShotSplit sample) (h_hat : ℕ → Ω → (S.𝒳 → ℝ)) (q_hat : ℕ → Ω → (S.𝒵 → ℝ)) (_hyps : TRAEDRRemainderHyps S hq₀ sample split h_hat q_hat) (h_law_W : μ.map S.W = P_W) (σ_hat_n : ℕ → Ω → ℝ) (σ₀ : ℝ) (_hσ₀_pos : 0 < σ₀) (_hσ_eq : σ₀ ^ 2 = ∫ w, (ρ₀ S q₀ w) ^ 2 ∂P_W) (_hσ_consistent : Tendsto_inProb σ_hat_n (fun _ => σ₀) μ) (h_ρ₀_meas : Measurable (ρ₀ S q₀)) (h_meas_θ : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (trae_dr_estimator S sample split h_hat q_hat) S.θ₀ split.foldB n) μ) (h_meas_sum : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum sample (ρ₀ S q₀) split.foldB n) μ) (h_studentized_meas : ∀ n, AEMeasurable (fun ω => sqrt ((split.foldB n).card : ℝ) * (trae_dr_estimator S sample split h_hat q_hat n ω - S.θ₀) / σ_hat_n n ω) μ) : Tendsto_dist (fun n ω => sqrt ((split.foldB n).card : ℝ) * (trae_dr_estimator S sample split h_hat q_hat n ω - S.θ₀) / σ_hat_n n ω) (gaussianMeasure 0 1) μ h_studentized_meas := by let Xn : ℕ → Ω → ℝ := IsAsymLinear.rescaledEstimator (trae_dr_estimator S sample split h_hat q_hat) S.θ₀ split.foldB have hAN : Tendsto_dist Xn (gaussianMeasure 0 (σ₀ ^ 2)) μ h_meas_θ := by have h := trae_dr_asymp_normal S hq₀ sample split h_hat q_hat _hyps h_law_W h_ρ₀_meas h_meas_θ h_meas_sum simpa [Xn, _hσ_eq] using h -- The studentized statistic is `Xn / σ̂ₙ`; apply the generic studentized CLT -- (`Tendsto_dist.div_tendsto_inProb_gaussian` in `Causalean/Stat/Studentize.lean`). have hdiv : ∀ n, AEMeasurable (fun ω => Xn n ω / σ_hat_n n ω) μ := by intro n simpa [Xn, IsAsymLinear.rescaledEstimator] using h_studentized_meas n have hres := Tendsto_dist.div_tendsto_inProb_gaussian _hσ₀_pos h_meas_θ hAN _hσ_consistent hdiv simpa [Xn, IsAsymLinear.rescaledEstimator] using hres

theorem trae_dr_wald_coverage {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] (S : InverseProblemSystem Ω μ) {q₀ : S.𝒵 → ℝ} (hq₀ : S.DualSolution q₀) {P_W : Measure S.𝒲} [IsProbabilityMeasure P_W] (sample : IIDSample Ω S.𝒲 μ P_W) (split : OneShotSplit sample) (h_hat : ℕ → Ω → (S.𝒳 → ℝ)) (q_hat : ℕ → Ω → (S.𝒵 → ℝ)) (_hyps : TRAEDRRemainderHyps S hq₀ sample split h_hat q_hat) (h_law_W : μ.map S.W = P_W) (σ_hat_n : ℕ → Ω → ℝ) (σ₀ : ℝ) (_hσ₀_pos : 0 < σ₀) (_hσ_eq : σ₀ ^ 2 = ∫ w, (ρ₀ S q₀ w) ^ 2 ∂P_W) (_hσ_consistent : Tendsto_inProb σ_hat_n (fun _ => σ₀) μ) (h_ρ₀_meas : Measurable (ρ₀ S q₀)) (h_meas_θ : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (trae_dr_estimator S sample split h_hat q_hat) S.θ₀ split.foldB n) μ) (h_meas_sum : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum sample (ρ₀ S q₀) split.foldB n) μ) (h_studentized_meas : ∀ n, AEMeasurable (fun ω => sqrt ((split.foldB n).card : ℝ) * (trae_dr_estimator S sample split h_hat q_hat n ω - S.θ₀) / σ_hat_n n ω) μ) (z : ℝ) (_hz_pos : 0 < z) : Tendsto (fun n => (μ {ω | |trae_dr_estimator S sample split h_hat q_hat n ω - S.θ₀| ≤ z * σ_hat_n n ω / sqrt ((split.foldB n).card : ℝ)}).toReal - (μ {ω | sqrt ((split.foldB n).card : ℝ) * (trae_dr_estimator S sample split h_hat q_hat n ω - S.θ₀) / σ_hat_n n ω ∈ Icc (-z) z}).toReal) atTop (𝓝 0) → Tendsto (fun n => (μ {ω | |trae_dr_estimator S sample split h_hat q_hat n ω - S.θ₀| ≤ z * σ_hat_n n ω / sqrt ((split.foldB n).card : ℝ)}).toReal) atTop (𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by intro h_wald_studentized let studentized : ℕ → Ω → ℝ := fun n ω => sqrt ((split.foldB n).card : ℝ) * (trae_dr_estimator S sample split h_hat q_hat n ω - S.θ₀) / σ_hat_n n ω let coverProb : ℕ → ℝ := fun n => (μ {ω | |trae_dr_estimator S sample split h_hat q_hat n ω - S.θ₀| ≤ z * σ_hat_n n ω / sqrt ((split.foldB n).card : ℝ)}).toReal let studProb : ℕ → ℝ := fun n => (μ {ω | studentized n ω ∈ Icc (-z) z}).toReal change Tendsto (fun n => coverProb n - studProb n) atTop (𝓝 0) at h_wald_studentized have hStud : Tendsto_dist studentized (gaussianMeasure 0 1) μ h_studentized_meas := by simpa [studentized] using trae_dr_studentized S hq₀ sample split h_hat q_hat _hyps h_law_W σ_hat_n σ₀ _hσ₀_pos _hσ_eq _hσ_consistent h_ρ₀_meas h_meas_θ h_meas_sum h_studentized_meas -- The portmanteau argument is now the generic `Tendsto_dist.wald_coverage` -- (in `Causalean/Stat/Studentize.lean`); the studentized limit `hStud` and the -- event-equivalence bridge `h_wald_studentized` are the only inputs. have hcover := Tendsto_dist.wald_coverage h_studentized_meas hStud _hz_pos coverProb h_wald_studentized simpa [coverProb] using hcover