MarkedDiskLimits.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous limits of marked round disks

Bounded centers and nonnegative bounded radii form a compact parameter space. A countable family therefore admits one subsequence on which all parameters converge. The limiting radius may be zero.

theorem OAI.CircleDomainRigidity.exists_marked_disk_parameter_limits line 23
theorem OAI.CircleDomainRigidity.closedBall_eq_affine_image line 47
theorem OAI.CircleDomainRigidity.exists_closedBall_point_dist_le line 53
theorem OAI.CircleDomainRigidity.hausdorffDist_closedBall_le_parameters line 74
theorem OAI.CircleDomainRigidity.tendsto_hausdorffDist_closedBall line 83

theorem OAI.CircleDomainRigidity.exists_marked_disk_hausdorff_limits line 97

Source documentation

One subsequence gives Hausdorff limits for every marked disk.

theorem exists_marked_disk_hausdorff_limits
    {B : Type*} [Countable B] {L : ℝ}
    (c : ℕ → B → ℂ) (r : ℕ → B → ℝ)
    (hc : ∀ n b, ‖c n b‖ ≤ L) (hr : ∀ n b, r n b ∈ Icc 0 L) :
    ∃ (s : ℕ → ℕ) (c₀ : B → ℂ) (r₀ : B → ℝ),
      StrictMono s ∧ (∀ b, ‖c₀ b‖ ≤ L ∧ r₀ b ∈ Icc 0 L) ∧
      ∀ b, Tendsto (fun n => hausdorffDist (closedBall (c (s n) b) (r (s n) b))
        (closedBall (c₀ b) (r₀ b))) atTop (𝓝 0) := by
…