Theorem: ZetaDerivUpperBnd (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
obtain ⟨A, hA, _, _, _⟩ := ZetaUpperBnd
State after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2

State before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
let C := 4 * Real.exp A * (5 + 8 * 2)
State after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2

State before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
refine ⟨A, hA, C, by positivity, ?_⟩
State after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
⊢ ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2

State before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
⊢ ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
intro σ t t_gt ⟨σ_ge, σ_le⟩
State after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2

State before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
obtain ⟨Npos, N_le_t, _, _, σPos, neOne⟩ := UpperBnd_aux hA t_gt σ_ge
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
rw [← DerivZeta0EqDerivZeta Npos (by simp [σPos]) neOne]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖deriv (ζ₀ ⌊|t|⌋₊) (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖deriv (ζ₀ ⌊|t|⌋₊) (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
apply le_trans (NormDerivZeta0Le Npos hA σ_ge σPos t_gt) ?_
State after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 * (↑⌊|t|⌋₊).log *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    C * |t|.log ^ 2

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 * (↑⌊|t|⌋₊).log *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    C * |t|.log ^ 2
Tactic:
conv => rw [mul_comm 4, mul_assoc _ 4 _]; rhs; rw [sq, ← mul_assoc, mul_comm C, mul_assoc]
State after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ (↑⌊|t|⌋₊).log *
      (4 *
        (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
              ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
            ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
          ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖)) ≤
    |t|.log * (C * |t|.log)

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ (↑⌊|t|⌋₊).log *
      (4 *
        (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
              ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
            ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
          ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖)) ≤
    |t|.log * (C * |t|.log)
Tactic:
refine mul_le_mul (Real.log_le_log (by positivity) N_le_t) ?_ (by positivity) (by positivity)
State after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    C * |t|.log

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    C * |t|.log
Tactic:
simp only [C, mul_assoc, Zeta0EqZeta Npos (by simp [σPos]) neOne]
State after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    4 * (A.exp * ((5 + 8 * 2) * |t|.log))

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 4 *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖) ≤
    4 * (A.exp * ((5 + 8 * 2) * |t|.log))
Tactic:
refine mul_le_mul_left (by norm_num) |>.mpr ?_
State after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ + ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
        ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
      ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤
    A.exp * ((5 + 8 * 2) * |t|.log)

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ + ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
        ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
      ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖ ≤
    A.exp * ((5 + 8 * 2) * |t|.log)
Tactic:
convert ZetaUpperBnd' hA t_gt ⟨σ_ge, σ_le⟩ using 1
State after:
case h.e'_4
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ A.exp * ((5 + 8 * 2) * |t|.log) = A.exp * (5 + 8 * 2) * |t|.log

State before:
case h.e'_4
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ A.exp * ((5 + 8 * 2) * |t|.log) = A.exp * (5 + 8 * 2) * |t|.log
Tactic:
ring
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
⊢ 0 < C
Tactic:
positivity
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 < (↑σ + ↑t * I).re
Tactic:
simp [σPos]
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 < ↑⌊|t|⌋₊
Tactic:
positivity
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 ≤
    4 *
      (‖∑ n ∈ Finset.range (⌊|t|⌋₊ + 1), 1 / ↑n ^ (↑σ + ↑t * I)‖ +
            ‖↑⌊|t|⌋₊ ^ (1 - (↑σ + ↑t * I)) / (1 - (↑σ + ↑t * I))‖ +
          ‖↑⌊|t|⌋₊ ^ (-(↑σ + ↑t * I)) / 2‖ +
        ‖(↑σ + ↑t * I) * ∫ (x : ℝ) in Ioi ↑⌊|t|⌋₊, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (↑σ + ↑t * I + 1)‖)
Tactic:
positivity
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 ≤ |t|.log
Tactic:
positivity
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
w✝¹ : ℝ
w✝ : 0 < w✝¹
h✝ : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ w✝¹ * |t|.log
C : ℝ := 4 * A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 < 4
Tactic:
norm_num
State after:
no goals