Circle Cauchy formulas under spectral enclosure (L4.2 support)

CircleCauchy.lean proves the operator Cauchy formulas on a circle C(0, R) under the operator-norm hypothesis ‖A‖ < R (Neumann series). Here they are transferred to any circle C(0, r) whose open disk contains the spectrum: the integrand z ↦ p(z) • R_A(z) is holomorphic on the resolvent set, which contains the closed annulus {r ≤ |z| ≤ R} when σ(A) ⊆ ball 0 r, so Mathlib's concentric-annulus Cauchy theorem (Complex.circleIntegral_eq_of_differentiable_on_annulus_off_countable) identifies the integral over C(0, r) with the one over the Neumann circle C(0, ‖A‖ + r).

Since σ(A) ⊆ closure W(A) (L2.2), this yields the symmetrized Crouzeix–Palencia estimate for the disk under the numerical-range hypothesis closure W(A) ⊆ ball 0 r, replacing the operator-norm enclosure of CircleSymmetrized.lean.

Main declarations

• circleIntegral_eval_smul_resolvent_eq_of_spectrum_subset_ball, circleIntegral_resolvent_eq_of_spectrum_subset_ball — annulus deformation of the resolvent kernels (any center, 0 < r ≤ R).
• normalized_circleIntegral_eval_smul_resolvent_eq_aeval_of_spectrum_subset_ball, circleIntegral_resolvent_eq_two_pi_I_smul_one_of_spectrum_subset_ball — the Cauchy formulas on C(0, r) for σ(A) ⊆ ball 0 r.
• norm_aeval_add_star_auxiliary_ball_le_of_closedNumericalRange_subset_ball — ‖p(A) + G†‖ ≤ 2 * sup_{|z| ≤ r} ‖p(z)‖ whenever closure (numericalRange A) ⊆ ball 0 r.
• circleIntegral_smul_resolvent_eq_of_spectrum_subset_ball — the deformation for a general scalar weight g holomorphic off the disk, and normalized_circleIntegral_inv_pow_smul_resolvent_eq_zero_of_spectrum_subset_ball — vanishing of the negative Laurent modes of the resolvent under spectral enclosure.
• circleIntegral_eval_smul_resolvent_eq_center, normalized_circleIntegral_eval_smul_resolvent_eq_aeval_of_norm_sub_smul_one_lt, normalized_circleIntegral_eval_smul_resolvent_eq_aeval_of_spectrum_subset_ball_center, circleIntegral_resolvent_eq_two_pi_I_smul_one_of_spectrum_subset_ball_center — the same formulas on a circle C(c, r) with arbitrary center, and norm_aeval_add_star_auxiliary_ball_le_of_closedNumericalRange_subset_ball_center — the symmetrized bound for an arbitrary open disk containing closure (numericalRange A).

The product side of the Crouzeix–Palencia argument is not upgraded here: the disk product bound of CircleProduct.lean uses von Neumann's inequality, which needs ‖A‖ ≤ r.

theorem mem_resolventSet_of_notMem_ball_of_spectrum_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {c : ℂ} {r : ℝ} (hσ : spectrum ℂ A ⊆ Metric.ball c r) {z : ℂ} (hz : z ∉ Metric.ball c r) : z ∈ resolventSet ℂ A

Points outside an open disk containing the spectrum lie in the resolvent set.

theorem differentiableAt_eval_smul_resolvent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (p : Polynomial ℂ) {z : ℂ} (hz : z ∈ resolventSet ℂ A) : DifferentiableAt ℂ (fun (w : ℂ) => Polynomial.eval w p • resolvent A w) z

z ↦ p(z) • R_A(z) is differentiable at every point of the resolvent set.

theorem circleIntegral_eval_smul_resolvent_eq_of_spectrum_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {r R : ℝ} (hr : 0 < r) (hrR : r ≤ R) (hσ : spectrum ℂ A ⊆ Metric.ball c r) (p : Polynomial ℂ) : ∮ (z : ℂ) in C(c, r), Polynomial.eval z p • resolvent A z = ∮ (z : ℂ) in C(c, R), Polynomial.eval z p • resolvent A z

Cauchy deformation for the resolvent kernel. If the spectrum lies in ball c r and 0 < r ≤ R, the circle integrals of p(z) • R_A(z) over C(c, r) and C(c, R) agree.

theorem circleIntegral_resolvent_eq_of_spectrum_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {r R : ℝ} (hr : 0 < r) (hrR : r ≤ R) (hσ : spectrum ℂ A ⊆ Metric.ball c r) : circleIntegral (resolvent A) c r = circleIntegral (resolvent A) c R

The same deformation for the bare resolvent z ↦ R_A(z).

theorem normalized_circleIntegral_eval_smul_resolvent_eq_aeval_of_spectrum_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {r : ℝ} (hr : 0 < r) (hσ : spectrum ℂ A ⊆ Metric.ball 0 r) (p : Polynomial ℂ) : (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(0, r), Polynomial.eval z p • resolvent A z = (Polynomial.aeval A) p

Circle Cauchy formula under spectral enclosure: if σ(A) ⊆ ball 0 r, then (2πi)⁻¹ ∮_{|z| = r} p(z) R_A(z) dz = p(A).

theorem circleIntegral_resolvent_eq_two_pi_I_smul_one_of_spectrum_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {r : ℝ} (hr : 0 < r) (hσ : spectrum ℂ A ⊆ Metric.ball 0 r) : circleIntegral (resolvent A) 0 r = (2 * ↑Real.pi * Complex.I) • 1

The un-normalized resolvent identity ∮_{|z| = r} R_A(z) dz = 2πi • 1 under spectral enclosure.

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

Symmetrized Crouzeix–Palencia bound under the numerical-range hypothesis. If the closure of the numerical range lies in the open disk ball 0 r, then for the auxiliary operator G of that disk, ‖p(A) + G†‖ ≤ 2 * sup_{|z| ≤ r} ‖p(z)‖.

General scalar weights and the negative Laurent modes

theorem circleIntegral_smul_resolvent_eq_of_spectrum_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {r R : ℝ} (hr : 0 < r) (hrR : r ≤ R) (hσ : spectrum ℂ A ⊆ Metric.ball c r) {g : ℂ → ℂ} (hg : ∀ z ∉ Metric.ball c r, DifferentiableAt ℂ g z) : ∮ (z : ℂ) in C(c, r), g z • resolvent A z = ∮ (z : ℂ) in C(c, R), g z • resolvent A z

Annulus deformation for a scalar-weighted resolvent kernel g z • R_A z, where g is differentiable off the disk ball c r containing the spectrum.

theorem normalized_circleIntegral_inv_pow_smul_resolvent_eq_zero_of_spectrum_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {r : ℝ} (hr : 0 < r) (hσ : spectrum ℂ A ⊆ Metric.ball 0 r) (n : ℕ) (hn : 0 < n) : (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(0, r), z⁻¹ ^ n • resolvent A z = 0

Under spectral enclosure σ(A) ⊆ ball 0 r, the negative Laurent modes of the resolvent vanish: (2πi)⁻¹ ∮_{|z| = r} z⁻ⁿ • R_A(z) dz = 0 for n ≥ 1.

Arbitrary centers

theorem circleIntegral_eval_smul_resolvent_eq_center {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (c : ℂ) (R : ℝ) (p : Polynomial ℂ) : ∮ (z : ℂ) in C(c, R), Polynomial.eval z p • resolvent A z = ∮ (w : ℂ) in C(0, R), Polynomial.eval w (p.affineComposition 1 c) • resolvent (A - c • 1) w

Translating a resolvent circle integral to the centered circle: the integral of p(z) • R_A(z) over C(c, R) is the integral of p(w + c) • R_{A - c}(w) over C(0, R).

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

The polynomial circle Cauchy formula on C(c, R) for ‖A - c • 1‖ < R.

theorem normalized_circleIntegral_eval_smul_resolvent_eq_aeval_of_spectrum_subset_ball_center {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 ℂ) : (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, r), Polynomial.eval z p • resolvent A z = (Polynomial.aeval A) p

The polynomial circle Cauchy formula on C(c, r) under spectral enclosure σ(A) ⊆ ball c r.

theorem circleIntegral_resolvent_eq_two_pi_I_smul_one_of_spectrum_subset_ball_center {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) : circleIntegral (resolvent A) c r = (2 * ↑Real.pi * Complex.I) • 1

The resolvent mass identity on C(c, r) under spectral enclosure.

theorem norm_aeval_add_star_auxiliary_ball_le_of_closedNumericalRange_subset_ball_center {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 + star (crouzeixPolynomialAuxiliaryOperator A (SmoothJordanDomain.ball c r hr) p)‖ ≤ 2 * polynomialSupNorm p (Metric.closedBall c r)

Symmetrized Crouzeix–Palencia bound for an arbitrary disk containing the numerical range. If closure W(A) ⊆ ball c r, then for the auxiliary operator G of that disk, ‖p(A) + G†‖ ≤ 2 * sup_{|z - c| ≤ r} ‖p(z)‖.