Theorem: ZetaSum_aux1_2 (PrimeNumberTheoremAnd/ZetaBounds.lean)

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))]
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

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⟩)
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

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
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

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]
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)

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
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]]

State before:
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]]
Tactic:
intro x hx
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
x : ℝ
hx : x ∈ [[a, b]]
⊢ (fun x => 1 / x ^ (c + 1)) x = (fun x => x ^ (-c - 1)) x

State before:
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
x : ℝ
hx : x ∈ [[a, b]]
⊢ (fun x => 1 / x ^ (c + 1)) x = (fun x => x ^ (-c - 1)) x
Tactic:
have : 0 ≤ x := (ZetaSum_aux1_1 apos a_lt_b hx).le
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
x : ℝ
hx : x ∈ [[a, b]]
this : 0 ≤ x
⊢ (fun x => 1 / x ^ (c + 1)) x = (fun x => x ^ (-c - 1)) x

State before:
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
x : ℝ
hx : x ∈ [[a, b]]
this : 0 ≤ x
⊢ (fun x => 1 / x ^ (c + 1)) x = (fun x => x ^ (-c - 1)) x
Tactic:
simp [div_rpow_eq_rpow_neg _ _ _ this, sub_eq_add_neg, add_comm]
State after:
no goals

State before:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
⊢ (a ^ (-c) - b ^ (-c)) / c = (b ^ (-c) - a ^ (-c)) / -c
Tactic:
ring
State after:
no goals

State before:
a b c : ℝ
apos : 0 < a
a_lt_b : a < b
h : c ≠ 0 ∧ 0 ∉ [[a, b]]
⊢ -c - 1 ≠ -1
Tactic:
simp [h.1]
State after:
no goals