internlm/Lean-Github huggingface dataset:
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case h.e'_2.h.e'_13
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ ↑z = (↑z⁻¹)⁻¹

c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ z⁻¹ ∈ t
Tactic:
rw [inv_coe (inv_ne_zero z0'), inv_inv]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ z⁻¹ ∈ t
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
e : EqOn (fun z => s.bottcher c (↑z)⁻¹) (bottcherNear (fl (f d) ∞ c) d) t
z0' : z ≠ 0
⊢ z⁻¹ ∈ t
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero, map_inv₀, inv_le_inv z0 c0, cz, t]
Proof state after:
no goals
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
⊢ HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
Tactic:
intro z m
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : z ∈ t
⊢ HolomorphicAt I I (fun z => s.bottcher c (↑z)⁻¹) z
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : z ∈ t
⊢ HolomorphicAt I I (fun z => s.bottcher c (↑z)⁻¹) z
Tactic:
refine (s.bottcher_holomorphicOn _ ?_).along_snd.comp (holomorphic_inv.comp holomorphic_coe _)
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : z ∈ t
⊢ (c, (↑z)⁻¹) ∈ s.post
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : z ∈ t
⊢ (c, (↑z)⁻¹) ∈ s.post
Tactic:
simp only [mem_closedBall, Complex.dist_eq, sub_zero, t] at m
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ (c, (↑z)⁻¹) ∈ s.post
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ (c, (↑z)⁻¹) ∈ s.post
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post
Tactic:
simp only [z0, coe_zero, inv_zero']
Proof state after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : z = 0
⊢ (c, ∞) ∈ s.post

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : z = 0
⊢ (c, ∞) ∈ s.post

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post
Tactic:
exact s.post_a c
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, (↑z)⁻¹) ∈ s.post
Tactic:
rw [inv_coe z0]
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, ↑z⁻¹) ∈ s.post
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ (c, ↑z⁻¹) ∈ s.post
Tactic:
refine postcritical_large (by linarith) ?_
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ Complex.abs (c, ↑z⁻¹).1 ≤ Complex.abs z⁻¹
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ Complex.abs (c, ↑z⁻¹).1 ≤ Complex.abs z⁻¹
Tactic:
rwa [map_inv₀, le_inv c0]
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ 0 < Complex.abs z
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ 0 < Complex.abs z
Tactic:
exact Complex.abs.pos z0
Proof state after:
no goals
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0✝ : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
z0 : ¬z = 0
⊢ 4 ≤ Complex.abs (c, ↑z⁻¹).1
Tactic:
linarith
Proof state after:
no goals
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
⊢ HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
Tactic:
intro z m
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ HolomorphicAt I I (bottcherNear (fl (f d) ∞ c) d) z
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ HolomorphicAt I I (bottcherNear (fl (f d) ∞ c) d) z
Tactic:
apply AnalyticAt.holomorphicAt
Proof state after:
case fa
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ AnalyticAt ℂ (bottcherNear (fl (f d) ∞ c) d) z
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case fa
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ AnalyticAt ℂ (bottcherNear (fl (f d) ∞ c) d) z
Tactic:
apply bottcherNear_analytic_z (superNearF d c)
Proof state after:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : z ∈ t
⊢ z ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Tactic:
simp only [mem_setOf, mem_closedBall, Complex.dist_eq, sub_zero, t] at m ⊢
Proof state after:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹
Tactic:
refine lt_of_le_of_lt m ?_
Proof state after:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ (Complex.abs c)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ (Complex.abs c)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹
Tactic:
refine inv_lt_inv_of_lt (lt_of_lt_of_le (by norm_num) (le_max_left _ _)) ?_
Proof state after:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ max 16 (Complex.abs c / 2) < Complex.abs c
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
case fa.a
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ max 16 (Complex.abs c / 2) < Complex.abs c
Tactic:
exact max_lt c16 (half_lt_self (lt_trans (by norm_num) c16))
Proof state after:
no goals
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z✝ : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z✝
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z✝
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
z : ℂ
m : Complex.abs z ≤ (Complex.abs c)⁻¹
⊢ 0 < 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ 0 ≤ (Complex.abs c)⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
⊢ ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
Tactic:
simp only [Super.bottcherNear, extChartAt_inf_apply, inv_inv, toComplex_coe,
  RiemannSphere.inv_inf, toComplex_zero, sub_zero, Super.fl, eq_self_iff_true,
  Filter.eventually_true]
Proof state after:
no goals
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
⊢ Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
Tactic:
have h : ContinuousAt (fun z : ℂ ↦ (z : 𝕊)⁻¹) 0 :=
  (RiemannSphere.continuous_inv.comp continuous_coe).continuousAt
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
h : ContinuousAt (fun z => (↑z)⁻¹) 0
⊢ Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
h : ContinuousAt (fun z => (↑z)⁻¹) 0
⊢ Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
Tactic:
simp only [ContinuousAt, coe_zero, inv_zero'] at h
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
h : Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
⊢ Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
Theorem: bottcher_eq_bottcherNear_z
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
c0 : 0 < Complex.abs c
z0 : 0 < Complex.abs z
s : Super (f d) d ∞ := superF d
t : Set ℂ := closedBall 0 (Complex.abs c)⁻¹
a0 : HolomorphicOn I I (fun z => s.bottcher c (↑z)⁻¹) t
a1 : HolomorphicOn I I (bottcherNear (fl (f d) ∞ c) d) t
e : ∀ᶠ (z : ℂ) in 𝓝 0, bottcherNear (fl (f d) ∞ c) d z = s.bottcherNear c (↑z)⁻¹
h : Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
⊢ Tendsto (fun z => (↑z)⁻¹) (𝓝 0) (𝓝 ∞)
Tactic:
exact h
Proof state after:
no goals
Theorem: inv_mem_t
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ z⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Tactic:
simp only [mem_setOf, map_inv₀]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ (Complex.abs z)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹
Theorem: inv_mem_t
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ (Complex.abs z)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹
Tactic:
refine inv_lt_inv_of_lt (lt_of_lt_of_le (by norm_num) (le_max_left _ _)) ?_
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ max 16 (Complex.abs c / 2) < Complex.abs z
Theorem: inv_mem_t
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ max 16 (Complex.abs c / 2) < Complex.abs z
Tactic:
exact lt_of_lt_of_le (max_lt c16 (half_lt_self (lt_trans (by norm_num) c16))) cz
Proof state after:
no goals
Theorem: inv_mem_t
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ 0 < 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
set s := superF d
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have z0 : abs z ≠ 0 := (lt_of_lt_of_le (lt_trans (by norm_num) c16) cz).ne'
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Theorem: term_approx
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹
Tactic:
have i8 : (abs z)⁻¹ ≤ 1 / 8 := by
  rw [one_div]; apply inv_le_inv_of_le; norm_num
  exact le_trans (by norm_num) (le_trans c16.le cz)
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
n : ℕ
s : Super (f d) d ∞ := superF d
z0 : Complex.abs z ≠ 0
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 2 * (1 / 2) ^ n * (Complex.abs z)⁻¹