Theorem: limiting_fourier_lim2_aux (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x C : ℝ
⊢ Integrable (fun t => |x| * (C / (1 + (t / (2 * π)) ^ 2))) (volume.restrict (Ici (-x.log)))
Tactic:
simp_rw [div_eq_mul_inv C]
State after:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x C : ℝ
⊢ Integrable (fun t => |x| * (C * (1 + (t / (2 * π)) ^ 2)⁻¹)) (volume.restrict (Ici (-x.log)))

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x C : ℝ
⊢ Integrable (fun t => |x| * (C * (1 + (t / (2 * π)) ^ 2)⁻¹)) (volume.restrict (Ici (-x.log)))
Tactic:
exact (((integrable_inv_one_add_sq.comp_div (by simp [pi_ne_zero])).const_mul _).const_mul _).restrict
State after:
no goals

State before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x C : ℝ
⊢ 2 * π ≠ 0
Tactic:
simp [pi_ne_zero]
State after:
no goals