Skip to content

Commit 850a224

Browse files
JoramSochJoramSoch
authored
added 4 proofs
1 parent 2a5bf16 commit 850a224

4 files changed

Lines changed: 268 additions & 0 deletions

File tree

‎P/gibbs-ineq.md‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
---
2+
layout: proof
3+
mathjax: true
4+
5+
author: "Joram Soch"
6+
affiliation: "BCCN Berlin"
7+
e_mail: "joram.soch@bccn-berlin.de"
8+
date: 2020-09-09 02:18:00
9+
10+
title: "Gibbs' inequality"
11+
chapter: "General Theorems"
12+
section: "Information theory"
13+
topic: "Shannon entropy"
14+
theorem: "Gibbs' inequality"
15+
16+
sources:
17+
- authors: "Wikipedia"
18+
year: 2020
19+
title: "Gibbs' inequality"
20+
in: "Wikipedia, the free encyclopedia"
21+
pages: "retrieved on 2020-09-09"
22+
url: "https://en.wikipedia.org/wiki/Gibbs%27_inequality#Proof"
23+
24+
proof_id: "P164"
25+
shortcut: "gibbs-ineq"
26+
username: "JoramSoch"
27+
---
28+
29+
30+
**Theorem:** Let $X$ be a discrete [random variable](/D/rvar) and consider two [probability distributions](/D/dist) with [probability mass functions](/D/pmf) $p(x)$ and $q(x)$. Then, Gibbs' inequality states that the [entropy](/D/ent) of $X$ according to $P$ is smaller than or equal to the [cross-entropy](/D/ent-cross) of $P$ and $Q$:
31+
32+
$$ \label{eq:Gibbs-ineq}
33+
- \sum_{x \in \mathcal{X}} p(x) \, \log_b p(x) \leq - \sum_{x \in \mathcal{X}} p(x) \, \log_b q(x) \; .
34+
$$
35+
36+
37+
**Proof:** Without loss of generality, we will use the natural logarithm, because a change in the base of the logarithm only implies multiplication by a constant:
38+
39+
$$ \label{eq:log-ln}
40+
\log_b a = \frac{\ln a}{\ln b} \; .
41+
$$
42+
43+
Let $I$ be the of all $x$ for which $p(x)$ is non-zero. Then, proving \eqref{eq:Gibbs-ineq} requires to show that
44+
45+
$$ \label{eq:Gibbs-ineq-s1}
46+
\sum_{x \in I} p(x) \, \frac{\ln p(x)}{\ln q(x)} \geq 0 \; .
47+
$$
48+
49+
Because $\ln x \leq x - 1$, i.e. $-\ln x \geq 1 - x$, for all $x > 0$, with equality only if $x = 1$, we can say about the left-hand side that
50+
51+
$$ \label{eq:Gibbs-ineq-s2}
52+
\begin{split}
53+
\sum_{x \in I} p(x) \, \frac{\ln p(x)}{\ln q(x)} &\geq \sum_{x \in I} p(x) \left( 1 - \frac{p(x)}{q(x)} \right) \\
54+
&= \sum_{x \in I} p(x) - \sum_{x \in I} q(x) \; .
55+
\end{split}
56+
$$
57+
58+
Finally, since $p(x)$ and $q(x)$ are [probability mass functions](/D/pmf), it holds that $0 \leq p(x),q(x) \leq 1$ and we also have
59+
60+
$$ \label{eq:p-q-pmf}
61+
\begin{split}
62+
\sum_{x \in I} p(x) &= 1 \\
63+
\sum_{x \in I} q(x) &\leq 1 \; ,
64+
\end{split}
65+
$$
66+
67+
such that it follows from \eqref{eq:Gibbs-ineq-s2} that
68+
69+
$$ \label{eq:Gibbs-ineq-s3}
70+
\begin{split}
71+
\sum_{x \in I} p(x) \, \frac{\ln p(x)}{\ln q(x)} &\geq \sum_{x \in I} p(x) - \sum_{x \in I} q(x) \\
72+
&= 1 - \sum_{x \in I} q(x) \geq 0 \; .
73+
\end{split}
74+
$$

‎P/kl-nonneg2.md‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
---
2+
layout: proof
3+
mathjax: true
4+
5+
author: "Joram Soch"
6+
affiliation: "BCCN Berlin"
7+
e_mail: "joram.soch@bccn-berlin.de"
8+
date: 2020-09-09 07:02:00
9+
10+
title: "Non-negativity of the Kullback-Leibler divergence"
11+
chapter: "General Theorems"
12+
section: "Information theory"
13+
topic: "Kullback-Leibler divergence"
14+
theorem: "Non-negativity"
15+
16+
sources:
17+
- authors: "Wikipedia"
18+
year: 2020
19+
title: "Log sum inequality"
20+
in: "Wikipedia, the free encyclopedia"
21+
pages: "retrieved on 2020-09-09"
22+
url: "https://en.wikipedia.org/wiki/Log_sum_inequality#Applications"
23+
24+
proof_id: "P166"
25+
shortcut: "kl-nonneg2"
26+
username: "JoramSoch"
27+
---
28+
29+
30+
**Theorem:** The [Kullback-Leibler divergence](/D/kl) is always non-negative
31+
32+
$$ \label{eq:KL-nonneg}
33+
\mathrm{KL}[P||Q] \geq 0
34+
$$
35+
36+
with $\mathrm{KL}[P \vert \vert Q] = 0$, if and only if $P = Q$.
37+
38+
39+
**Proof:** The discrete [Kullback-Leibler divergence](/D/kl) is defined as
40+
41+
$$ \label{eq:KL}
42+
\mathrm{KL}[P||Q] = \sum_{x \in \mathcal{X}} p(x) \cdot \log \frac{p(x)}{q(x)} \; .
43+
$$
44+
45+
The [log sum inequality](/P/logsum-ineq) states that
46+
47+
$$ \label{eq:logsum-ineq}
48+
\sum_{i=1}^n a_i \, \log_c \frac{a_i}{b_i} \geq a \, \log_c \frac{a}{b} \; .
49+
$$
50+
51+
where $a_1, \ldots, a_n$ and $b_1, \ldots, b_n$ be non-negative real numbers and $a = \sum_{i=1}^{n} a_i$ and $b = \sum_{i=1}^{n} b_i$. Because $p(x)$ and $q(x)$ are [probability mass functions](/D/pmf), such that
52+
53+
\begin{equation} \label{eq:p-q-pmf}
54+
\begin{split}
55+
p(x) \geq 0, \quad \sum_{x \in \mathcal{X}} p(x) &= 1 \quad \text{and} \\
56+
q(x) \geq 0, \quad \sum_{x \in \mathcal{X}} q(x) &= 1 \; ,
57+
\end{split}
58+
\end{equation}
59+
60+
theorem \eqref{eq:KL-nonneg} is simply a special case of \eqref{eq:logsum-ineq}, i.e.
61+
62+
$$ \label{eq:KL-nonneg-qed}
63+
\mathrm{KL}[P||Q] \overset{\eqref{eq:KL}}{=} \sum_{x \in \mathcal{X}} p(x) \cdot \log \frac{p(x)}{q(x)} \overset{\eqref{eq:logsum-ineq}}{\geq} 1 \, \log \frac{1}{1} = 0 \; .
64+
$$

‎P/logsum-ineq.md‎

Lines changed: 78 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,78 @@
1+
---
2+
layout: proof
3+
mathjax: true
4+
5+
author: "Joram Soch"
6+
affiliation: "BCCN Berlin"
7+
e_mail: "joram.soch@bccn-berlin.de"
8+
date: 2020-09-09 02:46:00
9+
10+
title: "Log sum inequality"
11+
chapter: "General Theorems"
12+
section: "Information theory"
13+
topic: "Shannon entropy"
14+
theorem: "Log sum inequality"
15+
16+
sources:
17+
- authors: "Wikipedia"
18+
year: 2020
19+
title: "Log sum inequality"
20+
in: "Wikipedia, the free encyclopedia"
21+
pages: "retrieved on 2020-09-09"
22+
url: "https://en.wikipedia.org/wiki/Log_sum_inequality#Proof"
23+
- authors: "Wikipedia"
24+
year: 2020
25+
title: "Jensen's inequality"
26+
in: "Wikipedia, the free encyclopedia"
27+
pages: "retrieved on 2020-09-09"
28+
url: "https://en.wikipedia.org/wiki/Jensen%27s_inequality#Statements"
29+
30+
proof_id: "P165"
31+
shortcut: "logsum-ineq"
32+
username: "JoramSoch"
33+
---
34+
35+
36+
**Theorem:** Let $a_1, \ldots, a_n$ and $b_1, \ldots, b_n$ be non-negative real numbers and define $a = \sum_{i=1}^{n} a_i$ and $b = \sum_{i=1}^{n} b_i$. Then, the log sum inequality states that
37+
38+
$$ \label{eq:logsum-ineq}
39+
\sum_{i=1}^n a_i \, \log_c \frac{a_i}{b_i} \geq a \, \log_c \frac{a}{b} \; .
40+
$$
41+
42+
43+
**Proof:** Without loss of generality, we will use the natural logarithm, because a change in the base of the logarithm only implies multiplication by a constant:
44+
45+
$$ \label{eq:log-ln}
46+
\log_c a = \frac{\ln a}{\ln c} \; .
47+
$$
48+
49+
Let $f(x) = x \ln x$. Then, the left-hand side of \eqref{eq:logsum-ineq} can be rewritten as
50+
51+
$$ \label{eq:logsum-ineq-s2}
52+
\begin{split}
53+
\sum_{i=1}^n a_i \, \ln \frac{a_i}{b_i} &= \sum_{i=1}^n b_i \, f\left( \frac{a_i}{b_i} \right) \\
54+
&= b \sum_{i=1}^n \frac{b_i}{b} \, f\left( \frac{a_i}{b_i} \right) \; .
55+
\end{split}
56+
$$
57+
58+
Because $f(x)$ is a convex function and
59+
60+
$$ \label{eq:sum-bi-b}
61+
\begin{split}
62+
\frac{b_i}{b} &\geq 0 \\
63+
\sum_{i=1}^n \frac{b_i}{b} &= 1 \; ,
64+
\end{split}
65+
$$
66+
67+
applying Jensen's inequality yields
68+
69+
$$ \label{eq:logsum-ineq-s3}
70+
\begin{split}
71+
b \sum_{i=1}^n \frac{b_i}{b} \, f\left( \frac{a_i}{b_i} \right) &\geq b \, f\left( \sum_{i=1}^n \frac{b_i}{b} \frac{a_i}{b_i} \right) \\
72+
&= b \, f\left( \frac{1}{b} \sum_{i=1}^n a_i \right) \\
73+
&= b \, f\left( \frac{a}{b} \right) \\
74+
&= a \, \ln \frac{a}{b} \; .
75+
\end{split}
76+
$$
77+
78+
Finally, combining \eqref{eq:logsum-ineq-s2} and \eqref{eq:logsum-ineq-s3}, this demonstrates \eqref{eq:logsum-ineq}.

‎P/momcent-1st.md‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
---
2+
layout: proof
3+
mathjax: true
4+
5+
author: "Joram Soch"
6+
affiliation: "BCCN Berlin"
7+
e_mail: "joram.soch@bccn-berlin.de"
8+
date: 2020-08-19 07:51:00
9+
10+
title: "First central moment is zero"
11+
chapter: "General Theorems"
12+
section: "Probability theory"
13+
topic: "Further moments"
14+
theorem: "First central moment is zero"
15+
16+
sources:
17+
- authors: "ProofWiki"
18+
year: 2020
19+
title: "First Central Moment is Zero"
20+
in: "ProofWiki"
21+
pages: "retrieved on 2020-09-09"
22+
url: "https://proofwiki.org/wiki/First_Central_Moment_is_Zero"
23+
24+
proof_id: "P167"
25+
shortcut: "momcent-1st"
26+
username: "JoramSoch"
27+
---
28+
29+
30+
**Theorem:** The first [central moment](/D/mom-cent) is zero, i.e.
31+
32+
$$ \label{eq:momcent-1st}
33+
\mu_1 = 0 \; .
34+
$$
35+
36+
37+
**Proof:** The first [central moment](/D/mom-cent) of a [random variable](/D/rvar) $X$ with [mean](/D/mean) $\mu$ is defined as
38+
39+
$$ \label{eq:momcent-1st-def}
40+
\mu_1 = \mathrm{E}\left[ (X-\mu)^1 \right] \; .
41+
$$
42+
43+
Due to the [linearity of the expected value](/P/mean-lin) and by plugging in $\mu = \mathrm{E}(X)$, we have
44+
45+
\begin{equation} \label{eq:momcent-1st-qed}
46+
\begin{split}
47+
\mu_1 &= \mathrm{E}\left[ X-\mu \right] \\
48+
&= \mathrm{E}(X) - \mu \\
49+
&= \mathrm{E}(X) - \mathrm{E}(X) \\
50+
&= 0 \; .
51+
\end{split}
52+
\end{equation}

0 commit comments

Comments
 (0)