Source indexedlemma · leanprover/lean4:v4.32.0

DerivUpperBnd_aux7_1

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1869 to 1875

Mathematical statement

Exact Lean statement

lemma DerivUpperBnd_aux7_1 {x σ t : ℝ} (hx : 1 ≤ x) :
    let s

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma DerivUpperBnd_aux7_1 {x σ t : ℝ} (hx : 1 ≤ x) :    let s := ↑σ + ↑t * I;    ‖(↑⌊x⌋ + 1 / 2 - ↑x) * (x : ℂ) ^ (-s - 1) * -↑x.log‖ = |(↑⌊x⌋ + 1 / 2 - x)| * x ^ (-σ - 1) * x.log := by  have xpos : 0 < x := lt_of_lt_of_le (by norm_num) hx  have : ‖(x.log : ℂ)‖ = x.log := Complex.norm_of_nonneg <| Real.log_nonneg hx  simp [← norm_real, this, Complex.norm_cpow_eq_rpow_re_of_pos xpos, ← Real.norm_eq_abs, ← ofReal_ofNat,    ← ofReal_inv, ← ofReal_add, ← ofReal_sub, ← ofReal_intCast, one_div]