Stat.Quantile.Sample­Quantile­Bahadur

lemma IIDSample.empProcess_increment_tendsto_zero (S : IIDSample Ω ℝ μ P) {τ q₀ f₀ : ℝ} (hreg : SampleQuantileReg P τ q₀ f₀) (u : ℝ) : Tendsto_inProb (fun n ω => S.empProcess n ω (q₀ + u / sqrt (n : ℝ)) - S.empProcess n ω q₀) (fun _ => 0) μ := by classical -- Abbreviations. set yn : ℕ → ℝ := fun n => q₀ + u / sqrt (n : ℝ) with hyn -- `g_n z = 1{z ≤ yn} − 1{z ≤ q₀}`, a fixed (in `ω`) increment of indicators. set g : ℕ → ℝ → ℝ := fun n z => cdfStat (yn n) z - cdfStat q₀ z with hg -- The centered tail probability: `pₙ = |F(yn) − F(q₀)| → 0`. set p : ℕ → ℝ := fun n => |cdf P (yn n) - cdf P q₀| with hp have hp_nonneg : ∀ n, 0 ≤ p n := fun n => abs_nonneg _ -- Each `g n` is bounded, hence in `L²(P)`. have hg_bdd : ∀ n z, |g n z| ≤ 1 := by intro n z have ha := cdfStat_nonneg (yn n) z; have hb := cdfStat_le_one (yn n) z have hc := cdfStat_nonneg q₀ z; have hd := cdfStat_le_one q₀ z rw [hg]; rw [abs_le]; constructor <;> simp only [] <;> linarith have hg_meas : ∀ n, Measurable (g n) := by intro n; exact (measurable_cdfStat (yn n)).sub (measurable_cdfStat q₀) have hg_memLp : ∀ n, MemLp (g n) 2 P := by intro n exact (memLp_top_of_bound (hg_meas n).aestronglyMeasurable 1 (Filter.Eventually.of_forall fun z => by rw [Real.norm_eq_abs]; exact hg_bdd n z)).mono_exponent (by norm_num) -- `∫ g n dP = F(yn) − F(q₀)`. have hg_int : ∀ n, ∫ z, g n z ∂P = cdf P (yn n) - cdf P q₀ := by intro n rw [hg, integral_sub (integrable_cdfStat _) (integrable_cdfStat _), integral_cdfStat, integral_cdfStat] -- `(g n z)² = |g n z|`, hence `∫ (g n)² dP = |F(yn) − F(q₀)| = p n`. have hg_sq_int : ∀ n, ∫ z, (g n z) ^ 2 ∂P = p n := by intro n rcases le_total q₀ (yn n) with hle | hle · -- `g n z ∈ {0, 1}`, so `(g n z)² = g n z`. have hsq : ∀ z, (g n z) ^ 2 = g n z := by intro z have h01 : g n z = 0 ∨ g n z = 1 := by simp only [hg, cdfStat, hyn] by_cases h1 : z ≤ yn n <;> by_cases h2 : z ≤ q₀ <;> simp_all [Set.indicator_of_mem, Set.indicator_of_notMem, Set.mem_Iic] ; linarith rcases h01 with h | h <;> simp [h] have hcong : ∫ z, (g n z) ^ 2 ∂P = ∫ z, g n z ∂P := integral_congr_ae (Filter.Eventually.of_forall hsq) rw [hcong, hg_int, hp] simp only [] rw [abs_of_nonneg (by linarith [monotone_cdf P hle])] · -- `g n z ∈ {0, -1}`, so `(g n z)² = - g n z`. have hsq : ∀ z, (g n z) ^ 2 = - g n z := by intro z have h01 : g n z = 0 ∨ g n z = -1 := by simp only [hg, cdfStat, hyn] by_cases h1 : z ≤ yn n <;> by_cases h2 : z ≤ q₀ <;> simp_all [Set.indicator_of_mem, Set.indicator_of_notMem, Set.mem_Iic] ; linarith rcases h01 with h | h <;> simp [h] have hcong : ∫ z, (g n z) ^ 2 ∂P = ∫ z, - g n z ∂P := integral_congr_ae (Filter.Eventually.of_forall hsq) rw [hcong, integral_neg, hg_int, hp] simp only [] rw [abs_of_nonpos (by linarith [monotone_cdf P hle]), neg_sub] -- `p n → 0` by continuity of the cdf and `yn n → q₀`. have hp_tendsto : Tendsto p atTop (𝓝 0) := by have hsqrt : Tendsto (fun n : ℕ => sqrt (n : ℝ)) atTop atTop := Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop have h0 : Tendsto (fun n : ℕ => u / sqrt (n : ℝ)) atTop (𝓝 0) := hsqrt.const_div_atTop u have hyn_tendsto : Tendsto yn atTop (𝓝 q₀) := by have := (tendsto_const_nhds (x := q₀)).add h0 simpa [hyn] using this have hcont : Tendsto (fun n => cdf P (yn n)) atTop (𝓝 (cdf P q₀)) := (hreg.cont.tendsto q₀).comp hyn_tendsto have hdiff : Tendsto (fun n => cdf P (yn n) - cdf P q₀) atTop (𝓝 0) := by have := hcont.sub (tendsto_const_nhds (x := cdf P q₀)) simpa using this have := (continuous_abs.tendsto (0 : ℝ)).comp hdiff simpa [hp, Function.comp_def] using this -- The increment equals the normalized centered i.i.d. sum. have hincr_eq : ∀ (n : ℕ) (ω : Ω), S.empProcess n ω (yn n) - S.empProcess n ω q₀ = (sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, (g n (S.Z i ω) - ∫ z, g n z ∂P) := by intro n ω have h1 := rescaledEmpiricalCDF_eq_normalizedSum S (yn n) n ω have h2 := rescaledEmpiricalCDF_eq_normalizedSum S q₀ n ω rw [Finset.card_range] at h1 h2 simp only [IIDSample.empProcess] rw [h1, h2, ← mul_sub, ← Finset.sum_sub_distrib] rw [hg_int] congr 1 apply Finset.sum_congr rfl intro i _ simp only [cdfIF, hg] ring -- AE-measurability of the normalized centered sum (for Markov). have hZsum_meas : ∀ (n : ℕ), AEMeasurable (fun ω => (sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, (g n (S.Z i ω) - ∫ z, g n z ∂P)) μ := by intro n refine (const_mul ?_ _).aemeasurable refine measurable_sum _ ?_ intro i _ exact ((hg_meas n).comp (S.meas i)).sub measurable_const -- i.i.d. product law for the first `n` coordinates. have hiid_pi : ∀ (n : ℕ), μ.map (fun ω (i : range n) => S.Z i ω) = Measure.pi (fun _ : range n => P) := by intro n have hiid : iIndepFun (fun i : range n => S.Z i) μ := S.indep.precomp (val_injective (p := fun i => i ∈ range n)) have hmap := (ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map (fun i : range n => (S.meas i).aemeasurable)).mp hiid calc μ.map (fun ω (i : range n) => S.Z i ω) = Measure.pi (fun i : range n => μ.map (S.Z i)) := hmap _ = Measure.pi (fun _ : range n => P) := by congr with i; rw [← (S.identDist i).map_eq, S.law] -- Second-moment bound: `∫⁻ incr² ≤ ofReal (p n)`. have hsecond : ∀ (n : ℕ), ∫⁻ ω, ofReal (((sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, (g n (S.Z i ω) - ∫ z, g n z ∂P)) ^ 2) ∂μ ≤ ofReal (p n) := by intro n rcases Nat.eq_zero_or_pos n with hn | hn · subst hn simp only [cast_zero, Real.sqrt_zero, inv_zero, zero_mul, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, ENNReal.ofReal_zero, lintegral_const, measure_univ, mul_one] exact zero_le · have hbound := iid_centered_sum_sq_lintegral_le (μ := μ) (P := P) (s := range n) (by simpa [Finset.card_range] using hn) (W := S.Z) (fun i _ => S.meas i) (m_A := ⊥) (hm_A_le := bot_le) (hW_indep_A := ProbabilityTheory.indep_bot_left _) (hW_iid_pi := hiid_pi n) (g := fun _ z => g n z) (hg_uncurry_meas := (hg_meas n).comp measurable_snd) (hg_memLp := fun _ => hg_memLp n) simp only [Finset.card_range] at hbound refine hbound.trans ?_ -- `(eLpNorm (g n) 2 P).toReal² = ∫ (g n)² dP = p n`. have heLp : (eLpNorm (g n) 2 P).toReal ^ 2 = p n := by have hpow := (hg_memLp n).eLpNorm_eq_integral_rpow_norm (by norm_num : (2 : ENNReal) ≠ 0) (by norm_num : (2 : ENNReal) ≠ ⊤) rw [hpow] simp only [ENNReal.toReal_ofNat] have hroot_nonneg : 0 ≤ (∫ a, ‖g n a‖ ^ (2 : ℝ) ∂P) ^ (2 : ℝ)⁻¹ := Real.rpow_nonneg (integral_nonneg fun x => by positivity) _ rw [ENNReal.toReal_ofReal hroot_nonneg] have hint_eq : (∫ a, ‖g n a‖ ^ (2 : ℝ) ∂P) = ∫ z, (g n z) ^ 2 ∂P := by congr with x; rw [Real.rpow_two, Real.norm_eq_abs, sq_abs] rw [hint_eq] rw [← Real.rpow_natCast ((∫ z, (g n z) ^ 2 ∂P) ^ (2 : ℝ)⁻¹) 2, ← Real.rpow_mul (integral_nonneg fun z => sq_nonneg _)] rw [show ((2 : ℝ)⁻¹ * (2 : ℕ)) = 1 by norm_num, Real.rpow_one, hg_sq_int n] rw [heLp] rw [lintegral_const] simp [measure_univ] -- Now fix `ε` and run Markov / squeeze. unfold Tendsto_inProb rw [MeasureTheory.tendstoInMeasure_iff_norm] intro ε hε -- Markov on `{ε ≤ ‖incr‖}`. have hmarkov : ∀ (n : ℕ), μ {ω | ε ≤ ‖(S.empProcess n ω (yn n) - S.empProcess n ω q₀) - 0‖} ≤ ofReal (p n) / ofReal (ε ^ 2) := by intro n have hεsq_ne : ofReal (ε ^ 2) ≠ 0 := by rw [ENNReal.ofReal_ne_zero_iff]; positivity have hεsq_top : ofReal (ε ^ 2) ≠ ⊤ := ENNReal.ofReal_ne_top have hsub : {ω | ε ≤ ‖(S.empProcess n ω (yn n) - S.empProcess n ω q₀) - 0‖} ⊆ {ω | ofReal (ε ^ 2) ≤ ofReal (((sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, (g n (S.Z i ω) - ∫ z, g n z ∂P)) ^ 2)} := by intro ω hω simp only [Set.mem_setOf_eq, sub_zero, Real.norm_eq_abs] at hω rw [hincr_eq n ω] at hω apply ENNReal.ofReal_le_ofReal rw [← sq_abs ((sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, (g n (S.Z i ω) - ∫ z, g n z ∂P))] exact pow_le_pow_left₀ hε.le hω 2 calc μ {ω | ε ≤ ‖(S.empProcess n ω (yn n) - S.empProcess n ω q₀) - 0‖} ≤ μ {ω | ofReal (ε ^ 2) ≤ ofReal (((sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, (g n (S.Z i ω) - ∫ z, g n z ∂P)) ^ 2)} := measure_mono hsub _ ≤ (∫⁻ ω, ofReal (((sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, (g n (S.Z i ω) - ∫ z, g n z ∂P)) ^ 2) ∂μ) / ofReal (ε ^ 2) := MeasureTheory.meas_ge_le_lintegral_div ((hZsum_meas n).pow_const 2).ennreal_ofReal hεsq_ne hεsq_top _ ≤ ofReal (p n) / ofReal (ε ^ 2) := by gcongr; exact hsecond n -- Squeeze the Markov bound to `0`. have hrhs_tendsto : Tendsto (fun n => ofReal (p n) / ofReal (ε ^ 2)) atTop (𝓝 0) := by have hp_en : Tendsto (fun n => ofReal (p n)) atTop (𝓝 0) := by rw [show (0 : ENNReal) = ofReal 0 by simp] exact (ENNReal.continuous_ofReal.tendsto 0).comp hp_tendsto have hεsq_ne : ofReal (ε ^ 2) ≠ 0 := by rw [ENNReal.ofReal_ne_zero_iff]; positivity have hc_ne_top : (ofReal (ε ^ 2))⁻¹ ≠ ⊤ := ENNReal.inv_ne_top.mpr hεsq_ne have := ENNReal.Tendsto.mul_const hp_en (inr hc_ne_top) simp only [zero_mul] at this simpa [ENNReal.div_eq_inv_mul, mul_comm] using this exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hrhs_tendsto (fun n => zero_le) (fun n => hmarkov n)

lemma IIDSample.empProcess_cell_sandwich (S : IIDSample Ω ℝ μ P) (n : ℕ) (ω : Ω) {q₀ a b u : ℝ} (hau : a ≤ u) (hub : u ≤ b) : |S.empProcess n ω (q₀ + u / sqrt (n : ℝ)) - S.empProcess n ω q₀| ≤ max |S.empProcess n ω (q₀ + a / sqrt (n : ℝ)) - S.empProcess n ω q₀| |S.empProcess n ω (q₀ + b / sqrt (n : ℝ)) - S.empProcess n ω q₀| + sqrt (n : ℝ) * (cdf P (q₀ + b / sqrt (n : ℝ)) - cdf P (q₀ + a / sqrt (n : ℝ))) := by set s : ℝ := sqrt (n : ℝ) with hs have hs0 : 0 ≤ s := Real.sqrt_nonneg _ set ya : ℝ := q₀ + a / s with hya set yb : ℝ := q₀ + b / s with hyb set yu : ℝ := q₀ + u / s with hyu -- Order of the evaluation points. have hsa : a / s ≤ u / s := by rcases eq_or_lt_of_le hs0 with h | h · simp [← h] · exact div_le_div_of_nonneg_right hau h.le have hsu : u / s ≤ b / s := by rcases eq_or_lt_of_le hs0 with h | h · simp [← h] · exact div_le_div_of_nonneg_right hub h.le have hau' : ya ≤ yu := by rw [hya, hyu]; linarith have hub' : yu ≤ yb := by rw [hyu, hyb]; linarith -- Monotonicities. have hFhat_mono := S.empiricalCDF_monotone n ω have hF_mono := monotone_cdf P -- `empProcess` unfolded: `Gₙ(y) = s·(F̂ₙ(y) − F(y))`. have hGdef : ∀ y, S.empProcess n ω y = s * (S.empiricalCDF y n ω - cdf P y) := by intro y; simp only [IIDSample.empProcess, hs] -- Differenced empirical-cdf monotonicities scaled by `s ≥ 0`. have hFhat_au : s * S.empiricalCDF ya n ω ≤ s * S.empiricalCDF yu n ω := mul_le_mul_of_nonneg_left (hFhat_mono hau') hs0 have hFhat_ub : s * S.empiricalCDF yu n ω ≤ s * S.empiricalCDF yb n ω := mul_le_mul_of_nonneg_left (hFhat_mono hub') hs0 have hF_au : s * cdf P ya ≤ s * cdf P yu := mul_le_mul_of_nonneg_left (hF_mono hau') hs0 have hF_ub : s * cdf P yu ≤ s * cdf P yb := mul_le_mul_of_nonneg_left (hF_mono hub') hs0 -- The deterministic mesh term `D := s·(F(yb) − F(ya)) ≥ 0`. set D : ℝ := s * (cdf P yb - cdf P ya) with hD have hD0 : 0 ≤ D := by rw [hD, mul_sub]; linarith [hF_au, hF_ub] -- Increment abbreviations. set Iu : ℝ := S.empProcess n ω yu - S.empProcess n ω q₀ with hIu set Ia : ℝ := S.empProcess n ω ya - S.empProcess n ω q₀ with hIa set Ib : ℝ := S.empProcess n ω yb - S.empProcess n ω q₀ with hIb -- Upper bound: `Iu ≤ Ib + D`. have hupper : Iu ≤ Ib + D := by rw [hIu, hIb, hD, mul_sub] rw [hGdef yu, hGdef yb, hGdef q₀] have e1 : s * S.empiricalCDF yu n ω ≤ s * S.empiricalCDF yb n ω := hFhat_ub have e2 : s * cdf P ya ≤ s * cdf P yu := hF_au nlinarith [e1, e2] -- Lower bound: `Ia − D ≤ Iu`. have hlower : Ia - D ≤ Iu := by rw [hIu, hIa, hD, mul_sub] rw [hGdef yu, hGdef ya, hGdef q₀] have e1 : s * S.empiricalCDF ya n ω ≤ s * S.empiricalCDF yu n ω := hFhat_au have e2 : s * cdf P yu ≤ s * cdf P yb := hF_ub nlinarith [e1, e2] -- Combine: `|Iu| ≤ max |Ia| |Ib| + D`. have hmaxa : Ia ≤ max |Ia| |Ib| := le_trans (le_abs_self _) (le_max_left _ _) have hmaxb : Ib ≤ max |Ia| |Ib| := le_trans (le_abs_self _) (le_max_right _ _) have hmaxa' : -(max |Ia| |Ib|) ≤ Ia := neg_le.mp (le_trans (neg_le_abs _) (le_max_left _ _)) have hmaxb' : -(max |Ia| |Ib|) ≤ Ib := neg_le.mp (le_trans (neg_le_abs _) (le_max_right _ _)) rw [abs_le] constructor · -- `-(max + D) ≤ Iu`. have : -(max |Ia| |Ib|) - D ≤ Iu := le_trans (by linarith [hmaxa']) hlower linarith · -- `Iu ≤ max + D`. have : Iu ≤ max |Ia| |Ib| + D := le_trans hupper (by linarith [hmaxb]) linarith

lemma IIDSample.empProcess_node_max_tendsto_zero (S : IIDSample Ω ℝ μ P) {τ q₀ f₀ : ℝ} (hreg : SampleQuantileReg P τ q₀ f₀) {ι : Type*} (s : Finset ι) (hs : s.Nonempty) (v : ι → ℝ) : Tendsto_inProb (fun n ω => s.sup' hs (fun i => |S.empProcess n ω (q₀ + v i / sqrt (n : ℝ)) - S.empProcess n ω q₀|)) (fun _ => 0) μ := by classical -- abbreviation for the per-node increment. set Δ : ι → ℕ → Ω → ℝ := fun i n ω => S.empProcess n ω (q₀ + v i / sqrt (n : ℝ)) - S.empProcess n ω q₀ with hΔ -- Each node increment vanishes in probability (L2). have heach : ∀ i ∈ s, Tendsto_inProb (Δ i) (fun _ => 0) μ := fun i _ => S.empProcess_increment_tendsto_zero hreg (v i) unfold Tendsto_inProb rw [MeasureTheory.tendstoInMeasure_iff_norm] intro ε hε -- Each summand tends to 0. have heach' : ∀ i ∈ s, Tendsto (fun n => μ {ω | ε ≤ |Δ i n ω - 0|}) atTop (𝓝 0) := by intro i hi have := (MeasureTheory.tendstoInMeasure_iff_norm.mp (heach i hi)) ε hε simpa [Real.norm_eq_abs] using this -- Finite sum of the per-node tails tends to 0. have hsum : Tendsto (fun n => ∑ i ∈ s, μ {ω | ε ≤ |Δ i n ω - 0|}) atTop (𝓝 0) := by have := tendsto_finset_sum s (fun i hi => heach' i hi) simpa using this -- Set inclusion: `{ε ≤ sup' s |Δ·|} ⊆ ⋃ i∈s {ε ≤ |Δ i|}`, hence ≤ the sum. have hbound : ∀ n, μ {ω | ε ≤ ‖s.sup' hs (fun i => |Δ i n ω|) - 0‖} ≤ ∑ i ∈ s, μ {ω | ε ≤ |Δ i n ω - 0|} := by intro n refine le_trans (measure_mono ?_) (MeasureTheory.measure_biUnion_finset_le s _) intro ω hω simp only [Set.mem_setOf_eq, sub_zero, Real.norm_eq_abs] at hω -- `sup'` of abs values is nonneg, so `|sup'| = sup'`. have hsup_nonneg : 0 ≤ s.sup' hs (fun i => |Δ i n ω|) := by obtain ⟨j, hj⟩ := hs exact le_trans (abs_nonneg _) (Finset.le_sup' (fun i => |Δ i n ω|) hj) rw [abs_of_nonneg hsup_nonneg] at hω -- `sup'` is attained, so some node exceeds `ε`. obtain ⟨i, hi, hival⟩ := Finset.exists_mem_eq_sup' hs (fun i => |Δ i n ω|) simp only [Set.mem_iUnion, Set.mem_setOf_eq, sub_zero, exists_prop] exact ⟨i, hi, by rw [← hival]; exact hω⟩ -- Squeeze. refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hsum (fun n => zero_le) (fun n => hbound n)

lemma exists_grid_bracket {M : ℝ} (hM : 0 < M) {K : ℕ} (hK : 1 ≤ K) {x : ℝ} (hx : -M ≤ x) (hx' : x ≤ M) : ∃ j, j < K ∧ -M + 2 * M * (j : ℝ) / K ≤ x ∧ x ≤ -M + 2 * M * ((j : ℝ) + 1) / K := by have hKpos : (0:ℝ) < K := by exact_mod_cast hK set h : ℝ := 2 * M / K with hh have hhpos : 0 < h := by rw [hh]; positivity set t : ℝ := (x + M) / h with ht have hxeq : x = -M + h * t := by rw [ht, mul_div_cancel₀ _ hhpos.ne']; ring have ht0 : 0 ≤ t := by rw [ht]; apply div_nonneg (by linarith) hhpos.le have htK : t ≤ K := by rw [ht, div_le_iff₀ hhpos, hh]; field_simp; nlinarith have hnode : ∀ r : ℝ, -M + 2 * M * r / K = -M + h * r := by intro r; rw [hh]; ring refine ⟨min (Nat.floor t) (K - 1), ?_, ?_, ?_⟩ · omega · have hjle : ((min (Nat.floor t) (K - 1) : ℕ) : ℝ) ≤ t := by have h1 : (Nat.floor t : ℝ) ≤ t := Nat.floor_le ht0 have h2 : ((min (Nat.floor t) (K - 1) : ℕ) : ℝ) ≤ (Nat.floor t : ℝ) := by exact_mod_cast Nat.min_le_left _ _ linarith rw [hnode, hxeq]; nlinarith [hhpos, hjle] · have htlt : t ≤ ((min (Nat.floor t) (K - 1) : ℕ) : ℝ) + 1 := by have h1 : t < (Nat.floor t : ℝ) + 1 := Nat.lt_floor_add_one t by_cases hc : Nat.floor t ≤ K - 1 · have he : min (Nat.floor t) (K - 1) = Nat.floor t := by omega rw [he]; linarith · have he : min (Nat.floor t) (K - 1) = K - 1 := by omega rw [he] have hKe : ((K - 1 : ℕ) : ℝ) + 1 = (K : ℝ) := by have h1 : 1 ≤ K := hK; push_cast [Nat.cast_sub h1]; ring rw [hKe]; exact htK rw [hnode, hxeq]; nlinarith [hhpos, htlt]

lemma cdf_increment_sqrt_tendsto {P : Measure ℝ} {τ q₀ f₀ : ℝ} (hreg : SampleQuantileReg P τ q₀ f₀) (a : ℝ) : Tendsto (fun n : ℕ => sqrt (n : ℝ) * (cdf P (q₀ + a / sqrt (n : ℝ)) - cdf P q₀)) atTop (𝓝 (f₀ * a)) := by set F : ℝ → ℝ := fun y => cdf P y with hFdef have hxn : Tendsto (fun n : ℕ => q₀ + a / sqrt (n : ℝ)) atTop (𝓝 q₀) := by have hsqrt : Tendsto (fun n : ℕ => sqrt (n : ℝ)) atTop atTop := Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop have h0 : Tendsto (fun n : ℕ => a / sqrt (n : ℝ)) atTop (𝓝 0) := hsqrt.const_div_atTop a simpa using (tendsto_const_nhds (x := q₀)).add h0 rcases eq_or_ne a 0 with ha0 | ha0 · subst ha0; simp · have hxn_ne : ∀ᶠ n : ℕ in atTop, q₀ + a / sqrt (n : ℝ) ≠ q₀ := by filter_upwards [eventually_gt_atTop 0] with n hn have hsq : 0 < sqrt (n : ℝ) := Real.sqrt_pos.mpr (by exact_mod_cast hn) have : a / sqrt (n : ℝ) ≠ 0 := div_ne_zero ha0 hsq.ne' intro h; exact this (by linarith [h]) have hslope : Tendsto (fun n : ℕ => slope F q₀ (q₀ + a / sqrt (n : ℝ))) atTop (𝓝 f₀) := by have htend := (hasDerivAt_iff_tendsto_slope.mp hreg.hasDeriv) exact htend.comp (tendsto_nhdsWithin_iff.mpr ⟨hxn, hxn_ne⟩) have hlim : Tendsto (fun n : ℕ => a * slope F q₀ (q₀ + a / sqrt (n : ℝ))) atTop (𝓝 (a * f₀)) := hslope.const_mul a rw [mul_comm f₀ a] refine hlim.congr' ?_ filter_upwards [eventually_gt_atTop 0] with n hn have hsq : 0 < sqrt (n : ℝ) := Real.sqrt_pos.mpr (by exact_mod_cast hn) have hden : (q₀ + a / sqrt (n : ℝ)) - q₀ = a / sqrt (n : ℝ) := by ring rw [slope_def_field, hden, hFdef] rw [div_div_eq_mul_div] field_simp

lemma Tendsto_inProb.add_zero_zero {Xn Yn : ℕ → Ω → ℝ} (hX : Tendsto_inProb Xn (fun _ => 0) μ) (hY : Tendsto_inProb Yn (fun _ => 0) μ) : Tendsto_inProb (fun n ω => Xn n ω + Yn n ω) (fun _ => 0) μ := by unfold Tendsto_inProb at hX hY ⊢ rw [tendstoInMeasure_iff_norm] at hX hY ⊢ intro ε hε have hX2 := hX (ε / 2) (by linarith) have hY2 := hY (ε / 2) (by linarith) have hsum := hX2.add hY2 rw [add_zero] at hsum refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hsum (fun n => zero_le) (fun n => ?_) refine le_trans (measure_mono ?_) (measure_union_le _ _) intro ω hω simp only [Set.mem_setOf_eq, sub_zero, Real.norm_eq_abs] at hω simp only [Set.mem_union, Set.mem_setOf_eq, sub_zero, Real.norm_eq_abs] by_contra hcon push_neg at hcon obtain ⟨h1, h2⟩ := hcon have : |Xn n ω + Yn n ω| < ε := by calc |Xn n ω + Yn n ω| ≤ |Xn n ω| + |Yn n ω| := abs_add_le _ _ _ < ε / 2 + ε / 2 := add_lt_add h1 h2 _ = ε := by ring exact absurd hω (not_le.mpr this)

lemma Tendsto_inProb.of_isLittleOp_one {Xn : ℕ → Ω → ℝ} (h : IsLittleOp Xn (fun _ => (1 : ℝ)) μ) : Tendsto_inProb Xn (fun _ => 0) μ := by unfold Tendsto_inProb rw [tendstoInMeasure_iff_norm] intro ε hε have h2 := h (ε / 2) (by linarith) simp only [mul_one] at h2 refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h2 (fun n => zero_le) (fun n => ?_) refine measure_mono fun ω hω => ?_ simp only [Set.mem_setOf_eq, sub_zero, Real.norm_eq_abs] at hω ⊢ linarith

lemma IIDSample.sampleQuantile_atom_term_tendsto_zero (S : IIDSample Ω ℝ μ P) {τ q₀ f₀ : ℝ} (hreg : SampleQuantileReg P τ q₀ f₀) : Tendsto_inProb (fun n ω => sqrt (n : ℝ) * (S.empiricalCDF (S.sampleQuantile τ n ω) n ω - τ)) (fun _ => 0) μ := by unfold Tendsto_inProb rw [tendstoInMeasure_iff_norm] intro ε hε -- `1/√n → 0`, so eventually `1/√n < ε`; combine with the a.e. atom bound. have hInvSqrt : Tendsto (fun n : ℕ => (sqrt (n : ℝ))⁻¹) atTop (𝓝 0) := by have hsqrt_atTop : Tendsto (fun n : ℕ => sqrt (n : ℝ)) atTop atTop := Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop exact tendsto_inv_atTop_zero.comp hsqrt_atTop have hev : ∀ᶠ n : ℕ in atTop, (sqrt (n : ℝ))⁻¹ < ε := by have := (Metric.tendsto_nhds.mp hInvSqrt) ε hε filter_upwards [this] with n hn have hnn : 0 ≤ (sqrt (n : ℝ))⁻¹ := by positivity rw [Real.dist_eq, sub_zero, abs_of_nonneg hnn] at hn exact hn -- For `n ≥ 1` with `1/√n < ε`, the measure of the exceptional set is 0. apply Filter.Tendsto.congr' (f₁ := fun _ : ℕ => (0 : ENNReal)) · symm filter_upwards [hev, eventually_ge_atTop 1] with n hnε hn1 have hnpos : 0 < n := hn1 have hnR : 0 < (n : ℝ) := by exact_mod_cast hnpos have hsq : 0 < sqrt (n : ℝ) := Real.sqrt_pos.mpr hnR -- a.e. the empirical-process atom term is ≤ 1/√n < ε. have hatom := S.sampleQuantile_atom_bound hreg.cont hnpos hreg.tau_pos hreg.tau_lt_one have hae : ∀ᵐ ω ∂μ, ‖Real.sqrt (n : ℝ) * (S.empiricalCDF (S.sampleQuantile τ n ω) n ω - τ) - 0‖ < ε := by filter_upwards [hatom] with ω hω simp only [sub_zero, Real.norm_eq_abs] -- `|√n·(F̂ₙ(q̂ₙ)−τ)| = √n·|F̂ₙ(q̂ₙ)−τ| ≤ √n·(1/n) = 1/√n < ε`. have hbound : |sqrt (n : ℝ) * (S.empiricalCDF (S.sampleQuantile τ n ω) n ω - τ)| ≤ (sqrt (n : ℝ))⁻¹ := by rw [abs_mul, abs_of_nonneg hsq.le] calc sqrt (n : ℝ) * |S.empiricalCDF (S.sampleQuantile τ n ω) n ω - τ| ≤ sqrt (n : ℝ) * (n : ℝ)⁻¹ := by exact mul_le_mul_of_nonneg_left hω hsq.le _ = (sqrt (n : ℝ))⁻¹ := by have h := Real.mul_self_sqrt hnR.le; field_simp; nlinarith [h] exact lt_of_le_of_lt hbound hnε -- The bad set is null: it is `{ω | ¬ ‖·‖ < ε}`, which `ae_iff` sends to 0. have hnull : μ {ω | ¬ ‖Real.sqrt (n : ℝ) * (S.empiricalCDF (S.sampleQuantile τ n ω) n ω - τ) - 0‖ < ε} = 0 := ae_iff.mp hae rw [show {ω | ε ≤ ‖Real.sqrt (n : ℝ) * (S.empiricalCDF (S.sampleQuantile τ n ω) n ω - τ) - 0‖} = {ω | ¬ ‖Real.sqrt (n : ℝ) * (S.empiricalCDF (S.sampleQuantile τ n ω) n ω - τ) - 0‖ < ε} from Set.ext fun ω => by simp [not_lt]] exact hnull · exact tendsto_const_nhds

lemma IIDSample.sampleQuantile_taylor_remainder_tendsto_zero (S : IIDSample Ω ℝ μ P) {τ q₀ f₀ : ℝ} (hreg : SampleQuantileReg P τ q₀ f₀) : Tendsto_inProb (fun n ω => sqrt (n : ℝ) * (cdf P (S.sampleQuantile τ n ω) - cdf P q₀ - f₀ * (S.sampleQuantile τ n ω - q₀))) (fun _ => 0) μ := by -- Driver `Un = √n(q̂ₙ − q₀)` is `O_p(1)` (L4). set Un : ℕ → Ω → ℝ := fun n ω => sqrt (n : ℝ) * (S.sampleQuantile τ n ω - q₀) with hUn have hUnBig : IsBigOp Un (fun _ => (1 : ℝ)) μ := S.sampleQuantile_rate hreg -- `(√n)⁻¹ → 0`. have hInvSqrt : Tendsto (fun n : ℕ => (sqrt (n : ℝ))⁻¹) atTop (𝓝 0) := by have hsqrt_atTop : Tendsto (fun n : ℕ => sqrt (n : ℝ)) atTop atTop := Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop exact tendsto_inv_atTop_zero.comp hsqrt_atTop -- `(√n)⁻¹ · Un = q̂ₙ − q₀` (eventually), hence `q̂ₙ →ₚ q₀` (consistency). have hDeltaScaled : IsLittleOp (fun n ω => (sqrt (n : ℝ))⁻¹ * Un n ω) (fun _ => (1 : ℝ)) μ := IsBigOp.const_mul_tendsto_zero hUnBig hInvSqrt have hEqD : ∀ᶠ (n : ℕ) in atTop, (fun ω => (sqrt (n : ℝ))⁻¹ * Un n ω) = (fun ω => S.sampleQuantile τ n ω - q₀) := 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' simp only [hUn] rw [← mul_assoc, inv_mul_cancel₀ hsqrt_ne, one_mul] have hDeltaProb : ∀ ρ : ℝ, 0 < ρ → Tendsto (fun n => μ {ω | ρ < |S.sampleQuantile τ n ω - q₀|}) atTop (𝓝 0) := by intro ρ hρ have h := hDeltaScaled ρ hρ refine h.congr' ?_ filter_upwards [hEqD] with n hn congr 1 ext ω have heq : (sqrt (n : ℝ))⁻¹ * Un n ω = S.sampleQuantile τ n ω - q₀ := congr_fun hn ω simp only [Set.mem_setOf_eq, mul_one] rw [heq] -- Now produce `IsLittleOp (√n·R(q̂ₙ)) 1`, copying `deltaMethod_scalar`'s hRn. apply Tendsto_inProb.of_isLittleOp_one 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 set α : ℝ := δ.toReal / 8 with hα have hαpos : 0 < α := by rw [hα]; linarith rcases hUnBig α hαpos with ⟨M0, hM0⟩ set M : ℝ := max M0 1 with hMdef have hMpos : 0 < M := lt_of_lt_of_le zero_lt_one (le_max_right M0 1) have hM0le : M0 ≤ M := le_max_left M0 1 set A : ℕ → Set Ω := fun n => {ω | M < |Un n ω|} with hAdef set C : ℕ → Set Ω := fun n => {ω | ε < |sqrt (n : ℝ) * (cdf P (S.sampleQuantile τ n ω) - cdf P q₀ - f₀ * (S.sampleQuantile τ n ω - q₀))|} with hCdef have hlimA : limsup (fun n => μ (A n)) atTop ≤ ofReal α := by refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0 intro n refine measure_mono fun ω hω => ?_ simp only [hAdef, Set.mem_setOf_eq, mul_one] at hω ⊢ nlinarith have halpha_two : ofReal α < ofReal (2 * α) := by rw [ENNReal.ofReal_lt_ofReal_iff (by linarith)]; linarith have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimA halpha_two) set η : ℝ := ε / M with hη have hηpos : 0 < η := div_pos hε hMpos -- Derivative little-o, localized near `q₀`. have hderiv_event : ∀ᶠ x in 𝓝 q₀, |cdf P x - cdf P q₀ - f₀ * (x - q₀)| ≤ η * |x - q₀| := by have hderiv_event0 := hreg.hasDeriv.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⟩ set B : ℕ → Set Ω := fun n => {ω | ρ ≤ |S.sampleQuantile τ n ω - q₀|} with hBdef have hDeltaHalf := hDeltaProb (ρ / 2) (by linarith) have hBsmall0 := (ENNReal.tendsto_nhds_zero.mp hDeltaHalf) (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) have hBevent : ∀ᶠ n in atTop, μ (B n) < ofReal (2 * α) := by filter_upwards [hBsmall0] with n hn refine lt_of_le_of_lt (le_trans (measure_mono fun ω hω => ?_) hn) halpha_two simp only [hBdef, Set.mem_setOf_eq] at hω simp only [Set.mem_setOf_eq]; linarith 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 < |Un n ω| := fun hx => hnot (inl hx) have hnotB : ¬ ρ ≤ |S.sampleQuantile τ n ω - q₀| := fun hx => hnot (inr hx) have hUnle : |Un n ω| ≤ M := le_of_not_gt hnotA have hnear : |S.sampleQuantile τ n ω - q₀| < ρ := lt_of_not_ge hnotB have hder := hρprop (by simpa [Real.dist_eq] using hnear) -- `|√n·R(q̂ₙ)| ≤ η·|Un|` from the derivative bound and `Un = √n(q̂ₙ−q₀)`. have hRabs : |sqrt (n : ℝ) * (cdf P (S.sampleQuantile τ n ω) - cdf P q₀ - f₀ * (S.sampleQuantile τ n ω - q₀))| ≤ η * |Un n ω| := by rw [abs_mul, abs_of_nonneg (Real.sqrt_nonneg _)] calc sqrt (n : ℝ) * |cdf P (S.sampleQuantile τ n ω) - cdf P q₀ - f₀ * (S.sampleQuantile τ n ω - q₀)| ≤ sqrt (n : ℝ) * (η * |S.sampleQuantile τ n ω - q₀|) := mul_le_mul_of_nonneg_left hder (Real.sqrt_nonneg _) _ = η * |Un n ω| := by rw [hUn]; simp only rw [abs_mul, abs_of_nonneg (Real.sqrt_nonneg _)]; ring have hRle : |sqrt (n : ℝ) * (cdf P (S.sampleQuantile τ n ω) - cdf P q₀ - f₀ * (S.sampleQuantile τ n ω - q₀))| ≤ ε := calc _ ≤ η * |Un n ω| := hRabs _ ≤ η * M := mul_le_mul_of_nonneg_left hUnle hηpos.le _ = ε := by rw [hη]; field_simp have hωlt : ε < |sqrt (n : ℝ) * (cdf P (S.sampleQuantile τ n ω) - cdf P q₀ - f₀ * (S.sampleQuantile τ n ω - q₀))| := by simpa [hCdef, Set.mem_setOf_eq] using hω exact absurd hRle (not_le.mpr hωlt) exact le_trans (measure_mono hsubset) (measure_union_le (A n) (B n)) have hfour_alpha_lt_delta : ofReal (4 * α) < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal (by positivity) hδtop, hα]; linarith filter_upwards [hAevent, hBevent] with n hAn hBn refine le_of_lt <| calc μ {ω | ε * (fun _ => (1 : ℝ)) n < |sqrt (n : ℝ) * (cdf P (S.sampleQuantile τ n ω) - cdf P q₀ - f₀ * (S.sampleQuantile τ n ω - q₀))|} = μ (C n) := by simp [hCdef] _ ≤ μ (A n) + μ (B n) := hpoint n _ < ofReal (2 * α) + ofReal (2 * α) := ENNReal.add_lt_add hAn hBn _ = ofReal (4 * α) := by rw [← ENNReal.ofReal_add (by linarith) (by linarith)]; congr 1; ring _ < δ := hfour_alpha_lt_delta

lemma IIDSample.normalizedSum_quantileIF_eq (S : IIDSample Ω ℝ μ P) {τ q₀ f₀ : ℝ} (_hf0 : f₀ ≠ 0) (hcdf : cdf P q₀ = τ) (n : ℕ) (ω : Ω) : (sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, quantileIF τ q₀ f₀ (S.Z i ω) = - S.empProcess n ω q₀ / f₀ := by -- `ψ_τ = −cdfIF/f₀` (using `cdf P q₀ = τ`), then the empirical-cdf key identity. have hpt : ∀ z, quantileIF τ q₀ f₀ z = - cdfIF P q₀ z / f₀ := by intro z; unfold quantileIF cdfIF; rw [hcdf]; ring have hemp : S.empProcess n ω q₀ = (sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, cdfIF P q₀ (S.Z i ω) := by have h := rescaledEmpiricalCDF_eq_normalizedSum S q₀ n ω simpa [IIDSample.empProcess, Finset.card_range] using h simp_rw [hpt] rw [hemp, show (∑ i ∈ range n, -cdfIF P q₀ (S.Z i ω) / f₀) = (- ∑ i ∈ range n, cdfIF P q₀ (S.Z i ω)) / f₀ by rw [← Finset.sum_div, Finset.sum_neg_distrib]] ring

lemma Tendsto_inProb.const_mul_zero {Xn : ℕ → Ω → ℝ} (c : ℝ) (h : Tendsto_inProb Xn (fun _ => 0) μ) : Tendsto_inProb (fun n ω => c * Xn n ω) (fun _ => 0) μ := by rcases eq_or_ne c 0 with hc | hc · subst hc unfold Tendsto_inProb rw [tendstoInMeasure_iff_norm] intro ε hε have hempty : ∀ n, {ω : Ω | ε ≤ ‖(0 : ℝ) * Xn n ω - 0‖} = (∅ : Set Ω) := by intro n; ext ω simp only [zero_mul, sub_zero, norm_zero, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_le] exact hε simp_rw [hempty, measure_empty] exact tendsto_const_nhds · unfold Tendsto_inProb at h ⊢ rw [tendstoInMeasure_iff_norm] at h ⊢ intro ε hε have hcpos : 0 < |c| := abs_pos.mpr hc have h' := h (ε / |c|) (div_pos hε hcpos) refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h' (fun _ => zero_le) (fun n => ?_) apply measure_mono intro ω hω simp only [Set.mem_setOf_eq, sub_zero, Real.norm_eq_abs] at hω ⊢ rw [abs_mul] at hω rw [div_le_iff₀ hcpos] calc ε ≤ |c| * |Xn n ω| := hω _ = |Xn n ω| * |c| := mul_comm _ _

lemma IIDSample.measurable_empProcess (S : IIDSample Ω ℝ μ P) (n : ℕ) (y : ℝ) : Measurable (fun ω => S.empProcess n ω y) := by unfold IIDSample.empProcess IIDSample.empiricalCDF IIDSample.sampleMean refine mul measurable_const ?_ refine Measurable.sub (const_mul ?_ _) measurable_const exact measurable_sum _ fun i _ => (measurable_cdfStat y).comp (S.meas i)

lemma IIDSample.empProcess_q0_tendsto_normal (S : IIDSample Ω ℝ μ P) {τ q₀ f₀ : ℝ} (hreg : SampleQuantileReg P τ q₀ f₀) (hmeas : ∀ n : ℕ, AEMeasurable (fun ω => S.empProcess n ω q₀) μ) : Tendsto_dist (fun n ω => S.empProcess n ω q₀) (gaussianMeasure 0 (τ * (1 - τ))) μ hmeas := by -- `rescaledEstimator (F̂ q₀) (F q₀) range n = empProcess(·,q₀)` (card_range). have hθeq : (IsAsymLinear.rescaledEstimator (S.empiricalCDF q₀) (cdf P q₀) (fun m => range m)) = fun n ω => S.empProcess n ω q₀ := by funext n ω simp only [IsAsymLinear.rescaledEstimator, IIDSample.empProcess, Finset.card_range] -- Measurability obligation for the underlying CLT. have hθn_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.rescaledEstimator (S.empiricalCDF q₀) (cdf P q₀) (fun m => range m) n) μ := by intro n; rw [hθeq]; exact (S.measurable_empProcess n q₀).aemeasurable have h := empiricalCDF_tendsto_normal S q₀ hθn_meas -- Rewrite the *goal's* variance `τ → cdf P q₀` (the goal's `hmeas` does not -- mention `cdf`, so this is motive-safe), matching `h`'s limit measure. rw [← hreg.cdf_eq] -- `h : Tendsto_dist (rescaledEstimator …) (gaussianMeasure 0 (F q₀*(1-F q₀))) μ hθn_meas`. unfold Tendsto_dist at h ⊢ -- The two probability-measure sequences agree pointwise (same function). refine h.congr' ?_ filter_upwards with n apply Subtype.ext change μ.map (IsAsymLinear.rescaledEstimator (S.empiricalCDF q₀) (cdf P q₀) (fun m => range m) n) = μ.map (fun ω => S.empProcess n ω q₀) rw [hθeq]

lemma IIDSample.empProcess_q0_bigO (S : IIDSample Ω ℝ μ P) {τ q₀ f₀ : ℝ} (hreg : SampleQuantileReg P τ q₀ f₀) : IsBigOp (fun n ω => S.empProcess n ω q₀) (fun _ => (1 : ℝ)) μ := Tendsto_dist.tightness (fun n => (S.measurable_empProcess n q₀).aemeasurable) (S.empProcess_q0_tendsto_normal hreg _)

theorem Tendsto_dist.limsup_measure_closed_le {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xn : ℕ → Ω → ℝ} {Q : Measure ℝ} [IsProbabilityMeasure Q] (hXn : ∀ n, AEMeasurable (Xn n) μ) (hX : Tendsto_dist Xn Q μ hXn) {F : Set ℝ} (hF : IsClosed F) : limsup (fun n => μ {ω | Xn n ω ∈ F}) atTop ≤ Q F := by unfold Tendsto_dist at hX let μs : ℕ → ProbabilityMeasure ℝ := fun n => ⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩ let ν : ProbabilityMeasure ℝ := ⟨Q, inferInstance⟩ have hpm : limsup (fun n => ((μs n : ProbabilityMeasure ℝ) : Measure ℝ) F) atTop ≤ (ν : Measure ℝ) F := ProbabilityMeasure.limsup_measure_closed_le_of_tendsto (μs := μs) (μ := ν) hX hF refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hpm intro n change μ {ω | Xn n ω ∈ F} ≤ (μ.map (Xn n)) F rw [Measure.map_apply_of_aemeasurable (hXn n) hF.measurableSet] exact le_refl _