Source indexedlemma · leanprover/lean4:v4.32.0

Ramanujan.hasDerivAt_li_antideriv

PrimeNumberTheoremAnd.IEANTN.Ramanujan.RamanujanCalculations · PrimeNumberTheoremAnd/IEANTN/Ramanujan/RamanujanCalculations.lean:334 to 351

Source documentation

The antiderivative x ↦ x / log x + ∫ 1 / log² u appearing in the integration-by-parts identity for Li has derivative 1 / log t at any t > 1, provided the lower limit a of the integral also exceeds 1 (so 1 / log² u is continuous across the interval).

Exact Lean statement

lemma hasDerivAt_li_antideriv {a t : ℝ} (ha : 1 < a) (ht : 1 < t) :
    HasDerivAt (fun x ↦ x / log x + ∫ u in (a : ℝ)..x, 1 / log u ^ 2) (1 / log t) t

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma hasDerivAt_li_antideriv {a t : ℝ} (ha : 1 < a) (ht : 1 < t) :    HasDerivAt (fun x ↦ x / log x + ∫ u in (a : ℝ)..x, 1 / log u ^ 2) (1 / log t) t := by  have ht0 : t ≠ 0 := (one_pos.trans ht).ne'  have htlog : log t ≠ 0 := ne_of_gt (log_pos ht)  have h_ftc : HasDerivAt (fun x ↦ ∫ u in (a : ℝ)..x, 1 / log u ^ 2) (1 / log t ^ 2) t := by    apply_rules [intervalIntegral.integral_hasDerivAt_right]    · apply_rules [ContinuousOn.intervalIntegrable]      exact continuousOn_of_forall_continuousAt fun u hu ↦        ContinuousAt.div continuousAt_const (ContinuousAt.pow          (continuousAt_log (by cases Set.mem_uIcc.mp hu <;> linarith)) _)            (ne_of_gt (sq_pos_of_pos (log_pos (by cases Set.mem_uIcc.mp hu <;> linarith))))    · exact (measurable_const.div (measurable_log.pow_const _)).stronglyMeasurable.stronglyMeasurableAtFilter    · exact ContinuousAt.div continuousAt_const        (ContinuousAt.pow (continuousAt_log ht0) _) (ne_of_gt (sq_pos_of_pos (log_pos ht)))  convert! (HasDerivAt.div (hasDerivAt_id t) (hasDerivAt_log ht0) htlog).add h_ftc using 1  simp only [id_eq]  field_simp  ring