Adjoint of operator-valued integrals

The symmetrized Crouzeix--Palencia contour operator contains the adjoint of an operator-valued integral. Since adjoint is conjugate-linear, moving it through integration is not an instance of the usual complex-linear integral API. This file supplies that bridge using Mathlib's semilinear integration theorem and records the resulting contour formula.

Main declarations

• ContinuousLinearMap.adjoint_integral -- adjoint commutes with an integrable Bochner integral.
• ContinuousLinearMap.adjoint_intervalIntegral -- the corresponding interval-integral statement.
• ContinuousLinearMap.adjoint_contourIntegral -- the adjoint of a contour integral has conjugated tangent weight and pointwise-adjoint integrand.
• ContinuousLinearMap.intervalIntegral_smul_add_adjoint -- complex-weighted symmetrization of an operator kernel and its adjoint.

theorem ContinuousLinearMap.adjoint_integral {X : Type u} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (f : X → E →L[ℂ] F) (hf : MeasureTheory.Integrable f μ) : adjoint (∫ (x : X), f x ∂μ) = ∫ (x : X), adjoint (f x) ∂μ

Adjoint commutes with an integrable operator-valued Bochner integral. The proof uses adjoint as a continuous conjugate-linear map and the fact that complex conjugation fixes real scalars.

theorem ContinuousLinearMap.adjoint_intervalIntegral {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (f : ℝ → E →L[ℂ] F) {a b : ℝ} {ν : MeasureTheory.Measure ℝ} (hf : IntervalIntegrable f ν a b) : adjoint (∫ (x : ℝ) in a..b, f x ∂ν) = ∫ (x : ℝ) in a..b, adjoint (f x) ∂ν

Adjoint commutes with an operator-valued interval integral whenever the integrand is interval integrable.

theorem ContinuousLinearMap.adjoint_contourIntegral {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F] (f : ℂ → E →L[ℂ] F) (γ : ℝ → ℂ) (hf : ContourIntegrable f γ) : adjoint (contourIntegral f γ) = ∫ (t : ℝ) in 0..2 * Real.pi, star (deriv γ t) • adjoint (f (γ t))

Moving adjoint through a contour integral conjugates the tangent scalar and takes the pointwise adjoint of the operator-valued integrand.

theorem ContinuousLinearMap.intervalIntegral_smul_add_adjoint {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (K : ℝ → E →L[ℂ] E) (f : ℝ → ℂ) {a b : ℝ} {ν : MeasureTheory.Measure ℝ} (hfK : IntervalIntegrable (fun (t : ℝ) => f t • K t) ν a b) (hstarfK : IntervalIntegrable (fun (t : ℝ) => star (f t) • K t) ν a b) : ∫ (t : ℝ) in a..b, f t • K t ∂ν + adjoint (∫ (t : ℝ) in a..b, star (f t) • K t ∂ν) = ∫ (t : ℝ) in a..b, f t • (K t + adjoint (K t)) ∂ν

Complex-weighted symmetrization of an operator-valued interval integral. The conjugate weight before taking adjoint becomes the original weight, so the two terms combine into the symmetric kernel K t + (K t)†.