Theorem: ZetaSum_aux1 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))
Tactic:
let φ := fun (x : ℝ) ↦ 1 / (x : ℂ) ^ s
State after:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

State before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))
Tactic:
let φ' := fun (x : ℝ) ↦ -s * (x : ℂ) ^ (-(s + 1))
State after:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

State before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))
Tactic:
have xpos : ∀ x ∈ [[(a : ℝ), b]], 0 < x := fun x hx ↦ xpos_of_uIcc ha hx
State after:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

State before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))
Tactic:
have φDiff : ∀ x ∈ [[(a : ℝ), b]], HasDerivAt φ (deriv φ x) x := fun x hx ↦ ZetaSum_aux1φDiff (xpos x hx)
State after:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

State before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))
Tactic:
have φderiv : ∀ x ∈ [[(a : ℝ), b]], deriv φ x = φ' x := by
  exact fun x hx ↦ ZetaSum_aux1φderiv s_ne_zero (xpos x hx)
State after:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

State before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))
Tactic:
have derivφCont : ContinuousOn (deriv φ) [[a, b]] := ZetaSum_aux1derivφCont s_ne_zero ha
State after:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

State before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))
Tactic:
convert sum_eq_int_deriv (by exact_mod_cast ha.2) φDiff derivφCont using 1
State after:
case h.e'_2
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s = ∑ n ∈ Finset.Ioc ⌊↑a⌋ ⌊↑b⌋, φ ↑n

case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) =
    (∫ (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 : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
⊢ ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
Tactic:
exact fun x hx ↦ ZetaSum_aux1φderiv s_ne_zero (xpos x hx)
State after:
no goals

State before:
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ ↑a < ↑b
Tactic:
exact_mod_cast ha.2
State after:
no goals

State before:
case h.e'_2
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ ∑ n ∈ Finset.Ioc ↑a ↑b, 1 / ↑n ^ s = ∑ n ∈ Finset.Ioc ⌊↑a⌋ ⌊↑b⌋, φ ↑n
Tactic:
congr <;> simp only [Int.floor_natCast]
State after:
no goals

State before:
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      s * ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) =
    (∫ (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:
rw [Int.floor_natCast, Int.floor_natCast, ← intervalIntegral.integral_const_mul]
State after:
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) =
    (∫ (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:
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) =
    (∫ (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:
simp_rw [mul_div, ← mul_div, ZetaSum_aux1₁ s_ne_one ha]
State after:
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + (↑↑b + 1 / 2 - ↑↑b) * φ ↑b - (↑↑a + 1 / 2 - ↑↑a) * φ ↑a -
      ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x

State before:
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + (↑↑b + 1 / 2 - ↑↑b) * φ ↑b - (↑↑a + 1 / 2 - ↑↑a) * φ ↑a -
      ∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
Tactic:
conv => rhs; rw [sub_eq_add_neg]
State after:
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + (↑↑b + 1 / 2 - ↑↑b) * φ ↑b - (↑↑a + 1 / 2 - ↑↑a) * φ ↑a +
      -∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x

State before:
case h.e'_3
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑b ^ s) - 1 / 2 * (1 / ↑a ^ s) +
      ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) =
    (↑b ^ (1 - s) - ↑a ^ (1 - s)) / (1 - s) + (↑↑b + 1 / 2 - ↑↑b) * φ ↑b - (↑↑a + 1 / 2 - ↑↑a) * φ ↑a +
      -∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
Tactic:
congr
State after:
case h.e'_3.e_a.e_a.e_a.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ 1 / 2 = ↑↑b + 1 / 2 - ↑↑b

case h.e'_3.e_a.e_a.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ 1 / 2 = ↑↑a + 1 / 2 - ↑↑a

case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) =
    -∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x

State before:
case h.e'_3.e_a.e_a.e_a.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ 1 / 2 = ↑↑b + 1 / 2 - ↑↑b

case h.e'_3.e_a.e_a.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ 1 / 2 = ↑↑a + 1 / 2 - ↑↑a

case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) =
    -∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
Tactic:
any_goals norm_cast; simp only [one_div, add_sub_cancel_left]
State after:
case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 2⁻¹ - ↑x) * ↑x ^ (-(s + 1))) = -∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 2⁻¹ - ↑x) * deriv φ x

State before:
case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 2⁻¹ - ↑x) * ↑x ^ (-(s + 1))) = -∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 2⁻¹ - ↑x) * deriv φ x
Tactic:
rw [← intervalIntegral.integral_neg, intervalIntegral.integral_congr]
State after:
case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ EqOn (fun x => s * ((↑⌊x⌋ + 2⁻¹ - ↑x) * ↑x ^ (-(s + 1)))) (fun x => -((↑⌊x⌋ + 2⁻¹ - ↑x) * deriv φ x)) [[↑a, ↑b]]

State before:
case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ EqOn (fun x => s * ((↑⌊x⌋ + 2⁻¹ - ↑x) * ↑x ^ (-(s + 1)))) (fun x => -((↑⌊x⌋ + 2⁻¹ - ↑x) * deriv φ x)) [[↑a, ↑b]]
Tactic:
intro x hx
State after:
case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
x : ℝ
hx : x ∈ [[↑a, ↑b]]
⊢ (fun x => s * ((↑⌊x⌋ + 2⁻¹ - ↑x) * ↑x ^ (-(s + 1)))) x = (fun x => -((↑⌊x⌋ + 2⁻¹ - ↑x) * deriv φ x)) x

State before:
case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
x : ℝ
hx : x ∈ [[↑a, ↑b]]
⊢ (fun x => s * ((↑⌊x⌋ + 2⁻¹ - ↑x) * ↑x ^ (-(s + 1)))) x = (fun x => -((↑⌊x⌋ + 2⁻¹ - ↑x) * deriv φ x)) x
Tactic:
simp_rw [φderiv x hx, φ']
State after:
case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
x : ℝ
hx : x ∈ [[↑a, ↑b]]
⊢ s * ((↑⌊x⌋ + 2⁻¹ - ↑x) * ↑x ^ (-(s + 1))) = -((↑⌊x⌋ + 2⁻¹ - ↑x) * (-s * ↑x ^ (-(s + 1))))

State before:
case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
x : ℝ
hx : x ∈ [[↑a, ↑b]]
⊢ s * ((↑⌊x⌋ + 2⁻¹ - ↑x) * ↑x ^ (-(s + 1))) = -((↑⌊x⌋ + 2⁻¹ - ↑x) * (-s * ↑x ^ (-(s + 1))))
Tactic:
ring_nf
State after:
no goals

State before:
case h.e'_3.e_a.e_a.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ 1 / 2 = ↑↑a + 1 / 2 - ↑↑a
Tactic:
norm_cast
State after:
case h.e'_3.e_a.e_a.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ 1 / 2 = ↑a + 1 / 2 - ↑a

State before:
case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) =
    -∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 1 / 2 - ↑x) * deriv φ x
Tactic:
simp only [one_div, add_sub_cancel_left]
State after:
case h.e'_3.e_a
a b : ℕ
s : ℂ
s_ne_one : s ≠ 1
s_ne_zero : s ≠ 0
ha : a ∈ Ioo 0 b
φ : ℝ → ℂ := fun x => 1 / ↑x ^ s
φ' : ℝ → ℂ := fun x => -s * ↑x ^ (-(s + 1))
xpos : ∀ x ∈ [[↑a, ↑b]], 0 < x
φDiff : ∀ x ∈ [[↑a, ↑b]], HasDerivAt φ (deriv φ x) x
φderiv : ∀ x ∈ [[↑a, ↑b]], deriv φ x = φ' x
derivφCont : ContinuousOn (deriv φ) [[↑a, ↑b]]
⊢ ∫ (x : ℝ) in ↑a..↑b, s * ((↑⌊x⌋ + 2⁻¹ - ↑x) * ↑x ^ (-(s + 1))) = -∫ (x : ℝ) in ↑a..↑b, (↑⌊x⌋ + 2⁻¹ - ↑x) * deriv φ x