Mathlib.Probability.Birthday

theorem positiveCeil_mul_div_tendsto (a : ℕ → ℝ) {c : ℝ} (ha : Tendsto a atTop atTop) (hc : 0 < c) : Tendsto (fun j => (positiveCeil (c * a j) : ℝ) / a j) atTop (nhds c) := by have hlarge : ∀ᶠ j in atTop, (1 : ℝ) ≤ c * a j := (ha.const_mul_atTop hc).eventually_ge_atTop 1 apply (tendsto_nat_ceil_mul_div_atTop hc.le).comp ha |>.congr' filter_upwards [hlarge] with j hj simp [positiveCeil, (Nat.one_le_ceil_iff).mpr (lt_of_lt_of_le zero_lt_one hj)]

theorem repeat_le_iff_mStar_le (T m : ℕ) (eta delta : ℝ) (heta : eta ∈ Icc (0 : ℝ) 1) (hdelta : 0 < delta) (hm : 0 < m) : birthdayRepeat T m eta ≤ delta ↔ mStar T eta delta ≤ m := by -- Forward: `Nat.sInf_le`; reverse: `Nat.sInf_mem` and `repeat_antitone`. constructor · intro hle exact Nat.sInf_le (s := {n : ℕ | 0 < n ∧ birthdayRepeat T n eta ≤ delta}) ⟨hm, hle⟩ · intro hle obtain ⟨n, hn, hbound⟩ := threshold_set_nonempty T eta delta heta hdelta have hs : 0 < mStar T eta delta ∧ birthdayRepeat T (mStar T eta delta) eta ≤ delta := by simpa only [mStar, Set.mem_ofPred_eq] using (Nat.sInf_mem (s := {k : ℕ | 0 < k ∧ birthdayRepeat T k eta ≤ delta}) ⟨n, hn, hbound⟩) exact (repeat_antitone T eta hs.1 hle heta).trans hs.2

theorem binomial_relative_deviation_tendsto_zero (Tseq : ℕ → ℕ) (etaseq : ℕ → ℝ) (heta : ∀ j, etaseq j ∈ Icc (0 : ℝ) 1) (hmean : Tendsto (fun j => mean (Tseq j) (etaseq j)) atTop atTop) {eps : ℝ} (heps : 0 < eps) : Tendsto (fun j => binomialAverage (Tseq j) (etaseq j) (fun r => if eps * mean (Tseq j) (etaseq j) ≤ |(r : ℝ) - mean (Tseq j) (etaseq j)| then 1 else 0)) atTop (nhds 0) := by have hpos : ∀ᶠ j : ℕ in atTop, 0 < mean (Tseq j) (etaseq j) := hmean.eventually_gt_atTop 0 have hupper : Tendsto (fun j => (eps ^ 2)⁻¹ * (mean (Tseq j) (etaseq j))⁻¹) atTop (nhds 0) := by simpa using (tendsto_const_nhds (x := (eps ^ 2)⁻¹)).mul (tendsto_inv_atTop_zero.comp hmean) apply squeeze_zero' _ _ hupper · filter_upwards with j exact binomialAverage_nonneg (Tseq j) (etaseq j) _ (heta j) (by intro r _; split_ifs <;> norm_num) · filter_upwards [hpos] with j hj have hband : 0 < eps * mean (Tseq j) (etaseq j) := mul_pos heps hj have hdev := binomialAverage_deviation_le (Tseq j) (heta j) hband have heps0 : eps ≠ 0 := ne_of_gt heps have hmu0 : mean (Tseq j) (etaseq j) ≠ 0 := ne_of_gt hj have hfac : mean (Tseq j) (etaseq j) * (1 - etaseq j) / (eps * mean (Tseq j) (etaseq j)) ^ 2 = (1 - etaseq j) * ((eps ^ 2)⁻¹ * (mean (Tseq j) (etaseq j))⁻¹) := by field_simp rw [hfac] at hdev exact hdev.trans (by have hc : 0 ≤ (eps ^ 2)⁻¹ * (mean (Tseq j) (etaseq j))⁻¹ := by positivity have heta1 : 1 - etaseq j ≤ 1 := by linarith [(heta j).1] simpa using mul_le_mul_of_nonneg_right heta1 hc)

theorem repeat_antitone (T : ℕ) (eta : ℝ) {m n : ℕ} (hm : 0 < m) (hmn : m ≤ n) (heta : eta ∈ Icc (0 : ℝ) 1) : birthdayRepeat T n eta ≤ birthdayRepeat T m eta := by induction n, hmn using Nat.le_induction with | base => exact le_rfl | succ n hmn ih => exact (repeat_antitone_succ T n eta (hm.trans_le hmn) heta).trans ih

theorem repeat_tendsto (Tseq mseq : ℕ → ℕ) (etaseq : ℕ → ℝ) {q : ℝ} (heta : ∀ j, etaseq j ∈ Icc (0 : ℝ) 1) (hmean : Tendsto (fun j => mean (Tseq j) (etaseq j)) atTop atTop) (hm : ∀ j, 0 < mseq j) (hscale : Tendsto (fun j => pairScale (Tseq j) (etaseq j) / (mseq j : ℝ)) atTop (nhds q)) (hq : 0 < q) : Tendsto (fun j => birthdayRepeat (Tseq j) (mseq j) (etaseq j)) atTop (nhds (1 - exp (-q))) := by -- Apply `binomialAverage_tendsto_of_relative_band` to -- `fun j r => repeatKernel (mseq j) r`. The finite kernel bound is -- `repeatKernel_mem_Icc`; rewrite the average by `birthdayRepeat`. have hc : 1 - exp (-q) ∈ Icc (0 : ℝ) 1 := by constructor · have := (Real.exp_le_one_iff).2 (by linarith : -q ≤ 0) linarith · have := Real.exp_nonneg (-q) linarith have hbound : ∀ j r, r ≤ Tseq j → repeatKernel (mseq j) r ∈ Icc (0 : ℝ) 1 := by intro j r _ exact repeatKernel_mem_Icc (mseq j) r (hm j) have h := binomialAverage_tendsto_of_relative_band Tseq etaseq (fun j r => repeatKernel (mseq j) r) (1 - exp (-q)) heta hmean hc hbound (repeatKernel_uniform_on_relative_band Tseq mseq etaseq heta hmean hm hscale hq) simpa only [birthdayRepeat] using h

theorem binomialAverage_tendsto_of_relative_band (Tseq : ℕ → ℕ) (etaseq : ℕ → ℝ) (f : ℕ → ℕ → ℝ) (c : ℝ) (heta : ∀ j, etaseq j ∈ Icc (0 : ℝ) 1) (hmean : Tendsto (fun j => mean (Tseq j) (etaseq j)) atTop atTop) (hc : c ∈ Icc (0 : ℝ) 1) (hbound : ∀ j r, r ≤ Tseq j → f j r ∈ Icc (0 : ℝ) 1) (hband : ∀ δ : ℝ, 0 < δ → ∃ ε : ℝ, 0 < ε ∧ ∀ᶠ j in atTop, ∀ r : ℕ, r ≤ Tseq j → |(r : ℝ) - mean (Tseq j) (etaseq j)| < ε * mean (Tseq j) (etaseq j) → |f j r - c| ≤ δ) : Tendsto (fun j => binomialAverage (Tseq j) (etaseq j) (f j)) atTop (nhds c) := by apply (Metric.tendsto_nhds).2 intro a ha obtain ⟨ε, hε, hbandε⟩ := hband (a / 2) (by positivity) have hbad := binomial_relative_deviation_tendsto_zero Tseq etaseq heta hmean hε have hsmall : ∀ᶠ j in atTop, binomialAverage (Tseq j) (etaseq j) (fun r => if ε * mean (Tseq j) (etaseq j) ≤ |(r : ℝ) - mean (Tseq j) (etaseq j)| then 1 else 0) < a / 2 := by have := (Metric.tendsto_nhds.mp hbad) (a / 2) (by positivity) filter_upwards [this] with j hj have hnn : 0 ≤ binomialAverage (Tseq j) (etaseq j) (fun r => if ε * mean (Tseq j) (etaseq j) ≤ |(r : ℝ) - mean (Tseq j) (etaseq j)| then 1 else 0) := by apply binomialAverage_nonneg (Tseq j) (etaseq j) _ (heta j) intro r _ split_ifs <;> norm_num simpa only [Real.dist_eq, sub_zero, abs_of_nonneg hnn] using hj filter_upwards [hbandε, hsmall] with j hjband hjbad let w : ℕ → ℝ := binomialWeight (Tseq j) (etaseq j) let b : ℕ → ℝ := fun r => if ε * mean (Tseq j) (etaseq j) ≤ |(r : ℝ) - mean (Tseq j) (etaseq j)| then 1 else 0 have hw (r : ℕ) : 0 ≤ w r := by dsimp [w, binomialWeight] exact mul_nonneg (mul_nonneg (Nat.cast_nonneg _) (pow_nonneg (heta j).1 _)) (pow_nonneg (sub_nonneg.mpr (heta j).2) _) have hp (r : ℕ) (hr : r ≤ Tseq j) : |f j r - c| ≤ a / 2 + b r := by dsimp [b] split_ifs with hb · have hf := hbound j r hr have : |f j r - c| ≤ 1 := abs_le.mpr ⟨by linarith [hf.1, hc.2], by linarith [hf.2, hc.1]⟩ linarith [le_of_lt ha] · simpa using hjband r hr (lt_of_not_ge hb) have hdiff : binomialAverage (Tseq j) (etaseq j) (f j) - c = ∑ r ∈ range (Tseq j + 1), w r * (f j r - c) := by calc _ = binomialAverage (Tseq j) (etaseq j) (f j) - c * binomialAverage (Tseq j) (etaseq j) (fun _ => 1) := by rw [binomialAverage_one]; ring _ = ∑ r ∈ range (Tseq j + 1), w r * (f j r - c) := by simp only [binomialAverage, mul_one] rw [Finset.mul_sum, ← Finset.sum_sub_distrib] apply Finset.sum_congr rfl intro r _ dsimp [w] ring have hboundavg : |binomialAverage (Tseq j) (etaseq j) (f j) - c| ≤ a / 2 + binomialAverage (Tseq j) (etaseq j) b := by rw [hdiff] calc |∑ r ∈ range (Tseq j + 1), w r * (f j r - c)| ≤ ∑ r ∈ range (Tseq j + 1), |w r * (f j r - c)| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ r ∈ range (Tseq j + 1), w r * (a / 2 + b r) := by apply Finset.sum_le_sum intro r hr rw [abs_mul, abs_of_nonneg (hw r)] exact mul_le_mul_of_nonneg_left (hp r (Nat.lt_succ_iff.mp (Finset.mem_range.mp hr))) (hw r) _ = a / 2 + binomialAverage (Tseq j) (etaseq j) b := by simp only [mul_add, Finset.sum_add_distrib] rw [← Finset.sum_mul] have hunit : (∑ r ∈ range (Tseq j + 1), w r) = 1 := by simpa [binomialAverage, w] using binomialAverage_one (Tseq j) (etaseq j) rw [hunit] change 1 * (a / 2) + binomialAverage (Tseq j) (etaseq j) b = _ ring change dist (binomialAverage (Tseq j) (etaseq j) (f j)) c < a rw [Real.dist_eq] change binomialAverage (Tseq j) (etaseq j) b < a / 2 at hjbad linarith

theorem pairCount_div_remaining_uniform_on_relative_band (Tseq mseq : ℕ → ℕ) (etaseq : ℕ → ℝ) {q : ℝ} (heta : ∀ j, etaseq j ∈ Icc (0 : ℝ) 1) (hmean : Tendsto (fun j => mean (Tseq j) (etaseq j)) atTop atTop) (hm : ∀ j, 0 < mseq j) (hscale : Tendsto (fun j => pairScale (Tseq j) (etaseq j) / (mseq j : ℝ)) atTop (nhds q)) (hq : 0 < q) : ∀ δ : ℝ, 0 < δ → ∃ ε : ℝ, 0 < ε ∧ ∀ᶠ j in atTop, ∀ r : ℕ, r ≤ mseq j → |(r : ℝ) - mean (Tseq j) (etaseq j)| < ε * mean (Tseq j) (etaseq j) → |(r.choose 2 : ℝ) / (mseq j + 1 - r : ℕ) - q| ≤ δ := by -- On the band, r/m→0 uniformly. Compare denominators using -- (m+1-r)/m = 1 + 1/m - r/m, then apply the full-denominator estimate. intro δ hδ obtain ⟨εa, hεa, ha⟩ := pairCount_div_alphabet_uniform_on_relative_band Tseq mseq etaseq heta hmean hm hscale hq (δ / 2) (by positivity) obtain ⟨εb, hεb, hb⟩ := pairCount_div_alphabet_uniform_on_relative_band Tseq mseq etaseq heta hmean hm hscale hq 1 (by norm_num) let ε : ℝ := min εa (min εb 1) have hε : 0 < ε := lt_min hεa (lt_min hεb (by norm_num)) have hεa' : ε ≤ εa := min_le_left _ _ have hεb' : ε ≤ εb := le_trans (min_le_right _ _) (min_le_left _ _) have hεone : ε ≤ 1 := le_trans (min_le_right _ _) (min_le_right _ _) refine ⟨ε, hε, ?_⟩ have hzero := mean_div_alphabet_tendsto_zero Tseq mseq etaseq heta hmean hm hscale have hQ : 0 < q + 1 := by linarith have hc : 0 < min (1 / 4 : ℝ) (δ / (8 * (q + 1))) := lt_min (by norm_num) (by positivity) have hsmall := hzero.eventually (eventually_lt_nhds hc) have hμpos := hmean.eventually_gt_atTop 0 filter_upwards [ha, hb, hsmall, hμpos] with j haj hbj hs hμ r hrle hr let μ : ℝ := mean (Tseq j) (etaseq j) let m : ℝ := mseq j let c : ℝ := (r.choose 2 : ℝ) let d : ℝ := (mseq j + 1 - r : ℕ) have hmpos : 0 < m := by dsimp [m]; exact_mod_cast hm j have hmne : m ≠ 0 := ne_of_gt hmpos have hbandA : |(r : ℝ) - μ| < εa * μ := by exact lt_of_lt_of_le hr (mul_le_mul_of_nonneg_right hεa' (le_of_lt hμ)) have hbandB : |(r : ℝ) - μ| < εb * μ := by exact lt_of_lt_of_le hr (mul_le_mul_of_nonneg_right hεb' (le_of_lt hμ)) have hnear : |c / m - q| ≤ δ / 2 := haj r hbandA have hupper : c / m ≤ q + 1 := by have ht := hbj r hbandB have := (abs_le.mp ht).2 linarith have hc0 : 0 ≤ c := by dsimp [c]; positivity have hcmax : c ≤ (q + 1) * m := (div_le_iff₀ hmpos).mp hupper have hμquarter : μ < m / 4 := by have ht : μ / m < (1 / 4 : ℝ) := lt_of_lt_of_le hs (min_le_left _ _) have ht' := (div_lt_iff₀ hmpos).mp ht nlinarith have hμdelta : (q + 1) * μ < (δ / 8) * m := by have ht : μ / m < δ / (8 * (q + 1)) := lt_of_lt_of_le hs (min_le_right _ _) have ht' := (lt_div_iff₀ (show 0 < 8 * (q + 1) by positivity)).mp ht have ht'' : μ * (8 * (q + 1)) < δ * m := by calc μ * (8 * (q + 1)) = (μ / m * (8 * (q + 1))) * m := by field_simp _ < δ * m := mul_lt_mul_of_pos_right ht' hmpos nlinarith have hrupper : (r : ℝ) ≤ 2 * μ := by have hh := mul_le_mul_of_nonneg_right hεone (le_of_lt hμ) have ht := (abs_lt.mp hr).2 nlinarith have hrhalf : (r : ℝ) ≤ m / 2 := by linarith have hrdelta : (q + 1) * (r : ℝ) ≤ (δ / 4) * m := by nlinarith [mul_le_mul_of_nonneg_left hrupper (le_of_lt hQ)] have hdidentity : d = m + 1 - (r : ℝ) := by dsimp [d, m] rw [Nat.cast_sub (by omega : r ≤ mseq j + 1)] push_cast ring have hdhalf : m / 2 ≤ d := by rw [hdidentity]; linarith have hdpos : 0 < d := by linarith have hdne : d ≠ 0 := ne_of_gt hdpos by_cases hrzero : r = 0 · subst r have ht : |q| ≤ δ / 2 := by simpa [c] using hnear simpa [c, d] using (le_trans ht (by linarith : δ / 2 ≤ δ)) have hrone : (1 : ℝ) ≤ r := by exact_mod_cast (Nat.one_le_iff_ne_zero.mpr hrzero) have hdiffident : c / d - c / m = c * ((r : ℝ) - 1) / (m * d) := by rw [hdidentity] have hdne' : m + 1 - (r : ℝ) ≠ 0 := by rw [← hdidentity]; exact hdne field_simp [hmne, hdne'] ring have hdiffnonneg : 0 ≤ c / d - c / m := by rw [hdiffident] positivity have hdiffcap : c / d - c / m ≤ δ / 2 := by rw [hdiffident] apply (div_le_iff₀ (mul_pos hmpos hdpos)).mpr have h1 : c * ((r : ℝ) - 1) ≤ c * (r : ℝ) := by nlinarith have h2 : c * (r : ℝ) ≤ ((q + 1) * m) * (r : ℝ) := mul_le_mul_of_nonneg_right hcmax (by positivity) have h3 : ((q + 1) * m) * (r : ℝ) ≤ (δ / 4) * m ^ 2 := by nlinarith [mul_le_mul_of_nonneg_right hrdelta (le_of_lt hmpos)] have h4 : (δ / 4) * m ^ 2 ≤ (δ / 2) * (m * d) := by nlinarith [mul_le_mul_of_nonneg_left hdhalf (by positivity : 0 ≤ (δ / 2) * m)] exact le_trans h1 (le_trans h2 (le_trans h3 h4)) have hfinal : |c / d - q| ≤ δ := by calc |c / d - q| = |(c / d - c / m) + (c / m - q)| := by congr 1; ring _ ≤ |c / d - c / m| + |c / m - q| := abs_add_le _ _ _ ≤ δ := by rw [abs_of_nonneg hdiffnonneg]; linarith simpa [c, d] using hfinal

theorem pairScale_div_half_mean_sq_tendsto_one (Tseq : ℕ → ℕ) (etaseq : ℕ → ℝ) (heta : ∀ j, etaseq j ∈ Icc (0 : ℝ) 1) (hmean : Tendsto (fun j => mean (Tseq j) (etaseq j)) atTop atTop) : Tendsto (fun j => pairScale (Tseq j) (etaseq j) / (mean (Tseq j) (etaseq j) ^ 2 / 2)) atTop (nhds 1) := by have hpos : ∀ᶠ j : ℕ in atTop, 0 < mean (Tseq j) (etaseq j) := hmean.eventually_gt_atTop 0 have hinv : Tendsto (fun j => (mean (Tseq j) (etaseq j))⁻¹) atTop (nhds 0) := tendsto_inv_atTop_zero.comp hmean have hratio : Tendsto (fun j => etaseq j / mean (Tseq j) (etaseq j)) atTop (nhds 0) := by apply squeeze_zero' _ _ hinv · filter_upwards [hpos] with j hj exact div_nonneg (heta j).1 (le_of_lt hj) · filter_upwards [hpos] with j hj simpa [div_eq_mul_inv] using mul_le_mul_of_nonneg_right (heta j).2 (inv_nonneg.mpr (le_of_lt hj)) have hlim : Tendsto (fun j => 1 - etaseq j / mean (Tseq j) (etaseq j)) atTop (nhds 1) := by simpa using (tendsto_const_nhds (x := (1 : ℝ))).sub hratio apply hlim.congr' filter_upwards [hpos] with j hj have hmu : mean (Tseq j) (etaseq j) ≠ 0 := ne_of_gt hj have hident : 2 * pairScale (Tseq j) (etaseq j) = mean (Tseq j) (etaseq j) * (mean (Tseq j) (etaseq j) - etaseq j) := by simp only [pairScale, mean, Nat.cast_choose_two] ring field_simp [hmu] nlinarith [hident]

theorem binomialAverage_pairs (T : ℕ) (eta : ℝ) : binomialAverage T eta (fun r => (r.choose 2 : ℝ)) = pairScale T eta := by by_cases hT : T < 2 · interval_cases T <;> norm_num [binomialAverage, pairScale, binomialWeight, Finset.sum_range_succ] · have hT2 : 2 ≤ T := by omega unfold binomialAverage pairScale calc (∑ r ∈ range (T + 1), binomialWeight T eta r * (r.choose 2 : ℝ)) = ∑ j ∈ range (T - 1), (T.choose 2 : ℝ) * eta ^ 2 * binomialWeight (T - 2) eta j := by rw [Finset.sum_range_succ' (f := fun r => binomialWeight T eta r * (r.choose 2 : ℝ))] simp only [Nat.choose_zero_succ, Nat.cast_zero, mul_zero, add_zero] rw [show T = (T - 1) + 1 by omega, Finset.sum_range_succ' (f := fun j => binomialWeight (T - 1 + 1) eta (j + 1) * ((j + 1).choose 2 : ℝ))] simp only [Nat.sub_add_cancel (show 1 ≤ T by omega)] simp only [Nat.zero_add, show (1 : ℕ).choose 2 = 0 by decide, Nat.cast_zero, mul_zero, add_zero] apply Finset.sum_congr rfl intro j hj have hjlt : j < T - 1 := Finset.mem_range.mp hj have hchoose : (T.choose (j + 2) : ℝ) * ((j + 2).choose 2 : ℝ) = (T.choose 2 : ℝ) * ((T - 2).choose j : ℝ) := by have h := Nat.choose_mul (n := T) (k := j + 2) (s := 2) (by omega) have h' : T.choose (j + 2) * (j + 2).choose 2 = T.choose 2 * (T - 2).choose j := by simpa [show j + 2 - 2 = j by omega] using h exact_mod_cast h' have hsub : T - (j + 2) = (T - 2) - j := by omega simp only [binomialWeight, hsub, show j + 1 + 1 = j + 2 by omega, pow_add] calc (T.choose (j + 2) : ℝ) * (eta ^ j * eta ^ 2) * (1 - eta) ^ (T - 2 - j) * ((j + 2).choose 2 : ℝ) = ((T.choose (j + 2) : ℝ) * ((j + 2).choose 2 : ℝ)) * eta ^ 2 * (eta ^ j * (1 - eta) ^ (T - 2 - j)) := by ring _ = _ := by rw [hchoose]; ring _ = (T.choose 2 : ℝ) * eta ^ 2 * binomialAverage (T - 2) eta (fun _ => 1) := by simp only [binomialAverage, mul_one] rw [show T - 1 = (T - 2) + 1 by omega, Finset.mul_sum] _ = (T.choose 2 : ℝ) * eta ^ 2 := by rw [binomialAverage_one]; ring

theorem mStar_div_calibratedScale_tendsto_one (Tseq : ℕ → ℕ) (etaseq : ℕ → ℝ) {delta : ℝ} (heta : ∀ j, etaseq j ∈ Icc (0 : ℝ) 1) (hmean : Tendsto (fun j => mean (Tseq j) (etaseq j)) atTop atTop) (hdelta : delta ∈ Ioo (0 : ℝ) 1) : Tendsto (fun j => (mStar (Tseq j) (etaseq j) delta : ℝ) / (pairScale (Tseq j) (etaseq j) / (-log (1 - delta)))) atTop (nhds 1) := by -- Set L = -log (1-delta) > 0 and a_j = pairScale_j/L, with a_j → ∞. -- Fix 0 < c₋ < 1 < c₊. At positiveCeil(c*a_j), `repeat_tendsto` -- and `pairScale_div_positiveCeil_tendsto` give limit 1-exp(-L/c). -- This is strictly above delta for c₋ and strictly below it for c₊; -- use `Real.exp_neg_log` / `Real.exp_log` and monotonicity of exp to -- identify delta = 1-exp(-L). Eventual strict inequalities and -- `repeat_le_iff_mStar_le` imply -- positiveCeil(c₋*a_j) < mStar_j ≤ positiveCeil(c₊*a_j). -- Divide by eventually positive a_j and apply -- `positiveCeil_mul_div_tendsto` for the two boundaries. To show -- convergence to 1, use `LinearOrderedAddCommGroup.tendsto_nhds`: -- for each ε>0 choose c₋ = 1-min (ε/2) (1/2) and c₊ = 1+ε/2, -- and combine the eventual bounds with the limits c₋ and c₊. let L : ℝ := -log (1 - delta) let a : ℕ → ℝ := fun j => pairScale (Tseq j) (etaseq j) / L let r : ℕ → ℝ := fun j => (mStar (Tseq j) (etaseq j) delta : ℝ) / a j have hL : 0 < L := neg_log_one_sub_pos hdelta have ha : Tendsto a atTop atTop := calibratedScale_tendsto_atTop Tseq etaseq heta hmean hdelta have hexp : exp (-L) = 1 - delta := by dsimp [L] rw [neg_neg, Real.exp_log (by linarith [hdelta.2])] have hboundary (c : ℝ) (hc : 0 < c) : Tendsto (fun j => birthdayRepeat (Tseq j) (positiveCeil (c * a j)) (etaseq j)) atTop (nhds (1 - exp (-(L / c)))) := by apply repeat_tendsto Tseq (fun j => positiveCeil (c * a j)) etaseq heta hmean (fun j => positiveCeil_pos _) · simpa only [a, L] using pairScale_div_positiveCeil_tendsto Tseq etaseq heta hmean hdelta hc · exact div_pos hL hc have hbelow (c : ℝ) (hc : 0 < c) (hc1 : c < 1) : ∀ᶠ j in atTop, (positiveCeil (c * a j) : ℝ) / a j < r j := by have hq : L < L / c := by apply (lt_div_iff₀ hc).2 nlinarith [mul_pos hL (sub_pos.mpr hc1)] have hlimit : delta < 1 - exp (-(L / c)) := by have he := Real.exp_strictMono (show -(L / c) < -L by linarith) linarith [hexp] have hev := (hboundary c hc).eventually (eventually_gt_nhds hlimit) filter_upwards [hev, ha.eventually_gt_atTop 0] with j hj haj have hm : positiveCeil (c * a j) < mStar (Tseq j) (etaseq j) delta := by by_contra hn have hle := (repeat_le_iff_mStar_le (Tseq j) (positiveCeil (c * a j)) (etaseq j) delta (heta j) hdelta.1 (positiveCeil_pos _)).2 (Nat.le_of_not_gt hn) exact (not_le_of_gt hj) hle exact (div_lt_div_iff_of_pos_right haj).2 (by exact_mod_cast hm) have habove (c : ℝ) (hc : 1 < c) : ∀ᶠ j in atTop, r j ≤ (positiveCeil (c * a j) : ℝ) / a j := by have hc0 : 0 < c := by linarith have hq : L / c < L := by apply (div_lt_iff₀ hc0).2 nlinarith [mul_pos hL (sub_pos.mpr hc)] have hlimit : 1 - exp (-(L / c)) < delta := by have he := Real.exp_strictMono (show -L < -(L / c) by linarith) linarith [hexp] have hev := (hboundary c hc0).eventually (eventually_lt_nhds hlimit) filter_upwards [hev, ha.eventually_gt_atTop 0] with j hj haj have hm : mStar (Tseq j) (etaseq j) delta ≤ positiveCeil (c * a j) := (repeat_le_iff_mStar_le (Tseq j) (positiveCeil (c * a j)) (etaseq j) delta (heta j) hdelta.1 (positiveCeil_pos _)).1 hj.le exact (div_le_div_iff_of_pos_right haj).2 (by exact_mod_cast hm) change Tendsto r atTop (nhds 1) apply tendsto_order.2 constructor · intro b hb let c : ℝ := max (1 / 2) ((b + 1) / 2) have hc : 0 < c := lt_of_lt_of_le (by norm_num) (le_max_left _ _) have hc1 : c < 1 := max_lt (by norm_num) (by dsimp [c] at *; linarith) have hbc : b < c := by dsimp [c] exact lt_of_lt_of_le (by linarith) (le_max_right _ _) filter_upwards [hbelow c hc hc1, (positiveCeil_mul_div_tendsto a ha hc).eventually (eventually_gt_nhds hbc)] with j hj hjc exact lt_trans hjc hj · intro b hb let c : ℝ := (b + 1) / 2 have hc : 1 < c := by dsimp [c]; linarith have hcb : c < b := by dsimp [c]; linarith filter_upwards [habove c hc, (positiveCeil_mul_div_tendsto a ha (by linarith : 0 < c)).eventually (eventually_lt_nhds hcb)] with j hj hjc exact lt_of_le_of_lt hj hjc

theorem pairScale_div_positiveCeil_tendsto (Tseq : ℕ → ℕ) (etaseq : ℕ → ℝ) {delta c : ℝ} (heta : ∀ j, etaseq j ∈ Icc (0 : ℝ) 1) (hmean : Tendsto (fun j => mean (Tseq j) (etaseq j)) atTop atTop) (hdelta : delta ∈ Ioo (0 : ℝ) 1) (hc : 0 < c) : Tendsto (fun j => pairScale (Tseq j) (etaseq j) / (positiveCeil (c * (pairScale (Tseq j) (etaseq j) / (-log (1 - delta)))) : ℝ)) atTop (nhds ((-log (1 - delta)) / c)) := by let L : ℝ := -log (1 - delta) let a : ℕ → ℝ := fun j => pairScale (Tseq j) (etaseq j) / L have hL : 0 < L := neg_log_one_sub_pos hdelta have ha : Tendsto a atTop atTop := calibratedScale_tendsto_atTop Tseq etaseq heta hmean hdelta have hround : Tendsto (fun j => (positiveCeil (c * a j) : ℝ) / a j) atTop (nhds c) := positiveCeil_mul_div_tendsto a ha hc have hlim : Tendsto (fun j => L / ((positiveCeil (c * a j) : ℝ) / a j)) atTop (nhds (L / c)) := tendsto_const_nhds.div hround hc.ne' change Tendsto (fun j => pairScale (Tseq j) (etaseq j) / (positiveCeil (c * a j) : ℝ)) atTop (nhds (L / c)) apply hlim.congr' filter_upwards [ha.eventually_gt_atTop 0] with j hj have hceil : (positiveCeil (c * a j) : ℝ) ≠ 0 := by exact_mod_cast (positiveCeil_pos (c * a j)).ne' have hane : a j ≠ 0 := hj.ne' have hident : pairScale (Tseq j) (etaseq j) = a j * L := by dsimp [a] field_simp [hL.ne'] rw [hident] field_simp