Theorem: second_fourier_aux (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ -(cexp (-((1 - ↑σ' - ↑t * I) * ↑x.log)) / (1 - ↑σ' - ↑t * I)) = ↑(x ^ (σ' - 1)) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)
Tactic:
calc
  _ = cexp (↑(Real.log x) * ((↑σ' - 1) + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹ := by rw [← div_neg]; ring_nf
  _ = (x ^ ((↑σ' - 1) + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹ := by
    rw [Complex.cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)), Complex.ofReal_log hx.le]
  _ = (x ^ ((σ' : ℂ) - 1)) * (x ^ (↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹ := by
    rw [Complex.cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt hx))]
  _ = _ := by rw [ofReal_cpow hx.le]; push_cast; ring
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ -(cexp (-((1 - ↑σ' - ↑t * I) * ↑x.log)) / (1 - ↑σ' - ↑t * I)) =
    cexp (↑x.log * (↑σ' - 1 + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹
Tactic:
rw [← div_neg]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ cexp (-((1 - ↑σ' - ↑t * I) * ↑x.log)) / -(1 - ↑σ' - ↑t * I) =
    cexp (↑x.log * (↑σ' - 1 + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ cexp (-((1 - ↑σ' - ↑t * I) * ↑x.log)) / -(1 - ↑σ' - ↑t * I) =
    cexp (↑x.log * (↑σ' - 1 + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹
Tactic:
ring_nf
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ cexp (↑x.log * (↑σ' - 1 + ↑t * I)) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ (↑σ' - 1 + ↑t * I) * (↑σ' + ↑t * I - 1)⁻¹
Tactic:
rw [Complex.cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)), Complex.ofReal_log hx.le]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1 + ↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹
Tactic:
rw [Complex.cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt hx))]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑(x ^ (σ' - 1)) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)
Tactic:
rw [ofReal_cpow hx.le]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ ↑(σ' - 1) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ ↑(σ' - 1) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)
Tactic:
push_cast
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ (↑σ' - 1) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ↑x ^ (↑σ' - 1) * ↑x ^ (↑t * I) * (↑σ' + ↑t * I - 1)⁻¹ = ↑x ^ (↑σ' - 1) * (↑σ' + ↑t * I - 1)⁻¹ * ↑x ^ (↑t * I)
Tactic:
ring
State after:
no goals