Stat.Bootstrap.Smooth­Function­Of­Means

@[fun_prop] theorem measurable_smoothMeanEstimator {g : X → E} {h : E → ℝ} [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (hg : Measurable g) (hh : Measurable h) (n : ℕ) : Measurable (smoothMeanEstimator g h n) := by unfold smoothMeanEstimator finMean apply hh.comp exact (Finset.measurable_sum _ (fun i _ ↦ hg.comp (measurable_pi_apply i))).const_smul _

theorem bootstrapMean_chebyshev (g : X → ℝ) (hg : Measurable g) {n : ℕ} (x : Fin n → X) (hn : n ≠ 0) (M : ℝ) (hM : 0 < M) : (bootstrapResample x).real {xstar | M < |scaledBootstrapMeanDifference g n x xstar|} ≤ (finMean (fun i ↦ (g (x i)) ^ 2) - (finMean (fun i ↦ g (x i))) ^ 2) / M ^ 2 := by let D : (Fin n → X) → ℝ := fun xstar ↦ scaledBootstrapMeanDifference g n x xstar have hD : Measurable D := by dsimp [D, scaledBootstrapMeanDifference] unfold finMean fun_prop let _ : IsProbabilityMeasure (bootstrapResample x) := bootstrapResample_isProbabilityMeasure x hn have hDsq : Integrable (fun xstar ↦ (D xstar) ^ 2) (bootstrapResample x) := integrable_bootstrapResample_real x _ (hD.pow_const 2) have hDmem : MemLp D 2 (bootstrapResample x) := (memLp_two_iff_integrable_sq hD.aestronglyMeasurable).2 hDsq have hmean : (∫ xstar, D xstar ∂bootstrapResample x) = 0 := by change (∫ xstar, sqrt n * (finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (x i))) ∂bootstrapResample x) = 0 rw [integral_const_mul, integral_sub (integrable_bootstrapResample_real x _ (by unfold finMean fun_prop)) (integrable_const _), integral_finMean_bootstrapResample_real x g hg hn] simp have hvar : variance D (bootstrapResample x) = finMean (fun i ↦ (g (x i)) ^ 2) - (finMean (fun i ↦ g (x i))) ^ 2 := by rw [variance_eq_integral hD.aemeasurable, hmean] simp only [sub_zero] change (∫ xstar, (sqrt n * (finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (x i)))) ^ 2 ∂bootstrapResample x) = _ rw [integral_centered_finMean_sq_bootstrapResample_real x g hg hn, centered_finMean_sq_eq (fun i ↦ g (x i)) hn] have hcheb := Concentration.probability_abs_sub_mean_gt_le (bootstrapResample x) D 0 (finMean (fun i ↦ (g (x i)) ^ 2) - (finMean (fun i ↦ g (x i))) ^ 2) M hDmem hM hmean hvar.le rw [measureReal_def] simpa only [D, sub_zero] using hcheb

theorem scaledBootstrapMeanDifferenceVec_conditionallyBounded {d : ℕ} (S : IIDSample Omega X mu P) (g : X → EuclideanSpace ℝ (Fin d)) (hg : Measurable g) (hg2 : Integrable (fun x ↦ ‖g x‖ ^ 2) P) : ConditionallyBoundedInProbability S (scaledBootstrapMeanDifference g) := by have hcoord_sq : ∀ j : Fin d, Integrable (fun x ↦ (g x j) ^ 2) P := by intro j apply hg2.mono (by fun_prop) filter_upwards with x have hnorm : |g x j| ≤ ‖g x‖ := by simpa [Real.norm_eq_abs] using PiLp.norm_apply_le (g x) j have hsq := (sq_le_sq₀ (abs_nonneg (g x j)) (norm_nonneg (g x))).2 hnorm simpa only [Real.norm_eq_abs, abs_sq, sq_abs] using hsq have hcoord : ∀ᵐ omega ∂mu, ∀ j : Fin d, ∀ epsilon : ℝ, 0 < epsilon → ∃ M : ℝ, 0 < M ∧ ∀ᶠ n : ℕ in atTop, (bootstrapResample (S.sampleVector n omega)).real {xstar | M < ‖scaledBootstrapMeanDifference (fun x ↦ g x j) n (S.sampleVector n omega) xstar‖} < epsilon := by rw [ae_all_iff] intro j exact scaledBootstrapMeanDifference_conditionallyBounded S (fun x ↦ g x j) (by fun_prop) (hcoord_sq j) unfold ConditionallyBoundedInProbability filter_upwards [hcoord] with omega homega intro epsilon hepsilon by_cases hd : d = 0 · subst d refine ⟨1, zero_lt_one, ?_⟩ filter_upwards with n have hv : ∀ xstar : Fin n → X, scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar = 0 := fun xstar ↦ Subsingleton.elim _ _ simp_rw [hv, norm_zero, not_lt_of_ge zero_le_one] simpa using hepsilon · let eta : ℝ := epsilon / d have heta : 0 < eta := by dsimp [eta] positivity choose M hM htail using fun j ↦ homega j eta heta let R : ℝ := ∑ j : Fin d, M j have hR : 0 < R := by dsimp [R] apply Finset.sum_pos · intro j hj exact hM j · exact ⟨⟨0, Nat.pos_of_ne_zero hd⟩, Finset.mem_univ _⟩ refine ⟨R, hR, ?_⟩ have hall : ∀ᶠ n : ℕ in atTop, ∀ j : Fin d, (bootstrapResample (S.sampleVector n omega)).real {xstar | M j < ‖scaledBootstrapMeanDifference (fun x ↦ g x j) n (S.sampleVector n omega) xstar‖} < eta := eventually_all.2 htail filter_upwards [hall, eventually_ne_atTop 0] with n hnall hn let data : Fin n → X := S.sampleVector n omega let V : (Fin n → X) → EuclideanSpace ℝ (Fin d) := fun xstar ↦ scaledBootstrapMeanDifference g n data xstar have hset : {xstar | R < ‖V xstar‖} ⊆ ⋃ j : Fin d, {xstar | M j < |V xstar j|} := by simpa only [R] using euclidean_norm_event_subset_coordinate_thresholds V M let _ : IsProbabilityMeasure (bootstrapResample data) := bootstrapResample_isProbabilityMeasure data hn calc (bootstrapResample (S.sampleVector n omega)).real {xstar | R < ‖scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar‖} = (bootstrapResample data).real {xstar | R < ‖V xstar‖} := rfl _ ≤ (bootstrapResample data).real (⋃ j : Fin d, {xstar | M j < |V xstar j|}) := measureReal_mono hset (measure_ne_top _ _) _ ≤ ∑ j : Fin d, (bootstrapResample data).real {xstar | M j < |V xstar j|} := measureReal_iUnion_fintype_le _ _ < ∑ _j : Fin d, eta := by apply Finset.sum_lt_sum_of_nonempty · exact ⟨⟨0, Nat.pos_of_ne_zero hd⟩, Finset.mem_univ _⟩ · intro j hj simpa only [data, V, scaledBootstrapMeanDifference, PiLp.smul_apply, PiLp.sub_apply, finMean_apply_real, Real.norm_eq_abs, smul_eq_mul] using hnall j _ = epsilon := by dsimp [eta] rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] field_simp

theorem samplingLinearization_smoothFunctionOfMeans {d : ℕ} (S : IIDSample Omega X mu P) (g : X → EuclideanSpace ℝ (Fin d)) (hg : Measurable g) (hg2 : Integrable (fun x ↦ ‖g x‖ ^ 2) P) (h : EuclideanSpace ℝ (Fin d) → ℝ) (Dh : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (hderiv : HasFDerivAt h Dh (∫ x, g x ∂P)) : Modes.TendstoInProbability (fun _ : ℕ => mu) (fun n omega ↦ sqrt (n : ℝ) * (smoothMeanEstimator g h n (S.sampleVector n omega) - h (∫ x, g x ∂P)) - IsAsymLinear.normalizedSum S (fun x ↦ Dh (g x - ∫ y, g y ∂P)) (fun k ↦ range k) n omega) atTop (fun _ _ ↦ 0) := by let _ : IsProbabilityMeasure mu := S.indep.isProbabilityMeasure let _ : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable let m : EuclideanSpace ℝ (Fin d) := ∫ x, g x ∂P let psi : X → EuclideanSpace ℝ (Fin d) := fun x ↦ g x - m let T : ℕ → Omega → EuclideanSpace ℝ (Fin d) := S.sampleMeanVec g let Sn : ℕ → Omega → EuclideanSpace ℝ (Fin d) := fun n omega ↦ sqrt (n : ℝ) • (T n omega - m) let R : ℕ → Omega → ℝ := fun n omega ↦ sqrt (n : ℝ) * (h (T n omega) - h m - Dh (T n omega - m)) have hg_int : Integrable g P := integrable_of_integrable_norm_sq g hg hg2 have hpsi : Measurable psi := by dsimp [psi, m] fun_prop have hpsi_mem : MemLp psi 2 P := by have hg_mem : MemLp g 2 P := (memLp_two_iff_integrable_sq_norm hg.aestronglyMeasurable).2 hg2 exact hg_mem.sub (memLp_const m) have hpsi2 : Integrable (fun x ↦ ‖psi x‖ ^ 2) P := (memLp_two_iff_integrable_sq_norm hpsi.aestronglyMeasurable).1 hpsi_mem have hpsi_mean : ∫ x, psi x ∂P = 0 := by dsimp [psi, m] rw [integral_sub hg_int (integrable_const _)] simp have hSn_eq : Sn = IsAsymLinearVec.normalizedSum S psi (fun k ↦ range k) := by exact sqrt_smul_sampleMeanVec_sub_eq_normalizedSum S g m have hSn_meas : ∀ n, AEMeasurable (Sn n) mu := by intro n dsimp [Sn, T] fun_prop have hSnDist : Modes.TendstoInLaw (fun _ : ℕ => mu) Sn atTop (gaussianLimit hpsi hpsi2) := by simpa only [hSn_eq] using S.clt_normalizedSum_vec hpsi hpsi2 hpsi_mean have hnorm_meas : ∀ n, AEMeasurable (fun omega ↦ ‖Sn n omega‖) mu := by intro n fun_prop let _ : IsProbabilityMeasure ((gaussianLimit hpsi hpsi2).map (fun z : EuclideanSpace ℝ (Fin d) ↦ ‖z‖)) := Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable have hnormDist : Modes.TendstoInLaw (fun _ : ℕ => mu) (fun n omega ↦ ‖Sn n omega‖) atTop ((gaussianLimit hpsi hpsi2).map fun z ↦ ‖z‖) := (Tendsto_dist_iff _ _ _ hnorm_meas).2 (Modes.TendstoInLaw.map_continuous hSnDist continuous_norm) have hSnBig : IsBigOp (fun n omega ↦ ‖Sn n omega‖) (fun _ ↦ (1 : ℝ)) mu := Modes.TendstoInLaw.tightness hnormDist have hTmeasure : TendstoInMeasure mu T atTop (fun _ ↦ m) := S.sampleMeanVec_tendstoInMeasure hg hg_int have hRlittle : IsLittleOp R (fun _ ↦ (1 : ℝ)) mu := by apply (Modes.isLittleOpF_iff_strict _ _ _ _ (Eventually.of_forall fun _ => zero_lt_one)).2 intro epsilon hepsilon rw [ENNReal.tendsto_nhds_zero] intro delta hdelta by_cases hdeltatop : delta = ⊤ · filter_upwards with n simp [hdeltatop] have hdeltapos : 0 < delta.toReal := ENNReal.toReal_pos (ne_of_gt hdelta) hdeltatop let alpha : ℝ := delta.toReal / 8 have halpha : 0 < alpha := by dsimp [alpha]; linarith rcases hSnBig (ofReal alpha) (ENNReal.ofReal_pos.mpr halpha) with ⟨M0, hM0pos, hM0⟩ let M : ℝ := max M0 1 have hM : 0 < M := lt_of_lt_of_le zero_lt_one (le_max_right M0 1) have hM0M : M0 ≤ M := le_max_left _ _ let A : ℕ → Set Omega := fun n ↦ {omega | M < ‖Sn n omega‖} have hlimA : limsup (fun n ↦ mu (A n)) atTop ≤ ofReal alpha := by refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) (Filter.limsup_le_of_le (h := hM0)) intro n apply measure_mono intro omega homega dsimp [A] at homega ⊢ have := lt_of_le_of_lt hM0M homega simpa [abs_of_nonneg (norm_nonneg _)] using this.le have halpha2 : ofReal alpha < ofReal (2 * alpha) := by rw [ENNReal.ofReal_lt_ofReal_iff] <;> linarith have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimA halpha2) let eta : ℝ := epsilon / M have heta : 0 < eta := div_pos hepsilon hM have hlocal : ∀ᶠ z in 𝓝 m, ‖h z - h m - Dh (z - m)‖ ≤ eta * ‖z - m‖ := by have h0 := (smoothRemainder_isLittleO hderiv).def heta simpa [m] using h0 rcases Metric.eventually_nhds_iff.mp hlocal with ⟨rho, hrho, hrhoprop⟩ have hTtail : Tendsto (fun n ↦ mu {omega | rho / 2 ≤ ‖T n omega - m‖}) atTop (𝓝 0) := by rw [tendstoInMeasure_iff_norm] at hTmeasure exact hTmeasure (rho / 2) (by positivity) have hBsmall := (ENNReal.tendsto_nhds_zero.mp hTtail) (ofReal alpha) (ENNReal.ofReal_pos.mpr halpha) filter_upwards [hAevent, hBsmall] with n hAn hBn let B : Set Omega := {omega | rho ≤ ‖T n omega - m‖} let C : Set Omega := {omega | epsilon < |R n omega|} have hB : mu B < ofReal (2 * alpha) := by refine lt_of_le_of_lt (le_trans (measure_mono ?_) hBn) halpha2 intro omega homega change rho ≤ ‖T n omega - m‖ at homega change rho / 2 ≤ ‖T n omega - m‖ linarith have hsubset : C ⊆ A n ∪ B := by intro omega homega by_contra hnot have hSnle : ‖Sn n omega‖ ≤ M := le_of_not_gt (fun hA ↦ hnot (inl hA)) have hnear : ‖T n omega - m‖ < rho := lt_of_not_ge (fun hB' ↦ hnot (inr hB')) have hder := hrhoprop (by simpa [dist_eq_norm] using hnear) have hRle : |R n omega| ≤ epsilon := by calc |R n omega| = sqrt (n : ℝ) * ‖h (T n omega) - h m - Dh (T n omega - m)‖ := by dsimp [R] rw [abs_mul, abs_of_nonneg (Real.sqrt_nonneg _)] _ ≤ sqrt (n : ℝ) * (eta * ‖T n omega - m‖) := mul_le_mul_of_nonneg_left hder (Real.sqrt_nonneg _) _ = eta * ‖Sn n omega‖ := by dsimp [Sn] rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _)] ring _ ≤ eta * M := mul_le_mul_of_nonneg_left hSnle heta.le _ = epsilon := by dsimp [eta]; field_simp [hM.ne'] exact not_lt_of_ge hRle homega have h4alpha : ofReal (4 * alpha) < delta := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [alpha]; linarith · dsimp [alpha]; linarith · exact hdeltatop exact le_of_lt <| calc mu {omega | epsilon * (fun _ ↦ (1 : ℝ)) n < |R n omega|} = mu C := by simp [C] _ ≤ mu (A n ∪ B) := measure_mono hsubset _ ≤ mu (A n) + mu B := measure_union_le _ _ _ < ofReal (2 * alpha) + ofReal (2 * alpha) := ENNReal.add_lt_add hAn hB _ = ofReal (4 * alpha) := by rw [← ENNReal.ofReal_add] <;> try linarith congr 1 <;> ring _ < delta := h4alpha have hRprob := Modes.TendstoInProbability.of_isLittleOp_one hRlittle rw [Tendsto_inProb_iff] at hRprob ⊢ refine hRprob.congr' ?_ EventuallyEq.rfl filter_upwards [eventually_ne_atTop 0] with n hn filter_upwards with omega dsimp [R, T, m] rw [← finMean_sampleVector_vec S g omega] unfold smoothMeanEstimator have hlin : IsAsymLinear.normalizedSum S (fun x ↦ Dh (g x - ∫ y, g y ∂P)) (fun k ↦ range k) n omega = sqrt (n : ℝ) * Dh (finMean (fun i ↦ g (S.sampleVector n omega i)) - ∫ y, g y ∂P) := by unfold IsAsymLinear.normalizedSum finMean IIDSample.sampleVector simp only [Finset.card_range, ContinuousLinearMap.map_sub, map_sum, map_smul, smul_eq_mul, Finset.sum_sub_distrib, Finset.sum_const, nsmul_eq_mul] have hfin : (∑ i : Fin n, Dh (g (S.Z i omega))) = ∑ i ∈ range n, Dh (g (S.Z i omega)) := Fin.sum_univ_eq_sum_range (fun i ↦ Dh (g (S.Z i omega))) n rw [hfin] have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast hn have hsqrt : sqrt (n : ℝ) ≠ 0 := Real.sqrt_ne_zero'.mpr (Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)) have hsqrt_sq : (sqrt (n : ℝ)) ^ 2 = (n : ℝ) := Real.sq_sqrt (Nat.cast_nonneg n) field_simp rw [hsqrt_sq] rw [hlin] ring

theorem bootstrapLinearization_smoothFunctionOfMeans {d : ℕ} (S : IIDSample Omega X mu P) (g : X → EuclideanSpace ℝ (Fin d)) (hg : Measurable g) (hg2 : Integrable (fun x ↦ ‖g x‖ ^ 2) P) (h : EuclideanSpace ℝ (Fin d) → ℝ) (Dh : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (hderiv : HasFDerivAt h Dh (∫ x, g x ∂P)) : ∀ epsilon : ℝ, 0 < epsilon → Tendsto (fun n ↦ mu.real {omega | epsilon < (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < abs (centeredEstimatorBootstrapStatistic (smoothMeanEstimator g h) n (S.sampleVector n omega) xstar - centeredBootstrapSum (fun x ↦ Dh (g x - ∫ y, g y ∂P)) (S.sampleVector n omega) xstar)}}) atTop (𝓝 0) := by classical let _ : IsProbabilityMeasure mu := S.indep.isProbabilityMeasure let _ : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable let m : EuclideanSpace ℝ (Fin d) := ∫ x, g x ∂P let psi : X → EuclideanSpace ℝ (Fin d) := fun x ↦ g x - m let T : ℕ → Omega → EuclideanSpace ℝ (Fin d) := S.sampleMeanVec g let Sn : ℕ → Omega → EuclideanSpace ℝ (Fin d) := fun n omega ↦ sqrt (n : ℝ) • (T n omega - m) have hg_int : Integrable g P := integrable_of_integrable_norm_sq g hg hg2 have hpsi : Measurable psi := by dsimp [psi, m] fun_prop have hpsi_mem : MemLp psi 2 P := by have hg_mem : MemLp g 2 P := (memLp_two_iff_integrable_sq_norm hg.aestronglyMeasurable).2 hg2 exact hg_mem.sub (memLp_const m) have hpsi2 : Integrable (fun x ↦ ‖psi x‖ ^ 2) P := (memLp_two_iff_integrable_sq_norm hpsi.aestronglyMeasurable).1 hpsi_mem have hpsi_mean : ∫ x, psi x ∂P = 0 := by dsimp [psi, m] rw [integral_sub hg_int (integrable_const _)] simp have hSn_eq : Sn = IsAsymLinearVec.normalizedSum S psi (fun k ↦ range k) := by exact sqrt_smul_sampleMeanVec_sub_eq_normalizedSum S g m have hSn_meas : ∀ n, AEMeasurable (Sn n) mu := by intro n dsimp [Sn, T] fun_prop have hSnDist : Modes.TendstoInLaw (fun _ : ℕ => mu) Sn atTop (gaussianLimit hpsi hpsi2) := by simpa only [hSn_eq] using S.clt_normalizedSum_vec hpsi hpsi2 hpsi_mean have hnorm_meas : ∀ n, AEMeasurable (fun omega ↦ ‖Sn n omega‖) mu := by intro n fun_prop let _ : IsProbabilityMeasure ((gaussianLimit hpsi hpsi2).map (fun z : EuclideanSpace ℝ (Fin d) ↦ ‖z‖)) := Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable have hnormDist : Modes.TendstoInLaw (fun _ : ℕ => mu) (fun n omega ↦ ‖Sn n omega‖) atTop ((gaussianLimit hpsi hpsi2).map fun z ↦ ‖z‖) := (Tendsto_dist_iff _ _ _ hnorm_meas).2 (Modes.TendstoInLaw.map_continuous hSnDist continuous_norm) have hSnBig : IsBigOp (fun n omega ↦ ‖Sn n omega‖) (fun _ ↦ (1 : ℝ)) mu := Modes.TendstoInLaw.tightness hnormDist intro epsilon hepsilon rw [Metric.tendsto_atTop] intro delta hdelta let alpha : ℝ := delta / 12 have halpha : 0 < alpha := by dsimp [alpha]; linarith rcases hSnBig (ofReal alpha) (ENNReal.ofReal_pos.mpr halpha) with ⟨M₀, hM₀pos, hM₀⟩ have hM₀lim : limsup (fun n ↦ mu {omega | M₀ < ‖Sn n omega‖}) atTop ≤ ofReal alpha := by refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) (Filter.limsup_le_of_le (h := hM₀)) intro n apply measure_mono intro omega homega simpa [abs_of_nonneg (norm_nonneg _)] using homega.le have halpha_lt : ofReal alpha < ofReal (2 * alpha) := by rw [ENNReal.ofReal_lt_ofReal_iff] <;> linarith have hdataENN := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hM₀lim halpha_lt) have hdata : ∀ᶠ n : ℕ in atTop, mu.real {omega | M₀ < ‖Sn n omega‖} < 2 * alpha := by filter_upwards [hdataENN] with n hn' rw [Measure.real_def] have hfin : mu {omega | M₀ < ‖Sn n omega‖} ≠ ⊤ := measure_ne_top _ _ have htop : ofReal (2 * alpha) ≠ ⊤ := ENNReal.ofReal_ne_top calc (mu {omega | M₀ < ‖Sn n omega‖}).toReal < (ofReal (2 * alpha)).toReal := (ENNReal.toReal_lt_toReal hfin htop).2 hn' _ = 2 * alpha := ENNReal.toReal_ofReal (by positivity) rcases scaledBootstrapMeanDifferenceVec_outer_tight S g hg hg2 (epsilon / 4) (by positivity) (delta / 3) (by positivity) with ⟨Mₑ, hMₑ, hboot⟩ let K : ℝ := max Mₑ (max M₀ 1) have hK : 0 < K := lt_of_lt_of_le zero_lt_one (le_trans (le_max_right M₀ 1) (le_max_right Mₑ (max M₀ 1))) let eta : ℝ := epsilon / (4 * K) have heta : 0 < eta := by dsimp [eta]; positivity have hlocal : ∀ᶠ z in nhds m, ‖h z - h m - Dh (z - m)‖ ≤ eta * ‖z - m‖ := by simpa [m] using (smoothRemainder_isLittleO hderiv).def heta rcases Metric.eventually_nhds_iff.mp hlocal with ⟨rho, hrho, hrhoprop⟩ let qNear : ℕ → Omega → ℝ := fun n omega ↦ (bootstrapResample (S.sampleVector n omega)).real {xstar | rho / 2 < ‖finMean (fun i ↦ g (xstar i)) - m‖} have hqNear_meas (n : ℕ) : Measurable (qNear n) := by let A : Set ((Fin n → X) × (Fin n → X)) := {z | rho / 2 < ‖finMean (fun i ↦ g (z.2 i)) - m‖} have hA : MeasurableSet A := by apply measurableSet_lt measurable_const unfold finMean fun_prop have hsamp : Measurable (fun omega ↦ S.sampleVector n omega) := by apply measurable_pi_iff.mpr intro i exact S.meas i change Measurable ((fun x : Fin n → X ↦ (bootstrapResample x).real {xstar | (x, xstar) ∈ A}) ∘ fun omega ↦ S.sampleVector n omega) exact (measurable_bootstrapResample_real_of_measurableSet A hA).comp hsamp have hqNear_ae : ∀ᵐ omega ∂mu, Tendsto (fun n ↦ qNear n omega) atTop (nhds 0) := by filter_upwards [bootstrapMeanVec_sub_populationMean_tendsto_zero_ae S g hg hg_int] with omega homega simpa [qNear, m] using homega (rho / 2) (by positivity) have hnearOuter : Tendsto (fun n ↦ mu.real {omega | epsilon / 4 < qNear n omega}) atTop (nhds 0) := measureReal_gt_tendsto_zero_of_ae_tendsto hqNear_meas hqNear_ae (epsilon / 4) (by positivity) have hnear := hnearOuter.eventually (Iio_mem_nhds (show 0 < delta / 3 by positivity)) have hsqrt : ∀ᶠ n : ℕ in atTop, 2 * K / rho < sqrt (n : ℝ) := (Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop).eventually_gt_atTop _ apply eventually_atTop.1 filter_upwards [hdata, hboot, hnear, hsqrt, eventually_ne_atTop 0] with n hdata_n hboot_n hnear_n hsqrt_n hn simp only [Real.dist_eq, sub_zero, abs_of_nonneg measureReal_nonneg] let badData : Set Omega := {omega | M₀ < ‖Sn n omega‖} let badNear : Set Omega := {omega | epsilon / 4 < qNear n omega} let badBoot : Set Omega := {omega | epsilon / 4 < (bootstrapResample (S.sampleVector n omega)).real {xstar | Mₑ < ‖scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar‖}} have houterSubset : {omega | epsilon < (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < abs (centeredEstimatorBootstrapStatistic (smoothMeanEstimator g h) n (S.sampleVector n omega) xstar - centeredBootstrapSum (fun x ↦ Dh (g x - ∫ y, g y ∂P)) (S.sampleVector n omega) xstar)}} ⊆ badData ∪ (badNear ∪ badBoot) := by intro omega homega by_contra hgood have hdata_good : ‖Sn n omega‖ ≤ M₀ := le_of_not_gt (fun hh ↦ hgood (inl hh)) have hnear_good : qNear n omega ≤ epsilon / 4 := le_of_not_gt (fun hh ↦ hgood (inr (inl hh))) have hboot_good : (bootstrapResample (S.sampleVector n omega)).real {xstar | Mₑ < ‖scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar‖} ≤ epsilon / 4 := le_of_not_gt (fun hh ↦ hgood (inr (inr hh))) let data : Fin n → X := S.sampleVector n omega let bad : Set (Fin n → X) := {xstar | epsilon < abs (centeredEstimatorBootstrapStatistic (smoothMeanEstimator g h) n data xstar - centeredBootstrapSum (fun x ↦ Dh (g x - ∫ y, g y ∂P)) data xstar)} let near : Set (Fin n → X) := {xstar | rho / 2 < ‖finMean (fun i ↦ g (xstar i)) - m‖} let boot : Set (Fin n → X) := {xstar | Mₑ < ‖scaledBootstrapMeanDifference g n data xstar‖} have hsqrt_pos : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 (Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)) have hKdata : ‖Sn n omega‖ ≤ K := hdata_good.trans (le_trans (le_max_left M₀ 1) (le_max_right Mₑ (max M₀ 1))) have hTm : ‖finMean (fun i ↦ g (data i)) - m‖ < rho := by have hscale : sqrt (n : ℝ) * ‖finMean (fun i ↦ g (data i)) - m‖ = ‖Sn n omega‖ := by dsimp [Sn, T, data] rw [← finMean_sampleVector_vec S g omega, norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _)] have hprod : sqrt (n : ℝ) * ‖finMean (fun i ↦ g (data i)) - m‖ < sqrt (n : ℝ) * rho := by rw [hscale] calc ‖Sn n omega‖ ≤ K := hKdata _ < sqrt (n : ℝ) * rho := by calc K < 2 * K := by linarith _ = (2 * K / rho) * rho := by field_simp _ < sqrt (n : ℝ) * rho := mul_lt_mul_of_pos_right hsqrt_n hrho nlinarith have hbadSubset : bad ⊆ near ∪ boot := by intro xstar hxstar by_contra hxgood have hxnear : ‖finMean (fun i ↦ g (xstar i)) - m‖ ≤ rho / 2 := le_of_not_gt (fun hh ↦ hxgood (inl hh)) have hxboot : ‖scaledBootstrapMeanDifference g n data xstar‖ ≤ Mₑ := le_of_not_gt (fun hh ↦ hxgood (inr hh)) have hlocalStar := hrhoprop (by simpa [dist_eq_norm] using lt_of_le_of_lt hxnear (by linarith)) have hlocalData := hrhoprop (by simpa [dist_eq_norm] using hTm) let starMean := finMean (fun i ↦ g (xstar i)) let dataMean := finMean (fun i ↦ g (data i)) have herror : centeredEstimatorBootstrapStatistic (smoothMeanEstimator g h) n data xstar - centeredBootstrapSum (fun x ↦ Dh (g x - ∫ y, g y ∂P)) data xstar = sqrt (n : ℝ) * ((h starMean - h m - Dh (starMean - m)) - (h dataMean - h m - Dh (dataMean - m))) := by rw [centeredBootstrapSum_eq_sqrt_mul_finAverage_sub hn] unfold centeredEstimatorBootstrapStatistic smoothMeanEstimator change _ = sqrt (n : ℝ) * ((h starMean - h m - Dh (starMean - m)) - (h dataMean - h m - Dh (dataMean - m))) have hstar : finMean (fun i ↦ Dh (g (xstar i) - ∫ y, g y ∂P)) = Dh (starMean - m) := by have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast hn unfold finMean starMean finMean simp only [Finset.sum_sub_distrib, map_sub, map_smul, map_sum, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, smul_eq_mul] field_simp simp [m] have hdat : finMean (fun i ↦ Dh (g (data i) - ∫ y, g y ∂P)) = Dh (dataMean - m) := by have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast hn unfold finMean dataMean finMean simp only [Finset.sum_sub_distrib, map_sub, map_smul, map_sum, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, smul_eq_mul] field_simp simp [m] rw [hstar, hdat] ring have hscaledStar : sqrt (n : ℝ) • (starMean - m) = scaledBootstrapMeanDifference g n data xstar + Sn n omega := by dsimp [scaledBootstrapMeanDifference, Sn, T, starMean, dataMean, data] rw [← finMean_sampleVector_vec S g omega] rw [← sub_add_sub_cancel starMean dataMean m, smul_add] have hstarScale : sqrt (n : ℝ) * ‖starMean - m‖ ≤ -- … truncated; follow the source link for the rest …

theorem smoothFunctionOfMeans {d : ℕ} (S : IIDSample Omega X mu P) (g : X → EuclideanSpace ℝ (Fin d)) (hg : Measurable g) (hg2 : Integrable (fun x ↦ ‖g x‖ ^ 2) P) (h : EuclideanSpace ℝ (Fin d) → ℝ) (hh : Measurable h) (Dh : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (hderiv : HasFDerivAt h Dh (∫ x, g x ∂P)) (hvar : 0 < ∫ x, (Dh (g x - ∫ y, g y ∂P)) ^ 2 ∂P) : BootstrapAsymLinear S (smoothMeanEstimator g h) (h (∫ x, g x ∂P)) (fun x ↦ Dh (g x - ∫ y, g y ∂P)) := by let _ : IsProbabilityMeasure mu := S.indep.isProbabilityMeasure let _ : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable have hg_mem : MemLp g 2 P := (memLp_two_iff_integrable_sq_norm hg.aestronglyMeasurable).2 hg2 have hg_int : Integrable g P := hg_mem.integrable (by norm_num) have hcentered_mem : MemLp (fun x ↦ g x - ∫ y, g y ∂P) 2 P := hg_mem.sub (memLp_const _) have hcentered_int : Integrable (fun x ↦ g x - ∫ y, g y ∂P) P := hcentered_mem.integrable (by norm_num) have hpsi_mem : MemLp (fun x ↦ Dh (g x - ∫ y, g y ∂P)) 2 P := hcentered_mem.continuousLinearMap_comp Dh have hpsi_meas : Measurable (fun x ↦ Dh (g x - ∫ y, g y ∂P)) := Dh.continuous.measurable.comp (hg.sub measurable_const) refine ⟨⟨fun n ↦ measurable_smoothMeanEstimator hg hh n, hpsi_meas⟩, ?_, ⟨hvar, (memLp_two_iff_integrable_sq hpsi_meas.aestronglyMeasurable).1 hpsi_mem⟩, samplingLinearization_smoothFunctionOfMeans S g hg hg2 h Dh hderiv, bootstrapLinearization_smoothFunctionOfMeans S g hg hg2 h Dh hderiv⟩ rw [Dh.integral_comp_comm hcentered_int] rw [integral_sub hg_int (integrable_const _)] simp

theorem percentileCI_coverage_smoothFunctionOfMeans {d : ℕ} (S : IIDSample Omega X mu P) (g : X → EuclideanSpace ℝ (Fin d)) (hg : Measurable g) (hg2 : Integrable (fun x ↦ ‖g x‖ ^ 2) P) (h : EuclideanSpace ℝ (Fin d) → ℝ) (hh : Measurable h) (Dh : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (hderiv : HasFDerivAt h Dh (∫ x, g x ∂P)) (hvar : 0 < ∫ x, (Dh (g x - ∫ y, g y ∂P)) ^ 2 ∂P) {alpha : ℝ} (halpha0 : 0 < alpha) (halpha1 : alpha < 1) : Tendsto (fun n ↦ mu.real {omega | h (∫ x, g x ∂P) ∈ percentileCI (smoothMeanEstimator g h) n alpha (S.sampleVector n omega)}) atTop (𝓝 (1 - alpha)) := by exact (smoothFunctionOfMeans S g hg hg2 h hh Dh hderiv hvar).percentileCI_coverage halpha0 halpha1

theorem ratioOfMeans (S : IIDSample Omega X mu P) (g : X → EuclideanSpace ℝ (Fin 2)) (hg : Measurable g) (hg2 : Integrable (fun x ↦ ‖g x‖ ^ 2) P) (hden : (∫ x, g x ∂P) 1 ≠ 0) (hvar : 0 < ∫ x, (ratioInfluence g (∫ y, g y ∂P) x) ^ 2 ∂P) : BootstrapAsymLinear S (ratioOfMeansEstimator g) ((∫ x, g x ∂P) 0 / (∫ x, g x ∂P) 1) (ratioInfluence g (∫ y, g y ∂P)) := by have hratio_meas : Measurable coordinateRatio := by unfold coordinateRatio exact Measurable.fun_div (EuclideanSpace.proj (𝕜 := ℝ) 0).continuous.measurable (EuclideanSpace.proj (𝕜 := ℝ) 1).continuous.measurable have hpsi_eq : (fun x ↦ fderiv ℝ coordinateRatio (∫ y, g y ∂P) (g x - ∫ y, g y ∂P)) = ratioInfluence g (∫ y, g y ∂P) := by funext x rw [fderiv_coordinateRatio_apply (∫ y, g y ∂P) _ hden] simp [ratioInfluence] have hvar' : 0 < ∫ x, (fderiv ℝ coordinateRatio (∫ y, g y ∂P) (g x - ∫ y, g y ∂P)) ^ 2 ∂P := by have hpsi_eq_apply (x : X) : fderiv ℝ coordinateRatio (∫ y, g y ∂P) (g x - ∫ y, g y ∂P) = ratioInfluence g (∫ y, g y ∂P) x := congrFun hpsi_eq x simpa only [hpsi_eq_apply] using hvar have hsmooth := smoothFunctionOfMeans S g hg hg2 coordinateRatio hratio_meas (fderiv ℝ coordinateRatio (∫ x, g x ∂P)) (coordinateRatio_hasFDerivAt (∫ x, g x ∂P) hden) hvar' have hest_eq : ratioOfMeansEstimator g = smoothMeanEstimator g coordinateRatio := by funext n x exact ratioOfMeansEstimator_eq_smoothMeanEstimator g n x rw [hest_eq] simpa only [coordinateRatio, hpsi_eq] using hsmooth

theorem measurable_bootstrapResample_real_of_measurableSet {n : ℕ} (A : Set ((Fin n → X) × (Fin n → X))) (hA : MeasurableSet A) : Measurable (fun x : Fin n → X ↦ (bootstrapResample x).real {xstar | (x, xstar) ∈ A}) := by classical by_cases hn : n = 0 · subst n exact Subsingleton.measurable · rw [show (fun x : Fin n → X ↦ (bootstrapResample x).real {xstar | (x, xstar) ∈ A}) = fun x ↦ ((n : ℝ) ^ n)⁻¹ * ∑ j : Fin n → Fin n, if (x, x ∘ j) ∈ A then 1 else 0 by funext x have hsection : MeasurableSet {xstar | (x, xstar) ∈ A} := hA.preimage (measurable_const.prodMk measurable_id) rw [bootstrapResample_eq_average_dirac, Measure.real, Measure.smul_apply, Measure.finsetSum_apply] simp only [Measure.dirac_apply' _ hsection, smul_eq_mul] rw [ENNReal.toReal_mul, ENNReal.toReal_inv, ENNReal.toReal_pow, ENNReal.toReal_natCast] rw [ENNReal.toReal_sum (by intro j hj by_cases h : (x, x ∘ j) ∈ A <;> simp [indicator, h])] congr 1 apply Finset.sum_congr rfl intro j hj by_cases h : (x, x ∘ j) ∈ A <;> simp [indicator, h]] apply Measurable.const_mul apply Finset.measurable_sum Finset.univ intro j hj have hcomp : Measurable (fun x : Fin n → X ↦ x ∘ j) := by refine measurable_pi_iff.mpr fun i ↦ ?_ exact measurable_pi_apply (j i) exact Measurable.ite (hA.preimage (measurable_id.prodMk hcomp)) measurable_const measurable_const

theorem smoothRemainder_isLittleO {d : ℕ} {h : EuclideanSpace ℝ (Fin d) → ℝ} {Dh : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ} {m : EuclideanSpace ℝ (Fin d)} (hderiv : HasFDerivAt h Dh m) : (fun z ↦ h z - h m - Dh (z - m)) =o[𝓝 m] (fun z ↦ z - m) := by exact hderiv.isLittleO

theorem scaledBootstrapMeanDifferenceVec_outer_tight {X : Type*} [MeasurableSpace X] {P : Measure X} {d : ℕ} (S : IIDSample Omega X mu P) (g : X → EuclideanSpace ℝ (Fin d)) (hg : Measurable g) (hg2 : Integrable (fun x ↦ ‖g x‖ ^ 2) P) (epsilon : ℝ) (hepsilon : 0 < epsilon) (delta : ℝ) (hdelta : 0 < delta) : ∃ M : ℝ, 0 < M ∧ ∀ᶠ n : ℕ in atTop, mu.real {omega | epsilon < (bootstrapResample (S.sampleVector n omega)).real {xstar | M < ‖scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar‖}} < delta := by classical let _ : IsProbabilityMeasure mu := S.indep.isProbabilityMeasure let q : ℕ → ℕ → Omega → ℝ := fun K n omega ↦ (bootstrapResample (S.sampleVector n omega)).real {xstar | (K + 1 : ℝ) < ‖scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar‖} have hq_meas (K n : ℕ) : Measurable (q K n) := by let A : Set ((Fin n → X) × (Fin n → X)) := {z | (K + 1 : ℝ) < ‖scaledBootstrapMeanDifference g n z.1 z.2‖} have hA : MeasurableSet A := by apply measurableSet_lt measurable_const unfold scaledBootstrapMeanDifference finMean fun_prop have hsamp : Measurable (fun omega ↦ S.sampleVector n omega) := by apply measurable_pi_iff.mpr intro i exact S.meas i change Measurable ((fun x : Fin n → X ↦ (bootstrapResample x).real {xstar | (x, xstar) ∈ A}) ∘ fun omega ↦ S.sampleVector n omega) exact (measurable_bootstrapResample_real_of_measurableSet A hA).comp hsamp let G : ℕ → Set Omega := fun K ↦ {omega | ∀ n, K ≤ n → q K n omega < epsilon} have hG_meas (K : ℕ) : MeasurableSet (G K) := by have hrepr : G K = ⋂ n : ℕ, ⋂ (_h : K ≤ n), {omega | q K n omega < epsilon} := by ext omega simp only [G, Set.mem_ofPred_eq, Set.mem_iInter] rw [hrepr] exact MeasurableSet.iInter fun n ↦ MeasurableSet.iInter fun _ ↦ measurableSet_lt (hq_meas K n) measurable_const have hG_mono : Monotone G := by intro K L hKL omega homega change ∀ n, K ≤ n → q K n omega < epsilon at homega change ∀ n, L ≤ n → q L n omega < epsilon intro n hLn have htail := homega n (hKL.trans hLn) by_cases hEq : K = L · simpa [hEq] using htail · have hKLlt : K < L := lt_of_le_of_ne hKL hEq have hn : n ≠ 0 := by omega let _ : IsProbabilityMeasure (bootstrapResample (S.sampleVector n omega)) := bootstrapResample_isProbabilityMeasure _ hn apply (measureReal_mono ?_).trans_lt htail intro xstar hxstar change (L + 1 : ℝ) < ‖scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar‖ at hxstar change (K + 1 : ℝ) < ‖scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar‖ have hcast : (K + 1 : ℝ) < (L + 1 : ℝ) := by exact_mod_cast Nat.add_lt_add_right hKLlt 1 exact hcast.trans hxstar have hbounded := scaledBootstrapMeanDifferenceVec_conditionallyBounded S g hg hg2 unfold ConditionallyBoundedInProbability at hbounded have heventually_G : ∀ᵐ omega ∂mu, ∀ᶠ K : ℕ in atTop, omega ∈ G K := by filter_upwards [hbounded] with omega homega rcases homega epsilon hepsilon with ⟨R, hR, htail⟩ rcases eventually_atTop.1 htail with ⟨N, hN⟩ obtain ⟨K₀ : ℕ, hK₀⟩ := exists_nat_gt R have hK₀pos : 0 < K₀ := by by_contra h have : K₀ = 0 := Nat.eq_zero_of_not_pos h subst K₀ norm_num at hK₀ linarith let K := max N K₀ have homegaK : omega ∈ G K := by change ∀ n, K ≤ n → q K n omega < epsilon intro n hKn have hNn : N ≤ n := (Nat.le_max_left N K₀).trans hKn have hK₀K : K₀ ≤ K := Nat.le_max_right N K₀ have hn : n ≠ 0 := by omega let _ : IsProbabilityMeasure (bootstrapResample (S.sampleVector n omega)) := bootstrapResample_isProbabilityMeasure _ hn apply (measureReal_mono ?_).trans_lt (hN n hNn) intro xstar hxstar change (K + 1 : ℝ) < ‖scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar‖ at hxstar change R < ‖scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar‖ apply (show R < (K + 1 : ℝ) by calc R < (K₀ : ℝ) := hK₀ _ ≤ (K : ℝ) := by exact_mod_cast hK₀K _ < (K + 1 : ℝ) := by norm_num).trans hxstar filter_upwards [eventually_ge_atTop K] with L hKL exact hG_mono hKL homegaK let f : ℕ → Omega → ℝ := fun K omega ↦ if omega ∈ G K then 0 else 1 have hf_meas (K : ℕ) : Measurable (f K) := by exact Measurable.ite (hG_meas K) measurable_const measurable_const have hf_zero : ∀ᵐ omega ∂mu, Tendsto (fun K ↦ f K omega) atTop (𝓝 0) := by filter_upwards [heventually_G] with omega homega have heq : ∀ᶠ K : ℕ in atTop, f K omega = 0 := by filter_upwards [homega] with K hK simp [f, hK] exact (tendsto_congr' heq).2 tendsto_const_nhds have hcompl_tendsto := measureReal_gt_tendsto_zero_of_ae_tendsto hf_meas hf_zero (1 / 2 : ℝ) (by norm_num) have hsmall : ∀ᶠ K : ℕ in atTop, mu.real {omega | (1 / 2 : ℝ) < f K omega} < delta := hcompl_tendsto.eventually (Iio_mem_nhds hdelta) rcases eventually_atTop.1 hsmall with ⟨K, hK⟩ refine ⟨K + 1, by positivity, ?_⟩ filter_upwards [eventually_ge_atTop K] with n hKn have hbad : {omega | epsilon < (bootstrapResample (S.sampleVector n omega)).real {xstar | (K + 1 : ℝ) < ‖scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar‖}} ⊆ (G K)ᶜ := by intro omega homega hgood exact (not_lt_of_ge homega.le) (hgood n hKn) calc mu.real {omega | epsilon < (bootstrapResample (S.sampleVector n omega)).real {xstar | (K + 1 : ℝ) < ‖scaledBootstrapMeanDifference g n (S.sampleVector n omega) xstar‖}} ≤ mu.real (G K)ᶜ := measureReal_mono hbad _ = mu.real {omega | (1 / 2 : ℝ) < f K omega} := by congr 1 ext omega by_cases homega : omega ∈ G K · simp [f, homega] · simp [f, homega] norm_num _ < delta := hK K le_rfl

theorem bootstrapMean_sub_dataMean_tendsto_zero_ae (S : IIDSample Omega X mu P) (g : X → ℝ) (hg : Measurable g) (hg_int : Integrable g P) : ∀ᵐ omega ∂mu, ∀ epsilon : ℝ, 0 < epsilon → Tendsto (fun n ↦ (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < |finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (S.sampleVector n omega i))|}) atTop (𝓝 0) := by have htails : ∀ᵐ omega ∂mu, ∀ M : ℕ, Tendsto (fun n ↦ S.sampleMean (fun x ↦ |g x - truncation g (M : ℝ) x|) n omega) atTop (nhds (∫ x, |g x - truncation g (M : ℝ) x| ∂P)) := by rw [ae_all_iff] intro M let r : X → ℝ := fun x ↦ |g x - truncation g (M : ℝ) x| have hr : Measurable r := by dsimp [r] unfold truncation exact (hg.sub ((measurable_id.indicator measurableSet_Ioc).comp hg)).abs have hrint : Integrable r P := by refine Integrable.mono (hg_int.norm.const_mul 2) hr.aestronglyMeasurable ?_ filter_upwards with x dsimp [r] rw [abs_abs, abs_of_nonneg (by positivity : 0 ≤ 2 * |g x|)] calc |g x - truncation g (M : ℝ) x| ≤ |g x| + |truncation g (M : ℝ) x| := abs_sub _ _ _ ≤ |g x| + |g x| := add_le_add_right (abs_truncation_le_abs_self g (M : ℝ) x) _ _ = 2 * |g x| := by ring simpa [r] using sampleMean_integrable_tendsto_ae S r hr hrint filter_upwards [htails] with omega homega intro epsilon hepsilon apply tendsto_order.2 constructor · intro a ha filter_upwards with n exact ha.trans_le measureReal_nonneg · intro delta hdelta let c : ℝ := min (delta * epsilon / 16) (epsilon / 4) have hc : 0 < c := by dsimp [c] exact lt_min (by positivity) (by positivity) have htailNat : Tendsto (fun M : ℕ ↦ ∫ x, |g x - truncation g (M : ℝ) x| ∂P) atTop (nhds 0) := by exact (tailIntegral_tendsto_zero g hg hg_int).comp (tendsto_natCast_atTop_atTop (R := ℝ)) have hsmall : ∀ᶠ M : ℕ in atTop, ∫ x, |g x - truncation g (M : ℝ) x| ∂P < c / 2 := htailNat.eventually (eventually_lt_nhds (by positivity)) rcases eventually_atTop.1 hsmall with ⟨M, hM⟩ have hpop : ∫ x, |g x - truncation g (M : ℝ) x| ∂P < c := (hM M le_rfl).trans (by linarith [hc]) have hsample : ∀ᶠ n : ℕ in atTop, S.sampleMean (fun x ↦ |g x - truncation g (M : ℝ) x|) n omega < c := (homega M).eventually (eventually_lt_nhds hpop) have hden : Tendsto (fun n : ℕ ↦ (n : ℝ) * (epsilon / 2) ^ 2) atTop atTop := by simpa [mul_comm] using (tendsto_natCast_atTop_atTop (R := ℝ)).const_mul_atTop (sq_pos_of_pos (by positivity : 0 < epsilon / 2)) have hrate : Tendsto (fun n : ℕ ↦ 4 * |(M : ℝ)| ^ 2 / ((n : ℝ) * (epsilon / 2) ^ 2)) atTop (nhds 0) := tendsto_const_nhds.div_atTop hden have hrateSmall : ∀ᶠ n : ℕ in atTop, 4 * |(M : ℝ)| ^ 2 / ((n : ℝ) * (epsilon / 2) ^ 2) < 3 * delta / 4 := hrate.eventually (eventually_lt_nhds (by linarith)) filter_upwards [hsample, hrateSmall, eventually_ne_atTop 0] with n hsample_n hrate_n hn let t : X → ℝ := truncation g (M : ℝ) let q : X → ℝ := g - t let r : X → ℝ := fun x ↦ |q x| let data : Fin n → X := S.sampleVector n omega have ht : Measurable t := by dsimp [t] unfold truncation exact (measurable_id.indicator measurableSet_Ioc).comp hg have hr : Measurable r := by dsimp [r, q] exact (hg.sub ht).abs have hrnonneg : ∀ x, 0 ≤ r x := fun x ↦ abs_nonneg _ have hdata : finMean (fun i ↦ r (data i)) ≤ epsilon / 4 := by rw [show finMean (fun i ↦ r (data i)) = S.sampleMean r n omega by exact finMean_sampleVector S r n omega] have hc_le : c ≤ epsilon / 4 := min_le_right _ _ exact (le_of_lt (by simpa [r, q, t, data] using hsample_n)).trans hc_le have hset : {xstar : Fin n → X | epsilon < |finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (data i))|} ⊆ {xstar : Fin n → X | epsilon / 2 < |finMean (fun i ↦ t (xstar i)) - finMean (fun i ↦ t (data i))|} ∪ {xstar : Fin n → X | epsilon / 2 < |finMean (fun i ↦ q (xstar i)) - finMean (fun i ↦ q (data i))|} := by intro xstar hxstar change epsilon < |finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (data i))| at hxstar rw [finMean_add_tail xstar g t, finMean_add_tail data g t] at hxstar change _ ∨ _ by_contra hnot simp only [Set.mem_setOf_eq] at hnot push_neg at hnot have htri := abs_add_le (finMean (fun i ↦ t (xstar i)) - finMean (fun i ↦ t (data i))) (finMean (fun i ↦ q (xstar i)) - finMean (fun i ↦ q (data i))) rw [show finMean (fun i ↦ t (xstar i)) + finMean (fun i ↦ q (xstar i)) - (finMean (fun i ↦ t (data i)) + finMean (fun i ↦ q (data i))) = (finMean (fun i ↦ t (xstar i)) - finMean (fun i ↦ t (data i))) + (finMean (fun i ↦ q (xstar i)) - finMean (fun i ↦ q (data i))) by ring] at hxstar linarith let _ : IsProbabilityMeasure (bootstrapResample data) := bootstrapResample_isProbabilityMeasure data hn have hmono := measureReal_mono (μ := bootstrapResample data) hset (measure_ne_top (bootstrapResample data) _) have hunion := measureReal_union_le (μ := bootstrapResample data) {xstar : Fin n → X | epsilon / 2 < |finMean (fun i ↦ t (xstar i)) - finMean (fun i ↦ t (data i))|} {xstar : Fin n → X | epsilon / 2 < |finMean (fun i ↦ q (xstar i)) - finMean (fun i ↦ q (data i))|} have hbounded := bootstrapMean_bounded_le data t ht hn |(M : ℝ)| (abs_nonneg _) (fun x ↦ abs_truncation_le_bound g (M : ℝ) x) (epsilon / 2) (by positivity) have htail := bootstrapMean_enveloped_le data q r hr hrnonneg (fun x ↦ le_rfl) hn epsilon hepsilon hdata have hsample_fin : finMean (fun i ↦ r (data i)) < c := by rw [show finMean (fun i ↦ r (data i)) = S.sampleMean r n omega by exact finMean_sampleVector S r n omega] simpa [r, q, t, data] using hsample_n have htailSmall : 4 / epsilon * finMean (fun i ↦ r (data i)) < delta / 4 := by have hc_le : c ≤ delta * epsilon / 16 := min_le_left _ _ have hrs : finMean (fun i ↦ r (data i)) < delta * epsilon / 16 := hsample_fin.trans_le hc_le have heinv : 0 < 4 / epsilon := by positivity calc 4 / epsilon * finMean (fun i ↦ r (data i)) < 4 / epsilon * (delta * epsilon / 16) := mul_lt_mul_of_pos_left hrs heinv _ = delta / 4 := by field_simp; norm_num calc (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < |finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (S.sampleVector n omega i))|} = (bootstrapResample data).real {xstar | epsilon < |finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (data i))|} := rfl _ ≤ (bootstrapResample data).real {xstar | epsilon / 2 < |finMean (fun i ↦ t (xstar i)) - finMean (fun i ↦ t (data i))|} + (bootstrapResample data).real {xstar | epsilon / 2 < |finMean (fun i ↦ q (xstar i)) - finMean (fun i ↦ q (data i))|} := hmono.trans hunion _ ≤ 4 * |(M : ℝ)| ^ 2 / ((n : ℝ) * (epsilon / 2) ^ 2) + 4 / epsilon * finMean (fun i ↦ r (data i)) := add_le_add hbounded htail _ < delta := by linarith

theorem bootstrapMean_sub_populationMean_tendsto_zero_ae (S : IIDSample Omega X mu P) (g : X → ℝ) (hg : Measurable g) (hg_int : Integrable g P) : ∀ᵐ omega ∂mu, ∀ epsilon : ℝ, 0 < epsilon → Tendsto (fun n ↦ (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < |finMean (fun i ↦ g (xstar i)) - ∫ x, g x ∂P|}) atTop (𝓝 0) := by filter_upwards [bootstrapMean_sub_dataMean_tendsto_zero_ae S g hg hg_int, sampleMean_integrable_tendsto_ae S g hg hg_int] with omega hboot hmean intro epsilon hepsilon have hbootHalf := hboot (epsilon / 2) (by positivity) have hmeanHalf : ∀ᶠ n : ℕ in atTop, |S.sampleMean g n omega - ∫ x, g x ∂P| < epsilon / 2 := by simpa [Real.dist_eq] using (Metric.tendsto_atTop.1 hmean (epsilon / 2) (by positivity)) apply tendsto_order.2 constructor · intro a ha filter_upwards with n exact ha.trans_le measureReal_nonneg · intro delta hdelta have hbootSmall : ∀ᶠ n : ℕ in atTop, (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon / 2 < |finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (S.sampleVector n omega i))|} < delta := hbootHalf.eventually (eventually_lt_nhds hdelta) filter_upwards [hmeanHalf, hbootSmall, eventually_ne_atTop 0] with n hmean_n hboot_n hn let _ : IsProbabilityMeasure (bootstrapResample (S.sampleVector n omega)) := bootstrapResample_isProbabilityMeasure _ hn have hset : {xstar : Fin n → X | epsilon < |finMean (fun i ↦ g (xstar i)) - ∫ x, g x ∂P|} ⊆ {xstar : Fin n → X | epsilon / 2 < |finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (S.sampleVector n omega i))|} := by intro xstar hxstar change epsilon < |finMean (fun i ↦ g (xstar i)) - ∫ x, g x ∂P| at hxstar rw [finMean_sampleVector S g n omega] by_contra hnot change ¬ epsilon / 2 < |finMean (fun i ↦ g (xstar i)) - S.sampleMean g n omega| at hnot have htri := abs_sub_le (finMean (fun i ↦ g (xstar i))) (S.sampleMean g n omega) (∫ x, g x ∂P) linarith [le_of_not_gt hnot] exact (measureReal_mono (μ := bootstrapResample (S.sampleVector n omega)) hset (measure_ne_top _ _)).trans_lt hboot_n

theorem bootstrapMeanVec_sub_dataMean_tendsto_zero_ae {d : ℕ} (S : IIDSample Omega X mu P) (g : X → EuclideanSpace ℝ (Fin d)) (hg : Measurable g) (hg_int : Integrable g P) : ∀ᵐ omega ∂mu, ∀ epsilon : ℝ, 0 < epsilon → Tendsto (fun n ↦ (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < ‖finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (S.sampleVector n omega i))‖}) atTop (𝓝 0) := by have hcoord : ∀ᵐ omega ∂mu, ∀ j : Fin d, ∀ epsilon : ℝ, 0 < epsilon → Tendsto (fun n ↦ (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < |finMean (fun i ↦ g (xstar i) j) - finMean (fun i ↦ g (S.sampleVector n omega i) j)|}) atTop (𝓝 0) := by rw [ae_all_iff] intro j exact bootstrapMean_sub_dataMean_tendsto_zero_ae S (fun x ↦ g x j) (by fun_prop) (hg_int.eval_piLp j) filter_upwards [hcoord] with omega homega intro epsilon hepsilon by_cases hd : d = 0 · subst d have hvzero : ∀ n (xstar : Fin n → X), finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (S.sampleVector n omega i)) = 0 := fun n xstar ↦ Subsingleton.elim _ _ simp_rw [hvzero, norm_zero, not_lt_of_ge hepsilon.le] simp · let eta : ℝ := epsilon / d have heta : 0 < eta := by dsimp [eta] positivity have hsum : Tendsto (fun n ↦ ∑ j : Fin d, (bootstrapResample (S.sampleVector n omega)).real {xstar | eta < |finMean (fun i ↦ g (xstar i) j) - finMean (fun i ↦ g (S.sampleVector n omega i) j)|}) atTop (𝓝 0) := by simpa using tendsto_finset_sum univ (fun j hj ↦ homega j eta heta) apply squeeze_zero' · exact Eventually.of_forall fun n ↦ measureReal_nonneg · filter_upwards [eventually_ne_atTop 0] with n hn let data : Fin n → X := S.sampleVector n omega let V : (Fin n → X) → EuclideanSpace ℝ (Fin d) := fun xstar ↦ finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (data i)) have hset : {xstar | epsilon < ‖V xstar‖} ⊆ ⋃ j : Fin d, {xstar | eta < |finMean (fun i ↦ g (xstar i) j) - finMean (fun i ↦ g (data i) j)|} := by have hs := euclidean_norm_event_subset hd V epsilon simpa only [V, eta, finMean_apply, PiLp.sub_apply] using hs let _ : IsProbabilityMeasure (bootstrapResample data) := bootstrapResample_isProbabilityMeasure data hn calc (bootstrapResample (S.sampleVector n omega)).real {xstar | epsilon < ‖finMean (fun i ↦ g (xstar i)) - finMean (fun i ↦ g (S.sampleVector n omega i))‖} = (bootstrapResample data).real {xstar | epsilon < ‖V xstar‖} := rfl _ ≤ (bootstrapResample data).real (⋃ j : Fin d, {xstar | eta < |finMean (fun i ↦ g (xstar i) j) - finMean (fun i ↦ g (data i) j)|}) := measureReal_mono hset (measure_ne_top _ _) _ ≤ ∑ j : Fin d, (bootstrapResample data).real {xstar | eta < |finMean (fun i ↦ g (xstar i) j) - finMean (fun i ↦ g (data i) j)|} := measureReal_iUnion_fintype_le _ · exact hsum