Source indexedlemma · leanprover/lean4:v4.32.0

integrableOn_of_Zeta0_fun

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:943 to 952

Mathematical statement

Exact Lean statement

lemma integrableOn_of_Zeta0_fun {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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma integrableOn_of_Zeta0_fun {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 := by  obtain ⟨c, hc⟩ := ZetaSum_aux2a  apply MeasureTheory.Integrable.bdd_mul (c := c) ?_ ?_  · apply MeasureTheory.ae_of_all    convert hc; simp only [← Complex.norm_real]; simp  · apply integrableOn_Ioi_cpow_iff (by positivity) |>.mpr (by simp [s_re_gt])  · refine Measurable.add ?_ measurable_const |>.sub (by fun_prop) |>.aestronglyMeasurable    exact Measurable.comp (by exact fun _ _ ↦ trivial) Int.measurable_floor