Stat.Bootstrap.Efron­Resampling

theorem bootstrapLaw_isProbabilityMeasure (T : (Fin n → X) → ℝ) (x : Fin n → X) (hn : n ≠ 0) (hT : Measurable T) : IsProbabilityMeasure (bootstrapLaw T x) := by -- Proof plan: install the preceding resample-law instance and apply -- `Measure.isProbabilityMeasure_map hT.aemeasurable`. let _ : IsProbabilityMeasure (bootstrapResample x) := bootstrapResample_isProbabilityMeasure x hn unfold bootstrapLaw exact Measure.isProbabilityMeasure_map hT.aemeasurable

theorem bootstrapResample_eq_average_dirac (x : Fin n → X) : bootstrapResample x = ((n : ℝ≥0∞) ^ n)⁻¹ • ∑ j : Fin n → Fin n, Measure.dirac (x ∘ j) := by -- Proof plan: express one empirical coordinate as the map of the uniform atomic law on -- `Fin n`, commute coordinatewise map with `Measure.pi`, and expand the finite product. -- The empty-index case is `Measure.pi_of_empty`; the successor case distributes the product -- over a finite sum and uses `Measure.map_dirac'`. classical by_cases hn : n = 0 · subst n simp only [bootstrapResample, empiricalMeasure, finiteSampleMeasure, Finset.univ_eq_empty, Finset.sum_empty, smul_zero, Nat.cast_zero, pow_zero, inv_one, one_smul, Fintype.sum_unique] rw [Measure.pi_of_empty _ (x ∘ default)] · let _ : IsProbabilityMeasure (empiricalMeasure x) := empiricalMeasure_isProbabilityMeasure x hn unfold bootstrapResample apply Measure.pi_eq intro s hs rw [Measure.smul_apply, Measure.finsetSum_apply] simp only [Measure.dirac_apply' _ (MeasurableSet.univ_pi hs)] unfold empiricalMeasure finiteSampleMeasure simp_rw [Measure.smul_apply, Measure.finsetSum_apply, Measure.dirac_apply' _ (hs _), smul_eq_mul] rw [ENNReal.ofReal_natCast, Finset.prod_mul_distrib] simp only [Finset.prod_const, Finset.card_univ, Fintype.card_fin, ENNReal.inv_pow] rw [Fintype.prod_sum] congr 1 apply Finset.sum_congr rfl intro j hj by_cases h : x ∘ j ∈ Set.univ.pi s · have hi : ∀ i, x (j i) ∈ s i := by simpa [Set.mem_pi] using h simp [indicator, h, hi] · have hi : ∃ i, x (j i) ∉ s i := by simpa [Set.mem_pi] using h obtain ⟨i, hi⟩ := hi rw [Finset.prod_eq_zero (Finset.mem_univ i)] · exact Set.indicator_of_notMem h (1 : (Fin n → X) → ℝ≥0∞) · exact Set.indicator_of_notMem hi (1 : X → ℝ≥0∞)

theorem variance_empiricalMeasure_eq_empiricalVar (S : IIDSample Ω X μ P) (ψ : X → ℝ) (hψ : Measurable ψ) (n : ℕ) (hn : n ≠ 0) (ω : Ω) : variance ψ (empiricalMeasure (fun i : Fin n ↦ S.Z i ω)) = empiricalVar S ψ n ω := by let _ : IsProbabilityMeasure (empiricalMeasure (fun i : Fin n ↦ S.Z i ω)) := empiricalMeasure_isProbabilityMeasure _ hn rw [ProbabilityTheory.variance_eq_integral hψ.aemeasurable] have hmean : ∫ x, ψ x ∂empiricalMeasure (fun i : Fin n ↦ S.Z i ω) = S.sampleMean ψ n ω := by unfold empiricalMeasure rw [integral_finiteSampleMeasure (fun i : Fin n ↦ S.Z i ω) hψ] rw [sampleMean, Fin.sum_univ_eq_sum_range (fun i ↦ ψ (S.Z i ω)) n] simp only [one_div] rw [hmean] unfold empiricalMeasure rw [integral_finiteSampleMeasure (f := fun x ↦ (ψ x - S.sampleMean ψ n ω) ^ 2) (fun i : Fin n ↦ S.Z i ω) ((hψ.sub measurable_const).pow_const 2)] rw [empiricalVar_eq_centered] rw [Fin.sum_univ_eq_sum_range (fun i ↦ (ψ (S.Z i ω) - S.sampleMean ψ n ω) ^ 2) n] simp only [one_div]

theorem measurable_bootstrapLowerQuantile (T : (Fin n → X) → ℝ) (hT : Measurable T) (hn : n ≠ 0) (β : ℝ) : Measurable (bootstrapLowerQuantile T β) := by -- Proof plan: split into `β ≤ 0`, `0 < β ≤ 1`, and `1 < β`. The outer cases are -- constant by CDF bounds. In the middle case, use `measurable_of_Iic`, rewrite each preimage -- with `bootstrapLowerQuantile_le_iff`, and apply `measurable_bootstrapCDF`. by_cases hβ0 : β ≤ 0 · rw [show bootstrapLowerQuantile T β = fun _ ↦ 0 by funext x unfold bootstrapLowerQuantile rw [show {t : ℝ | β ≤ bootstrapCDF T x t} = univ by ext t simp only [Set.mem_ofPred_eq, Set.mem_univ, iff_true] exact hβ0.trans (ENNReal.toReal_nonneg), Real.sInf_univ]] exact measurable_const · have hβ0' : 0 < β := lt_of_not_ge hβ0 by_cases hβ1 : β ≤ 1 · apply measurable_of_Iic intro t rw [show (bootstrapLowerQuantile T β) ⁻¹' Iic t = {x : Fin n → X | β ≤ bootstrapCDF T x t} by ext x simp only [Set.mem_preimage, Set.mem_Iic, Set.mem_ofPred_eq] exact bootstrapLowerQuantile_le_iff T hT x hn β t hβ0' hβ1] exact measurableSet_le measurable_const (measurable_bootstrapCDF T hT t) · have hβ1' : 1 < β := lt_of_not_ge hβ1 rw [show bootstrapLowerQuantile T β = fun _ ↦ 0 by funext x unfold bootstrapLowerQuantile rw [show {t : ℝ | β ≤ bootstrapCDF T x t} = ∅ by ext t simp only [Set.mem_ofPred_eq, Set.mem_empty_iff_false, iff_false] intro ht let _ : IsProbabilityMeasure (bootstrapLaw T x) := bootstrapLaw_isProbabilityMeasure T x hn hT have hcdf : bootstrapCDF T x t = cdf (bootstrapLaw T x) t := bootstrapCDF_eq_cdf T hT x hn t exact (not_le_of_gt hβ1') (ht.trans (by rw [hcdf] exact ProbabilityTheory.cdf_le_one (bootstrapLaw T x) t)), Real.sInf_empty]] exact measurable_const

theorem integral_centered_finMean_sq_bootstrapResample (x : Fin n → ℝ) (hn : n ≠ 0) : ∫ y, (sqrt n * (finMean y - finMean x)) ^ 2 ∂bootstrapResample x = (n : ℝ)⁻¹ * ∑ i, (x i - finMean x) ^ 2 := by let _ : IsProbabilityMeasure (empiricalMeasure x) := empiricalMeasure_isProbabilityMeasure x hn have hIdSq : Integrable (fun z : ℝ => z ^ 2) (empiricalMeasure x) := by unfold empiricalMeasure finiteSampleMeasure apply Integrable.smul_measure · rw [integrable_finsetSum_measure] intro i hi exact integrable_dirac' (stronglyMeasurable_id.pow 2) (by simp) · simp [hn] have hId : MemLp (fun z : ℝ => z) 2 (empiricalMeasure x) := (memLp_two_iff_integrable_sq measurable_id.aestronglyMeasurable).2 hIdSq have hvar := iid_average_variance (empiricalMeasure x) n (fun z : ℝ => z) hId have hmean : ∫ y, finMean y ∂bootstrapResample x = finMean x := integral_finMean_bootstrapResample x hn have hfin_meas : Measurable (finMean : (Fin n → ℝ) → ℝ) := by unfold finMean fun_prop have hpopmean : ∫ z, z ∂empiricalMeasure x = finMean x := by have h := integral_finiteSampleMeasure x measurable_id simpa only [empiricalMeasure, id_eq, one_div, finMean, smul_eq_mul] using h calc ∫ y, (sqrt n * (finMean y - finMean x)) ^ 2 ∂bootstrapResample x = (n : ℝ) * ∫ y, (finMean y - finMean x) ^ 2 ∂bootstrapResample x := by rw [← integral_const_mul] congr 1 funext y rw [mul_pow, Real.sq_sqrt (Nat.cast_nonneg n)] _ = (n : ℝ) * variance finMean (bootstrapResample x) := by congr 1 rw [ProbabilityTheory.variance_eq_integral hfin_meas.aemeasurable] rw [hmean] _ = variance (fun z : ℝ => z) (empiricalMeasure x) := by rw [show finMean = fun sample : Fin n → ℝ => (n : ℝ)⁻¹ * ∑ i, (fun z : ℝ => z) (sample i) by funext sample simp [finMean]] rw [show bootstrapResample x = Measure.pi (fun _ : Fin n => empiricalMeasure x) by rfl] rw [hvar] field_simp _ = ∫ z, (z - finMean x) ^ 2 ∂empiricalMeasure x := by rw [ProbabilityTheory.variance_eq_integral (X := fun z : ℝ => z) measurable_id.aemeasurable] rw [hpopmean] _ = (n : ℝ)⁻¹ * ∑ i, (x i - finMean x) ^ 2 := by have h := integral_finiteSampleMeasure (f := fun z : ℝ => (z - finMean x) ^ 2) x (by fun_prop) simpa only [empiricalMeasure, one_div] using h