Expectations

theorem FD1D.FiniteLaw.expect_add {α : Type u_1} [Fintype α] (μ : FiniteLaw α) (f g : α → ℝ) : (μ.expect fun (x : α) => f x + g x) = μ.expect f + μ.expect g

theorem FD1D.FiniteLaw.expect_sub {α : Type u_1} [Fintype α] (μ : FiniteLaw α) (f g : α → ℝ) : (μ.expect fun (x : α) => f x - g x) = μ.expect f - μ.expect g

theorem FD1D.FiniteLaw.expect_const_mul {α : Type u_1} [Fintype α] (μ : FiniteLaw α) (c : ℝ) (f : α → ℝ) : (μ.expect fun (x : α) => c * f x) = c * μ.expect f

theorem FD1D.FiniteLaw.expect_mul_const {α : Type u_1} [Fintype α] (μ : FiniteLaw α) (f : α → ℝ) (c : ℝ) : (μ.expect fun (x : α) => f x * c) = μ.expect f * c

theorem FD1D.FiniteKernel.expect_step {α : Type u_1} [Fintype α] (K : FiniteKernel α) (μ : FiniteLaw α) (f : α → ℝ) : (K.step μ).expect f = μ.expect fun (x : α) => ∑ y : α, K.trans x y * f y

The expectation after one kernel step is the expectation of the conditional next-state expectation.

theorem FD1D.FiniteKernel.expect_step_sub {α : Type u_1} [Fintype α] (K : FiniteKernel α) (μ : FiniteLaw α) (f : α → ℝ) : (K.step μ).expect f - μ.expect f = μ.expect fun (x : α) => ∑ y : α, K.trans x y * (f y - f x)

Expected one-step change, in conditional-drift form.

theorem FD1D.FiniteKernel.expect_iterate_succ {α : Type u_1} [Fintype α] (K : FiniteKernel α) (μ : FiniteLaw α) (n : ℕ) (f : α → ℝ) : (K.iterate (n + 1) μ).expect f - (K.iterate n μ).expect f = (K.iterate n μ).expect fun (x : α) => ∑ y : α, K.trans x y * (f y - f x)

theorem FD1D.FiniteKernel.IsStationary.expect_eq {α : Type u_1} [Fintype α] {K : FiniteKernel α} {μ : FiniteLaw α} (hμ : K.IsStationary μ) (f : α → ℝ) : (K.step μ).expect f = μ.expect f