Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-14 14:14 e3eb0eb0

View on Github →

feat(measure_theory/integral/set_to_l1): various properties of the set_to_fun construction (#10713)

Estimated changes

Modified src/measure_theory/function/l1_space.lean

added theorem measure_theory.integrable.of_measure_le_smul

Modified src/measure_theory/function/lp_space.lean

added theorem measure_theory.mem_ℒp.of_measure_le_smul

Modified src/measure_theory/integral/bochner.lean

Modified src/measure_theory/integral/set_to_l1.lean

added theorem measure_theory.L1.set_to_L1_add_left'

added theorem measure_theory.L1.set_to_L1_add_left

added theorem measure_theory.L1.set_to_L1_congr_left'

added theorem measure_theory.L1.set_to_L1_congr_left

added theorem measure_theory.L1.set_to_L1_const

added theorem measure_theory.L1.set_to_L1_simple_func_indicator_const

added theorem measure_theory.L1.set_to_L1_smul_left'

added theorem measure_theory.L1.set_to_L1_smul_left

added theorem measure_theory.L1.set_to_L1_zero_left'

added theorem measure_theory.L1.set_to_L1_zero_left

added theorem measure_theory.L1.simple_func.set_to_L1s_add_left'

added theorem measure_theory.L1.simple_func.set_to_L1s_add_left

added theorem measure_theory.L1.simple_func.set_to_L1s_clm_add_left'

added theorem measure_theory.L1.simple_func.set_to_L1s_clm_add_left

added theorem measure_theory.L1.simple_func.set_to_L1s_clm_congr_left'

added theorem measure_theory.L1.simple_func.set_to_L1s_clm_congr_left

added theorem measure_theory.L1.simple_func.set_to_L1s_clm_congr_measure

added theorem measure_theory.L1.simple_func.set_to_L1s_clm_const

added theorem measure_theory.L1.simple_func.set_to_L1s_clm_smul_left'

added theorem measure_theory.L1.simple_func.set_to_L1s_clm_smul_left

added theorem measure_theory.L1.simple_func.set_to_L1s_clm_zero_left'

added theorem measure_theory.L1.simple_func.set_to_L1s_clm_zero_left

added theorem measure_theory.L1.simple_func.set_to_L1s_congr_left

added theorem measure_theory.L1.simple_func.set_to_L1s_congr_measure

added theorem measure_theory.L1.simple_func.set_to_L1s_const

modified theorem measure_theory.L1.simple_func.set_to_L1s_indicator_const

added theorem measure_theory.L1.simple_func.set_to_L1s_neg

added theorem measure_theory.L1.simple_func.set_to_L1s_smul_left'

added theorem measure_theory.L1.simple_func.set_to_L1s_smul_left

added theorem measure_theory.L1.simple_func.set_to_L1s_sub

added theorem measure_theory.L1.simple_func.set_to_L1s_zero_left'

added theorem measure_theory.L1.simple_func.set_to_L1s_zero_left

added theorem measure_theory.continuous_L1_to_L1

added theorem measure_theory.set_to_fun_add_left'

added theorem measure_theory.set_to_fun_add_left

added theorem measure_theory.set_to_fun_congr_left'

added theorem measure_theory.set_to_fun_congr_left

added theorem measure_theory.set_to_fun_congr_measure

added theorem measure_theory.set_to_fun_congr_measure_of_add_left

added theorem measure_theory.set_to_fun_congr_measure_of_add_right

added theorem measure_theory.set_to_fun_congr_measure_of_integrable

added theorem measure_theory.set_to_fun_congr_smul_measure

added theorem measure_theory.set_to_fun_const

added theorem measure_theory.set_to_fun_finset_sum'

added theorem measure_theory.set_to_fun_finset_sum

added theorem measure_theory.set_to_fun_measure_zero'

added theorem measure_theory.set_to_fun_measure_zero

added theorem measure_theory.set_to_fun_smul_left'

added theorem measure_theory.set_to_fun_smul_left

added theorem measure_theory.set_to_fun_top_smul_measure

added theorem measure_theory.set_to_fun_zero_left'

added theorem measure_theory.set_to_fun_zero_left

added theorem measure_theory.simple_func.norm_set_to_simple_func_le_sum_mul_norm

added theorem measure_theory.simple_func.set_to_simple_func_congr_left

added theorem measure_theory.simple_func.set_to_simple_func_const'

added theorem measure_theory.simple_func.set_to_simple_func_const

added theorem measure_theory.simple_func.set_to_simple_func_smul_left'

added theorem measure_theory.simple_func.set_to_simple_func_smul_left

added theorem measure_theory.simple_func.set_to_simple_func_zero'

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.measure.absolutely_continuous_of_le_smul