Two-round extraction with a tampered transcript #
The first retained extraction supplies the next honest seed. Revealing the two initial seeds preserves the left source envelope in total. The second left extraction reveals both first outputs, paying their alphabet size. All seed discrepancies follow from the actual preceding calls.
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadSeedWeight_probability
{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}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Seed]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (lookAheadSeedWeight w l r x q q' initialSeed W QExt)
theorem
Algebraic.Cutwidth.Extractor.Internal.lookAheadExtractionWeight_probability
{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}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype Mid]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(initialSeed : Q → Seed)
(W : X → Seed → Mid)
(QExt : Q → Mid → Seed)
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
:
IsProbabilityWeight (lookAheadExtractionWeight w l r x x' q q' initialSeed W QExt)
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_lookAhead_seed_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}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype X]
[Fintype Q]
[Fintype Seed]
[Fintype Mid]
[Nonempty Seed]
[Nonempty Mid]
{W : X → Seed → Mid}
{QExt : Q → Mid → Seed}
{K L : ℕ}
{ε η δ : ℝ}
(first : WeightedStrongSeededExtractor W K ε)
(first_error : 0 ≤ ε)
(second : WeightedStrongSeededExtractor QExt L η)
(second_error : 0 ≤ η)
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → X)
(q q' : Z → B → Q)
(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) (q₀ : Q), w z * mapWeight (q z) (r z) q₀ ≤ ν 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 (lookAheadSeedWeight w l r x q q' initialSeed W QExt)
(uniformSecondWeight (lookAheadSeedWeight w l r x q q' initialSeed W QExt)) ≤ η + (ε + δ + ↑K * ∑ z : Z, μ z) + ↑L * ↑(Fintype.card (Seed × Seed)) * ∑ z : Z, ν z
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_lookAhead_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}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype X]
[Fintype Q]
[Fintype Seed]
[Fintype Mid]
[Nonempty Seed]
[Nonempty Mid]
{W : X → Seed → Mid}
{QExt : Q → Mid → Seed}
{K L : ℕ}
{ε η δ : ℝ}
(first : WeightedStrongSeededExtractor W K ε)
(first_error : 0 ≤ ε)
(second : WeightedStrongSeededExtractor QExt L η)
(second_error : 0 ≤ η)
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(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) (q₀ : Q), w z * mapWeight (q z) (r z) q₀ ≤ ν 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 (lookAheadExtractionWeight w l r x x' q q' initialSeed W QExt)
(uniformSecondWeight (lookAheadExtractionWeight w l r x x' q q' initialSeed W QExt)) ≤ 2 * ε + η + δ + ↑K * (1 + ↑(Fintype.card (Mid × Mid))) * ∑ z : Z, μ z + ↑L * ↑(Fintype.card (Seed × Seed)) * ∑ z : Z, ν z
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededExtractor_lookAhead_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}
[Fintype Z]
[Fintype A]
[Fintype B]
[Fintype X]
[Fintype Q]
[Fintype Seed]
[Fintype Mid]
[Nonempty Seed]
[Nonempty Mid]
{W : X → Seed → Mid}
{QExt : Q → Mid → Seed}
{K L : ℕ}
{ε η δ ρ : ℝ}
(first : WeightedStrongSeededExtractor W K ε)
(first_error : 0 ≤ ε)
(second : WeightedStrongSeededExtractor QExt L η)
(second_error : 0 ≤ η)
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x x' : Z → A → X)
(q q' : Z → B → Q)
(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) (q₀ : Q), w z * mapWeight (q z) (r z) q₀ ≤ ν 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 * (1 + ↑(Fintype.card (Mid × Mid))) * ∑ z : Z, μ z + ↑L * ↑(Fintype.card (Seed × Seed)) * ∑ z : Z, ν z ≤ ρ)
:
weightDist (lookAheadExtractionWeight w l r x x' q q' initialSeed W QExt)
(uniformSecondWeight (lookAheadExtractionWeight w l r x x' q q' initialSeed W QExt)) ≤ 2 * ε + η + δ + ρ