Commit 2021-03-28 12:00 0e4760b3

refactor(measure_theory): add typeclasses for measurability of operations (#6832) With these typeclasses and lemmas we can use, e.g., measurable.mul for any type with measurable uncurry (*), not only those with has_continuous_mul. New typeclasses:

• has_measurable_add, has_measurable_add₂: measurable left/right addition and measurable uncurry (+);
• has_measurable_mul, has_measurable_mul₂: measurable left/right multiplication and measurable uncurry (*);
• has_measurable_pow: measurable uncurry (^)
• has_measurable_sub, has_measurable_sub₂: measurable left/right subtraction and measurable λ (a, b), a - b
• has_measurable_div, has_measurable_div₂ : measurability of division as a function of numerator/denominator and measurability of λ (a, b), a / b;
• has_measurable_neg, has_measurable_inv: measurable negation/inverse;
• has_measurable_const_smul, has_measurable_smul: measurable λ x, c • x and measurable λ (c, x), c • x