Commit 2025-04-23 07:13 4b8d884b

View on Github →

feat: generalize order properties of the Bochner integral to real ordered Banach spaces (#24177) Currently, Mathlib only has order properties of the Bochner integral for ℝ-valued functions. This generalizes the fundamental results to real ordered Banach spaces. The motivation is to allow for:

variable {A : Type*} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
example {f : ℝ → A} (hf : 0 ≤ᵐ[volume] f) : 0 ≤ ∫ x, f x ∂(volume) :=
  integral_nonneg_of_ae hf

Estimated changes

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

modified theorem MeasureTheory.condExpInd_nonneg

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

Modified Mathlib/MeasureTheory/Function/LpOrder.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

modified theorem MeasureTheory.Lp.simpleFunc.coeFn_le

Modified Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

modified theorem MeasureTheory.integral_mono

modified theorem MeasureTheory.integral_mono_ae

modified theorem MeasureTheory.integral_mono_measure

modified theorem MeasureTheory.integral_mono_of_nonneg

modified theorem MeasureTheory.integral_nonneg

modified theorem MeasureTheory.integral_nonneg_of_ae

modified theorem MeasureTheory.integral_nonpos

modified theorem MeasureTheory.integral_nonpos_of_ae

Modified Mathlib/MeasureTheory/Integral/Bochner/L1.lean

modified theorem MeasureTheory.weightedSMul_nonneg

Modified Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean