Theorem: eqn_noncritical (Ray/Dynamics/Grow.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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
x : ℂ × ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 x, Eqn s n r y
x0 : x.2 ≠ 0
⊢ mfderiv I I (s.bottcherNearIter n x.1) (r x.1 x.2) ≠ 0
Tactic:
rcases x with ⟨c, x⟩
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : (c, x).2 ≠ 0
⊢ mfderiv I I (s.bottcherNearIter n (c, x).1) (r (c, x).1 (c, x).2) ≠ 0

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : (c, x).2 ≠ 0
⊢ mfderiv I I (s.bottcherNearIter n (c, x).1) (r (c, x).1 (c, x).2) ≠ 0
Tactic:
contrapose x0
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : ¬mfderiv I I (s.bottcherNearIter n (c, x).1) (r (c, x).1 (c, x).2) ≠ 0
⊢ ¬(c, x).2 ≠ 0

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : ¬mfderiv I I (s.bottcherNearIter n (c, x).1) (r (c, x).1 (c, x).2) ≠ 0
⊢ ¬(c, x).2 ≠ 0
Tactic:
simp only [not_not] at x0 ⊢
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (s.bottcherNearIter n c) (r c x) = 0
⊢ x = 0

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (s.bottcherNearIter n c) (r c x) = 0
⊢ x = 0
Tactic:
replace x0 : mfderiv I I (fun y ↦ s.bottcherNearIter n c (r c y)) x = 0 := by
  rw [←Function.comp_def,
    mfderiv_comp x (s.bottcherNearIter_holomorphic e.self_of_nhds.near).along_snd.mdifferentiableAt
      e.self_of_nhds.holo.along_snd.mdifferentiableAt,
    x0, ContinuousLinearMap.zero_comp]
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (fun y => s.bottcherNearIter n c (r c y)) x = 0
⊢ x = 0

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (fun y => s.bottcherNearIter n c (r c y)) x = 0
⊢ x = 0
Tactic:
have loc : (fun y ↦ s.bottcherNearIter n c (r c y)) =ᶠ[𝓝 x] fun y ↦ y ^ d ^ n :=
  ((continuousAt_const.prod continuousAt_id).eventually e).mp
    (eventually_of_forall fun _ e ↦ e.eqn)
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (fun y => s.bottcherNearIter n c (r c y)) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d ^ n
⊢ x = 0

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (fun y => s.bottcherNearIter n c (r c y)) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d ^ n
⊢ x = 0
Tactic:
rw [mfderiv_eq_fderiv, loc.fderiv_eq] at x0
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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : fderiv ℂ (fun y => y ^ d ^ n) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d ^ n
⊢ x = 0

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 : S
d n : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : fderiv ℂ (fun y => y ^ d ^ n) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d ^ n
⊢ x = 0
Tactic:
have d := (differentiableAt_pow (𝕜 := ℂ) (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv
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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : fderiv ℂ (fun y => y ^ d✝ ^ n) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
⊢ x = 0

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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : fderiv ℂ (fun y => y ^ d✝ ^ n) x = 0
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
⊢ x = 0
Tactic:
apply_fun (fun x ↦ x 1) at x0
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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0

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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = (fderiv ℂ (fun x => x ^ d✝ ^ n) x) 1
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Tactic:
rw [x0] at d
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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = 0 1
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0

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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
d : deriv (fun x => x ^ d✝ ^ n) x = 0 1
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
⊢ x = 0
Tactic:
replace d := Eq.trans d (ContinuousLinearMap.zero_apply _)
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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
d : deriv (fun x => x ^ d✝ ^ n) x = 0
⊢ x = 0

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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
d : deriv (fun x => x ^ d✝ ^ n) x = 0
⊢ x = 0
Tactic:
rw [deriv_pow, mul_eq_zero, Nat.cast_eq_zero, pow_eq_zero_iff', pow_eq_zero_iff'] at d
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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
d : d✝ = 0 ∧ n ≠ 0 ∨ x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0

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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
d : d✝ = 0 ∧ n ≠ 0 ∨ x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0
Tactic:
simp only [s.d0, false_and_iff, false_or_iff] at d
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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
d : x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0

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 : S
d✝ n : ℕ
p : ℝ
s : Super f d✝ a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
loc : (𝓝 x).EventuallyEq (fun y => s.bottcherNearIter n c (r c y)) fun y => y ^ d✝ ^ n
x0 : (fderiv ℂ (fun y => y ^ d✝ ^ n) x) 1 = 0 1
d : x = 0 ∧ d✝ ^ n - 1 ≠ 0
⊢ x = 0
Tactic:
exact d.1
State after:
no goals

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 : ℕ
p : ℝ
s : Super f d a
r : ℂ → ℂ → S
c x : ℂ
e : ∀ᶠ (y : ℂ × ℂ) in 𝓝 (c, x), Eqn s n r y
x0 : mfderiv I I (s.bottcherNearIter n c) (r c x) = 0
⊢ mfderiv I I (fun y => s.bottcherNearIter n c (r c y)) x = 0
Tactic:
rw [←Function.comp_def,
  mfderiv_comp x (s.bottcherNearIter_holomorphic e.self_of_nhds.near).along_snd.mdifferentiableAt
    e.self_of_nhds.holo.along_snd.mdifferentiableAt,
  x0, ContinuousLinearMap.zero_comp]
State after:
no goals