internlm/Lean-Github huggingface dataset:
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))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * C * |t|.log
Tactic:
rw [mul_assoc]
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)
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))‖ ≤ A.exp * ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹
⊢ ‖∑ n ∈ Finset.range (N + 1), ↑n ^ (-(↑σ + ↑t * I))‖ ≤ A.exp * (C * |t|.log)
Tactic:
apply le_trans this <| (mul_le_mul_left A.exp_pos).mpr ?_
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|⌋₊
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)⁻¹
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ ≤ 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|⌋₊
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)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ ≤ C * |t|.log
Tactic:
refine le_trans ?_ this
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|⌋₊
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)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ ≤ 1 + (↑N).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|⌋₊
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)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ ≤ 1 + (↑N).log
Tactic:
convert harmonic_eq_sum_Icc ▸ harmonic_le_one_add_log N
Proof state after:
case h.e'_3
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)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ = ↑(∑ i ∈ Finset.Icc 1 N, (↑i)⁻¹)
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|⌋₊
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)⁻¹
⊢ 1 + (↑N).log ≤ C * |t|.log
Tactic:
by_cases hN : N = 1
Proof state after:
case pos
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)⁻¹
hN : N = 1
⊢ 1 + (↑N).log ≤ C * |t|.log

case neg
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)⁻¹
hN : ¬N = 1
⊢ 1 + (↑N).log ≤ C * |t|.log
Theorem: UpperBnd_aux3
Proof state before:
case pos
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)⁻¹
hN : N = 1
⊢ 1 + (↑N).log ≤ C * |t|.log
Tactic:
simp only [hN, Nat.cast_one, Real.log_one, add_zero]
Proof state after:
case pos
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)⁻¹
hN : N = 1
⊢ 1 ≤ C * |t|.log
Theorem: UpperBnd_aux3
Proof state before:
case pos
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)⁻¹
hN : N = 1
⊢ 1 ≤ C * |t|.log
Tactic:
have : 2 * 1 ≤ C * Real.log |t| := mul_le_mul hC logt_gt.le (by linarith) (by linarith)
Proof state after:
case pos
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)⁻¹
hN : N = 1
this : 2 * 1 ≤ C * |t|.log
⊢ 1 ≤ C * |t|.log
Theorem: UpperBnd_aux3
Proof state before:
case pos
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)⁻¹
hN : N = 1
this : 2 * 1 ≤ C * |t|.log
⊢ 1 ≤ C * |t|.log
Tactic:
linarith
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
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)⁻¹
hN : N = 1
⊢ 0 ≤ 1
Tactic:
linarith
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
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)⁻¹
hN : N = 1
⊢ 0 ≤ C
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperBnd_aux3
Proof state before:
case neg
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)⁻¹
hN : ¬N = 1
⊢ 1 + (↑N).log ≤ C * |t|.log
Tactic:
rw [(by ring : C * Real.log |t| = Real.log |t| + (C - 1) * Real.log |t|),
  ← one_mul <| Real.log (N: ℝ)]
Proof state after:
case neg
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)⁻¹
hN : ¬N = 1
⊢ 1 + 1 * (↑N).log ≤ |t|.log + (C - 1) * |t|.log
Theorem: UpperBnd_aux3
Proof state before:
case neg
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)⁻¹
hN : ¬N = 1
⊢ 1 + 1 * (↑N).log ≤ |t|.log + (C - 1) * |t|.log
Tactic:
apply add_le_add logt_gt.le
Proof state after:
case neg
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)⁻¹
hN : ¬N = 1
⊢ 1 * (↑N).log ≤ (C - 1) * |t|.log
Theorem: UpperBnd_aux3
Proof state before:
case neg
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)⁻¹
hN : ¬N = 1
⊢ 1 * (↑N).log ≤ (C - 1) * |t|.log
Tactic:
refine mul_le_mul (by linarith) ?_ (by positivity) (by linarith)
Proof state after:
case neg
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)⁻¹
hN : ¬N = 1
⊢ (↑N).log ≤ |t|.log
Theorem: UpperBnd_aux3
Proof state before:
case neg
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)⁻¹
hN : ¬N = 1
⊢ (↑N).log ≤ |t|.log
Tactic:
exact Real.log_le_log (by positivity) N_le_t
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
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)⁻¹
hN : ¬N = 1
⊢ C * |t|.log = |t|.log + (C - 1) * |t|.log
Tactic:
ring
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
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)⁻¹
hN : ¬N = 1
⊢ 1 ≤ C - 1
Tactic:
linarith
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
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)⁻¹
hN : ¬N = 1
⊢ 0 ≤ (↑N).log
Tactic:
positivity
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
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)⁻¹
hN : ¬N = 1
⊢ 0 ≤ C - 1
Tactic:
linarith
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
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)⁻¹
hN : ¬N = 1
⊢ 0 < ↑N
Tactic:
positivity
Proof state after:
no goals
Theorem: UpperBnd_aux3
Proof state before:
case h.e'_3
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)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ i ∈ Finset.range (N + 1), (↑i)⁻¹ = ↑(∑ i ∈ Finset.Icc 1 N, (↑i)⁻¹)
Tactic:
simp only [Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast, Finset.range_eq_Ico]
Proof state after:
case h.e'_3
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)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ x ∈ Finset.Ico 0 (N + 1), (↑x)⁻¹ = ∑ x ∈ Finset.Icc 1 N, (↑x)⁻¹
Theorem: UpperBnd_aux3
Proof state before:
case h.e'_3
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)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ x ∈ Finset.Ico 0 (N + 1), (↑x)⁻¹ = ∑ x ∈ Finset.Icc 1 N, (↑x)⁻¹
Tactic:
rw [riemannZeta0_zero_aux (N + 1) (by linarith)]
Proof state after:
case h.e'_3
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)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ x ∈ Finset.Ico 1 (N + 1), (↑x)⁻¹ = ∑ x ∈ Finset.Icc 1 N, (↑x)⁻¹
Theorem: UpperBnd_aux3
Proof state before:
case h.e'_3
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)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ ∑ x ∈ Finset.Ico 1 (N + 1), (↑x)⁻¹ = ∑ x ∈ Finset.Icc 1 N, (↑x)⁻¹
Tactic:
congr! 1
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
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)⁻¹
this : 1 + (↑N).log ≤ C * |t|.log
⊢ 0 < N + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperBnd_aux3
Proof state before:
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|
Tactic:
simp only [Finset.mem_range] at hn
Proof state after:
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 < N + 1
⊢ ↑n ≤ |t|
Theorem: UpperBnd_aux3
Proof state before:
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 < N + 1
⊢ ↑n ≤ |t|
Tactic:
linarith [(by exact_mod_cast (by omega : n ≤ N) : (n : ℝ) ≤ N)]
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
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 < N + 1
⊢ ↑n ≤ ↑N
Tactic:
exact_mod_cast (by omega : n ≤ N)
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
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 < N + 1
⊢ n ≤ N
Tactic:
omega
Proof state after:
no goals
Theorem: Nat.self_div_floor_bound
Proof state before:
t : ℝ
t_ge : 1 ≤ |t|
⊢ let N := ⌊|t|⌋₊;
  |t| / ↑N ∈ Icc 1 2
Tactic:
intro N
Proof state after:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
⊢ |t| / ↑N ∈ Icc 1 2
Theorem: Nat.self_div_floor_bound
Proof state before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
⊢ |t| / ↑N ∈ Icc 1 2
Tactic:
have Npos : 0 < N := Nat.floor_pos.mpr (by linarith)
Proof state after:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
⊢ |t| / ↑N ∈ Icc 1 2
Theorem: Nat.self_div_floor_bound
Proof state before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
⊢ |t| / ↑N ∈ Icc 1 2
Tactic:
have N_le_t : N ≤ |t| := Nat.floor_le <| abs_nonneg _
Proof state after:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| / ↑N ∈ Icc 1 2
Theorem: Nat.self_div_floor_bound
Proof state before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| / ↑N ∈ Icc 1 2
Tactic:
constructor
Proof state after:
case left
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 1 ≤ |t| / ↑N

case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| / ↑N ≤ 2
Theorem: Nat.self_div_floor_bound
Proof state before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
⊢ 1 ≤ |t|
Tactic:
linarith
Proof state after:
no goals
Theorem: Nat.self_div_floor_bound
Proof state before:
case left
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 1 ≤ |t| / ↑N
Tactic:
apply le_div_iff (by simp [Npos]) |>.mpr
Proof state after:
case left
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 1 * ↑N ≤ |t|
Theorem: Nat.self_div_floor_bound
Proof state before:
case left
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 1 * ↑N ≤ |t|
Tactic:
simp [N_le_t]
Proof state after:
no goals
Theorem: Nat.self_div_floor_bound
Proof state before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 0 < ↑N
Tactic:
simp [Npos]
Proof state after:
no goals
Theorem: Nat.self_div_floor_bound
Proof state before:
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| / ↑N ≤ 2
Tactic:
apply div_le_iff (by positivity) |>.mpr
Proof state after:
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| ≤ 2 * ↑N
Theorem: Nat.self_div_floor_bound
Proof state before:
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| ≤ 2 * ↑N
Tactic:
suffices |t| < N + 1 by linarith [(by exact_mod_cast (by omega) : 1 ≤ (N : ℝ))]
Proof state after:
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| < ↑N + 1
Theorem: Nat.self_div_floor_bound
Proof state before:
case right
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ |t| < ↑N + 1
Tactic:
apply Nat.lt_floor_add_one
Proof state after:
no goals
Theorem: Nat.self_div_floor_bound
Proof state before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
⊢ 0 < ↑N
Tactic:
positivity
Proof state after:
no goals
Theorem: Nat.self_div_floor_bound
Proof state before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
this : |t| < ↑N + 1
⊢ |t| ≤ 2 * ↑N
Tactic:
linarith [(by exact_mod_cast (by omega) : 1 ≤ (N : ℝ))]
Proof state after:
no goals
Theorem: Nat.self_div_floor_bound
Proof state before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
this : |t| < ↑N + 1
⊢ 1 ≤ ↑N
Tactic:
exact_mod_cast (by omega)
Proof state after:
no goals
Theorem: Nat.self_div_floor_bound
Proof state before:
t : ℝ
t_ge : 1 ≤ |t|
N : ℕ := ⌊|t|⌋₊
Npos : 0 < N
N_le_t : ↑N ≤ |t|
this : |t| < ↑N + 1
⊢ 1 ≤ N
Tactic:
omega
Proof state after:
no goals
Theorem: UpperBnd_aux5
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
⊢ (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
Tactic:
obtain ⟨h₁, h₂⟩ := Nat.self_div_floor_bound (by linarith)
Proof state after:
case intro
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
Theorem: UpperBnd_aux5
Proof state before:
case intro
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
Tactic:
calc _ ≤ ((|t| / ↑⌊|t|⌋₊) ^ (2 : ℝ)) := by gcongr; exact h₁
     _ ≤ (2 : ℝ) ^ (2 : ℝ) := by gcongr
     _ = 4 := by norm_num
Proof state after:
no goals
Theorem: UpperBnd_aux5
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
⊢ 1 ≤ |?m.763672|
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperBnd_aux5
Proof state before:
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ (|t| / ↑⌊|t|⌋₊) ^ σ ≤ (|t| / ↑⌊|t|⌋₊) ^ 2
Tactic:
gcongr
Proof state after:
case hx
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ 1 ≤ |t| / ↑⌊|t|⌋₊
Theorem: UpperBnd_aux5
Proof state before:
case hx
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ 1 ≤ |t| / ↑⌊|t|⌋₊
Tactic:
exact h₁
Proof state after:
no goals