MeasureTheory.Memℒp.sup

theorem MeasureTheory.Memℒp.sup : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal} [inst : NormedLatticeAddCommGroup E] {f g : α → E}, MeasureTheory.Memℒp f p μ → MeasureTheory.Memℒp g p μ → MeasureTheory.Memℒp (f ⊔ g) p μ

The theorem `MeasureTheory.Memℒp.sup` states that for any nonnegative extended real number `p`, any measurable space `α`, any `E` that forms a normed lattice addition commutative group, any measure `μ` on the measurable space `α`, and any two functions `f` and `g` from `α` to `E`, if both `f` and `g` satisfy the property `Memℒp`, then the function which at each point takes the supremum (or maximum) of `f` and `g` also satisfies the property `Memℒp`. In mathematical terms, `f` and `g` being in `L^p` space (denoted by `Memℒp`) means that they are almost everywhere strongly measurable and their p-th power integrals are finite (if `p < ∞`), or their essential supremum is finite (if `p = ∞`). The theorem then states that the pointwise supremum of two functions in `L^p` space is also in `L^p` space.

More concisely: If `f` and `g` are measurable functions from a measurable space to a normed lattice addition commutative group with finite p-th power integrals (or essential supremum for p = ∞), then the pointwise supremum of `f` and `g` also has finite p-th power integrals (or essential supremum for p = ∞).