From binary products to finitary products

Stream: general

[Floris van Doorn]

I have defined binary product measures and now I want to define finitary product measures. The idea of course is just to iterate the binary product measure, but this is easier said than done. Eventually I want a result about Π i : ι, α i where ι is a fintype, and in that formulation there are no binary products in sight.

I have an approach that will (almost certainly) work, but isn't that pretty, and I was wondering if I'm doing things in a way that is too complicated. Any ideas/simplifications are welcome.

My idea is to define a new product of types as

/-- The product of a family of types over a list. -/
def tprod (α : ι → Type*) (l : list ι) : Type* :=
l.foldr (λ i β, α i × β) punit

Whatever result I have for binary products is easily extendible to tprod by induction on l.
Now translating this to Π i : ι, α i is a little tricky. I think I want this lemma: (eventually I also want a measurable_equiv)

lemma pi_fintype_equiv_foldl_prod [fintype ι] :
  ∃ l : list ι, nodup l ∧ nonempty ((Π i, α i) ≃ l.tprod α)

That lemma is a little tricky to prove by induction, but this will work:

def pi_finset_equiv_foldl_prod {s : finset ι} {l : list ι} (h : l.to_finset = s)
  (h : l.nodup) : (Π i ∈ s, α i) ≃ l.tprod α

However, this requires me to work with the type Π i ∈ s, α i, and as part of the proofs I have to rewrite inside i ∈ s a couple of times. However, Lean doesn't really like that: simp refuses to rewrite in i ∈ s (presumably because it's part of the type i ∈ s → α i) and rw refuses because the bound variable i occurs. This means I needed to use this lemma:

lemma pi_congr {α β : ι → Type*} (h : ∀ i, α i = β i) : (Π i, α i) = (Π i, β i)

This lemma raises many alarm bells: I'm talking about equality between types.
I'm sure that this proof will work, but I'm wondering if there is a much nicer way of doing this.

[Heather Macbeth]

A naive question -- is there any way to get the finitary product measure "all at once" rather than by iterating the binary one?

[Adam Topaz]

I think there is this? docs#category_theory.limits.has_finite_products_of_has_binary_products

[Adam Topaz]

Maybe not...

[Heather Macbeth]

@Adam Topaz catehory

[Adam Topaz]

Still no :frown:

[Frédéric Dupuis]

I don't really have an answer, but I'm working on a very similar issue (with tensor products rather than product measures) here: #5311. Right now I'm just basically duplicating the binary tensor product code but a trick like this would be nice. It's not clear how much one gets for free this way though, it seems like most of the API still has to get written anyway, and copy/pasting proofs can be a lot faster to write even if it's more lines of code in the end.

[Heather Macbeth]

Frédéric Dupuis said:

Right now I'm just basically duplicating the binary tensor product code but a trick like this would be nice. It's not clear how much one gets for free this way though, it seems like most of the API still has to get written anyway, and copy/pasting proofs can be a lot faster to write even if it's more lines of code in the end.

Would it be easier to get a "trick" going the other way, from a general finitary version to a binary version?

[Adam Topaz]

But the category theory limits are not explicit, so it might not be useful in this context anyway...

[Frédéric Dupuis]

Sounds much easier that way, going from Π i : (fin 2), β i to the binary version should be pretty simple.

[Floris van Doorn]

Heather Macbeth said:

A naive question -- is there any way to get the finitary product measure "all at once" rather than by iterating the binary one?

I don't know, but I have looked at a couple of books, and they all just say "iterate the binary product".
It would be pretty tricky, since the binary product of measures is defined as a unary integral. The n-ary product would be something like an n-1-ary integral, which sounds pretty hairy.

[Frédéric Dupuis]

The issue with the iterated binary product is that there is an inherent order in which the product is taken, which (at least in the case I'm working on) is not desirable in the final product. And it doesn't seem easy to get rid of.

[Floris van Doorn]

Oh, wait, my previous message was misleading. I define the finitary product measure directly:

/-- `measure.pi μ` is the finite product of the measures `{μ i | i : ι}`.
  It is defined to be the maximal product measure, i.e.
  the maximal measure `ν` with the property that `ν (pi univ s) ≤ ∏ i, μ i (s i)`,
  where `pi univ s` is the product of the sets `{ s i | i : ι }`. -/
protected def pi : measure (Π i, α i) :=
[...]

However, now I need to show that ν (pi univ s) = ∏ i, μ i (s i). To show this, I need to know that there is some measure that has this property. And for this I want to use iterated binary products. So I only use a specific order in which the product is taken to prove some properties, not to define anything.

[Bhavik Mehta]

Adam Topaz said:

I think there is this? docs#category_theory.limits.has_finite_products_of_has_binary_products

there's nothing of this form in mathlib (yet) for categories, i'm planning to pr it fairly soon though

[Mario Carneiro]

I think the definition of list.pmap is relevant to these considerations. Something similar comes up when lifting that to quotients in multiset.pmap

[Mario Carneiro]

import data.fintype.basic

variables {ι : Type*}

namespace list
def tprod (α : ι → Type*) (l : list ι) : Type* :=
l.foldr (λ i β, α i × β) punit

end list

variables (α : ι → Type*)

def pi_list_equiv_foldl_prod [decidable_eq ι] :
  ∀ {l : list ι} (h : l.nodup), (Π i : {i//i∈l}, α i) ≃ l.tprod α
| [] _ := begin
    refine @equiv_of_unique_of_unique _ _ ⟨⟨_⟩, _⟩ punit.unique,
    exact λ x, x.2.elim,
    intro, funext x, exact x.2.elim,
  end
| (a :: l) h := begin
    have := list.nodup_cons.1 h,
    refine equiv.trans _ (equiv.prod_congr_right (λ _, pi_list_equiv_foldl_prod this.2)),
    refine ⟨
      λ f, (f ⟨a, or.inl rfl⟩, λ b, f ⟨b.1, or.inr b.2⟩),
      λ g x, if h : ↑x = a then by rw h; exact g.1
        else g.2 ⟨x.1, x.2.resolve_left h⟩,
      _, _⟩,
    { intro f, ext ⟨x, h⟩, simp, split_ifs,
      { subst h_1, refl },
      { refl } },
    { rintro ⟨v, g⟩, ext, {simp, refl},
      cases x with x hx,
      simp, rw [dif_neg (_ : x ≠ a)], {refl},
      rintro rfl, exact this.1 hx },
  end

lemma pi_fintype_equiv_foldl_prod [fintype ι] :
  ∃ l : list ι, list.nodup l ∧ nonempty ((Π i, α i) ≃ l.tprod α) :=
begin
  classical,
  obtain ⟨l, nd, al⟩ := fintype.exists_univ_list ι,
  exact ⟨l, nd, ⟨
    (equiv.Pi_congr_left α (equiv.subtype_univ_equiv al)).symm.trans
    (pi_list_equiv_foldl_prod α nd)⟩⟩,
end

[Floris van Doorn]

Hmm... Using Π i : {i//i∈l}, α iis probably a more convenient than Π i ∈ s, α i. Good idea

Thanks for the definition. I also defined it myself. I also need to prove additional properties about the forward and backward functions, so I split it up into separate definitions a bit more :)

[Yury G. Kudryashov]

You can also do induction on the cardinality of the index type, see src#continuous_equiv_fun_basis for an example.