Initial seeds from an exactly uniform repaired state #
A map that sends the uniform state law to the uniform seed law preserves uniformity given an arbitrary transcript. The hypothesis is a weighted marginal identity, so the calculation also includes transcript rows of mass zero. This is the seed step after repairing a nearly uniform state.
theorem
Algebraic.Cutwidth.Extractor.Internal.retainedSeedWeight_image_dist_le
{Z : Type u_1}
{B : Type u_2}
{Q : Type u_3}
{Seed : Type u_4}
[Fintype Z]
[Fintype B]
[Fintype Q]
[Fintype Seed]
(w : Z → ℝ)
(r : Z → B → ℝ)
(q : Z → B → Q)
(initialSeed : Q → Seed)
(balanced : mapWeight initialSeed (uniformWeight Q) = uniformWeight Seed)
:
weightDist (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b))
(uniformSecondWeight (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b))) ≤ weightDist (retainedSeedWeight w r q) (uniformSecondWeight (retainedSeedWeight w r q))
theorem
Algebraic.Cutwidth.Extractor.Internal.retainedSeedWeight_uniform_image
{Z : Type u_1}
{B : Type u_2}
{Q : Type u_3}
{Seed : Type u_4}
[Fintype Z]
[Fintype B]
[Fintype Q]
[Fintype Seed]
(w : Z → ℝ)
(r : Z → B → ℝ)
(q : Z → B → Q)
(initialSeed : Q → Seed)
(balanced : mapWeight initialSeed (uniformWeight Q) = uniformWeight Seed)
(uniform : ∀ (z : Z) (u : Q), w z * mapWeight (q z) (r z) u = w z * uniformWeight Q u)
:
theorem
Algebraic.Cutwidth.Extractor.Internal.retainedSeedWeight_uniform_image_dist
{Z : Type u_1}
{B : Type u_2}
{Q : Type u_3}
{Seed : Type u_4}
[Fintype Z]
[Fintype B]
[Fintype Q]
[Fintype Seed]
[Nonempty Seed]
(w : Z → ℝ)
(r : Z → B → ℝ)
(q : Z → B → Q)
(initialSeed : Q → Seed)
(balanced : mapWeight initialSeed (uniformWeight Q) = uniformWeight Seed)
(uniform : ∀ (z : Z) (u : Q), w z * mapWeight (q z) (r z) u = w z * uniformWeight Q u)
:
weightDist (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b))
(uniformSecondWeight (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b))) = 0