Normalization of the integrated double-layer kernel

The positive-kernel route to the symmetrized Crouzeix--Palencia estimate needs two independent inputs: pointwise positivity of the double-layer kernel, and its total mass. This file supplies the algebraic second input.

First, integration commutes with symmetrization B ↦ B + B†. Consequently, if a parametrized resolvent satisfies the Cauchy identity

integral (gamma' • R_A(gamma)) = 2 * pi * i • 1,

then its outward-normal kernel (-i * gamma') • R_A(gamma) has integral 2 * pi • 1, and the double-layer kernel obtained by adding the pointwise adjoint has integral 4 * pi • 1.

The resolvent Cauchy identity remains an explicit hypothesis here. It is the analytic input supplied separately by a circle or contour Cauchy theorem; no such boundary-value assertion is hidden in the normalization argument.

Main declarations

• ContinuousLinearMap.intervalIntegral_add_adjoint -- interval integration commutes with pointwise symmetrization.
• intervalIntegral_resolvent_doubleLayer_eq_four_pi_smul_one_of_cauchy -- the double-layer kernel has total mass 4 * pi • 1 whenever the underlying resolvent contour has Cauchy integral 2 * pi * i • 1.

theorem ContinuousLinearMap.intervalIntegral_add_adjoint {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {f : ℝ → E →L[ℂ] E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) : ∫ (t : ℝ) in a..b, f t + adjoint (f t) = (∫ (t : ℝ) in a..b, f t) + adjoint (∫ (t : ℝ) in a..b, f t)

Interval integration commutes with symmetrization of an operator-valued integrand.

theorem intervalIntegral_resolvent_doubleLayer_eq_four_pi_smul_one_of_cauchy {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (gamma : ℝ → ℂ) (hint : IntervalIntegrable (fun (t : ℝ) => deriv gamma t • resolvent A (gamma t)) MeasureTheory.volume 0 (2 * Real.pi)) (hCauchy : ∫ (t : ℝ) in 0..2 * Real.pi, deriv gamma t • resolvent A (gamma t) = (2 * ↑Real.pi * Complex.I) • 1) : ∫ (t : ℝ) in 0..2 * Real.pi, (-Complex.I * deriv gamma t) • resolvent A (gamma t) + ContinuousLinearMap.adjoint ((-Complex.I * deriv gamma t) • resolvent A (gamma t)) = (4 * Real.pi) • 1

If the parametrized resolvent has its expected Cauchy integral 2 * pi * i • 1, then the associated outward-normal double-layer kernel has total mass 4 * pi • 1.