Uniform Selection Over a Type

This file defines a typeclass SampleableType β for types β with a canonical uniform selection operation, using the ProbComp monad.

As compared to HasUniformSelect this provides much more structure on the behavior, enforcing that every possible output has the same output probability never fails.

class SampleableType (β : Type) : Type

A SampleableType β instance means that β is a finite inhabited type, with a computation selectElem that selects uniformly at random from the type. This generally requires choosing some "canonical" ordering for the type, so we include this to get a computable version of selection. We also require that each element has the same probability of being chosen from by selectElem, see SampleableType.probOutput_uniformSample for the reduction when α has a fintype instance involving the explicit cardinality of the type.

• selectElem : ProbComp β
• mem_support_selectElem (x : β) : x ∈ support selectElem
• probOutput_selectElem_eq (x y : β) : Pr[=x | selectElem] = Pr[=y | selectElem]

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

Select uniformly from the type β using a type-class provided definition. NOTE: naming is somewhat strange now that Fintype isn't explicitly required.

def «term$ᵗ_» : Lean.ParserDescr

@[simp]

theorem probOutput_uniformSample (α : Type) [hα : SampleableType α] [Fintype α] (x : α) : Pr[=x | $ᵗα] = (↑(Fintype.card α))⁻¹

theorem probFailure_uniformSample (α : Type) [hα : SampleableType α] : Pr[⊥ | $ᵗα] = 0

@[simp]

instance instNeverFailProbCompUniformSample (α : Type) [hα : SampleableType α] : NeverFail ($ᵗα)

@[simp]

theorem evalDist_uniformSample (α : Type) [hα : SampleableType α] [Fintype α] [Nonempty α] : evalDist ($ᵗα) = liftM (PMF.uniformOfFintype α)

@[simp]

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

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

@[simp]

theorem finSupport_uniformSample (α : Type) [hα : SampleableType α] [Fintype α] [DecidableEq α] : finSupport ($ᵗα) = Finset.univ

@[simp]

theorem probEvent_uniformSample (α : Type) [hα : SampleableType α] [Fintype α] (p : α → Prop) [DecidablePred p] : Pr[p | $ᵗα] = ↑(Finset.filter p Finset.univ).card / ↑(Fintype.card α)

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

instance instSampleableTypeBool : SampleableType Bool

instance instSampleableTypeProdOfFintypeOfInhabited (α β : Type) [Fintype α] [Fintype β] [Inhabited α] [Inhabited β] [SampleableType α] [SampleableType β] : SampleableType (α × β)

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

instance instSampleableTypeFinHAddNatOfNat (n : ℕ) : SampleableType (Fin (n + 1))

Nonempty Fin types can be selected from, using implicit casting of Fin (n - 1 + 1).

instance instSampleableTypeZModHAddNatOfNat (n : ℕ) : SampleableType (ZMod (n + 1))

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

Version of Fin selection using the NeZero typeclass, avoiding the need for n + 1.

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

Select a uniform element from Vector α n by independently selecting α at each index.

instance instSampleableTypeMatrixFinOfDecidableEq (α : Type) (n m : ℕ) [SampleableType α] [DecidableEq α] : SampleableType (Matrix (Fin n) (Fin m) α)

Select a uniform element from Matrix α n by independently selecting α at each index.

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

A type equivalent to a SampleableType is also SampleableType.

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

A function from Fin n to a SampleableType is also SampleableType.

theorem probOutput_uniformBool_not_decide_eq_decide {ob : ProbComp Bool} : Pr[=true | do let b ← $ᵗBool let b' ← ob pure !decide (b = b')] = Pr[=true | do let b ← $ᵗBool let b' ← ob pure (decide (b = b'))]

Given an independent probabilistic computation ob : ProbComp Bool, the probability that its output b' differs from a uniformly chosen boolean b is the same as the probability that they are equal. In other words, P(b ≠ b') = P(b = b') where b is uniform.