internlm/Lean-Github huggingface dataset:
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_5.h
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : -3 / 4 = -(3 / 4)
⊢ ‖((σ - 1) / c) ^ (-(3 / 4))‖ = ‖(σ - 1) ^ (-(3 / 4))‖ * ‖c ^ (3 / 4)‖ ∨ ‖C ^ (1 / 4)‖ = 0
Tactic:
left
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_5.h.h
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : -3 / 4 = -(3 / 4)
⊢ ‖((σ - 1) / c) ^ (-(3 / 4))‖ = ‖(σ - 1) ^ (-(3 / 4))‖ * ‖c ^ (3 / 4)‖
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_5.h.h
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : -3 / 4 = -(3 / 4)
⊢ ‖((σ - 1) / c) ^ (-(3 / 4))‖ = ‖(σ - 1) ^ (-(3 / 4))‖ * ‖c ^ (3 / 4)‖
Tactic:
conv => lhs; rw [Real.div_rpow (by linarith) hc.le, Real.rpow_neg hc.le, div_inv_eq_mul, norm_mul]
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ -3 / 4 = -(3 / 4)
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : -3 / 4 = -(3 / 4)
⊢ 0 ≤ σ - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_6
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ ‖(σ - 1) ^ (-3 / 4) * c ^ (3 / 4) * (C ^ (1 / 4) * (|t| ^ 2).log ^ (1 / 4))‖ =
    ‖(σ - 1) ^ (-3 / 4) * c ^ (3 / 4) * ((2 * C) ^ (1 / 4) * |t|.log ^ (1 / 4))‖
Tactic:
simp only [Real.log_pow, Nat.cast_ofNat, norm_mul, Real.norm_eq_abs]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_6
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ |(σ - 1) ^ (-3 / 4)| * |c ^ (3 / 4)| * (|C ^ (1 / 4)| * |(2 * |t|.log) ^ (1 / 4)|) =
    |(σ - 1) ^ (-3 / 4)| * |c ^ (3 / 4)| * (|(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|)
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_6
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ |(σ - 1) ^ (-3 / 4)| * |c ^ (3 / 4)| * (|C ^ (1 / 4)| * |(2 * |t|.log) ^ (1 / 4)|) =
    |(σ - 1) ^ (-3 / 4)| * |c ^ (3 / 4)| * (|(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|)
Tactic:
congr! 1
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_6.h.e'_6
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ |C ^ (1 / 4)| * |(2 * |t|.log) ^ (1 / 4)| = |(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_6.h.e'_6
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ |C ^ (1 / 4)| * |(2 * |t|.log) ^ (1 / 4)| = |(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|
Tactic:
rw [Real.mul_rpow (by norm_num) hC.le, Real.mul_rpow (by norm_num) <|
    Real.log_nonneg (by linarith), abs_mul, abs_mul, ← mul_assoc, mul_comm _ |2 ^ (1 / 4)|]
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_7
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ ‖(σ - 1) ^ (-3 / 4) * c ^ (3 / 4) * ((2 * C) ^ (1 / 4) * |t|.log ^ (1 / 4))‖ =
    (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
simp only [norm_mul, Real.norm_eq_abs]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_7
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ |(σ - 1) ^ (-3 / 4)| * |c ^ (3 / 4)| * (|(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|) =
    (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_7
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ |(σ - 1) ^ (-3 / 4)| * |c ^ (3 / 4)| * (|(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|) =
    (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
have : (2 * C) ^ ((1 : ℝ)/ 4) * c ^ ((3 : ℝ)/ 4) =
  |(2 * C) ^ ((1 : ℝ)/ 4) * c ^ ((3 : ℝ)/ 4)| := by
  rw [abs_eq_self.mpr (by apply mul_nonneg <;> (apply Real.rpow_nonneg; linarith))]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_7
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ |(σ - 1) ^ (-3 / 4)| * |c ^ (3 / 4)| * (|(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|) =
    (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_7
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ |(σ - 1) ^ (-3 / 4)| * |c ^ (3 / 4)| * (|(2 * C) ^ (1 / 4)| * ||t|.log ^ (1 / 4)|) =
    (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
rw [this, abs_mul, abs_eq_self.mpr (by apply Real.rpow_nonneg; linarith), abs_eq_self.mpr (by positivity),
  abs_eq_self.mpr (by positivity), abs_eq_self.mpr (by apply Real.rpow_nonneg (Real.log_nonneg (by linarith)))]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.calc_7
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ (σ - 1) ^ (-3 / 4) * c ^ (3 / 4) * ((2 * C) ^ (1 / 4) * |t|.log ^ (1 / 4)) =
    (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Theorem: ZetaInvBound2
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.calc_7
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ (σ - 1) ^ (-3 / 4) * c ^ (3 / 4) * ((2 * C) ^ (1 / 4) * |t|.log ^ (1 / 4)) =
    (2 * C) ^ (1 / 4) * c ^ (3 / 4) * (σ - 1) ^ (-3 / 4) * |t|.log ^ (1 / 4)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
Tactic:
rw [abs_eq_self.mpr (by apply mul_nonneg <;> (apply Real.rpow_nonneg; linarith))]
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ 0 ≤ (2 * C) ^ (1 / 4) * c ^ (3 / 4)
Tactic:
apply mul_nonneg <;> (apply Real.rpow_nonneg; linarith)
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
case hb
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ 0 ≤ c ^ (3 / 4)
Tactic:
apply Real.rpow_nonneg
Proof state after:
case hb.hx
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ 0 ≤ c
Theorem: ZetaInvBound2
Proof state before:
case hb.hx
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
⊢ 0 ≤ c
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ (σ - 1) ^ (-3 / 4)
Tactic:
apply Real.rpow_nonneg
Proof state after:
case hx
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ σ - 1
Theorem: ZetaInvBound2
Proof state before:
case hx
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ σ - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ c ^ (3 / 4)
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ (2 * C) ^ (1 / 4)
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 0 ≤ |t|.log ^ (1 / 4)
Tactic:
apply Real.rpow_nonneg (Real.log_nonneg (by linarith))
Proof state after:
no goals
Theorem: ZetaInvBound2
Proof state before:
A : ℝ
ha : A ∈ Ioc 0 (1 / 2)
C : ℝ
hC : 0 < C
h : ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
c : ℝ
hc : 0 < c
h_inv : ∀ σ ∈ Ioc 1 2, ‖ζ ↑σ‖ ≤ c / (σ - 1)
σ t : ℝ
t_gt : 3 < |t|
σ_gt : 1 < σ
σ_le : σ ≤ 2
ht' : 3 < |2 * t|
hnezero : ((σ - 1) / c) ^ (-3 / 4) ≠ 0
this : (2 * C) ^ (1 / 4) * c ^ (3 / 4) = |(2 * C) ^ (1 / 4) * c ^ (3 / 4)|
⊢ 1 ≤ |t|
Tactic:
linarith
Proof state after:
no goals
Theorem: deriv_fun_re
Proof state before:
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
⊢ (deriv fun {σ₂} => f (↑σ₂ + ↑t * I)) = fun σ => deriv f (↑σ + ↑t * I)
Tactic:
ext σ
Proof state after:
case h
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)
Theorem: deriv_fun_re
Proof state before:
case h
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)
Tactic:
have := deriv.comp (h := fun (σ : ℝ) ↦ σ + t * I) (h₂ := f) σ (diff σ) ?_
Proof state after:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f ((fun σ => ↑σ + ↑t * I) σ) * deriv (fun σ => ↑σ + ↑t * I) σ
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)

case h.refine_1
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
⊢ DifferentiableAt ℝ (fun σ => ↑σ + ↑t * I) σ
Theorem: deriv_fun_re
Proof state before:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f ((fun σ => ↑σ + ↑t * I) σ) * deriv (fun σ => ↑σ + ↑t * I) σ
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)
Tactic:
simp only [deriv_add_const', _root_.deriv_ofReal, mul_one] at this
Proof state after:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f (↑σ + ↑t * I)
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)
Theorem: deriv_fun_re
Proof state before:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f (↑σ + ↑t * I)
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv f (↑σ + ↑t * I)
Tactic:
rw [← this]
Proof state after:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f (↑σ + ↑t * I)
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv (f ∘ fun σ => ↑σ + ↑t * I) σ
Theorem: deriv_fun_re
Proof state before:
case h.refine_2
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
this : deriv (f ∘ fun σ => ↑σ + ↑t * I) σ = deriv f (↑σ + ↑t * I)
⊢ deriv (fun {σ₂} => f (↑σ₂ + ↑t * I)) σ = deriv (f ∘ fun σ => ↑σ + ↑t * I) σ
Tactic:
rfl
Proof state after:
no goals
Theorem: deriv_fun_re
Proof state before:
case h.refine_1
t : ℝ
f : ℂ → ℂ
diff : ∀ (σ : ℝ), DifferentiableAt ℂ f (↑σ + ↑t * I)
σ : ℝ
⊢ DifferentiableAt ℝ (fun σ => ↑σ + ↑t * I) σ
Tactic:
apply DifferentiableAt.add_const <| differentiableAt_ofReal σ
Proof state after:
no goals
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
⊢ ∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I) = ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)
Tactic:
have diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (σ + t * I) := by
  intro σ
  refine differentiableAt_riemannZeta ?_
  contrapose! t_ne_zero; apply And.right; simpa [Complex.ext_iff] using t_ne_zero
Proof state after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I) = ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∫ (σ : ℝ) in σ₁..σ₂, deriv ζ (↑σ + ↑t * I) = ζ (↑σ₂ + ↑t * I) - ζ (↑σ₁ + ↑t * I)
Tactic:
apply intervalIntegral.integral_deriv_eq_sub'
Proof state after:
case hderiv
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ (deriv fun {σ₂} => ζ (↑σ₂ + ↑t * I)) = fun y => deriv ζ (↑y + ↑t * I)

case hdiff
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∀ x ∈ [[σ₁, σ₂]], DifferentiableAt ℝ (fun {σ₂} => ζ (↑σ₂ + ↑t * I)) x

case hcont
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (fun y => deriv ζ (↑y + ↑t * I)) [[σ₁, σ₂]]
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
⊢ ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
Tactic:
intro σ
Proof state after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
σ : ℝ
⊢ DifferentiableAt ℂ ζ (↑σ + ↑t * I)
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
σ : ℝ
⊢ DifferentiableAt ℂ ζ (↑σ + ↑t * I)
Tactic:
refine differentiableAt_riemannZeta ?_
Proof state after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
σ : ℝ
⊢ ↑σ + ↑t * I ≠ 1
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
σ : ℝ
⊢ ↑σ + ↑t * I ≠ 1
Tactic:
contrapose! t_ne_zero
Proof state after:
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ t = 0
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ t = 0
Tactic:
apply And.right
Proof state after:
case self
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ ?a ∧ t = 0

case a
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ Prop
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case self
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ ?a ∧ t = 0

case a
σ₁ σ₂ t σ : ℝ
t_ne_zero : ↑σ + ↑t * I = 1
⊢ Prop
Tactic:
simpa [Complex.ext_iff] using t_ne_zero
Proof state after:
no goals
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case hderiv
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ (deriv fun {σ₂} => ζ (↑σ₂ + ↑t * I)) = fun y => deriv ζ (↑y + ↑t * I)
Tactic:
exact deriv_fun_re diff
Proof state after:
no goals
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case hdiff
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∀ x ∈ [[σ₁, σ₂]], DifferentiableAt ℝ (fun {σ₂} => ζ (↑σ₂ + ↑t * I)) x
Tactic:
intro s _
Proof state after:
case hdiff
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ (fun {σ₂} => ζ (↑σ₂ + ↑t * I)) s
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case hdiff
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ (fun {σ₂} => ζ (↑σ₂ + ↑t * I)) s
Tactic:
apply DifferentiableAt.comp
Proof state after:
case hdiff.hg
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ ζ (↑s + ↑t * I)

case hdiff.hf
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ (fun σ₂ => ↑σ₂ + ↑t * I) s
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case hdiff.hg
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ ζ (↑s + ↑t * I)
Tactic:
exact (diff s).restrictScalars ℝ
Proof state after:
no goals
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case hdiff.hf
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
s : ℝ
a✝ : s ∈ [[σ₁, σ₂]]
⊢ DifferentiableAt ℝ (fun σ₂ => ↑σ₂ + ↑t * I) s
Tactic:
exact DifferentiableAt.add_const (c := t * I) <| differentiableAt_ofReal _
Proof state after:
no goals
Theorem: Zeta_eq_int_derivZeta
Proof state before:
case hcont
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (fun y => deriv ζ (↑y + ↑t * I)) [[σ₁, σ₂]]
Tactic:
apply ContinuousOn.comp (g := deriv ζ) ?_ ?_ (mapsTo_image _ _)
Proof state after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (deriv ζ) ((fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]])

σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (fun y => ↑y + ↑t * I) [[σ₁, σ₂]]
Theorem: Zeta_eq_int_derivZeta
Proof state before:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (deriv ζ) ((fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]])
Tactic:
apply HasDerivAt.continuousOn (f' := deriv <| deriv ζ)
Proof state after:
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ∀ x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]], HasDerivAt (deriv ζ) (deriv (deriv ζ) x) x