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

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⟩
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

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

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

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⟩
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

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

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 ⊢
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))

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 : 1 ≤ Complex.abs (bottcherNear f d z)
⊢ 1 ≤ Complex.abs (bottcherNear f d (f^[n] z))
Tactic:
simp only [bottcherNear_eqn_iter s zt n, Complex.abs.map_pow, one_le_pow_of_one_le b]
State after:
no goals

State before:
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
⊢ ∀ᶠ (n : ℕ) in atTop, Complex.abs (bottcherNear f d (f^[n] z)) < 1
Tactic:
refine (Metric.tendsto_nhds.mp (iterates_tendsto s zt) r rp).mp
    (Filter.eventually_of_forall fun n h ↦ ?_)
State after:
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
n : ℕ
h : dist (f^[n] z) 0 < r
⊢ Complex.abs (bottcherNear f d (f^[n] z)) < 1

State before:
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
n : ℕ
h : dist (f^[n] z) 0 < r
⊢ Complex.abs (bottcherNear f d (f^[n] z)) < 1
Tactic:
rw [Complex.dist_eq, sub_zero] at h
State after:
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
n : ℕ
h : Complex.abs (f^[n] z) < r
⊢ Complex.abs (bottcherNear f d (f^[n] z)) < 1

State before:
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
n : ℕ
h : Complex.abs (f^[n] z) < r
⊢ Complex.abs (bottcherNear f d (f^[n] z)) < 1
Tactic:
exact rs h
State after:
no goals