The measurable structure on lists

Mathlib equips no type of lists with a measurable structure. This file gives List α the structure transported from its length-indexed representation Σ n, Fin n → α. Thus each fixed-length stratum has the finite product structure, and the list space is their countable disjoint union.

When α is countable with measurable singletons, this structure is discrete. In particular, a process whose values are finite words over a countable alphabet, such as the excursion process of a path, has a countable discrete value space.

Main definitions

• TauCeti.instMeasurableSpaceList: the measurable structure on List α induced by its length-indexed representation.
• TauCeti.instDiscreteMeasurableSpaceList: discreteness when α is countable with measurable singletons.

@[instance_reducible]

instance TauCeti.instMeasurableSpaceList {α : Type u_1} [MeasurableSpace α] : MeasurableSpace (List α)

The measurable structure on lists induced through List.equivSigmaTuple : List α ≃ Σ n, Fin n → α.

Equations

• TauCeti.instMeasurableSpaceList = MeasurableSpace.comap (⇑List.equivSigmaTuple) inferInstance

instance TauCeti.instDiscreteMeasurableSpaceList {α : Type u_1} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] : DiscreteMeasurableSpace (List α)

Lists over a countable measurable space with measurable singletons form a discrete measurable space.