Initialization

Refreshed inventory initialization

The refreshed inventory is obtained from m labeled, independently uniform leaf assignments by forgetting the labels and retaining only the fiber cardinalities. The resulting law is invariant under every leaf relabeling.

@[reducible, inline]

abbrev FD1D.Assignment (ι : Type u_1) (m : ℕ) : Type u_1

Assignments of m labeled inventory items to a finite set of locations.

Equations

• FD1D.Assignment ι m = (Fin m → ι)

@[reducible, inline]

abbrev FD1D.DyadicAssignment (L m : ℕ) : Type

Assignments of m labeled inventory items to the depth-L leaves.

Equations

• FD1D.DyadicAssignment L m = FD1D.Assignment (FD1D.DyadicNode L) m

def FD1D.assignmentCount {ι : Type u_1} [DecidableEq ι] {m : ℕ} (ω : Assignment ι m) (i : ι) : ℕ

Number of labels assigned to one location.

Equations

• FD1D.assignmentCount ω i = {j : Fin m | ω j = i}.card

theorem FD1D.sum_assignmentCount {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (ω : Assignment ι m) : ∑ i : ι, assignmentCount ω i = m

Fiber cardinalities partition all m assignment labels.

def FD1D.assignmentState {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (ω : Assignment ι m) : InventoryState ι m

The fixed-total inventory state formed from assignment fiber cardinalities.

Equations

• FD1D.assignmentState ω = ⟨FD1D.assignmentCount ω, ⋯⟩

@[simp]

theorem FD1D.assignmentState_count {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (ω : Assignment ι m) (i : ι) : ↑(assignmentState ω) i = assignmentCount ω i

def FD1D.assignmentPerm {ι : Type u_1} {m : ℕ} (e : Equiv.Perm ι) : Equiv.Perm (Assignment ι m)

Postcompose every assignment with a location permutation.

Equations

• FD1D.assignmentPerm e = (Equiv.refl (Fin m)).arrowCongr e

@[simp]

theorem FD1D.assignmentPerm_apply {ι : Type u_1} {m : ℕ} (e : Equiv.Perm ι) (ω : Assignment ι m) (j : Fin m) : (assignmentPerm e) ω j = e (ω j)

def FD1D.inventoryStatePerm {ι : Type u_1} [Fintype ι] {m : ℕ} (e : Equiv.Perm ι) : Equiv.Perm (InventoryState ι m)

Push a fixed-total count vector forward along a location permutation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FD1D.inventoryStatePerm_count {ι : Type u_1} [Fintype ι] {m : ℕ} (e : Equiv.Perm ι) (x : InventoryState ι m) (i : ι) : ↑((inventoryStatePerm e) x) i = ↑x ((Equiv.symm e) i)

theorem FD1D.inventoryStatePerm_image_count {ι : Type u_1} [Fintype ι] {m : ℕ} (e : Equiv.Perm ι) (x : InventoryState ι m) (i : ι) : ↑((inventoryStatePerm e) x) (e i) = ↑x i

@[simp]

theorem FD1D.assignmentCount_perm {ι : Type u_1} [DecidableEq ι] {m : ℕ} (e : Equiv.Perm ι) (ω : Assignment ι m) (i : ι) : assignmentCount ((assignmentPerm e) ω) (e i) = assignmentCount ω i

Relabeling an assignment relabels its fiber-count state.

theorem FD1D.assignmentState_perm {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (e : Equiv.Perm ι) (ω : Assignment ι m) : assignmentState ((assignmentPerm e) ω) = (inventoryStatePerm e) (assignmentState ω)

The assignment-to-state map is equivariant for the canonical lifts.

theorem FD1D.uniform_map_lawInvariant {A : Type u_1} {B : Type u_2} [Fintype A] [Nonempty A] [Fintype B] [DecidableEq B] (f : A → B) (ea : Equiv.Perm A) (eb : Equiv.Perm B) (h : ∀ (a : A), f (ea a) = eb (f a)) : FiniteKernel.LawInvariant (FiniteLaw.map f FiniteLaw.uniform) eb

A uniform pushforward is invariant under any compatible permutations of its source and target.

noncomputable def FD1D.refreshedLaw (L m : ℕ) : FiniteLaw (InventoryState (DyadicNode L) m)

The refreshed inventory law: choose every labeled item's leaf uniformly and independently, then forget the labels and retain only fiber counts.

Equations

• FD1D.refreshedLaw L m = FD1D.FiniteLaw.map FD1D.assignmentState FD1D.FiniteLaw.uniform

@[simp]

theorem FD1D.refreshedLaw_mass (L m : ℕ) (x : InventoryState (DyadicNode L) m) : (refreshedLaw L m).mass x = ∑ ω : Assignment (DyadicNode L) m with assignmentState ω = x, 1 / ↑(Fintype.card (DyadicAssignment L m))

theorem FD1D.refreshedLaw_lawInvariant_of_compatible {L m : ℕ} (leafPerm : Equiv.Perm (DyadicNode L)) (statePerm : Equiv.Perm (InventoryState (DyadicNode L) m)) (hcompat : ∀ (ω : DyadicAssignment L m), assignmentState ((assignmentPerm leafPerm) ω) = statePerm (assignmentState ω)) : FiniteKernel.LawInvariant (refreshedLaw L m) statePerm

A form parameterized by the target-state permutation, for clients that already define their own lift of a leaf permutation.

theorem FD1D.refreshedLaw_lawInvariant {L m : ℕ} (leafPerm : Equiv.Perm (DyadicNode L)) : FiniteKernel.LawInvariant (refreshedLaw L m) (inventoryStatePerm leafPerm)

The refreshed law is invariant under the canonical lift of every leaf permutation to inventory states.

theorem FD1D.iterate_refreshedLaw_lawInvariant_of_compatible {L m : ℕ} (K : FiniteKernel (InventoryState (DyadicNode L) m)) (leafPerm : Equiv.Perm (DyadicNode L)) (statePerm : Equiv.Perm (InventoryState (DyadicNode L) m)) (hcompat : ∀ (ω : DyadicAssignment L m), assignmentState ((assignmentPerm leafPerm) ω) = statePerm (assignmentState ω)) (hK : K.Equivariant statePerm) (n : ℕ) : FiniteKernel.LawInvariant (K.iterate n (refreshedLaw L m)) statePerm

Kernel equivariance preserves refreshed-law invariance through every iterate, for any compatible state-space lift.

theorem FD1D.iterate_refreshedLaw_lawInvariant {L m : ℕ} (K : FiniteKernel (InventoryState (DyadicNode L) m)) (leafPerm : Equiv.Perm (DyadicNode L)) (hK : K.Equivariant (inventoryStatePerm leafPerm)) (n : ℕ) : FiniteKernel.LawInvariant (K.iterate n (refreshedLaw L m)) (inventoryStatePerm leafPerm)

If a kernel is equivariant under the canonical lift of a leaf permutation, every iterate from the refreshed law remains invariant.