Theorem: ZetaSum_aux1_5d (PrimeNumberTheoremAnd/ZetaBounds.lean)

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:
set g : ℝ → ℝ := (fun u ↦ |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1))
State after:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ IntervalIntegrable g MeasureTheory.volume a b

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ IntervalIntegrable g MeasureTheory.volume a b
Tactic:
apply ZetaSum_aux1_5b apos a_lt_b σpos |>.mono_fun ZetaSum_aux1_5c ?_
State after:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ (fun x => ‖|↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1)‖) ≤ᵐ[MeasureTheory.volume.restrict (Ι a b)] fun x =>
    ‖1 / x ^ (s.re + 1)‖

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
⊢ (fun x => ‖|↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1)‖) ≤ᵐ[MeasureTheory.volume.restrict (Ι a b)] fun x =>
    ‖1 / x ^ (s.re + 1)‖
Tactic:
filter_upwards with x
State after:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ ‖|↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1)‖ ≤ ‖1 / x ^ (s.re + 1)‖

State before:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ ‖|↑⌊x⌋ + 1 / 2 - x| / x ^ (s.re + 1)‖ ≤ ‖1 / x ^ (s.re + 1)‖
Tactic:
simp only [g, Real.norm_eq_abs, one_div, norm_inv, abs_div, _root_.abs_abs]
State after:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 2⁻¹ - x| / |x ^ (s.re + 1)| ≤ |x ^ (s.re + 1)|⁻¹

State before:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 2⁻¹ - x| / |x ^ (s.re + 1)| ≤ |x ^ (s.re + 1)|⁻¹
Tactic:
conv => rw [div_eq_mul_inv, ← one_div]; rhs; rw [← one_mul |x ^ (s.re + 1)|⁻¹]
State after:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 1 / 2 - x| * |x ^ (s.re + 1)|⁻¹ ≤ 1 * |x ^ (s.re + 1)|⁻¹

State before:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 1 / 2 - x| * |x ^ (s.re + 1)|⁻¹ ≤ 1 * |x ^ (s.re + 1)|⁻¹
Tactic:
refine mul_le_mul ?_ (le_refl _) (by simp) <| by norm_num
State after:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 1 / 2 - x| ≤ 1

State before:
case h
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ |↑⌊x⌋ + 1 / 2 - x| ≤ 1
Tactic:
exact le_trans (ZetaSum_aux1_3 x) <| by norm_num
State after:
no goals

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ 0 ≤ |x ^ (s.re + 1)|⁻¹
Tactic:
simp
State after:
no goals

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ 0 ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
a b : ℝ
apos : 0 < a
a_lt_b : a < b
s : ℂ
σpos : 0 < s.re
g : ℝ → ℝ := fun u => |↑⌊u⌋ + 1 / 2 - u| / u ^ (s.re + 1)
x : ℝ
⊢ 1 / 2 ≤ 1
Tactic:
norm_num
State after:
no goals