Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-08 11:43 fb0cfbd4

View on Github →

feat(measure_theory/measure/complex): define complex measures (#10166) Complex measures was defined to be a vector measure over ℂ without any API. This PR adds some basic definitions about complex measures and proves the complex version of the Lebesgue decomposition theorem.

Estimated changes

Modified src/measure_theory/decomposition/lebesgue.lean

added theorem measure_theory.complex_measure.integrable_rn_deriv

added def measure_theory.complex_measure.rn_deriv

added def measure_theory.complex_measure.singular_part

added theorem measure_theory.complex_measure.singular_part_add_with_density_rn_deriv_eq

modified theorem measure_theory.signed_measure.singular_part_smul

Created src/measure_theory/measure/complex.lean

added theorem measure_theory.complex_measure.absolutely_continuous_ennreal_iff

added def measure_theory.complex_measure.equiv_signed_measure

added def measure_theory.complex_measure.equiv_signed_measureₗ

added def measure_theory.complex_measure.im

added def measure_theory.complex_measure.re

added theorem measure_theory.complex_measure.to_complex_measure_to_signed_measure

added theorem measure_theory.signed_measure.im_to_complex_measure

added theorem measure_theory.signed_measure.re_to_complex_measure

added def measure_theory.signed_measure.to_complex_measure

added theorem measure_theory.signed_measure.to_complex_measure_apply

Modified src/measure_theory/measure/vector_measure.lean

added def measure_theory.vector_measure.map_range

added theorem measure_theory.vector_measure.map_range_add

added theorem measure_theory.vector_measure.map_range_apply

added def measure_theory.vector_measure.map_range_hom

added theorem measure_theory.vector_measure.map_range_id

added theorem measure_theory.vector_measure.map_range_zero

added def measure_theory.vector_measure.map_rangeₗ