Commit 2025-05-13 12:03 c46bd00f

View on Github →

feat(LpSeminorm/TriangleInequality): generalise to enorms (#24839) Almost all lemmas generalise with almost no modifications; a few lemmas involving subtraction need to stay within normed spaces (for now). The first two proofs simplify, as we can avoid additional coercions from NNReal.

Estimated changes

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

Modified Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean

modified theorem MeasureTheory.MemLp.add

modified theorem MeasureTheory.eLpNorm'_sum_le

modified theorem MeasureTheory.eLpNormEssSup_add_le

modified theorem MeasureTheory.eLpNorm_add_le

modified theorem MeasureTheory.eLpNorm_add_lt_top

modified theorem MeasureTheory.eLpNorm_sub_le'

modified theorem MeasureTheory.eLpNorm_sum_le

modified theorem MeasureTheory.memLp_finset_sum'

modified theorem MeasureTheory.memLp_finset_sum

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

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean