Distributions on finite sets

We define the type Distribution α on a Fintype α. By restricting ourselves to distributoins on finite types, a lot of notation and casts are greatly simplified. This suffices for (most) finite-dimensional quantum theory.

def ProbDistribution (α : Type u) [Fintype α] : Type u

We define our own (discrete) probability distribution notion here, instead of using PMF from Mathlib, because that uses ENNReals everywhere to maintain compatibility with MeasureTheory.Measure.

The probabilities internal to a Distribution are NNReals. This lets us more easily write the statement that they sum to 1, since NNReals can be added. (Probabilities, on their own, cannot.) But the FunLike instance gives Prob out, which carry the information that they are all in the range [0,1].

Equations

• ProbDistribution α = { f : α → Prob // ∑ i : α, ↑(f i) = 1 }

def ProbDistribution.mk' {α : Type u_1} [Fintype α] (f : α → ℝ) (h₁ : ∀ (i : α), 0 ≤ f i) (hN : ∑ i : α, f i = 1) : ProbDistribution α

Make a distribution, proving only that the values are nonnegative and that the sum is 1. The fact that the values are at most 1 is derived as a consequence.

Equations

• ProbDistribution.mk' f h₁ hN = ⟨fun (i : α) => ⟨f i, ⋯⟩, hN⟩

instance ProbDistribution.instFunLikeProb {α : Type u_1} [Fintype α] : FunLike (ProbDistribution α) α Prob

Equations

• ProbDistribution.instFunLikeProb = { coe := fun (p : ProbDistribution α) (a : α) => ↑p a, coe_injective' := ⋯ }

@[simp]

theorem ProbDistribution.normalized {α : Type u_1} [Fintype α] (d : ProbDistribution α) : ∑ i : α, ↑(d i) = 1

@[reducible, inline]

abbrev ProbDistribution.prob {α : Type u_1} [Fintype α] (d : ProbDistribution α) (a : α) : Prob

Equations

• d.prob = ⇑d

@[simp]

theorem ProbDistribution.fun_eq_val {α : Type u_1} [Fintype α] (d : ProbDistribution α) : ↑d = ⇑d

@[simp]

theorem ProbDistribution.funlike_apply {α : Type u_1} [Fintype α] (d : α → Prob) (h : ∑ i : α, ↑(d i) = 1) (x : α) : ⟨d, h⟩ x = d x

theorem ProbDistribution.ext {α : Type u_1} [Fintype α] {p q : ProbDistribution α} (h : ∀ (x : α), p x = q x) : p = q

theorem ProbDistribution.ext_iff {α : Type u_1} [Fintype α] {p q : ProbDistribution α} : p = q ↔ ∀ (x : α), p x = q x

theorem ProbDistribution.nonempty {α : Type u_1} [Fintype α] (d : ProbDistribution α) : Nonempty α

A distribution provides a witness that d is nonempty.

def ProbDistribution.constant {α : Type u_1} [Fintype α] (x : α) : ProbDistribution α

Make an constant distribution: supported on a single element. This is also called, variously, a "One-point distribution", a "Degenerate distribution", a "Deterministic distribution", a "Delta function", or a "Point mass distribution".

Equations

• ProbDistribution.constant x = ⟨fun (y : α) => if x = y then 1 else 0, ⋯⟩

theorem ProbDistribution.constant_def {α : Type u_1} [Fintype α] (x : α) : ⇑(constant x) = fun (y : α) => if x = y then 1 else 0

@[simp]

theorem ProbDistribution.constant_eq {α : Type u_1} [Fintype α] {y : α} (x : α) : (constant x) y = if x = y then 1 else 0

@[simp]

theorem ProbDistribution.constant_def' {α : Type u_1} [Fintype α] (x y : α) : (constant x) y = if x = y then 1 else 0

theorem ProbDistribution.constant_of_exists_one {α : Type u_1} [Fintype α] {D : ProbDistribution α} {x : α} (h : D x = 1) : D = constant x

If a distribution has an element with probability 1, the distribution has a constant.

def ProbDistribution.uniform {α : Type u_1} [Fintype α] [n : Nonempty α] : ProbDistribution α

Make an uniform distribution.

Equations

• ProbDistribution.uniform = ⟨fun (x : α) => ⟨1 / ↑Finset.univ.card, ⋯⟩, ⋯⟩

@[simp]

theorem ProbDistribution.uniform_def {α : Type u_1} [Fintype α] [Nonempty α] (y : α) : ↑(uniform y) = 1 / ↑Finset.univ.card

def ProbDistribution.prod {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (d1 : ProbDistribution α) (d2 : ProbDistribution β) : ProbDistribution (α × β)

Make a distribution on a product of two Fintypes.

Equations

• d1.prod d2 = ⟨fun (x : α × β) => d1 x.1 * d2 x.2, ⋯⟩

@[simp]

theorem ProbDistribution.prod_def {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {d1 : ProbDistribution α} {d2 : ProbDistribution β} (x : α) (y : β) : (d1.prod d2) (x, y) = d1 x * d2 y

def ProbDistribution.extend_right {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (d : ProbDistribution α) : ProbDistribution (α ⊕ β)

Given a distribution on α, extend it to a distribution on Sum α β by giving it no support on β.

Equations

• d.extend_right = ⟨fun (x : α ⊕ β) => Sum.casesOn x (↑d) (Function.const β 0), ⋯⟩

def ProbDistribution.extend_left {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (d : ProbDistribution α) : ProbDistribution (β ⊕ α)

Given a distribution on α, extend it to a distribution on Sum β α by giving it no support on β.

Equations

• d.extend_left = ⟨fun (x : β ⊕ α) => Sum.casesOn x (Function.const β 0) ↑d, ⋯⟩

instance ProbDistribution.instMixable {α : Type u_1} [Fintype α] : Mixable (α → ℝ) (ProbDistribution α)

Make a convex mixture of two distributions on the same set.

Equations

• ProbDistribution.instMixable = inferInstance.instSubtype ⋯

def ProbDistribution.relabel {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (d : ProbDistribution α) (σ : β ≃ α) : ProbDistribution β

Given a distribution on type α and an equivalence to type β, get the corresponding distribution on type β.

Equations

• d.relabel σ = ⟨fun (b : β) => d (σ b), ⋯⟩

def ProbDistribution.congr {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (σ : α ≃ β) : ProbDistribution α ≃ ProbDistribution β

ProbDistribution on α and β are equivalent for equivalent types α ≃ β.

Equations

• ProbDistribution.congr σ = { toFun := fun (d : ProbDistribution α) => d.relabel σ.symm, invFun := fun (d : ProbDistribution β) => d.relabel σ, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem ProbDistribution.congr_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (σ : α ≃ β) (d : ProbDistribution α) (j : β) : ((congr σ) d) j = d (σ.symm j)

@[simp]

theorem ProbDistribution.congr_symm_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (σ : α ≃ β) : (congr σ).symm = congr σ.symm

The inverse and congruence operations for distributions commute

def ProbDistribution.coin (p : Prob) : ProbDistribution (Fin 2)

The distribution on Fin 2 corresponding to a coin with probability p. Chance p of 1, 1-p of 0.

Equations

• ProbDistribution.coin p = ⟨fun (x : Fin 2) => if x = 0 then p else 1 - p, ⋯⟩

@[simp]

theorem ProbDistribution.coin_val_zero (p : Prob) : (coin p) 0 = p

@[simp]

theorem ProbDistribution.coin_val_one (p : Prob) : (coin p) 1 = 1 - p

theorem ProbDistribution.fin_two_eq_coin (d : ProbDistribution (Fin 2)) : d = coin (d 0)

Every distribution on two variable is some coin.

theorem ProbDistribution.coin_eq_iff (p : Prob) (f : ProbDistribution (Fin 2)) : coin p = f ↔ p = f 0

structure ProbDistribution.RandVar (α : Type u_3) [Fintype α] (T : Type u_4) : Type (max u_3 u_4)

A T-valued random variable over α is a map var : α → T along with a probability distribution distr : Distribution α.

• var : α → T
• distr : ProbDistribution α

instance ProbDistribution.instFunctor {α : Type u_1} [Fintype α] : Functor (RandVar α)

Equations

• ProbDistribution.instFunctor = { map := fun {α_1 β : Type ?u.22} (f : α_1 → β) (e : ProbDistribution.RandVar α α_1) => { var := f ∘ e.var, distr := e.distr } }

instance ProbDistribution.instLawfulFunctor {α : Type u_1} [Fintype α] : LawfulFunctor (RandVar α)

def ProbDistribution.expect_val {α : Type u_1} [Fintype α] {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (X : RandVar α T) : T

Distribution.exp_val is the expectation value of a random variable X. Under the hood, it is the "convex combination over a finite family" on the type T, afforded by the Mixable instance, with the probability distribution of X as weights.

Equations

• ProbDistribution.expect_val X = ↑(Mixable.mkT ⋯)

theorem ProbDistribution.expect_val_eq_mixable_mix {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (d : ProbDistribution (Fin 2)) (x₁ x₂ : T) : expect_val { var := ![x₁, x₂], distr := d } = d 0[x₁↔x₂]

The expectation value of a random variable over α = Fin 2 is the same as Mixable.mix with probabiliy weight X.distr 0

theorem ProbDistribution.expect_val_constant {α : Type u_1} [Fintype α] {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (x : α) (f : α → T) : expect_val { var := f, distr := constant x } = f x

The expectation value of a random variable with constant probability distribution constant x is its value at x

theorem ProbDistribution.zero_le_expect_val {α : Type u_1} [Fintype α] (d : ProbDistribution α) (f : α → ℝ) (hpos : 0 ≤ f) : 0 ≤ expect_val { var := f, distr := d }

The expectation value of a nonnegative real random variable is also nonnegative

def ProbDistribution.congrRandVar {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {T : Type u_3} (σ : α ≃ β) : RandVar α T ≃ RandVar β T

T-valued random variables on α and β are equivalent if α ≃ β

Equations

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

def ProbDistribution.map_congr_eq_congr_map {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] {S : Type u_3} [Mixable U S] (f : T → S) (σ : α ≃ β) (X : RandVar α T) : f <$> (congrRandVar σ) X = (congrRandVar σ) (f <$> X)

Given a T-valued random variable X over α, mapping over T commutes with the equivalence over α

Equations

• ⋯ = ⋯

@[simp]

theorem ProbDistribution.expect_val_congr_eq_expect_val {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (σ : α ≃ β) (X : RandVar α T) : expect_val ((congrRandVar σ) X) = expect_val X

The expectation value is invariant under equivalence of random variables