Finite laws for extraction with two-sided leakage

A transcript indexes independent left and right distributions. The source and its first leak depend on the left variable; the seed and its transcript depend on the right variable. An additional finite leak may depend on the left variable and the right transcript together. All maps count every source occurrence, including collisions. The laws remain defined for arbitrary real weights; normalization and independence are hypotheses of the theorems.

These finite laws support the independence-merging argument of Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Lemma 3.26, https://arxiv.org/abs/2110.12652.

noncomputable def Algebraic.Cutwidth.Extractor.factoredWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (p : (Z × B) × A) : ℝ

Independent left and right laws conditioned on a shared transcript, retaining the right tag.

Equations

• Algebraic.Cutwidth.Extractor.factoredWeight w l r p = w p.1.1 * r p.1.1 p.1.2 * l p.1.1 p.2

noncomputable def Algebraic.Cutwidth.Extractor.observedSeedWeight {Z : Type u_1} {B : Type u_3} {Seed : Type u_5} {V : Type u_8} [Fintype Z] [Fintype B] (w : Z → ℝ) (r : Z → B → ℝ) (v : Z → B → V) (y : Z → B → Seed) : (Z × V) × Seed → ℝ

The joint law of the transcript, right-side observation, and actual seed.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.leakageSourceWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {U : Type u_7} {V : Type u_8} {W : Type u_9} [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (u : Z → A → U) (v : Z → B → V) (leak : Z → V → A → W) (p : ((Z × V) × U × W) × X) : ℝ

The source law retaining both observations and the additional finite leak.

Equations

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

noncomputable def Algebraic.Cutwidth.Extractor.twoSidedExtractionWeight {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Seed : Type u_5} {Out : Type u_6} {U : Type u_7} {V : Type u_8} {W : Type u_9} [Fintype A] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (y : Z → B → Seed) (u : Z → A → U) (v : Z → B → V) (leak : Z → V → A → W) (E : X → Seed → Out) (p : ((Z × B) × U × W) × Out) : ℝ

Extraction retaining the full right variable, the left observation, and the extra leak.

Equations

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