Projection from smooth merging to overlapping tampering sets #
The smooth-source theorem retains the original source copies in T,
all original right data, and the extraction outputs in S. These data
reconstruct every output in S ∪ T: use the stored output on S and
recompute from the retained source copy and original seed otherwise.
Projection preserves the actual prefix and full original right state.
theorem
Algebraic.Cutwidth.Extractor.Internal.smoothIndependenceSourceWeight_eq_map
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{t : ℕ}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(xs : Z → A → Option (Fin t) → X)
(T : Finset (Fin t))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.smoothIndependenceSourceWeight_probability
{Z : Type u_1}
{A : Type u_2}
{X : Type u_3}
{t : ℕ}
[Fintype Z]
[Fintype A]
[Fintype X]
(w : Z → ℝ)
(l : Z → A → ℝ)
(xs : Z → A → Option (Fin t) → X)
(T : Finset (Fin t))
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.smoothIndependenceSeedWeight_eq_map
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{Q : Type u_4}
{Seed : Type u_5}
{t : ℕ}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Q]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(q : Z → A → Q)
(ys : Z × Q → B → Option (Fin t) → Seed)
(S : Finset (Fin t))
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
:
theorem
Algebraic.Cutwidth.Extractor.Internal.smoothIndependenceSeedWeight_probability
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{Q : Type u_4}
{Seed : Type u_5}
{t : ℕ}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Q]
[Fintype Seed]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(q : Z → A → Q)
(ys : Z × Q → B → Option (Fin t) → Seed)
(S : Finset (Fin t))
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (smoothIndependenceSeedWeight w l r q ys S)
theorem
Algebraic.Cutwidth.Extractor.Internal.smoothIndependenceMergingWeight_probability
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Out : Type u_7}
{t : ℕ}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Q]
[Fintype Out]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(xs : Z → A → Option (Fin t) → X)
(q : Z → A → Q)
(ys : Z × Q → B → Option (Fin t) → Seed)
(E : X → Seed → Out)
(S T : Finset (Fin t))
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (smoothIndependenceMergingWeight w l r xs q ys E S T)
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_smooth_independence_merging_dist_le
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Out : Type u_7}
{t : ℕ}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype X]
[Fintype Q]
[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 → ℝ)
(xs : Z → A → Option (Fin t) → X)
(q : Z → A → Q)
(ys : Z × Q → B → Option (Fin t) → Seed)
(S T : Finset (Fin t))
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(source :
weightDist (smoothIndependenceSourceWeight w l xs T) (uniformSecondWeight (smoothIndependenceSourceWeight w l xs T)) ≤ ρ)
(seed :
weightDist (smoothIndependenceSeedWeight w l r q ys S)
(uniformSecondWeight (smoothIndependenceSeedWeight w l r q ys S)) ≤ δ)
:
weightDist (smoothIndependenceMergingWeight w l r xs q ys E S T)
(uniformSecondWeight (smoothIndependenceMergingWeight w l r xs q ys E S T)) ≤ ε + δ + ρ + ↑K * ↑(Fintype.card Out) ^ S.card * ↑(Fintype.card Q) / ↑(Fintype.card X)