Theorem: f_error_le_generic (Ray/Dynamics/Multibrot/Iterates.lean)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
lb : l.exp ≤ b
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
have z3 := le_trans b3 bz
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
lb : l.exp ≤ b
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
lb : l.exp ≤ b
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
replace lb := (Real.le_log_iff_exp_le (by positivity)).mpr (le_trans lb bz)
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
have l0' : 0 < log (abs z) := trans l0 lb
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
have inner_le : -log (1 - 1 / abs z) ≤ s / abs z := by
  rw [one_div, div_eq_mul_inv]
  apply neg_log_one_sub_le_linear (by positivity) s1
  exact le_trans (inv_le_inv_of_le (by positivity) bz) bs
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
have dm : 2 * log (abs z) ≤ d * log (abs z) := by bound
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
have div_le : -log (1 - 1 / abs z) / (d * log (abs z)) ≤ t := by
  have sz : s / abs z ≤ s / b := div_le_div_of_nonneg_left (by positivity) (by positivity) bz
  exact le_trans (div_le_div (by positivity) (le_trans inner_le sz) (by positivity)
    (le_trans (mul_le_mul_of_nonneg_left lb (by norm_num)) dm)) st
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ f_error d z ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine le_trans (neg_log_one_sub_le_linear (f_error_inner_nonneg d z3) c1 ?_) ?_
State after:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹

case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ c * (-(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)) ≤ g / (Complex.abs z * (Complex.abs z).log)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
lb : l.exp ≤ b
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
⊢ 0 < Complex.abs z
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
⊢ -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
Tactic:
rw [one_div, div_eq_mul_inv]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ s * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
⊢ -(1 - (Complex.abs z)⁻¹).log ≤ s * (Complex.abs z)⁻¹
Tactic:
apply neg_log_one_sub_le_linear (by positivity) s1
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
⊢ (Complex.abs z)⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
⊢ (Complex.abs z)⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
exact le_trans (inv_le_inv_of_le (by positivity) bz) bs
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
⊢ 0 ≤ (Complex.abs z)⁻¹
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
⊢ 0 < b
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
⊢ 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
⊢ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
Tactic:
have sz : s / abs z ≤ s / b := div_le_div_of_nonneg_left (by positivity) (by positivity) bz
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
sz : s / Complex.abs z ≤ s / b
⊢ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
sz : s / Complex.abs z ≤ s / b
⊢ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
Tactic:
exact le_trans (div_le_div (by positivity) (le_trans inner_le sz) (by positivity)
  (le_trans (mul_le_mul_of_nonneg_left lb (by norm_num)) dm)) st
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
⊢ 0 ≤ s
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
⊢ 0 < b
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
sz : s / Complex.abs z ≤ s / b
⊢ 0 ≤ s / b
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
sz : s / Complex.abs z ≤ s / b
⊢ 0 < 2 * l
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
sz : s / Complex.abs z ≤ s / b
⊢ 0 ≤ 2
Tactic:
norm_num
State after:
no goals

State before:
case refine_1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹
Tactic:
exact le_trans div_le tc
State after:
no goals

State before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ c * (-(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log)) ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
refine le_trans (mul_le_mul_of_nonneg_left (div_le_div (by positivity) inner_le
  (by positivity) dm) (by positivity)) ?_
State after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ c * (s / Complex.abs z / (2 * (Complex.abs z).log)) ≤ g / (Complex.abs z * (Complex.abs z).log)

State before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ c * (s / Complex.abs z / (2 * (Complex.abs z).log)) ≤ g / (Complex.abs z * (Complex.abs z).log)
Tactic:
simp only [div_eq_mul_inv, ←mul_assoc, mul_inv, mul_comm _ (2⁻¹ : ℝ)]
State after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 2⁻¹ * c * s * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹ ≤ g * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹

State before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 2⁻¹ * c * s * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹ ≤ g * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹
Tactic:
norm_num
State after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 1 / 2 * c * s * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹ ≤ g * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹

State before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 1 / 2 * c * s * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹ ≤ g * (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹
Tactic:
simp only [mul_assoc _ (abs z)⁻¹ _]
State after:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 1 / 2 * c * s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹) ≤ g * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹)

State before:
case refine_2
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 1 / 2 * c * s * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹) ≤ g * ((Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹)
Tactic:
exact mul_le_mul_of_nonneg_right csg (by positivity)
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 0 ≤ s / Complex.abs z
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 0 < 2 * (Complex.abs z).log
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 0 ≤ c
Tactic:
positivity
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b l s t c g : ℝ
z : ℂ
bz : b ≤ Complex.abs z
b3 : autoParam (3 ≤ b) _auto✝
st : autoParam (s / b / (2 * l) ≤ t) _auto✝
tc : autoParam (t ≤ min 1 (((c - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
bs : autoParam (b⁻¹ ≤ min 1 (((s - 1) * 2)⁻¹ + 1)⁻¹) _auto✝
csg : autoParam (1 / 2 * c * s ≤ g) _auto✝
l0 : autoParam (0 < l) _auto✝
c1 : autoParam (1 < c) _auto✝
s1 : autoParam (1 < s) _auto✝
z3 : 3 ≤ Complex.abs z
lb : l ≤ (Complex.abs z).log
l0' : 0 < (Complex.abs z).log
inner_le : -(1 - 1 / Complex.abs z).log ≤ s / Complex.abs z
dm : 2 * (Complex.abs z).log ≤ ↑d * (Complex.abs z).log
div_le : -(1 - 1 / Complex.abs z).log / (↑d * (Complex.abs z).log) ≤ t
⊢ 0 ≤ (Complex.abs z)⁻¹ * (Complex.abs z).log⁻¹
Tactic:
positivity
State after:
no goals