Refreshing the second output while retaining the tampered first refresh #
The right inputs and first left outputs form an exact observed transcript. The two-round theorem supplies the honest seed error. Revealing the tampered refresh costs its output alphabet only in the original right-source envelope. The other left outputs are appended after extraction, using the retained left state; they are not treated as independent messages or as uniform seeds.
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_lookAhead_tampered_refresh_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}
{QExt : Q → Mid → Seed}
{R : Y → Mid → Out}
{K L J : ℕ}
{ε η θ δ : ℝ}
(first : WeightedStrongSeededExtractor W K ε)
(first_error : 0 ≤ ε)
(second : WeightedStrongSeededExtractor QExt L η)
(second_error : 0 ≤ η)
(refresh : WeightedStrongSeededExtractor R J θ)
(refresh_error : 0 ≤ θ)
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(y y' : Z → B → Y)
(μ ν ξ : 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)
(refresh_nonnegative : ∀ (z : Z), 0 ≤ ξ z)
(left_cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(right_cap : ∀ (z : Z) (q₀ : Q), w z * mapWeight (q z) (r z) q₀ ≤ ν z)
(refresh_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 (lookAheadTamperedRefreshWeight w l r x x' q q' initialSeed W QExt y y' R)
(uniformSecondWeight (lookAheadTamperedRefreshWeight w l r x x' q q' initialSeed W QExt y y' R)) ≤ θ + (2 * ε + η + δ + ↑K * (1 + ↑(Fintype.card (Mid × Mid))) * ∑ z : Z, μ z + ↑L * ↑(Fintype.card (Seed × Seed)) * ∑ z : Z, ν z) + ↑J * ↑(Fintype.card (Q × Q)) * ↑(Fintype.card Out) * ∑ z : Z, ξ z