Lemmas on finite distributions

Extensionality of Dynamics.Distribution (by weights or by expectations) and the expectations of uniform, point, normalized and conditioned distributions.

theorem Crn.dist_ext {α : Type u_1} [Fintype α] {p q : Dynamics.Distribution α} (h : ∀ (a : α), p.weight a = q.weight a) : p = q

Distributions with the same weights are equal.

theorem Crn.weight_eq_expect {α : Type u_1} [Fintype α] [DecidableEq α] (p : Dynamics.Distribution α) (a : α) : p.weight a = p.expect fun (b : α) => if b = a then 1 else 0

The weight of a is the expectation of the indicator of a.

theorem Crn.dist_ext_expect {α : Type u_1} [Fintype α] {p q : Dynamics.Distribution α} (h : ∀ (f : α → ℝ), p.expect f = q.expect f) : p = q

Distributions with the same expectations are equal.

theorem Crn.prob_eq_sum {α : Type u_1} [Fintype α] (p : Dynamics.Distribution α) (E : α → Prop) [DecidablePred E] : p.prob E = ∑ a : α, if E a then p.weight a else 0

The probability of an event, as a sum of weights, for any decidability instance.

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

The probability of an event is the expectation of its indicator, for any decidability instance.

theorem Crn.expect_ite {α : Type u_1} [Fintype α] (p : Dynamics.Distribution α) (E : α → Prop) [DecidablePred E] (f : α → ℝ) : (p.expect fun (a : α) => if E a then f a else 0) = ∑ a : α, if E a then p.weight a * f a else 0

Expectation of an observable vanishing off E, for any decidability instance.

theorem Crn.normalize_expect {α : Type u_1} [Fintype α] (w : α → ℝ) (hw : ∀ (a : α), 0 ≤ w a) (h : ∑ a : α, w a ≠ 0) (f : α → ℝ) : (normalize w hw h).expect f = (∑ a : α, w a * f a) / ∑ a : α, w a

Expectation under normalized weights: ∑ w·f / ∑ w.

theorem Crn.condition_expect {α : Type u_1} [Fintype α] (p : Dynamics.Distribution α) (E : α → Prop) [DecidablePred E] (h : p.prob E ≠ 0) (f : α → ℝ) : (condition p E h).expect f = (p.expect fun (a : α) => if E a then f a else 0) / p.prob E

Expectation under a conditioned distribution.

theorem Crn.uniform_expect_sum {α : Type u_1} [Fintype α] [Nonempty α] (f : α → ℝ) : (Dynamics.Distribution.uniform α).expect f = (∑ a : α, f a) / ↑(Fintype.card α)

Uniform expectation as a sum divided by the cardinality.

theorem Crn.uniform_prob {α : Type u_1} [Fintype α] [Nonempty α] (E : α → Prop) [DecidablePred E] : (Dynamics.Distribution.uniform α).prob E = ↑(Finset.filter E Finset.univ).card / ↑(Fintype.card α)

Uniform probability as a counting ratio.

theorem Crn.uniform_prod_expect {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] [Nonempty α] [Nonempty β] (f : α × β → ℝ) : (Dynamics.Distribution.uniform (α × β)).expect f = (∑ b : β, (Dynamics.Distribution.uniform α).expect fun (a : α) => f (a, b)) / ↑(Fintype.card β)

Uniform expectation over a product, the first coordinate averaged first.