PMF.binomial_one_eq_bernoulli

theorem PMF.binomial_one_eq_bernoulli : ∀ (p : ENNReal) (h : p ≤ 1), PMF.binomial p h 1 = PMF.map (fun x => bif x then 1 else 0) (PMF.bernoulli p h) := by sorry

The theorem `PMF.binomial_one_eq_bernoulli` states that for all extended nonnegative real numbers `p` such that `p` is less than or equal to 1, the binomial distribution with `n` equals to 1 (which is the probability of observing exactly `i` "heads" in a sequence of 1 independent coin toss) is equal to the mapping of the Bernoulli distribution (which assigns probability `p` to `true` and `1 - p` to `false`) with a function that assigns `1` for `true` and `0` for `false`. This theorem essentially expresses that the binomial distribution for a single coin toss is equivalent to the Bernoulli distribution.

More concisely: The binomial distribution for a single coin toss with probability `p` of heads is equal to the Bernoulli distribution with parameter `p`.