internlm/Lean-Github huggingface dataset:
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 * (1 / 4) * (1 / 2 * (1 / 2) ^ n)
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 * (1 / 4) * (1 / 2 * (1 / 2) ^ n) = 1 / 2 * (1 / 2) ^ n
Tactic:
ring
Proof state after:
no goals
Theorem: term_nonzero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), z ∈ t → term f d n z ≠ 0
Tactic:
intro n zt
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ term f d n z ≠ 0
Theorem: term_nonzero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
⊢ term f d n z ≠ 0
Tactic:
have h := term_converges s n zt
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
⊢ term f d n z ≠ 0
Theorem: term_nonzero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
⊢ term f d n z ≠ 0
Tactic:
have o : 1 / 2 * (1 / 2 : ℝ) ^ n < 1 := by
  have p : (1 / 2 : ℝ) ^ n ≤ 1 := pow_le_one n (by norm_num) (by linarith)
  calc
    1 / 2 * (1 / 2 : ℝ) ^ n ≤ 1 / 2 * 1 := by linarith
    _ < 1 := by norm_num
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
o : 1 / 2 * (1 / 2) ^ n < 1
⊢ term f d n z ≠ 0
Theorem: term_nonzero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
o : 1 / 2 * (1 / 2) ^ n < 1
⊢ term f d n z ≠ 0
Tactic:
exact near_one_avoids_zero (lt_of_le_of_lt h o)
Proof state after:
no goals
Theorem: term_nonzero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 1 / 2 * (1 / 2) ^ n < 1
Tactic:
have p : (1 / 2 : ℝ) ^ n ≤ 1 := pow_le_one n (by norm_num) (by linarith)
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
p : (1 / 2) ^ n ≤ 1
⊢ 1 / 2 * (1 / 2) ^ n < 1
Theorem: term_nonzero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
p : (1 / 2) ^ n ≤ 1
⊢ 1 / 2 * (1 / 2) ^ n < 1
Tactic:
calc
  1 / 2 * (1 / 2 : ℝ) ^ n ≤ 1 / 2 * 1 := by linarith
  _ < 1 := by norm_num
Proof state after:
no goals
Theorem: term_nonzero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 0 ≤ 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_nonzero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
⊢ 1 / 2 ≤ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: term_nonzero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
p : (1 / 2) ^ n ≤ 1
⊢ 1 / 2 * (1 / 2) ^ n ≤ 1 / 2 * 1
Tactic:
linarith
Proof state after:
no goals
Theorem: term_nonzero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
zt : z ∈ t
h : Complex.abs (term f d n z - 1) ≤ 1 / 2 * (1 / 2) ^ n
p : (1 / 2) ^ n ≤ 1
⊢ 1 / 2 * 1 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_prod
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ProdExistsOn (term f d) t ∧ AnalyticOn ℂ (tprodOn (term f d)) t ∧ ∀ z ∈ t, tprodOn (term f d) z ≠ 0
Tactic:
have c12 : (1 / 2 : ℝ) ≤ 1 / 2 := by norm_num
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
⊢ ProdExistsOn (term f d) t ∧ AnalyticOn ℂ (tprodOn (term f d)) t ∧ ∀ z ∈ t, tprodOn (term f d) z ≠ 0
Theorem: term_prod
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
⊢ ProdExistsOn (term f d) t ∧ AnalyticOn ℂ (tprodOn (term f d)) t ∧ ∀ z ∈ t, tprodOn (term f d) z ≠ 0
Tactic:
have a0 : 0 ≤ (1 / 2 : ℝ) := by norm_num
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
⊢ ProdExistsOn (term f d) t ∧ AnalyticOn ℂ (tprodOn (term f d)) t ∧ ∀ z ∈ t, tprodOn (term f d) z ≠ 0
Theorem: term_prod
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
⊢ ProdExistsOn (term f d) t ∧ AnalyticOn ℂ (tprodOn (term f d)) t ∧ ∀ z ∈ t, tprodOn (term f d) z ≠ 0
Tactic:
exact fast_products_converge' s.o c12 a0 (by linarith) (term_analytic s)
  fun n z ↦ term_converges s n
Proof state after:
no goals
Theorem: term_prod
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ 1 / 2 ≤ 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_prod
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
⊢ 0 ≤ 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_prod
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
c12 : 1 / 2 ≤ 1 / 2
a0 : 0 ≤ 1 / 2
⊢ 1 / 2 < 1
Tactic:
linarith
Proof state after:
no goals
Theorem: bottcherNear_eqn
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ bottcherNear f d (f z) = bottcherNear f d z ^ d
Tactic:
simp_rw [bottcherNear]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ f z * ∏' (n : ℕ), term f d n (f z) = (z * ∏' (n : ℕ), term f d n z) ^ d
Theorem: bottcherNear_eqn
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ f z * ∏' (n : ℕ), term f d n (f z) = (z * ∏' (n : ℕ), term f d n z) ^ d
Tactic:
have pe := (term_prod_exists s) z zt
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe : ProdExists fun n => term f d n z
⊢ f z * ∏' (n : ℕ), term f d n (f z) = (z * ∏' (n : ℕ), term f d n z) ^ d
Theorem: bottcherNear_eqn
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe : ProdExists fun n => term f d n z
⊢ f z * ∏' (n : ℕ), term f d n (f z) = (z * ∏' (n : ℕ), term f d n z) ^ d
Tactic:
simp only [mul_pow, product_pow' pe]
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe : ProdExists fun n => term f d n z
⊢ f z * ∏' (n : ℕ), term f d n (f z) = z ^ d * ∏' (n : ℕ), term f d n z ^ d
Theorem: bottcherNear_eqn
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe : ProdExists fun n => term f d n z
⊢ f z * ∏' (n : ℕ), term f d n (f z) = z ^ d * ∏' (n : ℕ), term f d n z ^ d
Tactic:
have pe : ProdExists fun n ↦ term f d n z ^ d := by
  rcases pe with ⟨g, hg⟩; exact ⟨_, product_pow d hg⟩
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe✝ : ProdExists fun n => term f d n z
pe : ProdExists fun n => term f d n z ^ d
⊢ f z * ∏' (n : ℕ), term f d n (f z) = z ^ d * ∏' (n : ℕ), term f d n z ^ d
Theorem: bottcherNear_eqn
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe✝ : ProdExists fun n => term f d n z
pe : ProdExists fun n => term f d n z ^ d
⊢ f z * ∏' (n : ℕ), term f d n (f z) = z ^ d * ∏' (n : ℕ), term f d n z ^ d
Tactic:
simp only [product_split pe, ← term_eqn s, ← mul_assoc, ← mul_pow, ← term_base s]
Proof state after:
no goals
Theorem: bottcherNear_eqn
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
pe : ProdExists fun n => term f d n z
⊢ ProdExists fun n => term f d n z ^ d
Tactic:
rcases pe with ⟨g, hg⟩
Proof state after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
g : ℂ
hg : HasProd (fun n => term f d n z) g
⊢ ProdExists fun n => term f d n z ^ d
Theorem: bottcherNear_eqn
Proof state before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
g : ℂ
hg : HasProd (fun n => term f d n z) g
⊢ ProdExists fun n => term f d n z ^ d
Tactic:
exact ⟨_, product_pow d hg⟩
Proof state after:
no goals
Theorem: bottcherNear_eqn_iter
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
⊢ bottcherNear f d (f^[n] z) = bottcherNear f d z ^ d ^ n
Tactic:
induction' n with n h
Proof state after:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ bottcherNear f d (f^[0] z) = bottcherNear f d z ^ d ^ 0

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
h : bottcherNear f d (f^[n] z) = bottcherNear f d z ^ d ^ n
⊢ bottcherNear f d (f^[n + 1] z) = bottcherNear f d z ^ d ^ (n + 1)
Theorem: bottcherNear_eqn_iter
Proof state before:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ bottcherNear f d (f^[0] z) = bottcherNear f d z ^ d ^ 0

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
h : bottcherNear f d (f^[n] z) = bottcherNear f d z ^ d ^ n
⊢ bottcherNear f d (f^[n + 1] z) = bottcherNear f d z ^ d ^ (n + 1)
Tactic:
simp only [Function.iterate_zero, id, pow_zero, pow_one]
Proof state after:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
h : bottcherNear f d (f^[n] z) = bottcherNear f d z ^ d ^ n
⊢ bottcherNear f d (f^[n + 1] z) = bottcherNear f d z ^ d ^ (n + 1)
Theorem: bottcherNear_eqn_iter
Proof state before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
n : ℕ
h : bottcherNear f d (f^[n] z) = bottcherNear f d z ^ d ^ n
⊢ bottcherNear f d (f^[n + 1] z) = bottcherNear f d z ^ d ^ (n + 1)
Tactic:
simp only [Function.comp, Function.iterate_succ', pow_succ, pow_mul,
  bottcherNear_eqn s (s.mapsTo n zt), h]
Proof state after:
no goals
Theorem: iterates_at_zero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), f^[n] 0 = 0
Tactic:
intro n
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ f^[n] 0 = 0
Theorem: iterates_at_zero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ f^[n] 0 = 0
Tactic:
induction' n with n h
Proof state after:
case zero
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ f^[0] 0 = 0

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

case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : f^[n] 0 = 0
⊢ f^[n + 1] 0 = 0
Tactic:
simp only [Function.iterate_zero, id]
Proof state after:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : f^[n] 0 = 0
⊢ f^[n + 1] 0 = 0
Theorem: iterates_at_zero
Proof state before:
case succ
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
h : f^[n] 0 = 0
⊢ f^[n + 1] 0 = 0
Tactic:
simp only [Function.iterate_succ', Function.comp_apply, h, s.f0]
Proof state after:
no goals
Theorem: term_at_zero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
⊢ term f d n 0 = 1
Tactic:
simp only [term, iterates_at_zero s, g0, Complex.one_cpow]
Proof state after:
no goals
Theorem: term_prod_at_zero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ tprodOn (term f d) 0 = 1
Tactic:
simp_rw [tprodOn, term_at_zero s, tprod_one]
Proof state after:
no goals
Theorem: bottcherNear_monic
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ HasDerivAt (bottcherNear f d) 1 0
Tactic:
have dz : HasDerivAt (fun z : ℂ ↦ z) 1 0 := hasDerivAt_id 0
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Theorem: bottcherNear_monic
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Tactic:
have db := HasDerivAt.mul dz (term_prod_analytic_z s 0 s.t0).differentiableAt.hasDerivAt
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) (1 * tprodOn (term f d) 0 + 0 * deriv (tprodOn (term f d)) 0) 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Theorem: bottcherNear_monic
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) (1 * tprodOn (term f d) 0 + 0 * deriv (tprodOn (term f d)) 0) 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Tactic:
simp only [one_mul, MulZeroClass.zero_mul, add_zero] at db
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) (tprodOn (term f d) 0) 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Theorem: bottcherNear_monic
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) (tprodOn (term f d) 0) 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Tactic:
rw [term_prod_at_zero s] at db
Proof state after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) 1 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Theorem: bottcherNear_monic
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
dz : HasDerivAt (fun z => z) 1 0
db : HasDerivAt (fun y => y * tprodOn (term f d) y) 1 0
⊢ HasDerivAt (bottcherNear f d) 1 0
Tactic:
exact db
Proof state after:
no goals
Theorem: bottcherNear_zero
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
⊢ bottcherNear f d 0 = 0
Tactic:
simp only [bottcherNear, MulZeroClass.zero_mul]
Proof state after:
no goals
Theorem: iterates_tendsto
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)

case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)
Theorem: iterates_tendsto
Proof state before:
case pos
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)

case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)
Tactic:
simp only [z0, iterates_at_zero s, tendsto_const_nhds]
Proof state after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)
Theorem: iterates_tendsto
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ Tendsto (fun n => f^[n] z) atTop (𝓝 0)
Tactic:
rw [Metric.tendsto_atTop]
Proof state after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f^[n] z) 0 < ε
Theorem: iterates_tendsto
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (f^[n] z) 0 < ε
Tactic:
intro e ep
Proof state after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (f^[n] z) 0 < e
Theorem: iterates_tendsto
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (f^[n] z) 0 < e
Tactic:
simp only [Complex.dist_eq, sub_zero]
Proof state after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Theorem: iterates_tendsto
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Tactic:
have xp : e / abs z > 0 := div_pos ep (Complex.abs.pos z0)
Proof state after:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Theorem: iterates_tendsto
Proof state before:
case neg
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Tactic:
rcases exists_pow_lt_of_lt_one xp (by norm_num : (5 / 8 : ℝ) < 1) with ⟨N, Nb⟩
Proof state after:
case neg.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N < e / Complex.abs z
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Theorem: iterates_tendsto
Proof state before:
case neg.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N < e / Complex.abs z
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Tactic:
simp only [lt_div_iff (Complex.abs.pos z0)] at Nb
Proof state after:
case neg.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Theorem: iterates_tendsto
Proof state before:
case neg.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
⊢ ∃ N, ∀ n ≥ N, Complex.abs (f^[n] z) < e
Tactic:
use N
Proof state after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
⊢ ∀ n ≥ N, Complex.abs (f^[n] z) < e
Theorem: iterates_tendsto
Proof state before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
⊢ ∀ n ≥ N, Complex.abs (f^[n] z) < e
Tactic:
intro n nN
Proof state after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
n : ℕ
nN : n ≥ N
⊢ Complex.abs (f^[n] z) < e
Theorem: iterates_tendsto
Proof state before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
n : ℕ
nN : n ≥ N
⊢ Complex.abs (f^[n] z) < e
Tactic:
refine lt_of_le_of_lt (iterates_converge s n zt) (lt_of_le_of_lt ?_ Nb)
Proof state after:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
n : ℕ
nN : n ≥ N
⊢ (5 / 8) ^ n * Complex.abs z ≤ (5 / 8) ^ N * Complex.abs z
Theorem: iterates_tendsto
Proof state before:
case h
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
N : ℕ
Nb : (5 / 8) ^ N * Complex.abs z < e
n : ℕ
nN : n ≥ N
⊢ (5 / 8) ^ n * Complex.abs z ≤ (5 / 8) ^ N * Complex.abs z
Tactic:
bound
Proof state after:
no goals
Theorem: iterates_tendsto
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
z0 : ¬z = 0
e : ℝ
ep : e > 0
xp : e / Complex.abs z > 0
⊢ 5 / 8 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcherNear_lt_one
Proof state before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (bottcherNear f d z) < 1
Tactic:
rcases Metric.continuousAt_iff.mp (bottcherNear_analytic_z s _ s.t0).continuousAt 1 zero_lt_one
  with ⟨r, rp, rs⟩
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, dist x 0 < r → dist (bottcherNear f d x) (bottcherNear f d 0) < 1
⊢ Complex.abs (bottcherNear f d z) < 1
Theorem: bottcherNear_lt_one
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, dist x 0 < r → dist (bottcherNear f d x) (bottcherNear f d 0) < 1
⊢ Complex.abs (bottcherNear f d z) < 1
Tactic:
simp only [Complex.dist_eq, sub_zero, bottcherNear_zero] at rs
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
⊢ Complex.abs (bottcherNear f d z) < 1
Theorem: bottcherNear_lt_one
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
⊢ Complex.abs (bottcherNear f d z) < 1
Tactic:
have b' : ∀ᶠ n in atTop, abs (bottcherNear f d (f^[n] z)) < 1 := by
  refine (Metric.tendsto_nhds.mp (iterates_tendsto s zt) r rp).mp
      (Filter.eventually_of_forall fun n h ↦ ?_)
  rw [Complex.dist_eq, sub_zero] at h; exact rs h
Proof state after:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
b' : ∀ᶠ (n : ℕ) in atTop, Complex.abs (bottcherNear f d (f^[n] z)) < 1
⊢ Complex.abs (bottcherNear f d z) < 1
Theorem: bottcherNear_lt_one
Proof state before:
case intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
b' : ∀ᶠ (n : ℕ) in atTop, Complex.abs (bottcherNear f d (f^[n] z)) < 1
⊢ Complex.abs (bottcherNear f d z) < 1
Tactic:
rcases b'.exists with ⟨n, b⟩
Proof state after:
case intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
b' : ∀ᶠ (n : ℕ) in atTop, Complex.abs (bottcherNear f d (f^[n] z)) < 1
n : ℕ
b : Complex.abs (bottcherNear f d (f^[n] z)) < 1
⊢ Complex.abs (bottcherNear f d z) < 1
Theorem: bottcherNear_lt_one
Proof state before:
case intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
b' : ∀ᶠ (n : ℕ) in atTop, Complex.abs (bottcherNear f d (f^[n] z)) < 1
n : ℕ
b : Complex.abs (bottcherNear f d (f^[n] z)) < 1
⊢ Complex.abs (bottcherNear f d z) < 1
Tactic:
contrapose b
Proof state after:
case intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
b' : ∀ᶠ (n : ℕ) in atTop, Complex.abs (bottcherNear f d (f^[n] z)) < 1
n : ℕ
b : ¬Complex.abs (bottcherNear f d z) < 1
⊢ ¬Complex.abs (bottcherNear f d (f^[n] z)) < 1
Theorem: bottcherNear_lt_one
Proof state before:
case intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
b' : ∀ᶠ (n : ℕ) in atTop, Complex.abs (bottcherNear f d (f^[n] z)) < 1
n : ℕ
b : ¬Complex.abs (bottcherNear f d z) < 1
⊢ ¬Complex.abs (bottcherNear f d (f^[n] z)) < 1
Tactic:
simp only [not_lt] at b ⊢
Proof state after:
case intro.intro.intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
r : ℝ
rp : r > 0
rs : ∀ {x : ℂ}, Complex.abs x < r → Complex.abs (bottcherNear f d x) < 1
b' : ∀ᶠ (n : ℕ) in atTop, Complex.abs (bottcherNear f d (f^[n] z)) < 1
n : ℕ
b : 1 ≤ Complex.abs (bottcherNear f d z)
⊢ 1 ≤ Complex.abs (bottcherNear f d (f^[n] z))