Exact dyadic distribution ensembles -- definitions

A DyadicEnsemble α represents each parameter slice by a uniformly random finite Boolean seed and a deterministic sample map. Repeated samples may map to the same output, so this representation captures arbitrary finite dyadic distributions without quotienting away sampler multiplicity.

This is the representation-independent finite layer needed by average-case complexity. Polynomial-time samplability is a separate machine-level property.

structure Complexity.DyadicEnsemble (α : Type u) : Type u

A parameterized family of finite dyadic distributions on α.

At parameter n, a uniformly random Boolean string of length seedLength n is mapped to an output by sample n. Distinct seeds may produce the same output.

• seedLength : ℕ → ℕ

  Number of uniformly random bits used by the nth slice.

• sample (n : ℕ) : (Fin (self.seedLength n) → Bool) → α

  Deterministic sample produced from the parameter and random seed.

def Complexity.DyadicEnsemble.event {α : Type u} (D : DyadicEnsemble α) (n : ℕ) (P : α → Prop) [DecidablePred P] : Finset (Fin (D.seedLength n) → Bool)

The seed event whose samples satisfy P.

Equations

• D.event n P = {seed : Fin (D.seedLength n) → Bool | P (D.sample n seed)}

def Complexity.DyadicEnsemble.probability {α : Type u} (D : DyadicEnsemble α) (n : ℕ) (P : α → Prop) [DecidablePred P] : ℚ

Exact probability of P in the nth ensemble slice.

Equations

• D.probability n P = Complexity.eventProb (D.event n P)

def Complexity.DyadicEnsemble.mass {α : Type u} [DecidableEq α] (D : DyadicEnsemble α) (n : ℕ) (x : α) : ℚ

Probability mass of one output in the nth slice.

Equations

• D.mass n x = D.probability n fun (y : α) => y = x

def Complexity.DyadicEnsemble.support {α : Type u} [DecidableEq α] (D : DyadicEnsemble α) (n : ℕ) : Finset α

Finite support of the nth slice.

Equations

• D.support n = Finset.image (D.sample n) Finset.univ

def Complexity.DyadicEnsemble.map {α : Type u} {β : Type v} (D : DyadicEnsemble α) (f : α → β) : DyadicEnsemble β

Push an ensemble forward through a deterministic map.

Equations

• D.map f = { seedLength := D.seedLength, sample := fun (n : ℕ) (seed : Fin (D.seedLength n) → Bool) => f (D.sample n seed) }

def Complexity.DyadicEnsemble.product {α : Type u} {β : Type v} (D : DyadicEnsemble α) (E : DyadicEnsemble β) : DyadicEnsemble (α × β)

Independently sample two ensembles using disjoint blocks of one seed.

Equations

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

def Complexity.DyadicEnsemble.dirac {α : Type u} (x : ℕ → α) : DyadicEnsemble α

Point-mass ensemble. Its slices use no random bits.

Equations

• Complexity.DyadicEnsemble.dirac x = { seedLength := fun (x : ℕ) => 0, sample := fun (n : ℕ) (x_1 : Fin 0 → Bool) => x n }

def Complexity.DyadicEnsemble.uniformBits : DyadicEnsemble (List Bool)

Uniform distribution on all Boolean strings of length n, represented as lists in increasing index order.

Equations

• Complexity.DyadicEnsemble.uniformBits = { seedLength := fun (n : ℕ) => n, sample := fun (x : ℕ) (seed : Fin x → Bool) => List.ofFn seed }