Stat.Inference

theorem expectedRestrictedVolume_affineInversion_frontier_le {Ω : Type*} [MeasurableSpace Ω] (Q : Measure Ω) [IsProbabilityMeasure Q] (region : Set ℝ) (hregionFinite : volume region ≠ ⊤) (A B K : Ω → ℝ) (n : ℕ) (L mu Kbar q kappa inflation Y t : ℝ) (hL : 0 ≤ L) (hmu : 0 < mu) (hn : 0 < n) (hK : ∀ w, 0 ≤ K w) (hKint : Integrable K Q) (hKbar : (∫ w, K w ∂Q) ≤ Kbar) (hbad : (Q {w | mu / 2 < |B w - mu|}).toReal ≤ q) (hkappa : 0 < kappa) (hinflation : 0 ≤ inflation) (hY : 0 ≤ Y) (hKbar_le : Kbar ≤ inflation * kappa) (hbadContribution : (volume region).toReal * q ≤ Y / t) (ht : t = (n : ℝ) * mu ^ 2 / kappa) : (∫ w, restrictedSetVolume region (affineInversionSet region (A w) (B w) (L * sqrt (K w / n))) ∂Q) ≤ max (volume region).toReal (4 * sqrt inflation * L + Y) * min 1 (t ^ (-1 / 2 : ℝ)) := by have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have htpos : 0 < t := by rw [ht]; positivity have hbase := expectedRestrictedVolume_affineInversion_le Q region hregionFinite A B K n L mu Kbar q hL hmu hn hK hKint hKbar hbad have hcap := expectedRestrictedVolume_affineInversion_le_region Q region hregionFinite A B (fun w => L * sqrt (K w / n)) have hsqrt : sqrt (Kbar / (n : ℝ)) ≤ sqrt (inflation * kappa / (n : ℝ)) := Real.sqrt_le_sqrt (div_le_div_of_nonneg_right hKbar_le hnR.le) have hratio : sqrt (inflation * kappa / (n : ℝ)) / mu = sqrt inflation / sqrt t := sqrt_mul_kappa_div_n_div_mu inflation n mu kappa t hinflation hnR hmu hkappa ht have hradius : 4 * L * sqrt (Kbar / (n : ℝ)) / mu ≤ (4 * sqrt inflation * L) / sqrt t := by calc 4 * L * sqrt (Kbar / (n : ℝ)) / mu ≤ 4 * L * sqrt (inflation * kappa / (n : ℝ)) / mu := by gcongr _ = 4 * L * (sqrt (inflation * kappa / (n : ℝ)) / mu) := by ring _ = (4 * sqrt inflation * L) / sqrt t := by rw [hratio] ring have hsum : 4 * L * sqrt (Kbar / (n : ℝ)) / mu + (volume region).toReal * q ≤ (4 * sqrt inflation * L) / sqrt t + Y / t := add_le_add hradius hbadContribution calc (∫ w, restrictedSetVolume region (affineInversionSet region (A w) (B w) (L * sqrt (K w / n))) ∂Q) ≤ min (volume region).toReal (4 * L * sqrt (Kbar / (n : ℝ)) / mu + (volume region).toReal * q) := le_min hcap hbase _ ≤ min (volume region).toReal ((4 * sqrt inflation * L) / sqrt t + Y / t) := min_le_min_left _ hsum _ ≤ max (volume region).toReal (4 * sqrt inflation * L + Y) * min 1 (t ^ (-1 / 2 : ℝ)) := inverseStrength_to_frontier hY htpos

theorem gaussianLimit_waldForm_map (hinj : Injective (secondMomentLM hψ hvar)) : (gaussianLimit hψ hvar).map (fun S => ⟪S, secondMomentInv hψ hvar hinj S⟫) = chiSqDist (finrank ℝ E) := by have hQmeas : Measurable (fun S : E => ⟪S, secondMomentInv hψ hvar hinj S⟫) := (continuous_id.inner (secondMomentInv hψ hvar hinj).continuous).measurable rw [gaussianLimit, Measure.map_map hQmeas (secondMomentLM_isPositive hψ hvar).posSqrtCLM.continuous.measurable, ← stdGaussian_map_normSq (E := E)] refine Measure.map_congr (ae_of_all _ fun w => ?_) change ⟪(secondMomentLM_isPositive hψ hvar).posSqrtCLM w, secondMomentInv hψ hvar hinj ((secondMomentLM_isPositive hψ hvar).posSqrtCLM w)⟫ = ‖w‖ ^ 2 rw [(secondMomentLM_isPositive hψ hvar).posSqrtCLM_apply] exact waldForm_posSqrt hψ hvar hinj w

theorem Tendsto_dist.wald_coverage_chiSq {Ω : Type*} [MeasurableSpace Ω] {ν : Measure Ω} [IsProbabilityMeasure ν] {Wn : ℕ → Ω → ℝ} (hWn : ∀ n, AEMeasurable (Wn n) ν) {d : ℕ} (hd : 1 ≤ d) (hW : Tendsto_dist Wn (chiSqDist d) ν hWn) (c : ℝ) (coverProb : ℕ → ℝ) (h_bridge : Tendsto (fun n => coverProb n - (ν {ω | Wn n ω ≤ c}).toReal) atTop (𝓝 0)) : Tendsto coverProb atTop (𝓝 ((chiSqDist d (Iic c)).toReal)) := by haveI := noAtoms_chiSqDist hd exact Tendsto_dist.wald_coverage_Iic_of_noAtoms hWn hW c coverProb h_bridge

theorem deltaMethod_scalar (Tn : ℕ → Ω → ℝ) (t₀ : ℝ) (g : ℝ → ℝ) (g' σsq : ℝ) (hTn : ∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) * (Tn n ω - t₀)) μ) (hgTn : ∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) * (g (Tn n ω) - g t₀)) μ) (_hg : HasDerivAt g g' t₀) (_hCLT : Tendsto_dist (fun (n : ℕ) ω => sqrt (n : ℝ) * (Tn n ω - t₀)) (gaussianMeasure 0 σsq) μ hTn) : Tendsto_dist (fun (n : ℕ) ω => sqrt (n : ℝ) * (g (Tn n ω) - g t₀)) (gaussianMeasure 0 (g' ^ 2 * σsq)) μ hgTn := by let Sn : ℕ → Ω → ℝ := fun n ω => sqrt (n : ℝ) * (Tn n ω - t₀) let Zn : ℕ → Ω → ℝ := fun n ω => g' * Sn n ω let Yn : ℕ → Ω → ℝ := fun n ω => sqrt (n : ℝ) * (g (Tn n ω) - g t₀) have hSn_meas : ∀ n, AEMeasurable (Sn n) μ := by simpa [Sn] using hTn have hZn_meas : ∀ n, AEMeasurable (Zn n) μ := by intro n exact (hSn_meas n).const_mul g' have hYn_meas : ∀ n, AEMeasurable (Yn n) μ := by simpa [Yn] using hgTn have hSnBig : IsBigOp Sn (fun _ => (1 : ℝ)) μ := by simpa [Sn] using Tendsto_dist.tightness hTn _hCLT have hZdist : Tendsto_dist Zn (gaussianMeasure 0 (g' ^ 2 * σsq)) μ hZn_meas := by simpa [Sn, Zn] using Tendsto_dist.const_mul_tendsto_gaussian (a := fun _ : ℕ => g') (a₀ := g') (v := σsq) hSn_meas (by simpa [Sn] using _hCLT) tendsto_const_nhds have hInvSqrt : Tendsto (fun n : ℕ => (sqrt (n : ℝ))⁻¹) atTop (𝓝 0) := by have hsqrt_atTop : Tendsto (fun n : ℕ => sqrt (n : ℝ)) atTop atTop := by exact Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop exact tendsto_inv_atTop_zero.comp hsqrt_atTop have hDeltaScaled : IsLittleOp (fun n ω => (sqrt (n : ℝ))⁻¹ * Sn n ω) (fun _ => (1 : ℝ)) μ := IsBigOp.const_mul_tendsto_zero hSnBig hInvSqrt have hEqD : ∀ᶠ (n : ℕ) in atTop, (fun ω => (sqrt (n : ℝ))⁻¹ * Sn n ω) = (fun ω => Tn n ω - t₀) := by filter_upwards [eventually_ge_atTop (1 : ℕ)] with n hn funext ω have hnpos_nat : 0 < n := lt_of_lt_of_le zero_lt_one hn have hnpos : 0 < (n : ℝ) := by exact_mod_cast hnpos_nat have hsqrt_ne : sqrt (n : ℝ) ≠ 0 := (Real.sqrt_pos.2 hnpos).ne' calc (sqrt (n : ℝ))⁻¹ * Sn n ω = (sqrt (n : ℝ))⁻¹ * (sqrt (n : ℝ) * (Tn n ω - t₀)) := by rfl _ = ((sqrt (n : ℝ))⁻¹ * sqrt (n : ℝ)) * (Tn n ω - t₀) := by ring _ = Tn n ω - t₀ := by rw [inv_mul_cancel₀ hsqrt_ne, one_mul] have hDeltaProb : ∀ ρ : ℝ, 0 < ρ → Tendsto (fun n => μ {ω | ρ < |Tn n ω - t₀|}) atTop (𝓝 0) := by intro ρ hρ have h := hDeltaScaled ρ hρ refine h.congr' ?_ filter_upwards [hEqD] with n hn congr 1 ext ω change ρ * (fun _ => (1 : ℝ)) n < |(fun ω => (sqrt (n : ℝ))⁻¹ * Sn n ω) ω| ↔ ρ < |Tn n ω - t₀| have heq : (fun ω => (sqrt (n : ℝ))⁻¹ * Sn n ω) ω = Tn n ω - t₀ := congr_fun hn ω simp [heq] have hRn : IsLittleOp (fun n ω => Yn n ω - Zn n ω) (fun _ => (1 : ℝ)) μ := by intro ε 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 / 8 have hαpos : 0 < α := by dsimp [α] linarith rcases hSnBig α hαpos with ⟨M0, hM0⟩ let M : ℝ := max M0 1 have hMpos : 0 < M := by dsimp [M] exact lt_of_lt_of_le zero_lt_one (le_max_right M0 1) have hM0le : M0 ≤ M := by dsimp [M] exact le_max_left M0 1 let A : ℕ → Set Ω := fun n => {ω | M < |Sn n ω|} let C : ℕ → Set Ω := fun n => {ω | ε < |Yn n ω - Zn n ω|} have hlimA : limsup (fun n => μ (A n)) atTop ≤ ofReal α := by refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0 intro n apply measure_mono intro ω hω dsimp [A, Sn] at hω ⊢ nlinarith have halpha_two : ofReal α < ofReal (2 * α) := by rw [ENNReal.ofReal_lt_ofReal_iff] · linarith · linarith have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimA halpha_two) let η : ℝ := ε / M have hηpos : 0 < η := by dsimp [η] exact div_pos hε hMpos have hderiv_event : ∀ᶠ x in 𝓝 t₀, |g x - g t₀ - g' * (x - t₀)| ≤ η * |x - t₀| := by have hderiv_event0 := _hg.isLittleO.def hηpos filter_upwards [hderiv_event0] with x hx simpa [Real.norm_eq_abs, smul_eq_mul, mul_comm, mul_left_comm, mul_assoc] using hx rcases Metric.eventually_nhds_iff.mp hderiv_event with ⟨ρ, hρpos, hρprop⟩ let B : ℕ → Set Ω := fun n => {ω | ρ ≤ |Tn n ω - t₀|} have hDeltaHalf := hDeltaProb (ρ / 2) (by linarith) have hBsmall0 := (ENNReal.tendsto_nhds_zero.mp hDeltaHalf) (ofReal α) (by exact ENNReal.ofReal_pos.mpr hαpos) have hBevent : ∀ᶠ n in atTop, μ (B n) < ofReal (2 * α) := by filter_upwards [hBsmall0] with n hn exact lt_of_le_of_lt (le_trans (measure_mono (by intro ω hω dsimp [B] at hω have : ρ / 2 < |Tn n ω - t₀| := by linarith exact this)) hn) halpha_two have hpoint : ∀ n, μ (C n) ≤ μ (A n) + μ (B n) := by intro n have hsubset : C n ⊆ A n ∪ B n := by intro ω hω by_contra hnot have hnotA : ¬ M < |Sn n ω| := by intro hx exact hnot (inl hx) have hnotB : ¬ ρ ≤ |Tn n ω - t₀| := by intro hx exact hnot (inr hx) have hSnle : |Sn n ω| ≤ M := le_of_not_gt hnotA have hnear : |Tn n ω - t₀| < ρ := lt_of_not_ge hnotB have hder := hρprop (by simpa [Real.dist_eq] using hnear) have hRabs : |Yn n ω - Zn n ω| ≤ η * |Sn n ω| := by calc |Yn n ω - Zn n ω| = |sqrt (n : ℝ) * (g (Tn n ω) - g t₀ - g' * (Tn n ω - t₀))| := by dsimp [Yn, Zn, Sn] congr 1 ring _ = |sqrt (n : ℝ)| * |g (Tn n ω) - g t₀ - g' * (Tn n ω - t₀)| := by rw [abs_mul] _ = sqrt (n : ℝ) * |g (Tn n ω) - g t₀ - g' * (Tn n ω - t₀)| := by rw [abs_of_nonneg (Real.sqrt_nonneg _)] _ ≤ sqrt (n : ℝ) * (η * |Tn n ω - t₀|) := by exact mul_le_mul_of_nonneg_left hder (Real.sqrt_nonneg _) _ = η * |Sn n ω| := by dsimp [Sn] rw [abs_mul, abs_of_nonneg (Real.sqrt_nonneg _)] ring have hRle : |Yn n ω - Zn n ω| ≤ ε := by calc |Yn n ω - Zn n ω| ≤ η * |Sn n ω| := hRabs _ ≤ η * M := by exact mul_le_mul_of_nonneg_left hSnle (le_of_lt hηpos) _ = ε := by dsimp [η] field_simp [hMpos.ne'] exact not_lt_of_ge hRle hω calc μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) have hfour_alpha_lt_delta : ofReal (4 * α) < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [α] linarith · dsimp [α] linarith [le_of_lt hδpos] · exact hδtop filter_upwards [hAevent, hBevent] with n hAn hBn exact le_of_lt <| calc μ {ω | ε * (fun _ => (1 : ℝ)) n < |Yn n ω - Zn n ω|} = μ (C n) := by simp [C] _ ≤ μ (A n) + μ (B n) := hpoint n _ < ofReal (2 * α) + ofReal (2 * α) := ENNReal.add_lt_add hAn hBn _ = ofReal (4 * α) := by rw [← ENNReal.ofReal_add] · congr 1; ring · linarith · linarith _ < δ := hfour_alpha_lt_delta simpa [Yn] using Tendsto_dist.add_isLittleOp_one hZn_meas hYn_meas hZdist hRn

theorem deltaMethod (Tn : ℕ → Ω → E) (t₀ : E) (g : E → F) (Dg : E →L[ℝ] F) (Q : ProbabilityMeasure E) (hTn : ∀ n, AEMeasurable (fun ω => (sqrt ((n : ℕ) : ℝ)) • (Tn n ω - t₀)) μ) (hgTn : ∀ n, AEMeasurable (fun ω => (sqrt ((n : ℕ) : ℝ)) • (g (Tn n ω) - g t₀)) μ) (_hg : HasFDerivAt g Dg t₀) (_hCLT : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (fun ω => (sqrt ((n : ℕ) : ℝ)) • (Tn n ω - t₀)), Measure.isProbabilityMeasure_map (hTn n)⟩) atTop (𝓝 Q)) : Tendsto (β := ProbabilityMeasure F) (fun n => ⟨μ.map (fun ω => (sqrt ((n : ℕ) : ℝ)) • (g (Tn n ω) - g t₀)), Measure.isProbabilityMeasure_map (hgTn n)⟩) atTop (𝓝 ⟨Q.toMeasure.map Dg, Measure.isProbabilityMeasure_map Dg.continuous.measurable.aemeasurable⟩) := by let Sn : ℕ → Ω → E := fun n ω => (sqrt ((n : ℕ) : ℝ)) • (Tn n ω - t₀) let Zn : ℕ → Ω → F := fun n ω => Dg (Sn n ω) let Yn : ℕ → Ω → F := fun n ω => (sqrt ((n : ℕ) : ℝ)) • (g (Tn n ω) - g t₀) haveI : IsProbabilityMeasure (Q.toMeasure) := Q.2 haveI : IsProbabilityMeasure (Q.toMeasure.map (fun x : E => ‖x‖)) := Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable haveI : IsProbabilityMeasure (Q.toMeasure.map Dg) := Measure.isProbabilityMeasure_map Dg.continuous.measurable.aemeasurable have hSn_meas : ∀ n, AEMeasurable (Sn n) μ := by simpa [Sn] using hTn have hZn_meas : ∀ n, AEMeasurable (Zn n) μ := by intro n exact Dg.continuous.measurable.comp_aemeasurable (hSn_meas n) have hYn_meas : ∀ n, AEMeasurable (Yn n) μ := by simpa [Yn] using hgTn have hSnDist : Tendsto_dist_vec Sn Q.toMeasure μ hSn_meas := by change Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (Sn n), Measure.isProbabilityMeasure_map (hSn_meas n)⟩) atTop (𝓝 Q) simpa [Sn] using _hCLT have hNormSn_meas : ∀ n, AEMeasurable (fun ω => ‖Sn n ω‖) μ := by intro n exact continuous_norm.measurable.comp_aemeasurable (hSn_meas n) have hNormDistVec : Tendsto_dist_vec (fun n ω => ‖Sn n ω‖) (Q.toMeasure.map (fun x : E => ‖x‖)) μ hNormSn_meas := by exact Tendsto_dist_vec.map_continuous (Q := Q.toMeasure) (g := fun x : E => ‖x‖) continuous_norm hSn_meas hSnDist have hNormDist : Tendsto_dist (fun n ω => ‖Sn n ω‖) (Q.toMeasure.map (fun x : E => ‖x‖)) μ hNormSn_meas := by change Tendsto (β := ProbabilityMeasure ℝ) (fun n => ⟨μ.map ((fun n ω => ‖Sn n ω‖) n), Measure.isProbabilityMeasure_map (hNormSn_meas n)⟩) atTop (𝓝 ⟨Q.toMeasure.map (fun x : E => ‖x‖), inferInstance⟩) at hNormDistVec exact hNormDistVec have hSnBig : IsBigOp (fun n ω => ‖Sn n ω‖) (fun _ => (1 : ℝ)) μ := Tendsto_dist.tightness hNormSn_meas hNormDist have hInvSqrt : Tendsto (fun n : ℕ => (sqrt (n : ℝ))⁻¹) atTop (𝓝 0) := by have hsqrt_atTop : Tendsto (fun n : ℕ => sqrt (n : ℝ)) atTop atTop := by exact Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop exact tendsto_inv_atTop_zero.comp hsqrt_atTop have hDeltaScaled : IsLittleOp (fun n ω => (sqrt (n : ℝ))⁻¹ * ‖Sn n ω‖) (fun _ => (1 : ℝ)) μ := IsBigOp.const_mul_tendsto_zero hSnBig hInvSqrt have hEqD : ∀ᶠ (n : ℕ) in atTop, (fun ω => (sqrt (n : ℝ))⁻¹ * ‖Sn n ω‖) = (fun ω => ‖Tn n ω - t₀‖) := by filter_upwards [eventually_ge_atTop (1 : ℕ)] with n hn funext ω have hnpos_nat : 0 < n := lt_of_lt_of_le zero_lt_one hn have hnpos : 0 < (n : ℝ) := by exact_mod_cast hnpos_nat have hsqrt_ne : sqrt (n : ℝ) ≠ 0 := (Real.sqrt_pos.2 hnpos).ne' calc (sqrt (n : ℝ))⁻¹ * ‖Sn n ω‖ = (sqrt (n : ℝ))⁻¹ * ‖(sqrt (n : ℝ)) • (Tn n ω - t₀)‖ := by rfl _ = (sqrt (n : ℝ))⁻¹ * (sqrt (n : ℝ) * ‖Tn n ω - t₀‖) := by rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _)] _ = ‖Tn n ω - t₀‖ := by rw [← mul_assoc, inv_mul_cancel₀ hsqrt_ne, one_mul] have hDeltaProb : ∀ ρ : ℝ, 0 < ρ → Tendsto (fun n => μ {ω | ρ < ‖Tn n ω - t₀‖}) atTop (𝓝 0) := by intro ρ hρ have h := hDeltaScaled ρ hρ refine h.congr' ?_ filter_upwards [hEqD] with n hn congr 1 ext ω change ρ * (fun _ => (1 : ℝ)) n < |(fun ω => (sqrt (n : ℝ))⁻¹ * ‖Sn n ω‖) ω| ↔ ρ < ‖Tn n ω - t₀‖ have heq : (fun ω => (sqrt (n : ℝ))⁻¹ * ‖Sn n ω‖) ω = ‖Tn n ω - t₀‖ := congr_fun hn ω simp [heq] have hRn : IsLittleOp (fun n ω => ‖Yn n ω - Zn n ω‖) (fun _ => (1 : ℝ)) μ := by intro ε 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 / 8 have hαpos : 0 < α := by dsimp [α] linarith rcases hSnBig α hαpos with ⟨M0, hM0⟩ let M : ℝ := max M0 1 have hMpos : 0 < M := by dsimp [M] exact lt_of_lt_of_le zero_lt_one (le_max_right M0 1) have hM0le : M0 ≤ M := by dsimp [M] exact le_max_left M0 1 let A : ℕ → Set Ω := fun n => {ω | M < ‖Sn n ω‖} let C : ℕ → Set Ω := fun n => {ω | ε < ‖Yn n ω - Zn n ω‖} have hlimA : limsup (fun n => μ (A n)) atTop ≤ ofReal α := by refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0 intro n apply measure_mono intro ω hω dsimp [A] at hω ⊢ have hM0_lt : M0 < ‖Sn n ω‖ := lt_of_le_of_lt hM0le hω simpa [abs_of_nonneg (norm_nonneg (Sn n ω))] using hM0_lt have halpha_two : ofReal α < ofReal (2 * α) := by rw [ENNReal.ofReal_lt_ofReal_iff] · linarith · linarith have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimA halpha_two) let η : ℝ := ε / M have hηpos : 0 < η := by dsimp [η] exact div_pos hε hMpos have hderiv_event : ∀ᶠ x in 𝓝 t₀, ‖g x - g t₀ - Dg (x - t₀)‖ ≤ η * ‖x - t₀‖ := by have hderiv_event0 := _hg.isLittleO.def hηpos filter_upwards [hderiv_event0] with x hx simpa using hx rcases Metric.eventually_nhds_iff.mp hderiv_event with ⟨ρ, hρpos, hρprop⟩ let B : ℕ → Set Ω := fun n => {ω | ρ ≤ ‖Tn n ω - t₀‖} have hDeltaHalf := hDeltaProb (ρ / 2) (by linarith) have hBsmall0 := (ENNReal.tendsto_nhds_zero.mp hDeltaHalf) (ofReal α) (by exact ENNReal.ofReal_pos.mpr hαpos) have hBevent : ∀ᶠ n in atTop, μ (B n) < ofReal (2 * α) := by filter_upwards [hBsmall0] with n hn exact lt_of_le_of_lt (le_trans (measure_mono (by intro ω hω dsimp [B] at hω have : ρ / 2 < ‖Tn n ω - t₀‖ := by linarith exact this)) hn) halpha_two have hpoint : ∀ n, μ (C n) ≤ μ (A n) + μ (B n) := by intro n have hsubset : C n ⊆ A n ∪ B n := by intro ω hω by_contra hnot have hnotA : ¬ M < ‖Sn n ω‖ := by intro hx exact hnot (inl hx) have hnotB : ¬ ρ ≤ ‖Tn n ω - t₀‖ := by intro hx exact hnot (inr hx) have hSnle : ‖Sn n ω‖ ≤ M := le_of_not_gt hnotA have hnear : ‖Tn n ω - t₀‖ < ρ := lt_of_not_ge hnotB have hder := hρprop (by simpa [dist_eq_norm] using hnear) have hRnorm : ‖Yn n ω - Zn n ω‖ ≤ η * ‖Sn n ω‖ := by calc ‖Yn n ω - Zn n ω‖ = ‖(sqrt (n : ℝ)) • (g (Tn n ω) - g t₀ - Dg (Tn n ω - t₀))‖ := by dsimp [Yn, Zn, Sn] rw [Dg.map_smul] congr 1 simp [smul_sub] _ = sqrt (n : ℝ) * ‖g (Tn n ω) - g t₀ - Dg (Tn n ω - t₀)‖ := by rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _)] _ ≤ sqrt (n : ℝ) * (η * ‖Tn n ω - t₀‖) := by exact mul_le_mul_of_nonneg_left hder (Real.sqrt_nonneg _) _ = η * ‖Sn n ω‖ := by dsimp [Sn] rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _)] ring have hRle : ‖Yn n ω - Zn n ω‖ ≤ ε := by calc ‖Yn n ω - Zn n ω‖ ≤ η * ‖Sn n ω‖ := hRnorm _ ≤ η * M := by exact mul_le_mul_of_nonneg_left hSnle (le_of_lt hηpos) _ = ε := by dsimp [η] field_simp [hMpos.ne'] exact not_lt_of_ge hRle hω calc μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) have hfour_alpha_lt_delta : ofReal (4 * α) < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [α] linarith · dsimp [α] linarith [le_of_lt hδpos] · exact hδtop filter_upwards [hAevent, hBevent] with n hAn hBn exact le_of_lt <| calc μ {ω | ε * (fun _ => (1 : ℝ)) n < |‖Yn n ω - Zn n ω‖|} = μ (C n) := by simp [C] _ ≤ μ (A n) + μ (B n) := hpoint n _ < ofReal (2 * α) + ofReal (2 * α) := ENNReal.add_lt_add hAn hBn _ = ofReal (4 * α) := by rw [← ENNReal.ofReal_add] · congr 1; ring · linarith · linarith _ < δ := hfour_alpha_lt_delta have hZdist : Tendsto_dist_vec Zn (Q.toMeasure.map Dg) μ hZn_meas := by exact Tendsto_dist_vec.map_continuous (Q := Q.toMeasure) (g := fun x : E => Dg x) Dg.continuous hSn_meas hSnDist change Tendsto_dist_vec Yn (Q.toMeasure.map Dg) μ hYn_meas exact Tendsto_dist_vec.add_isLittleOp_one (Q := Q.toMeasure.map Dg) (Xn := Zn) (Yn := Yn) hZn_meas hYn_meas hZdist hRn

theorem deltaMethod_max_tie (an bn : ℕ → Ω → ℝ) (a : ℝ) (Q : Measure (ℝ × ℝ)) [IsProbabilityMeasure Q] (hSn_meas : ∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) • ((an n ω, bn n ω) - (a, a))) μ) (hCLT : Tendsto_dist_vec (fun (n : ℕ) ω => sqrt (n : ℝ) • ((an n ω, bn n ω) - (a, a))) Q μ hSn_meas) : Tendsto_dist (fun (n : ℕ) ω => sqrt (n : ℝ) * (max (an n ω) (bn n ω) - a)) (Q.map (fun z : ℝ × ℝ => max z.1 z.2)) μ (maxStat_aemeasurable an bn a hSn_meas) := by -- continuous mapping theorem on the joint CLT: the rescaled image is `max ∘ Sₙ` -- exactly (`sqrt_mul_max_sub`), with no linearization remainder. have hgmeas : ∀ (n : ℕ), AEMeasurable (fun ω => (fun z : ℝ × ℝ => max z.1 z.2) (sqrt (n : ℝ) • ((an n ω, bn n ω) - (a, a)))) μ := fun (n : ℕ) => (continuous_fst.max continuous_snd).measurable.comp_aemeasurable (hSn_meas n) have hmap : Tendsto_dist_vec (fun (n : ℕ) ω => (fun z : ℝ × ℝ => max z.1 z.2) (sqrt (n : ℝ) • ((an n ω, bn n ω) - (a, a)))) (Q.map (fun z : ℝ × ℝ => max z.1 z.2)) μ hgmeas := by exact Tendsto_dist_vec.map_continuous (continuous_fst.max continuous_snd) hSn_meas hCLT -- transport `max ∘ Sₙ ⇒ Q.map max` to the (pointwise-equal) rescaled image exact hmap.congr_ae hgmeas (maxStat_aemeasurable an bn a hSn_meas) (Eventually.of_forall fun n => Eventually.of_forall fun ω => (sqrt_mul_max_sub an bn a n ω).symm)

theorem deltaMethod_min_tie (an bn : ℕ → Ω → ℝ) (a : ℝ) (Q : Measure (ℝ × ℝ)) [IsProbabilityMeasure Q] (hSn_meas : ∀ (n : ℕ), AEMeasurable (fun ω => sqrt (n : ℝ) • ((an n ω, bn n ω) - (a, a))) μ) (hCLT : Tendsto_dist_vec (fun (n : ℕ) ω => sqrt (n : ℝ) • ((an n ω, bn n ω) - (a, a))) Q μ hSn_meas) : Tendsto_dist (fun (n : ℕ) ω => sqrt (n : ℝ) * (min (an n ω) (bn n ω) - a)) (Q.map (fun z : ℝ × ℝ => min z.1 z.2)) μ (minStat_aemeasurable an bn a hSn_meas) := by have hgmeas : ∀ (n : ℕ), AEMeasurable (fun ω => (fun z : ℝ × ℝ => min z.1 z.2) (sqrt (n : ℝ) • ((an n ω, bn n ω) - (a, a)))) μ := fun (n : ℕ) => (continuous_fst.min continuous_snd).measurable.comp_aemeasurable (hSn_meas n) have hmap : Tendsto_dist_vec (fun (n : ℕ) ω => (fun z : ℝ × ℝ => min z.1 z.2) (sqrt (n : ℝ) • ((an n ω, bn n ω) - (a, a)))) (Q.map (fun z : ℝ × ℝ => min z.1 z.2)) μ hgmeas := by exact Tendsto_dist_vec.map_continuous (continuous_fst.min continuous_snd) hSn_meas hCLT -- transport `min ∘ Sₙ ⇒ Q.map min` to the (pointwise-equal) rescaled image exact hmap.congr_ae hgmeas (minStat_aemeasurable an bn a hSn_meas) (Eventually.of_forall fun n => Eventually.of_forall fun ω => (sqrt_mul_min_sub an bn a n ω).symm)

theorem HasFDerivAt.hasHadamardDirDerivAt {φ : E → F} {L : E →L[ℝ] F} {θ : E} (hL : HasFDerivAt φ L θ) : HasHadamardDirDerivAt φ (fun x => L x) θ := by intro h hn tn hhn htn htn_pos have hxn : Tendsto (fun n => θ + tn n • hn n) atTop (𝓝 θ) := by have h0 : Tendsto (fun n => tn n • hn n) atTop (𝓝 0) := by simpa using htn.smul hhn simpa using (tendsto_const_nhds (x := θ)).add h0 have hLhn : Tendsto (fun n => L (hn n)) atTop (𝓝 (L h)) := (L.continuous.tendsto h).comp hhn -- remainder `rₙ := φ(θ + tₙ•hₙ) − φθ − tₙ • L hₙ` set rn : ℕ → F := fun n => φ (θ + tn n • hn n) - φ θ - tn n • L (hn n) with hrn_def have hrec : ∀ n, (tn n)⁻¹ • (φ (θ + tn n • hn n) - φ θ) = L (hn n) + (tn n)⁻¹ • rn n := by intro n have htn_ne : tn n ≠ 0 := (htn_pos n).ne' have hsplit : (tn n)⁻¹ • rn n = (tn n)⁻¹ • (φ (θ + tn n • hn n) - φ θ) - L (hn n) := by rw [hrn_def] rw [smul_sub, smul_smul, inv_mul_cancel₀ htn_ne, one_smul] rw [hsplit]; abel have hrem : Tendsto (fun n => (tn n)⁻¹ • rn n) atTop (𝓝 0) := by -- Step 1: the Fréchet remainder composed with the curve `xₙ = θ + tₙ•hₙ` is -- little-o of `tₙ•hₙ` (`= xₙ − θ`). have hf : (fun n => φ (θ + tn n • hn n) - φ θ - L ((θ + tn n • hn n) - θ)) =ᶠ[atTop] rn := by apply Filter.Eventually.of_forall intro n simp only [hrn_def, add_sub_cancel_left, map_smul] have hg : (fun n => (θ + tn n • hn n) - θ) =ᶠ[atTop] (fun n => tn n • hn n) := by apply Filter.Eventually.of_forall intro n simp only [add_sub_cancel_left] have hlitt := (hL.isLittleO.comp_tendsto hxn).congr' hf hg -- Step 2: divide by the rate `tₙ`. Since `‖hₙ‖` is bounded, `(tₙ)⁻¹•rₙ → 0`. rw [NormedAddGroup.tendsto_nhds_zero] intro ε hε obtain ⟨M, hMpos, hMev⟩ : ∃ M : ℝ, 0 < M ∧ ∀ᶠ n in atTop, ‖hn n‖ ≤ M := by refine ⟨‖h‖ + 1, by positivity, ?_⟩ have hnorm : Tendsto (fun n => ‖hn n‖) atTop (𝓝 ‖h‖) := (continuous_norm.tendsto h).comp hhn filter_upwards [hnorm.eventually_lt_const (lt_add_one ‖h‖)] with n hn_ev exact hn_ev.le have hc : (0 : ℝ) < ε / (2 * M) := div_pos hε (by linarith) have hbound := hlitt.def hc filter_upwards [hbound, hMev] with n hb hMn have htn_pos' := htn_pos n have htn_ne : tn n ≠ 0 := htn_pos'.ne' have hsmul_norm : ‖tn n • hn n‖ = tn n * ‖hn n‖ := by rw [norm_smul, Real.norm_eq_abs, abs_of_pos htn_pos'] rw [hsmul_norm] at hb rw [norm_smul, norm_inv, Real.norm_eq_abs, abs_of_pos htn_pos'] calc (tn n)⁻¹ * ‖rn n‖ ≤ (tn n)⁻¹ * (ε / (2 * M) * (tn n * ‖hn n‖)) := mul_le_mul_of_nonneg_left hb (inv_nonneg.mpr htn_pos'.le) _ = ε / (2 * M) * ‖hn n‖ := by have he : (tn n)⁻¹ * (ε / (2 * M) * (tn n * ‖hn n‖)) = ε / (2 * M) * ((tn n)⁻¹ * tn n) * ‖hn n‖ := by ring rw [he, inv_mul_cancel₀ htn_ne, mul_one] _ ≤ ε / (2 * M) * M := mul_le_mul_of_nonneg_left hMn (div_nonneg hε.le (by linarith)) _ = ε / 2 := by field_simp _ < ε := by linarith have := hLhn.add hrem simpa [hrec] using this

theorem deltaMethod_ratio (Tn : ℕ → Ω → EuclideanSpace ℝ (Fin 2)) (t₀ : EuclideanSpace ℝ (Fin 2)) (hb : t₀ 1 ≠ 0) (Q : ProbabilityMeasure (EuclideanSpace ℝ (Fin 2))) (hTn : ∀ n, AEMeasurable (fun ω => (sqrt ((n : ℕ) : ℝ)) • (Tn n ω - t₀)) μ) (hgTn : ∀ n, AEMeasurable (fun ω => (sqrt ((n : ℕ) : ℝ)) • ((Tn n ω 0 / Tn n ω 1) - t₀ 0 / t₀ 1)) μ) (_hCLT : Tendsto (β := ProbabilityMeasure (EuclideanSpace ℝ (Fin 2))) (fun n => ⟨μ.map (fun ω => (sqrt ((n : ℕ) : ℝ)) • (Tn n ω - t₀)), Measure.isProbabilityMeasure_map (hTn n)⟩) atTop (𝓝 Q)) : Tendsto (β := ProbabilityMeasure ℝ) (fun n => ⟨μ.map (fun ω => (sqrt ((n : ℕ) : ℝ)) • ((Tn n ω 0 / Tn n ω 1) - t₀ 0 / t₀ 1)), Measure.isProbabilityMeasure_map (hgTn n)⟩) atTop (𝓝 ⟨Q.toMeasure.map (ratioDeriv t₀), Measure.isProbabilityMeasure_map (ratioDeriv t₀).continuous.measurable.aemeasurable⟩) := deltaMethod Tn t₀ (fun v => v 0 / v 1) (ratioDeriv t₀) Q hTn hgTn (hasFDerivAt_ratio hb) _hCLT

theorem Tendsto_dist.div_tendsto_inProb_gaussian {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xn : ℕ → Ω → ℝ} {σ_hat : ℕ → Ω → ℝ} {σ₀ : ℝ} (hσ₀_pos : 0 < σ₀) (hXn : ∀ n, AEMeasurable (Xn n) μ) (hX : Tendsto_dist Xn (gaussianMeasure 0 (σ₀ ^ 2)) μ hXn) (hσ : Tendsto_inProb σ_hat (fun _ => σ₀) μ) (hdiv : ∀ n, AEMeasurable (fun ω => Xn n ω / σ_hat n ω) μ) : Tendsto_dist (fun n ω => Xn n ω / σ_hat n ω) (gaussianMeasure 0 1) μ hdiv := by have hσ₀_ne : σ₀ ≠ 0 := ne_of_gt hσ₀_pos have hscaled_meas : ∀ n, AEMeasurable (fun ω => (1 / σ₀) * Xn n ω) μ := by intro n exact aemeasurable_const.mul (hXn n) have hscaled : Tendsto_dist (fun n ω => (1 / σ₀) * Xn n ω) (gaussianMeasure 0 1) μ hscaled_meas := by have h := Tendsto_dist.const_mul_tendsto_gaussian (Xn := Xn) (a := fun _ : ℕ => 1 / σ₀) (a₀ := 1 / σ₀) (v := σ₀ ^ 2) hXn hX tendsto_const_nhds have hvar : ((σ₀ ^ 2)⁻¹ * σ₀ ^ 2) = 1 := by have hσsq_ne : σ₀ ^ 2 ≠ 0 := pow_ne_zero 2 hσ₀_ne field_simp [hσsq_ne] simpa [hvar] using h have hXbig : IsBigOp Xn (fun _ => (1 : ℝ)) μ := Tendsto_dist.tightness hXn hX have hinv_little : IsLittleOp (fun n ω => 1 / σ_hat n ω - 1 / σ₀) (fun _ => (1 : ℝ)) μ := by exact Tendsto_inProb.isLittleOp_one (Tendsto_inProb.sub_const (Tendsto_inProb.inv hσ hσ₀_ne)) have hrem_prod : IsLittleOp (fun n ω => Xn n ω * (1 / σ_hat n ω - 1 / σ₀)) (fun _ => (1 : ℝ)) μ := IsBigOp.mul_isLittleOp_one_isLittleOp hXbig hinv_little have hrem : IsLittleOp (fun n ω => Xn n ω / σ_hat n ω - (1 / σ₀) * Xn n ω) (fun _ => (1 : ℝ)) μ := by convert hrem_prod using 1 funext n ω ring exact Tendsto_dist.add_isLittleOp_one hscaled_meas hdiv hscaled hrem

theorem Tendsto_dist.wald_coverage {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Sn : ℕ → Ω → ℝ} (hSn : ∀ n, AEMeasurable (Sn n) μ) (hS : Tendsto_dist Sn (gaussianMeasure 0 1) μ hSn) {z : ℝ} (hz : 0 < z) (coverProb : ℕ → ℝ) (h_bridge : Tendsto (fun n => coverProb n - (μ {ω | Sn n ω ∈ Icc (-z) z}).toReal) atTop (𝓝 0)) : Tendsto coverProb atTop (𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by let studProb : ℕ → ℝ := fun n => (μ {ω | Sn n ω ∈ Icc (-z) z}).toReal change Tendsto (fun n => coverProb n - studProb n) atTop (𝓝 0) at h_bridge have hpm : Tendsto (fun n => ((μ.map (Sn n)) (Icc (-z) z)).toReal) atTop (𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by exact Tendsto_dist.tendsto_measure_of_null_frontier hSn hS (gaussianMeasure_zero_one_frontier_Icc hz) have hstudent_event : Tendsto studProb atTop (𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by refine hpm.congr' ?_ filter_upwards with n rw [Measure.map_apply_of_aemeasurable (hSn n) measurableSet_Icc] rfl have hsum := hstudent_event.add h_bridge have hsum' : Tendsto (fun n => studProb n + (coverProb n - studProb n)) atTop (𝓝 ((gaussianMeasure 0 1) (Icc (-z) z)).toReal) := by simpa using hsum refine hsum'.congr' ?_ filter_upwards with n ring

theorem sampleCov_entry_tendsto_inProb (S : IIDSample Ω X μ P) [IsProbabilityMeasure P] {ψ : X → E} (hψ_meas : Measurable ψ) (hψ_sq_int : Integrable (fun ω => ‖ψ (S.Z 0 ω)‖ ^ 2) μ) (φ φ' : E →L[ℝ] ℝ) : Tendsto_inProb (S.sampleMean (fun x => φ (ψ x) * φ' (ψ x))) (fun _ => ∫ x, φ (ψ x) * φ' (ψ x) ∂P) μ := by -- coordinate measurability have hφ : Measurable (fun x => φ (ψ x)) := by fun_prop have hφ' : Measurable (fun x => φ' (ψ x)) := by fun_prop -- entrywise integrability of the product, dominated by (‖φ‖‖φ'‖)·‖ψ‖² have hprod_int : Integrable (fun ω => φ (ψ (S.Z 0 ω)) * φ' (ψ (S.Z 0 ω))) μ := by have hmeas : AEStronglyMeasurable (fun ω => φ (ψ (S.Z 0 ω)) * φ' (ψ (S.Z 0 ω))) μ := ((hφ.comp (S.meas 0)).mul (hφ'.comp (S.meas 0))).aestronglyMeasurable refine Integrable.mono' (hψ_sq_int.const_mul (‖φ‖ * ‖φ'‖)) hmeas ?_ filter_upwards with ω simpa [Real.norm_eq_abs] using abs_apply_mul_le_norm_sq φ φ' ψ (S.Z 0 ω) exact S.sampleMean_mul_tendsto_inProb hφ hφ' hprod_int

theorem sqrt_var_tendsto_inProb {Ω : Type*} [MeasurableSpace Ω] {varhat : ℕ → Ω → ℝ} {σ₀ : ℝ} {μ : Measure Ω} (hσ₀_pos : 0 < σ₀) (h : Tendsto_inProb varhat (fun _ => σ₀ ^ 2) μ) : Tendsto_inProb (fun n ω => sqrt (varhat n ω)) (fun _ => σ₀) μ := by have hsqrt := Tendsto_inProb.sqrt h have heq : sqrt (σ₀ ^ 2) = σ₀ := by rw [Real.sqrt_sq (le_of_lt hσ₀_pos)] rwa [heq] at hsqrt

theorem Tendsto_dist.wald_coverage_Iic {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Wn : ℕ → Ω → ℝ} (hWn : ∀ n, AEMeasurable (Wn n) μ) {χ : Measure ℝ} [IsProbabilityMeasure χ] (hW : Tendsto_dist Wn χ μ hWn) {c : ℝ} (hfront : χ (frontier (Iic c)) = 0) (coverProb : ℕ → ℝ) (h_bridge : Tendsto (fun n => coverProb n - (μ {ω | Wn n ω ≤ c}).toReal) atTop (𝓝 0)) : Tendsto coverProb atTop (𝓝 ((χ (Iic c)).toReal)) := by let ellProb : ℕ → ℝ := fun n => (μ {ω | Wn n ω ≤ c}).toReal change Tendsto (fun n => coverProb n - ellProb n) atTop (𝓝 0) at h_bridge have hpm : Tendsto (fun n => ((μ.map (Wn n)) (Iic c)).toReal) atTop (𝓝 ((χ (Iic c)).toReal)) := Tendsto_dist.tendsto_measure_of_null_frontier hWn hW hfront have hell : Tendsto ellProb atTop (𝓝 ((χ (Iic c)).toReal)) := by refine hpm.congr' ?_ filter_upwards with n rw [Measure.map_apply_of_aemeasurable (hWn n) measurableSet_Iic] rfl have hsum := hell.add h_bridge have hsum' : Tendsto (fun n => ellProb n + (coverProb n - ellProb n)) atTop (𝓝 ((χ (Iic c)).toReal)) := by simpa using hsum refine hsum'.congr' ?_ filter_upwards with n ring

theorem Tendsto_dist.wald_coverage_Iic_of_noAtoms {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Wn : ℕ → Ω → ℝ} (hWn : ∀ n, AEMeasurable (Wn n) μ) {χ : Measure ℝ} [IsProbabilityMeasure χ] [NullSingletonClass χ] (hW : Tendsto_dist Wn χ μ hWn) (c : ℝ) (coverProb : ℕ → ℝ) (h_bridge : Tendsto (fun n => coverProb n - (μ {ω | Wn n ω ≤ c}).toReal) atTop (𝓝 0)) : Tendsto coverProb atTop (𝓝 ((χ (Iic c)).toReal)) := by refine Tendsto_dist.wald_coverage_Iic hWn hW ?_ coverProb h_bridge rw [frontier_Iic] exact measure_singleton c