avewright/proofwiki-math huggingface dataset:
Theorem: Negative Binomial Distribution as Generalized Geometric Distribution/Type 2

The type $2$ negative binomial distribution is a generalization of the geometric distribution:
Let $\sequence {X_i}$ be a binomial experiment with parameter $p$.
Let $\EE$ be the experiment which consists of:
:Perform the Bernoulli trial $X_i$ until $n$ failures occur, and then stop.
Let $k$ be the number of successes before before $n$ failures have been encountered.
Let $\EE'$ be the experiment which consists of:
:Perform the Bernoulli trial $X_i$ until '''one''' failure occurs, and then stop.
Then $k$ is modelled by the experiment:
:Perform experiment $\EE'$ until $n$ failures occur, and then stop.

Proof:
Consider the experiment $\EE$ as described.
By definition, $\EE$ is modelled by a type $2$ negative binomial distribution with parameters $n$ and $p$:
:$\forall k \in \Z, k \ge 0: \map \Pr {X = k} = \dbinom {n + k - 1} {n - 1} p^k q^n $
where $q = 1 - p$.
Now consider the experiment $\EE'$ as described.
By Bernoulli Process as Geometric Distribution, $\EE'$ is modelled by a geometric distribution with parameter $p$:
:$\forall k \in \Z, k \ge 0: \map \Pr {X = k} = p^k q$
where $q = 1 - p$.
{{proof wanted|Requires further results}}
Theorem: Negative Binomial Distribution as Generalized Geometric Distribution/Type 1

The type $1$ negative binomial distribution is a generalization of the shifted geometric distribution:
Let $\sequence {Y_i}$ be a binomial experiment with parameter $p$.
Let $\FF$ be the experiment which consists of:
:Perform the Bernoulli trial $Y_i$ as many times as it takes to achieve $n$ successes, and then stop.
Let $k$ be the number of Bernoulli trials that need to be taken in order to achieve up to (and including) the $n$th success.
Let $\FF'$ be the experiment which consists of:
:Perform the Bernoulli trial $Y_i$ until '''one''' success is achieved, and then stop.
Then $k$ is modelled by the experiment:
:Perform experiment $\FF'$ until $n$ failures occur, and then stop.

Proof:
Consider the experiment $\FF$ as described.
By definition, $\FF$ is modelled by a negative binomial distribution with parameters $n$ and $p$:
:$\ds \forall k \in \Z, k \ge n: \map \Pr {Y = k} = \binom {k - 1} {n - 1} q^{k - n} p^n$
where $q = 1 - p$.
Now consider the experiment $\FF'$ as described.
By Bernoulli Process as Shifted Geometric Distribution, $\FF'$ is modelled by a geometric distribution with parameter $p$:
:$\forall k \in \Z, k \ge 1: \map \Pr {Y = k} = q^{k - 1} p$
where $q = 1 - p$.
{{proof wanted|Requires further results, which are on their way.}}
Category:Negative Binomial Distribution as Generalized Geometric Distribution
Category:Negative Binomial Distribution (Type 1)
Category:Geometric Distribution
ascg1t4wo8l6imvwn92kx29yid7romk
Theorem: Equivalence of Definitions of Variance of Discrete Random Variable

Let $X$ be a discrete random variable.
Let $\mu = \expect X$ be the expectation of $X$.
{{TFAE|def = Variance of Discrete Random Variable}}

Proof:
=== Definition 1 equivalent to Definition 2 ===
Let $\var X$ be defined as:
:$\var X := \expect {\paren {X - \expect X}^2}$
Let $\mu = \expect X$.
Let $\map f X = \paren {X - \mu}^2$ be considered as a function of $X$.
Then by applying Expectation of Function of Discrete Random Variable:
:$\ds \expect {\map f X} = \sum_{x \mathop \in \Omega_X} \map f x \, \map \Pr {X = x}$
which leads to:
:$\ds \expect {\paren {X - \mu}^2} = \sum_{x \mathop \in \Omega_X} \paren {\paren {X - \mu}^2} \map \Pr {X = x}$
thus demonstrating the equality of Definition 1 to Definition 2.
{{qed|lemma}}
Theorem: Derivative of Geometric Sequence/Corollary

:$\ds \sum_{n \mathop \ge 1} n \paren {n + 1} x^{n - 1} = \frac 2 {\paren {1 - x}^3}$

Proof:
We have from Power Rule for Derivatives that:
:$\ds \frac {\d} {\d x} \sum_{n \mathop \ge 1} \paren {n + 1} x^n = \sum_{n \mathop \ge 1} n \paren {n + 1} x^{n - 1}$
But from Sum of Infinite Geometric Sequence:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop \ge 1} \paren {n + 1} x^n
      | r = \sum_{m \mathop \ge 2} m x^{m - 1}
      | c = 
}}
{{eqn | r = \sum_{m \mathop \ge 1} m x^{m - 1} - 1
      | c = taking into account the first term
}}
{{eqn | r = \frac 1 {\paren {1 - x}^2} - 1
      | c = from main result above
}}
{{end-eqn}}
The result follows by Power Rule for Derivatives and the Chain Rule for Derivatives applied to $\dfrac 1 {\paren {1 - x}^2}$.
{{Qed}}
Category:Analysis
Category:Differential Calculus
Category:Geometric Sequences
b6dw3ganjx86hk3lzxelqjtbmq9vrse
Theorem: Equivalence of Definitions of Countable Set

Let $S$ be a set.
{{TFAE|def = Countable Set}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $S$ be a countable set by Definition 1.
Then there is an injection $f: S \to \N$.
By Law of Excluded Middle, $S$ is finite or infinite.
If $S$ is finite, then it trivially satisfies Definition 2.
{{explain|Implicitly we take $S \cong f[S]$ here}}
If $S$ is infinite, then it is countably infinite by Infinite Set of Natural Numbers is Countably Infinite, and thus satisfies Definition 2.
{{qed|lemma}}
Theorem: Infinite Set of Natural Numbers is Countably Infinite

Let $\N$ be the set of natural numbers.
Let $S$ be an infinite subset of $\N$.
Then $S$ is countably infinite.
That is, there is a bijection $f: \N \to S$.

Proof:
By Infinite Set has Countably Infinite Subset, we have an injection $g: \N \to S$
But by Cantor-Bernstein-Schröder Theorem/Lemma this produces a bijection $f: \N \to S$
{{qed}}
Theorem: Generating Function for Powers of Two

Let $\sequence {a_n}$ be the sequence defined as:
:$\forall n \in \N: a_n = 2^n$
That is:
:$\sequence {a_n} = 1, 2, 4, 8, \ldots$
Then the generating function for $\sequence {a_n}$ is given as:
:$\map G z = \dfrac 1 {1 - 2 z}$ for $\size z < \dfrac 1 2$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = 1 + 2 z + 4 z^2 + \cdots
      | c = 
}}
{{eqn | r = \sum_{n \mathop \ge 0} \paren {2 z}^n
      | c = 
}}
{{eqn | r = \frac 1 {1 - 2 z}
      | c = Sum of Infinite Geometric Sequence
}}
{{end-eqn}}
This is valid for:
:$\size {2 z} < 1$
from which:
:$\size z < \dfrac 1 2$
follows directly by division by $2$.
The result follows from the definition of a generating function.
{{qed}}
Theorem: Generating Function for Natural Numbers

Let $\sequence {a_n}$ be the sequence defined as:
:$\forall n \in \N_{> 0}: a_n = n - 1$
That is:
:$\sequence {a_n} = 0, 1, 2, 3, 4, \ldots$
Then the generating function for $\sequence {a_n}$ is given as:
:$G \paren z = \dfrac 1 {\paren {1 - z}^2}$

Proof:
Take the sequence:
:$S_n = 1, 1, 1, \ldots$
From Generating Function for Constant Sequence, this has the generating function:
:$\ds G \paren z = \sum_{n \mathop = 1}^\infty z^n = \frac 1 {1 - z}$
By Derivative of Generating Function:
:$\ds \dfrac \d {\d z} G \paren z = 0 + 1 + 2 z + 3 z^2 \cdots = \sum_{n \mathop \ge 0} \paren {n + 1} z^n$
which is the generating function for the sequence $\sequence {a_n}$.
But:
:$G \paren z = \dfrac 1 {1 - z}$
and so by Power Rule for Derivatives and the Chain Rule for Derivatives:
:$\dfrac \d {\d z} G \paren z = \dfrac 1 {\paren {1 - z}^2}$
The result follows from the definition of a generating function.
{{qed}}
Theorem: Injection has Surjective Left Inverse Mapping

Let $S$ and $T$ be sets such that $S \ne \O$.
Let $f: S \to T$ be a injection.
Then there exists a surjection $g: T \to S$ such that:
:$g \circ f = I_S$

Proof:
Since $S$ is non-empty, we can choose an element $x \in S$.
Since $f$ is an injection, for each $t \in \Img f$ there exists a unique $s \in S$ such that:
:$\map f s = t$
Thus by Law of Excluded Middle there exists a well-defined mapping $T \to S$ given by:
:$\map g t = \begin {cases} s & : \paren {t \in \Img f} \land \paren {\map f s = t} \\ x & : t \notin \Img f \end {cases}$
By construction, for any given $s \in S$, the element $\map f s$ maps to $s$ under $g$.
Therefore $g: T \to S$ is a surjection.
{{qed}}
Theorem: Injection has Surjective Left Inverse Mapping

Let $S$ and $T$ be sets such that $S \ne \O$.
Let $f: S \to T$ be a injection.
Then there exists a surjection $g: T \to S$ such that:
:$g \circ f = I_S$

Proof:
By Injection iff Left Inverse, $f$ has a left inverse $g: T \to S$.
By Left Inverse Mapping is Surjection, $g$ is a surjection.
{{qed}}
Theorem: Many-to-One Relation Extends to Mapping

Let $S$ and $T$ be sets.
Let $T$ be non-empty.
Let $\RR \subset S \times T$ be a many-to-one relation.
Then there exists a mapping $f: S \to T$ such that $\RR \subseteq f$.

Proof:
Since $T$ is not empty, it has an element $t_0$.
Define a mapping $g: S \setminus \Preimg \RR$ by letting $\map g x = t_0$ for all $x \in S$.
Let $f = \RR \cup g$ be a relation on $S \times T$.
By Union of Many-to-One Relations with Disjoint Domains is Many-to-One, $f$ is a many-to-one relation.
By Union with Relative Complement, $f$ is total.
Thus $f$ is a mapping.
{{qed}}
{{LEM|Union with Relative Complement}}
Category:Relation Theory
Category:Mapping Theory
8v93vvxcxbhep6xqmr1x1zw5vphfapm
Theorem: Generating Function for Binomial Coefficients

Let $\sequence {a_n}$ be the sequence defined as:
:$\forall n \in \N: a_n = \begin{cases}
\dbinom m n & : n = 0, 1, 2, \ldots, m \\
0 & : \text{otherwise}\end{cases}$
where $\dbinom m n$ denotes a binomial coefficient.
Then the generating function for $\sequence {a_n}$ is given as:
:$\ds \map G z = \sum_{n \mathop = 0}^m \dbinom m n z^n = \paren {1 + z}^m$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {1 + z}^m
      | r = \sum_{n \mathop = 0}^m \binom m n z^n
      | c = Binomial Theorem
}}
{{end-eqn}}
The result follows from the definition of a generating function.
{{qed}}
Theorem: Probability Generating Function of Zero

:$\map {\Pi_X} 0 = \map {p_X} 0$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\Pi_X} 0
      | r = \map {p_X} 0 + 0^1 \cdot \map {p_X} 1 + 0^2 \cdot \map {p_X} 2 + \cdots
      | c = {{Defof|Probability Generating Function}}
}}
{{eqn | r = \map {p_X} 0 + 0 + 0 + \cdots
      | c = as $\forall n \in \N_{>0}: s^n = 0$
}}
{{eqn | r = \map {p_X} 0
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Probability Generating Function of One

:$\map {\Pi_X} 1 = 1$

Proof:
{{begin-eqn}}
{{eqn | l=\map {\Pi_X} 1
      | r=\map {p_X} 0 + 1^1 \cdot \map {p_X} 1 + 1^2 \cdot \map {p_X} 2 + \cdots
      | c={{Defof|Probability Generating Function}}
}}
{{eqn | r=\map {p_X} 0 + \map {p_X} 1 + \map {p_X} 2 + \cdots
      | c=as $\forall n \in \N_{>0}: s^n = 1$
}}
{{eqn | r=\sum_{n \mathop = 0}^\infty \map {p_X} n
      | c=
}}
{{eqn | r=\sum_{x \mathop \in \Omega_X} \map {p_X} x
      | c=by definition of $\Omega_X$
}}
{{eqn | r=1
      | c={{Defof|Probability Mass Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Probability Generating Function as Expectation

Let $X$ be a discrete random variable whose codomain, $\Omega_X$, is a subset of the natural numbers $\N$.
Let $p_X$ be the probability mass function for $X$.
Let $\map {\Pi_X} s$ be the probability generating function for $X$.
Then:
:$\map {\Pi_X} s = \expect {s^X}$
where $\expect {s^X}$ denotes the expectation of $s^X$.

Proof:
By definition of probability generating function:
:$\ds \map {\Pi_X} s := \sum_{n \mathop = 0}^\infty \map {p_X} n s^n = \map {p_X} 0 + \map {p_X} 1 s + \map {p_X} 2 s^2 + \cdots$
where $p_X$ is the probability mass function for $X$.
For any real function $g: \R \to \R$, by Expectation of Function of Discrete Random Variable:
:$\ds \expect {\map g X} = \sum_{x \mathop \in \Omega_X} \map g X \map \Pr {X = x}$
whenever the sum is absolutely convergent.
In this case:
:$\map g X = s^X$
Thus:
:$\ds \expect {s^X} = \sum_{x \mathop \in \Omega_X} s^x \map \Pr {X = x}$
or, using $\map {p_X} x := \map \Pr {X = x}$:
:$\ds \expect {s^X} = \sum_{x \mathop \in \Omega_X} \map {p_X} x s^x$
By definition of $X$, this can then be expressed as:
:$\ds \expect {s^X} = \sum_{n \mathop = 0}^\infty \map {p_X} n s^n$
Thus whenever $\ds \sum_{n \mathop = 0}^\infty \map {p_X} n s^n$ is absolutely convergent:
:$\map {\Pi_X} s = \expect {s^X}$
by definition of probability mass function.
As $p_X$ is a probability mass function for $X$:
:$\ds \sum_{k \mathop = 0}^\infty \map {p_X} k = 1$
Thus the condition on absolute convergence is satisfied by all $s$ such that $\size s < 1$ by the observation:
:$\ds  \sum_{k \mathop = 0}^\infty \size {\map {p_X} k s^k} \le \sum_{k \mathop = 0}^\infty \map {p_X} k= 1$
{{qed}}
Theorem: Probability Generating Function defines Probability Distribution

Let $X$ and $Y$ be discrete random variables  whose codomain, $\Omega_X$, is a subset of the natural numbers $\N$.
Let the probability generating functions of $X$ and $Y$ be $\map {\Pi_X} s$ and $\map {\Pi_Y} s$ respectively.
Then:
:$\forall s \in \closedint {-1} 1: \map {\Pi_X} s = \map {\Pi_Y} s$
{{iff}}:
:$\forall k \in \N: \Pr \left({X = k}\right) = \map \Pr {Y = k}$
That is, discrete random variables which are integer-valued have the same PGFs {{iff}} they have the same PMF.

Proof:
By the definition of PGF, it follows that if:
:$\forall k \in \N: \map \Pr {X = k} = \map \Pr {Y = k}$
then:
:$\forall s \in \closedint {-1} 1: \map {\Pi_X} s = \map {\Pi_Y} s$
Suppose that $\map {\Pi_X} s = \map {\Pi_Y} s$ for all $s \in \closedint {-1} 1$.
From Probability Generating Function as Expectation the radius of convergence of both $\map {\Pi_X} s$ and $\Pi_Y \left({s}\right)$ is at least $1$.
Therefore they have unique power series expansions about $s = 0$:
:$\ds \map {\Pi_X} s = \sum_{n \mathop = 0}^\infty s^n \map \Pr {X = k}$
:$\ds \map {\Pi_Y} s = \sum_{n \mathop = 0}^\infty s^n \map \Pr {Y = k}$
As $\map {\Pi_X} s = \map {\Pi_Y} s$, these two power series have identical coefficients.
{{handwaving|It needs to be demonstrated that those power series expansions actually are unique. This has not been done.}}
Hence the result.
{{qed}}
Theorem: Probability Generating Function of Negative Binomial Distribution/Type 2

Let $X$ be a discrete random variable with the type $2$ negative binomial distribution with parameters $n$ and $p$.
Then the p.g.f. of $X$ is:
:$\map {\Pi_X} s = \paren {\dfrac q {1 - p s} }^n$
where $q = 1 - p$.

Proof:
From the definition of p.g.f:
:$\ds \map {\Pi_X} s = \sum_{k \mathop \ge 0} \map {p_X} k s^k$
From the definition of the type $2$ negative binomial distribution:
:$\map {p_X} k = \dbinom {n + k - 1} {n - 1} p^k q^n$
where $q = 1 - p$.
So:
{{begin-eqn}}
{{eqn | l = \map {\Pi_X} s
      | r = \sum_{k \mathop \ge 0} \binom {n + k - 1} {n - 1} p^k q^n s^k
      | c = 
}}
{{eqn | r = q^n \sum_{k \mathop \ge 0} \binom {n + k - 1} {n - 1} \paren {p s}^k
      | c = 
}}
{{eqn | r = \paren {\frac q {1 - p s} }^n
      | c = 
}}
{{end-eqn}}
For the third equality, the equation in the second line is rewritten in terms of binomial series.
{{explain|Yes all very well, but it's still not trivial.}}
Hence the result.
{{qed}}
Theorem: Probability Generating Function of Negative Binomial Distribution/Type 1

Let $X$ be a discrete random variable with the type 1 negative binomial distribution with parameters $n$ and $p$.
Then the p.g.f. of $X$ is:
:$\ds \map {\Pi_X} s = \paren {\frac {p s} {1 - q s} }^n$
where $q = 1 - p$.

Proof:
From the definition of p.g.f:
:$\ds \map {\Pi_X} s = \sum_{k \mathop \ge 0} \map {p_X} k s^k$
From the definition of the type $1$ negative binomial distribution:
:$\map {p_X} k = \dbinom {k - 1} {n - 1} p^n q^{k - n}$
where $q = 1 - p$.
So:
{{begin-eqn}}
{{eqn | l = \map {\Pi_X} s
      | r = \sum_{k \mathop \ge n} \binom {k - 1} {n - 1} p^n q^{k - n} s^k
      | c = 
}}
{{eqn | r = \frac {p^n} {q^n} \sum_{k \mathop \ge n} \binom {k - 1} {n - 1} \paren {q s}^k
      | c = 
}}
{{eqn | r = \paren {\frac {p s} {1 - q s} }^n
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Fundamental Theorem of Calculus for Contour Integrals/Corollary

Let $D \subseteq \C$ be an open set.
Let $f: D \to \C$ be a continuous function.
Suppose that $F: D \to \C$ is an antiderivative of $f$.
Let $\gamma: \closedint a b \to D$ be a contour that consists of one directed smooth curve.
Then the contour integral:
:$\ds \int_\gamma \map f z \rd z =  \map F {\map \gamma b} - \map F {\map \gamma a}$

Proof:
By the chain rule:
:$\dfrac \d {\d t} \map F {\map \gamma t} = \map {F'} {\map \gamma t} \map {\gamma'} t = \map f {\map \gamma t} \map {\gamma'} t$
Thus:
{{begin-eqn}}
{{eqn | l = \int_\gamma \map f z \rd z
      | r = \int_a^b \map f {\map \gamma t} \map {\gamma'} t \rd t
      | c = {{Defof|Complex Primitive|Antiderivative}}
}}
{{eqn | r = \int_a^b \frac \d {\d t} \map F {\map \gamma t} \rd t
      | c = 
}}
{{eqn | r = \map F {\map \gamma b} - \map F {\map \gamma a}
      | c = Fundamental Theorem of Calculus
}}
{{end-eqn}}
{{qed}}
Category:Fundamental Theorem of Calculus for Contour Integrals
7yr2fzwetcfd1ef47ro21v5qt4alc8e
Theorem: Probability Generating Function of Scalar Multiple of Random Variable

Let $X$ be a discrete random variable whose probability generating function is $\map {\Pi_X} s$.
Let $k \in \Z_{\ge 0}$ be a positive integer.
Let $Y$ be a discrete random variable such that $Y = m X$.
Then
:$\map {\Pi_Y} s = \map {\Pi_X} {s^m}$
where $\map {\Pi_Y} s$ is the probability generating function of $Y$.

Proof:
From the definition of p.g.f:
:$\ds \map {\Pi_X} s = \sum_{k \mathop \ge 0} \map \Pr {X = k} s^k$
We have {{hypothesis}}:
:$\map \Pr {Y = m k} = \map \Pr {X = k}$
Thus:
:$\ds \map {\Pi_Y} s = \sum_{m k \mathop \ge 0} \map \Pr {X = k} s^{m k}$
From the definition of a probability generating function:
:$\map {\Pi_Y} s = \map {\Pi_X} {s^m}$
{{qed}}
Theorem: Probability Generating Function of Shifted Random Variable

Let $X$ be a discrete random variable whose probability generating function is $\map {\Pi_X} s$.
Let $k \in \Z_{\ge 0}$ be a positive integer.
Let $Y$ be a discrete random variable such that $Y = X + m$.
Then
:$\map {\Pi_Y} s = s^m \map {\Pi_X} s$
where $\map {\Pi_Y} s$ is the probability generating function of $Y$.

Proof:
From the definition of p.g.f:
:$\ds \map {\Pi_X} s = \sum_{k \mathop \ge 0} \map \Pr {X = k} s^k$
By hypothesis:
:$\map \Pr {Y = k + m} = \map \Pr {X = k}$
Thus:
{{begin-eqn}}
{{eqn | l = \map {\Pi_Y} s
      | r = \sum_{k + m \mathop \ge 0} \map \Pr {X = k} s^{k + m}
      | c = 
}}
{{eqn | r = \sum_{k + m \mathop \ge 0} \map \Pr {X = k} s^m s^k
      | c = 
}}
{{eqn | r = s^m \sum_{k \mathop \ge 0} \map \Pr {X = k} s^k
      | c = Translation of Index Variable of Summation
}}
{{end-eqn}}
{{finish|The last step needs to be expanded and explained as to why we can just lose the $m$ out of the index.}}
From the definition of a probability generating function:
:$\map {\Pi_Y} s = s^m \map {\Pi_X} s$
{{qed}}
Theorem: Derivatives of Probability Generating Function at One

Let $X$ be a discrete random variable whose probability generating function is $\map {\Pi_X} s$.
Then the $n$th derivative of $\map {\Pi_X} s$ at $s = 1$ is given by:
:$\dfrac {\d^n} {\d s^n} \map {\Pi_X} 1 = \expect {X \paren {X - 1}  \cdots \paren {X - n + 1} }$
for $n = 1, 2, \ldots$

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\dfrac {\d^n} {\d s^n} \map {\Pi_X} 1 = \expect {X \paren {X - 1}  \cdots \paren {X - n + 1} }$
Theorem: Expectation of Square of Discrete Random Variable

Let $X$ be a discrete random variable whose probability generating function is $\map {\Pi_X} s$.
Then the square of the expectation of $X$ is given by the expression:
:$\expect {X^2} = \map { {\Pi_X}''} 1 + \map { {\Pi_X}'} 1$
where $\map { {\Pi_X}''} 1$ and $\map { {\Pi_X}'} 1$ denote the second and first derivative respectively of the PGF $\map {\Pi_X} s$ evaluated at $1$.

Proof:
From Derivatives of Probability Generating Function at One:
:$\map { {\Pi_X}''} 1 = \expect {X \paren {X - 1} }$
and from Expectation of Discrete Random Variable from PGF:
:$\map { {\Pi_X}'} 1 = \expect X$
So:
{{begin-eqn}}
{{eqn | l = \expect {X^2}
      | r = \expect {X \paren {X - 1} + X}
      | c = Algebra: $X \paren {X - 1} + X = X^2 - X + X$
}}
{{eqn | r = \expect {X \paren {X - 1} } + \expect X
      | c = Expectation is Linear
}}
{{eqn | r = \map { {\Pi_X}''} 1 + \map { {\Pi_X}'} 1
      | c = from above
}}
{{end-eqn}}
{{qed}}
Theorem: Non-Equivalence of Proposition and Negation/Formulation 1

:$p \implies \neg p, \neg p \implies p \vdash \bot$

Proof:
{{BeginTableau|p \implies \neg p, \neg p \implies p \vdash \bot}}
{{Premise|1|p \implies \neg p}}
{{Premise|2|\neg p \implies p}}
{{SequentIntro|3|1|\neg p|1|Proof by Contradiction: Variant 3}}
{{ModusPonens|4|1, 2|p|2|3}}
{{NonContradiction|5|1, 2|4|3}}
{{EndTableau}}
{{qed}}
Category:Contradiction
Category:Conditional
tg7z0cwpdzx5xrf99qzslj4umnnh9ke
Theorem: Non-Equivalence of Proposition and Negation/Formulation 2

:$\vdash \neg \left({p \iff \neg p}\right)$

Proof:
{{BeginTableau|$\vdash \neg \left({p \iff \neg p}\right)$}}
{{Assumption|1|p \iff \neg p}}
{{BiconditionalElimination|2|1|p \implies \neg p|1|1}}
{{BiconditionalElimination|3|1|\neg p \implies p|1|2}}
{{SequentIntro|4|1|\bot|2,3|Non-Equivalence of Proposition and Negation: Formulation 1}}
{{Contradiction|5||\neg \left({p \iff \neg p}\right)|1|4}}
{{EndTableau}}
Category:Biconditional
Category:Contradiction
6y8o80gajctqmhj9do2tot370fd1goa
Theorem: No Injection from Power Set to Set/Lemma

Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Then there does not exist a set $B$ such that there is an injection from $B$ into $S$ and a surjection from $B$ onto $\powerset S$.

Proof:
{{AimForCont}} there exists such a $B$.
Let $i: B \to S$ be an injection.
Let $f: B \to \powerset S$ be a surjection.
Let $i^\gets: \powerset S \to \powerset B$ be the inverse image mapping of $i$.
By Mapping Induced by Inverse of Injection is Surjection, $i^\gets$ is a surjection.
Let $f^\to: \powerset B \to \powerset {\powerset S}$ be the direct image mapping of $f$.
By Direct Image Mapping of Surjection is Surjection, $f^\to$ is a surjection:
We have that $i^\gets: \powerset S \to \powerset B$ and $f^\to: \powerset B \to \powerset {\powerset S}$ are surjective.
By Composite of Surjections is Surjection, their composition $f^\to \circ i^\gets: \powerset S \to \powerset {\powerset S}$ is a surjection by Composite of Surjections is Surjection.
But this violates Cantor's Theorem, contradicting the assumption that such a $B$ exists.
{{qed}}
Category:No Injection from Power Set to Set
1ql65yf6orlqu33iz4o99xptqbjb2mu
Theorem: No Injection from Power Set to Set

Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Then there is no injection from $\powerset S$ into $S$.

Proof:
{{AimForCont}} $f: \powerset S \to S$ is an injection.
By Injection has Surjective Left Inverse Mapping, there is a surjection $g: S \to \powerset S$.
But this contradicts Cantor's Theorem.
Thus there can be no such injection. 
{{qed}}
{{LEM|Injection has Surjective Left Inverse Mapping|3}}
Theorem: No Injection from Power Set to Set

Let $S$ be a set.
Let $\powerset S$ be the power set of $S$.
Then there is no injection from $\powerset S$ into $S$.

Proof:
=== Lemma ===
{{:No Injection from Power Set to Set/Lemma}}{{qed|lemma}}
The identity mapping $I_{\powerset S}: \powerset S \to \powerset S$ is a surjection by Identity Mapping is Surjection.
Thus, by the lemma, there can be no injection from $\powerset S$ into $S$.
{{qed}}
Theorem: Inverse Image Mapping of Injection is Surjection

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a injection.
Let $f^\gets: \powerset T \to \powerset S$ be the inverse image mapping of $f$.
Then $f^\gets$ is a surjection.

Proof:
Let $f^\to: \powerset S \to \powerset T$ be the direct image mapping by $f$.
Let $X \in \powerset S$.
Let $Y = \map {f^\to} X$.
By Subset equals Preimage of Image iff Mapping is Injection:
:$\map {f^\gets} Y = X$
As such a $Y$ exists for each $X \in \powerset S$, $f^\gets$ is surjective.
{{qed}}
Category:Injections
Category:Surjections
Category:Inverse Image Mappings
ltk5ardk0aufh7a49pbn3p9w47lqk9x
Theorem: Expectation and Variance of Poisson Distribution equal its Parameter

Let $X$ be a discrete random variable with the Poisson distribution with parameter $\lambda$.
Then the expectation of $X$ equals the variance of $X$, that is, $\lambda$ itself.

Proof:
From Expectation of Poisson Distribution:
:$\expect X = \lambda$
From Variance of Poisson Distribution:
:$\var X = \lambda$
{{qed}}