internlm/Lean-Github huggingface dataset:
Theorem: le_self_iter
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ Complex.abs z ≤ 2 ^ n * Complex.abs z
Tactic:
exact le_mul_of_one_le_left (Complex.abs.nonneg _) (one_le_pow_of_one_le (by norm_num) _)
Proof state after:
no goals
Theorem: le_self_iter
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ 1 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: tendsto_iter_atInf
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => (f' d c)^[n] z) atTop atInf
Tactic:
simp only [tendsto_atInf_iff_norm_tendsto_atTop, Complex.norm_eq_abs]
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun x => Complex.abs ((f' d c)^[x] z)) atTop atTop
Theorem: tendsto_iter_atInf
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun x => Complex.abs ((f' d c)^[x] z)) atTop atTop
Tactic:
refine Filter.tendsto_atTop_mono (iter_large_z3 d z3 cz) ?_
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => 2 ^ n * Complex.abs z) atTop atTop
Theorem: tendsto_iter_atInf
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => 2 ^ n * Complex.abs z) atTop atTop
Tactic:
exact Filter.Tendsto.atTop_mul_const (by linarith) (tendsto_pow_atTop_atTop_of_one_lt one_lt_two)
Proof state after:
no goals
Theorem: tendsto_iter_atInf
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
z3 : 3 ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: f_ne_zero
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ z ^ d + c ≠ 0
Tactic:
rw [← Complex.abs.ne_zero_iff]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ Complex.abs (z ^ d + c) ≠ 0
Theorem: f_ne_zero
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ Complex.abs (z ^ d + c) ≠ 0
Tactic:
apply ne_of_gt
Proof state after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ 0 < Complex.abs (z ^ d + c)
Theorem: f_ne_zero
Proof state before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ 0 < Complex.abs (z ^ d + c)
Tactic:
have z1 : 1 ≤ abs z := le_trans (by norm_num) z3
Proof state after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ 0 < Complex.abs (z ^ d + c)
Theorem: f_ne_zero
Proof state before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ 0 < Complex.abs (z ^ d + c)
Tactic:
calc abs (z ^ d + c)
  _ ≥ abs (z ^ d) - abs c := by bound
  _ = abs z ^ d - abs c := by rw [Complex.abs.map_pow]
  _ ≥ abs z ^ 2 - abs z := by bound
  _ = abs z * (abs z - 1) := by ring
  _ ≥ 3 * (3 - 1) := by bound
  _ > 0 := by norm_num
Proof state after:
no goals
Theorem: f_ne_zero
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ 1 ≤ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_ne_zero
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ Complex.abs (z ^ d + c) ≥ Complex.abs (z ^ d) - Complex.abs c
Tactic:
bound
Proof state after:
no goals
Theorem: f_ne_zero
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ Complex.abs (z ^ d) - Complex.abs c = Complex.abs z ^ d - Complex.abs c
Tactic:
rw [Complex.abs.map_pow]
Proof state after:
no goals
Theorem: f_ne_zero
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ Complex.abs z ^ d - Complex.abs c ≥ Complex.abs z ^ 2 - Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: f_ne_zero
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ Complex.abs z ^ 2 - Complex.abs z = Complex.abs z * (Complex.abs z - 1)
Tactic:
ring
Proof state after:
no goals
Theorem: f_ne_zero
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ Complex.abs z * (Complex.abs z - 1) ≥ 3 * (3 - 1)
Tactic:
bound
Proof state after:
no goals
Theorem: f_ne_zero
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ 3 * (3 - 1) > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: le_log_abs_z
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ 1.0986 ≤ (Complex.abs z).log
Tactic:
rw [Real.le_log_iff_exp_le (by linarith)]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ Complex.abs z
Theorem: le_log_abs_z
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ Complex.abs z
Tactic:
refine le_trans ?_ z3
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ 3
Theorem: le_log_abs_z
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ exp 1.0986 ≤ 3
Tactic:
norm_num
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (5493 / 5000).exp ≤ 3
Theorem: le_log_abs_z
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (5493 / 5000).exp ≤ 3
Tactic:
exact (exp_div_lt).le
Proof state after:
no goals
Theorem: le_log_abs_z
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ 0 < Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
have z0 : 0 < abs z := lt_of_lt_of_le (by norm_num) z3
Proof state after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
have z0' : z ≠ 0 := by exact nnnorm_pos.mp z0
Proof state after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
have i1 : 1 / abs z ≤ 1 := by rw [one_div_le z0]; exact le_trans (by norm_num) z3; norm_num
Proof state after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
have s1 : 1 - 1 / abs z < 1 := by rw [tsub_lt_iff_tsub_lt]; norm_num; exact z0'; exact i1; rfl
Proof state after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
s1 : 1 - 1 / Complex.abs z < 1
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
s1 : 1 - 1 / Complex.abs z < 1
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
have l1 := le_log_abs_z z3
Proof state after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
s1 : 1 - 1 / Complex.abs z < 1
l1 : 1.0986 ≤ (Complex.abs z).log
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
s1 : 1 - 1 / Complex.abs z < 1
l1 : 1.0986 ≤ (Complex.abs z).log
⊢ 0 ≤ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
exact div_nonneg (neg_nonneg.mpr (Real.log_nonpos (sub_nonneg.mpr i1) s1.le)) (by positivity)
Proof state after:
no goals
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
⊢ z ≠ 0
Tactic:
exact nnnorm_pos.mp z0
Proof state after:
no goals
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 1 / Complex.abs z ≤ 1
Tactic:
rw [one_div_le z0]
Proof state after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 1 / 1 ≤ Complex.abs z

c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 0 < 1
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 1 / 1 ≤ Complex.abs z

c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 0 < 1
Tactic:
exact le_trans (by norm_num) z3
Proof state after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 0 < 1
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
⊢ 1 / 1 ≤ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 - 1 / Complex.abs z < 1
Tactic:
rw [tsub_lt_iff_tsub_lt]
Proof state after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 - 1 < 1 / Complex.abs z

case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 - 1 < 1 / Complex.abs z

case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Tactic:
norm_num
Proof state after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ ¬z = 0

case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ ¬z = 0

case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Tactic:
exact z0'
Proof state after:
case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Theorem: f_error_inner_nonneg
Proof state before:
case h₁
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 / Complex.abs z ≤ 1

case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Tactic:
exact i1
Proof state after:
case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Theorem: f_error_inner_nonneg
Proof state before:
case h₂
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
⊢ 1 ≤ 1
Tactic:
rfl
Proof state after:
no goals
Theorem: f_error_inner_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
z : ℂ
z3 : 3 ≤ Complex.abs z
z0 : 0 < Complex.abs z
z0' : z ≠ 0
i1 : 1 / Complex.abs z ≤ 1
s1 : 1 - 1 / Complex.abs z < 1
l1 : 1.0986 ≤ (Complex.abs z).log
⊢ 0 ≤ ↑d * (Complex.abs z).log
Tactic:
positivity
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ 0 ≤ f_error d z
Tactic:
rw [f_error, le_neg, neg_zero]
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0
Tactic:
have d0 : 0 < d := d_pos d
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0
Tactic:
have  l1 : 1 ≤ log (abs z) := le_trans (by norm_num) (le_log_abs_z z3)
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)).log ≤ 0
Tactic:
apply Real.log_nonpos
Proof state after:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 ≤ 1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)

case h'x
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ 1
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
⊢ 1 ≤ 1.0986
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 ≤ 1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)
Tactic:
simp only [one_div, neg_div, sub_nonneg, neg_le]
Proof state after:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -1 ≤ (1 - (Complex.abs z)⁻¹).log / (↑d * (Complex.abs z).log)
Theorem: f_error_nonneg
Proof state before:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -1 ≤ (1 - (Complex.abs z)⁻¹).log / (↑d * (Complex.abs z).log)
Tactic:
rw [le_div_iff (by positivity), neg_one_mul, neg_le]
Proof state after:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ ↑d * (Complex.abs z).log
Theorem: f_error_nonneg
Proof state before:
case hx
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ ↑d * (Complex.abs z).log
Tactic:
trans 2
Proof state after:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ 2

c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 2 ≤ ↑d * (Complex.abs z).log
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 < ↑d * (Complex.abs z).log
Tactic:
positivity
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ 2
Tactic:
refine le_trans (neg_log_one_sub_le_linear (c := 2) (by positivity) (by norm_num) ?_) ?_
Proof state after:
case refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (Complex.abs z)⁻¹ ≤ min 1 (((2 - 1) * 2)⁻¹ + 1)⁻¹

case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 2 * (Complex.abs z)⁻¹ ≤ 2
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 ≤ (Complex.abs z)⁻¹
Tactic:
positivity
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
case refine_1
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (Complex.abs z)⁻¹ ≤ min 1 (((2 - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
exact le_trans (inv_le_inv_of_le (by positivity) z3) (by norm_num)
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 < 3
Tactic:
positivity
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 3⁻¹ ≤ min 1 (((2 - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 2 * (Complex.abs z)⁻¹ ≤ 2
Tactic:
simp only [zero_lt_two, mul_le_iff_le_one_right]
Proof state after:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (Complex.abs z)⁻¹ ≤ 1
Theorem: f_error_nonneg
Proof state before:
case refine_2
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ (Complex.abs z)⁻¹ ≤ 1
Tactic:
apply inv_le_one
Proof state after:
case refine_2.ha
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 1 ≤ Complex.abs z
Theorem: f_error_nonneg
Proof state before:
case refine_2.ha
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 1 ≤ Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 2 ≤ ↑d * (Complex.abs z).log
Tactic:
exact le_trans (by norm_num) (mul_le_mul (two_le_cast_d d) l1 zero_le_one (by positivity))
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 2 ≤ 2 * 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 0 ≤ ↑d
Tactic:
positivity
Proof state after:
no goals
Theorem: f_error_nonneg
Proof state before:
case h'x
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z3 : 3 ≤ Complex.abs z
d0 : 0 < d
l1 : 1 ≤ (Complex.abs z).log
⊢ 1 - -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ 1
Tactic:
linarith [f_error_inner_nonneg d z3]
Proof state after:
no goals