Adaptive witnesses and finite bad-seed counting #
Choose one actual shift and tuple of tampered seeds on each bad honest seed. The average bound for this deterministic choice controls the sum over the bad set. No rowwise discrepancy or source normalization is used in the counting argument.
theorem
Algebraic.Cutwidth.Extractor.Internal.affineLeakageOutputWeight_probability
{n d t : ℕ}
{Out : Type u_1}
[Fintype Out]
(cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Out)
(p : (Fin n → Bool) → ℝ)
(leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool)
(advice : Option (Fin t) → List Bool)
(b : Fin n → Bool)
(y : Fin d → Bool)
(ys : Fin t → Fin d → Bool)
(probability : IsProbabilityWeight p)
:
IsProbabilityWeight (affineLeakageOutputWeight cb p leak advice b y ys)
theorem
Algebraic.Cutwidth.Extractor.Internal.mem_affineLeakageBadSeeds
{n d t : ℕ}
{Out : Type u_1}
[Fintype Out]
(cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Out)
(p : (Fin n → Bool) → ℝ)
(leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool)
(advice : Option (Fin t) → List Bool)
(γ : ℝ)
(y : Fin d → Bool)
:
y ∈ affineLeakageBadSeeds cb p leak advice γ ↔ ∃ (b : Fin n → Bool) (ys : Fin t → Fin d → Bool),
γ < weightDist (affineLeakageOutputWeight cb p leak advice b y ys)
(uniformSecondWeight (affineLeakageOutputWeight cb p leak advice b y ys))
theorem
Algebraic.Cutwidth.Extractor.Internal.not_mem_affineLeakageBadSeeds
{n d t : ℕ}
{Out : Type u_1}
[Fintype Out]
(cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Out)
(p : (Fin n → Bool) → ℝ)
(leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool)
(advice : Option (Fin t) → List Bool)
(γ : ℝ)
(y : Fin d → Bool)
:
y ∉ affineLeakageBadSeeds cb p leak advice γ ↔ ∀ (b : Fin n → Bool) (ys : Fin t → Fin d → Bool),
weightDist (affineLeakageOutputWeight cb p leak advice b y ys)
(uniformSecondWeight (affineLeakageOutputWeight cb p leak advice b y ys)) ≤ γ
theorem
Algebraic.Cutwidth.Extractor.Internal.affineLeakageBadSeeds_card_le
{n d t : ℕ}
{Out : Type u_1}
[Fintype Out]
(cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Out)
(p : (Fin n → Bool) → ℝ)
(leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool)
(advice : Option (Fin t) → List Bool)
{γ ε : ℝ}
(positive : 0 < γ)
(average :
∀ (g : (Fin d → Bool) → Fin n → Bool) (f : (Fin d → Bool) → Fin t → Fin d → Bool),
∑ y : Fin d → Bool,
uniformWeight (Fin d → Bool) y * weightDist (affineLeakageOutputWeight cb p leak advice (g y) y (f y))
(uniformSecondWeight (affineLeakageOutputWeight cb p leak advice (g y) y (f y))) ≤ ε)
: