Theorem: term_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 => term (f c) d n z) c
Tactic:
refine AnalyticAt.cpow ?_ analyticAt_const ?_
State after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => g (f c) d ((f c)^[n] z)) c

case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ g (f c) d ((f c)^[n] z) ∈ Complex.slitPlane

State before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ AnalyticAt ℂ (fun c => g (f c) d ((f c)^[n] z)) c
Tactic:
have e : (fun c ↦ g (f c) d ((f c)^[n] z)) = fun c ↦ g2 f d (c, (f c)^[n] z) := rfl
State after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => g (f c) d ((f c)^[n] z)) c

State before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => g (f c) d ((f c)^[n] z)) c
Tactic:
rw [e]
State after:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => g2 f d (c, (f c)^[n] z)) c

State before:
case refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => g2 f d (c, (f c)^[n] z)) c
Tactic:
refine (s.ga _ ?_).comp ?_
State after:
case refine_1.refine_1
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ (c, (f c)^[n] z) ∈ t

case refine_1.refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => (c, (f c)^[n] z)) c

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

State before:
case refine_1.refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
e : (fun c => g (f c) d ((f c)^[n] z)) = fun c => g2 f d (c, (f c)^[n] z)
⊢ AnalyticAt ℂ (fun c => (c, (f c)^[n] z)) c
Tactic:
apply (analyticAt_id _ _).prod (iterates_analytic_c s n m)
State after:
no goals

State before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ g (f c) d ((f c)^[n] z) ∈ Complex.slitPlane
Tactic:
refine mem_slitPlane_of_near_one ?_
State after:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ Complex.abs (g (f c) d ((f c)^[n] z) - 1) < 1

State before:
case refine_2
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ Complex.abs (g (f c) d ((f c)^[n] z) - 1) < 1
Tactic:
exact lt_of_le_of_lt ((s.ts m).gs ((s.ts m).mapsTo n m)) (by norm_num)
State after:
no goals

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperNearC f d u t
c z : ℂ
n : ℕ
m : (c, z) ∈ t
⊢ 1 / 4 < 1
Tactic:
norm_num
State after:
no goals