Merging the independence of two selected tampering sets #
Retain the source copies in T, the seed copies in S, and the extracted
outputs in S. The two-sided leakage theorem applies with extra alphabet
S → Out. Its retained data reconstruct every output in S ∪ T, choosing
the stored output on overlaps. Processing that side information preserves
the independent uniform comparison law.
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_independence_merging_dist_le
{Z : Type u_1}
{X : Type u_2}
{Seed : Type u_3}
{Out : Type u_4}
{t : ℕ}
[Fintype Z]
[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 → X × (Fin t → X) → ℝ)
(r : Z → Seed × (Fin t → Seed) → ℝ)
(S T : Finset (Fin t))
(μ : Z × (↥T → X) → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(nonnegative : ∀ (zu : Z × (↥T → X)), 0 ≤ μ zu)
(cap :
∀ (z : Z) (u : ↥T → X) (x : X),
w z * mapWeight (fun (a : X × (Fin t → X)) => (fun (j : ↥T) => a.2 ↑j, a.1)) (l z) (u, x) ≤ μ (z, u))
(seed :
weightDist
(observedSeedWeight w r (fun (x : Z) (b : Seed × (Fin t → Seed)) (j : ↥S) => b.2 ↑j)
fun (x : Z) (b : Seed × (Fin t → Seed)) => b.1)
(uniformSecondWeight
(observedSeedWeight w r (fun (x : Z) (b : Seed × (Fin t → Seed)) (j : ↥S) => b.2 ↑j)
fun (x : Z) (b : Seed × (Fin t → Seed)) => b.1)) ≤ δ)
:
weightDist (independenceMergingWeight w l r E S T) (uniformSecondWeight (independenceMergingWeight w l r E S T)) ≤ ε + δ + ↑K * ↑(Fintype.card Out) ^ S.card * ∑ zu : Z × (↥T → X), μ zu
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_independence_merging_dist_le_of_budget
{Z : Type u_1}
{X : Type u_2}
{Seed : Type u_3}
{Out : Type u_4}
{t : ℕ}
[Fintype Z]
[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 → X × (Fin t → X) → ℝ)
(r : Z → Seed × (Fin t → Seed) → ℝ)
(S T : Finset (Fin t))
(μ : Z × (↥T → X) → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(nonnegative : ∀ (zu : Z × (↥T → X)), 0 ≤ μ zu)
(cap :
∀ (z : Z) (u : ↥T → X) (x : X),
w z * mapWeight (fun (a : X × (Fin t → X)) => (fun (j : ↥T) => a.2 ↑j, a.1)) (l z) (u, x) ≤ μ (z, u))
(seed :
weightDist
(observedSeedWeight w r (fun (x : Z) (b : Seed × (Fin t → Seed)) (j : ↥S) => b.2 ↑j)
fun (x : Z) (b : Seed × (Fin t → Seed)) => b.1)
(uniformSecondWeight
(observedSeedWeight w r (fun (x : Z) (b : Seed × (Fin t → Seed)) (j : ↥S) => b.2 ↑j)
fun (x : Z) (b : Seed × (Fin t → Seed)) => b.1)) ≤ δ)
(budget : ↑K * ↑(Fintype.card Out) ^ S.card * ∑ zu : Z × (↥T → X), μ zu ≤ ε)
:
weightDist (independenceMergingWeight w l r E S T) (uniformSecondWeight (independenceMergingWeight w l r E S T)) ≤ 2 * ε + δ