Theorem: wiener_ikehara_smooth_real (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))
Tactic:
let Ψ' := ofReal' ∘ Ψ
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))
Tactic:
have l1 : ContDiff ℝ ⊤ Ψ' := contDiff_ofReal.comp hsmooth
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))
Tactic:
have l2 : HasCompactSupport Ψ' := hsupp.comp_left rfl
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))
Tactic:
have l3 : closure (Function.support Ψ') ⊆ Ioi 0 := by rwa [Function.support_comp_eq] ; simp
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
l3 : closure (Function.support Ψ') ⊆ Ioi 0
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
l3 : closure (Function.support Ψ') ⊆ Ioi 0
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))
Tactic:
have key := (continuous_re.tendsto _).comp (@wiener_ikehara_smooth' A Ψ G f hf hcheby hG hG' l1 l2 l3)
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
l3 : closure (Function.support Ψ') ⊆ Ioi 0
key :
  Tendsto (re ∘ fun x => (∑' (n : ℕ), (fun n => ↑(f n)) n * (fun n => ↑(Ψ n)) (↑n / x)) / ↑x) atTop
    (𝓝 (↑A * ∫ (y : ℝ) in Ioi 0, (fun n => ↑(Ψ n)) y).re)
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
l3 : closure (Function.support Ψ') ⊆ Ioi 0
key :
  Tendsto (re ∘ fun x => (∑' (n : ℕ), (fun n => ↑(f n)) n * (fun n => ↑(Ψ n)) (↑n / x)) / ↑x) atTop
    (𝓝 (↑A * ∫ (y : ℝ) in Ioi 0, (fun n => ↑(Ψ n)) y).re)
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))
Tactic:
simp at key
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
l3 : closure (Function.support Ψ') ⊆ Ioi 0
key : Tendsto (re ∘ fun x => (∑' (n : ℕ), ↑(f n) * ↑(Ψ (↑n / x))) / ↑x) atTop (𝓝 (A * (∫ (y : ℝ) in Ioi 0, ↑(Ψ y)).re))
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
l3 : closure (Function.support Ψ') ⊆ Ioi 0
key : Tendsto (re ∘ fun x => (∑' (n : ℕ), ↑(f n) * ↑(Ψ (↑n / x))) / ↑x) atTop (𝓝 (A * (∫ (y : ℝ) in Ioi 0, ↑(Ψ y)).re))
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / x) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, Ψ y))
Tactic:
norm_cast at key
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
⊢ closure (Function.support Ψ') ⊆ Ioi 0
Tactic:
rwa [Function.support_comp_eq]
State after:
case hg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
⊢ ∀ {x : ℝ}, ↑x = 0 ↔ x = 0

State before:
case hg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
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}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
Ψ' : ℝ → ℂ := ofReal' ∘ Ψ
l1 : ContDiff ℝ ⊤ Ψ'
l2 : HasCompactSupport Ψ'
⊢ ∀ {x : ℝ}, ↑x = 0 ↔ x = 0
Tactic:
simp
State after:
no goals