hardy_sigma_delayed_tendsto

theorem hardy_sigma_delayed_tendsto (u : ℕ → ℝ) (S : ℝ) (k : ℕ → ℕ)    (h_sigma : Filter.Tendsto (hardy_sigma u) Filter.atTop (nhds S))    (h_bounded : Filter.IsBoundedUnder (· ≤ ·) Filter.atTop (fun (n : ℕ) => (n : ℝ) / k n))    (hk_pos : ∀ n, 0 < k n) :    Filter.Tendsto (fun n => hardy_sigma_delayed u n (k n)) Filter.atTop (nhds S) := by  -- Since $\lim_{n\to\infty} \frac{n}{k_n}$ exists and is finite, we have $\lim_{n\to\infty} \frac{1}{k_n} = 0$.  have h_lim_k_n_inv : Filter.Tendsto (fun n => (1 : ℝ) / (k n)) Filter.atTop (nhds 0) := by    -- Since $k_n$ is bounded above, there exists some $M > 0$ such that $k_n \geq \frac{n}{M}$ for all $n$.    obtain ⟨M, hM⟩ : ∃ M > 0, ∀ n, (k n : ℝ) ≥ n / M := by      obtain ⟨ M, hM ⟩ := h_bounded;      -- Since $k_n$ is bounded above, there exists some $N$ such that for all $n \geq N$, $n / k_n \leq M$.      obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ n ≥ N, (n : ℝ) / (k n : ℝ) ≤ M := by        aesop;      -- Since $k_n$ is bounded above, there exists some $M > 0$ such that for all $n \geq N$, $k_n \geq \frac{n}{M}$.      obtain ⟨M', hM'⟩ : ∃ M' > 0, ∀ n ≥ N, (k n : ℝ) ≥ n / M' := by        exact ⟨ Max.max M 1, by positivity, fun n hn => by rw [ ge_iff_le ] ; rw [ div_le_iff₀ ] <;> nlinarith [ hN n hn, le_max_left M 1, le_max_right M 1, show ( k n : ℝ ) ≥ 1 from mod_cast hk_pos n, div_mul_cancel₀ ( n : ℝ ) ( show ( k n : ℝ ) ≠ 0 from mod_cast ne_of_gt ( hk_pos n ) ) ] ⟩;      -- Since $k_n$ is bounded above, there exists some $M > 0$ such that for all $n < N$, $k_n \geq \frac{n}{M}$.      obtain ⟨M'', hM''⟩ : ∃ M'' > 0, ∀ n < N, (k n : ℝ) ≥ n / M'' := by        field_simp;        exact ⟨ N + 1, by positivity, fun n hn => by rw [ div_le_iff₀ ] <;> nlinarith [ show ( n : ℝ ) + 1 ≤ N by norm_cast, show ( k n : ℝ ) ≥ 1 by exact_mod_cast hk_pos n ] ⟩;      exact ⟨ Max.max M' M'', lt_max_of_lt_left hM'.1, fun n => if hn : n < N then le_trans ( div_le_div_of_nonneg_left ( Nat.cast_nonneg _ ) ( by linarith [ hM''.1 ] ) ( le_max_right _ _ ) ) ( hM''.2 n hn ) else le_trans ( div_le_div_of_nonneg_left ( Nat.cast_nonneg _ ) ( by linarith [ hM'.1 ] ) ( le_max_left _ _ ) ) ( hM'.2 n ( le_of_not_gt hn ) ) ⟩;    refine' tendsto_const_nhds.div_atTop _;    exact Filter.tendsto_atTop_mono hM.2 <| tendsto_natCast_atTop_atTop.atTop_div_const hM.1;  -- Using the fact that $n / k_n$ is bounded, we can apply the squeeze theorem.  have h_squeeze : Filter.Tendsto (fun n => ((n + k n + 1 : ℝ) / (k n)) * (hardy_sigma u (n + k n)) - ((n + 1 : ℝ) / (k n)) * (hardy_sigma u n)) Filter.atTop (nhds S) := by    -- We can split the limit into two parts: the term involving $hardy_sigma u$ and the term involving $1$.    have h_split : Filter.Tendsto (fun n => (hardy_sigma u (n + k n) - hardy_sigma u n) * (n / (k n) : ℝ)) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun n => hardy_sigma u (n + k n) + (hardy_sigma u (n + k n) - hardy_sigma u n) * (1 / (k n) : ℝ)) Filter.atTop (nhds S) := by      constructor;      · -- Since $hardy_sigma u (n + k n) - hardy_sigma u n$ tends to $0$ as $n$ tends to infinity, and $n / k n$ is bounded, their product tends to $0$.        have h_prod_zero : Filter.Tendsto (fun n => hardy_sigma u (n + k n) - hardy_sigma u n) Filter.atTop (nhds 0) := by          simpa using Filter.Tendsto.sub ( h_sigma.comp ( Filter.tendsto_atTop_mono ( fun n => Nat.le_add_right _ _ ) Filter.tendsto_id ) ) h_sigma;        rw [ Metric.tendsto_nhds ] at *;        field_simp;        intro ε hε; rcases h_bounded with ⟨ M, hM ⟩ ; rcases h_prod_zero ( ε / ( Max.max M 1 + 1 ) ) ( by positivity ) with h; filter_upwards [ h, hM ] with n hn hn'; simp_all +decide [ abs_div, abs_mul, div_lt_iff₀ ] ;        rw [ lt_div_iff₀ ( by positivity ) ] at hn;        rw [ div_le_iff₀ ( Nat.cast_pos.mpr ( hk_pos n ) ) ] at hn';        nlinarith [ abs_nonneg ( hardy_sigma u ( n + k n ) - hardy_sigma u n ), show ( k n : ℝ ) ≥ 1 by exact_mod_cast hk_pos n, le_max_left M 1, le_max_right M 1, mul_le_mul_of_nonneg_left ( le_max_left M 1 ) ( show ( 0 : ℝ ) ≤ k n by positivity ), mul_le_mul_of_nonneg_left ( le_max_right M 1 ) ( show ( 0 : ℝ ) ≤ k n by positivity ) ];      · simpa using Filter.Tendsto.add ( h_sigma.comp ( Filter.tendsto_atTop_mono ( fun n => Nat.le_add_right _ _ ) Filter.tendsto_id ) ) ( Filter.Tendsto.mul ( Filter.Tendsto.sub ( h_sigma.comp ( Filter.tendsto_atTop_mono ( fun n => Nat.le_add_right _ _ ) Filter.tendsto_id ) ) h_sigma ) h_lim_k_n_inv );    convert h_split.2.add h_split.1 using 2 <;> ring;    simpa [ ne_of_gt ( hk_pos _ ) ] using by ring;  exact h_squeeze.congr fun n => by rw [ hardy_sigma_delayed_eq _ _ _ ( ne_of_gt ( hk_pos n ) ) ] ;