Commit 2023-05-30 21:51 dea27b27

View on Github →

feat: port MeasureTheory.Decomposition.Jordan (#4500)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Decomposition/Jordan.lean

added theorem MeasureTheory.JordanDecomposition.coe_smul

added theorem MeasureTheory.JordanDecomposition.exists_compl_positive_negative

added theorem MeasureTheory.JordanDecomposition.neg_negPart

added theorem MeasureTheory.JordanDecomposition.neg_posPart

added theorem MeasureTheory.JordanDecomposition.real_smul_def

added theorem MeasureTheory.JordanDecomposition.real_smul_neg

added theorem MeasureTheory.JordanDecomposition.real_smul_negPart_neg

added theorem MeasureTheory.JordanDecomposition.real_smul_negPart_nonneg

added theorem MeasureTheory.JordanDecomposition.real_smul_nonneg

added theorem MeasureTheory.JordanDecomposition.real_smul_posPart_neg

added theorem MeasureTheory.JordanDecomposition.real_smul_posPart_nonneg

added theorem MeasureTheory.JordanDecomposition.smul_negPart

added theorem MeasureTheory.JordanDecomposition.smul_posPart

added theorem MeasureTheory.JordanDecomposition.toJordanDecomposition_toSignedMeasure

added def MeasureTheory.JordanDecomposition.toSignedMeasure

added theorem MeasureTheory.JordanDecomposition.toSignedMeasure_injective

added theorem MeasureTheory.JordanDecomposition.toSignedMeasure_neg

added theorem MeasureTheory.JordanDecomposition.toSignedMeasure_smul

added theorem MeasureTheory.JordanDecomposition.toSignedMeasure_zero

added theorem MeasureTheory.JordanDecomposition.zero_negPart

added theorem MeasureTheory.JordanDecomposition.zero_posPart

added structure MeasureTheory.JordanDecomposition

added theorem MeasureTheory.SignedMeasure.absolutelyContinuous_ennreal_iff

added theorem MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff

added theorem MeasureTheory.SignedMeasure.mutuallySingular_iff

added theorem MeasureTheory.SignedMeasure.null_of_totalVariation_zero

added theorem MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_negative

added theorem MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_positive

added theorem MeasureTheory.SignedMeasure.of_inter_eq_of_symmDiff_eq_zero_negative

added theorem MeasureTheory.SignedMeasure.of_inter_eq_of_symmDiff_eq_zero_positive

added theorem MeasureTheory.SignedMeasure.subset_negative_null_set

added theorem MeasureTheory.SignedMeasure.subset_positive_null_set

added def MeasureTheory.SignedMeasure.toJordanDecomposition

added def MeasureTheory.SignedMeasure.toJordanDecompositionEquiv

added theorem MeasureTheory.SignedMeasure.toJordanDecomposition_eq

added theorem MeasureTheory.SignedMeasure.toJordanDecomposition_neg

added theorem MeasureTheory.SignedMeasure.toJordanDecomposition_smul

added theorem MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real

added theorem MeasureTheory.SignedMeasure.toJordanDecomposition_spec

added theorem MeasureTheory.SignedMeasure.toJordanDecomposition_zero

added theorem MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition

added def MeasureTheory.SignedMeasure.totalVariation

added theorem MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iff

added theorem MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff

added theorem MeasureTheory.SignedMeasure.totalVariation_neg

added theorem MeasureTheory.SignedMeasure.totalVariation_zero

Modified Mathlib/MeasureTheory/Measure/VectorMeasure.lean

added theorem MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLE

deleted theorem MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLe

added def MeasureTheory.SignedMeasure.toMeasureOfLEZero

added theorem MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply

added theorem MeasureTheory.SignedMeasure.toMeasureOfLEZero_toSignedMeasure

deleted def MeasureTheory.SignedMeasure.toMeasureOfLeZero

deleted theorem MeasureTheory.SignedMeasure.toMeasureOfLeZero_apply

deleted 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

deleted def MeasureTheory.SignedMeasure.toMeasureOfZeroLe'

deleted def MeasureTheory.SignedMeasure.toMeasureOfZeroLe

deleted theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLe_apply

deleted theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLe_toSignedMeasure