Von Neumann's inequality (L4.1) #

For a contraction T on a complex Hilbert space E and a polynomial p, ‖p(T)‖ ≤ sup_{‖z‖ ≤ 1} ‖p(z)‖.

Route (task-spec L4.1, via dilation): the Schäffer dilation (L3.1) gives a Hilbert space H, an inner-product-preserving V : E →L[ℂ] H and a unitary U on H with V† U^n V = T^n for all n. Then

V† p(U) V = p(T) by linearity (adjoint_aeval_apply_of_forall_pow);
‖p(T)‖ ≤ ‖V†‖ ‖p(U)‖ ‖V‖ ≤ ‖p(U)‖ since ‖V†‖ = ‖V‖ ≤ 1 (norm_aeval_le_norm_aeval_of_dilation);
for unitary U the element p(U) is normal, so ‖p(U)‖ equals its spectral radius; the spectral mapping theorem and σ(U) ⊆ 𝕊¹ ⊆ closedBall 0 1 bound this by the sup-norm of p on the closed unit disk (norm_aeval_le_polynomialSupNorm_closedBall_of_mem_unitary).

Main declarations #

norm_eval_le_polynomialSupNorm — ‖p.eval z‖ ≤ polynomialSupNorm p X for z ∈ X whenever the values of p on X are bounded; polynomialSupNorm_nonneg; and bddAbove_norm_eval_image_of_isCompact for compact X.
norm_aeval_le_polynomialSupNorm_closedBall_of_mem_unitary — step 3, in any C*-algebra.
adjoint_aeval_apply_of_forall_pow, norm_aeval_le_norm_aeval_of_dilation — steps 1–2.
vonNeumann_inequality_of_exists_unitary_power_dilation — the inequality for any T admitting a unitary power dilation (the exact conclusion of L3.1 as a hypothesis).
vonNeumann_inequality — the boundary theorem for contractions, obtained by applying the preceding dilation inequality to L3.1 (exists_unitary_power_dilation).

Requires [CompleteSpace E] (adjoints, the C*-algebra structure on E →L[ℂ] E).

The polynomial sup-norm #

source

theorem polynomialSupNorm_nonneg (p : Polynomial ℂ) (X : Set ℂ) :

0 ≤ polynomialSupNorm p X

The polynomial sup-norm is nonnegative.

source

theorem norm_eval_le_polynomialSupNorm (p : Polynomial ℂ) {X : Set ℂ} (hX : BddAbove ((fun (z : ℂ) => ‖Polynomial.eval z p‖) '' X)) {z : ℂ} (hz : z ∈ X) :

‖Polynomial.eval z p‖ ≤ polynomialSupNorm p X

If the values ‖p.eval z‖, z ∈ X, are bounded above, then each of them is at most polynomialSupNorm p X.

source

theorem bddAbove_norm_eval_image_of_isCompact (p : Polynomial ℂ) {K : Set ℂ} (hK : IsCompact K) :

BddAbove ((fun (z : ℂ) => ‖Polynomial.eval z p‖) '' K)

On a compact set the values ‖p.eval z‖ are bounded above.

Polynomials in a unitary #

source

theorem norm_aeval_le_polynomialSupNorm_closedBall_of_mem_unitary {A : Type u_1} [CStarAlgebra A] {U : A} (hU : U ∈ unitary A) (p : Polynomial ℂ) :

‖(Polynomial.aeval U) p‖ ≤ polynomialSupNorm p (Metric.closedBall 0 1)

Von Neumann's inequality for unitaries, in any C*-algebra: for U unitary, ‖p(U)‖ ≤ sup_{‖z‖ ≤ 1} ‖p(z)‖. Since p(U) is normal, ‖p(U)‖ is its spectral radius, and σ(p(U)) = p(σ(U)) with σ(U) contained in the unit circle.

Compression through a power dilation #

source

theorem adjoint_aeval_apply_of_forall_pow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : E →L[ℂ ] E) (V : E →L[ℂ ] H) (U : H →L[ℂ ] H) (hpow : ∀ (n : ℕ) (x : E), (ContinuousLinearMap.adjoint V) ((U ^ n) (V x)) = (T ^ n) x) (p : Polynomial ℂ) (x : E) :

(ContinuousLinearMap.adjoint V) (((Polynomial.aeval U) p) (V x)) = ((Polynomial.aeval T) p) x

If V† U^n V = T^n for all n, then V† p(U) V = p(T) for every polynomial p.

source

theorem norm_aeval_le_norm_aeval_of_dilation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (T : E →L[ℂ ] E) (V : E →L[ℂ ] H) (U : H →L[ℂ ] H) (hV : ∀ (x y : E), inner ℂ (V x) (V y) = inner ℂ x y) (hpow : ∀ (n : ℕ) (x : E), (ContinuousLinearMap.adjoint V) ((U ^ n) (V x)) = (T ^ n) x) (p : Polynomial ℂ) :

‖(Polynomial.aeval T) p‖ ≤ ‖(Polynomial.aeval U) p‖

If V preserves inner products and V† U^n V = T^n for all n, then ‖p(T)‖ ≤ ‖p(U)‖ for every polynomial p.