Commit 2020-12-30 20:43 99881936

View on Github →

feat(measure_theory): various additions (#5389) Some computations of measures on non-measurable sets Some more measurability lemmas for pi-types Cleanup in measure_space

Estimated changes

Modified src/data/equiv/list.lean

Modified src/measure_theory/borel_space.lean

Modified src/measure_theory/measurable_space.lean

added theorem is_measurable.Inter_fintype

added theorem is_measurable.Union_fintype

added theorem is_measurable.pi

added theorem is_measurable.pi_fintype

added theorem is_measurable.pi_univ

modified theorem is_measurable_pi

added theorem is_measurable_pi_of_nonempty

added theorem measurable.eval

added def measurable_equiv.Pi_congr_right

added theorem measurable_equiv.coe_mk

added theorem measurable_equiv.coe_symm_mk

added theorem measurable_pi_iff

added theorem measurable_update

added theorem nonempty_measurable_superset

Modified src/measure_theory/measure_space.lean

modified def completion

modified theorem is_measurable.diff_null

modified theorem is_measurable.is_null_measurable

modified theorem is_null_measurable.Union_nat

modified theorem is_null_measurable.compl

modified theorem is_null_measurable.diff_null

modified theorem is_null_measurable.union_null

modified def is_null_measurable

modified theorem is_null_measurable_iff

modified theorem is_null_measurable_measure_eq

modified theorem is_null_measurable_of_complete

modified theorem measure_theory.ae_all_iff

modified theorem measure_theory.ae_ball_iff

modified theorem measure_theory.ae_eq_empty

modified theorem measure_theory.ae_eq_refl

modified theorem measure_theory.ae_eq_symm

modified theorem measure_theory.ae_eq_trans

modified theorem measure_theory.ae_le_set

modified theorem measure_theory.ae_map_iff

modified theorem measure_theory.ae_of_all

modified theorem measure_theory.ae_restrict_eq

modified theorem measure_theory.ae_restrict_iff

modified theorem measure_theory.diff_ae_eq_self

modified theorem measure_theory.eventually_eq_dirac'

modified theorem measure_theory.eventually_eq_dirac

modified theorem measure_theory.exists_is_measurable_superset_iff_measure_eq_zero

modified theorem measure_theory.exists_is_measurable_superset_of_measure_eq_zero

modified theorem measure_theory.le_to_measure_apply

modified theorem measure_theory.le_to_outer_measure_caratheodory

modified theorem measure_theory.measure.Inf_apply

modified theorem measure_theory.measure.add_apply

modified theorem measure_theory.measure.coe_smul

modified theorem measure_theory.measure.compl_mem_cofinite

modified theorem measure_theory.measure.count_apply

modified theorem measure_theory.measure.count_apply_eq_top

modified theorem measure_theory.measure.count_apply_infinite

modified theorem measure_theory.measure.count_apply_lt_top

modified theorem measure_theory.measure.dirac_apply'

modified theorem measure_theory.measure.dirac_apply

modified theorem measure_theory.measure.dirac_apply_of_mem

modified theorem measure_theory.measure.ext

modified theorem measure_theory.measure.ext_iff

modified theorem measure_theory.measure.finite_at_principal

modified def measure_theory.measure.is_complete

modified theorem measure_theory.measure.le_lift_linear_apply

added theorem measure_theory.measure.le_map_apply

modified theorem measure_theory.measure.le_sum

modified theorem measure_theory.measure.map_comap_subtype_coe

modified theorem measure_theory.measure.measure_univ_eq_zero

modified theorem measure_theory.measure.mem_cofinite

modified def measure_theory.measure.of_measurable

modified theorem measure_theory.measure.of_measurable_apply

modified theorem measure_theory.measure.restrict_Inf_eq_Inf_restrict

modified theorem measure_theory.measure.restrict_Union

modified theorem measure_theory.measure.restrict_Union_apply

modified theorem measure_theory.measure.restrict_Union_apply_eq_supr

modified theorem measure_theory.measure.restrict_Union_le

modified theorem measure_theory.measure.restrict_add_restrict_compl

modified theorem measure_theory.measure.restrict_apply

modified theorem measure_theory.measure.restrict_apply_eq_zero'

modified theorem measure_theory.measure.restrict_apply_eq_zero

modified theorem measure_theory.measure.restrict_compl_add_restrict

modified theorem measure_theory.measure.restrict_congr_meas

modified theorem measure_theory.measure.restrict_congr_mono

modified theorem measure_theory.measure.restrict_eq_zero

modified theorem measure_theory.measure.restrict_le_self

modified theorem measure_theory.measure.restrict_restrict

modified theorem measure_theory.measure.restrict_sum

modified theorem measure_theory.measure.restrict_to_outer_measure_eq_to_outer_measure_restrict

modified theorem measure_theory.measure.restrict_union

modified theorem measure_theory.measure.restrict_union_add_inter

modified theorem measure_theory.measure.restrict_union_apply

modified theorem measure_theory.measure.restrict_union_congr

modified theorem measure_theory.measure.smul_apply

modified theorem measure_theory.measure.sub_apply

modified def measure_theory.measure.sum

modified theorem measure_theory.measure.sum_apply

modified theorem measure_theory.measure.supr_restrict_spanning_sets

modified theorem measure_theory.measure.to_outer_measure_injective

modified theorem measure_theory.measure_Union

modified theorem measure_theory.measure_Union_le

modified theorem measure_theory.measure_Union_null

modified theorem measure_theory.measure_Union_null_iff

modified theorem measure_theory.measure_compl

modified theorem measure_theory.measure_congr

modified theorem measure_theory.measure_countable

modified theorem measure_theory.measure_diff

added theorem measure_theory.measure_eq_infi'

modified theorem measure_theory.measure_eq_infi

modified theorem measure_theory.measure_eq_inter_diff

modified theorem measure_theory.measure_eq_trim

modified theorem measure_theory.measure_finite

modified theorem measure_theory.measure_if

modified theorem measure_theory.measure_mono_ae

modified theorem measure_theory.measure_union_add_inter

modified theorem measure_theory.measure_union_null

modified theorem measure_theory.measure_union_null_iff

modified theorem measure_theory.mem_ae_map_iff

modified theorem measure_theory.mem_dirac_ae_iff

modified def measure_theory.outer_measure.to_measure

modified theorem measure_theory.restrict_congr_set

modified theorem measure_theory.restrict_mono_ae

modified theorem measure_theory.tendsto_measure_Inter

modified theorem measure_theory.tendsto_measure_Union

modified theorem measure_theory.to_measure_apply

modified theorem measure_theory.to_measure_to_outer_measure

modified theorem measure_theory.to_outer_measure_apply

modified theorem measure_theory.to_outer_measure_to_measure

modified theorem measure_theory.union_ae_eq_right

modified theorem metric.bounded.finite_measure

modified theorem null_is_null_measurable

modified def null_measurable

Modified src/measure_theory/prod.lean

added theorem measure_theory.measure.prod_prod_le