simp only [subset_inter_iff, r3, true_and]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
⊢ Ico 1 2 ⊆ Function.support ψ ∩ Ioi 0
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h4 : (Ico 1 2).indicator 1 ≤ ψ
key : Tendsto (fun x => (∑' (n : ℕ), f n * ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : 0 ≤ ψ
l1 : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S ψ x
l3 : 0 ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
r1 : 0 ≤ᶠ[ae (volume.restrict (Ioi 0))] ψ
r2 : IntegrableOn (fun y => ψ y) (Ioi 0) volume
r3 : Ico 1 2 ⊆ Function.support ψ
⊢ Ico 1 2 ⊆ Ioi 0