Theorem: Perron.map_conj (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ f x ((starRingEnd ℂ) s) = (starRingEnd ℂ) (f x s)
Tactic:
simp only [f, map_div₀, map_mul, map_add, map_one]
State after:
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ ↑x ^ (starRingEnd ℂ) s / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1)) =
    (starRingEnd ℂ) (↑x ^ s) / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1))

State before:
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ ↑x ^ (starRingEnd ℂ) s / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1)) =
    (starRingEnd ℂ) (↑x ^ s) / ((starRingEnd ℂ) s * ((starRingEnd ℂ) s + 1))
Tactic:
congr
State after:
case e_a
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ ↑x ^ (starRingEnd ℂ) s = (starRingEnd ℂ) (↑x ^ s)

State before:
case e_a
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ ↑x ^ (starRingEnd ℂ) s = (starRingEnd ℂ) (↑x ^ s)
Tactic:
rw [cpow_conj, Complex.conj_ofReal]
State after:
case e_a.hx
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ (↑x).arg ≠ π

State before:
case e_a.hx
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ (↑x).arg ≠ π
Tactic:
rw [Complex.arg_ofReal_of_nonneg hx]
State after:
case e_a.hx
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ 0 ≠ π

State before:
case e_a.hx
x σ σ' σ'' T : ℝ
hx : 0 ≤ x
s : ℂ
⊢ 0 ≠ π
Tactic:
exact pi_ne_zero.symm
State after:
no goals