Universal circle symmetrization implies the normal auxiliary product bound

For any operator, the sharp symmetrized estimate on every polynomial forces an enclosing circle's center into the closed numerical range. Indeed, if the center were outside, an affine polynomial separator would have value one at the center and norm at most r < 1 on the closed numerical range. Applying symmetrization to its powers makes the functional-calculus term tend to zero by the unconditional Crouzeix--Palencia bound, while the circle auxiliary remains the identity, a contradiction.

The aligned-circle normal product theorem then supplies the literal sharp auxiliary product estimate.

Main declarations

• circle_center_mem_of_isCompact_nonempty_convex_of_forall_symmetrized_bound proves alignment over a compact nonempty convex control set directly from universal symmetrization.
• circle_center_mem_of_compactConvex_of_globalBound_of_symmetrization retains the earlier finite-calculus interface as a corollary.
• circle_center_mem_closedNumericalRange_of_globalBound_of_symmetrization specializes that result to the closed numerical range.
• circle_center_mem_closure_numericalRange_of_forall_symmetrized_bound specializes direct center alignment to the closed numerical range.
• norm_pow_aeval_le_two_mul_pow_polynomialNorm_of_eval_eq_zero_of_symmetrization gives a uniform power bound on the polynomial ideal vanishing at the circle center.
• norm_shifted_aeval_pow_add_shifted_eval_pow_le_two_mul_pow_norm_of_symmetrization preserves the coupled operator/scalar cancellation for every shifted power.
• norm_pow_aeval_sub_eval_smul_one_le_two_mul_pow_polynomialNorm_sub_C_of_symmetrization gives the corresponding centered power bound for every polynomial.
• spectrum_aeval_sub_eval_smul_one_subset_closedBall_of_forall_symmetrized_bound derives the sharp centered spectral inclusion from those power bounds.
• spectrum_aeval_subset_closedBall_eval_of_forall_symmetrized_bound translates that inclusion back to the spectrum of p(A).
• spectrum_aeval_subset_closedBall_shift_of_mem_of_forall_symmetrized_bound gives the analogous sharp spectral disk around every scalar shift.
• spectrum_aeval_subset_closedBall_shift_of_compactConvex_of_symmetrization discharges center membership from compact convex geometry.
• spectralRadius_aeval_sub_smul_one_le_polynomialNorm_sub_C_of_mem_of_symmetrization converts a shifted disk and center membership to a shifted spectral radius.
• spectralRadius_aeval_sub_smul_one_le_polynomialNorm_sub_C_of_compactConvex_of_symmetrization gives the sharp spectral-radius bound after every scalar shift.
• spectralRadius_aeval_le_polynomialNorm_of_compactConvex_of_symmetrization records its zero-shift specialization.
• spectrum_aeval_subset_closedBall_shift_closure_numericalRange_of_forall_symmetrized_bound specializes every shifted disk to the closed numerical range.
• spectralRadius_aeval_sub_smul_one_le_polynomialNorm_sub_C_closedNumericalRange_of_symmetrization gives the corresponding sharp shifted spectral-radius bound.
• spectralRadius_aeval_le_polynomialNorm_closedNumericalRange_of_symmetrization gives its zero-shift consequence.
• spectrum_subset_of_isCompact_nonempty_convex_of_forall_symmetrized_bound proves that the compact convex control set itself contains the spectrum.
• norm_aeval_mul_auxiliary_ball_center_le_of_eval_center_le_sqrt_two_sub_one_mul proves the sharp product bound without normality when the center value is at most sqrt 2 - 1 times the control norm.
• norm_aeval_le_two_mul_polynomialNorm_sub_C_add_norm_eval_sub_two_mul_of_symmetrization extracts the operator-norm estimate obtained from any scalar shift.
• isKPolynomialSpectralSet_three_of_isCompact_nonempty_convex_of_forall_symmetrized_bound packages universal symmetrization as a constant-three polynomial spectral set.
• norm_aeval_mul_auxiliary_ball_center_le_of_shifted_scalar_bound_of_symmetrization exposes an arbitrary scalar shift for optimizing the product estimate.
• norm_aeval_mul_auxiliary_ball_center_le_of_half_centered_scalar_bound_of_symmetrization specializes the shift to p(c) / 2, eliminating the residual scalar term.
• norm_aeval_mul_auxiliary_ball_center_le_of_centered_scalar_bound_of_symmetrization isolates the exact adaptive scalar criterion obtained by centering p.
• norm_aeval_mul_auxiliary_ball_center_le_of_centered_polynomialNorm_le_sub_of_symmetrization proves the complementary sharp near-constant branch.
• norm_aeval_mul_auxiliary_ball_center_le_one_add_sqrt_two_mul_sq_of_symmetrization gives the resulting product estimate for an arbitrary operator at the global Crouzeix--Palencia factor.
• norm_aeval_mul_auxiliary_ball_center_le_of_isStarNormal_aeval_of_symmetrization gives the sharp product estimate whenever the individual value p(A) is star-normal.
• norm_aeval_mul_auxiliary_ball_center_le_of_isStarNormal_of_symmetrization specializes the sharp estimate to a star-normal operator.

theorem circle_center_mem_of_isCompact_nonempty_convex_of_forall_symmetrized_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) {K : Set ℂ} (hcompact : IsCompact K) (hnonempty : K.Nonempty) (hconvex : Convex ℝ K) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) : c ∈ K

Universal sharp symmetrization on an enclosing circle, controlled by a compact nonempty convex set, forces the circle center into that set. No independent polynomial-calculus bound is needed: if a separator power B is close to -1, its square is close to 1, while symmetrization of the squared power would make it close to -1.

theorem circle_center_mem_of_compactConvex_of_globalBound_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) {K : Set ℂ} (hcompact : IsCompact K) (hnonempty : K.Nonempty) (hconvex : Convex ℝ K) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (C : ℝ) (_hC : 0 ≤ C) (_hcalc : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q‖ ≤ C * polynomialSupNorm q K) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) : c ∈ K

A finite polynomial-calculus bound on a compact nonempty convex set, together with universal sharp symmetrization on an enclosing circle controlled by the same set, forces the circle center into that set. No normality or particular value of the finite constant is needed.

theorem circle_center_mem_closedNumericalRange_of_globalBound_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (C : ℝ) (_hC : 0 ≤ C) (_hcalc : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q‖ ≤ C * polynomialSupNorm q (closure (numericalRange A))) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q (closure (numericalRange A))) : c ∈ closure (numericalRange A)

A finite global polynomial-calculus bound, together with universal sharp symmetrization on an enclosing circle, forces the circle center into the closed numerical range. No normality or particular value of the finite constant is needed.

theorem circle_center_mem_closure_numericalRange_of_forall_symmetrized_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q (closure (numericalRange A))) : c ∈ closure (numericalRange A)

Universal sharp symmetrization on an enclosing circle forces its center into the closed numerical range of an arbitrary operator.

theorem norm_pow_aeval_le_two_mul_pow_polynomialNorm_of_eval_eq_zero_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hK : IsCompact K) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (hpc : Polynomial.eval c p = 0) (n : ℕ) : ‖(Polynomial.aeval A) p ^ (n + 1)‖ ≤ 2 * polynomialSupNorm p K ^ (n + 1)

Universal circle symmetrization makes the functional calculus uniformly power-bounded on the ideal of polynomials vanishing at the circle center. If p(c) = 0, every positive power of p(A) has norm at most twice the corresponding power of the sup norm on the compact control set.

theorem norm_shifted_aeval_pow_add_shifted_eval_pow_le_two_mul_pow_norm_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hK : IsCompact K) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (b : ℂ) (n : ℕ) : ‖((Polynomial.aeval A) p - b • 1) ^ (n + 1) + (Polynomial.eval c p - b) ^ (n + 1) • 1‖ ≤ 2 * polynomialSupNorm (p - Polynomial.C b) K ^ (n + 1)

Universal circle symmetrization preserves the operator/scalar coupling for every positive power after an arbitrary shift b. This is stronger than separately bounding the two summands and retains the cancellation that is relevant to the sharp product problem.

theorem norm_pow_aeval_sub_eval_smul_one_le_two_mul_pow_polynomialNorm_sub_C_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hK : IsCompact K) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (n : ℕ) : ‖((Polynomial.aeval A) p - Polynomial.eval c p • 1) ^ (n + 1)‖ ≤ 2 * polynomialSupNorm (p - Polynomial.C (Polynomial.eval c p)) K ^ (n + 1)

Universal circle symmetrization uniformly power-bounds the centered functional calculus. For every polynomial p, positive powers of p(A) - p(c)I are controlled by twice the corresponding power of the sup norm of p - p(c) on the compact control set.

theorem spectrum_aeval_sub_eval_smul_one_subset_closedBall_of_forall_symmetrized_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hK : IsCompact K) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) : spectrum ℂ ((Polynomial.aeval A) p - Polynomial.eval c p • 1) ⊆ Metric.closedBall 0 (polynomialSupNorm (p - Polynomial.C (Polynomial.eval c p)) K)

Universal circle symmetrization alone confines the spectrum of the centered value p(A) - p(c)I to the disk whose radius is the sup norm of p - p(c) on the compact control set. No independent global polynomial-calculus estimate is assumed; the zero Hilbert space has empty spectrum.

theorem spectrum_aeval_subset_closedBall_eval_of_forall_symmetrized_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hK : IsCompact K) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) : spectrum ℂ ((Polynomial.aeval A) p) ⊆ Metric.closedBall (Polynomial.eval c p) (polynomialSupNorm (p - Polynomial.C (Polynomial.eval c p)) K)

Equivalently, universal circle symmetrization confines the spectrum of p(A) to the disk centered at p(c) with radius sup_K |p - p(c)|, including the zero-space case.

theorem spectrum_aeval_subset_closedBall_shift_of_mem_of_forall_symmetrized_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hK : IsCompact K) (hc : c ∈ K) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (b : ℂ) : spectrum ℂ ((Polynomial.aeval A) p) ⊆ Metric.closedBall b (polynomialSupNorm (p - Polynomial.C b) K)

If the circle center belongs to the compact control set, the coupled shifted moments force spectrum p(A) into the sharp disk around every scalar b, with radius sup_K |p-b|. The proof keeps the shifted scalar power inside the moment and lets its norm be absorbed asymptotically; the zero Hilbert space is handled by its empty spectrum.

theorem spectralRadius_aeval_sub_smul_one_le_polynomialNorm_sub_C_of_mem_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hK : IsCompact K) (hc : c ∈ K) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (b : ℂ) : spectralRadius ℂ ((Polynomial.aeval A) p - b • 1) ≤ ↑(polynomialSupNorm (p - Polynomial.C b) K).toNNReal

If the circle center belongs to the compact control set, universal circle symmetrization gives a sharp factor-one spectral-radius bound after every scalar shift.

theorem spectrum_aeval_subset_closedBall_shift_of_compactConvex_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {K : Set ℂ} (hcompact : IsCompact K) (hnonempty : K.Nonempty) (hconvex : Convex ℝ K) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (b : ℂ) : spectrum ℂ ((Polynomial.aeval A) p) ⊆ Metric.closedBall b (polynomialSupNorm (p - Polynomial.C b) K)

On a compact nonempty convex control set, universal circle symmetrization supplies the center membership needed by the arbitrary-shift spectral localization theorem; the zero Hilbert space has empty spectrum.

theorem spectralRadius_aeval_sub_smul_one_le_polynomialNorm_sub_C_of_compactConvex_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {K : Set ℂ} (hcompact : IsCompact K) (hnonempty : K.Nonempty) (hconvex : Convex ℝ K) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (b : ℂ) : spectralRadius ℂ ((Polynomial.aeval A) p - b • 1) ≤ ↑(polynomialSupNorm (p - Polynomial.C b) K).toNNReal

Universal circle symmetrization over a compact nonempty convex control set gives a sharp factor-one spectral-radius bound after every scalar shift.

theorem spectralRadius_aeval_le_polynomialNorm_of_compactConvex_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {K : Set ℂ} (hcompact : IsCompact K) (hnonempty : K.Nonempty) (hconvex : Convex ℝ K) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) : spectralRadius ℂ ((Polynomial.aeval A) p) ≤ ↑(polynomialSupNorm p K).toNNReal

Universal circle symmetrization over a compact nonempty convex control set gives the sharp factor-one spectral-radius bound for every polynomial value. This is a spectral conclusion and therefore also covers the zero Hilbert space.

theorem spectrum_aeval_subset_closedBall_shift_closure_numericalRange_of_forall_symmetrized_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q (closure (numericalRange A))) (p : Polynomial ℂ) (b : ℂ) : spectrum ℂ ((Polynomial.aeval A) p) ⊆ Metric.closedBall b (polynomialSupNorm (p - Polynomial.C b) (closure (numericalRange A)))

Universal circle symmetrization controlled by the closed numerical range places spectrum p(A) in every disk centered at b with radius sup_{closure W(A)} |p-b|; the zero Hilbert space has empty spectrum.

theorem spectralRadius_aeval_sub_smul_one_le_polynomialNorm_sub_C_closedNumericalRange_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q (closure (numericalRange A))) (p : Polynomial ℂ) (b : ℂ) : spectralRadius ℂ ((Polynomial.aeval A) p - b • 1) ≤ ↑(polynomialSupNorm (p - Polynomial.C b) (closure (numericalRange A))).toNNReal

Universal circle symmetrization controlled by the closed numerical range gives a sharp factor-one spectral-radius bound after every scalar shift.

theorem spectralRadius_aeval_le_polynomialNorm_closedNumericalRange_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q (closure (numericalRange A))) (p : Polynomial ℂ) : spectralRadius ℂ ((Polynomial.aeval A) p) ≤ ↑(polynomialSupNorm p (closure (numericalRange A))).toNNReal

Universal circle symmetrization controlled by the closed numerical range gives the sharp factor-one spectral-radius bound for every polynomial value, including on the zero Hilbert space.

theorem spectrum_subset_of_isCompact_nonempty_convex_of_forall_symmetrized_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {K : Set ℂ} (hcompact : IsCompact K) (hnonempty : K.Nonempty) (hconvex : Convex ℝ K) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) : spectrum ℂ A ⊆ K

Universal circle symmetrization controlled by a compact nonempty convex set forces that set to contain the spectrum of A. An exterior spectral value would yield a polynomial separator equal to one there and strictly contractive on K, contradicting the corresponding zero-centered shifted spectral disk. The zero Hilbert space has empty spectrum and is handled separately.

theorem norm_aeval_mul_auxiliary_ball_center_le_of_eval_center_le_sqrt_two_sub_one_mul {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (p : Polynomial ℂ) (hsymm : ‖(Polynomial.aeval A) p + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p)‖ ≤ 2 * polynomialSupNorm p K) (hsmall : ‖Polynomial.eval c p‖ ≤ (√2 - 1) * polynomialSupNorm p K) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p‖ ≤ polynomialSupNorm p K ^ 2

The sharp auxiliary product bound holds without any normality assumption whenever the center value is small: if |p(c)| ≤ (sqrt 2 - 1) m, the same-polynomial symmetrized estimate bounds ‖p(A)‖ by 2m + |p(c)|, and the identity (sqrt 2 - 1)^2 + 2 (sqrt 2 - 1) = 1 closes the product estimate.

theorem norm_aeval_le_two_mul_polynomialNorm_sub_C_add_norm_eval_sub_two_mul_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (b : ℂ) : ‖(Polynomial.aeval A) p‖ ≤ 2 * polynomialSupNorm (p - Polynomial.C b) K + ‖Polynomial.eval c p - 2 * b‖

Universal circle symmetrization applied to p - C b controls p(A) after an arbitrary scalar shift. The symmetrized operator is exactly p(A) + (p(c) - 2b)I, giving the displayed quantitative estimate.

theorem isKPolynomialSpectralSet_three_of_isCompact_nonempty_convex_of_forall_symmetrized_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {K : Set ℂ} (hcompact : IsCompact K) (hnonempty : K.Nonempty) (hconvex : Convex ℝ K) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) : IsKPolynomialSpectralSet A 3 K

Universal circle symmetrization controlled by a compact nonempty convex set makes that set a 3-polynomial spectral set. Spectrum containment comes from shifted moments and polynomial separation; the norm estimate is the zero-shift bound 2m + |p(c)| ≤ 3m after center alignment. The zero Hilbert space is discharged separately.

theorem norm_aeval_mul_auxiliary_ball_center_le_of_shifted_scalar_bound_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (b : ℂ) (hscalar : (2 * polynomialSupNorm (p - Polynomial.C b) K + ‖Polynomial.eval c p - 2 * b‖) * ‖Polynomial.eval c p‖ ≤ polynomialSupNorm p K ^ 2) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p‖ ≤ polynomialSupNorm p K ^ 2

Shifting p by an arbitrary scalar before applying universal symmetrization gives a family of sharp-product criteria. The shift b controls p(A) through p(A) + (p(c) - 2b)I; the displayed scalar inequality is exactly what is needed after the triangle estimate.

theorem norm_aeval_mul_auxiliary_ball_center_le_of_half_centered_scalar_bound_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (hscalar : 2 * polynomialSupNorm (p - Polynomial.C (Polynomial.eval c p / 2)) K * ‖Polynomial.eval c p‖ ≤ polynomialSupNorm p K ^ 2) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p‖ ≤ polynomialSupNorm p K ^ 2

The midpoint shift b = p(c) / 2 eliminates the scalar residual in the shifted symmetrization estimate. Thus the displayed bound on sup_K |p - p(c)/2| alone suffices for the literal sharp product.

theorem norm_aeval_mul_auxiliary_ball_center_le_of_centered_scalar_bound_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (hscalar : (2 * polynomialSupNorm (p - Polynomial.C (Polynomial.eval c p)) K + ‖Polynomial.eval c p‖) * ‖Polynomial.eval c p‖ ≤ polynomialSupNorm p K ^ 2) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p‖ ≤ polynomialSupNorm p K ^ 2

Centering p gives an adaptive sharp-product criterion without normality. Universal symmetrization bounds p(A) - p(c)I by twice the sup norm of p - p(c); hence the displayed scalar inequality suffices for the literal auxiliary product bound.

theorem norm_aeval_mul_auxiliary_ball_center_le_of_centered_polynomialNorm_le_sub_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) {K : Set ℂ} (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q K) (p : Polynomial ℂ) (hcentered : polynomialSupNorm (p - Polynomial.C (Polynomial.eval c p)) K ≤ polynomialSupNorm p K - ‖Polynomial.eval c p‖) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p‖ ≤ polynomialSupNorm p K ^ 2

The sharp auxiliary product bound also holds without normality in the near-constant regime. If the sup norm of p - p(c) is at most m - |p(c)|, universal symmetrization bounds the centered operator by twice that variation, and (m - |p(c)|)^2 ≥ 0 closes the exact product estimate.

theorem norm_aeval_mul_auxiliary_ball_center_le_one_add_sqrt_two_mul_sq_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q (closure (numericalRange A))) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p‖ ≤ (1 + √2) * polynomialSupNorm p (closure (numericalRange A)) ^ 2

For an arbitrary operator, universal sharp symmetrization on an enclosing circle implies an auxiliary product bound with the global 1 + sqrt 2 Crouzeix--Palencia factor. The universal family first aligns the circle center with the closed numerical range; scalar evaluation is then sharp, while polynomial evaluation uses the unconditional global bound.

theorem norm_aeval_mul_auxiliary_ball_center_le_of_isStarNormal_aeval_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q (closure (numericalRange A))) (p : Polynomial ℂ) [IsStarNormal ((Polynomial.aeval A) p)] : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p‖ ≤ polynomialSupNorm p (closure (numericalRange A)) ^ 2

Universal sharp symmetrization on an enclosing circle implies the literal sharp auxiliary product bound for every polynomial whose individual value p(A) is star-normal. The ambient operator need not be star-normal.

theorem norm_aeval_mul_auxiliary_ball_center_le_of_isStarNormal_of_symmetrization {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) [IsStarNormal A] (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (hsymm : ∀ (q : Polynomial ℂ), ‖(Polynomial.aeval A) q + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) q)‖ ≤ 2 * polynomialSupNorm q (closure (numericalRange A))) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p * crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p‖ ≤ polynomialSupNorm p (closure (numericalRange A)) ^ 2

In the star-normal branch, universal sharp symmetrization on an enclosing circle implies the literal sharp auxiliary product bound for every polynomial.