The block sigma equivalence

The block enumeration pairs a block index with an offset within the block to enumerate the concatenated total.

def RS.blockSigmaSplitFun (d : ℕ) (ds : List ℕ) : (v : Fin (ds.length + 1)) × Fin ((d :: ds).get v) → Fin d ⊕ (w : Fin ds.length) × Fin (ds.get w)

Split the sigma over a cons list into head + tail.

Equations

• RS.blockSigmaSplitFun d ds ⟨⟨0, isLt⟩, j⟩ = Sum.inl j
• RS.blockSigmaSplitFun d ds ⟨⟨v.succ, hv⟩, j⟩ = Sum.inr ⟨⟨v, ⋯⟩, j⟩

def RS.blockSigmaSplitInv (d : ℕ) (ds : List ℕ) : Fin d ⊕ (w : Fin ds.length) × Fin (ds.get w) → (v : Fin (ds.length + 1)) × Fin ((d :: ds).get v)

Inverse of the split.

Equations

• RS.blockSigmaSplitInv d ds (Sum.inl j) = ⟨⟨0, ⋯⟩, j⟩
• RS.blockSigmaSplitInv d ds (Sum.inr ⟨w, j⟩) = ⟨w.succ, j⟩

def RS.blockSigmaSplit (d : ℕ) (ds : List ℕ) : (v : Fin (ds.length + 1)) × Fin ((d :: ds).get v) ≃ Fin d ⊕ (w : Fin ds.length) × Fin (ds.get w)

The sigma over a cons list splits as head + tail.

Equations

• RS.blockSigmaSplit d ds = { toFun := RS.blockSigmaSplitFun d ds, invFun := RS.blockSigmaSplitInv d ds, left_inv := ⋯, right_inv := ⋯ }

noncomputable def RS.blockSigmaEquiv (ds : List ℕ) : (v : Fin ds.length) × Fin (ds.get v) ≃ Fin ds.sum

The block enumeration: a block index and an offset within the block enumerate the concatenated total.

Equations

• RS.blockSigmaEquiv [] = Equiv.equivOfIsEmpty ((v : Fin [].length) × Fin ([].get v)) (Fin [].sum)
• RS.blockSigmaEquiv (d :: ds) = (RS.blockSigmaSplit d ds).trans (((Equiv.refl (Fin d)).sumCongr (RS.blockSigmaEquiv ds)).trans (finSumFinEquiv.trans (finCongr ⋯)))

theorem RS.blockAssign_blockSigmaEquiv (ds : List ℕ) (p : (v : Fin ds.length) × Fin (ds.get v)) : blockAssign ds ((blockSigmaEquiv ds) p) = p.fst

The block enumeration lands in its own block.