Actual joint laws of two-round look-ahead extraction #
The first call extracts from the left input using a prefix of the right input. The next call extracts from the original right input using that first output, and the final call returns to the original left input. Honest and tampered inputs are arbitrary functions of their respective complete side states. The retained variables include the tampered first output; the tampered second seed is determined by these variables.
noncomputable def
Algebraic.Cutwidth.Extractor.lookAheadSeedWeight
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Mid : Type u_7}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
:
The actual second seed, retaining both initial seeds and the complete left state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
Algebraic.Cutwidth.Extractor.lookAheadExtractionWeight
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Mid : Type u_7}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
:
The actual second left output, retaining the full right state and both first outputs.
Equations
- One or more equations did not get rendered due to their size.