Commit 2023-05-29 08:45 a6e9434c

View on Github →

feat: port MeasureTheory.Measure.VectorMeasure (#4016)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/VectorMeasure.lean

added def MeasureTheory.Measure.toEnnrealVectorMeasure

added theorem MeasureTheory.Measure.toEnnrealVectorMeasure_add

added theorem MeasureTheory.Measure.toEnnrealVectorMeasure_apply_measurable

added theorem MeasureTheory.Measure.toEnnrealVectorMeasure_zero

added def MeasureTheory.Measure.toSignedMeasure

added theorem MeasureTheory.Measure.toSignedMeasure_add

added theorem MeasureTheory.Measure.toSignedMeasure_apply_measurable

added theorem MeasureTheory.Measure.toSignedMeasure_congr

added theorem MeasureTheory.Measure.toSignedMeasure_eq_toSignedMeasure_iff

added theorem MeasureTheory.Measure.toSignedMeasure_smul

added theorem MeasureTheory.Measure.toSignedMeasure_sub_apply

added theorem MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLe

added theorem MeasureTheory.Measure.toSignedMeasure_zero

added theorem MeasureTheory.Measure.zero_le_toSignedMeasure

added def MeasureTheory.SignedMeasure.toMeasureOfLeZero

added theorem MeasureTheory.SignedMeasure.toMeasureOfLeZero_apply

added theorem MeasureTheory.SignedMeasure.toMeasureOfLeZero_toSignedMeasure

added def MeasureTheory.SignedMeasure.toMeasureOfZeroLe'

added def MeasureTheory.SignedMeasure.toMeasureOfZeroLe

added theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLe_apply

added theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLe_toSignedMeasure

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.add

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.ennrealToMeasure

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.eq

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.map

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.neg_left

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.neg_right

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.refl

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.smul

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.sub

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.trans

added theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.zero

added def MeasureTheory.VectorMeasure.AbsolutelyContinuous

added theorem MeasureTheory.VectorMeasure.MutuallySingular.add_left

added theorem MeasureTheory.VectorMeasure.MutuallySingular.add_right

added theorem MeasureTheory.VectorMeasure.MutuallySingular.mk

added theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_left

added theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_left_iff

added theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_right

added theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_right_iff

added theorem MeasureTheory.VectorMeasure.MutuallySingular.smul_left

added theorem MeasureTheory.VectorMeasure.MutuallySingular.smul_right

added theorem MeasureTheory.VectorMeasure.MutuallySingular.symm

added theorem MeasureTheory.VectorMeasure.MutuallySingular.zero_left

added theorem MeasureTheory.VectorMeasure.MutuallySingular.zero_right

added def MeasureTheory.VectorMeasure.MutuallySingular

added def MeasureTheory.VectorMeasure.add

added theorem MeasureTheory.VectorMeasure.add_apply

added def MeasureTheory.VectorMeasure.coeFnAddMonoidHom

added theorem MeasureTheory.VectorMeasure.coe_add

added theorem MeasureTheory.VectorMeasure.coe_injective

added theorem MeasureTheory.VectorMeasure.coe_neg

added theorem MeasureTheory.VectorMeasure.coe_smul

added theorem MeasureTheory.VectorMeasure.coe_sub

added theorem MeasureTheory.VectorMeasure.coe_zero

added theorem MeasureTheory.VectorMeasure.empty

added def MeasureTheory.VectorMeasure.ennrealToMeasure

added theorem MeasureTheory.VectorMeasure.ennrealToMeasure_apply

added def MeasureTheory.VectorMeasure.equivMeasure

added theorem MeasureTheory.VectorMeasure.exists_pos_measure_of_not_restrict_le_zero

added theorem MeasureTheory.VectorMeasure.ext

added theorem MeasureTheory.VectorMeasure.ext_iff'

added theorem MeasureTheory.VectorMeasure.ext_iff

added theorem MeasureTheory.VectorMeasure.hasSum_of_disjoint_iUnion

added theorem MeasureTheory.VectorMeasure.le_iff'

added theorem MeasureTheory.VectorMeasure.le_iff

added theorem MeasureTheory.VectorMeasure.le_restrict_empty

added theorem MeasureTheory.VectorMeasure.le_restrict_univ_iff_le

added theorem MeasureTheory.VectorMeasure.m_iUnion

added def MeasureTheory.VectorMeasure.map

added def MeasureTheory.VectorMeasure.mapGm

added def MeasureTheory.VectorMeasure.mapRange

added def MeasureTheory.VectorMeasure.mapRangeHom

added theorem MeasureTheory.VectorMeasure.mapRange_add

added theorem MeasureTheory.VectorMeasure.mapRange_apply

added theorem MeasureTheory.VectorMeasure.mapRange_id

added theorem MeasureTheory.VectorMeasure.mapRange_zero

added def MeasureTheory.VectorMeasure.mapRangeₗ

added theorem MeasureTheory.VectorMeasure.map_add

added theorem MeasureTheory.VectorMeasure.map_apply

added theorem MeasureTheory.VectorMeasure.map_id

added theorem MeasureTheory.VectorMeasure.map_not_measurable

added theorem MeasureTheory.VectorMeasure.map_smul

added theorem MeasureTheory.VectorMeasure.map_zero

added def MeasureTheory.VectorMeasure.mapₗ

added theorem MeasureTheory.VectorMeasure.measurable_of_not_restrict_le_zero

added theorem MeasureTheory.VectorMeasure.measurable_of_not_zero_le_restrict

added def MeasureTheory.VectorMeasure.neg

added theorem MeasureTheory.VectorMeasure.neg_apply

added theorem MeasureTheory.VectorMeasure.neg_le_neg_iff

added theorem MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict

added theorem MeasureTheory.VectorMeasure.nonpos_of_restrict_le_zero

added theorem MeasureTheory.VectorMeasure.not_measurable

added theorem MeasureTheory.VectorMeasure.of_add_of_diff

added theorem MeasureTheory.VectorMeasure.of_diff

added theorem MeasureTheory.VectorMeasure.of_diff_of_diff_eq_zero

added theorem MeasureTheory.VectorMeasure.of_disjoint_iUnion

added theorem MeasureTheory.VectorMeasure.of_disjoint_iUnion_nat

added theorem MeasureTheory.VectorMeasure.of_iUnion_nonneg

added theorem MeasureTheory.VectorMeasure.of_iUnion_nonpos

added theorem MeasureTheory.VectorMeasure.of_nonneg_disjoint_union_eq_zero

added theorem MeasureTheory.VectorMeasure.of_nonpos_disjoint_union_eq_zero

added theorem MeasureTheory.VectorMeasure.of_union

added def MeasureTheory.VectorMeasure.restrict

added def MeasureTheory.VectorMeasure.restrictGm

added theorem MeasureTheory.VectorMeasure.restrict_add

added theorem MeasureTheory.VectorMeasure.restrict_apply

added theorem MeasureTheory.VectorMeasure.restrict_empty

added theorem MeasureTheory.VectorMeasure.restrict_eq_self

added theorem MeasureTheory.VectorMeasure.restrict_le_restrict_countable_iUnion

added theorem MeasureTheory.VectorMeasure.restrict_le_restrict_iUnion

added theorem MeasureTheory.VectorMeasure.restrict_le_restrict_iff

added theorem MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le

added theorem MeasureTheory.VectorMeasure.restrict_le_restrict_subset

added theorem MeasureTheory.VectorMeasure.restrict_le_restrict_union

added theorem MeasureTheory.VectorMeasure.restrict_le_zero_of_not_measurable

added theorem MeasureTheory.VectorMeasure.restrict_le_zero_subset

added theorem MeasureTheory.VectorMeasure.restrict_not_measurable

added theorem MeasureTheory.VectorMeasure.restrict_smul

added theorem MeasureTheory.VectorMeasure.restrict_trim

added theorem MeasureTheory.VectorMeasure.restrict_univ

added theorem MeasureTheory.VectorMeasure.restrict_zero

added def MeasureTheory.VectorMeasure.restrictₗ

added def MeasureTheory.VectorMeasure.smul

added theorem MeasureTheory.VectorMeasure.smul_apply

added def MeasureTheory.VectorMeasure.sub

added theorem MeasureTheory.VectorMeasure.sub_apply

added theorem MeasureTheory.VectorMeasure.subset_le_of_restrict_le_restrict

added def MeasureTheory.VectorMeasure.trim

added theorem MeasureTheory.VectorMeasure.trim_eq_self

added theorem MeasureTheory.VectorMeasure.trim_measurableSet_eq

added theorem MeasureTheory.VectorMeasure.zero_apply

added theorem MeasureTheory.VectorMeasure.zero_le_restrict_not_measurable

added theorem MeasureTheory.VectorMeasure.zero_le_restrict_subset

added theorem MeasureTheory.VectorMeasure.zero_trim

added structure MeasureTheory.VectorMeasure