Starting block-source recursion with an actual condenser #
Represent each condenser output as a one-coordinate tuple. Its normalized capped conditional witnesses are one-block sources at the same threshold, and the retained-seed distance bound is unchanged. This supplies the initial block-source family from the condenser guarantee itself.
This is the initial condensation step in Chattopadhyay--Goodman--Liao, Theorem 5.6 of Affine Extractors for Almost Logarithmic Entropy: https://eccc.weizmann.ac.il/report/2021/075/download/. Empty seed types retain the existing zero-mass convention.
theorem
Algebraic.Cutwidth.Extractor.WeightedStrongSeededCondenser.singleton
{X : Type u_1}
{Earlier : Type u_2}
{α : Type u_3}
[Fintype X]
[Fintype Earlier]
[Fintype α]
{C : X → Earlier → α}
{Kin Kout : ℕ}
{ε : ℝ}
(cond : WeightedStrongSeededCondenser C Kin Kout ε)
(p : X → ℝ)
(probability : IsProbabilityWeight p)
(cap : CappedWeight p Kin)
:
∃ (q : Earlier → (Fin 1 → α) → ℝ),
(∀ (y : Earlier), IsBlockSource (q y) Kout) ∧ weightDist (weightedSeededOutput p fun (x : X) (y : Earlier) (x_1 : Fin 1) => C x y) (seedFamilyWeight q) ≤ ε
An actual condenser starts a one-block source family with the same cap and error.