Smooth Jordan domains containing compact planar sets

This file supplies the first kernel-checked part of L4.2b. It packages the geometric data needed to integrate around the boundary of a smooth strictly convex planar domain and proves that every compact set in ℂ is contained in such a domain: take a sufficiently large open disk.

The stronger approximation needed by the full Crouzeix--Palencia argument -- a nested sequence of smooth domains whose intersection is the original compact convex set -- is not asserted here. In particular, the enclosing-disk theorem must not be mistaken for that remaining planar approximation result.

The imports have separate roles: Strict supplies strict convexity of open convex sets, Ball.Pointwise identifies closures of metric thickenings, RCLike.Real identifies the frontier of a complex ball, and CircleIntegral supplies the smooth regular circle parametrization API.

structure SmoothJordanDomain : Type

A smooth Jordan domain, represented by a 2π-periodic regular boundary parametrization. Injectivity is imposed on the half-open fundamental interval [0, 2π), so the periodic identification of its two endpoints is the only allowed repetition there.

• carrier : Set ℂ

  The open strictly convex region bounded by the curve.

• isOpen_carrier : IsOpen self.carrier
• strictConvex_carrier : StrictConvex ℝ self.carrier
• boundaryParam : ℝ → ℂ

  The regular periodic parametrization of the frontier.

• boundaryParam_periodic : Function.Periodic self.boundaryParam (2 * Real.pi)
• boundaryParam_contDiff : ContDiff ℝ (↑⊤) self.boundaryParam
• boundaryParam_range : Set.range self.boundaryParam = frontier self.carrier
• boundaryParam_injOn : Set.InjOn self.boundaryParam (Set.Ico 0 (2 * Real.pi))
• boundaryParam_regular (t : ℝ) : deriv self.boundaryParam t ≠ 0

noncomputable def SmoothJordanDomain.ball (c : ℂ) (R : ℝ) (hR : 0 < R) : SmoothJordanDomain

A positive-radius open disk, with circleMap as its smooth Jordan boundary.

Equations

• One or more equations did not get rendered due to their size.

theorem exists_smoothJordanDomain_superset_of_isCompact (K : Set ℂ) (hK : IsCompact K) : ∃ (Ω : SmoothJordanDomain), K ⊆ Ω.carrier

Every compact subset of ℂ lies in a smooth strictly convex Jordan domain.

This is the one-domain existence result consumed by the initial auxiliary operator construction. It does not provide the nested exhaustion whose intersection is K.

noncomputable def smoothApproxRadius (n : ℕ) : ℝ

The positive radii 1, 1/2, 1/3, ... used for the explicit thickening approximation.

Equations

• smoothApproxRadius n = 1 / (↑n + 1)

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

The nth open metric thickening of K, at radius 1 / (n + 1).

Equations

• convexThickeningApprox K n = Metric.thickening (smoothApproxRadius n) K

theorem closure_convexThickeningApprox_succ_subset (K : Set ℂ) (n : ℕ) : closure (convexThickeningApprox K (n + 1)) ⊆ convexThickeningApprox K n

The closure of each later open thickening is contained in the preceding open thickening. Thus the explicit metric approximation has strict adjacent nesting, not merely antitonicity.

theorem convexThickeningApprox_spec (K : Set ℂ) (hcompact : IsCompact K) (hconvex : Convex ℝ K) : (∀ (n : ℕ), K ⊆ convexThickeningApprox K n ∧ IsOpen (convexThickeningApprox K n) ∧ StrictConvex ℝ (convexThickeningApprox K n)) ∧ ⋂ (n : ℕ), convexThickeningApprox K n = K

A compact convex planar set is the exact intersection of an explicit sequence of open strictly convex supersets.

This discharges the containment, convexity, openness, and intersection parts of L4.2b. The remaining gap is to replace or perturb these thickenings so that every frontier has a smooth regular Jordan parametrization.

structure SmoothConvexApproximation (K : Set ℂ) : Type

A sequence of smooth strictly convex Jordan domains that contains K at every stage and has intersection exactly K. Existence of this structure for an arbitrary compact convex planar set is the remaining geometric content of L4.2b.

• domain : ℕ → SmoothJordanDomain

  The approximating smooth Jordan domain at each stage.

• subset_domain (n : ℕ) : K ⊆ (self.domain n).carrier
• iInter_domain : ⋂ (n : ℕ), (self.domain n).carrier = K

noncomputable def smoothClosedBallApproximation (c : ℂ) (R : ℝ) (hR : 0 ≤ R) : SmoothConvexApproximation (Metric.closedBall c R)

Closed disks admit a complete smooth convex approximation: enlarge the radius by 1 / (n + 1) and use the standard circle parametrization at every stage. This is the fully verified model case for the general L4.2b package.

Equations

• smoothClosedBallApproximation c R hR = { domain := fun (n : ℕ) => SmoothJordanDomain.ball c (smoothApproxRadius n + R) ⋯, subset_domain := ⋯, iInter_domain := ⋯ }