Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.hasDerivAt_log_div_self_mul_integral

PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:3401 to 3410

Mathematical statement

Exact Lean statement

lemma hasDerivAt_log_div_self_mul_integral {x₁ : ℝ} (hx₁ : 1 < x₁) {t : ℝ} (ht : x₁ < t) :
    HasDerivAt (fun t => (Real.log t / t) * ∫ s in x₁..t, 1 / (Real.log s) ^ 2)
      ((t / Real.log t - (Real.log t - 1) * ∫ s in x₁..t, 1 / (Real.log s) ^ 2) / t^2) t

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasDerivAt_log_div_self_mul_integral {x₁ : ℝ} (hx₁ : 1 < x₁) {t : ℝ} (ht : x₁ < t) :    HasDerivAt (fun t => (Real.log t / t) * ∫ s in x₁..t, 1 / (Real.log s) ^ 2)      ((t / Real.log t - (Real.log t - 1) * ∫ s in x₁..t, 1 / (Real.log s) ^ 2) / t^2) t := by  have ht0 : t ≠ 0 := by linarith  have hlogt0 : Real.log t ≠ 0 := ne_of_gt ( Real.log_pos (by linarith : 1 < t) )  have ht20 : t ^ 2 ≠ 0 := pow_ne_zero 2 ht0  have hlogt20 : Real.log t ^ 2 ≠ 0 := pow_ne_zero 2 hlogt0  have h_deriv_I := hasDerivAt_integral_one_div_log_sq hx₁ ht.le  convert! HasDerivAt.mul ( HasDerivAt.div ( Real.hasDerivAt_log ht0 ) ( hasDerivAt_id t ) ht0 ) h_deriv_I using 1  dsimp; field_simp [ht0, hlogt0, ht20, hlogt20]; ring_nf