OmittedLimits.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Limits of omitted points and disks

Hurwitz applied to Fₙ - wₙ keeps every convergent sequence of omitted points out of a nonconstant locally uniform limit's image. The argument works on each retained core. Convergence of disk parameters then keeps the whole limiting closed disk in the complement.

theorem OAI.CircleDomainRigidity.omitted_point_limit line 22

theorem OAI.CircleDomainRigidity.omitted_closedBall_limit line 47

Source documentation

The disks may depend on the index, and need be omitted only eventually on a fixed connected open source set.

theorem omitted_closedBall_limit
    (hhurwitz : HurwitzZeroFreeLimit)
    {D : Set ℂ} {F : ℕ → ℂ → ℂ} {f : ℂ → ℂ}
    {c : ℕ → ℂ} {r : ℕ → ℝ} {c₀ : ℂ} {r₀ : ℝ}
    (hD : IsOpen D) (hconn : IsConnected D)
    (hF : ∀ᶠ n in atTop, DifferentiableOn ℂ (F n) D ∧
      ∀ z ∈ D, F n z ∉ Metric.closedBall (c n) (r n))
    (hr : ∀ n, 0 ≤ r n) (hr₀ : 0 ≤ r₀)
    (hlim : TendstoLocallyUniformlyOn F f atTop D)
    (hc : Tendsto c atTop (𝓝 c₀)) (hrlim : Tendsto r atTop (𝓝 r₀))
    (hnonconst : ¬ ∃ a : ℂ, ∀ z ∈ D, f z = a) :
    Metric.closedBall c₀ r₀ ⊆ (f '' D)ᶜ := by
…

Mentions: OAI.CircleDomainRigidity.HurwitzZeroFreeLimit

theorem OAI.CircleDomainRigidity.omitted_closedBall_limit_on_eventual_cores line 77

Source documentation

Eventual holomorphy and omission on each retained core suffice; no single finite map has to be defined on the full union.

theorem omitted_closedBall_limit_on_eventual_cores
    (hhurwitz : HurwitzZeroFreeLimit)
    {D : ℕ → Set ℂ} {F : ℕ → ℂ → ℂ} {f : ℂ → ℂ}
    {c : ℕ → ℂ} {r : ℕ → ℝ} {c₀ : ℂ} {r₀ : ℝ}
    (hD : ∀ m, IsOpen (D m)) (hconn : ∀ m, IsConnected (D m))
    (hF : ∀ m, ∀ᶠ n in atTop, DifferentiableOn ℂ (F n) (D m) ∧
      ∀ z ∈ D m, F n z ∉ Metric.closedBall (c n) (r n))
    (hr : ∀ n, 0 ≤ r n) (hr₀ : 0 ≤ r₀)
    (hlim : TendstoLocallyUniformlyOn F f atTop (⋃ m, D m))
    (hc : Tendsto c atTop (𝓝 c₀)) (hrlim : Tendsto r atTop (𝓝 r₀))
    (hnonconst : ∀ m, ¬ ∃ a : ℂ, ∀ z ∈ D m, f z = a) :
    Metric.closedBall c₀ r₀ ⊆ (f '' (⋃ m, D m))ᶜ := by
…

Mentions: OAI.CircleDomainRigidity.HurwitzZeroFreeLimit

theorem OAI.CircleDomainRigidity.omitted_point_limit_on_exhaustion line 94
theorem OAI.CircleDomainRigidity.omitted_closedBall_limit_on_exhaustion line 112

theorem OAI.CircleDomainRigidity.sphere_disk_omitted_of_plane_disk line 139

Source documentation

Passing to the normalized sphere extension introduces only infinity, so a finite omitted disk remains omitted.

theorem sphere_disk_omitted_of_plane_disk
    {D : Set ℂ} {f : ℂ → ℂ} {c : ℂ} {r : ℝ}
    (h : Metric.closedBall c r ⊆ (f '' D)ᶜ) :
    ((↑) : ℂ → Sphere) '' Metric.closedBall c r ⊆
      (extendAtInfinity f '' (((↑) : ℂ → Sphere) '' D ∪ {OnePoint.infty}))ᶜ := by
…

Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.extendAtInfinity

theorem OAI.CircleDomainRigidity.marked_component_limit_omitted line 153

Source documentation

Actual complementary components of the approximating circle domains remain omitted in the normalized limiting sphere image.

theorem marked_component_limit_omitted
    (hhurwitz : HurwitzZeroFreeLimit)
    {D : ℕ → Set ℂ} {V : ℕ → Set Sphere} {p : ℕ → Sphere}
    {F : ℕ → ℂ → ℂ} {f : ℂ → ℂ}
    {c : ℕ → ℂ} {r : ℕ → ℝ} {c₀ : ℂ} {r₀ : ℝ}
    (hD : ∀ m, IsOpen (D m)) (hconn : ∀ m, IsConnected (D m))
    (hF : ∀ m, ∀ᶠ n in atTop, DifferentiableOn ℂ (F n) (D m) ∧
      ∀ z ∈ D m, (F n z : Sphere) ∈ V n)
    (he : ∀ᶠ n in atTop, connectedComponentIn (V n)ᶜ (p n) =
      ((↑) : ℂ → Sphere) '' Metric.closedBall (c n) (r n))
    (hr : ∀ n, 0 ≤ r n) (hr₀ : 0 ≤ r₀)
    (hlim : TendstoLocallyUniformlyOn F f atTop (⋃ m, D m))
…

Mentions: OAI.CircleDomainRigidity.HurwitzZeroFreeLimit, OAI.CircleDomainRigidity.Sphere