internlm/Lean-Github huggingface dataset:
Theorem: tendsto_coe_atTop
Proof state before:
case pos
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : a = 0
⊢ b ≤ ↑a
Tactic:
simp [a_zero] at ha
Proof state after:
no goals
Theorem: tendsto_coe_atTop
Proof state before:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
⊢ b ≤ ↑a
Tactic:
by_cases h : ⌊b⌋.toNat < a
Proof state after:
case pos
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : ⌊b⌋.toNat < a
⊢ b ≤ ↑a

case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : ¬⌊b⌋.toNat < a
⊢ b ≤ ↑a
Theorem: tendsto_coe_atTop
Proof state before:
case pos
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : ⌊b⌋.toNat < a
⊢ b ≤ ↑a
Tactic:
exact (Int.floor_lt.mp <| (Int.toNat_lt' a_zero).mp h).le
Proof state after:
no goals
Theorem: tendsto_coe_atTop
Proof state before:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : ¬⌊b⌋.toNat < a
⊢ b ≤ ↑a
Tactic:
simp only [not_lt] at h
Proof state after:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : a ≤ ⌊b⌋.toNat
⊢ b ≤ ↑a
Theorem: tendsto_coe_atTop
Proof state before:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : a ≤ ⌊b⌋.toNat
⊢ b ≤ ↑a
Tactic:
absurd le_trans ha h
Proof state after:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : a ≤ ⌊b⌋.toNat
⊢ ¬⌊b⌋.toNat + 1 ≤ ⌊b⌋.toNat
Theorem: tendsto_coe_atTop
Proof state before:
case neg
b : ℝ
a : ℕ
ha : ⌊b⌋.toNat + 1 ≤ a
a_zero : ¬a = 0
h : a ≤ ⌊b⌋.toNat
⊢ ¬⌊b⌋.toNat + 1 ≤ ⌊b⌋.toNat
Tactic:
simp
Proof state after:
no goals
Theorem: Summable_rpow
Proof state before:
s : ℂ
s_re_gt : 1 < s.re
⊢ Summable fun n => 1 / ↑n ^ s
Tactic:
apply Summable.of_norm
Proof state after:
case hf
s : ℂ
s_re_gt : 1 < s.re
⊢ Summable fun a => ‖1 / ↑a ^ s‖
Theorem: Summable_rpow
Proof state before:
case hf
s : ℂ
s_re_gt : 1 < s.re
⊢ Summable fun a => ‖1 / ↑a ^ s‖
Tactic:
have : s.re ≠ 0 := by linarith
Proof state after:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => ‖1 / ↑a ^ s‖
Theorem: Summable_rpow
Proof state before:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => ‖1 / ↑a ^ s‖
Tactic:
simp only [one_div, norm_inv]
Proof state after:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => ‖↑a ^ s‖⁻¹
Theorem: Summable_rpow
Proof state before:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => ‖↑a ^ s‖⁻¹
Tactic:
simp_rw [norm_natCast_cpow_of_re_ne_zero _ this]
Proof state after:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => (↑a ^ s.re)⁻¹
Theorem: Summable_rpow
Proof state before:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => (↑a ^ s.re)⁻¹
Tactic:
exact (Real.summable_nat_rpow_inv (p := s.re)).mpr s_re_gt
Proof state after:
no goals
Theorem: Summable_rpow
Proof state before:
s : ℂ
s_re_gt : 1 < s.re
⊢ s.re ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n : ℕ
⊢ ∑ x ∈ Finset.Ioc m n, f ↑x = ∑ x ∈ Finset.Ioc ↑m ↑n, f x
Tactic:
apply Finset.sum_nbij (i := (fun (x : ℕ) ↦ (x : ℤ))) ?_ ?_ ?_ fun _ _ ↦ rfl
Proof state after:
f : ℤ → ℂ
m n : ℕ
⊢ ∀ a ∈ Finset.Ioc m n, (fun x => ↑x) a ∈ Finset.Ioc ↑m ↑n

f : ℤ → ℂ
m n : ℕ
⊢ InjOn (fun x => ↑x) ↑(Finset.Ioc m n)

f : ℤ → ℂ
m n : ℕ
⊢ SurjOn (fun x => ↑x) ↑(Finset.Ioc m n) ↑(Finset.Ioc ↑m ↑n)
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n : ℕ
⊢ ∀ a ∈ Finset.Ioc m n, (fun x => ↑x) a ∈ Finset.Ioc ↑m ↑n
Tactic:
intro x hx
Proof state after:
f : ℤ → ℂ
m n x : ℕ
hx : x ∈ Finset.Ioc m n
⊢ (fun x => ↑x) x ∈ Finset.Ioc ↑m ↑n
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n x : ℕ
hx : x ∈ Finset.Ioc m n
⊢ (fun x => ↑x) x ∈ Finset.Ioc ↑m ↑n
Tactic:
simp only [Finset.mem_Ioc, Nat.cast_lt, Nat.cast_le] at hx ⊢
Proof state after:
f : ℤ → ℂ
m n x : ℕ
hx : m < x ∧ x ≤ n
⊢ m < x ∧ x ≤ n
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n x : ℕ
hx : m < x ∧ x ≤ n
⊢ m < x ∧ x ≤ n
Tactic:
exact hx
Proof state after:
no goals
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n : ℕ
⊢ InjOn (fun x => ↑x) ↑(Finset.Ioc m n)
Tactic:
intro x₁ _ x₂ _ h
Proof state after:
f : ℤ → ℂ
m n x₁ : ℕ
a✝¹ : x₁ ∈ ↑(Finset.Ioc m n)
x₂ : ℕ
a✝ : x₂ ∈ ↑(Finset.Ioc m n)
h : (fun x => ↑x) x₁ = (fun x => ↑x) x₂
⊢ x₁ = x₂
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n x₁ : ℕ
a✝¹ : x₁ ∈ ↑(Finset.Ioc m n)
x₂ : ℕ
a✝ : x₂ ∈ ↑(Finset.Ioc m n)
h : (fun x => ↑x) x₁ = (fun x => ↑x) x₂
⊢ x₁ = x₂
Tactic:
simp only [Nat.cast_inj] at h
Proof state after:
f : ℤ → ℂ
m n x₁ : ℕ
a✝¹ : x₁ ∈ ↑(Finset.Ioc m n)
x₂ : ℕ
a✝ : x₂ ∈ ↑(Finset.Ioc m n)
h : x₁ = x₂
⊢ x₁ = x₂
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n x₁ : ℕ
a✝¹ : x₁ ∈ ↑(Finset.Ioc m n)
x₂ : ℕ
a✝ : x₂ ∈ ↑(Finset.Ioc m n)
h : x₁ = x₂
⊢ x₁ = x₂
Tactic:
exact h
Proof state after:
no goals
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n : ℕ
⊢ SurjOn (fun x => ↑x) ↑(Finset.Ioc m n) ↑(Finset.Ioc ↑m ↑n)
Tactic:
intro x hx
Proof state after:
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : x ∈ ↑(Finset.Ioc ↑m ↑n)
⊢ x ∈ (fun x => ↑x) '' ↑(Finset.Ioc m n)
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : x ∈ ↑(Finset.Ioc ↑m ↑n)
⊢ x ∈ (fun x => ↑x) '' ↑(Finset.Ioc m n)
Tactic:
simp only [Finset.coe_Ioc, mem_image, mem_Ioc] at hx ⊢
Proof state after:
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : ↑m < x ∧ x ≤ ↑n
⊢ ∃ x_1, (m < x_1 ∧ x_1 ≤ n) ∧ ↑x_1 = x
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : ↑m < x ∧ x ≤ ↑n
⊢ ∃ x_1, (m < x_1 ∧ x_1 ≤ n) ∧ ↑x_1 = x
Tactic:
lift x to ℕ using (by linarith)
Proof state after:
case intro
f : ℤ → ℂ
m n x : ℕ
hx : ↑m < ↑x ∧ ↑x ≤ ↑n
⊢ ∃ x_1, (m < x_1 ∧ x_1 ≤ n) ∧ ↑x_1 = ↑x
Theorem: Finset_coe_Nat_Int
Proof state before:
case intro
f : ℤ → ℂ
m n x : ℕ
hx : ↑m < ↑x ∧ ↑x ≤ ↑n
⊢ ∃ x_1, (m < x_1 ∧ x_1 ≤ n) ∧ ↑x_1 = ↑x
Tactic:
exact ⟨x, by exact_mod_cast hx, rfl⟩
Proof state after:
no goals
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : ↑m < x ∧ x ≤ ↑n
⊢ 0 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: Finset_coe_Nat_Int
Proof state before:
f : ℤ → ℂ
m n x : ℕ
hx : ↑m < ↑x ∧ ↑x ≤ ↑n
⊢ m < x ∧ x ≤ n
Tactic:
exact_mod_cast hx
Proof state after:
no goals
Theorem: Complex.cpow_tendsto
Proof state before:
s : ℂ
s_re_gt : 1 < s.re
⊢ Tendsto (fun x => ↑x ^ (1 - s)) atTop (𝓝 0)
Tactic:
have one_sub_s_re_ne : (1 - s).re ≠ 0 := by simp only [sub_re, one_re]; linarith
Proof state after:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (1 - s)) atTop (𝓝 0)
Theorem: Complex.cpow_tendsto
Proof state before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (1 - s)) atTop (𝓝 0)
Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]
Proof state after:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ‖↑x ^ (1 - s)‖) atTop (𝓝 0)
Theorem: Complex.cpow_tendsto
Proof state before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ‖↑x ^ (1 - s)‖) atTop (𝓝 0)
Tactic:
simp_rw [Complex.norm_natCast_cpow_of_re_ne_zero _ (one_sub_s_re_ne)]
Proof state after:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (1 - s).re) atTop (𝓝 0)
Theorem: Complex.cpow_tendsto
Proof state before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (1 - s).re) atTop (𝓝 0)
Tactic:
rw [(by simp only [sub_re, one_re, neg_sub] : (1 - s).re = - (s - 1).re)]
Proof state after:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (-(s - 1).re)) atTop (𝓝 0)
Theorem: Complex.cpow_tendsto
Proof state before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ Tendsto (fun x => ↑x ^ (-(s - 1).re)) atTop (𝓝 0)
Tactic:
apply (tendsto_rpow_neg_atTop _).comp tendsto_natCast_atTop_atTop
Proof state after:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ 0 < (s - 1).re
Theorem: Complex.cpow_tendsto
Proof state before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ 0 < (s - 1).re
Tactic:
simp [s_re_gt]
Proof state after:
no goals
Theorem: Complex.cpow_tendsto
Proof state before:
s : ℂ
s_re_gt : 1 < s.re
⊢ (1 - s).re ≠ 0
Tactic:
simp only [sub_re, one_re]
Proof state after:
s : ℂ
s_re_gt : 1 < s.re
⊢ 1 - s.re ≠ 0
Theorem: Complex.cpow_tendsto
Proof state before:
s : ℂ
s_re_gt : 1 < s.re
⊢ 1 - s.re ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Complex.cpow_tendsto
Proof state before:
s : ℂ
s_re_gt : 1 < s.re
one_sub_s_re_ne : (1 - s).re ≠ 0
⊢ (1 - s).re = -(s - 1).re
Tactic:
simp only [sub_re, one_re, neg_sub]
Proof state after:
no goals
Theorem: Complex.cpow_inv_tendsto
Proof state before:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => (↑x ^ s)⁻¹) atTop (𝓝 0)
Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]
Proof state after:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ‖(↑x ^ s)⁻¹‖) atTop (𝓝 0)
Theorem: Complex.cpow_inv_tendsto
Proof state before:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ‖(↑x ^ s)⁻¹‖) atTop (𝓝 0)
Tactic:
simp_rw [norm_inv, Complex.norm_natCast_cpow_of_re_ne_zero _ <| ne_of_gt hs]
Proof state after:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => (↑x ^ s.re)⁻¹) atTop (𝓝 0)
Theorem: Complex.cpow_inv_tendsto
Proof state before:
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => (↑x ^ s.re)⁻¹) atTop (𝓝 0)
Tactic:
apply Filter.Tendsto.inv_tendsto_atTop
Proof state after:
case h
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ↑x ^ s.re) atTop atTop
Theorem: Complex.cpow_inv_tendsto
Proof state before:
case h
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x => ↑x ^ s.re) atTop atTop
Tactic:
exact (tendsto_rpow_atTop hs).comp tendsto_natCast_atTop_atTop
Proof state after:
no goals
Theorem: ZetaSum_aux2a
Proof state before:
⊢ ∃ C, ∀ (x : ℝ), |↑⌊x⌋ + 1 / 2 - x| ≤ C
Tactic:
use 1 / 2
Proof state after:
case h

⊢ ∀ (x : ℝ), |↑⌊x⌋ + 1 / 2 - x| ≤ 1 / 2
Theorem: ZetaSum_aux2a
Proof state before:
case h

⊢ ∀ (x : ℝ), |↑⌊x⌋ + 1 / 2 - x| ≤ 1 / 2
Tactic:
exact ZetaSum_aux1_3
Proof state after:
no goals
Theorem: ZetaSum_aux3
Proof state before:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Tactic:
let f := fun (n : ℕ) ↦ 1 / (n : ℂ) ^ s
Proof state after:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Theorem: ZetaSum_aux3
Proof state before:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Tactic:
have hf := Summable_rpow s_re_gt
Proof state after:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Theorem: ZetaSum_aux3
Proof state before:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ n ∈ Finset.Ioc N k, 1 / ↑n ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Tactic:
simp_rw [Finset.Ioc_eq_Ico]
Proof state after:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Theorem: ZetaSum_aux3
Proof state before:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Tendsto (fun k => ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s) atTop (𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s))
Tactic:
convert finsetSum_tendsto_tsum (f := fun n ↦ f (n + 1)) (N := N) ?_ using 1
Proof state after:
case h.e'_3
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ (fun k => ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s) = fun k => ∑ n ∈ Finset.Ico N k, f (n + 1)

case h.e'_5
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ 𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s) = 𝓝 (∑' (n : ℕ), f (n + N + 1))

N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Summable fun n => f (n + 1)
Theorem: ZetaSum_aux3
Proof state before:
case h.e'_3
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ (fun k => ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s) = fun k => ∑ n ∈ Finset.Ico N k, f (n + 1)
Tactic:
ext k
Proof state after:
case h.e'_3.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s = ∑ n ∈ Finset.Ico N k, f (n + 1)
Theorem: ZetaSum_aux3
Proof state before:
case h.e'_3.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s = ∑ n ∈ Finset.Ico N k, f (n + 1)
Tactic:
simp only [f]
Proof state after:
case h.e'_3.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s = ∑ x ∈ Finset.Ico N k, 1 / ↑(x + 1) ^ s
Theorem: ZetaSum_aux3
Proof state before:
case h.e'_3.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ ∑ x ∈ Finset.Ico (N + 1) (k + 1), 1 / ↑x ^ s = ∑ x ∈ Finset.Ico N k, 1 / ↑(x + 1) ^ s
Tactic:
convert Finset.sum_map (e := addRightEmbedding 1) ?_  ?_ using 2
Proof state after:
case h.e'_2.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ Finset.Ico (N + 1) (k + 1) = Finset.map (addRightEmbedding 1) (Finset.Ico N k)
Theorem: ZetaSum_aux3
Proof state before:
case h.e'_2.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k : ℕ
⊢ Finset.Ico (N + 1) (k + 1) = Finset.map (addRightEmbedding 1) (Finset.Ico N k)
Tactic:
ext n
Proof state after:
case h.e'_2.h.a
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k n : ℕ
⊢ n ∈ Finset.Ico (N + 1) (k + 1) ↔ n ∈ Finset.map (addRightEmbedding 1) (Finset.Ico N k)
Theorem: ZetaSum_aux3
Proof state before:
case h.e'_2.h.a
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
k n : ℕ
⊢ n ∈ Finset.Ico (N + 1) (k + 1) ↔ n ∈ Finset.map (addRightEmbedding 1) (Finset.Ico N k)
Tactic:
simp only [Finset.mem_Ico, Finset.map_add_right_Ico]
Proof state after:
no goals
Theorem: ZetaSum_aux3
Proof state before:
case h.e'_5
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ 𝓝 (∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ s) = 𝓝 (∑' (n : ℕ), f (n + N + 1))
Tactic:
congr
Proof state after:
case h.e'_5.e_x.e_f
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ (fun n => 1 / (↑n + ↑N + 1) ^ s) = fun n => f (n + N + 1)
Theorem: ZetaSum_aux3
Proof state before:
case h.e'_5.e_x.e_f
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ (fun n => 1 / (↑n + ↑N + 1) ^ s) = fun n => f (n + N + 1)
Tactic:
ext n
Proof state after:
case h.e'_5.e_x.e_f.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
n : ℕ
⊢ 1 / (↑n + ↑N + 1) ^ s = f (n + N + 1)
Theorem: ZetaSum_aux3
Proof state before:
case h.e'_5.e_x.e_f.h
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
n : ℕ
⊢ 1 / (↑n + ↑N + 1) ^ s = f (n + N + 1)
Tactic:
simp only [one_div, Nat.cast_add, Nat.cast_one, f]
Proof state after:
no goals
Theorem: ZetaSum_aux3
Proof state before:
N : ℕ
s : ℂ
s_re_gt : 1 < s.re
f : ℕ → ℂ := fun n => 1 / ↑n ^ s
hf : Summable fun n => 1 / ↑n ^ s
⊢ Summable fun n => f (n + 1)
Tactic:
rwa [summable_nat_add_iff (k := 1)]
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun
Proof state before:
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
Tactic:
apply MeasureTheory.Integrable.bdd_mul ?_ ?_
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∃ C, ∀ (x : ℝ), ‖↑⌊x⌋ + 1 / 2 - ↑x‖ ≤ C

N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.Integrable (fun x => ↑x ^ (-(s + 1))) (MeasureTheory.volume.restrict (Ioi ↑N))

N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.AEStronglyMeasurable (fun x => ↑⌊x⌋ + 1 / 2 - ↑x) (MeasureTheory.volume.restrict (Ioi ↑N))
Theorem: integrableOn_of_Zeta0_fun
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ ∃ C, ∀ (x : ℝ), ‖↑⌊x⌋ + 1 / 2 - ↑x‖ ≤ C
Tactic:
convert ZetaSum_aux2a
Proof state after:
case h.e'_2.h.h.h.e'_3
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x✝ a✝ : ℝ
⊢ ‖↑⌊a✝⌋ + 1 / 2 - ↑a✝‖ = |↑⌊a✝⌋ + 1 / 2 - a✝|
Theorem: integrableOn_of_Zeta0_fun
Proof state before:
case h.e'_2.h.h.h.e'_3
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
x✝ a✝ : ℝ
⊢ ‖↑⌊a✝⌋ + 1 / 2 - ↑a✝‖ = |↑⌊a✝⌋ + 1 / 2 - a✝|
Tactic:
simp [← Complex.abs_ofReal]
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.Integrable (fun x => ↑x ^ (-(s + 1))) (MeasureTheory.volume.restrict (Ioi ↑N))
Tactic:
apply integrableOn_Ioi_cpow_iff (by positivity) |>.mpr (by simp [s_re_gt])
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ 0 < ↑N
Tactic:
positivity
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ (-(s + 1)).re < -1
Tactic:
simp [s_re_gt]
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ MeasureTheory.AEStronglyMeasurable (fun x => ↑⌊x⌋ + 1 / 2 - ↑x) (MeasureTheory.volume.restrict (Ioi ↑N))
Tactic:
refine Measurable.add ?_ measurable_const |>.sub (by fun_prop) |>.aestronglyMeasurable
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable fun x => ↑⌊x⌋
Theorem: integrableOn_of_Zeta0_fun
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable fun x => ↑⌊x⌋
Tactic:
exact Measurable.comp (by exact fun _ _ ↦ trivial) Int.measurable_floor
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable fun x => ↑x
Tactic:
fun_prop
Proof state after:
no goals
Theorem: integrableOn_of_Zeta0_fun
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
s_re_gt : 0 < s.re
⊢ Measurable IntCast.intCast
Tactic:
exact fun _ _ ↦ trivial
Proof state after:
no goals
Theorem: ZetaSum_aux2
Proof 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]
Proof 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))
Theorem: ZetaSum_aux2
Proof 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
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
⊢ ∑' (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))
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 / (↑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)))
Proof 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))))
Theorem: ZetaSum_aux2
Proof 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]
Proof state after:
no goals
Theorem: ZetaSum_aux2
Proof 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)
Proof 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))
Theorem: ZetaSum_aux2
Proof 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
Proof 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
Theorem: ZetaSum_aux2
Proof 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
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
⊢ ∀ 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