The double-layer circle kernel: continuity and integrability (L4.2d support)

For an operator A whose numerical range closure lies in the open disk ball c R, the circle sphere c R lies in the resolvent set (by spectrum_subset_closure_numericalRange), so the double-layer circle kernel B t = (-i γ'(t)) • R_A(γ(t)), γ = circleMap c R, is continuous in t. This file records that continuity and the interval integrability over [0, 2π] of B, of the symmetrized kernel B + B†, and of its polynomial weighting p(γ(t)) • (B t + (B t)†) — the side conditions consumed by the positive-kernel contractivity bound (PositiveKernelBound.lean, DoubleLayerBound.lean).

Main declarations

• sphere_subset_resolventSet_of_closure_numericalRange_subset_ball
• continuous_resolvent_circleMap, continuous_circleKernel, continuous_circleKernel_add_adjoint
• intervalIntegrable_circleKernel, intervalIntegrable_circleKernel_add_adjoint, intervalIntegrable_eval_smul_circleKernel_add_adjoint

Requires [CompleteSpace E] (spectrum, adjoints).

theorem sphere_subset_resolventSet_of_closure_numericalRange_subset_ball {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hW : closure (numericalRange A) ⊆ Metric.ball c R) : Metric.sphere c R ⊆ resolventSet ℂ A

If the closure of the numerical range lies in the open disk ball c R, the circle sphere c R lies in the resolvent set.

theorem continuous_resolvent_circleMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hρ : Metric.sphere c R ⊆ resolventSet ℂ A) (hR : 0 ≤ R) : Continuous fun (t : ℝ) => resolvent A (circleMap c R t)

The resolvent is continuous along a circle contained in the resolvent set.

theorem continuous_circleKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hρ : Metric.sphere c R ⊆ resolventSet ℂ A) (hR : 0 ≤ R) : Continuous fun (t : ℝ) => (-Complex.I * deriv (circleMap c R) t) • resolvent A (circleMap c R t)

The double-layer circle kernel B t = (-i γ'(t)) • R_A(γ(t)), γ = circleMap c R, is continuous when the circle lies in the resolvent set.

theorem continuous_circleKernel_add_adjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hρ : Metric.sphere c R ⊆ resolventSet ℂ A) (hR : 0 ≤ R) : Continuous fun (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))

The symmetrized circle kernel B t + (B t)† is continuous.

theorem intervalIntegrable_circleKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hρ : Metric.sphere c R ⊆ resolventSet ℂ A) (hR : 0 ≤ R) : IntervalIntegrable (fun (t : ℝ) => (-Complex.I * deriv (circleMap c R) t) • resolvent A (circleMap c R t)) MeasureTheory.volume 0 (2 * Real.pi)

The circle kernel is interval integrable over [0, 2π].

theorem intervalIntegrable_circleKernel_add_adjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hρ : Metric.sphere c R ⊆ resolventSet ℂ A) (hR : 0 ≤ R) : IntervalIntegrable (fun (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))) MeasureTheory.volume 0 (2 * Real.pi)

The symmetrized circle kernel is interval integrable over [0, 2π].

theorem intervalIntegrable_eval_smul_circleKernel_add_adjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) {c : ℂ} {R : ℝ} (hρ : Metric.sphere c R ⊆ resolventSet ℂ A) (hR : 0 ≤ R) (p : Polynomial ℂ) : IntervalIntegrable (fun (t : ℝ) => Polynomial.eval (circleMap c R t) p • ((-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)))) MeasureTheory.volume 0 (2 * Real.pi)

The polynomially weighted symmetrized circle kernel is interval integrable over [0, 2π].