Theorem: LogDerivZetaBnd (PrimeNumberTheoremAnd/ZetaBounds.lean)

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

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

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C),
          ∀ (σ t : ℝ),
            3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 9
Tactic:
use min A A', ⟨lt_min hA.1 hA'.1, min_le_of_right_le hA'.2⟩, C * C', mul_pos hC hC'
State after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ∀ (σ t : ℝ),
    3 < |t| → σ ∈ Ico (1 - min A A' / |t|.log ^ 9) 1 → ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9

State before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ∀ (σ t : ℝ),
    3 < |t| → σ ∈ Ico (1 - min A A' / |t|.log ^ 9) 1 → ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
intro σ t t_gt ⟨σ_ge, σ_lt⟩
State after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9

State before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
have logt_gt : (1 : ℝ) < Real.log |t| := by
  refine (Real.lt_log_iff_exp_lt (by linarith)).mpr (lt_trans ?_ t_gt)
  exact lt_trans Real.exp_one_lt_d9 (by norm_num)
State after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9

State before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
have σ_ge' : 1 - A / Real.log |t| ^ 9 ≤ σ := by
  apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge
  apply div_le_div hA.1.le (min_le_left A A') ?_ (by rfl)
  exact pow_pos (lt_trans (by norm_num) logt_gt) 9
State after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9

State before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
have σ_ge'' : 1 - A' / Real.log |t| ≤ σ := by
  apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge
  apply div_le_div hA'.1.le (min_le_right A A') (lt_trans (by norm_num) logt_gt) ?_
  exact le_self_pow logt_gt.le (by norm_num)
State after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9

State before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
replace h := h σ t t_gt ⟨σ_ge', σ_lt⟩
State after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9

State before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
replace h' := h' σ t t_gt ⟨σ_ge'', by linarith⟩
State after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9

State before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ‖deriv ζ (↑σ + ↑t * I) / ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
simp only [norm_div, norm_one, norm_mul, norm_inv]
State after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ / ‖ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9

State before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ / ‖ζ (↑σ + ↑t * I)‖ ≤ C * C' * |t|.log ^ 9
Tactic:
convert mul_le_mul h h' (by simp [apply_nonneg]) ?_ using 1 <;> (norm_cast; ring_nf)
State after:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ 0 ≤ C * |t|.log ^ 7

State before:
case h
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ 0 ≤ C * |t|.log ^ 7
Tactic:
positivity
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ 1 < |t|.log
Tactic:
refine (Real.lt_log_iff_exp_lt (by linarith)).mpr (lt_trans ?_ t_gt)
State after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ Real.exp 1 < 3

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ Real.exp 1 < 3
Tactic:
exact lt_trans Real.exp_one_lt_d9 (by norm_num)
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ 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| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
⊢ 2.7182818286 < 3
Tactic:
norm_num
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ 1 - A / |t|.log ^ 9 ≤ σ
Tactic:
apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge
State after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ min A A' / |t|.log ^ 9 ≤ A / |t|.log ^ 9

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ min A A' / |t|.log ^ 9 ≤ A / |t|.log ^ 9
Tactic:
apply div_le_div hA.1.le (min_le_left A A') ?_ (by rfl)
State after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ 0 < |t|.log ^ 9

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ 0 < |t|.log ^ 9
Tactic:
exact pow_pos (lt_trans (by norm_num) logt_gt) 9
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ |t|.log ^ 9 ≤ |t|.log ^ 9
Tactic:
rfl
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
⊢ 0 < 1
Tactic:
norm_num
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ 1 - A' / |t|.log ≤ σ
Tactic:
apply le_trans (tsub_le_tsub_left ?_ 1) σ_ge
State after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ min A A' / |t|.log ^ 9 ≤ A' / |t|.log

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ min A A' / |t|.log ^ 9 ≤ A' / |t|.log
Tactic:
apply div_le_div hA'.1.le (min_le_right A A') (lt_trans (by norm_num) logt_gt) ?_
State after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ |t|.log ≤ |t|.log ^ 9

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ |t|.log ≤ |t|.log ^ 9
Tactic:
exact le_self_pow logt_gt.le (by norm_num)
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ 0 < 1
Tactic:
norm_num
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
⊢ 9 ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
h' : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A' / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
⊢ σ ≤ 2
Tactic:
linarith
State after:
no goals

State before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ 0 ≤ ‖deriv ζ (↑σ + ↑t * I)‖
Tactic:
simp [apply_nonneg]
State after:
no goals

State before:
case h.e'_4
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
A' : ℝ
hA' : A' ∈ Ioc 0 (1 / 2)
C' : ℝ
hC' : 0 < C'
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - min A A' / |t|.log ^ 9 ≤ σ
σ_lt : σ < 1
logt_gt : 1 < |t|.log
σ_ge' : 1 - A / |t|.log ^ 9 ≤ σ
σ_ge'' : 1 - A' / |t|.log ≤ σ
h : 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
h' : ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C' * |t|.log ^ 2
⊢ C * C' * |t|.log ^ 9 = C * |t|.log ^ 7 * (C' * |t|.log ^ 2)
Tactic:
ring_nf
State after:
no goals