Alternating extraction retaining selected tampered outputs #
A nearly uniform left seed supplies a right extraction while retaining all executed left seeds and any chosen set of actual tampered outputs. The original right-source envelope pays only the selected output alphabet. The law equals the observed seed law after fixing all left seeds, making it suitable for the following extraction on the original left source.
This is the finite alternating step in Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1: https://arxiv.org/pdf/2110.12652.
theorem
Algebraic.Cutwidth.Extractor.alternatingCopiesWeight_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}
{t : ℕ}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Seed]
[Fintype Out]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(ss : Z → A → Option (Fin t) → Seed)
(xs : Z → B → Option (Fin t) → X)
(E : X → Seed → Out)
(S : Finset (Fin t))
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (alternatingCopiesWeight w l r ss xs E S)
Actual alternating extraction preserves normalization.
theorem
Algebraic.Cutwidth.Extractor.alternatingCopiesWeight_eq_observed
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Seed : Type u_5}
{Out : Type u_6}
{t : ℕ}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Seed]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(ss : Z → A → Option (Fin t) → Seed)
(xs : Z → B → Option (Fin t) → X)
(E : X → Seed → Out)
(S : Finset (Fin t))
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
:
alternatingCopiesWeight w l r ss xs E S = observedSeedWeight (observedTranscriptWeight w l ss) (fun (zs : Z × (Option (Fin t) → Seed)) => r zs.1)
(fun (zs : Z × (Option (Fin t) → Seed)) (b : B) (j : ↥S) => E (xs zs.1 b (some ↑j)) (zs.2 (some ↑j)))
fun (zs : Z × (Option (Fin t) → Seed)) (b : B) => E (xs zs.1 b none) (zs.2 none)
Fixing all executed seeds gives exactly the next observed seed law.
theorem
Algebraic.Cutwidth.Extractor.WeightedStrongSeededExtractor.alternating_copies_dist_le
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Seed : Type u_5}
{Out : Type u_6}
{t : ℕ}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype X]
[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 → ℝ)
(ss : Z → A → Option (Fin t) → Seed)
(xs : Z → B → Option (Fin t) → X)
(S : Finset (Fin t))
(μ : Z → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(nonnegative : ∀ (z : Z), 0 ≤ μ z)
(cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (fun (b : B) => xs z b none) (r z) x₀ ≤ μ z)
(seed :
weightDist
(observedSeedWeight w l (fun (z : Z) (a : A) (j : ↥S) => ss z a (some ↑j)) fun (z : Z) (a : A) => ss z a none)
(uniformSecondWeight
(observedSeedWeight w l (fun (z : Z) (a : A) (j : ↥S) => ss z a (some ↑j)) fun (z : Z) (a : A) =>
ss z a none)) ≤ δ)
:
weightDist (alternatingCopiesWeight w l r ss xs E S) (uniformSecondWeight (alternatingCopiesWeight w l r ss xs E S)) ≤ ε + δ + ↑K * ↑(Fintype.card Out) ^ S.card * ∑ z : Z, μ z
Original source and seed bounds control all selected actual tampered outputs.