Bridges between the expectation APIs

Three finite expectation APIs are available to the packages of this repository:

• Dynamics.avg f, the uniform average (∑ a, f a) / |α| (zero on an empty type), and its iterate Dynamics.expList α T F over T i.i.d. uniform rounds (Dynamics.Uniform);
• Dynamics.Distribution.expect, the expectation under a weighted finite distribution, with the uniform law Distribution.uniform and the independent product Distribution.independent (Dynamics.Distribution);
• Mathlib's Finset.expect, written 𝔼 a, f a (Mathlib.Algebra.BigOperators.Expect).

This file identifies them, so that results proved in one API apply in the others:

• avg_eq_expect: avg f = 𝔼 a, f a;
• Distribution.uniform_expect (in Dynamics.Distribution): (uniform α).expect f = avg f;
• Distribution.independent_uniform_expect: the independent product of uniform laws is the uniform law on the product space;
• expList_eq_expect and expList_eq_independent_expect: expList α T F is the expectation of F over T i.i.d. uniform draws, in Mathlib's and in the distribution form. They complete expList_eq_avg_ofFn (in Dynamics.Equivalence), the uniform-average form.

theorem Dynamics.avg_eq_expect {α : Type u_1} [Fintype α] (f : α → ℝ) : avg f = Finset.univ.expect fun (a : α) => f a

The uniform average is Mathlib's finite expectation (blueprint def:avg): avg f = 𝔼 a, f a, i.e. Finset.expect univ f. Both sides vanish on an empty type.

theorem Dynamics.expList_eq_expect {α : Type u_1} [Fintype α] (T : ℕ) (F : List α → ℝ) : expList α T F = Finset.univ.expect fun (ω : Fin T → α) => F (List.ofFn ω)

T i.i.d. uniform rounds, Mathlib form (blueprint lem:uniform-trajectory): expList α T F is the finite expectation of F over all length-T sequences of draws.

theorem Dynamics.Distribution.independent_uniform_expect {α : Type u_1} [Fintype α] {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Nonempty α] (g : (ι → α) → ℝ) : (independent fun (x : ι) => uniform α).expect g = avg g

The independent product of uniform laws is uniform (blueprint lem:uniform-agreement, lem:weighted-product): the expectation under independent fun _ : ι => uniform α is the uniform average over ι → α.

theorem Dynamics.expList_eq_independent_expect {α : Type u_1} [Fintype α] [Nonempty α] (T : ℕ) (F : List α → ℝ) : expList α T F = (Distribution.independent fun (x : Fin T) => Distribution.uniform α).expect fun (ω : Fin T → α) => F (List.ofFn ω)

T i.i.d. uniform rounds, distribution form (blueprint lem:uniform-trajectory): expList α T F is the expectation of F (List.ofFn ω) under the independent product of T uniform distributions on α.