Strong extraction from finite flat sources

A strong seeded extractor preserves the seed in every test and compares its joint output with an independent uniform seed and uniform output. The source is uniform on any nonempty finite support above the cardinality threshold. The explicit nonemptiness requirement allows threshold zero without treating the empty support as a probability distribution.

The probability definitions use real division, which is zero at a zero denominator. Results using probability normalization state nonempty seed and output assumptions explicitly. Every source and seed pair is counted, including repeated output values.

noncomputable def Algebraic.Cutwidth.Extractor.uniformSeededTestProb {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] [Fintype Ω] (T : Finset (Seed × Ω)) : ℝ

Probability of a joint test under independent uniform seed and output. The value is zero if either finite sampling type is empty.

Equations

• Algebraic.Cutwidth.Extractor.uniformSeededTestProb T = ↑T.card / (↑(Fintype.card Seed) * ↑(Fintype.card Ω))

def Algebraic.Cutwidth.Extractor.FlatStrongSeededExtractor {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype Seed] [Fintype Ω] (E : α → Seed → Ω) (K : ℕ) (ε : ℝ) : Prop

Every nonempty flat support above K gives a joint seed-output distribution within ε of the independent uniform distribution on every retained-seed test.

Equations

• One or more equations did not get rendered due to their size.