residue_nonneg

theorem residue_nonneg {f : ℕ → ℝ} (hpos : 0 ≤ f)    (hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n ↦ ↑(f n)) σ')) (hcheby : cheby fun n ↦ ↑(f n))    (hG : ContinuousOn G {s | 1 ≤ s.re}) (hG' : EqOn G (fun s ↦ LSeries (fun n ↦ ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}) : 0 ≤ A := by  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    exact div_nonneg (tsum_nonneg (fun i => mul_nonneg (hpos _) (hg _))) hx  obtain ⟨ε, ψ, h1, h2, h3, h4, -⟩ := (interval_approx_sup zero_lt_one one_lt_two).exists  have key := @wiener_ikehara_smooth_real A G f ψ hf hcheby hG hG' h1 h2 h3  have l2 : 0 ≤ ψ := by apply le_trans _ h4 ; apply indicator_nonneg ; simp  have l1 : ∀ᶠ x in atTop, 0 ≤ S ψ x := hSnonneg l2  have l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y := ge_of_tendsto key l1  have l4 : 0 < ∫ (y : ℝ) in Ioi 0, ψ y := by    have r1 : 0 ≤ᵐ[Measure.restrict volume (Ioi 0)] ψ := Eventually.of_forall l2    have r2 : IntegrableOn (fun y ↦ ψ y) (Ioi 0) volume :=      (h1.continuous.integrable_of_hasCompactSupport h2).integrableOn    have r3 : Ico 1 2 ⊆ Function.support ψ := by intro x hx ; have := h4 x ; simp [hx] at this ⊢ ; linarith    have r4 : Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0 := by      simp only [subset_inter_iff, r3, true_and] ; apply Ico_subset_Icc_self.trans ; rw [Icc_subset_Ioi_iff] <;> linarith    have r5 : 1 ≤ volume ((Function.support fun y ↦ ψ y) ∩ Ioi 0) := by convert! volume.mono r4 ; norm_num    simpa [setIntegral_pos_iff_support_of_nonneg_ae r1 r2] using! zero_lt_one.trans_le r5  have := div_nonneg l3 l4.le ; field_simp at this ; exact this