internlm/Lean-Github huggingface dataset:
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 : ∀ᶠ (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
Tactic:
rw [← Nat.sub_add_cancel 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
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (m - n + n) c x = s.bottcherNearIter (m - n + 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 : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (m - n + n) c x = s.bottcherNearIter (m - n + n) c z
Tactic:
generalize hk : m - n = k
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
k : ℕ
hk : m - n = k
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + 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 : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
hk : m - n = k
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
clear hk nm mc r' p m
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
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + 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
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
have er : ∀ᶠ w in 𝓝 z, (c, (f c)^[n] w) ∈ s.near :=
  (continuousAt_const.prod (s.continuousAt_iter continuousAt_const
    continuousAt_id)).eventually_mem (s.isOpen_near.mem_nhds r)
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
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + 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
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
⊢ ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
refine (h.and er).mp (eventually_of_forall ?_)
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
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
⊢ ∀ (x : S),
    s.bottcherNearIter n c x = s.bottcherNearIter n c z ∧ (c, (f c)^[n] x) ∈ s.near →
      s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + 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
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
⊢ ∀ (x : S),
    s.bottcherNearIter n c x = s.bottcherNearIter n c z ∧ (c, (f c)^[n] x) ∈ s.near →
      s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
intro x ⟨e, m⟩
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
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
x : S
e : s.bottcherNearIter n c x = s.bottcherNearIter n c z
m : (c, (f c)^[n] x) ∈ s.near
⊢ s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + 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
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
x : S
e : s.bottcherNearIter n c x = s.bottcherNearIter n c z
m : (c, (f c)^[n] x) ∈ s.near
⊢ s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
simp only [Super.bottcherNearIter] at e
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
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
x : S
e : s.bottcherNear c ((f c)^[n] x) = s.bottcherNear c ((f c)^[n] z)
m : (c, (f c)^[n] x) ∈ s.near
⊢ s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + 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
inst✝ : OnePreimage s
h : ∀ᶠ (x : S) in 𝓝 z, s.bottcherNearIter n c x = s.bottcherNearIter n c z
k : ℕ
er : ∀ᶠ (w : S) in 𝓝 z, (c, (f c)^[n] w) ∈ s.near
x : S
e : s.bottcherNear c ((f c)^[n] x) = s.bottcherNear c ((f c)^[n] z)
m : (c, (f c)^[n] x) ∈ s.near
⊢ s.bottcherNearIter (k + n) c x = s.bottcherNearIter (k + n) c z
Tactic:
simp only [Super.bottcherNearIter, Function.iterate_add_apply, s.bottcherNear_eqn_iter m,
  s.bottcherNear_eqn_iter r, e]
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
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 m c) z
Tactic:
by_cases p0 : s.potential c z = 0
Proof state after:
case pos
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
p0 : s.potential c z = 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z

case neg
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
p0 : ¬s.potential c z = 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z
Theorem: Super.bottcherNearIterNontrivial
Proof state before:
case pos
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
p0 : s.potential c z = 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z
Tactic:
rw [s.potential_eq_zero_of_onePreimage] at p0
Proof state after:
case pos
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
p0 : z = a
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z
Theorem: Super.bottcherNearIterNontrivial
Proof state before:
case pos
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
p0 : z = a
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z
Tactic:
rw [p0]
Proof state after:
case pos
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
p0 : z = a
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) a
Theorem: Super.bottcherNearIterNontrivial
Proof state before:
case pos
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
p0 : z = a
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) a
Tactic:
exact s.bottcherNearIter_nontrivial_a
Proof state after:
no goals
Theorem: Super.bottcherNearIterNontrivial
Proof state before:
case neg
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
p0 : ¬s.potential c z = 0
⊢ NontrivialHolomorphicAt (s.bottcherNearIter m c) z
Tactic:
exact nontrivialHolomorphicAt_of_mfderiv_ne_zero (s.bottcherNearIter_holomorphic r').along_snd
    (s.bottcherNearIter_mfderiv_ne_zero mc (p.not_precritical p0))
Proof state after:
no goals
Theorem: Super.potential_minima_only_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
p : Postcritical s c z
m : ∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
⊢ z = a
Tactic:
contrapose 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✝ s : Super f d a
inst✝ : OnePreimage s
p : Postcritical s c z
m : ¬z = a
⊢ ¬∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
Theorem: Super.potential_minima_only_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
p : Postcritical s c z
m : ¬z = a
⊢ ¬∀ᶠ (w : S) in 𝓝 z, s.potential c z ≤ s.potential c w
Tactic:
simp only [Filter.not_eventually, not_le]
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
p : Postcritical s c z
m : ¬z = a
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Theorem: Super.potential_minima_only_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
p : Postcritical s c z
m : ¬z = a
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
rcases s.nice_nz p.basin z (le_refl _) with ⟨near, nc⟩
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Theorem: Super.potential_minima_only_a
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
set f : S → ℂ := s.bottcherNearIter (s.nz c z) c
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Theorem: Super.potential_minima_only_a
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
have o : 𝓝 (f z) = Filter.map f (𝓝 z) :=
  (nontrivialHolomorphicAt_of_mfderiv_ne_zero (s.bottcherNearIter_holomorphic near).along_snd
      (s.bottcherNearIter_mfderiv_ne_zero (nc _ (le_refl _))
        (p.not_precritical ((s.potential_ne_zero _).mpr m)))).nhds_eq_map_nhds
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Theorem: Super.potential_minima_only_a
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
have e : ∃ᶠ x : ℂ in 𝓝 (f z), abs x < abs (f z) := by
  apply frequently_smaller; contrapose m; simp only [not_not] at m ⊢
  replace m := (s.bottcherNear_eq_zero near).mp m
  rw [s.preimage_eq] at m; exact m
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (x : ℂ) in 𝓝 (f z), Complex.abs x < Complex.abs (f z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Theorem: Super.potential_minima_only_a
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (x : ℂ) in 𝓝 (f z), Complex.abs x < Complex.abs (f z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
rw [o, Filter.frequently_map] at e
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Theorem: Super.potential_minima_only_a
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∃ᶠ (x : S) in 𝓝 z, s.potential c x < s.potential c z
Tactic:
apply e.mp
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∀ᶠ (x : S) in 𝓝 z, Complex.abs (f x) < Complex.abs (f z) → s.potential c x < s.potential c z
Theorem: Super.potential_minima_only_a
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∀ᶠ (x : S) in 𝓝 z, Complex.abs (f x) < Complex.abs (f z) → s.potential c x < s.potential c z
Tactic:
apply (((s.isOpen_preimage _).snd_preimage c).eventually_mem near).mp
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
p : Postcritical s c z
m : ¬z = a
near : (c, (f✝ c)^[s.nz c z] z) ∈ s.near
nc : ∀ (k : ℕ), s.nz c z ≤ k → mfderiv I I (s.bottcherNear c) ((f✝ c)^[k] z) ≠ 0
f : S → ℂ := s.bottcherNearIter (s.nz c z) c
o : 𝓝 (f z) = Filter.map f (𝓝 z)
e : ∃ᶠ (a : S) in 𝓝 z, Complex.abs (f a) < Complex.abs (f z)
⊢ ∀ᶠ (x : S) in 𝓝 z,
    x ∈ {b | (c, b) ∈ {p | (p.1, (f✝ p.1)^[s.nz c z] p.2) ∈ s.near}} →
      Complex.abs (f x) < Complex.abs (f z) → s.potential c x < s.potential c z