Commit 2023-10-19 11:09 36114b7a

View on Github →

feat: some lemmas about nnnorm and integration / L1-norm (#7753)

From the Sobolev project

Estimated changes

Modified Mathlib/MeasureTheory/Function/L1Space.lean

added theorem MeasureTheory.Integrable.nnnorm_toL1

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

added theorem MeasureTheory.L1.nnnorm_Integral_le_one

added theorem MeasureTheory.L1.nnnorm_integral_le

modified theorem MeasureTheory.L1.norm_Integral_le_one