internlm/Lean-Github huggingface dataset:
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ z ∈ t → Complex.abs (f z) ≤ 5 / 8 * Complex.abs z
Tactic:
intro zt
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (f z) ≤ 5 / 8 * Complex.abs z
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (f z) ≤ 5 / 8 * Complex.abs z
Tactic:
rw [s.fg]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (z ^ d * g f d z) ≤ 5 / 8 * Complex.abs z
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (z ^ d * g f d z) ≤ 5 / 8 * Complex.abs z
Tactic:
simp
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z
Tactic:
have gs : abs (g f d z) ≤ 5 / 4 := by
  calc abs (g f d z)
    _ = abs (g f d z - 1 + 1) := by ring_nf
    _ ≤ abs (g f d z - 1) + abs (1 : ℂ) := by bound
    _ ≤ 1 / 4 + abs (1 : ℂ) := by linarith [s.gs zt]
    _ ≤ 5 / 4 := by norm_num
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z
Tactic:
have az1 : abs z ≤ 1 := le_trans (s.t2 zt) (by norm_num)
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
az1 : Complex.abs z ≤ 1
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
az1 : Complex.abs z ≤ 1
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ 5 / 8 * Complex.abs z
Tactic:
calc abs z ^ d * abs (g f d z)
  _ ≤ abs z ^ 2 * (5 / 4) := by bound
  _ = abs z * abs z * (5 / 4) := by ring_nf
  _ ≤ 1 / 2 * abs z * (5 / 4) := by bound [s.t2 zt]
  _ = 5 / 8 * abs z := by ring
Proof state after:
no goals
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (g f d z) ≤ 5 / 4
Tactic:
calc abs (g f d z)
  _ = abs (g f d z - 1 + 1) := by ring_nf
  _ ≤ abs (g f d z - 1) + abs (1 : ℂ) := by bound
  _ ≤ 1 / 4 + abs (1 : ℂ) := by linarith [s.gs zt]
  _ ≤ 5 / 4 := by norm_num
Proof state after:
no goals
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (g f d z) = Complex.abs (g f d z - 1 + 1)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (g f d z - 1 + 1) ≤ Complex.abs (g f d z - 1) + Complex.abs 1
Tactic:
bound
Proof state after:
no goals
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (g f d z - 1) + Complex.abs 1 ≤ 1 / 4 + Complex.abs 1
Tactic:
linarith [s.gs zt]
Proof state after:
no goals
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ 1 / 4 + Complex.abs 1 ≤ 5 / 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
⊢ 1 / 2 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
az1 : Complex.abs z ≤ 1
⊢ Complex.abs z ^ d * Complex.abs (g f d z) ≤ Complex.abs z ^ 2 * (5 / 4)
Tactic:
bound
Proof state after:
no goals
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
az1 : Complex.abs z ≤ 1
⊢ Complex.abs z ^ 2 * (5 / 4) = Complex.abs z * Complex.abs z * (5 / 4)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
az1 : Complex.abs z ≤ 1
⊢ Complex.abs z * Complex.abs z * (5 / 4) ≤ 1 / 2 * Complex.abs z * (5 / 4)
Tactic:
bound [s.t2 zt]
Proof state after:
no goals
Theorem: f_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
gs : Complex.abs (g f d z) ≤ 5 / 4
az1 : Complex.abs z ≤ 1
⊢ 1 / 2 * Complex.abs z * (5 / 4) = 5 / 8 * Complex.abs z
Tactic:
ring
Proof state after:
no goals
Theorem: five_eights_pow_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
⊢ r > 0 → (5 / 8) ^ n * r ≤ r
Tactic:
intro rp
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ (5 / 8) ^ n * r ≤ r
Theorem: five_eights_pow_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ (5 / 8) ^ n * r ≤ r
Tactic:
trans (1:ℝ) ^ n * r
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ (5 / 8) ^ n * r ≤ 1 ^ n * r

f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ 1 ^ n * r ≤ r
Theorem: five_eights_pow_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ (5 / 8) ^ n * r ≤ 1 ^ n * r

f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ 1 ^ n * r ≤ r
Tactic:
bound
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ 1 ^ n * r ≤ r
Theorem: five_eights_pow_le
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
⊢ 1 ^ n * r ≤ r
Tactic:
simp only [one_pow, one_mul, le_refl]
Proof state after:
no goals
Theorem: five_eights_pow_lt
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
⊢ r > 0 → n ≠ 0 → (5 / 8) ^ n * r < r
Tactic:
intro rp np
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
⊢ (5 / 8) ^ n * r < r
Theorem: five_eights_pow_lt
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
⊢ (5 / 8) ^ n * r < r
Tactic:
have h : (5 / 8 : ℝ) ^ n < 1 := pow_lt_one (by norm_num) (by norm_num) np
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
h : (5 / 8) ^ n < 1
⊢ (5 / 8) ^ n * r < r
Theorem: five_eights_pow_lt
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
h : (5 / 8) ^ n < 1
⊢ (5 / 8) ^ n * r < r
Tactic:
exact lt_of_lt_of_le (mul_lt_mul_of_pos_right h rp) (by simp only [one_mul, le_refl])
Proof state after:
no goals
Theorem: five_eights_pow_lt
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
⊢ 0 ≤ 5 / 8
Tactic:
norm_num
Proof state after:
no goals
Theorem: five_eights_pow_lt
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
⊢ 5 / 8 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: five_eights_pow_lt
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
n : ℕ
r : ℝ
rp : r > 0
np : n ≠ 0
h : (5 / 8) ^ n < 1
⊢ 1 * r ≤ r
Tactic:
simp only [one_mul, le_refl]
Proof state after:
no goals
Theorem: SuperNear.mapsTo
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ MapsTo f^[n] t t
Tactic:
induction' n with n h
Proof state after:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ MapsTo f^[0] t t

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : MapsTo f^[n] t t
⊢ MapsTo f^[n + 1] t t
Theorem: SuperNear.mapsTo
Proof state before:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ MapsTo f^[0] t t

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : MapsTo f^[n] t t
⊢ MapsTo f^[n + 1] t t
Tactic:
simp only [Set.mapsTo_id, Function.iterate_zero]
Proof state after:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : MapsTo f^[n] t t
⊢ MapsTo f^[n + 1] t t
Theorem: SuperNear.mapsTo
Proof state before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : MapsTo f^[n] t t
⊢ MapsTo f^[n + 1] t t
Tactic:
rw [Function.iterate_succ']
Proof state after:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : MapsTo f^[n] t t
⊢ MapsTo (f ∘ f^[n]) t t
Theorem: SuperNear.mapsTo
Proof state before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : MapsTo f^[n] t t
⊢ MapsTo (f ∘ f^[n]) t t
Tactic:
exact s.ft.comp h
Proof state after:
no goals
Theorem: iterates_converge
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), z ∈ t → Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
Tactic:
intro n zt
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
Theorem: iterates_converge
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
Tactic:
induction' n with n nh
Proof state after:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (f^[0] z) ≤ (5 / 8) ^ 0 * Complex.abs z

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs (f^[n + 1] z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z
Theorem: iterates_converge
Proof state before:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (f^[0] z) ≤ (5 / 8) ^ 0 * Complex.abs z
Tactic:
simp only [Function.iterate_zero, id, pow_zero, one_mul, Nat.cast_one, le_refl]
Proof state after:
no goals
Theorem: iterates_converge
Proof state before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs (f^[n + 1] z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z
Tactic:
rw [Function.iterate_succ']
Proof state after:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs ((f ∘ f^[n]) z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z
Theorem: iterates_converge
Proof state before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs ((f ∘ f^[n]) z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z
Tactic:
trans (5/8 : ℝ) * abs (f^[n] z)
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs ((f ∘ f^[n]) z) ≤ 5 / 8 * Complex.abs (f^[n] z)

f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ 5 / 8 * Complex.abs (f^[n] z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z
Theorem: iterates_converge
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ Complex.abs ((f ∘ f^[n]) z) ≤ 5 / 8 * Complex.abs (f^[n] z)
Tactic:
exact f_converges s (s.mapsTo n zt)
Proof state after:
no goals
Theorem: iterates_converge
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ 5 / 8 * Complex.abs (f^[n] z) ≤ (5 / 8) ^ (n + 1) * Complex.abs z
Tactic:
calc (5/8 : ℝ) * abs (f^[n] z)
  _ ≤ (5/8 : ℝ) * ((5/8 : ℝ) ^ n * abs z) := by bound
  _ = 5/8 * (5/8 : ℝ) ^ n * abs z := by ring
  _ = (5/8 : ℝ) ^ (n + 1) * abs z := by rw [← pow_succ']
  _ = (5/8 : ℝ) ^ n.succ * abs z := rfl
Proof state after:
no goals
Theorem: iterates_converge
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ 5 / 8 * Complex.abs (f^[n] z) ≤ 5 / 8 * ((5 / 8) ^ n * Complex.abs z)
Tactic:
bound
Proof state after:
no goals
Theorem: iterates_converge
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ 5 / 8 * ((5 / 8) ^ n * Complex.abs z) = 5 / 8 * (5 / 8) ^ n * Complex.abs z
Tactic:
ring
Proof state after:
no goals
Theorem: iterates_converge
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
nh : Complex.abs (f^[n] z) ≤ (5 / 8) ^ n * Complex.abs z
⊢ 5 / 8 * (5 / 8) ^ n * Complex.abs z = (5 / 8) ^ (n + 1) * Complex.abs z
Tactic:
rw [← pow_succ']
Proof state after:
no goals
Theorem: iterates_analytic
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), AnalyticOn ℂ f^[n] t
Tactic:
intro n
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ AnalyticOn ℂ f^[n] t
Theorem: iterates_analytic
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ AnalyticOn ℂ f^[n] t
Tactic:
induction' n with n h
Proof state after:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ AnalyticOn ℂ f^[0] t

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : AnalyticOn ℂ f^[n] t
⊢ AnalyticOn ℂ f^[n + 1] t
Theorem: iterates_analytic
Proof state before:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ AnalyticOn ℂ f^[0] t
Tactic:
simp only [Function.iterate_zero]
Proof state after:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ AnalyticOn ℂ id t
Theorem: iterates_analytic
Proof state before:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ AnalyticOn ℂ id t
Tactic:
exact analyticOn_id _
Proof state after:
no goals
Theorem: iterates_analytic
Proof state before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : AnalyticOn ℂ f^[n] t
⊢ AnalyticOn ℂ f^[n + 1] t
Tactic:
rw [Function.iterate_succ']
Proof state after:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : AnalyticOn ℂ f^[n] t
⊢ AnalyticOn ℂ (f ∘ f^[n]) t
Theorem: iterates_analytic
Proof state before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : AnalyticOn ℂ f^[n] t
⊢ AnalyticOn ℂ (f ∘ f^[n]) t
Tactic:
intro z zt
Proof state after:
case succ
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : AnalyticOn ℂ f^[n] t
z : ℂ
zt : z ∈ t
⊢ AnalyticAt ℂ (f ∘ f^[n]) z
Theorem: iterates_analytic
Proof state before:
case succ
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : AnalyticOn ℂ f^[n] t
z : ℂ
zt : z ∈ t
⊢ AnalyticAt ℂ (f ∘ f^[n]) z
Tactic:
exact (s.fa _ (s.mapsTo n zt)).comp (h z zt)
Proof state after:
no goals
Theorem: term_analytic
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), AnalyticOn ℂ (term f d n) t
Tactic:
intro n z zt
Proof state after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
z : ℂ
zt : z ∈ t
⊢ AnalyticAt ℂ (term f d n) z
Theorem: term_analytic
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
z : ℂ
zt : z ∈ t
⊢ AnalyticAt ℂ (term f d n) z
Tactic:
refine AnalyticAt.cpow ?_ analyticAt_const ?_
Proof state after:
case refine_1
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
z : ℂ
zt : z ∈ t
⊢ AnalyticAt ℂ (fun z => g f d (f^[n] z)) z

case refine_2
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
z : ℂ
zt : z ∈ t
⊢ g f d (f^[n] z) ∈ Complex.slitPlane
Theorem: term_analytic
Proof state before:
case refine_1
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
z : ℂ
zt : z ∈ t
⊢ AnalyticAt ℂ (fun z => g f d (f^[n] z)) z
Tactic:
exact (s.ga _ (s.mapsTo n zt)).comp (iterates_analytic s n z zt)
Proof state after:
no goals
Theorem: term_analytic
Proof state before:
case refine_2
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
z : ℂ
zt : z ∈ t
⊢ g f d (f^[n] z) ∈ Complex.slitPlane
Tactic:
exact mem_slitPlane_of_near_one (lt_of_le_of_lt (s.gs (s.mapsTo n zt)) (by norm_num))
Proof state after:
no goals
Theorem: term_analytic
Proof state before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
z : ℂ
zt : z ∈ t
⊢ 1 / 4 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), z ∈ t → Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
intro n zt
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
rw [term]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 1 / 2 * (1 / 2) ^ n
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
trans 4 * abs (g f d (f^[n] z) - 1) * abs (1 / (d ^ (n + 1) : ℕ) : ℂ)
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1)))

f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) ^ (1 / ↑(d ^ (n + 1))) - 1) ≤
    4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1)))
Tactic:
apply pow_small
Proof state after:
case zs
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 2

case ws
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1
Theorem: term_converges
Proof state before:
case zs
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 2
Tactic:
exact le_trans (s.gs (s.mapsTo n zt)) (by norm_num)
Proof state after:
no goals
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 1 / 4 ≤ 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_converges
Proof state before:
case ws
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1
Tactic:
simp only [one_div, map_inv₀, Complex.abs_pow, Complex.abs_natCast, Nat.cast_pow]
Proof state after:
case ws
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ (↑d ^ (n + 1))⁻¹ ≤ 1
Theorem: term_converges
Proof state before:
case ws
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ (↑d ^ (n + 1))⁻¹ ≤ 1
Tactic:
apply inv_le_one
Proof state after:
case ws.ha
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 1 ≤ ↑d ^ (n + 1)
Theorem: term_converges
Proof state before:
case ws.ha
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 1 ≤ ↑d ^ (n + 1)
Tactic:
have hd : 1 ≤ (d : ℝ) := le_trans (by norm_num) s.dr2
Proof state after:
case ws.ha
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
hd : 1 ≤ ↑d
⊢ 1 ≤ ↑d ^ (n + 1)
Theorem: term_converges
Proof state before:
case ws.ha
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
hd : 1 ≤ ↑d
⊢ 1 ≤ ↑d ^ (n + 1)
Tactic:
exact one_le_pow_of_one_le hd _
Proof state after:
no goals
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 1 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
have gs : abs (g f d (f^[n] z) - 1) ≤ 1 / 4 := s.gs (s.mapsTo n zt)
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
have ps : abs (1 / (d:ℂ) ^ (n + 1) : ℂ) ≤ 1/2 * (1/2 : ℝ) ^ n := by
  have nn : (1/2:ℝ) * (1/2 : ℝ) ^ n = (1/2 : ℝ) ^ (n + 1) := (pow_succ' _ _).symm
  rw [nn]
  simp only [one_div, map_inv₀, map_pow, Complex.abs_natCast, inv_pow, ge_iff_le]
  bound
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
ps : Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
ps : Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
calc (4:ℝ) * abs (g f d (f^[n] z) - 1) * abs ((1:ℂ) / (d ^ (n + 1) : ℕ) : ℂ)
  _ = (4:ℝ) * abs (g f d (f^[n] z) - 1) * abs ((1:ℂ) / (d:ℂ) ^ (n + 1) : ℂ) := by
    rw [Nat.cast_pow]
  _ ≤ 4 * (1 / 4) * (1 / 2 * (1 / 2 : ℝ) ^ n) := by bound
  _ = 1 / 2 * (1 / 2 : ℝ) ^ n := by ring
Proof state after:
no goals
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
⊢ Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
have nn : (1/2:ℝ) * (1/2 : ℝ) ^ n = (1/2 : ℝ) ^ (n + 1) := (pow_succ' _ _).symm
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
Tactic:
rw [nn]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ Complex.abs (1 / ↑d ^ (n + 1)) ≤ (1 / 2) ^ (n + 1)
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ Complex.abs (1 / ↑d ^ (n + 1)) ≤ (1 / 2) ^ (n + 1)
Tactic:
simp only [one_div, map_inv₀, map_pow, Complex.abs_natCast, inv_pow, ge_iff_le]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ (↑d ^ (n + 1))⁻¹ ≤ (2 ^ (n + 1))⁻¹
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
nn : 1 / 2 * (1 / 2) ^ n = (1 / 2) ^ (n + 1)
⊢ (↑d ^ (n + 1))⁻¹ ≤ (2 ^ (n + 1))⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: term_converges
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
gs : Complex.abs (g f d (f^[n] z) - 1) ≤ 1 / 4
ps : Complex.abs (1 / ↑d ^ (n + 1)) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑(d ^ (n + 1))) =
    4 * Complex.abs (g f d (f^[n] z) - 1) * Complex.abs (1 / ↑d ^ (n + 1))
Tactic:
rw [Nat.cast_pow]
Proof state after:
no goals