Theorem: sum_eq_int_deriv_aux_lt (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_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:
have flb_eq_k : ⌊b⌋ = k := Int.floor_eq_iff.mpr ⟨by linarith [ha.1, ha.2], by linarith⟩
State after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ 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:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ 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:
simp only [flb_eq_k, gt_iff_lt, lt_add_iff_pos_right, zero_lt_one, Finset.Icc_eq_empty_of_lt,
  Finset.sum_empty]
State after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
rw [sum_eq_int_deriv_aux2 (k + 1 / 2) φDiff derivφCont]
State after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)
Tactic:
have : Finset.Ioc k k = {} := by simp only [ge_iff_le, le_refl, Finset.Ioc_eq_empty_of_le]
State after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
this : Finset.Ioc k k = ∅
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
this : Finset.Ioc k k = ∅
⊢ ∑ x ∈ Finset.Ioc k k, φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)
Tactic:
simp only [this, Finset.sum_empty, one_div]
State after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
this : Finset.Ioc k k = ∅
⊢ 0 =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 2⁻¹ - ↑b) * φ b - (↑k + 2⁻¹ - ↑a) * φ a -
      ((↑k + 2⁻¹ - ↑b) * φ b - (↑k + 2⁻¹ - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
this : Finset.Ioc k k = ∅
⊢ 0 =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 2⁻¹ - ↑b) * φ b - (↑k + 2⁻¹ - ↑a) * φ a -
      ((↑k + 2⁻¹ - ↑b) * φ b - (↑k + 2⁻¹ - ↑a) * φ a + ∫ (x : ℝ) in a..b, φ x)
Tactic:
ring_nf
State after:
no goals

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ↑k ≤ b
Tactic:
linarith [ha.1, ha.2]
State after:
no goals

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ b < ↑k + 1
Tactic:
linarith
State after:
no goals

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
ha : a ∈ Ico (↑k) b
b_lt_kpOne : b < ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k
⊢ Finset.Ioc k k = ∅
Tactic:
simp only [ge_iff_le, le_refl, Finset.Ioc_eq_empty_of_le]
State after:
no goals