Source indexedlemma · leanprover/lean4:v4.32.0

Perron.f_mul_eq_f

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:389 to 400

Mathematical statement

Exact Lean statement

lemma f_mul_eq_f {x t : ℝ} (tpos : 0 < t) (xpos : 0 < x) (s : ℂ) :
    f t s * (x : ℂ) ^ (-s) = f (t / x) s

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma f_mul_eq_f {x t : ℝ} (tpos : 0 < t) (xpos : 0 < x) (s : ℂ) :    f t s * (x : ℂ) ^ (-s) = f (t / x) s := by  by_cases s_eq_zero : s = 0  · simp [f, s_eq_zero]  by_cases s_eq_neg_one : s = -1  · simp [f, s_eq_neg_one]  field_simp [f, s_eq_zero,    show s + 1 ≠ 0 from fun hs ↦ add_eq_zero_iff_eq_neg.mp hs |> s_eq_neg_one]  convert (Complex.mul_cpow_ofReal_nonneg tpos.le (inv_pos.mpr xpos).le s).symm using 2  · convert Complex.cpow_neg_eq_inv_pow_ofReal_pos xpos s    exact ofReal_inv x  · norm_cast