Independent products of sub-distributions

prod d₁ d₂ is the distribution of an independent pair: sample d₁, sample d₂, return both. piFin ds is the finite indexed product — one independent draw per index of Fin n, returned as a function.

Main definitions

• prod d₁ d₂ — the independent product of two sub-distributions
• piFin ds — the independent product of a Fin n-indexed family
• replicateFin n d — piFin of the constant family, n independent draws from one sub-distribution

Main results

• mass_bind_of_mass_one — a bind of total distributions is total
• mass_prod, mass_piFin, mass_replicateFin — a product of total distributions is total
• prod_bind_fst, prod_bind_snd — the two marginals of a product, when the discarded factor is total

Correspondence with EasyCrypt

prod is the image of EasyCrypt's (`*`) of the Distr theory, whose definition dprod_dlet gives as dlet da (fun a => dmap db (fun b => (a, b))) — the bind form prod is defined by.

Mass of a bind

theorem CatCrypt.NonUniform.mass_bind_of_mass_one {α : Type u_1} {β : Type u_2} {d : Prob.SDistr α} {f : α → Prob.SDistr β} (hd : d.mass = 1) (hf : ∀ (a : α), (f a).mass = 1) : (d.bind f).mass = 1

Bind of total distributions is total. Obtained from Unary.lossless_bind through sampleFrom, whose mass is the mass of its distribution.

The binary product

noncomputable def CatCrypt.NonUniform.prod {α : Type u_1} {β : Type u_2} (d₁ : Prob.SDistr α) (d₂ : Prob.SDistr β) : Prob.SDistr (α × β)

The independent product of two sub-distributions: a pair whose components are drawn from d₁ and d₂.

Equations

• CatCrypt.NonUniform.prod d₁ d₂ = d₁.bind fun (a : α) => d₂.bind fun (b : β) => CatCrypt.Prob.SDistr.pure (a, b)

theorem CatCrypt.NonUniform.prod_eq_bind {α : Type u_1} {β : Type u_2} (d₁ : Prob.SDistr α) (d₂ : Prob.SDistr β) : prod d₁ d₂ = d₁.bind fun (a : α) => d₂.bind fun (b : β) => Prob.SDistr.pure (a, b)

The product is the two binds its definition is.

theorem CatCrypt.NonUniform.mass_prod {α : Type u_1} {β : Type u_2} {d₁ : Prob.SDistr α} {d₂ : Prob.SDistr β} (h₁ : d₁.mass = 1) (h₂ : d₂.mass = 1) : (prod d₁ d₂).mass = 1

A product of total distributions is total.

theorem CatCrypt.NonUniform.prod_bind_fst {α : Type u_1} {β : Type u_2} {d₁ : Prob.SDistr α} {d₂ : Prob.SDistr β} (h₂ : d₂.mass = 1) : ((prod d₁ d₂).bind fun (p : α × β) => Prob.SDistr.pure p.1) = d₁

The first marginal of a product is the first factor, when the second factor is total.

theorem CatCrypt.NonUniform.prod_bind_snd {α : Type u_1} {β : Type u_2} {d₁ : Prob.SDistr α} {d₂ : Prob.SDistr β} (h₁ : d₁.mass = 1) : ((prod d₁ d₂).bind fun (p : α × β) => Prob.SDistr.pure p.2) = d₂

The second marginal of a product is the second factor, when the first factor is total.

The finite indexed product

noncomputable def CatCrypt.NonUniform.piFin {α : Type u_1} {n : ℕ} : (Fin n → Prob.SDistr α) → Prob.SDistr (Fin n → α)

The independent product of a Fin n-indexed family: one draw per index, returned as a function.

Equations

• CatCrypt.NonUniform.piFin x_2 = CatCrypt.Prob.SDistr.pure fun (i : Fin 0) => i.elim0
• CatCrypt.NonUniform.piFin ds = (ds 0).bind fun (a : α) => (CatCrypt.NonUniform.piFin fun (i : Fin n) => ds i.succ).bind fun (f : Fin n → α) => CatCrypt.Prob.SDistr.pure (Fin.cons a f)

@[simp]

theorem CatCrypt.NonUniform.piFin_zero {α : Type u_1} (ds : Fin 0 → Prob.SDistr α) : piFin ds = Prob.SDistr.pure fun (i : Fin 0) => i.elim0

@[simp]

theorem CatCrypt.NonUniform.piFin_succ {α : Type u_1} {n : ℕ} (ds : Fin (n + 1) → Prob.SDistr α) : piFin ds = (ds 0).bind fun (a : α) => (piFin fun (i : Fin n) => ds i.succ).bind fun (f : Fin n → α) => Prob.SDistr.pure (Fin.cons a f)

theorem CatCrypt.NonUniform.mass_piFin {α : Type u_1} {n : ℕ} {ds : Fin n → Prob.SDistr α} : (∀ (i : Fin n), (ds i).mass = 1) → (piFin ds).mass = 1

An indexed product of total distributions is total.

noncomputable def CatCrypt.NonUniform.replicateFin {α : Type u_1} (n : ℕ) (d : Prob.SDistr α) : Prob.SDistr (Fin n → α)

n independent draws from one sub-distribution.

Equations

• CatCrypt.NonUniform.replicateFin n d = CatCrypt.NonUniform.piFin fun (x : Fin n) => d

theorem CatCrypt.NonUniform.mass_replicateFin {α : Type u_1} {n : ℕ} {d : Prob.SDistr α} (h : d.mass = 1) : (replicateFin n d).mass = 1

Repeated independent draws from a total distribution are total.