Theorem: term_analytic (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
⊢ ∀ (n : ℕ), AnalyticOn ℂ (term f d n) t
Tactic:
intro n z zt
State after:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
z : ℂ
zt : z ∈ t
⊢ AnalyticAt ℂ (term f d n) z

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 ?_
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

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)
State after:
no goals

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))
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z✝ : ℂ
t : Set ℂ
s : SuperNear f d t
n : ℕ
z : ℂ
zt : z ∈ t
⊢ 1 / 4 < 1
Tactic:
norm_num
State after:
no goals