Affine transport of the polynomial auxiliary operator

Translation of the circle center is accompanied by translation of the operator and precomposition of the polynomial. The parameterized auxiliary contour is unchanged under these three simultaneous operations.

Main declaration

• crouzeixPolynomialAuxiliaryOperator_ball_center_of_resolvent_shift -- transports the auxiliary operator from ball c R to the centered ball, given the explicit translated-resolvent identity.
• crouzeixPolynomialAuxiliaryOperator_ball_center -- the unconditional transport identity, using the resolvent translation formula.
• crouzeixPolynomialAuxiliaryOperator_ball_center_eq_eval_center_smul_one -- the resulting scalar auxiliary identity on an arbitrary enclosing disk.

theorem crouzeixPolynomialAuxiliaryOperator_ball_center_of_resolvent_shift {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) (hshift : ∀ (z : ℂ), resolvent (A - c • 1) z = resolvent A (z + c)) : crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R hR) p = crouzeixPolynomialAuxiliaryOperator (A - c • 1) (SmoothJordanDomain.ball 0 R hR) (p.affineComposition 1 c)

The polynomial auxiliary contour on ball c R agrees with the centered contour for A - cI and the translated polynomial z ↦ p(z + c), provided the corresponding translated-resolvent identity is available.

theorem crouzeixPolynomialAuxiliaryOperator_ball_center {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hR : 0 < R) (p : Polynomial ℂ) : crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R hR) p = crouzeixPolynomialAuxiliaryOperator (A - c • 1) (SmoothJordanDomain.ball 0 R hR) (p.affineComposition 1 c)

Translating the circle center, the operator, and the polynomial leaves the polynomial auxiliary contour operator unchanged.

theorem crouzeixPolynomialAuxiliaryOperator_ball_center_eq_eval_center_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hA : ‖A - c • 1‖ < R) (p : Polynomial ℂ) : crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c R ⋯) p = star (Polynomial.eval c p) • 1

If ‖A - cI‖ < R, the polynomial auxiliary operator on the disk centered at c is the constant operator star (p.eval c) • 1.