internlm/Lean-Github huggingface dataset:
Theorem: ZetaBnd_aux2
Proof state before:
case neg.calc_3
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ |t|.log⁻¹ * (↑n).log * A ≤ 1 * A
Tactic:
gcongr
Proof state after:
case neg.calc_3.h
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ |t|.log⁻¹ * (↑n).log ≤ 1
Theorem: ZetaBnd_aux2
Proof state before:
case neg.calc_3.h
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
⊢ |t|.log⁻¹ * (↑n).log ≤ 1
Tactic:
by_cases ht1 : |t| = 1
Proof state after:
case pos
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : |t| = 1
⊢ |t|.log⁻¹ * (↑n).log ≤ 1

case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ |t|.log⁻¹ * (↑n).log ≤ 1
Theorem: ZetaBnd_aux2
Proof state before:
case pos
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : |t| = 1
⊢ |t|.log⁻¹ * (↑n).log ≤ 1

case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ |t|.log⁻¹ * (↑n).log ≤ 1
Tactic:
simp [ht1]
Proof state after:
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ |t|.log⁻¹ * (↑n).log ≤ 1
Theorem: ZetaBnd_aux2
Proof state before:
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ |t|.log⁻¹ * (↑n).log ≤ 1
Tactic:
apply (inv_mul_le_iff ?_).mpr
Proof state after:
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ (↑n).log ≤ |t|.log * 1

n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ 0 < |t|.log
Theorem: ZetaBnd_aux2
Proof state before:
case neg
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ (↑n).log ≤ |t|.log * 1

n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ 0 < |t|.log
Tactic:
convert Real.log_le_log n_gt_0' n_le_t using 1
Proof state after:
case h.e'_4
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ |t|.log * 1 = |t|.log

n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ 0 < |t|.log
Theorem: ZetaBnd_aux2
Proof state before:
case h.e'_4
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ |t|.log * 1 = |t|.log

n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ 0 < |t|.log
Tactic:
rw [mul_one]
Proof state after:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ 0 < |t|.log
Theorem: ZetaBnd_aux2
Proof state before:
n : ℕ
t A σ : ℝ
Apos : 0 < A
σpos : 0 < σ
n_le_t : ↑n ≤ |t|
σ_ge : 1 - A / |t|.log ≤ σ
s : ℂ := ↑σ + ↑t * I
n0 : ¬n = 0
n_gt_0 : 0 < n
n_gt_0' : 0 < ↑n
n_ge_1 : 1 ≤ ↑n
ht1 : ¬|t| = 1
⊢ 0 < |t|.log
Tactic:
exact Real.log_pos <| lt_of_le_of_ne (le_trans n_ge_1 n_le_t) <| fun t ↦ ht1 (t.symm)
Proof state after:
no goals
Theorem: logt_gt_one
Proof state before:
t : ℝ
t_ge : 3 < |t|
⊢ 1 < |t|.log
Tactic:
rw [← Real.log_exp (x := 1)]
Proof state after:
t : ℝ
t_ge : 3 < |t|
⊢ (Real.exp 1).log < |t|.log
Theorem: logt_gt_one
Proof state before:
t : ℝ
t_ge : 3 < |t|
⊢ (Real.exp 1).log < |t|.log
Tactic:
apply Real.log_lt_log (Real.exp_pos _)
Proof state after:
t : ℝ
t_ge : 3 < |t|
⊢ Real.exp 1 < |t|
Theorem: logt_gt_one
Proof state before:
t : ℝ
t_ge : 3 < |t|
⊢ Real.exp 1 < |t|
Tactic:
linarith [(by exact lt_trans Real.exp_one_lt_d9 (by norm_num) : Real.exp 1 < 3)]
Proof state after:
no goals
Theorem: logt_gt_one
Proof state before:
t : ℝ
t_ge : 3 < |t|
⊢ Real.exp 1 < 3
Tactic:
exact lt_trans Real.exp_one_lt_d9 (by norm_num)
Proof state after:
no goals
Theorem: logt_gt_one
Proof state before:
t : ℝ
t_ge : 3 < |t|
⊢ 2.7182818286 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
⊢ let N := ⌊|t|⌋₊;
  0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
intro N
Proof state after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
have Npos : 0 < N := Nat.floor_pos.mpr (by linarith)
Proof state after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
have N_le_t : N ≤ |t| := Nat.floor_le <| abs_nonneg _
Proof state after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
have logt_gt := logt_gt_one t_gt
Proof state after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
have σ_gt : 1 - A < σ := by
  apply lt_of_lt_of_le ((sub_lt_sub_iff_left (a := 1)).mpr ?_) σ_ge
  exact (div_lt_iff (by linarith)).mpr <| lt_mul_right hA.1 logt_gt
Proof state after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ 0 < N ∧ ↑N ≤ |t| ∧ 1 < |t|.log ∧ 1 - A < σ ∧ 0 < σ ∧ ↑σ + ↑t * I ≠ 1
Tactic:
refine ⟨Npos, N_le_t, logt_gt, σ_gt, by linarith [hA.2], ?_⟩
Proof state after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ ↑σ + ↑t * I ≠ 1
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ ↑σ + ↑t * I ≠ 1
Tactic:
contrapose! t_gt
Proof state after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
t_gt : ↑σ + ↑t * I = 1
⊢ |t| ≤ 3
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
t_gt : ↑σ + ↑t * I = 1
⊢ |t| ≤ 3
Tactic:
simp only [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] at t_gt
Proof state after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
t_gt : σ = 1 ∧ t = 0
⊢ |t| ≤ 3
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
t_gt : σ = 1 ∧ t = 0
⊢ |t| ≤ 3
Tactic:
norm_num [t_gt.2]
Proof state after:
no goals
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
⊢ 1 ≤ |t|
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ 1 - A < σ
Tactic:
apply lt_of_lt_of_le ((sub_lt_sub_iff_left (a := 1)).mpr ?_) σ_ge
Proof state after:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ A / |t|.log < A
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ A / |t|.log < A
Tactic:
exact (div_lt_iff (by linarith)).mpr <| lt_mul_right hA.1 logt_gt
Proof state after:
no goals
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
⊢ 0 < |t|.log
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperBnd_aux
Proof state before:
A σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
t_gt : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
logt_gt : 1 < |t|.log
σ_gt : 1 - A < σ
⊢ 0 < σ
Tactic:
linarith [hA.2]
Proof state after:
no goals
Theorem: UpperBnd_aux2
Proof state before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
⊢ |t| ^ (1 - σ) ≤ A.exp
Tactic:
have : |t| ^ (1 - σ) ≤ |t| ^ (A / Real.log |t|) :=
  Real.rpow_le_rpow_of_exponent_le (by linarith) (by linarith)
Proof state after:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ^ (1 - σ) ≤ A.exp
Theorem: UpperBnd_aux2
Proof state before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ^ (1 - σ) ≤ A.exp
Tactic:
apply le_trans this ?_
Proof state after:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ^ (A / |t|.log) ≤ A.exp
Theorem: UpperBnd_aux2
Proof state before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ^ (A / |t|.log) ≤ A.exp
Tactic:
conv => lhs; lhs; rw [← Real.exp_log (by linarith : 0 < |t|)]
Proof state after:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t|.log.exp ^ (A / |t|.log) ≤ A.exp
Theorem: UpperBnd_aux2
Proof state before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t|.log.exp ^ (A / |t|.log) ≤ A.exp
Tactic:
rw [div_eq_mul_inv, Real.rpow_mul (by positivity), ← Real.exp_mul, ← Real.exp_mul, mul_comm,
  ← mul_assoc, inv_mul_cancel, one_mul]
Proof state after:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t|.log ≠ 0
Theorem: UpperBnd_aux2
Proof state before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t|.log ≠ 0
Tactic:
apply Real.log_ne_zero.mpr
Proof state after:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ≠ 0 ∧ |t| ≠ 1 ∧ |t| ≠ -1
Theorem: UpperBnd_aux2
Proof state before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ |t| ≠ 0 ∧ |t| ≠ 1 ∧ |t| ≠ -1
Tactic:
split_ands <;> linarith
Proof state after:
no goals
Theorem: UpperBnd_aux2
Proof state before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
⊢ 1 ≤ |t|
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperBnd_aux2
Proof state before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
⊢ 1 - σ ≤ A / |t|.log
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperBnd_aux2
Proof state before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ 0 < |t|
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperBnd_aux2
Proof state before:
A σ t : ℝ
t_ge : 3 < |t|
σ_ge : 1 - A / |t|.log ≤ σ
this : |t| ^ (1 - σ) ≤ |t| ^ (A / |t|.log)
⊢ 0 ≤ |t|.log.exp
Tactic:
positivity
Proof state after:
no goals
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
⊢ ∑ x ∈ Finset.Ico 0 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Tactic:
have : Finset.Ico 1 N ⊆ Finset.Ico 0 N := by
  intro x hx
  simp only [Finset.mem_Ico, Nat.Ico_zero_eq_range, Finset.mem_range] at hx ⊢
  exact hx.2
Proof state after:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ ∑ x ∈ Finset.Ico 0 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ ∑ x ∈ Finset.Ico 0 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Tactic:
rw [← Finset.sum_sdiff (s₁ := Finset.Ico 1 N) (s₂ := Finset.Ico 0 N) this]
Proof state after:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ ∑ x ∈ Finset.Ico 0 N \ Finset.Ico 1 N, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ ∑ x ∈ Finset.Ico 0 N \ Finset.Ico 1 N, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Tactic:
have : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1 := by
  ext a
  simp only [Nat.Ico_zero_eq_range, Finset.mem_sdiff, Finset.mem_range, Finset.mem_Ico, not_and,
    not_lt, Finset.range_one, Finset.mem_singleton]
  exact ⟨fun _ ↦ by omega, fun ha ↦ ⟨by simp [ha, Npos], by omega⟩⟩
Proof state after:
N : ℕ
Npos : 0 < N
this✝ : Finset.Ico 1 N ⊆ Finset.Ico 0 N
this : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
⊢ ∑ x ∈ Finset.Ico 0 N \ Finset.Ico 1 N, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
this✝ : Finset.Ico 1 N ⊆ Finset.Ico 0 N
this : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
⊢ ∑ x ∈ Finset.Ico 0 N \ Finset.Ico 1 N, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Tactic:
rw [this]
Proof state after:
N : ℕ
Npos : 0 < N
this✝ : Finset.Ico 1 N ⊆ Finset.Ico 0 N
this : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
⊢ ∑ x ∈ Finset.range 1, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
this✝ : Finset.Ico 1 N ⊆ Finset.Ico 0 N
this : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
⊢ ∑ x ∈ Finset.range 1, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
Tactic:
simp
Proof state after:
no goals
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
⊢ Finset.Ico 1 N ⊆ Finset.Ico 0 N
Tactic:
intro x hx
Proof state after:
N : ℕ
Npos : 0 < N
x : ℕ
hx : x ∈ Finset.Ico 1 N
⊢ x ∈ Finset.Ico 0 N
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
x : ℕ
hx : x ∈ Finset.Ico 1 N
⊢ x ∈ Finset.Ico 0 N
Tactic:
simp only [Finset.mem_Ico, Nat.Ico_zero_eq_range, Finset.mem_range] at hx ⊢
Proof state after:
N : ℕ
Npos : 0 < N
x : ℕ
hx : 1 ≤ x ∧ x < N
⊢ x < N
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
x : ℕ
hx : 1 ≤ x ∧ x < N
⊢ x < N
Tactic:
exact hx.2
Proof state after:
no goals
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
Tactic:
ext a
Proof state after:
case a
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
⊢ a ∈ Finset.Ico 0 N \ Finset.Ico 1 N ↔ a ∈ Finset.range 1
Theorem: riemannZeta0_zero_aux
Proof state before:
case a
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
⊢ a ∈ Finset.Ico 0 N \ Finset.Ico 1 N ↔ a ∈ Finset.range 1
Tactic:
simp only [Nat.Ico_zero_eq_range, Finset.mem_sdiff, Finset.mem_range, Finset.mem_Ico, not_and,
  not_lt, Finset.range_one, Finset.mem_singleton]
Proof state after:
case a
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
⊢ a < N ∧ (1 ≤ a → N ≤ a) ↔ a = 0
Theorem: riemannZeta0_zero_aux
Proof state before:
case a
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
⊢ a < N ∧ (1 ≤ a → N ≤ a) ↔ a = 0
Tactic:
exact ⟨fun _ ↦ by omega, fun ha ↦ ⟨by simp [ha, Npos], by omega⟩⟩
Proof state after:
no goals
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
x✝ : a < N ∧ (1 ≤ a → N ≤ a)
⊢ a = 0
Tactic:
omega
Proof state after:
no goals
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
ha : a = 0
⊢ a < N
Tactic:
simp [ha, Npos]
Proof state after:
no goals
Theorem: riemannZeta0_zero_aux
Proof state before:
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
a : ℕ
ha : a = 0
⊢ 1 ≤ a → N ≤ a
Tactic:
omega
Proof state after:
no goals
Theorem: UpperBnd_aux3
Proof state before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
⊢ let N := ⌊|t|⌋₊;
  ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
intro N
Proof state after:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Theorem: UpperBnd_aux3
Proof state before:
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
obtain ⟨Npos, N_le_t, _, _, σPos, _⟩ := UpperBnd_aux hA t_gt σ_ge
Proof state after:
case intro.intro.intro.intro.intro
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Theorem: UpperBnd_aux3
Proof state before:
case intro.intro.intro.intro.intro
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
have logt_gt := logt_gt_one t_gt
Proof state after:
case intro.intro.intro.intro.intro
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Theorem: UpperBnd_aux3
Proof state before:
case intro.intro.intro.intro.intro
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
have (n : ℕ) (hn : n ∈ Finset.range (N + 1)) := ZetaBnd_aux2 (n := n) hA.1 σPos ?_ σ_ge
Proof state after:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ∀ n ∈ Finset.range (N + 1), ‖↑n ^ (-(↑σ + ↑t * I))‖ ≤ (↑n)⁻¹ * A.exp
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log

case intro.intro.intro.intro.intro.refine_1
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
n : ℕ
hn : n ∈ Finset.range (N + 1)
⊢ ↑n ≤ |t|
Theorem: UpperBnd_aux3
Proof state before:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ∀ n ∈ Finset.range (N + 1), ‖↑n ^ (-(↑σ + ↑t * I))‖ ≤ (↑n)⁻¹ * A.exp
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
replace := norm_sum_le_of_le (Finset.range (N + 1)) this
Proof state after:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ ∑ b ∈ Finset.range (N + 1), (↑b)⁻¹ * A.exp
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Theorem: UpperBnd_aux3
Proof state before:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ ∑ b ∈ Finset.range (N + 1), (↑b)⁻¹ * A.exp
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
rw [← Finset.sum_mul, mul_comm _ (Real.exp A)] at this
Proof state after:
case intro.intro.intro.intro.intro.refine_2
A C σ t : ℝ
hA : A ∈ Ioc 0 (1 / 2)
σ_ge : 1 - A / |t|.log ≤ σ
t_gt : 3 < |t|
hC : 2 ≤ C
N : ℕ := ⌊|t|⌋₊
Npos : 0 < ⌊|t|⌋₊
N_le_t : ↑⌊|t|⌋₊ ≤ |t|
left✝¹ : 1 < |t|.log
left✝ : 1 - A < σ
σPos : 0 < σ
right✝ : ↑σ + ↑t * I ≠ 1
logt_gt : 1 < |t|.log
this : ‖∑ b ∈ Finset.range (N + 1), ↑b ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log