PMF.bind_bind
theorem PMF.bind_bind :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (f : α → PMF β) (g : β → PMF γ),
(p.bind f).bind g = p.bind fun a => (f a).bind g
The theorem `PMF.bind_bind` states that for any probability mass function `p` mapping from type `α`, and functions `f` and `g` mapping from `α` to `PMF β` and `β` to `PMF γ` respectively, the operation of binding `p` to `f` and then binding the result to `g` is the same as binding `p` to a function that takes an element of `α` and binds `f a` to `g`. In other words, this is demonstrating the associativity of the bind operation for `PMF`, which is a key feature of monadic operations.
More concisely: For any probability mass functions $p : \alpha \rightarrow \mathbb{P}(\beta)$ and $f : \alpha \rightarrow \mathbb{P}(\gamma)$, $g : \beta \rightarrow \mathbb{P}(\delta)$, the law of the deep binding $\bind \circ \bind$ holds: $(p \bind f) \bind g = p \bind (\lambda x : \alpha. f(x) \bind g)$.
|
PMF.pure_bind
theorem PMF.pure_bind : ∀ {α : Type u_1} {β : Type u_2} (a : α) (f : α → PMF β), (PMF.pure a).bind f = f a
The theorem `PMF.pure_bind` states that for any type `α` and `β`, any element `a` of type `α`, and any function `f` mapping from `α` to probability mass function on `β` (PMF β), the bind operation of the "pure" probability mass function based on `a` and the function `f` is equivalent to directly applying the function `f` on `a`. In other words, it asserts that binding a function `f` onto a probability mass function that has all its mass concentrated at a single point `a` (i.e., `PMF.pure a`) simply results in the probability mass function that `f` maps `a` to.
More concisely: For any type `α`, element `a` of type `α`, and function `f` mapping from `α` to probability mass functions on `β`, `PMF.pure a >>= f = f a`.
|
PMF.support_pure
theorem PMF.support_pure : ∀ {α : Type u_1} (a : α), (PMF.pure a).support = {a}
This theorem states that for any type `α` and any element `a` of type `α`, the support of the pure probability mass function (PMF) at `a` is the set consisting only of `a`. In other words, the pure PMF, which assigns a probability of 1 to `a` and a probability of 0 to all other points, has its support (the set where it is nonzero) at just the one point `a`.
More concisely: For any type `α` and element `a` of type `α`, the support of the pure probability mass function at `a` is the singleton set `{a}`.
|
Mathlib.Probability.ProbabilityMassFunction.Monad._auxLemma.4
theorem Mathlib.Probability.ProbabilityMassFunction.Monad._auxLemma.4 :
∀ {α : Type u} {ι : Sort v} {x : α} {s : ι → Set α}, (x ∈ ⋃ i, s i) = ∃ i, x ∈ s i
This theorem, named `Mathlib.Probability.ProbabilityMassFunction.Monad._auxLemma.4`, states that for all types `α` and a sort `ι`, and for any element `x` of type `α` and a function `s` from `ι` to a set of `α`, the membership of `x` in the union of all sets `s i` (for all `i` in `ι`) is equivalent to the existence of an `i` such that `x` is in `s i`. In other words, an element belongs to the union of a collection of sets if and only if it belongs to at least one of the sets in the collection.
More concisely: For any type `α` and sort `ι`, and for any element `x` of type `α` and function `s` from `ι` to a set of `α`, the element `x` belongs to the union of `s i` for all `i` in `ι` if and only if there exists an `i` such that `x` belongs to `s i`.
|
PMF.toMeasure_bindOnSupport_apply
theorem PMF.toMeasure_bindOnSupport_apply :
∀ {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a ∈ p.support → PMF β) (s : Set β)
[inst : MeasurableSpace β],
MeasurableSet s →
↑↑(p.bindOnSupport f).toMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else ↑↑(f a h).toMeasure s
This theorem states that for any type `α` and `β`, a probability mass function `p` on `α`, a function `f` from `α` to `β` that is defined only when `α` is in the support of `p`, and a measurable set `s` of type `β` in a measurable space `β`, if `s` is a measurable set, then the measure of the set `s` under the operation `p.bindOnSupport f` equals the sum over all `a` of type `α` of the product of the probability of `a` under `p` and the measure of the set `s` under `f a _`. The function `f` is only partially defined, thus there is an additional condition that if `p a` equals 0, then the measure of the set under `f a _` is also 0.
More concisely: For any probability mass function `p` on type `α`, measurable function `f` from `α` to `β` defined only on the support of `p`, and measurable set `s` in `β`, the measure of `s` under `p.bindOnSupport f` equals the sum over all `a` in the support of `p` of the product of `p a` and the measure of `s` under `f a`. If `p a` equals 0, then the measure of `s` under `f a` is also 0.
|
PMF.bind_pure
theorem PMF.bind_pure : ∀ {α : Type u_1} (p : PMF α), p.bind PMF.pure = p
The theorem `PMF.bind_pure` states that for any probability mass function `p` over a certain type `α`, if we apply the bind operation on `p` with the pure probability mass function, we get back the original probability mass function `p`. In other words, binding any probability mass function with the pure function (which assigns the probability of `1` to a single point and `0` elsewhere) is an identity operation in the context of probability mass functions.
More concisely: For any probability mass function `p` over type `α`, `bind p (pure ℙ1) = p`, where `pure ℙ1` is the pure probability mass function assigning mass 1 to a single point and 0 elsewhere.
|
PMF.toMeasure_pure_apply
theorem PMF.toMeasure_pure_apply :
∀ {α : Type u_1} (a : α) (s : Set α) [inst : MeasurableSpace α],
MeasurableSet s → ↑↑(PMF.pure a).toMeasure s = if a ∈ s then 1 else 0
This theorem states that for any type 'α', element 'a' of type 'α', and measurable set 's' of type 'α' in a measurable space, if the set is measurable, then the measure of the set under the Probability Mass Function (PMF) that puts all mass on the point 'a' (`PMF.pure a`) is '1' if the set contains the element 'a', and '0' otherwise. Essentially, this is saying that the measure of a set in the context of a PMF that is completely concentrated on a single point, is 1 if that point is in the set, or 0 if not.
More concisely: For any measurable space, measurable set, and element, the measure of the set under a probability mass function that is a Dirac delta function at the element equals 1 if the element is in the set, and 0 otherwise.
|
PMF.toMeasure_bind_apply
theorem PMF.toMeasure_bind_apply :
∀ {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β) (s : Set β) [inst : MeasurableSpace β],
MeasurableSet s → ↑↑(p.bind f).toMeasure s = ∑' (a : α), p a * ↑↑(f a).toMeasure s
This theorem is stating that given a probability mass function `p` of type `α`, another function `f` mapping type `α` to another type `β`, and a set `s` of type `β` that is measurable (i.e., in a space where it is meaningful to talk about the "measure" or "size" of the set), the measure of the set under the function `p.bind f` is equal to the sum, over all elements `a` of type `α`, of the probability of `a` under `p` multiplied by the measure of the set under `f a`. This theorem essentially describes how the measure of a set changes when it is transformed by a function that binds the probability mass function `p` to another function `f`.
More concisely: The theorem states that for a probability mass function `p` over type `α`, a measurable set `s` over type `β`, and a function `f` from `α` to `β`, the measure of `s` under `p.bind f` equals the sum of the product of the probability of `p` at each `a` and the measure of `f a` in `s`.
|
PMF.support_bind
theorem PMF.support_bind :
∀ {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β), (p.bind f).support = ⋃ a ∈ p.support, (f a).support
The theorem `PMF.support_bind` states that for any probability mass function `p` of type `α` and any function `f` that takes a value of type `α` and returns a probability mass function of type `β`, the support (the set where the function is nonzero) of the result of binding `p` through `f` is equal to the union of the supports of the probability mass functions `f a` for each `a` in the support of `p`. In other words, if we create a new probability mass function by applying `f` to each possible outcome of `p`, the new function will be nonzero exactly where the individual probability mass functions given by `f a` are nonzero.
More concisely: The support of the probability mass function obtained by binding another probability mass function through a function is equal to the union of the supports of the resulting functions for each input in the original support.
|
PMF.bindOnSupport_eq_bind
theorem PMF.bindOnSupport_eq_bind :
∀ {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β), (p.bindOnSupport fun a x => f a) = p.bind f
The theorem `PMF.bindOnSupport_eq_bind` states that for any two types `α` and `β`, any probability mass function `p` from `α`, and any function `f` mapping from `α` to a probability mass function on `β`, binding `f` on the support of `p` is equivalent to simply binding `f` on `p`. In other words, if the function `f` does not rely on the additional hypothesis introduced by `bindOnSupport`, then the use of `bind` and `bindOnSupport` yield the same result.
More concisely: For any types `α` and `β`, probability mass function `p` on `α`, and function `f` from `α` to probability mass functions on `β`, the following hold equal: `(bind p f)` and `(bindOnSupport p f)`, where `bind` and `bindOnSupport` are used in the context of Lean's probabilistic programming library.
|