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

State before:
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Tactic:
by_cases s_eq_zero : s = 0
State after:
case pos
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : s = 0
⊢ f t s * ↑x ^ (-s) = f (t / x) s

case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
⊢ f t s * ↑x ^ (-s) = f (t / x) s

State before:
case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Tactic:
by_cases s_eq_neg_one : s = -1
State after:
case pos
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : s = -1
⊢ f t s * ↑x ^ (-s) = f (t / x) s

case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ f t s * ↑x ^ (-s) = f (t / x) s

State before:
case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Tactic:
field_simp [f, mul_ne_zero s_eq_zero (fun hs ↦ add_eq_zero_iff_eq_neg.mp hs |> s_eq_neg_one)]
State after:
case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑t ^ s * ↑x ^ (-s) = (↑t / ↑x) ^ s

State before:
case neg
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑t ^ s * ↑x ^ (-s) = (↑t / ↑x) ^ s
Tactic:
convert (Complex.mul_cpow_ofReal_nonneg tpos.le (inv_pos.mpr xpos).le s).symm using 2
State after:
case h.e'_2.h.e'_6
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑x ^ (-s) = ↑x⁻¹ ^ s

case h.e'_3.h.e'_5
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑t / ↑x = ↑t * ↑x⁻¹

State before:
case pos
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : s = 0
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Tactic:
simp [f, s_eq_zero]
State after:
no goals

State before:
case pos
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : s = -1
⊢ f t s * ↑x ^ (-s) = f (t / x) s
Tactic:
simp [f, s_eq_neg_one]
State after:
no goals

State before:
case h.e'_2.h.e'_6
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑x ^ (-s) = ↑x⁻¹ ^ s
Tactic:
convert Complex.cpow_neg_eq_inv_pow_ofReal_pos xpos s
State after:
case h.e'_3.h.e'_5
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑x⁻¹ = (↑x)⁻¹

State before:
case h.e'_3.h.e'_5
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑x⁻¹ = (↑x)⁻¹
Tactic:
exact ofReal_inv x
State after:
no goals

State before:
case h.e'_3.h.e'_5
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑t / ↑x = ↑t * ↑x⁻¹
Tactic:
simp only [ofReal_inv]
State after:
case h.e'_3.h.e'_5
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑t / ↑x = ↑t * (↑x)⁻¹

State before:
case h.e'_3.h.e'_5
x✝ σ σ' σ'' T x t : ℝ
tpos : 0 < t
xpos : 0 < x
s : ℂ
s_eq_zero : ¬s = 0
s_eq_neg_one : ¬s = -1
⊢ ↑t / ↑x = ↑t * (↑x)⁻¹
Tactic:
rfl
State after:
no goals