Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-02 19:32 2b0aeda1

View on Github →

feat(measure/function/l*_space): a sample of useful lemmas on L^p spaces (#13823) Used in #13690

Estimated changes

Modified src/measure_theory/function/l1_space.lean

added theorem measure_theory.integrable.abs

added theorem measure_theory.integrable.const_mul'

deleted theorem measure_theory.integrable.max_zero

deleted theorem measure_theory.integrable.min_zero

added theorem measure_theory.integrable.mul_const'

added theorem measure_theory.integrable.neg_part

added theorem measure_theory.integrable.pos_part

added theorem measure_theory.integrable_finset_sum'

added theorem measure_theory.mem_ℒp.integrable_norm_rpow'

added theorem measure_theory.mem_ℒp.integrable_norm_rpow

Modified src/measure_theory/function/l2_space.lean

added theorem measure_theory.mem_ℒp.integrable_sq

added theorem measure_theory.mem_ℒp_two_iff_integrable_sq

added theorem measure_theory.mem_ℒp_two_iff_integrable_sq_norm

Modified src/measure_theory/function/lp_space.lean

added theorem measure_theory.mem_ℒp.neg_part

added theorem measure_theory.mem_ℒp.norm_rpow_div

added theorem measure_theory.mem_ℒp.pos_part

modified def measure_theory.mem_ℒp

added theorem measure_theory.mem_ℒp_finset_sum'

added theorem measure_theory.mem_ℒp_norm_rpow_iff

added theorem measure_theory.mem_ℒp_top_const

Modified src/measure_theory/integral/bochner.lean

added theorem measure_theory.mem_ℒp.snorm_eq_integral_rpow_norm

Modified src/measure_theory/measure/ae_measurable.lean

added theorem ae_measurable.map_map_of_ae_measurable

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.is_probability_measure_map

Modified src/probability/integration.lean