Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-11 20:13 19beb127

View on Github →

feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C (#8210)

Estimated changes

Modified src/analysis/calculus/parametric_integral.lean

Modified src/measure_theory/lp_space.lean

modified theorem continuous_linear_map.coe_fn_comp_Lp

modified def continuous_linear_map.comp_Lp

modified def continuous_linear_map.comp_LpL

modified def continuous_linear_map.comp_Lpₗ

modified theorem continuous_linear_map.norm_compLpL_le

modified theorem continuous_linear_map.norm_comp_Lp_le

Modified src/measure_theory/set_integral.lean

modified theorem continuous_linear_map.continuous_integral_comp_L1

modified theorem continuous_linear_map.integral_comp_L1_comm

modified theorem continuous_linear_map.integral_comp_Lp

modified theorem continuous_linear_map.integral_comp_comm'

modified theorem continuous_linear_map.integral_comp_comm

modified theorem integral_conj

added theorem integral_im

modified theorem integral_of_real

added theorem integral_re

modified theorem linear_isometry.integral_comp_comm