Finite uniform expectations

Shared finite averages, trajectory expectations, independence, and reindexing. The average on an empty type is zero.

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

Expectation under the uniform distribution on a fintype.

Equations

• Dynamics.avg f = (∑ a : α, f a) / ↑(Fintype.card α)

theorem Dynamics.avg_nonneg {α : Type u_1} [Fintype α] {f : α → ℝ} (hf : ∀ (a : α), 0 ≤ f a) : 0 ≤ avg f

theorem Dynamics.avg_le_avg {α : Type u_1} [Fintype α] {f g : α → ℝ} (h : ∀ (a : α), f a ≤ g a) : avg f ≤ avg g

theorem Dynamics.avg_add {α : Type u_1} [Fintype α] (f g : α → ℝ) : (avg fun (a : α) => f a + g a) = avg f + avg g

theorem Dynamics.avg_sub {α : Type u_1} [Fintype α] (f g : α → ℝ) : (avg fun (a : α) => f a - g a) = avg f - avg g

theorem Dynamics.avg_const_mul {α : Type u_1} [Fintype α] (c : ℝ) (f : α → ℝ) : (avg fun (a : α) => c * f a) = c * avg f

theorem Dynamics.avg_sum {α : Type u_1} [Fintype α] {ι : Type u_2} (s : Finset ι) (f : ι → α → ℝ) : (avg fun (a : α) => ∑ i ∈ s, f i a) = ∑ i ∈ s, avg (f i)

theorem Dynamics.avg_indicator {α : Type u_1} [Fintype α] (P : α → Prop) [DecidablePred P] : (avg fun (a : α) => if P a then 1 else 0) = ↑(Finset.filter P Finset.univ).card / ↑(Fintype.card α)

The expectation of an indicator is a counting ratio.

theorem Dynamics.card_cast_pos {α : Type u_1} [Fintype α] [Nonempty α] : 0 < ↑(Fintype.card α)

theorem Dynamics.avg_const {α : Type u_1} [Fintype α] [Nonempty α] (c : ℝ) : (avg fun (x : α) => c) = c

noncomputable def Dynamics.expList (α : Type u_2) [Fintype α] : ℕ → (List α → ℝ) → ℝ

Expectation of a functional of T i.i.d. uniform draws from α, in transition-operator form: the head draw is averaged out first.

Equations

• Dynamics.expList α 0 x✝ = x✝ []
• Dynamics.expList α T.succ x✝ = Dynamics.avg fun (a : α) => Dynamics.expList α T fun (l : List α) => x✝ (a :: l)

@[simp]

theorem Dynamics.expList_zero {α : Type u_1} [Fintype α] (F : List α → ℝ) : expList α 0 F = F []

theorem Dynamics.expList_succ {α : Type u_1} [Fintype α] (T : ℕ) (F : List α → ℝ) : expList α (T + 1) F = avg fun (a : α) => expList α T fun (l : List α) => F (a :: l)

theorem Dynamics.expList_nonneg {α : Type u_1} [Fintype α] {T : ℕ} {F : List α → ℝ} (h : ∀ (l : List α), 0 ≤ F l) : 0 ≤ expList α T F

theorem Dynamics.expList_le_expList {α : Type u_1} [Fintype α] {T : ℕ} {F G : List α → ℝ} (h : ∀ (l : List α), F l ≤ G l) : expList α T F ≤ expList α T G

theorem Dynamics.expList_add {α : Type u_1} [Fintype α] (T : ℕ) (F G : List α → ℝ) : (expList α T fun (l : List α) => F l + G l) = expList α T F + expList α T G

theorem Dynamics.expList_const_mul {α : Type u_1} [Fintype α] (T : ℕ) (c : ℝ) (F : List α → ℝ) : (expList α T fun (l : List α) => c * F l) = c * expList α T F

theorem Dynamics.expList_const {α : Type u_1} [Fintype α] [Nonempty α] (T : ℕ) (c : ℝ) : (expList α T fun (x : List α) => c) = c

theorem Dynamics.expList_sum {α : Type u_1} [Fintype α] {ι : Type u_2} (s : Finset ι) (T : ℕ) (F : ι → List α → ℝ) : (expList α T fun (l : List α) => ∑ i ∈ s, F i l) = ∑ i ∈ s, expList α T (F i)

theorem Dynamics.expList_append {α : Type u_1} [Fintype α] (T₁ T₂ : ℕ) (F : List α → ℝ) : expList α (T₁ + T₂) F = expList α T₁ fun (l₁ : List α) => expList α T₂ fun (l₂ : List α) => F (l₁ ++ l₂)

Independence: average of a product over a product space

theorem Dynamics.avg_mul_prod {β : Type u_2} {δ : Type u_3} [Fintype β] [Fintype δ] (g : β → ℝ) (h : δ → ℝ) : (avg fun (p : β × δ) => g p.1 * h p.2) = avg g * avg h

Independence for a pair of coordinates: the average of a product g p.1 * h p.2 over a product Fintype β × δ (uniform measure) equals the product of the individual averages. No Nonempty hypothesis is needed: if either factor is empty, both sides are 0 by the 0/0 = 0 convention.

theorem Dynamics.avg_fst_mul {β : Type u_2} {δ : Type u_3} [Fintype β] [Fintype δ] [Nonempty δ] (g : β → ℝ) : (avg fun (p : β × δ) => g p.1) = avg g

Marginal: the average of a function of the first coordinate only, over a product space, equals its average over the first factor alone.

theorem Dynamics.avg_snd_mul {β : Type u_2} {δ : Type u_3} [Fintype β] [Nonempty β] [Fintype δ] (h : δ → ℝ) : (avg fun (p : β × δ) => h p.2) = avg h

Marginal: the average of a function of the second coordinate only, over a product space, equals its average over the second factor alone.

theorem Dynamics.avg_equiv {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] (e : α ≃ β) (F : β → ℝ) : (avg fun (a : α) => F (e a)) = avg F

Reindexing avg along an Equiv between the underlying Fintypes.

theorem Dynamics.avg_prod_pi {γ : Type u_2} [Fintype γ] (n : ℕ) (f : Fin n → γ → ℝ) : (avg fun (x : Fin n → γ) => ∏ i : Fin n, f i (x i)) = ∏ i : Fin n, avg (f i)

Independence over a Fin n-indexed product: the average of a product ∏ i, f i (x i) over the product Fintype Fin n → γ (uniform measure) equals the product of the individual averages avg (f i). This is the discrete, measure-theory-free form of "coordinate projections on a product space are independent."

theorem Dynamics.avg_eval {γ : Type u_2} [Fintype γ] [Nonempty γ] (n : ℕ) (v : Fin n) (G : γ → ℝ) : (avg fun (x : Fin n → γ) => G (x v)) = avg G

Marginal for Fin n-indexed Pi types: the average of a function of a single fixed coordinate, over the whole product space, equals its average over that one factor alone.

theorem Dynamics.avg_avg_swap {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] (F : α → β → ℝ) : (avg fun (a : α) => avg fun (b : β) => F a b) = avg fun (b : β) => avg fun (a : α) => F a b

Finite uniform averages over a product of index sets commute.

theorem Dynamics.expList_avg_comm {α : Type u_1} [Fintype α] {β : Type u_2} [Fintype β] (T : ℕ) (G : α → List β → ℝ) : (avg fun (a : α) => expList β T (G a)) = expList β T fun (l : List β) => avg fun (a : α) => G a l

expList is an iterated average, so it commutes with an outer uniform average.

theorem Dynamics.expList_zero_fun {α : Type u_1} [Fintype α] (T : ℕ) : (expList α T fun (x : List α) => 0) = 0

The expectation of the zero functional vanishes (no nonemptiness needed).

theorem Dynamics.expList_finset_sum {α : Type u_1} [Fintype α] {ι : Type u_2} (T : ℕ) (s : Finset ι) (F : ι → List α → ℝ) : (expList α T fun (l : List α) => ∑ i ∈ s, F i l) = ∑ i ∈ s, expList α T (F i)

expList commutes with finite sums.