internlm/Lean-Github huggingface dataset:
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), cexp (2 * ↑π * (↑u / (2 * ↑π))) * Ψ (rexp (2 * π * (u / (2 * π)))) =
    ∫ (y : ℝ) in Ioi x⁻¹, Ψ y
Tactic:
norm_cast
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), ↑(rexp (2 * π * (u / (2 * π)))) * Ψ (rexp (2 * π * (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), ↑(rexp (2 * π * (u / (2 * π)))) * Ψ (rexp (2 * π * (u / (2 * π)))) =
    ∫ (y : ℝ) in Ioi x⁻¹, Ψ y
Tactic:
field_simp [why]
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 ↑u * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / 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), cexp ↑u * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Tactic:
norm_cast
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), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / 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), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Tactic:
rw [MeasureTheory.integral_Ici_eq_integral_Ioi]
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
⊢ ∫ (t : ℝ) in Ioi (-x.log), ↑(rexp t) * Ψ (rexp t) = ∫ (y : ℝ) in Ioi (1 / 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
⊢ ∫ (t : ℝ) in Ioi (-x.log), ↑(rexp t) * Ψ (rexp t) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Tactic:
exact wiener_ikehara_smooth_aux hsmooth.continuous hsupp hplus x hx
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
l3 : ∀ᶠ (x : ℝ) in atTop, ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (⇑g) (u / (2 * π)) = ↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y
⊢ Tendsto (fun x => (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
exact wiener_ikehara_smooth_sub (hsmooth.continuous.integrable_of_hasCompactSupport hsupp) hplus
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_real
Proof 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' ∘ Ψ
Proof 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))
Theorem: wiener_ikehara_smooth_real
Proof 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
Proof 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))
Theorem: wiener_ikehara_smooth_real
Proof 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
Proof 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))
Theorem: wiener_ikehara_smooth_real
Proof 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
Proof 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))
Theorem: wiener_ikehara_smooth_real
Proof 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)
Proof 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))
Theorem: wiener_ikehara_smooth_real
Proof 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
Proof 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))
Theorem: wiener_ikehara_smooth_real
Proof 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
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_real
Proof 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]
Proof 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
Theorem: wiener_ikehara_smooth_real
Proof 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
Proof state after:
no goals
Theorem: interval_approx_inf
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ ψ,
      ContDiff ℝ ⊤ ψ ∧
        HasCompactSupport ψ ∧
          closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
have l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0 := nhdsWithin_le_nhds <| Iio_mem_nhds (by linarith)
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ ψ,
      ContDiff ℝ ⊤ ψ ∧
        HasCompactSupport ψ ∧
          closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Theorem: interval_approx_inf
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ ψ,
      ContDiff ℝ ⊤ ψ ∧
        HasCompactSupport ψ ∧
          closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
filter_upwards [self_mem_nhdsWithin, l1] with ε (hε : 0 < ε) (hε' : ε < (b - a) / 3)
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio ((b - a) / 3) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < (b - a) / 3
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ ψ ≤ (Ico a b).indicator 1 ∧ b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y