Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ ‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤
    C * |t|.log
Tactic:
calc
  _ ≤ Real.exp A * 2 * Real.log |t| + ‖N ^ (1 - s) / (1 - s)‖ + ‖(N : ℂ) ^ (-s) / 2‖ +
    ‖s * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ (s + 1)‖ := ?_
  _ ≤ Real.exp A * 2 * Real.log |t| + ‖N ^ (1 - s) / (1 - s)‖ + ‖(N : ℂ) ^ (-s) / 2‖ +
    2 * |t| * N ^ (-σ) / σ  := ?_
  _ = Real.exp A * 2 * Real.log |t| + N ^ (1 - σ) / ‖(1 - s)‖ + N ^ (-σ) / 2 +
    2 * |t| * N ^ (-σ) / σ  := ?_
  _ ≤ Real.exp A * 2 * Real.log |t| + |t| ^ (1 - σ) * 2 +
      |t| ^ (1 - σ) + 2 * |t| * (8 * |t| ^ (-σ)) := ?_
  _ = Real.exp A * 2 * Real.log |t| + (3 + 8 * 2) * |t| ^ (1 - σ) := ?_
  _ ≤ Real.exp A * 2 * Real.log |t| + (3 + 8 * 2) * Real.exp A * 1 := ?_
  _ ≤ Real.exp A * 2 * Real.log |t| + (3 + 8 * 2) * Real.exp A * Real.log |t| := ?_
  _ = _ := by ring
Proof state after:
case intro.intro.intro.intro.intro.calc_1
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ ‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤
    A.exp * 2 * |t|.log + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖

case intro.intro.intro.intro.intro.calc_2
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
      ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖ ≤
    A.exp * 2 * |t|.log + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ + 2 * |t| * ↑N ^ (-σ) / σ

case intro.intro.intro.intro.intro.calc_3
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ + 2 * |t| * ↑N ^ (-σ) / σ =
    A.exp * 2 * |t|.log + ↑N ^ (1 - σ) / ‖1 - s‖ + ↑N ^ (-σ) / 2 + 2 * |t| * ↑N ^ (-σ) / σ

case intro.intro.intro.intro.intro.calc_4
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + ↑N ^ (1 - σ) / ‖1 - s‖ + ↑N ^ (-σ) / 2 + 2 * |t| * ↑N ^ (-σ) / σ ≤
    A.exp * 2 * |t|.log + |t| ^ (1 - σ) * 2 + |t| ^ (1 - σ) + 2 * |t| * (8 * |t| ^ (-σ))

case intro.intro.intro.intro.intro.calc_5
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + |t| ^ (1 - σ) * 2 + |t| ^ (1 - σ) + 2 * |t| * (8 * |t| ^ (-σ)) =
    A.exp * 2 * |t|.log + (3 + 8 * 2) * |t| ^ (1 - σ)

case intro.intro.intro.intro.intro.calc_6
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + (3 + 8 * 2) * |t| ^ (1 - σ) ≤ A.exp * 2 * |t|.log + (3 + 8 * 2) * A.exp * 1

case intro.intro.intro.intro.intro.calc_7
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + (3 + 8 * 2) * A.exp * 1 ≤ A.exp * 2 * |t|.log + (3 + 8 * 2) * A.exp * |t|.log