avewright/proofwiki-math huggingface dataset:
Theorem: Poincaré Conjecture/Dimension 3

Let $\Sigma^3$ be a smooth $3$-manifold.
Let $\Sigma^3$ satisfy:
:$H_0 \struct {\Sigma; \Z} = 0$
and:
:$H_3 \struct {\Sigma; \Z} = \Z$
Then $\Sigma^3$ is homeomorphic to the $3$-sphere $\Bbb S^3$.
{{explain|Definition of the notation $H_0 \struct {\Sigma; \Z}$, nature of $H_0$ and $H_3$}}

Proof:
Follows from Thurston's Geometrization Conjecture.
{{ProofWanted}}
Theorem: Poincaré Conjecture/Dimension 4

Let $\Sigma^4$ be a smooth $4$-manifold.
Let $\Sigma^4$ satisfy:
:$H_0 \struct {\Sigma; \Z} = 0$
and:
:$H_4 \struct {\Sigma; \Z} = \Z$
Then $\Sigma^4$ is homeomorphic to the $4$-sphere $\Bbb S^4$.
{{explain|Definition of the notation $H_0 \struct {\Sigma; \Z}$, nature of $H_0$ and $H_4$}}

Proof:
Follows from $4$-dimensional Topological $h$-Cobordism Theorem.
{{ProofWanted}}
Theorem: Poincaré Conjecture/Dimension 6 or Greater

Let $\Sigma^m$ be a smooth $m$-manifold where $m \ge 6$.
Let $\Sigma^m$ satisfy:
:$H_0 \struct {\Sigma; \Z} = 0$
and:
:$H_m \struct {\Sigma; \Z} = \Z$
Then $\Sigma^m$ is homeomorphic to the $m$-sphere $\Bbb S^m$.

Proof:
We can cut two small $m$-disks $D', D' '$ from $\Sigma$.
The remaining manifold, $\Sigma \setminus \paren {D' \cup D' '}$ is an h-cobordism between $\partial D'$ and $\partial D' '$.
These are just two copies of $\Bbb S^{m-1}$.
By the $h$-cobordism theorem, there exists a diffeomorphism:
:$\phi: \Sigma \setminus \paren {D' \cup D' '} \to \Bbb S^{m - 1} \times \closedint 0 1$
which can be chosen to restrict to the identity on one of the $\Bbb S^{m - 1}$.
Let $\Xi$ denote this $\Bbb S^{m - 1}$ such that $\phi$ restricts to the identity.
Since $\psi \vert_\Xi = Id$, we can extend $\psi$ across $D' '$, the interior of $\Xi$ to obtain a diffeomorphism $\phi': \Sigma \setminus D' ' \to \Bbb S^{m - 1} \cup D'$.
{{explain|What does $\psi \vert_\Xi$ mean?}}
Let $\Bbb D^m$ denote this latter manifold, which is merely an $m$-disk.
Our diffeomorphism $\phi': \Sigma \setminus D' ' \to \Bbb D^m$ induces a diffeomorphism on the boundary spheres $\Bbb S^{m - 1}$.
Any diffeomorphism of the boundary sphere $\Bbb S^{m - 1}$ can be extended radially to the whole disk:
:$\map {\operatorname {int} } {\Bbb S^{m - 1} } = D' '$
but only as a homeomorphism of $D' '$.  
Hence the extended function $\phi' ': \Sigma \to \Bbb S^m$ is a homeomorphism.
Theorem: Addition in Minimally Inductive Set is Unique

Let $\omega$ be the minimally inductive set.
Let $A: \omega \times \omega \to \omega$ be the mapping defined as the addition operation:
:$\forall \tuple {x, y} \in \omega \times \omega: \map A {x, y} = \begin {cases} x & : y = 0 \\ \paren {\map A {x, r} }^+ & : y = r^+ \end {cases}$
where $r^+$ is the successor set of $r$.
Then $A$ exists and is unique.

Proof:
Recall the Principle of Recursive Definition (Strong Version):
{{:Principle of Recursive Definition/Strong Version}}
From the von Neumann construction, this $\omega$ is exactly the minimally inductive set as defined in the problem statement.
Let $g: \omega \times \omega \to \omega$ be the mapping defined as:
:$\forall \tuple {x, y} \in \omega \times \omega: \map g {x, y} := y^+$
Hence from the Principle of Recursive Definition (Strong Version), there exists a unique mapping $f: \omega \to \omega$ such that:
:$\forall x \in \omega: \map f x = \begin{cases}
c & : x = \O \\
x^+ & : x = n^+
\end{cases}$
which we get by identifying $\map g {x, y}$ with $y^+$.
Let us fix some arbitrary $x_0 \in \omega$.
{{finish|I will defeat this beast}}
Theorem: Increasing Sequence of Sets forms Nest

Let $\sequence {a_n}$ be an increasing sequence of sets:
:$\forall k \in \N: S_k \subseteq S_{k + 1}$
Let $c = \set {a_1, a_1, \ldots, a_n, a_{n + 1}, \ldots}$ be the class of all terms of $\sequence {a_n}$.
Then $c$ is a nest.

Proof:
Recall the definition of nest:
$c$ is a '''nest''' {{iff}}:
:$\forall x, y \in c: x \subseteq y$ or $y \subseteq x$
Let $a_i$ and $a_j$ be arbitrary elements of $c$.
From Ordering on Natural Numbers is Trichotomy, either $i < j$ or $i = j$ or $i > j$.
;Case $(1)$
Let $i = j$.
Then we have $a_i = a_j$ and so both $a_i \subseteq a_j$ and $a_j \subseteq a_i$.
;Case $(2)$
Let $i \ne j$.
{{WLOG}}, suppose $i < j$.
Then as Subset Relation is Transitive:
:$a_i \subseteq a_j$
{{qed}}
{{improve|I believe the object of this exercise was to use theorems specifically introduced as part of the exposition by S&F in order to construct the minimally inductive class, but right now I have a day job to attend}}
Theorem: Minimally Inductive Class under Slowly Progressing Mapping is Nest

Let $M$ be a class.
Let $g: M \to M$ be a slowly progressing mapping on $M$.
Let $M$ be a minimally inductive class under $g$.
Then $M$ is a nest.

Proof:
By definition, a slowly progressing mapping is indeed a progressing mapping.
The result then follows from Minimally Inductive Class under Progressing Mapping induces Nest.
Theorem: Closed Form for Millin Series

The '''Millin series''' has the closed form expression:
:$\ds \sum_{n \mathop = 0}^\infty \frac 1 {F_{2^n} } = \frac {7 - \sqrt 5} 2$

Proof:
First we will prove that:
:$\ds \sum_{r \mathop = 0}^n \frac 1 {F_{2^r} } = 3 - \frac {F_{2^n - 1} } {F_{2^n} }$
for $n \ge 1$.
We see that:
:$\dfrac 1 {F_1} + \dfrac 1 {F_2} = 2 = 3 - \dfrac {F_1} {F_2}$ 
so the proposition holds for $n = 1$.
Suppose the proposition is true for $n = k$.
Then:
{{begin-eqn}}
{{eqn | l = \sum_{r \mathop = 0}^{k + 1}  \frac 1 {F_{2^r} } 
      | r = 3 - \frac {F_{2^k - 1} } {F_{2^k} } + \frac 1 {F_{2^{k + 1} } }
      | c = 
}}
{{eqn | r = 3 - \frac {F_{2^k - 1} F_{2^{k + 1} } - F_{2^k} } {F_{2^k} F_{2^{k + 1} } }
      | c = 
}}
{{eqn | r = 3 - \frac {F_{2^k - 1} F_{2^k} \paren {F_{2^k + 1} + F_{2^k - 1} } - F_{2^k} } {F_{2^k} F_{2^{k + 1} } }
      | c = repeated Fibonacci recurrence formula on $F_{2^{k + 1} }$ 
}}
{{eqn | r = 3 - \frac {F_{2^k - 1} F_{2^k + 1} + F_{2^k - 1}^2 - 1} {F_{2^{k + 1} } }
      | c = 
}}
{{eqn | r = 3 - \frac {F_{2^k}^2 + F_{2^k - 1}^2} {F_{2^{k + 1} } }
      | c = Cassini's Identity
}}
{{eqn | r = 3 - \frac {F_{2^{k + 1} - 1} } {F_{2^{k + 1} } }
      | c = repeated Fibonacci recurrence formula on $F_{2^{k + 1} - 1}$ 
}}
{{end-eqn}}
Thus by Principle of Mathematical Induction, the proof is complete. 
{{qed|lemma}}
Now taking the limit, we have:
{{begin-eqn}}
{{eqn | l = \sum_{r \mathop = 0}^\infty \frac 1 {F_{2^r} } 
      | r = \lim_{n \mathop \to \infty} \sum_{r \mathop = 0}^n \frac 1 {F_{2^r} }
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \paren {3 - \frac {F_{2^n - 1} } {F_{2^n } } }
      | c = 
}}
{{eqn | r = 3 - \frac 2 {\sqrt 5 + 1 } 
      | c = Ratio of Consecutive Fibonacci Numbers
}}
{{eqn | r = 3 - \frac 2 {\sqrt 5 + 1 } \paren {\frac {\sqrt 5 - 1 } {\sqrt 5 - 1 } }
      | c = multiplying by $1$
}}
{{eqn | r = 3 - \frac {2 \paren {\sqrt 5 - 1 } } 4
      | c = 
}}
{{eqn | r = 3 - \frac {\sqrt 5 - 1} 2
      | c = 
}}
{{eqn | r = \frac {7 - \sqrt 5} 2 
      | c = 
}}
{{end-eqn}}
as required.
{{qed}}
Theorem: Closed Form for Millin Series

The '''Millin series''' has the closed form expression:
:$\ds \sum_{n \mathop = 0}^\infty \frac 1 {F_{2^n} } = \frac {7 - \sqrt 5} 2$

Proof:
Let:
:$\ds \map F x := \sum_{k \mathop = 1}^\infty \frac {x^{2^{k - 1} } } {F_{2^k} }$
:$\alpha := \dfrac {1 + \sqrt 5} 2$
:$\beta := \dfrac {1 - \sqrt 5} 2$
Note that for $\size x \le 1$ we have:
:$\size {\dfrac {x^{2^{k - 1} } } {F_{2^k} } } \le \dfrac 1 {F_{2^k} }$
Given that the Millin Series converges, by Comparison Test:
:$\ds \map F x = \sum_{k \mathop = 1}^\infty \frac {x^{2^{k - 1} } } {F_{2^k} }$ converges for $\size x \le 1$
We have:
:$\ds \map F {\alpha x} := \sum_{k \mathop = 1}^\infty \frac {\alpha^{2^{k - 1} } x^{2^{k - 1} } } {F_{2^k} }$
Hence:
{{begin-eqn}}
{{eqn | l = \map F {\alpha x} + \map F {\beta x}
      | r = \sum_{k \mathop = 1}^\infty \frac {\alpha^{2^{k - 1} } + \beta^{2^{k - 1} } } {F_{2^k} } x^{2^{k - 1} }
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^\infty \frac {L_{2^{k - 1} } } {F_{2^k} } x^{2^{k - 1} }
      | c = Closed Form for Lucas Numbers
}}
{{eqn | r = \sum_{k \mathop = 1}^\infty \frac {x^{2^{k - 1} } } {F_{2^{k - 1} } } 
      | c = Fibonacci Number 2n equals Fibonacci Number n by Lucas Number n
}}
{{eqn | r = \sum_{k \mathop = 0}^\infty \frac {x^{2^k} } {F_{2^k} } 
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \frac {x^{2^0} } {F_{2^0} } + \sum_{k \mathop = 1}^\infty \frac {\paren {x^2}^{2^{k - 1} } } {F_{2^k} } 
      | c = 
}}
{{eqn | r = x + \map F {x^2}
      | c = 
}}
{{end-eqn}}
Since $\beta^2 = \dfrac {3 - \sqrt 5} 2 \le 1$, we can substitute $x = -\beta$:
{{begin-eqn}}
{{eqn | q = 
      | l = -\beta + \map F {\beta^2}
      | r = \map F {-\beta^2} + \map F {-\alpha \beta}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map F 1
      | r = -\beta + 2 \beta^2
      | c = as $\alpha \beta = -1$ and $\map F {\beta^2} = \map F {-\beta^2} + 2 \beta^2$
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 0}^\infty \frac 1 {F_{2^k} }
      | r = 1 + \map F 1
      | c = 
}}
{{eqn | r = 1 - \beta + 2 \beta^2
      | c = 
}}
{{eqn | r = 2 - \paren {1 + \beta - \beta^2} + \beta^2
      | c = 
}}
{{eqn | r = 2 + \dfrac {3 - \sqrt 5} 2
      | c = 
}}
{{eqn | r = \dfrac {7 - \sqrt 5} 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Successor Mapping is Slowly Progressing

Let $V$ be a basic universe.
Let $s: V \to V$ denote the '''successor mapping''' on $V$:
:$\forall x \in V: \map s x := x \cup \set x$
Then $s$ is a slowly progressing mapping.

Proof:
From Successor Mapping is Progressing we have that $s$ is a progressing mapping.
Then we have that:
:$\set x \notin x$
Thus:
:$\card {x \cup \set x} = \card x + 1$
Hence the result.
{{qed}}
Theorem: Subset Relation is Reflexive

Let $C$ be a class.
The subset relation $\subseteq$  on $C$ is a reflexive relation on $C$.

Proof:
{{begin-eqn}}
{{eqn | q = \forall x \in C
      | l = x
      | o = \subseteq
      | r = x
      | c = Set is Subset of Itself
}}
{{eqn | ll= \leadsto
      | q = \forall x \in C
      | l = \tuple {x, x}
      | o = \in
      | r = \subseteq
      | c = 
}}
{{end-eqn}}
So $\subseteq$ is reflexive.
Theorem: Identity Mapping on Normed Vector Space is Bounded Linear Operator

Let $\Bbb F$ be a subfield of $\C$. 
Let $\struct {X, \norm \cdot}$ be a normed vector space.
Let $I : X \to X$ be the identity mapping on $X$. 
Then $I$ is a bounded linear operator.
Further: 
Let $\map B X$, be the space of bounded linear operators on $X$.
Then:
:$\norm I_{\map B X} = 1$
where $\norm {\, \cdot \,}_{\map B X}$ denotes the norm on $\map B X$.

Proof:
Let $\lambda \in \Bbb F$ and $x, y \in X$.
Then, we have: 
:$\map I {\lambda x + y} = \lambda x + y = \lambda I x + I y$
So $I$ is a linear operator.
Further, we have: 
:$\norm {I x} = \norm x$ 
for each $x \in X$, so $I$ is bounded.
Further, for all $x \in X$ with $\norm x = 1$ we have that $\norm {I x} = 1$, so that: 
:$\set {\norm {I x} : \norm x = 1} = \set 1$
so that: 
:$\norm I_{\map B X} = 1$
{{qed}}
Category:Bounded Linear Operators
k3x1eqqyfkcg16g4db6st1vh509ibio
Theorem: Hensel's Lemma/P-adic Integers/Lemma 10

:$\forall x \in \Z_p: p^k x \equiv 0 \pmod {p^{k + 1} \Z_p} \implies x \equiv 0 \pmod {p \Z_p}$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = p^k x
      | o = \equiv
      | r = 0
      | rr= \pmod {p^{k + 1} \Z_p}
}}
{{eqn | ll= \leadsto
      | l = p^k x
      | o = \in
      | r = p^{k + 1} \Z_p
      | c = {{Defof|Congruence Modulo Ideal}}
}}
{{eqn | ll= \leadsto
      | q = \exists y \in \Z_p
      | l = p^k x
      | r = p^{k + 1} y
      | c = {{Defof|Principal Ideal}}
}}
{{eqn | ll= \leadsto
      | q = \exists y \in \Z_p
      | l = x
      | r = p y
      | c = dividing by $p^k$
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = p \Z_p
      | c = {{Defof|Principal Ideal}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \equiv
      | r = 0
      | rr= \pmod {p \Z_p}
      | c = {{Defof|Congruence Modulo Ideal}}
}}
{{end-eqn}}
{{qed}}
Category:Hensel's Lemma
i624vbcofkj22iqf695fxdplvv11c25
Theorem: Closure of product equals product of closures

Let $\set {X_i}_{i \mathop \in I}$ be an arbitrary family of topological spaces.
Let:
:$A_i \subset X_i$
for each $i \in I$.
Let $X = \ds \prod_{i \mathop \in I} X_i$ have the product topology.
Then:
:$\ds \prod_{i \mathop \in I} \overline{A_i} = \overline {\prod_{i \mathop \in I} A_i}$

Proof:
We proceed by double inclusion.
{{explain|what does "double inclusion" mean?}}
Suppose:
:$\ds \family {x_i}_{i \mathop \in I} \in \prod_{i \mathop \in I} \overline {A_i}$
This means:
:$x_i \in \overline {A_i}$ 
for each $i \in I$. 
Let $U$ be an open set containing $\family {x_i}_{i \mathop \in I}$. 
Since:
:$x_i \in \overline {A_i}$
we can choose:
:$y_i \in U_i \cap A_i$ 
and then:
:$\ds \family {y_i}_{i \mathop \in I} \in U \cap \prod_{i \mathop \in I} A_i$
But $U$ was arbitrary, hence:
:$\ds \family {x_i}_{i \mathop \in I} \in \overline {\prod_{i \mathop \in I} A_i}$
Conversely, suppose:
:$\ds \family {x_i}_{i \mathop \in I} \in \overline {\prod_{i \mathop \in I} A_i}$
We want to show that:
:$x_j \in \overline {A_j}$ for all $j$
Fixed $j$, we take $V_j$ to be open set in $X_j$ such that:
:$x_j \in V_j$
Since $\pi_j^{-1} \sqbrk {V_j}$ is open in $\ds \prod_{i \mathop \in I} X_i$, we can pick:
:$\ds \family {y_i}_{i \mathop \in I} \in \prod_{i \mathop \in I} A_i$
Then:
:$y_j \in V_j \cap A_j$
so it follows that:
:$x_j \in \overline {A_j}$
namely:
:$\family {x_i}_{i \mathop \in I} \in \prod_{i \mathop \in I} \overline{A_i}$
{{qed}}
n7dxpka6lcrvpic4p7gjzuqdtfpgwp7
Theorem: Minimal Polynomial Exists

Let $L / K$ be a field extension.
Let $\alpha \in L$ be algebraic over $K$.
Then there exists a minimal polynomial $f \in K \sqbrk x$ for $\alpha$ over $K$.

Proof:
According to definition 1 of minimal polynomial, we ought to find $f \in K \sqbrk x$ such that:
:$f \in K \sqbrk x$ is a monic polynomial of smallest degree such that $\map f \alpha = 0$
Since $\alpha$ is algebraic over $K$, there is some $f \in K \sqbrk x$ such that $\map f \alpha = 0$.
Therefore we can define:
:$n = \min \set { \deg f : f \in K \sqbrk x, \map f \alpha = 0 }$
where $\deg f$ is the degree of $f$.
It follows that there is some $f \in K \sqbrk x$ such that $\deg f = n$.
Then $f$ is of smallest degree such that $\map f \alpha = 0$.
Let the first coefficient of $f$ be $a \in K$.
Since $K$ is a field, it follows that $g := f / a$ is monic.
Therefore $g$ is the sought monic polynomial of smallest degree such that $\map g \alpha = 0$.
{{qed}}
Theorem: Minimal Polynomial Exists

Let $L / K$ be a field extension.
Let $\alpha \in L$ be algebraic over $K$.
Then there exists a minimal polynomial $f \in K \sqbrk x$ for $\alpha$ over $K$.

Proof:
According to definition 2 of minimal polynomial, we ought to find $f \in K \sqbrk x$ such that:
:$f \in K \sqbrk x$ is an irreducible, monic polynomial such that $\map f \alpha = 0$
Since $\alpha$ is algebraic over $K$, there is some $f \in K \sqbrk x$ such that $\map f \alpha = 0$.
By Polynomial Forms over Field form Unique Factorization Domain, $\map f x$ has a complete factorization:
:$\map f x = a \cdot \map {g_1} x \cdots \map {g_n} x$
where $a \in K, a \ne 0$, and the $g_i$ are irreducible and monic.
Since $\map f \alpha = 0$, it follows that for some $g_i$:
:$\map {g_i} \alpha = 0$
as required.
{{qed}}
Theorem: Congruence Modulo Principal Ideal of P-adic Integers

Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Let $\Z_p$ be the $p$-adic integers.
For any $\epsilon \in \R_{>0}$ and $a \in \Q_p$ let $\map B a$ denote the open ball of center $a$ of radius $\epsilon$. 
For any $\epsilon \in \R_{>0}$ and $a \in \Q_p$ let $\map { {B_\epsilon}^-} a$ denote the closed ball of center $a$ of radius $\epsilon$. 
For any $a \in \Z_p$ and $n \in \N$ let $a + p^n\Z_p$ denote the coset of $a$ modulo $p^n\Z_p$. 
For any $a, b \in \Z_p$ and $n \in \N$ let $x \equiv y \pmod{p^n \Z_p}$ denote congruence modulo the principal ideal $p^n\Z_p$.
Let $x, y \in \Z_p$.
Let $k \in \N$.
{{TFAE}}
::$(1)\quad x \equiv y \pmod{p^{k+1} \Z_p}$
::$(2)\quad x \in y + p^{k+1} \Z_p$
::$(3)\quad x + p^{k+1} \Z_p = y + p^{k+1} \Z_p$
::$(4)\quad x \in \map {B_{p^{-k}}} y$
::$(5)\quad \norm{x - y}_p < p^{-k}$
::$(6)\quad \map {B_{p^{-k}}} x = \map {B_{p^{-k}}} y$
::$(7)\quad x \in \map {B^{\,-}_{p^{-k-1}}} y$
::$(8)\quad \norm{x - y}_p \le p^{-k-1}$
::$(9)\quad \map {B^{\,-}_{p^{-k-1}}} x = \map {B^{\,-}_{p^{-k-1}}} y$

Proof:
=== Condition (1) is Equivalent to Condition (3) ===
We have:
{{begin-eqn}}
{{eqn | l = x \equiv y \pmod{p^{k+1} \Z_p}
      | o = \iff
      | r = x - y \in p^{k+1} \Z_p
      | c = {{Defof|Congruence Modulo Ideal}}
}}
{{eqn | o = \iff
      | r = x + p^{k+1} \Z_p = y + p^{k+1} \Z_p
      | c = Cosets are Equal iff Product with Inverse in Subgroup
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Congruence Modulo Equivalence for Integers in P-adic Integers

Let $\Z_p$ be the $p$-adic integers for some prime $p$.
For any $a, b \in \Z_p$ and $n \in \N$, let $x \equiv y \pmod{p^n \Z_p}$ denote congruence modulo the principal ideal $p^n\Z_p$.
For any integers $a, b \in \Z$ and $n \in \N$, let $x \equiv y \pmod{p^n}$ denote congruence modulo integer $p^n$.
Let $x, y \in \Z$ be integers.
Let $k \in \N_{>0}$.
{{TFAE}}
{{begin-eqn}}
{{eqn | n = 1
      | l = x
      | o = \equiv
      | r = y
      | rr= \pmod {p^k \Z_p}
}}
{{eqn | n = 2
      | l = x
      | o = \equiv
      | r = y
      | rr= \pmod {p^k}
}}
{{eqn | n = 3
      | l = p^k
      | o = \divides
      | r = \paren{x - y}
}}
{{end-eqn}}

Proof:
=== Lemma ===
{{:Congruence Modulo Equivalence for Integers in P-adic Integers/Lemma 1}}{{qed|lemma}}
We have:
{{begin-eqn}}
{{eqn | n = 1
      | l = x
      | o = \equiv
      | r = y
      | rr= \pmod {p^k \Z_p}
}}
{{eqn | ll = \leadstoandfrom
      | l = x - y
      | o = \in
      | r = p^k \Z_p
      | c = {{Defof|Congruence Modulo Ideal}}
}}
{{eqn | ll = \leadstoandfrom
      | q = \exists z \in \Z_p
      | l = x - y
      | r = p^k z
      | c = {{Defof|Principal Ideal}}
}}
{{eqn | ll = \leadstoandfrom
      | l = \frac {x - y} {p^k}
      | o = \in
      | r = \Z_p 
      | c = Divide both sides by $p^k$
}}
{{eqn | ll = \leadstoandfrom
      | l = \frac {x - y} {p^k}
      | o = \in
      | r = \Z
      | c = Lemma
}}
{{eqn | ll = \leadstoandfrom
      | q = \exists a \in \Z
      | l = \frac {x - y} {p^k}
      | r = a
}}
{{eqn | ll = \leadstoandfrom
      | q = \exists a \in \Z
      | l = x - y
      | r = p^k a
      | c = Multiply both sides by $p^k$
}}
{{eqn | n = 3
      | ll = \leadstoandfrom
      | l = p^k
      | o = \divides
      | r = \paren{x - y}
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | n = 2
      | ll = \leadstoandfrom
      | l = x
      | o = \equiv
      | r = y
      | rr= \pmod {p^k}
      | c = {{Defof|Congruence Modulo Integer}}
}}
{{end-eqn}}
{{qed}}
Category:P-adic Integers
Category:Congruence Modulo Equivalence for Integers in P-adic Integers
33faclp87unni5anzisdiimu00vlw5z
Theorem: Congruence Modulo Equivalence for Integers in P-adic Integers/Lemma 1

:$\forall a \in \Z: \dfrac a {p^k} \in \Z_p \iff \dfrac a {p^k} \in \Z$

Proof:
=== Necessary Condition ===
Let $a \in \Z$.
We have:
{{begin-eqn}}
{{eqn | l = \dfrac a {p^k}
      | o = \in
      | r = \Z_p
}}
{{eqn | ll = \leadsto
      | l = \dfrac a {p^k}
      | o = \in
      | r = \Z_p \cap \Q
}}
{{eqn | ll = \leadsto
      | q = \exists c, d \in \Z : p \nmid d 
      | l = \dfrac a {p^k}
      | r = \dfrac c d
      | c = Characterization of Rational P-adic Integer
}}
{{eqn | ll = \leadsto
      | l = ad
      | r = cp^k
      | c = Multiply both sides by $dp^k$
}}
{{eqn | ll = \leadsto
      | l = p^k
      | o = \divides
      | r = ad
      | c = {{Defof|Divisor}}
}}
{{eqn | ll = \leadsto
      | l = p^k
      | o = \divides
      | r = a
      | c = Euclid's Lemma and $p \nmid d$
}}
{{eqn | ll = \leadsto
      | l = \dfrac a {p^k}
      | o = \in
      | r = \Z
      | c = {{Defof|Divisor}}
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Skewness of Binomial Distribution

Let $X$ be a discrete random variable with a Binomial distribution with parameter $n$ and $p$ for some $n \in \N$ and $0 \le p \le 1$.
Then the skewness $\gamma_1$ of $X$ is given by: 
:$\gamma_1 = \dfrac {1 - 2 p} {\sqrt {n p q} }$
where $q = 1 - p$.

Proof:
From Skewness in terms of Non-Central Moments: 
:$\gamma_1 = \dfrac {\expect {X^3} - 3 \mu \sigma^2 - \mu^3} {\sigma^3}$ 
where $\mu$ is the mean of $X$, and $\sigma$ the standard deviation.
We have, by Expectation of Binomial Distribution:
:$\mu = n p$
By Variance of Binomial Distribution, we also have: 
:$\var X = \sigma^2 = n p \paren {1 - p}$
so: 
:$\sigma = \sqrt {n p \paren {1 - p} }$
To calculate $\gamma_1$, we must calculate $\expect {X^3}$.
We find this using the moment generating function of $X$, $M_X$. 
By Moment Generating Function of Binomial Distribution, this is given by: 
:$\map {M_X} t = \paren {1 - p + p e^t}^n$
From Moment in terms of Moment Generating Function:
:$\expect {X^3} = \map {M_X' ' '} 0$
So:
{{begin-eqn}}
{{eqn | l = \map {M_X'} t
      | r = n p e^t \paren {1 - p + p e^t}^{n - 1}
      | c = Chain Rule for Derivatives, Derivative of Power
}}
{{eqn | l = \map {M_X' '} t
      | r = n p e^t \paren {1 - p + p e^t}^{n - 1} + n \paren {n - 1} p^2 e^{2 t} \paren {1 - p + p e^t}^{n - 2}
      | c = Product Rule for Derivatives, Chain Rule for Derivatives, Derivative of Power
}}
{{eqn | l = \map {M_X' ' '} t
      | r = \map {M_X' '} t + 2 n \paren {n - 1} p^2 e^{2 t} \paren {1 - p + p e^t}^{n - 2} + n \paren {n - 1} \paren {n - 2} p^3 e^{3 t} \paren {1 - p + p e^t}^{n - 3}
      | c = Product Rule for Derivatives, Chain Rule for Derivatives, Derivative of Power
}}
{{end-eqn}}
Setting $t = 0$:
{{begin-eqn}}
{{eqn | l = \expect {X^3}
      | r = \map {M_X' '} 0 + 2 n \paren {n - 1} p^2 \paren {1 - p + p}^{n - 2} + n \paren {n - 1} \paren {n - 2} p^3 \paren {1 - p + p}^{n - 3}
}}
{{eqn | r = n p \paren {1 - p + p}^{n - 1} + n \paren {n - 1} p^2 \paren {1 - p + p}^{n - 2} + 2 n \paren {n - 1} p^2 + n \paren {n - 1} \paren {n - 2} p^3
      | c = 
}}
{{eqn | r = n p + 3 n \paren {n - 1} p^2 + n \paren {n - 1} \paren {n - 2} p^3
      | c = 
}}
{{eqn | r = n p + 3 n^2 p^2 - 3 n p^2 + n^3 p^3 - 3 n^2 p^3 + 2 n p^3
      | c = 
}}
{{end-eqn}}
Plugging this result back into our equation above:
{{begin-eqn}}
{{eqn | l = \gamma_1
      | r = \frac {\expect {X^3} - 3 \mu \sigma^2 - \mu^3} {\sigma^3}
}}
{{eqn | r = \frac {n p + 3 n^2 p^2 - 3 n p^2 + n^3 p^3 - 3 n^2 p^3 + 2 n p^3 - 3 n^2 p^2 \paren {1 - p} - n^3 p^3} {\paren {n p \paren {1 - p} }^{3/2} }
}}
{{eqn | r = \frac {n p - 3 n p^2 + 2 n p^3} {\paren {n p \paren {1 - p} }^{3/2} }
}}
{{eqn | r = \frac {n p \paren {1 - p} \paren {1 - 2 p} } {\paren {n p \paren {1 - p} }^{3/2} }
}}
{{eqn | r = \frac {1 - 2 p} {\sqrt {n p \paren {1 - p} } }
}}
{{eqn | r = \frac {1 - 2 p} {\sqrt {n p q} }
      | c = $q = 1 - p$
}}
{{end-eqn}}
{{qed}}
Category:Binomial Distribution
Category:Skewness
npd5pxu40onx8sl5125t7sdvp8toc0v