Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-18 15:50 0d09e993

View on Github →

feat(measure_theory/integral/{set_to_l1,bochner}): generalize results about integrals to set_to_fun (#10369) The Bochner integral is a particular case of the set_to_fun construction. We generalize some lemmas which were proved for integrals to set_to_fun, notably the Lebesgue dominated convergence theorem.

Estimated changes

Modified src/measure_theory/integral/bochner.lean

Modified src/measure_theory/integral/set_to_l1.lean

added theorem measure_theory.L1.norm_set_to_L1_le'

added theorem measure_theory.L1.norm_set_to_L1_le

added theorem measure_theory.L1.norm_set_to_L1_le_mul_norm'

added theorem measure_theory.L1.norm_set_to_L1_le_mul_norm

added theorem measure_theory.L1.norm_set_to_L1_le_norm_set_to_L1s_clm

modified theorem measure_theory.L1.set_to_L1_eq_set_to_L1s_clm

added theorem measure_theory.L1.set_to_L1_lipschitz

added theorem measure_theory.L1.simple_func.norm_set_to_L1s_clm_le'

added theorem measure_theory.L1.simple_func.norm_set_to_L1s_clm_le

added theorem measure_theory.L1.tendsto_set_to_L1

added theorem measure_theory.continuous_at_set_to_fun_of_dominated

added theorem measure_theory.continuous_set_to_fun

added theorem measure_theory.continuous_set_to_fun_of_dominated

added theorem measure_theory.norm_set_to_fun_le'

added theorem measure_theory.norm_set_to_fun_le

added theorem measure_theory.norm_set_to_fun_le_mul_norm'

added theorem measure_theory.norm_set_to_fun_le_mul_norm

added theorem measure_theory.set_to_fun_to_L1

added theorem measure_theory.tendsto_set_to_fun_filter_of_dominated_convergence

added theorem measure_theory.tendsto_set_to_fun_of_dominated_convergence