Normalized finite distributions

Real weights make expectations finite sums. Unlike avg, a normalized distribution cannot exist on an empty type. Uniform expectations retain their old empty-type convention.

structure Dynamics.Distribution (α : Type u_1) [Fintype α] : Type u_1

Nonnegative real weights with total mass one.

• weight : α → ℝ
• nonneg (a : α) : 0 ≤ self.weight a
• sum_one : ∑ a : α, self.weight a = 1

noncomputable def Dynamics.Distribution.expect {α : Type u_1} [Fintype α] (p : Distribution α) (f : α → ℝ) : ℝ

Expectation of a real observable.

Equations

• p.expect f = ∑ a : α, p.weight a * f a

noncomputable def Dynamics.Distribution.prob {α : Type u_1} [Fintype α] (p : Distribution α) (s : α → Prop) : ℝ

Probability of an event.

Equations

• p.prob s = p.expect fun (a : α) => if s a then 1 else 0

@[simp]

theorem Dynamics.Distribution.expect_const {α : Type u_1} [Fintype α] (p : Distribution α) (c : ℝ) : (p.expect fun (x : α) => c) = c

theorem Dynamics.Distribution.expect_nonneg {α : Type u_1} [Fintype α] (p : Distribution α) {f : α → ℝ} (h : ∀ (a : α), 0 ≤ f a) : 0 ≤ p.expect f

theorem Dynamics.Distribution.expect_mono {α : Type u_1} [Fintype α] (p : Distribution α) {f g : α → ℝ} (h : ∀ (a : α), f a ≤ g a) : p.expect f ≤ p.expect g

theorem Dynamics.Distribution.expect_add {α : Type u_1} [Fintype α] (p : Distribution α) (f g : α → ℝ) : (p.expect fun (a : α) => f a + g a) = p.expect f + p.expect g

theorem Dynamics.Distribution.expect_sub {α : Type u_1} [Fintype α] (p : Distribution α) (f g : α → ℝ) : (p.expect fun (a : α) => f a - g a) = p.expect f - p.expect g

theorem Dynamics.Distribution.expect_mul {α : Type u_1} [Fintype α] (p : Distribution α) (c : ℝ) (f : α → ℝ) : (p.expect fun (a : α) => c * f a) = c * p.expect f

theorem Dynamics.Distribution.expect_sum {α : Type u_1} {ι : Type u_3} [Fintype α] [Fintype ι] (p : Distribution α) (f : ι → α → ℝ) : (p.expect fun (a : α) => ∑ i : ι, f i a) = ∑ i : ι, p.expect (f i)

theorem Dynamics.Distribution.prob_nonneg {α : Type u_1} [Fintype α] (p : Distribution α) (s : α → Prop) : 0 ≤ p.prob s

theorem Dynamics.Distribution.prob_le_one {α : Type u_1} [Fintype α] (p : Distribution α) (s : α → Prop) : p.prob s ≤ 1

theorem Dynamics.Distribution.prob_eq_expect {α : Type u_1} [Fintype α] (p : Distribution α) (s : α → Prop) [DecidablePred s] : p.prob s = p.expect fun (a : α) => if s a then 1 else 0

prob computed with any decidability instance for the event.

noncomputable def Dynamics.Distribution.uniform (α : Type u_4) [Fintype α] [Nonempty α] : Distribution α

Uniform distribution, available precisely when the sample type is nonempty.

Equations

• Dynamics.Distribution.uniform α = { weight := fun (x : α) => (↑(Fintype.card α))⁻¹, nonneg := ⋯, sum_one := ⋯ }

theorem Dynamics.Distribution.uniform_expect {α : Type u_1} [Fintype α] [Nonempty α] (f : α → ℝ) : (uniform α).expect f = avg f

noncomputable def Dynamics.Distribution.point {α : Type u_1} [Fintype α] (a : α) : Distribution α

Point mass.

Equations

• Dynamics.Distribution.point a = { weight := fun (b : α) => if b = a then 1 else 0, nonneg := ⋯, sum_one := ⋯ }

@[simp]

theorem Dynamics.Distribution.point_expect {α : Type u_1} [Fintype α] (a : α) (f : α → ℝ) : (point a).expect f = f a

noncomputable def Dynamics.Distribution.map {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : Distribution α) (f : α → β) : Distribution β

Transport a distribution along a function, summing over its fibers.

Equations

• p.map f = { weight := fun (b : β) => ∑ a : α, if f a = b then p.weight a else 0, nonneg := ⋯, sum_one := ⋯ }

theorem Dynamics.Distribution.map_expect {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : Distribution α) (f : α → β) (g : β → ℝ) : (p.map f).expect g = p.expect fun (a : α) => g (f a)

noncomputable def Dynamics.Distribution.independent {α : Type u_1} {ι : Type u_3} [Fintype α] [Fintype ι] [DecidableEq ι] (p : ι → Distribution α) : Distribution (ι → α)

Independent product of a finite family of distributions.

Equations

• Dynamics.Distribution.independent p = { weight := fun (x : ι → α) => ∏ i : ι, (p i).weight (x i), nonneg := ⋯, sum_one := ⋯ }

theorem Dynamics.Distribution.independent_expect_prod {α : Type u_1} {ι : Type u_3} [Fintype α] [Fintype ι] [DecidableEq ι] (p : ι → Distribution α) (f : ι → α → ℝ) : ((independent p).expect fun (x : ι → α) => ∏ i : ι, f i (x i)) = ∏ i : ι, (p i).expect (f i)

theorem Dynamics.Distribution.independent_expect_eval {α : Type u_1} {ι : Type u_3} [Fintype α] [Fintype ι] [DecidableEq ι] (p : ι → Distribution α) (i : ι) (f : α → ℝ) : ((independent p).expect fun (x : ι → α) => f (x i)) = (p i).expect f