Limiting fourier variant

@[blueprint "limiting-fourier-variant"  (title := "limiting-fourier-variant")  (statement := /--    If $\psi: \R \to \C$ is $C^2$ and compactly supported with $f$ and $\hat \psi$ non-negative, and $0 < x$, then  $$ \sum_{n=1}^\infty \frac{f(n)}{n} \hat \psi( \frac{1}{2\pi} \log \frac{n}{x} ) - A \int_{-\log x}^\infty \hat \psi(\frac{u}{2\pi})\ du =  \int_\R G(1+it) \psi(t) x^{it}\ dt.$$  -/)  (proof := /-- Repeat the proof of Lemma \ref{limiting-fourier-variant}, but use monotone convergence instead of dominated convergence.  (The proof should be simpler, as one no longer needs to establish domination for the sum.) -/)  (proofUses := ["decay", "second-fourier", "first-fourier"])  (latexEnv := "lemma")]lemma limiting_fourier_variant    (hpos : 0 ≤ f)    (hG : ContinuousOn G {s | 1 ≤ s.re})    (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})    (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ'))    (ψ : CS 2 ℂ)    (hψpos : ∀ y, 0 ≤ (𝓕 (ψ : ℝ → ℂ) y).re ∧ (𝓕 (ψ : ℝ → ℂ) y).im = 0)    (hx : 0 < x) :    ∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * log (n / x)) -      A * ∫ u in Set.Ici (-log x), 𝓕 (ψ : ℝ → ℂ) (u / (2 * π)) =      ∫ (t : ℝ), (G (1 + t * I)) * (ψ t) * x ^ (t * I) := by   have l2 := limiting_fourier_lim2_gt_zero (A := A) (x := x) ψ hx  have l3 := limiting_fourier_lim3_gt_zero (G := G) (x := x) hG ψ hx   let S : ℝ → ℂ := fun σ' =>    ∑' n : ℕ,      term (fun n ↦ (f n : ℂ)) σ' n *        𝓕 ψ.toFun (1 / (2 * π) * Real.log ((n : ℝ) / x))  let Pole : ℝ → ℂ := fun σ' =>    (A : ℂ) * ((x ^ (1 - σ') : ℝ) : ℂ) *      ∫ u in Set.Ici (-Real.log x),        (rexp (-u * (σ' - 1)) : ℂ) *          𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))  let RHS : ℝ → ℂ := fun σ' =>    ∫ t : ℝ, G (σ' + t * I) * ψ.toFun t * (x : ℂ) ^ (t * I)    have haux :    (fun σ' ↦        ∑' (n : ℕ),          term (fun n ↦ (f n : ℂ)) (σ' : ℂ) n *            𝓕 ψ.toFun (π⁻¹ * 2⁻¹ * Real.log ((n : ℝ) / x))        - (A : ℂ) * ((x ^ (1 - σ') : ℝ) : ℂ) *          ∫ (u : ℝ) in Ici (-Real.log x),            cexp (-( (u : ℂ) * ((σ' : ℂ) - 1))) *              𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π)))      =ᶠ[𝓝[>] (1 : ℝ)]    (fun σ' ↦      ∫ (t : ℝ), G ((σ' : ℂ) + (t : ℂ) * I) * ψ.toFun t * (x : ℂ) ^ ((t : ℂ) * I)) := by    rw [Filter.EventuallyEq]     refine eventually_nhdsWithin_of_forall ?_    intro σ' hσ'    have hσ' : (1 : ℝ) < σ' := by      simpa [Set.mem_Ioi] using hσ'    simpa using! (limiting_fourier_aux_gt_zero (G := G) (f := f) (A := A) hG' hf ψ hx σ' hσ')   have haux' :    (fun σ' : ℝ => S σ') =ᶠ[𝓝[>] (1 : ℝ)] (fun σ' : ℝ => RHS σ' + Pole σ') := by    rw [Filter.EventuallyEq] at haux ⊢    filter_upwards [haux] with σ' hσ'    have hσ'' : S σ' - Pole σ' = RHS σ' := by      simpa [S, Pole, RHS] using hσ'    have hadd : (S σ' - Pole σ') + Pole σ' = RHS σ' + Pole σ' :=      congrArg (fun z : ℂ => z + Pole σ') hσ''    simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using hadd   let Pole₁ : ℂ := (A : ℂ) * ∫ u in Set.Ici (-Real.log x), 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))  let RHS₁ : ℂ := ∫ t : ℝ, G (1 + (t : ℂ) * I) * ψ.toFun t * (x : ℂ) ^ ((t : ℂ) * I)   have hRHS_le :      ∀ᶠ σ' : ℝ in 𝓝[>] (1 : ℝ), ‖RHS σ'‖ ≤ ‖RHS₁‖ + 1 := by    have hball : Metric.ball RHS₁ (1 : ℝ) ∈ 𝓝 RHS₁ := by      simpa using (Metric.ball_mem_nhds (x := RHS₁) (ε := (1 : ℝ)) (by norm_num))    have hpre : {σ' : ℝ | RHS σ' ∈ Metric.ball RHS₁ (1 : ℝ)} ∈ (𝓝[>] (1 : ℝ)) :=      l3 hball    filter_upwards [hpre] with σ' hmem    have hdist' : dist (RHS σ') RHS₁ < (1 : ℝ) := by      simpa [Metric.mem_ball] using hmem    have hdist : ‖RHS σ' - RHS₁‖ < (1 : ℝ) := by      simpa [dist_eq_norm] using hdist'    have htri : ‖RHS σ'‖ ≤ ‖RHS₁‖ + ‖RHS σ' - RHS₁‖ := by      have h := norm_add_le (RHS σ' - RHS₁) RHS₁      simpa [sub_add_cancel, add_comm, add_left_comm, add_assoc] using h    have hle : ‖RHS₁‖ + ‖RHS σ' - RHS₁‖ ≤ ‖RHS₁‖ + (1 : ℝ) := by      exact add_le_add_right (le_of_lt hdist) ‖RHS₁‖    exact htri.trans hle   have hPole_le :    ∀ᶠ σ' : ℝ in 𝓝[>] (1 : ℝ), ‖Pole σ'‖ ≤ ‖Pole₁‖ + 1 := by    have hball : Metric.ball Pole₁ 1 ∈ 𝓝 Pole₁ := by      simpa using (Metric.ball_mem_nhds Pole₁ (by norm_num : (0 : ℝ) < 1))    have hpre : {σ' : ℝ | Pole σ' ∈ Metric.ball Pole₁ 1} ∈ (𝓝[>] (1 : ℝ)) := l2 hball    filter_upwards [hpre] with σ' hmem    have hdist : ‖Pole σ' - Pole₁‖ < 1 := by      simpa [Metric.mem_ball, dist_eq_norm] using hmem    have htri : ‖Pole σ'‖ ≤ ‖Pole₁‖ + ‖Pole σ' - Pole₁‖ := by      have hdecomp : Pole σ' = Pole₁ + (Pole σ' - Pole₁) := by abel      have hnorm_eq : ‖Pole σ'‖ = ‖Pole₁ + (Pole σ' - Pole₁)‖ := by        simp [congrArg (fun z : ℂ => ‖z‖) hdecomp]      calc        ‖Pole σ'‖ = ‖Pole₁ + (Pole σ' - Pole₁)‖ := hnorm_eq        _ ≤ ‖Pole₁‖ + ‖Pole σ' - Pole₁‖ := norm_add_le _ _    have hdist_le : ‖Pole σ' - Pole₁‖ ≤ 1 := le_of_lt hdist    have hsum : ‖Pole₁‖ + ‖Pole σ' - Pole₁‖ ≤ ‖Pole₁‖ + 1 := by      simpa [add_comm, add_left_comm, add_assoc] using (add_le_add_left hdist_le ‖Pole₁‖)    exact htri.trans hsum   have hS_le :      ∀ᶠ σ' : ℝ in 𝓝[>] (1 : ℝ),        ‖S σ'‖ ≤ (‖RHS₁‖ + 1) + (‖Pole₁‖ + 1) := by    rw [Filter.EventuallyEq] at haux'    filter_upwards [haux', hRHS_le, hPole_le] with σ' hEq hR hP    calc      ‖S σ'‖ = ‖RHS σ' + Pole σ'‖ := by simp [hEq]      _ ≤ ‖RHS σ'‖ + ‖Pole σ'‖ := norm_add_le _ _      _ ≤ (‖RHS₁‖ + 1) + (‖Pole₁‖ + 1) := by        exact add_le_add hR hP   have hbounded : BoundedAtFilter (𝓝[>] (1 : ℝ)) (fun σ' : ℝ => ‖S σ'‖) := by    let C : ℝ := ‖RHS₁‖ + 1 + (‖Pole₁‖ + 1)    simp only [BoundedAtFilter, Asymptotics.IsBigO, Asymptotics.IsBigOWith]    refine ⟨C, ?_⟩    filter_upwards [hS_le] with σ' hσ'    simpa [Real.norm_eq_abs, abs_of_nonneg (norm_nonneg (S σ'))] using hσ'   have hcoef : (1 / (2 * π) : ℝ) = (π⁻¹ * 2⁻¹ : ℝ) := by field_simp [pi_ne_zero]   have l1 :=    limiting_fourier_variant_lim1      (f := f) (x := x) (ψ := ψ)      hpos hψpos      (S := S)      (hSdef := by        intro σ        simp [S, hcoef] )      hbounded      hf  have l1S :    Tendsto S (𝓝[>] (1 : ℝ))      (𝓝 (∑' n : ℕ, (f n : ℂ) / (n : ℂ) * 𝓕 ψ.toFun (1 / (2 * π) * Real.log (↑n / x)))) := by    simpa [S, hcoef] using l1   have l12 : Tendsto (fun σ' : ℝ => S σ' - Pole σ') (𝓝[>] (1 : ℝ))    (𝓝 ((∑' n : ℕ, (f n : ℂ) / (n : ℂ) * 𝓕 ψ.toFun (1 / (2 * π) * Real.log (↑n / x))) - Pole₁)) :=  l1S.sub l2   have hPole : (Pole : ℝ → ℂ) =ᶠ[𝓝[>] (1 : ℝ)] Pole := by simp  have haux_sub :    (fun σ' : ℝ => S σ' - Pole σ') =ᶠ[𝓝[>] (1 : ℝ)] RHS := by    filter_upwards [haux'] with σ' hσ'    calc      S σ' - Pole σ'          = (RHS σ' + Pole σ') - Pole σ' := by simp [hσ']      _   = RHS σ' := by simp  have hlim :=    tendsto_nhds_unique_of_eventuallyEq (l1S.sub l2) l3 haux_sub   simpa [Pole₁, RHS₁] using! hlim