Selected refresh after a correlated uniform-coordinate repair #
Repair only the honest state coordinate inside the full right state. The left source and original right-source envelopes are unchanged. Apply the common selected-refresh estimate with an exact uniform state envelope, then transfer to the actual retained transcript at twice the repair cost. No independence between the repaired coordinate and original right state is used.
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_lookAhead_uniformRefresh_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 : Z → B → Y)
(μ ξ : Z → ℝ)
(chooseSecond : Bool)
(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)
(balanced : mapWeight initialSeed (uniformWeight Q) = uniformWeight Seed)
(state : weightDist (retainedSeedWeight w r q) (uniformSecondWeight (retainedSeedWeight w r q)) ≤ ρ)
:
weightDist (lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R chooseSecond)
(uniformSecondWeight (lookAheadSelectedRefreshWeight w l r x x' q q' initialSeed W QExt y R chooseSecond)) ≤ θ + 2 * ε + η + 2 * ρ + ↑K * (1 + ↑(Fintype.card (Mid × Mid))) * ∑ z : Z, μ z + ↑L * ↑(Fintype.card (Seed × Seed)) / ↑(Fintype.card Q) + ↑J * ↑(Fintype.card (Q × Q)) * ↑(Fintype.card Out) * ∑ z : Z, ξ z