internlm/Lean-Github huggingface dataset:
Theorem: norm_dirichlet_product_ge_one
Proof state before:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
χ₀ : DirichletCharacter ℂ N := 1
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ 1 + ↑x = ↑(1 + ↑x).re
Tactic:
simp only [add_re, one_re, ofReal_re, ofReal_add, ofReal_one]
Proof state after:
no goals
Theorem: norm_zeta_product_ge_one
Proof state before:
x : ℝ
hx : 0 < x
y : ℝ
⊢ ‖ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑y) ^ 4 * ζ (1 + ↑x + 2 * I * ↑y)‖ ≥ 1
Tactic:
have ⟨h₀, h₁, h₂⟩ := one_lt_re_of_pos y hx
Proof state after:
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑y) ^ 4 * ζ (1 + ↑x + 2 * I * ↑y)‖ ≥ 1
Theorem: norm_zeta_product_ge_one
Proof state before:
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
⊢ ‖ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑y) ^ 4 * ζ (1 + ↑x + 2 * I * ↑y)‖ ≥ 1
Tactic:
simpa only [one_pow, norm_mul, norm_pow, DirichletCharacter.LSeries_modOne_eq,
  LSeries_one_eq_riemannZeta, h₀, h₁, h₂] using norm_dirichlet_product_ge_one χ₁ hx y
Proof state after:
no goals
Theorem: riemannZeta_isBigO_near_one_horizontal
Proof state before:
this : (fun w => ζ (1 + w)) =O[𝓝[≠] 0] fun x => 1 / x
⊢ (fun x => ζ (1 + ↑x)) =O[𝓝[>] 0] fun x => 1 / ↑x
Tactic:
exact (isBigO_comp_ofReal_nhds_ne this).mono <| nhds_right'_le_nhds_ne 0
Proof state after:
no goals
Theorem: riemannZeta_isBigO_near_one_horizontal
Proof state before:
H : Tendsto (fun w => w * ζ (1 + w)) (𝓝[≠] 0) (𝓝 1)
⊢ (fun w => ζ (1 + w)) =O[𝓝[≠] 0] fun x => 1 / x
Tactic:
exact ((isBigO_mul_iff_isBigO_div eventually_mem_nhdsWithin).mp <|
  Tendsto.isBigO_one ℂ H).trans <| isBigO_refl ..
Proof state after:
no goals
Theorem: riemannZeta_isBigO_near_one_horizontal
Proof state before:
⊢ Tendsto (fun w => w * ζ (1 + w)) (𝓝[≠] 0) (𝓝 1)
Tactic:
convert Tendsto.comp (f := fun w ↦ 1 + w) riemannZeta_residue_one ?_ using 1
Proof state after:
case h.e'_3

⊢ (fun w => w * ζ (1 + w)) = (fun s => (s - 1) * ζ s) ∘ fun w => 1 + w

case convert_2

⊢ Tendsto (fun w => 1 + w) (𝓝[≠] 0) (𝓝[≠] 1)
Theorem: riemannZeta_isBigO_near_one_horizontal
Proof state before:
case h.e'_3

⊢ (fun w => w * ζ (1 + w)) = (fun s => (s - 1) * ζ s) ∘ fun w => 1 + w
Tactic:
ext w
Proof state after:
case h.e'_3.h
w : ℂ
⊢ w * ζ (1 + w) = ((fun s => (s - 1) * ζ s) ∘ fun w => 1 + w) w
Theorem: riemannZeta_isBigO_near_one_horizontal
Proof state before:
case h.e'_3.h
w : ℂ
⊢ w * ζ (1 + w) = ((fun s => (s - 1) * ζ s) ∘ fun w => 1 + w) w
Tactic:
simp only [Function.comp_apply, add_sub_cancel_left]
Proof state after:
no goals
Theorem: riemannZeta_isBigO_near_one_horizontal
Proof state before:
case convert_2

⊢ Tendsto (fun w => 1 + w) (𝓝[≠] 0) (𝓝[≠] 1)
Tactic:
refine tendsto_iff_comap.mpr <| map_le_iff_le_comap.mp <| Eq.le ?_
Proof state after:
case convert_2

⊢ map (fun w => 1 + w) (𝓝[≠] 0) = 𝓝[≠] 1
Theorem: riemannZeta_isBigO_near_one_horizontal
Proof state before:
case convert_2

⊢ map (fun w => 1 + w) (𝓝[≠] 0) = 𝓝[≠] 1
Tactic:
convert map_punctured_nhds_eq (Homeomorph.addLeft (1 : ℂ)) 0 using 2 <;> simp
Proof state after:
no goals
Theorem: riemannZeta_isBigO_of_ne_one_horizontal
Proof state before:
y : ℝ
hy : y ≠ 0
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x => 1
Tactic:
refine Asymptotics.IsBigO.mono ?_ nhdsWithin_le_nhds
Proof state after:
y : ℝ
hy : y ≠ 0
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝 0] fun x => 1
Theorem: riemannZeta_isBigO_of_ne_one_horizontal
Proof state before:
y : ℝ
hy : y ≠ 0
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝 0] fun x => 1
Tactic:
have hy' : 1 + I * y ≠ 1 := by simp [hy]
Proof state after:
y : ℝ
hy : y ≠ 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝 0] fun x => 1
Theorem: riemannZeta_isBigO_of_ne_one_horizontal
Proof state before:
y : ℝ
hy : y ≠ 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝 0] fun x => 1
Tactic:
convert isBigO_comp_ofReal
  (differentiableAt_riemannZeta hy').continuousAt.isBigO using 3 with x
Proof state after:
case h.e'_7.h.h.e'_1
y : ℝ
hy : y ≠ 0
hy' : 1 + I * ↑y ≠ 1
x : ℝ
⊢ 1 + ↑x + I * ↑y = ↑x + (1 + I * ↑y)
Theorem: riemannZeta_isBigO_of_ne_one_horizontal
Proof state before:
case h.e'_7.h.h.e'_1
y : ℝ
hy : y ≠ 0
hy' : 1 + I * ↑y ≠ 1
x : ℝ
⊢ 1 + ↑x + I * ↑y = ↑x + (1 + I * ↑y)
Tactic:
ring
Proof state after:
no goals
Theorem: riemannZeta_isBigO_of_ne_one_horizontal
Proof state before:
y : ℝ
hy : y ≠ 0
⊢ 1 + I * ↑y ≠ 1
Tactic:
simp [hy]
Proof state after:
no goals
Theorem: riemannZeta_isBigO_near_root_horizontal
Proof state before:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x => ↑x
Tactic:
have hy' : 1 + I * y ≠ 1 := by simp [hy]
Proof state after:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x => ↑x
Theorem: riemannZeta_isBigO_near_root_horizontal
Proof state before:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x => ↑x
Tactic:
conv => enter [2, x]; rw [add_comm 1, add_assoc]
Proof state after:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x => ↑x
Theorem: riemannZeta_isBigO_near_root_horizontal
Proof state before:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x => ↑x
Tactic:
exact (isBigO_comp_ofReal <| (differentiableAt_riemannZeta hy').isBigO_of_eq_zero h).mono
  nhdsWithin_le_nhds
Proof state after:
no goals
Theorem: riemannZeta_isBigO_near_root_horizontal
Proof state before:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
⊢ 1 + I * ↑y ≠ 1
Tactic:
simp [hy]
Proof state after:
no goals
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
⊢ ζ z ≠ 0
Tactic:
refine hz'.eq_or_lt.elim (fun h Hz ↦ ?_) riemannZeta_ne_zero_of_one_lt_re
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
⊢ False
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
⊢ False
Tactic:
have hz₀ : z.im ≠ 0 := by
  rw [← re_add_im z, ← h, ofReal_one] at hz
  simpa only [ne_eq, add_right_eq_self, mul_eq_zero, ofReal_eq_zero, I_ne_zero, or_false]
    using hz
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ False
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ False
Tactic:
have hzeq : z = 1 + I * z.im := by
  rw [mul_comm I, ← re_add_im z, ← h]
  push_cast
  simp only [add_im, one_im, mul_im, ofReal_re, I_im, mul_one, ofReal_im, I_re, mul_zero,
    add_zero, zero_add]
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
⊢ False
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
⊢ False
Tactic:
have H₀ : (fun _ : ℝ ↦ (1 : ℝ)) =O[𝓝[>] 0]
    (fun x ↦ ζ (1 + x) ^ 3 * ζ (1 + x + I * z.im) ^ 4 * ζ (1 + x + 2 * I * z.im)) :=
  IsBigO.of_bound' <| eventually_nhdsWithin_of_forall
    fun _ hx ↦ (norm_one (α := ℝ)).symm ▸ (norm_zeta_product_ge_one hx z.im).le
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
⊢ False
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
⊢ False
Tactic:
have H := (riemannZeta_isBigO_near_one_horizontal.pow 3).mul
  ((riemannZeta_isBigO_near_root_horizontal hz₀ (hzeq ▸ Hz)).pow 4)|>.mul <|
  riemannZeta_isBigO_of_ne_one_horizontal <| mul_ne_zero two_ne_zero hz₀
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
⊢ False
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
⊢ False
Tactic:
conv at H => enter [3, x]; rw [help]
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
⊢ False
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
⊢ False
Tactic:
conv at H =>
  enter [2, x]; rw [show 1 + x + I * ↑(2 * z.im) = 1 + x + 2 * I * z.im by simp; ring]
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
⊢ False
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
⊢ False
Tactic:
replace H := (H₀.trans H).norm_right
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => ‖↑x‖
⊢ False
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => ‖↑x‖
⊢ False
Tactic:
simp only [norm_eq_abs, abs_ofReal] at H
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ False
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ False
Tactic:
refine isLittleO_irrefl ?_ <| H.of_abs_right.trans_isLittleO <|
  isLittleO_id_nhdsWithin (Set.Ioi 0)
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ ∃ᶠ (x : ℝ) in 𝓝[>] 0, 1 ≠ 0
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ ∃ᶠ (x : ℝ) in 𝓝[>] 0, 1 ≠ 0
Tactic:
simp only [ne_eq, one_ne_zero, not_false_eq_true, frequently_true_iff_neBot]
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ (𝓝[>] 0).NeBot
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H : (fun x => 1) =O[𝓝[>] 0] fun x => |x|
⊢ (𝓝[>] 0).NeBot
Tactic:
exact mem_closure_iff_nhdsWithin_neBot.mp <| closure_Ioi (0 : ℝ) ▸ Set.left_mem_Ici
Proof state after:
no goals
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
⊢ z.im ≠ 0
Tactic:
rw [← re_add_im z, ← h, ofReal_one] at hz
Proof state after:
z : ℂ
hz : 1 + ↑z.im * I ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
⊢ z.im ≠ 0
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : 1 + ↑z.im * I ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
⊢ z.im ≠ 0
Tactic:
simpa only [ne_eq, add_right_eq_self, mul_eq_zero, ofReal_eq_zero, I_ne_zero, or_false]
  using hz
Proof state after:
no goals
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ z = 1 + I * ↑z.im
Tactic:
rw [mul_comm I, ← re_add_im z, ← h]
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ ↑1 + ↑z.im * I = 1 + ↑(↑1 + ↑z.im * I).im * I
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ ↑1 + ↑z.im * I = 1 + ↑(↑1 + ↑z.im * I).im * I
Tactic:
push_cast
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ 1 + ↑z.im * I = 1 + ↑(1 + ↑z.im * I).im * I
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
⊢ 1 + ↑z.im * I = 1 + ↑(1 + ↑z.im * I).im * I
Tactic:
simp only [add_im, one_im, mul_im, ofReal_re, I_im, mul_one, ofReal_im, I_re, mul_zero,
  add_zero, zero_add]
Proof state after:
no goals
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
x : ℝ
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
Tactic:
rcases eq_or_ne x 0 with rfl | h
Proof state after:
case inl
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
⊢ (1 / ↑0) ^ 3 * ↑0 ^ 4 * 1 = ↑0

case inr
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h✝ : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
x : ℝ
h : x ≠ 0
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
case inl
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
⊢ (1 / ↑0) ^ 3 * ↑0 ^ 4 * 1 = ↑0
Tactic:
rw [ofReal_zero, zero_pow (by norm_num), mul_zero, mul_one]
Proof state after:
no goals
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
⊢ 4 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
case inr
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h✝ : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
x : ℝ
h : x ≠ 0
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
Tactic:
field_simp [h]
Proof state after:
case inr
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h✝ : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
x : ℝ
h : x ≠ 0
⊢ ↑x ^ 4 = ↑x * ↑x ^ 3
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
case inr
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h✝ : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H :
  (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x =>
    (1 / ↑x) ^ 3 * ↑x ^ 4 * 1
x : ℝ
h : x ≠ 0
⊢ ↑x ^ 4 = ↑x * ↑x ^ 3
Tactic:
ring
Proof state after:
no goals
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
x : ℝ
⊢ 1 + ↑x + I * ↑(2 * z.im) = 1 + ↑x + 2 * I * ↑z.im
Tactic:
simp
Proof state after:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
x : ℝ
⊢ I * (2 * ↑z.im) = 2 * I * ↑z.im
Theorem: riemannZeta_ne_zero_of_one_le_re
Proof state before:
z : ℂ
hz : z ≠ 1
hz' : 1 ≤ z.re
h : 1 = z.re
Hz : ζ z = 0
hz₀ : z.im ≠ 0
hzeq : z = 1 + I * ↑z.im
H₀ : (fun x => 1) =O[𝓝[>] 0] fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + 2 * I * ↑z.im)
H : (fun x => ζ (1 + ↑x) ^ 3 * ζ (1 + ↑x + I * ↑z.im) ^ 4 * ζ (1 + ↑x + I * ↑(2 * z.im))) =O[𝓝[>] 0] fun x => ↑x
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
x : ℝ
⊢ I * (2 * ↑z.im) = 2 * I * ↑z.im
Tactic:
ring
Proof state after:
no goals
Theorem: ζ₁_apply_of_ne_one
Proof state before:
z : ℂ
hz : z ≠ 1
⊢ ζ₁ z = ζ z * (z - 1)
Tactic:
simp [ζ₁, hz]
Proof state after:
no goals
Theorem: ζ₁_differentiable
Proof state before:
⊢ Differentiable ℂ ζ₁
Tactic:
rw [← differentiableOn_univ,
  ← differentiableOn_compl_singleton_and_continuousAt_iff (c := 1) Filter.univ_mem, ζ₁]
Proof state after:
⊢ DifferentiableOn ℂ (Function.update (fun z => ζ z * (z - 1)) 1 1) (Set.univ \ {1}) ∧
    ContinuousAt (Function.update (fun z => ζ z * (z - 1)) 1 1) 1
Theorem: ζ₁_differentiable
Proof state before:
⊢ DifferentiableOn ℂ (Function.update (fun z => ζ z * (z - 1)) 1 1) (Set.univ \ {1}) ∧
    ContinuousAt (Function.update (fun z => ζ z * (z - 1)) 1 1) 1
Tactic:
refine ⟨DifferentiableOn.congr (f := fun z ↦ ζ z * (z - 1))
  (fun _ hz ↦ DifferentiableAt.differentiableWithinAt ?_) fun _ hz ↦ ?_,
  continuousWithinAt_compl_self.mp ?_⟩
Proof state after:
case refine_1
x✝ : ℂ
hz : x✝ ∈ Set.univ \ {1}
⊢ DifferentiableAt ℂ (fun z => ζ z * (z - 1)) x✝

case refine_2
x✝ : ℂ
hz : x✝ ∈ Set.univ \ {1}
⊢ Function.update (fun z => ζ z * (z - 1)) 1 1 x✝ = (fun z => ζ z * (z - 1)) x✝

case refine_3

⊢ ContinuousWithinAt (Function.update (fun z => ζ z * (z - 1)) 1 1) {1}ᶜ 1
Theorem: ζ₁_differentiable
Proof state before:
case refine_1
x✝ : ℂ
hz : x✝ ∈ Set.univ \ {1}
⊢ DifferentiableAt ℂ (fun z => ζ z * (z - 1)) x✝
Tactic:
simp only [Set.mem_diff, Set.mem_univ, Set.mem_singleton_iff, true_and] at hz
Proof state after:
case refine_1
x✝ : ℂ
hz : ¬x✝ = 1
⊢ DifferentiableAt ℂ (fun z => ζ z * (z - 1)) x✝
Theorem: ζ₁_differentiable
Proof state before:
case refine_1
x✝ : ℂ
hz : ¬x✝ = 1
⊢ DifferentiableAt ℂ (fun z => ζ z * (z - 1)) x✝
Tactic:
exact (differentiableAt_riemannZeta hz).mul <| (differentiableAt_id').sub <|
  differentiableAt_const 1
Proof state after:
no goals
Theorem: ζ₁_differentiable
Proof state before:
case refine_2
x✝ : ℂ
hz : x✝ ∈ Set.univ \ {1}
⊢ Function.update (fun z => ζ z * (z - 1)) 1 1 x✝ = (fun z => ζ z * (z - 1)) x✝
Tactic:
simp only [Set.mem_diff, Set.mem_univ, Set.mem_singleton_iff, true_and] at hz
Proof state after:
case refine_2
x✝ : ℂ
hz : ¬x✝ = 1
⊢ Function.update (fun z => ζ z * (z - 1)) 1 1 x✝ = (fun z => ζ z * (z - 1)) x✝
Theorem: ζ₁_differentiable
Proof state before:
case refine_2
x✝ : ℂ
hz : ¬x✝ = 1
⊢ Function.update (fun z => ζ z * (z - 1)) 1 1 x✝ = (fun z => ζ z * (z - 1)) x✝
Tactic:
simp only [ne_eq, hz, not_false_eq_true, Function.update_noteq]
Proof state after:
no goals
Theorem: ζ₁_differentiable
Proof state before:
case refine_3

⊢ ContinuousWithinAt (Function.update (fun z => ζ z * (z - 1)) 1 1) {1}ᶜ 1
Tactic:
conv in (_ * _) => rw [mul_comm]
Proof state after:
case refine_3

⊢ ContinuousWithinAt (Function.update (fun z => (z - 1) * ζ z) 1 1) {1}ᶜ 1
Theorem: ζ₁_differentiable
Proof state before:
case refine_3

⊢ ContinuousWithinAt (Function.update (fun z => (z - 1) * ζ z) 1 1) {1}ᶜ 1
Tactic:
simp only [continuousWithinAt_compl_self, continuousAt_update_same]
Proof state after:
case refine_3

⊢ Filter.Tendsto (fun z => (z - 1) * ζ z) (nhdsWithin 1 {1}ᶜ) (nhds 1)
Theorem: ζ₁_differentiable
Proof state before:
case refine_3

⊢ Filter.Tendsto (fun z => (z - 1) * ζ z) (nhdsWithin 1 {1}ᶜ) (nhds 1)
Tactic:
exact riemannZeta_residue_one
Proof state after:
no goals