Extracting from a uniform coordinate after an actual finite prefix #
Uniformity is only required before observing the prefix. Each observed joint source mass is bounded by the old transcript weight divided by the source alphabet size. Summing over prefix values pays exactly that alphabet's cardinality. This lemma will consume a constructed coordinate repair, rather than assume the original smooth source has a pointwise cap.
theorem
Algebraic.Cutwidth.Extractor.Internal.smoothPrefixExtractionWeight_uniform_dist_le
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{V : Type u_6}
{W : Type u_7}
{Seed : Type u_8}
{Out : Type u_9}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype X]
[Fintype Q]
[Fintype V]
[Fintype W]
[Fintype Seed]
[Fintype Out]
[Nonempty Seed]
[Nonempty Out]
{E : X → Seed → Out}
{K : ℕ}
{ε δ : ℝ}
(extract : WeightedStrongSeededExtractor E K ε)
(error : 0 ≤ ε)
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(q : Z → A → Q)
(v : Z × Q → B → V)
(y : Z × Q → B → Seed)
(leak : Z × Q → V → A → W)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(uniform : ∀ (z : Z), mapWeight (x z) (l z) = uniformWeight X)
(seed : weightDist (smoothPrefixSeedWeight w l r q v y) (uniformSecondWeight (smoothPrefixSeedWeight w l r q v y)) ≤ δ)
:
weightDist (smoothPrefixExtractionWeight w l r x q v y leak E)
(uniformSecondWeight (smoothPrefixExtractionWeight w l r x q v y leak E)) ≤ ε + δ + ↑K * ↑(Fintype.card W) * ↑(Fintype.card Q) / ↑(Fintype.card X)