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

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => (f c)^[n] z) c
Tactic:
induction' n with n nh
State after:
case zero
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => (f c)^[0] z) c

case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => (f c)^[n + 1] z) c

State before:
case zero
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => (f c)^[0] z) c
Tactic:
simp only [Function.iterate_zero, id]
State after:
case zero
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => z) c

State before:
case zero
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => z) c
Tactic:
exact analyticAt_const
State after:
no goals

State before:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => (f c)^[n + 1] z) c
Tactic:
simp_rw [Function.iterate_succ']
State after:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => (f c ∘ (f c)^[n]) z) c

State before:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => (f c ∘ (f c)^[n]) z) c
Tactic:
simp only [Function.comp_apply]
State after:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => f c ((f c)^[n] z)) c

State before:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ AnalyticAt ℂ (fun c => f c ((f c)^[n] z)) c
Tactic:
refine (s.fa _ ?_).comp ((analyticAt_id _ _).prod nh)
State after:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ (id c, (f c)^[n] z) ∈ t

State before:
case succ
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
m : (c, z) ∈ t
n : ℕ
nh : AnalyticAt ℂ (fun c => (f c)^[n] z) c
⊢ (id c, (f c)^[n] z) ∈ t
Tactic:
exact (s.ts m).mapsTo n m
State after:
no goals