# Documentation

Counterexamples.Phillips

# A counterexample on Pettis integrability #

There are several theories of integration for functions taking values in Banach spaces. Bochner integration, requiring approximation by simple functions, is the analogue of the one-dimensional theory. It is very well behaved, but only works for functions with second-countable range.

For functions f taking values in a larger Banach space B, one can define the Dunford integral as follows. Assume that, for all continuous linear functional φ, the function φ ∘ f is measurable (we say that f is weakly measurable, or scalarly measurable) and integrable. Then φ ↦ ∫ φ ∘ f is continuous (by the closed graph theorem), and therefore defines an element of the bidual B**. This is the Dunford integral of f.

This Dunford integral is not usable in practice as it does not belong to the right space. Let us say that a function is Pettis integrable if its Dunford integral belongs to the canonical image of B in B**. In this case, we define the Pettis integral as the Dunford integral inside B.

This integral is very general, but not really usable to do analysis. This file illustrates this, by giving an example of a function with nice properties but which is not Pettis-integrable. This function:

• is defined from [0, 1] to a complete Banach space;
• is weakly measurable;
• has norm everywhere bounded by 1 (in particular, its norm is integrable);
• and yet it is not Pettis-integrable with respect to Lebesgue measure.

This construction is due to [Ralph S. Phillips, Integration in a convex linear topological space][phillips1940], in Example 10.8. It requires the continuum hypothesis. The example is the following.

Under the continuum hypothesis, one can find a subset of ℝ² which, along each vertical line, only misses a countable set of points, while it is countable along each horizontal line. This is due to Sierpinski, and formalized in sierpinski_pathological_family. (In fact, Sierpinski proves that the existence of such a set is equivalent to the continuum hypothesis).

Let B be the set of all bounded functions on ℝ (we are really talking about everywhere defined functions here). Define f : ℝ → B by taking f x to be the characteristic function of the vertical slice at position x of Sierpinski's set. It is our counterexample.

To show that it is weakly measurable, we should consider φ ∘ f where φ is an arbitrary continuous linear form on B. There is no reasonable classification of such linear forms (they can be very wild). But if one restricts such a linear form to characteristic functions, one gets a finitely additive signed "measure". Such a "measure" can be decomposed into a discrete part (supported on a countable set) and a continuous part (giving zero mass to countable sets). For all but countably many points, f x will not intersect the discrete support of φ thanks to the definition of the Sierpinski set. This implies that φ ∘ f is constant outside of a countable set, and equal to the total mass of the continuous part of φ there. In particular, it is measurable (and its integral is the total mass of the continuous part of φ).

Assume that f has a Pettis integral g. For all continuous linear form φ, then φ g should be the total mass of the continuous part of φ. Taking for φ the evaluation at the point x (which has no continuous part), one gets g x = 0. Take then for φ the Lebesgue integral on [0, 1] (or rather an arbitrary extension of Lebesgue integration to all bounded functions, thanks to Hahn-Banach). Then φ g should be the total mass of the continuous part of φ, which is 1. This contradicts the fact that g = 0, and concludes the proof that f has no Pettis integral.

## Implementation notes #

The space of all bounded functions is defined as the space of all bounded continuous functions on a discrete copy of the original type, as mathlib only contains the space of all bounded continuous functions (which is the useful one).

A copy of a type, endowed with the discrete topology

Instances For

### Extending the integral #

Thanks to Hahn-Banach, one can define a (non-canonical) continuous linear functional on the space of all bounded functions, coinciding with the integral on the integrable ones.

The subspace of integrable functions in the space of all bounded functions on a type. This is a technical device, used to apply Hahn-Banach theorem to construct an extension of the integral to all bounded functions.

Instances For

The integral, as a continuous linear map on the subspace of integrable functions in the space of all bounded functions on a type. This is a technical device, that we will extend through Hahn-Banach.

Instances For
theorem Counterexample.Phillips1940.exists_linear_extension_to_boundedFunctions {α : Type u} [] (μ : ) :
φ, ∀ (f : ), φ f = ∫ (x : α), f xμ

Given a measure, there exists a continuous linear form on the space of all bounded functions (not necessarily measurable) that coincides with the integral on bounded measurable functions.

An arbitrary extension of the integral to all bounded functions, as a continuous linear map. It is not at all canonical, and constructed using Hahn-Banach.

Instances For
theorem Counterexample.Phillips1940.extensionToBoundedFunctions_apply {α : Type u} [] (μ : ) (hf : ) :
= ∫ (x : α), f xμ

### Additive measures on the space of all sets #

We define bounded finitely additive signed measures on the space of all subsets of a type α, and show that such an object can be split into a discrete part and a continuous part.

• toFun : Set α
• additive' : ∀ (s_1 t : Set α), Disjoint s_1 ts (s_1 t) = s s_1 + s t
• exists_bound : C, ∀ (s_1 : Set α), |s s_1| C

A bounded signed finitely additive measure defined on all subsets of a type.

Instances For

A constant bounding the mass of any set for f.

Instances For
theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.additive {α : Type u} (s : Set α) (t : Set α) (h : Disjoint s t) :
f (s t) = f s + f t
@[simp]

Restricting a bounded additive measure to a subset still gives a bounded additive measure.

Instances For
@[simp]
theorem Counterexample.Phillips1940.BoundedAdditiveMeasure.restrict_apply {α : Type u} (s : Set α) (t : Set α) :
= f (s t)

There is a maximal countable set of positive measure, in the sense that any countable set not intersecting it has nonpositive measure. Auxiliary lemma to prove exists_discrete_support.

A countable set outside of which the measure gives zero mass to countable sets. We are not claiming this set is unique, but we make an arbitrary choice of such a set.

Instances For

The discrete part of a bounded additive measure, obtained by restricting the measure to its countable support.

Instances For

The continuous part of a bounded additive measure, giving zero measure to every countable set.

Instances For

### Relationship between continuous functionals and finitely additive measures. #

A functional in the dual space of bounded functions gives rise to a bounded additive measure, by applying the functional to the indicator functions.

Instances For
@[simp]
theorem Counterexample.Phillips1940.continuousPart_evalClm_eq_zero {α : Type u} [] [] (s : Set α) (x : α) :
theorem Counterexample.Phillips1940.toFunctions_toMeasure {α : Type u} [] (μ : ) (s : Set α) (hs : ) :

### A set in ℝ² large along verticals, small along horizontals #

We construct a subset of ℝ², given as a family of sets, which is large along verticals (i.e., it only misses a countable set along each vertical) but small along horizontals (it is countable along horizontals). Such a set can not be measurable as it would contradict Fubini theorem. We need the continuum hypothesis to construct it.

theorem Counterexample.Phillips1940.sierpinski_pathological_family (Hcont : ) :
f, (∀ (x : ), Set.Countable (Set.univ \ f x)) ∀ (y : ), Set.Countable {x | y f x}
def Counterexample.Phillips1940.spf (Hcont : ) (x : ) :

A family of sets in ℝ which only miss countably many points, but such that any point is contained in only countably many of them.

Instances For

### A counterexample for the Pettis integral #

We construct a function f from [0,1] to a complete Banach space B, which is weakly measurable (i.e., for any continuous linear form φ on B the function φ ∘ f is measurable), bounded in norm (i.e., for all x, one has ‖f x‖ ≤ 1), and still f has no Pettis integral.

This construction, due to Phillips, requires the continuum hypothesis. We will take for B the space of all bounded functions on ℝ, with the supremum norm (no measure here, we are really talking of everywhere defined functions). And f x will be the characteristic function of a set which is large (it has countable complement), as in the Sierpinski pathological family.

def Counterexample.Phillips1940.f (Hcont : ) (x : ) :

A family of bounded functions f_x from ℝ (seen with the discrete topology) to ℝ (in fact taking values in {0, 1}), indexed by a real parameter x, corresponding to the characteristic functions of the different fibers of the Sierpinski pathological family

Instances For
theorem Counterexample.Phillips1940.countable_ne (Hcont : ) :
Set.Countable {x | ↑() Set.univ φ ()}
theorem Counterexample.Phillips1940.comp_ae_eq_const (Hcont : ) :
∀ᵐ (x : ) ∂MeasureTheory.Measure.restrict MeasureTheory.volume (Set.Icc 0 1), = φ ()
theorem Counterexample.Phillips1940.integral_comp (Hcont : ) :
∫ (x : ) in Set.Icc 0 1, φ () =

The next few statements show that the function f Hcont : ℝ → (DiscreteCopy ℝ →ᵇ ℝ) takes its values in a complete space, is scalarly measurable, is everywhere bounded by 1, and still has no Pettis integral.

theorem Counterexample.Phillips1940.measurable_comp (Hcont : ) :
Measurable fun x => φ ()

The function f Hcont : ℝ → (DiscreteCopy ℝ →ᵇ ℝ) is scalarly measurable.

The function f Hcont : ℝ → (DiscreteCopy ℝ →ᵇ ℝ) is uniformly bounded by 1 in norm.

theorem Counterexample.Phillips1940.no_pettis_integral (Hcont : ) :
¬g, ∀ (φ : ), ∫ (x : ) in Set.Icc 0 1, φ () = φ g

The function f Hcont : ℝ → (DiscreteCopy ℝ →ᵇ ℝ) has no Pettis integral.