Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.intervalIntegrable_second_ibp_integrand

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3151 to 3163

Mathematical statement

Exact Lean statement

lemma intervalIntegrable_second_ibp_integrand {u v : ℝ} (hu_pos : 0 < u)
    (huv : u ≤ v) (s : ℂ) :
    IntervalIntegrable
      (fun y : ℝ ↦
        (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *
          (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ))
      volume u v

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma intervalIntegrable_second_ibp_integrand {u v : ℝ} (hu_pos : 0 < u)    (huv : u ≤ v) (s : ℂ) :    IntervalIntegrable      (fun y : ℝ ↦        (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *          (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ))      volume u v := by  have hH2 : ContinuousOn      (fun y : ℝ ↦ s * (s + 1) * (y : ℂ) ^ (-s - 2))      (Set.uIcc u v) := by    simpa [Set.uIcc_of_le huv] using      (continuousOn_second_deriv_ofReal_cpow_neg (s := s) (a := u) (b := v) hu_pos)  exact (hH2.mul continuous_bernoulli2_primitive.continuousOn).intervalIntegrable