Operator theory (Solution)

Compatibility namespace for the upstream CrouzeixPalenciaChallenge.lean statements. The definitions abbreviate the proof library's public representations, and the theorems delegate to its proofs.

@[reducible, inline]

noncomputable abbrev PalomarCrouzeixPalencia.numericalRange {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : Set ℂ

The numerical range of a bounded operator.

Equations

• PalomarCrouzeixPalencia.numericalRange A = numericalRange A

@[reducible, inline]

noncomputable abbrev PalomarCrouzeixPalencia.polynomialSupNorm (p : Polynomial ℂ) (X : Set ℂ) : ℝ

The supremum norm of a polynomial on a set.

Equations

• PalomarCrouzeixPalencia.polynomialSupNorm p X = polynomialSupNorm p X

@[reducible, inline]

abbrev PalomarCrouzeixPalencia.IsKPolynomialSpectralSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (K : ℝ) (X : Set ℂ) : Prop

The predicate that X is a K-polynomial spectral set for A.

Equations

• PalomarCrouzeixPalencia.IsKPolynomialSpectralSet A K X = IsKPolynomialSpectralSet A K X

theorem PalomarCrouzeixPalencia.exists_unitary_power_dilation {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (T : E →L[ℂ] E) (hT : ‖T‖ ≤ 1) : ∃ (H : Type u) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℂ H) (x_2 : CompleteSpace H) (V : E →L[ℂ] H) (U : H →L[ℂ] H), (∀ (x_3 y : E), inner ℂ (V x_3) (V y) = inner ℂ x_3 y) ∧ U ∈ unitary (H →L[ℂ] H) ∧ ∀ (n : ℕ) (x_3 : E), (ContinuousLinearMap.adjoint V) ((U ^ n) (V x_3)) = (T ^ n) x_3

theorem PalomarCrouzeixPalencia.vonNeumann_inequality {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (T : E →L[ℂ] E) (hT : ‖T‖ ≤ 1) (p : Polynomial ℂ) : ‖(Polynomial.aeval T) p‖ ≤ polynomialSupNorm p (Metric.closedBall 0 1)

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