avewright/proofwiki-math huggingface dataset:
Theorem: Borel-Cantelli Lemma

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\sequence {E_n}_{n \mathop \in \N}$ be a sequence of $\Sigma$-measurable sets.
Let:
:$\ds \sum_{n \mathop = 1}^\infty \map \mu {E_n} < \infty$
Then:
:$\ds \map \mu {\limsup_{n \mathop \to \infty} E_n} = 0$
where $\limsup$ denotes limit superior of sets.

Proof:
By definition of limit superior:
:$\ds \limsup_{n \mathop \to \infty} E_n = \bigcap_{i \mathop = 1}^\infty \bigcup_{j \mathop = i}^\infty E_j$
Thus, by Measure is Monotone and Intersection is Subset:
:$(1): \quad \ds \map \mu {\limsup_{n \mathop \to \infty} E_n} = \map \mu {\bigcap_{i \mathop = 1}^\infty \bigcup_{j \mathop = i}^\infty E_j} \le \map \mu {\bigcup_{j \mathop = i}^\infty E_j}$
for all $i \in \N$.
By Measure is Subadditive:
:$\ds \map \mu {\bigcup_{j \mathop = i}^\infty E_j} \le \sum_{j \mathop = i}^\infty \map \mu {E_j}$
However, by assumption $\ds \sum_{n \mathop = 1}^\infty \map \mu {E_n}$ converges.
By Tail of Convergent Series tends to Zero this implies:
:$\ds \lim_{i \mathop \to \infty} \sum_{n \mathop = i}^\infty \map \mu {E_n} = 0$
Now $(1)$ implies, together with Lower and Upper Bounds for Sequences, that:
:$\ds \map \mu {\limsup_{n \mathop \to \infty} E_n} \le 0$
But as $\mu$ is a measure, the converse inequality also holds.
Hence:
:$\ds \map \mu {\limsup_{n \mathop \to \infty} E_n} = 0$
{{qed}}
Theorem: Weierstrass M-Test

Let $f_n$ be a sequence of real functions defined on a domain $D \subseteq \R$.
Let $\ds \sup_{x \mathop \in D} \size {\map {f_n} x} \le M_n$ for each integer $n$ and some constants $M_n$
Let $\ds \sum_{i \mathop = 1}^\infty M_i < \infty$.
Then $\ds \sum_{i \mathop = 1}^\infty f_i$ converges uniformly on $D$.

Proof:
Let:
:$\ds S_n = \sum_{i \mathop = 1}^n f_i$
Let:
:$\ds f = \lim_{n \mathop \to \infty} S_n$
To show the sequence of partial sums converge uniformly to $f$, we must show that:
:$\ds \lim_{n \mathop \to \infty} \sup_{x \mathop \in D} \size {f - S_n} = 0$
But:
{{begin-eqn}}
{{eqn | l = \sup_{x \mathop \in D} \size {f - S_n}
      | r = \sup_{x \mathop \in D} \size {\paren {f_1 + f_2 + \dotsb} - \paren {f_1 + f_2 + \dotsb + f_n} }
      | c = 
}}
{{eqn | r = \sup_{x \mathop \in D} \size {f_{n + 1} + f_{n + 2} + \dotsc}
      | c = 
}}
{{end-eqn}}
By the Triangle Inequality, this value is less than or equal to:
:$\ds \sum_{i \mathop = n + 1}^\infty \sup_{x \mathop \in D} \size {\map {f_i} x} \le \sum_{i \mathop = n + 1}^\infty M_i$
We have that:
:$\ds 0 \le \sum_{i \mathop = 1}^\infty M_n < \infty$
It follows from Tail of Convergent Series tends to Zero:
:$\ds 0 \le \lim_{n \mathop \to \infty} \sum_{i \mathop = n + 1}^\infty \sup_{x \mathop \in D} \size {\map {f_i} x} \le \lim_{n \mathop \to \infty} \sum_{i \mathop = n + 1}^\infty M_i = 0$
So:
:$\ds \lim_{n \mathop \to \infty} \sup_{x \mathop \in D} \size {f - S_n} = 0$
Hence the series converges uniformly on the domain.
{{qed}}
{{expand|Establish how broadly this can be applied - it's defined for real functions but should also apply to complex ones and possibly a general metric space.}}
Theorem: Measurable Sets form Sigma-Algebra

Let $\mu^*$ be an outer measure on a set $X$.
Then the set $\map {\mathfrak M} {\mu^*}$ of all $\mu^*$-measurable subsets of $X$ is a $\sigma$-algebra.

Proof:
First, note that $\map {\mathfrak M} {\mu^*}$ is an algebra (of sets).
It remains to be shown that $\map {\mathfrak M} {\mu^*}$ is closed under countable union.
Because $\map {\mathfrak M} {\mu^*}$ is an algebra (of sets), the union of any two $\mu^*$-measurable sets is $\mu^*$-measurable.
Using mathematical induction, it directly follows that the finite union of $\mu^*$-measurable sets is $\mu^*$-measurable.
Let $\sequence {S_n}$ be a sequence of $\mu^*$-measurable subsets of $X$.
Define $\ds S = \bigcup_{n \mathop = 1}^\infty S_n$.
We wish to prove that $S$ is $\mu^*$-measurable.
For all $n \in \N$, the set $T_n = S_1 \cup S_2 \cup \cdots \cup S_n$ is $\mu^*$-measurable.
By Subset of Union, the sequence $\sequence {T_n}$ is increasing.
Also, $T_n \uparrow S$ (as $n \to \infty$) where $\uparrow$ denotes the limit of an increasing sequence of sets.
Let $A$ be any subset of $X$.
By Set Difference Union Intersection:
:$A = \paren {A \cap S} \cup \paren {A \setminus S}$
So by the subadditivity of $\mu^*$, it suffices to prove that $\map {\mu^*} A \ge \map {\mu^*} {A \cap S} + \map {\mu^*} {A \setminus S}$ for any subset $A \subseteq X$.
Then:
{{begin-eqn}}
{{eqn | l = \map {\mu^*} A
      | r = \map {\mu^*} {A \cap T_n} + \map {\mu^*} {A \setminus T_n}
      | c = {{Defof|Measurable Set of Arbitrary Outer Measure|Measurability}} of $T_n$
}}
{{eqn | o = \ge
      | r = \map {\mu^*} {A \cap T_n} + \map {\mu^*} {A \setminus S}
      | c = Set Complement inverts Subsets and Monotonicity of $\mu^*$
}}
{{end-eqn}}
Letting $n \to \infty$, the result follows by Outer Measure of Limit of Increasing Sequence of Sets.
{{qed}}
Theorem: Markov's Inequality

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $A \in \Sigma$.
Let $f : A \to \overline \R$ be an $A$-measurable function.
Then:
:$\ds \map \mu {\set {x \in A: \size {\map f x} \ge t} } \le \frac 1 t \int_A \size f \rd \mu$
for any positive $t \in \R$.

Proof:
Let $t > 0$ and define:
:$B = \set {x \in A: \size {\map f x} \ge t}$
Let $\chi_B$ denote the indicator function of $B$ on $A$. 
For any $x \in A$, either $x \in B$ or $x \notin B$.
In the first case:
:$t \map {\chi_B} x = t \cdot 1 = t \le \size {\map f x}$
In the second case:
:$t \map {\chi_B} x = t \cdot 0 = 0 \le \size {\map f x}$
Hence:
:$\forall x \in A: t \map {\chi_B} x \le \size {\map f x}$
By Integral of Integrable Function is Monotone:
:$\ds \int_A t \chi_B \rd \mu \le \int_A \size f \rd \mu$
But by Integral of Integrable Function is Homogeneous:
:$\ds \int_A t \chi_B \rd \mu = t \int_A \chi_B \rd \mu = t \map \mu B$
Dividing through by $t > 0$:
:$\ds \map \mu B \le \frac 1 t \int_A \size f \rd \mu$
{{qed}}
{{WIP|Cover alternative renditions and extensions from Schilling}}
{{Namedfor|Andrey Andreyevich Markov|cat = Markov A A}}
Theorem: Limit Superior includes Limit Inferior

Let $\set {E_n : n \in \N}$ be a sequence of sets.
Then:
:$\ds \liminf_{n \mathop \to \infty} E_n \subseteq \limsup_{n \mathop \to \infty} E_n$

Proof:
Select any $\ds x \in \liminf_{n \mathop \to \infty} E_n$.
Then by definition 2 of Limit Inferior of Sequence of Sets, $x$ belongs to $E_i$ for all but finitely many values of $i$.
Therefore $x$ belongs to $E_i$ for infinitely many values of $i$.
So by the definition 2 of Limit Superior of Sequence of Sets:
:$\ds x \in \limsup_{n \mathop \to \infty} E_n$
{{qed}}
Theorem: Construction of Outer Measure

Let $X$ be a set.
Let $\powerset X$ be the power set of $X$.
Let $\AA$ be a subset of $\powerset X$ which contains the empty set.
Let $\overline \R_{\ge 0}$ denote the set of positive extended real numbers.
Let $\gamma: \AA \to \overline \R_{\ge 0}$ be a mapping such that $\map \gamma \O = 0$.
Let $\mu^*: \powerset X \to \overline \R_{\ge 0}$ be the mapping defined as:
:$\ds \forall S \in \powerset X: \map {\mu^*} S = \inf \set {\sum_{n \mathop = 0}^\infty \map \gamma {A_n}: \forall n \in \N : A_n \in \AA, \ S \subseteq \bigcup_{n \mathop = 0}^\infty A_n}$
where the infimum of the empty set is $+\infty$.
Then $\mu^*$ is an outer measure on $X$.

Proof:
We check each of the criteria for an outer measure.
From the assumption $\map \gamma \O = 0$:
:$\map {\mu^*} \O = 0$
Any cover of a set is also a cover of a subset of it.
Thus $\mu^*$ is monotone by Infimum of Subset.
It remains to be shown that $\mu^*$ is countably subadditive.
Let $\sequence {S_n}$ be a sequence of subsets of $X$.
Let $\ds S := \bigcup_{n \mathop = 0}^\infty S_n$.
Suppose there does not exist a countable cover for $S_n$ by elements of $\AA$ for some  $n \in \N$.
Then there does not exist a countable cover for $S$ by elements of $\AA$.
In this case, the result follows immediately.
Now suppose that for each $n \in \N$, there exists a countable cover for $S_n$ by elements of $\AA$.
Let $\epsilon \in \R_{>0}$ be an arbitrary (strictly) positive real number.
By definition of infimum, for each $n \in \N$, we can apply the axiom of countable choice to choose a countable cover $\CC_n \subseteq \AA$ of $S_n$ such that:
:$\ds \sum_{x \mathop \in \CC_n} \map \gamma x < \map {\mu^*} {S_n} + \frac \epsilon {2^{n + 1} }$
Let $\ds \CC = \bigcup_{n \mathop = 0}^\infty \CC_n$.
Then $\CC$ is a subset of $\AA$ and a cover for $S$.
Furthermore, $\CC$ is the countable union of countable sets.
By Countable Union of Countable Sets is Countable, $\CC$ is itself countable.
Therefore:
{{begin-eqn}}
{{eqn | l = \map {\mu^*} S
      | o = \le
      | r = \sum_{x \mathop \in \CC} \map \gamma x
      | c = by definition of $\mu^*$
}}
{{eqn | o = \le
      | r = \sum_{n \mathop = 0}^\infty \sum_{x \mathop \in \CC_n} \map \gamma x
      | c = since each $x \in \CC$ belongs to some $\CC_n$
}}
{{eqn | o = \le
      | r = \sum_{n \mathop = 0}^\infty \paren {\map {\mu^*} {S_n} + \frac \epsilon {2^{n + 1} } }
}}
{{eqn | r = \epsilon + \sum_{n \mathop = 0}^\infty \map {\mu^*} {S_n}
      | c = Sum of Infinite Geometric Sequence
}}
{{end-eqn}}
Since $\epsilon$ was arbitrary, the result follows.
{{qed}}
{{ACC}}
Theorem: Additive and Countably Subadditive Function is Countably Additive

Let $\Sigma$ be a $\sigma$-algebra over a set $X$.
Let $f: \Sigma \to \overline \R_{\ge 0}$ be an additive and countably subadditive function, where $\overline \R_{\ge 0}$ denotes the set of positive extended real numbers.
Then $f$ is countably additive.

Proof:
{{rewrite|Eqn templates would be good, I think}}
Let $\sequence {S_n}_{n \mathop \in \N}$ be a sequence of pairwise disjoint elements of $\Sigma$.
Let $N \in \N$ be any natural number.
By Set is Subset of Union:
:$\ds \bigcup_{n \mathop = 0}^N S_n \subseteq \bigcup_{n \mathop = 0}^\infty S_n$
From Non-Negative Additive Function is Monotone:
:$\ds \map f {\bigcup_{n \mathop = 0}^N S_n} \le \map f {\bigcup_{n \mathop = 0}^\infty S_n}$
Also, from Finite Union of Sets in Additive Function:
:$\ds \map f {\bigcup_{n \mathop = 0}^N S_n} = \sum_{n \mathop = 0}^N \map f {S_n}$
Hence:
:$\ds \sum_{n \mathop = 0}^N \map f {S_n} \le \map f {\bigcup_{n \mathop = 0}^\infty S_n}$
{{wtd|Lower and Upper Bounds for Sequences still needs generalization to $\overline \R$ before it can be applied here}}
Taking the limit as $N \to \infty$, it follows by Lower and Upper Bounds for Sequences that:
:$\ds \sum_{n \mathop = 0}^\infty \map f {S_n} \le \map f {\bigcup_{n \mathop = 0}^\infty S_n}$
The reverse inequality holds because of the countable subadditivity of $f$, and thus equality holds.
{{qed}}
Category:Measure Theory
fyunl4x15bfol5ebii5bh9jvfj6cmtq
Theorem: Measure Space from Outer Measure

Suppose $\mu^*$ is an outer measure on a set $X$.
Let $\map {\mathfrak M} {\mu^*}$ be the collection of $\mu^*$-measurable sets.
Let $\mu$ be the restriction of $\mu^*$ to $\map {\mathfrak M} {\mu^*}$.
Then $\struct {X, \map {\mathfrak M} {\mu^*}, \mu}$ is a measure space.

Proof:
First, note that $\map {\mathfrak M} {\mu^*}$ is a $\sigma$-algebra over $X$.
Next, choose $E_1, E_2 \in \map {\mathfrak M} {\mu^*}$ such that $E_1 \cap E_2 = \O$.
Thus:
{{begin-eqn}}
{{eqn | l = \map \mu {E_1 \cup E_2}
      | r = \map {\mu^*} {E_1 \cup E_2}
      | c = as $E_1 \cup E_2 \in \map {\mathfrak M} {\mu^*}$
}}
{{eqn | r = \map {\mu^*} {\paren {E_1 \cup E_2} \cap E_1} + \map {\mu^*} {\paren {E_1 \cup E_2} - E_1}
      | c = {{Defof|Measurable Set}}
}}
{{eqn | r = \map {\mu^*} {E_1} + \map {\mu^*} {E_2}
      | c = since $E_1$ and $E_2$ are disjoint
}}
{{eqn | r = \map \mu {E_1} + \map \mu {E_2}
      | c = since $E_1, E_2 \in \map {\mathfrak M} {\mu^*}$
}}
{{end-eqn}}
Therefore $\mu$ is additive. But because it is constructed from an outer measure, it is also countably subadditive.
Since Additive and Countably Subadditive Function is Countably Additive, it follows that $\mu$ is countably additive.
Finally, also because it is constructed from an outer measure, $\mu$ is nonnegative.
Hence $\struct {X, \map {\mathfrak M} {\mu^*} \mu}$ meets all the criteria of a measure space.
{{qed}}
Theorem: Banach Fixed-Point Theorem

Let $\struct {M, d}$ be a complete metric space.
Let $f: M \to M$ be a contraction.
That is, there exists $q \in \hointr 0 1$ such that for all $x, y \in M$:
:$\map d {\map f x, \map f y} \le q \, \map d {x, y}$
Then there exists a unique fixed point of $f$.

Proof:
=== Uniqueness ===
Let $f$ have two fixed points $p_1, p_2 \in M$.
It is to be proved that $p_1 = p_2$.
{{begin-eqn}}
{{eqn | l = \map d {p_1, p_2}
      | r = \map d {\map f {p_1}, \map f {p_2} }
      | c = {{Defof|Fixed Point}}
}}
{{eqn | o = \le
      | r = q \, \map d {p_1, p_2}
      | c = {{Defof|Contraction Mapping (Metric Space)}}
}}
{{eqn | ll= \leadsto
      | l = \paren {1 - q} \map d {p_1, p_2}
      | o = \le
      | r = 0
      | c = subtracting $q \, \map d {p_1, p_2}$ from both sides
}}
{{end-eqn}}
Then from $\paren {1 - q} > 0$ and $\map d {p_1, p_2} \ge 0$:
:$\map d {p_1, p_2} = 0$
From {{Metric-space-axiom|4}}:
:$p_1 = p_2$
Theorem: Egorov's Theorem

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $D \in \Sigma$ be such that $\map \mu D < +\infty$.
Let $\sequence {f_n}_{n \mathop \in \N}, f_n: D \to \R$ be a sequence of $\Sigma$-measurable functions.
Suppose that $f_n$ converges a.e. to $f$, for some $\Sigma$-measurable function $f: D \to \R$.
Then $f_n$ converges a.u. to $f$.

Proof:
Let $\epsilon \in \R_{>0}$ be arbitrary.
By definition of convergence a.e., there is a set $E \in \Sigma$ such that $E \subseteq D$, $\map \mu E = 0$ and:
:$\ds \lim_{n \mathop \to \infty} \map {f_n} x = \map f x$
for each $x \in A$ where $A = D \setminus E$ is the set difference of $D$ with $E$.
For all $n, k \in \N$, define $A_{n, k}$ by:
:$A_{n, k} = \set {x \in A: \size {\map {f_n} x - \map f x} \ge \dfrac 1 k}$
Also, define $B_{n, k}$ by:
:$B_{n, k} = \ds \bigcup_{i \mathop = n}^\infty A_{i, k}$
Since $f_n$ converges pointwise to $f$ on $A$, it follows by definition of convergence that for each $x \in A$ and $k \in \N$:
:$\size {\map {f_i} x - \map f x} < \dfrac 1 k$
for all $i \in \N$ sufficiently large.
Thus, when $k$ is fixed, no element of $A$ belongs to $A_{n, k}$ for infinitely many $n$. 
Hence, by Definition 2 of Limit Superior of Sequence of Sets:
:$\ds \limsup_{n \mathop \to \infty} A_{n, k} = \O$
So we have:
{{begin-eqn}}
{{eqn | l = 0
      | r = \map \mu \O
      | c = Measure of Empty Set is Zero
}}
{{eqn | r = \map \mu {\limsup_{n \mathop \to \infty} A_{n, k} }
}}
{{eqn | r = \map \mu {\bigcap_{n \mathop = 0}^\infty B_{n, k} }
      | c = {{Defof|Limit Superior of Sequence of Sets}}
}}
{{eqn | r = \map \mu {\limsup_{n \mathop \to \infty} B_{n, k} }
      | c = {{Defof|Limit Superior of Sequence of Sets|index = 2}}
}}
{{eqn | r = \map \mu {\lim_{n \mathop \to \infty} B_{n, k} }
      | c = since $B_{n, k}$ is a decreasing sequence of sets
}}
{{eqn | r = \lim_{n \mathop \to \infty} \map \mu {B_{n, k} }
      | c = since $B_{n, k} \subseteq D$, $\map \mu D < \infty$ and by Continuity of Measure
}}
{{end-eqn}}
{{MissingLinks|}}
{{handwaving|last two lines}}
Thus, since $k$ was arbitrary, we can associate some $n_k \in N$ with each $k$ such that $\map \mu {B_{n_k, k} } < \dfrac \epsilon {2^{k + 1} }$.
Setting $B = \ds \bigcup_{k \mathop \in \N} B_{n_k, k}$, we have:
:$\ds \map \mu B \le \sum_{k \mathop \in \N} \map \mu { B_{n_k, k} } < \sum_{k \mathop \in \N} \frac \epsilon {2^{k + 1} } = \epsilon$
by the countable additivity of $\mu$ and by Sum of Infinite Geometric Sequence.
Also, given any $k$, we have that $x \in A \setminus B$ implies $x \notin B_{n_k, k}$, which means:
:$\size {\map {f_i} x - \map f x} < \dfrac 1 k$ 
for all $i \ge n_k$.
Since this is true for ''all'' $x \in A \setminus B$, it follows that $f_n$ converges to $f$ uniformly on $A \setminus B$.
Finally, note that $A \setminus B = D \setminus \paren {E \cup B}$, and:
:$\map \mu {E \cup B} \le \map \mu B + \map \mu E = \map \mu B + 0 < \epsilon$
Since $\epsilon$ was arbitrary, it follows that:
:$\map \mu {E \cup B} = 0$
Hence $f_n$ converges to $f$ almost uniformly.
{{qed}}
Theorem: Measure of Empty Set is Zero

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Then $\map \mu \O = 0$.
That is, $\O$ is a $\mu$-null set.

Proof:
By definition of measure, there exists at least one $E \in \Sigma$ such that $\map \mu E$ is finite.
So, suppose that $E \in \Sigma$ such that $\map \mu E$ is finite.
Let $\map \mu E = x$.
Consider the sequence $\sequence {S_n}_{n \mathop \in \N} \subseteq \Sigma$ defined as:
:$S_n = \begin {cases} E & : n = 1 \\ \O & : n > 1 \end {cases}$
Then:
:$\ds \bigcup_{n \mathop = 1}^\infty S_n = E$
Hence:
{{begin-eqn}}
{{eqn | l = \map \mu E
      | r = x
}}
{{eqn | ll= \leadsto
      | l = \mu \paren {\bigcup_{n \mathop = 1}^\infty S_n}
      | r = x
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 1}^\infty \map \mu {S_n}
      | r = x
      | c = Property $(2)$
}}
{{eqn | ll= \leadsto
      | l = \map \mu E + \sum_{n \mathop = 2}^\infty \map \mu \O
      | r = x
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 2}^\infty \map \mu \O
      | r = 0
}}
{{end-eqn}}
It follows directly that $\map \mu \O = 0$.
{{qed}}
Theorem: Convergence a.u. Implies Convergence a.e.

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f_n: D \to \R$ be a sequence of $\Sigma$-measurable functions for $D \in \Sigma$.
Let $f_n$ converge a.u. to a function $f$ on $D$.
Then $f_n$ converges a.e. to $f$.

Proof:
Assume $f_n$ converge a.u. to $f$ on $D$.
Then for each $\epsilon > 0$ there is a $B_\epsilon \subseteq D$ with $\map \mu {B_\epsilon} < \epsilon$ outside of which $f_n$ converges uniformly to $f$.
Thus, $f_n$ converges pointwise to $f$ outside of each $B_\epsilon$.
Next, define $\ds B \equiv \bigcap_{n \mathop \in \N} B_{\frac 1 n}$.
First, $B \in \Sigma$ since $\Sigma$ is a sigma-algebra, so that $\map \mu B$ is defined.
Second, note that since the measure is monotonic:
:$\forall n \in \N: \map \mu B \le \map \mu {B_{\frac 1 n} } < \dfrac 1 n$
Hence:
:$\map \mu B = 0$
But $x \in D - B$ only if $x \notin B_{\frac 1 k}$ for some $k \in \N$.
So by the above:
:$\map {f_n} x \to \map f x$
It follows by definition that $f_n$ converges a.e. to $f$.
{{qed}}
Theorem: Existence of Solution of 2nd Order Linear ODE

Let $\map P x$, $\map Q x$ and $\map R x$ be continuous real functions on a closed interval $I = \closedint a b$.
Let $x_0 \in I$, and let $y_0 \in \R$ and $y_0' \in \R$ be arbitrary.
Then the initial value problem:
:$\ds \frac {\d^2 y}{\d x^2} + \map P x \frac {\d y}{\d x} + \map Q x y = \map R x, \map y {x_0} = y_0, \map {y'} {x_0} = y_0'$
has one and only one solution $y = \map y x$ on the interval $I$.

Proof:
Let us introduce the variable $z = \dfrac {\d y}{\d x}$.
Then the initial ODE can be written:
:<nowiki>$\begin{cases}
\dfrac {\d y}{\d x} = z & : \map y {x_0} = y_0 \\
& \\
\dfrac {\d z}{\d x} = - \map P x z - \map Q x y + \map R x & : \map z {x_0} = y_0'
\end{cases}$</nowiki>
The converse is also true.
The result follows from Existence of Solution to System of First Order ODEs.
{{qed}}
Category:Differential Equations
bjail7u1i0hff59t2sjfr111fsto1ch
Theorem: Existence of Solution to System of First Order ODEs

Consider the system of initial value problems:
:<nowiki>$\begin{cases}
\dfrac {\d y} {\d x} = \map f {x, y, z} & : \map y {x_0} = y_0 \\
& \\
\dfrac {\d z} {\d x} = \map g {x, y, z} & : \map z {x_0} = z_0 \\
\end{cases}$</nowiki>
where $\map f {x, y, z}$ and $\map g {x, y, z}$ are continuous real functions in some region of space $x y z$ that contains the point $\tuple {x_0, y_0, z_0}$.
Then this system of equations has a unique solution which exists on some interval $\size {x - x_0} \le h$.

Proof:
{{proof wanted|Needs more work so as to state the problem more precisely.}}
Category:Differential Equations
dufy90jx3cpjawt9yrvf4fd6m3hux5d
Theorem: Cartesian Metric is Rotation Invariant

The cartesian metric does not change under rotation.

Proof:
Let the cartesian metric be $\delta_{ij} = \innerprod {e_i} {e_j}$.
Also, let $\delta_{ij}'$ be the metric of the coordinate system of $\delta_{ij}$ rotated by a rotation matrix $A$.
Then, $\delta_{ij}' = \innerprod {A e_i} {A e_j}$.
$\innerprod {A x} y = \innerprod x {A^T y}$, see Factor Matrix in the Inner Product, so
$\delta_{ij}' = \innerprod {A e_i} {A e_j} = \innerprod {e_i} {A^T A e_j}$.
For rotation matrices, we have $A^T = A^{-1}$, so $\delta_{ij}'$ reduces to:
:$\delta_{ij}' = \innerprod {e_i} {A^T A e_j} = \innerprod {e_i} {A^{-1} A e_j} = \innerprod {e_i} {I e_j} = \innerprod {e_i} {e_j}$
where $I$ is the unit matrix.
Thus:
:$\delta_{ij}' = \delta_{ij}$
The result follows.
{{Qed}}
{{MissingLinks}}
{{ExtractTheorem}}
This proof holds for any finite-dimensional Euclidean space.
Category:Metric Spaces
feb6xzuqzj5ikks963xjefyh3mjnoei
Theorem: Little Bézout Theorem

Let $\map {P_n} x$ be a polynomial of degree $n$ in $x$.
Let $a$ be a constant.
Then the remainder of $\map {P_n} x$ when divided by $x - a$ is equal to $\map {P_n} a$.

Proof:
By the process of Polynomial Long Division, we can express $\map {P_n} x$ as:
:$(1): \quad \map {P_n} x = \paren {x - a} \map {Q_{n - 1} } x + R$
where:
:$\map {Q_{n - 1} } x$ is a polynomial in $x$ of degree $n - 1$
:$R$ is a polynomial in $x$ of degree no greater than $0$; that is, a constant.
It follows that, by setting $x = a$ in $(1)$, we get $\map {P_n} a = R$.
Hence the result.
{{qed}}
Theorem: Thales' Theorem

Let $A$ and $B$ be two points on opposite ends of the diameter of a circle.
Let $C$ be another point on the circle such that $C \ne A, B$.
Then the lines $AC$ and $BC$ are perpendicular to each other.
:400px

Proof:
:400px
Let $O$ be the center of the circle, and define the vectors:
:$\mathbf u = \overrightarrow{OC}$
:$\mathbf v = \overrightarrow{OB}$
:$\mathbf w = \overrightarrow{OA}$
Thus:
:$\overrightarrow{AC} = \mathbf u - \mathbf w$
:$\overrightarrow{BC} = \mathbf u - \mathbf v$
Then:
{{begin-eqn}}
{{eqn | o =
      | r = \overrightarrow{AC} \cdot \overrightarrow{BC}
      | c = where $\cdot$ is the dot product
}}
{{eqn | r = \paren {\mathbf u - \mathbf w} \cdot \paren {\mathbf u - \mathbf v}
      | c = from above
}}
{{eqn | r = \paren {\mathbf u + \mathbf v} \cdot \paren {\mathbf u - \mathbf v}
      | c = Since $A$ is directly opposite $B$ in the circle, $\mathbf w = - \mathbf v$
}}
{{eqn | r = \mathbf u \cdot \mathbf u - \mathbf u \cdot \mathbf v + \mathbf v \cdot \mathbf u - \mathbf v \cdot \mathbf v
      | c = Dot Product Distributes over Addition
}}
{{eqn | r = \mathbf u \cdot \mathbf u - \mathbf u \cdot \mathbf v + \mathbf u \cdot \mathbf v - \mathbf v \cdot \mathbf v
      | c = Dot Product Operator is Commutative
}}
{{eqn | r = \norm {\mathbf u}^2 - \mathbf u \cdot \mathbf v + \mathbf u \cdot \mathbf v - \norm {\mathbf v}^2
      | c = Dot Product of Vector with Itself
}}
{{eqn | r = \norm {\mathbf u}^2 - \norm {\mathbf v}^2
      | c = simplification
}}
{{eqn | r = \norm {\mathbf u}^2 - \norm {\mathbf u}^2
      | c = as $\norm {\mathbf u} = \norm {\mathbf v}$
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
From Non-Zero Vectors are Orthogonal iff Perpendicular, it follows that $AC$ and $BC$ are perpendicular to each other.
{{Qed}}
Theorem: Thales' Theorem

Let $A$ and $B$ be two points on opposite ends of the diameter of a circle.
Let $C$ be another point on the circle such that $C \ne A, B$.
Then the lines $AC$ and $BC$ are perpendicular to each other.
:400px

Proof:
Let $O$ be the center of $ACB$.
From the Inscribed Angle Theorem, $\angle AOB = 2 \angle ACB$.
Then we have that $\angle AOB$ is a straight angle.
Hence the result.
{{qed}}