PMF.ext
theorem PMF.ext : ∀ {α : Type u_1} {p q : PMF α}, (∀ (x : α), p x = q x) → p = q
The theorem `PMF.ext` states that, for any type `α` and any two probability mass functions `p` and `q` over `α`, if for every element `x` of type `α`, `p` evaluated at `x` equals `q` evaluated at `x`, then `p` is equal to `q`. In other words, two probability mass functions are equal if they assign the same probability to each element in their domain.
More concisely: If two probability mass functions over a type assign the same probability to every element, then they are equal.
|
PMF.toMeasure_apply_eq_toOuterMeasure_apply
theorem PMF.toMeasure_apply_eq_toOuterMeasure_apply :
∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) (s : Set α),
MeasurableSet s → ↑↑p.toMeasure s = ↑p.toOuterMeasure s
This theorem states that for any type `α` equipped with a measurable space, any probability mass function `p` of type `α`, and any set `s` of type `α` that is measurable, the measure assigned to the set `s` by the measure derived from the `PMF p` is equal to the measure assigned to the set `s` by the outer measure derived from the `PMF p`. In other words, when applied to a measurable set, the measure and the outer measure derived from a probability mass function assign the same measure to that set.
More concisely: For any measurable space, measurable set, and probability mass function, the measure and outer measure derived from the probability mass function agree on the measurable set.
|
PMF.tsum_coe_indicator_ne_top
theorem PMF.tsum_coe_indicator_ne_top : ∀ {α : Type u_1} (p : PMF α) (s : Set α), ∑' (a : α), s.indicator (⇑p) a ≠ ⊤
The theorem `PMF.tsum_coe_indicator_ne_top` states that for any given probability mass function `p` and any set `s` of the same type `α`, the infinite sum of the `Set.indicator` function applied to `s` and `p` for all elements in `α` is never equal to infinity. The `Set.indicator` function here returns the value of `p` for an element if the element is in the set `s`, and `0` otherwise.
More concisely: For any probability mass function `p` and set `s` of the same type, the sum of `Set.indicator` functions of `s` and `p` over all elements of the type is finite.
|
PMF.tsum_coe
theorem PMF.tsum_coe : ∀ {α : Type u_1} (p : PMF α), ∑' (a : α), p a = 1
The theorem `PMF.tsum_coe` states that for any given probability mass function `p` defined over a type `α`, the sum of probabilities assigned by `p` to all elements of `α` equals to `1`. This is essentially the property of a probability mass function being a probability measure on a discrete set, where the total probability assigned to the entire set is `1`.
More concisely: For any probability mass function `p` over type `α`, the sum of `p` over all elements of `α` equals 1. In Lean syntax: `∑ (x : α), p x = 1`.
|
Mathlib.Probability.ProbabilityMassFunction.Basic._auxLemma.2
theorem Mathlib.Probability.ProbabilityMassFunction.Basic._auxLemma.2 :
∀ {α : Type u_1} (p : PMF α) (a : α), (a ∈ p.support) = (p a ≠ 0)
This theorem states that for any type `α` and a probability mass function `p` over that type, and any element `a` of type `α`, `a` is in the support of `p` if and only if the value of `p` at `a` is not zero. The support of a probability mass function is the set of all points where the function is non-zero. So, this theorem is essentially defining the support of `p` in terms of the values of `p`.
More concisely: The support of a probability mass function `p` over type `α` equals the set of elements `a` in `α` such that `p a ≠ 0`.
|
PMF.toOuterMeasure_apply
theorem PMF.toOuterMeasure_apply :
∀ {α : Type u_1} (p : PMF α) (s : Set α), ↑p.toOuterMeasure s = ∑' (x : α), s.indicator (⇑p) x
This theorem, `PMF.toOuterMeasure_apply`, states that for any type `α`, any probability mass function `p` over `α`, and any set `s` of `α`, the measure of the set `s` under the outer measure constructed from the probability mass function `p` is equal to the sum (potentially infinite) over all elements `x` of `α` of the value of `p` at `x`, but only considering those `x` that belong to `s` (this is what the set indicator function ensures). In other words, it is summing up the probabilities of each element in the set `s` according to the probability mass function `p`, which corresponds to the measure of `s`.
More concisely: For any probability mass function `p` over a type `α` and any set `s` of `α`, the outer measure of `s` constructed from `p` equals the sum of `p` over all elements in `s`.
|
PMF.mem_support_iff
theorem PMF.mem_support_iff : ∀ {α : Type u_1} (p : PMF α) (a : α), a ∈ p.support ↔ p a ≠ 0
The theorem `PMF.mem_support_iff` states that for any type `α` and any probability mass function `p : PMF α`, an element `a : α` belongs to the support of `p` if and only if the value of `p` at `a` is not equal to zero. In other words, the support of a probability mass function is exactly the set of points where the function is nonzero.
More concisely: The support of a probability mass function `p : PMF α` equals the set of elements `a : α` such that `p a ≠ 0`.
|
PMF.toOuterMeasure_mono
theorem PMF.toOuterMeasure_mono :
∀ {α : Type u_1} (p : PMF α) {s t : Set α}, s ∩ p.support ⊆ t → ↑p.toOuterMeasure s ≤ ↑p.toOuterMeasure t := by
sorry
This theorem, `PMF.toOuterMeasure_mono`, is a slightly stronger variation of `OuterMeasure.mono` that incorporates an intersection with `p.support`. It states that for any type `α`, given a probability mass function `p` of type `α`, and sets `s` and `t` of type `α`, if the intersection of `s` and `p.support` is a subset of `t`, then the outer measure of `s` with respect to `p` is less than or equal to the outer measure of `t` with respect to `p`. Here, `p.support` refers to the set of elements where the probability mass function `p` is positive. The outer measure of a set is a generalized concept of the size of the set, possibly infinite, compliant with `p`.
More concisely: For any probability mass function `p` and sets `s` and `t` such that `s ⊆ p.support ∩ t`, we have `OuterMeasure p s ≤ OuterMeasure p t`.
|