Actual alternating extraction with selected tamperings #
Every left seed and right source copy is read from the original factored sample. The law retains all executed left seeds and the chosen tampered outputs. It is the alternating step of Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1: https://arxiv.org/pdf/2110.12652.
noncomputable def
Algebraic.Cutwidth.Extractor.alternatingCopiesWeight
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Seed : Type u_5}
{Out : Type u_6}
{t : ℕ}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(ss : Z → A → Option (Fin t) → Seed)
(xs : Z → B → Option (Fin t) → X)
(E : X → Seed → Out)
(S : Finset (Fin t))
:
The actual right extraction retains all left seeds and selected tampered outputs.
Equations
- One or more equations did not get rendered due to their size.