Theorem: WienerIkeharaInterval_discrete (PrimeNumberTheoremAnd/Wiener.lean)

State before:
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}
ha : 0 < a
hb : a ≤ b
⊢ Tendsto (fun x => (∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n) / x) atTop (𝓝 (A * (b - a)))
Tactic:
apply (WienerIkeharaInterval hpos hf hcheby hG hG' ha hb).congr'
State after:
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}
ha : 0 < a
hb : a ≤ b
⊢ (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) =ᶠ[atTop] fun x =>
    (∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n) / x

State before:
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}
ha : 0 < a
hb : a ≤ b
⊢ (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) =ᶠ[atTop] fun x =>
    (∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n) / x
Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx
State after:
case h
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}
ha : 0 < a
hb : a ≤ b
x : ℝ
hx : 0 < x
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x = (∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n) / x

State before:
case h
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}
ha : 0 < a
hb : a ≤ b
x : ℝ
hx : 0 < x
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x = (∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n) / x
Tactic:
rw [tsum_indicator hx]
State after:
no goals