internlm/Lean-Github huggingface dataset:
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∀ x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]], HasDerivAt (deriv ζ) (deriv (deriv ζ) x) x
Tactic:
intro x hx
Proof state after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ HasDerivAt (deriv ζ) (deriv (deriv ζ) x) x
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ HasDerivAt (deriv ζ) (deriv (deriv ζ) x) x
Tactic:
apply hasDerivAt_deriv_iff.mpr
Proof state after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ DifferentiableAt ℂ (deriv ζ) x
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ DifferentiableAt ℂ (deriv ζ) x
Tactic:
replace hx : x ≠ 1 := by
  contrapose! hx
  simp only [hx, mem_image, Complex.ext_iff, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im,
    I_im, mul_one, sub_self, add_zero, one_re, add_im, mul_im, zero_add, one_im, not_exists,
    not_and]
  exact fun _ _ _ ↦ t_ne_zero
Proof state after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
⊢ DifferentiableAt ℂ (deriv ζ) x
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
⊢ DifferentiableAt ℂ (deriv ζ) x
Tactic:
have := (Complex.analyticAt_iff_eventually_differentiableAt (c := x) (f := ζ)).mpr ?_
Proof state after:
case refine_2
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
⊢ DifferentiableAt ℂ (deriv ζ) x

case refine_1
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
⊢ ∀ᶠ (z : ℂ) in 𝓝 x, DifferentiableAt ℂ ζ z
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ x ≠ 1
Tactic:
contrapose! hx
Proof state after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x = 1
⊢ x ∉ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x = 1
⊢ x ∉ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
Tactic:
simp only [hx, mem_image, Complex.ext_iff, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im,
  I_im, mul_one, sub_self, add_zero, one_re, add_im, mul_im, zero_add, one_im, not_exists,
  not_and]
Proof state after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x = 1
⊢ ∀ x ∈ [[σ₁, σ₂]], x = 1 → ¬t = 0
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x = 1
⊢ ∀ x ∈ [[σ₁, σ₂]], x = 1 → ¬t = 0
Tactic:
exact fun _ _ _ ↦ t_ne_zero
Proof state after:
no goals
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case refine_2
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
⊢ DifferentiableAt ℂ (deriv ζ) x
Tactic:
obtain ⟨r, hr, h⟩ := this.exists_ball_analyticOn
Proof state after:
case refine_2.intro.intro
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
r : ℝ
hr : 0 < r
h : AnalyticOn ℂ ζ (Metric.ball x r)
⊢ DifferentiableAt ℂ (deriv ζ) x
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case refine_2.intro.intro
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
r : ℝ
hr : 0 < r
h : AnalyticOn ℂ ζ (Metric.ball x r)
⊢ DifferentiableAt ℂ (deriv ζ) x
Tactic:
apply (h.deriv x ?_).differentiableAt
Proof state after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
r : ℝ
hr : 0 < r
h : AnalyticOn ℂ ζ (Metric.ball x r)
⊢ x ∈ Metric.ball x r
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
this : AnalyticAt ℂ ζ x
r : ℝ
hr : 0 < r
h : AnalyticOn ℂ ζ (Metric.ball x r)
⊢ x ∈ Metric.ball x r
Tactic:
simp [hr]
Proof state after:
no goals
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case refine_1
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
⊢ ∀ᶠ (z : ℂ) in 𝓝 x, DifferentiableAt ℂ ζ z
Tactic:
filter_upwards [compl_singleton_mem_nhds hx] with z hz
Proof state after:
case h
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
z : ℂ
hz : z ∈ {1}ᶜ
⊢ DifferentiableAt ℂ ζ z
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case h
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
z : ℂ
hz : z ∈ {1}ᶜ
⊢ DifferentiableAt ℂ ζ z
Tactic:
apply differentiableAt_riemannZeta
Proof state after:
case h.hs'
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
z : ℂ
hz : z ∈ {1}ᶜ
⊢ z ≠ 1
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case h.hs'
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ≠ 1
z : ℂ
hz : z ∈ {1}ᶜ
⊢ z ≠ 1
Tactic:
simpa [mem_compl_iff, mem_singleton_iff] using hz
Proof state after:
no goals
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (fun y => ↑y + ↑t * I) [[σ₁, σ₂]]
Tactic:
exact continuous_ofReal.continuousOn.add continuousOn_const
Proof state after:
no goals
Theorem: Zeta_diff_Bnd
Proof state before:
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C),
          ∀ (σ₁ σ₂ t : ℝ),
            3 < |t| →
              1 - A / |t|.log ≤ σ₁ →
                σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
obtain ⟨A, hA, C, Cpos, hC⟩ := ZetaDerivUpperBnd
Proof state after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ 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| →
              1 - A / |t|.log ≤ σ₁ →
                σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Theorem: Zeta_diff_Bnd
Proof state before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ 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| →
              1 - A / |t|.log ≤ σ₁ →
                σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
refine ⟨A, hA, C, Cpos, ?_⟩
Proof state after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
⊢ ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Theorem: Zeta_diff_Bnd
Proof state before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
⊢ ∀ (σ₁ σ₂ t : ℝ),
    3 < |t| →
      1 - A / |t|.log ≤ σ₁ → σ₂ ≤ 2 → σ₁ < σ₂ → ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
intro σ₁ σ₂ t t_gt σ₁_ge σ₂_le σ₁_lt_σ₂
Proof state after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
⊢ ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Theorem: Zeta_diff_Bnd
Proof state before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
⊢ ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
have t_ne_zero : t ≠ 0 := by contrapose! t_gt; simp only [t_gt, abs_zero, Nat.ofNat_nonneg]
Proof state after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Theorem: Zeta_diff_Bnd
Proof state before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ‖ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
rw [← Zeta_eq_int_derivZeta t_ne_zero]
Proof state after:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ‖∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Theorem: Zeta_diff_Bnd
Proof state before:
case intro.intro.intro.intro
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ‖∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2 * (σ₂ - σ₁)
Tactic:
convert intervalIntegral.norm_integral_le_of_norm_le_const ?_ using 1
Proof state after:
case h.e'_4
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ C * |t|.log ^ 2 * (σ₂ - σ₁) = ?intro.intro.intro.intro.convert_6 * |σ₂ - σ₁|

case intro.intro.intro.intro.convert_6
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ℝ

case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ∀ x ∈ Ι σ₁ σ₂, ‖deriv ζ (↑x + ↑t * I)‖ ≤ ?intro.intro.intro.intro.convert_6
Theorem: Zeta_diff_Bnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
⊢ t ≠ 0
Tactic:
contrapose! t_gt
Proof state after:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_gt : t = 0
⊢ |t| ≤ 3
Theorem: Zeta_diff_Bnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_gt : t = 0
⊢ |t| ≤ 3
Tactic:
simp only [t_gt, abs_zero, Nat.ofNat_nonneg]
Proof state after:
no goals
Theorem: Zeta_diff_Bnd
Proof state before:
case h.e'_4
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ C * |t|.log ^ 2 * (σ₂ - σ₁) = ?intro.intro.intro.intro.convert_6 * |σ₂ - σ₁|
Tactic:
congr
Proof state after:
case h.e'_4.e_a
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ σ₂ - σ₁ = |σ₂ - σ₁|
Theorem: Zeta_diff_Bnd
Proof state before:
case h.e'_4.e_a
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ σ₂ - σ₁ = |σ₂ - σ₁|
Tactic:
rw [_root_.abs_of_nonneg (by linarith)]
Proof state after:
no goals
Theorem: Zeta_diff_Bnd
Proof state before:
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ 0 ≤ σ₂ - σ₁
Tactic:
linarith
Proof state after:
no goals
Theorem: Zeta_diff_Bnd
Proof state before:
case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
⊢ ∀ x ∈ Ι σ₁ σ₂, ‖deriv ζ (↑x + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
intro σ hσ
Proof state after:
case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
σ : ℝ
hσ : σ ∈ Ι σ₁ σ₂
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Theorem: Zeta_diff_Bnd
Proof state before:
case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
σ : ℝ
hσ : σ ∈ Ι σ₁ σ₂
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
rw [uIoc_of_le σ₁_lt_σ₂.le, mem_Ioc] at hσ
Proof state after:
case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
σ : ℝ
hσ : σ₁ < σ ∧ σ ≤ σ₂
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Theorem: Zeta_diff_Bnd
Proof state before:
case intro.intro.intro.intro.convert_8
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
C : ℝ
Cpos : 0 < C
hC : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
σ₁ σ₂ t : ℝ
t_gt : 3 < |t|
σ₁_ge : 1 - A / |t|.log ≤ σ₁
σ₂_le : σ₂ ≤ 2
σ₁_lt_σ₂ : σ₁ < σ₂
t_ne_zero : t ≠ 0
σ : ℝ
hσ : σ₁ < σ ∧ σ ≤ σ₂
⊢ ‖deriv ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 2
Tactic:
exact hC σ t t_gt ⟨le_trans σ₁_ge hσ.1.le, le_trans hσ.2 σ₂_le⟩
Proof state after:
no goals
Theorem: ZetaInvBnd_aux'
Proof state before:
t : ℝ
logt_gt_one : 1 < |t|.log
⊢ |t|.log < |t|.log ^ 9
Tactic:
nth_rewrite 1 [← Real.rpow_one <| Real.log |t|]
Proof state after:
t : ℝ
logt_gt_one : 1 < |t|.log
⊢ |t|.log ^ 1 < |t|.log ^ 9
Theorem: ZetaInvBnd_aux'
Proof state before:
t : ℝ
logt_gt_one : 1 < |t|.log
⊢ |t|.log ^ 1 < |t|.log ^ 9
Tactic:
exact mod_cast Real.rpow_lt_rpow_left_iff (y := 1) (z := 9) logt_gt_one |>.mpr (by norm_num)
Proof state after:
no goals
Theorem: ZetaInvBnd_aux'
Proof state before:
t : ℝ
logt_gt_one : 1 < |t|.log
⊢ 1 < 9
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < (C₁ * A ^ (3 / 4) - C₂ * 2 * A)⁻¹
Tactic:
simp only [inv_pos, sub_pos]
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * A < C₁ * A ^ (3 / 4)
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * A < C₁ * A ^ (3 / 4)
Tactic:
apply div_lt_iff (by positivity) |>.mp
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * A / A ^ (3 / 4) < C₁
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * A / A ^ (3 / 4) < C₁
Tactic:
rw [div_eq_mul_inv, ← Real.rpow_neg (by positivity), mul_assoc]
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * (A * A ^ (-(3 / 4))) < C₁
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ C₂ * 2 * (A * A ^ (-(3 / 4))) < C₁
Tactic:
apply lt_div_iff' (by positivity) |>.mp
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A * A ^ (-(3 / 4)) < C₁ / (C₂ * 2)
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A * A ^ (-(3 / 4)) < C₁ / (C₂ * 2)
Tactic:
nth_rewrite 1 [← Real.rpow_one A]
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ 1 * A ^ (-(3 / 4)) < C₁ / (C₂ * 2)
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ 1 * A ^ (-(3 / 4)) < C₁ / (C₂ * 2)
Tactic:
rw [← Real.rpow_add (by positivity)]
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 + -(3 / 4)) < C₁ / (C₂ * 2)
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 + -(3 / 4)) < C₁ / (C₂ * 2)
Tactic:
norm_num
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 / 4) < C₁ / (C₂ * 2)
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 / 4) < C₁ / (C₂ * 2)
Tactic:
apply Real.rpow_lt_rpow_iff (z := 4) (by positivity) (by positivity) (by positivity) |>.mp
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ (A ^ (1 / 4)) ^ 4 < (C₁ / (C₂ * 2)) ^ 4
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ (A ^ (1 / 4)) ^ 4 < (C₁ / (C₂ * 2)) ^ 4
Tactic:
rw [← Real.rpow_mul (by positivity)]
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 / 4 * 4) < (C₁ / (C₂ * 2)) ^ 4
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 / 4 * 4) < (C₁ / (C₂ * 2)) ^ 4
Tactic:
norm_num
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A < (C₁ / (C₂ * 2)) ^ 4
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A < (C₁ / (C₂ * 2)) ^ 4
Tactic:
apply lt_of_le_of_lt hA
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4 < (C₁ / (C₂ * 2)) ^ 4
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4 < (C₁ / (C₂ * 2)) ^ 4
Tactic:
rw [div_mul_comm, mul_one]
Proof state after:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ (C₁ / (C₂ * 2)) ^ 4 / 2 < (C₁ / (C₂ * 2)) ^ 4
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ (C₁ / (C₂ * 2)) ^ 4 / 2 < (C₁ / (C₂ * 2)) ^ 4
Tactic:
apply half_lt_self
Proof state after:
case a
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < (C₁ / (C₂ * 2)) ^ 4
Theorem: ZetaInvBnd_aux2
Proof state before:
case a
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < (C₁ / (C₂ * 2)) ^ 4
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < A ^ (3 / 4)
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 ≤ A
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < C₂ * 2
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < A
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 ≤ A ^ (1 / 4)
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 ≤ C₁ / (C₂ * 2)
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaInvBnd_aux2
Proof state before:
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ 0 < 4
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaInvBnd
Proof state before:
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7
Tactic:
obtain ⟨C', C'pos, hC₁⟩ := ZetaInvBound2
Proof state after:
case intro.intro
C' : ℝ
C'pos : C' > 0
hC₁ : ∀ {σ : ℝ}, σ ∈ Ioc 1 2 → ∀ (t : ℝ), 3 < |t| → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C' * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C,
        ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Ico (1 - A / |t|.log ^ 9) 1 → 1 / ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log ^ 7