Exact distance averages for two-sided extraction #
The actual joint distance and its uniform-seed counterpart are expectations
of the same statistic in [0,1]. The entire right variable remains in the
actual output tag. Independence conditioned on the transcript makes its
additional values irrelevant to each fixed left-row distance.
theorem
Algebraic.Cutwidth.Extractor.Internal.merging_uniform_expectation
{ι : Type u_1}
{Seed : Type u_2}
[Fintype ι]
[Fintype Seed]
(p f : ι × Seed → ℝ)
:
∑ iy : ι × Seed, uniformSecondWeight p iy * f iy = (∑ y : Seed, ∑ i : ι, firstWeight p i * f (i, y)) / ↑(Fintype.card Seed)
theorem
Algebraic.Cutwidth.Extractor.Internal.merging_seeded_nested_dist
{ι : Type u_1}
{Tag : Type u_2}
{X : Type u_3}
{Seed : Type u_4}
{Out : Type u_5}
[Fintype ι]
[Fintype Tag]
[Fintype X]
[Fintype Seed]
[Fintype Out]
(w : ι → ℝ)
(p : ι → Tag × X → ℝ)
(E : X → Seed → Out)
(nonnegative : ∀ (i : ι), 0 ≤ w i)
:
weightDist
(weightedSeededOutput (fun (tx : (ι × Tag) × X) => w tx.1.1 * p tx.1.1 (tx.1.2, tx.2))
fun (tx : (ι × Tag) × X) (y : Seed) => (tx.1, E tx.2 y))
(seedFamilyWeight fun (x : Seed) =>
uniformExtensionWeight Out (firstWeight fun (tx : (ι × Tag) × X) => w tx.1.1 * p tx.1.1 (tx.1.2, tx.2))) = (∑ y : Seed,
∑ i : ι,
w i * weightDist (mapWeight (fun (tx : Tag × X) => (tx.1, E tx.2 y)) (p i))
(uniformSecondWeight (mapWeight (fun (tx : Tag × X) => (tx.1, E tx.2 y)) (p i)))) / ↑(Fintype.card Seed)
theorem
Algebraic.Cutwidth.Extractor.Internal.mergingDistance_range
{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]
[Nonempty Out]
(l : Z → A → ℝ)
(x : Z → A → X)
(u : Z → A → U)
(leak : Z → V → A → W)
(E : X → Seed → Out)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(p : (Z × V) × Seed)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.twoSidedExtractionWeight_dist_eq
{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 X]
[Fintype Seed]
[Fintype Out]
[Fintype U]
[Fintype V]
[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)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
weightDist (twoSidedExtractionWeight w l r x y u v leak E)
(uniformSecondWeight (twoSidedExtractionWeight w l r x y u v leak E)) = ∑ p : (Z × V) × Seed, observedSeedWeight w r v y p * mergingDistance l x u leak E p
theorem
Algebraic.Cutwidth.Extractor.Internal.leakageSourceWeight_dist_eq
{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 X]
[Fintype Seed]
[Fintype Out]
[Fintype U]
[Fintype V]
[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)
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
weightDist
(weightedSeededOutput (leakageSourceWeight w l r x u v leak) fun (tx : ((Z × V) × U × W) × X) (seed : Seed) =>
(tx.1, E tx.2 seed))
(seedFamilyWeight fun (x_1 : Seed) =>
uniformExtensionWeight Out (firstWeight (leakageSourceWeight w l r x u v leak))) = ∑ p : (Z × V) × Seed, uniformSecondWeight (observedSeedWeight w r v y) p * mergingDistance l x u leak E p