Crouzeix--Palencia assembly along compact exhaustions

This file joins compact-set sup-norm convergence to the sequence-limit auxiliary assembly. It reduces the exact Crouzeix--Palencia conclusion to constructing the sharp auxiliary bounds at every stage of a decreasing compact exhaustion of the closed numerical range.

Main declaration

• crouzeix_palencia_of_antitone_compact_auxiliary_bounds -- exact L4.2 from stagewise auxiliary bounds along a decreasing compact exhaustion.
• crouzeix_palencia_of_compactThickening_auxiliary_bounds -- the canonical specialization to closed thickenings of the closed numerical range.

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

On a subsingleton Hilbert space, every polynomial operator vanishes, so the Crouzeix–Palencia bound follows directly from nonnegativity.

theorem crouzeix_palencia_of_antitone_compact_auxiliary_bounds {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (K : ℕ → Set ℂ) (hanti : Antitone K) (hcompact : ∀ (n : ℕ), IsCompact (K n)) (hnonempty : ∀ (n : ℕ), (K n).Nonempty) (hinter : ⋂ (n : ℕ), K n = closure (numericalRange A)) (haux : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (G : E →L[ℂ] E), ‖(Polynomial.aeval A) p + star G‖ ≤ 2 * polynomialSupNorm p (K n) ∧ ‖(Polynomial.aeval A) p * G‖ ≤ polynomialSupNorm p (K n) ^ 2) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

If a decreasing sequence of nonempty compact sets intersects to the closed numerical range and the sharp auxiliary bounds hold on every stage, then the exact Crouzeix--Palencia polynomial spectral-set conclusion holds.

theorem crouzeix_palencia_of_antitone_compact_tendsto_polynomial_companions {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (K : ℕ → Set ℂ) (hanti : Antitone K) (hcompact : ∀ (n : ℕ), IsCompact (K n)) (hnonempty : ∀ (n : ℕ), (K n).Nonempty) (hinter : ⋂ (n : ℕ), K n = closure (numericalRange A)) (hfinite : ∀ (n : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (p : Polynomial ℂ), ‖(Polynomial.aeval A) p‖ ≤ C * polynomialSupNorm p (K n)) (hcompanion : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (G : E →L[ℂ] E) (q : ℕ → Polynomial ℂ), (∀ (j : ℕ), polynomialSupNorm (q j) (K n) ≤ polynomialSupNorm p (K n)) ∧ Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (q j)) Filter.atTop (nhds G) ∧ ‖(Polynomial.aeval A) p + star G‖ ≤ 2 * polynomialSupNorm p (K n)) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

If every stage of a decreasing compact exhaustion has a finite global polynomial-calculus bound and uniformly contractive polynomial companions converging in operator norm, then the stagewise fourth-power bootstraps and sup-norm convergence give the exact Crouzeix--Palencia conclusion on the intersection.

theorem crouzeix_palencia_of_compactThickening_tendsto_polynomial_companions {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hfinite : ∀ (n : ℕ), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (p : Polynomial ℂ), ‖(Polynomial.aeval A) p‖ ≤ C * polynomialSupNorm p (compactThickeningApprox (closure (numericalRange A)) n)) (hcompanion : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (G : E →L[ℂ] E) (q : ℕ → Polynomial ℂ), (∀ (j : ℕ), polynomialSupNorm (q j) (compactThickeningApprox (closure (numericalRange A)) n) ≤ polynomialSupNorm p (compactThickeningApprox (closure (numericalRange A)) n)) ∧ Filter.Tendsto (fun (j : ℕ) => (Polynomial.aeval A) (q j)) Filter.atTop (nhds G) ∧ ‖(Polynomial.aeval A) p + star G‖ ≤ 2 * polynomialSupNorm p (compactThickeningApprox (closure (numericalRange A)) n)) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Finite polynomial-calculus bounds and convergent contractive polynomial companions on every canonical closed thickening imply the exact Crouzeix--Palencia conclusion.

theorem crouzeix_palencia_of_compactThickening_auxiliary_bounds {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (haux : ∀ (p : Polynomial ℂ) (n : ℕ), ∃ (G : E →L[ℂ] E), ‖(Polynomial.aeval A) p + star G‖ ≤ 2 * polynomialSupNorm p (compactThickeningApprox (closure (numericalRange A)) n) ∧ ‖(Polynomial.aeval A) p * G‖ ≤ polynomialSupNorm p (compactThickeningApprox (closure (numericalRange A)) n) ^ 2) : IsKPolynomialSpectralSet A (1 + √2) (closure (numericalRange A))

Sharp auxiliary bounds on the canonical compact thickenings of the closed numerical range imply the exact Crouzeix--Palencia conclusion. The zero Hilbert space is discharged directly; otherwise the closed numerical range is a nonempty compact set, so compactThickeningApprox_spec applies.