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 hXlt : |Xn n ω| < ε / 2 := lt_of_not_ge hnotA have hYlt : |Yn n ω| < ε / 2 := lt_of_not_ge hnotB have hsum : |Xn n ω + Yn n ω| < ε := by calc |Xn n ω + Yn n ω| ≤ |Xn n ω| + |Yn n ω| := abs_add_le _ _ _ < ε / 2 + ε / 2 := add_lt_add hXlt hYlt _ = ε := by ring exact (not_le_of_gt 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) μ) : Modes.TendstoInLaw (fun _ : ℕ => μ) (IsAsymLinear.rescaledEstimator (trae_dr_estimator S sample split h_hat q_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 (∫ w, (ρ₀ S q₀ w) ^ 2 ∂P_W)) := 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 : Modes.TendstoInProbability (fun _ : ℕ => μ) σ_hat_n atTop (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 ω) μ) : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => sqrt ((split.foldB n).card : ℝ) * (trae_dr_estimator S sample split h_hat q_hat n ω - S.θ₀) / σ_hat_n n ω) atTop (gaussianMeasure 0 1) := by let Xn : ℕ → Ω → ℝ := IsAsymLinear.rescaledEstimator (trae_dr_estimator S sample split h_hat q_hat) S.θ₀ split.foldB have hAN : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop (gaussianMeasure 0 (σ₀ ^ 2)) := 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 -- (`Modes.TendstoInLaw.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 := Modes.TendstoInLaw.div_tendsto_inProb_gaussian hAN _hσ₀_pos _hσ_consistent hdiv simpa [Xn, IsAsymLinear.rescaledEstimator] using hres

theorem primal_l2_consistency_of_rate {Omega : Type*} [MeasurableSpace Omega] {mu : Measure Omega} (S : OperatorSystem Omega mu) {TC : TRAEClasses S} {P_W : Measure S.𝒲} {sample : IIDSample Omega S.𝒲 mu P_W} {split : OneShotSplit sample} {lambda_n : ℕ → ℝ} {beta : ℝ} {delta zeta : ℕ → ℝ} {h_hat : ℕ → Omega → S.𝒳 → ℝ} (is_estimator : IsTRAEPrimalEstimatorSequence S TC sample split lambda_n h_hat) (sc : SourceCondition S beta) (bias : TikhonovBiasBound S beta sc) [IsProbabilityMeasure mu] (hbeta : 0 < beta) (hlambda_pos : ∀ n, 0 < lambda_n n) (hlambda_lt : ∀ n, lambda_n n < 2) (regimes : ∀ n, LocalizedRegimes S TC sample sc { uniform := bias, lambda_pos := hlambda_pos n } (split.n₁ n) (delta n)) (hzeta_pos : ∀ n, 0 < zeta n) (hzeta_lt : ∀ n, zeta n < 1) (floors : ∀ n, PerSampleConfidenceFloor (regimes n) (zeta n)) (peeling : ∀ n, PeelingFloor (regimes n) (zeta n / 4)) (hzeta_zero : Tendsto zeta atTop (nhds 0)) (hdelta_zero : Tendsto delta atTop (nhds 0)) (hlambda_zero : Tendsto lambda_n atTop (nhds 0)) (hdelta_sq_div_lambda_zero : Tendsto (fun n => (delta n) ^ 2 / lambda_n n) atTop (nhds 0)) : Modes.TendstoInProbability (fun _ : ℕ => mu) (fun n omega => (eLpNorm (fun omega' => h_hat n omega (S.xOf (S.W omega')) - S.h₀ (S.xOf (S.W omega'))) 2 mu).toReal) atTop (fun _ _ => 0) := by let hmem : ∀ n omega, h_hat n omega ∈ S.Hbar := fun n omega => TC.H_subset (is_estimator.mem_H n omega) have hrate := Primal.primal_strongNorm_tendstoInProb_of_rates is_estimator sc bias hbeta hlambda_pos hlambda_lt regimes hzeta_pos hzeta_lt floors peeling hzeta_zero hdelta_zero hlambda_zero hdelta_sq_div_lambda_zero exact (primal_l2_consistency_iff_strongNorm S h_hat hmem).mp <| by simpa [hmem] using hrate