Commit 2023-06-07 04:25 aab87ec2

View on Github →

feat: port MeasureTheory.Decomposition.Lebesgue (#4736)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

added theorem MeasureTheory.ComplexMeasure.integrable_rnDeriv

added def MeasureTheory.ComplexMeasure.rnDeriv

added def MeasureTheory.ComplexMeasure.singularPart

added theorem MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq

added theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le

added theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE'

added theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE

added theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone'

added theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone

added theorem MeasureTheory.Measure.LebesgueDecomposition.iSup_succ_eq_sup

added def MeasureTheory.Measure.LebesgueDecomposition.measurableLE

added def MeasureTheory.Measure.LebesgueDecomposition.measurableLEEval

added theorem MeasureTheory.Measure.LebesgueDecomposition.sup_mem_measurableLE

added theorem MeasureTheory.Measure.LebesgueDecomposition.zero_mem_measurableLE

added theorem MeasureTheory.Measure.eq_rnDeriv

added theorem MeasureTheory.Measure.eq_singularPart

added theorem MeasureTheory.Measure.eq_withDensity_rnDeriv

added theorem MeasureTheory.Measure.exists_positive_of_not_mutuallySingular

added theorem MeasureTheory.Measure.haveLebesgueDecomposition_add

added theorem MeasureTheory.Measure.haveLebesgueDecomposition_of_finiteMeasure

added theorem MeasureTheory.Measure.haveLebesgueDecomposition_spec

added theorem MeasureTheory.Measure.lintegral_rnDeriv_lt_top

added theorem MeasureTheory.Measure.lintegral_rnDeriv_lt_top_of_measure_ne_top

added theorem MeasureTheory.Measure.measurable_rnDeriv

added theorem MeasureTheory.Measure.mutuallySingular_singularPart

added theorem MeasureTheory.Measure.rnDeriv_lt_top

added theorem MeasureTheory.Measure.rnDeriv_restrict

added theorem MeasureTheory.Measure.rnDeriv_withDensity

added theorem MeasureTheory.Measure.singularPart_add

added theorem MeasureTheory.Measure.singularPart_le

added theorem MeasureTheory.Measure.singularPart_smul

added theorem MeasureTheory.Measure.singularPart_withDensity

added theorem MeasureTheory.Measure.singularPart_zero

added theorem MeasureTheory.Measure.withDensity_rnDeriv_le

added theorem MeasureTheory.SignedMeasure.eq_rnDeriv

added theorem MeasureTheory.SignedMeasure.eq_singularPart

added theorem MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mk

added theorem MeasureTheory.SignedMeasure.integrable_rnDeriv

added theorem MeasureTheory.SignedMeasure.jordanDecomposition_add_withDensity_mutuallySingular

added theorem MeasureTheory.SignedMeasure.measurable_rnDeriv

added theorem MeasureTheory.SignedMeasure.not_haveLebesgueDecomposition_iff

added def MeasureTheory.SignedMeasure.rnDeriv

added theorem MeasureTheory.SignedMeasure.rnDeriv_add

added theorem MeasureTheory.SignedMeasure.rnDeriv_def

added theorem MeasureTheory.SignedMeasure.rnDeriv_neg

added theorem MeasureTheory.SignedMeasure.rnDeriv_smul

added theorem MeasureTheory.SignedMeasure.rnDeriv_sub

added def MeasureTheory.SignedMeasure.singularPart

added theorem MeasureTheory.SignedMeasure.singularPart_add

added theorem MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq

added theorem MeasureTheory.SignedMeasure.singularPart_mutuallySingular

added theorem MeasureTheory.SignedMeasure.singularPart_neg

added theorem MeasureTheory.SignedMeasure.singularPart_smul_nnreal

added theorem MeasureTheory.SignedMeasure.singularPart_sub

added theorem MeasureTheory.SignedMeasure.singularPart_totalVariation

added theorem MeasureTheory.SignedMeasure.singularPart_zero

added theorem MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity