Commit 2021-08-09 15:47 5e368484

View on Github →

feat(measure_theory/decomposition/signed_hahn): signed version of the Hahn decomposition theorem (#8388) This PR defined positive and negative sets with respect to a vector measure and prove the signed version of the Hahn decomposition theorem.

Estimated changes

Created src/measure_theory/decomposition/signed_hahn.lean

added theorem measure_theory.signed_measure.bdd_below_measure_of_negatives

added theorem measure_theory.signed_measure.exists_compl_positive_negative

added theorem measure_theory.signed_measure.exists_is_compl_positive_negative

added theorem measure_theory.signed_measure.exists_subset_restrict_nonpos

added def measure_theory.signed_measure.measure_of_negatives

added theorem measure_theory.signed_measure.of_symm_diff_compl_positive_negative

added theorem measure_theory.signed_measure.zero_mem_measure_of_negatives

Modified src/measure_theory/vector_measure.lean

added theorem measure_theory.vector_measure.exists_pos_measure_of_not_restrict_le_zero

added theorem measure_theory.vector_measure.le_restrict_empty

added theorem measure_theory.vector_measure.measurable_of_not_restrict_le_zero

added theorem measure_theory.vector_measure.measurable_of_not_zero_le_restrict

added theorem measure_theory.vector_measure.nonneg_of_zero_le_restrict

added theorem measure_theory.vector_measure.nonpos_of_restrict_le_zero

added theorem measure_theory.vector_measure.restrict_le_restrict_Union

added theorem measure_theory.vector_measure.restrict_le_restrict_encodable_Union

added theorem measure_theory.vector_measure.restrict_le_restrict_iff

added theorem measure_theory.vector_measure.restrict_le_restrict_of_subset_le

added theorem measure_theory.vector_measure.restrict_le_restrict_subset

added theorem measure_theory.vector_measure.restrict_le_restrict_union

added theorem measure_theory.vector_measure.restrict_le_zero_of_not_measurable

added theorem measure_theory.vector_measure.restrict_le_zero_subset

added theorem measure_theory.vector_measure.restrict_not_measurable

added theorem measure_theory.vector_measure.subset_le_of_restrict_le_restrict

added theorem measure_theory.vector_measure.zero_le_restrict_not_measurable

added theorem measure_theory.vector_measure.zero_le_restrict_subset

Modified src/topology/algebra/infinite_sum.lean

added theorem summable.tendsto_top_of_pos