Theorem: integrableOn_of_Zeta0_fun_log (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ IntegrableOn (fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)) * -↑x.log) (Ioi ↑N) volume
Tactic:
simp_rw [mul_assoc]
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ IntegrableOn (fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * (↑x ^ (-(s + 1)) * -↑x.log)) (Ioi ↑N) volume

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ IntegrableOn (fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * (↑x ^ (-(s + 1)) * -↑x.log)) (Ioi ↑N) volume
Tactic:
apply Integrable.bdd_mul ?_ ?_ ?_
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun x => ↑x ^ (-(s + 1)) * -↑x.log) (volume.restrict (Ioi ↑N))

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

N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∃ C, ∀ (x : ℝ), ‖↑⌊x⌋ + 1 / 2 - ↑x‖ ≤ C

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun x => ↑x ^ (-(s + 1)) * -↑x.log) (volume.restrict (Ioi ↑N))
Tactic:
simp only [neg_add_rev, mul_neg, add_comm, ← sub_eq_add_neg]
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun x => -(↑x ^ (-s - 1) * ↑x.log)) (volume.restrict (Ioi ↑N))

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun x => -(↑x ^ (-s - 1) * ↑x.log)) (volume.restrict (Ioi ↑N))
Tactic:
apply integrable_norm_iff ?_ |>.mp ?_ |>.neg
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ AEStronglyMeasurable (fun x => ↑x ^ (-s - 1) * ↑x.log) (volume.restrict (Ioi ↑N))

N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun a => ‖↑a ^ (-s - 1) * ↑a.log‖) (volume.restrict (Ioi ↑N))

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ AEStronglyMeasurable (fun x => ↑x ^ (-s - 1) * ↑x.log) (volume.restrict (Ioi ↑N))
Tactic:
apply ContinuousOn.mul ?_ ?_ |>.aestronglyMeasurable (by simp)
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn (fun x => ↑x ^ (-s - 1)) (Ioi ↑N)

N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn (fun x => ↑x.log) (Ioi ↑N)

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasurableSet (Ioi ↑N)
Tactic:
simp
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn (fun x => ↑x ^ (-s - 1)) (Ioi ↑N)
Tactic:
intro x hx
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ContinuousWithinAt (fun x => ↑x ^ (-s - 1)) (Ioi ↑N) x

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ContinuousWithinAt (fun x => ↑x ^ (-s - 1)) (Ioi ↑N) x
Tactic:
apply ContinuousWithinAt.cpow ?_ continuous_const.continuousWithinAt ?_
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ContinuousWithinAt (fun x => ↑x) (Ioi ↑N) x

N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ↑x ∈ slitPlane

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ContinuousWithinAt (fun x => ↑x) (Ioi ↑N) x
Tactic:
exact RCLike.continuous_ofReal.continuousWithinAt
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ ↑x ∈ slitPlane
Tactic:
simp only [ofReal_mem_slitPlane]
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ 0 < x

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ 0 < x
Tactic:
linarith [mem_Ioi.mp hx]
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn (fun x => ↑x.log) (Ioi ↑N)
Tactic:
apply RCLike.continuous_ofReal.continuousOn.comp ?_ (mapsTo_image _ _)
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn
    (fun x =>
      Decidable.rec (fun h => (fun hx => Real.expOrderIso.symm ⟨|x|, ⋯⟩) h) (fun h => (fun hx => 0) h)
        (x.decidableEq 0))
    (Ioi ↑N)

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ContinuousOn
    (fun x =>
      Decidable.rec (fun h => (fun hx => Real.expOrderIso.symm ⟨|x|, ⋯⟩) h) (fun h => (fun hx => 0) h)
        (x.decidableEq 0))
    (Ioi ↑N)
Tactic:
refine continuous_id.continuousOn.log ?_
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∀ x ∈ Ioi ↑N, id x ≠ 0

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∀ x ∈ Ioi ↑N, id x ≠ 0
Tactic:
intro x hx
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ id x ≠ 0

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ id x ≠ 0
Tactic:
simp only [id_eq]
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ x ≠ 0

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x : ℝ
hx : x ∈ Ioi ↑N
⊢ x ≠ 0
Tactic:
linarith [mem_Ioi.mp hx]
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun a => ‖↑a ^ (-s - 1) * ↑a.log‖) (volume.restrict (Ioi ↑N))
Tactic:
simp only [norm_mul, norm_eq_abs, abs_ofReal]
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (volume.restrict (Ioi ↑N))

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Integrable (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (volume.restrict (Ioi ↑N))
Tactic:
have := integrable_log_over_pow (r := -s.re) (by linarith) Npos
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ Integrable (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (volume.restrict (Ioi ↑N))

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ Integrable (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (volume.restrict (Ioi ↑N))
Tactic:
apply IntegrableOn.congr_fun this ?_ (by simp)
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ EqOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (Ioi ↑N)

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ EqOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) (Ioi ↑N)
Tactic:
intro x hx
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ (fun x => |x ^ (-s.re - 1)| * |x.log|) x = (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) x

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ (fun x => |x ^ (-s.re - 1)| * |x.log|) x = (fun a => Complex.abs (↑a ^ (-s - 1)) * |a.log|) x
Tactic:
simp only [mul_eq_mul_right_iff, abs_eq_zero, Real.log_eq_zero]
State after:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1)) ∨ x = 0 ∨ x = 1 ∨ x = -1

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1)) ∨ x = 0 ∨ x = 1 ∨ x = -1
Tactic:
left
State after:
case h
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1))

State before:
case h
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1))
Tactic:
have xpos : 0 < x := by linarith [mem_Ioi.mp hx]
State after:
case h
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
xpos : 0 < x
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1))

State before:
case h
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
xpos : 0 < x
⊢ |x ^ (-s.re - 1)| = Complex.abs (↑x ^ (-s - 1))
Tactic:
simp [abs_cpow_eq_rpow_re_of_pos xpos, Real.abs_rpow_of_nonneg xpos.le,
  abs_eq_self.mpr xpos.le]
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ -s.re < 0
Tactic:
linarith
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
⊢ MeasurableSet (Ioi ↑N)
Tactic:
simp
State after:
no goals

State before:
N : ℕ
Npos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
this : IntegrableOn (fun x => |x ^ (-s.re - 1)| * |x.log|) (Ioi ↑N) volume
x : ℝ
hx : x ∈ Ioi ↑N
⊢ 0 < x
Tactic:
linarith [mem_Ioi.mp hx]
State after:
no goals

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

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

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

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

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