Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-22 06:47 76212e65

View on Github →

feat(measure_theory/integral/set_integral): integral of a is_R_or_C function equals integral of real part + integral of imaginary part (#9735)

Estimated changes

Modified src/data/complex/is_R_or_C.lean

added theorem is_R_or_C.norm_of_real

Modified src/measure_theory/function/conditional_expectation.lean

Modified src/measure_theory/function/l1_space.lean

added theorem measure_theory.integrable.of_real

added theorem measure_theory.integrable.re_im_iff

Modified src/measure_theory/function/lp_space.lean

added theorem continuous_linear_map.comp_mem_ℒp'

added theorem continuous_linear_map.comp_mem_ℒp

added theorem lipschitz_with.comp_mem_ℒp

added theorem measure_theory.mem_ℒp.of_comp_antilipschitz_with

added theorem measure_theory.mem_ℒp.of_real

added theorem measure_theory.mem_ℒp_re_im_iff

Modified src/measure_theory/function/special_functions.lean

added theorem ae_measurable_of_re_im

added theorem is_R_or_C.measurable_of_real

added theorem measurable_of_re_im

Modified src/measure_theory/integral/set_integral.lean

added theorem integral_coe_re_add_coe_im

added theorem integral_re_add_im

added theorem set_integral_re_add_im

Modified test/measurability.lean