Theorem: ZetaInvBound1 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)
Tactic:
apply (div_le_iff ?_).mpr
State after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖

σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖

σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖
Tactic:
apply (Real.rpow_le_rpow_iff (z := 4) (by norm_num) ?_ (by norm_num)).mp
State after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ^ 4 ≤ (‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖) ^ 4

σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖

σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < 4
Tactic:
norm_num
State after:
no goals

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ^ 4 ≤ (‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖) ^ 4
Tactic:
simp only [Real.one_rpow]
State after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ (‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖) ^ 4

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ (‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖) ^ 4
Tactic:
rw [Real.mul_rpow, Real.mul_rpow, ← Real.rpow_mul, ← Real.rpow_mul]
State after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ (3 / 4 * 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4 * 4) * ‖ζ (↑σ + ↑t * I)‖ ^ 4

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ (3 / 4 * 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4 * 4) * ‖ζ (↑σ + ↑t * I)‖ ^ 4

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
  IsUnit.div_mul_cancel, IsUnit.inv_mul_cancel, Real.rpow_one]
State after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + 2 * ↑t * I)‖ * ‖ζ (↑σ + ↑t * I)‖ ^ 4

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + 2 * ↑t * I)‖ * ‖ζ (↑σ + ↑t * I)‖ ^ 4

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
conv => rw [mul_assoc]; rhs; rhs; rw [mul_comm]
State after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * (‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * (‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
rw [← mul_assoc]
State after:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
have := norm_zeta_product_ge_one (x := σ - 1) (by linarith) t
State after:
σ t : ℝ
σ_gt : 1 < σ
this : ‖ζ (1 + ↑(σ - 1)) ^ 3 * ζ (1 + ↑(σ - 1) + I * ↑t) ^ 4 * ζ (1 + ↑(σ - 1) + 2 * I * ↑t)‖ ≥ 1
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖

State before:
σ t : ℝ
σ_gt : 1 < σ
this : ‖ζ (1 + ↑(σ - 1)) ^ 3 * ζ (1 + ↑(σ - 1) + I * ↑t) ^ 4 * ζ (1 + ↑(σ - 1) + 2 * I * ↑t)‖ ≥ 1
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
simp_rw [ge_iff_le, norm_mul, norm_pow, ofReal_sub, ofReal_one, add_sub_cancel, ← Real.rpow_natCast] at this
State after:
σ t : ℝ
σ_gt : 1 < σ
this : 1 ≤ ‖ζ ↑σ‖ ^ ↑3 * ‖ζ (↑σ + I * ↑t)‖ ^ ↑4 * ‖ζ (↑σ + 2 * I * ↑t)‖
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖

State before:
σ t : ℝ
σ_gt : 1 < σ
this : 1 ≤ ‖ζ ↑σ‖ ^ ↑3 * ‖ζ (↑σ + I * ↑t)‖ ^ ↑4 * ‖ζ (↑σ + 2 * I * ↑t)‖
⊢ 1 ≤ ‖ζ ↑σ‖ ^ 3 * ‖ζ (↑σ + ↑t * I)‖ ^ 4 * ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
convert this using 3 <;> ring_nf
State after:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖

State before:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
any_goals ring_nf
State after:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖

State before:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
any_goals apply norm_nonneg
State after:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

State before:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4)

case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)
Tactic:
any_goals apply Real.rpow_nonneg <| norm_nonneg _
State after:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

State before:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)
Tactic:
apply mul_nonneg <;> apply Real.rpow_nonneg <| norm_nonneg _
State after:
no goals

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < σ - 1
Tactic:
linarith
State after:
no goals

State before:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4)
Tactic:
ring_nf
State after:
case hx
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)

State before:
case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I)‖
Tactic:
apply norm_nonneg
State after:
no goals

State before:
case hy
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ (↑σ + ↑t * I * 2)‖ ^ (1 / 4)
Tactic:
apply Real.rpow_nonneg <| norm_nonneg _
State after:
no goals

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖
Tactic:
refine mul_nonneg (mul_nonneg ?_ ?_) ?_ <;> simp [Real.rpow_nonneg]
State after:
no goals

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖
Tactic:
have s_ne_one : σ + t * I ≠ 1 := by
  contrapose! σ_gt; apply le_of_eq; apply And.left; simpa [Complex.ext_iff] using σ_gt
State after:
σ t : ℝ
σ_gt : 1 < σ
s_ne_one : ↑σ + ↑t * I ≠ 1
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖

State before:
σ t : ℝ
σ_gt : 1 < σ
s_ne_one : ↑σ + ↑t * I ≠ 1
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖
Tactic:
simpa using riemannZeta_ne_zero_of_one_le_re s_ne_one (by simp [σ_gt.le])
State after:
no goals

State before:
σ t : ℝ
σ_gt : 1 < σ
⊢ ↑σ + ↑t * I ≠ 1
Tactic:
contrapose! σ_gt
State after:
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ ≤ 1

State before:
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ ≤ 1
Tactic:
apply le_of_eq
State after:
case a
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ = 1

State before:
case a
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ = 1
Tactic:
apply And.left
State after:
case a.self
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ = 1 ∧ ?a.b✝

case a.b
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ Prop

State before:
case a.self
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ σ = 1 ∧ ?a.b✝

case a.b
σ t : ℝ
σ_gt : ↑σ + ↑t * I = 1
⊢ Prop
Tactic:
simpa [Complex.ext_iff] using σ_gt
State after:
no goals

State before:
σ t : ℝ
σ_gt : 1 < σ
s_ne_one : ↑σ + ↑t * I ≠ 1
⊢ 1 ≤ (↑σ + ↑t * I).re
Tactic:
simp [σ_gt.le]
State after:
no goals