nyuuzyou/wikis huggingface dataset:
Minimum Rule for Continuous Functions

== Theorem ==
Let $\struct {S, \tau}$ be a topological space.
Let $f, g: S \to \R$ be continuous real-valued functions.
Let $\min \set {f, g}: S \to \R$ denote the pointwise minimum of $f$ and $g$.
Then:
:$\min \set {f, g}$ is continuous.
== Proof ==
Let $x \in S$.
Let $\epsilon > 0$.
, assume that $\map f x \le \map g x$. 
==== Case 1 : $\map f x = \map g x$ ====
Let $ y = \map f x = \map g x$
By definition of the min operation, $\min \set {\map f x, \map g x} = y$.
From Continuity Test for Real-Valued Functions applied to $f$:
:$\exists U \in \tau : x \in U : \forall z \in U : \map f z \in \openint {y - \epsilon} {y + \epsilon}$
Similarly, Continuity Test for Real-Valued Functions applied to $g$:
:$\exists V \in \tau : x \in V : \forall z \in V : \map g z \in \openint {y - \epsilon} {y + \epsilon}$
Thus for all $z \in U \cap V$:
:$\map f z \in \openint {y - \epsilon} {y + \epsilon}$
:$\map g z \in \openint {y - \epsilon} {y + \epsilon}$
By definition of the min operation, for all $z \in U \cap V$:
:$\min \set {\map f z, \map g z} \in \openint {y - \epsilon} {y + \epsilon}$
By the :
:$U \cap V \in \tau$
Since $\epsilon > 0$ was arbitrary then:
:$\forall \epsilon > 0 : \exists W \in \tau : x \in W : \forall z \in W : \min \set {\map f z, \map g z} \in \openint {y - \epsilon} {y + \epsilon}$
From Continuity Test for Real-Valued Functions, $\min \set {f, g}$ is continuous at $x$.
==== Case 2 : $\map f x < \map g x$ ====
Let $\map f x < \map g x$.
Then:
:$\min \set {\map f x, \map g x} = \map f x$
Let $\delta = \min \set {\epsilon, \dfrac 1 2 \paren {\map g x - \map f x} }$.
Then $\delta > 0$.
From Continuity Test for Real-Valued Functions applied to $f$:
:$\exists U \in \tau : x \in U : \forall z \in U : \map f z \in \openint {\map f x - \delta} {\map f x + \delta}$
Similarly, Continuity Test for Real-Valued Functions applied to $g$:
:$\exists V \in \tau : x \in V : \forall z \in V : \map g z \in \openint {\map g x - \delta} {\map g x + \delta}$
Thus for all $z \in U \cap V$:
:$\map f z \in \openint {\map f x - \delta} {\map f x + \delta}$
:$\map g z \in \openint {\map g x - \delta} {\map g x + \delta}$
Now:
Thus:
:$\min \set {\map f z, \map g z} = \map f z$
As
:$\map f z \in \openint {\map f x - \delta} {\map f x + \delta}$
and
:$\map f x = \min \set {\map f x, \map g x}$
then
:$\min \set {\map f z, \map g z} \in \openint {\min \set {\map f x, \map g x} - \delta} {\min \set {\map f x, \map g x} + \delta}$
By the :
:$U \cap V \in \tau$
Since $\epsilon > 0$ was arbitrary then:
:$\forall \epsilon > 0 : \exists W \in \tau : x \in W : \forall z \in W : \min \set{\map f z, \map g z} \in \openint {\min \set {\map f x, \map g x} - \delta} {\min \set {\map f x, \map g x} + \delta}$
From Continuity Test for Real-Valued Functions, $\min \set {f, g}$ is continuous at $x$.
In either case, $\min \set {f, g}$ is continuous at $x$.
Since $x \in S$ was arbitrary, then $\min \set {f, g}$ is everywhere continuous.
== Also see ==
* Maximum Rule for Continuous Functions
Category:Min Operation
Category:Continuous Mappings
Minimum Rule for Real Sequences

== Theorem == 
Let $\sequence {x_n}$ and $\sequence {y_n}$ be sequences in $\R$.
Let $\sequence {x_n}$ and $\sequence {y_n}$ be convergent to the following limits:
:$\ds \lim_{n \mathop \to \infty} x_n = l$
:$\ds \lim_{n \mathop \to \infty} y_n = m$
Then:
:$\ds \lim_{n \mathop \to \infty} \min \set {x_n, y_n} = \min \set {l, m}$
== Proof ==
By Sum Less Maximum is Minimum:
:$\forall n \in \R: \min \set {x_n, y_n} = x_n + y_n - \max \set {x_n, y_n}$
and
:$\min \set {m, l} = m + l - \max \set {m, l}$
By Maximum Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \max \set {x_n, y_n} = \max \set {m, l}$
By the Multiple Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} - \max \set {x_n, y_n} = - \max \set {m, l}$
By the Sum Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} x_n + y_n - \max \set {x_n, y_n} = m + l - \max \set {m, l}$
Hence:
:$\ds \lim_{n \mathop \to \infty} \min \set {x_n, y_n} = \min \set {l, m}$
== Also see ==
* Maximum Rule for Real Sequences
Category:Real Sequences
Minimum Value of Real Quadratic Function

== Theorem ==
Let $a \in \R_{>0}$ be a (strictly) positive real number.
Consider the quadratic function:
:$\map Q x = a x^2 + b x + c$
$\map Q x$ achieves a minimum at $x = -\dfrac b {2 a}$, at which point $\map Q x = c - \dfrac {b^2} {4 a}$.
== Proof ==
As $\paren {2 a x + b}^2 > 0$, it follows that:
Equality occurs when $2 a x + b = 0$, that is:
:$x = -\dfrac b {2 a}$
== Sources ==
* : $\S 1$: Real Numbers: Exercise $\S 1.12 \ (4)$
Category:Quadratic Functions
Minimum is Less than or Equal to Geometric Mean

== Theorem ==
Let $x_1, x_2, \ldots, x_n \in \R_{\ge 0}$ be positive real numbers.
Let $p \in \R$ be a real number.
Let $\map G {x_1, x_2, \ldots, x_n}$ denote the geometric mean of $x_1, x_2, \ldots, x_n$.
Then:
:$\min \set {x_1, x_2, \ldots, x_n} \le \map G {x_1, x_2, \ldots, x_n}$
Equality holds :
:$x_1 = x_2 = \cdots x_n$
or $x_k = 0$ for some $k \in \set {1, 2, \ldots, n}$.
== Proof ==
From Limit of Hölder Mean as Exponent tends to Zero is Geometric Mean:
:$\map G {x_1, x_2, \ldots, x_n} = \ds \lim_{p \mathop \to 0} \map {M_p} {x_1, x_2, \ldots, x_n}$
where $\map {M_p} {x_1, x_2, \ldots, x_n}$ denotes the Hölder mean with exponent $p$ of $x_1, x_2, \ldots, x_n$.
Then from Minimum is Less than or Equal to Hölder Mean:
$\min \set {x_1, x_2, \ldots, x_n} \le \map {M_p} {x_1, x_2, \ldots, x_n}$
where equality holds :
:$x_1 = x_2 = \cdots x_n$
or:
:$p < 0$ and $x_k = 0$ for some $k \in \set {1, 2, \ldots, n}$.
In this context, if such an $x_k = 0$ then:
:$\ds \prod_{k \mathop = 1}^n x_k = 0$
and so by definition:
$\map G {x_1, x_2, \ldots, x_n} = 0$
Thus we have:
:$\min \set {x_1, x_2, \ldots, x_n} \le \map G {x_1, x_2, \ldots, x_n}$
== Sources ==
* : $3$: Elementary Analytic Methods: $3.2$ Inequalities: Relation Between Arithmetic, Geometric, Harmonic and Generalized Means: $3.2.3$
Category:Geometric Mean
Minimum is Less than or Equal to Hölder Mean

== Theorem ==
Let $x_1, x_2, \ldots, x_n \in \R_{\ge 0}$ be positive real numbers.
Let $p \in \R$ be a real number.
Let $\map {M_p} {x_1, x_2, \ldots, x_n}$ denote the Hölder mean with exponent $p$ of $x_1, x_2, \ldots, x_n$.
Then:
:$\min \set {x_1, x_2, \ldots, x_n} \le \map {M_p} {x_1, x_2, \ldots, x_n}$
Equality holds :
:$x_1 = x_2 = \cdots x_n$
or:
:$p < 0$ and $x_k = 0$ for some $k \in \set {1, 2, \ldots, n}$.
== Proof ==
== Sources ==
* : $3$: Elementary Analytic Methods: $3.2$ Inequalities: Relation Between Arithmetic, Geometric, Harmonic and Generalized Means: $3.2.2$
Category:Hölder Mean
Minimum of Exponential Random Variables has Exponential Distribution

== Theorem ==
Let $\beta_1, \beta_2, \ldots, \beta_n$ be positive real numbers.
Let $X_1, X_2, \ldots, X_n$ be independent random variables.
For each $i$, let $X_i \sim \Exponential {\beta_i}$, where $\Exponential {\beta_i}$ is the exponential distribution with parameter $\beta_i$. 
Let: 
:$\ds M = \map {\min_{1 \mathop \le i \mathop \le n} } {X_i} $
Then: 
:$\ds M \sim \Exponential {\paren {\sum_{i \mathop = 1}^n \frac 1 {\beta_i} }^{-1} }$
== Proof ==
We aim to show that: 
:$\ds \map \Pr {M \le m} = 1 - \map \exp {-m \sum_{i \mathop = 1}^n \frac 1 {\beta_i} }$
for each $m > 0$.
Note that: 
:$\ds M > m$
:
:$\ds X_i > m$
for each $i$. 
We therefore have: 
so:
:$\ds \map \Pr {M \le m} = 1 - \map \exp {-m \sum_{i \mathop = 1}^n \frac 1 {\beta_i} }$
Category:Exponential Distribution
Minimum of Finitely Many Continuous Real Functions is Continuous

== Theorem ==
Let $n \ge 2$ be a natural number.
Let $X \subseteq \R$. 
Let $f_1, f_2, \ldots, f_n$ be functions $X \to \R$.
Define the function $m : X \to \R$ by:
:$\ds \map m x = \min_i \map {f_i} x$
for all $x \in X$.
Then $m$ is continuous. 
== Proof ==
We proceed by induction.
For all natural numbers $n \ge 2$, let $\map P n$ be the proposition:
:for every collection of $n$ functions $f_1, f_2, \ldots, f_n : X \to \R$, $m$ is continuous.
=== Basis for the Induction ===
Take $n = 2$. 
We have, for each $x \in X$:
From Combined Sum Rule for Continuous Real Functions:
:$f_1 + f_2$ and $f_1 - f_2$ are continuous.
From Absolute Value of Continuous Real Function is Continuous:
:$\size {f_1 - f_2}$ is continuous.
Applying Combined Sum Rule for Continuous Real Functions again, we obtain:
:$m$ is continuous.
So $\map P 2$ is true.
This is our base case.
=== Induction Hypothesis ===
Suppose that: 
:for every collection of $N$ functions $f_1, f_2, \ldots, f_N : X \to \R$, $m$ is continuous.
That is:
:$\map P N$ is true for some $N$.
We aim to show that: 
:$\map P {N + 1}$ is true. 
=== Induction Step ===
For each $x \in X$, we have:
By the induction hypothesis: 
:$\ds \min_{i \mathop \le N} f_i$
is continuous.
Since $m$ is the minimum of two continuous functions, it is continuous by the base case.
So $\map P N \implies \map P {N + 1}$ and the result follows by the Principle of Mathematical Induction.
Category:Proofs by Induction
Category:Continuous Functions
Minimum of Real Hyperbolic Cosine Function

== Theorem ==
Let $x$ be a real number.
Then:
:$\cosh x \ge 1$
where $\cosh$ denotes the hyperbolic cosine function.
== Proof ==
Furthermore, $\cosh x = 1$ when $x = 0$, satisfying the equality case.
Category:Hyperbolic Cosine Function
Minkowski's Inequality for Double Integrals

== Theorem ==
Let $\struct {X, \Sigma, \mu}$ and $\struct {Y, \Sigma', \nu}$ be $\sigma$-finite measure spaces.
Let $\struct {X \times Y, \Sigma \otimes \Sigma', \mu \times \nu}$ be their product measure space.
Let $f: X \times Y \to \overline \R$ be a $\Sigma \otimes \Sigma'$-measurable function.
Then, for all $p \in \R$ with $p \ge 1$:
:$\ds \paren {\int_X \paren {\int_Y \size {\map f {x, y} } \map {\rd \nu} y}^p \map {\rd \mu} x}^{1/p} \le \int_Y \paren {\int_X \size {\map f {x, y} }^p \map {\rd \mu} x}^{1/p} \map {\rd \nu} y$
== Proof ==
== Also see ==
* Minkowski's Inequality for Integrals
== Sources ==
* : $13.14$
Category:Measure Theory
Minkowski's Inequality for Integrals

== Theorem ==
Let $f, g$ be (Darboux) integrable functions.
Let $p \in \R$ such that $p > 1$.
Then:
:$\ds \paren {\int_a^b \size {\map f x + \map g x}^p \rd x}^{1/p} \le \paren {\int_a^b \size {\map f x}^p \rd x}^{1 / p} + \paren {\int_a^b \size {\map g x}^p \rd x}^{1 / p}$
=== Condition for Equality ===
== Proof ==
Define:
:$q = \dfrac p {p - 1}$
Then:
:$\dfrac 1 p + \dfrac 1 q = \dfrac 1 p + \dfrac {p - 1} p = 1$
It follows that:
== Sources ==
* : $3$: Elementary Analytic Methods: $3.2$ Inequalities: Minkowski's Inequality for Integrals: $3.2.13$
* : $\S 36$: Inequalities: $36.15$: Minkowski's Inequality for Integrals
Category:Minkowski's Inequality for Integrals
Category:Minkowski's Inequality
Category:Integral Calculus
Minkowski's Inequality for Integrals/Equality

== Theorem ==
Let $f, g$ be (Darboux) integrable functions.
Let $p \in \R$ such that $p > 1$.
Then equality in Minkowski's Inequality for Integrals, that is:
:$\ds \paren {\int_a^b \size {\map f x + \map g x}^p \rd x}^{1/p} = \paren {\int_a^b \size {\map f x}^p \rd x}^{1 / p} + \paren {\int_a^b \size {\map g x}^p \rd x}^{1 / p}$
holds , for all $x \in \closedint a b$:
:$\map g x = c \map f x$
for some $c \in \R_{>0}$.
== Proof ==
== Also presented as ==
== Sources ==
* : $3$: Elementary Analytic Methods: $3.2$ Inequalities: Minkowski's Inequality for Integrals: $3.2.13$
* : $\S 36$: Inequalities: $36.15$: Minkowski's Inequality for Integrals
Category:Minkowski's Inequality for Integrals
Minkowski's Inequality for Integrals/Equality/Also presented as

== Equality Condition for Minkowski's Inequality for Integrals: Also presented as == 
Some sources present the equality condition for Minkowski's inequality for integrals as:
:$\ds \paren {\int_a^b \size {\map f x + \map g x}^p \rd x}^{1/p} = \paren {\int_a^b \size {\map f x}^p \rd x}^{1 / p} + \paren {\int_a^b \size {\map g x}^p \rd x}^{1 / p}$
holds , for all $x \in \closedint a b$:
:$\dfrac {\map f x} {\map g x} = c$
for some $c \in \R_{>0}$.
This may confuse those who ask the question as to what happens if $\map g x 0$.
The immediate response here is that if $\map g x 0$, then $\dfrac {\map f x} {\map g x} \ne c$ unless it is the case that $\map f x = 0$ also.
However, this would then suggest that the equality condition is undefined at such a point.
Hence the given equality condition $\map g x = c \map f x$ is in general preferred.
== Sources ==
* : $\S 36$: Inequalities: $36.15$: Minkowski's Inequality for Integrals
Category:Minkowski's Inequality for Integrals
Minkowski's Inequality for Sums

== Theorem ==
Let $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n \in \R_{\ge 0}$ be non-negative real numbers.
Let $p \in \R$, $p \ne 0$ be a real number.
If $p < 0$, then we require that $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n$ be strictly positive.
If $p > 1$, then:
:$\ds \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1/p} \le \paren {\sum_{k \mathop = 1}^n a_k^p}^{1/p} + \paren {\sum_{k \mathop = 1}^n b_k^p}^{1/p}$
If $p < 1$, $p \ne 0$, then:
:$\ds \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1/p} \ge \paren {\sum_{k \mathop = 1}^n a_k^p}^{1/p} + \paren {\sum_{k \mathop = 1}^n b_k^p}^{1/p}$
=== Condition for Equality ===
=== Corollary ===
== Proof ==
=== Proof for $p = 2$ ===
$p = 2$ is an easily proved special case:
=== Proof for $p > 1$ ===
=== Proof for $p < 1$, $p \ne 0$ ===
== Also known as ==
== Also see ==
* Minkowski's Inequality for Integrals
== Sources ==
* : $3$: Elementary Analytic Methods: $3.2$ Inequalities: Minkowski's Inequality for Sums: $3.2.12$
* : $\S 36$: Inequalities: $36.12$: Minkowski's Inequality
* 
Category:Minkowski's Inequality for Sums
Category:Minkowski's Inequality
Category:Algebra
Category:Analysis
Minkowski's Inequality for Sums/Also known as

== Minkowski's Inequality for Sums: Also known as ==
Minkowski's Inequality for Sums is also known just as Minkowski's Inequality.
However, this can cause it to be confused with Minkowski's Inequality for Integrals, so will not be used in this context on .
== Sources ==
* : $\S 36$: Inequalities: $36.12$: Minkowski's Inequality
* 
Category:Minkowski's Inequality for Sums
Minkowski's Inequality for Sums/Corollary

== Corollary to Minkowski's Inequality for Sums ==
Let $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n \in \R$ be real numbers.
Let $p \in \R$ be a real number.
If $p > 1$, then:
:$\ds \paren {\sum_{k \mathop = 1}^n \size {a_k + b_k}^p}^{1/p} \le \paren {\sum_{k \mathop = 1}^n \size {a_k}^p}^{1/p} + \paren {\sum_{k \mathop = 1}^n \size {b_k}^p}^{1/p}$
== Proof ==
== Also known as ==
This result itself, like the main result of which it is referenced as a corollary, is sometimes called Minkowski's Inequality for Sums.
Category:Minkowski's Inequality for Sums
Minkowski's Inequality for Sums/Equality

== Theorem ==
Let $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n \in \R_{\ge 0}$ be non-negative real numbers.
Let $p \in \R$, $p \ne 0$ be a real number.
Then equality in Minkowski's Inequality for Sums, that is:
:$\ds \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1 / p} = \paren {\sum_{k \mathop = 1}^n a_k^p}^{1 / p} + \paren {\sum_{k \mathop = 1}^n b_k^p}^{1 / p}$
holds , for all $k \in \closedint 1 n$:
:$\dfrac {a_k} {b_k} = c$
for some $c \in \R_{>0}$.
== Proof ==
== Also known as ==
== Sources ==
* : $3$: Elementary Analytic Methods: $3.2$ Inequalities: Minkowski's Inequality for Sums: $3.2.12$
* : $\S 36$: Inequalities: $36.12$: Minkowski's Inequality
Category:Minkowski's Inequality for Sums
Minkowski's Inequality for Sums/Index 2

== Theorem ==
Let $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n \ge 0$ be non-negative real numbers.
Then:
:$\ds \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^2}^{1 / 2} \le \paren {\sum_{k \mathop = 1}^n a_k^2}^{1 / 2} + \paren {\sum_{k \mathop = 1}^n b_k^2}^{1 / 2}$
== Proof ==
The result follows from Order is Preserved on Positive Reals by Squaring.
== Also see ==
This result is a special case of Minkowski's Inequality for Sums, where $p = 2$.
== Sources ==
* : $\S 1$: Real Numbers: Exercise $\S 1.12 \ (6)$
Category:Minkowski's Inequality for Sums
Minkowski's Inequality for Sums/Index Greater than 1

== Theorem ==
Let $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n \in \R_{\ge 0}$ be non-negative real numbers.
Let $p \in \R$ be a real number such that $p > 1$.
Then:
:$\ds \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1 / p} \le \paren {\sum_{k \mathop = 1}^n {a_k}^p}^{1 / p} + \paren {\sum_{k \mathop = 1}^n {b_k}^p}^{1 / p}$
== Proof 1 ==
== Proof 2 ==
Category:Minkowski's Inequality for Sums
Minkowski's Inequality for Sums/Index Greater than 1/Proof 1

== Theorem ==
== Proof ==
Define:
:$q = \dfrac p {p - 1}$
Then:
:$\dfrac 1 p + \dfrac 1 q = \dfrac 1 p + \dfrac {p - 1} p = 1$
It follows that:
Category:Minkowski's Inequality for Sums
Minkowski's Inequality for Sums/Index Greater than 1/Proof 2

== Theorem ==
== Proof ==
Let $\mathbf a$ and $\mathbf b$ be real finite sequences:
Let $\norm {\mathbf a}_p$ denote the $p$-norm of $\mathbf a$:
:$\norm {\mathbf a}_p := \paren {\ds \sum_{k \mathop = 1}^n {a_k}^p}^{1 / p}$
Define:
:$q = \dfrac p {p - 1}$
Then:
:$\dfrac 1 p + \dfrac 1 q = \dfrac 1 p + \dfrac {p - 1} p = 1$
Then:
Category:Minkowski's Inequality for Sums
Minkowski's Inequality for Sums/Index Less than 1

== Theorem ==
Let $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n \in \R_{\ge 0}$ be non-negative real numbers.
Let $p \in \R$ be a real number.
If $p < 0$, then we require that $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_n$ be strictly positive.
If $p < 1$, $p \ne 0$, then:
:$\ds \paren {\sum_{k \mathop = 1}^n \paren {a_k + b_k}^p}^{1/p} \ge \paren {\sum_{k \mathop = 1}^n a_k^p}^{1/p} + \paren {\sum_{k \mathop = 1}^n b_k^p}^{1/p}$
== Proof ==
Define:
:$q = \dfrac p {p - 1}$
Then:
:$\dfrac 1 p + \dfrac 1 q = \dfrac 1 p + \dfrac {p - 1} p = 1$
In this case, $p$ and $q$ have opposite sign.
The proof then follows the same lines as the proof for $p > 1$, except that the Reverse Hölder's Inequality for Sums is applied instead.
== Also known as ==
This result is also known as the Reverse Minkowski's Inequality (for Sums).
Category:Algebra
Category:Analysis
Minkowski's Theorem

== Theorem ==
Let $L$ be a lattice in $\R^n$.
Let $d$ be the covolume of $L$.
Let $\mu$ be a translation invariant measure on $\R^n$
Let $S$ be a convex subset of $\R^n$ that is symmetric about the origin, i.e. such that:
:$\forall p \in S : -p \in S$ 
Let the volume of $S$ be greater than $2^n d$.
Then $S$ contains a non-zero point of $L$.
== Proof ==
Let $D$ be any fundamental parallelepiped.
Then by definition:
:$\ds \R^n = \coprod \limits_{\vec x \mathop \in L} \paren {D + \vec x}$
where:
: $A + \vec x := \set {\vec a + \vec x : \vec a \in A}$
By Intersection with Subset is Subset:
:$\dfrac 1 2 S \cap \R^n = \dfrac 1 2 S \iff \dfrac 1 2 S \subseteq \R^n$
Hence by Intersection Distributes over Union:
:$(1): \quad \ds \frac 1 2 S = \coprod \limits_{\vec x \mathop \in L} \paren {\frac 1 2 S \cap \paren {D + \vec x} }$
where:
: $\dfrac 1 2 S := \set {\dfrac 1 2 \vec s: \vec s \in S}$
Consider the intersection of $D + \vec x$ and $\dfrac 1 2 S$.
This is obtained by adding $\vec x$ to every point in $D$ then taking those points that are also in $S$.
However, this is the same as subtracting $\vec x$ from all elements of $\dfrac 1 2 S$, taking the elements that are also in $D$ and adding $\vec x$ to restore them to their original position.
Thus:
:$\ds \frac 1 2 S \cap \paren {D + \vec x} = \paren {\paren {\frac 1 2 S - \vec x} \cap D} + \vec x$
Since, , $\mu$ is translation invariant:
 the sets $\ds \set {\frac 1 2 S - \vec x: \vec x \in L}$ are pairwise disjoint.
That is:
:$\ds \forall \vec x, \vec y \in L: \paren {\frac 1 2 S - \vec x} \cap \paren {\frac 1 2 S - \vec y} \ne \O \iff \vec x \ne \vec y$
Then:
which is a contradiction.
So $\ds \set {\frac 1 2 S - \vec x: \vec x \in L}$ are not pairwise disjoint.
This means:
:$\ds \exists \vec x, \vec y \in L: \vec x \ne \vec y, \paren {\frac 1 2 S - \vec x} \cap \paren {\frac 1 2 S - \vec y} \ne \O$
Therefore there exist $\vec {p_1}, \vec {p_2} \in L$ such that $\vec {p_1} \ne \vec {p_2}$ and:
:$\ds \frac 1 2 \vec {p_1} - \vec x = \frac 1 2 \vec {p_2} - \vec y$
and therefore:
:$\ds \frac 1 2 \paren {\vec {p_1} - \vec {p_2} } = \vec x - \vec y \in L$
Since $S$ is convex, we have that:
:$\dfrac 1 2 \paren {\vec {p_1} - \vec {p_2} } \in S$
As $\vec {p_1} \ne \vec {p_2}$ by definition:
:$\dfrac 1 2 \paren {\vec {p_1} - \vec {p_2} } \ne \vec 0$
Hence the result.
== Sources ==
* 
Category:Number Theory
Category:Geometry of Numbers
Category:Convex Sets (Vector Spaces)
Minkowski Functional of Balanced Convex Absorbing Set in Vector Space is Seminorm

== Theorem ==
Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$. 
Let $A \subseteq X$ be a set that is balanced, convex and absorbing.
Let $\mu_A$ be the Minkowski functional of $A$. 
Then $\mu_A$ is a seminorm. 
== Proof ==
=== Case 1: $\GF = \R$ ===
From Balanced Set in Vector Space is Symmetric, $A$ is symmetric.
Hence by Minkowski Functional of Symmetric Convex Absorbing Set in Real Vector Space is Seminorm, $\mu_A$ is a seminorm in this case.
=== Case 2: $\GF = \C$ ===
From Minkowski Functional of Convex Absorbing Set is Positive Homogeneous, $\mu_A$ is a sublinear functional.
Hence we have: 
:$\map {\mu_A} {x + y} \le \map {\mu_A} x + \map {\mu_A} y$ for all $x, y \in X$
and hence .
We also have: 
:$\map {\mu_A} {r x} = r \map {\mu_A} x$ for all $r \in \hointr 0 \infty$ and $x \in X$.
Towards , we want to show that: 
:$\map {\mu_A} {r x} = \map {\mu_A} x$ for all $r \in \C$ with $\cmod r = 1$.
From the definition of a balanced set, we have: 
:$r A \subseteq A$
and since $\cmod {r^{-1} } = 1$, we have: 
:$r^{-1} A \subseteq A$
Then we have: 
:$r A \subseteq A \subseteq r A$
so that: 
:$A = r A$
Then we have: 
Now take $r \in \C \setminus \hointl 0 \infty$ and $x \in X$. 
We have: 
proving .
Category:Minkowski Functionals
Category:Seminorms
Minkowski Functional of Convex Absorbing Set is Finite

== Theorem ==
Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$.
Let $A \subseteq X$ be a convex absorbing set. 
Let $\mu_A$ be the Minkowski functional of $A$. 
Then for each $x \in X$, $\map {\mu_A} x$ is a finite extended real number.
That is:
:$\forall x \in X: \map {\mu_A} x < \infty$
== Proof ==
Let $x \in X$. 
From Characterization of Convex Absorbing Set in Vector Space:
:$\exists t \in \R_{>0}: x \in t A$
where $t A$ denotes the dilation of $A$ by $t$.
Then: 
:$x \in t^{-1} C$
so that:
:$t \in \set {t > 0 : t^{-1} x \in A}$
Then, we have:
:$\map {\mu_A} x \le t < \infty$ 
Category:Minkowski Functionals
Minkowski Functional of Convex Absorbing Set is Positive Homogeneous

== Theorem ==
Let $\GF \in \set {\R, \C}$. 
Let $X$ be a vector space over $\GF$.
Let $A$ be a convex absorbing set. 
Let $\mu_A$ be the Minkowski functional of $A$. 
Then $\mu_A$ is positive homogeneous. 
That is, for each $t \ge 0$ we have:
:$\map {\mu_A} {t x} = t \map {\mu_A} x$
== Proof ==
From Absorbing Set in Vector Space contains Zero Vector, we have ${\mathbf 0}_X \in A$. 
So $\map {\mu_A} {\mathbf 0_X} = 0$.
So the claim clearly holds for $t = 0$.
Now take $t > 0$. 
We argue that: 
:$\set {s > 0 : t x \in s C} = t \set {s > 0 : x \in s C}$
We have: 
:$s \in \set {s > 0 : t x \in s C}$
 $s > 0$ and:
:$t x \in s C$
This is equivalent to: 
:$x \in \paren {\dfrac s t} C$
which is equivalent to: 
:$\dfrac s t \in \set {s > 0 : x \in s C}$
Hence we deduce: 
:$\set {s > 0 : t x \in s C} = t \set {s > 0 : x \in s C}$
From Multiple of Infimum, we obtain: 
:$\map {\mu_C} {t x} = t \map {\mu_C} x$ 
Category:Minkowski Functionals