Finite weighted sources and strong extraction

Real weights describe finite distributions without requiring their atoms to have equal probability. Normalization and the point-mass cap are separate predicates. The cap K * p x ≤ 1 expresses min-entropy at least log₂ K without logarithms or division in conditional-source arguments.

Distance is half the sum of absolute coordinate differences. The weighted seeded test samples the source according to its weights and an independent uniform seed, retaining both the seed and output in the test. All finite-sum operations remain defined on arbitrary real weights; probability theorems state normalization and nonnegativity explicitly.

def Algebraic.Cutwidth.Extractor.IsProbabilityWeight {α : Type u_1} [Fintype α] (p : α → ℝ) : Prop

Nonnegative finite weights whose total mass is one.

Equations

• Algebraic.Cutwidth.Extractor.IsProbabilityWeight p = ((∀ (x : α), 0 ≤ p x) ∧ ∑ x : α, p x = 1)

def Algebraic.Cutwidth.Extractor.CappedWeight {α : Type u_1} (p : α → ℝ) (K : ℕ) : Prop

Every point has probability at most the reciprocal of the support threshold.

Equations

• Algebraic.Cutwidth.Extractor.CappedWeight p K = ∀ (x : α), ↑K * p x ≤ 1

noncomputable def Algebraic.Cutwidth.Extractor.weightDist {α : Type u_1} [Fintype α] (p q : α → ℝ) : ℝ

Total variation distance for finite probability weights.

Equations

• Algebraic.Cutwidth.Extractor.weightDist p q = (∑ x : α, |p x - q x|) / 2

noncomputable def Algebraic.Cutwidth.Extractor.weightTestProb {α : Type u_1} (p : α → ℝ) (T : Finset α) : ℝ

The probability mass assigned to a finite test.

Equations

• Algebraic.Cutwidth.Extractor.weightTestProb p T = ∑ x ∈ T, p x

noncomputable def Algebraic.Cutwidth.Extractor.mapWeight {α : Type u_1} {β : Type u_2} [Fintype α] (f : α → β) (p : α → ℝ) (y : β) : ℝ

Push weights through a deterministic map, counting every source occurrence.

Equations

• Algebraic.Cutwidth.Extractor.mapWeight f p y = ∑ x : α, if f x = y then p x else 0

noncomputable def Algebraic.Cutwidth.Extractor.firstWeight {α : Type u_1} {β : Type u_2} [Fintype β] (p : α × β → ℝ) (a : α) : ℝ

Marginal weights on the first component of a finite product.

Equations

• Algebraic.Cutwidth.Extractor.firstWeight p a = ∑ b : β, p (a, b)

noncomputable def Algebraic.Cutwidth.Extractor.uniformWeight (α : Type u_1) [Fintype α] : α → ℝ

Uniform weights, with the zero convention on an empty sampling type.

Equations

• Algebraic.Cutwidth.Extractor.uniformWeight α x✝ = (↑(Fintype.card α))⁻¹

noncomputable def Algebraic.Cutwidth.Extractor.flatWeight {α : Type u_1} (P : Finset α) (x : α) : ℝ

Uniform weights on a finite support, and zero weights for the empty support.

Equations

• Algebraic.Cutwidth.Extractor.flatWeight P x = if x ∈ P then (↑P.card)⁻¹ else 0

noncomputable def Algebraic.Cutwidth.Extractor.weightedSeededTestProb {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (p : α → ℝ) (E : α → Seed → Ω) (T : Finset (Seed × Ω)) : ℝ

Test probability for a weighted source and an independent uniform seed.

Equations

• Algebraic.Cutwidth.Extractor.weightedSeededTestProb p E T = (∑ x : α, p x * ↑{y : Seed | (y, E x y) ∈ T}.card) / ↑(Fintype.card Seed)

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

Strong extraction from every normalized source satisfying the point-mass cap.

Equations

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