Commit 2026-05-26 05:08 01a171fa

View on Github →

feat: if an L^p space is complete, so is its target space unless the measure is zero (#39614)

Estimated changes

Modified Mathlib.lean

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

added def ContinuousLinearMap.compLpL₂

added theorem ContinuousLinearMap.compLpL₂_apply_apply

modified def ContinuousLinearMap.compLpₗ

added def ContinuousLinearMap.compLpₗ₂

added theorem ContinuousLinearMap.norm_compLpL₂_le

Created Mathlib/MeasureTheory/Function/LpSpace/CompleteOfCompleteLp.lean

added theorem MeasureTheory.AEFinStronglyMeasurable.exists_measurableSet_measure_pos_lt_top

added theorem MeasureTheory.FinStronglyMeasurable.exists_measurableSet_measure_pos_lt_top

added theorem MeasureTheory.completeSpace_of_completeSpace_Lp

added theorem MeasureTheory.nontrivial_Lp_real_of_nontrivial_Lp