Crouzeix--Palencia assembly from approximate auxiliary bounds

Smooth-domain approximation naturally produces auxiliary operators whose sharp bounds contain an arbitrarily small scalar error. This file removes that error after applying the algebraic Crouzeix--Palencia balance estimate.

Main declarations

• norm_le_one_add_sqrt_two_mul_of_approximate_auxiliary_bounds -- the abstract epsilon-limit form of the balance estimate.
• crouzeix_palencia_of_approximate_auxiliary_bounds -- the corresponding polynomial spectral-set package over the closure of the numerical range.
• norm_le_one_add_sqrt_two_mul_of_tendsto_auxiliary_bounds and crouzeix_palencia_of_tendsto_auxiliary_bounds -- sequence-limit forms suited to a smooth exhaustion.

theorem norm_le_one_add_sqrt_two_mul_of_approximate_auxiliary_bounds {B : Type u_1} [NonUnitalNormedRing B] [StarRing B] [CStarRing B] (F : B) {m : ℝ} (haux : ∀ (ε : ℝ), 0 < ε → ∃ (G : B), ‖F + star G‖ ≤ 2 * (m + ε) ∧ ‖F * G‖ ≤ (m + ε) ^ 2) : ‖F‖ ≤ (1 + √2) * m

If auxiliary operators satisfy the two sharp bounds with every positive additive error in m, then the exact Crouzeix--Palencia estimate follows.

theorem norm_le_one_add_sqrt_two_mul_of_tendsto_auxiliary_bounds {B : Type u_1} [NonUnitalNormedRing B] [StarRing B] [CStarRing B] (F : B) {m : ℝ} (M : ℕ → ℝ) (hM : Filter.Tendsto M Filter.atTop (nhds m)) (haux : ∀ (n : ℕ), ∃ (G : B), ‖F + star G‖ ≤ 2 * M n ∧ ‖F * G‖ ≤ M n ^ 2) : ‖F‖ ≤ (1 + √2) * m

If the two auxiliary bounds hold along a scalar sequence converging to m, then the exact Crouzeix--Palencia estimate follows.

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

Approximate L4.2d/e auxiliary bounds for every polynomial suffice for the exact Crouzeix--Palencia polynomial spectral-set conclusion.

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

Stagewise L4.2d/e bounds controlled by sequences converging to the target polynomial sup norms imply the exact spectral-set conclusion.