Operator-valued Cauchy formula on a centered circle

This file proves the circle model of the operator-valued Cauchy formula used in the Crouzeix--Palencia argument. If a circle has radius strictly larger than the norm of an element A in a complex Banach algebra, then the normalized contour integral of its resolvent is the identity. Multiplying the integrand by a polynomial recovers polynomial evaluation at A.

The resolvent identity is proved directly from the uniformly convergent Laurent expansion

R_A(z) = sum n, z^(-(n + 1)) • A^n.

Thus no holomorphic-functional-calculus theorem is hidden in the result. The present hypotheses describe the centered disk model ‖A‖ < R; they do not replace the separate smooth-domain or numerical-range approximation needed for the full Crouzeix--Palencia capstone.

Main declarations

• normalized_circleIntegral_resolvent_eq_one -- the normalized resolvent integral is the identity.
• circleIntegral_resolvent_eq_two_pi_I_smul_one -- the same identity in the unnormalized form used by double-layer mass calculations.
• circleIntegral_resolvent_eq_two_pi_I_smul_one_of_norm_sub_smul_one_lt -- the corresponding identity on a circle with arbitrary center.
• normalized_circleIntegral_zpow_smul_resolvent_eq_pow -- the monomial operator Cauchy formula.
• normalized_circleIntegral_inv_pow_smul_resolvent_eq_zero -- every strictly negative Laurent mode of the centered resolvent integral vanishes.
• normalized_circleIntegral_eval_smul_resolvent_eq_aeval -- the polynomial operator Cauchy formula.

theorem normalized_circleIntegral_resolvent_eq_one_of_normOne {B : Type u} [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [NormOneClass B] (A : B) {R : ℝ} (hR : ‖A‖ < R) : (2 * ↑Real.pi * Complex.I)⁻¹ • circleIntegral (resolvent A) 0 R = 1

The normalized resolvent integral on a centered circle enclosing A is the identity. The strict norm bound supplies a uniformly convergent Laurent series on the whole circle.

theorem normalized_circleIntegral_zpow_smul_resolvent_eq_pow_of_normOne {B : Type u} [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [NormOneClass B] (A : B) {R : ℝ} (hR : ‖A‖ < R) (n : ℕ) : (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(0, R), z ^ n • resolvent A z = A ^ n

The normalized resolvent integral sends the scalar monomial z^n to the algebra power A^n.

theorem normalized_circleIntegral_eval_smul_resolvent_eq_aeval_of_normOne {B : Type u} [NormedRing B] [NormedAlgebra ℂ B] [CompleteSpace B] [NormOneClass B] (A : B) {R : ℝ} (hR : ‖A‖ < R) (p : Polynomial ℂ) : (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(0, R), Polynomial.eval z p • resolvent A z = (Polynomial.aeval A) p

The operator-valued Cauchy formula for polynomials on a centered circle: integrating p(z) R_A(z) recovers p(A).

theorem normalized_circleIntegral_inv_pow_smul_resolvent_eq_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) (n : ℕ) (hn : 0 < n) : (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(0, R), z⁻¹ ^ n • resolvent A z = 0

Every strictly negative Laurent mode of the normalized centered resolvent integral vanishes.

theorem normalized_circleIntegral_resolvent_eq_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) : (2 * ↑Real.pi * Complex.I)⁻¹ • circleIntegral (resolvent A) 0 R = 1

The normalized resolvent integral for an operator on any complex Hilbert space, including the zero space.

theorem circleIntegral_resolvent_eq_two_pi_I_smul_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) : circleIntegral (resolvent A) 0 R = (2 * ↑Real.pi * Complex.I) • 1

Unnormalized form of the resolvent Cauchy identity, matching the mass hypothesis used by the double-layer normalization lemmas.

theorem normalized_circleIntegral_zpow_smul_resolvent_eq_pow {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) (n : ℕ) : (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(0, R), z ^ n • resolvent A z = A ^ n

The monomial operator Cauchy formula on any complex Hilbert space.

theorem normalized_circleIntegral_eval_smul_resolvent_eq_aeval {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) (p : Polynomial ℂ) : (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(0, R), Polynomial.eval z p • resolvent A z = (Polynomial.aeval A) p

The polynomial operator Cauchy formula on any complex Hilbert space.

theorem circleIntegral_eval_smul_resolvent_eq_two_pi_I_smul_aeval {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {R : ℝ} (hR : ‖A‖ < R) (p : Polynomial ℂ) : ∮ (z : ℂ) in C(0, R), Polynomial.eval z p • resolvent A z = (2 * ↑Real.pi * Complex.I) • (Polynomial.aeval A) p

Unnormalized polynomial operator Cauchy formula.

theorem resolvent_sub_smul_one_shift {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (c z : ℂ) : resolvent (A - c • 1) z = resolvent A (z + c)

Translating both the operator and spectral parameter by c leaves the resolvent unchanged.

theorem circleIntegral_resolvent_eq_two_pi_I_smul_one_of_norm_sub_smul_one_lt {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) {R : ℝ} (hR : ‖A - c • 1‖ < R) : circleIntegral (resolvent A) c R = (2 * ↑Real.pi * Complex.I) • 1

The unnormalized resolvent Cauchy identity on a circle centered at c. The hypothesis is the translated Neumann-series condition ‖A - c • 1‖ < R.