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.


Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

docs/references.bib

@@ -789,6 +789,22 @@ @Article{         orosi2018faulhaber
   zbl           = {1411.41023}
 }
 
+@article{phillips1940,
+    AUTHOR = {Phillips, Ralph S.},
+     TITLE = {Integration in a convex linear topological space},
+   JOURNAL = {Trans. Amer. Math. Soc.},
+  FJOURNAL = {Transactions of the American Mathematical Society},
+    VOLUME = {47},
+      YEAR = {1940},
+     PAGES = {114--145},
+      ISSN = {0002-9947},
+   MRCLASS = {46.3X},
+  MRNUMBER = {2707},
+MRREVIEWER = {B. J. Pettis},
+       DOI = {10.2307/1990004},
+       URL = {https://doi.org/10.2307/1990004},
+}
+
 @Misc{            ponton2020chebyshev,
   title         = {Roots of {C}hebyshev polynomials: a purely algebraic
                   approach},

src/data/set/basic.lean

@@ -913,6 +913,9 @@ inf_sdiff_self_right
 @[simp] theorem inter_union_diff (s t : set α) : (s ∩ t) ∪ (s \ t) = s :=
 sup_inf_sdiff s t
 
+@[simp] lemma diff_union_inter (s t : set α) : (s \ t) ∪ (s ∩ t) = s :=
+by { rw union_comm, exact sup_inf_sdiff _ _ }
+
 @[simp] theorem inter_union_compl (s t : set α) : (s ∩ t) ∪ (s ∩ tᶜ) = s := inter_union_diff _ _
 
 theorem diff_subset_diff {s₁ s₂ t₁ t₂ : set α} : s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂ :=
@@ -1047,7 +1050,7 @@ lemma mem_diff_singleton_empty {s : set α} {t : set (set α)} :
   s ∈ t \ {∅} ↔ (s ∈ t ∧ s.nonempty) :=
 mem_diff_singleton.trans $ and_congr iff.rfl ne_empty_iff_nonempty
 
-lemma union_eq_sdiff_union_sdiff_union_inter (s t : set α) :
+lemma union_eq_diff_union_diff_union_inter (s t : set α) :
   s ∪ t = (s \ t) ∪ (t \ s) ∪ (s ∩ t) :=
 sup_eq_sdiff_sup_sdiff_sup_inf
 

src/measure_theory/lebesgue_measure.lean

@@ -285,6 +285,18 @@ instance locally_finite_volume : locally_finite_measure (volume : measure ℝ) :
   mem_nhds_sets is_open_Ioo ⟨sub_lt_self _ zero_lt_one, lt_add_of_pos_right _ zero_lt_one⟩,
   by simp only [real.volume_Ioo, ennreal.of_real_lt_top]⟩⟩
 
+instance finite_measure_restrict_Icc (x y : ℝ) : finite_measure (volume.restrict (Icc x y)) :=
+⟨by simp⟩
+
+instance finite_measure_restrict_Ico (x y : ℝ) : finite_measure (volume.restrict (Ico x y)) :=
+⟨by simp⟩
+
+instance finite_measure_restrict_Ioc (x y : ℝ) : finite_measure (volume.restrict (Ioc x y)) :=
+ ⟨by simp⟩
+
+instance finite_measure_restrict_Ioo (x y : ℝ) : finite_measure (volume.restrict (Ioo x y)) :=
+⟨by simp⟩
+
 /-!
 ### Volume of a box in `ℝⁿ`
 -/

src/measure_theory/lp_space.lean

@@ -1781,7 +1781,7 @@ def to_Lp [normed_field 𝕜] [opens_measurable_space 𝕜] [normed_space 𝕜 E
 linear_map.mk_continuous
   (linear_map.cod_restrict
     (Lp.Lp_submodule E p μ 𝕜)
-    ((continuous_map.to_ae_eq_fun_linear_map μ).comp (forget_boundedness_linear_map α E))
+    ((continuous_map.to_ae_eq_fun_linear_map μ).comp (forget_boundedness_linear_map α E 𝕜))
     mem_Lp)
   _
   Lp_norm_le

src/measure_theory/measurable_space.lean

@@ -263,6 +263,12 @@ finite.induction_on hs measurable_set.empty $ λ a s ha hsf hsm, hsm.insert _
 protected lemma finset.measurable_set (s : finset α) : measurable_set (↑s : set α) :=
 s.finite_to_set.measurable_set
 
+lemma set.countable.measurable_set {s : set α} (hs : countable s) : measurable_set s :=
+begin
+  rw [← bUnion_of_singleton s],
+  exact measurable_set.bUnion hs (λ b hb, measurable_set_singleton b)
+end
+
 end measurable_singleton_class
 
 namespace measurable_space
@@ -556,6 +562,22 @@ end
   measurable_set (mul_support f) :=
 hf (measurable_set_singleton 1).compl
 
+/-- If a function coincides with a measurable function outside of a countable set, it is
+measurable. -/
+lemma measurable.measurable_of_countable_ne [measurable_singleton_class α]
+  {f g : α → β} (hf : measurable f) (h : countable {x | f x ≠ g x}) : measurable g :=
+begin
+  assume t ht,
+  have : g ⁻¹' t = (g ⁻¹' t ∩ {x | f x = g x}ᶜ) ∪ (g ⁻¹' t ∩ {x | f x = g x}),
+    by simp [← inter_union_distrib_left],
+  rw this,
+  apply measurable_set.union (h.mono (inter_subset_right _ _)).measurable_set,
+  have : g ⁻¹' t ∩ {x : α | f x = g x} = f ⁻¹' t ∩ {x : α | f x = g x},
+    by { ext x, simp {contextual := tt} },
+  rw this,
+  exact (hf ht).inter h.measurable_set.of_compl,
+end
+
 end measurable_functions
 
 section constructions

src/measure_theory/measure_space.lean

@@ -1731,18 +1731,27 @@ section no_atoms
 
 variables [has_no_atoms μ]
 
-lemma measure_countable (h : countable s) : μ s = 0 :=
+instance (s : set α) : has_no_atoms (μ.restrict s) :=
+begin
+  refine ⟨λ x, _⟩,
+  obtain ⟨t, hxt, ht1, ht2⟩ := exists_measurable_superset_of_null (measure_singleton x : μ {x} = 0),
+  apply measure_mono_null hxt,
+  rw measure.restrict_apply ht1,
+  apply measure_mono_null (inter_subset_left t s) ht2
+end
+
+lemma _root_.set.countable.measure_zero (h : countable s) : μ s = 0 :=
 begin
   rw [← bUnion_of_singleton s, ← nonpos_iff_eq_zero],
   refine le_trans (measure_bUnion_le h _) _,
   simp
 end
 
-lemma measure_finite (h : s.finite) : μ s = 0 :=
-measure_countable h.countable
+lemma _root_.set.finite.measure_zero (h : s.finite) : μ s = 0 :=
+h.countable.measure_zero
 
-lemma measure_finset (s : finset α) : μ ↑s = 0 :=
-measure_finite s.finite_to_set
+lemma _root_.finset.measure_zero (s : finset α) : μ ↑s = 0 :=
+s.finite_to_set.measure_zero
 
 lemma insert_ae_eq_self (a : α) (s : set α) :
   (insert a s : set α) =ᵐ[μ] s :=

src/set_theory/cardinal_ordinal.lean

@@ -222,6 +222,12 @@ theorem aleph'_is_normal : is_normal (ord ∘ aleph') :=
 theorem aleph_is_normal : is_normal (ord ∘ aleph) :=
 aleph'_is_normal.trans $ add_is_normal ordinal.omega
 
+lemma countable_iff_lt_aleph_one {α : Type*} (s : set α) : countable s ↔ #s < aleph 1 :=
+begin
+  have : aleph 1 = (aleph 0).succ, by simp only [← aleph_succ, ordinal.succ_zero],
+  rw [countable_iff, ← aleph_zero, this, lt_succ],
+end
+
 /-! ### Properties of `mul` -/
 
 /-- If `α` is an infinite type, then `α × α` and `α` have the same cardinality. -/

src/topology/continuous_function/bounded.lean

@@ -68,7 +68,7 @@ rfl
 /-- If a function is bounded on a discrete space, it is automatically continuous,
 and therefore gives rise to an element of the type of bounded continuous functions -/
 def mk_of_discrete [discrete_topology α] (f : α → β)
-  (C : ℝ) (h :  ∀ x y : α, dist (f x) (f y) ≤ C) : α →ᵇ β :=
+  (C : ℝ) (h : ∀ x y : α, dist (f x) (f y) ≤ C) : α →ᵇ β :=
 ⟨⟨f, continuous_of_discrete_topology⟩, ⟨C, h⟩⟩
 
 @[simp] lemma mk_of_discrete_apply
@@ -185,7 +185,7 @@ lemma const_apply (a : α) (b : β) : (const α b : α → β) a = b := rfl
 instance [inhabited β] : inhabited (α →ᵇ β) := ⟨const α (default β)⟩
 
 /-- The evaluation map is continuous, as a joint function of `u` and `x` -/
-theorem continuous_eval : continuous (λ p : (α →ᵇ β) × α, p.1 p.2) :=
+@[continuity] theorem continuous_eval : continuous (λ p : (α →ᵇ β) × α, p.1 p.2) :=
 continuous_iff'.2 $ λ ⟨f, x⟩ ε ε0,
 /- use the continuity of `f` to find a neighborhood of `x` where it varies at most by ε/2 -/
 have Hs : _ := continuous_iff'.1 f.continuous x (ε/2) (half_pos ε0),
@@ -196,7 +196,7 @@ mem_sets_of_superset (prod_mem_nhds_sets (ball_mem_nhds _ (half_pos ε0)) Hs) $
   ... = ε : add_halves _
 
 /-- In particular, when `x` is fixed, `f → f x` is continuous -/
-theorem continuous_evalx {x : α} : continuous (λ f : α →ᵇ β, f x) :=
+@[continuity] theorem continuous_evalx {x : α} : continuous (λ f : α →ᵇ β, f x) :=
 continuous_eval.comp (continuous_id.prod_mk continuous_const)
 
 /-- Bounded continuous functions taking values in a complete space form a complete space. -/
@@ -497,9 +497,14 @@ le_antisymm (norm_const_le b) $ h.elim $ λ x, (const α b).norm_coe_le_norm x
 /-- Constructing a bounded continuous function from a uniformly bounded continuous
 function taking values in a normed group. -/
 def of_normed_group {α : Type u} {β : Type v} [topological_space α] [normed_group β]
-  (f : α  → β) (Hf : continuous f) (C : ℝ) (H : ∀x, ∥f x∥ ≤ C) : α →ᵇ β :=
+  (f : α → β) (Hf : continuous f) (C : ℝ) (H : ∀x, ∥f x∥ ≤ C) : α →ᵇ β :=
 ⟨⟨λn, f n, Hf⟩, ⟨_, dist_le_two_norm' H⟩⟩
 
+@[simp] lemma coe_of_normed_group
+  {α : Type u} {β : Type v} [topological_space α] [normed_group β]
+  (f : α → β) (Hf : continuous f) (C : ℝ) (H : ∀x, ∥f x∥ ≤ C) :
+  (of_normed_group f Hf C H : α → β) = f := rfl
+
 lemma norm_of_normed_group_le {f : α → β} (hfc : continuous f) {C : ℝ} (hC : 0 ≤ C)
   (hfC : ∀ x, ∥f x∥ ≤ C) : ∥of_normed_group f hfc C hfC∥ ≤ C :=
 (norm_le hC).2 hfC
@@ -511,6 +516,11 @@ def of_normed_group_discrete {α : Type u} {β : Type v}
   (f : α  → β) (C : ℝ) (H : ∀x, norm (f x) ≤ C) : α →ᵇ β :=
 of_normed_group f continuous_of_discrete_topology C H
 
+@[simp] lemma coe_of_normed_group_discrete
+  {α : Type u} {β : Type v} [topological_space α] [discrete_topology α] [normed_group β]
+  (f : α → β) (C : ℝ) (H : ∀x, ∥f x∥ ≤ C) :
+  (of_normed_group_discrete f C H : α → β) = f := rfl
+
 /-- The pointwise sum of two bounded continuous functions is again bounded continuous. -/
 instance : has_add (α →ᵇ β) :=
 ⟨λf g, of_normed_group (f + g) (f.continuous.add g.continuous) (∥f∥ + ∥g∥) $ λ x,
@@ -618,6 +628,16 @@ module.of_core $
 instance : normed_space 𝕜 (α →ᵇ β) := ⟨λ c f, norm_of_normed_group_le _
   (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _⟩
 
+variables (𝕜)
+/-- The evaluation at a point, as a continuous linear map from `α →ᵇ β` to `β`. -/
+def eval_clm (x : α) : (α →ᵇ β) →L[𝕜] β :=
+{ to_fun := λ f, f x,
+  map_add' := λ f g, by simp only [pi.add_apply, coe_add],
+  map_smul' := λ c f, by simp only [coe_smul] }
+
+@[simp] lemma eval_clm_apply (x : α) (f : α →ᵇ β) :
+  eval_clm 𝕜 x f = f x := rfl
+
 variables (α β)
 
 /-- The linear map forgetting that a bounded continuous function is bounded. -/