Strong extraction for arbitrary finite probability weights

For positive thresholds, the flat and weighted strong-extractor contracts are equivalent. Decomposing a capped source into exact-size flat sources and averaging their test bounds introduces no extra statistical error. The converse identifies the uniform law on every finite support with its weights on the ambient type. This allows the checked flat-source extractor to be used on nonuniform conditional distributions.

The mixture decomposition is a finite existence argument, supplied by Strong.FlatMixture using Mathlib's Birkhoff--von Neumann theorem. It makes no claim about computing a decomposition of arbitrary real probabilities.

theorem Algebraic.Cutwidth.Extractor.isProbabilityWeight_flatWeight {α : Type u_1} [Fintype α] (P : Finset α) (nonempty : P.Nonempty) : IsProbabilityWeight (flatWeight P)

Uniform weights on a nonempty finite support are normalized.

theorem Algebraic.Cutwidth.Extractor.cappedWeight_flatWeight {α : Type u_1} (P : Finset α) {K : ℕ} (size : K ≤ P.card) : CappedWeight (flatWeight P) K

A uniform support satisfies every cap whose threshold is at most its size.

theorem Algebraic.Cutwidth.Extractor.weightedSeededTestProb_uniformWeight {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (E : α → Seed → Ω) (T : Finset (Seed × Ω)) : weightedSeededTestProb (uniformWeight α) E T = seededTestProb E T

Uniform weights recover the existing finite seeded-test probability.

theorem Algebraic.Cutwidth.Extractor.weightedSeededTestProb_flatWeight {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (E : α → Seed → Ω) (P : Finset α) (T : Finset (Seed × Ω)) : weightedSeededTestProb (flatWeight P) E T = seededTestProb (fun (x : ↥P) => E ↑x) T

Sampling uniformly on a finite support agrees with the corresponding weights.

theorem Algebraic.Cutwidth.Extractor.weightedSeededTestProb_mixture {α : Type u_1} {ι : Type u_2} {Seed : Type u_3} {Ω : Type u_4} [Fintype α] [Fintype ι] [Fintype Seed] (w : ι → ℝ) (p : ι → α → ℝ) (E : α → Seed → Ω) (T : Finset (Seed × Ω)) : weightedSeededTestProb (fun (x : α) => ∑ i : ι, w i * p i x) E T = ∑ i : ι, w i * weightedSeededTestProb (p i) E T

Seeded-test probability is linear in the source weights.

theorem Algebraic.Cutwidth.Extractor.FlatStrongSeededExtractor.weightedStrongSeededExtractor {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] {E : α → Seed → Ω} {K : ℕ} {ε : ℝ} (extract : FlatStrongSeededExtractor E K ε) (positive : 0 < K) : WeightedStrongSeededExtractor E K ε

Flat strong extraction extends to all capped finite sources with the same error.

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

A weighted strong-extractor guarantee includes every nonempty flat source.

theorem Algebraic.Cutwidth.Extractor.weightedStrongSeededExtractor_iff_flat {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] {E : α → Seed → Ω} {K : ℕ} {ε : ℝ} (positive : 0 < K) : WeightedStrongSeededExtractor E K ε ↔ FlatStrongSeededExtractor E K ε

At positive thresholds, the weighted and flat strong contracts are equivalent.