Theorem: ZetaBnd_aux1a (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∫ (x : ℝ) in a..b, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤ (a ^ (-s.re) - b ^ (-s.re)) / s.re
Tactic:
calc
  _ = ∫ x in a..b, |(⌊x⌋ + 1 / 2 - x)| / x ^ (s+1).re := ZetaSum_aux1_4 apos a_lt_b
  _ ≤ ∫ x in a..b, 1 / x ^ (s.re + 1) := ZetaSum_aux1_5 apos a_lt_b σpos
  _ = (a ^ (-s.re) - b ^ (-s.re)) / s.re := ?_
State after:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (s.re + 1) = (a ^ (-s.re) - b ^ (-s.re)) / s.re

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∫ (x : ℝ) in a..b, 1 / x ^ (s.re + 1) = (a ^ (-s.re) - b ^ (-s.re)) / s.re
Tactic:
refine ZetaSum_aux1_2 (c := s.re) apos a_lt_b ⟨ne_of_gt σpos, ?_⟩
State after:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ 0 ∉ [[a, b]]

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ 0 ∉ [[a, b]]
Tactic:
exact fun h ↦ (lt_self_iff_false 0).mp <| ZetaSum_aux1_1 apos a_lt_b h
State after:
no goals