Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.second_ibp_expr_add_adjacent

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3176 to 3203

Mathematical statement

Exact Lean statement

lemma second_ibp_expr_add_adjacent {a c b : ℝ} (hac : a ≤ c) (hcb : c ≤ b)
    (ha_pos : 0 < a) (s : ℂ) :
    (deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) c *
          (((-(Int.fract c ^ 2 - Int.fract c + 1 / 6) / 2) : ℝ) : ℂ) -
        deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) a *
          (((-(Int.fract a ^ 2 - Int.fract a + 1 / 6) / 2) : ℝ) : ℂ) -
        ∫ y in a..c,
          (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *
            (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ)) +
      (deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) b *
          (((-(Int.fract b ^ 2 - Int.fract b + 1 / 6) / 2) : ℝ) : ℂ) -
        deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) c *
          (((-(Int.fract c ^ 2 - Int.fract c + 1 / 6) / 2) : ℝ) : ℂ) -
        ∫ y in c..b,
          (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *
            (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ)) =
      deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) b *
          (((-(Int.fract b ^ 2 - Int.fract b + 1 / 6) / 2) : ℝ) : ℂ) -
        deriv (fun t : ℝ ↦ (t : ℂ) ^ (-s)) a *
          (((-(Int.fract a ^ 2 - Int.fract a + 1 / 6) / 2) : ℝ) : ℂ) -
        ∫ y in a..b,
          (s * (s + 1) * (y : ℂ) ^ (-s - 2)) *
            (((-(Int.fract y ^ 2 - Int.fract y + 1 / 6) / 2) : ℝ) : ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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