The disk auxiliary operator at an arbitrary center under spectral enclosure (L4.2 support)

SpectralAuxiliary.lean identifies the conjugate-polynomial auxiliary operator of the centered disk ball 0 r with star (p.eval 0) • 1 whenever σ(A) ⊆ ball 0 r. Translating by AffineAuxiliary.lean (G(A, ball c r, p) = G(A - c•1, ball 0 r, p(z + c))) and the spectrum shift σ(A - c•1) = σ(A) - {c}, the same holds at any center: G = star (p.eval c) • 1 whenever σ(A) ⊆ ball c r. Combined with the symmetrized bound of SpectralCauchy.lean, this gives the classical-looking estimate ‖p(A) + p(c) • 1‖ ≤ 2 * sup_{|z - c| ≤ r} ‖p(z)‖ whenever the closure of the numerical range lies in the open disk ball c r.

Main declarations

• spectrum_sub_smul_one_subset_ball_of_subset_ball — the spectrum shift.
• auxiliary_ball_center_eq_eval_center_smul_one_of_spectrum_subset_ball
• norm_aeval_add_eval_center_smul_one_le_of_closure_numericalRange_subset_ball
• norm_aeval_le_three_mul_polynomialSupNorm_of_numericalRange_subset_ball, isKPolynomialSpectralSet_three_closedBall_of_closure_numericalRange_subset_ball — an open disk containing closure (numericalRange A) yields a 3-polynomial-spectral set (from the symmetrized bound and |p(c)| ≤ sup; the sharp constant needs the product estimate).
• isKPolynomialSpectralSet_three_closedBall_of_closure_numericalRange_subset_closedBall — the same for a closed disk closure (numericalRange A) ⊆ closedBall c r, by passing to the limit through the open disks ball c (r + 1/(n+1)) (ApproximationSupNorm.lean).

theorem spectrum_sub_smul_one_subset_ball_of_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {c : ℂ} {r : ℝ} (hσ : spectrum ℂ A ⊆ Metric.ball c r) : spectrum ℂ (A - c • 1) ⊆ Metric.ball 0 r

Translating the spectrum: if σ(A) ⊆ ball c r then σ(A - c • 1) ⊆ ball 0 r.

theorem auxiliary_ball_center_eq_eval_center_smul_one_of_spectrum_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {r : ℝ} (hr : 0 < r) (hσ : spectrum ℂ A ⊆ Metric.ball c r) (p : Polynomial ℂ) : crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c r hr) p = star (Polynomial.eval c p) • 1

The disk auxiliary operator with center c under spectral enclosure equals star (p.eval c) • 1.

theorem norm_aeval_add_eval_center_smul_one_le_of_closure_numericalRange_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {r : ℝ} (hr : 0 < r) (hW : closure (numericalRange A) ⊆ Metric.ball c r) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p + Polynomial.eval c p • 1‖ ≤ 2 * polynomialSupNorm p (Metric.closedBall c r)

Classical symmetrized bound for a disk containing the numerical range: if closure W(A) ⊆ ball c r, then ‖p(A) + p(c) • 1‖ ≤ 2 * sup_{|z - c| ≤ r} ‖p(z)‖.

A 3-polynomial-spectral set from the symmetrized bound alone

theorem norm_aeval_le_three_mul_polynomialSupNorm_of_numericalRange_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {r : ℝ} (hr : 0 < r) (hW : closure (numericalRange A) ⊆ Metric.ball c r) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p‖ ≤ 3 * polynomialSupNorm p (Metric.closedBall c r)

If closure W(A) ⊆ ball c r, then ‖p(A)‖ ≤ 3 * sup_{|z - c| ≤ r} ‖p(z)‖.

theorem isKPolynomialSpectralSet_three_closedBall_of_closure_numericalRange_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {r : ℝ} (hr : 0 < r) (hW : closure (numericalRange A) ⊆ Metric.ball c r) : IsKPolynomialSpectralSet A 3 (Metric.closedBall c r)

Disks containing the numerical range are 3-polynomial-spectral sets: if closure W(A) ⊆ ball c r, then closedBall c r is a 3-polynomial-spectral set for A.

Closed disks, by passing to the limit

theorem iInter_closedBall_add_inv_succ (c : ℂ) (r : ℝ) : ⋂ (n : ℕ), Metric.closedBall c (r + 1 / (↑n + 1)) = Metric.closedBall c r

The closed disks closedBall c (r + 1 / (n + 1)) intersect to closedBall c r.

theorem norm_aeval_le_three_mul_polynomialNorm_of_numericalRange_subset_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {r : ℝ} (hr : 0 ≤ r) (hW : closure (numericalRange A) ⊆ Metric.closedBall c r) (p : Polynomial ℂ) : ‖(Polynomial.aeval A) p‖ ≤ 3 * polynomialSupNorm p (Metric.closedBall c r)

If closure W(A) ⊆ closedBall c r with 0 ≤ r, then ‖p(A)‖ ≤ 3 * sup_{|z - c| ≤ r} ‖p(z)‖.

theorem isKPolynomialSpectralSet_three_closedBall_of_closure_numericalRange_subset_closedBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {r : ℝ} (hr : 0 ≤ r) (hW : closure (numericalRange A) ⊆ Metric.closedBall c r) : IsKPolynomialSpectralSet A 3 (Metric.closedBall c r)

Closed disks containing the numerical range are 3-polynomial-spectral sets.