Theorem: ZetaSum_aux2 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
⊢ ∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s =
    -↑N ^ (1 - s) / (1 - s) - ↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))
Tactic:
have s_ne_zero : s ≠ 0 := fun hs ↦ by linarith [zero_re ▸ hs ▸ s_re_gt]
State after:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
⊢ ∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s =
    -↑N ^ (1 - s) / (1 - s) - ↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
⊢ ∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s =
    -↑N ^ (1 - s) / (1 - s) - ↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))
Tactic:
have s_ne_one : s ≠ 1 := fun hs ↦ (lt_self_iff_false _).mp <| one_re ▸ hs ▸ s_re_gt
State after:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ ∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s =
    -↑N ^ (1 - s) / (1 - s) - ↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))

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 / (↑n + ↑N + 1) ^ s =
    -↑N ^ (1 - s) / (1 - s) - ↑N ^ (-s) / 2 + s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(s + 1))
Tactic:
apply tendsto_nhds_unique (X := ℂ) (Y := ℕ) (l := atTop)
  (f := 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 := (- N ^ (1 - s)) / (1 - s) - N ^ (-s) / 2
    + s * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) * (x : ℂ) ^ (-(s + 1)))
State after:
case ha
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 / (↑n + ↑N + 1) ^ s))

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))))

State before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
hs : s = 0
⊢ False
Tactic:
linarith [zero_re ▸ hs ▸ s_re_gt]
State after:
no goals

State before:
case ha
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 / (↑n + ↑N + 1) ^ s))
Tactic:
apply Filter.Tendsto.congr' (f₁ := fun (k : ℕ) ↦ ∑ n in Finset.Ioc N k, 1 / (n : ℂ) ^ s) (l₁ := atTop)
State after:
case ha.hl
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) =ᶠ[atTop] 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))

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))

State before:
case ha.hl
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) =ᶠ[atTop] 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))
Tactic:
apply Filter.eventually_atTop.mpr
State after:
case ha.hl
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ ∃ a,
    ∀ b ≥ a,
      (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

State before:
case ha.hl
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 1 < s.re
s_ne_zero : s ≠ 0
s_ne_one : s ≠ 1
⊢ ∃ a,
    ∀ b ≥ a,
      (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:
use N + 1
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
⊢ ∀ 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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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 _ ?_)
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))))

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)]
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))

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
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)

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))]
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))

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)
State after:
no goals

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
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals

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]
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))

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
State after:
no goals

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
State after:
no goals