Finite uniform-seed distribution ensembles -- definitions

FiniteEnsemble α allows each parameter slice to use any nonempty finite uniform seed type. This strictly generalizes fixed-length Boolean seeds and, crucially, supports exact choices such as a uniform element of Fin m when m is not a power of two.

The distribution remembers sampler multiplicity: probability is the fraction of seeds whose samples satisfy an event, not the fraction of distinct outputs.

def Complexity.uniformProbability {Ω : Type u} [Fintype Ω] (event : Finset Ω) : ℚ

Uniform probability of an event in an arbitrary finite sample space.

Equations

• Complexity.uniformProbability event = ↑event.card / ↑(Fintype.card Ω)

def Complexity.uniformMean {Ω : Type u} [Fintype Ω] (value : Ω → ℚ) : ℚ

Mean of a rational-valued statistic on a finite uniform sample space.

Equations

• Complexity.uniformMean value = (∑ sample : Ω, value sample) / ↑(Fintype.card Ω)

def Complexity.uniformAtLeastOneEvent {Ω : Type u} [Fintype Ω] [DecidableEq Ω] (event : Finset Ω) (trials : ℕ) : Finset (Fin trials → Ω)

Samples in which at least one of trials independent uniform draws lands in event.

Equations

• Complexity.uniformAtLeastOneEvent event trials = {draws : Fin trials → Ω | ∃ (trial : Fin trials), draws trial ∈ event}

def Complexity.uniformAtLeastOneProbability {Ω : Type u} [Fintype Ω] [DecidableEq Ω] (event : Finset Ω) (trials : ℕ) : ℚ

Probability that at least one of trials independent uniform draws lands in event.

Equations

• Complexity.uniformAtLeastOneProbability event trials = Complexity.uniformProbability (Complexity.uniformAtLeastOneEvent event trials)

structure Complexity.FiniteEnsemble (α : Type u) : Type (max u (v + 1))

A parameterized distribution represented by a nonempty finite uniform seed space and deterministic sampler at every slice.

• Seed : ℕ → Type v

  Seed type used at each parameter.

• seedFintype (n : ℕ) : Fintype (self.Seed n)

  Every seed type is finite.

• seedDecidableEq (n : ℕ) : DecidableEq (self.Seed n)

  Seed equality is decidable, so events can be enumerated exactly.

• seedNonempty (n : ℕ) : Nonempty (self.Seed n)

  No slice has an empty sample space.

• sample (n : ℕ) : self.Seed n → α

  Deterministic output associated to each seed.

def Complexity.FiniteEnsemble.event {α : Type u} (D : FiniteEnsemble α) (n : ℕ) (P : α → Prop) [DecidablePred P] : Finset (D.Seed n)

The seed event whose samples satisfy P.

Equations

• D.event n P = {seed : D.Seed n | P (D.sample n seed)}

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

Exact uniform-seed probability of P in the nth slice.

Equations

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

def Complexity.FiniteEnsemble.mass {α : Type u} [DecidableEq α] (D : FiniteEnsemble α) (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.FiniteEnsemble.support {α : Type u} [DecidableEq α] (D : FiniteEnsemble α) (n : ℕ) : Finset α

Finite support of the nth slice.

Equations

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

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

Push an ensemble forward through a deterministic map.

Equations

• D.map f = { Seed := D.Seed, seedFintype := D.seedFintype, seedDecidableEq := D.seedDecidableEq, seedNonempty := ⋯, sample := fun (n : ℕ) (seed : D.Seed n) => f (D.sample n seed) }

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

Independently sample two ensembles from the product of their seed spaces.

Equations

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

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

Point-mass ensemble. Its seed type is a singleton at every slice.

Equations

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

def Complexity.DyadicEnsemble.toFinite {α : Type u} (D : DyadicEnsemble α) : FiniteEnsemble α

Regard a Boolean-seed ensemble as a general finite uniform-seed ensemble.

Equations

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