Double-layer positivity of the resolvent kernel (L4.2d)

The symmetrized Crouzeix--Palencia bound ‖p(A) + G⋆‖ ≤ 2 m rests on one positivity fact: along a positively oriented boundary curve γ of a convex domain containing W(A), the operator kernel of p(A) + G⋆ is (2π)⁻¹ p(γ t) • (ν R_A(γ t) + (ν R_A(γ t))⋆) with ν = -i γ'(t) an outward normal, and the symmetric part ν R_A(σ) + (ν R_A(σ))⋆ is a positive operator. This file proves that positivity pointwise, in its natural generality: the only input is that W(A) lies in the closed half-plane cut out at σ by the direction ν.

Route: for y = R_A(σ) x one has x = σ • y - A y, hence ⟪x, ν • R_A(σ) x⟫ = ν · conj (σ‖y‖² - ⟪y, A y⟫), whose real part is ‖y‖² · re (conj ν · (σ - a)) with a = ⟪y, A y⟫ / ‖y‖² ∈ W(A).

Main declarations

• re_inner_smul_resolvent_nonneg -- the pointwise positivity at a supporting point.
• re_inner_add_adjoint_smul_resolvent_nonneg -- positivity of the self-adjoint double-layer kernel.
• isPositive_add_adjoint_smul_resolvent -- the corresponding operator-order positivity statement.
• re_inner_smul_resolvent_circleMap_nonneg -- its instance on a circle enclosing W(A), with ν = -I * deriv (circleMap c R) t, the kernel direction produced by contourIntegral.
• re_inner_add_adjoint_smul_resolvent_circleMap_nonneg -- positivity of the symmetric circle kernel.
• isPositive_add_adjoint_smul_resolvent_circleMap -- the circle kernel in positive-operator form.

theorem eq_smul_resolvent_apply_sub_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {σ : ℂ} (hσ : σ ∈ resolventSet ℂ A) (x : E) : x = σ • (resolvent A σ) x - A ((resolvent A σ) x)

x = σ • y - A y for y = R_A(σ) x and σ in the resolvent set.

theorem re_inner_smul_resolvent_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {σ ν : ℂ} (hW : ∀ w ∈ numericalRange A, ((starRingEnd ℂ) ν * (w - σ)).re ≤ 0) (x : E) : 0 ≤ (inner ℂ x ((ν • resolvent A σ) x)).re

Double-layer positivity at a supporting point. If the numerical range of A lies in the closed half-plane {w | re (conj ν * (w - σ)) ≤ 0} -- for instance σ a boundary point of a convex domain containing W(A) and ν an outward normal there -- then the quadratic form of ν • R_A(σ) has nonnegative real part. No resolvent-set hypothesis is needed: off the resolvent set Mathlib's resolvent is 0 and the form vanishes.

theorem re_inner_add_adjoint_smul_resolvent_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {σ ν : ℂ} (hW : ∀ w ∈ numericalRange A, ((starRingEnd ℂ) ν * (w - σ)).re ≤ 0) (x : E) : 0 ≤ (inner ℂ x ((ν • resolvent A σ + ContinuousLinearMap.adjoint (ν • resolvent A σ)) x)).re

The self-adjoint double-layer kernel nu • R_A(sigma) + (nu • R_A(sigma))† has nonnegative quadratic form at a supporting point.

theorem isPositive_add_adjoint_smul_resolvent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {σ ν : ℂ} (hW : ∀ w ∈ numericalRange A, ((starRingEnd ℂ) ν * (w - σ)).re ≤ 0) : (ν • resolvent A σ + ContinuousLinearMap.adjoint (ν • resolvent A σ)).IsPositive

The symmetric double-layer kernel is a positive continuous linear map at every supporting point.

theorem re_inner_smul_resolvent_circleMap_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hW : numericalRange A ⊆ Metric.closedBall c R) (t : ℝ) (x : E) : 0 ≤ (inner ℂ x (((-Complex.I * deriv (circleMap c R) t) • resolvent A (circleMap c R t)) x)).re

The circle instance: on the positively oriented circle circleMap c R the contour kernel direction is ν = -I * deriv (circleMap c R) t = R • exp (t I), an outward normal, so the quadratic form of ν • R_A(circleMap c R t) has nonnegative real part whenever W(A) lies in the closed disk.

theorem re_inner_add_adjoint_smul_resolvent_circleMap_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hW : numericalRange A ⊆ Metric.closedBall c R) (t : ℝ) (x : E) : 0 ≤ (inner ℂ x (((-Complex.I * deriv (circleMap c R) t) • resolvent A (circleMap c R t) + ContinuousLinearMap.adjoint ((-Complex.I * deriv (circleMap c R) t) • resolvent A (circleMap c R t))) x)).re

The symmetric double-layer kernel is positive along every enclosing circle, with the outward normal induced by the positive circle orientation.

theorem isPositive_add_adjoint_smul_resolvent_circleMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hW : numericalRange A ⊆ Metric.closedBall c R) (t : ℝ) : ((-Complex.I * deriv (circleMap c R) t) • resolvent A (circleMap c R t) + ContinuousLinearMap.adjoint ((-Complex.I * deriv (circleMap c R) t) • resolvent A (circleMap c R t))).IsPositive

The symmetric double-layer kernel along an enclosing circle is a positive continuous linear map.