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₀
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
Tactic:
by_cases h : p = 0
State after:
case pos
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)

case neg
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)

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:
case neg => exact exists_cindex_eq_order' hp h
State after:
no goals

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:
case pos =>
  subst_vars
  obtain ⟨R, hR, hf⟩ := Metric.eventually_nhds_iff.mp (hp.locally_zero_iff.mpr rfl)
  refine ⟨R, hR, λ r hr => ?_⟩
  simp [cindex, Real.pi_ne_zero, Complex.I_ne_zero]
  have : Set.EqOn (λ z => deriv f z / f z) 0 (sphere z₀ r) := by
    intro z hz
    simp
    right
    apply hf
    rw [hz.symm.symm]
    exact hr.2
  rw [circleIntegral.integral_congr hr.1.le this]
  simp [circleIntegral]
State after:
no goals

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:
exact exists_cindex_eq_order' hp h
State after:
no goals

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:
subst_vars
State after:
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f 0 z₀
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order 0)

State before:
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f 0 z₀
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order 0)
Tactic:
obtain ⟨R, hR, hf⟩ := Metric.eventually_nhds_iff.mp (hp.locally_zero_iff.mpr rfl)
State after:
case intro.intro
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order 0)

State before:
case intro.intro
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
⊢ ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order 0)
Tactic:
refine ⟨R, hR, λ r hr => ?_⟩
State after:
case intro.intro
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
⊢ cindex z₀ r f = ↑(FormalMultilinearSeries.order 0)

State before:
case intro.intro
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
⊢ cindex z₀ r f = ↑(FormalMultilinearSeries.order 0)
Tactic:
simp [cindex, Real.pi_ne_zero, Complex.I_ne_zero]
State after:
case intro.intro
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
⊢ (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = 0

State before:
case intro.intro
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
⊢ (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = 0
Tactic:
have : Set.EqOn (λ z => deriv f z / f z) 0 (sphere z₀ r) := by
  intro z hz
  simp
  right
  apply hf
  rw [hz.symm.symm]
  exact hr.2
State after:
case intro.intro
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
this : Set.EqOn (fun z => deriv f z / f z) 0 (sphere z₀ r)
⊢ (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = 0

State before:
case intro.intro
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
this : Set.EqOn (fun z => deriv f z / f z) 0 (sphere z₀ r)
⊢ (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = 0
Tactic:
rw [circleIntegral.integral_congr hr.1.le this]
State after:
case intro.intro
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
this : Set.EqOn (fun z => deriv f z / f z) 0 (sphere z₀ r)
⊢ (∮ (z : ℂ) in C(z₀, r), 0 z) = 0

State before:
case intro.intro
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
this : Set.EqOn (fun z => deriv f z / f z) 0 (sphere z₀ r)
⊢ (∮ (z : ℂ) in C(z₀, r), 0 z) = 0
Tactic:
simp [circleIntegral]
State after:
no goals

State before:
f g : ℂ → ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
⊢ Set.EqOn (fun z => deriv f z / f z) 0 (sphere z₀ r)
Tactic:
intro z hz
State after:
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ (fun z => deriv f z / f z) z = 0 z

State before:
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ (fun z => deriv f z / f z) z = 0 z
Tactic:
simp
State after:
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ deriv f z = 0 ∨ f z = 0

State before:
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ deriv f z = 0 ∨ f z = 0
Tactic:
right
State after:
case h
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ f z = 0

State before:
case h
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ f z = 0
Tactic:
apply hf
State after:
case h.a
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ dist z z₀ < R

State before:
case h.a
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ dist z z₀ < R
Tactic:
rw [hz.symm.symm]
State after:
case h.a
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ r < R

State before:
case h.a
f g : ℂ → ℂ
z✝ z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f 0 z₀
R : ℝ
hR : R > 0
hf : ∀ ⦃y : ℂ⦄, dist y z₀ < R → f y = 0
r : ℝ
hr : r ∈ Set.Ioo 0 R
z : ℂ
hz : z ∈ sphere z₀ r
⊢ r < R
Tactic:
exact hr.2
State after:
no goals