internlm/Lean-Github huggingface dataset:
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
⊢ ‖‖ζ (↑σ + 2 * ↑t * I)‖‖ ≤ ‖C * |2 * t|.log‖
Tactic:
convert h using 1
Proof state after:
case h.e'_3
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)‖‖ = ‖ζ (↑σ + ↑(2 * t) * I)‖

case h.e'_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
⊢ ‖C * |2 * t|.log‖ = C * |2 * t|.log
Theorem: ZetaInvBound2
Proof state before:
case h.e'_3
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)‖‖ = ‖ζ (↑σ + ↑(2 * t) * I)‖

case h.e'_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
⊢ ‖C * |2 * t|.log‖ = C * |2 * t|.log
Tactic:
simp
Proof state after:
case h.e'_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
⊢ ‖C * |2 * t|.log‖ = C * |2 * t|.log
Theorem: ZetaInvBound2
Proof state before:
case h.e'_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
⊢ ‖C * |2 * t|.log‖ = C * |2 * t|.log
Tactic:
rw [Real.norm_eq_abs, abs_eq_self.mpr <| mul_nonneg hC.le this]
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) / c) ^ (-3 / 4)‖
Tactic:
simpa only [Real.norm_eq_abs, abs_pos]
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
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 ≤ σ
Tactic:
linarith [(div_nonneg ha.1.le (Real.log_nonneg (by linarith)) : 0 ≤ A / Real.log |2 * t|)]
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
⊢ 1 ≤ |2 * t|
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_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
⊢ ‖((σ - 1) / c) ^ (-3 / 4) * C ^ (1 / 4) * |2 * t|.log ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4) * C ^ (1 / 4) * (|t| ^ 2).log ^ (1 / 4)‖
Tactic:
simp only [Real.log_abs, norm_mul]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_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
⊢ ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖C ^ (1 / 4)‖ * ‖(2 * t).log ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖C ^ (1 / 4)‖ * ‖(|t| ^ 2).log ^ (1 / 4)‖
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_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
⊢ ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖C ^ (1 / 4)‖ * ‖(2 * t).log ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖C ^ (1 / 4)‖ * ‖(|t| ^ 2).log ^ (1 / 4)‖
Tactic:
apply (mul_le_mul_left ?_).mpr
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_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
⊢ ‖(2 * t).log ^ (1 / 4)‖ ≤ ‖(|t| ^ 2).log ^ (1 / 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
⊢ 0 < ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖C ^ (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
⊢ 0 < ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖C ^ (1 / 4)‖
Tactic:
. apply mul_pos (abs_pos.mpr hnezero) (abs_pos.mpr ?_)
  have : C ≠ 0 := ne_of_gt hC
  contrapose! this; rwa [Real.rpow_eq_zero (by linarith) (by norm_num)] at this
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_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
⊢ ‖(2 * t).log ^ (1 / 4)‖ ≤ ‖(|t| ^ 2).log ^ (1 / 4)‖
Tactic:
rw [← Real.log_abs, Real.norm_rpow_of_nonneg <| Real.log_nonneg (by linarith)]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_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
⊢ ‖|2 * t|.log‖ ^ (1 / 4) ≤ ‖(|t| ^ 2).log ^ (1 / 4)‖
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_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
⊢ ‖|2 * t|.log‖ ^ (1 / 4) ≤ ‖(|t| ^ 2).log ^ (1 / 4)‖
Tactic:
have : 1 ≤ |(|t| ^ 2)| := by
  simp only [_root_.sq_abs, _root_.abs_pow, one_le_sq_iff_one_le_abs]
  linarith
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_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
this : 1 ≤ ||t| ^ 2|
⊢ ‖|2 * t|.log‖ ^ (1 / 4) ≤ ‖(|t| ^ 2).log ^ (1 / 4)‖
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_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
this : 1 ≤ ||t| ^ 2|
⊢ ‖|2 * t|.log‖ ^ (1 / 4) ≤ ‖(|t| ^ 2).log ^ (1 / 4)‖
Tactic:
conv => rhs; rw [← Real.log_abs, Real.norm_rpow_of_nonneg <| Real.log_nonneg this]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_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
this : 1 ≤ ||t| ^ 2|
⊢ ‖|2 * t|.log‖ ^ (1 / 4) ≤ ‖||t| ^ 2|.log‖ ^ (1 / 4)
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_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
this : 1 ≤ ||t| ^ 2|
⊢ ‖|2 * t|.log‖ ^ (1 / 4) ≤ ‖||t| ^ 2|.log‖ ^ (1 / 4)
Tactic:
apply Real.rpow_le_rpow (abs_nonneg _) ?_ (by norm_num)
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
this : 1 ≤ ||t| ^ 2|
⊢ ||2 * t|.log| ≤ ‖||t| ^ 2|.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
⊢ 1 ≤ ||t| ^ 2|
Tactic:
simp only [_root_.sq_abs, _root_.abs_pow, one_le_sq_iff_one_le_abs]
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
⊢ 1 ≤ |t|
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
⊢ 1 ≤ |t|
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 ≤ ||t| ^ 2|
⊢ 0 ≤ 1 / 4
Tactic:
norm_num
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 ≤ ||t| ^ 2|
⊢ ||2 * t|.log| ≤ ‖||t| ^ 2|.log‖
Tactic:
rw [Real.norm_eq_abs, abs_eq_self.mpr <| Real.log_nonneg (by linarith)]
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
this : 1 ≤ ||t| ^ 2|
⊢ |2 * t|.log ≤ |||t| ^ 2|.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
this : 1 ≤ ||t| ^ 2|
⊢ |2 * t|.log ≤ |||t| ^ 2|.log|
Tactic:
rw [abs_eq_self.mpr <| Real.log_nonneg this, abs_mul, Real.log_abs, Nat.abs_ofNat]
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
this : 1 ≤ ||t| ^ 2|
⊢ (2 * |t|).log ≤ (|t| ^ 2).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
this : 1 ≤ ||t| ^ 2|
⊢ (2 * |t|).log ≤ (|t| ^ 2).log
Tactic:
apply Real.log_le_log (mul_pos (by norm_num) (by linarith)) (by nlinarith)
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 ≤ ||t| ^ 2|
⊢ 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
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 ≤ ||t| ^ 2|
⊢ 0 < 2
Tactic:
norm_num
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 ≤ ||t| ^ 2|
⊢ 0 < |t|
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 ≤ ||t| ^ 2|
⊢ 2 * |t| ≤ |t| ^ 2
Tactic:
nlinarith
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) / c) ^ (-3 / 4)‖ * ‖C ^ (1 / 4)‖
Tactic:
apply mul_pos (abs_pos.mpr hnezero) (abs_pos.mpr ?_)
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
⊢ C ^ (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
⊢ C ^ (1 / 4) ≠ 0
Tactic:
have : C ≠ 0 := ne_of_gt hC
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
this : C ≠ 0
⊢ C ^ (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
this : C ≠ 0
⊢ C ^ (1 / 4) ≠ 0
Tactic:
contrapose! this
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
this : C ^ (1 / 4) = 0
⊢ C = 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
this : C ^ (1 / 4) = 0
⊢ C = 0
Tactic:
rwa [Real.rpow_eq_zero (by linarith) (by norm_num)] at this
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 : C ^ (1 / 4) = 0
⊢ 0 ≤ C
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 : C ^ (1 / 4) = 0
⊢ 1 / 4 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_5
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) * C ^ (1 / 4) * (|t| ^ 2).log ^ (1 / 4)‖ =
    ‖(σ - 1) ^ (-3 / 4) * c ^ (3 / 4) * (C ^ (1 / 4) * (|t| ^ 2).log ^ (1 / 4))‖
Tactic:
have : (-3 : ℝ) / 4 = -((3 : ℝ)/ 4) := by norm_num
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_5
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 : -3 / 4 = -(3 / 4)
⊢ ‖((σ - 1) / c) ^ (-3 / 4) * C ^ (1 / 4) * (|t| ^ 2).log ^ (1 / 4)‖ =
    ‖(σ - 1) ^ (-3 / 4) * c ^ (3 / 4) * (C ^ (1 / 4) * (|t| ^ 2).log ^ (1 / 4))‖
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_5
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 : -3 / 4 = -(3 / 4)
⊢ ‖((σ - 1) / c) ^ (-3 / 4) * C ^ (1 / 4) * (|t| ^ 2).log ^ (1 / 4)‖ =
    ‖(σ - 1) ^ (-3 / 4) * c ^ (3 / 4) * (C ^ (1 / 4) * (|t| ^ 2).log ^ (1 / 4))‖
Tactic:
simp only [norm_mul, mul_eq_mul_right_iff, abs_eq_zero, this, ← mul_assoc]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_5
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 : -3 / 4 = -(3 / 4)
⊢ (‖((σ - 1) / c) ^ (-(3 / 4))‖ = ‖(σ - 1) ^ (-(3 / 4))‖ * ‖c ^ (3 / 4)‖ ∨ ‖C ^ (1 / 4)‖ = 0) ∨
    ‖(|t| ^ 2).log ^ (1 / 4)‖ = 0
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_5
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 : -3 / 4 = -(3 / 4)
⊢ (‖((σ - 1) / c) ^ (-(3 / 4))‖ = ‖(σ - 1) ^ (-(3 / 4))‖ * ‖c ^ (3 / 4)‖ ∨ ‖C ^ (1 / 4)‖ = 0) ∨
    ‖(|t| ^ 2).log ^ (1 / 4)‖ = 0
Tactic:
left
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_5.h
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 : -3 / 4 = -(3 / 4)
⊢ ‖((σ - 1) / c) ^ (-(3 / 4))‖ = ‖(σ - 1) ^ (-(3 / 4))‖ * ‖c ^ (3 / 4)‖ ∨ ‖C ^ (1 / 4)‖ = 0