Theorem: exists_cindex_eq_order' (RMT4/cindex.lean)

State before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
Tactic:
set g : ℂ → ℂ := iterate (swap dslope z₀) p.order f
State after:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)

State before:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
Tactic:
have lh1 : ∀ᶠ z in 𝓝 z₀, g z ≠ 0 := hp.dslope_order_eventually_ne_zero h
State after:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)

State before:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
Tactic:
have lh2 : ∀ᶠ z in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = p.order / (z - z₀) + deriv g z / g z :=
  eventually_deriv_div_self_eq hp h
State after:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)

State before:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
Tactic:
have lh3 : ∀ᶠ z in 𝓝 z₀, DifferentiableAt ℂ g z :=
  (hp.has_fpower_series_iterate_dslope_fslope p.order).eventually_differentiable_at
State after:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
lh3 : ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ g z
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)

State before:
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
lh3 : ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ g z
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
Tactic:
obtain ⟨R, hR₁, hh⟩ := Metric.mem_nhds_iff.mp (lh1.and (lh2.and lh3))
State after:
case intro.intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
lh3 : ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ g z
R : ℝ
hR₁ : R > 0
hh :
  ball z₀ R ⊆
    {x |
      (fun x =>
          g x ≠ 0 ∧
            (x ≠ z₀ → deriv f x / f x = ↑(FormalMultilinearSeries.order p) / (x - z₀) + deriv g x / g x) ∧
              DifferentiableAt ℂ g x)
        x}
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)

State before:
case intro.intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
lh3 : ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ g z
R : ℝ
hR₁ : R > 0
hh :
  ball z₀ R ⊆
    {x |
      (fun x =>
          g x ≠ 0 ∧
            (x ≠ z₀ → deriv f x / f x = ↑(FormalMultilinearSeries.order p) / (x - z₀) + deriv g x / g x) ∧
              DifferentiableAt ℂ g x)
        x}
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
Tactic:
refine ⟨R, hR₁, λ r hr => ?_⟩
State after:
case intro.intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
lh3 : ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ g z
R : ℝ
hR₁ : R > 0
hh :
  ball z₀ R ⊆
    {x |
      (fun x =>
          g x ≠ 0 ∧
            (x ≠ z₀ → deriv f x / f x = ↑(FormalMultilinearSeries.order p) / (x - z₀) + deriv g x / g x) ∧
              DifferentiableAt ℂ g x)
        x}
r : ℝ
hr : r ∈ Set.Ioo 0 R
⊢ cindex z₀ r f = ↑(FormalMultilinearSeries.order p)

State before:
case intro.intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
lh3 : ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ g z
R : ℝ
hR₁ : R > 0
hh :
  ball z₀ R ⊆
    {x |
      (fun x =>
          g x ≠ 0 ∧
            (x ≠ z₀ → deriv f x / f x = ↑(FormalMultilinearSeries.order p) / (x - z₀) + deriv g x / g x) ∧
              DifferentiableAt ℂ g x)
        x}
r : ℝ
hr : r ∈ Set.Ioo 0 R
⊢ cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
Tactic:
refine cindex_eq_order_aux isOpen_ball hr.1 (closedBall_subset_ball hr.2)
  (λ z hz => (hh hz).2.2.differentiableWithinAt)
  (λ z hz => (hh (closedBall_subset_ball hr.2 hz)).1)
  (λ hz => ?_)
State after:
case intro.intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
lh3 : ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ g z
R : ℝ
hR₁ : R > 0
hh :
  ball z₀ R ⊆
    {x |
      (fun x =>
          g x ≠ 0 ∧
            (x ≠ z₀ → deriv f x / f x = ↑(FormalMultilinearSeries.order p) / (x - z₀) + deriv g x / g x) ∧
              DifferentiableAt ℂ g x)
        x}
r : ℝ
hr : r ∈ Set.Ioo 0 R
z✝ : ℂ
hz : z✝ ∈ sphere z₀ r
⊢ deriv f z✝ / f z✝ = ↑(FormalMultilinearSeries.order p) / (z✝ - z₀) + deriv g z✝ / g z✝

State before:
case intro.intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
lh3 : ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ g z
R : ℝ
hR₁ : R > 0
hh :
  ball z₀ R ⊆
    {x |
      (fun x =>
          g x ≠ 0 ∧
            (x ≠ z₀ → deriv f x / f x = ↑(FormalMultilinearSeries.order p) / (x - z₀) + deriv g x / g x) ∧
              DifferentiableAt ℂ g x)
        x}
r : ℝ
hr : r ∈ Set.Ioo 0 R
z✝ : ℂ
hz : z✝ ∈ sphere z₀ r
⊢ deriv f z✝ / f z✝ = ↑(FormalMultilinearSeries.order p) / (z✝ - z₀) + deriv g z✝ / g z✝
Tactic:
refine (hh (sphere_subset_closedBall.trans (closedBall_subset_ball hr.2) hz)).2.1 ?_
State after:
case intro.intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
lh3 : ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ g z
R : ℝ
hR₁ : R > 0
hh :
  ball z₀ R ⊆
    {x |
      (fun x =>
          g x ≠ 0 ∧
            (x ≠ z₀ → deriv f x / f x = ↑(FormalMultilinearSeries.order p) / (x - z₀) + deriv g x / g x) ∧
              DifferentiableAt ℂ g x)
        x}
r : ℝ
hr : r ∈ Set.Ioo 0 R
z✝ : ℂ
hz : z✝ ∈ sphere z₀ r
⊢ z✝ ≠ z₀

State before:
case intro.intro
f g✝ : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
g : ℂ → ℂ := (swap dslope z₀)^[FormalMultilinearSeries.order p] f
lh1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z ≠ 0
lh2 : ∀ᶠ (z : ℂ) in 𝓝 z₀, z ≠ z₀ → deriv f z / f z = ↑(FormalMultilinearSeries.order p) / (z - z₀) + deriv g z / g z
lh3 : ∀ᶠ (z : ℂ) in 𝓝 z₀, DifferentiableAt ℂ g z
R : ℝ
hR₁ : R > 0
hh :
  ball z₀ R ⊆
    {x |
      (fun x =>
          g x ≠ 0 ∧
            (x ≠ z₀ → deriv f x / f x = ↑(FormalMultilinearSeries.order p) / (x - z₀) + deriv g x / g x) ∧
              DifferentiableAt ℂ g x)
        x}
r : ℝ
hr : r ∈ Set.Ioo 0 R
z✝ : ℂ
hz : z✝ ∈ sphere z₀ r
⊢ z✝ ≠ z₀
Tactic:
exact ne_of_mem_sphere hz hr.1.ne.symm
State after:
no goals