Theorem: Super.isNice_zero (Ray/Dynamics/Potential.lean)

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 : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
⊢ s.IsNiceN c 0 0
Tactic:
intro z zp
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0

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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
have za := le_antisymm zp s.potential_nonneg
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : s.potential c z = 0
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0

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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : s.potential c z = 0
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
simp only [s.potential_eq_zero_of_onePreimage] at za
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0

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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ (c, (f c)^[0] z) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] z) ≠ 0
Tactic:
rw [za, Function.iterate_zero_apply]
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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ (c, a) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0

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✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ (c, a) ∈ s.near ∧ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0
Tactic:
use s.mem_near c
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
⊢ ∀ (k : ℕ), 0 ≤ k → mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0
Tactic:
intro k _
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
k : ℕ
a✝ : 0 ≤ k
⊢ mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
k : ℕ
a✝ : 0 ≤ k
⊢ mfderiv I I (s.bottcherNear c) ((f c)^[k] a) ≠ 0
Tactic:
rw [s.iter_a]
State after:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
k : ℕ
a✝ : 0 ≤ k
⊢ mfderiv I I (s.bottcherNear c) a ≠ 0

State before:
case right
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
inst✝ : OnePreimage s
z : S
zp : s.potential c z ≤ 0
za : z = a
k : ℕ
a✝ : 0 ≤ k
⊢ mfderiv I I (s.bottcherNear c) a ≠ 0
Tactic:
exact s.bottcherNear_mfderiv_ne_zero c
State after:
no goals