Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-27 09:34 cafd6fbc

View on Github →

chore(measure_theory/decomposition/lebesgue): rename radon_nikodym_deriv to rn_deriv (#9386)

Estimated changes

Modified src/measure_theory/decomposition/lebesgue.lean

deleted theorem measure_theory.measure.eq_radon_nikodym_deriv

added theorem measure_theory.measure.eq_rn_deriv

deleted theorem measure_theory.measure.lintegral_radon_nikodym_deriv_lt_top

added theorem measure_theory.measure.lintegral_rn_deriv_lt_top

deleted theorem measure_theory.measure.measurable_radon_nikodym_deriv

added theorem measure_theory.measure.measurable_rn_deriv

deleted def measure_theory.measure.radon_nikodym_deriv

added def measure_theory.measure.rn_deriv

deleted theorem measure_theory.measure.with_density_radon_nikodym_deriv_le

added theorem measure_theory.measure.with_density_rn_deriv_le

deleted theorem measure_theory.signed_measure.eq_radon_nikodym_deriv

added theorem measure_theory.signed_measure.eq_rn_deriv

deleted theorem measure_theory.signed_measure.integrable_radon_nikodym_deriv

added theorem measure_theory.signed_measure.integrable_rn_deriv

deleted theorem measure_theory.signed_measure.measurable_radon_nikodym_deriv

added theorem measure_theory.signed_measure.measurable_rn_deriv

deleted def measure_theory.signed_measure.radon_nikodym_deriv

deleted theorem measure_theory.signed_measure.radon_nikodym_deriv_add

deleted theorem measure_theory.signed_measure.radon_nikodym_deriv_neg

deleted theorem measure_theory.signed_measure.radon_nikodym_deriv_smul

deleted theorem measure_theory.signed_measure.radon_nikodym_deriv_sub

added def measure_theory.signed_measure.rn_deriv

added theorem measure_theory.signed_measure.rn_deriv_add

added theorem measure_theory.signed_measure.rn_deriv_neg

added theorem measure_theory.signed_measure.rn_deriv_smul

added theorem measure_theory.signed_measure.rn_deriv_sub

deleted theorem measure_theory.signed_measure.singular_part_add_with_density_radon_nikodym_deriv_eq

added theorem measure_theory.signed_measure.singular_part_add_with_density_rn_deriv_eq

Modified src/measure_theory/decomposition/radon_nikodym.lean

deleted theorem measure_theory.measure.absolutely_continuous_iff_with_density_radon_nikodym_deriv_eq

added theorem measure_theory.measure.absolutely_continuous_iff_with_density_rn_deriv_eq

deleted theorem measure_theory.measure.with_density_radon_nikodym_deriv_eq

deleted theorem measure_theory.measure.with_density_radon_nikodym_deriv_to_real_eq

added theorem measure_theory.measure.with_density_rn_deriv_eq

added theorem measure_theory.measure.with_density_rn_deriv_to_real_eq

deleted theorem measure_theory.signed_measure.absolutely_continuous_iff_with_densityᵥ_radon_nikodym_deriv_eq

added theorem measure_theory.signed_measure.absolutely_continuous_iff_with_densityᵥ_rn_deriv_eq

deleted theorem measure_theory.signed_measure.with_densityᵥ_radon_nikodym_deriv_eq

added theorem measure_theory.signed_measure.with_densityᵥ_rn_deriv_eq