internlm/Lean-Github huggingface dataset:
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ 0 ≤ (σ - 1) / c
Tactic:
exact div_nonneg (by linarith) hc.le
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ 0 ≤ σ - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : ((σ - 1) / c) ^ (-3 / 4) = (((σ - 1) / c) ^ (-1)) ^ (3 / 4)
⊢ 0 ≤ ‖ζ ↑σ‖
Tactic:
simp [apply_nonneg]
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : ((σ - 1) / c) ^ (-3 / 4) = (((σ - 1) / c) ^ (-1)) ^ (3 / 4)
⊢ 0 ≤ 3 / 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
case h.e'_3
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ ‖‖ζ ↑σ‖ ^ (3 / 4)‖ = ‖ζ ↑σ‖ ^ (3 / 4)
Tactic:
exact abs_eq_self.mpr <| Real.rpow_nonneg (apply_nonneg _ _) _
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
case h.e'_4
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ ‖((σ - 1) / c) ^ (-3 / 4)‖ = ((σ - 1) / c) ^ (-3 / 4)
Tactic:
exact abs_eq_self.mpr <| Real.rpow_nonneg (div_nonneg (by linarith) hc.le) _
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ 0 ≤ σ - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ 0 < ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖
Tactic:
apply lt_iff_le_and_ne.mpr ⟨(by simp), ?_⟩
Proof state after:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ 0 ≠ ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ 0 ≠ ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖
Tactic:
have : ζ (↑σ + 2 * ↑t * I) ≠ 0 := by
  apply riemannZeta_ne_zero_of_one_le_re ?_ (by simp [σ_gt.le])
  contrapose! σ_gt; apply le_of_eq; apply And.left; simpa [Complex.ext_iff] using σ_gt
Proof state after:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
this : ζ (↑σ + 2 * ↑t * I) ≠ 0
⊢ 0 ≠ ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
this : ζ (↑σ + 2 * ↑t * I) ≠ 0
⊢ 0 ≠ ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖
Tactic:
symm
Proof state after:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
this : ζ (↑σ + 2 * ↑t * I) ≠ 0
⊢ ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≠ 0
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
this : ζ (↑σ + 2 * ↑t * I) ≠ 0
⊢ ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≠ 0
Tactic:
exact fun h2 ↦ this (by simpa using h2)
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ 0 ≤ ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖
Tactic:
simp
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ ζ (↑σ + 2 * ↑t * I) ≠ 0
Tactic:
apply riemannZeta_ne_zero_of_one_le_re ?_ (by simp [σ_gt.le])
Proof state after:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ ↑σ + 2 * ↑t * I ≠ 1
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ ↑σ + 2 * ↑t * I ≠ 1
Tactic:
contrapose! σ_gt
Proof state after:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
σ_gt : ↑σ + 2 * ↑t * I = 1
⊢ σ ≤ 1
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
σ_gt : ↑σ + 2 * ↑t * I = 1
⊢ σ ≤ 1
Tactic:
apply le_of_eq
Proof state after:
case a
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
σ_gt : ↑σ + 2 * ↑t * I = 1
⊢ σ = 1
Theorem: ZetaInvBound2
Proof state before:
case a
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
σ_gt : ↑σ + 2 * ↑t * I = 1
⊢ σ = 1
Tactic:
apply And.left
Proof state after:
case a.self
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
σ_gt : ↑σ + 2 * ↑t * I = 1
⊢ σ = 1 ∧ ?a.b✝

case a.b
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
σ_gt : ↑σ + 2 * ↑t * I = 1
⊢ Prop
Theorem: ZetaInvBound2
Proof state before:
case a.self
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
σ_gt : ↑σ + 2 * ↑t * I = 1
⊢ σ = 1 ∧ ?a.b✝

case a.b
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
σ_gt : ↑σ + 2 * ↑t * I = 1
⊢ Prop
Tactic:
simpa [Complex.ext_iff] using σ_gt
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ 1 ≤ (↑σ + 2 * ↑t * I).re
Tactic:
simp [σ_gt.le]
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
this : ζ (↑σ + 2 * ↑t * I) ≠ 0
h2 : ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ = 0
⊢ ζ (↑σ + 2 * ↑t * I) = 0
Tactic:
simpa using h2
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_3
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ ‖((σ - 1) / c) ^ (-3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4) * C ^ (1 / 4) * |2 * t|.log ^ (1 / 4)‖
Tactic:
replace h := h σ (2 * t) (by simp [ht']) ⟨?_, σ_le⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4) * C ^ (1 / 4) * |2 * t|.log ^ (1 / 4)‖

case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_1
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ 1 - A / |2 * t|.log ≤ σ
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ 3 < |2 * t|
Tactic:
simp [ht']
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4) * C ^ (1 / 4) * |2 * t|.log ^ (1 / 4)‖
Tactic:
have : 0 ≤ Real.log |2 * t| := Real.log_nonneg (by linarith)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4) * C ^ (1 / 4) * |2 * t|.log ^ (1 / 4)‖
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4) * C ^ (1 / 4) * |2 * t|.log ^ (1 / 4)‖
Tactic:
conv => rhs; rw [mul_assoc, ← Real.mul_rpow hC.le this]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4) * (C * |2 * t|.log) ^ (1 / 4)‖
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4) * (C * |2 * t|.log) ^ (1 / 4)‖
Tactic:
rw [norm_mul, norm_mul]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖(C * |2 * t|.log) ^ (1 / 4)‖
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖(C * |2 * t|.log) ^ (1 / 4)‖
Tactic:
conv => rhs; rhs; rw [Real.norm_rpow_of_nonneg <| mul_nonneg hC.le this]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖C * |2 * t|.log‖ ^ (1 / 4)
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖C * |2 * t|.log‖ ^ (1 / 4)
Tactic:
conv => lhs; rhs; rw [Real.norm_rpow_of_nonneg <| norm_nonneg _]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖‖ζ (↑σ + 2 * ↑t * I)‖‖ ^ (1 / 4) ≤
    ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖C * |2 * t|.log‖ ^ (1 / 4)
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖‖ζ (↑σ + 2 * ↑t * I)‖‖ ^ (1 / 4) ≤
    ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖C * |2 * t|.log‖ ^ (1 / 4)
Tactic:
apply (mul_le_mul_left ?_).mpr
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖‖ζ (↑σ + 2 * ↑t * I)‖‖ ^ (1 / 4) ≤ ‖C * |2 * t|.log‖ ^ (1 / 4)

A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ 0 < ‖((σ - 1) / c) ^ (-3 / 4)‖
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_3.refine_2
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖‖ζ (↑σ + 2 * ↑t * I)‖‖ ^ (1 / 4) ≤ ‖C * |2 * t|.log‖ ^ (1 / 4)

A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ 0 < ‖((σ - 1) / c) ^ (-3 / 4)‖
Tactic:
apply Real.rpow_le_rpow (norm_nonneg _) ?_ (by norm_num)
Proof state after:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ ‖‖ζ (↑σ + 2 * ↑t * I)‖‖ ≤ ‖C * |2 * t|.log‖

A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ 0 < ‖((σ - 1) / c) ^ (-3 / 4)‖
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
⊢ 1 ≤ |2 * t|
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
h : ‖ζ (↑σ + ↑(2 * t) * I)‖ ≤ C * |2 * t|.log
this : 0 ≤ |2 * t|.log
⊢ 0 ≤ 1 / 4
Tactic:
norm_num
Proof state after:
no goals