Canonical uniform samplers: the $ᵗ notation class

SampleableType β gives the notation $ᵗ β its meaning: an executable ProbComp β together with the one law that makes it a uniform sampler, 𝒟[$ᵗ β] = uniformOn Set.univ for every measurable structure with measurable singletons. The law is part of the contract because no consumer wants a canonical sampler that is not uniform; it is the only field besides the program, and every construction below discharges it once.

Nonemptiness of β follows from having a sampler at all (SampleableType.nonempty), and finiteness and full operational support follow from the law (SampleableType.finite, support_uniformSample). The two Prop-valued facts are instances so that a hypothesis [SampleableType β] supplies them wherever Mathlib asks, but at low priority: ordinary instances such as Finite.of_fintype and instNonemptyOfInhabited are tried first, so a fact about Fin 3 never routes through sampler code and the sampler instances only answer for types whose finiteness is known through nothing else (typically spec.Range t under [∀ t, SampleableType (spec.Range t)]). Since the classes are propositions, which instance answers is invisible to definitional equality (docs/agents/gotchas.md §8b).

Products, vectors, and equivalences transport the sampler together with its law.

class SampleableType (β : Type) : Type

A canonical uniform sampler for β, written $ᵗ β: an executable program whose output measure is uniform for every measurable structure with measurable singletons.

• selectElem : ProbComp β

  The canonical sampler of β, written $ᵗ β.

• evalDist_selectElem_eq_uniform [MeasurableSpace β] [MeasurableSingletonClass β] : 𝒟[selectElem] = ProbabilityTheory.uniformOn Set.univ

  The canonical sampler denotes the uniform measure on β.

def uniformSample (β : Type) [h : SampleableType β] : ProbComp β

Select uniformly from the type β using a type-class provided definition.

def «term$ᵗ_» : Lean.ParserDescr

theorem SampleableType.evalDist_uniformSample {β : Type} [SampleableType β] [MeasurableSpace β] [MeasurableSingletonClass β] : 𝒟[$ᵗ β] = ProbabilityTheory.uniformOn Set.univ

The canonical sample has uniform output measure under native oracle semantics.

@[instance 100]

instance SampleableType.nonempty (β : Type) [SampleableType β] : Nonempty β

A sampler yields an element of its type: run it on default oracle answers. Low priority so that ordinary nonemptiness instances answer first.

@[instance 100]

instance SampleableType.finite (β : Type) [SampleableType β] : Finite β

A uniform sampler denotes a probability measure only on a finite type. Low priority so that ordinary finiteness instances answer first.

@[simp]

theorem support_uniformSample (α : Type) [SampleableType α] : support ($ᵗ α) = Set.univ

A uniform sampler can output every element: positive uniform mass on each singleton is operational reachability.

theorem mem_support_uniformSample (α : Type) [SampleableType α] {x : α} : x ∈ support ($ᵗ α)

theorem support_uniformSample_nonempty (α : Type) [SampleableType α] : (support ($ᵗ α)).Nonempty

The canonical sampler has a possible output.

@[reducible]

def SampleableType.Fin (n : ℕ) : SampleableType (_root_.Fin (n + 1))

The uniform sampler of Fin (n + 1).

@[instance_reducible]

instance instSampleableTypeFinOfNeZeroNat (n : ℕ) [hn : NeZero n] : SampleableType (Fin n)

@[instance_reducible]

instance instSampleableTypeOfUnique (α : Type) [Unique α] : SampleableType α

@[instance_reducible]

instance instSampleableTypeRangeSumHAddOracleSpec {ι : Type u_1} {ι' : Type u_2} {spec : OracleSpec ι} {spec' : OracleSpec ι'} [h : (t : ι) → SampleableType (spec.Range t)] [h' : (t : ι') → SampleableType (spec'.Range t)] (t : ι ⊕ ι') : SampleableType ((spec + spec').Range t)

A sum of oracle specs with sampleable ranges again has sampleable ranges.

@[instance_reducible]

instance instSampleableTypeProd (α β : Type) [SampleableType α] [SampleableType β] : SampleableType (α × β)

Select a uniform element from α × β by independently selecting from α and β.

@[reducible]

def SampleableType.ofEquiv {α β : Type} [SampleableType α] (e : α ≃ β) : SampleableType β

Transport a uniform sampler along an equivalence.

@[instance_reducible]

instance FinEnum.SampleableType (α : Type) [h : FinEnum α] [Nonempty α] : _root_.SampleableType α

Any finitely enumerable type can be sampled uniformly using the underlying equivalence.

@[reducible]

noncomputable def SampleableType.ofFintype (α : Type) [Fintype α] [Nonempty α] : SampleableType α

Noncomputable bridge from a nonempty Fintype with decidable equality to SampleableType, via Fintype.equivFin. Used by downstream instances (e.g. Sym α n, Equiv.Perm α, β ↪ α) whose Mathlib Fintype instances are not paired with a FinEnum. Provided as a def rather than an instance to avoid overlap with FinEnum.SampleableType.

@[reducible]

noncomputable def SampleableType.piOfFintype {ι : Type} [Fintype ι] (α : ι → Type) [(i : ι) → Fintype (α i)] [∀ (i : ι), Nonempty (α i)] : SampleableType ((i : ι) → α i)

Explicit noncomputable uniform sampler for a dependent finite product. This constructor is a definition rather than an instance so it cannot compete with executable samplers for particular dependent function types.

@[reducible]

noncomputable def SampleableType.subtype (α : Type) [Fintype α] (p : α → Prop) [DecidablePred p] [Nonempty { x : α // p x }] : SampleableType { x : α // p x }

Uniform sampling of a nonempty subtype of a finite type, by enumeration. Provided as a definition so that it never competes with executable enumeration-based instances.

@[reducible]

noncomputable def SampleableType.finsetCoe {α : Type} (U : Finset α) (hU : U.Nonempty) : SampleableType ↥U

Uniform sampling from a nonempty finite set, by enumeration.

@[instance_reducible]

instance instFinEnumZModOfNeZeroNat_vCVio (n : ℕ) [NeZero n] : FinEnum (ZMod n)

@[instance_reducible]

instance instFinEnumUSize_vCVio : FinEnum USize

@[instance_reducible]

instance instFinEnumISize_vCVio : FinEnum ISize

def arrayVectorEquivFin (α : Type u) (n : ℕ) : Vector α n ≃ (Fin n → α)

The array-backed Vector α n is equivalent to an n-indexed function.

@[instance_reducible]

instance instFintypeVector (α : Type u) (n : ℕ) [Fintype α] : Fintype (Vector α n)

Vector α n is finite when α is finite, via the equivalence with Fin n → α.

instance instFiniteVector (α : Type u) (n : ℕ) [Finite α] : Finite (Vector α n)

Finite entries give a finite array-backed vector type.

def SampleableType.vector (α : Type) [SampleableType α] (n : ℕ) : ProbComp (Vector α n)

Sample a Vector α n by independently sampling α at each index.

theorem SampleableType.evalDist_vector (α : Type) [SampleableType α] (n : ℕ) [MeasurableSpace (Vector α n)] [MeasurableSingletonClass (Vector α n)] : 𝒟[vector α n] = ProbabilityTheory.uniformOn Set.univ

Independent uniform samples at each index give the uniform measure on Vector α n.

@[instance_reducible]

instance instSampleableTypeVector (α : Type) (n : ℕ) [SampleableType α] : SampleableType (Vector α n)

@[instance_reducible]

instance instSampleableTypeFinFunc {n : ℕ} {α : Type} [SampleableType α] : SampleableType (Fin n → α)

A function from Fin n to a SampleableType is also SampleableType. This is the base case used by the general FinEnum-indexed instSampleableTypeFunc below.

@[instance_reducible]

instance instSampleableTypeFunc {β α : Type} [FinEnum β] [SampleableType α] : SampleableType (β → α)

A function β → α for β finitely enumerable and α sampleable is itself sampleable. This generalizes the Fin n → α instance above: the FinEnum.fin instance recovers it.

@[instance_reducible]

instance instSampleableTypeListVector {α : Type} {n : ℕ} [SampleableType α] : SampleableType (List.Vector α n)

Select a uniform element from List.Vector α n by independently selecting α at each index. The construction goes through the equivalence with Fin n → α.

@[instance_reducible]

instance instSampleableTypeMatrix {α ι κ : Type} [FinEnum ι] [FinEnum κ] [SampleableType α] : SampleableType (Matrix ι κ α)

Select a uniform element from Matrix ι κ α by independently selecting an entry for each (i, j). Both index types only need to be FinEnum.

@[instance_reducible]

instance instSampleableTypeSum {α β : Type} [FinEnum α] [FinEnum β] [Nonempty (α ⊕ β)] : SampleableType (α ⊕ β)

Discoverability wrapper: SampleableType (α ⊕ β) follows from FinEnum on each side plus nonemptiness of the sum, via Mathlib's FinEnum.sum instance and FinEnum.SampleableType. Listed explicitly so users can see it in the instance set rather than relying on a multi-step search.

@[instance_reducible]

instance instSampleableTypeFinset {α : Type} [FinEnum α] : SampleableType (Finset α)

Discoverability wrapper: SampleableType (Finset α) for FinEnum α. Uniform sampling draws every subset of α with the same probability (2^|α| outcomes). Finset α is always inhabited by ∅, so no Nonempty hypothesis is needed.

@[instance_reducible]

instance instSampleableTypeSym {α : Type} {n : ℕ} [FinEnum α] [Nonempty α] : SampleableType (Sym α n)

Uniform sampling of size-n multisets over a FinEnum type. Sym α n is the correct finite analogue of Multiset α: a plain Multiset α is unbounded in multiplicity and thus not finite, while Sym α n is finite whenever α is. We obtain a computable uniform sampler from the canonical enumeration Sym.finEnum; for a base type with only a Fintype instance use SampleableType.ofFintype instead.

Note this is genuinely uniform on multisets: mapping a uniform List.Vector α n through Sym.ofVector is not (it weights each multiset by its number of orderings), so we enumerate Sym α n canonically rather than pushing forward from vectors.

@[instance_reducible]

instance instSampleableTypePerm {α : Type} [FinEnum α] : SampleableType (Equiv.Perm α)

Uniform sampling of permutations of a FinEnum type. Equiv.Perm α has n! elements when Fintype.card α = n. We obtain a computable uniform sampler from the canonical enumeration Equiv.Perm.finEnum. Useful for shuffle-based protocols and oblivious-permutation games.

@[instance_reducible]

instance instSampleableTypeEmbedding {β α : Type} [FinEnum β] [FinEnum α] [Nonempty (β ↪ α)] : SampleableType (β ↪ α)

Uniform sampling of injections β ↪ α for FinEnum types. The number of such embeddings is α.card! / (α.card - β.card)! when β.card ≤ α.card, else 0; the Nonempty (β ↪ α) hypothesis rules out the latter case. We obtain a computable uniform sampler from the canonical enumeration Function.Embedding.finEnum (itself computable, unlike Mathlib's Fintype (β ↪ α)).

@[instance_reducible, instance 100]

noncomputable instance instSampleableTypePiFintype {D : Type} [Fintype D] [DecidableEq D] {α : Type} [SampleableType α] : SampleableType (D → α)

A function from a finite type D with Fintype + DecidableEq (not necessarily FinEnum) to a SampleableType is itself SampleableType, transporting the Fin (Fintype.card D) → α sampler across the canonical equivalence (D → α) ≃ (Fin (Fintype.card D) → α).

This is the noncomputable counterpart to the computable FinEnum-domain instance instSampleableTypeFunc, and is given lower priority so that for a FinEnum domain the computable instance is preferred; it is the fallback for Fintype + DecidableEq-only domains.

def uniformSampleImpl {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → SampleableType (spec.Range i)] : QueryImpl spec ProbComp

Given that the output type of all oracles has a SampleableType instance, replace all queries with uniformly random responses by calling the corresponding uniformSample at each query.

@[simp]

theorem uniformSampleImpl_apply {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → SampleableType (spec.Range i)] (t : spec.Domain) : uniformSampleImpl t = $ᵗ spec.Range t

A uniformly sampled implementation answers each query with the uniform sampler for that query's response type.

@[simp]

theorem uniformSampleImpl.support_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → SampleableType (spec.Range i)] {α : Type} (oa : OracleComp spec α) : support (simulateQ uniformSampleImpl oa) = support oa

Interpreting queries by full-support samplers preserves operational reachability.

@[simp]

theorem uniformSampleImpl.finSupport_simulateQ {ι : Type u_1} {spec : OracleSpec ι} [(i : ι) → SampleableType (spec.Range i)] [(t : ι) → Fintype (spec.Range t)] {α : Type} [DecidableEq α] (oa : OracleComp spec α) : finSupport (simulateQ uniformSampleImpl oa) = finSupport oa

Full-support query sampling also preserves the finite support when answers are enumerable.