LeanPool.RiemannMappingTheorem.Cindex

noncomputable def cindex (z₀ : ℂ) (r : ℝ) (f : ℂ → ℂ) : ℂ

The argument-principle integral (2πi)⁻¹ ∮_{C(z₀, r)} f'(z)/f(z) dz, which counts zeroes of f inside the circle of radius r around z₀ (with multiplicity).

Equations

• cindex z₀ r f = (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(z₀, r), deriv f z / f z

theorem circle_integral_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} {r : ℝ} {U : Set ℂ} {c : ℂ} (hU : IsOpen U) (hr : 0 < r) (hcr : Metric.closedBall c r ⊆ U) (f_hol : DifferentiableOn ℂ f U) : ∮ (z : ℂ) in C(c, r), f z = 0

theorem circle_integral_sub_center_inv_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {r : ℝ} {c : ℂ} [CompleteSpace E] {v : E} (hr : 0 < r) : ∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • v = (2 * ↑Real.pi * Complex.I) • v

theorem DifferentiableOn.iterate_dslope {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {U : Set ℂ} {c : ℂ} {n : ℕ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hc : c ∈ U) : DifferentiableOn ℂ ((Function.swap dslope c)^[n] f) U

theorem HasFPowerSeriesAt.dslope_order_eventually_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {p : FormalMultilinearSeries ℂ ℂ E} {z₀ : ℂ} (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) : ∀ᶠ (z : ℂ) in nhds z₀, (Function.swap dslope z₀)^[p.order] f z ≠ 0

theorem deriv_div_self_eq_div_add_deriv_div_self {f g : ℂ → ℂ} {z z₀ : ℂ} {n : ℕ} (hg : DifferentiableAt ℂ g z) (hgz : g z ≠ 0) (hfg : f =ᶠ[nhds z] fun (w : ℂ) => (w - z₀) ^ n * g w) (hz : z ≠ z₀) : deriv f z / f z = ↑n / (z - z₀) + deriv g z / g z

theorem eventually_deriv_div_self_eq {f : ℂ → ℂ} {p : FormalMultilinearSeries ℂ ℂ ℂ} {z₀ : ℂ} (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) : have g := (Function.swap dslope z₀)^[p.order] f; ∀ᶠ (z : ℂ) in nhds z₀, z ≠ z₀ → deriv f z / f z = ↑p.order / (z - z₀) + deriv g z / g z

theorem cindex_eq_zero {f : ℂ → ℂ} {c : ℂ} {U : Set ℂ} {r : ℝ} (hU : IsOpen U) (hr : 0 < r) (hcr : Metric.closedBall c r ⊆ U) (f_hol : DifferentiableOn ℂ f U) (hf : ∀ z ∈ Metric.closedBall c r, f z ≠ 0) : cindex c r f = 0

theorem cindex_eq_order_aux {f g : ℂ → ℂ} {z₀ c : ℂ} {U : Set ℂ} {r : ℝ} (hU : IsOpen U) (hr : 0 < r) (h0 : Metric.closedBall z₀ r ⊆ U) (h1 : DifferentiableOn ℂ g U) (h2 : ∀ z ∈ Metric.closedBall z₀ r, g z ≠ 0) (h3 : ∀ {z : ℂ}, z ∈ Metric.sphere z₀ r → deriv f z / f z = c / (z - z₀) + deriv g z / g z) : cindex z₀ r f = c

theorem exists_cindex_eq_order' {f : ℂ → ℂ} {p : FormalMultilinearSeries ℂ ℂ ℂ} {z₀ : ℂ} (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) : ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑p.order

theorem exists_cindex_eq_order {f : ℂ → ℂ} {p : FormalMultilinearSeries ℂ ℂ ℂ} {z₀ : ℂ} (hp : HasFPowerSeriesAt f p z₀) : ∃ R > 0, ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑p.order

theorem cindex_eventually_eq_order {f : ℂ → ℂ} {p : FormalMultilinearSeries ℂ ℂ ℂ} {z₀ : ℂ} (hp : HasFPowerSeriesAt f p z₀) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), cindex z₀ r f = ↑p.order