Stat.Quantile.Atomic­Approximation

theorem cdfDistance_equalAtomMeasure_weight_le (a b : ℝ) (hab : a ≤ b) (N : ℕ) (hN : 0 < N) (m q : ℝ) (hm : 0 ≤ m) (hq : 0 ≤ q) (x : Fin N → ℝ) : cdfDistance a b (equalAtomMeasure N m x) (equalAtomMeasure N q x) ≤ (1 + (b - a)) * |m - q| := by /- The two CDFs are the same empirical counting function multiplied by `m/N` or `q/N`. Its values lie in `[0,1]`. Integrate the resulting pointwise bound `|Fₘ(t)-F_q(t)| ≤ |m-q|` and use the mass lemma above. -/ have hformula (w : ℝ) (hw : 0 ≤ w) (s : Set ℝ) : (equalAtomMeasure N w x).real s = (w / N) * ∑ i, (Measure.dirac (x i)).real s := by simp only [equalAtomMeasure, Measure.real, Measure.finsetSum_apply, Measure.smul_apply] rw [ENNReal.toReal_sum (by intro i hi by_cases hx : x i ∈ s <;> simp [Measure.dirac_apply, hx])] simp [ENNReal.toReal_mul, ENNReal.toReal_ofReal (div_nonneg hw (Nat.cast_nonneg _)), ← Finset.mul_sum] have hscale (w : ℝ) (hw : 0 ≤ w) (s : Set ℝ) : (equalAtomMeasure N w x).real s = w * (equalAtomMeasure N 1 x).real s := by rw [hformula w hw s, hformula 1 (by norm_num) s] ring have hfinite (w : ℝ) : IsFiniteMeasure (equalAtomMeasure N w x) := by haveI : ∀ i : Fin N, IsFiniteMeasure (ofReal (w / N) • Measure.dirac (x i)) := fun i => Measure.smul_finite _ (by simp) unfold equalAtomMeasure infer_instance letI : IsFiniteMeasure (equalAtomMeasure N 1 x) := hfinite 1 have hunit : (equalAtomMeasure N 1 x).real univ = 1 := equalAtomMeasure_mass N hN 1 (by norm_num) x have hpoint (t : ℝ) : |(equalAtomMeasure N m x).real (Iic t) - (equalAtomMeasure N q x).real (Iic t)| ≤ |m - q| := by rw [hscale m hm, hscale q hq, ← sub_mul, abs_mul, abs_of_nonneg (measureReal_nonneg (μ := equalAtomMeasure N 1 x))] apply mul_le_of_le_one_right (abs_nonneg _) have hle := measureReal_mono (μ := equalAtomMeasure N 1 x) (subset_univ (Iic t)) (by finiteness) rwa [hunit] at hle let μf : FiniteMeasure ℝ := ⟨equalAtomMeasure N m x, hfinite m⟩ let νf : FiniteMeasure ℝ := ⟨equalAtomMeasure N q x, hfinite q⟩ have hint := intervalIntegrable_abs_raw_cdf_sub μf νf a b change IntervalIntegrable (fun t : ℝ => |(equalAtomMeasure N m x).real (Iic t) - (equalAtomMeasure N q x).real (Iic t)|) volume a b at hint have hbound := intervalIntegral.integral_mono_on hab hint (intervalIntegrable_const : IntervalIntegrable (fun _ : ℝ => |m - q|) volume a b) (fun t _ => hpoint t) rw [intervalIntegral.integral_const] at hbound simp only [smul_eq_mul] at hbound rw [cdfDistance, equalAtomMeasure_mass N hN m hm x, equalAtomMeasure_mass N hN q hq x] nlinarith [abs_nonneg (m - q)]

theorem equalAtomMeasure_dense_locations (a b : ℝ) (hab : a ≤ b) (D : Set ℝ) (hDense : Dense ((Subtype.val : Icc a b → ℝ) ⁻¹' D)) (N : ℕ) (hN : 0 < N) (w : ℝ) (hw : 0 ≤ w) (x : Fin N → Icc a b) (ε : ℝ) (hε : 0 < ε) : ∃ y : Fin N → D, cdfDistance a b (equalAtomMeasure N w (fun i => (x i : ℝ))) (equalAtomMeasure N w (fun i => (y i : ℝ))) < ε := by let δ : ℝ := ε / (w + 1) have hδ : 0 < δ := div_pos hε (by linarith) have hnear (i : Fin N) : ∃ z : Icc a b, (z : ℝ) ∈ D ∧ |(x i : ℝ) - (z : ℝ)| < δ := by obtain ⟨z, hz, hdist⟩ := hDense.exists_dist_lt (x i) hδ refine ⟨z, hz, ?_⟩ simpa only [Subtype.dist_eq, Real.dist_eq] using hdist choose z hz hdist using hnear let y : Fin N → D := fun i => ⟨(z i : ℝ), hz i⟩ refine ⟨y, ?_⟩ have hsum : (∑ i : Fin N, |(x i : ℝ) - (z i : ℝ)|) ≤ (N : ℝ) * δ := by calc (∑ i : Fin N, |(x i : ℝ) - (z i : ℝ)|) ≤ ∑ _i : Fin N, δ := Finset.sum_le_sum (fun i _ => le_of_lt (hdist i)) _ = (N : ℝ) * δ := by simp have hNreal : (0 : ℝ) < N := Nat.cast_pos.mpr hN have hcoef : 0 ≤ w / (N : ℝ) := div_nonneg hw (le_of_lt hNreal) calc cdfDistance a b (equalAtomMeasure N w (fun i => (x i : ℝ))) (equalAtomMeasure N w (fun i => (y i : ℝ))) ≤ (w / N) * ∑ i, |(x i : ℝ) - (z i : ℝ)| := by simpa [y] using cdfDistance_equalAtomMeasure_locations_le a b hab N hN w hw x z _ ≤ (w / N) * ((N : ℝ) * δ) := mul_le_mul_of_nonneg_left hsum hcoef _ = w * δ := by field_simp _ < ε := by dsimp [δ] calc w * (ε / (w + 1)) = w * ε / (w + 1) := by ring _ < ε := (div_lt_iff₀ (by linarith : (0 : ℝ) < w + 1)).2 (by nlinarith)

theorem eventually_equalAtomMeasure_approx (μ : Measure ℝ) [IsFiniteMeasure μ] (a b : ℝ) (hab : a ≤ b) (hμ : μ (Icc a b)ᶜ = 0) (D : Set ℝ) (hDense : Dense ((Subtype.val : Icc a b → ℝ) ⁻¹' D)) (ε : ℝ) (hε : 0 < ε) : ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N → 0 < N → ∃ x : Fin N → D, cdfDistance a b μ (equalAtomMeasure N (μ.real univ) (fun i => (x i : ℝ))) < ε := by /- Apply `eventually_equalAtomMeasure_interval_approx` with half the tolerance and then `equalAtomMeasure_dense_locations` to each grid. More precisely, choose `ε / 2` for both steps, extract their common threshold `N₀`, and for each positive `N ≥ N₀` obtain `x₀` in `Icc a b` and then `x` in `D`. Supply `IsFiniteMeasure` for the two finite Dirac sums using `Measure.smul_finite` and `infer_instance`, as in `QuantileGrid.eventually_equalAtomMeasure_interval_approx`. Apply `cdfDistance_triangle a b hab` and close the strict inequality with the two half-tolerance bounds. This also covers zero mass and endpoint atoms without further cases. -/ obtain ⟨N₀, hN₀⟩ := eventually_equalAtomMeasure_interval_approx μ a b hab hμ (ε / 2) (by linarith) refine ⟨N₀, ?_⟩ intro N hN₀N hN obtain ⟨x₀, hx₀⟩ := hN₀ N hN₀N hN obtain ⟨x, hx⟩ := equalAtomMeasure_dense_locations a b hab D hDense N hN (μ.real univ) measureReal_nonneg x₀ (ε / 2) (by linarith) refine ⟨x, ?_⟩ have hfinite (z : Fin N → ℝ) : IsFiniteMeasure (equalAtomMeasure N (μ.real univ) z) := by haveI : ∀ i : Fin N, IsFiniteMeasure (ofReal (μ.real univ / N) • Measure.dirac (z i)) := fun _ => Measure.smul_finite _ (by simp) unfold equalAtomMeasure infer_instance letI : IsFiniteMeasure (equalAtomMeasure N (μ.real univ) (fun i => (x₀ i : ℝ))) := hfinite _ letI : IsFiniteMeasure (equalAtomMeasure N (μ.real univ) (fun i => (x i : ℝ))) := hfinite _ have htri := cdfDistance_triangle a b hab μ (equalAtomMeasure N (μ.real univ) (fun i => (x₀ i : ℝ))) (equalAtomMeasure N (μ.real univ) (fun i => (x i : ℝ))) linarith

theorem exists_synchronized_rational_equalAtom_approx (μ₁ μ₂ : Measure ℝ) [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂] (a₁ b₁ a₂ b₂ : ℝ) (hab₁ : a₁ ≤ b₁) (hab₂ : a₂ ≤ b₂) (hμ₁ : μ₁ (Icc a₁ b₁)ᶜ = 0) (hμ₂ : μ₂ (Icc a₂ b₂)ᶜ = 0) (hmass : μ₁.real Set.univ = μ₂.real Set.univ) (D₁ D₂ : Set ℝ) (hdense₁ : Dense ((Subtype.val : Icc a₁ b₁ → ℝ) ⁻¹' D₁)) (hdense₂ : Dense ((Subtype.val : Icc a₂ b₂ → ℝ) ⁻¹' D₂)) (η : ℝ) (hη : 0 < η) : ∃ (N : ℕ) (hN : 0 < N) (q : ℚ), 0 ≤ q ∧ ∃ (x : Fin N → D₁) (y : Fin N → D₂), (equalAtomMeasure N (q : ℝ) (fun i => (x i : ℝ))).real Set.univ = (q : ℝ) ∧ (equalAtomMeasure N (q : ℝ) (fun i => (y i : ℝ))).real Set.univ = (q : ℝ) ∧ cdfDistance a₁ b₁ μ₁ (equalAtomMeasure N (q : ℝ) (fun i => (x i : ℝ))) + cdfDistance a₂ b₂ μ₂ (equalAtomMeasure N (q : ℝ) (fun i => (y i : ℝ))) < η := by /- Put `m = μ₁.real univ = μ₂.real univ` and `C = (1 + (b₁-a₁)) + (1 + (b₂-a₂))`, so `m ≥ 0` and `C ≥ 2`. Apply `exists_rat_btwn` to `m < m + η/(2*C)` to obtain a rational `q > m ≥ 0`; then `|m-q| < η/(2*C)`, including when `m = 0`. Apply `eventually_equalAtomMeasure_approx` to each measure with tolerance `η/4`, and take a positive `N` above both thresholds. For each interval, use `cdfDistance_triangle` followed by `cdfDistance_equalAtomMeasure_weight_le` to replace the empirical measure's weight `m` by `q`. The two empirical errors total less than `η/2`, and the two weight-change bounds total less than `η/2`. Close exact masses with `equalAtomMeasure_mass`. Countability remains in the public API for sieve reuse; the density hypotheses do the work here. -/ let m : ℝ := μ₁.real Set.univ let C : ℝ := (1 + (b₁ - a₁)) + (1 + (b₂ - a₂)) have hm : 0 ≤ m := measureReal_nonneg have hC : 0 < C := by dsimp [C]; linarith have hδ : 0 < η / (2 * C) := div_pos hη (by positivity) obtain ⟨q, hmq, hqUpper⟩ := exists_rat_btwn (lt_add_of_pos_right m hδ) have hq : 0 ≤ (q : ℝ) := le_trans hm hmq.le have hweight : C * |m - (q : ℝ)| < η / 2 := by rw [abs_sub_comm, abs_of_pos (sub_pos.mpr hmq)] have hdiff : (q : ℝ) - m < η / (2 * C) := by linarith calc C * ((q : ℝ) - m) < C * (η / (2 * C)) := mul_lt_mul_of_pos_left hdiff hC _ = η / 2 := by field_simp obtain ⟨N₁, hN₁⟩ := eventually_equalAtomMeasure_approx μ₁ a₁ b₁ hab₁ hμ₁ D₁ hdense₁ (η / 4) (by linarith) obtain ⟨N₂, hN₂⟩ := eventually_equalAtomMeasure_approx μ₂ a₂ b₂ hab₂ hμ₂ D₂ hdense₂ (η / 4) (by linarith) let N := max N₁ N₂ + 1 have hN : 0 < N := by dsimp [N]; omega have hN₁' : N₁ ≤ N := by dsimp [N]; omega have hN₂' : N₂ ≤ N := by dsimp [N]; omega obtain ⟨x, hx⟩ := hN₁ N hN₁' hN obtain ⟨y, hy⟩ := hN₂ N hN₂' hN have hfinite (w : ℝ) (z : Fin N → ℝ) : IsFiniteMeasure (equalAtomMeasure N w z) := by haveI : ∀ i : Fin N, IsFiniteMeasure (ofReal (w / N) • Measure.dirac (z i)) := fun _ => Measure.smul_finite _ (by simp) unfold equalAtomMeasure infer_instance letI : IsFiniteMeasure (equalAtomMeasure N m (fun i => (x i : ℝ))) := hfinite _ _ letI : IsFiniteMeasure (equalAtomMeasure N (q : ℝ) (fun i => (x i : ℝ))) := hfinite _ _ letI : IsFiniteMeasure (equalAtomMeasure N m (fun i => (y i : ℝ))) := hfinite _ _ letI : IsFiniteMeasure (equalAtomMeasure N (q : ℝ) (fun i => (y i : ℝ))) := hfinite _ _ have htri₁ := cdfDistance_triangle a₁ b₁ hab₁ μ₁ (equalAtomMeasure N m (fun i => (x i : ℝ))) (equalAtomMeasure N (q : ℝ) (fun i => (x i : ℝ))) have htri₂ := cdfDistance_triangle a₂ b₂ hab₂ μ₂ (equalAtomMeasure N m (fun i => (y i : ℝ))) (equalAtomMeasure N (q : ℝ) (fun i => (y i : ℝ))) have hw₁ := cdfDistance_equalAtomMeasure_weight_le a₁ b₁ hab₁ N hN m (q : ℝ) hm hq (fun i => (x i : ℝ)) have hw₂ := cdfDistance_equalAtomMeasure_weight_le a₂ b₂ hab₂ N hN m (q : ℝ) hm hq (fun i => (y i : ℝ)) have hsumWeight : cdfDistance a₁ b₁ (equalAtomMeasure N m (fun i => (x i : ℝ))) (equalAtomMeasure N (q : ℝ) (fun i => (x i : ℝ))) + cdfDistance a₂ b₂ (equalAtomMeasure N m (fun i => (y i : ℝ))) (equalAtomMeasure N (q : ℝ) (fun i => (y i : ℝ))) < η / 2 := by have hbound : cdfDistance a₁ b₁ (equalAtomMeasure N m (fun i => (x i : ℝ))) (equalAtomMeasure N (q : ℝ) (fun i => (x i : ℝ))) + cdfDistance a₂ b₂ (equalAtomMeasure N m (fun i => (y i : ℝ))) (equalAtomMeasure N (q : ℝ) (fun i => (y i : ℝ))) ≤ C * |m - (q : ℝ)| := by dsimp [C] nlinarith [hw₁, hw₂] exact lt_of_le_of_lt hbound hweight refine ⟨N, hN, q, ?_, x, y, ?_, ?_, ?_⟩ · exact_mod_cast hq · exact equalAtomMeasure_mass N hN (q : ℝ) hq _ · exact equalAtomMeasure_mass N hN (q : ℝ) hq _ · have hx' : cdfDistance a₁ b₁ μ₁ (equalAtomMeasure N m (fun i => (x i : ℝ))) < η / 4 := hx have hy' : cdfDistance a₂ b₂ μ₂ (equalAtomMeasure N m (fun i => (y i : ℝ))) < η / 4 := by simpa [m, hmass] using hy linarith

theorem exists_probability_equalAtom_interval_cdf_error_le (μ : Measure ℝ) [IsProbabilityMeasure μ] (a b : ℝ) (hμ : μ (Icc a b)ᶜ = 0) (N : ℕ) (hN : 0 < N) : ∃ x : Fin N → Icc a b, ∀ t : ℝ, |μ.real (Iic t) - (equalAtomMeasure N 1 (fun i => (x i : ℝ))).real (Iic t)| ≤ 1 / (N : ℝ) := by /- Use normalized midpoint ranks `((i : ℝ) + 1/2) / N`, all strictly in `(0,1)`. The quantile/CDF adjunction in Mathlib (`quantile_le_iff`) makes each atom's indicator at `t` equivalent to its rank being below `μ.real (Iic t)`. Count midpoint ranks below a value in `[0,1]` using floor bounds. Compact support puts every selected quantile in `Icc a b`, including when the measure charges either endpoint. -/ have hNreal : (0 : ℝ) < N := by exact_mod_cast hN have hgrid (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : |p - (((Finset.univ.filter (fun i : Fin N => ((i : ℝ) + 1 / 2) / N ≤ p)).card : ℝ) / N)| ≤ 1 / (N : ℝ) := by let m := ⌊(N : ℝ) * p + 1 / 2⌋₊ have hnonneg : 0 ≤ (N : ℝ) * p + 1 / 2 := by positivity have hmle : m ≤ N := by have hmul : (N : ℝ) * p ≤ N := (mul_le_mul_of_nonneg_left hp1 hNreal.le).trans_eq (mul_one _) have hbound : (N : ℝ) * p + 1 / 2 < (N : ℝ) + 1 := by linarith have hh : m < N + 1 := (Nat.floor_lt hnonneg).mpr (by simpa only [Nat.cast_add, Nat.cast_one] using hbound) omega have hiff (i : Fin N) : ((i : ℝ) + 1 / 2) / N ≤ p ↔ (i : ℕ) < m := by have hm : (i : ℕ) + 1 ≤ m ↔ ((i : ℝ) + 1 : ℝ) ≤ (N : ℝ) * p + 1 / 2 := by simpa only [Nat.cast_add, Nat.cast_one] using (Nat.le_floor_iff hnonneg (n := (i : ℕ) + 1)) constructor · intro h have hh := (div_le_iff₀ hNreal).mp h have hi : ((i : ℝ) + 1 : ℝ) ≤ (N : ℝ) * p + 1 / 2 := by linarith exact Nat.lt_of_succ_le (hm.mpr (by exact_mod_cast hi)) · intro h have hh : ((i : ℝ) + 1 : ℝ) ≤ (N : ℝ) * p + 1 / 2 := hm.mp (Nat.succ_le_iff.mpr h) apply (div_le_iff₀ hNreal).mpr linarith have hc : (Finset.univ.filter (fun i : Fin N => ((i : ℝ) + 1 / 2) / N ≤ p)).card = m := by have heq : Finset.univ.filter (fun i : Fin N => ((i : ℝ) + 1 / 2) / N ≤ p) = Finset.univ.filter (fun i : Fin N => (i : ℕ) < m) := by ext i simp only [mem_filter, Finset.mem_univ, true_and] exact hiff i rw [heq, Fin.card_filter_val_lt, min_eq_right hmle] rw [hc] have hmlo : (m : ℝ) ≤ (N : ℝ) * p + 1 / 2 := Nat.floor_le hnonneg have hmhi : (N : ℝ) * p + 1 / 2 < (m : ℝ) + 1 := Nat.lt_floor_add_one _ have hdu : (1 : ℝ) / N * N = 1 := by field_simp rw [abs_le] constructor · have hh : (m : ℝ) / N ≤ p + 1 / N := by apply (div_le_iff₀ hNreal).mpr calc (m : ℝ) ≤ N * p + 1 / 2 := hmlo _ ≤ (p + 1 / N) * N := by rw [add_mul, hdu]; nlinarith linarith · have hh : p ≤ ((m : ℝ) + 1) / N := by apply (le_div_iff₀ hNreal).mpr nlinarith rw [add_div] at hh linarith have hcompb : μ (Iic b)ᶜ = 0 := measure_mono_null (by intro x hx hxab exact hx hxab.2) hμ have hmu_b : μ (Iic b) = 1 := by have hh := measure_compl (μ := μ) (s := (Iic b)ᶜ) (by measurability) (by simp) simpa only [compl_compl, hcompb, tsub_zero, measure_univ] using hh have hcdfb : cdf μ b = 1 := by rw [cdf_eq_real, measureReal_def, hmu_b] norm_num have hlow (t : ℝ) (ht : t < a) : cdf μ t = 0 := by have hh : μ (Iic t) = 0 := measure_mono_null (by intro x hx hxab exact (not_le_of_gt (lt_of_le_of_lt hx ht)) hxab.1) hμ rw [cdf_eq_real, measureReal_def, hh] norm_num have hrank (i : Fin N) : 0 < ((i : ℝ) + 1 / 2) / N ∧ ((i : ℝ) + 1 / 2) / N < 1 := by have hi : ((i : ℝ) + 1 : ℝ) ≤ N := by exact_mod_cast (Nat.succ_le_iff.mpr i.isLt) constructor · positivity · apply (div_lt_iff₀ hNreal).mpr norm_num only [one_mul] linarith have hmem (i : Fin N) : quantile μ (((i : ℝ) + 1 / 2) / N) ∈ Icc a b := by obtain ⟨hu0, hu1⟩ := hrank i refine ⟨?_, ?_⟩ · by_contra hh have hqa : quantile μ (((i : ℝ) + 1 / 2) / N) < a := lt_of_not_ge hh have huq : ((i : ℝ) + 1 / 2) / N ≤ cdf μ (quantile μ (((i : ℝ) + 1 / 2) / N)) := le_cdf_quantile hu1 rw [hlow _ hqa] at huq linarith · exact (quantile_le_iff hu0 hu1).mpr (by rw [hcdfb]; exact hu1.le) let x : Fin N → Icc a b := fun i => ⟨quantile μ (((i : ℝ) + 1 / 2) / N), hmem i⟩ refine ⟨x, ?_⟩ intro t have hemp : (equalAtomMeasure N 1 (fun i => (x i : ℝ))).real (Iic t) = ((Finset.univ.filter (fun i : Fin N => (x i : ℝ) ≤ t)).card : ℝ) / N := by have hformula : (equalAtomMeasure N 1 (fun i => (x i : ℝ))).real (Iic t) = (1 / (N : ℝ)) * ∑ i, (Measure.dirac (x i : ℝ)).real (Iic t) := by simp only [equalAtomMeasure, Measure.real, Measure.finsetSum_apply, Measure.smul_apply] rw [ENNReal.toReal_sum (by intro i hi by_cases hx : (x i : ℝ) ∈ Iic t <;> simp [hx])] simp [ENNReal.toReal_mul, ← Finset.mul_sum] rw [hformula] have hsum : (∑ i, (Measure.dirac (x i : ℝ)).real (Iic t)) = ((Finset.univ.filter (fun i : Fin N => (x i : ℝ) ≤ t)).card : ℝ) := by classical simp only [Measure.real, Measure.dirac_apply, indicator, Set.mem_Iic] simp_rw [apply_ite toReal] simp rw [hsum] ring have heq : Finset.univ.filter (fun i : Fin N => (x i : ℝ) ≤ t) = Finset.univ.filter (fun i : Fin N => ((i : ℝ) + 1 / 2) / N ≤ μ.real (Iic t)) := by ext i simp only [mem_filter, Finset.mem_univ, true_and] exact (quantile_le_iff (hrank i).1 (hrank i).2).trans (by rw [cdf_eq_real]) rw [hemp, heq] exact hgrid (μ.real (Iic t)) (measureReal_nonneg) (by rw [← cdf_eq_real] exact cdf_le_one μ t)

theorem eventually_equalAtomMeasure_interval_approx (μ : Measure ℝ) [IsFiniteMeasure μ] (a b : ℝ) (hab : a ≤ b) (hμ : μ (Icc a b)ᶜ = 0) (ε : ℝ) (hε : 0 < ε) : ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N → 0 < N → ∃ x : Fin N → Icc a b, cdfDistance a b μ (equalAtomMeasure N (μ.real univ) (fun i => (x i : ℝ))) < ε := by /- Apply `exists_equalAtomMeasure_interval_cdf_error_le` and `cdfDistance_le_of_pointwise_cdf_le` with the mass identity from `equalAtomMeasure_mass`; the distance is bounded by `(b-a) * μ.real univ / N`. For the numerical step, `tendsto_const_div_atTop_nhds_zero_nat` applied to `(b-a) * μ.real univ`, followed by `Filter.Tendsto.eventually (eventually_lt_nhds hε)`, gives an eventual strict bound. Extract `N₀` with `Filter.eventually_atTop.1`; take its maximum with `1`. The mass can be zero, so avoid division by the mass. -/ have hlim : Tendsto (fun N : ℕ => ((b - a) * μ.real univ) / (N : ℝ)) atTop (nhds 0) := tendsto_const_div_atTop_nhds_zero_nat _ have hev : ∀ᶠ N : ℕ in atTop, ((b - a) * μ.real univ) / (N : ℝ) < ε := hlim.eventually (eventually_lt_nhds hε) obtain ⟨N₀, hN₀⟩ := Filter.eventually_atTop.1 hev refine ⟨N₀, ?_⟩ intro N hN₀N hN obtain ⟨x, hx⟩ := exists_equalAtomMeasure_interval_cdf_error_le μ a b hab hμ N hN refine ⟨x, ?_⟩ have hm : 0 ≤ μ.real univ := measureReal_nonneg have hmass : μ.real univ = (equalAtomMeasure N (μ.real univ) (fun i => (x i : ℝ))).real univ := by symm exact equalAtomMeasure_mass N hN _ hm _ haveI : IsFiniteMeasure (equalAtomMeasure N (μ.real univ) (fun i => (x i : ℝ))) := by haveI : ∀ i : Fin N, IsFiniteMeasure (ofReal (μ.real univ / N) • Measure.dirac (x i : ℝ)) := fun _ => Measure.smul_finite _ (by simp) unfold equalAtomMeasure infer_instance have hbound := cdfDistance_le_of_pointwise_cdf_le μ (equalAtomMeasure N (μ.real univ) (fun i => (x i : ℝ))) a b (μ.real univ / N) hab hmass (fun t _ => hx t) calc cdfDistance a b μ (equalAtomMeasure N (μ.real univ) (fun i => (x i : ℝ))) ≤ (b - a) * (μ.real univ / N) := hbound _ = ((b - a) * μ.real univ) / (N : ℝ) := by ring _ < ε := hN₀ N hN₀N