Actual laws for smooth independence merging

The original left state determines the honest source, every tampered source, and the actual prefix. The original right state determines all seeds after that prefix. The two sides are independent only conditional on the original transcript; observing the prefix is an exact update of that factored law. Source and seed hypotheses concern their actual joint laws, and the output retains the original right state and prefix.

These definitions support the smooth-source independence-merging step in Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Theorem 6.1, using Lemma 3.26: https://arxiv.org/abs/2110.12652. No statistical claim is part of the definitions.

noncomputable def Algebraic.Cutwidth.Extractor.smoothIndependenceSourceWeight {Z : Type u_1} {A : Type u_2} {X : Type u_3} {t : ℕ} [Fintype Z] [Fintype A] (w : Z → ℝ) (l : Z → A → ℝ) (xs : Z → A → Option (Fin t) → X) (T : Finset (Fin t)) : (Z × (↥T → X)) × X → ℝ

The honest original source together with the selected original tampered source copies.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.smoothIndependenceSeedWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} {Q : Type u_4} {Seed : Type u_5} {t : ℕ} [Fintype Z] [Fintype A] [Fintype B] [Fintype Q] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (q : Z → A → Q) (ys : Z × Q → B → Option (Fin t) → Seed) (S : Finset (Fin t)) : ((Z × Q) × (↥S → Seed)) × Seed → ℝ

Actual seed copies after the original left prefix, retaining the selected tampered seeds.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.smoothIndependenceMergingWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Out : Type u_7} {t : ℕ} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (xs : Z → A → Option (Fin t) → X) (q : Z → A → Q) (ys : Z × Q → B → Option (Fin t) → Seed) (E : X → Seed → Out) (S T : Finset (Fin t)) : (((Z × Q) × B) × (↥(S ∪ T) → Out)) × Out → ℝ

Actual extraction retaining the original prefix, full right state, and union of tamperings.

Equations

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