Theorem: wiener_ikehara_smooth_aux (PrimeNumberTheoremAnd/Wiener.lean)

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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

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))
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)

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
State after:
no goals

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
State after:
no goals