Commit 2023-06-02 12:29 0273cb34

View on Github →

feat: port MeasureTheory.Function.StronglyMeasurable.Lp (#4578)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/StronglyMeasurable/Lp.lean

added theorem MeasureTheory.Integrable.aefinStronglyMeasurable

added theorem MeasureTheory.Lp.finStronglyMeasurable

added theorem MeasureTheory.Memℒp.aefinStronglyMeasurable

added theorem MeasureTheory.Memℒp.finStronglyMeasurable_of_stronglyMeasurable