internlm/Lean-Github huggingface dataset:
Theorem: cindex_eq_order_aux
Proof state before:
case hg
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContinuousOn (fun z => deriv g z) U
Tactic:
apply ContDiffOn.continuousOn_deriv_of_isOpen ?_ hU le_rfl
Proof state after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContDiffOn ℂ 1 g U
Theorem: cindex_eq_order_aux
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
⊢ ContDiffOn ℂ 1 g U
Tactic:
exact h1.contDiffOn hU
Proof state after:
no goals
Theorem: cindex_eq_order_aux
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
⊢ (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
Tactic:
have := cindex_eq_zero hU hr h0 h1 h2
Proof state after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
this : cindex z₀ r g = 0
⊢ (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
Theorem: cindex_eq_order_aux
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
this : cindex z₀ r g = 0
⊢ (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
Tactic:
simpa [cindex, Real.pi_ne_zero, I_ne_zero] using this
Proof state after:
no goals
Theorem: cindex_eq_order_aux
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hU : IsOpen U
hr : 0 < r
h0 : closedBall z₀ r ⊆ U
h1 : DifferentiableOn ℂ g U
h2 : ∀ z ∈ closedBall z₀ r, g z ≠ 0
h3 : ∀ {z : ℂ}, z ∈ sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z
e2 : sphere z₀ r ⊆ U
e4 : (∮ (z : ℂ) in C(z₀, r), deriv f z / f z) = ∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z
e5 :
  (∮ (z : ℂ) in C(z₀, r), c / (z - z₀) + deriv g z / g z) =
    (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) + ∮ (z : ℂ) in C(z₀, r), deriv g z / g z
e6 : (∮ (z : ℂ) in C(z₀, r), deriv g z / g z) = 0
⊢ (∮ (z : ℂ) in C(z₀, r), c / (z - z₀)) = 2 * ↑π * I * c
Tactic:
simpa [div_eq_mul_inv, mul_comm _ _⁻¹] using circle_integral_sub_center_inv_smul hr
Proof state after:
no goals
Theorem: exists_cindex_eq_order'
Proof 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
Proof 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)
Theorem: exists_cindex_eq_order'
Proof 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
Proof 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)
Theorem: exists_cindex_eq_order'
Proof 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
Proof 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)
Theorem: exists_cindex_eq_order'
Proof 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
Proof 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)
Theorem: exists_cindex_eq_order'
Proof 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))
Proof 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)
Theorem: exists_cindex_eq_order'
Proof 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 => ?_⟩
Proof 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)
Theorem: exists_cindex_eq_order'
Proof 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 => ?_)
Proof 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✝
Theorem: exists_cindex_eq_order'
Proof 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 ?_
Proof 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₀
Theorem: exists_cindex_eq_order'
Proof 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
Proof state after:
no goals
Theorem: exists_cindex_eq_order
Proof 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
Proof 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)
Theorem: exists_cindex_eq_order
Proof 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
Proof state after:
no goals
Theorem: exists_cindex_eq_order
Proof 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]
Proof state after:
no goals
Theorem: exists_cindex_eq_order
Proof 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
Proof state after:
no goals
Theorem: exists_cindex_eq_order
Proof 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
Proof 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)
Theorem: exists_cindex_eq_order
Proof 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)
Proof 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)
Theorem: exists_cindex_eq_order
Proof 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 => ?_⟩
Proof 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)
Theorem: exists_cindex_eq_order
Proof 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]
Proof 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
Theorem: exists_cindex_eq_order
Proof 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
Proof 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
Theorem: exists_cindex_eq_order
Proof 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]
Proof 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
Theorem: exists_cindex_eq_order
Proof 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]
Proof state after:
no goals
Theorem: exists_cindex_eq_order
Proof 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
Proof 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
Theorem: exists_cindex_eq_order
Proof 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
Proof 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
Theorem: exists_cindex_eq_order
Proof 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
Proof 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
Theorem: exists_cindex_eq_order
Proof 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
Proof 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
Theorem: exists_cindex_eq_order
Proof 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]
Proof 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
Theorem: exists_cindex_eq_order
Proof 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
Proof state after:
no goals
Theorem: cindex_eventually_eq_order
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
Tactic:
rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff]
Proof state after:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
⊢ ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Set.Ioi 0 → cindex z₀ y f = ↑(FormalMultilinearSeries.order p)