Source indexedlemma · leanprover/lean4:v4.32.0

DerivUpperBnd_aux7_3

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1883 to 1896

Mathematical statement

Exact Lean statement

lemma DerivUpperBnd_aux7_3 {x σ : ℝ} (xpos : 0 < x) (σnz : σ ≠ 0) :
    HasDerivAt (fun t ↦ -(1 / σ ^ 2 * t ^ (-σ) + 1 / σ * t ^ (-σ) * Real.log t))
      (x ^ (-σ - 1) * Real.log x) x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma DerivUpperBnd_aux7_3 {x σ : ℝ} (xpos : 0 < x) (σnz : σ ≠ 0) :    HasDerivAt (fun t ↦ -(1 / σ ^ 2 * t ^ (-σ) + 1 / σ * t ^ (-σ) * Real.log t))      (x ^ (-σ - 1) * Real.log x) x := by  have h1 := Real.hasDerivAt_rpow_const (p := -σ) (Or.inl xpos.ne.symm)  have h2 := h1.const_mul (1 / σ^2)  have cancel : 1 / σ^2 * σ = 1 / σ := by field_simp  rw [neg_mul, mul_neg, ← mul_assoc, cancel] at h2  have h3 := Real.hasDerivAt_log xpos.ne.symm  have h4 := HasDerivAt.mul (h1.const_mul (1 / σ)) h3  have cancel := Real.rpow_add xpos (-σ) (-1)  have : -σ + -1 = -σ - 1 := by rfl  rw [← Real.rpow_neg_one x, mul_assoc (1 / σ) (x ^ (-σ)), ← cancel, this] at h4  convert! h2.add h4 |>.neg using 1  field_simp; ring