Polynomial sup-norms on decreasing compact sets

This file supplies the compact-exhaustion transfer needed by approximation arguments in the Crouzeix chain. If K n is a decreasing sequence of nonempty compact subsets of ℂ, then the polynomial sup-norms on K n decrease to the sup-norm on their intersection.

The proof uses the extreme value theorem and Cantor's intersection theorem: if the limiting infimum were strictly above the sup-norm on the intersection, the corresponding closed superlevel subsets of every K n would be nonempty and nested, hence would have a point in their common intersection.

Main declarations

• polynomialSupNorm_mono_of_isCompact gives monotonicity when the larger set is compact.
• polynomialSupNorm_iInter_eq_iInf_of_antitone_isCompact identifies the sup-norm on the intersection with the infimum of the approximating norms.
• tendsto_polynomialSupNorm_atTop_of_antitone_isCompact is the sequential convergence form of the same result.
• exists_polynomialSupNorm_convexThickeningApprox_le_add and tendsto_polynomialSupNorm_convexThickeningApprox_atTop apply this approximation principle to the explicit open thickenings from SmoothApprox.lean.

theorem polynomialSupNorm_mono_of_isCompact (p : Polynomial ℂ) {K L : Set ℂ} (hKL : K ⊆ L) (hL : IsCompact L) : polynomialSupNorm p K ≤ polynomialSupNorm p L

Polynomial sup norms are monotone under set inclusion whenever the values on the larger set are bounded, in particular when that set is compact.

theorem polynomialSupNorm_iInter_eq_iInf_of_antitone_isCompact (p : Polynomial ℂ) (K : ℕ → Set ℂ) (hanti : Antitone K) (hcompact : ∀ (n : ℕ), IsCompact (K n)) (hnonempty : ∀ (n : ℕ), (K n).Nonempty) : polynomialSupNorm p (⋂ (n : ℕ), K n) = ⨅ (n : ℕ), polynomialSupNorm p (K n)

The polynomial sup-norm on the intersection of a decreasing sequence of nonempty compact sets is the infimum of the sup-norms on those sets.

theorem tendsto_polynomialSupNorm_atTop_of_antitone_isCompact (p : Polynomial ℂ) (K : ℕ → Set ℂ) (hanti : Antitone K) (hcompact : ∀ (n : ℕ), IsCompact (K n)) (hnonempty : ∀ (n : ℕ), (K n).Nonempty) : Filter.Tendsto (fun (n : ℕ) => polynomialSupNorm p (K n)) Filter.atTop (nhds (polynomialSupNorm p (⋂ (n : ℕ), K n)))

Along a decreasing sequence of nonempty compact sets, polynomial sup-norms converge to the sup-norm on the intersection.

The explicit open thickening approximation

theorem exists_polynomialSupNorm_convexThickeningApprox_le_add (p : Polynomial ℂ) {K : Set ℂ} (hK : IsCompact K) {ε : ℝ} (hε : 0 < ε) : ∃ (n : ℕ), polynomialSupNorm p (convexThickeningApprox K n) ≤ polynomialSupNorm p K + ε

Every positive error tolerance is achieved by one of the explicit open metric thickenings of a compact set.

theorem tendsto_polynomialSupNorm_convexThickeningApprox_atTop (p : Polynomial ℂ) {K : Set ℂ} (hK : IsCompact K) : Filter.Tendsto (fun (n : ℕ) => polynomialSupNorm p (convexThickeningApprox K n)) Filter.atTop (nhds (polynomialSupNorm p K))

Polynomial sup-norms on the explicit open metric thickenings of a compact set converge to the sup-norm on that set.