Positivity of operator-valued Bochner integrals

The double-layer argument produces a positive continuous-linear-map kernel pointwise along a contour. This file supplies the measure-theoretic bridge: an integrable operator-valued function which is positive almost everywhere has a positive Bochner integral.

Main declarations

• ContinuousLinearMap.isPositive_integral -- positivity passes through a Bochner integral over a positive measure.
• ContinuousLinearMap.isPositive_intervalIntegral -- the oriented-interval specialization used by contour parametrizations.
• ContinuousLinearMap.integral_mono_ae -- almost-everywhere Loewner order passes to Bochner integrals.
• ContinuousLinearMap.intervalIntegral_mono_ae -- the corresponding result on positively oriented intervals.

theorem ContinuousLinearMap.isPositive_integral {X : Type u} {E : Type v} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (f : X → E →L[ℂ] E) (hf : MeasureTheory.Integrable f μ) (hpos : ∀ᵐ (x : X) ∂μ, (f x).IsPositive) : (∫ (x : X), f x ∂μ).IsPositive

The Bochner integral of an integrable family of positive continuous linear maps is positive when the family is positive almost everywhere.

theorem ContinuousLinearMap.isPositive_intervalIntegral {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (f : ℝ → E →L[ℂ] E) {a b : ℝ} (hab : a ≤ b) (hf : IntervalIntegrable f MeasureTheory.volume a b) (hpos : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc a b), (f x).IsPositive) : (∫ (x : ℝ) in a..b, f x).IsPositive

A positively oriented interval integral of positive operators is positive.

theorem ContinuousLinearMap.integral_mono_ae {X : Type u} {E : Type v} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (f g : X → E →L[ℂ] E) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hfg : f ≤ᵐ[μ] g) : ∫ (x : X), f x ∂μ ≤ ∫ (x : X), g x ∂μ

Bochner integration is monotone for the Loewner order on continuous linear maps.

theorem ContinuousLinearMap.intervalIntegral_mono_ae {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (f g : ℝ → E →L[ℂ] E) {a b : ℝ} (hab : a ≤ b) (hf : IntervalIntegrable f MeasureTheory.volume a b) (hg : IntervalIntegrable g MeasureTheory.volume a b) (hfg : f ≤ᵐ[MeasureTheory.volume.restrict (Set.Ioc a b)] g) : ∫ (x : ℝ) in a..b, f x ≤ ∫ (x : ℝ) in a..b, g x

Positively oriented interval integration is monotone for the Loewner order on continuous linear maps.