Commit 2021-09-21 15:54 420f11ab

View on Github →

feat(measure_theory/decomposition/radon_nikodym): Radon-Nikodym and Lebesgue decomposition for signed measures (#9065) This PR proves the Radon-Nikodym theorem for signed measures.

Estimated changes

Modified src/measure_theory/decomposition/jordan.lean

added theorem measure_theory.jordan_decomposition.coe_smul

added theorem measure_theory.jordan_decomposition.real_smul_def

added theorem measure_theory.jordan_decomposition.real_smul_neg

added theorem measure_theory.jordan_decomposition.real_smul_neg_part_neg

added theorem measure_theory.jordan_decomposition.real_smul_neg_part_nonneg

added theorem measure_theory.jordan_decomposition.real_smul_nonneg

added theorem measure_theory.jordan_decomposition.real_smul_pos_part_neg

added theorem measure_theory.jordan_decomposition.real_smul_pos_part_nonneg

added theorem measure_theory.jordan_decomposition.smul_neg_part

added theorem measure_theory.jordan_decomposition.smul_pos_part

added theorem measure_theory.jordan_decomposition.to_signed_measure_smul

added theorem measure_theory.signed_measure.to_jordan_decomposition_eq

added theorem measure_theory.signed_measure.to_jordan_decomposition_smul

added theorem measure_theory.signed_measure.to_jordan_decomposition_smul_real

added theorem measure_theory.signed_measure.to_jordan_decomposition_smul_real_nonneg

added theorem measure_theory.signed_measure.total_variation_mutually_singular_iff

Modified src/measure_theory/decomposition/lebesgue.lean

added theorem measure_theory.measure.lintegral_radon_nikodym_deriv_lt_top

added theorem measure_theory.measure.singular_part_add

added theorem measure_theory.measure.singular_part_smul

added theorem measure_theory.measure.singular_part_zero

added theorem measure_theory.signed_measure.eq_radon_nikodym_deriv

added theorem measure_theory.signed_measure.eq_singular_part

added theorem measure_theory.signed_measure.have_lebesgue_decomposition_mk

added theorem measure_theory.signed_measure.integrable_radon_nikodym_deriv

added theorem measure_theory.signed_measure.jordan_decomposition_add_with_density_mutually_singular

added theorem measure_theory.signed_measure.measurable_radon_nikodym_deriv

added theorem measure_theory.signed_measure.mutually_singular_singular_part

added theorem measure_theory.signed_measure.not_have_lebesgue_decomposition_iff

added def measure_theory.signed_measure.radon_nikodym_deriv

added theorem measure_theory.signed_measure.radon_nikodym_deriv_add

added theorem measure_theory.signed_measure.radon_nikodym_deriv_neg

added theorem measure_theory.signed_measure.radon_nikodym_deriv_smul

added theorem measure_theory.signed_measure.radon_nikodym_deriv_sub

added def measure_theory.signed_measure.singular_part

added theorem measure_theory.signed_measure.singular_part_add

added theorem measure_theory.signed_measure.singular_part_add_with_density_radon_nikodym_deriv_eq

added theorem measure_theory.signed_measure.singular_part_mutually_singular

added theorem measure_theory.signed_measure.singular_part_neg

added theorem measure_theory.signed_measure.singular_part_smul

added theorem measure_theory.signed_measure.singular_part_smul_nnreal

added theorem measure_theory.signed_measure.singular_part_sub

added theorem measure_theory.signed_measure.singular_part_total_variation

added theorem measure_theory.signed_measure.singular_part_zero

added theorem measure_theory.signed_measure.to_jordan_decomposition_eq_of_eq_add_with_density

Modified src/measure_theory/decomposition/radon_nikodym.lean

added theorem measure_theory.measure.with_density_radon_nikodym_deriv_to_real_eq

added theorem measure_theory.signed_measure.absolutely_continuous_iff_with_densityᵥ_radon_nikodym_deriv_eq

added theorem measure_theory.signed_measure.with_densityᵥ_radon_nikodym_deriv_eq

Modified src/measure_theory/integral/lebesgue.lean

added theorem measure_theory.with_density_of_real_mutually_singular

Modified src/measure_theory/measure/vector_measure.lean

added theorem measure_theory.measure.to_signed_measure_congr

Modified src/measure_theory/measure/with_density_vector_measure.lean