Actual laws of an alternating extraction step #
A right-side message is revealed before the left side supplies the next seed. The extraction output retains that message and the entire left state. These laws use the original joint distribution, rather than a newly sampled independent copy of either source.
noncomputable def
Algebraic.Cutwidth.Extractor.alternatingSeedWeight
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{V : Type u_4}
{Seed : Type u_5}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(v : Z → B → V)
(s : Z × V → A → Seed)
:
The actual next seed, retaining the transcript and the preceding right message.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algebraic.Cutwidth.Extractor.alternatingExtractionWeight
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{V : Type u_4}
{X : Type u_5}
{Seed : Type u_6}
{Out : Type u_7}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(v : Z → B → V)
(s : Z × V → A → Seed)
(x : Z → B → X)
(E : X → Seed → Out)
:
Extract from the right source using the left seed, retaining all of the left state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algebraic.Cutwidth.Extractor.affineAlternatingWeight
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Seed : Type u_5}
{Mid : Type u_6}
{Y : Type u_7}
{Out : Type u_8}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(mask : Z → B → X)
(y : Z → B → Seed)
(source : Z → B → Y)
(combine : X → X → X)
(E : X → Seed → Mid)
(F : Y → Mid → Out)
:
An actual affine extraction supplies the seed for extraction from the right source. The retained right message consists only of the first seed and extracted mask.
Equations
- One or more equations did not get rendered due to their size.