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 (λ 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.piEquivTProdbelow (or enhanced versions of it, like a
MeasurableEquivfor product measures) to get the construction on
∀ i : ι, α i, at least when assuming
[Fintype ι] [Encodable ι](using
local attribute [instance] Fintype.toEncodablewe can get rid of the argument
Main definitions #
Turning a function
f : ∀ i, α i into an element of the iterated product
TProd α l.
Given an element of the iterated product
l.Prod α, take a projection into direction
i appears multiple times in
l, this chooses the first component in direction