Direct polynomial consequences of the Crouzeix--Palencia theorem

The spectral-set statement is naturally formulated on the closed numerical range because the spectrum need not lie in the numerical range itself. Polynomial sup norms, however, are unchanged by closing a bounded set. This file records the standard norm inequality directly on the numerical range and specializes it to powers, centered operators, and the numerical radius.

theorem polynomialSupNorm_closure_numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (p : Polynomial ℂ) : polynomialSupNorm p (closure (numericalRange A)) = polynomialSupNorm p (numericalRange A)

Closing the numerical range does not alter a polynomial sup norm.

theorem polynomialSupNorm_X_numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : polynomialSupNorm Polynomial.X (numericalRange A) = numericalRadius A

The polynomial sup norm of X on the numerical range is the numerical radius.

theorem iSup_norm_pow_numericalRange_le_numericalRadius_pow {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (n : ℕ) : ⨆ z ∈ numericalRange A, ‖z ^ n‖ ≤ numericalRadius A ^ n

The supremum of the nth powers on the numerical range is bounded by the nth power of the numerical radius.

theorem norm_aeval_le_one_add_sqrt_two_mul_polynomialSupNorm_numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p‖ ≤ (1 + √2) * polynomialSupNorm p (numericalRange A)

The usual norm form of the Crouzeix--Palencia theorem, with the supremum taken directly over the numerical range.

theorem norm_le_one_add_sqrt_two_mul_numericalRadius {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : ‖A‖ ≤ (1 + √2) * numericalRadius A

The Crouzeix--Palencia numerical-radius bound for an operator.

theorem norm_sub_smul_one_le_one_add_sqrt_two_mul_numericalRadius {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) : ‖A - c • 1‖ ≤ (1 + √2) * numericalRadius (A - c • 1)

The Crouzeix--Palencia numerical-radius bound centered at an arbitrary scalar operator.

theorem norm_pow_le_one_add_sqrt_two_mul_iSup_numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (n : ℕ) : ‖A ^ n‖ ≤ (1 + √2) * ⨆ z ∈ numericalRange A, ‖z ^ n‖

Every power of an operator is controlled by the corresponding power on its numerical range.

theorem norm_pow_le_one_add_sqrt_two_mul_numericalRadius_pow {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (n : ℕ) : ‖A ^ n‖ ≤ (1 + √2) * numericalRadius A ^ n

Every operator power is controlled directly by the corresponding power of the numerical radius with the Crouzeix--Palencia constant.

theorem norm_pow_sub_smul_one_le_one_add_sqrt_two_mul_numericalRadius_pow {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) (n : ℕ) : ‖(A - c • 1) ^ n‖ ≤ (1 + √2) * numericalRadius (A - c • 1) ^ n

Every centered operator power is controlled by the corresponding power of its centered numerical radius.

theorem norm_pow_le_one_add_sqrt_two_of_numericalRadius_le_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : numericalRadius A ≤ 1) (n : ℕ) : ‖A ^ n‖ ≤ 1 + √2

Operators in the numerical-radius unit ball are uniformly power-bounded by the Crouzeix--Palencia constant.

theorem norm_pow_sub_smul_one_le_one_add_sqrt_two_of_numericalRadius_le_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) (hA : numericalRadius (A - c • 1) ≤ 1) (n : ℕ) : ‖(A - c • 1) ^ n‖ ≤ 1 + √2

A centered operator in the numerical-radius unit ball is uniformly power-bounded by the Crouzeix--Palencia constant.

theorem tendsto_pow_atTop_nhds_zero_of_numericalRadius_lt_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : numericalRadius A < 1) : Filter.Tendsto (fun (n : ℕ) => A ^ n) Filter.atTop (nhds 0)

If the numerical radius is strictly less than one, the operator powers converge to zero in operator norm.

theorem tendsto_pow_sub_smul_one_atTop_nhds_zero_of_numericalRadius_lt_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) (hA : numericalRadius (A - c • 1) < 1) : Filter.Tendsto (fun (n : ℕ) => (A - c • 1) ^ n) Filter.atTop (nhds 0)

If a centered numerical radius is strictly less than one, the powers of the centered operator converge to zero in operator norm.

theorem norm_sub_smul_one_le_one_add_sqrt_two_mul_iSup_numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) : ‖A - c • 1‖ ≤ (1 + √2) * ⨆ z ∈ numericalRange A, ‖z - c‖

A centered form of the bound: the distance of A from a scalar operator is controlled by the farthest point of its numerical range from that scalar.

theorem norm_aeval_mul_aeval_le_one_add_sqrt_two_mul_iSup_numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (p q : Polynomial ℂ) : ‖(Polynomial.aeval A) p * (Polynomial.aeval A) q‖ ≤ (1 + √2) * ⨆ z ∈ numericalRange A, ‖Polynomial.eval z p * Polynomial.eval z q‖

A product of two polynomial functional-calculus values is controlled with a single Crouzeix--Palencia constant.

theorem norm_aeval_pow_le_one_add_sqrt_two_mul_iSup_numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (p : Polynomial ℂ) (n : ℕ) : ‖(Polynomial.aeval A) p ^ n‖ ≤ (1 + √2) * ⨆ z ∈ numericalRange A, ‖Polynomial.eval z p ^ n‖

Powers of a polynomial functional-calculus value retain a single Crouzeix--Palencia constant.