Theorem: hh_integral' (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t = 2 * π ^ 2
Tactic:
have := hh_integral (a := 1) (b := 1 / (2 * π)) (c := 1) (by positivity) (by positivity) (by positivity)
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
this : ∫ (t : ℝ) in Ioi 0, 1 * hh (1 / (2 * π)) (t / 1) = 1 * 1 / (1 / (2 * π)) * π
⊢ ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t = 2 * π ^ 2

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
this : ∫ (t : ℝ) in Ioi 0, 1 * hh (1 / (2 * π)) (t / 1) = 1 * 1 / (1 / (2 * π)) * π
⊢ ∫ (t : ℝ) in Ioi 0, hh (1 / (2 * π)) t = 2 * π ^ 2
Tactic:
convert this using 1 <;> simp
State after:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
this : ∫ (t : ℝ) in Ioi 0, 1 * hh (1 / (2 * π)) (t / 1) = 1 * 1 / (1 / (2 * π)) * π
⊢ 2 * π ^ 2 = 2 * π * π

State before:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
this : ∫ (t : ℝ) in Ioi 0, 1 * hh (1 / (2 * π)) (t / 1) = 1 * 1 / (1 / (2 * π)) * π
⊢ 2 * π ^ 2 = 2 * π * π
Tactic:
ring
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 0 < 1
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 0 < 1 / (2 * π)
Tactic:
positivity
State after:
no goals