internlm/Lean-Github huggingface dataset:
Theorem: wiener_ikehara_smooth
Proof state before:
case h.e_f.h
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
⊢ f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = f n * Ψ (↑n / x) / ↑x
Tactic:
by_cases hn : n = 0
Proof state after:
case pos
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : n = 0
⊢ f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = f n * Ψ (↑n / x) / ↑x

case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = f n * Ψ (↑n / x) / ↑x
Theorem: wiener_ikehara_smooth
Proof state before:
case pos
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : n = 0
⊢ f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = f n * Ψ (↑n / x) / ↑x

case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = f n * Ψ (↑n / x) / ↑x
Tactic:
simp [hn, (comp_exp_support0 hplus).self_of_nhds]
Proof state after:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = f n * Ψ (↑n / x) / ↑x
Theorem: wiener_ikehara_smooth
Proof state before:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = f n * Ψ (↑n / x) / ↑x
Tactic:
rw [← l1 (by positivity)]
Proof state after:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n * (↑(↑n / x) * Ψ (↑n / x)) = f n * Ψ (↑n / x) / ↑x
Theorem: wiener_ikehara_smooth
Proof state before:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n * (↑(↑n / x) * Ψ (↑n / x)) = f n * Ψ (↑n / x) / ↑x
Tactic:
have : (n : ℂ) ≠ 0 := by simpa using hn
Proof state after:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ≠ 0
⊢ f n / ↑n * (↑(↑n / x) * Ψ (↑n / x)) = f n * Ψ (↑n / x) / ↑x
Theorem: wiener_ikehara_smooth
Proof state before:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ≠ 0
⊢ f n / ↑n * (↑(↑n / x) * Ψ (↑n / x)) = f n * Ψ (↑n / x) / ↑x
Tactic:
have : (x : ℂ) ≠ 0 := by simpa using hx.ne.symm
Proof state after:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
this✝ : ↑n ≠ 0
this : ↑x ≠ 0
⊢ f n / ↑n * (↑(↑n / x) * Ψ (↑n / x)) = f n * Ψ (↑n / x) / ↑x
Theorem: wiener_ikehara_smooth
Proof state before:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
this✝ : ↑n ≠ 0
this : ↑x ≠ 0
⊢ f n / ↑n * (↑(↑n / x) * Ψ (↑n / x)) = f n * Ψ (↑n / x) / ↑x
Tactic:
field_simp
Proof state after:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
this✝ : ↑n ≠ 0
this : ↑x ≠ 0
⊢ f n * (↑n * Ψ (↑n / x)) * ↑x = f n * Ψ (↑n / x) * (↑n * ↑x)
Theorem: wiener_ikehara_smooth
Proof state before:
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
this✝ : ↑n ≠ 0
this : ↑x ≠ 0
⊢ f n * (↑n * Ψ (↑n / x)) * ↑x = f n * Ψ (↑n / x) * (↑n * ↑x)
Tactic:
ring
Proof state after:
no goals
Theorem: wiener_ikehara_smooth
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ 0 < ↑n / x
Tactic:
positivity
Proof state after:
no goals
Theorem: wiener_ikehara_smooth
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ ↑n ≠ 0
Tactic:
simpa using hn
Proof state after:
no goals
Theorem: wiener_ikehara_smooth
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
x : ℝ
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ≠ 0
⊢ ↑x ≠ 0
Tactic:
simpa using hx.ne.symm
Proof state after:
no goals
Theorem: wiener_ikehara_smooth
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
l2 : ∀ᶠ (x : ℝ) in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = ∑' (n : ℕ), f n * Ψ (↑n / x) / ↑x
⊢ ∀ᶠ (x : ℝ) in atTop, ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)) = ↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y
Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
l2 : ∀ᶠ (x : ℝ) in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = ∑' (n : ℕ), f n * Ψ (↑n / x) / ↑x
x : ℝ
hx : 0 < x
⊢ ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)) = ↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y
Theorem: wiener_ikehara_smooth
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
l2 : ∀ᶠ (x : ℝ) in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = ∑' (n : ℕ), f n * Ψ (↑n / x) / ↑x
x : ℝ
hx : 0 < x
⊢ ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)) = ↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y
Tactic:
congr 1
Proof state after:
case h.e_a
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
l2 : ∀ᶠ (x : ℝ) in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = ∑' (n : ℕ), f n * Ψ (↑n / x) / ↑x
x : ℝ
hx : 0 < x
⊢ ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)) = ∫ (y : ℝ) in Ioi x⁻¹, Ψ y
Theorem: wiener_ikehara_smooth
Proof state before:
case h.e_a
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
l2 : ∀ᶠ (x : ℝ) in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = ∑' (n : ℕ), f n * Ψ (↑n / x) / ↑x
x : ℝ
hx : 0 < x
⊢ ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)) = ∫ (y : ℝ) in Ioi x⁻¹, Ψ y
Tactic:
simp [hg, toSchwartz, h]
Proof state after:
case h.e_a
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hsmooth : ContDiff ℝ ⊤ Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
h : ℝ → ℂ := fun x => ↑(rexp (2 * π * x)) * Ψ (rexp (2 * π * x))
h1 : ContDiff ℝ ⊤ h
h2 : HasCompactSupport h
g : 𝓢(ℝ, ℂ)
hg : 𝓕 ⇑g = ⇑(toSchwartz h h1 h2)
why : ∀ (x : ℝ), 2 * π * x / (2 * π) = x
l1 : ∀ {y : ℝ}, 0 < y → ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
key :
  Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) - ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)))
    atTop (𝓝 0)
l2 : ∀ᶠ (x : ℝ) in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = ∑' (n : ℕ), f n * Ψ (↑n / x) / ↑x
x : ℝ
hx : 0 < x
⊢ ∫ (u : ℝ) in Ici (-x.log), cexp (2 * ↑π * (↑u / (2 * ↑π))) * Ψ (rexp (2 * π * (u / (2 * π)))) =
    ∫ (y : ℝ) in Ioi x⁻¹, Ψ y