MarkedComponentLimits.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Marked complementary-component limits

The center/radius sequences are selected from actual circle-domain components. Their Hausdorff-convergent subsequence preserves a previously constructed locally uniform map limit.

theorem OAI.CircleDomainRigidity.exists_marked_component_limits line 21

theorem OAI.CircleDomainRigidity.exists_eventual_marked_component_limits line 50

Source documentation

A mark need only be included eventually. Dummy radius-zero disks at its earlier stages do not affect the simultaneous parameter limits.

theorem exists_eventual_marked_component_limits
    {B : Type*} [Countable B] (V : ℕ → Set Sphere)
    (hV : ∀ n, IsCircleDomain (V n)) (hinf : ∀ n, OnePoint.infty ∈ V n)
    {L : ℝ} (hL : 0 ≤ L)
    (hbound : ∀ n, (V n)ᶜ ⊆ ((↑) : ℂ → Sphere) '' closedBall 0 L)
    (p : ℕ → B → Sphere) (hp : ∀ b, ∀ᶠ n in atTop, p n b ∈ (V n)ᶜ)
    {D : Set ℂ} {F : ℕ → ℂ → ℂ} {f : ℂ → ℂ}
    (hlim : TendstoLocallyUniformlyOn F f atTop D) :
    ∃ (s : ℕ → ℕ) (c : ℕ → B → ℂ) (r : ℕ → B → ℝ)
      (c₀ : B → ℂ) (r₀ : B → ℝ),
      StrictMono s ∧ TendstoLocallyUniformlyOn (fun n => F (s n)) f atTop D ∧
      (∀ n b, ‖c n b‖ ≤ L ∧ r n b ∈ Icc 0 L) ∧
…

Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsCircleDomain