internlm/Lean-Github huggingface dataset:
Theorem: limiting_cor_W21
Proof state before:
case hg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
key3 : ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
S1_sub_1 : ∀ (x : ℝ), 𝓕 (ψ.toFun - (Ψ R).toFun) x = 𝓕 ψ.toFun x - 𝓕 (Ψ R).toFun x
S1_sub : S1 x (ψ.toFun - (Ψ R).toFun) = S1 x ψ.toFun - S1 x (Ψ R).toFun
⊢ Integrable (fun u => 𝓕 (Ψ R).toFun (u / (2 * π))) (volume.restrict (Ici (-x.log)))
Tactic:
exact (Ψ R : W21).integrable_fourier (by positivity) |>.restrict
Proof state after:
no goals
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
key3 : ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
S1_sub_1 : ∀ (x : ℝ), 𝓕 (ψ.toFun - (Ψ R).toFun) x = 𝓕 ψ.toFun x - 𝓕 (Ψ R).toFun x
S1_sub : S1 x (ψ.toFun - (Ψ R).toFun) = S1 x ψ.toFun - S1 x (Ψ R).toFun
S2_sub : S2 x (ψ.toFun - (Ψ R).toFun) = S2 x ψ.toFun - S2 x (Ψ R).toFun
⊢ S x (ψ.toFun - (Ψ R).toFun) = S x ψ.toFun - S x (Ψ R).toFun
Tactic:
simp [S, S1_sub, S2_sub]
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
key3 : ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
S1_sub_1 : ∀ (x : ℝ), 𝓕 (ψ.toFun - (Ψ R).toFun) x = 𝓕 ψ.toFun x - 𝓕 (Ψ R).toFun x
S1_sub : S1 x (ψ.toFun - (Ψ R).toFun) = S1 x ψ.toFun - S1 x (Ψ R).toFun
S2_sub : S2 x (ψ.toFun - (Ψ R).toFun) = S2 x ψ.toFun - S2 x (Ψ R).toFun
⊢ S1 x ψ.toFun - S1 x (Ψ R).toFun - (S2 x ψ.toFun - S2 x (Ψ R).toFun) =
    S1 x ψ.toFun - S2 x ψ.toFun - (S1 x (Ψ R).toFun - S2 x (Ψ R).toFun)
Theorem: limiting_cor_W21
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ✝ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : W21
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
S1 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ∑' (n : ℕ), f n / ↑n * 𝓕 ψ (1 / (2 * π) * (↑n / x).log)
S2 : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ (u / (2 * π))
S : ℝ → (ℝ → ℂ) → ℂ := fun x ψ => S1 x ψ - S2 x ψ
g : trunc
Ψ : ℝ → CS 2 ℂ := fun R => g.scale R * ψ
C : ℝ
hcheby : chebyWith C f
hC : 0 ≤ C
key2 : ∀ ε > 0, ∀ᶠ (x : ℝ) in atTop, dist (W21.norm (ψ.toFun - (Ψ x).toFun)) 0 < ε
ε : ℝ
hε : ε > 0
M : ℝ := C * (1 + 2 * π ^ 2) + ‖↑A‖ * (2 * π ^ 2)
R : ℝ
hRψ : W21.norm (ψ.toFun - (Ψ R).toFun) < ε / 2 / (1 + M)
key✝ : ∀ (R ε : ℝ), ε > 0 → ∀ᶠ (x : ℝ) in atTop, ‖S x (Ψ R).toFun‖ < ε
x : ℝ
hx : 1 ≤ x
key : ‖S x (Ψ R).toFun‖ < ε / 2
key3 : ‖S x (ψ.toFun - (Ψ R).toFun)‖ < ε / 2
S1_sub_1 : ∀ (x : ℝ), 𝓕 (ψ.toFun - (Ψ R).toFun) x = 𝓕 ψ.toFun x - 𝓕 (Ψ R).toFun x
S1_sub : S1 x (ψ.toFun - (Ψ R).toFun) = S1 x ψ.toFun - S1 x (Ψ R).toFun
S2_sub : S2 x (ψ.toFun - (Ψ R).toFun) = S2 x ψ.toFun - S2 x (Ψ R).toFun
⊢ S1 x ψ.toFun - S1 x (Ψ R).toFun - (S2 x ψ.toFun - S2 x (Ψ R).toFun) =
    S1 x ψ.toFun - S2 x ψ.toFun - (S1 x (Ψ R).toFun - S2 x (Ψ R).toFun)
Tactic:
ring
Proof state after:
no goals
Theorem: fourier_surjection_on_schwartz
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : 𝓢(ℝ, ℂ)
⊢ ∃ g, 𝓕 ⇑g = ⇑f
Tactic:
refine ⟨(fourierTransformCLE ℝ).symm f, ?_⟩
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : 𝓢(ℝ, ℂ)
⊢ 𝓕 ⇑((fourierTransformCLE ℝ).symm f) = ⇑f
Theorem: fourier_surjection_on_schwartz
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : 𝓢(ℝ, ℂ)
⊢ 𝓕 ⇑((fourierTransformCLE ℝ).symm f) = ⇑f
Tactic:
rw [← fourierTransformCLE_apply ℝ]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : 𝓢(ℝ, ℂ)
⊢ ⇑((fourierTransformCLE ℝ) ((fourierTransformCLE ℝ).symm f)) = ⇑f
Theorem: fourier_surjection_on_schwartz
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : 𝓢(ℝ, ℂ)
⊢ ⇑((fourierTransformCLE ℝ) ((fourierTransformCLE ℝ).symm f)) = ⇑f
Tactic:
simp
Proof state after:
no goals
Theorem: comp_exp_support2
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
Ψ : ℝ → ℂ
hsupp : HasCompactSupport Ψ
⊢ ∀ᶠ (x : ℝ) in atTop, (Ψ ∘ rexp) x = 0
Tactic:
simp only [hasCompactSupport_iff_eventuallyEq, coclosedCompact_eq_cocompact, cocompact_eq_atBot_atTop] at hsupp
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
Ψ : ℝ → ℂ
hsupp : Ψ =ᶠ[atBot ⊔ atTop] 0
⊢ ∀ᶠ (x : ℝ) in atTop, (Ψ ∘ rexp) x = 0
Theorem: comp_exp_support2
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
Ψ : ℝ → ℂ
hsupp : Ψ =ᶠ[atBot ⊔ atTop] 0
⊢ ∀ᶠ (x : ℝ) in atTop, (Ψ ∘ rexp) x = 0
Tactic:
exact Real.tendsto_exp_atTop hsupp.2
Proof state after:
no goals
Theorem: comp_exp_support
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
Ψ : ℝ → ℂ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
⊢ HasCompactSupport (Ψ ∘ rexp)
Tactic:
simp only [hasCompactSupport_iff_eventuallyEq, coclosedCompact_eq_cocompact, cocompact_eq_atBot_atTop]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
Ψ : ℝ → ℂ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
⊢ Ψ ∘ rexp =ᶠ[atBot ⊔ atTop] 0
Theorem: comp_exp_support
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
Ψ : ℝ → ℂ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
⊢ Ψ ∘ rexp =ᶠ[atBot ⊔ atTop] 0
Tactic:
exact ⟨comp_exp_support1 hplus, comp_exp_support2 hsupp⟩
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Tactic:
have l1 : ContinuousOn rexp (Ici (-Real.log x)) := by fun_prop
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Tactic:
have l2 : Tendsto rexp atTop atTop := Real.tendsto_exp_atTop
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Tactic:
have l3 t (_ : t ∈ Ioi (-log x)) : HasDerivWithinAt rexp (rexp t) (Ioi t) t :=
  (Real.hasDerivAt_exp t).hasDerivWithinAt
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Tactic:
have l4 : ContinuousOn Ψ (rexp '' Ioi (-Real.log x)) := by fun_prop
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Tactic:
have l5 : IntegrableOn Ψ (rexp '' Ici (-Real.log x)) volume :=
  (l0.integrable_of_hasCompactSupport hsupp).integrableOn
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Tactic:
have l6 : IntegrableOn (fun x ↦ rexp x • (Ψ ∘ rexp) x) (Ici (-Real.log x)) volume := by
  refine (Continuous.integrable_of_hasCompactSupport (by continuity) ?_).integrableOn
  change HasCompactSupport (rexp • (Ψ ∘ rexp))
  exact (comp_exp_support hsupp hplus).smul_left
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
l6 : IntegrableOn (fun x => rexp x • (Ψ ∘ rexp) x) (Ici (-x.log)) volume
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
l6 : IntegrableOn (fun x => rexp x • (Ψ ∘ rexp) x) (Ici (-x.log)) volume
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Tactic:
have := MeasureTheory.integral_comp_smul_deriv_Ioi l1 l2 l3 l4 l5 l6
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
l6 : IntegrableOn (fun x => rexp x • (Ψ ∘ rexp) x) (Ici (-x.log)) volume
this : ∫ (x : ℝ) in Ioi (-x.log), rexp x • (Ψ ∘ rexp) x = ∫ (u : ℝ) in Ioi (rexp (-x.log)), Ψ u
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
l6 : IntegrableOn (fun x => rexp x • (Ψ ∘ rexp) x) (Ici (-x.log)) volume
this : ∫ (x : ℝ) in Ioi (-x.log), rexp x • (Ψ ∘ rexp) x = ∫ (u : ℝ) in Ioi (rexp (-x.log)), Ψ u
⊢ ∫ (u : ℝ) in Ioi (-x.log), ↑(rexp u) * Ψ (rexp u) = ∫ (y : ℝ) in Ioi (1 / x), Ψ y
Tactic:
simpa [Real.exp_neg, Real.exp_log hx] using this
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
⊢ ContinuousOn rexp (Ici (-x.log))
Tactic:
fun_prop
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
⊢ ContinuousOn Ψ (rexp '' Ioi (-x.log))
Tactic:
fun_prop
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
⊢ IntegrableOn (fun x => rexp x • (Ψ ∘ rexp) x) (Ici (-x.log)) volume
Tactic:
refine (Continuous.integrable_of_hasCompactSupport (by continuity) ?_).integrableOn
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
⊢ HasCompactSupport fun x => rexp x • (Ψ ∘ rexp) x
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
⊢ HasCompactSupport fun x => rexp x • (Ψ ∘ rexp) x
Tactic:
change HasCompactSupport (rexp • (Ψ ∘ rexp))
Proof state after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
⊢ HasCompactSupport (rexp • Ψ ∘ rexp)
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
⊢ HasCompactSupport (rexp • Ψ ∘ rexp)
Tactic:
exact (comp_exp_support hsupp hplus).smul_left
Proof state after:
no goals
Theorem: wiener_ikehara_smooth_aux
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l0 : Continuous Ψ
hsupp : HasCompactSupport Ψ
hplus : closure (Function.support Ψ) ⊆ Ioi 0
x : ℝ
hx : 0 < x
l1 : ContinuousOn rexp (Ici (-x.log))
l2 : Tendsto rexp atTop atTop
l3 : ∀ t ∈ Ioi (-x.log), HasDerivWithinAt rexp (rexp t) (Ioi t) t
l4 : ContinuousOn Ψ (rexp '' Ioi (-x.log))
l5 : IntegrableOn Ψ (rexp '' Ici (-x.log)) volume
⊢ Continuous fun x => rexp x • (Ψ ∘ rexp) x
Tactic:
continuity
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
⊢ Tendsto (fun x => (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
obtain ⟨ε, hε, hh⟩ := Metric.eventually_nhds_iff.mp <| comp_exp_support0 hplus
Proof state after:
case intro.intro
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
⊢ Tendsto (fun x => (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Theorem: wiener_ikehara_smooth_sub
Proof state before:
case intro.intro
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
⊢ Tendsto (fun x => (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y) atTop (𝓝 0)
Tactic:
apply tendsto_nhds_of_eventually_eq
Proof state after:
case intro.intro.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' : ℝ) in atTop, (↑A * ∫ (y : ℝ) in Ioi x'⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0
Theorem: wiener_ikehara_smooth_sub
Proof state before:
case intro.intro.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' : ℝ) in atTop, (↑A * ∫ (y : ℝ) in Ioi x'⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0
Tactic:
filter_upwards [eventually_gt_atTop ε⁻¹] 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 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
⊢ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0
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
⊢ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0
Tactic:
have l1 : Integrable (indicator (Ioi x⁻¹) (fun x : ℝ => Ψ x)) := h1.indicator measurableSet_Ioi
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
⊢ (↑A * ∫ (y : ℝ) in Ioi x⁻¹, Ψ y) - ↑A * ∫ (y : ℝ) in Ioi 0, Ψ y = 0