Refreshing after a left-only tampered seed #
Two-sided leakage bounds the actual first output while retaining the full right state and the left leak. The opposite source envelope is preserved in total by observing this left message. Observing the right input and its tampered refresh then costs their product alphabet size. Alternating extraction supplies the final honest output with all messages retained.
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_fixedTampering_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}
{Mid : Type u_7}
{Y : Type u_8}
{Out : Type u_9}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype X]
[Fintype Q]
[Fintype Seed]
[Fintype Mid]
[Fintype Y]
[Fintype Out]
[Nonempty Seed]
[Nonempty Mid]
[Nonempty Out]
{W : X → Seed → Mid}
{R : Y → Mid → Out}
{K L : ℕ}
{ε η δ : ℝ}
(first : WeightedStrongSeededExtractor W K ε)
(first_error : 0 ≤ ε)
(refresh : WeightedStrongSeededExtractor R L η)
(refresh_error : 0 ≤ η)
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(q : Z → B → Q)
(y y' : Z → B → Y)
(leak : Z → A → Mid)
(initialSeed : Q → Seed)
(μ ν : Z → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(left_nonnegative : ∀ (z : Z), 0 ≤ μ z)
(right_nonnegative : ∀ (z : Z), 0 ≤ ν z)
(left_cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(right_cap : ∀ (z : Z) (y₀ : Y), w z * mapWeight (y z) (r z) y₀ ≤ ν z)
(seed :
weightDist (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b))
(uniformSecondWeight (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b))) ≤ δ)
:
weightDist (fixedTamperingRefreshWeight w l r x q y y' leak initialSeed W R)
(uniformSecondWeight (fixedTamperingRefreshWeight w l r x q y y' leak initialSeed W R)) ≤ η + ε + δ + ↑K * ↑(Fintype.card Mid) * ∑ z : Z, μ z + ↑L * ↑(Fintype.card Q) * ↑(Fintype.card Out) * ∑ z : Z, ν z
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_fixedTampering_dist_le_of_budget
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
{X : Type u_4}
{Q : Type u_5}
{Seed : Type u_6}
{Mid : Type u_7}
{Y : Type u_8}
{Out : Type u_9}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype X]
[Fintype Q]
[Fintype Seed]
[Fintype Mid]
[Fintype Y]
[Fintype Out]
[Nonempty Seed]
[Nonempty Mid]
[Nonempty Out]
{W : X → Seed → Mid}
{R : Y → Mid → Out}
{K L : ℕ}
{ε η δ ρ : ℝ}
(first : WeightedStrongSeededExtractor W K ε)
(first_error : 0 ≤ ε)
(refresh : WeightedStrongSeededExtractor R L η)
(refresh_error : 0 ≤ η)
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(q : Z → B → Q)
(y y' : Z → B → Y)
(leak : Z → A → Mid)
(initialSeed : Q → Seed)
(μ ν : Z → ℝ)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(left_nonnegative : ∀ (z : Z), 0 ≤ μ z)
(right_nonnegative : ∀ (z : Z), 0 ≤ ν z)
(left_cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(right_cap : ∀ (z : Z) (y₀ : Y), w z * mapWeight (y z) (r z) y₀ ≤ ν z)
(seed :
weightDist (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b))
(uniformSecondWeight (retainedSeedWeight w r fun (z : Z) (b : B) => initialSeed (q z b))) ≤ δ)
(budget : ↑K * ↑(Fintype.card Mid) * ∑ z : Z, μ z + ↑L * ↑(Fintype.card Q) * ↑(Fintype.card Out) * ∑ z : Z, ν z ≤ ρ)
:
weightDist (fixedTamperingRefreshWeight w l r x q y y' leak initialSeed W R)
(uniformSecondWeight (fixedTamperingRefreshWeight w l r x q y y' leak initialSeed W R)) ≤ η + ε + δ + ρ