Lᵖ is an ordered module

Mathlib orders Lᵖ almost everywhere (MeasureTheory.Lp.coeFn_le). If scalar multiplication on the values is monotone, then so is scalar multiplication on Lᵖ classes, since it is computed almost everywhere pointwise. In particular real Lᵖ is an ordered real module, which is the hypothesis under which Mathlib's Bochner integral of almost everywhere nonnegative functions is nonnegative (MeasureTheory.integral_nonneg_of_ae), now applicable to Lᵖ-valued functions.

instance MeasureTheory.Lp.instPosSMulMonoSubtypeAEEqFunMemAddSubgroup_tauCeti {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedRing 𝕜] [PartialOrder 𝕜] [NormedAddCommGroup E] [PartialOrder E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [PosSMulMono 𝕜 E] : PosSMulMono 𝕜 ↥(Lp E p μ)

Multiplying an Lᵖ class by a nonnegative scalar is monotone if it is so on the values.

instance MeasureTheory.Lp.instSMulPosMonoSubtypeAEEqFunMemAddSubgroup_tauCeti {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedRing 𝕜] [PartialOrder 𝕜] [NormedAddCommGroup E] [PartialOrder E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [SMulPosMono 𝕜 E] : SMulPosMono 𝕜 ↥(Lp E p μ)

Multiplying a nonnegative Lᵖ class by scalars is monotone if it is so on the values.

instance MeasureTheory.Lp.instIsOrderedModuleSubtypeAEEqFunMemAddSubgroup_tauCeti {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {m : MeasurableSpace α} {μ : Measure α} {p : ENNReal} [NormedRing 𝕜] [PartialOrder 𝕜] [NormedAddCommGroup E] [PartialOrder E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] [IsOrderedModule 𝕜 E] : IsOrderedModule 𝕜 ↥(Lp E p μ)

Lᵖ with values in an ordered module is an ordered module, ordered almost everywhere.