Finite factorization identities for two-sided leakage

The actual observations preserve multiplicities. Regrouping product tags exposes normalized left rows and the exact right observation law; the row envelope is charged once for every value of the additional finite leak.

theorem Algebraic.Cutwidth.Extractor.Internal.merging_probability_tagged {ι : Type u_1} {α : Type u_2} [Fintype ι] [Fintype α] {w : ι → ℝ} {p : ι → α → ℝ} (hw : IsProbabilityWeight w) (hp : ∀ (i : ι), IsProbabilityWeight (p i)) : IsProbabilityWeight fun (ix : ι × α) => w ix.1 * p ix.1 ix.2

theorem Algebraic.Cutwidth.Extractor.Internal.merging_probability_nested {ι : Type u_1} {α : Type u_2} {β : Type u_3} [Fintype ι] [Fintype α] [Fintype β] {w : ι → ℝ} {p : ι → α × β → ℝ} (hw : IsProbabilityWeight w) (hp : ∀ (i : ι), IsProbabilityWeight (p i)) : IsProbabilityWeight fun (ix : (ι × α) × β) => w ix.1.1 * p ix.1.1 (ix.1.2, ix.2)

theorem Algebraic.Cutwidth.Extractor.Internal.merging_sum_mapWeight_mul {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : α → ℝ) (f : α → β) (g : β → ℝ) : ∑ b : β, mapWeight f p b * g b = ∑ a : α, p a * g (f a)

theorem Algebraic.Cutwidth.Extractor.Internal.merging_map_nested {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Fintype ι] [Fintype α] [Fintype β] (w : ι → ℝ) (p : ι → α × β → ℝ) (f : ι → β → γ) : (mapWeight (fun (itx : (ι × α) × β) => (itx.1, f itx.1.1 itx.2)) fun (itx : (ι × α) × β) => w itx.1.1 * p itx.1.1 (itx.1.2, itx.2)) = fun (ito : (ι × α) × γ) => w ito.1.1 * mapWeight (fun (tx : α × β) => (tx.1, f ito.1.1 tx.2)) (p ito.1.1) (ito.1.2, ito.2)

theorem Algebraic.Cutwidth.Extractor.Internal.merging_map_refinement_le {α : Type u_1} {U : Type u_2} {W : Type u_3} {X : Type u_4} [Fintype α] (p : α → ℝ) (nonnegative : ∀ (a : α), 0 ≤ p a) (u : α → U) (leak : α → W) (x : α → X) (u₀ : U) (w₀ : W) (x₀ : X) : mapWeight (fun (a : α) => ((u a, leak a), x a)) p ((u₀, w₀), x₀) ≤ mapWeight (fun (a : α) => (u a, x a)) p (u₀, x₀)

noncomputable def Algebraic.Cutwidth.Extractor.Internal.mergingLeftWeight {Z : Type u_1} {A : Type u_2} {X : Type u_4} {U : Type u_7} {V : Type u_8} {W : Type u_9} [Fintype A] (l : Z → A → ℝ) (x : Z → A → X) (u : Z → A → U) (leak : Z → V → A → W) (zv : Z × V) : (U × W) × X → ℝ

The left source together with its two observations at a fixed right transcript.

Equations

• Algebraic.Cutwidth.Extractor.Internal.mergingLeftWeight l x u leak zv = Algebraic.Cutwidth.Extractor.mapWeight (fun (a : A) => ((u zv.1 a, leak zv.1 zv.2 a), x zv.1 a)) (l zv.1)

noncomputable def Algebraic.Cutwidth.Extractor.Internal.mergingOutputWeight {X : Type u_4} {Seed : Type u_5} {Out : Type u_6} {U : Type u_7} {W : Type u_9} [Fintype X] [Fintype U] [Fintype W] (p : (U × W) × X → ℝ) (E : X → Seed → Out) (y : Seed) : (U × W) × Out → ℝ

Extract from a fixed left joint source while keeping both of its observations.

Equations

• Algebraic.Cutwidth.Extractor.Internal.mergingOutputWeight p E y = Algebraic.Cutwidth.Extractor.mapWeight (fun (tx : (U × W) × X) => (tx.1, E tx.2 y)) p

noncomputable def Algebraic.Cutwidth.Extractor.Internal.mergingDistance {Z : Type u_1} {A : Type u_2} {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] [Fintype X] [Fintype Out] [Fintype U] [Fintype W] (l : Z → A → ℝ) (x : Z → A → X) (u : Z → A → U) (leak : Z → V → A → W) (E : X → Seed → Out) (p : (Z × V) × Seed) : ℝ

The seed-by-seed discrepancy of a fixed pair of transcript values.

Equations

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

theorem Algebraic.Cutwidth.Extractor.Internal.mergingLeftWeight_probability {Z : Type u_1} {A : Type u_2} {X : Type u_4} {U : Type u_7} {V : Type u_8} {W : Type u_9} [Fintype A] [Fintype X] [Fintype U] [Fintype W] (l : Z → A → ℝ) (x : Z → A → X) (u : Z → A → U) (leak : Z → V → A → W) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (zv : Z × V) : IsProbabilityWeight (mergingLeftWeight l x u leak zv)

theorem Algebraic.Cutwidth.Extractor.Internal.mergingOutputWeight_probability {X : Type u_4} {Seed : Type u_5} {Out : Type u_6} {U : Type u_7} {W : Type u_9} [Fintype X] [Fintype Out] [Fintype U] [Fintype W] (p : (U × W) × X → ℝ) (E : X → Seed → Out) (hp : IsProbabilityWeight p) (y : Seed) : IsProbabilityWeight (mergingOutputWeight p E y)

theorem Algebraic.Cutwidth.Extractor.Internal.mergingOutputWeight_left {Z : Type u_1} {A : Type u_2} {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] [Fintype X] [Fintype U] [Fintype W] (l : Z → A → ℝ) (x : Z → A → X) (u : Z → A → U) (leak : Z → V → A → W) (E : X → Seed → Out) (zv : Z × V) (y : Seed) : mergingOutputWeight (mergingLeftWeight l x u leak zv) E y = mapWeight (fun (a : A) => ((u zv.1 a, leak zv.1 zv.2 a), E (x zv.1 a) y)) (l zv.1)

theorem Algebraic.Cutwidth.Extractor.Internal.observedSeedWeight_probability {Z : Type u_1} {B : Type u_3} {Seed : Type u_5} {V : Type u_8} [Fintype Z] [Fintype B] [Fintype Seed] [Fintype V] (w : Z → ℝ) (r : Z → B → ℝ) (v : Z → B → V) (y : Z → B → Seed) (hw : IsProbabilityWeight w) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (observedSeedWeight w r v y)

theorem Algebraic.Cutwidth.Extractor.Internal.observedSeedWeight_first {Z : Type u_1} {B : Type u_3} {Seed : Type u_5} {V : Type u_8} [Fintype Z] [Fintype B] [Fintype Seed] [Fintype V] (w : Z → ℝ) (r : Z → B → ℝ) (v : Z → B → V) (y : Z → B → Seed) : firstWeight (observedSeedWeight w r v y) = fun (zv : Z × V) => w zv.1 * mapWeight (v zv.1) (r zv.1) zv.2

theorem Algebraic.Cutwidth.Extractor.Internal.leakageSourceWeight_probability {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 Z] [Fintype A] [Fintype B] [Fintype X] [Fintype U] [Fintype V] [Fintype W] (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) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (leakageSourceWeight w l r x u v leak)

theorem Algebraic.Cutwidth.Extractor.Internal.twoSidedExtractionWeight_probability {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 Z] [Fintype A] [Fintype B] [Fintype Out] [Fintype U] [Fintype W] (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) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (twoSidedExtractionWeight w l r x y u v leak E)

theorem Algebraic.Cutwidth.Extractor.Internal.twoSidedExtractionWeight_eq_map {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 Z] [Fintype A] [Fintype B] (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) : twoSidedExtractionWeight w l r x y u v leak E = mapWeight (fun (p : (Z × B) × A) => ((p.1, u p.1.1 p.2, leak p.1.1 (v p.1.1 p.1.2) p.2), E (x p.1.1 p.2) (y p.1.1 p.1.2))) (factoredWeight w l r)