Alternating extraction with finite tampered-output leakage #
Swap the original independent factors, retain the complete opposite state, and charge the selected output alphabet to the original source envelope. Projecting the retained opposite state to every actual seed gives precisely the next observed seed law. The sources are never resampled.
theorem
Algebraic.Cutwidth.Extractor.Internal.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)
theorem
Algebraic.Cutwidth.Extractor.Internal.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)
theorem
Algebraic.Cutwidth.Extractor.Internal.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