limiting_cor_W21

lemma limiting_cor_W21 (ψ : W21) (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ'))    (hcheby : cheby f) (hG : ContinuousOn G {s | 1 ≤ s.re})    (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re}) :    Tendsto (fun x : ℝ ↦ ∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * log (n / x)) -      A * ∫ u in Set.Ici (-log x), 𝓕 (ψ : ℝ → ℂ) (u / (2 * π))) atTop (𝓝 0) := by   -- Shorter notation for clarity  let S1 x (ψ : ℝ → ℂ) := ∑' (n : ℕ), f n / ↑n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * Real.log (↑n / x))  let S2 x (ψ : ℝ → ℂ) := ↑A * ∫ (u : ℝ) in Ici (-Real.log x), 𝓕 (ψ : ℝ → ℂ) (u / (2 * π))  let S x ψ := S1 x ψ - S2 x ψ ; change Tendsto (fun x ↦ S x ψ) atTop (𝓝 0)   -- Build the truncation  obtain g := exists_trunc  let Ψ R := g.scale R * ψ  have key R : Tendsto (fun x ↦ S x (Ψ R)) atTop (𝓝 0) := limiting_cor (Ψ R) hf hcheby hG hG'   -- Choose the truncation radius  obtain ⟨C, hcheby⟩ := hcheby  have hC : 0 ≤ C := by    have : ‖f 0‖ ≤ C := by simpa [cumsum] using hcheby 1    have : 0 ≤ ‖f 0‖ := by positivity    linarith  have key2 : Tendsto (fun R ↦ W21.norm (ψ - Ψ R)) atTop (𝓝 0) := W21_approximation ψ g  simp_rw [Metric.tendsto_nhds] at key key2 ⊢ ; intro ε hε  let M := C * (1 + 2 * π ^ 2) + ‖(A : ℂ)‖ * (2 * π ^ 2)  obtain ⟨R, hRψ⟩ := (key2 ((ε / 2) / (1 + M)) (by positivity)).exists  simp only [dist_zero_right, Real.norm_eq_abs, abs_eq_self.mpr W21.norm_nonneg] at hRψ key   -- Apply the compact support case  filter_upwards [eventually_ge_atTop 1, key R (ε / 2) (by positivity)] with x hx key   -- Control the tail term  have key3 : ‖S x (ψ - Ψ R)‖ < ε / 2 := by    have : ‖S x _‖ ≤ _ * M := @bound_main f C A x hx (ψ - Ψ R) hcheby    apply this.trans_lt    apply (mul_le_mul (d := 1 + M) le_rfl (by simp) (by positivity) W21.norm_nonneg).trans_lt    have : 0 < 1 + M := by positivity    convert! (mul_lt_mul_iff_left₀ this).mpr hRψ using 1 ; field_simp   -- Conclude the proof  have S1_sub_1 x : 𝓕 (⇑ψ - ⇑(Ψ R)) x = 𝓕 (ψ : ℝ → ℂ) x - 𝓕 ⇑(Ψ R) x := by    have l1 : AEStronglyMeasurable (fun x_1 : ℝ ↦ cexp (-(2 * ↑π * (↑x_1 * ↑x) * I))) volume := by      refine (Continuous.mul ?_ continuous_const).neg.cexp.aestronglyMeasurable      apply continuous_const.mul <| contDiff_ofReal.continuous.mul continuous_const    simp only [Real.fourier_eq', neg_mul, RCLike.inner_apply', conj_trivial, ofReal_neg,      ofReal_mul, ofReal_ofNat, Pi.sub_apply, smul_eq_mul, mul_sub]    apply integral_sub    · apply ψ.hf.bdd_mul (c := 1) l1 ; simp [Complex.norm_exp]    · apply (Ψ R : W21) |>.hf |>.bdd_mul (c := 1) l1      simp [Complex.norm_exp]   have S1_sub : S1 x (ψ - Ψ R) = S1 x ψ - S1 x (Ψ R) := by    simp only [one_div, mul_inv_rev, S1_sub_1, mul_sub, S1] ; apply Summable.tsum_sub    · have := summable_fourier x (by positivity) ψ ⟨_, hcheby⟩      rw [summable_norm_iff] at this      simpa using this    · have := summable_fourier x (by positivity) (Ψ R) ⟨_, hcheby⟩      rw [summable_norm_iff] at this      simpa using! this   have S2_sub : S2 x (ψ - Ψ R) = S2 x ψ - S2 x (Ψ R) := by    simp only [S1_sub_1, S2] ; rw [integral_sub]    · ring    · exact ψ.integrable_fourier (by positivity) |>.restrict    · exact (Ψ R : W21).integrable_fourier (by positivity) |>.restrict   have S_sub : S x (ψ - Ψ R) = S x ψ - S x (Ψ R) := by simp [S, S1_sub, S2_sub] ; ring  simpa [S_sub, Ψ] using norm_add_le _ _ |>.trans_lt (_root_.add_lt_add key3 key)