Theorem: sum_eq_int_deriv_aux1 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
by_cases h : b = k + 1
State after:
case pos
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
h : b = ↑k + 1
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x

case neg
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
h : ¬b = ↑k + 1
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x

State before:
case pos
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
h : b = ↑k + 1
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
exact sum_eq_int_deriv_aux_eq h φDiff derivφCont
State after:
no goals

State before:
case neg
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_le_kpOne : b ≤ ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
h : ¬b = ↑k + 1
⊢ ∑ n ∈ Finset.Ioc k ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
exact sum_eq_int_deriv_aux_lt ha (Ne.lt_of_le h b_le_kpOne) φDiff derivφCont
State after:
no goals