Commit 2023-06-12 04:10 04fc2f1c

View on Github →

feat: port MeasureTheory.Integral.TorusIntegral (#4942)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/TorusIntegral.lean

added theorem TorusIntegrable.function_integrable

added theorem TorusIntegrable.torusIntegrable_const

added theorem TorusIntegrable.torusIntegrable_zero_radius

added def TorusIntegrable

added theorem norm_torusIntegral_le_of_norm_le_const

added def torusIntegral

added theorem torusIntegral_add

added theorem torusIntegral_const_mul

added theorem torusIntegral_dim0

added theorem torusIntegral_dim1

added theorem torusIntegral_neg

added theorem torusIntegral_radius_zero

added theorem torusIntegral_smul

added theorem torusIntegral_sub

added theorem torusIntegral_succ

added theorem torusIntegral_succAbove

added def torusMap

added theorem torusMap_eq_center_iff

added theorem torusMap_sub_center

added theorem torusMap_zero_radius