Joint law for finite independence merging

The left variable contains a source and all its tampered copies. The right variable contains a seed and all its tampered copies. Their conditional laws are independent given a shared transcript. The output law retains the entire right variable, the transcript, and every tampered extraction indexed by the union of two supplied sets. The sets may overlap.

This is the finite law in Chattopadhyay--Liao, Extractors for Sum of Two Sources, Lemma 3.26: https://arxiv.org/pdf/2110.12652.

noncomputable def Algebraic.Cutwidth.Extractor.independenceMergingWeight {Z : Type u_1} {X : Type u_2} {Seed : Type u_3} {Out : Type u_4} {t : ℕ} [Fintype Z] [Fintype X] [Fintype Seed] (w : Z → ℝ) (l : Z → X × (Fin t → X) → ℝ) (r : Z → Seed × (Fin t → Seed) → ℝ) (E : X → Seed → Out) (S T : Finset (Fin t)) : ((Z × Seed × (Fin t → Seed)) × (↥(S ∪ T) → Out)) × Out → ℝ

Extract while retaining the transcript, every seed, and the chosen tampered outputs.

Equations

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