Matched linear extraction on a masked original source #
The actual matched program preserves source XOR at every fixed seed. Consequently its output mask is a permutation within every retained right state. The actual strong extractor certificates supply the finite error and entropy thresholds, including the growing-depth row used for merging.
theorem
Algebraic.Cutwidth.Extractor.Internal.matchedBlockExtractor_depth64_affine_dist_le
(n L e : ℕ)
(length : Nat.clog 2 (n + 1) ≤ L)
(room : 64 ≤ L)
(error : e + 64 + 2 ≤ L)
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → Fin n → Bool)
(mask : Z → B → Fin n → Bool)
(y : Z → B → Fin (matchedBlockSeedBits L) → Bool)
(μ : Z → ℝ)
{δ : ℝ}
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(nonnegative : ∀ (z : Z), 0 ≤ μ z)
(cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(seed : weightDist (retainedSeedWeight w r y) (uniformSecondWeight (retainedSeedWeight w r y)) ≤ δ)
:
have actual :=
affineExtractionWeight w l r x mask y (fun (a b : Fin n → Bool) (i : Fin n) => a i ^^ b i)
(matchedBlockExtractor n 64 L e);
weightDist actual (uniformSecondWeight actual) ≤ (2 ^ e)⁻¹ + δ + 2 ^ (2 ^ 142 * L) * ∑ z : Z, μ z
theorem
Algebraic.Cutwidth.Extractor.Internal.matchedBlockExtractor_growing_affine_dist_le
(n h L e : ℕ)
(length : Nat.clog 2 (n + 1) ≤ L)
(error : e + h + 2 ≤ L)
(budget : (h + 1) * (e + 2 * h + Nat.clog 2 (L + 1) + 4) ≤ L)
{Z : Type u_1}
{A : Type u_2}
{B : Type u_3}
[Fintype Z]
[Fintype A]
[Fintype B]
(w : Z → ℝ)
(l : Z → A → ℝ)
(r : Z → B → ℝ)
(x : Z → A → Fin n → Bool)
(mask : Z → B → Fin n → Bool)
(y : Z → B → Fin (matchedBlockSeedBits L) → Bool)
(μ : Z → ℝ)
{δ : ℝ}
(hw : IsProbabilityWeight w)
(hl : ∀ (z : Z), IsProbabilityWeight (l z))
(hr : ∀ (z : Z), IsProbabilityWeight (r z))
(nonnegative : ∀ (z : Z), 0 ≤ μ z)
(cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z)
(seed : weightDist (retainedSeedWeight w r y) (uniformSecondWeight (retainedSeedWeight w r y)) ≤ δ)
:
have actual :=
affineExtractionWeight w l r x mask y (fun (a b : Fin n → Bool) (i : Fin n) => a i ^^ b i)
(matchedBlockExtractor n h L e);
weightDist actual (uniformSecondWeight actual) ≤ (2 ^ e)⁻¹ + δ + 2 ^ (2 ^ (2 * h + 14) * L) * ∑ z : Z, μ z