wiener_ikehara_smooth_sub

theorem wiener_ikehara_smooth_sub (h1 : Integrable Ψ)    (hplus : closure (Function.support Ψ) ⊆ Ioi 0) :    Tendsto (fun x ↦ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y)      atTop (𝓝 0) := by   obtain ⟨ε, hε, hh⟩ := Metric.eventually_nhds_iff.mp <| comp_exp_support0 hplus  apply tendsto_nhds_of_eventually_eq ; filter_upwards [eventually_gt_atTop ε⁻¹] with x hxε   have l1 : Integrable (indicator (Ioi x⁻¹) (fun x : ℝ => Ψ x)) := h1.indicator measurableSet_Ioi  have l2 : Integrable (indicator (Ioi 0) (fun x : ℝ => Ψ x)) := h1.indicator measurableSet_Ioi   simp_rw [← MeasureTheory.integral_indicator measurableSet_Ioi, ← mul_sub, ← integral_sub l1 l2]  simp only [mul_eq_zero, ofReal_eq_zero]  right  apply MeasureTheory.integral_eq_zero_of_ae  apply Eventually.of_forall  intro t  simp only [Pi.zero_apply]   have hε' : 0 < ε⁻¹ := by positivity  have hx : 0 < x := by linarith  have hx' : 0 < x⁻¹ := by positivity  have hεx : x⁻¹ < ε := (inv_lt_comm₀ hε hx).mp hxε   have l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹ := by    ext t ; simp only [mem_Ioi, mem_union, mem_Ioc] ; constructor <;> intro h    · simp [h, le_or_gt]    · cases h with      | inl h => exact h.1      | inr h => exact hx'.trans h  have l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹) := by simp  have l5 := Set.indicator_union_of_disjoint l4 Ψ  rw [l3, l5]  simp only  rw [add_comm, sub_add_cancel_left]  by_cases ht : t ∈ Ioc 0 x⁻¹  · simp only [ht, indicator_of_mem, neg_eq_zero]    apply hh ; simp only [mem_Ioc, dist_zero_right, norm_eq_abs] at ht ⊢    apply hεx.trans_le'    rw [abs_le] ; constructor <;> linarith  simp [ht]