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 Distribution (α : 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

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

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

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

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

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

Equations

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

@[simp]

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

@[reducible, inline]

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

Equations

• d.prob = ⇑d

@[simp]

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

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

instance Distribution.nonempty {α : Type u_1} [Fintype α] (d : Distribution α) : Nonempty α

A distribution is a witness that d is nonempty.

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

Make an uniform distribution.

Equations

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

@[simp]

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

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

Make a distribution on a product of two Fintypes.

Equations

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

@[simp]

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

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

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 Distribution.extend_left {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (d : Distribution α) : Distribution (β ⊕ α)

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 Distribution.instMixable {α : Type u_1} [Fintype α] : Mixable (α → ℝ) (Distribution α)

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

Equations

• Distribution.instMixable = inferInstance.instSubtype ⋯

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

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

Equations

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

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

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

Equations

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

@[simp]

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

@[simp]

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

The inverse and congruence operations for distributions commute

structure Distribution.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 : Distribution α

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

Equations

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

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

def Distribution.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

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

theorem Distribution.expect_val_eq_mixable_mix {T : Type u_3} {U : Type u_4} [AddCommGroup U] [Module ℝ U] [inst : Mixable U T] (d : Distribution (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 Distribution.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 Distribution.zero_le_expect_val {α : Type u_1} [Fintype α] (d : Distribution α) (f : α → ℝ) (hpos : 0 ≤ f) : 0 ≤ expect_val { var := f, distr := d }

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

def Distribution.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 Distribution.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 Distribution.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