LeanPool.RiemannMappingTheorem.Hurwitz #
theorem
eventually_nhds_iff_eventually_ball
{α : Type u_1}
{z₀ : α}
{P : α → Prop}
[PseudoMetricSpace α]
:
theorem
eventually_nhds_iff_eventually_closed_ball
{α : Type u_1}
{z₀ : α}
{P : α → Prop}
[PseudoMetricSpace α]
:
theorem
dist_inv_le_dist_div
{𝕜 : Type u_1}
[NormedField 𝕜]
{x y : 𝕜}
{η η' : ℝ}
(hη : 0 < η)
(hη' : 0 < η')
(hx : x ∉ Metric.ball 0 η)
(hy : y ∉ Metric.ball 0 η')
:
theorem
uniform_ContinuousOn_inv
{𝕜 : Type u_1}
[NormedField 𝕜]
{s : Set 𝕜}
(hs : Filter.principal s ⊓ nhds 0 = ⊥)
:
theorem
TendstoUniformlyOn.inv_of_isolated_zero
{𝕜 : Type u_1}
{ι : Type u_2}
{α : Type u_3}
{s : Set α}
[NormedField 𝕜]
{F : ι → α → 𝕜}
{f : α → 𝕜}
{p : Filter ι}
(hF : TendstoUniformlyOn F f p s)
(hf : Filter.principal (f '' s) ⊓ nhds 0 = ⊥)
:
TendstoUniformlyOn F⁻¹ f⁻¹ p s
theorem
TendstoUniformlyOn.mul_of_le
{𝕜 : Type u_1}
{ι : Type u_2}
{α : Type u_3}
{s : Set α}
[NormedField 𝕜]
{F G : ι → α → 𝕜}
{f g : α → 𝕜}
{p : Filter ι}
{mf mg : ℝ}
(hF : TendstoUniformlyOn F f p s)
(hG : TendstoUniformlyOn G g p s)
(hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf)
(hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg)
:
TendstoUniformlyOn (F * G) (f * g) p s
theorem
TendstoUniformlyOn.mul_of_bound
{𝕜 : Type u_1}
{ι : Type u_2}
{α : Type u_3}
{s : Set α}
[NormedField 𝕜]
{F G : ι → α → 𝕜}
{f g : α → 𝕜}
{p : Filter ι}
{mf mg : ℝ}
(hF : TendstoUniformlyOn F f p s)
(hG : TendstoUniformlyOn G g p s)
(hf : ∀ x ∈ s, ‖f x‖ ≤ mf)
(hg : ∀ x ∈ s, ‖g x‖ ≤ mg)
:
TendstoUniformlyOn (F * G) (f * g) p s
theorem
TendstoUniformlyOn.inv_of_compact
{𝕜 : Type u_1}
{ι : Type u_2}
{α : Type u_3}
{K : Set α}
[NormedField 𝕜]
{F : ι → α → 𝕜}
{f : α → 𝕜}
{p : Filter ι}
[TopologicalSpace α]
(hF : TendstoUniformlyOn F f p K)
(hf : ContinuousOn f K)
(hK : IsCompact K)
(hfz : ∀ x ∈ K, f x ≠ 0)
:
TendstoUniformlyOn F⁻¹ f⁻¹ p K
theorem
TendstoUniformlyOn.mul_of_compact
{𝕜 : Type u_1}
{ι : Type u_2}
{α : Type u_3}
{K : Set α}
[NormedField 𝕜]
{F G : ι → α → 𝕜}
{f g : α → 𝕜}
{p : Filter ι}
[TopologicalSpace α]
(hF : TendstoUniformlyOn F f p K)
(hG : TendstoUniformlyOn G g p K)
(hf : ContinuousOn f K)
(hg : ContinuousOn g K)
(hK : IsCompact K)
:
TendstoUniformlyOn (F * G) (f * g) p K
theorem
TendstoUniformlyOn.div_of_compact
{𝕜 : Type u_1}
{ι : Type u_2}
{α : Type u_3}
{K : Set α}
[NormedField 𝕜]
{F G : ι → α → 𝕜}
{f g : α → 𝕜}
{p : Filter ι}
[TopologicalSpace α]
(hF : TendstoUniformlyOn F f p K)
(hG : TendstoUniformlyOn G g p K)
(hf : ContinuousOn f K)
(hg : ContinuousOn g K)
(hgK : ∀ z ∈ K, g z ≠ 0)
(hK : IsCompact K)
:
TendstoUniformlyOn (F / G) (f / g) p K
theorem
TendstoUniformlyOn.tendsto_circle_integral
{ι : Type u_1}
{F : ι → ℂ → ℂ}
{f : ℂ → ℂ}
{z₀ : ℂ}
{p : Filter ι}
{r : ℝ}
(hr : 0 < r)
(F_cont : ∀ᶠ (n : ι) in p, ContinuousOn (F n) (Metric.sphere z₀ r))
(F_conv : TendstoUniformlyOn F f p (Metric.sphere z₀ r))
:
theorem
hurwitz2_2
{ι : Type u_1}
{F : ι → ℂ → ℂ}
{f : ℂ → ℂ}
{z₀ : ℂ}
{p : Filter ι}
{r : ℝ}
{U : Set ℂ}
(hU : IsOpen U)
(hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U)
(hf : TendstoLocallyUniformlyOn F f p U)
(hr1 : 0 < r)
(hr2 : Metric.sphere z₀ r ⊆ U)
(hf1 : ∀ z ∈ Metric.sphere z₀ r, f z ≠ 0)
:
Filter.Tendsto (cindex z₀ r ∘ F) p (nhds (cindex z₀ r f))
theorem
hurwitz2
{ι : Type u_1}
{F : ι → ℂ → ℂ}
{f : ℂ → ℂ}
{z₀ : ℂ}
{p : Filter ι}
{r : ℝ}
{U : Set ℂ}
(hU : IsOpen U)
(hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U)
(hf : TendstoLocallyUniformlyOn F f p U)
(hr1 : 0 < r)
(hr2 : Metric.closedBall z₀ r ⊆ U)
(hf1 : ∀ z ∈ Metric.sphere z₀ r, f z ≠ 0)
(hf2 : cindex z₀ r f ≠ 0)
:
∀ᶠ (n : ι) in p, ∃ z ∈ Metric.ball z₀ r, F n z = 0
theorem
hurwitz3
{ι : Type u_1}
{F : ι → ℂ → ℂ}
{f : ℂ → ℂ}
{z₀ : ℂ}
{p : Filter ι}
{U s : Set ℂ}
(hU : IsOpen U)
(hF : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U)
(hf : TendstoLocallyUniformlyOn F f p U)
(hz₀ : z₀ ∈ U)
(h1 : f z₀ = 0)
(h2 : ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0)
(hs : s ∈ nhds z₀)
:
theorem
local_hurwitz
{ι : Type u_1}
{F : ι → ℂ → ℂ}
{f : ℂ → ℂ}
{z₀ : ℂ}
{p : Filter ι}
{U : Set ℂ}
[p.NeBot]
(hU : IsOpen U)
(F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U)
(F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0)
(F_conv : TendstoLocallyUniformlyOn F f p U)
(hz₀ : z₀ ∈ U)
(hfz₀ : f z₀ = 0)
:
theorem
hurwitz
{ι : Type u_1}
{F : ι → ℂ → ℂ}
{f : ℂ → ℂ}
{z₀ : ℂ}
{p : Filter ι}
{U : Set ℂ}
[p.NeBot]
(hU : IsOpen U)
(hU' : IsPreconnected U)
(F_holo : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (F n) U)
(F_noz : ∀ (n : ι), ∀ z ∈ U, F n z ≠ 0)
(F_conv : TendstoLocallyUniformlyOn F f p U)
(hz₀ : z₀ ∈ U)
(hfz₀ : f z₀ = 0)
(z : ℂ)
:
theorem
hurwitz4
{ι : Type u_1}
{p : Filter ι}
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{U : Set α}
[TopologicalSpace α]
[UniformSpace β]
[UniformSpace γ]
{F : ι → α → β}
{f : α → β}
{φ : β → γ}
(hf : TendstoLocallyUniformlyOn F f p U)
(hφ : UniformContinuous φ)
:
TendstoLocallyUniformlyOn (fun (n : ι) => φ ∘ F n) (φ ∘ f) p U