internlm/Lean-Github huggingface dataset:
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_3
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ + 2 * |t| * ↑N ^ (-σ) / σ =
    A.exp * 2 * |t|.log + ↑N ^ (1 - σ) / ‖1 - s‖ + ↑N ^ (-σ) / 2 + 2 * |t| * ↑N ^ (-σ) / σ
Tactic:
simp only [norm_div, norm_neg, norm_eq_abs, RCLike.norm_ofNat, Nat.abs_cast, s]
Proof state after:
case intro.intro.intro.intro.intro.calc_3
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + Complex.abs (↑N ^ (1 - (↑σ + ↑t * I))) / Complex.abs (1 - (↑σ + ↑t * I)) +
        Complex.abs (↑N ^ (-(↑σ + ↑t * I))) / 2 +
      2 * |t| * ↑N ^ (-σ) / σ =
    A.exp * 2 * |t|.log + ↑N ^ (1 - σ) / Complex.abs (1 - (↑σ + ↑t * I)) + ↑N ^ (-σ) / 2 + 2 * |t| * ↑N ^ (-σ) / σ
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_3
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + Complex.abs (↑N ^ (1 - (↑σ + ↑t * I))) / Complex.abs (1 - (↑σ + ↑t * I)) +
        Complex.abs (↑N ^ (-(↑σ + ↑t * I))) / 2 +
      2 * |t| * ↑N ^ (-σ) / σ =
    A.exp * 2 * |t|.log + ↑N ^ (1 - σ) / Complex.abs (1 - (↑σ + ↑t * I)) + ↑N ^ (-σ) / 2 + 2 * |t| * ↑N ^ (-σ) / σ
Tactic:
congr <;> (convert norm_natCast_cpow_of_pos Npos _; simp)
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_3.e_a.e_a.e_a
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ Complex.abs (↑N ^ (-(↑σ + ↑t * I))) = ↑N ^ (-σ)
Tactic:
convert norm_natCast_cpow_of_pos Npos _
Proof state after:
case h.e'_3.h.e'_6
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ -σ = (-(↑σ + ↑t * I)).re
Theorem: ZetaUpperBnd'
Proof state before:
case h.e'_3.h.e'_6
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ -σ = (-(↑σ + ↑t * I)).re
Tactic:
simp
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_4
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + ↑N ^ (1 - σ) / ‖1 - s‖ + ↑N ^ (-σ) / 2 + 2 * |t| * ↑N ^ (-σ) / σ ≤
    A.exp * 2 * |t|.log + |t| ^ (1 - σ) * 2 + |t| ^ (1 - σ) + 2 * |t| * (8 * |t| ^ (-σ))
Tactic:
have ⟨h₁, h₂, h₃⟩ := UpperBnd_aux6 t_gt ⟨σ_gt, hσ.2⟩ neOne Npos N_le_t
Proof state after:
case intro.intro.intro.intro.intro.calc_4
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
h₁ : ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2
h₂ : ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)
h₃ : ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
⊢ A.exp * 2 * |t|.log + ↑N ^ (1 - σ) / ‖1 - s‖ + ↑N ^ (-σ) / 2 + 2 * |t| * ↑N ^ (-σ) / σ ≤
    A.exp * 2 * |t|.log + |t| ^ (1 - σ) * 2 + |t| ^ (1 - σ) + 2 * |t| * (8 * |t| ^ (-σ))
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_4
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
h₁ : ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2
h₂ : ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)
h₃ : ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
⊢ A.exp * 2 * |t|.log + ↑N ^ (1 - σ) / ‖1 - s‖ + ↑N ^ (-σ) / 2 + 2 * |t| * ↑N ^ (-σ) / σ ≤
    A.exp * 2 * |t|.log + |t| ^ (1 - σ) * 2 + |t| ^ (1 - σ) + 2 * |t| * (8 * |t| ^ (-σ))
Tactic:
refine add_le_add_le_add_le_add le_rfl h₁ h₂ ?_
Proof state after:
case intro.intro.intro.intro.intro.calc_4
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
h₁ : ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2
h₂ : ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)
h₃ : ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
⊢ 2 * |t| * ↑N ^ (-σ) / σ ≤ 2 * |t| * (8 * |t| ^ (-σ))
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_4
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
h₁ : ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2
h₂ : ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)
h₃ : ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
⊢ 2 * |t| * ↑N ^ (-σ) / σ ≤ 2 * |t| * (8 * |t| ^ (-σ))
Tactic:
rw [mul_div_assoc]
Proof state after:
case intro.intro.intro.intro.intro.calc_4
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
h₁ : ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2
h₂ : ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)
h₃ : ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
⊢ 2 * |t| * (↑N ^ (-σ) / σ) ≤ 2 * |t| * (8 * |t| ^ (-σ))
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_4
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
h₁ : ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2
h₂ : ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)
h₃ : ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
⊢ 2 * |t| * (↑N ^ (-σ) / σ) ≤ 2 * |t| * (8 * |t| ^ (-σ))
Tactic:
exact mul_le_mul_left (mul_pos (by norm_num) (by positivity)) |>.mpr h₃
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
h₁ : ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2
h₂ : ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)
h₃ : ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
h₁ : ↑⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (↑σ + ↑t * I)‖ ≤ |t| ^ (1 - σ) * 2
h₂ : ↑⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ)
h₃ : ↑⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ)
⊢ 0 < |t|
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_5
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + |t| ^ (1 - σ) * 2 + |t| ^ (1 - σ) + 2 * |t| * (8 * |t| ^ (-σ)) =
    A.exp * 2 * |t|.log + (3 + 8 * 2) * |t| ^ (1 - σ)
Tactic:
ring_nf
Proof state after:
case intro.intro.intro.intro.intro.calc_5
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 3 + |t| * |t| ^ (-σ) * 16 = A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 19
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_5
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 3 + |t| * |t| ^ (-σ) * 16 = A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 19
Tactic:
conv => lhs; rhs; lhs; rw [mul_comm |t|]
Proof state after:
case intro.intro.intro.intro.intro.calc_5
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 3 + |t| ^ (-σ) * |t| * 16 = A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 19
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_5
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 3 + |t| ^ (-σ) * |t| * 16 = A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 19
Tactic:
rw [← Real.rpow_add_one (by positivity)]
Proof state after:
case intro.intro.intro.intro.intro.calc_5
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 3 + |t| ^ (-σ + 1) * 16 = A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 19
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_5
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 3 + |t| ^ (-σ + 1) * 16 = A.exp * |t|.log * 2 + |t| ^ (1 - σ) * 19
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ |t| ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_6
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + (3 + 8 * 2) * |t| ^ (1 - σ) ≤ A.exp * 2 * |t|.log + (3 + 8 * 2) * A.exp * 1
Tactic:
simp only [Real.log_abs, add_le_add_iff_left, mul_one]
Proof state after:
case intro.intro.intro.intro.intro.calc_6
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ (3 + 8 * 2) * |t| ^ (1 - σ) ≤ (3 + 8 * 2) * A.exp
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_6
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ (3 + 8 * 2) * |t| ^ (1 - σ) ≤ (3 + 8 * 2) * A.exp
Tactic:
exact mul_le_mul_left (by positivity) |>.mpr <| UpperBnd_aux2 t_gt hσ.1
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ 0 < 3 + 8 * 2
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_7
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ A.exp * 2 * |t|.log + (3 + 8 * 2) * A.exp * 1 ≤ A.exp * 2 * |t|.log + (3 + 8 * 2) * A.exp * |t|.log
Tactic:
simp only [add_le_add_iff_left]
Proof state after:
case intro.intro.intro.intro.intro.calc_7
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ (3 + 8 * 2) * A.exp * 1 ≤ (3 + 8 * 2) * A.exp * |t|.log
Theorem: ZetaUpperBnd'
Proof state before:
case intro.intro.intro.intro.intro.calc_7
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ (3 + 8 * 2) * A.exp * 1 ≤ (3 + 8 * 2) * A.exp * |t|.log
Tactic:
apply mul_le_mul_left (by norm_num [Real.exp_pos]) |>.mpr <| logt_gt.le
Proof state after:
no goals
Theorem: ZetaUpperBnd'
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
hσ : σ ∈ Icc (1 - A / |t|.log) 2
C : ℝ := A.exp * (5 + 8 * 2)
N : ℕ := ⌊|t|⌋₊
s : ℂ := ↑σ + ↑t * I
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
logt_gt : 1 < |t|.log
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
σ_gt : 1 / 2 < σ
⊢ 0 < (3 + 8 * 2) * A.exp
Tactic:
norm_num [Real.exp_pos]
Proof state after:
no goals
Theorem: ZetaUpperBnd
Proof state before:
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Tactic:
let A := (1 / 2 : ℝ)
Proof state after:
A : ℝ := 1 / 2
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Tactic:
let C := Real.exp A * (5 + 8 * 2)
Proof state after:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
⊢ ∃ A,
    ∃ (_ : A ∈ Ioc 0 (1 / 2)),
      ∃ C, ∃ (_ : 0 < C), ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Tactic:
refine ⟨A, ⟨by norm_num, by norm_num⟩ , C, (by positivity), ?_⟩
Proof state after:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
⊢ ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
⊢ ∀ (σ t : ℝ), 3 < |t| → σ ∈ Icc (1 - A / |t|.log) 2 → ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Tactic:
intro σ t t_gt ⟨σ_ge, σ_le⟩
Proof state after:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
⊢ ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
⊢ ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Tactic:
obtain ⟨Npos, _, _, _, σPos, neOne⟩ := UpperBnd_aux ⟨by norm_num, by norm_num⟩ t_gt σ_ge
Proof state after:
case intro.intro.intro.intro.intro
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Theorem: ZetaUpperBnd
Proof state before:
case intro.intro.intro.intro.intro
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖ζ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Tactic:
rw [← Zeta0EqZeta Npos (by simp [σPos]) neOne]
Proof state after:
case intro.intro.intro.intro.intro
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖ζ₀ ⌊|t|⌋₊ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Theorem: ZetaUpperBnd
Proof state before:
case intro.intro.intro.intro.intro
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖ζ₀ ⌊|t|⌋₊ (↑σ + ↑t * I)‖ ≤ C * |t|.log
Tactic:
apply le_trans (by apply norm_add₄_le) ?_
Proof state after:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|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)‖ ≤
    C * |t|.log
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|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)‖ ≤
    C * |t|.log
Tactic:
convert ZetaUpperBnd' ⟨by norm_num, le_rfl⟩ t_gt ⟨σ_ge, σ_le⟩ using 1
Proof state after:
case h.e'_3
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|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)‖ =
    ‖∑ 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)‖
Theorem: ZetaUpperBnd
Proof state before:
case h.e'_3
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|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)‖ =
    ‖∑ 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:
simp
Proof state after:
no goals
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
⊢ 0 < A
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
⊢ A ≤ 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
⊢ 0 < C
Tactic:
positivity
Proof state after:
no goals
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
⊢ 0 < A
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
⊢ A ≤ 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 < (↑σ + ↑t * I).re
Tactic:
simp [σPos]
Proof state after:
no goals
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ ‖ζ₀ ⌊|t|⌋₊ (↑σ + ↑t * I)‖ ≤ ?m.863712
Tactic:
apply norm_add₄_le
Proof state after:
no goals
Theorem: ZetaUpperBnd
Proof state before:
A : ℝ := 1 / 2
C : ℝ := A.exp * (5 + 8 * 2)
σ t : ℝ
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
σ_le : σ ≤ 2
Npos : 0 < ⌊|t|⌋₊
left✝² : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
neOne : ↑σ + ↑t * I ≠ 1
⊢ 0 < 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: NormDerivZeta0Le
Proof state before:
N : ℕ
Npos : 0 < N
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ t : ℝ
σ_ge : 1 - A / |t|.log ≤ σ
σpos : 0 < σ
t_gt : 3 < |t|
⊢ let s := ↑σ + ↑t * I;
  ‖deriv (ζ₀ N) s‖ ≤
    4 * (↑N).log *
      (‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
        ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖)
Tactic:
set s := σ + t * I
Proof state after:
N : ℕ
Npos : 0 < N
A : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ t : ℝ
σ_ge : 1 - A / |t|.log ≤ σ
σpos : 0 < σ
t_gt : 3 < |t|
s : ℂ := ↑σ + ↑t * I
⊢ let s := s;
  ‖deriv (ζ₀ N) s‖ ≤
    4 * (↑N).log *
      (‖∑ n ∈ Finset.range (N + 1), 1 / ↑n ^ s‖ + ‖↑N ^ (1 - s) / (1 - s)‖ + ‖↑N ^ (-s) / 2‖ +
        ‖s * ∫ (x : ℝ) in Ioi ↑N, (↑⌊x⌋ + 1 / 2 - ↑x) / ↑x ^ (s + 1)‖)