Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
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 * I)‖ ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
calc
  _ ≤ ‖‖ζ σ‖ ^ (3 / 4 : ℝ) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4 : ℝ)‖ := ?_
  _ ≤ ‖((σ - 1) / c) ^ (-3 / 4 : ℝ) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4 : ℝ)‖ := ?_
  _ ≤ ‖((σ - 1) / c) ^ (-3 / 4 : ℝ) * C ^ (1 / 4 : ℝ) * (Real.log |2 * t|) ^ (1 / 4 : ℝ)‖ := ?_
  _ ≤ ‖((σ - 1) / c) ^ (-3 / 4 : ℝ) * C ^ (1 / 4 : ℝ) * (Real.log (|t| ^ 2)) ^ (1 / 4 : ℝ)‖ := ?_
  _ = ‖((σ - 1)) ^ (-3 / 4 : ℝ) * c ^ (3 / 4 : ℝ) * (C ^ (1 / 4 : ℝ) * (Real.log (|t| ^ 2)) ^ (1 / 4 : ℝ))‖ := ?_
  _ = ‖((σ - 1)) ^ (-3 / 4 : ℝ) * c ^ (3 / 4 : ℝ) * ((2 * C) ^ (1 / 4 : ℝ) * Real.log |t| ^ (1 / 4 : ℝ))‖ := ?_
  _ = _ := ?_
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_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 / ‖ζ (↑σ + ↑t * I)‖ ≤ ‖‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖

case intro.intro.intro.intro.intro.intro.intro.calc_2
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 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤ ‖((σ - 1) / c) ^ (-3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖

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)‖

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)‖

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))‖

case intro.intro.intro.intro.intro.intro.intro.calc_6
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) ^ (-3 / 4) * c ^ (3 / 4) * (C ^ (1 / 4) * (|t| ^ 2).log ^ (1 / 4))‖ =
    ‖(σ - 1) ^ (-3 / 4) * c ^ (3 / 4) * ((2 * C) ^ (1 / 4) * |t|.log ^ (1 / 4))‖

case intro.intro.intro.intro.intro.intro.intro.calc_7
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) ^ (-3 / 4) * c ^ (3 / 4) * ((2 * C) ^ (1 / 4) * |t|.log ^ (1 / 4))‖ =
    (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)