From local smooth outer approximation to a nested exhaustion

An exact realization of every metric thickening by a smooth Jordan domain is far stronger than the planar approximation theorem needed by the Crouzeix--Palencia assembly. This file isolates the correct local statement: for every positive radius there is a smooth Jordan domain between K and that radius's open thickening of K.

Compactness then turns these independent approximations into a strict nested exhaustion. At each successor stage, a closed thickening of K is chosen inside the preceding open carrier, and the next approximation radius is also bounded by 1/(n+1). The first bound gives strict nesting; the second makes the intersection exactly K.

def HasSmoothJordanOuterApproximation (K : Set ℂ) : Prop

A planar set admits smooth Jordan outer approximations at every positive metric scale.

Equations

• HasSmoothJordanOuterApproximation K = ∀ (ε : ℝ), 0 < ε → ∃ (Omega : SmoothJordanDomain), K ⊆ Omega.carrier ∧ closure Omega.carrier ⊆ Metric.thickening ε K

noncomputable def chooseSmoothJordanOuter {K : Set ℂ} (houter : HasSmoothJordanOuterApproximation K) (ε : ℝ) (hε : 0 < ε) : SmoothJordanDomain

Choose a smooth Jordan domain approximating a set at a prescribed positive scale.

Equations

• chooseSmoothJordanOuter houter ε hε = Classical.choose ⋯

theorem target_subset_chooseSmoothJordanOuter {K : Set ℂ} (houter : HasSmoothJordanOuterApproximation K) (ε : ℝ) (hε : 0 < ε) : K ⊆ (chooseSmoothJordanOuter houter ε hε).carrier

The chosen outer domain contains the target set.

theorem closure_chooseSmoothJordanOuter_subset_thickening {K : Set ℂ} (houter : HasSmoothJordanOuterApproximation K) (ε : ℝ) (hε : 0 < ε) : closure (chooseSmoothJordanOuter houter ε hε).carrier ⊆ Metric.thickening ε K

The chosen outer domain has closure inside the prescribed thickening.

@[reducible, inline]

abbrev ContainingSmoothJordanDomain (K : Set ℂ) : Type

A smooth Jordan domain whose interior contains the target set.

Equations

• ContainingSmoothJordanDomain K = { Omega : SmoothJordanDomain // K ⊆ Omega.carrier }

noncomputable def smoothJordanNestingRadius {K : Set ℂ} (hK : IsCompact K) (Omega : ContainingSmoothJordanDomain K) : ℝ

A positive thickening radius for a compact set inside the current Jordan domain.

Equations

• smoothJordanNestingRadius hK Omega = Classical.choose ⋯

theorem smoothJordanNestingRadius_pos {K : Set ℂ} (hK : IsCompact K) (Omega : ContainingSmoothJordanDomain K) : 0 < smoothJordanNestingRadius hK Omega

The nesting radius is strictly positive.

theorem cthickening_smoothJordanNestingRadius_subset {K : Set ℂ} (hK : IsCompact K) (Omega : ContainingSmoothJordanDomain K) : Metric.cthickening (smoothJordanNestingRadius hK Omega) K ⊆ (↑Omega).carrier

The closed thickening at the nesting radius lies inside the current domain.

noncomputable def smoothJordanOuterStepRadius {K : Set ℂ} (hK : IsCompact K) (n : ℕ) (Omega : ContainingSmoothJordanDomain K) : ℝ

The smaller of the nesting radius and the next approximation scale.

Equations

• smoothJordanOuterStepRadius hK n Omega = min (smoothJordanNestingRadius hK Omega) (smoothApproxRadius (n + 1))

theorem smoothJordanOuterStepRadius_pos {K : Set ℂ} (hK : IsCompact K) (n : ℕ) (Omega : ContainingSmoothJordanDomain K) : 0 < smoothJordanOuterStepRadius hK n Omega

The next approximation scale is strictly positive.

theorem smoothJordanOuterStepRadius_le_nesting {K : Set ℂ} (hK : IsCompact K) (n : ℕ) (Omega : ContainingSmoothJordanDomain K) : smoothJordanOuterStepRadius hK n Omega ≤ smoothJordanNestingRadius hK Omega

The next approximation scale does not exceed the nesting radius.

theorem smoothJordanOuterStepRadius_le_schedule {K : Set ℂ} (hK : IsCompact K) (n : ℕ) (Omega : ContainingSmoothJordanDomain K) : smoothJordanOuterStepRadius hK n Omega ≤ smoothApproxRadius (n + 1)

The next approximation scale does not exceed the scheduled radius.

noncomputable def nextSmoothJordanOuter {K : Set ℂ} (hK : IsCompact K) (houter : HasSmoothJordanOuterApproximation K) (n : ℕ) (Omega : ContainingSmoothJordanDomain K) : ContainingSmoothJordanDomain K

The next containing Jordan domain, chosen inside the current domain and scale.

Equations

• nextSmoothJordanOuter hK houter n Omega = ⟨chooseSmoothJordanOuter houter (smoothJordanOuterStepRadius hK n Omega) ⋯, ⋯⟩

theorem closure_nextSmoothJordanOuter_subset_carrier {K : Set ℂ} (hK : IsCompact K) (houter : HasSmoothJordanOuterApproximation K) (n : ℕ) (Omega : ContainingSmoothJordanDomain K) : closure (↑(nextSmoothJordanOuter hK houter n Omega)).carrier ⊆ (↑Omega).carrier

The closure of the next outer domain lies inside the current domain.

theorem closure_nextSmoothJordanOuter_subset_schedule {K : Set ℂ} (hK : IsCompact K) (houter : HasSmoothJordanOuterApproximation K) (n : ℕ) (Omega : ContainingSmoothJordanDomain K) : closure (↑(nextSmoothJordanOuter hK houter n Omega)).carrier ⊆ convexThickeningApprox K (n + 1)

The closure of the next outer domain lies inside the next scheduled thickening.

noncomputable def firstSmoothJordanOuter {K : Set ℂ} (houter : HasSmoothJordanOuterApproximation K) : ContainingSmoothJordanDomain K

The initial Jordan domain at the first approximation scale.

Equations

• firstSmoothJordanOuter houter = ⟨chooseSmoothJordanOuter houter (smoothApproxRadius 0) firstSmoothJordanOuter._proof_1, ⋯⟩

theorem closure_firstSmoothJordanOuter_subset_schedule {K : Set ℂ} (houter : HasSmoothJordanOuterApproximation K) : closure (↑(firstSmoothJordanOuter houter)).carrier ⊆ convexThickeningApprox K 0

The initial outer domain has closure inside the initial scheduled thickening.

noncomputable def nestedSmoothJordanOuterStage {K : Set ℂ} (hK : IsCompact K) (houter : HasSmoothJordanOuterApproximation K) : ℕ → ContainingSmoothJordanDomain K

The recursively chosen sequence of nested smooth Jordan outer approximations.

Equations

• nestedSmoothJordanOuterStage hK houter n = Nat.rec (firstSmoothJordanOuter houter) (fun (n : ℕ) (Omega : ContainingSmoothJordanDomain K) => nextSmoothJordanOuter hK houter n Omega) n

theorem closure_nestedSmoothJordanOuterStage_succ_subset {K : Set ℂ} (hK : IsCompact K) (houter : HasSmoothJordanOuterApproximation K) (n : ℕ) : closure (↑(nestedSmoothJordanOuterStage hK houter (n + 1))).carrier ⊆ (↑(nestedSmoothJordanOuterStage hK houter n)).carrier

The closure of each successive outer approximation lies inside the previous domain.

theorem closure_nestedSmoothJordanOuterStage_subset_schedule {K : Set ℂ} (hK : IsCompact K) (houter : HasSmoothJordanOuterApproximation K) (n : ℕ) : closure (↑(nestedSmoothJordanOuterStage hK houter n)).carrier ⊆ convexThickeningApprox K n

Each outer approximation has closure inside its scheduled thickening.

noncomputable def StrictNestedSmoothJordanExhaustion.ofOuterApproximation (K : Set ℂ) (hK : IsCompact K) (hconvex : Convex ℝ K) (houter : HasSmoothJordanOuterApproximation K) : StrictNestedSmoothJordanExhaustion K

Arbitrarily tight smooth Jordan outer approximations can be chosen recursively to form a strict nested smooth Jordan exhaustion.

Equations

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

theorem crouzeix_palencia_of_smoothJordanOuterApproximation {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (houter : HasSmoothJordanOuterApproximation (closure (numericalRange A))) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Local smooth outer approximation of the closed numerical range is the remaining geometric input for the exact Crouzeix--Palencia bound.