internlm/Lean-Github huggingface dataset:
Theorem: iter_large
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
have nd : n + 1 ≤ n * d + 1 := by bound
Proof state after:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Theorem: iter_large
Proof state before:
case succ
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z ≤ Complex.abs (f' d c w)
Tactic:
calc abs (w ^ d + c)
  _ ≥ abs (w ^ d) - abs c := by bound
  _ = abs w ^ d - abs c := by rw [Complex.abs.map_pow]
  _ ≥ ((b-1) ^ n * abs z) ^ d - abs c := by bound
  _ = (b-1) ^ (n*d) * abs z ^ d - abs c := by rw [mul_pow, pow_mul]
  _ ≥ (b-1) ^ (n*d) * abs z ^ 2 - abs c := by bound
  _ = (b-1) ^ (n*d) * (abs z * abs z) - abs c := by rw [pow_two]
  _ ≥ (b-1) ^ (n*d) * (b * abs z) - abs c := by bound
  _ = (b-1) ^ (n*d) * (b-1) * abs z + ((b-1) ^ (n*d) * abs z - abs c) := by ring
  _ = (b-1) ^ (n*d + 1) * abs z + ((b-1) ^ (n * d) * abs z - abs c) := by rw [pow_succ]
  _ ≥ (b-1) ^ (n + 1) * abs z + (1 * abs z - abs c) := by bound
  _ = (b-1) ^ (n + 1) * abs z + (abs z - abs c) := by rw [one_mul]
  _ ≥ (b-1) ^ (n + 1) * abs z := by bound
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
⊢ 1 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
⊢ 1 ≤ b - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
⊢ 0 ≤ b - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
⊢ n + 1 ≤ n * d + 1
Tactic:
bound
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ Complex.abs (w ^ d + c) ≥ Complex.abs (w ^ d) - Complex.abs c
Tactic:
bound
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ Complex.abs (w ^ d) - Complex.abs c = Complex.abs w ^ d - Complex.abs c
Tactic:
rw [Complex.abs.map_pow]
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ Complex.abs w ^ d - Complex.abs c ≥ ((b - 1) ^ n * Complex.abs z) ^ d - Complex.abs c
Tactic:
bound
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ ((b - 1) ^ n * Complex.abs z) ^ d - Complex.abs c = (b - 1) ^ (n * d) * Complex.abs z ^ d - Complex.abs c
Tactic:
rw [mul_pow, pow_mul]
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d) * Complex.abs z ^ d - Complex.abs c ≥ (b - 1) ^ (n * d) * Complex.abs z ^ 2 - Complex.abs c
Tactic:
bound
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d) * Complex.abs z ^ 2 - Complex.abs c =
    (b - 1) ^ (n * d) * (Complex.abs z * Complex.abs z) - Complex.abs c
Tactic:
rw [pow_two]
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d) * (Complex.abs z * Complex.abs z) - Complex.abs c ≥
    (b - 1) ^ (n * d) * (b * Complex.abs z) - Complex.abs c
Tactic:
bound
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d) * (b * Complex.abs z) - Complex.abs c =
    (b - 1) ^ (n * d) * (b - 1) * Complex.abs z + ((b - 1) ^ (n * d) * Complex.abs z - Complex.abs c)
Tactic:
ring
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d) * (b - 1) * Complex.abs z + ((b - 1) ^ (n * d) * Complex.abs z - Complex.abs c) =
    (b - 1) ^ (n * d + 1) * Complex.abs z + ((b - 1) ^ (n * d) * Complex.abs z - Complex.abs c)
Tactic:
rw [pow_succ]
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n * d + 1) * Complex.abs z + ((b - 1) ^ (n * d) * Complex.abs z - Complex.abs c) ≥
    (b - 1) ^ (n + 1) * Complex.abs z + (1 * Complex.abs z - Complex.abs c)
Tactic:
bound
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z + (1 * Complex.abs z - Complex.abs c) =
    (b - 1) ^ (n + 1) * Complex.abs z + (Complex.abs z - Complex.abs c)
Tactic:
rw [one_mul]
Proof state after:
no goals
Theorem: iter_large
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
b : ℝ
c z : ℂ
b2 : 2 ≤ b
bz : b ≤ Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
w : ℂ
h : (b - 1) ^ n * Complex.abs z ≤ Complex.abs w
z1 : 1 ≤ Complex.abs z
b1 : 1 ≤ b - 1
b0 : 0 ≤ b - 1
nd : n + 1 ≤ n * d + 1
⊢ (b - 1) ^ (n + 1) * Complex.abs z + (Complex.abs z - Complex.abs c) ≥ (b - 1) ^ (n + 1) * Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: iter_small
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
c z : ℂ
⊢ Complex.abs (f' d c z) ≤ Complex.abs z ^ d + Complex.abs 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]
Proof state after:
no goals
Theorem: iter_small
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
c z : ℂ
⊢ Complex.abs (z ^ d + c) ≤ Complex.abs (z ^ d) + Complex.abs c
Tactic:
bound
Proof state after:
no goals
Theorem: iter_small
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
d : ℕ
c 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_f'_iter
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
z : ℂ
⊢ (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
Tactic:
induction' n with n h
Proof state after:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ (f d c)^[0] ↑z = ↑((f' d c)^[0] z)

case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ (f d c)^[n + 1] ↑z = ↑((f' d c)^[n + 1] z)
Theorem: f_f'_iter
Proof state before:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
⊢ (f d c)^[0] ↑z = ↑((f' d c)^[0] z)

case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ (f d c)^[n + 1] ↑z = ↑((f' d c)^[n + 1] z)
Tactic:
simp only [Function.iterate_zero, id]
Proof state after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ (f d c)^[n + 1] ↑z = ↑((f' d c)^[n + 1] z)
Theorem: f_f'_iter
Proof state before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ (f d c)^[n + 1] ↑z = ↑((f' d c)^[n + 1] z)
Tactic:
simp only [h, Function.iterate_succ_apply']
Proof state after:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ f d c ↑((f' d c)^[n] z) = ↑(f' d c ((f' d c)^[n] z))
Theorem: f_f'_iter
Proof state before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
n : ℕ
h : (f d c)^[n] ↑z = ↑((f' d c)^[n] z)
⊢ f d c ↑((f' d c)^[n] z) = ↑(f' d c ((f' d c)^[n] z))
Tactic:
simp only [f, lift', rec_coe]
Proof state after:
no goals
Theorem: multibrot_coe
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ c ∈ multibrot d ↔ ¬Tendsto (fun n => (f' d c)^[n] c) atTop atInf
Tactic:
simp only [multibrot, mem_setOf, f_f'_iter, not_iff_not, tendsto_inf_iff_tendsto_atInf]
Proof state after:
no goals
Theorem: julia_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ (c, ↑z) ∈ ⋯.basin
Tactic:
simp only [multibrot_coe, not_le, not_not, (superF d).basin_iff_attracts, Attracts, f_f'_iter,
  tendsto_inf_iff_tendsto_atInf, tendsto_atInf_iff_norm_tendsto_atTop,
  Complex.norm_eq_abs] at z2 ⊢
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun x => Complex.abs ((f' d c)^[x] z)) atTop atTop
Theorem: julia_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun x => Complex.abs ((f' d c)^[x] z)) atTop atTop
Tactic:
apply Filter.tendsto_atTop_mono (iter_large d (abs z) z2.le (le_refl _) cz)
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => (Complex.abs z - 1) ^ n * Complex.abs z) atTop atTop
Theorem: julia_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => (Complex.abs z - 1) ^ n * Complex.abs z) atTop atTop
Tactic:
refine Filter.Tendsto.atTop_mul (by linarith) ?_ tendsto_const_nhds
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => (Complex.abs z - 1) ^ n) atTop atTop
Theorem: julia_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ Tendsto (fun n => (Complex.abs z - 1) ^ n) atTop atTop
Tactic:
apply tendsto_pow_atTop_atTop_of_one_lt
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1 < Complex.abs z - 1
Theorem: julia_two_lt
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 1 < Complex.abs z - 1
Tactic:
linarith
Proof state after:
no goals
Theorem: julia_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
z2 : 2 < Complex.abs z
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < Complex.abs z
Tactic:
linarith
Proof state after:
no goals
Theorem: julia_le_two
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
m : (c, ↑z) ∉ ⋯.basin
cz : Complex.abs c ≤ Complex.abs z
⊢ Complex.abs z ≤ 2
Tactic:
contrapose m
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
cz : Complex.abs c ≤ Complex.abs z
m : ¬Complex.abs z ≤ 2
⊢ ¬(c, ↑z) ∉ ⋯.basin
Theorem: julia_le_two
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
cz : Complex.abs c ≤ Complex.abs z
m : ¬Complex.abs z ≤ 2
⊢ ¬(c, ↑z) ∉ ⋯.basin
Tactic:
simp only [not_le, not_not] at m ⊢
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
cz : Complex.abs c ≤ Complex.abs z
m : 2 < Complex.abs z
⊢ (c, ↑z) ∈ ⋯.basin
Theorem: julia_le_two
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
z : ℂ
cz : Complex.abs c ≤ Complex.abs z
m : 2 < Complex.abs z
⊢ (c, ↑z) ∈ ⋯.basin
Tactic:
exact julia_two_lt m cz
Proof state after:
no goals
Theorem: multibrot_le_two
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : c ∈ multibrot d
⊢ Complex.abs c ≤ 2
Tactic:
rw [multibrot_basin' (d := d)] at m
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : (c, ↑c) ∉ ⋯.basin
⊢ Complex.abs c ≤ 2
Theorem: multibrot_le_two
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
m : (c, ↑c) ∉ ⋯.basin
⊢ Complex.abs c ≤ 2
Tactic:
exact julia_le_two m (le_refl _)
Proof state after:
no goals
Theorem: multibrot_subset_closedBall
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ multibrot d ⊆ closedBall 0 2
Tactic:
intro c m
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ c ∈ closedBall 0 2
Theorem: multibrot_subset_closedBall
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ c ∈ closedBall 0 2
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ Complex.abs c ≤ 2
Theorem: multibrot_subset_closedBall
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
⊢ Complex.abs c ≤ 2
Tactic:
exact multibrot_le_two m
Proof state after:
no goals
Theorem: multibrot_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a : 2 < Complex.abs c
⊢ c ∉ multibrot d
Tactic:
contrapose a
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a : ¬c ∉ multibrot d
⊢ ¬2 < Complex.abs c
Theorem: multibrot_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a : ¬c ∉ multibrot d
⊢ ¬2 < Complex.abs c
Tactic:
simp only [not_lt, not_not] at a ⊢
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a : c ∈ multibrot d
⊢ Complex.abs c ≤ 2
Theorem: multibrot_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a : c ∈ multibrot d
⊢ Complex.abs c ≤ 2
Tactic:
exact multibrot_le_two a
Proof state after:
no goals
Theorem: multibrot_of_repeat
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
⊢ c ∈ multibrot d
Tactic:
generalize hg : (fun n ↦ (f' d c)^[n] c) = g
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
g : ℕ → ℂ
hg : (fun n => (f' d c)^[n] c) = g
⊢ c ∈ multibrot d
Theorem: multibrot_of_repeat
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
g : ℕ → ℂ
hg : (fun n => (f' d c)^[n] c) = g
⊢ c ∈ multibrot d
Tactic:
replace hg : ∀ n, (f' d c)^[n] c = g n := fun n ↦ by rw [← hg]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
⊢ c ∈ multibrot d
Theorem: multibrot_of_repeat
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
⊢ c ∈ multibrot d
Tactic:
simp only [f_f'_iter, ← coe_zero, coe_eq_coe, hg] at h
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
⊢ c ∈ multibrot d
Theorem: multibrot_of_repeat
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ c ∈ multibrot d
Tactic:
simp only [multibrot_coe, atInf_basis.tendsto_right_iff, true_imp_iff, not_forall,
  Filter.not_eventually, mem_setOf, not_lt, Complex.norm_eq_abs, hg]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∃ x, ∃ᶠ (x_1 : ℕ) in atTop, Complex.abs (g x_1) ≤ x
Theorem: multibrot_of_repeat
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∃ x, ∃ᶠ (x_1 : ℕ) in atTop, Complex.abs (g x_1) ≤ x
Tactic:
use partialSups (fun k ↦ Complex.abs (g k)) b
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∃ᶠ (x : ℕ) in atTop, Complex.abs (g x) ≤ (partialSups fun k => Complex.abs (g k)) b
Theorem: multibrot_of_repeat
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∃ᶠ (x : ℕ) in atTop, Complex.abs (g x) ≤ (partialSups fun k => Complex.abs (g k)) b
Tactic:
apply Filter.frequently_of_forall
Proof state after:
case h.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∀ (x : ℕ), Complex.abs (g x) ≤ (partialSups fun k => Complex.abs (g k)) b
Theorem: multibrot_of_repeat
Proof state before:
case h.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
⊢ ∀ (x : ℕ), Complex.abs (g x) ≤ (partialSups fun k => Complex.abs (g k)) b
Tactic:
intro k
Proof state after:
case h.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k : ℕ
⊢ Complex.abs (g k) ≤ (partialSups fun k => Complex.abs (g k)) b
Theorem: multibrot_of_repeat
Proof state before:
case h.h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k : ℕ
⊢ Complex.abs (g k) ≤ (partialSups fun k => Complex.abs (g k)) b
Tactic:
rcases lo k with ⟨l, lb, kl⟩
Proof state after:
case h.h.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k l : ℕ
lb : l ≤ b
kl : g k = g l
⊢ Complex.abs (g k) ≤ (partialSups fun k => Complex.abs (g k)) b
Theorem: multibrot_of_repeat
Proof state before:
case h.h.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k l : ℕ
lb : l ≤ b
kl : g k = g l
⊢ Complex.abs (g k) ≤ (partialSups fun k => Complex.abs (g k)) b
Tactic:
rw [kl]
Proof state after:
case h.h.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k l : ℕ
lb : l ≤ b
kl : g k = g l
⊢ Complex.abs (g l) ≤ (partialSups fun k => Complex.abs (g k)) b
Theorem: multibrot_of_repeat
Proof state before:
case h.h.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
lo : ∀ (n : ℕ), ∃ k ≤ b, g n = g k
k l : ℕ
lb : l ≤ b
kl : g k = g l
⊢ Complex.abs (g l) ≤ (partialSups fun k => Complex.abs (g k)) b
Tactic:
exact le_partialSups_of_le (fun k ↦ abs (g k)) lb
Proof state after:
no goals
Theorem: multibrot_of_repeat
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
h : (f d c)^[a] ↑c = (f d c)^[b] ↑c
g : ℕ → ℂ
hg : (fun n => (f' d c)^[n] c) = g
n : ℕ
⊢ (f' d c)^[n] c = g n
Tactic:
rw [← hg]
Proof state after:
no goals
Theorem: multibrot_of_repeat
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
⊢ ∀ (n : ℕ), ∃ k ≤ b, g n = g k
Tactic:
intro n
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n : ℕ
⊢ ∃ k ≤ b, g n = g k
Theorem: multibrot_of_repeat
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n : ℕ
⊢ ∃ k ≤ b, g n = g k
Tactic:
induction' n with n h
Proof state after:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
⊢ ∃ k ≤ b, g 0 = g k

case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h✝ : g a = g b
n : ℕ
h : ∃ k ≤ b, g n = g k
⊢ ∃ k ≤ b, g (n + 1) = g k
Theorem: multibrot_of_repeat
Proof state before:
case zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
⊢ ∃ k ≤ b, g 0 = g k
Tactic:
use 0, Nat.zero_le _
Proof state after:
no goals
Theorem: multibrot_of_repeat
Proof state before:
case succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h✝ : g a = g b
n : ℕ
h : ∃ k ≤ b, g n = g k
⊢ ∃ k ≤ b, g (n + 1) = g k
Tactic:
rcases h with ⟨k, kb, nk⟩
Proof state after:
case succ.intro.intro
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
a b : ℕ
ab : a < b
g : ℕ → ℂ
hg : ∀ (n : ℕ), (f' d c)^[n] c = g n
h : g a = g b
n k : ℕ
kb : k ≤ b
nk : g n = g k
⊢ ∃ k ≤ b, g (n + 1) = g k