Finite products of types

This file defines the product of types over a list. For l : List ι and α : ι → Type v we define List.TProd α l = l.foldr (fun i β ↦ α i × β) PUnit. This type should not be used if ∀ i, α i or ∀ i ∈ l, α i can be used instead (in the last expression, we could also replace the list l by a set or a finset). This type is used as an intermediary between binary products and finitary products. The application of this type is finitary product measures, but it could be used in any construction/theorem that is easier to define/prove on binary products than on finitary products.

• Once we have the construction on binary products (like binary product measures in MeasureTheory.prod), we can easily define a finitary version on the type TProd l α by iterating. Properties can also be easily extended from the binary case to the finitary case by iterating.
• Then we can use the equivalence List.TProd.piEquivTProd below (or enhanced versions of it, like a MeasurableEquiv for product measures) to get the construction on ∀ i : ι, α i, at least when assuming [Fintype ι] [Encodable ι] (using Encodable.sortedUniv). Using attribute [local instance] Fintype.toEncodable we can get rid of the argument [Encodable ι].

Main definitions

• We have the equivalence TProd.piEquivTProd : (∀ i, α i) ≃ TProd α l if l contains every element of ι exactly once.
• The product of sets is Set.tprod : (∀ i, Set (α i)) → Set (TProd α l).

@[reducible, inline]

abbrev List.TProd {ι : Type u} (α : ι → Type v) (l : List ι) : Type v

The product of a family of types over a list.

Equations

• List.TProd α l = List.foldr (fun (i : ι) (β : Type ?u.23) => α i × β) PUnit.{?u.23 + 1} l

def List.TProd.mk {ι : Type u} {α : ι → Type v} (l : List ι) (_f : (i : ι) → α i) : List.TProd α l

Turning a function f : ∀ i, α i into an element of the iterated product TProd α l.

Equations

• List.TProd.mk [] = fun (x : (i : ι) → α i) => PUnit.unit
• List.TProd.mk (i :: is) = fun (f : (i : ι) → α i) => (f i, List.TProd.mk is f)

instance List.TProd.instInhabited {ι : Type u} {α : ι → Type v} {l : List ι} [(i : ι) → Inhabited (α i)] : Inhabited (List.TProd α l)

Equations

• List.TProd.instInhabited = { default := List.TProd.mk l default }

@[simp]

theorem List.TProd.fst_mk {ι : Type u} {α : ι → Type v} (i : ι) (l : List ι) (f : (i : ι) → α i) : (List.TProd.mk (i :: l) f).1 = f i

@[simp]

theorem List.TProd.snd_mk {ι : Type u} {α : ι → Type v} (i : ι) (l : List ι) (f : (i : ι) → α i) : (List.TProd.mk (i :: l) f).2 = List.TProd.mk l f

def List.TProd.elim {ι : Type u} {α : ι → Type v} [DecidableEq ι] {l : List ι} : List.TProd α l → {i : ι} → i ∈ l → α i

Given an element of the iterated product l.Prod α, take a projection into direction i. If i appears multiple times in l, this chooses the first component in direction i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem List.TProd.elim_self {ι : Type u} {α : ι → Type v} {i : ι} {l : List ι} [DecidableEq ι] (v : List.TProd α (i :: l)) : v.elim ⋯ = v.1

@[simp]

theorem List.TProd.elim_of_ne {ι : Type u} {α : ι → Type v} {i : ι} {j : ι} {l : List ι} [DecidableEq ι] (hj : j ∈ i :: l) (hji : j ≠ i) (v : List.TProd α (i :: l)) : v.elim hj = List.TProd.elim v.2 ⋯

@[simp]

theorem List.TProd.elim_of_mem {ι : Type u} {α : ι → Type v} {i : ι} {j : ι} {l : List ι} [DecidableEq ι] (hl : (i :: l).Nodup) (hj : j ∈ l) (v : List.TProd α (i :: l)) : v.elim ⋯ = List.TProd.elim v.2 hj

theorem List.TProd.elim_mk {ι : Type u} {α : ι → Type v} [DecidableEq ι] (l : List ι) (f : (i : ι) → α i) {i : ι} (hi : i ∈ l) : (List.TProd.mk l f).elim hi = f i

theorem List.TProd.ext_iff {ι : Type u} {α : ι → Type v} [DecidableEq ι] {l : List ι} : ∀ {x : l.Nodup} {v w : List.TProd α l}, v = w ↔ ∀ (i : ι) (hi : i ∈ l), v.elim hi = w.elim hi

theorem List.TProd.ext {ι : Type u} {α : ι → Type v} [DecidableEq ι] {l : List ι} : l.Nodup → ∀ {v w : List.TProd α l}, (∀ (i : ι) (hi : i ∈ l), v.elim hi = w.elim hi) → v = w

def List.TProd.elim' {ι : Type u} {α : ι → Type v} {l : List ι} [DecidableEq ι] (h : ∀ (i : ι), i ∈ l) (v : List.TProd α l) (i : ι) : α i

A version of TProd.elim when l contains all elements. In this case we get a function into Π i, α i.

Equations

• List.TProd.elim' h v i = v.elim ⋯

theorem List.TProd.mk_elim {ι : Type u} {α : ι → Type v} {l : List ι} [DecidableEq ι] (hnd : l.Nodup) (h : ∀ (i : ι), i ∈ l) (v : List.TProd α l) : List.TProd.mk l (List.TProd.elim' h v) = v

def List.TProd.piEquivTProd {ι : Type u} {α : ι → Type v} {l : List ι} [DecidableEq ι] (hnd : l.Nodup) (h : ∀ (i : ι), i ∈ l) : ((i : ι) → α i) ≃ List.TProd α l

Pi-types are equivalent to iterated products.

Equations

• List.TProd.piEquivTProd hnd h = { toFun := List.TProd.mk l, invFun := List.TProd.elim' h, left_inv := ⋯, right_inv := ⋯ }

def Set.tprod {ι : Type u} {α : ι → Type v} (l : List ι) (_t : (i : ι) → Set (α i)) : Set (List.TProd α l)

A product of sets in TProd α l.

Equations

• Set.tprod [] x = Set.univ
• Set.tprod (i :: is) x = x i ×ˢ Set.tprod is x

theorem Set.mk_preimage_tprod {ι : Type u} {α : ι → Type v} (l : List ι) (t : (i : ι) → Set (α i)) : List.TProd.mk l ⁻¹' Set.tprod l t = {i : ι | i ∈ l}.pi t

theorem Set.elim_preimage_pi {ι : Type u} {α : ι → Type v} [DecidableEq ι] {l : List ι} (hnd : l.Nodup) (h : ∀ (i : ι), i ∈ l) (t : (i : ι) → Set (α i)) : List.TProd.elim' h ⁻¹' Set.univ.pi t = Set.tprod l t