Averaging

noncomputable def FD1D.FiniteLaw.timeAverage {α : Type u_1} [Fintype α] {T : ℕ} (hT : 0 < T) (μ : Fin T → FiniteLaw α) : FiniteLaw (Fin T × α)

Choose a time uniformly from Fin T, then sample from the law assigned to that time.

Equations

• FD1D.FiniteLaw.timeAverage hT μ = { mass := fun (z : Fin T × α) => 1 / ↑T * (μ z.1).mass z.2, mass_nonneg := ⋯, sum_mass := ⋯ }

@[simp]

theorem FD1D.FiniteLaw.timeAverage_mass {α : Type u_1} [Fintype α] {T : ℕ} (hT : 0 < T) (μ : Fin T → FiniteLaw α) (t : Fin T) (x : α) : (timeAverage hT μ).mass (t, x) = 1 / ↑T * (μ t).mass x

theorem FD1D.FiniteLaw.expect_timeAverage {α : Type u_1} [Fintype α] {T : ℕ} (hT : 0 < T) (μ : Fin T → FiniteLaw α) (f : Fin T × α → ℝ) : (timeAverage hT μ).expect f = (∑ t : Fin T, (μ t).expect fun (x : α) => f (t, x)) / ↑T

Expectation under the time/state mixture is the average expectation.

theorem FD1D.FiniteLaw.expect_timeAverage_eq_sum_range {α : Type u_1} [Fintype α] {T : ℕ} (hT : 0 < T) (μ : ℕ → FiniteLaw α) (f : ℕ → α → ℝ) : ((timeAverage hT fun (t : Fin T) => μ ↑t).expect fun (z : Fin T × α) => f (↑z.1) z.2) = (∑ t ∈ Finset.range T, (μ t).expect (f t)) / ↑T

Range-indexed form of expect_timeAverage.

theorem FD1D.FiniteLaw.expect_timeAverage_state {α : Type u_1} [Fintype α] {T : ℕ} (hT : 0 < T) (μ : ℕ → FiniteLaw α) (f : α → ℝ) : ((timeAverage hT fun (t : Fin T) => μ ↑t).expect fun (z : Fin T × α) => f z.2) = (∑ t ∈ Finset.range T, (μ t).expect f) / ↑T

A state-only observable averages in the same way.

def FD1D.FiniteLaw.timeLiftPerm {α : Type u_1} {T : ℕ} (e : Equiv.Perm α) : Equiv.Perm (Fin T × α)

Lift a state permutation without changing the sampled time.

Equations

• FD1D.FiniteLaw.timeLiftPerm e = (Equiv.refl (Fin T)).prodCongr e

@[simp]

theorem FD1D.FiniteLaw.timeLiftPerm_apply {α : Type u_1} {T : ℕ} (e : Equiv.Perm α) (t : Fin T) (x : α) : (timeLiftPerm e) (t, x) = (t, e x)

theorem FD1D.FiniteLaw.timeAverage_lawInvariant {α : Type u_1} [Fintype α] {T : ℕ} (hT : 0 < T) (μ : Fin T → FiniteLaw α) (e : Equiv.Perm α) (hinv : ∀ (t : Fin T), FiniteKernel.LawInvariant (μ t) e) : FiniteKernel.LawInvariant (timeAverage hT μ) (timeLiftPerm e)

Pointwise state-law invariance passes to the uniform time mixture.