internlm/Lean-Github huggingface dataset:
Theorem: wiener_ikehara_smooth_sub
Proof state before:
case pos.a
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : 0 < t ∧ t ≤ x⁻¹
this : |t| ≤ x⁻¹
⊢ |t| < ε
Tactic:
linarith
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_sub
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
⊢ 0 < ε⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_sub
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
⊢ 0 < x
Tactic:
linarith
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_sub
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
⊢ 0 < x⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_sub
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
⊢ x⁻¹ < ε
Tactic:
apply (inv_lt hε hx).mp hxε
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_sub
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
⊢ Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
Tactic:
ext t
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
⊢ t ∈ Ioi 0 ↔ t ∈ Ioc 0 x⁻¹ ∪ Ioi x⁻¹
Theorem: wiener_ikehara_smooth_sub
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
⊢ t ∈ Ioi 0 ↔ t ∈ Ioc 0 x⁻¹ ∪ Ioi x⁻¹
Tactic:
simp
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
⊢ 0 < t ↔ 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t
Theorem: wiener_ikehara_smooth_sub
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
⊢ 0 < t ↔ 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t
Tactic:
constructor <;> intro h
Proof state after:
case h.mp
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
h : 0 < t
⊢ 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t

case h.mpr
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
h : 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t
⊢ 0 < t
Theorem: wiener_ikehara_smooth_sub
Proof state before:
case h.mp
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
h : 0 < t
⊢ 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t
Tactic:
simp [h, le_or_lt]
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_sub
Proof state before:
case h.mpr
n : ℕ
A a b c d u x✝ y t✝¹ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t✝ : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
t : ℝ
h : 0 < t ∧ t ≤ x⁻¹ ∨ x⁻¹ < t
⊢ 0 < t
Tactic:
cases h <;> linarith
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_sub
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
⊢ Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
Tactic:
simp
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_sub
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : 0 < t ∧ t ≤ x⁻¹
⊢ |t| ≤ x⁻¹
Tactic:
rw [abs_le]
Proof state after:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : 0 < t ∧ t ≤ x⁻¹
⊢ -x⁻¹ ≤ t ∧ t ≤ x⁻¹
Theorem: wiener_ikehara_smooth_sub
Proof state before:
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : 0 < t ∧ t ≤ x⁻¹
⊢ -x⁻¹ ≤ t ∧ t ≤ x⁻¹
Tactic:
constructor <;> linarith
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
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
let h (x : ℝ) : ℂ := rexp (2 * π * x) * Ψ (exp (2 * π * x))
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))
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
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))
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
have h1 : ContDiff ℝ ⊤ h := by
  have : ContDiff ℝ ⊤ (fun x : ℝ => (rexp (2 * π * x))) := (contDiff_const.mul contDiff_id).exp
  exact (contDiff_ofReal.comp this).mul (hsmooth.comp this)
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
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
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
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
have h2 : HasCompactSupport h := by
  have : 2 * π ≠ 0 := by simp [pi_ne_zero]
  simpa using (comp_exp_support hsupp hplus).comp_smul this |>.mul_left
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
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
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
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
obtain ⟨g, hg⟩ := fourier_surjection_on_schwartz (toSchwartz h h1 h2)
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)
⊢ 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)
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
have why (x : ℝ) : 2 * π * x / (2 * π) = x := by field_simp
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
⊢ 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
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
have l1 {y} (hy : 0 < y) : y * Ψ y = 𝓕 g (1 / (2 * π) * Real.log y) := by
  field_simp [hg, toSchwartz, h] ; norm_cast ; field_simp [why] ; norm_cast
  rw [Real.exp_log hy]
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)
⊢ 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)
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
have key := limiting_cor_schwartz g hf hcheby hG hG'
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)
⊢ 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)
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
have l2 : ∀ᶠ x in atTop, ∑' (n : ℕ), f n / ↑n * 𝓕 (⇑g) (1 / (2 * π) * Real.log (↑n / x)) =
    ∑' (n : ℕ), f n * Ψ (↑n / x) / x := by
  filter_upwards [eventually_gt_atTop 0] with x hx
  congr ; ext n
  by_cases hn : n = 0 ; simp [hn, (comp_exp_support0 hplus).self_of_nhds]
  rw [← l1 (by positivity)]
  have : (n : ℂ) ≠ 0 := by simpa using hn
  have : (x : ℂ) ≠ 0 := by simpa using hx.ne.symm
  field_simp ; ring
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
⊢ Tendsto (fun x => (∑' (n : ℕ), f n * Ψ (↑n / x)) / ↑x - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)