Strong condensation of finite weighted sources

The actual joint output retains an independent uniform seed. An ideal witness supplies a normalized output distribution for each seed, with a point-mass cap at every seed. Strong condensation bounds the total variation between these joint distributions while preserving the uniform seed.

The operations are defined for arbitrary real weights. Empty seed types use the zero-division convention; probability-preservation theorems require a nonempty seed type explicitly.

noncomputable def Algebraic.Cutwidth.Extractor.weightedSeededOutput {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] (p : α → ℝ) (C : α → Seed → Ω) (yz : Seed × Ω) : ℝ

Joint output weights of a weighted source and an independent uniform seed.

Equations

• Algebraic.Cutwidth.Extractor.weightedSeededOutput p C yz = Algebraic.Cutwidth.Extractor.mapWeight (fun (x : α) => C x yz.1) p yz.2 / ↑(Fintype.card Seed)

noncomputable def Algebraic.Cutwidth.Extractor.seedFamilyWeight {Seed : Type u_1} {Ω : Type u_2} [Fintype Seed] (q : Seed → Ω → ℝ) (yz : Seed × Ω) : ℝ

Joint weights of a uniform seed and its supplied conditional output weights.

Equations

• Algebraic.Cutwidth.Extractor.seedFamilyWeight q yz = q yz.1 yz.2 / ↑(Fintype.card Seed)

def Algebraic.Cutwidth.Extractor.WeightedStrongSeededCondenser {α : Type u_1} {Seed : Type u_2} {Ω : Type u_3} [Fintype α] [Fintype Seed] [Fintype Ω] (C : α → Seed → Ω) (Kin Kout : ℕ) (ε : ℝ) : Prop

Every capped probability source has a close retained-seed output witness, normalized and capped at the requested output threshold for every seed.

Equations

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