Commit 2022-02-21 22:53 eb5c5ed5

View on Github →

feat(measure_theory/integral/set_integral): Bochner integral with respect to a measure with density (#12123) This PR shows that ∫ a, g a ∂(μ.with_density (λ x, f x)) = ∫ a, f a • g a ∂μ. (This fact is already available for the Lebesgue integral, not for the Bochner integral.)

Estimated changes

Modified src/measure_theory/constructions/borel_space.lean

added theorem continuous_on.measurable_piecewise

Modified src/measure_theory/function/l1_space.lean

added theorem measure_theory.integrable_with_density_iff_integrable_coe_smul

added theorem measure_theory.integrable_with_density_iff_integrable_coe_smul₀

modified theorem measure_theory.integrable_with_density_iff_integrable_smul

added theorem measure_theory.integrable_with_density_iff_integrable_smul₀

added theorem measure_theory.mem_ℒ1_smul_of_L1_with_density

added theorem measure_theory.with_density_smul_li_apply

Modified src/measure_theory/group/measure.lean

Modified src/measure_theory/integral/set_integral.lean

added theorem integral_with_density_eq_integral_smul

added theorem integral_with_density_eq_integral_smul₀

added theorem set_integral_with_density_eq_set_integral_smul

added theorem set_integral_with_density_eq_set_integral_smul₀