internlm/Lean-Github huggingface dataset:
Theorem: Zeta0EqZeta
Proof state before:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
z : ℂ
hz : 1 < z.re
⊢ ∑' (n : ℕ), 1 / ↑n ^ z =
    ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ z +
      (-↑N ^ (1 - z) / (1 - z) + -(↑N ^ (-z) / 2) + z * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) * ↑x ^ (-(z + 1)))
Tactic:
rw [← sub_eq_add_neg, ← ZetaSum_aux2 N_pos hz, ← sum_add_tsum_nat_add (N + 1) (Summable_rpow hz)]
Proof state after:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
z : ℂ
hz : 1 < z.re
⊢ ∑ i ∈ Finset.range (N + 1), 1 / ↑i ^ z + ∑' (i : ℕ), 1 / ↑(i + (N + 1)) ^ z =
    ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ z + ∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ z
Theorem: Zeta0EqZeta
Proof state before:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
u_mem : {z | 1 < z.re} ∈ 𝓝 2
z : ℂ
hz : 1 < z.re
⊢ ∑ i ∈ Finset.range (N + 1), 1 / ↑i ^ z + ∑' (i : ℕ), 1 / ↑(i + (N + 1)) ^ z =
    ∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ z + ∑' (n : ℕ), 1 / (↑n + ↑N + 1) ^ z
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ AnalyticOn ℂ f U
Tactic:
apply (HolomophicOn_riemannZeta.analyticOn isOpen_ne).mono
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ U ⊆ {s | s ≠ 1}
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ U ⊆ {s | s ≠ 1}
Tactic:
simp only [ne_eq, setOf_subset_setOf, and_imp, U]
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ ∀ (a : ℂ), ¬a = 1 → 0 < a.re → ¬a = 1
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ ∀ (a : ℂ), ¬a = 1 → 0 < a.re → ¬a = 1
Tactic:
exact fun a ha _ ↦ ha
Proof state after:
no goals
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
⊢ IsPreconnected U
Tactic:
apply IsConnected.isPreconnected
Proof state after:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
⊢ IsConnected U
Theorem: Zeta0EqZeta
Proof state before:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
⊢ IsConnected U
Tactic:
apply (IsOpen.isConnected_iff_isPathConnected isOpen_aux).mp isPathConnected_aux
Proof state after:
no goals
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
⊢ 2 ∈ U
Tactic:
simp [U]
Proof state after:
no goals
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
⊢ s ∈ U
Tactic:
simp [U, reS_pos, s_ne_one]
Proof state after:
no goals
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ {z | 1 < z.re} ∈ 𝓝 2
Tactic:
apply mem_nhds_iff.mpr
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ ∃ t ⊆ {z | 1 < z.re}, IsOpen t ∧ 2 ∈ t
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ ∃ t ⊆ {z | 1 < z.re}, IsOpen t ∧ 2 ∈ t
Tactic:
use {z : ℂ | 1 < z.re}
Proof state after:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ {z | 1 < z.re} ⊆ {z | 1 < z.re} ∧ IsOpen {z | 1 < z.re} ∧ 2 ∈ {z | 1 < z.re}
Theorem: Zeta0EqZeta
Proof state before:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ {z | 1 < z.re} ⊆ {z | 1 < z.re} ∧ IsOpen {z | 1 < z.re} ∧ 2 ∈ {z | 1 < z.re}
Tactic:
simp only [setOf_subset_setOf, imp_self, forall_const, mem_setOf_eq, re_ofNat,
  Nat.one_lt_ofNat, and_true, true_and]
Proof state after:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ IsOpen {z | 1 < z.re}
Theorem: Zeta0EqZeta
Proof state before:
case h
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ IsOpen {z | 1 < z.re}
Tactic:
exact isOpen_lt (by continuity) (by continuity)
Proof state after:
no goals
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ Continuous fun z => 1
Tactic:
continuity
Proof state after:
no goals
Theorem: Zeta0EqZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
f : ℂ → ℂ := ζ
g : ℂ → ℂ := ζ₀ N
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
f_an : AnalyticOn ℂ f U
g_an : AnalyticOn ℂ g U
preconU : IsPreconnected U
h2 : 2 ∈ U
s_mem : s ∈ U
⊢ Continuous fun z => z.re
Tactic:
continuity
Proof state after:
no goals
Theorem: DerivZeta0EqDerivZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
⊢ deriv (ζ₀ N) s = deriv ζ s
Tactic:
let U := {z : ℂ | z ≠ 1 ∧ 0 < z.re}
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ deriv (ζ₀ N) s = deriv ζ s
Theorem: DerivZeta0EqDerivZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
⊢ deriv (ζ₀ N) s = deriv ζ s
Tactic:
have {x : ℂ} (hx : x ∈ U) : ζ₀ N x = ζ x := by
  simp only [mem_setOf_eq, U] at hx; exact Zeta0EqZeta (N := N) N_pos hx.2 hx.1
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ deriv (ζ₀ N) s = deriv ζ s
Theorem: DerivZeta0EqDerivZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ deriv (ζ₀ N) s = deriv ζ s
Tactic:
refine deriv_eqOn isOpen_aux ?_ (by simp [U, s_ne_one, reS_pos])
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ ∀ x ∈ {z | z ≠ 1 ∧ 0 < z.re}, HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x
Theorem: DerivZeta0EqDerivZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ ∀ x ∈ {z | z ≠ 1 ∧ 0 < z.re}, HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x
Tactic:
intro x hx
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
x : ℂ
hx : x ∈ {z | z ≠ 1 ∧ 0 < z.re}
⊢ HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x
Theorem: DerivZeta0EqDerivZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
x : ℂ
hx : x ∈ {z | z ≠ 1 ∧ 0 < z.re}
⊢ HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x
Tactic:
have hζ := HolomophicOn_riemannZeta.mono (by aesop)|>.hasDerivAt (s := U) <| isOpen_aux.mem_nhds hx
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
x : ℂ
hx : x ∈ {z | z ≠ 1 ∧ 0 < z.re}
hζ : HasDerivAt ζ (deriv ζ x) x
⊢ HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x
Theorem: DerivZeta0EqDerivZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
x : ℂ
hx : x ∈ {z | z ≠ 1 ∧ 0 < z.re}
hζ : HasDerivAt ζ (deriv ζ x) x
⊢ HasDerivWithinAt (ζ₀ N) (deriv ζ x) {z | z ≠ 1 ∧ 0 < z.re} x
Tactic:
exact hζ.hasDerivWithinAt.congr (fun y hy ↦ this hy) (this hx)
Proof state after:
no goals
Theorem: DerivZeta0EqDerivZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
x : ℂ
hx : x ∈ U
⊢ ζ₀ N x = ζ x
Tactic:
simp only [mem_setOf_eq, U] at hx
Proof state after:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
x : ℂ
hx : x ≠ 1 ∧ 0 < x.re
⊢ ζ₀ N x = ζ x
Theorem: DerivZeta0EqDerivZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
x : ℂ
hx : x ≠ 1 ∧ 0 < x.re
⊢ ζ₀ N x = ζ x
Tactic:
exact Zeta0EqZeta (N := N) N_pos hx.2 hx.1
Proof state after:
no goals
Theorem: DerivZeta0EqDerivZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
⊢ s ∈ {z | z ≠ 1 ∧ 0 < z.re}
Tactic:
simp [U, s_ne_one, reS_pos]
Proof state after:
no goals
Theorem: DerivZeta0EqDerivZeta
Proof state before:
N : ℕ
N_pos : 0 < N
s : ℂ
reS_pos : 0 < s.re
s_ne_one : s ≠ 1
U : Set ℂ := {z | z ≠ 1 ∧ 0 < z.re}
this : ∀ {x : ℂ}, x ∈ U → ζ₀ N x = ζ x
x : ℂ
hx : x ∈ {z | z ≠ 1 ∧ 0 < z.re}
⊢ U ⊆ {s | s ≠ 1}
Tactic:
aesop
Proof state after:
no goals
Theorem: norm_add₄_le
Proof state before:
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d : E
⊢ ‖a + b + c + d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖
Tactic:
apply le_trans <| norm_add_le (a + b + c) d
Proof state after:
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d : E
⊢ ‖a + b + c‖ + ‖d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖
Theorem: norm_add₄_le
Proof state before:
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d : E
⊢ ‖a + b + c‖ + ‖d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖
Tactic:
simp only [add_le_add_iff_right]
Proof state after:
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d : E
⊢ ‖a + b + c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖
Theorem: norm_add₄_le
Proof state before:
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d : E
⊢ ‖a + b + c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖
Tactic:
apply norm_add₃_le
Proof state after:
no goals
Theorem: norm_add₅_le
Proof state before:
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d e : E
⊢ ‖a + b + c + d + e‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖ + ‖e‖
Tactic:
apply le_trans <| norm_add_le (a + b + c + d) e
Proof state after:
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d e : E
⊢ ‖a + b + c + d‖ + ‖e‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖ + ‖e‖
Theorem: norm_add₅_le
Proof state before:
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d e : E
⊢ ‖a + b + c + d‖ + ‖e‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖ + ‖e‖
Tactic:
simp only [add_le_add_iff_right]
Proof state after:
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d e : E
⊢ ‖a + b + c + d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖
Theorem: norm_add₅_le
Proof state before:
E : Type u_1
inst✝ : SeminormedAddGroup E
a b c d e : E
⊢ ‖a + b + c + d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖
Tactic:
apply norm_add₄_le
Proof state after:
no goals
Theorem: mul_le_mul₃
Proof state before:
α : Type u_1
a b c d e f : α
inst✝³ : MulZeroClass α
inst✝² : Preorder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
h₁ : a ≤ b
h₂ : c ≤ d
h₃ : e ≤ f
c0 : 0 ≤ c
b0 : 0 ≤ b
e0 : 0 ≤ e
⊢ a * c * e ≤ b * d * f
Tactic:
apply mul_le_mul (mul_le_mul h₁ h₂ c0 b0) h₃ e0 <| mul_nonneg b0 <| le_trans c0 h₂
Proof state after:
no goals
Theorem: ZetaBnd_aux2
Proof state before:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
⊢ ‖↑n ^ (-(↑σ + ↑t * I))‖ ≤ (↑n)⁻¹ * A.exp
Tactic:
set s := σ + t * I
Proof state after:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
Theorem: ZetaBnd_aux2
Proof state before:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
Tactic:
by_cases n0 : n = 0
Proof state after:
case pos
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp

case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
Theorem: ZetaBnd_aux2
Proof state before:
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
Tactic:
have n_gt_0 : 0 < n := Nat.pos_of_ne_zero n0
Proof state after:
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
Theorem: ZetaBnd_aux2
Proof state before:
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
Tactic:
have n_gt_0' : (0 : ℝ) < (n : ℝ) := Nat.cast_pos.mpr n_gt_0
Proof state after:
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
Theorem: ZetaBnd_aux2
Proof state before:
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
Tactic:
have n_ge_1 : 1 ≤ (n : ℝ) := Nat.one_le_cast.mpr <| Nat.succ_le_of_lt n_gt_0
Proof state after:
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
Theorem: ZetaBnd_aux2
Proof state before:
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
Tactic:
calc
  _ = |((n : ℝ) ^ (-σ))| := ?_
  _ ≤ Real.exp (Real.log n * -σ) := Real.abs_rpow_le_exp_log_mul (n : ℝ) (-σ)
  _ ≤ Real.exp (Real.log n *  -(1 - A / Real.log t)) := ?_
  _ ≤ Real.exp (- Real.log n + A) := Real.exp_le_exp_of_le ?_
  _ ≤ _ := by rw [Real.exp_add, Real.exp_neg, Real.exp_log n_gt_0']
Proof state after:
case neg.calc_1
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ ‖↑n ^ (-s)‖ = |↑n ^ (-σ)|

case neg.calc_2
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ ((↑n).log * -σ).exp ≤ ((↑n).log * -(1 - A / t.log)).exp

case neg.calc_3
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ (↑n).log * -(1 - A / t.log) ≤ -(↑n).log + A
Theorem: ZetaBnd_aux2
Proof state before:
case pos
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
⊢ ‖↑n ^ (-s)‖ ≤ (↑n)⁻¹ * A.exp
Tactic:
simp_rw [n0, CharP.cast_eq_zero, inv_zero, zero_mul]
Proof state after:
case pos
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
⊢ ‖0 ^ (-s)‖ ≤ 0
Theorem: ZetaBnd_aux2
Proof state before:
case pos
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
⊢ ‖0 ^ (-s)‖ ≤ 0
Tactic:
rw [Complex.zero_cpow ?_]
Proof state after:
case pos
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
⊢ ‖0‖ ≤ 0

n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
⊢ -s ≠ 0
Theorem: ZetaBnd_aux2
Proof state before:
case pos
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
⊢ ‖0‖ ≤ 0

n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
⊢ -s ≠ 0
Tactic:
simp
Proof state after:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
⊢ -s ≠ 0
Theorem: ZetaBnd_aux2
Proof state before:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
⊢ -s ≠ 0
Tactic:
exact fun h ↦ (NeZero.of_pos σpos).ne <| zero_eq_neg.mp <| zero_re ▸ h ▸ (by simp [s])
Proof state after:
no goals
Theorem: ZetaBnd_aux2
Proof state before:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : n = 0
h : -s = 0
⊢ (-s).re = -σ
Tactic:
simp [s]
Proof state after:
no goals
Theorem: ZetaBnd_aux2
Proof state before:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ (-(↑n).log + A).exp ≤ (↑n)⁻¹ * A.exp
Tactic:
rw [Real.exp_add, Real.exp_neg, Real.exp_log n_gt_0']
Proof state after:
no goals
Theorem: ZetaBnd_aux2
Proof state before:
case neg.calc_1
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ ‖↑n ^ (-s)‖ = |↑n ^ (-σ)|
Tactic:
have : ‖(n : ℂ) ^ (-s)‖ = n ^ (-s.re) := abs_cpow_eq_rpow_re_of_pos n_gt_0' (-s)
Proof state after:
case neg.calc_1
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
this : ‖↑n ^ (-s)‖ = ↑n ^ (-s.re)
⊢ ‖↑n ^ (-s)‖ = |↑n ^ (-σ)|
Theorem: ZetaBnd_aux2
Proof state before:
case neg.calc_1
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
this : ‖↑n ^ (-s)‖ = ↑n ^ (-s.re)
⊢ ‖↑n ^ (-s)‖ = |↑n ^ (-σ)|
Tactic:
rw [this, abs_eq_self.mpr <| Real.rpow_nonneg n_gt_0'.le _]
Proof state after:
case neg.calc_1
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
this : ‖↑n ^ (-s)‖ = ↑n ^ (-s.re)
⊢ ↑n ^ (-s.re) = ↑n ^ (-σ)
Theorem: ZetaBnd_aux2
Proof state before:
case neg.calc_1
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
this : ‖↑n ^ (-s)‖ = ↑n ^ (-s.re)
⊢ ↑n ^ (-s.re) = ↑n ^ (-σ)
Tactic:
simp [s]
Proof state after:
no goals
Theorem: ZetaBnd_aux2
Proof state before:
case neg.calc_2
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ ((↑n).log * -σ).exp ≤ ((↑n).log * -(1 - A / t.log)).exp
Tactic:
apply Real.exp_le_exp_of_le <| mul_le_mul_of_nonneg_left _ <| Real.log_nonneg n_ge_1
Proof state after:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ -σ ≤ -(1 - A / t.log)
Theorem: ZetaBnd_aux2
Proof state before:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ -σ ≤ -(1 - A / t.log)
Tactic:
rw [neg_sub, neg_le_sub_iff_le_add, add_comm, ← Real.log_abs]
Proof state after:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ 1 ≤ σ + A / |t|.log
Theorem: ZetaBnd_aux2
Proof state before:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ 1 ≤ σ + A / |t|.log
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaBnd_aux2
Proof state before:
case neg.calc_3
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ (↑n).log * -(1 - A / t.log) ≤ -(↑n).log + A
Tactic:
simp only [neg_sub, le_neg_add_iff_add_le]
Proof state after:
case neg.calc_3
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ (↑n).log + (↑n).log * (A / t.log - 1) ≤ A
Theorem: ZetaBnd_aux2
Proof state before:
case neg.calc_3
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ (↑n).log + (↑n).log * (A / t.log - 1) ≤ A
Tactic:
ring_nf
Proof state after:
case neg.calc_3
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ (↑n).log * A * t.log⁻¹ ≤ A
Theorem: ZetaBnd_aux2
Proof state before:
case neg.calc_3
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ (↑n).log * A * t.log⁻¹ ≤ A
Tactic:
conv => rw [mul_comm, ← mul_assoc, ← Real.log_abs]; rhs; rw [← one_mul A]
Proof state after:
case neg.calc_3
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ |t|.log⁻¹ * (↑n).log * A ≤ 1 * A