Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-14 13:38 8f863f6b

View on Github →

feat(measure_theory/decomposition/jordan): the Jordan decomposition theorem for signed measures (#8645) This PR proves the Jordan decomposition theorem for signed measures, that is, given a signed measure s, there exists a unique pair of mutually singular measures μ and ν, such that s = μ - ν.

Estimated changes

Created src/measure_theory/decomposition/jordan.lean

added theorem measure_theory.jordan_decomposition.exists_compl_positive_negative

added theorem measure_theory.jordan_decomposition.neg_neg_part

added theorem measure_theory.jordan_decomposition.neg_pos_part

added theorem measure_theory.jordan_decomposition.to_jordan_decomposition_to_signed_measure

added def measure_theory.jordan_decomposition.to_signed_measure

added theorem measure_theory.jordan_decomposition.to_signed_measure_injective

added theorem measure_theory.jordan_decomposition.to_signed_measure_neg

added theorem measure_theory.jordan_decomposition.to_signed_measure_zero

added theorem measure_theory.jordan_decomposition.zero_neg_part

added theorem measure_theory.jordan_decomposition.zero_pos_part

added structure measure_theory.jordan_decomposition

added theorem measure_theory.signed_measure.of_diff_eq_zero_of_symm_diff_eq_zero_negative

added theorem measure_theory.signed_measure.of_diff_eq_zero_of_symm_diff_eq_zero_positive

added theorem measure_theory.signed_measure.of_inter_eq_of_symm_diff_eq_zero_negative

added theorem measure_theory.signed_measure.of_inter_eq_of_symm_diff_eq_zero_positive

added theorem measure_theory.signed_measure.subset_negative_null_set

added theorem measure_theory.signed_measure.subset_positive_null_set

added def measure_theory.signed_measure.to_jordan_decomposition

added def measure_theory.signed_measure.to_jordan_decomposition_equiv

added theorem measure_theory.signed_measure.to_jordan_decomposition_neg

added theorem measure_theory.signed_measure.to_jordan_decomposition_spec

added theorem measure_theory.signed_measure.to_jordan_decomposition_zero

added theorem measure_theory.signed_measure.to_signed_measure_to_jordan_decomposition

Modified src/measure_theory/measure/vector_measure.lean

deleted def measure_theory.measure.sub_to_signed_measure

deleted theorem measure_theory.measure.sub_to_signed_measure_apply

added theorem measure_theory.measure.to_signed_measure_eq_to_signed_measure_iff

added theorem measure_theory.measure.to_signed_measure_sub_apply

added theorem measure_theory.vector_measure.of_diff_of_diff_eq_zero