internlm/Lean-Github huggingface dataset:
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
⊢ 0 ≤ (x - 1).log / x.log
Tactic:
positivity
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
⊢ 0 < x - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
⊢ x - 1 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
⊢ 0 ≤ x.log
Tactic:
positivity
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ 1 < (x - 1) * x
Tactic:
nlinarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ ((x - 1) * x).log.log = (x.log + (x - 1).log).log
Tactic:
rw [mul_comm, Real.log_mul (by positivity) (by linarith)]
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x - 1 ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ (x.log + (x - 1).log).log = x.log.log + (1 + (x - 1).log / x.log).log
Tactic:
rw [log_add _ _ (by linarith) (by linarith)]
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ 0 < x.log
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ 0 < x.log + (x - 1).log
Tactic:
linarith
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x.log.log + (1 + (x - 1).log / x.log).log ≥ x.log.log + log 2 * ((x - 1).log / x.log)
Tactic:
bound [le_log_one_add ll0 ll1]
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x.log.log + log 2 * ((x - 1).log / x.log) ≥ x.log.log + 0.693 * 0.791
Tactic:
bound [lt_log_2]
Proof state after:
no goals
Theorem: log_log_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
w x : ℝ
z4 : 4 ≤ x
x0 : 0 < x
x1 : 1 < x
zw : (x - 1) * x ≤ w
lx1 : 1 < (x - 1).log
lx : 1 < x.log
ll : 0.791 ≤ (x - 1).log / x.log
ll0 : 0 ≤ (x - 1).log / x.log
ll1 : (x - 1).log / x.log ≤ 1
⊢ x.log.log + 0.693 * 0.791 ≥ x.log.log + 0.548
Tactic:
bound
Proof state after:
no goals
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ Postcritical ⋯ c ↑z
Tactic:
have d0 : 0 < d := d_pos d
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
⊢ Postcritical ⋯ c ↑z
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
⊢ Postcritical ⋯ c ↑z
Tactic:
have lcz : log (log (abs c)) ≤ log (log (abs z)) := log_log_mono (by linarith) cz
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
⊢ Postcritical ⋯ c ↑z
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
⊢ Postcritical ⋯ c ↑z
Tactic:
simp only [Postcritical, multibrot_p]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
⊢ ⋯.potential c ↑z < ⋯.potential c 0
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
⊢ ⋯.potential c ↑z < ⋯.potential c 0
Tactic:
set s := superF d
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c ↑z < s.potential c 0
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c ↑z < s.potential c 0
Tactic:
rw [← Real.pow_rpow_inv_natCast s.potential_nonneg d0.ne', ←
  Real.pow_rpow_inv_natCast (s.potential_nonneg : 0 ≤ s.potential c 0) d0.ne']
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ (s.potential c ↑z ^ d) ^ (↑d)⁻¹ < (s.potential c 0 ^ d) ^ (↑d)⁻¹
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ (s.potential c ↑z ^ d) ^ (↑d)⁻¹ < (s.potential c 0 ^ d) ^ (↑d)⁻¹
Tactic:
simp only [← s.potential_eqn]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c (f d c ↑z) ^ (↑d)⁻¹ < s.potential c (f d c 0) ^ (↑d)⁻¹
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c (f d c ↑z) ^ (↑d)⁻¹ < s.potential c (f d c 0) ^ (↑d)⁻¹
Tactic:
refine Real.rpow_lt_rpow s.potential_nonneg ?_ (by bound)
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)
Tactic:
generalize hw : f' d c z = w
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)
Tactic:
have e : f d c z = w := by rw [f, lift_coe', hw]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
e : f d c ↑z = ↑w
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
e : f d c ↑z = ↑w
⊢ s.potential c (f d c ↑z) < s.potential c (f d c 0)
Tactic:
simp only [f_0, e]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
e : f d c ↑z = ↑w
⊢ s.potential c ↑w < s.potential c ↑c
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
e : f d c ↑z = ↑w
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
clear e
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ s.potential c ↑w < s.potential c ↑c
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
have zw : abs z ≤ abs w := by rw [←hw]; exact le_self_iter d (by linarith) cz 1
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
⊢ s.potential c ↑w < s.potential c ↑c
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
have cw : abs c ≤ abs w := le_trans cz zw
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
⊢ s.potential c ↑w < s.potential c ↑c
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
have pc1 : s.potential c c < 1 := potential_lt_one_of_two_lt (by linarith) (le_refl _)
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
⊢ s.potential c ↑w < s.potential c ↑c
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
have pw1 : s.potential c w < 1 := potential_lt_one_of_two_lt (by linarith) (by linarith)
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ s.potential c ↑w < s.potential c ↑c
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ s.potential c ↑w < s.potential c ↑c
Tactic:
rw [←log_neg_log_strict_anti potential_pos potential_pos pw1 pc1]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (-(⋯.potential c ↑c).log).log < (-(⋯.potential c ↑w).log).log
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (-(⋯.potential c ↑c).log).log < (-(⋯.potential c ↑w).log).log
Tactic:
refine lt_of_lt_of_le ?_ (le_sub_iff_add_le.mp (abs_le.mp
  (log_neg_log_potential_approx d (by linarith) cw)).1)
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (-(⋯.potential c ↑c).log).log < -iter_error d c w + (Complex.abs w).log.log
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ (-(⋯.potential c ↑c).log).log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
refine lt_of_le_of_lt (sub_le_iff_le_add.mp (abs_le.mp
  (log_neg_log_potential_approx d (by linarith) (le_refl _))).2) ?_
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
have lzw : log (log (abs z)) + 0.548 ≤ log (log (abs w)) := by
  rw [←hw]; exact log_log_iter (by linarith) cz
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
have ie : ∀ z : ℂ, 4 ≤ abs z → abs c ≤ abs z → iter_error d c z ≤ 0.15 := by
  intro z z4 cz
  refine le_trans (iter_error_le_of_z4 d z4 cz) ?_
  calc 0.8095 / (abs z * log (abs z))
    _ ≤ 0.8095 / (4 * log 4) := by bound
    _ ≤ 0.8095 / (4 * 1.386) := by bound [lt_log_4]
    _ ≤ 0.15 := by norm_num
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
have iec := ie c c4 (le_refl _)
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
have iew := ie w (by linarith) cw
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Theorem: postcritical_large
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ iter_error d c c + (Complex.abs c).log.log < -iter_error d c w + (Complex.abs w).log.log
Tactic:
refine lt_of_lt_of_le (lt_of_le_of_lt (add_le_add iec lcz) ?_) (add_le_add (neg_le_neg iew) lzw)
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c4 : 4 ≤ Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
d0 : 0 < d
lcz : (Complex.abs c).log.log ≤ (Complex.abs z).log.log
s : Super (f d) d ∞ := superF d
w : ℂ
hw : f' d c z = w
zw : Complex.abs z ≤ Complex.abs w
cw : Complex.abs c ≤ Complex.abs w
pc1 : s.potential c ↑c < 1
pw1 : s.potential c ↑w < 1
lzw : (Complex.abs z).log.log + 0.548 ≤ (Complex.abs w).log.log
ie : ∀ (z : ℂ), 4 ≤ Complex.abs z → Complex.abs c ≤ Complex.abs z → iter_error d c z ≤ 0.15
iec : iter_error d c c ≤ 0.15
iew : iter_error d c w ≤ 0.15
⊢ 0.15 + (Complex.abs z).log.log < -0.15 + ((Complex.abs z).log.log + 0.548)