Compact metric-thickening approximations

The open thickenings in SmoothApprox.lean supply the convex domains used by the analytic argument. At the same radii, their closed metric thickenings form a decreasing compact exhaustion and contain the corresponding domain frontiers. These are the compact control sets used by the limiting Palencia assembly.

Main declarations

• compactThickeningApprox -- the closed thickening at radius 1 / (n + 1).
• compactThickeningApprox_infinite -- every stage over a nonempty set is infinite.
• compactThickeningApprox_spec -- antitonicity, compactness, nonemptiness, and exact intersection of the compact exhaustion.
• frontier_convexThickeningApprox_subset_compactThickeningApprox -- the open-stage frontier lies in the compact control set at the same radius.

noncomputable def compactThickeningApprox (K : Set ℂ) (n : ℕ) : Set ℂ

The closed metric thickening of K at radius 1 / (n + 1).

Equations

• compactThickeningApprox K n = Metric.cthickening (smoothApproxRadius n) K

theorem compactThickeningApprox_infinite (K : Set ℂ) (n : ℕ) (hnonempty : K.Nonempty) : (compactThickeningApprox K n).Infinite

A closed thickening of a nonempty planar set at the positive approximation radius contains a nondegenerate closed disk, hence is infinite.

theorem compactThickeningApprox_spec (K : Set ℂ) (hcompact : IsCompact K) (hnonempty : K.Nonempty) : Antitone (compactThickeningApprox K) ∧ (∀ (n : ℕ), IsCompact (compactThickeningApprox K n)) ∧ (∀ (n : ℕ), (compactThickeningApprox K n).Nonempty) ∧ ⋂ (n : ℕ), compactThickeningApprox K n = K

Closed thickenings of a nonempty compact planar set form an antitone sequence of nonempty compact sets whose intersection is exactly the set.

theorem frontier_convexThickeningApprox_subset_compactThickeningApprox (K : Set ℂ) (n : ℕ) : frontier (convexThickeningApprox K n) ⊆ compactThickeningApprox K n

The frontier of the open thickening at stage n lies in the closed thickening at the same radius.