internlm/Lean-Github huggingface dataset:
Theorem: ZetaSum_aux1
Proof 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
Proof 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))
Theorem: ZetaSum_aux1
Proof 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))
Proof 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))
Theorem: ZetaSum_aux1
Proof 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
Proof 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))
Theorem: ZetaSum_aux1
Proof 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)
Proof 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))
Theorem: ZetaSum_aux1
Proof 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)
Proof 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))
Theorem: ZetaSum_aux1
Proof 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
Proof 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))
Theorem: ZetaSum_aux1
Proof 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
Proof 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
Theorem: ZetaSum_aux1
Proof 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)
Proof state after:
no goals
Theorem: ZetaSum_aux1
Proof 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
Proof state after:
no goals
Theorem: ZetaSum_aux1
Proof 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]
Proof state after:
no goals
Theorem: ZetaSum_aux1
Proof 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]
Proof 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
Theorem: ZetaSum_aux1
Proof 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]
Proof 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
Theorem: ZetaSum_aux1
Proof 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]
Proof 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
Theorem: ZetaSum_aux1
Proof 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
Proof 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
Theorem: ZetaSum_aux1
Proof 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]
Proof 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
Theorem: ZetaSum_aux1
Proof 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]
Proof 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]]
Theorem: ZetaSum_aux1
Proof 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
Proof 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
Theorem: ZetaSum_aux1
Proof 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, φ']
Proof 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))))
Theorem: ZetaSum_aux1
Proof 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
Proof state after:
no goals
Theorem: ZetaSum_aux1
Proof 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
Proof 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
Theorem: ZetaSum_aux1
Proof 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]
Proof 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
Theorem: ZetaSum_aux1_2
Proof state before:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (c + 1) = (a ^ (-c) - b ^ (-c)) / c
Tactic:
rw [(by ring : (a ^ (-c) - b ^ (-c)) / c = (b ^ (-c) - a ^ (-c)) / (-c))]
Proof state after:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (c + 1) = (b ^ (-c) - a ^ (-c)) / -c
Theorem: ZetaSum_aux1_2
Proof state before:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (c + 1) = (b ^ (-c) - a ^ (-c)) / -c
Tactic:
have := integral_rpow (a := a) (b := b) (r := -c-1) (Or.inr ⟨by simp [h.1], h.2⟩)
Proof state after:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c - 1 + 1) - a ^ (-c - 1 + 1)) / (-c - 1 + 1)
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (c + 1) = (b ^ (-c) - a ^ (-c)) / -c
Theorem: ZetaSum_aux1_2
Proof state before:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c - 1 + 1) - a ^ (-c - 1 + 1)) / (-c - 1 + 1)
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (c + 1) = (b ^ (-c) - a ^ (-c)) / -c
Tactic:
simp only [sub_add_cancel] at this
Proof state after:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c) - a ^ (-c)) / -c
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (c + 1) = (b ^ (-c) - a ^ (-c)) / -c
Theorem: ZetaSum_aux1_2
Proof state before:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c) - a ^ (-c)) / -c
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (c + 1) = (b ^ (-c) - a ^ (-c)) / -c
Tactic:
rw [← this]
Proof state after:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c) - a ^ (-c)) / -c
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (c + 1) = ∫ (x : ℝ) in a..b, x ^ (-c - 1)
Theorem: ZetaSum_aux1_2
Proof state before:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c) - a ^ (-c)) / -c
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (c + 1) = ∫ (x : ℝ) in a..b, x ^ (-c - 1)
Tactic:
apply intervalIntegral.integral_congr
Proof state after:
case h
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
this : ∫ (x : ℝ) in a..b, x ^ (-c - 1) = (b ^ (-c) - a ^ (-c)) / -c
⊢ EqOn (fun x => 1 / x ^ (c + 1)) (fun x => x ^ (-c - 1)) [[a, b]]