Theorem: ZetaBnd_aux1b (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ ‖∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ ↑N ^ (-σ) / σ
Tactic:
apply le_trans (by apply norm_integral_le_integral_norm)
State after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ ∫ (a : ℝ) in Ioi ↑N, ‖(↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)‖ ≤ ↑N ^ (-σ) / σ

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ ∫ (a : ℝ) in Ioi ↑N, ‖(↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)‖ ≤ ↑N ^ (-σ) / σ
Tactic:
apply le_of_tendsto (x := atTop (α := ℝ)) (f := fun (t : ℝ) ↦ ∫ (x : ℝ) in N..t,
  ‖(⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ (σ + t * I + 1)‖) ?_ ?_
State after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ Tendsto (fun t => ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) atTop
    (𝓝 (∫ (a : ℝ) in Ioi ↑N, ‖(↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)‖))

N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ ∀ᶠ (c : ℝ) in atTop, (fun t => ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) c ≤ ↑N ^ (-σ) / σ

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ ‖∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ ?m.335483
Tactic:
apply norm_integral_le_integral_norm
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ Tendsto (fun t => ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) atTop
    (𝓝 (∫ (a : ℝ) in Ioi ↑N, ‖(↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)‖))
Tactic:
apply intervalIntegral_tendsto_integral_Ioi (μ := volume) (l := atTop) (b := id)
  (f := fun (x : ℝ) ↦ ‖(⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ (σ + t * I + 1)‖) N ?_ ?_ |>.congr' ?_
State after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ (fun i => ∫ (x : ℝ) in ↑N..id i, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) =ᶠ[atTop] fun t =>
    ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖

N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ IntegrableOn (fun x => ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) (Ioi ↑N) volume

N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ Tendsto id atTop atTop

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ (fun i => ∫ (x : ℝ) in ↑N..id i, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) =ᶠ[atTop] fun t =>
    ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖
Tactic:
filter_upwards [Filter.mem_atTop ((N : ℝ))]
State after:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ ∀ (a : ℝ),
    ↑N ≤ a →
      ∫ (x : ℝ) in ↑N..id a, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ =
        ∫ (x : ℝ) in ↑N..a, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑a * I + 1)‖

State before:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ ∀ (a : ℝ),
    ↑N ≤ a →
      ∫ (x : ℝ) in ↑N..id a, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ =
        ∫ (x : ℝ) in ↑N..a, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑a * I + 1)‖
Tactic:
intro u hu
State after:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
⊢ ∫ (x : ℝ) in ↑N..id u, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ =
    ∫ (x : ℝ) in ↑N..u, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑u * I + 1)‖

State before:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
⊢ ∫ (x : ℝ) in ↑N..id u, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ =
    ∫ (x : ℝ) in ↑N..u, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑u * I + 1)‖
Tactic:
simp only [id_eq, intervalIntegral.integral_of_le hu, norm_div, norm_eq_abs]
State after:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
⊢ ∫ (x : ℝ) in Ioc (↑N) u, Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑t * I + 1)) ∂volume =
    ∫ (x : ℝ) in Ioc (↑N) u, Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1)) ∂volume

State before:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
⊢ ∫ (x : ℝ) in Ioc (↑N) u, Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑t * I + 1)) ∂volume =
    ∫ (x : ℝ) in Ioc (↑N) u, Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1)) ∂volume
Tactic:
apply setIntegral_congr (by simp)
State after:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
⊢ EqOn (fun x => Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑t * I + 1)))
    (fun x => Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1))) (Ioc (↑N) u)

State before:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
⊢ EqOn (fun x => Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑t * I + 1)))
    (fun x => Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1))) (Ioc (↑N) u)
Tactic:
intro x hx
State after:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ (fun x => Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑t * I + 1))) x =
    (fun x => Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1))) x

State before:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ (fun x => Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑t * I + 1))) x =
    (fun x => Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1))) x
Tactic:
beta_reduce
State after:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑t * I + 1)) =
    Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1))

State before:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑t * I + 1)) =
    Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1))
Tactic:
iterate 2 (rw [abs_cpow_eq_rpow_re_of_pos (by linarith [hx.1])])
State after:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑t * I + 1).re =
    Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑u * I + 1).re

State before:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑t * I + 1).re =
    Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑u * I + 1).re
Tactic:
simp
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
⊢ MeasurableSet (Ioc (↑N) u)
Tactic:
simp
State after:
no goals

State before:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑t * I + 1).re =
    Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1))
Tactic:
(rw [abs_cpow_eq_rpow_re_of_pos (by linarith [hx.1])])
State after:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑t * I + 1).re =
    Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑u * I + 1).re

State before:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑t * I + 1).re =
    Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / Complex.abs (↑x ^ (↑σ + ↑u * I + 1))
Tactic:
rw [abs_cpow_eq_rpow_re_of_pos (by linarith [hx.1])]
State after:
case h
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑t * I + 1).re =
    Complex.abs (↑⌊x⌋ + 1 / 2 - ↑x) / x ^ (↑σ + ↑u * I + 1).re

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
x : ℝ
hx : x ∈ Ioc (↑N) u
⊢ 0 < x
Tactic:
linarith [hx.1]
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ IntegrableOn (fun x => ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) (Ioi ↑N) volume
Tactic:
apply IntegrableOn.integrable ?_ |>.norm
State after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ IntegrableOn (fun a => (↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)) (Ioi ↑N) volume

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ IntegrableOn (fun a => (↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)) (Ioi ↑N) volume
Tactic:
convert integrableOn_of_Zeta0_fun (s := σ + t * I) Npos (by simp [σpos]) using 1
State after:
case h.e'_5
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ (fun a => (↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)) = fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(↑σ + ↑t * I + 1))

State before:
case h.e'_5
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ (fun a => (↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)) = fun x => (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(↑σ + ↑t * I + 1))
Tactic:
simp_rw [div_eq_mul_inv, cpow_neg]
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ 0 < (↑σ + ↑t * I).re
Tactic:
simp [σpos]
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ Tendsto id atTop atTop
Tactic:
exact fun ⦃_⦄ a ↦ a
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ ∀ᶠ (c : ℝ) in atTop, (fun t => ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) c ≤ ↑N ^ (-σ) / σ
Tactic:
filter_upwards [mem_atTop (N + 1 : ℝ)] with t ht
State after:
case h
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
⊢ ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ ↑N ^ (-σ) / σ

State before:
case h
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
⊢ ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ ↑N ^ (-σ) / σ
Tactic:
have : (N ^ (-σ) - t ^ (-σ)) / σ ≤ N ^ (-σ) / σ :=
  div_le_div_right σpos |>.mpr (by simp [Real.rpow_nonneg (by linarith)])
State after:
case h
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
this : (↑N ^ (-σ) - t ^ (-σ)) / σ ≤ ↑N ^ (-σ) / σ
⊢ ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ ↑N ^ (-σ) / σ

State before:
case h
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
this : (↑N ^ (-σ) - t ^ (-σ)) / σ ≤ ↑N ^ (-σ) / σ
⊢ ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ ↑N ^ (-σ) / σ
Tactic:
apply le_trans ?_ this
State after:
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
this : (↑N ^ (-σ) - t ^ (-σ)) / σ ≤ ↑N ^ (-σ) / σ
⊢ ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ (↑N ^ (-σ) - t ^ (-σ)) / σ

State before:
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
this : (↑N ^ (-σ) - t ^ (-σ)) / σ ≤ ↑N ^ (-σ) / σ
⊢ ∫ (x : ℝ) in ↑N..t, ‖(↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ (↑N ^ (-σ) - t ^ (-σ)) / σ
Tactic:
convert ZetaBnd_aux1a (a := N) (b := t) (by positivity) (by linarith) ?_ <;> simp [σpos]
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
⊢ ↑N ^ (-σ) - t ^ (-σ) ≤ ↑N ^ (-σ)
Tactic:
simp [Real.rpow_nonneg (by linarith)]
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
⊢ 0 ≤ ?m.357753
Tactic:
linarith
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
this : (↑N ^ (-σ) - t ^ (-σ)) / σ ≤ ↑N ^ (-σ) / σ
⊢ 0 < ↑N
Tactic:
positivity
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
this : (↑N ^ (-σ) - t ^ (-σ)) / σ ≤ ↑N ^ (-σ) / σ
⊢ ↑N < t
Tactic:
linarith
State after:
no goals