Markov

Finite inventory Markov chains

This file uses elementary finite sums throughout. A FiniteKernel is a row-stochastic matrix, and FiniteLaw.step is left multiplication by that matrix. The inventory chain near the end of the file removes one item and then adds an independent uniformly distributed item.

Finite laws and stochastic kernels

theorem FD1D.FiniteLaw.ext {α : Type u_1} [Fintype α] {μ ν : FiniteLaw α} (h : ∀ (x : α), μ.mass x = ν.mass x) : μ = ν

theorem FD1D.FiniteLaw.ext_iff {α : Type u_1} [Fintype α] {μ ν : FiniteLaw α} : μ = ν ↔ ∀ (x : α), μ.mass x = ν.mass x

def FD1D.FiniteLaw.dirac {α : Type u_1} [Fintype α] [DecidableEq α] (x : α) : FiniteLaw α

The point mass at x.

Equations

• FD1D.FiniteLaw.dirac x = { mass := fun (y : α) => if y = x then 1 else 0, mass_nonneg := ⋯, sum_mass := ⋯ }

@[simp]

theorem FD1D.FiniteLaw.mass_dirac {α : Type u_1} [Fintype α] [DecidableEq α] (x y : α) : (dirac x).mass y = if y = x then 1 else 0

noncomputable def FD1D.FiniteLaw.uniform {α : Type u_1} [Fintype α] [Nonempty α] : FiniteLaw α

The uniform law on a nonempty finite type.

Equations

• FD1D.FiniteLaw.uniform = { mass := fun (x : α) => 1 / ↑(Fintype.card α), mass_nonneg := ⋯, sum_mass := ⋯ }

@[simp]

theorem FD1D.FiniteLaw.mass_uniform {α : Type u_1} [Fintype α] [Nonempty α] (x : α) : uniform.mass x = 1 / ↑(Fintype.card α)

def FD1D.FiniteLaw.map {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (f : α → β) (μ : FiniteLaw α) : FiniteLaw β

Push a finite law forward along a map.

Equations

• FD1D.FiniteLaw.map f μ = { mass := fun (y : β) => ∑ x : α with f x = y, μ.mass x, mass_nonneg := ⋯, sum_mass := ⋯ }

@[simp]

theorem FD1D.FiniteLaw.mass_map {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (f : α → β) (μ : FiniteLaw α) (y : β) : (map f μ).mass y = ∑ x : α with f x = y, μ.mass x

structure FD1D.FiniteKernel (α : Type u_1) [Fintype α] : Type u_1

A stochastic kernel on a finite state space.

• trans : α → α → ℝ

  One-step transition probability from the first state to the second.

• trans_nonneg (x y : α) : 0 ≤ self.trans x y
• sum_trans (x : α) : ∑ y : α, self.trans x y = 1

@[instance_reducible]

instance FD1D.FiniteKernel.instCoeFunForallForallReal {α : Type u_1} [Fintype α] : CoeFun (FiniteKernel α) fun (x : FiniteKernel α) => α → α → ℝ

Equations

• FD1D.FiniteKernel.instCoeFunForallForallReal = { coe := FD1D.FiniteKernel.trans }

def FD1D.FiniteKernel.matrix {α : Type u_1} [Fintype α] (K : FiniteKernel α) : Matrix α α ℝ

The row-stochastic matrix of a finite kernel.

Equations

• K.matrix = K.trans

theorem FD1D.FiniteKernel.matrix_rowStochastic {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) : K.matrix ∈ Matrix.rowStochastic ℝ α

def FD1D.FiniteKernel.step {α : Type u_1} [Fintype α] (K : FiniteKernel α) (μ : FiniteLaw α) : FiniteLaw α

Advance a law by one step of the kernel.

Equations

• K.step μ = { mass := fun (y : α) => ∑ x : α, μ.mass x * K.trans x y, mass_nonneg := ⋯, sum_mass := ⋯ }

@[simp]

theorem FD1D.FiniteKernel.mass_step {α : Type u_1} [Fintype α] (K : FiniteKernel α) (μ : FiniteLaw α) (y : α) : (K.step μ).mass y = ∑ x : α, μ.mass x * K.trans x y

def FD1D.FiniteKernel.iterate {α : Type u_1} [Fintype α] (K : FiniteKernel α) : ℕ → FiniteLaw α → FiniteLaw α

The law after n steps.

Equations

• K.iterate 0 x✝ = x✝
• K.iterate n.succ x✝ = K.step (K.iterate n x✝)

@[simp]

theorem FD1D.FiniteKernel.iterate_zero {α : Type u_1} [Fintype α] (K : FiniteKernel α) (μ : FiniteLaw α) : K.iterate 0 μ = μ

@[simp]

theorem FD1D.FiniteKernel.iterate_succ {α : Type u_1} [Fintype α] (K : FiniteKernel α) (n : ℕ) (μ : FiniteLaw α) : K.iterate (n + 1) μ = K.step (K.iterate n μ)

theorem FD1D.FiniteKernel.iterate_add {α : Type u_1} [Fintype α] (K : FiniteKernel α) (m n : ℕ) (μ : FiniteLaw α) : K.iterate (m + n) μ = K.iterate m (K.iterate n μ)

def FD1D.FiniteKernel.pow {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (n : ℕ) (x y : α) : ℝ

The n-step transition probability.

Equations

• K.pow n x y = (K.matrix ^ n) x y

@[simp]

theorem FD1D.FiniteKernel.pow_zero {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (x y : α) : K.pow 0 x y = if x = y then 1 else 0

@[simp]

theorem FD1D.FiniteKernel.pow_one {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (x y : α) : K.pow 1 x y = K.trans x y

theorem FD1D.FiniteKernel.pow_nonneg {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (n : ℕ) (x y : α) : 0 ≤ K.pow n x y

theorem FD1D.FiniteKernel.sum_pow {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (n : ℕ) (x : α) : ∑ y : α, K.pow n x y = 1

theorem FD1D.FiniteKernel.pow_add {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (m n : ℕ) (x z : α) : K.pow (m + n) x z = ∑ y : α, K.pow m x y * K.pow n y z

theorem FD1D.FiniteKernel.mass_iterate {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (n : ℕ) (μ : FiniteLaw α) (y : α) : (K.iterate n μ).mass y = ∑ x : α, μ.mass x * K.pow n x y

theorem FD1D.FiniteKernel.iterate_dirac {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (n : ℕ) (x y : α) : (K.iterate n (FiniteLaw.dirac x)).mass y = K.pow n x y

def FD1D.FiniteKernel.IsStationary {α : Type u_1} [Fintype α] (K : FiniteKernel α) (μ : FiniteLaw α) : Prop

A law is stationary when one step leaves it unchanged.

Equations

• K.IsStationary μ = (K.step μ = μ)

theorem FD1D.FiniteKernel.IsStationary.iterate {α : Type u_1} [Fintype α] {K : FiniteKernel α} {μ : FiniteLaw α} (h : K.IsStationary μ) (n : ℕ) : K.iterate n μ = μ

Existence of a stationary law

def FD1D.FiniteKernel.orbit {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (μ : FiniteLaw α) (n : ℕ) : α → ℝ

The mass vector after n steps, written as a matrix product.

Equations

• K.orbit μ n = Matrix.vecMul μ.mass (K.matrix ^ n)

theorem FD1D.FiniteKernel.orbit_eq_iterate {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (μ : FiniteLaw α) (n : ℕ) (x : α) : K.orbit μ n x = (K.iterate n μ).mass x

theorem FD1D.FiniteKernel.orbit_nonneg {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (μ : FiniteLaw α) (n : ℕ) (x : α) : 0 ≤ K.orbit μ n x

theorem FD1D.FiniteKernel.orbit_le_one {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (μ : FiniteLaw α) (n : ℕ) (x : α) : K.orbit μ n x ≤ 1

theorem FD1D.FiniteKernel.sum_orbit {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (μ : FiniteLaw α) (n : ℕ) : ∑ x : α, K.orbit μ n x = 1

theorem FD1D.FiniteKernel.orbit_succ {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (μ : FiniteLaw α) (n : ℕ) : K.orbit μ (n + 1) = Matrix.vecMul (K.orbit μ n) K.matrix

noncomputable def FD1D.FiniteKernel.cesaroVec {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (μ : FiniteLaw α) (n : ℕ) : α → ℝ

The average of the first n+1 orbit vectors.

Equations

• K.cesaroVec μ n = (↑(n + 1))⁻¹ • ∑ k ∈ Finset.range (n + 1), K.orbit μ k

noncomputable def FD1D.FiniteKernel.cesaroLaw {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (μ : FiniteLaw α) (n : ℕ) : FiniteLaw α

Cesaro averages remain probability laws.

Equations

• K.cesaroLaw μ n = { mass := K.cesaroVec μ n, mass_nonneg := ⋯, sum_mass := ⋯ }

theorem FD1D.FiniteKernel.cesaro_step_sub {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (μ : FiniteLaw α) (n : ℕ) : Matrix.vecMul (K.cesaroVec μ n) K.matrix - K.cesaroVec μ n = (↑(n + 1))⁻¹ • (K.orbit μ (n + 1) - K.orbit μ 0)

The one-step error of a Cesaro average is its final endpoint minus its initial endpoint, divided by the averaging length.

theorem FD1D.FiniteKernel.tendsto_cesaro_error {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (μ : FiniteLaw α) : Filter.Tendsto (fun (n : ℕ) => Matrix.vecMul (K.cesaroVec μ n) K.matrix - K.cesaroVec μ n) Filter.atTop (nhds 0)

theorem FD1D.FiniteKernel.exists_stationary {α : Type u_1} [Fintype α] [Nonempty α] (K : FiniteKernel α) : ∃ (μ : FiniteLaw α), K.IsStationary μ

Every finite stochastic kernel on a nonempty state space has a stationary law. The proof takes a convergent subsequence of Cesaro averages in the compact finite probability simplex.

def FD1D.FiniteKernel.Reaches {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (x y : α) : Prop

Reachability by a positive-probability path.

Equations

• K.Reaches x y = ∃ (n : ℕ), 0 < K.pow n x y

def FD1D.FiniteKernel.Irreducible {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) : Prop

Every state can be reached from every other state.

Equations

• K.Irreducible = ∀ (x y : α), K.Reaches x y

theorem FD1D.FiniteKernel.reaches_refl {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (x : α) : K.Reaches x x

theorem FD1D.FiniteKernel.reaches_of_pos {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) {x y : α} (h : 0 < K.trans x y) : K.Reaches x y

theorem FD1D.FiniteKernel.reaches_trans {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) {x y z : α} (hxy : K.Reaches x y) (hyz : K.Reaches y z) : K.Reaches x z

theorem FD1D.FiniteKernel.stationary_mass_pos {α : Type u_1} [Fintype α] [DecidableEq α] {K : FiniteKernel α} (hirr : K.Irreducible) {μ : FiniteLaw α} (hμ : K.IsStationary μ) (y : α) : 0 < μ.mass y

Every state has positive mass under a stationary law of an irreducible finite kernel.

theorem FD1D.FiniteKernel.stationary_unique {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] {K : FiniteKernel α} (hirr : K.Irreducible) {μ ν : FiniteLaw α} (hμ : K.IsStationary μ) (hν : K.IsStationary ν) : μ = ν

An irreducible finite kernel has at most one stationary law.

def FD1D.FiniteKernel.HasPositiveLoops {α : Type u_1} [Fintype α] (K : FiniteKernel α) : Prop

Strictly positive one-step self-loops.

Equations

• K.HasPositiveLoops = ∀ (x : α), 0 < K.trans x x

Equivariance and invariant laws

def FD1D.FiniteKernel.Equivariant {α : Type u_1} [Fintype α] (K : FiniteKernel α) (e : Equiv.Perm α) : Prop

Equivariance of a kernel under a permutation of its state space.

Equations

• K.Equivariant e = ∀ (x y : α), K.trans (e x) (e y) = K.trans x y

def FD1D.FiniteKernel.LawInvariant {α : Type u_1} [Fintype α] (μ : FiniteLaw α) (e : Equiv.Perm α) : Prop

Invariance of a law under a permutation of its state space.

Equations

• FD1D.FiniteKernel.LawInvariant μ e = ∀ (x : α), μ.mass (e x) = μ.mass x

theorem FD1D.FiniteKernel.step_lawInvariant {α : Type u_1} [Fintype α] {K : FiniteKernel α} {μ : FiniteLaw α} {e : Equiv.Perm α} (hK : K.Equivariant e) (hμ : LawInvariant μ e) : LawInvariant (K.step μ) e

theorem FD1D.FiniteKernel.iterate_lawInvariant {α : Type u_1} [Fintype α] {K : FiniteKernel α} {μ : FiniteLaw α} {e : Equiv.Perm α} (hK : K.Equivariant e) (hμ : LawInvariant μ e) (n : ℕ) : LawInvariant (K.iterate n μ) e

def FD1D.FiniteKernel.GroupInvariant {α : Type u_1} [Fintype α] {G : Type u_3} [Group G] (ρ : G →* Equiv.Perm α) (μ : FiniteLaw α) : Prop

A finite group action preserves a law.

Equations

• FD1D.FiniteKernel.GroupInvariant ρ μ = ∀ (g : G), FD1D.FiniteKernel.LawInvariant μ (ρ g)

def FD1D.FiniteKernel.GroupEquivariant {α : Type u_1} [Fintype α] {G : Type u_3} [Group G] (ρ : G →* Equiv.Perm α) (K : FiniteKernel α) : Prop

A finite kernel is equivariant for a group action.

Equations

• FD1D.FiniteKernel.GroupEquivariant ρ K = ∀ (g : G), K.Equivariant (ρ g)

theorem FD1D.FiniteKernel.step_groupInvariant {α : Type u_1} [Fintype α] {G : Type u_3} [Group G] (ρ : G →* Equiv.Perm α) {K : FiniteKernel α} {μ : FiniteLaw α} (hK : GroupEquivariant ρ K) (hμ : GroupInvariant ρ μ) : GroupInvariant ρ (K.step μ)

theorem FD1D.FiniteKernel.iterate_groupInvariant {α : Type u_1} [Fintype α] {G : Type u_3} [Group G] (ρ : G →* Equiv.Perm α) {K : FiniteKernel α} {μ : FiniteLaw α} (hK : GroupEquivariant ρ K) (hμ : GroupInvariant ρ μ) (n : ℕ) : GroupInvariant ρ (K.iterate n μ)

theorem FD1D.FiniteKernel.uniform_groupInvariant {α : Type u_1} [Fintype α] [Nonempty α] {G : Type u_3} [Group G] (ρ : G →* Equiv.Perm α) : GroupInvariant ρ FiniteLaw.uniform

theorem FD1D.FiniteKernel.cesaroLaw_groupInvariant {α : Type u_1} [Fintype α] [DecidableEq α] {G : Type u_3} [Group G] (ρ : G →* Equiv.Perm α) {K : FiniteKernel α} {μ : FiniteLaw α} (hK : GroupEquivariant ρ K) (hμ : GroupInvariant ρ μ) (n : ℕ) : GroupInvariant ρ (K.cesaroLaw μ n)

theorem FD1D.FiniteKernel.exists_stationary_groupInvariant {α : Type u_1} [Fintype α] [Nonempty α] {G : Type u_3} [Group G] (ρ : G →* Equiv.Perm α) (K : FiniteKernel α) (hK : GroupEquivariant ρ K) : ∃ (μ : FiniteLaw α), K.IsStationary μ ∧ GroupInvariant ρ μ

A finite equivariant Markov kernel has a stationary law invariant under the entire finite group action.

Inventory vectors and delete/arrive dynamics

@[reducible, inline]

abbrev FD1D.InventoryState (ι : Type u_1) [Fintype ι] (m : ℕ) : Type u_1

Leaf-count vectors with fixed total inventory m.

Equations

• FD1D.InventoryState ι m = { x : ι → ℕ // ∑ i : ι, x i = m }

theorem FD1D.InventoryState.ext {ι : Type u_1} [Fintype ι] {m : ℕ} {x y : InventoryState ι m} (h : ∀ (i : ι), ↑x i = ↑y i) : x = y

theorem FD1D.InventoryState.ext_iff {ι : Type u_1} [Fintype ι] {m : ℕ} {x y : InventoryState ι m} : x = y ↔ ∀ (i : ι), ↑x i = ↑y i

@[instance_reducible]

noncomputable instance FD1D.InventoryState.instFintype {ι : Type u_1} [Fintype ι] [DecidableEq ι] (m : ℕ) : Fintype (InventoryState ι m)

Equations

• FD1D.InventoryState.instFintype m = Fintype.ofInjective (fun (x : FD1D.InventoryState ι m) (i : ι) => ⟨↑x i, ⋯⟩) ⋯

@[instance_reducible]

noncomputable instance FD1D.InventoryState.instDecidableEq {ι : Type u_1} [Fintype ι] (m : ℕ) : DecidableEq (InventoryState ι m)

Equations

• FD1D.InventoryState.instDecidableEq m = Classical.decEq (FD1D.InventoryState ι m)

def FD1D.InventoryState.move {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (x : InventoryState ι m) (d a : ι) : InventoryState ι m

The count vector after deleting at d and arriving at a. If d is empty, this is defined to be the original state.

Equations

• x.move d a = if hd : 0 < ↑x d then let removed := Function.update (↑x) d (↑x d - 1); ⟨Function.update removed a (removed a + 1), ⋯⟩ else x

@[simp]

theorem FD1D.InventoryState.move_empty {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (x : InventoryState ι m) {d a : ι} (hd : ↑x d = 0) : x.move d a = x

@[simp]

theorem FD1D.InventoryState.move_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (x : InventoryState ι m) (d : ι) : x.move d d = x

theorem FD1D.InventoryState.move_apply_of_pos {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (x : InventoryState ι m) {d a i : ι} (hd : 0 < ↑x d) : ↑(x.move d a) i = (↑x i + if i = a then 1 else 0) - if i = d then 1 else 0

structure FD1D.DeletionRule (ι : Type u_1) [Fintype ι] (m : ℕ) : Type u_1

A deletion rule chooses an occupied leaf, assigning every occupied leaf strictly positive probability.

• prob : InventoryState ι m → ι → ℝ

  Probability of deleting an item from each occupied inventory coordinate.

• nonneg (x : InventoryState ι m) (i : ι) : 0 ≤ self.prob x i
• empty (x : InventoryState ι m) (i : ι) : ↑x i = 0 → self.prob x i = 0
• occupied_pos (x : InventoryState ι m) (i : ι) : 0 < ↑x i → 0 < self.prob x i
• sum_prob (x : InventoryState ι m) : ∑ i : ι, self.prob x i = 1

noncomputable def FD1D.DeletionRule.kernel {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {m : ℕ} (R : DeletionRule ι m) : FiniteKernel (InventoryState ι m)

Transition probability: delete according to R, then independently arrive at a uniformly chosen leaf.

Equations

• R.kernel = { trans := fun (x y : FD1D.InventoryState ι m) => ∑ d : ι, ∑ a : ι, if x.move d a = y then R.prob x d * (1 / ↑(Fintype.card ι)) else 0, trans_nonneg := ⋯, sum_trans := ⋯ }

@[simp]

theorem FD1D.DeletionRule.kernel_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {m : ℕ} (R : DeletionRule ι m) (x y : InventoryState ι m) : R.kernel.trans x y = ∑ d : ι, ∑ a : ι, if x.move d a = y then R.prob x d * (1 / ↑(Fintype.card ι)) else 0

theorem FD1D.DeletionRule.kernel_move_pos {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {m : ℕ} (R : DeletionRule ι m) (x : InventoryState ι m) {d a : ι} (hd : 0 < ↑x d) : 0 < R.kernel.trans x (x.move d a)

Every legal delete/arrive move has positive one-step probability.

theorem FD1D.DeletionRule.one_div_card_le_kernel_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {m : ℕ} (R : DeletionRule ι m) (x : InventoryState ι m) : 1 / ↑(Fintype.card ι) ≤ R.kernel.trans x x

The self-loop probability is at least the uniform arrival mass.

theorem FD1D.DeletionRule.kernel_hasPositiveLoops {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {m : ℕ} (R : DeletionRule ι m) : R.kernel.HasPositiveLoops

theorem FD1D.DeletionRule.kernel_expectation_eq_delete_arrive {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {m : ℕ} (R : DeletionRule ι m) (x : InventoryState ι m) (f : InventoryState ι m → ℝ) : ∑ y : InventoryState ι m, R.kernel.trans x y * f y = ∑ deleted : ι, ∑ arrived : ι, R.prob x deleted * (1 / ↑(Fintype.card ι)) * f (x.move deleted arrived)

Integrating against a deletion kernel amounts to summing over its two moves.