Theorem: sum_eq_int_deriv_aux (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 ⌊a⌋ ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
Tactic:
have fl_a_eq_k : ⌊a⌋ = k := Int.floor_eq_iff.mpr ⟨ha.1, by linarith [ha.2]⟩
State after:
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∑ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x

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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∑ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋, φ ↑n =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a -
      ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
Tactic:
convert sum_eq_int_deriv_aux1 ha b_le_kpOne φDiff derivφCont using 2
State after:
case h.e'_2.h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ Finset.Ioc ⌊a⌋ ⌊b⌋ = Finset.Ioc k ⌊b⌋

case h.e'_3.h.e'_5
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a

case h.e'_3.h.e'_6
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x

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]]
⊢ a < ↑k + 1
Tactic:
linarith [ha.2]
State after:
no goals

State before:
case h.e'_2.h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ Finset.Ioc ⌊a⌋ ⌊b⌋ = Finset.Ioc k ⌊b⌋
Tactic:
rw [fl_a_eq_k]
State after:
no goals

State before:
case h.e'_3.h.e'_5
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑⌊a⌋ + 1 / 2 - ↑a) * φ a =
    (∫ (x : ℝ) in a..b, φ x) + (↑⌊b⌋ + 1 / 2 - ↑b) * φ b - (↑k + 1 / 2 - ↑a) * φ a
Tactic:
congr
State after:
no goals

State before:
case h.e'_3.h.e'_6
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∫ (x : ℝ) in a..b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = ∫ (x : ℝ) in a..b, (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
apply intervalIntegral.integral_congr_ae
State after:
case h.e'_3.h.e'_6.h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∀ᵐ (x : ℝ), x ∈ Ι a b → (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x

State before:
case h.e'_3.h.e'_6.h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∀ᵐ (x : ℝ), x ∈ Ι a b → (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
have : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume, x ≠ b := by
  convert Countable.ae_not_mem (s := {b}) (by simp) (μ := MeasureTheory.volume) using 1
State after:
case h.e'_3.h.e'_6.h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
⊢ ∀ᵐ (x : ℝ), x ∈ Ι a b → (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x

State before:
case h.e'_3.h.e'_6.h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
⊢ ∀ᵐ (x : ℝ), x ∈ Ι a b → (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
filter_upwards [this]
State after:
case h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
⊢ ∀ (a_1 : ℝ), a_1 ≠ b → a_1 ∈ Ι a b → (↑⌊a_1⌋ + 1 / 2 - ↑a_1) * deriv φ a_1 = (↑k + 1 / 2 - ↑a_1) * deriv φ a_1

State before:
case h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
⊢ ∀ (a_1 : ℝ), a_1 ≠ b → a_1 ∈ Ι a b → (↑⌊a_1⌋ + 1 / 2 - ↑a_1) * deriv φ a_1 = (↑k + 1 / 2 - ↑a_1) * deriv φ a_1
Tactic:
intro x x_ne_b hx
State after:
case h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : x ∈ Ι a b
⊢ (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x

State before:
case h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : x ∈ Ι a b
⊢ (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
rw [uIoc_of_le ha.2.le, mem_Ioc] at hx
State after:
case h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x

State before:
case h
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x = (↑k + 1 / 2 - ↑x) * deriv φ x
Tactic:
congr
State after:
case h.e_a.e_a.e_a.e_a
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ ⌊x⌋ = k

State before:
case h.e_a.e_a.e_a.e_a
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ ⌊x⌋ = k
Tactic:
exact Int.floor_eq_iff.mpr ⟨by linarith [ha.1], by have := Ne.lt_of_le x_ne_b hx.2; linarith⟩
State after:
no goals

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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ ∀ᵐ (x : ℝ), x ≠ b
Tactic:
convert Countable.ae_not_mem (s := {b}) (by simp) (μ := MeasureTheory.volume) using 1
State after:
no goals

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]]
fl_a_eq_k : ⌊a⌋ = k
⊢ {b}.Countable
Tactic:
simp
State after:
no goals

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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ ↑k ≤ x
Tactic:
linarith [ha.1]
State after:
no goals

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]]
fl_a_eq_k : ⌊a⌋ = k
this : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
⊢ x < ↑k + 1
Tactic:
have := Ne.lt_of_le x_ne_b hx.2
State after:
φ : ℝ → ℂ
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]]
fl_a_eq_k : ⌊a⌋ = k
this✝ : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
this : x < b
⊢ x < ↑k + 1

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]]
fl_a_eq_k : ⌊a⌋ = k
this✝ : ∀ᵐ (x : ℝ), x ≠ b
x : ℝ
x_ne_b : x ≠ b
hx : a < x ∧ x ≤ b
this : x < b
⊢ x < ↑k + 1
Tactic:
linarith
State after:
no goals