Commit 2023-07-24 16:15 c652e603

View on Github →

feat: Integrability of g • f for g continuous with compact support and f locally integrable (#6100)

Estimated changes

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

added theorem MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport

added theorem MeasureTheory.LocallyIntegrable.integrable_smul_right_of_hasCompactSupport

Modified Mathlib/MeasureTheory/Function/LpSeminorm.lean

added theorem Continuous.memℒp_top_of_hasCompactSupport

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

added theorem Continuous.stronglyMeasurable_of_hasCompactSupport

Modified Mathlib/Topology/Support.lean

added theorem HasCompactMulSupport.of_mulSupport_subset_isCompact