Stat.Bootstrap.Efron­Resampling.Mean

theorem bootstrapMeanLaw_eq_iidRowNormalizedSumLaw {n : ℕ} (hn : n ≠ 0) (S : IIDSample Ω X μ P) (ψ : X → ℝ) (hψ : Measurable ψ) (ω : Ω) : bootstrapMeanLaw S ψ hψ n ω = iidRowNormalizedSumLaw (fun m ↦ centeredEmpiricalLaw S ψ m ω) n := by -- Push each empirical draw through subtraction of the fixed sample mean, commute this -- coordinatewise map with `Measure.pi`, and finish with `Measure.map_map` and extensionality. apply ProbabilityMeasure.toMeasure_injective rw [bootstrapMeanLaw_toMeasure hn] change bootstrapLaw (centeredBootstrapSum ψ (S.sampleVector n ω)) (S.sampleVector n ω) = (Measure.pi (fun _ : Fin n => centeredEmpiricalLaw S ψ n ω)).map (fun y => (sqrt (n : ℝ))⁻¹ * iidRowSum n y) rw [centeredEmpiricalLaw, if_neg hn] let g : X → ℝ := fun z => ψ z - S.sampleMean ψ n ω have hg : Measurable g := hψ.sub measurable_const have hemp : empiricalMeasure (fun i : Fin n => g (S.sampleVector n ω i)) = (empiricalMeasure (S.sampleVector n ω)).map g := by unfold empiricalMeasure finiteSampleMeasure rw [Measure.map_smul] rw [Measure.map_finset_sum hg.aemeasurable] simp_rw [Measure.map_dirac' hg] let _ : IsProbabilityMeasure (empiricalMeasure (S.sampleVector n ω)) := empiricalMeasure_isProbabilityMeasure _ hn change ((Measure.pi (fun _ : Fin n => empiricalMeasure (S.sampleVector n ω))).map (centeredBootstrapSum ψ (S.sampleVector n ω))) = (Measure.pi (fun _ : Fin n => empiricalMeasure (fun i : Fin n => g (S.sampleVector n ω i)))).map (fun y => (sqrt (n : ℝ))⁻¹ * iidRowSum n y) rw [hemp] rw [← Measure.pi_map_pi (fun _ => hg.aemeasurable)] have hcoord : Measurable (fun x : Fin n → X => fun i => g (x i)) := by fun_prop have hnorm : Measurable (fun y : Fin n → ℝ => (sqrt (n : ℝ))⁻¹ * iidRowSum n y) := measurable_const.mul (measurable_iidRowSum n) rw [Measure.map_map (μ := Measure.pi (fun _ : Fin n => empiricalMeasure (S.sampleVector n ω))) (g := fun y : Fin n → ℝ => (sqrt (n : ℝ))⁻¹ * iidRowSum n y) (f := fun x : Fin n → X => fun i => g (x i)) hnorm hcoord] congr 1 have hmean : finMean (fun i : Fin n => ψ (S.sampleVector n ω i)) = S.sampleMean ψ n ω := by unfold finMean IIDSample.sampleVector IIDSample.sampleMean rw [smul_eq_mul, Fin.sum_univ_eq_sum_range (fun i ↦ ψ (S.Z i ω)) n] funext y unfold centeredBootstrapSum iidRowSum g simp only [Function.comp_apply] rw [hmean]

theorem centeredEmpiricalSecondMoment_tendsto_ae (S : IIDSample Ω X μ P) (ψ : X → ℝ) (hψ : Measurable ψ) (hψ2 : Integrable (fun x ↦ (ψ x) ^ 2) P) : ∀ᵐ ω ∂μ, Tendsto (fun n ↦ ∫ y, y ^ 2 ∂centeredEmpiricalLaw S ψ n ω) atTop (𝓝 (variance ψ P)) := by filter_upwards [empiricalVar_tendsto_ae S ψ hψ hψ2] with ω hvar apply hvar.congr' filter_upwards [eventually_ne_atTop 0] with n hn exact (integral_sq_centeredEmpiricalLaw_eq_empiricalVar hn S ψ ω).symm

theorem centeredEmpiricalLindeberg_tendsto_ae (S : IIDSample Ω X μ P) (ψ : X → ℝ) (hψ : Measurable ψ) (hψ2 : Integrable (fun x ↦ (ψ x) ^ 2) P) : ∀ᵐ ω ∂μ, ∀ ε : ℝ, 0 < ε → Tendsto (fun n ↦ ∫ y in {y : ℝ | ε * sqrt (n : ℝ) ≤ |y|}, y ^ 2 ∂centeredEmpiricalLaw S ψ n ω) atTop (𝓝 0) := by filter_upwards [sampleMean_tendsto_ae S ψ hψ hψ2, sampleSquaredTail_tendsto_ae S ψ hψ hψ2] with ω hmean htails intro ε hε apply tendsto_order.2 constructor · intro a ha filter_upwards with n exact lt_of_lt_of_le ha (setIntegral_nonneg (measurableSet_le measurable_const measurable_id.abs) (fun _ _ ↦ sq_nonneg _)) · intro δ hδ have htailNat : Tendsto (fun M : ℕ ↦ 4 * ∫ x, squaredTail ψ (M : ℝ) x ∂P) atTop (𝓝 0) := by convert ((integral_squaredTail_tendsto_zero ψ hψ hψ2).const_mul 4).comp (tendsto_natCast_atTop_atTop (R := ℝ)) using 1 <;> simp [Function.comp_def] have hsmallEventually : ∀ᶠ M : ℕ in atTop, 4 * ∫ x, squaredTail ψ (M : ℝ) x ∂P < δ := htailNat.eventually (eventually_lt_nhds hδ) rcases eventually_atTop.1 hsmallEventually with ⟨M, hM⟩ have hMsmall : 4 * ∫ x, squaredTail ψ (M : ℝ) x ∂P < δ := hM M le_rfl have hmeanBound : ∀ᶠ n : ℕ in atTop, |S.sampleMean ψ n ω| < |∫ x, ψ x ∂P| + 1 := hmean.abs.eventually (eventually_lt_nhds (lt_add_one _)) have hroot : Tendsto (fun n : ℕ ↦ ε * sqrt (n : ℝ)) atTop atTop := (Real.tendsto_sqrt_atTop.comp (tendsto_natCast_atTop_atTop (R := ℝ))).const_mul_atTop hε have hthreshold : ∀ᶠ n : ℕ in atTop, 2 * ((M : ℝ) + (|∫ x, ψ x ∂P| + 1)) ≤ ε * sqrt (n : ℝ) := hroot.eventually (eventually_ge_atTop _) have htailSmall : ∀ᶠ n : ℕ in atTop, 4 * S.sampleMean (squaredTail ψ M) n ω < δ := (htails M).const_mul 4 |>.eventually (eventually_lt_nhds hMsmall) filter_upwards [hmeanBound, hthreshold, htailSmall, eventually_ne_atTop 0] with n hnmean hnthreshold hntail hn have hthreshold' : 2 * ((M : ℝ) + |S.sampleMean ψ n ω|) ≤ ε * sqrt (n : ℝ) := by linarith have hdom : (∫ y in {y : ℝ | ε * sqrt (n : ℝ) ≤ |y|}, y ^ 2 ∂centeredEmpiricalLaw S ψ n ω) ≤ 4 * S.sampleMean (squaredTail ψ M) n ω := by have hA : MeasurableSet {y : ℝ | ε * sqrt (n : ℝ) ≤ |y|} := by exact measurableSet_le measurable_const measurable_id.abs rw [setIntegral_sq_centeredEmpiricalLaw_eq_average hn S ψ ω (A := {y : ℝ | ε * sqrt (n : ℝ) ≤ |y|}) hA] unfold IIDSample.sampleMean rw [← Fin.sum_univ_eq_sum_range (fun i ↦ squaredTail ψ M (S.Z i ω)) n] calc (n : ℝ)⁻¹ * ∑ i : Fin n, indicator {y : ℝ | ε * sqrt (n : ℝ) ≤ |y|} (fun y : ℝ ↦ y ^ 2) (ψ (S.Z i ω) - S.sampleMean ψ n ω) ≤ (n : ℝ)⁻¹ * ∑ i : Fin n, 4 * squaredTail ψ M (S.Z i ω) := by apply mul_le_mul_of_nonneg_left (Finset.sum_le_sum fun i _ ↦ ?_) (by positivity) let x := ψ (S.Z i ω) let m := S.sampleMean ψ n ω by_cases hc : ε * sqrt (n : ℝ) ≤ |x - m| · have hbig : 2 * ((M : ℝ) + |m|) ≤ |x - m| := hthreshold'.trans hc have htri : |x - m| ≤ |x| + |m| := abs_sub x m have haux : 2 * ((M : ℝ) + |m|) ≤ |x| + |m| := hbig.trans htri have hm_le : |m| ≤ |x| := by have hMnonneg : 0 ≤ (M : ℝ) := Nat.cast_nonneg M linarith [abs_nonneg m] have hM_le : (M : ℝ) ≤ |x| := by have hMnonneg : 0 ≤ (M : ℝ) := Nat.cast_nonneg M linarith [abs_nonneg m] have habs : |x - m| ≤ 2 * |x| := by linarith have hsquares : (x - m) ^ 2 ≤ 4 * x ^ 2 := by have hs := (sq_le_sq₀ (abs_nonneg (x - m)) (by positivity : 0 ≤ 2 * |x|)).2 habs rw [sq_abs] at hs nlinarith [sq_abs x] simpa [x, m, squaredTail, hc, hM_le] using hsquares · by_cases ht : (M : ℝ) ≤ |x| · simp [x, m, squaredTail, hc, ht, sq_nonneg] · simp [x, m, squaredTail, hc, ht] _ = 4 * ((n : ℝ)⁻¹ * ∑ i : Fin n, squaredTail ψ M (S.Z i ω)) := by rw [← Finset.mul_sum] ring exact lt_of_le_of_lt hdom hntail

theorem bootstrapMeanLaw_tendsto_gaussian_ae (S : IIDSample Ω X μ P) (ψ : X → ℝ) (hψ : Measurable ψ) (hψ2 : Integrable (fun x ↦ (ψ x) ^ 2) P) : ∀ᵐ ω ∂μ, Tendsto (fun n ↦ bootstrapMeanLaw S ψ hψ n ω) atTop (𝓝 (⟨gaussianReal 0 (populationVariance ψ P), inferInstance⟩ : ProbabilityMeasure ℝ)) := by letI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable filter_upwards [centeredEmpiricalSecondMoment_tendsto_ae S ψ hψ hψ2, centeredEmpiricalLindeberg_tendsto_ae S ψ hψ hψ2] with ω hsecond hlindeberg have hcenter : ∀ n, ∫ x, x ∂centeredEmpiricalLaw S ψ n ω = 0 := by intro n by_cases hn : n = 0 · subst n simp [centeredEmpiricalLaw] · exact integral_id_centeredEmpiricalLaw hn S ψ ω have hsecond' : Tendsto (fun n : ℕ ↦ ∫ x, x ^ 2 ∂centeredEmpiricalLaw S ψ n ω) atTop (𝓝 ((populationVariance ψ P : NNReal) : ℝ)) := by simpa [populationVariance, Real.toNNReal_of_nonneg (variance_nonneg ψ P)] using hsecond have hrow := iidRowNormalizedSumLaw_tendsto_gaussian (fun n ↦ centeredEmpiricalLaw S ψ n ω) (populationVariance ψ P) (fun n ↦ memLp_id_centeredEmpiricalLaw S ψ n ω) hcenter hsecond' hlindeberg apply hrow.congr' filter_upwards [eventually_ne_atTop 0] with n hn exact (bootstrapMeanLaw_eq_iidRowNormalizedSumLaw hn S ψ hψ ω).symm

theorem bootstrapMeanLaw_cdfKolmogorov_samplingMeanLaw_tendsto_ae (S : IIDSample Ω X μ P) (ψ : X → ℝ) (hψ : Measurable ψ) (hψ2 : Integrable (fun x ↦ (ψ x) ^ 2) P) (hvar : 0 < variance ψ P) : ∀ᵐ ω ∂μ, Tendsto (fun n ↦ cdfKolmogorov (bootstrapMeanLaw S ψ hψ n ω) (samplingMeanLaw S ψ hψ n)) atTop (𝓝 0) := by have hvar' : 0 < populationVariance ψ P := by simpa [populationVariance, Real.toNNReal_pos] using hvar filter_upwards [bootstrapMeanLaw_tendsto_gaussian_ae S ψ hψ hψ2] with ω hboot exact tendsto_cdfKolmogorov_of_tendsto hboot (samplingMeanLaw_tendsto_gaussian S ψ hψ hψ2) (continuous_cdf_gaussianReal_zero hvar')