Adding a fresh seed while retaining earlier seeds

The input is a joint weighting of an earlier seed and a current source. One fresh independent uniform seed is sampled, a deterministic map is applied, and both seeds are kept in their original order. The definitions are total on arbitrary real weights, with the existing zero-mass convention for empty seed types.

def Algebraic.Cutwidth.Extractor.retainSeedEquiv (Earlier : Type u_1) (Fresh : Type u_2) (Ω : Type u_3) : Fresh × Earlier × Ω ≃ (Earlier × Fresh) × Ω

Put the earlier seed first while retaining the newly sampled seed.

Equations

• Algebraic.Cutwidth.Extractor.retainSeedEquiv Earlier Fresh Ω = (Equiv.prodAssoc Fresh Earlier Ω).symm.trans ((Equiv.prodComm Fresh Earlier).prodCongr (Equiv.refl Ω))

noncomputable def Algebraic.Cutwidth.Extractor.retainedSeedStep {Earlier : Type u_1} {Fresh : Type u_2} {X : Type u_3} {Ω : Type u_4} [Fintype Earlier] [Fintype Fresh] [Fintype X] [Fintype Ω] (F : Earlier → X → Fresh → Ω) (r : Earlier × X → ℝ) : (Earlier × Fresh) × Ω → ℝ

Sample a fresh independent uniform seed, apply F, and retain both seeds.

Equations

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