WienerIkeharaInterval

@[blueprint  (title := "Wiener-Ikehara in an interval")  (statement := /--  For any closed interval $I \subset (0,+\infty)$, we have  $$ \sum_{n=1}^\infty f(n) 1_I( \frac{n}{x} ) = A x |I|  + o(x).$$  -/)  (proof := /-- Use Lemma \ref{smooth-ury} to bound $1_I$ above and below by smooth compactly supported functions whose integral is close to the measure of $|I|$, and use the non-negativity of $f$. -/)  (latexEnv := "proposition")]lemma WienerIkeharaInterval {f : ℕ → ℝ} (hpos : 0 ≤ f) (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}) (ha : 0 < a) (hb : a ≤ b) :    Tendsto (fun x : ℝ ↦ (∑' n, f n * (indicator (Ico a b) 1 (n / x))) / x) atTop (nhds (A * (b - a))) := by   -- Take care of the trivial case `a = b`  by_cases hab : a = b  · simp [hab]  replace hb : a < b := lt_of_le_of_ne hb hab ; clear hab   -- Notation to make the proof more readable  let S (g : ℝ → ℝ) (x : ℝ) :=  (∑' n, f n * g (n / x)) / x  have hSnonneg {g : ℝ → ℝ} (hg : 0 ≤ g) : ∀ᶠ x : ℝ in atTop, 0 ≤ S g x := by    filter_upwards [eventually_ge_atTop 0] with x hx    refine div_nonneg ?_ hx    refine tsum_nonneg (fun i => mul_nonneg (hpos _) (hg _))  have hA : 0 ≤ A := residue_nonneg hpos hf hcheby hG hG'   -- A few facts about the indicator function of `Icc a b`  let Iab : ℝ → ℝ := indicator (Ico a b) 1  change Tendsto (S Iab) atTop (𝓝 (A * (b - a)))  have hIab : HasCompactSupport Iab := by simpa [Iab, HasCompactSupport, tsupport, hb.ne] using isCompact_Icc  have Iab_nonneg : ∀ᶠ x : ℝ in atTop, 0 ≤ S Iab x := hSnonneg (indicator_nonneg (by simp))  have Iab2 : IsBoundedUnder (· ≤ ·) atTop (S Iab) := by    obtain ⟨C, hC⟩ := hcheby ; exact ⟨C * 2 * b, WI_sum_Iab_le' hpos hC (by linarith)⟩  have Iab3 : IsBoundedUnder (· ≥ ·) atTop (S Iab) := ⟨0, Iab_nonneg⟩  have Iab0 : IsCoboundedUnder (· ≥ ·) atTop (S Iab) := Iab2.isCoboundedUnder_ge  have Iab1 : IsCoboundedUnder (· ≤ ·) atTop (S Iab) := Iab3.isCoboundedUnder_le   -- Bound from above by a smooth function  have sup_le : limsup (S Iab) atTop ≤ A * (b - a) := by    have l_sup : ∀ᶠ ε in 𝓝[>] 0, limsup (S Iab) atTop ≤ A * (b - a + ε) := by      filter_upwards [interval_approx_sup ha hb] with ε ⟨ψ, h1, h2, h3, h4, h6⟩      have l1 : Tendsto (S ψ) atTop _ := wiener_ikehara_smooth_real hf hcheby hG hG' h1 h2 h3      have l6 : S Iab ≤ᶠ[atTop] S ψ := by        filter_upwards [eventually_gt_atTop 0] with x hx using WI_sum_le hpos h4 hx hIab h2      have l5 : IsBoundedUnder (· ≤ ·) atTop (S ψ) := l1.isBoundedUnder_le      have l3 : limsup (S Iab) atTop ≤ limsup (S ψ) atTop := limsup_le_limsup l6 Iab1 l5      apply l3.trans ; rw [l1.limsup_eq] ; gcongr    obtain rfl | h := eq_or_ne A 0    · simpa using l_sup    apply le_of_eventually_nhdsWithin    have key : 0 < A := lt_of_le_of_ne hA h.symm    filter_upwards [WI_tendsto_aux a b key l_sup] with x hx    simpa [mul_div_cancel₀ _ h] using hx   -- Bound from below by a smooth function  have le_inf : A * (b - a) ≤ liminf (S Iab) atTop := by    have l_inf : ∀ᶠ ε in 𝓝[>] 0, A * (b - a - ε) ≤ liminf (S Iab) atTop := by      filter_upwards [interval_approx_inf ha hb] with ε ⟨ψ, h1, h2, h3, h5, h6⟩      have l1 : Tendsto (S ψ) atTop _ := wiener_ikehara_smooth_real hf hcheby hG hG' h1 h2 h3      have l2 : S ψ ≤ᶠ[atTop] S Iab := by        filter_upwards [eventually_gt_atTop 0] with x hx using WI_sum_le hpos h5 hx h2 hIab      have l4 : IsBoundedUnder (· ≥ ·) atTop (S ψ) := l1.isBoundedUnder_ge      have l3 : liminf (S ψ) atTop ≤ liminf (S Iab) atTop := liminf_le_liminf l2 l4 Iab0      apply le_trans ?_ l3 ; rw [l1.liminf_eq] ; gcongr    obtain rfl | h := eq_or_ne A 0    · simpa using l_inf    apply ge_of_eventually_nhdsWithin    have key : 0 < A := lt_of_le_of_ne hA h.symm    filter_upwards [WI_tendsto_aux' a b key l_inf] with x hx    simpa [mul_div_cancel₀ _ h] using hx   -- Combine the two bounds  have : liminf (S Iab) atTop ≤ limsup (S Iab) atTop := liminf_le_limsup Iab2 Iab3  refine tendsto_of_liminf_eq_limsup ?_ ?_ Iab2 Iab3 <;> linarith