Refreshing from the honest first look-ahead output #
The first extractor supplies the seed error while retaining the right state. After revealing both right inputs, the seed is left-only. The refresh retains the entire left state, so all four look-ahead outputs can be appended afterward without changing its output guarantee.
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_lookAhead_first_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}
{R : Y → Mid → Out}
{K J : ℕ}
{ε η δ : ℝ}
(first : WeightedStrongSeededExtractor W K ε)
(first_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)
(QExt : Q → Mid → Seed)
(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)
(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 (lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R)
(uniformSecondWeight (lookAheadFirstRefreshWeight w l r x x' q q' initialSeed W QExt y R)) ≤ η + (ε + δ + ↑K * ∑ z : Z, μ z) + ↑J * ↑(Fintype.card (Q × Q)) * ∑ z : Z, ν z