Lists over Quasi-Borel Spaces

This file defines the quasi-borel structure on lists and proves various operations on lists are homomorphisms.

Main definitions

• QuasiBorelSpace (List A): the quasi-borel structure on lists
• sequence: converts a list of probability measures into a measure over lists

Main results

• Basic list operations (cons, tail, append, map, etc.) are homomorphisms
• List query operations (mem, elem, length, get, etc.) are homomorphisms
• Set-like operations (insert, union, erase, diff) are homomorphisms

Encoding Homomorphisms

theorem List.Encoding.isHom_cons {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace.IsHom fun (x : A × Encoding A) => cons x.1 x.2

cons is a homomorphism.

theorem List.Encoding.isHom_fold {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {cons : A → B → B} (hcons : QuasiBorelSpace.IsHom fun (x : A × B) => match x with | (x, y) => cons x y) (nil : B) : QuasiBorelSpace.IsHom (foldr cons nil)

Folding over an encoded list is a homomorphism.

QuasiBorel Structure

instance QuasiBorelSpace.List.instList {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace (List A)

The QuasiBorelSpace structure on List A.

Equations

• QuasiBorelSpace.List.instList = QuasiBorelSpace.lift List.Encoding.encode

@[simp]

theorem QuasiBorelSpace.List.isHom_encode {A : Type u_1} [QuasiBorelSpace A] : IsHom List.Encoding.encode

encode is a homomorphism.

@[simp]

theorem QuasiBorelSpace.List.isHom_cons {A : Type u_1} [QuasiBorelSpace A] : IsHom fun (x : A × List A) => x.1 :: x.2

List cons is a homomorphism.

theorem QuasiBorelSpace.List.isHom_cons' {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} (hf : IsHom f) {g : A → List B} (hg : IsHom g) : IsHom fun (x : A) => f x :: g x

cons is a homomorphism when composed with other homomorphisms.

Basic List Operations

theorem QuasiBorelSpace.List.isHom_foldr {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {cons : A → B → B} (hcons : IsHom fun (x : A × B) => match x with | (x, xs) => cons x xs) (nil : B) : IsHom (List.foldr cons nil)

foldr is a homomorphism.

theorem QuasiBorelSpace.List.isHom_foldr' {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {cons : A → B → C → C} (hcons : IsHom fun (x : A × B × C) => match x with | (x, y, z) => cons x y z) {nil : A → C} (hnil : IsHom nil) {f : A → List B} (hf : IsHom f) : IsHom fun (x : A) => List.foldr (cons x) (nil x) (f x)

foldr is a homomorphism when composed with other homomorphisms.

theorem QuasiBorelSpace.List.isHom_map {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : A → B → C} (hf : IsHom fun (x : A × B) => match x with | (x, y) => f x y) {g : A → List B} (hg : IsHom g) : IsHom fun (x : A) => List.map (f x) (g x)

map is a homomorphism.

List Queries

theorem QuasiBorelSpace.List.isHom_getElem? {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → List B} (hf : IsHom f) {g : A → ℕ} (hg : IsHom g) : IsHom fun (x : A) => (f x)[g x]?

getElem? is a homomorphism.

theorem QuasiBorelSpace.List.isHom_length {A : Type u_1} [QuasiBorelSpace A] : IsHom List.length

length is a homomorphism.

theorem QuasiBorelSpace.List.isHom_get {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → List B} (hf : IsHom f) {g : A → ℕ} (hg : IsHom g) (h : ∀ (x : A), g x < (f x).length) : IsHom fun (x : A) => (f x)[g x]

get is a homomorphism for valid indices.

theorem QuasiBorelSpace.List.isHom_ofFn {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {n : ℕ} {f : A → Fin n → B} (hf : IsHom fun (x : A × Fin n) => match x with | (x, y) => f x y) : IsHom fun (x : A) => List.ofFn (f x)

ofFn is a homomorphism.

theorem QuasiBorelSpace.List.isHom_tail {A : Type u_1} [QuasiBorelSpace A] : IsHom List.tail

tail is a homomorphism.

theorem QuasiBorelSpace.List.isHom_append {A : Type u_1} [QuasiBorelSpace A] : IsHom fun (x : List A × List A) => x.1 ++ x.2

List append is a homomorphism.

List Membership and Set Operations

theorem QuasiBorelSpace.List.isHom_mem {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] [IsHomDiagonal B] {f : A → B} (hf : IsHom f) {g : A → List B} (hg : IsHom g) : IsHom fun (x : A) => f x ∈ g x

List membership is a homomorphism.

theorem QuasiBorelSpace.List.isHom_elem {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] [DecidableEq B] [IsHomDiagonal B] {f : A → B} (hf : IsHom f) {g : A → List B} (hg : IsHom g) : IsHom fun (x : A) => List.elem (f x) (g x)

elem is a homomorphism.

@[simp]

theorem QuasiBorelSpace.List.isHom_insert {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] [DecidableEq B] [IsHomDiagonal B] {f : A → B} (hf : IsHom f) {g : A → List B} (hg : IsHom g) : IsHom fun (x : A) => insert (f x) (g x)

insert is a homomorphism.

theorem QuasiBorelSpace.List.isHom_union {A : Type u_1} [QuasiBorelSpace A] [DecidableEq A] [IsHomDiagonal A] : IsHom fun (x : List A × List A) => x.1.union x.2

List union is a homomorphism.

theorem QuasiBorelSpace.List.isHom_erase {A : Type u_1} [QuasiBorelSpace A] [BEq A] [LawfulBEq A] [IsHomDiagonal A] : IsHom fun (x : List A × A) => x.1.erase x.2

erase is a homomorphism.

theorem QuasiBorelSpace.List.isHom_diff {A : Type u_1} [QuasiBorelSpace A] [BEq A] [LawfulBEq A] [IsHomDiagonal A] : IsHom fun (x : List A × List A) => x.1.diff x.2

List diff is a homomorphism.

Measurable Structure

instance QuasiBorelSpace.List.instMeasurableQuasiBorelSpaceList {A : Type u_1} [QuasiBorelSpace A] [MeasurableSpace A] [MeasurableQuasiBorelSpace A] : MeasurableQuasiBorelSpace (List A)

The MeasurableQuasiBorelSpace instance for List A.

Probability Measures on Lists

noncomputable def QuasiBorelSpace.List.sequence {A : Type u_1} [QuasiBorelSpace A] : List (ProbabilityMeasure A) → ProbabilityMeasure (List A)

Converts a sequence of measures into a measure of sequences, where each element is drawn from an element of the original sequence.

Equations

• One or more equations did not get rendered due to their size.
• QuasiBorelSpace.List.sequence [] = QuasiBorelSpace.ProbabilityMeasure.unit []

noncomputable def QuasiBorelSpace.List.lintegral {A : Type u_1} [QuasiBorelSpace A] (k : List A → ENNReal) : List (ProbabilityMeasure A) → ENNReal

Lifting integration to sequences.

Equations

• QuasiBorelSpace.List.lintegral k [] = k []
• QuasiBorelSpace.List.lintegral k (μ :: μs) = QuasiBorelSpace.ProbabilityMeasure.lintegral (fun (x : A) => QuasiBorelSpace.List.lintegral (fun (xs : List A) => k (x :: xs)) μs) μ

@[simp]

theorem QuasiBorelSpace.List.lintegral_sequence {A : Type u_1} [QuasiBorelSpace A] (μs : List (ProbabilityMeasure A)) (k : List A → ENNReal) (hk : IsHom k) : ProbabilityMeasure.lintegral k (sequence μs) = lintegral k μs

Computing the integral of a sequence.

Point Separation

instance QuasiBorelSpace.List.instSeparatesPointsList {A : Type u_1} [QuasiBorelSpace A] [SeparatesPoints A] : SeparatesPoints (List A)

The SeparatesPoints instance for List A.