Theorem: integrableOn_of_Zeta0_fun (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.IntegrableOn (fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) (Ioi ↑N) MeasureTheory.volume
Tactic:
apply MeasureTheory.Integrable.bdd_mul ?_ ?_
State after:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∃ C, ∀ (x : ℝ), ‖↑⌊x⌋ + 1 / 2 - ↑x‖ ≤ C

N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.Integrable (fun x => ↑x ^ (-(s + 1))) (MeasureTheory.volume.restrict (Ioi ↑N))

N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.AEStronglyMeasurable (fun x => ↑⌊x⌋ + 1 / 2 - ↑x) (MeasureTheory.volume.restrict (Ioi ↑N))

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∃ C, ∀ (x : ℝ), ‖↑⌊x⌋ + 1 / 2 - ↑x‖ ≤ C
Tactic:
convert ZetaSum_aux2a
State after:
case h.e'_2.h.h.h.e'_3
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x✝ a✝ : ℝ
⊢ ‖↑⌊a✝⌋ + 1 / 2 - ↑a✝‖ = |↑⌊a✝⌋ + 1 / 2 - a✝|

State before:
case h.e'_2.h.h.h.e'_3
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x✝ a✝ : ℝ
⊢ ‖↑⌊a✝⌋ + 1 / 2 - ↑a✝‖ = |↑⌊a✝⌋ + 1 / 2 - a✝|
Tactic:
simp [← Complex.abs_ofReal]
State after:
no goals

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.Integrable (fun x => ↑x ^ (-(s + 1))) (MeasureTheory.volume.restrict (Ioi ↑N))
Tactic:
apply integrableOn_Ioi_cpow_iff (by positivity) |>.mpr (by simp [s_re_gt])
State after:
no goals

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ 0 < ↑N
Tactic:
positivity
State after:
no goals

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ (-(s + 1)).re < -1
Tactic:
simp [s_re_gt]
State after:
no goals

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.AEStronglyMeasurable (fun x => ↑⌊x⌋ + 1 / 2 - ↑x) (MeasureTheory.volume.restrict (Ioi ↑N))
Tactic:
refine Measurable.add ?_ measurable_const |>.sub (by fun_prop) |>.aestronglyMeasurable
State after:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable fun x => ↑⌊x⌋

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable fun x => ↑⌊x⌋
Tactic:
exact Measurable.comp (by exact fun _ _ ↦ trivial) Int.measurable_floor
State after:
no goals

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable fun x => ↑x
Tactic:
fun_prop
State after:
no goals

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable IntCast.intCast
Tactic:
exact fun _ _ ↦ trivial
State after:
no goals