Commit 2025-06-21 12:16 e2f8bf7b

View on Github →

feat: specific lemmas about integrability of ContinuousMap[Zero]-valued functions (#26058)

<!-- The text above the `

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/SpecificCodomains/ContinuousMap.lean

added theorem ContinuousMap.aeStronglyMeasurable_mkD_of_uncurry

added theorem ContinuousMap.aeStronglyMeasurable_mkD_restrict_of_uncurry

added theorem ContinuousMap.aeStronglyMeasurable_restrict_mkD_of_uncurry

added theorem ContinuousMap.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry

added theorem ContinuousMap.hasFiniteIntegral_mkD_of_bound

added theorem ContinuousMap.hasFiniteIntegral_mkD_restrict_of_bound

added theorem ContinuousMap.hasFiniteIntegral_of_bound

Created Mathlib/MeasureTheory/SpecificCodomains/ContinuousMapZero.lean

added theorem ContinuousMapZero.aeStronglyMeasurable_mkD_of_uncurry

added theorem ContinuousMapZero.aeStronglyMeasurable_mkD_restrict_of_uncurry

added theorem ContinuousMapZero.aeStronglyMeasurable_restrict_mkD_of_uncurry

added theorem ContinuousMapZero.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry

added theorem ContinuousMapZero.hasFiniteIntegral_mkD_of_bound

added theorem ContinuousMapZero.hasFiniteIntegral_mkD_restrict_of_bound

added theorem ContinuousMapZero.hasFiniteIntegral_of_bound