Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.neg_B1_integral_add_adjacent

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3205 to 3214

Mathematical statement

Exact Lean statement

lemma neg_B1_integral_add_adjacent {a c b : ℝ} (hac : a ≤ c) (hcb : c ≤ b)
    (ha_pos : 0 < a) (s : ℂ) :
    -(∫ y in a..c, deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y * ((B1 y : ℝ) : ℂ)) +
      -(∫ y in c..b, deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y * ((B1 y : ℝ) : ℂ)) =
        -(∫ y in a..b, deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y * ((B1 y : ℝ) : ℂ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma neg_B1_integral_add_adjacent {a c b : ℝ} (hac : a ≤ c) (hcb : c ≤ b)    (ha_pos : 0 < a) (s : ℂ) :    -(∫ y in a..c, deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y * ((B1 y : ℝ) : ℂ)) +      -(∫ y in c..b, deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y * ((B1 y : ℝ) : ℂ)) =        -(∫ y in a..b, deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) y * ((B1 y : ℝ) : ℂ)) := by  have hc_pos : 0 < c := lt_of_lt_of_le ha_pos hac  have hInt_ac := intervalIntegrable_deriv_cpow_mul_B1 (u := a) (v := c) ha_pos hac s  have hInt_cb := intervalIntegrable_deriv_cpow_mul_B1 (u := c) (v := b) hc_pos hcb s  rw [← intervalIntegral.integral_add_adjacent_intervals hInt_ac hInt_cb]  ring