Stat.Quantile

lemma cdfIF_variance [IsProbabilityMeasure P] (y : ℝ) : ∫ z, (cdfIF P y z) ^ 2 ∂P = cdf P y * (1 - cdf P y) := by have hstat_int : Integrable (cdfStat y) P := integrable_cdfStat y -- `(1{·} − F)² = 1{·} − 2F·1{·} + F²` via idempotence of the indicator. have hexpand : (fun z => (cdfIF P y z) ^ 2) = (fun z => cdfStat y z - 2 * cdf P y * cdfStat y z + (cdf P y) ^ 2) := by funext z simp only [cdfIF] rw [show (cdfStat y z - cdf P y) ^ 2 = (cdfStat y z) ^ 2 - 2 * cdf P y * cdfStat y z + (cdf P y) ^ 2 from by ring, cdfStat_sq y z] have h1 : Integrable (fun z => cdfStat y z - 2 * cdf P y * cdfStat y z) P := hstat_int.sub (hstat_int.const_mul (2 * cdf P y)) rw [hexpand, integral_add h1 (integrable_const _), integral_sub hstat_int (hstat_int.const_mul (2 * cdf P y)), integral_const_mul] simp only [integral_cdfStat, integral_const, probReal_univ, one_smul] ring

lemma empiricalCDF_isAsymLinear (S : IIDSample Ω ℝ μ P) (y : ℝ) : IsAsymLinear (S.empiricalCDF y) (cdf P y) (cdfIF P y) S (fun m => range m) where mean_zero := cdfIF_mean_zero y finite_var := cdfIF_sq_integrable y remainder := by have hzero : (fun n (ω : Ω) => sqrt ((range n).card : ℝ) * (S.empiricalCDF y n ω - cdf P y) - (sqrt ((range n).card : ℝ))⁻¹ * ∑ i ∈ range n, cdfIF P y (S.Z i ω)) = (fun _ _ => (0 : ℝ)) := by funext n ω; rw [rescaledEmpiricalCDF_eq_normalizedSum S y n ω, sub_self] simpa only [hzero] using (isLittleOp_zero : IsLittleOp (fun _ (_ : Ω) => (0 : ℝ)) (fun _ => (1 : ℝ)) μ)

theorem empiricalCDF_tendsto_normal (S : IIDSample Ω ℝ μ P) (y : ℝ) (hθn_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.rescaledEstimator (S.empiricalCDF y) (cdf P y) (fun m => range m) n) μ) : Tendsto_dist (IsAsymLinear.rescaledEstimator (S.empiricalCDF y) (cdf P y) (fun m => range m)) (gaussianMeasure 0 (cdf P y * (1 - cdf P y))) μ hθn_meas := by have h := (empiricalCDF_isAsymLinear S y).tendsto_normal (measurable_cdfIF y) hθn_meas rwa [cdfIF_variance] at h

theorem empiricalCDF_tendsto_inProb (S : IIDSample Ω ℝ μ P) (y : ℝ) : Tendsto_inProb (S.empiricalCDF y) (fun _ => cdf P y) μ := by have h := S.sampleMean_tendsto_inProb (measurable_cdfStat y) (integrable_cdfStat y) rw [integral_cdfStat] at h exact h

lemma quantileIF_variance [IsProbabilityMeasure P] {τ q₀ f₀ : ℝ} (hcdf : cdf P q₀ = τ) : ∫ z, (quantileIF τ q₀ f₀ z) ^ 2 ∂P = τ * (1 - τ) / f₀ ^ 2 := by have hstat : Integrable (cdfStat q₀) P := integrable_cdfStat q₀ have hexpand : (fun z => (quantileIF τ q₀ f₀ z) ^ 2) = (fun z => (τ ^ 2 - 2 * τ * cdfStat q₀ z + cdfStat q₀ z) / f₀ ^ 2) := by funext z unfold quantileIF rw [div_pow] congr 1 rw [show (τ - cdfStat q₀ z) ^ 2 = τ ^ 2 - 2 * τ * cdfStat q₀ z + (cdfStat q₀ z) ^ 2 from by ring, cdfStat_sq] rw [hexpand, integral_div] have h1 : Integrable (fun z => τ ^ 2 - 2 * τ * cdfStat q₀ z) P := (integrable_const (τ ^ 2)).sub (hstat.const_mul (2 * τ)) have hinner : ∫ z, (τ ^ 2 - 2 * τ * cdfStat q₀ z + cdfStat q₀ z) ∂P = τ - τ ^ 2 := by rw [integral_add h1 hstat, integral_sub (integrable_const _) (hstat.const_mul (2 * τ)), integral_const_mul] simp only [integral_cdfStat, integral_const, probReal_univ, one_smul] rw [hcdf]; ring rw [hinner]; congr 1; ring

lemma QuantileRegularity.isAsymLinear {S : IIDSample Ω ℝ μ P} {qn : ℕ → Ω → ℝ} {τ q₀ f₀ : ℝ} (h : QuantileRegularity S qn τ q₀ f₀) : IsAsymLinear qn q₀ (quantileIF τ q₀ f₀) S (fun m => range m) where mean_zero := quantileIF_mean_zero h.cdf_eq finite_var := quantileIF_sq_integrable remainder := h.bahadur

theorem QuantileRegularity.tendsto_normal {S : IIDSample Ω ℝ μ P} {qn : ℕ → Ω → ℝ} {τ q₀ f₀ : ℝ} (h : QuantileRegularity S qn τ q₀ f₀) (hθn_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.rescaledEstimator qn q₀ (fun m => range m) n) μ) (_hSum_meas : ∀ n : ℕ, AEMeasurable (IsAsymLinear.normalizedSum S (quantileIF τ q₀ f₀) (fun m => range m) n) μ) : Tendsto_dist (IsAsymLinear.rescaledEstimator qn q₀ (fun m => range m)) (gaussianMeasure 0 (τ * (1 - τ) / f₀ ^ 2)) μ hθn_meas := by have hAL := h.isAsymLinear.tendsto_normal (measurable_quantileIF τ q₀ f₀) hθn_meas rwa [quantileIF_variance h.cdf_eq] at hAL

lemma IIDSample.empiricalMeasure_cdf (S : IIDSample Ω ℝ μ P) {n : ℕ} (hn : 0 < n) (ω : Ω) (y : ℝ) : cdf (S.empiricalMeasure n ω) y = S.empiricalCDF y n ω := by haveI := S.empiricalMeasure_isProbabilityMeasure hn ω rw [cdf_eq_real, S.empiricalMeasure_real_Iic hn ω y]

lemma IIDSample.sampleQuantile_le_iff (S : IIDSample Ω ℝ μ P) {n : ℕ} (hn : 0 < n) (ω : Ω) {τ : ℝ} (hτ0 : 0 < τ) (hτ1 : τ < 1) (x : ℝ) : S.sampleQuantile τ n ω ≤ x ↔ τ ≤ S.empiricalCDF x n ω := by haveI := S.empiricalMeasure_isProbabilityMeasure hn ω rw [IIDSample.sampleQuantile, quantile_le_iff hτ0 hτ1, S.empiricalMeasure_cdf hn ω]

lemma IIDSample.sampleQuantile_atom_bound [IsProbabilityMeasure μ] (S : IIDSample Ω ℝ μ P) (hcont : Continuous (fun y => cdf P y)) {n : ℕ} (hn : 0 < n) {τ : ℝ} (hτ0 : 0 < τ) (hτ1 : τ < 1) : ∀ᵐ ω ∂μ, |S.empiricalCDF (S.sampleQuantile τ n ω) n ω - τ| ≤ (n : ℝ)⁻¹ := by -- `P` is atomless: `Continuous (cdf P)` ⇒ no jumps ⇒ every singleton is null. haveI hP : IsProbabilityMeasure P := by rw [← S.law] exact isProbabilityMeasure_map (S.meas 0).aemeasurable haveI hPna : NullSingletonClass P := by refine ⟨fun x => ?_⟩ have heq : P = (cdf P).measure := (measure_cdf P).symm rw [heq, StieltjesFunction.measure_singleton, ContinuousWithinAt.leftLim_eq (hcont.continuousWithinAt), sub_self, ENNReal.ofReal_zero] -- Each coordinate has law `P`. have hlaw : ∀ i : ℕ, μ.map (S.Z i) = P := fun i => (S.identDist i).map_eq.symm.trans S.law -- Pairwise a.s. distinctness: `μ{Zᵢ = Zⱼ} = 0` for `i ≠ j` (independence + atomless law). have hpair : ∀ i j : ℕ, i ≠ j → μ {ω | S.Z i ω = S.Z j ω} = 0 := by intro i j hij have hind : IndepFun (S.Z i) (S.Z j) μ := S.indep.indepFun hij have hmeas : MeasurableSet {p : ℝ × ℝ | p.1 = p.2} := measurableSet_eq_fun measurable_fst measurable_snd have hpre : {ω | S.Z i ω = S.Z j ω} = (fun ω => (S.Z i ω, S.Z j ω)) ⁻¹' {p : ℝ × ℝ | p.1 = p.2} := rfl rw [hpre, ← Measure.map_apply ((S.meas i).prodMk (S.meas j)) hmeas, (indepFun_iff_map_prod_eq_prod_map_map (S.meas i).aemeasurable (S.meas j).aemeasurable).mp hind, hlaw i, hlaw j, Measure.measure_prod_null hmeas] refine Filter.Eventually.of_forall (fun x => ?_) have hsing : (Prod.mk x ⁻¹' {p : ℝ × ℝ | p.1 = p.2}) = {x} := by ext y; simp [eq_comm] simp [hsing, measure_singleton] -- Assemble into one a.s. tie-free event on `range n`. have hae : ∀ᵐ ω ∂μ, ∀ i ∈ (Finset.range n : Set ℕ), ∀ j ∈ (Finset.range n : Set ℕ), i ≠ j → S.Z i ω ≠ S.Z j ω := by rw [ae_ball_iff (Set.to_countable _)] intro i _ rw [ae_ball_iff (Set.to_countable _)] intro j _ by_cases hij : i = j · exact ae_of_all _ (fun ω hne => absurd hij hne) · rw [ae_iff] have heqset : {ω | ¬ (i ≠ j → S.Z i ω ≠ S.Z j ω)} = {ω | S.Z i ω = S.Z j ω} := by ext ω; simp [hij] rw [heqset, hpair i j hij] -- The empirical-cdf sum counts the sample points below the threshold. have hcard : ∀ (x : ℝ) (ω : Ω), ∑ i ∈ Finset.range n, cdfStat x (S.Z i ω) = (((Finset.range n).filter (fun i => S.Z i ω ≤ x)).card : ℝ) := by intro x ω rw [Finset.card_filter] push_cast refine Finset.sum_congr rfl (fun i _ => ?_) unfold cdfStat by_cases h : S.Z i ω ≤ x · rw [Set.indicator_of_mem (Set.mem_Iic.mpr h)]; simp [h] · rw [Set.indicator_of_notMem (by simpa using h)]; simp [h] have hnR : (0 : ℝ) < (n : ℝ) := by exact_mod_cast hn filter_upwards [hae] with ω haeω set q := S.sampleQuantile τ n ω with hq -- LOWER bound `τ ≤ F̂ₙ(q)` is deterministic (switching at `x = q`, reflexivity). have hlower : τ ≤ S.empiricalCDF q n ω := (S.sampleQuantile_le_iff hn ω hτ0 hτ1 q).mp (le_refl q) -- Strict switching: any `x < q` has `F̂ₙ(x) < τ`. have hstrict : ∀ x : ℝ, x < q → S.empiricalCDF x n ω < τ := by intro x hx by_contra hcon push_neg at hcon exact absurd ((S.sampleQuantile_le_iff hn ω hτ0 hτ1 x).mpr hcon) (not_le.mpr hx) -- Abbreviations for the three counts. set Cle : ℝ → Finset ℕ := fun x => (Finset.range n).filter (fun i => S.Z i ω ≤ x) with hCle set Clt : Finset ℕ := (Finset.range n).filter (fun i => S.Z i ω < q) with hClt set Ceq : Finset ℕ := (Finset.range n).filter (fun i => S.Z i ω = q) with hCeq -- `F̂ₙ(x) = (Cle x).card / n`. have hFcard : ∀ x : ℝ, S.empiricalCDF x n ω = (n : ℝ)⁻¹ * ((Cle x).card : ℝ) := by intro x rw [IIDSample.empiricalCDF, IIDSample.sampleMean, hcard x ω] -- `Cle q = Clt ∪ Ceq`, disjointly: `Zᵢ ≤ q ↔ Zᵢ < q ∨ Zᵢ = q`. have hdisj : Disjoint Clt Ceq := by rw [hClt, hCeq, Finset.disjoint_filter] intro i _ hlt heq; exact absurd heq (ne_of_lt hlt) have hunion : Cle q = Clt ∪ Ceq := by rw [hCle, hClt, hCeq, ← Finset.filter_or] refine filter_congr (fun i _ => ?_) exact ⟨fun h => h.lt_or_eq, fun h => h.elim le_of_lt le_of_eq⟩ have hcountsplit : (Cle q).card = Clt.card + Ceq.card := by rw [hunion, Finset.card_union_of_disjoint hdisj] -- Tie-free ⇒ at most one index equals `q`. have hCeq_le : Ceq.card ≤ 1 := by rw [Finset.card_le_one] intro a ha b hb rw [hCeq, mem_filter] at ha hb by_contra hab exact haeω a (by simpa using ha.1) b (by simpa using hb.1) hab (ha.2.trans hb.2.symm) -- Strict part: `(Clt.card : ℝ) ≤ n·τ`, via a threshold `x < q` with `Cle x = Clt`. have hClt_le : (Clt.card : ℝ) ≤ (n : ℝ) * τ := by rcases Finset.eq_empty_or_nonempty Clt with hempty | hne · rw [hempty, Finset.card_empty, cast_zero]; positivity · -- `m = max{Zᵢ : Zᵢ < q}`; choose threshold `x = m < q`, then `Cle m = Clt`. set T : Finset ℝ := Clt.image (fun i => S.Z i ω) with hT have hTne : T.Nonempty := hne.image _ set m : ℝ := T.max' hTne with hm have hmlt : m < q := by obtain ⟨a, haT, ham⟩ := Finset.mem_image.mp (T.max'_mem hTne) rw [hClt, mem_filter] at haT rw [hm, ← ham]; exact haT.2 have hCleq : Cle m = Clt := by rw [hCle, hClt] refine filter_congr (fun i hi => ?_) constructor · intro hle; exact lt_of_le_of_lt hle hmlt · intro hlt refine Finset.le_max' T _ ?_ rw [hT] exact Finset.mem_image.mpr ⟨i, by rw [hClt, mem_filter]; exact ⟨hi, hlt⟩, rfl⟩ have hlt2 : S.empiricalCDF m n ω < τ := hstrict m hmlt rw [hFcard m, hCleq] at hlt2 -- `(n)⁻¹ * card < τ` ⟹ `card < n·τ`. have hkey := (inv_mul_lt_iff₀ hnR).mp hlt2 linarith [hkey] -- Combine: `n·F̂ₙ(q) = (Cle q).card ≤ n·τ + 1`, so `F̂ₙ(q) ≤ τ + 1/n`. have hupper : S.empiricalCDF q n ω ≤ τ + (n : ℝ)⁻¹ := by rw [hFcard q, hcountsplit] push_cast rw [mul_add] have h1 : (n : ℝ)⁻¹ * (Clt.card : ℝ) ≤ τ := by rw [inv_mul_le_iff₀ hnR]; linarith [hClt_le] have h2 : (n : ℝ)⁻¹ * (Ceq.card : ℝ) ≤ (n : ℝ)⁻¹ := by have : (Ceq.card : ℝ) ≤ 1 := by exact_mod_cast hCeq_le nlinarith [inv_nonneg.mpr hnR.le, this] linarith rw [abs_le] exact ⟨by linarith [inv_nonneg.mpr hnR.le], by linarith⟩

lemma quantileIF_cross [IsProbabilityMeasure P] {τj qj fj τl ql fl : ℝ} (hj : cdf P qj = τj) (hl : cdf P ql = τl) : ∫ z, quantileIF τj qj fj z * quantileIF τl ql fl z ∂P = (min τj τl - τj * τl) / (fj * fl) := by -- Product of two lower-ray indicators is the indicator of the smaller ray. have hprod : ∀ z, cdfStat qj z * cdfStat ql z = cdfStat (min qj ql) z := by intro z simp only [cdfStat, Set.indicator_apply, Set.mem_Iic, le_min_iff] by_cases hzj : z ≤ qj <;> by_cases hzl : z ≤ ql <;> simp [hzj, hzl] -- The cdf of the min equals the min of the cdfs (by monotonicity). have hmin : cdf P (min qj ql) = min τj τl := by rcases le_total qj ql with hq | hq · rw [min_eq_left hq, hj, min_eq_left] rw [← hj, ← hl]; exact monotone_cdf P hq · rw [min_eq_right hq, hl, min_eq_right] rw [← hj, ← hl]; exact monotone_cdf P hq -- Expand the product of influence functions. have hexpand : (fun z => quantileIF τj qj fj z * quantileIF τl ql fl z) = (fun z => (τj * τl - τj * cdfStat ql z - τl * cdfStat qj z + cdfStat (min qj ql) z) / (fj * fl)) := by funext z unfold quantileIF rw [div_mul_div_comm, ← hprod z]; ring rw [hexpand] have hil : Integrable (cdfStat ql) P := integrable_cdfStat ql have hij : Integrable (cdfStat qj) P := integrable_cdfStat qj have him : Integrable (cdfStat (min qj ql)) P := integrable_cdfStat (min qj ql) rw [integral_div] have e1 : ∫ z, (τj * τl - τj * cdfStat ql z - τl * cdfStat qj z + cdfStat (min qj ql) z) ∂P = τj * τl - τj * cdf P ql - τl * cdf P qj + cdf P (min qj ql) := by have hB : Integrable (fun z => τj * τl - τj * cdfStat ql z) P := (integrable_const (τj * τl)).sub (hil.const_mul τj) have hC : Integrable (fun z => τl * cdfStat qj z) P := hij.const_mul τl have hA : Integrable (fun z => τj * τl - τj * cdfStat ql z - τl * cdfStat qj z) P := hB.sub hC rw [integral_add hA him, integral_sub hB hC, integral_sub (integrable_const (τj * τl)) (hil.const_mul τj)] simp only [integral_const, probReal_univ, one_smul, integral_const_mul, integral_cdfStat] rw [e1, hl, hj, hmin] ring

theorem IIDSample.sampleQuantileVec_isAsymLinearVec (S : IIDSample Ω ℝ μ P) {τ q f : Fin k → ℝ} (hreg : ∀ j, SampleQuantileReg P (τ j) (q j) (f j)) : IsAsymLinearVec (S.sampleQuantileVec τ) (eucl q) (quantileIFVec τ q f) S (fun m => range m) := by -- Per-coordinate scalar asymptotic linearity. set AL : ∀ j, IsAsymLinear (S.sampleQuantile (τ j)) (q j) (quantileIF (τ j) (q j) (f j)) S (fun m => range m) := fun j => S.sampleQuantile_isAsymLinear (hreg j) with hAL -- The coordinate influence functions, packaged as `g x = (fun j => quantileIF…)`. set g : ℝ → Fin k → ℝ := fun x j => quantileIF (τ j) (q j) (f j) x with hg -- Coordinatewise bound used throughout. have hcoordbound : ∀ x j, |g x j| ≤ (|τ j| + 1) / |f j| := by intro x j have hc0 : 0 ≤ cdfStat (q j) x := cdfStat_nonneg (q j) x have hc1 : cdfStat (q j) x ≤ 1 := cdfStat_le_one (q j) x have hnum : |τ j - cdfStat (q j) x| ≤ |τ j| + 1 := by rw [abs_le] exact ⟨by have := neg_abs_le (τ j); linarith, by have := le_abs_self (τ j); linarith⟩ change |quantileIF (τ j) (q j) (f j) x| ≤ _ unfold quantileIF rw [abs_div, div_eq_mul_inv, div_eq_mul_inv] exact mul_le_mul_of_nonneg_right hnum (inv_nonneg.mpr (abs_nonneg _)) have hg_int : Integrable g P := by -- bounded by a constant (sup-norm ≤ sum of coordinate bounds) on a prob. measure refine (integrable_const (∑ j, (|τ j| + 1) / |f j|)).mono' (measurable_pi_lambda _ (fun j => measurable_quantileIF (τ j) (q j) (f j))).aestronglyMeasurable ?_ filter_upwards with x refine (pi_norm_le_iff_of_nonneg (sum_nonneg fun j _ => div_nonneg (by positivity) (abs_nonneg _))).2 (fun j => ?_) rw [Real.norm_eq_abs] exact (hcoordbound x j).trans (Finset.single_le_sum (f := fun j => (|τ j| + 1) / |f j|) (fun i _ => div_nonneg (by positivity) (abs_nonneg _)) (Finset.mem_univ j)) refine ⟨?_, ?_, ?_⟩ · -- mean_zero : ∫ quantileIFVec = 0 change ∫ x, eucl (g x) ∂P = 0 rw [ContinuousLinearEquiv.integral_comp_comm (EuclideanSpace.equiv (Fin k) ℝ).symm g] have hzero : (∫ x, g x ∂P) = 0 := by funext j have hproj := ContinuousLinearMap.integral_comp_comm (ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : Fin k => ℝ) j) hg_int simp only [ContinuousLinearMap.proj_apply] at hproj rw [← hproj] exact (AL j).mean_zero rw [hzero, map_zero] · -- finite_var : ‖quantileIFVec‖² ∈ L¹(P) have hsum : (fun x => ‖quantileIFVec τ q f x‖ ^ 2) = fun x => ∑ j, (quantileIF (τ j) (q j) (f j) x) ^ 2 := by funext x exact norm_sq_eucl (g x) rw [hsum] exact integrable_finset_sum _ (fun j _ => quantileIF_sq_integrable) · -- remainder : the vector Bahadur remainder is o_p(1) -- The per-coordinate scalar remainder `Rₙⱼ`. set R : Fin k → ℕ → Ω → ℝ := fun j n ω => sqrt ((range n).card : ℝ) * (S.sampleQuantile (τ j) n ω - q j) - (sqrt ((range n).card : ℝ))⁻¹ * ∑ i ∈ range n, quantileIF (τ j) (q j) (f j) (S.Z i ω) with hR have hRlit : ∀ j, IsLittleOp (R j) (fun _ => (1 : ℝ)) μ := fun j => (AL j).remainder -- The vector bracket equals `eucl (fun j => R j n ω)`. have hbracket : ∀ n ω, sqrt (((range n).card : ℝ)) • (S.sampleQuantileVec τ n ω - eucl q) - (sqrt (((range n).card : ℝ)))⁻¹ • ∑ i ∈ range n, quantileIFVec τ q f (S.Z i ω) = eucl (fun j => R j n ω) := by intro n ω change sqrt _ • (eucl (fun j => S.sampleQuantile (τ j) n ω) - eucl q) - (sqrt _)⁻¹ • ∑ i ∈ range n, eucl (g (S.Z i ω)) = eucl (fun j => R j n ω) rw [← map_sub, ← map_smul, ← map_sum, ← map_smul, ← map_sub] congr 1 funext j simp only [Pi.sub_apply, Pi.smul_apply, Finset.sum_apply, smul_eq_mul, hR, hg] -- `∑ⱼ |Rₙⱼ|` is o_p(1), and the vector norm is bounded by it. have hsum_lit : IsLittleOp (fun n ω => ∑ j, |R j n ω|) (fun _ => (1 : ℝ)) μ := isLittleOp_finset_sum_one univ (fun j n ω => |R j n ω|) (fun j _ => isLittleOp_abs (hRlit j)) refine isLittleOp_of_abs_le_const_mul_one (C := 1) one_pos hsum_lit ?_ intro n ω rw [hbracket n ω] rw [abs_of_nonneg (norm_nonneg _), one_mul, abs_of_nonneg (sum_nonneg fun j _ => abs_nonneg _)] exact norm_eucl_le_sum_abs (fun j => R j n ω)

theorem IIDSample.sampleQuantileVec_tendsto_normal (S : IIDSample Ω ℝ μ P) {τ q f : Fin k → ℝ} (hreg : ∀ j, SampleQuantileReg P (τ j) (q j) (f j)) (Q : Measure (EuclideanSpace ℝ (Fin k))) [IsProbabilityMeasure Q] (hQ : ∀ t : EuclideanSpace ℝ (Fin k), charFun Q t = exp (-(((∫ z, (⟪t, quantileIFVec τ q f z⟫) ^ 2 ∂P : ℝ)) : ℂ) / 2)) (hθn_meas : ∀ n, AEMeasurable (IsAsymLinearVec.rescaledEstimator (S.sampleQuantileVec τ) (eucl q) (fun m => range m) n) μ) : Tendsto (β := ProbabilityMeasure (EuclideanSpace ℝ (Fin k))) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator (S.sampleQuantileVec τ) (eucl q) (fun m => range m) n), Measure.isProbabilityMeasure_map (hθn_meas n)⟩) atTop (𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩) := by exact (S.sampleQuantileVec_isAsymLinearVec hreg).tendsto_normal_vec_clt (measurable_quantileIFVec τ q f) Q hQ hθn_meas