Theorem: sum_eq_int_deriv_aux_eq (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_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 + 1 := Int.floor_eq_iff.mpr ⟨by exact_mod_cast b_eq_kpOne.symm.le,
  by rw [b_eq_kpOne]; simp⟩
State after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊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:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊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:
simp only [flb_eq_k, Finset.Icc_self, Finset.sum_singleton, Int.cast_add, Int.cast_one]
State after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ x ∈ Finset.Ioc k (k + 1), φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ x ∈ Finset.Ioc k (k + 1), φ ↑x =
    (∫ (x : ℝ) in a..b, φ x) + (↑k + 1 + 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, b_eq_kpOne]
State after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ ∑ x ∈ Finset.Ioc k (k + 1), φ ↑x =
    (∫ (x : ℝ) in a..↑k + 1, φ x) + (↑k + 1 + 1 / 2 - ↑(↑k + 1)) * φ (↑k + 1) - (↑k + 1 / 2 - ↑a) * φ a -
      ((↑k + 1 / 2 - ↑(↑k + 1)) * φ (↑k + 1) - (↑k + 1 / 2 - ↑a) * φ a + ∫ (x : ℝ) in a..↑k + 1, φ x)

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

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
this : Finset.Ioc k (1 + k) = {k + 1}
⊢ ∑ x ∈ Finset.Ioc k (1 + k), φ ↑x = φ (1 + ↑k)
Tactic:
simp_rw [this, Finset.sum_singleton, Int.cast_add, Int.cast_one, add_comm]
State after:
no goals

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ↑(k + 1) ≤ b
Tactic:
exact_mod_cast b_eq_kpOne.symm.le
State after:
no goals

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ b < ↑(k + 1) + 1
Tactic:
rw [b_eq_kpOne]
State after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
⊢ ↑k + 1 < ↑(k + 1) + 1

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

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
⊢ Finset.Ioc k (1 + k) = {k + 1}
Tactic:
ext m
State after:
case a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ m ∈ Finset.Ioc k (1 + k) ↔ m ∈ {k + 1}

State before:
case a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ m ∈ Finset.Ioc k (1 + k) ↔ m ∈ {k + 1}
Tactic:
simp only [Finset.mem_Ioc, Finset.mem_singleton]
State after:
case a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ k < m ∧ m ≤ 1 + k ↔ m = k + 1

State before:
case a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ k < m ∧ m ≤ 1 + k ↔ m = k + 1
Tactic:
constructor
State after:
case a.mp
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ k < m ∧ m ≤ 1 + k → m = k + 1

case a.mpr
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ m = k + 1 → k < m ∧ m ≤ 1 + k

State before:
case a.mp
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ k < m ∧ m ≤ 1 + k → m = k + 1
Tactic:
exact fun ⟨h₁, h₂⟩ ↦ by rw [add_comm] at h₂; exact Int.le_antisymm h₂ h₁
State after:
no goals

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
x✝ : k < m ∧ m ≤ 1 + k
h₁ : k < m
h₂ : m ≤ 1 + k
⊢ m = k + 1
Tactic:
rw [add_comm] at h₂
State after:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
x✝ : k < m ∧ m ≤ 1 + k
h₁ : k < m
h₂ : m ≤ k + 1
⊢ m = k + 1

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
x✝ : k < m ∧ m ≤ 1 + k
h₁ : k < m
h₂ : m ≤ k + 1
⊢ m = k + 1
Tactic:
exact Int.le_antisymm h₂ h₁
State after:
no goals

State before:
case a.mpr
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ m = k + 1 → k < m ∧ m ≤ 1 + k
Tactic:
exact fun h ↦ ⟨by simp [h], by simp [h, add_comm]⟩
State after:
no goals

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
h : m = k + 1
⊢ k < m
Tactic:
simp [h]
State after:
no goals

State before:
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
h : m = k + 1
⊢ m ≤ 1 + k
Tactic:
simp [h, add_comm]
State after:
no goals