Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-18 04:29 db06b677

View on Github →

feat(measure_theory/prod): product measures and Fubini's theorem (#4590)

Define the product measure of two σ-finite measures.
Prove Tonelli's theorem.
Prove Fubini's theorem.

Estimated changes

Modified docs/overview.yaml

Modified docs/references.bib

Modified docs/undergrad.yaml

Modified src/data/indicator_function.lean

added theorem set.indicator_mul_left

added theorem set.indicator_mul_right

Modified src/measure_theory/measure_space.lean

Created src/measure_theory/prod.lean

added theorem generate_from_prod

added theorem is_measurable_integrable

added theorem is_pi_system_prod

added theorem measurable.integral_prod_left'

added theorem measurable.integral_prod_left

added theorem measurable.integral_prod_right'

added theorem measurable.integral_prod_right

added theorem measurable.lintegral_prod_left'

added theorem measurable.lintegral_prod_left

added theorem measurable.lintegral_prod_right'

added theorem measurable.lintegral_prod_right

added theorem measurable.map_prod_mk_left

added theorem measurable.map_prod_mk_right

added theorem measurable_measure_prod_mk_left

added theorem measurable_measure_prod_mk_left_finite

added theorem measurable_measure_prod_mk_right

added theorem measure_theory.continuous_integral_integral

added theorem measure_theory.has_finite_integral_prod_iff

added theorem measure_theory.integrable.integral_norm_prod_left

added theorem measure_theory.integrable.integral_norm_prod_right

added theorem measure_theory.integrable.integral_prod_left

added theorem measure_theory.integrable.integral_prod_right

added theorem measure_theory.integrable.prod_left_ae

added theorem measure_theory.integrable.prod_right_ae

added theorem measure_theory.integrable.swap

added theorem measure_theory.integrable_prod_iff'

added theorem measure_theory.integrable_prod_iff

added theorem measure_theory.integrable_swap_iff

added theorem measure_theory.integral_fn_integral_add

added theorem measure_theory.integral_fn_integral_sub

added theorem measure_theory.integral_integral

added theorem measure_theory.integral_integral_add'

added theorem measure_theory.integral_integral_add

added theorem measure_theory.integral_integral_sub'

added theorem measure_theory.integral_integral_sub

added theorem measure_theory.integral_integral_swap

added theorem measure_theory.integral_integral_symm

added theorem measure_theory.integral_prod

added theorem measure_theory.integral_prod_swap

added theorem measure_theory.integral_prod_symm

added theorem measure_theory.lintegral_fn_integral_sub

added theorem measure_theory.lintegral_lintegral

added theorem measure_theory.lintegral_lintegral_swap

added theorem measure_theory.lintegral_lintegral_symm

added theorem measure_theory.lintegral_prod

added theorem measure_theory.lintegral_prod_swap

added theorem measure_theory.lintegral_prod_symm

added theorem measure_theory.measure.add_prod

added theorem measure_theory.measure.ae_ae_of_ae_prod

added theorem measure_theory.measure.ae_measure_lt_top

added theorem measure_theory.measure.dirac_prod

added theorem measure_theory.measure.dirac_prod_dirac

added theorem measure_theory.measure.integrable_measure_prod_mk_left

added theorem measure_theory.measure.measure_ae_null_of_prod_null

added theorem measure_theory.measure.measure_prod_null

added theorem measure_theory.measure.prod_add

added theorem measure_theory.measure.prod_apply

added theorem measure_theory.measure.prod_apply_symm

added theorem measure_theory.measure.prod_dirac

added theorem measure_theory.measure.prod_eq

added theorem measure_theory.measure.prod_prod

added theorem measure_theory.measure.prod_restrict

added theorem measure_theory.measure.prod_sum

added theorem measure_theory.measure.prod_swap

added theorem measure_theory.measure.prod_unique

added theorem measure_theory.measure.sum_prod