Commit 2021-05-15 08:16 fc94b47f

View on Github →

feat(counterexamples): a counterexample on the Pettis integral (#7553) Phillips (1940) has exhibited under the continuum hypothesis a bounded weakly measurable function which is not Pettis-integrable. We formalize this counterexample.

Estimated changes

Created counterexamples/phillips.lean

added def continuous_linear_map.to_bounded_additive_measure

added def discrete_copy

added def measure_theory.measure.extension_to_bounded_functions

added theorem phillips_1940.apply_f_eq_continuous_part

added def phillips_1940.bounded_additive_measure.C

added theorem phillips_1940.bounded_additive_measure.abs_le_bound

added theorem phillips_1940.bounded_additive_measure.additive

added theorem phillips_1940.bounded_additive_measure.apply_countable

added def phillips_1940.bounded_additive_measure.continuous_part

added theorem phillips_1940.bounded_additive_measure.continuous_part_apply_diff

added theorem phillips_1940.bounded_additive_measure.continuous_part_apply_eq_zero_of_countable

added theorem phillips_1940.bounded_additive_measure.countable_discrete_support

added def phillips_1940.bounded_additive_measure.discrete_part

added theorem phillips_1940.bounded_additive_measure.discrete_part_apply

added def phillips_1940.bounded_additive_measure.discrete_support

added theorem phillips_1940.bounded_additive_measure.empty

added theorem phillips_1940.bounded_additive_measure.eq_add_parts

added theorem phillips_1940.bounded_additive_measure.exists_discrete_support

added theorem phillips_1940.bounded_additive_measure.exists_discrete_support_nonpos

added theorem phillips_1940.bounded_additive_measure.le_bound

added theorem phillips_1940.bounded_additive_measure.neg_apply

added def phillips_1940.bounded_additive_measure.restrict

added theorem phillips_1940.bounded_additive_measure.restrict_apply

added structure phillips_1940.bounded_additive_measure

added def phillips_1940.bounded_integrable_functions

added def phillips_1940.bounded_integrable_functions_integral_clm

added theorem phillips_1940.comp_ae_eq_const

added theorem phillips_1940.continuous_part_eval_clm_eq_zero

added theorem phillips_1940.countable_compl_spf

added theorem phillips_1940.countable_ne

added theorem phillips_1940.countable_spf_mem

added theorem phillips_1940.exists_linear_extension_to_bounded_functions

added theorem phillips_1940.extension_to_bounded_functions_apply

added def phillips_1940.f

added theorem phillips_1940.integrable_comp

added theorem phillips_1940.integral_comp

added theorem phillips_1940.measurable_comp

added theorem phillips_1940.no_pettis_integral

added theorem phillips_1940.norm_bound

added theorem phillips_1940.norm_indicator_le_one

added theorem phillips_1940.sierpinski_pathological_family

added def phillips_1940.spf

added theorem phillips_1940.to_functions_to_measure

added theorem phillips_1940.to_functions_to_measure_continuous_part

Modified docs/references.bib

Modified src/data/set/basic.lean

added theorem set.diff_union_inter

added theorem set.union_eq_diff_union_diff_union_inter

deleted theorem set.union_eq_sdiff_union_sdiff_union_inter

Modified src/measure_theory/lebesgue_measure.lean

Modified src/measure_theory/lp_space.lean

Modified src/measure_theory/measurable_space.lean

added theorem measurable.measurable_of_countable_ne

added theorem set.countable.measurable_set

Modified src/measure_theory/measure_space.lean

added theorem finset.measure_zero

deleted theorem measure_theory.measure_countable

deleted theorem measure_theory.measure_finite

deleted theorem measure_theory.measure_finset

added theorem set.countable.measure_zero

added theorem set.finite.measure_zero

Modified src/set_theory/cardinal_ordinal.lean

added theorem cardinal.countable_iff_lt_aleph_one

Modified src/topology/continuous_function/bounded.lean

added theorem bounded_continuous_function.coe_of_normed_group

added theorem bounded_continuous_function.coe_of_normed_group_discrete

modified theorem bounded_continuous_function.continuous_eval

modified theorem bounded_continuous_function.continuous_evalx

added def bounded_continuous_function.eval_clm

added theorem bounded_continuous_function.eval_clm_apply