Theorem: ZetaBnd_aux1 (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ 2 * |t| * ↑N ^ (-σ) / σ
Tactic:
rw [norm_mul, mul_div_assoc]
State after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ * ‖∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ 2 * |t| * (↑N ^ (-σ) / σ)

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ * ‖∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤ 2 * |t| * (↑N ^ (-σ) / σ)
Tactic:
apply mul_le_mul ?_ (ZetaBnd_aux1b N Npos hσ.1) (norm_nonneg _) (by positivity)
State after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ ≤ 2 * |t|

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ ≤ 2 * |t|
Tactic:
refine le_trans (by apply norm_add_le) ?_
State after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ‖ + ‖↑t * I‖ ≤ 2 * |t|

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ‖ + ‖↑t * I‖ ≤ 2 * |t|
Tactic:
simp only [norm_eq_abs, abs_ofReal, norm_mul, abs_I, mul_one, abs_of_pos hσ.1]
State after:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ σ + |t| ≤ 2 * |t|

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ σ + |t| ≤ 2 * |t|
Tactic:
linarith [hσ.2]
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ 0 ≤ 2 * |t|
Tactic:
positivity
State after:
no goals

State before:
N : ℕ
Npos : 1 ≤ N
σ t : ℝ
hσ : σ ∈ Ioc 0 2
ht : 2 ≤ |t|
⊢ ‖↑σ + ↑t * I‖ ≤ ?m.373229
Tactic:
apply norm_add_le
State after:
no goals