Documentation

CslibFrontier.Probability.PMF.Uniform

Uniform distributions and resampling #

Every value of a nonempty finite type has positive uniform mass (mem_support_uniformOfFintype), and the uniform probability or measure of an event under uniformOfFinset or uniformOfFintype is the fraction of members in the event (toOuterMeasure_uniformOfFinset, toOuterMeasure_uniformOfFinset_toReal, toMeasure_uniformOfFinset, toOuterMeasure_uniformOfFintype, toOuterMeasure_uniformOfFintype_toReal, toMeasure_uniformOfFintype).

Draw a uniformly from α and, independently, b uniformly from β. For any equivalence e : α × β ≃ γ × δ, the pair e (a, b) is uniform on γ × δ, so its first component is uniform on γ (uniformOfFintype_bind_map_fst_equiv). This is the resampling step of hybrid arguments: overwriting part of a uniform string a by independent uniform values b leaves it uniform, since the overwritten string and the old part together determine (a, b).

Main results #

source
theorem Cslib.Probability.PMF.mem_support_uniformOfFintype {α : Type u_1} [Fintype α] [Nonempty α] (a : α) :
a ∈ (uniformOfFintype α).support

Every value of a nonempty finite type is in the uniform distribution's support.

source
theorem Cslib.Probability.PMF.uniformOfFintype_finset_map_val {α : Type u_1} (s : Finset α) [Nonempty ↥s] :
PMF.map Subtype.val (uniformOfFintype ↥s) = uniformOfFinset s ⋯

Forgetting membership proofs in a uniform draw from a finset subtype gives its uniform finite-set law.

source
theorem Cslib.Probability.PMF.uniformOfFintype_bind_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] (e : α ≃ α) (f : α → PMF β) :
((uniformOfFintype α).bind fun (a : α) => f (e a)) = (uniformOfFintype α).bind f

Reparametrizing a uniform draw by a bijection does not change an experiment.

source
theorem Cslib.Probability.PMF.uniformOfFintype_prod_map_fst {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] :
PMF.map Prod.fst (uniformOfFintype (α × β)) = uniformOfFintype α

The first component of a uniform pair is uniform.

source
theorem Cslib.Probability.PMF.uniformOfFintype_bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] (f : α → β → γ) :
((uniformOfFintype α).bind fun (a : α) => PMF.map (fun (b : β) => f a b) (uniformOfFintype β)) = PMF.map (fun (p : α × β) => f p.1 p.2) (uniformOfFintype (α × β))

Mapping a curried binary function over two independent uniform draws is equivalent to mapping the uncurried function over a uniform pair. Iterating this rewrite collapses n-ary chains of independent uniform draws into a single uniformOfFintype over a nested product.

source
theorem Cslib.Probability.PMF.uniformOfFintype_pi_map_restrict {ι : Type u_6} [Fintype ι] [DecidableEq ι] {π : ι → Type u_7} [(i : ι) → Fintype (π i)] [∀ (i : ι), Nonempty (π i)] (I : Finset ι) :
PMF.map I.restrict (uniformOfFintype ((i : ι) → π i)) = uniformOfFintype ((i : ↥I) → π ↑i)

Restricting a uniform dependent function on ι to I : Finset ι gives the uniform distribution on (i : I) → π i.

source
theorem Cslib.Probability.PMF.uniformOfFintype_pi_bind_restrict {ε : Type u_5} {ι : Type u_6} [Fintype ι] [DecidableEq ι] {π : ι → Type u_7} [(i : ι) → Fintype (π i)] [∀ (i : ι), Nonempty (π i)] (I : Finset ι) (f : ((i : ↥I) → π ↑i) → PMF ε) :
((uniformOfFintype ((i : ι) → π i)).bind fun (a : (i : ι) → π i) => f (I.restrict a)) = (uniformOfFintype ((i : ↥I) → π ↑i)).bind f

Binding a uniform dependent function on ι to a continuation that depends only on its restriction to I : Finset ι is equivalent to sampling uniformly on (i : I) → π i.

source
theorem Cslib.Probability.PMF.uniformOfFintype_bind_map_fst_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] [Fintype γ] [Nonempty γ] [Finite δ] (e : α × β ≃ γ × δ) :
((uniformOfFintype α).bind fun (a : α) => PMF.map (fun (b : β) => (e (a, b)).1) (uniformOfFintype β)) = uniformOfFintype γ

Resampling: for independent uniform a and b and an equivalence e : α × β ≃ γ × δ, the first component of e (a, b) is uniform.

source
theorem Cslib.Probability.PMF.uniformOfFintype_bind_bind_fst_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} [Fintype α] [Nonempty α] [Fintype β] [Nonempty β] [Fintype γ] [Nonempty γ] [Finite δ] (e : α × β ≃ γ × δ) (f : γ → PMF ε) :
((uniformOfFintype α).bind fun (a : α) => (uniformOfFintype β).bind fun (b : β) => f (e (a, b)).1) = (uniformOfFintype γ).bind f

Resampling inside an experiment: running f on the first component of e (a, b), for independent uniform a and b, is running f on a uniform input.

source
theorem Cslib.Probability.PMF.uniformOfFintype_bind_bind_adaptiveUpdate {ε : Type u_5} {ι : Type u_6} {κ : Type u_7} [Fintype ι] [DecidableEq ι] [Fintype κ] [Nonempty κ] (p : (ι → κ) → ι) (hp : ∀ (f : ι → κ) (v : κ), p (Function.update f (p f) v) = p f) (g : (ι → κ) → PMF ε) :
((uniformOfFintype (ι → κ)).bind fun (f : ι → κ) => (uniformOfFintype κ).bind fun (v : κ) => g (Function.update f (p f) v)) = (uniformOfFintype (ι → κ)).bind g

Adaptive resampling: a uniform function whose value at a point p f, chosen from the function itself, is replaced by a fresh uniform value is uniform, provided that replacing that value does not move the point. (f, v) ↦ (Function.update f (p f) v, f (p f)) is an involution.

source
theorem Cslib.Probability.PMF.toOuterMeasure_uniformOfFinset {α : Type u_1} (s : Finset α) (hs : s.Nonempty) (event : Set α) [DecidablePred fun (x : α) => x ∈ event] :
(uniformOfFinset s hs).toOuterMeasure event = ↑{x ∈ s | x ∈ event}.card * (↑s.card)⁻¹

The uniform distribution on a nonempty finite set gives an event the fraction of the set's members in the event, as an extended nonnegative real.

source
theorem Cslib.Probability.PMF.toOuterMeasure_uniformOfFinset_toReal {α : Type u_1} (s : Finset α) (hs : s.Nonempty) (event : Set α) [DecidablePred fun (x : α) => x ∈ event] :
((uniformOfFinset s hs).toOuterMeasure event).toReal = ↑{x ∈ s | x ∈ event}.card / ↑s.card

The probability of an event under the uniform distribution on a nonempty finite set is the fraction of the set's members in the event.

source
theorem Cslib.Probability.PMF.toMeasure_uniformOfFinset {α : Type u_1} [MeasurableSpace α] (s : Finset α) (hs : s.Nonempty) {event : Set α} [DecidablePred fun (x : α) => x ∈ event] (he : MeasurableSet event) :
(uniformOfFinset s hs).toMeasure event = ↑{x ∈ s | x ∈ event}.card * (↑s.card)⁻¹

The measure of a measurable event under the uniform distribution on a nonempty finite set is the fraction of the set's members in the event.

source
theorem Cslib.Probability.PMF.toOuterMeasure_uniformOfFintype {α : Type u_1} [Fintype α] [Nonempty α] (event : Set α) [DecidablePred fun (x : α) => x ∈ event] :
(uniformOfFintype α).toOuterMeasure event = ↑{x : α | x ∈ event}.card * (↑(Fintype.card α))⁻¹

The uniform distribution on a finite type gives an event the fraction of its members, as an extended nonnegative real.

source
theorem Cslib.Probability.PMF.toOuterMeasure_uniformOfFintype_toReal {α : Type u_1} [Fintype α] [Nonempty α] (event : Set α) [DecidablePred fun (x : α) => x ∈ event] :
((uniformOfFintype α).toOuterMeasure event).toReal = ↑{x : α | x ∈ event}.card / ↑(Fintype.card α)

The probability of an event under the uniform distribution on a finite type is the fraction of its members.

source
theorem Cslib.Probability.PMF.toMeasure_uniformOfFintype {α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] {event : Set α} [DecidablePred fun (x : α) => x ∈ event] (he : MeasurableSet event) :
(uniformOfFintype α).toMeasure event = ↑{x : α | x ∈ event}.card * (↑(Fintype.card α))⁻¹

The measure of a measurable event under the uniform distribution on a finite type is the fraction of its members.