internlm/Lean-Github huggingface dataset:
Theorem: wiener_ikehara_smooth
Proof state before:
case intro
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
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
have l3 : ∀ᶠ x in atTop, ↑A * ∫ (u : ℝ) in Ici (-Real.log x), 𝓕 (⇑g) (u / (2 * π)) =
    ↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y := by
  filter_upwards [eventually_gt_atTop 0] with x hx
  congr 1 ; simp [hg, toSchwartz, h] ; norm_cast ; field_simp [why] ; norm_cast
  rw [MeasureTheory.integral_Ici_eq_integral_Ioi]
  exact wiener_ikehara_smooth_aux hsmooth.continuous hsupp hplus x hx
Proof state after:
case intro
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 => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Theorem: wiener_ikehara_smooth
Proof state before:
case intro
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 => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
have l4 : Tendsto (fun x => (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0) := by
  exact wiener_ikehara_smooth_sub (hsmooth.continuous.integrable_of_hasCompactSupport hsupp) hplus
Proof state after:
case intro
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
l4 : Tendsto (fun x => (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Theorem: wiener_ikehara_smooth
Proof state before:
case intro
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
l4 : Tendsto (fun x => (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
simpa [tsum_div_const] using (key.congr' <| EventuallyEq.sub l2 l3) |>.add l4
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))
⊢ ContDiff ℝ ⊤ h
Tactic:
have : ContDiff ℝ ⊤ (fun x : ℝ => (rexp (2 * π * x))) := (contDiff_const.mul contDiff_id).exp
Proof state after:
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))
this : ContDiff ℝ ⊤ fun x => rexp (2 * π * x)
⊢ ContDiff ℝ ⊤ h
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))
this : ContDiff ℝ ⊤ fun x => rexp (2 * π * x)
⊢ ContDiff ℝ ⊤ h
Tactic:
exact (contDiff_ofReal.comp this).mul (hsmooth.comp this)
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
⊢ HasCompactSupport h
Tactic:
have : 2 * π ≠ 0 := by simp [pi_ne_zero]
Proof state after:
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
this : 2 * π ≠ 0
⊢ HasCompactSupport h
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
this : 2 * π ≠ 0
⊢ HasCompactSupport h
Tactic:
simpa using (comp_exp_support hsupp hplus).comp_smul this |>.mul_left
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
⊢ 2 * π ≠ 0
Tactic:
simp [pi_ne_zero]
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)
x : ℝ
⊢ 2 * π * x / (2 * π) = x
Tactic:
field_simp
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
y : ℝ
hy : 0 < y
⊢ ↑y * Ψ y = 𝓕 (⇑g) (1 / (2 * π) * y.log)
Tactic:
field_simp [hg, toSchwartz, h]
Proof state after:
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
y : ℝ
hy : 0 < y
⊢ ↑y * Ψ y = cexp (2 * ↑π * ↑y.log / (2 * ↑π)) * Ψ (rexp y.log)
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
y : ℝ
hy : 0 < y
⊢ ↑y * Ψ y = cexp (2 * ↑π * ↑y.log / (2 * ↑π)) * Ψ (rexp y.log)
Tactic:
norm_cast
Proof state after:
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
y : ℝ
hy : 0 < y
⊢ ↑y * Ψ y = ↑(rexp (2 * π * y.log / (2 * π))) * Ψ (rexp y.log)
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
y : ℝ
hy : 0 < y
⊢ ↑y * Ψ y = ↑(rexp (2 * π * y.log / (2 * π))) * Ψ (rexp y.log)
Tactic:
field_simp [why]
Proof state after:
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
y : ℝ
hy : 0 < y
⊢ ↑y * Ψ y = cexp ↑y.log * Ψ (rexp y.log)
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
y : ℝ
hy : 0 < y
⊢ ↑y * Ψ y = cexp ↑y.log * Ψ (rexp y.log)
Tactic:
norm_cast
Proof state after:
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
y : ℝ
hy : 0 < y
⊢ ↑y * Ψ y = ↑(rexp y.log) * Ψ (rexp y.log)
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
y : ℝ
hy : 0 < y
⊢ ↑y * Ψ y = ↑(rexp y.log) * Ψ (rexp y.log)
Tactic:
rw [Real.exp_log hy]
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 : ℝ) in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = ∑' (n : ℕ), f n * Ψ (↑n / x) / ↑x
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)
x : ℝ
hx : 0 < x
⊢ ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = ∑' (n : ℕ), f n * Ψ (↑n / x) / ↑x
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)
x : ℝ
hx : 0 < x
⊢ ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log) = ∑' (n : ℕ), f n * Ψ (↑n / x) / ↑x
Tactic:
congr
Proof state after:
case h.e_f
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
⊢ (fun n => f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log)) = fun n => f n * Ψ (↑n / x) / ↑x
Theorem: wiener_ikehara_smooth
Proof state before:
case h.e_f
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
⊢ (fun n => f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * (↑n / x).log)) = fun n => f n * Ψ (↑n / x) / ↑x
Tactic:
ext n
Proof state after:
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