avewright/proofwiki-math huggingface dataset:
Theorem: Exchange of Order of Summation

:$\ds \sum_{\map R i} \sum_{\map S j} a_{i j} = \sum_{\map S j} \sum_{\map R i} a_{i j}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{\map R i} \sum_{\map S {i, j} } a_{i j}
      | r = \sum_{i, j \mathop \in \Z} a_{i j} \sqbrk {\map R i} \sqbrk {\map S {i, j} }
      | c = 
}}
{{eqn | r = \sum_{i, j \mathop \in \Z} a_{i j} \sqbrk {\map R i \land \map S {i, j} }
      | c = 
}}
{{eqn | r = \sum_{i, j \mathop \in \Z} a_{i j} \sqbrk {\map {S'} j} \sqbrk {\map {R'} {i, j} }
      | c = 
}}
{{eqn | r = \sum_{\map {S'} j} \sum_{\map {R'} {i, j} } a_{i j}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Exchange of Order of Summation

:$\ds \sum_{\map R i} \sum_{\map S j} a_{i j} = \sum_{\map S j} \sum_{\map R i} a_{i j}$

Proof:
Let $n$ be the cardinality of $T$.
The proof goes by induction on $n$.
=== Basis for the Induction ===
Let $n = 0$.
{{finish}}
=== Induction Step ===
Let $n > 0$.
Let $t \in T$.
Use Cardinality of Set minus Singleton
{{ProofWanted}}
Theorem: Sum of Summations equals Summation of Sum/Infinite Sequence

Let $R: \Z \to \set {\T, \F}$ be a propositional function on the set of integers $\Z$.
Let $\ds \sum_{\map R i} x_i$ denote a summation over $R$.
Let the fiber of truth of $R$ be infinite.
Let $\ds \sum_{\map R i} b_i$ and $\ds \sum_{\map R i} c_i$ be convergent.
Then:
:$\ds \sum_{\map R i} \paren {b_i + c_i} = \sum_{\map R i} b_i + \sum_{\map R i} c_i$

Proof:
Let $b_i =: a_{i 1}$ and $c_i =: a_{i 2}$.
Then:
{{begin-eqn}}
{{eqn | l = \sum_{\map R i} \paren {b_i + c_i}
      | r = \sum_{\map R i} \paren {a_{i 1} + a_{i 2} }
      | c = by definition
}}
{{eqn | r = \sum_{\map R i} \paren {\sum_{1 \mathop \le j \mathop \le 2} a_{i j} }
      | c = {{Defof|Summation}}
}}
{{eqn | r = \sum_{1 \mathop \le j \mathop \le 2} \paren {\sum_{\map R i} a_{i j} }
      | c = Exchange of Order of Summation: Finite and Infinite Series
}}
{{eqn | r = \sum_{\map R i} a_{i 1} + \sum_{\map R i} a_{i 2}
      | c = {{Defof|Summation}}
}}
{{eqn | r = \sum_{\map R i} b_i + \sum_{\map R i} c_i
      | c = by definition
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Summations equals Summation of Sum/Infinite Sequence

Let $R: \Z \to \set {\T, \F}$ be a propositional function on the set of integers $\Z$.
Let $\ds \sum_{\map R i} x_i$ denote a summation over $R$.
Let the fiber of truth of $R$ be infinite.
Let $\ds \sum_{\map R i} b_i$ and $\ds \sum_{\map R i} c_i$ be convergent.
Then:
:$\ds \sum_{\map R i} \paren {b_i + c_i} = \sum_{\map R i} b_i + \sum_{\map R i} c_i$

Proof:
By definition, $\ds \sum_{\map R i} b_i$ and $\ds \sum_{\map R i} c_i$ are sequences in $\R$.
Hence the result as an instance of Sum Rule for Real Sequences.
{{qed}}
Theorem: Exchange of Order of Summation with Dependency on Both Indices

:$\ds \sum_{\map R i} \sum_{\map S {i, j} } a_{i j} = \sum_{\map {S'} j} \sum_{\map {R'} {i, j} } a_{i j}$
where:
:$\map {S'} j$ denotes the propositional function:
::there exists an $i$ such that both $\map R i$ and $\map S {i, j}$ hold
:$\map {R'} {i, j}$ denotes the propositional function:
::both $\map R i$ and $\map S {i, j}$ hold.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{\map R i} \sum_{\map S {i, j} } a_{i j}
      | r = \sum_{i, j \mathop \in \Z} a_{i j} \sqbrk {\map R i} \sqbrk {\map S {i, j} }
      | c = 
}}
{{eqn | r = \sum_{i, j \mathop \in \Z} a_{i j} \sqbrk {\map R i \land \map S {i, j} }
      | c = 
}}
{{eqn | r = \sum_{i, j \mathop \in \Z} a_{i j} \sqbrk {\map {S'} j} \sqbrk {\map {R'} {i, j} }
      | c = 
}}
{{eqn | r = \sum_{\map {S'} j} \sum_{\map {R'} {i, j} } a_{i j}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Summation of i from 1 to n of Summation of j from 1 to i

:$\ds \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^i a_{i j} = \sum_{j \mathop = 1}^n \sum_{i \mathop = j}^n a_{i j}$

Proof:
:$\ds \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^i$
can be expressed as:
:$\ds \sum_{\map R i} \sum_{\map S {i, j} } a_{i j}$
where:
:$\map R i$ is the propositional function $1 \le i \le n$
:$\map S {i, j}$ is the propositional function $1 \le j \le i$
We wish to find a propositional function $\map {S'} j$ which is to be:
:there exists an $i$ such that both $1 \le i \le n$ and $1 \le j \le i$
This is satisfied by the propositional function:
:$\map {S'} j := 1 \le j \le n$
Next we wish to find a propositional function $\map {R'} {i, j}$ which is to be:
:both $1 \le i \le n$ and $1 \le j \le i$
This is satisfied by the propositional function:
:$\map {R'} {i, j} := j \le i \le n$
Hence the result, from Exchange of Order of Summation with Dependency on Both Indices.
{{qed}}
Theorem: Summation of i from 1 to n of Summation of j from 1 to i

:$\ds \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^i a_{i j} = \sum_{j \mathop = 1}^n \sum_{i \mathop = j}^n a_{i j}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^i a_{i j}
      | r = \sum_{i, j \mathop \in \Z} a_{i j} \left[{1 \le i \le n}\right] \left[{1 \le j \le i}\right]
      | c = 
}}
{{eqn | r = \sum_{i, j \mathop \in \Z} a_{i j} \left[{1 \le j \le i \le n}\right]
      | c = 
}}
{{eqn | r = \sum_{i, j \mathop \in \Z} a_{i j} \left[{1 \le j \le n}\right] \left[{j \le i \le n}\right]
      | c = 
}}
{{eqn | r = \sum_{j \mathop = 1}^n \sum_{i \mathop = j}^n a_{i j}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Permutation of Indices of Summation/Infinite Series

Let the fiber of truth of $R$ be infinite.
Let $\ds \sum_{\map R i} a_i$ be absolutely convergent.
Then:
:$\ds \sum_{\map R j} a_j = \sum_{\map R {\map \pi j} } a_{\map \pi j}$

Proof:
This is a restatemtent of Manipulation of Absolutely Convergent Series: Permutation in the context of summations.
{{qed}}
Theorem: Sum of Summations equals Summation of Sum

Let $R: \Z \to \set {\T, \F}$ be a propositional function on the set of integers.
Let $\ds \sum_{\map R i} x_i$ denote a summation over $R$.
Let the fiber of truth of $R$ be finite.
Then:
:$\ds \sum_{\map R i} \paren {b_i + c_i} = \sum_{\map R i} b_i + \sum_{\map R i} c_i$

Proof:
Let $b_i =: a_{i 1}$ and $c_i =: a_{i 2}$.
Then:
{{begin-eqn}}
{{eqn | l = \sum_{\map R i} \paren {b_i + c_i}
      | r = \sum_{\map R i} \paren {a_{i 1} + a_{i 2} }
      | c = Definition of $b_i$ and $c_i$
}}
{{eqn | r = \sum_{\map R i} \paren {\sum_{j \mathop = 1}^2 a_{i j} }
      | c = {{Defof|Summation}}
}}
{{eqn | r = \sum_{j \mathop = 1}^2 \paren {\sum_{\map R i} a_{i j} }
      | c = Exchange of Order of Summation
}}
{{eqn | r = \sum_{\map R i} a_{i 1} + \sum_{\map R i} a_{i 2}
      | c = {{Defof|Summation}}
}}
{{eqn | r = \sum_{\map R i} b_i + \sum_{\map R i} c_i
      | c = Definition of $b_i$ and $c_i$
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Summations equals Summation of Sum

Let $R: \Z \to \set {\T, \F}$ be a propositional function on the set of integers.
Let $\ds \sum_{\map R i} x_i$ denote a summation over $R$.
Let the fiber of truth of $R$ be finite.
Then:
:$\ds \sum_{\map R i} \paren {b_i + c_i} = \sum_{\map R i} b_i + \sum_{\map R i} c_i$

Proof:
Let $b_i =: a_{i 1}$ and $c_i =: a_{i 2}$.
Then:
{{begin-eqn}}
{{eqn | l = \sum_{\map R i} \paren {b_i + c_i}
      | r = \sum_{\map R i} \paren {a_{i 1} + a_{i 2} }
      | c = by definition
}}
{{eqn | r = \sum_{\map R i} \paren {\sum_{1 \mathop \le j \mathop \le 2} a_{i j} }
      | c = {{Defof|Summation}}
}}
{{eqn | r = \sum_{1 \mathop \le j \mathop \le 2} \paren {\sum_{\map R i} a_{i j} }
      | c = Exchange of Order of Summation: Finite and Infinite Series
}}
{{eqn | r = \sum_{\map R i} a_{i 1} + \sum_{\map R i} a_{i 2}
      | c = {{Defof|Summation}}
}}
{{eqn | r = \sum_{\map R i} b_i + \sum_{\map R i} c_i
      | c = by definition
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Summations equals Summation of Sum

Let $R: \Z \to \set {\T, \F}$ be a propositional function on the set of integers.
Let $\ds \sum_{\map R i} x_i$ denote a summation over $R$.
Let the fiber of truth of $R$ be finite.
Then:
:$\ds \sum_{\map R i} \paren {b_i + c_i} = \sum_{\map R i} b_i + \sum_{\map R i} c_i$

Proof:
By definition, $\ds \sum_{\map R i} b_i$ and $\ds \sum_{\map R i} c_i$ are sequences in $\R$.
Hence the result as an instance of Sum Rule for Real Sequences.
{{qed}}
Theorem: Sum of Summations over Overlapping Domains

:$\ds \sum_{\map R j} a_j + \sum_{\map S j} a_j = \sum_{\map R j \mathop \lor \map S j} a_j + \sum_{\map R j \mathop \land \map S j} a_j$
where $\lor$ and $\land$ signify logical disjunction and logical conjunction respectively.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{\map R j} a_j + \sum_{\map S j} a_j
      | r = \sum_{j \mathop \in \Z} a_j \sqbrk {\map R j} + \sum_{j \mathop \in \Z} a_j \sqbrk {\map R j}
      | c = {{Defof|Summation by Iverson's Convention}}
}}
{{eqn | r = \sum_{j \mathop \in \Z} a_j \paren {\sqbrk {\map R j} + \sqbrk {\map R j} }
      | c = 
}}
{{end-eqn}}
Let:
:$A := \set {j \in \Z: \map R j}$
:$B := \set {j \in \Z: \map R j}$
The result then follows from Cardinality of Set Union.
{{qed}}
Theorem: Summation of Products of n Numbers taken m at a time with Repetitions/Examples/Order 2

:$\ds \sum_{i \mathop = a}^b \sum_{j \mathop = a}^i x_i x_j = \dfrac 1 2 \paren {\paren {\sum_{i \mathop = a}^b x_i}^2 + \paren {\sum_{i \mathop = a}^b {x_i}^2} }$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = S_1
      | o = :=
      | r = \sum_{i \mathop = a}^b \sum_{j \mathop = a}^i x_i x_j
      | c = 
}}
{{eqn | r = \sum_{j \mathop = a}^b \sum_{i \mathop = j}^b x_i x_j
      | c = Summation of i from 1 to n of Summation of j from 1 to i
}}
{{eqn | r = \sum_{i \mathop = a}^b \sum_{j \mathop = i}^b x_i x_j
      | c = Change of Index Variable of Summation
}}
{{eqn | o = =:
      | r = S_2
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = 2 S_1
      | r = S_1 + S_2
      | c = 
}}
{{eqn | r = \sum_{i \mathop = a}^b \paren {\sum_{j \mathop = a}^i x_i x_j + \sum_{j \mathop = i}^b x_i x_j}
      | c = 
}}
{{eqn | r = \sum_{i \mathop = a}^b \paren {\paren {\sum_{j \mathop = a}^b x_i x_j} + x_i x_i}
      | c = Sum of Summations over Overlapping Domains: Example
}}
{{eqn | r = \sum_{i \mathop = a}^b \sum_{j \mathop = a}^b x_i x_j + \sum_{i \mathop = a}^b x_i x_i
      | c = Sum of Summations equals Summation of Sum
}}
{{eqn | r = \paren {\sum_{i \mathop = a}^b x_i} \paren {\sum_{j \mathop = a}^b x_j} + \paren {\sum_{i \mathop = a}^b {x_i}^2}
      | c = General Distributivity Theorem and Change of Index Variable of Summation
}}
{{end-eqn}}
The result follows on multiplying by $\dfrac 1 2$.
{{qed}}
Theorem: Summation of Products of n Numbers taken m at a time with Repetitions/Examples/Order 2

:$\ds \sum_{i \mathop = a}^b \sum_{j \mathop = a}^i x_i x_j = \dfrac 1 2 \paren {\paren {\sum_{i \mathop = a}^b x_i}^2 + \paren {\sum_{i \mathop = a}^b {x_i}^2} }$

Proof:
We have that:
:$\ds \sum_{i \mathop = a}^b \sum_{j \mathop = a}^i x_i x_j = \sum_{a \mathop \le j_1 \mathop \le j_2 \mathop \le b} x_{j_1} x_{j_2}$
From Summation of Products of n Numbers taken m at a time with Repetitions:
:$\ds \sum_{a \mathop \le j_1 \mathop \le \cdots \mathop \le j_m \mathop \le b} x_{j_1} \cdots x_{j_m} = \sum_{\substack {k_1, k_2, \ldots, k_m \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop + \cdots \mathop + m k_m \mathop = m} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !} \dfrac { {S_2}^{k_2} } {2^{k_2} k_2 !} \cdots \dfrac { {S_m}^{k_m} } {m^{k_m} k_m !}$
where:
:$S_r = \ds \sum_{k \mathop = a}^b {x_k}^r$ for $r \in \Z_{\ge 0}$.
Setting $m = 2$:
{{begin-eqn}}
{{eqn | l = \sum_{a \mathop \le j_1 \mathop \le j_2 \mathop \le b} x_{j_1} x_{j_2}
      | r = \sum_{\substack {k_1, k_2 \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop = 2} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !} \dfrac { {S_2}^{k_2} } {2^{k_2} k_2 !}
      | c = 
}}
{{eqn | r = \dfrac { {S_1}^2 {S_2}^0} {\paren {1^2 \times 2!} \paren {2^0 \times 0!} } + \dfrac { {S_1}^0 {S_2}^1} {\paren {1^0 \times 0!} \paren {2^1 \times 1!} }
      | c = as $k_1 = 2, k_2 = 0$ and $k_1 = 0, k_2 = 1$ are the only $k_1$ and $k_2$ to fulfil the criteria
}}
{{eqn | r = \frac 1 2 \paren { {S_1}^2 + S_2}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Uniqueness of Continuously Differentiable Solution to Initial Value Problem

Let $D \subseteq \R^2$ be a region containing $\tuple {a, b}$.
Let $f: D \to \R$ be real-valued mapping such that $f$ and $\dfrac {\partial f} {\partial x}$ are continuous on $D$.
Consider the initial value problem:
:$\dfrac {\d x} {\d t} = \map f {t, x}$
:$\map x a = b$
Suppose the initial value problem above has a solution $\phi$ for all $x$ in some interval $J$ containing $a$.
Then the solution $\phi$ is  unique on $J$.

Proof:
{{ProofWanted|Is this the same as Picard's Little Theorem?}}
Theorem: Exhausting Sequence of Sets on the Strictly Positive Real Numbers

For each $k \in \N$, let $S_k = \openint {\dfrac 1 k} k$.
Then $\sequence {S_k}_k$ is an exhausting sequence of sets on $\R_{>0}$.

Proof:
To prove that $\sequence {S_k}_k$ is exhausting $\R_{>0}$, it is sufficient to show:
:$(1): \quad \forall k \in \N: S_k \subseteq S_{k + 1}$
:$(2): \quad \ds \bigcup_{k \mathop \in \N} S_k = \R_{>0}$
Theorem: Way Below in Ordered Set of Topology

Let $\struct {S, \tau}$ be a topological space.
Let $\struct {\tau, \preceq}$ be an ordered set
where $\preceq \mathop = \subseteq \restriction_{\tau \times \tau}$
Let $x, y \in \tau$.
Then:
:$x \ll y$ in $\struct {\tau, \preceq}$
{{iff}}
:for every set $F$ of open subsets of $S$: if $y \subseteq \bigcup F$, then:
::there exists a finite subset $G$ of $F$: $x \subseteq \bigcup G$
where $\ll$ denotes the way below relation.

Proof:
=== Sufficient Condition ===
Let
:$x \ll y$
Let $F$ be a set of open subsets of $S$ such that
:$y \subseteq \bigcup F$
By definition of subset:
:$F \subseteq \tau$
By proof of Topology forms Complete Lattice:
:$\sup F = \bigcup F$
By assumption:
:$y \preceq \sup F$
By Topology forms Complete Lattice:
:$\struct {\tau, \preceq}$ is complete lattice.
By Way Below in Complete Lattice:
:$\exists G \in \map {\it Fin} F: x \preceq \sup G$
where $\map {\it Fin} F$ denotes the set of all finite subsets of $F$.
Thus by proof of Topology forms Complete Lattice:
:$x \subseteq \bigcup G$
{{qed|lemma}}
Theorem: Continuous Inverse Theorem

Let $f$ be a real function defined on an interval $I$.
Let $f$ be strictly monotone and continuous on $I$.
Let $g$ be the inverse mapping to $f$.
Let $J := f \left[{I}\right]$ be the image of $I$ under $f$.
Then $g$ is strictly monotone and continuous on $J$.

Proof:
From Strictly Monotone Real Function is Bijective, $f$ is a bijection.
From Inverse of Strictly Monotone Function, $f^{-1} : J \to I$ exists and is strictly monotone.
From Surjective Monotone Function is Continuous, $f^{-1}$ is continuous.
Hence the result.
{{qed}}
Theorem: Logarithm is Strictly Concave

:$\ln x: x > 0$ strictly concave.

Proof:
From Logarithm is Strictly Increasing, $\ln x$ is strictly increasing on $x > 0$.
From Second Derivative of Natural Logarithm Function:
:$D^2 \ln x = -\dfrac 1 {x^2}$
Thus $D^2 \ln x$ is strictly negative on $x > 0$ (in fact is strictly negative for all $x \ne 0$).
Thus from Derivative of Monotone Function, $D \dfrac 1 x$ is strictly decreasing on $x > 0$.
So from Real Function is Strictly Concave iff Derivative is Strictly Decreasing, $\ln x$ is strictly concave on $x > 0$.
{{qed}}
Theorem: Exponential is Strictly Convex

:The function $f \left({x}\right) = \exp x$ is strictly convex.

Proof:
By definition, the exponential function is the inverse of the natural logarithm function.
From Logarithm is Strictly Increasing, $\ln x$ is strictly increasing.
From Logarithm is Strictly Concave, $\ln x$ is strictly concave.
The result follows from Inverse of Strictly Increasing Strictly Concave Real Function is Strictly Convex.
{{qed}}
Category:Exponential Function
pa119jqwoaw6rc4k41qso9nu8eayuv8
Theorem: Way Below in Complete Lattice

Let $\struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x, y \in S$.
Then
:$x \ll y$
{{iff}}
:$\forall X \subseteq S: y \preceq \sup X \implies \exists A \in \map {\operatorname {Fin} } X: x \preceq \sup A$
where
:$\ll$ denotes the way below relation,
:$\map {\operatorname {Fin} } X$ denotes the set of all finite subsets of $X$.

Proof:
=== Sufficient Condition ===
Let
:$x \ll y$
Let $X \subseteq S$ such that
:$y \preceq \sup X$
By Set of Finite Suprema is Directed:
:$\set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$ is directed.
By definition of union:
:$\bigcup \map {\operatorname {Fin} } X \setminus \set \O = X$
By Supremum of Suprema:
:$\sup X = \sup \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}$
By definition of way below relation:
:$\exists z \in \set {\sup A: A \in \map {\operatorname {Fin} } X \land A \ne \O}: x \preceq z$
Thus
:$\exists A \in \map {\operatorname {Fin} } X: x \preceq \sup A$
{{qed|lemma}}
Theorem: Continuous Midpoint-Convex Function is Convex

Let $f$ be a real function which is defined on a real interval $I$.
Let $f$ be midpoint-convex and continuous on $I$.
Then $f$ is convex.

Proof:
Let $x, y \in I$ and let $t \in \closedint 0 1$.
Let $\sequence {t_n}_{n \mathop \in \N}$ be a sequence of rational numbers in $\closedint 0 1$ converging to $t$.
It follows that:
{{begin-eqn}}
{{eqn | l = \lim \limits_{n \mathop \to\infty} \paren {t_n x + \paren {1 - t_n} y}
      | r = t x + \paren {1 - t} y
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \lim \limits_{n \mathop \to \infty} \paren {t_n \map f x + \paren {1 - t_n} \map f y}
      | r = t \map f x + \paren {1 - t} \map f y
}}
{{end-eqn}}
{{explain|Follows from where? Links needed to results quoted}}
From Midpoint-Convex Function is Rational Convex, $f$ is rational convex. 
From Continuous Mapping is Sequentially Continuous, $f$ is sequentially continuous.
{{explain|Technically, we have sequential continuity defined under the {{ProofWiki}} link above only in terms of the general topological space. In order to connect all the pieces here, we need either to invoke the clauses which state that the real number line is a topological space under which the properties of continuity "mean the same thing" as the traditionally real-analytical definition of continuity, or we need to define sequential continuity in terms of real analysis.}}
As $f$ is rational convex:
:$\forall n \in \N: \map f {t_n x + \paren {1 - t_n} y} \le t_n \map f x + \paren {1 - t_n} \map f y$
From sequential continuity of $f$ and Inequality Rule for Real Sequences:
{{begin-eqn}}
{{eqn | l = \map f {t x + \paren {1 - t} y}
      | r = \lim_{n \mathop \to \infty} \map f {t_n x + \paren {1 - t_n} y}
}}
{{eqn | o = \le
      | r = \lim_{n \mathop \to \infty} \paren {t_n \map f x + \paren {1 - t_n} \map f y}
}}
{{eqn | r = t \map f x + \paren {1 - t} \map f y
}}
{{end-eqn}}
which completes the proof.
{{qed}}
Theorem: Way Below Compact is Topological Compact

Let $T = \struct {S, \tau}$ be a topological space.
Let $L = \struct {\tau, \preceq}$ be an ordered set where $\preceq \mathop = \subseteq\restriction_{\tau \times \tau}$
Let $x \in \tau$.
Then
:$x$ is compact in $L$ (it means: $x \ll x$)
{{iff}}
:$T_x$ is compact (topologically)
where $T_x = \struct {x, \tau_x}$ denotes the topological subspace of $x$.

Proof:
=== Sufficient Condition ===
Let
:$x \ll x$
Let $F \subseteq  \tau_x$ be a open cover of $x$.
By definition of cover:
:$x \subseteq \bigcup F$
By definition of topological space:
:$\forall y \in \tau: x \cap y \in \tau$
By definition of subset:
:$\tau_x \subseteq \tau$
By Subset Relation is Transitive:
:$F \subseteq \tau$
By Way Below in Ordered Set of Topology:
:there exists a finite subset $G$ of $F$: $\ds x \subseteq \bigcup G$
By definition:
:$G$ is cover of $x$
Thus by definition:
:$x$ has finite subcover.
Thus by definition:
:$T_x$ is compact.
{{qed|lemma}}
Theorem: Continuous Midpoint-Concave Function is Concave

Let $f$ be midpoint-concave and continuous on $I$.
Then $f$ is concave.

Proof:
As $f$ is midpoint-concave, then $-f$ is midpoint-convex.
{{LinkWanted|Prove the above}}
From Continuous Midpoint-Convex Function is Convex, $-f$ is convex. 
From Real Function is Concave iff its Negative is Convex, $f$ is concave. 
{{qed}}
Theorem: Power Function on Strictly Positive Base is Convex

Let $a \in \R_{>0}$ be a strictly positive real number.
Let $f: \R \to \R$ be the real function defined as:
:$\map f x = a^x$
where $a^x$ denotes $a$ to the power of $x$.
Then $f$ is convex.

Proof:
Let $x, y \in \R$.
Note that, from Power of Positive Real Number is Positive: Real Number:
:$\forall t \in \R: a^t > 0$.
So:
{{begin-eqn}}
{{eqn | l = a^{\paren {x + y} / 2}
      | r = \sqrt {a^{x + y} }
      | c = Exponent Combination Laws: Power of Power: Proof 2
}}
{{eqn | r = \sqrt {a^x a^y}
      | c = Exponent Combination Laws: Product of Powers: Proof 2
}}
{{eqn | o = \le
      | r = \frac {a^x + a^y} 2
      | c = Cauchy's Mean Theorem
}}
{{end-eqn}}
Hence $a^x$ is midpoint-convex.
Further, from Power Function on Strictly Positive Base is Continuous: Real Power, $a^x$ is continuous.
Thus, from Continuous Midpoint-Convex Function is Convex, $a^x$ is convex.
{{qed}}
Category:Real Analysis
Category:Powers
ozrx4xqacs1l03nudbcq362bc9qbixd
Theorem: Derivative of Exponential Function/Proof 5/Lemma

:$\forall x \in \R : n \ge \ceiling {\size x} \implies \sequence {\dfrac n {n + x} \paren {1 + \dfrac x n}^n}$ is increasing.

Proof:
First:
{{begin-eqn}}
{{eqn | l = n
      | o = >
      | r = \ceiling {\size x}
}}
{{eqn | ll= \leadsto
      | l = n 
      | o = >
      | r = -x
      | c = Negative of Absolute Value and Real Number is between Ceiling Functions
}}
{{eqn | ll= \leadsto
      | l = \frac n {n + x}
      | o = >
      | r = 0
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = n
      | o = >
      | m = \ceiling {\size x}
}}
{{eqn | ll= \leadsto
      | l = n
      | o = >
      | m = \size x
      | c = Real Number is between Ceiling Functions
}}
{{eqn | ll= \leadsto
      | l = \size {\frac x n}
      | o = <
      | m = 1
      | c = dividing both sides by $n$
}}
{{eqn | ll= \leadsto
      | l = -1
      | o = <
      | m = \frac x n
      | mo= <
      | r = 1
      | c = Negative of Absolute Value: Corollary 1
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | m = 1 + \frac x n
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = <
      | m = \paren {1 + \frac x n}^n
      | c = Power of Positive Real Number is Positive: Natural Number
}}
{{end-eqn}}
So, for $n \ge \ceiling {\size x}$:
:$\sequence {\dfrac n {n + x} }$
and:
:$\sequence {\paren {1 + \dfrac x n}^n}$
are positive.
Now let $n \ge \ceiling {\size x}$.
Suppose first that $x \in \R_{\ge 0}$.
Then:
{{begin-eqn}}
{{eqn | l = \frac n {n + x}
      | o = \le
      | r = \frac {n + 1} {n + x + 1}
}}
{{eqn | ll= \leadstoandfrom
      | l = n \paren {n + x + 1}
      | o = \le
      | r = \paren {n + 1} \paren {n + x}
      | c = Real Number Ordering is Compatible with Multiplication
}}
{{eqn | ll= \leadstoandfrom
      | l = n^2 + n x + n
      | o = \le
      | r = n^2 + n x + n + x
}}
{{eqn | ll= \leadstoandfrom
      | l = 0
      | o = \le
      | r = x
}}
{{end-eqn}}
So $\sequence {\dfrac n {n + x} }$ is increasing.
Further, from Exponential Sequence is Eventually Increasing:
:$\sequence {\paren {1 + \dfrac x n}^n}$ is increasing.
Hence, from Product of Positive Increasing Functions is Increasing:
:$n \ge \ceiling {size x} \implies \sequence {\dfrac n {n + x} \paren {1 + \dfrac x n}^n}$ is increasing.
Suppose instead that $x \in \R_{<0}$.
{{AimForCont}}:
:$\sequence {\dfrac n {n + x} \sequence {1 + \dfrac x n}^n}$ is decreasing.
From above: $\sequence {1 + \dfrac x n} = \sequence {\dfrac {n + x} n}$ is decreasing.
Thus, from Product of Positive Increasing and Decreasing Functions is Decreasing:
:$\sequence {\dfrac {n + x} n \dfrac n {n + x} \paren {1 + \dfrac x n}^n} = \sequence {\paren {1 + \dfrac x n}^n}$ is decreasing.
This contradicts Exponential Sequence is Eventually Increasing.
Hence the result, by Proof by Contradiction.
{{qed}}
Category:Derivative of Exponential Function
rservdv6oiqa01mavewdbulb3cv90ik