Symmetry

Local child-swap symmetries

A swap at a depth-d node exchanges its two child subtrees. The permutation is propagated to deeper levels by preserving every subsequent left/right choice. This file also lifts the permutations to inventory states and records the equivariance of the hierarchical policy.

def FD1D.TreeSymmetry.liftNodePerm {k : ℕ} (e : Equiv.Perm (DyadicNode k)) : Equiv.Perm (DyadicNode (k + 1))

Lift a permutation of one tree level to the next level, preserving the left/right choice below every permuted node.

Equations

• FD1D.TreeSymmetry.liftNodePerm e = (FD1D.childrenEquiv k).symm.trans ((Equiv.prodCongr e (Equiv.refl (Fin 2))).trans (FD1D.childrenEquiv k))

@[simp]

theorem FD1D.TreeSymmetry.liftNodePerm_leftChild {k : ℕ} (e : Equiv.Perm (DyadicNode k)) (w : DyadicNode k) : (liftNodePerm e) (leftChild w) = leftChild (e w)

@[simp]

theorem FD1D.TreeSymmetry.liftNodePerm_rightChild {k : ℕ} (e : Equiv.Perm (DyadicNode k)) (w : DyadicNode k) : (liftNodePerm e) (rightChild w) = rightChild (e w)

def FD1D.TreeSymmetry.subtreeSwap {d : ℕ} (v : DyadicNode d) (r : ℕ) : Equiv.Perm (DyadicNode (d + 1 + r))

The permutation at level d+1+r induced by swapping the children of v.

Equations

• FD1D.TreeSymmetry.subtreeSwap v 0 = Equiv.swap (FD1D.leftChild v) (FD1D.rightChild v)
• FD1D.TreeSymmetry.subtreeSwap v r.succ = FD1D.TreeSymmetry.liftNodePerm (FD1D.TreeSymmetry.subtreeSwap v r)

@[simp]

theorem FD1D.TreeSymmetry.subtreeSwap_zero_left {d : ℕ} (v : DyadicNode d) : (subtreeSwap v 0) (leftChild v) = rightChild v

@[simp]

theorem FD1D.TreeSymmetry.subtreeSwap_zero_right {d : ℕ} (v : DyadicNode d) : (subtreeSwap v 0) (rightChild v) = leftChild v

theorem FD1D.TreeSymmetry.subtreeSwap_zero_of_ne {d : ℕ} (v : DyadicNode d) {w : DyadicNode (d + 1)} (hleft : w ≠ leftChild v) (hright : w ≠ rightChild v) : (subtreeSwap v 0) w = w

@[simp]

theorem FD1D.TreeSymmetry.subtreeSwap_succ_leftChild {d r : ℕ} (v : DyadicNode d) (w : DyadicNode (d + 1 + r)) : (subtreeSwap v (r + 1)) (leftChild w) = leftChild ((subtreeSwap v r) w)

@[simp]

theorem FD1D.TreeSymmetry.subtreeSwap_succ_rightChild {d r : ℕ} (v : DyadicNode d) (w : DyadicNode (d + 1 + r)) : (subtreeSwap v (r + 1)) (rightChild w) = rightChild ((subtreeSwap v r) w)

theorem FD1D.TreeSymmetry.liftNodePerm_involutive {k : ℕ} (e : Equiv.Perm (DyadicNode k)) (he : ∀ (w : DyadicNode k), e (e w) = w) (w : DyadicNode (k + 1)) : (liftNodePerm e) ((liftNodePerm e) w) = w

@[simp]

theorem FD1D.TreeSymmetry.subtreeSwap_involutive {d r : ℕ} (v : DyadicNode d) (w : DyadicNode (d + 1 + r)) : (subtreeSwap v r) ((subtreeSwap v r) w) = w

theorem FD1D.TreeSymmetry.subtreeSwap_symm {d r : ℕ} (v : DyadicNode d) : Equiv.symm (subtreeSwap v r) = subtreeSwap v r

def FD1D.TreeSymmetry.ancestorNode {k : ℕ} (r : ℕ) : DyadicNode (k + r) → DyadicNode k

The ancestor r levels above a node.

Equations

• FD1D.TreeSymmetry.ancestorNode 0 w = w
• FD1D.TreeSymmetry.ancestorNode r.succ w = FD1D.TreeSymmetry.ancestorNode r (FD1D.parent w)

@[simp]

theorem FD1D.TreeSymmetry.ancestorNode_zero {k : ℕ} (w : DyadicNode k) : ancestorNode 0 w = w

@[simp]

theorem FD1D.TreeSymmetry.ancestorNode_succ_leftChild {k r : ℕ} (w : DyadicNode (k + r)) : ancestorNode (r + 1) (leftChild w) = ancestorNode r w

@[simp]

theorem FD1D.TreeSymmetry.ancestorNode_succ_rightChild {k r : ℕ} (w : DyadicNode (k + r)) : ancestorNode (r + 1) (rightChild w) = ancestorNode r w

theorem FD1D.TreeSymmetry.subtreeSwap_fixed_of_ancestor_ne {d r : ℕ} (v : DyadicNode d) (w : DyadicNode (d + 1 + r)) (hleft : ancestorNode r w ≠ leftChild v) (hright : ancestorNode r w ≠ rightChild v) : (subtreeSwap v r) w = w

A node outside the two exchanged descendant blocks is fixed pointwise.

theorem FD1D.TreeSymmetry.conjugate_involutive {α : Type u_1} {β : Type u_2} (c : α ≃ β) (e : Equiv.Perm α) (he : ∀ (x : α), e (e x) = x) (y : β) : (c.symm.trans (Equiv.trans e c)) ((c.symm.trans (Equiv.trans e c)) y) = y

Relabeling finite inventories

instance FD1D.TreeSymmetry.inventoryStateNonempty {ι : Type u_1} [Fintype ι] [Nonempty ι] {m : ℕ} : Nonempty (InventoryState ι m)

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

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

Equations

• FD1D.TreeSymmetry.inventoryPerm e = FD1D.inventoryStatePerm e

@[simp]

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

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

def FD1D.TreeSymmetry.leafSwapWithGap {d L : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) : Equiv.Perm (DyadicNode L)

Transport an explicitly iterated subtree swap to a named leaf depth.

Equations

• FD1D.TreeSymmetry.leafSwapWithGap v r hlevel = (Equiv.cast ⋯).symm.trans (Equiv.trans (FD1D.TreeSymmetry.subtreeSwap v r) (Equiv.cast ⋯))

def FD1D.TreeSymmetry.leafSwap {d L : ℕ} (hdL : d < L) (v : DyadicNode d) : Equiv.Perm (DyadicNode L)

The involution of depth-L leaves induced by a child swap at v.

Equations

• FD1D.TreeSymmetry.leafSwap hdL v = FD1D.TreeSymmetry.leafSwapWithGap v (L - (d + 1)) ⋯

def FD1D.TreeSymmetry.inventorySwap {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) : Equiv.Perm (InventoryState (DyadicNode L) m)

The child swap lifted to fixed-total leaf inventories.

Equations

• FD1D.TreeSymmetry.inventorySwap hdL v = FD1D.TreeSymmetry.inventoryPerm (FD1D.TreeSymmetry.leafSwap hdL v)

def FD1D.TreeSymmetry.inventorySwapWithGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) : Equiv.Perm (InventoryState (DyadicNode L) m)

The lifted inventory swap with an explicit depth gap.

Equations

• FD1D.TreeSymmetry.inventorySwapWithGap v r hlevel = FD1D.TreeSymmetry.inventoryPerm (FD1D.TreeSymmetry.leafSwapWithGap v r hlevel)

@[simp]

theorem FD1D.TreeSymmetry.leafSwap_involutive {d L : ℕ} (hdL : d < L) (v : DyadicNode d) (w : DyadicNode L) : (leafSwap hdL v) ((leafSwap hdL v) w) = w

theorem FD1D.TreeSymmetry.leafSwap_symm {d L : ℕ} (hdL : d < L) (v : DyadicNode d) : Equiv.symm (leafSwap hdL v) = leafSwap hdL v

@[simp]

theorem FD1D.TreeSymmetry.leafSwapWithGap_rfl {d n : ℕ} (v : DyadicNode d) : leafSwapWithGap v n ⋯ = subtreeSwap v n

@[simp]

theorem FD1D.TreeSymmetry.inventorySwapWithGap_rfl {d n m : ℕ} (v : DyadicNode d) : inventorySwapWithGap v n ⋯ = inventoryPerm (subtreeSwap v n)

@[simp]

theorem FD1D.TreeSymmetry.inventorySwap_apply_image_count {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (w : DyadicNode L) : ↑((inventorySwap hdL v) x) ((leafSwap hdL v) w) = ↑x w

Canonical aggregate counts under a swap

def FD1D.TreeSymmetry.stateLeafInventory {L m : ℕ} (x : InventoryState (DyadicNode L) m) : LeafInventory L m

Regard a fixed-total state as a leaf inventory.

Equations

• FD1D.TreeSymmetry.stateLeafInventory x = FD1D.HierarchicalDynamics.leafInventory x

def FD1D.TreeSymmetry.stateAggregate {L m : ℕ} (x : InventoryState (DyadicNode L) m) : AggregatedInventory L m

The canonical aggregate counts of a fixed-total state.

Equations

• FD1D.TreeSymmetry.stateAggregate x = FD1D.HierarchicalDynamics.aggregatedInventory x

theorem FD1D.TreeSymmetry.stateAggregate_leaf_count {L m : ℕ} (x : InventoryState (DyadicNode L) m) (w : DyadicNode L) : (stateAggregate x).count L w = ↑x w

def FD1D.TreeSymmetry.singletonInventoryState {L : ℕ} (w : DyadicNode L) : InventoryState (DyadicNode L) 1

The inventory consisting of one item at w.

Equations

• FD1D.TreeSymmetry.singletonInventoryState w = ⟨fun (z : FD1D.DyadicNode L) => if z = w then 1 else 0, ⋯⟩

@[simp]

theorem FD1D.TreeSymmetry.inventoryPerm_singleton {L : ℕ} (e : Equiv.Perm (DyadicNode L)) (w : DyadicNode L) : (inventoryPerm e) (singletonInventoryState w) = singletonInventoryState (e w)

theorem FD1D.TreeSymmetry.stateAggregate_singleton_count {L k : ℕ} (w : DyadicNode L) (hkL : k ≤ L) (u : DyadicNode k) : (stateAggregate (singletonInventoryState w)).count k u = if w ∈ leafBlock hkL u then 1 else 0

theorem FD1D.TreeSymmetry.stateAggregate_count_subtreeSwap {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) {r : ℕ} (hrn : r ≤ n) (w : DyadicNode (d + 1 + r)) : (stateAggregate ((inventoryPerm (subtreeSwap v n)) x)).count (d + 1 + r) ((subtreeSwap v r) w) = (stateAggregate x).count (d + 1 + r) w

Below the swapped children, canonical aggregate counts are carried to the corresponding node by subtreeSwap.

theorem FD1D.TreeSymmetry.stateAggregate_count_swapLevel {d n m : ℕ} (v w : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) : (stateAggregate ((inventoryPerm (subtreeSwap v n)) x)).count d w = (stateAggregate x).count d w

Counts at the level of the swapped node itself are unchanged.

theorem FD1D.TreeSymmetry.stateAggregate_count_aboveSwap {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) {k : ℕ} (hkd : k ≤ d) (w : DyadicNode k) : (stateAggregate ((inventoryPerm (subtreeSwap v n)) x)).count k w = (stateAggregate x).count k w

Every count at or above the swapped node's depth is unchanged.

Action on descendant blocks

theorem FD1D.TreeSymmetry.mem_leafBlock_subtreeSwap_iff {d n s : ℕ} (v : DyadicNode d) (hsn : s ≤ n) (u : DyadicNode (d + 1 + s)) (w : DyadicNode (d + 1 + n)) : (subtreeSwap v n) w ∈ leafBlock ⋯ ((subtreeSwap v s) u) ↔ w ∈ leafBlock ⋯ u

theorem FD1D.TreeSymmetry.leafSwap_exchanges_leftBlock {d n : ℕ} (v : DyadicNode d) (w : DyadicNode (d + 1 + n)) : (subtreeSwap v n) w ∈ leafBlock ⋯ (rightChild v) ↔ w ∈ leafBlock ⋯ (leftChild v)

theorem FD1D.TreeSymmetry.leafSwap_exchanges_rightBlock {d n : ℕ} (v : DyadicNode d) (w : DyadicNode (d + 1 + n)) : (subtreeSwap v n) w ∈ leafBlock ⋯ (leftChild v) ↔ w ∈ leafBlock ⋯ (rightChild v)

theorem FD1D.TreeSymmetry.leafSwap_preserves_otherBlock {d n : ℕ} (v : DyadicNode d) (u : DyadicNode (d + 1)) (hleft : u ≠ leftChild v) (hright : u ≠ rightChild v) (w : DyadicNode (d + 1 + n)) : (subtreeSwap v n) w ∈ leafBlock ⋯ u ↔ w ∈ leafBlock ⋯ u

theorem FD1D.TreeSymmetry.leafSwapWithGap_exchanges_leftBlock {d L : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (w : DyadicNode L) : (leafSwapWithGap v r hlevel) w ∈ leafBlock ⋯ (rightChild v) ↔ w ∈ leafBlock ⋯ (leftChild v)

theorem FD1D.TreeSymmetry.leafSwapWithGap_exchanges_rightBlock {d L : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (w : DyadicNode L) : (leafSwapWithGap v r hlevel) w ∈ leafBlock ⋯ (leftChild v) ↔ w ∈ leafBlock ⋯ (rightChild v)

theorem FD1D.TreeSymmetry.leafSwapWithGap_preserves_otherBlock {d L : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (u : DyadicNode (d + 1)) (hleft : u ≠ leftChild v) (hright : u ≠ rightChild v) (w : DyadicNode L) : (leafSwapWithGap v r hlevel) w ∈ leafBlock ⋯ u ↔ w ∈ leafBlock ⋯ u

theorem FD1D.TreeSymmetry.leafSwap_exchanges_leftBlock_general {d L : ℕ} (hdL : d < L) (v : DyadicNode d) (w : DyadicNode L) : (leafSwap hdL v) w ∈ leafBlock ⋯ (rightChild v) ↔ w ∈ leafBlock ⋯ (leftChild v)

theorem FD1D.TreeSymmetry.leafSwap_exchanges_rightBlock_general {d L : ℕ} (hdL : d < L) (v : DyadicNode d) (w : DyadicNode L) : (leafSwap hdL v) w ∈ leafBlock ⋯ (leftChild v) ↔ w ∈ leafBlock ⋯ (rightChild v)

theorem FD1D.TreeSymmetry.leafSwap_preserves_otherBlock_general {d L : ℕ} (hdL : d < L) (v : DyadicNode d) (u : DyadicNode (d + 1)) (hleft : u ≠ leftChild v) (hright : u ≠ rightChild v) (w : DyadicNode L) : (leafSwap hdL v) w ∈ leafBlock ⋯ u ↔ w ∈ leafBlock ⋯ u

Equivariance of the hierarchical policy

theorem FD1D.TreeSymmetry.hL_swap_counts (a h : ℝ) (x y : ℕ) : LocalHazard.hL a h y x = LocalHazard.hR a h x y

theorem FD1D.TreeSymmetry.hR_swap_counts (a h : ℝ) (x y : ℕ) : LocalHazard.hR a h y x = LocalHazard.hL a h x y

theorem FD1D.TreeSymmetry.policy_hazard_aboveSwap {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) {k : ℕ} (hkd : k ≤ d) (w : DyadicNode k) : HierarchicalPolicy.hazard (stateAggregate ((inventoryPerm (subtreeSwap v n)) x)) a k w = HierarchicalPolicy.hazard (stateAggregate x) a k w

Hazards at every level weakly above the swapped node are unchanged.

theorem FD1D.TreeSymmetry.policy_hazard_subtreeSwap_zero {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) (w : DyadicNode (d + 1)) : HierarchicalPolicy.hazard (stateAggregate ((inventoryPerm (subtreeSwap v n)) x)) a (d + 1) ((subtreeSwap v 0) w) = HierarchicalPolicy.hazard (stateAggregate x) a (d + 1) w

At the first level below v, hazards follow the child swap.

theorem FD1D.TreeSymmetry.policy_hazard_subtreeSwap {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) {r : ℕ} (hrn : r ≤ n) (w : DyadicNode (d + 1 + r)) : HierarchicalPolicy.hazard (stateAggregate ((inventoryPerm (subtreeSwap v n)) x)) a (d + 1 + r) ((subtreeSwap v r) w) = HierarchicalPolicy.hazard (stateAggregate x) a (d + 1 + r) w

Hazards at every descendant node are transported by the tree swap.

theorem FD1D.TreeSymmetry.policy_deletionMass_aboveSwap {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) {k : ℕ} (hkd : k ≤ d) (w : DyadicNode k) : HierarchicalPolicy.deletionMass (stateAggregate ((inventoryPerm (subtreeSwap v n)) x)) a k w = HierarchicalPolicy.deletionMass (stateAggregate x) a k w

Deletion masses at and above the swapped node are unchanged.

theorem FD1D.TreeSymmetry.policy_deletionMass_subtreeSwap {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) {r : ℕ} (hrn : r ≤ n) (w : DyadicNode (d + 1 + r)) : HierarchicalPolicy.deletionMass (stateAggregate ((inventoryPerm (subtreeSwap v n)) x)) a (d + 1 + r) ((subtreeSwap v r) w) = HierarchicalPolicy.deletionMass (stateAggregate x) a (d + 1 + r) w

Deletion masses at descendant nodes are transported by the swap.

theorem FD1D.TreeSymmetry.policy_imbalance_swapNode {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) : HierarchicalPolicy.imbalance (stateAggregate ((inventoryPerm (subtreeSwap v n)) x)) a d v = -HierarchicalPolicy.imbalance (stateAggregate x) a d v

The Haar-type deletion coefficient at the swapped node changes sign.

theorem FD1D.TreeSymmetry.policy_imbalance_strictAncestor {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) {k : ℕ} (hkd : k < d) (w : DyadicNode k) : HierarchicalPolicy.imbalance (stateAggregate ((inventoryPerm (subtreeSwap v n)) x)) a k w = HierarchicalPolicy.imbalance (stateAggregate x) a k w

A strict ancestor's deletion coefficient is unchanged.

Arbitrary-depth wrappers

theorem FD1D.TreeSymmetry.stateAggregate_count_subtreeSwapWithGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (x : InventoryState (DyadicNode L) m) {s : ℕ} (hsr : s ≤ r) (w : DyadicNode (d + 1 + s)) : (stateAggregate ((inventorySwapWithGap v r hlevel) x)).count (d + 1 + s) ((subtreeSwap v s) w) = (stateAggregate x).count (d + 1 + s) w

theorem FD1D.TreeSymmetry.stateAggregate_count_leafSwapWithGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (x : InventoryState (DyadicNode L) m) (w : DyadicNode L) : (stateAggregate ((inventorySwapWithGap v r hlevel) x)).count L ((leafSwapWithGap v r hlevel) w) = (stateAggregate x).count L w

theorem FD1D.TreeSymmetry.stateAggregate_count_aboveSwapWithGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (x : InventoryState (DyadicNode L) m) {k : ℕ} (hkd : k ≤ d) (w : DyadicNode k) : (stateAggregate ((inventorySwapWithGap v r hlevel) x)).count k w = (stateAggregate x).count k w

theorem FD1D.TreeSymmetry.policy_deletionMass_subtreeSwapWithGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (x : InventoryState (DyadicNode L) m) (a : ℝ) {s : ℕ} (hsr : s ≤ r) (w : DyadicNode (d + 1 + s)) : HierarchicalPolicy.deletionMass (stateAggregate ((inventorySwapWithGap v r hlevel) x)) a (d + 1 + s) ((subtreeSwap v s) w) = HierarchicalPolicy.deletionMass (stateAggregate x) a (d + 1 + s) w

theorem FD1D.TreeSymmetry.policy_deletionMass_leafSwapWithGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (x : InventoryState (DyadicNode L) m) (a : ℝ) (w : DyadicNode L) : HierarchicalPolicy.deletionMass (stateAggregate ((inventorySwapWithGap v r hlevel) x)) a L ((leafSwapWithGap v r hlevel) w) = HierarchicalPolicy.deletionMass (stateAggregate x) a L w

theorem FD1D.TreeSymmetry.policy_imbalance_swapNodeWithGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (x : InventoryState (DyadicNode L) m) (a : ℝ) : HierarchicalPolicy.imbalance (stateAggregate ((inventorySwapWithGap v r hlevel) x)) a d v = -HierarchicalPolicy.imbalance (stateAggregate x) a d v

theorem FD1D.TreeSymmetry.policy_imbalance_strictAncestorWithGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (x : InventoryState (DyadicNode L) m) (a : ℝ) {k : ℕ} (hkd : k < d) (w : DyadicNode k) : HierarchicalPolicy.imbalance (stateAggregate ((inventorySwapWithGap v r hlevel) x)) a k w = HierarchicalPolicy.imbalance (stateAggregate x) a k w

theorem FD1D.TreeSymmetry.stateAggregate_count_leafSwap {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (w : DyadicNode L) : (stateAggregate ((inventorySwap hdL v) x)).count L ((leafSwap hdL v) w) = (stateAggregate x).count L w

theorem FD1D.TreeSymmetry.policy_deletionMass_leafSwap {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (a : ℝ) (w : DyadicNode L) : HierarchicalPolicy.deletionMass (stateAggregate ((inventorySwap hdL v) x)) a L ((leafSwap hdL v) w) = HierarchicalPolicy.deletionMass (stateAggregate x) a L w

theorem FD1D.TreeSymmetry.policy_imbalance_swapNode_general {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (a : ℝ) : HierarchicalPolicy.imbalance (stateAggregate ((inventorySwap hdL v) x)) a d v = -HierarchicalPolicy.imbalance (stateAggregate x) a d v

theorem FD1D.TreeSymmetry.policy_imbalance_strictAncestor_general {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (a : ℝ) {k : ℕ} (hkd : k < d) (w : DyadicNode k) : HierarchicalPolicy.imbalance (stateAggregate ((inventorySwap hdL v) x)) a k w = HierarchicalPolicy.imbalance (stateAggregate x) a k w

Generic move and kernel equivariance

theorem FD1D.TreeSymmetry.inventoryPerm_move {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : ℕ} (e : Equiv.Perm ι) (x : InventoryState ι m) (deleted arrived : ι) : (inventoryPerm e) (x.move deleted arrived) = ((inventoryPerm e) x).move (e deleted) (e arrived)

theorem FD1D.TreeSymmetry.deletionKernel_equivariant {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] {m : ℕ} (R : DeletionRule ι m) (e : Equiv.Perm ι) (hprob : ∀ (x : InventoryState ι m) (i : ι), R.prob ((inventoryPerm e) x) (e i) = R.prob x i) : R.kernel.Equivariant (inventoryPerm e)

The concrete hierarchical deletion kernel

@[simp]

theorem FD1D.TreeSymmetry.stateAggregate_eq_aggregatedInventory {L m : ℕ} (x : InventoryState (DyadicNode L) m) : stateAggregate x = HierarchicalDynamics.aggregatedInventory x

theorem FD1D.TreeSymmetry.concrete_aggregateCount_leafSwap {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (w : DyadicNode L) : (HierarchicalDynamics.aggregatedInventory ((inventorySwap hdL v) x)).count L ((leafSwap hdL v) w) = (HierarchicalDynamics.aggregatedInventory x).count L w

theorem FD1D.TreeSymmetry.concrete_deletionMass_leafSwap {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (a : ℝ) (w : DyadicNode L) : HierarchicalPolicy.deletionMass (HierarchicalDynamics.aggregatedInventory ((inventorySwap hdL v) x)) a L ((leafSwap hdL v) w) = HierarchicalPolicy.deletionMass (HierarchicalDynamics.aggregatedInventory x) a L w

theorem FD1D.TreeSymmetry.concrete_imbalance_swapNode {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (a : ℝ) : HierarchicalPolicy.imbalance (HierarchicalDynamics.aggregatedInventory ((inventorySwap hdL v) x)) a d v = -HierarchicalPolicy.imbalance (HierarchicalDynamics.aggregatedInventory x) a d v

theorem FD1D.TreeSymmetry.concrete_imbalance_strictAncestor {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (a : ℝ) {k : ℕ} (hkd : k < d) (w : DyadicNode k) : HierarchicalPolicy.imbalance (HierarchicalDynamics.aggregatedInventory ((inventorySwap hdL v) x)) a k w = HierarchicalPolicy.imbalance (HierarchicalDynamics.aggregatedInventory x) a k w

theorem FD1D.TreeSymmetry.concrete_deletionRule_prob_subtreeSwap {d n m : ℕ} (v : DyadicNode d) (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode (d + 1 + n)) m) (w : DyadicNode (d + 1 + n)) : (HierarchicalDynamics.deletionRule a ha hm).prob ((inventoryPerm (subtreeSwap v n)) x) ((subtreeSwap v n) w) = (HierarchicalDynamics.deletionRule a ha hm).prob x w

theorem FD1D.TreeSymmetry.concrete_kernel_equivariant_subtreeSwap {d n m : ℕ} (v : DyadicNode d) (a : ℝ) (ha : 0 < a) (hm : 0 < m) : (HierarchicalDynamics.kernel a ha hm).Equivariant (inventoryPerm (subtreeSwap v n))

theorem FD1D.TreeSymmetry.concrete_kernel_equivariant_withGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (a : ℝ) (ha : 0 < a) (hm : 0 < m) : (HierarchicalDynamics.kernel a ha hm).Equivariant (inventorySwapWithGap v r hlevel)

theorem FD1D.TreeSymmetry.concrete_kernel_equivariant {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (a : ℝ) (ha : 0 < a) (hm : 0 < m) : (HierarchicalDynamics.kernel a ha hm).Equivariant (inventorySwap hdL v)

Invariant stationary laws for a single permutation

def FD1D.TreeSymmetry.permuteLaw {α : Type u_1} [Fintype α] (e : Equiv.Perm α) (μ : FiniteLaw α) : FiniteLaw α

Push a finite law forward along a permutation, in pointwise form.

Equations

• FD1D.TreeSymmetry.permuteLaw e μ = { mass := fun (x : α) => μ.mass ((Equiv.symm e) x), mass_nonneg := ⋯, sum_mass := ⋯ }

@[simp]

theorem FD1D.TreeSymmetry.permuteLaw_mass {α : Type u_1} [Fintype α] (e : Equiv.Perm α) (μ : FiniteLaw α) (x : α) : (permuteLaw e μ).mass x = μ.mass ((Equiv.symm e) x)

theorem FD1D.TreeSymmetry.permuteLaw_stationary {α : Type u_1} [Fintype α] {K : FiniteKernel α} {μ : FiniteLaw α} {e : Equiv.Perm α} (hK : K.Equivariant e) (hμ : K.IsStationary μ) : K.IsStationary (permuteLaw e μ)

theorem FD1D.TreeSymmetry.stationary_lawInvariant_of_irreducible {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] {K : FiniteKernel α} {μ : FiniteLaw α} {e : Equiv.Perm α} (hirr : K.Irreducible) (hK : K.Equivariant e) (hμ : K.IsStationary μ) : FiniteKernel.LawInvariant μ e

theorem FD1D.TreeSymmetry.concrete_stationary_lawInvariant {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (a : ℝ) (ha : 0 < a) (hm : 0 < m) {μ : FiniteLaw (InventoryState (DyadicNode L) m)} (hirr : (HierarchicalDynamics.kernel a ha hm).Irreducible) (hμ : (HierarchicalDynamics.kernel a ha hm).IsStationary μ) : FiniteKernel.LawInvariant μ (inventorySwap hdL v)