Closing the finite recursive extraction argument #
The initial condenser supplies its own one-block witnesses. Recursive condensation and splitting propagate their joint approximation, and final retained-seed extraction compares all leaf outputs with uniform. The dyadic specialization sums every initial, internal, and leaf error.
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededCondenser_recursiveExtractor
{X : Type v}
{Earlier : Type u}
{Fresh : ℕ → Type u}
{α : ℕ → Type w}
{Last : Type z}
{Ω : Type r}
[Fintype X]
[Fintype Earlier]
[Nonempty Earlier]
[(i : ℕ) → Fintype (Fresh i)]
[∀ (i : ℕ), Nonempty (Fresh i)]
[(i : ℕ) → Fintype (α i)]
[Fintype Last]
[Nonempty Last]
[Fintype Ω]
[Nonempty Ω]
{initial : X → Earlier → α 0}
{Kin : ℕ}
{k m e : ℕ → ℕ}
{ε : ℕ → ℝ}
{ε₀ εL : ℝ}
{n : ℕ}
(initial_cond : WeightedStrongSeededCondenser initial Kin (2 ^ k 0) ε₀)
(C : (i : ℕ) → α i → Fresh i → α (i + 1) × α (i + 1))
(condensers : ∀ i < n, WeightedStrongSeededCondenser (C i) (2 ^ k i) (2 ^ k i) (ε i))
(cards : ∀ i < n, Fintype.card (α (i + 1)) = 2 ^ m i)
(widths : ∀ i < n, k (i + 1) ≤ m i)
(entropies : ∀ i < n, m i + k (i + 1) + e i ≤ k i)
{E : α n → Last → Ω}
(final_extract : WeightedStrongSeededExtractor E (2 ^ k n) εL)
:
WeightedStrongSeededExtractor (recursiveBlockExtractor initial C n E) Kin
(ε₀ + recursiveBlockError 1 ε e n + ↑(recursiveBlockCount 1 n) * εL)
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededCondenser_recursiveExtractor_dyadic
{X : Type v}
{Earlier : Type u}
{Fresh : ℕ → Type u}
{α : ℕ → Type w}
{Last : Type z}
{Ω : Type r}
[Fintype X]
[Fintype Earlier]
[Nonempty Earlier]
[(i : ℕ) → Fintype (Fresh i)]
[∀ (i : ℕ), Nonempty (Fresh i)]
[(i : ℕ) → Fintype (α i)]
[Fintype Last]
[Nonempty Last]
[Fintype Ω]
[Nonempty Ω]
{initial : X → Earlier → α 0}
{Kin : ℕ}
{k m : ℕ → ℕ}
{n e : ℕ}
(initial_cond : WeightedStrongSeededCondenser initial Kin (2 ^ k 0) (2 ^ (e + n + 2))⁻¹)
(C : (i : ℕ) → α i → Fresh i → α (i + 1) × α (i + 1))
(condensers : ∀ i < n, WeightedStrongSeededCondenser (C i) (2 ^ k i) (2 ^ k i) (2 ^ (e + n + 2))⁻¹)
(cards : ∀ i < n, Fintype.card (α (i + 1)) = 2 ^ m i)
(widths : ∀ i < n, k (i + 1) ≤ m i)
(entropies : ∀ i < n, m i + k (i + 1) + (e + n + 2) ≤ k i)
{E : α n → Last → Ω}
(final_extract : WeightedStrongSeededExtractor E (2 ^ k n) (2 ^ (e + n + 2))⁻¹)
:
WeightedStrongSeededExtractor (recursiveBlockExtractor initial C n E) Kin (2 ^ e)⁻¹