Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-10 23:56 886b15b5

View on Github →

doc(measure_theory/l1_space): add doc and some lemmas (#1657)

Add doc and lemmas
Remove unnecessary assumption
Fix integrable_neg
Remove extra assumptions
Wrong variable used

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem nnnorm_norm

Modified src/measure_theory/integration.lean

added theorem measure_theory.lintegral_const_mul'

added theorem measure_theory.lintegral_const_mul_le

Modified src/measure_theory/l1_space.lean

modified def measure_theory.ae_eq_fun.integrable

modified theorem measure_theory.ae_eq_fun.integrable_add

modified theorem measure_theory.ae_eq_fun.integrable_mk

modified theorem measure_theory.ae_eq_fun.integrable_neg

modified theorem measure_theory.ae_eq_fun.integrable_smul

added theorem measure_theory.ae_eq_fun.integrable_sub

added theorem measure_theory.ae_eq_fun.integrable_to_fun

modified theorem measure_theory.ae_eq_fun.integrable_zero

modified def measure_theory.integrable

modified theorem measure_theory.integrable_add

added theorem measure_theory.integrable_iff_lintegral_edist

added theorem measure_theory.integrable_iff_of_ae_eq

modified theorem measure_theory.integrable_neg

added theorem measure_theory.integrable_norm

added theorem measure_theory.integrable_of_ae_eq

modified theorem measure_theory.integrable_smul

added theorem measure_theory.integrable_sub

modified theorem measure_theory.integrable_zero

modified theorem measure_theory.l1.add_def

added theorem measure_theory.l1.add_to_fun

added theorem measure_theory.l1.all_ae_mk_to_fun

modified theorem measure_theory.l1.dist_def

added theorem measure_theory.l1.dist_to_fun

added theorem measure_theory.l1.ext_iff

added theorem measure_theory.l1.lintegral_edist_to_fun_lt_top

modified def measure_theory.l1.mk

added theorem measure_theory.l1.mk_add

added theorem measure_theory.l1.mk_eq_mk

added theorem measure_theory.l1.mk_zero

added theorem measure_theory.l1.neg_mk

added theorem measure_theory.l1.neg_to_fun

modified theorem measure_theory.l1.norm_def

added theorem measure_theory.l1.norm_mk

added theorem measure_theory.l1.norm_to_fun

added theorem measure_theory.l1.self_eq_mk

modified theorem measure_theory.l1.smul_def

added theorem measure_theory.l1.smul_mk

added theorem measure_theory.l1.smul_to_fun

added theorem measure_theory.l1.sub_to_fun

modified theorem measure_theory.l1.zero_def

added theorem measure_theory.l1.zero_to_fun

modified def measure_theory.l1

added theorem measure_theory.lintegral_edist_lt_top

added theorem measure_theory.lintegral_edist_triangle

modified theorem measure_theory.lintegral_nnnorm_add

added theorem measure_theory.lintegral_nnnorm_eq_lintegral_edist

modified theorem measure_theory.lintegral_nnnorm_neg

modified theorem measure_theory.lintegral_nnnorm_zero

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.all_ae_eq_refl

added theorem measure_theory.all_ae_eq_symm

added theorem measure_theory.all_ae_eq_trans