Affine homotopy invariance of the resolvent contour mass

The contour integral of the operator resolvent is constant along a commuting affine operator path as long as the contour stays in the resolvent set. For the path from a scalar operator c • 1 to A, convexity of the carrier and the spectral inclusion spectrum A ⊆ closure (numericalRange A) provide that resolvent-set condition. Oriented scalar winding then computes the common mass as 2 * pi * I • 1.

theorem hasDerivAt_resolvent_affineOperator {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (B D : E →L[ℂ] E) (s z : ℂ) (hres : z ∈ resolventSet ℂ (B + s • D)) : HasDerivAt (fun (w : ℂ) => resolvent (B + w • D) z) (resolvent (B + s • D) z * D * resolvent (B + s • D) z) s

theorem hasDerivAt_contourIntegral_resolvent_affineOperator {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (B D : E →L[ℂ] E) (Omega : SmoothJordanDomain) (s : ℂ) {epsilon C : ℝ} (hepsilon : 0 < epsilon) (hC : 0 ≤ C) (hres : ∀ w ∈ Metric.ball s epsilon, ∀ (t : ℝ), Omega.boundaryParam t ∈ resolventSet ℂ (B + w • D)) (hbound : ∀ w ∈ Metric.ball s epsilon, ∀ (t : ℝ), ‖resolvent (B + w • D) (Omega.boundaryParam t)‖ ≤ C) : HasDerivAt (fun (w : ℂ) => contourIntegral (resolvent (B + w • D)) Omega.boundaryParam) (contourIntegral (fun (z : ℂ) => resolvent (B + s • D) z * D * resolvent (B + s • D) z) Omega.boundaryParam) s

theorem exists_resolvent_affineOperator_neighborhood_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (B D : E →L[ℂ] E) (Omega : SmoothJordanDomain) (s : ℂ) (hres : ∀ (t : ℝ), Omega.boundaryParam t ∈ resolventSet ℂ (B + s • D)) : ∃ (epsilon : ℝ) (C : ℝ), 0 < epsilon ∧ 0 ≤ C ∧ ∀ w ∈ Metric.ball s epsilon, ∀ (t : ℝ), Omega.boundaryParam t ∈ resolventSet ℂ (B + w • D) ∧ ‖resolvent (B + w • D) (Omega.boundaryParam t)‖ ≤ C

theorem hasDerivAt_contourIntegral_resolvent_affineOperator_of_boundary_subset_resolventSet {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (B D : E →L[ℂ] E) (Omega : SmoothJordanDomain) (s : ℂ) (hres : ∀ (t : ℝ), Omega.boundaryParam t ∈ resolventSet ℂ (B + s • D)) : HasDerivAt (fun (w : ℂ) => contourIntegral (resolvent (B + w • D)) Omega.boundaryParam) (contourIntegral (fun (z : ℂ) => resolvent (B + s • D) z * D * resolvent (B + s • D) z) Omega.boundaryParam) s

theorem commute_resolvent_of_commute {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (B D : E →L[ℂ] E) (z : ℂ) (hDB : Commute D B) (hres : z ∈ resolventSet ℂ B) : Commute D (resolvent B z)

theorem contourIntegral_const_mul_resolvent_sq_eq_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (B D : E →L[ℂ] E) (Omega : SmoothJordanDomain) (hres : ∀ (t : ℝ), Omega.boundaryParam t ∈ resolventSet ℂ B) : contourIntegral (fun (z : ℂ) => D * resolvent B z ^ 2) Omega.boundaryParam = 0

theorem contourIntegral_const_mul_resolvent_sq_eq_zero_of_numericalRange {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (B D : E →L[ℂ] E) (Omega : SmoothJordanDomain) (hOmega : closure (numericalRange B) ⊆ Omega.carrier) : contourIntegral (fun (z : ℂ) => D * resolvent B z ^ 2) Omega.boundaryParam = 0

theorem hasDerivAt_contourIntegral_resolvent_affineOperator_eq_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (B D : E →L[ℂ] E) (Omega : SmoothJordanDomain) (s : ℂ) (hBD : Commute B D) (hres : ∀ (t : ℝ), Omega.boundaryParam t ∈ resolventSet ℂ (B + s • D)) : HasDerivAt (fun (w : ℂ) => contourIntegral (resolvent (B + w • D)) Omega.boundaryParam) 0 s

theorem contourIntegral_resolvent_affineOperator_eq_of_boundary_subset_resolventSet {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (B D : E →L[ℂ] E) (Omega : SmoothJordanDomain) (hBD : Commute B D) (hres : ∀ r ∈ Set.Icc 0 1, ∀ (t : ℝ), Omega.boundaryParam t ∈ resolventSet ℂ (B + ↑r • D)) : contourIntegral (resolvent (B + D)) Omega.boundaryParam = contourIntegral (resolvent B) Omega.boundaryParam

theorem spectrum_affine_smul_one_subset_convex_carrier {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) (r : ℝ) (hr : r ∈ Set.Icc 0 1) : spectrum ℂ (c • 1 + ↑r • (A - c • 1)) ⊆ Omega.carrier

theorem contourIntegral_resolvent_eq_scalar_of_convex_carrier {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : contourIntegral (resolvent A) Omega.boundaryParam = contourIntegral (resolvent (c • 1)) Omega.boundaryParam

theorem resolvent_smul_one_eq_inv_smul_one {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (c z : ℂ) (hz : z ≠ c) : resolvent (c • 1) z = (z - c)⁻¹ • 1

theorem contourIntegral_resolvent_smul_one_eq_scalar {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) : contourIntegral (resolvent (c • 1)) Omega.boundaryParam = contourIntegral (fun (z : ℂ) => (z - c)⁻¹) Omega.boundaryParam • 1

theorem contourIntegral_resolvent_eq_two_pi_I_smul_one_of_oriented_convex_carrier_of_nontrivial {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [Nontrivial E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (hcside : ∀ (t : ℝ), ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : contourIntegral (resolvent A) Omega.boundaryParam = (2 * ↑Real.pi * Complex.I) • 1

theorem contourIntegral_resolvent_eq_two_pi_I_smul_one_of_oriented_convex_carrier {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (Omega : SmoothJordanDomain) (c : ℂ) (hc : c ∈ Omega.carrier) (hcside : ∀ (t : ℝ), ((starRingEnd ℂ) (-Complex.I * deriv Omega.boundaryParam t) * (c - Omega.boundaryParam t)).re ≤ 0) (hOmega : closure (numericalRange A) ⊆ Omega.carrier) : contourIntegral (resolvent A) Omega.boundaryParam = (2 * ↑Real.pi * Complex.I) • 1

Oriented convex geometry computes the operator resolvent contour mass. The subsingleton case is automatic, while in the nontrivial case the affine homotopy joins A to the scalar operator at the oriented carrier point.