Measures on lists

Lists carry the discrete σ-algebra, so every function out of a list type is measurable and, over a countable type, every measure on lists is s-finite. Measure.listProd is the law of a list of independent draws, one from each measure in a list of measures: the List-indexed product measure, built from the binary product.

The prefix sets {y | x <+: y} of a measure on lists are counted two ways. The lists of length at least n are partitioned by their prefix of length n, and a list has one prefix more than its length, so the total measure of the prefix sets is the integral of the length plus one.

Main definitions

• MeasureTheory.Measure.listProd: the product of a list of measures.

Main results

• MeasureTheory.Measure.listProd_cons_singleton_cons: the product measure of a singleton list is the product of the singleton measures.
• MeasureTheory.Measure.ωScottContinuous_listProd: the product is ω-Scott-continuous in each factor.
• MeasureTheory.Measure.tsum_measure_setOf_prefix_length, MeasureTheory.Measure.tsum_measure_setOf_prefix: the prefix sets counted by length, and in total.

Implementation notes

The discrete σ-algebra is the only reasonable choice on lists over a countable discrete type, which is the case of interest for derivation trees and branching processes; it is registered globally here as the library's convention.

@[instance_reducible]

instance instMeasurableSpaceList_linglib {α : Type u_1} : MeasurableSpace (List α)

Equations

• instMeasurableSpaceList_linglib = ⊤

Prefix sets

theorem MeasureTheory.Measure.tsum_measure_setOf_prefix_length {α : Type u_1} [Countable α] (μ : Measure (List α)) (n : ℕ) : ∑' (x : { x : List α // x.length = n }), μ {y : List α | ↑x <+: y} = μ {y : List α | n ≤ y.length}

The lists of length at least n are partitioned by their prefix of length n.

theorem MeasureTheory.Measure.tsum_measure_setOf_prefix {α : Type u_1} [Countable α] (μ : Measure (List α)) : ∑' (x : List α), μ {y : List α | x <+: y} = ∫⁻ (y : List α), ↑y.length + 1 ∂μ

The total measure of the prefix sets is the integral of the number of prefixes, the length plus one.

Products of lists of measures

noncomputable def MeasureTheory.Measure.listProd {α : Type u_1} [MeasurableSpace α] : List (Measure α) → Measure (List α)

The law of a list of independent draws, one from each measure in the list.

Equations

• MeasureTheory.Measure.listProd [] = MeasureTheory.Measure.dirac []
• MeasureTheory.Measure.listProd (μ :: μs) = MeasureTheory.Measure.map (Function.uncurry List.cons) (μ.prod (MeasureTheory.Measure.listProd μs))

@[simp]

theorem MeasureTheory.Measure.listProd_nil {α : Type u_1} [MeasurableSpace α] : listProd [] = dirac []

theorem MeasureTheory.Measure.listProd_cons {α : Type u_1} [MeasurableSpace α] (μ : Measure α) (μs : List (Measure α)) : listProd (μ :: μs) = map (Function.uncurry List.cons) (μ.prod (listProd μs))

@[simp]

theorem MeasureTheory.Measure.listProd_nil_singleton_cons {α : Type u_1} [MeasurableSpace α] (x : α) (xs : List α) : (listProd []) {x :: xs} = 0

theorem MeasureTheory.Measure.isProbabilityMeasure_listProd {α : Type u_1} [MeasurableSpace α] {μs : List (Measure α)} (h : ∀ μ ∈ μs, IsProbabilityMeasure μ) : IsProbabilityMeasure (listProd μs)

theorem MeasureTheory.Measure.listProd_univ_le_one {α : Type u_1} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μs : List (Measure α)} (h : ∀ μ ∈ μs, μ Set.univ ≤ 1) : (listProd μs) Set.univ ≤ 1

@[simp]

theorem MeasureTheory.Measure.listProd_cons_singleton_nil {α : Type u_1} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] (μ : Measure α) (μs : List (Measure α)) : (listProd (μ :: μs)) {[]} = 0

@[simp]

theorem MeasureTheory.Measure.listProd_cons_singleton_cons {α : Type u_1} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] (μ : Measure α) (μs : List (Measure α)) (x : α) (xs : List α) : (listProd (μ :: μs)) {x :: xs} = μ {x} * (listProd μs) {xs}

theorem MeasureTheory.Measure.ωScottContinuous_listProd {α : Type u_1} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {γ : Type u_2} [OmegaCompletePartialOrder γ] {ι : Type u_3} {F : ι → γ → Measure α} {l : List ι} (hF : ∀ i ∈ l, OmegaCompletePartialOrder.ωScottContinuous (F i)) : OmegaCompletePartialOrder.ωScottContinuous fun (x : γ) => listProd (List.map (fun (i : ι) => F i x) l)