Commit 2021-07-20 08:59 f5d25b48

View on Github →

feat(measure_theory/vector_measure): introduce vector-valued measures (#8247) This PR introduces vector-valued measures and provides a method of creating signed measures without the summability requirement.

Estimated changes

Modified src/analysis/normed_space/basic.lean

added theorem real.norm_of_nonpos

Modified src/data/real/ennreal.lean

added theorem ennreal.coe_smul

added theorem ennreal.to_real_smul

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.summable_measure_to_real

Created src/measure_theory/vector_measure.lean

added def measure_theory.complex_measure

added def measure_theory.measure.sub_to_signed_measure

added theorem measure_theory.measure.sub_to_signed_measure_apply

added def measure_theory.measure.to_ennreal_vector_measure

added theorem measure_theory.measure.to_ennreal_vector_measure_add

added theorem measure_theory.measure.to_ennreal_vector_measure_apply_measurable

added theorem measure_theory.measure.to_ennreal_vector_measure_zero

added def measure_theory.measure.to_signed_measure

added theorem measure_theory.measure.to_signed_measure_add

added theorem measure_theory.measure.to_signed_measure_apply_measurable

added theorem measure_theory.measure.to_signed_measure_smul

added theorem measure_theory.measure.to_signed_measure_zero

added def measure_theory.signed_measure

added def measure_theory.vector_measure.add

added theorem measure_theory.vector_measure.add_apply

added theorem measure_theory.vector_measure.coe_add

added def measure_theory.vector_measure.coe_fn_add_monoid_hom

added theorem measure_theory.vector_measure.coe_injective

added theorem measure_theory.vector_measure.coe_neg

added theorem measure_theory.vector_measure.coe_smul

added theorem measure_theory.vector_measure.coe_sub

added theorem measure_theory.vector_measure.coe_zero

added theorem measure_theory.vector_measure.empty

added theorem measure_theory.vector_measure.ext

added theorem measure_theory.vector_measure.ext_iff'

added theorem measure_theory.vector_measure.ext_iff

added theorem measure_theory.vector_measure.has_sum_of_disjoint_Union

added theorem measure_theory.vector_measure.m_Union

added theorem measure_theory.vector_measure.measure_of_eq_coe

added def measure_theory.vector_measure.neg

added theorem measure_theory.vector_measure.neg_apply

added theorem measure_theory.vector_measure.not_measurable

added theorem measure_theory.vector_measure.of_Union_nonneg

added theorem measure_theory.vector_measure.of_Union_nonpos

added theorem measure_theory.vector_measure.of_add_of_diff

added theorem measure_theory.vector_measure.of_diff

added theorem measure_theory.vector_measure.of_disjoint_Union

added theorem measure_theory.vector_measure.of_disjoint_Union_nat

added theorem measure_theory.vector_measure.of_nonneg_disjoint_union_eq_zero

added theorem measure_theory.vector_measure.of_nonpos_disjoint_union_eq_zero

added theorem measure_theory.vector_measure.of_union

added def measure_theory.vector_measure.smul

added theorem measure_theory.vector_measure.smul_apply

added def measure_theory.vector_measure.sub

added theorem measure_theory.vector_measure.sub_apply

added theorem measure_theory.vector_measure.zero_apply

added structure measure_theory.vector_measure

Modified src/topology/instances/ennreal.lean

added theorem ennreal.summable_to_real

Modified src/topology/instances/nnreal.lean