Commit 2020-09-14 15:35 49fc7edd

View on Github →

feat(measure_theory): assorted integration lemmas (#4145) from the sphere eversion project This is still preparations for differentiation of integals depending on a parameter.

Estimated changes

Modified src/measure_theory/bochner_integration.lean

added theorem measure_theory.continuous_integral

added theorem measure_theory.l1.continuous_integral

added theorem measure_theory.l1.integral_eq_integral

added theorem measure_theory.l1.integral_of_fun_eq_integral

added theorem measure_theory.l1.norm_eq_integral_norm

added theorem measure_theory.l1.norm_of_fun_eq_integral_norm

Modified src/measure_theory/borel_space.lean

added theorem continuous_linear_map.measurable

added theorem measurable.clm_apply

added theorem measurable.const_mul

added theorem measurable.mul_const

Modified src/measure_theory/l1_space.lean

added theorem measure_theory.integrable.const_mul

added theorem measure_theory.integrable.mul_const

added theorem measure_theory.l1.integrable_norm

added theorem measure_theory.l1.measurable_norm

Modified src/measure_theory/set_integral.lean

added theorem measure_theory.integral_indicator_const