internlm/Lean-Github huggingface dataset:
Theorem: Postcritical.not_precritical
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s : Super f d a
p0 : s.potential c z ≠ 0
n : ℕ
p : Critical (f c) ((f c)^[n] z)
⊢ s.potential c z ^ d ^ n ≤ s.potential c z
Tactic:
exact pow_le_of_le_one s.potential_nonneg s.potential_le_one (pow_ne_zero _ s.d0)
Proof state after:
no goals
Theorem: Postcritical.not_precritical'
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s : Super f d a
p : Postcritical s c z
za : z ≠ a
inst✝ : OnePreimage s
⊢ ¬Precritical (f c) z
Tactic:
apply p.not_precritical
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s : Super f d a
p : Postcritical s c z
za : z ≠ a
inst✝ : OnePreimage s
⊢ s.potential c z ≠ 0
Theorem: Postcritical.not_precritical'
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s : Super f d a
p : Postcritical s c z
za : z ≠ a
inst✝ : OnePreimage s
⊢ s.potential c z ≠ 0
Tactic:
simp only [Ne, s.potential_eq_zero_of_onePreimage]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s : Super f d a
p : Postcritical s c z
za : z ≠ a
inst✝ : OnePreimage s
⊢ ¬z = a
Theorem: Postcritical.not_precritical'
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s : Super f d a
p : Postcritical s c z
za : z ≠ a
inst✝ : OnePreimage s
⊢ ¬z = a
Tactic:
exact za
Proof state after:
no goals
Theorem: Super.isOpen_post
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
⊢ IsOpen s.post
Tactic:
set f := fun x : ℂ × S ↦ s.p x.1 - s.potential x.1 x.2
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
⊢ IsOpen s.post
Theorem: Super.isOpen_post
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
⊢ IsOpen s.post
Tactic:
have fc : LowerSemicontinuous f :=
  (s.lowerSemicontinuous_p.comp continuous_fst).add
    (Continuous.potential s).neg.lowerSemicontinuous
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
⊢ IsOpen s.post
Theorem: Super.isOpen_post
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
⊢ IsOpen s.post
Tactic:
have e : s.post = f ⁻¹' Ioi 0 :=
  Set.ext fun _ ↦ by
    simp only [Super.post, mem_setOf, Postcritical, mem_preimage, mem_Ioi, sub_pos, f]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
e : s.post = f ⁻¹' Ioi 0
⊢ IsOpen s.post
Theorem: Super.isOpen_post
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
e : s.post = f ⁻¹' Ioi 0
⊢ IsOpen s.post
Tactic:
rw [e]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
e : s.post = f ⁻¹' Ioi 0
⊢ IsOpen (f ⁻¹' Ioi 0)
Theorem: Super.isOpen_post
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
e : s.post = f ⁻¹' Ioi 0
⊢ IsOpen (f ⁻¹' Ioi 0)
Tactic:
exact fc.isOpen_preimage _
Proof state after:
no goals
Theorem: Super.isOpen_post
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f✝ : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f✝ d a
inst✝ : OnePreimage s
f : ℂ × S → ℝ := fun x => s.p x.1 - s.potential x.1 x.2
fc : LowerSemicontinuous f
x✝ : ℂ × S
⊢ x✝ ∈ s.post ↔ x✝ ∈ f ⁻¹' Ioi 0
Tactic:
simp only [Super.post, mem_setOf, Postcritical, mem_preimage, mem_Ioi, sub_pos, f]
Proof state after:
no goals
Theorem: Postcritical.eventually
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s : Super f d a
p : Postcritical s c z
inst✝ : OnePreimage s
⊢ ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), Postcritical s p.1 p.2
Tactic:
refine (s.isOpen_post.eventually_mem ?_).mp (eventually_of_forall fun _ m ↦ m)
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s : Super f d a
p : Postcritical s c z
inst✝ : OnePreimage s
⊢ (c, z) ∈ s.post
Theorem: Postcritical.eventually
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s : Super f d a
p : Postcritical s c z
inst✝ : OnePreimage s
⊢ (c, z) ∈ s.post
Tactic:
exact p
Proof state after:
no goals
Theorem: Super.post_a
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ (c, a) ∈ s.post
Tactic:
simp only [Super.post, Postcritical, s.potential_a, mem_setOf]
Proof state after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ 0 < s.p c
Theorem: Super.post_a
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
c : ℂ
⊢ 0 < s.p c
Tactic:
exact s.p_pos c
Proof state after:
no goals
Theorem: Super.stays_post
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
⊢ (p.1, f p.1 p.2) ∈ s.post
Tactic:
rcases p with ⟨c, z⟩
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ ((c, z).1, f (c, z).1 (c, z).2) ∈ s.post
Theorem: Super.stays_post
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ ((c, z).1, f (c, z).1 (c, z).2) ∈ s.post
Tactic:
simp only [Super.post, mem_setOf, Postcritical, s.potential_eqn]
Proof state after:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ s.potential c z ^ d < s.p c
Theorem: Super.stays_post
Proof state before:
case mk
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ z0 z1 : S
d n : ℕ
s✝ s : Super f d a
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ s.potential c z ^ d < s.p c
Tactic:
exact lt_of_le_of_lt (pow_le_of_le_one s.potential_nonneg s.potential_le_one s.d0) m
Proof state after:
no goals
Theorem: Super.iter_stays_post
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
⊢ (p.1, (f p.1)^[n] p.2) ∈ s.post
Tactic:
induction' n with n h
Proof state after:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
⊢ (p.1, (f p.1)^[0] p.2) ∈ s.post

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post
Theorem: Super.iter_stays_post
Proof state before:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
⊢ (p.1, (f p.1)^[0] p.2) ∈ s.post

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post
Tactic:
simp only [Function.iterate_zero_apply]
Proof state after:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
⊢ (p.1, p.2) ∈ s.post

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post
Theorem: Super.iter_stays_post
Proof state before:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
⊢ (p.1, p.2) ∈ s.post

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post
Tactic:
exact m
Proof state after:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post
Theorem: Super.iter_stays_post
Proof state before:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, (f p.1)^[n + 1] p.2) ∈ s.post
Tactic:
simp only [Function.iterate_succ_apply']
Proof state after:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, f p.1 ((f p.1)^[n] p.2)) ∈ s.post
Theorem: Super.iter_stays_post
Proof state before:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
p : ℂ × S
m : p ∈ s.post
n : ℕ
h : (p.1, (f p.1)^[n] p.2) ∈ s.post
⊢ (p.1, f p.1 ((f p.1)^[n] p.2)) ∈ s.post
Tactic:
exact s.stays_post h
Proof state after:
no goals
Theorem: Super.basin_post
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post
Tactic:
rcases tendsto_atTop_nhds.mp (s.basin_attracts m) {z | (c, z) ∈ s.post} (s.post_a c)
    (s.isOpen_post.snd_preimage c) with ⟨n, h⟩
Proof state after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : ∀ (n_1 : ℕ), n ≤ n_1 → (f c)^[n_1] z ∈ {z | (c, z) ∈ s.post}
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post
Theorem: Super.basin_post
Proof state before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : ∀ (n_1 : ℕ), n ≤ n_1 → (f c)^[n_1] z ∈ {z | (c, z) ∈ s.post}
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post
Tactic:
specialize h n (le_refl n)
Proof state after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : (f c)^[n] z ∈ {z | (c, z) ∈ s.post}
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post
Theorem: Super.basin_post
Proof state before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : (f c)^[n] z ∈ {z | (c, z) ∈ s.post}
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post
Tactic:
simp only [mem_setOf] at h
Proof state after:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : (c, (f c)^[n] z) ∈ s.post
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post
Theorem: Super.basin_post
Proof state before:
case intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n✝ : ℕ
s✝ s : Super f d a
inst✝ : OnePreimage s
m : (c, z) ∈ s.basin
n : ℕ
h : (c, (f c)^[n] z) ∈ s.post
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.post
Tactic:
use n, h
Proof state after:
no goals
Theorem: Super.bottcherNearIterNontrivial
Proof state before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z
Tactic:
rcases((Filter.eventually_ge_atTop n).and (s.eventually_noncritical ⟨_, r⟩)).exists with
  ⟨m, nm, mc⟩
Proof state after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z
Theorem: Super.bottcherNearIterNontrivial
Proof state before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z
Tactic:
have r' := s.iter_stays_near' r nm
Proof state after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z
Theorem: Super.bottcherNearIterNontrivial
Proof state before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : NontrivialHolomorphicAt (s.bottcherNearIter m c) z
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z
Tactic:
replace h := h.nonconst
Proof state after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z
Theorem: Super.bottcherNearIterNontrivial
Proof state before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z
⊢ NontrivialHolomorphicAt (s.bottcherNearIter n c) z
Tactic:
refine ⟨(s.bottcherNearIter_holomorphic r).along_snd, ?_⟩
Proof state after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z
⊢ ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter n c w ≠ s.bottcherNearIter n c z
Theorem: Super.bottcherNearIterNontrivial
Proof state before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z
⊢ ∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter n c w ≠ s.bottcherNearIter n c z
Tactic:
contrapose h
Proof state after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ¬∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter n c w ≠ s.bottcherNearIter n c z
⊢ ¬∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z
Theorem: Super.bottcherNearIterNontrivial
Proof state before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ¬∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter n c w ≠ s.bottcherNearIter n c z
⊢ ¬∃ᶠ (w : S) in 𝓝 z, s.bottcherNearIter m c w ≠ s.bottcherNearIter m c z
Tactic:
simp only [Filter.not_frequently, not_not] at h ⊢
Proof state after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z z0 z1 : S
d n : ℕ
s✝ s : Super f d a
r : (c, (f c)^[n] z) ∈ s.near
p : Postcritical s c z
inst✝ : OnePreimage s
m : ℕ
nm : n ≤ m
mc : mfderiv I I (s.bottcherNear c) ((f c)^[m] z) ≠ 0
r' : (c, (f c)^[m] z) ∈ s.near
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter m c x = s.bottcherNearIter m c z