Theorem: ZetaInvBound2 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
⊢ ∃ C > 0,
    ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
obtain ⟨A, ha, C, hC, h⟩ := ZetaUpperBnd
State after:
case 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 > 0,
    ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)

State before:
case 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 > 0,
    ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
obtain ⟨c, hc, h_inv⟩ := ZetaNear1BndExact
State after:
case 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)
⊢ ∃ C > 0,
    ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)

State before:
case 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)
⊢ ∃ C > 0,
    ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
refine ⟨(2 * C) ^ ((1 : ℝ)/ 4) * c ^ ((3 : ℝ)/ 4), by positivity, ?_⟩
State after:
case 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)
⊢ ∀ {σ : ℝ},
    σ ∈ Ioc 1 2 →
      ∀ (t : ℝ),
        3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)

State before:
case 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)
⊢ ∀ {σ : ℝ},
    σ ∈ Ioc 1 2 →
      ∀ (t : ℝ),
        3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
intro σ hσ t t_gt
State after:
case 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)
σ : ℝ
hσ : σ ∈ Ioc 1 2
t : ℝ
t_gt : 3 < |t|
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)

State before:
case 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)
σ : ℝ
hσ : σ ∈ Ioc 1 2
t : ℝ
t_gt : 3 < |t|
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
obtain ⟨σ_gt, σ_le⟩ := hσ
State after:
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
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)

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
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
have ht' : 3 < |2 * t| := by simp only [abs_mul, Nat.abs_ofNat]; linarith
State after:
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|
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)

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|
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
have hnezero: ((σ - 1) / c) ^ (-3 / 4 : ℝ) ≠ 0 := by
  have : (σ - 1) / c ≠ 0 := ne_of_gt <| div_pos (by linarith) hc
  contrapose! this
  rwa [Real.rpow_eq_zero (div_nonneg (by linarith) hc.le) (by norm_num)] at this
State after:
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)

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 : ℝ))‖ := ?_
  _ = _ := ?_
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)

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)
⊢ (2 * C) ^ (1 / 4) * c ^ (3 / 4) > 0
Tactic:
positivity
State after:
no goals

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
⊢ 3 < |2 * t|
Tactic:
simp only [abs_mul, Nat.abs_ofNat]
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
⊢ 3 < 2 * |t|

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
⊢ 3 < 2 * |t|
Tactic:
linarith
State after:
no goals

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|
⊢ ((σ - 1) / c) ^ (-3 / 4) ≠ 0
Tactic:
have : (σ - 1) / c ≠ 0 := ne_of_gt <| div_pos (by linarith) hc
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|
this : (σ - 1) / c ≠ 0
⊢ ((σ - 1) / c) ^ (-3 / 4) ≠ 0

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|
this : (σ - 1) / c ≠ 0
⊢ ((σ - 1) / c) ^ (-3 / 4) ≠ 0
Tactic:
contrapose! this
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|
this : ((σ - 1) / c) ^ (-3 / 4) = 0
⊢ (σ - 1) / c = 0

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|
this : ((σ - 1) / c) ^ (-3 / 4) = 0
⊢ (σ - 1) / c = 0
Tactic:
rwa [Real.rpow_eq_zero (div_nonneg (by linarith) hc.le) (by norm_num)] at this
State after:
no goals

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|
⊢ 0 < σ - 1
Tactic:
linarith
State after:
no goals

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|
this : ((σ - 1) / c) ^ (-3 / 4) = 0
⊢ 0 ≤ σ - 1
Tactic:
linarith
State after:
no goals

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|
this : ((σ - 1) / c) ^ (-3 / 4) = 0
⊢ -3 / 4 ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
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)‖
Tactic:
simp only [norm_div, norm_one, norm_mul, norm_norm]
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)‖

State before:
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)‖
Tactic:
convert ZetaInvBound1 σ_gt using 2
<;> exact abs_eq_self.mpr <| Real.rpow_nonneg (apply_nonneg _ _) _
State after:
no goals

State before:
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)‖
Tactic:
have bnd1: ‖ζ σ‖ ^ (3 / 4 : ℝ) ≤ ((σ - 1) / c) ^ (-(3 : ℝ) / 4) := by
  have : ((σ - 1) / c) ^ (-(3 : ℝ) / 4) = (((σ - 1) / c) ^ (-1 : ℝ)) ^ (3 / 4 : ℝ) := by
    rw [← Real.rpow_mul ?_]; ring_nf; exact div_nonneg (by linarith) hc.le
  rw [this]
  apply Real.rpow_le_rpow (by simp [apply_nonneg]) ?_ (by norm_num)
  convert h_inv σ ⟨σ_gt, σ_le⟩ using 1; simp [Real.rpow_neg_one, inv_div]
State after:
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
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ ‖‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤ ‖((σ - 1) / c) ^ (-3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖

State before:
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
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ ‖‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤ ‖((σ - 1) / c) ^ (-3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖
Tactic:
simp only [norm_div, norm_one, norm_mul]
State after:
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
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ ‖‖ζ ↑σ‖ ^ (3 / 4)‖ * ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖

State before:
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
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ ‖‖ζ ↑σ‖ ^ (3 / 4)‖ * ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖ ≤
    ‖((σ - 1) / c) ^ (-3 / 4)‖ * ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖
Tactic:
apply (mul_le_mul_right ?_).mpr
State after:
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
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ ‖‖ζ ↑σ‖ ^ (3 / 4)‖ ≤ ‖((σ - 1) / c) ^ (-3 / 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)
⊢ 0 < ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖

State before:
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
bnd1 : ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
⊢ ‖‖ζ ↑σ‖ ^ (3 / 4)‖ ≤ ‖((σ - 1) / c) ^ (-3 / 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)
⊢ 0 < ‖‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)‖
Tactic:
convert bnd1 using 1
State after:
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)

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)

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

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 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
Tactic:
have : ((σ - 1) / c) ^ (-(3 : ℝ) / 4) = (((σ - 1) / c) ^ (-1 : ℝ)) ^ (3 / 4 : ℝ) := by
  rw [← Real.rpow_mul ?_]; ring_nf; exact div_nonneg (by linarith) hc.le
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) / c) ^ (-3 / 4) = (((σ - 1) / c) ^ (-1)) ^ (3 / 4)
⊢ ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)

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)
⊢ ‖ζ ↑σ‖ ^ (3 / 4) ≤ ((σ - 1) / c) ^ (-3 / 4)
Tactic:
rw [this]
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) / c) ^ (-3 / 4) = (((σ - 1) / c) ^ (-1)) ^ (3 / 4)
⊢ ‖ζ ↑σ‖ ^ (3 / 4) ≤ (((σ - 1) / c) ^ (-1)) ^ (3 / 4)

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)
⊢ ‖ζ ↑σ‖ ^ (3 / 4) ≤ (((σ - 1) / c) ^ (-1)) ^ (3 / 4)
Tactic:
apply Real.rpow_le_rpow (by simp [apply_nonneg]) ?_ (by norm_num)
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) / c) ^ (-3 / 4) = (((σ - 1) / c) ^ (-1)) ^ (3 / 4)
⊢ ‖ζ ↑σ‖ ≤ ((σ - 1) / c) ^ (-1)

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)
⊢ ‖ζ ↑σ‖ ≤ ((σ - 1) / c) ^ (-1)
Tactic:
convert h_inv σ ⟨σ_gt, σ_le⟩ using 1
State after:
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
this : ((σ - 1) / c) ^ (-3 / 4) = (((σ - 1) / c) ^ (-1)) ^ (3 / 4)
⊢ ((σ - 1) / c) ^ (-1) = c / (σ - 1)

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
this : ((σ - 1) / c) ^ (-3 / 4) = (((σ - 1) / c) ^ (-1)) ^ (3 / 4)
⊢ ((σ - 1) / c) ^ (-1) = c / (σ - 1)
Tactic:
simp [Real.rpow_neg_one, inv_div]
State after:
no goals

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) / c) ^ (-3 / 4) = (((σ - 1) / c) ^ (-1)) ^ (3 / 4)
Tactic:
rw [← Real.rpow_mul ?_]
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) / c) ^ (-3 / 4) = ((σ - 1) / c) ^ (-1 * (3 / 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

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) / c) ^ (-3 / 4) = ((σ - 1) / c) ^ (-1 * (3 / 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
Tactic:
ring_nf
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
⊢ 0 ≤ (σ - 1) / c

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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 _ _) _
State after:
no goals

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) _
State after:
no goals

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
State after:
no goals

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), ?_⟩
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)‖

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

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

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)
State after:
no goals

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
State after:
no goals

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

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

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

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

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
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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⟩
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 ≤ σ

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']
State after:
no goals

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

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

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

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

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 _]
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)

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

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

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
State after:
no goals

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
State after:
no goals

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

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

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]
State after:
no goals

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]
State after:
no goals

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|)]
State after:
no goals

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
State after:
no goals

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

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

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
State after:
no goals

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

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

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

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

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]
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|

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
State after:
no goals

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
State after:
no goals

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

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]
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

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)
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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 ?_)
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

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

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

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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

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]
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

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

State before:
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
Tactic:
left
State after:
case intro.intro.intro.intro.intro.intro.intro.calc_5.h.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)‖

State before:
case intro.intro.intro.intro.intro.intro.intro.calc_5.h.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)‖
Tactic:
conv => lhs; rw [Real.div_rpow (by linarith) hc.le, Real.rpow_neg hc.le, div_inv_eq_mul, norm_mul]
State after:
no goals

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 / 4 = -(3 / 4)
Tactic:
norm_num
State after:
no goals

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 : -3 / 4 = -(3 / 4)
⊢ 0 ≤ σ - 1
Tactic:
linarith
State after:
no goals

State before:
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))‖
Tactic:
simp only [Real.log_pow, Nat.cast_ofNat, norm_mul, Real.norm_eq_abs]
State after:
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)| * |(2 * |t|.log) ^ (1 / 4)|) =
    |(σ - 1) ^ (-3 / 4)| * |c ^ (3 / 4)| * (|(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|)

State before:
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)| * |(2 * |t|.log) ^ (1 / 4)|) =
    |(σ - 1) ^ (-3 / 4)| * |c ^ (3 / 4)| * (|(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|)
Tactic:
congr! 1
State after:
case intro.intro.intro.intro.intro.intro.intro.calc_6.h.e'_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
⊢ |C ^ (1 / 4)| * |(2 * |t|.log) ^ (1 / 4)| = |(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|

State before:
case intro.intro.intro.intro.intro.intro.intro.calc_6.h.e'_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
⊢ |C ^ (1 / 4)| * |(2 * |t|.log) ^ (1 / 4)| = |(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|
Tactic:
rw [Real.mul_rpow (by norm_num) hC.le, Real.mul_rpow (by norm_num) <|
    Real.log_nonneg (by linarith), abs_mul, abs_mul, ← mul_assoc, mul_comm _ |2 ^ (1 / 4)|]
State after:
no goals

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 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
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)
Tactic:
simp only [norm_mul, Real.norm_eq_abs]
State after:
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)

State before:
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)
Tactic:
have : (2 * C) ^ ((1 : ℝ)/ 4) * c ^ ((3 : ℝ)/ 4) =
  |(2 * C) ^ ((1 : ℝ)/ 4) * c ^ ((3 : ℝ)/ 4)| := by
  rw [abs_eq_self.mpr (by apply mul_nonneg <;> (apply Real.rpow_nonneg; linarith))]
State after:
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
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ |(σ - 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)

State before:
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
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ |(σ - 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)
Tactic:
rw [this, abs_mul, abs_eq_self.mpr (by apply Real.rpow_nonneg; linarith), abs_eq_self.mpr (by positivity),
  abs_eq_self.mpr (by positivity), abs_eq_self.mpr (by apply Real.rpow_nonneg (Real.log_nonneg (by linarith)))]
State after:
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
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ (σ - 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)

State before:
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
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ (σ - 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)
Tactic:
ring_nf
State after:
no goals

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
⊢ (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
Tactic:
rw [abs_eq_self.mpr (by apply mul_nonneg <;> (apply Real.rpow_nonneg; linarith))]
State after:
no goals

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 ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4)
Tactic:
apply mul_nonneg <;> (apply Real.rpow_nonneg; linarith)
State after:
no goals

State before:
case hb
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 ≤ c ^ (3 / 4)
Tactic:
apply Real.rpow_nonneg
State after:
case hb.hx
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 ≤ c

State before:
case hb.hx
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 ≤ c
Tactic:
linarith
State after:
no goals

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 : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ (σ - 1) ^ (-3 / 4)
Tactic:
apply Real.rpow_nonneg
State after:
case hx
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 : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ σ - 1

State before:
case hx
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 : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ σ - 1
Tactic:
linarith
State after:
no goals

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 : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ c ^ (3 / 4)
Tactic:
positivity
State after:
no goals

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 : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ (2 * C) ^ (1 / 4)
Tactic:
positivity
State after:
no goals

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 : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ |t|.log ^ (1 / 4)
Tactic:
apply Real.rpow_nonneg (Real.log_nonneg (by linarith))
State after:
no goals

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 : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 1 ≤ |t|
Tactic:
linarith
State after:
no goals