avewright/proofwiki-math huggingface dataset:
Theorem: Uniform Product of Continuous Functions is Continuous

Let $X$ be a metric space.
Let $\struct {\mathbb K, \norm{\,\cdot\,}}$ be a valued field.
Let $\sequence {f_n}$ be a sequence of bounded continuous mappings $f_n: X \to \mathbb K$.
Let the product $\ds \prod_{n \mathop = 1}^\infty f_n$ converge uniformly to $f$.
Then $f$ is continuous.

Proof:
Let $n_0 \in \N$ be such that the sequence of partial products of $\ds \prod_{n \mathop = n_0}^\infty f_n$ converges uniformly.
By the Uniform Limit Theorem, $\ds \prod_{n \mathop = n_0}^\infty f_n$ is continuous.
Because $f_1, \ldots, f_{n_0 - 1}$ are continuous, so is $\ds \prod_{n \mathop = 1}^\infty f_n$.
{{qed}}
Theorem: Logarithm of Infinite Product of Complex Functions

Let $X$ be a weakly locally compact topological space.
Let $\sequence {f_n}$ be a sequence of everywhere nonzero continuous mappings $f_n: X \to \C$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|The product $\ds \prod_{n \mathop {{=}} 1}^\infty f_n$ converges locally uniformly to $f$}}
{{item|(2):|The series $\ds \sum_{n \mathop {{=}} 1}^\infty \ln f_n$ converges locally uniformly to $\ln f + 2 k \pi i$ for some mapping $k: K\to\Z$}}
{{end-itemize}}

Proof:
=== 1 implies 2 ===
It suffices to show that:
{{begin-itemize}}
{{item|(3):|$\ds \sum_{n \mathop {{=}} 1}^\infty \map \Re {\ln f_n} {{=}} \map \Re {\ln f}$ locally uniformly}}
{{item|(4):|$\ds \sum_{n \mathop {{=}} 1}^\infty \map \Im {\ln f_n} {{=}} \map \Im {\ln f} + 2 k \pi$ locally uniformly for some $k: K \to \Z$}}
{{end-itemize}}
Theorem: Logarithmic Derivative of Infinite Product of Analytic Functions

Let $D \subseteq \C$ be open.
Let $\sequence {f_n}$ be a sequence of analytic functions $f_n: D \to \C$.
Let none of the $f_n$ be identically zero on any open subset of $D$.
Let the product $\ds \prod_{n \mathop = 1}^\infty f_n$ converge locally uniformly to $f$.
Then:
:$\ds \dfrac {f'} f = \sum_{n \mathop = 1}^\infty \frac {f_n'} {f_n}$
and the series converges locally uniformly in $D \setminus \set {z \in D : \map f z = 0}$.

Proof:
{{questionable|this needs a stronger version of {{Corollary|Logarithm of Infinite Product of Complex Functions}}, where the logarithms are analytic}}
Note that by Infinite Product of Analytic Functions is Analytic, $f$ is analytic.
Let $z_0 \in D$ with $\map f {z_0} \ne 0$.
By {{Corollary|Logarithm of Infinite Product of Complex Functions}}, there exist $n_0 \in \N$, $k \in \Z$ and a open neighborhood $U$ of $z_0$ such that:
:$\map {f_n} z \ne 0$ for $n \ge n_0$ and $z \in U$
:The series $\ds \sum_{n \mathop = n_0}^\infty \log f_n$ converges uniformly on $U$ to $\log g + 2 k \pi i$, where $g = \ds \prod_{n \mathop = n_0}^\infty f_n$.
We have, for $z \in U$:
{{begin-eqn}}
{{eqn | l = \frac {f'} f
      | r = \frac {\paren {f_1 \cdots f_{n_0 - 1} \cdot g}'} {f_1 \cdots f_{n_0 - 1} \cdot g}
      | c = 
}}
{{eqn | l = 
      | r = \frac {f_1'} {f_1} + \cdots + \frac {f_{n_0 - 1}'} {f_{n_0 - 1} } + \frac {g'} g
      | c = Logarithmic Derivative of Product of Analytic Functions
}}
{{end-eqn}}
and
{{begin-eqn}}
{{eqn | l = \frac {g'} g
      | r = \paren {\log g}'
      | c = Logarithmic Derivative is Derivative of Logarithm
}}
{{eqn | r = \sum_{n \mathop = n_0}^\infty \paren {\log f_n}' - \paren {2 k \pi i}'
      | c = Derivative of Uniform Limit of Analytic Functions
}}
{{eqn | r = \sum_{n \mathop = n_0}^\infty \frac {f_n'} {f_n}
      | c = Logarithmic Derivative is Derivative of Logarithm
}}
{{end-eqn}}
and the series converges locally uniformly on $U$.
Thus $\ds \frac {f'} f = \sum_{n \mathop = 1}^\infty \frac {f_n'} {f_n}$ converges locally uniformly on $U \setminus \set {z \in U : \map f z = 0}$.
{{qed}}
Theorem: Galois Connection implies Upper Adjoint is Surjection iff Lower Adjoint is Injection

Let $L = \struct {S, \preceq}$ and $R = \struct {T, \precsim}$ be ordered sets.
Let $g: S \to T$ and $d: T \to S$ be mappings such that $\struct {g, d}$ is a Galois connection.
Then $g$ is a surjection {{iff}} $d$ is an injection.

Proof:
=== Sufficient Condition ===
Assume that
:$d$ is a surjection.
By Upper Adjoint of Galois Connection is Surjection implies Lower Adjoint at Element is Minimum of Preimage of Singleton of Element
:$\forall t \in T: \map d t = \min \set {g^{-1} \sqbrk {\set t} }$
By Lower Adjoint at Element is Minimum of Preimage of Singleton of Element implies Composition is Identity:
:$g \circ d = I_T$
Thus by Injection iff Left Inverse:
:$d$ is an injection.
{{qed|lemma}}
Theorem: Derivative of Uniform Limit of Analytic Functions

Let $U$ be an open subset of $\C$.
Let $\sequence {f_n}_{n \mathop \in \N}$ be a sequence of analytic functions $f_n : U \to \C$.
Let $\sequence {f_n}$ converge locally uniformly to $f$ on $U$.
Let $f'$ denote the derivative of $f$.
Then the sequence $\sequence { {f_n}'}_{n \mathop \in \N}$ converges locally uniformly to $f'$.

Proof:
Let $a \in U$.
By definition of locally uniform convergence, there exists an open disk $\map {D_{2 r} } a \subseteq U$ such that $f_n$ converges uniformly to $f$ on $\map {D_{2 r} } a$.
That is:
:$\ds (1): \quad \lim_{n \mathop \to \infty} \sup_{z \mathop \in \map {D_{2 r} } a} \cmod {\map {f_n} z - \map f z} = 0$ 
We shall show that:
:$\ds \lim_{n \mathop \to \infty} \sup_{w \mathop \in \map {D_r} a} \cmod {\map {f'_n} w - \map {f'} w} = 0$
Let $w \in \map {D_r} a$.
By Triangle Inequality for Complex Numbers:
:$(2): \quad \map {D_r} w \subseteq \map {D_{2 r} } a \subseteq U$
Thus by Cauchy's Integral Formula for Derivatives:
{{begin-eqn}}
{{eqn | l = \map {f'_n} w
      | r = \frac 1 {2 \pi i} \oint_{\partial \map {D_r} w} \frac {\map {f_n} z} {\paren {z - w}^2} \rd z
}}
{{eqn-intertext|and:}}
{{eqn | l = \map {f'} w
      | r = \frac 1 {2 \pi i} \oint_{\partial \map {D_r} w} \frac {\map f z} {\paren {z - w}^2} \rd z
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \cmod {\map {f'_n} w - \map {f'} w}
      | r = \frac 1 {2 \pi} \cmod {\oint_{\partial \map {D_r} w} \frac {\map {f_n} z - \map f z} {\paren {z - w}^2} \rd z}
}}
{{eqn | o = \le
      | r = \frac {2 \pi r} {2 \pi} \sup_{z \mathop \in \partial \map {D_r} w} \frac {\cmod {\map {f_n} z - \map f z} } {r^2}
      | c = Estimation Lemma for Contour Integrals
}}
{{eqn | r = \frac 1 r \sup_{z \mathop \in \partial \map {D_r} w} \cmod {\map {f_n} z - \map f z}
}}
{{eqn | o = \le
      | r = \frac 1 r \sup_{z \mathop \in \map {D_{2 r} } a} \cmod {\map {f_n} z - \map f z}
      | c = by $(2)$
}}
{{end-eqn}}
Since $w \in \map {D_r} a$ was arbitrary, we have:
{{begin-eqn}}
{{eqn | l = \sup_{w \mathop \in \map {D_r} a} \cmod {\map {f'_n} w - \map {f'} w}
      | o = \le
      | r = \frac 1 r \sup_{z \mathop \in \map {D_{2 r} } a} \cmod {\map {f_n} z - \map f z}
}}
{{eqn | o = \to
      | r = 0
      | c = as $n \to \infty$ by $\paren 1$
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Infinite Product of Analytic Functions

Let $D \subset \C$ be open.
Let $\sequence {f_n}$ be a sequence of analytic functions $f_n: D \to \C$.
Let the product $\ds \prod_{n \mathop = 1}^\infty f_n$ converge locally uniformly to $f$.
Then:
:$\ds f' = \sum_{n \mathop = 1}^\infty f_n' \cdot \prod_{\substack {k \mathop = 1 \\ k \mathop \ne n} }^\infty f_k$
and the series converges locally uniformly in $D$.
{{explain|Exactly what is meant by "the series"? Specify it.}}

Proof:
By Infinite Product of Analytic Functions is Analytic, $f$ is analytic.
We may suppose none of the $f_n$ is identically zero on any open subset of $D$.
Let $E = D \setminus \set {z \in D: \map f z = 0}$.
By Logarithmic Derivative of Infinite Product of Analytic Functions, $\ds \frac {f'} f = \sum_{n \mathop = 1}^\infty \frac {f_n'} {f_n}$ converges locally uniformly in $E$.
By Linear Combination of Convergent Series:
:$\ds f' = \sum_{n \mathop = 1}^\infty f_n' \cdot \prod_{\substack {k \mathop = 1 \\ k \mathop \ne n}}^\infty f_k$ on $E$
By Uniformly Convergent Sequence Multiplied with Function, the series converges locally uniformly in $E$.
By Uniformly Convergent Sequence on Dense Subset, the series converges locally uniformly in $D$.
{{questionable|The above does not work. All the above link does is show that the series is uniformly convergent on $D$, and not locally uniformly convergent.}}
Let $g$ denote its limit.
By Uniform Limit of Analytic Functions is Analytic, $g$ is analytic in $D$.
By Uniqueness of Analytic Continuation, $f' = g$.
{{qed}}
Theorem: Uniformly Convergent Sequence Multiplied with Function

Let $X$ be a set.
Let $V$ be a normed vector space over $\mathbb K$.
Let $\sequence {f_n}$ be a sequence of mappings $f_n: X \to V$.
Let $\sequence {f_n}$ be uniformly convergent.
Let $g: X \to \mathbb K$ be bounded.
Then $\sequence {f_n g}$ is uniformly convergent.

Proof:
Denote $\norm {\, \cdot \,}$ as the norm on $V$.
Let $\epsilon > 0$.
By boundedness of $g$:
:$\exists M \in \R: \forall x \in X: \norm {\map g x} < M$
By uniformly convergence of $\sequence {f_n}$:
:$\exists f: X \to \mathbb K: \exists N \in \R: \forall x \in X: \norm {\map {f_n} x - \map f x} < \dfrac \epsilon M$
Pick any $x \in X$. Then:
{{begin-eqn}}
{{eqn | l = \norm {\map {f_n} x \map g x - \map f x \map g x}
      | r = \norm {\map g x \paren {\map {f_n} x - \map f x} }
}}
{{eqn | r = \norm {\map g x} \norm {\map {f_n} x - \map f x} 
      | c = {{Norm-axiom-mult|2}}
}}
{{eqn | o = <
      | r = M \cdot \dfrac \epsilon M
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
As the choice of $x$ is arbitrary, $\sequence {f_n g}$ uniformly converges to $\sequence {f g}$.
{{qed}}
Theorem: Logarithmic Derivative of Product of Analytic Functions

Let $D \subset \C$ be open.
Let $f, g: D \to \C$ be analytic.
Let $f g$ be their pointwise product.
Let $z \in D$ with $\map f z \ne 0 \ne \map g z$.
Then:
:$\dfrac {\map {\paren {f g}' } z} {\map {\paren {f g} } z} = \dfrac{\map {f'} z} {\map f z} + \dfrac {\map {g'} z} {\map g z}$

Proof:
Follows directly from Product Rule for Complex Derivatives.
{{qed}}
Theorem: Uniformly Convergent Sequence on Dense Subset

Let $X$ be a metric space.
Let $Y \subset X$ be dense.
Let $V$ be a Banach space.
Let $\sequence {f_n}$ be a sequence of continuous mappings $f_n : X\to V$.
Let $\sequence {f_n}$ be uniformly convergent on $Y$.
Then $\sequence {f_n}$ is uniformly convergent on $X$.

Proof:
Let $\epsilon>0$.
Let $N \in\N$ be such that $\norm {f_n - f_m} < \epsilon$ for $n, m > N$ on $Y$.
Let $x \in X$.
Then there exists a sequence $\sequence {y_n} \in Y$ with $y_n \to x$.
By continuity:
:$\norm {\map {f_n} x - \map {f_m} x} \le \epsilon$
Because $V$ is complete, $\sequence {f_n}$ is uniformly convergent on $X$.
{{qed}}
Category:Uniform Convergence
4admzzw3uwxw37uthv76co97u9dce7t
Theorem: Factors in Uniformly Convergent Product Converge Uniformly to One

Let $X$ be a set.
Let $\struct {\mathbb K, \norm {\, \cdot \,} }$ be a valued field.
Let $\sequence {f_n}$ be a sequence of bounded mappings $f_n: X \to \mathbb K$.
Let the infinite product $\ds \prod_{n \mathop = 1}^\infty f_n$ converge uniformly on $X$.
Then $f_n$ converges uniformly to $1$.

Proof:
Follows directly from Uniformly Convergent Product Satisfies Uniform Cauchy Criterion.
{{qed}}
Theorem: Quintuplets of Consecutive Integers which are not Divisor Sum Values

The elements of the following $5$-tuples of consecutive integers have the property that they are not values of the divisor sum function $\map {\sigma_1} n$ for any $n$:
:$\tuple {49, 50, 51, 52, 53}$
:$\tuple {115, 116, 117, 118, 119}$
:$\tuple {145, 146, 147, 148, 149}$

Proof:
{{ProofWanted|Can be done by listing all $\sigma_1$s less than the numbers concerned, which is tedious}}
Theorem: Positive Integers which are not Divisor Sum Values

The following positive integers are not the values of the divisor sum function $\map {\sigma_1} n$ for any $n$:
:$2, 5, 9, 10, 11, 16, 17, 19, 21, 22, 23, 25, 26, 27, 29, 33, 34, 35, 37, 41, 43, 45, 46, 47, 49, 50, 51, 52, 53, 55, 58, 59, 61, 64, 65, \ldots$
{{OEIS|A007369}}

Proof:
{{ProofWanted|By exhaustion}}
Category:Divisor Sum Function
7od12pz6xwzbv54kx4p04gnwv37ng0u
Theorem: Uniformly Absolutely Convergent Product is Uniformly Convergent

Let $X$ be a set.
Let $\struct {\mathbb K, \norm {\, \cdot \,} }$ be a valued field.
Let $\mathbb K$ be complete.
Let $\sequence {f_n}$ be a sequence of bounded mappings $f_n: X \to \mathbb K$.
Let the infinite product $\ds \prod_{n \mathop = 1}^\infty f_n$ converge uniformly absolutely on $X$.
Then it converges uniformly.

Proof:
{{ProofWanted}}
Category:Uniform Convergence
Category:Infinite Products
enywz0kpgqttb7mm01wfxavpe4axpw7
Theorem: Zeroes of Infinite Product of Analytic Functions

Let $D \subset \C$ be an open connected set.
Let $\sequence {f_n}$ be a sequence of analytic functions $f_n: D \to \C$.
Let $\ds \prod_{n \mathop = 1}^\infty f_n$ converge locally uniformly to $f$.
Let $z_0\in D$.
Then:
:$(1): \quad$ $f$ is identically zero {{iff}} some $f_n$ is identically zero 
:$(2): \quad$ $\map {f_n} {z_0} = 0$ for finitely many $n \in \N$
:$(3): \quad$ If $f$ is not identically zero, $\map {\operatorname {mult}_{z_0} } f = \ds \sum_{n \mathop = 1}^\infty \map {\operatorname {mult}_{z_0} } {f_n}$
where $\operatorname {mult}$ denotes multiplicity.

Proof:
Note that by Infinite Product of Analytic Functions is Analytic, $f$ is analytic.
Let $n_0 \in \N$ and $U\subset D$ an open neighborhood of $z_0$ such that $\ds \prod_{n \mathop = n_0}^\infty \map {f_n} z \ne 0$ for $z\in U$.
Let $f$ be identically zero on $U$.
Then $\ds \prod_{n \mathop = 1}^{n_0 - 1} \map {f_n} z$ is identically zero on $U$.
Then some $f_k$ with $k < n_0$ is identically zero on $U$.
By Uniqueness of Analytic Continuation, $f_k$ is identically zero on $D$.
Now let $f$ be not identically zero on $U$.
We have:
{{begin-eqn}}
{{eqn | l = \map {\operatorname {mult}_{z_0} } f
      | r = \sum_{n \mathop = 1}^{n_0} \map {\operatorname {mult}_{z_0} } {f_n} + \map {\operatorname {mult}_{z_0} } {\prod_{n \mathop = n_0}^\infty f_n}
      | c = Multiplicity of Product of Analytic Functions
}}
{{eqn | r = \sum_{n \mathop = 1}^{n_0} \map {\operatorname {mult}_{z_0} } {f_n}
      | c = $\ds \prod_{n \mathop = n_0}^\infty \map {f_n} {z_0} \ne 0$
}}
{{eqn | l = 
      | r = \sum_{n \mathop = 1}^\infty \map {\operatorname {mult}_{z_0} } {f_n}
      | c =  $\map {f_n} {z_0} \ne 0$ for $n \ge n_0$
}}
{{end-eqn}}
{{qed}}
Theorem: Infinite Product of Analytic Functions is Analytic

Let $D \subset \C$ be an open set.
Let $\sequence {f_n}$ be a sequence of analytic functions $f_n: D \to \C$.
Let $\ds \prod_{n \mathop = 1}^\infty f_n$ converge locally uniformly to $f$.
Then $f$ is analytic.

Proof:
Follows directly from:
:Partial Products of Uniformly Convergent Product Converge Uniformly
:Uniform Limit of Analytic Functions is Analytic
{{qed}}
Theorem: Sum of 2 Squares in 2 Distinct Ways

Let $m, n \in \Z_{>0}$ be distinct positive integers that can be expressed as the sum of two distinct square numbers.
Then $m n$ can be expressed as the sum of two square numbers in at least two distinct ways.

Proof:
Let:
:$m = a^2 + b^2$
:$n = c^2 + d^2$
Then:
{{begin-eqn}}
{{eqn | l = m n
      | r = \paren {a^2 + b^2} \paren {c^2 + d^2}
      | c = 
}}
{{eqn | r = \paren {a c + b d}^2 + \paren {a d - b c}^2
      | c = Brahmagupta-Fibonacci Identity
}}
{{eqn | r = \paren {a c - b d}^2 + \paren {a d + b c}^2
      | c = {{Corollary|Brahmagupta-Fibonacci Identity}}
}}
{{end-eqn}}
It remains to be shown that if $a \ne b$ and $c \ne d$, then the four numbers:
:$a c + b d, a d - b c, a c - b d, a d + b c$
are distinct.
Because $a, b, c, d > 0$, we have:
:$a c + b d \ne a c - b d$
:$a d + b c \ne a d - b c$
We also have:
{{begin-eqn}}
{{eqn | l = a c \pm b d
      | r = a d \pm b c
}}
{{eqn | ll= \leadstoandfrom
      | l = a c \mp b c - a d \pm b d
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = c \paren {a \mp b} - d \paren {a \mp b}
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {a \mp b} \paren {c \mp d}
      | r = 0
}}
{{end-eqn}}
Thus $a \ne b$ and $c \ne d$ implies $a c \pm b d \ne a d \pm b c$.
The case for $a c \pm b d \ne a d \mp b c$ is similar.
{{qed}}
Theorem: Bounds for Finite Product of Real Numbers

Let $a_1, a_2, \ldots, a_n$ be positive real numbers.
Then:
:$\ds \sum_{k \mathop = 1}^n a_k \le \prod_{k \mathop = 1}^n \paren {1 + a_k} \le \map \exp {\sum_{k \mathop = 1}^n a_k}$

Proof:
=== Lower bound ===
Follows by expanding.
{{qed|lemma}}
Theorem: Bounds for Complex Exponential

Let $\exp$ denote the complex exponential.
Let $z \in \C$ with $\cmod z \le \dfrac 1 2$.
Then
:$\dfrac 1 2 \cmod z \le \cmod {\exp z - 1} \le \dfrac 3 2 \cmod z$

Proof:
By definition of complex exponential:
:$\exp z = \ds \sum_{n \mathop = 1}^\infty \frac {z^n} {n!}$
Thus
{{begin-eqn}}
{{eqn  | l = \cmod {\exp z - 1 - z}
       | r = \cmod {\sum_{n \mathop = 2}^\infty \frac {z^n} {n!} }
       | c = Linear Combination of Convergent Series
}}
{{eqn  | o = \le
       | r = \sum_{n \mathop = 2}^\infty \cmod {\frac {z^n} {n!} }
       | c = Triangle Inequality for Series
}}
{{eqn  | o = \le
       | r = \sum_{n \mathop = 2}^\infty \frac {\cmod z^n} 2
       | c = as $n \ge 2$
}}
{{eqn  | o = =
       | r = \frac {\cmod z^2 / 2} {1 - \cmod z}
       | c = Sum of Infinite Geometric Sequence
}}
{{eqn  | o = \le
       | r = \frac 1 2 \cmod z
       | c = as $\cmod z \le \dfrac 1 2$
}}
{{end-eqn}}
By the Triangle Inequality:
:$\dfrac 1 2 \cmod z \le \cmod {\exp z - 1} \le \dfrac 3 2 \cmod z$
{{qed}}
Theorem: Sum of 2 Squares in 2 Distinct Ways/Examples/50

$50$ is the smallest positive integer which can be expressed as the sum of two square numbers in two distinct ways:
{{begin-eqn}}
{{eqn | l = 50
      | r = 5^2 + 5^2
}}
{{eqn | r = 7^2 + 1^2
}}
{{end-eqn}}

Proof:
The smallest two positive integers which can be expressed as the sum of two distinct square numbers are:
{{begin-eqn}}
{{eqn | l = 5
      | r = 1^2 + 2^2
}}
{{eqn | l = 10
      | r = 1^2 + 3^2
}}
{{end-eqn}}
We have that:
:$50 = 5 \times 10$
Thus:
{{begin-eqn}}
{{eqn | r = \paren {1^2 + 2^2} \paren {1^2 + 3^2}
      | c = 
}}
{{eqn | r = \paren {1 \times 1 + 2 \times 3}^2 + \paren {1 \times 3 - 2 \times 1}^2
      | c = Brahmagupta-Fibonacci Identity
}}
{{eqn | r = \paren {1 + 6}^2 + \paren {3 - 2}^2
      | c = 
}}
{{eqn | r = 7^2 + 1^2
      | c = 
}}
{{eqn | r = 49 + 1
      | c = 
}}
{{eqn | r = 50
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | r = \paren {1^2 + 2^2} \paren {1^2 + 3^2}
      | c = 
}}
{{eqn | r = \paren {1 \times 1 - 2 \times 3}^2 + \paren {1 \times 3 + 2 \times 1}^2
      | c = {{Corollary|Brahmagupta-Fibonacci Identity}}
}}
{{eqn | r = \paren {1 - 6}^2 + \paren {3 + 2}^2
      | c = 
}}
{{eqn | r = \paren {6 - 1}^2 + \paren {3 + 2}^2
      | c = 
}}
{{eqn | r = 5^2 + 5^2
      | c = 
}}
{{eqn | r = 25 + 25
      | c = 
}}
{{eqn | r = 50
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of 2 Squares in 2 Distinct Ways/Examples/65

$65$ can be expressed as the sum of two square numbers in two distinct ways:
{{begin-eqn}}
{{eqn | l = 65
      | r = 8^2 + 1^2
}}
{{eqn | r = 7^2 + 4^2
}}
{{end-eqn}}

Proof:
We have that:
:$65 = 5 \times 13$
Both $5$ and $13$ can be expressed as the sum of two distinct square numbers:
{{begin-eqn}}
{{eqn | l = 5
      | r = 1^2 + 2^2
}}
{{eqn | l = 13
      | r = 2^2 + 3^2
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | r = \paren {1^2 + 2^2} \paren {2^2 + 3^2}
      | c = 
}}
{{eqn | r = \paren {1 \times 2 + 2 \times 3}^2 + \paren {1 \times 3 - 2 \times 2}^2
      | c = Brahmagupta-Fibonacci Identity
}}
{{eqn | r = \paren {2 + 6}^2 + \paren {3 - 4}^2
      | c = 
}}
{{eqn | r = \paren {2 + 6}^2 + \paren {4 - 3}^2
      | c = 
}}
{{eqn | r = 8^2 + 1^2
      | c = 
}}
{{eqn | r = 64 + 1
      | c = 
}}
{{eqn | r = 65
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | r = \paren {1^2 + 2^2} \paren {2^2 + 3^2}
      | c = 
}}
{{eqn | r = \paren {1 \times 2 - 2 \times 3}^2 + \paren {1 \times 3 + 2 \times 2}^2
      | c = {{Corollary|Brahmagupta-Fibonacci Identity}}
}}
{{eqn | r = \paren {2 - 6}^2 + \paren {3 + 4}^2
      | c = 
}}
{{eqn | r = \paren {6 - 2}^2 + \paren {3 + 4}^2
      | c = 
}}
{{eqn | r = 4^2 + 7^2
      | c = 
}}
{{eqn | r = 16 + 49
      | c = 
}}
{{eqn | r = 65
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Continuous Implies Locally Bounded

Let $X$ be a topological space.
Let $M$ be a metric space.
Let $f: X \to M$ be continuous.
Then $f$ is locally bounded.

Proof:
Let $x \in X$.
Let $U = \map {f^{-1} } {\map B {\map f x, 1} }$.
{{explain|$\map B {\map f x, 1}$}}
By continuity, $U$ is a neighborhood of $x$.
Because $\map f U \subset \map B {\map f x, 1}$, $f$ is bounded on $U$.
Thus $f$ is locally bounded.
{{qed}}
Category:Boundedness
032x9q3dgsc1qdh2h7vr31bk99m0l6f
Theorem: Lower Adjoint at Element is Minimum of Preimage of Singleton of Element implies Composition is Identity

Let $L = \struct {S, \preceq}, R = \struct {T, \precsim}$ be ordered sets.
Let $g: S \to T, d: T \to S$ be mappings such that
:$\forall t \in T: \map d t = \min \set {g^{-1} \sqbrk {\set t} }$
Then $g \circ d = I_T$
where $I_T$ denotes the identity mapping of $T$.

Proof:
Let $t \in T$.
By assumption:
:$\map d t = \min \set {g^{-1} \sqbrk {\set t} }$
By definition of min operation:
:$\map d t = \map \inf {g^{-1} \sqbrk {\set t} }$ and $\map d t \in g^{-1} \sqbrk {\set t}$
By definition of image of set:
:$\map g {\map d t} \in \set t$
By definition of singleton:
:$\map g {\map d t} = t$
Thus by definition of composition of mappings:
:$\map {\paren {g \circ d} } t = t$
{{qed}}
Theorem: Bounds for Weierstrass Elementary Factors

Let $E_p: \C \to \C$ denote the $p$th Weierstrass elementary factor:
$\quad\map {E_p} z = \begin {cases} 1 - z & : p = 0 \\ 
\paren {1 - z} \map \exp {z + \dfrac {z^2} 2 + \cdots + \dfrac {z^p} p} & : \text {otherwise} \end {cases}$
Let $z \in \C$.

Proof:
=== Proof of some bound ===
Let $\cmod z \le \dfrac 1 2$.
We may assume $p \ge 1$.
We have:
:$\map {E_p} z = \map \exp {\map \log {1 - z} + \ds \sum_{k \mathop = 1}^p \frac {z^k} k}$
Then:
{{begin-eqn}}
{{eqn | l = \cmod {\map \log {1 - z} + \sum_{k \mathop = 1}^p \frac {z^k} k}
      | r = \cmod {-\sum_{k \mathop = p + 1}^\infty \frac{z^k} k}
      | c = Series Expansion of Complex Logarithm
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = p + 1}^\infty \frac {\cmod z^k} k
      | c = Triangle Inequality for Series
}}
{{eqn | o = \le
      | r = \sum_{k \mathop = p + 1}^\infty \cmod z^k
      | c = because $k \ge 1$
}}
{{eqn | r = \frac {\cmod z^{p + 1} } {1 - \cmod z}
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | o = \le
      | r = 2 \cmod z^{p + 1}
      | c = because $\cmod z \le \dfrac 1 2$
}}
{{end-eqn}}
Because $p \ge 1$:
:$2 \cmod z^{p + 1} \le \dfrac 1 2$
By Bounds for Complex Exponential:
:$\cmod {\map {E_p} z - 1} \le 3 \cmod z^{p + 1}$
{{qed}}