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 := by fun_prop 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_inProb (S : IIDSample Ω ℝ μ P) (y : ℝ) : Modes.TendstoInProbability (fun _ : ℕ => μ) (S.empiricalCDF y) atTop (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 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) {q₀ ρ : ℝ} (hcont : ContinuousOn (fun y => cdf P y) (Icc (q₀ - ρ) (q₀ + ρ))) {n : ℕ} (hn : 0 < n) {τ : ℝ} (hτ0 : 0 < τ) (hτ1 : τ < 1) : ∀ᵐ ω ∂μ, S.sampleQuantile τ n ω ∈ Ioo (q₀ - ρ) (q₀ + ρ) → |S.empiricalCDF (S.sampleQuantile τ n ω) n ω - τ| ≤ (n : ℝ)⁻¹ := by -- Local continuity of the cdf makes each singleton in the open neighborhood null. haveI hP : IsProbabilityMeasure P := by rw [← S.law] exact isProbabilityMeasure_map (S.meas 0).aemeasurable have hsingleton : ∀ x ∈ Ioo (q₀ - ρ) (q₀ + ρ), P {x} = 0 := by intro x hx have hxnhds : Icc (q₀ - ρ) (q₀ + ρ) ∈ nhds x := by simpa using hx have hcx : ContinuousAt (fun y => cdf P y) x := hcont.continuousAt hxnhds have heq : P = (cdf P).measure := (measure_cdf P).symm rw [heq, StieltjesFunction.measure_singleton, ContinuousWithinAt.leftLim_eq hcx.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 local distinctness follows from independence and the local singleton nullity. have hpair : ∀ i j : ℕ, i ≠ j → μ {ω | S.Z i ω = S.Z j ω ∧ S.Z i ω ∈ Ioo (q₀ - ρ) (q₀ + ρ)} = 0 := by intro i j hij have hind : IndepFun (S.Z i) (S.Z j) μ := S.indep.indepFun hij let A : Set (ℝ × ℝ) := {p | p.1 = p.2 ∧ p.1 ∈ Ioo (q₀ - ρ) (q₀ + ρ)} have hmeas : MeasurableSet A := (measurableSet_eq_fun measurable_fst measurable_snd).inter (measurableSet_Ioo.preimage measurable_fst) have hpre : {ω | S.Z i ω = S.Z j ω ∧ S.Z i ω ∈ Ioo (q₀ - ρ) (q₀ + ρ)} = (fun ω => (S.Z i ω, S.Z j ω)) ⁻¹' A := 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 => ?_) by_cases hx : x ∈ Ioo (q₀ - ρ) (q₀ + ρ) · have hsing : Prod.mk x ⁻¹' A = {x} := by ext y simp only [A, Set.mem_preimage, Set.mem_setOf_eq, Set.mem_singleton_iff] exact ⟨fun h => h.1.symm, fun h => ⟨h.symm, hx⟩⟩ change P (Prod.mk x ⁻¹' A) = 0 rw [hsing, hsingleton x hx] · have hempty : Prod.mk x ⁻¹' A = ∅ := by ext y simp only [A, Set.mem_preimage, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false] exact fun h => hx h.2 change P (Prod.mk x ⁻¹' A) = 0 rw [hempty, measure_empty] -- Assemble into one a.s. event with no ties whose common value is local. have hae : ∀ᵐ ω ∂μ, ∀ i ∈ (Finset.range n : Set ℕ), ∀ j ∈ (Finset.range n : Set ℕ), i ≠ j → ¬ (S.Z i ω = S.Z j ω ∧ S.Z i ω ∈ Ioo (q₀ - ρ) (q₀ + ρ)) := 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 ω ∈ Ioo (q₀ - ρ) (q₀ + ρ)))} = {ω | S.Z i ω = S.Z j ω ∧ S.Z i ω ∈ Ioo (q₀ - ρ) (q₀ + ρ)} := 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ω intro hq_local 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 Finset.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 have hqlocalq : q ∈ Ioo (q₀ - ρ) (q₀ + ρ) := by simpa [hq] using hq_local exact haeω a (by simpa using ha.1) b (by simpa using hb.1) hab ⟨ha.2.trans hb.2.symm, by rw [ha.2]; exact hqlocalq⟩ -- 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, Nat.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 Finset.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 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) μ) : Modes.TendstoInLaw (fun _ : ℕ => μ) (IsAsymLinear.rescaledEstimator qn q₀ (fun m => range m)) atTop (gaussianMeasure 0 (τ * (1 - τ) / f₀ ^ 2)) := by have hAL := h.isAsymLinear.tendsto_normal (measurable_quantileIF τ q₀ f₀) hθn_meas rwa [quantileIF_variance h.cdf_eq] at hAL

theorem tendstoUniformly_cdf_of_tendsto {ι : Type*} {l : Filter ι} {νs : ι → ProbabilityMeasure ℝ} {ν : ProbabilityMeasure ℝ} (hν : Tendsto νs l (𝓝 ν)) (hcont : Continuous (cdf (ν : Measure ℝ))) : TendstoUniformly (fun i ↦ cdf (νs i : Measure ℝ)) (cdf (ν : Measure ℝ)) l := by apply tendstoUniformly_of_monotone_of_tendsto_at_of_bounds (fun i ↦ monotone_cdf (νs i : Measure ℝ)) (fun i ↦ cdf_nonneg (νs i : Measure ℝ)) (fun i ↦ cdf_le_one (νs i : Measure ℝ)) (monotone_cdf (ν : Measure ℝ)) hcont (tendsto_cdf_atBot (ν : Measure ℝ)) (tendsto_cdf_atTop (ν : Measure ℝ)) intro t exact tendsto_cdf_at_of_tendsto hν hcont.continuousAt

theorem tendsto_quantile_of_tendsto {ι : Type*} {l : Filter ι} {νs : ι → ProbabilityMeasure ℝ} {ν : ProbabilityMeasure ℝ} {β : ℝ} (hν : Tendsto νs l (𝓝 ν)) (hβ0 : 0 < β) (hβ1 : β < 1) (hcont : Continuous (cdf (ν : Measure ℝ))) (hstrict : StrictlyIncreasingAt (cdf (ν : Measure ℝ)) (quantile (ν : Measure ℝ) β)) : Tendsto (fun i ↦ quantile (νs i : Measure ℝ) β) l (𝓝 (quantile (ν : Measure ℝ) β)) := by exact tendsto_quantile_of_tendstoUniformly hβ0 hβ1 (tendstoUniformly_cdf_of_tendsto hν hcont) hcont.continuousAt hstrict

theorem quantile_gaussianReal_zero {v : NNReal} (hv : 0 < v) {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1) : quantile (gaussianReal 0 v) β = sqrt (v : ℝ) * probit β := by have hvR : 0 < (v : ℝ) := by exact_mod_cast hv have hs : 0 < sqrt (v : ℝ) := Real.sqrt_pos.2 hvR have hcont := continuous_cdf_gaussianReal_zero hv have hquant : cdf (gaussianReal 0 v) (quantile (gaussianReal 0 v) β) = β := cdf_quantile_eq _ hβ0 hβ1 hcont.continuousAt have hcand : cdf (gaussianReal 0 v) (sqrt (v : ℝ) * probit β) = β := by rw [cdf_gaussianReal_zero hv] rw [mul_div_cancel_left₀ _ hs.ne'] exact stdNormalCDF_probit hβ0 hβ1 exact (strictMono_cdf_gaussianReal_zero hv).injective (hquant.trans hcand.symm)

theorem finite_mass_quantile_transport_le (μ ν : FiniteMeasure ℝ) {a b : ℝ} (hab : a ≤ b) (hp : 0 < (μ.mass : ℝ)) (hq : 0 < (ν.mass : ℝ)) (hμ : (μ : Measure ℝ) (Icc a b)ᶜ = 0) (hν : (ν : Measure ℝ) (Icc a b)ᶜ = 0) : min (μ.mass : ℝ) (ν.mass : ℝ) * (∫ u in (0 : ℝ)..1, |quantile (μ.normalize : Measure ℝ) u - quantile (ν.normalize : Measure ℝ) u|) ≤ (∫ t in a..b, |((μ : Measure ℝ) (Iic t)).toReal - ((ν : Measure ℝ) (Iic t)).toReal|) + (b - a) * |(μ.mass : ℝ) - (ν.mass : ℝ)| := by /- Apply `quantile_transport_eq_cdf_distance` to the two normalized probability measures. Their support follows from `hμ,hν` and `normalize_eq_of_nonzero`. Rewrite normalized CDFs with `cdf_normalize_eq_div`, then apply the integrated algebra bound. For each raw CDF, `measure_mono (Set.subset_univ _)` followed by `ENNReal.toReal_mono` gives the upper mass bound; the lower bound is `ENNReal.toReal_nonneg`. Use `intervalIntegrable_abs_cdf_sub` for the normalized difference and `intervalIntegrable_abs_raw_cdf_sub` for the raw difference. -/ have hμ' := normalize_support_Icc μ hp hμ have hν' := normalize_support_Icc ν hq hν have htransport := quantile_transport_eq_cdf_distance (μ.normalize : Measure ℝ) (ν.normalize : Measure ℝ) hab hμ' hν' have hμbound (t : ℝ) : 0 ≤ ((μ : Measure ℝ) (Iic t)).toReal ∧ ((μ : Measure ℝ) (Iic t)).toReal ≤ (μ.mass : ℝ) := by exact ⟨ENNReal.toReal_nonneg, ENNReal.toReal_mono (measure_ne_top _ _) (measure_mono (subset_univ _))⟩ have hνbound (t : ℝ) : 0 ≤ ((ν : Measure ℝ) (Iic t)).toReal ∧ ((ν : Measure ℝ) (Iic t)).toReal ≤ (ν.mass : ℝ) := by exact ⟨ENNReal.toReal_nonneg, ENNReal.toReal_mono (measure_ne_top _ _) (measure_mono (subset_univ _))⟩ have hnorm := intervalIntegrable_abs_cdf_sub (μ.normalize : Measure ℝ) (ν.normalize : Measure ℝ) a b have hraw := intervalIntegrable_abs_raw_cdf_sub μ ν a b have hnorm' : IntervalIntegrable (fun t => |((μ : Measure ℝ) (Iic t)).toReal / (μ.mass : ℝ) - ((ν : Measure ℝ) (Iic t)).toReal / (ν.mass : ℝ)|) volume a b := by simpa only [cdf_normalize_eq_div μ hp, cdf_normalize_eq_div ν hq] using hnorm rw [htransport] have hrewrite : (∫ t in a..b, |cdf (μ.normalize : Measure ℝ) t - cdf (ν.normalize : Measure ℝ) t|) = ∫ t in a..b, |((μ : Measure ℝ) (Iic t)).toReal / (μ.mass : ℝ) - ((ν : Measure ℝ) (Iic t)).toReal / (ν.mass : ℝ)| := by apply intervalIntegral.integral_congr intro t _ change |cdf (μ.normalize : Measure ℝ) t - cdf (ν.normalize : Measure ℝ) t| = _ rw [cdf_normalize_eq_div μ hp, cdf_normalize_eq_div ν hq] rw [hrewrite] exact min_mul_integral_abs_div_sub_div_le hab hp hq (fun t _ => hμbound t) (fun t _ => hνbound t) hnorm' hraw

theorem finite_mass_quantile_transport_eq_of_mass_eq (μ ν : FiniteMeasure ℝ) {a b : ℝ} (hab : a ≤ b) (hm : μ.mass = ν.mass) (hp : 0 < (μ.mass : ℝ)) (hμ : (μ : Measure ℝ) (Icc a b)ᶜ = 0) (hν : (ν : Measure ℝ) (Icc a b)ᶜ = 0) : (μ.mass : ℝ) * (∫ u in (0 : ℝ)..1, |quantile (μ.normalize : Measure ℝ) u - quantile (ν.normalize : Measure ℝ) u|) = ∫ t in a..b, |((μ : Measure ℝ) (Iic t)).toReal - ((ν : Measure ℝ) (Iic t)).toReal| := by /- Normalize support, apply `quantile_transport_eq_cdf_distance`, rewrite both CDFs with `cdf_normalize_eq_div`, then pull out the common positive mass through absolute value and interval integration. `hm` identifies the denominators. Pointwise, positive `p` gives `p * |x / p - y / p| = |x - y|`; use this inside `intervalIntegral.integral_congr` after `integral_const_mul`. -/ have hq : 0 < (ν.mass : ℝ) := by simpa [hm] using hp have hμ' := normalize_support_Icc μ hp hμ have hν' := normalize_support_Icc ν hq hν have htransport := quantile_transport_eq_cdf_distance (μ.normalize : Measure ℝ) (ν.normalize : Measure ℝ) hab hμ' hν' rw [htransport] have hrewrite : (∫ t in a..b, |cdf (μ.normalize : Measure ℝ) t - cdf (ν.normalize : Measure ℝ) t|) = ∫ t in a..b, |((μ : Measure ℝ) (Iic t)).toReal / (μ.mass : ℝ) - ((ν : Measure ℝ) (Iic t)).toReal / (ν.mass : ℝ)| := by apply intervalIntegral.integral_congr intro t _ change |cdf (μ.normalize : Measure ℝ) t - cdf (ν.normalize : Measure ℝ) t| = _ rw [cdf_normalize_eq_div μ hp, cdf_normalize_eq_div ν hq] rw [hrewrite] rw [hm] rw [← intervalIntegral.integral_const_mul] apply intervalIntegral.integral_congr intro t _ change (ν.mass : ℝ) * |((μ : Measure ℝ) (Iic t)).toReal / (ν.mass : ℝ) - ((ν : Measure ℝ) (Iic t)).toReal / (ν.mass : ℝ)| = |((μ : Measure ℝ) (Iic t)).toReal - ((ν : Measure ℝ) (Iic t)).toReal| rw [← sub_div, abs_div, abs_of_pos hq] exact mul_div_cancel₀ _ (ne_of_gt hq)

theorem quantile_pushforward_lipschitzOn (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {a b L : ℝ} (hab : a ≤ b) (hμ : μ (Icc a b)ᶜ = 0) (hν : ν (Icc a b)ᶜ = 0) (hL : 0 ≤ L) (f : ℝ → ℝ) (hf : Measurable f) (hLip : ∀ x ∈ Icc a b, ∀ y ∈ Icc a b, |f x - f y| ≤ L * |x - y|) : (∫ u in (0 : ℝ)..1, |quantile (μ.map f) u - quantile (ν.map f) u|) ≤ L * ∫ u in (0 : ℝ)..1, |quantile μ u - quantile ν u| := by letI : IsProbabilityMeasure (μ.map f) := Measure.isProbabilityMeasure_map hf.aemeasurable letI : IsProbabilityMeasure (ν.map f) := Measure.isProbabilityMeasure_map hf.aemeasurable let c := f a - L * (b - a) let d := f a + L * (b - a) have hcd : c ≤ d := by dsimp [c, d] have hba : 0 ≤ b - a := sub_nonneg.mpr hab nlinarith [mul_nonneg hL hba] have hμ' : (μ.map f) (Icc c d)ᶜ = 0 := map_supported_in_lipschitz_range μ hab hμ hL f hf hLip have hν' : (ν.map f) (Icc c d)ᶜ = 0 := map_supported_in_lipschitz_range ν hab hν hL f hf hLip let π := comonotoneCoupling μ ν have hπ : IsCoupling π μ ν := isCoupling_comonotoneCoupling μ ν have hπ' : IsCoupling (π.map (fun z : ℝ × ℝ => (f z.1, f z.2))) (μ.map f) (ν.map f) := map_pair_isCoupling μ ν f hf hπ have hopt := quantile_cost_le_coupling_cost (μ.map f) (ν.map f) hcd hμ' hν' hπ' have hcost := mapped_coupling_cost_le μ ν hμ hν f hf hLip hπ have hquant : (∫ z : ℝ × ℝ, |z.1 - z.2| ∂π) = ∫ u in (0 : ℝ)..1, |quantile μ u - quantile ν u| := by have hpair : AEMeasurable (fun u : ℝ => (quantile μ u, quantile ν u)) unifOI := (aemeasurable_quantile_unifOI μ).prodMk (aemeasurable_quantile_unifOI ν) have hmeas : AEStronglyMeasurable (fun z : ℝ × ℝ => |z.1 - z.2|) π := by fun_prop change (∫ z : ℝ × ℝ, |z.1 - z.2| ∂ (unifOI.map (fun u : ℝ => (quantile μ u, quantile ν u)))) = _ rw [integral_map hpair hmeas] have hrest : volume.restrict (Ioc (0 : ℝ) 1) = unifOI := by rw [unifOI, restrict_Ioo_eq_restrict_Ioc] rw [intervalIntegral.integral_of_le (by norm_num : (0 : ℝ) ≤ 1), hrest] exact hopt.trans (hcost.trans_eq (congrArg (L * ·) hquant))

theorem quantile_pushforward_lipschitz (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {a b L : ℝ} (hab : a ≤ b) (hμ : μ (Icc a b)ᶜ = 0) (hν : ν (Icc a b)ᶜ = 0) (hL : 0 ≤ L) (f : ℝ → ℝ) (hf : Measurable f) (hLip : ∀ x y : ℝ, |f x - f y| ≤ L * |x - y|) : (∫ u in (0 : ℝ)..1, |quantile (μ.map f) u - quantile (ν.map f) u|) ≤ L * ∫ u in (0 : ℝ)..1, |quantile μ u - quantile ν u| := by exact quantile_pushforward_lipschitzOn μ ν hab hμ hν hL f hf (fun x _ y _ => hLip x y)

theorem IIDSample.quantileBand_coverage (S : IIDSample Ω ℝ μ P) [IsProbabilityMeasure P] {n : ℕ} (hn : 0 < n) {α : ℝ} (hα : 0 < α) (hα_one : α ≤ 1) : μ (S.quantileBandCoverageEvent α n) ≥ 1 - ofReal α := by have hCDF := S.cdfBand_coverage hn hα hα_one exact hCDF.trans (measure_mono fun ω hω => by intro τ hτ_lower hτ_upper apply S.quantile_mem_quantileBand_of_cdfBand (vcMcDiarmidRadius_nonneg α n) hn ω hτ_lower hτ_upper intro x have hx := hω x change cdf P x ∈ Icc (max 0 (S.empiricalCDF x n ω - vcMcDiarmidRadius α n)) (min 1 (S.empiricalCDF x n ω + vcMcDiarmidRadius α n)) at hx exact ⟨(le_max_right _ _).trans hx.1, hx.2.trans (min_le_right _ _)⟩)

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 (Finset.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 (Finset.sum_nonneg fun j _ => abs_nonneg _)] exact norm_eucl_le_sum_abs (fun j => R j n ω)

theorem IIDSample.sampleQuantileVec_tendsto_of_charFun (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