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

• Cslib.Probability.PMF.mem_support_uniformOfFintype: every value has positive uniform mass.
• Cslib.Probability.PMF.uniformOfFintype_prod_map_fst: the first component of a uniform pair is uniform.
• Cslib.Probability.PMF.uniformOfFintype_bind_map_fst_equiv, Cslib.Probability.PMF.uniformOfFintype_bind_bind_fst_equiv: resampling along an equivalence.
• Cslib.Probability.PMF.toOuterMeasure_uniformOfFinset, Cslib.Probability.PMF.toOuterMeasure_uniformOfFinset_toReal, Cslib.Probability.PMF.toMeasure_uniformOfFinset, Cslib.Probability.PMF.toOuterMeasure_uniformOfFintype, Cslib.Probability.PMF.toOuterMeasure_uniformOfFintype_toReal, Cslib.Probability.PMF.toMeasure_uniformOfFintype: the uniform probability of an event is the fraction of its members.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.