internlm/Lean-Github huggingface dataset:
Theorem: ZetaSum_aux2
Proof state before:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ ∀ b ≥ N + 1,
    (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) b =
      (fun k =>
          (↑k ^ (1 - s) - ↑N ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) +
            s * ∫ (x : ℝ) in ↑N..↑k, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))
        b
Tactic:
intro k hk
Proof state after:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
k : ℕ
hk : k ≥ N + 1
⊢ (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) k =
    (fun k =>
        (↑k ^ (1 - s) - ↑N ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) +
          s * ∫ (x : ℝ) in ↑N..↑k, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))
      k
Theorem: ZetaSum_aux2
Proof state before:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
k : ℕ
hk : k ≥ N + 1
⊢ (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) k =
    (fun k =>
        (↑k ^ (1 - s) - ↑N ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) +
          s * ∫ (x : ℝ) in ↑N..↑k, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))
      k
Tactic:
convert ZetaSum_aux1 (a := N) (b := k) s_ne_one s_ne_zero ⟨N_pos, hk⟩ using 1
Proof state after:
case h.e'_2
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
k : ℕ
hk : k ≥ N + 1
⊢ (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) k = ∑ n ∈ Finset.Ioc ↑N ↑k, 1 / ↑n ^ s
Theorem: ZetaSum_aux2
Proof state before:
case h.e'_2
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
k : ℕ
hk : k ≥ N + 1
⊢ (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) k = ∑ n ∈ Finset.Ioc ↑N ↑k, 1 / ↑n ^ s
Tactic:
convert Finset_coe_Nat_Int (fun n ↦ 1 / (n : ℂ) ^ s) N k
Proof state after:
no goals
Theorem: ZetaSum_aux2
Proof state before:
case ha.h
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Tactic:
exact ZetaSum_aux3 s_re_gt
Proof state after:
no goals
Theorem: ZetaSum_aux2
Proof state before:
case hb
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto
    (fun k =>
      (↑k ^ (1 - s) - ↑N ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑k ^ s) - 1 / 2 * (1 / ↑N ^ s) +
        s * ∫ (x : ℝ) in ↑N..↑k, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1)))
    atTop (𝓝 (-↑N ^ (1 - s) / (1 - s) - ↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))))
Tactic:
apply (Tendsto.sub ?_ ?_).add (Tendsto.const_mul _ ?_)
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => (↑x ^ (1 - s) - ↑N ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑x ^ s)) atTop (𝓝 (-↑N ^ (1 - s) / (1 - s)))

N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => 1 / 2 * (1 / ↑N ^ s)) atTop (𝓝 (↑N ^ (-s) / 2))

N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun k => ∫ (x : ℝ) in ↑N..↑k, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) atTop
    (𝓝 (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))))
Theorem: ZetaSum_aux2
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => (↑x ^ (1 - s) - ↑N ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑x ^ s)) atTop (𝓝 (-↑N ^ (1 - s) / (1 - s)))
Tactic:
rw [(by ring : -↑N ^ (1 - s) / (1 - s) = (0 - ↑N ^ (1 - s)) / (1 - s) + 0)]
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => (↑x ^ (1 - s) - ↑N ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑x ^ s)) atTop
    (𝓝 ((0 - ↑N ^ (1 - s)) / (1 - s) + 0))
Theorem: ZetaSum_aux2
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => (↑x ^ (1 - s) - ↑N ^ (1 - s)) / (1 - s) + 1 / 2 * (1 / ↑x ^ s)) atTop
    (𝓝 ((0 - ↑N ^ (1 - s)) / (1 - s) + 0))
Tactic:
apply cpow_tendsto s_re_gt |>.sub_const _ |>.div_const _ |>.add
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => 1 / 2 * (1 / ↑x ^ s)) atTop (𝓝 0)
Theorem: ZetaSum_aux2
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => 1 / 2 * (1 / ↑x ^ s)) atTop (𝓝 0)
Tactic:
simp_rw [mul_comm_div, one_mul, one_div, (by congr; ring : 𝓝 (0 : ℂ) = 𝓝 ((0 : ℂ) / 2))]
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => (↑x ^ s)⁻¹ / 2) atTop (𝓝 (0 / 2))
Theorem: ZetaSum_aux2
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => (↑x ^ s)⁻¹ / 2) atTop (𝓝 (0 / 2))
Tactic:
apply Tendsto.div_const <| cpow_inv_tendsto (by positivity)
Proof state after:
no goals
Theorem: ZetaSum_aux2
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ -↑N ^ (1 - s) / (1 - s) = (0 - ↑N ^ (1 - s)) / (1 - s) + 0
Tactic:
ring
Proof state after:
no goals
Theorem: ZetaSum_aux2
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ 𝓝 0 = 𝓝 (0 / 2)
Tactic:
congr
Proof state after:
case e_x
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ 0 = 0 / 2
Theorem: ZetaSum_aux2
Proof state before:
case e_x
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ 0 = 0 / 2
Tactic:
ring
Proof state after:
no goals
Theorem: ZetaSum_aux2
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ 0 < s.re
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaSum_aux2
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => 1 / 2 * (1 / ↑N ^ s)) atTop (𝓝 (↑N ^ (-s) / 2))
Tactic:
simp_rw [mul_comm_div, one_mul, one_div, cpow_neg]
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => (↑N ^ s)⁻¹ / 2) atTop (𝓝 ((↑N ^ s)⁻¹ / 2))
Theorem: ZetaSum_aux2
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun x => (↑N ^ s)⁻¹ / 2) atTop (𝓝 ((↑N ^ s)⁻¹ / 2))
Tactic:
exact tendsto_const_nhds
Proof state after:
no goals
Theorem: ZetaSum_aux2
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ Tendsto (fun k => ∫ (x : ℝ) in ↑N..↑k, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))) atTop
    (𝓝 (∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))))
Tactic:
exact MeasureTheory.intervalIntegral_tendsto_integral_Ioi (a := N)
  (b := (fun (n : ℕ) ↦ (n : ℝ))) (integrableOn_of_Zeta0_fun N_pos <| by positivity) tendsto_coe_atTop
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof 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)
Proof state after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ ∫ (a : ℝ) in Ioi ↑N, ‖(↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)‖ ≤ ↑N ^ (-σ) / σ
Theorem: ZetaBnd_aux1b
Proof 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)‖) ?_ ?_
Proof 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 ^ (-σ) / σ
Theorem: ZetaBnd_aux1b
Proof 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
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof 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' ?_
Proof 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
Theorem: ZetaBnd_aux1b
Proof 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 : ℝ))]
Proof 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)‖
Theorem: ZetaBnd_aux1b
Proof 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
Proof 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)‖
Theorem: ZetaBnd_aux1b
Proof 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]
Proof 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
Theorem: ZetaBnd_aux1b
Proof 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)
Proof 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)
Theorem: ZetaBnd_aux1b
Proof 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
Proof 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
Theorem: ZetaBnd_aux1b
Proof 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
Proof 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))
Theorem: ZetaBnd_aux1b
Proof 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])])
Proof 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
Theorem: ZetaBnd_aux1b
Proof 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
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
u : ℝ
hu : ↑N ≤ u
⊢ MeasurableSet (Ioc (↑N) u)
Tactic:
simp
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof 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])])
Proof 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
Theorem: ZetaBnd_aux1b
Proof 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])]
Proof 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
Theorem: ZetaBnd_aux1b
Proof 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]
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof 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
Proof state after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ IntegrableOn (fun a => (↑⌊a⌋ + 1 / 2 - ↑a) / ↑a ^ (↑σ + ↑t * I + 1)) (Ioi ↑N) volume
Theorem: ZetaBnd_aux1b
Proof 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
Proof 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))
Theorem: ZetaBnd_aux1b
Proof 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]
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ 0 < (↑σ + ↑t * I).re
Tactic:
simp [σpos]
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
σpos : 0 < σ
⊢ Tendsto id atTop atTop
Tactic:
exact fun ⦃_⦄ a ↦ a
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof 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
Proof 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 ^ (-σ) / σ
Theorem: ZetaBnd_aux1b
Proof 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)])
Proof 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 ^ (-σ) / σ
Theorem: ZetaBnd_aux1b
Proof 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
Proof 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 ^ (-σ)) / σ
Theorem: ZetaBnd_aux1b
Proof 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]
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
⊢ ↑N ^ (-σ) - t ^ (-σ) ≤ ↑N ^ (-σ)
Tactic:
simp [Real.rpow_nonneg (by linarith)]
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
⊢ 0 ≤ ?m.357753
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
this : (↑N ^ (-σ) - t ^ (-σ)) / σ ≤ ↑N ^ (-σ) / σ
⊢ 0 < ↑N
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaBnd_aux1b
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t✝ : ℝ
σpos : 0 < σ
t : ℝ
ht : ↑N + 1 ≤ t
this : (↑N ^ (-σ) - t ^ (-σ)) / σ ≤ ↑N ^ (-σ) / σ
⊢ ↑N < t
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaBnd_aux1
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ 2 * |t| * ↑N ^ (-σ) / σ
Tactic:
rw [norm_mul, mul_div_assoc]
Proof state after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ * ‖∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ 2 * |t| * (↑N ^ (-σ) / σ)
Theorem: ZetaBnd_aux1
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ * ‖∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ 2 * |t| * (↑N ^ (-σ) / σ)
Tactic:
apply mul_le_mul ?_ (ZetaBnd_aux1b N Npos hσ.1) (norm_nonneg _) (by positivity)
Proof state after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ ≤ 2 * |t|
Theorem: ZetaBnd_aux1
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ ≤ 2 * |t|
Tactic:
refine le_trans (by apply norm_add_le) ?_
Proof state after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ‖ + ‖↑t * I‖ ≤ 2 * |t|
Theorem: ZetaBnd_aux1
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ‖ + ‖↑t * I‖ ≤ 2 * |t|
Tactic:
simp only [norm_eq_abs, abs_ofReal, norm_mul, abs_I, mul_one, abs_of_pos hσ.1]
Proof state after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ σ + |t| ≤ 2 * |t|
Theorem: ZetaBnd_aux1
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ σ + |t| ≤ 2 * |t|
Tactic:
linarith [hσ.2]
Proof state after:
no goals
Theorem: ZetaBnd_aux1
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ 0 ≤ 2 * |t|
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaBnd_aux1
Proof state before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ ≤ ?m.373229
Tactic:
apply norm_add_le
Proof state after:
no goals
Theorem: isOpen_aux
Proof state before:
⊢ IsOpen {z | z ≠ 1 ∧ 0 < z.re}
Tactic:
refine IsOpen.inter isOpen_ne ?_
Proof state after:
⊢ IsOpen fun z => Real.lt 0 z.re
Theorem: isOpen_aux
Proof state before:
⊢ IsOpen fun z => Real.lt 0 z.re
Tactic:
exact isOpen_lt (g := fun (z : ℂ) ↦ z.re) (by continuity) (by continuity)
Proof state after:
no goals
Theorem: isOpen_aux
Proof state before:
⊢ Continuous fun z => 0
Tactic:
continuity
Proof state after:
no goals
Theorem: isOpen_aux
Proof state before:
⊢ Continuous fun z => z.re
Tactic:
continuity
Proof state after:
no goals
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ioi ↑N) volume
Tactic:
apply IntegrableOn.mono_set (hst := Set.Ioi_subset_Ici <| le_refl (N : ℝ))
Proof state after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ici ↑N) volume
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ici ↑N) volume
Tactic:
apply LocallyIntegrableOn.integrableOn_of_isBigO_atTop (g := fun x ↦ x ^ (r / 2 - 1))
Proof state after:
case hf
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ LocallyIntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ici ↑N) volume

case ho
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ (fun x => |x ^ (r - 1)| * |x.log|) =O[atTop] fun x => x ^ (r / 2 - 1)

case hg
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ IntegrableAtFilter (fun x => x ^ (r / 2 - 1)) atTop volume
Theorem: integrable_log_over_pow
Proof state before:
case hf
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ LocallyIntegrableOn (fun x => |x ^ (r - 1)| * |x.log|) (Ici ↑N) volume
Tactic:
apply ContinuousOn.abs ?_ |>.mul ?_ |>.locallyIntegrableOn (by simp)
Proof state after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun x => x ^ (r - 1)) (Ici ↑N)

r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun x => |x.log|) (Ici ↑N)
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ MeasurableSet (Ici ↑N)
Tactic:
simp
Proof state after:
no goals
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ContinuousOn (fun x => x ^ (r - 1)) (Ici ↑N)
Tactic:
apply ContinuousOn.rpow (by fun_prop) (by fun_prop)
Proof state after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ∀ x ∈ Ici ↑N, x ≠ 0 ∨ 0 < r - 1
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
⊢ ∀ x ∈ Ici ↑N, x ≠ 0 ∨ 0 < r - 1
Tactic:
intro x hx
Proof state after:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0 ∨ 0 < r - 1
Theorem: integrable_log_over_pow
Proof state before:
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0 ∨ 0 < r - 1
Tactic:
left
Proof state after:
case h
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0
Theorem: integrable_log_over_pow
Proof state before:
case h
r : ℝ
rneg : r < 0
N : ℕ
Npos : 0 < N
x : ℝ
hx : x ∈ Ici ↑N
⊢ x ≠ 0
Tactic:
contrapose! Npos with h
Proof state after:
case h
r : ℝ
rneg : r < 0
N : ℕ
x : ℝ
hx : x ∈ Ici ↑N
h : x = 0
⊢ N ≤ 0
Theorem: integrable_log_over_pow
Proof state before:
case h
r : ℝ
rneg : r < 0
N : ℕ
x : ℝ
hx : x ∈ Ici ↑N
h : x = 0
⊢ N ≤ 0
Tactic:
exact_mod_cast h ▸ mem_Ici.mp hx
Proof state after:
no goals