Theorem: ZetaSum_aux1_5 (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.re + 1) ≤ ∫ (x : ℝ) in a..b, 1 / x ^ (s.re + 1)
Tactic:
apply intervalIntegral.integral_mono_on (le_of_lt a_lt_b) ?_ ?_
State after:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∀ x ∈ Icc a b, |↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1) ≤ 1 / x ^ (s.re + 1)

a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)) MeasureTheory.volume a b

a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => 1 / u ^ (s.re + 1)) MeasureTheory.volume a b

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ ∀ x ∈ Icc a b, |↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1) ≤ 1 / x ^ (s.re + 1)
Tactic:
exact ZetaSum_aux1_5a apos
State after:
no goals

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)) MeasureTheory.volume a b
Tactic:
exact ZetaSum_aux1_5d apos a_lt_b σpos
State after:
no goals

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
⊢ IntervalIntegrable (fun u => 1 / u ^ (s.re + 1)) MeasureTheory.volume a b
Tactic:
exact ZetaSum_aux1_5b apos a_lt_b σpos
State after:
no goals