avewright/proofwiki-math huggingface dataset:
Theorem: Standard Continuous Uniform Distribution in terms of Exponential Distribution

Let $X$ and $Y$ be independent random variables.
Let $\beta$ be a strictly positive real number.
Let $X$ and $Y$ be random samples from the exponential distribution with parameter $\beta$. 
Then:
:$\dfrac X {X + Y} \sim \operatorname U \openint 0 1$
where $\operatorname U \openint 0 1$ is the uniform distribution on $\openint 0 1$.

Proof:
Note that the support of $\operatorname U \openint 0 1$ is $\openint 0 1$.
It is therefore sufficient to show that for $0 < z < 1$: 
:$\map \Pr {\dfrac X {X + Y} \le z} = z$
Note that if $x, y > 0$ then: 
:$0 < \dfrac x {x + y} < 1$
Note also that: 
:$\dfrac x {x + y} \le z$ 
with $0 < z < 1$ is equivalent to: 
:$x \le z x + z y$
which is in turn equivalent to: 
:$\paren {1 - z} x \le z y$
That is: 
:$x \le \dfrac z {1 - z} y$
We therefore have: 
:$\map \Pr {\dfrac X {X + Y} \le z} = \map \Pr {X \le \dfrac z {1 - z} Y}$
Let $f_{X, Y}$ be the joint probability density function of $X$ and $Y$. 
Let $f_X$ and $f_Y$ be the probability density function of $X$ and $Y$ respectively. 
From Condition for Independence from Joint Probability Density Function, we have for each $x, y \in \R_{> 0}$:
:$\map {f_{X, Y} } {x, y} = \map {f_X} x \map {f_Y} y$
We therefore have: 
{{begin-eqn}}
{{eqn | l = \map \Pr {\dfrac X {X + Y} \le z}
      | r = \map \Pr {X \le \frac z {1 - z} Y}
}}
{{eqn | r = \int_0^\infty \int_0^{\frac z {1 - z} y} \map {f_{X, Y} } {x, y} \rd x \rd y
}}
{{eqn | r = \int_0^\infty \int_0^{\frac z {1 - z} y} \map {f_X} x \map {f_Y} y \rd x \rd y
}}
{{eqn | r = \int_0^\infty \frac 1 \beta \map \exp {-\frac y \beta} \paren {\int_0^{\frac z {1 - z} y} \frac 1 \beta \map \exp {-\frac x \beta} \rd x} \rd y
      | c = {{Defof|Exponential Distribution}}
}}
{{eqn | r = \int_0^\infty \frac 1 \beta \map \exp {-\frac y \beta} \intlimits {-\map \exp {-\frac x \beta} } 0 {\frac z {1 - z} y} \rd y
      | c = Primitive of Exponential of $a x$
}}
{{eqn | r = \int_0^\infty \frac 1 \beta \map \exp {-\frac y \beta} \paren {1 - \map \exp {-\frac z {\beta \paren {1 - z} } y} } \rd y
      | c = Exponential of Zero
}}
{{eqn | r = 1 - \frac 1 \beta \int_0^\infty \map \exp {-y \paren {\frac z {\beta \paren {1 - z} } + \frac 1 \beta} } \rd y
}}
{{eqn | r = 1 - \frac 1 \beta \int_0^\infty \map \exp {-\frac y {\beta \paren {1 - z} } } \rd y
}}
{{eqn | r = 1 + \frac 1 \beta \intlimits {\beta \paren {1 - z} \map \exp {-\frac y {\beta \paren {1 - z} } } } 0 \infty
      | c = Primitive of Exponential of $a x$
}}
{{eqn | r = 1 + \frac 1 \beta \paren {0 - \beta \paren {1 - z} }
      | c = Exponential Tends to Zero and Infinity, Exponential of Zero
}}
{{eqn | r = 1 - \paren {1 - z}
}}
{{eqn | r = z
}}
{{end-eqn}}
{{qed}}
Category:Continuous Uniform Distribution
Category:Exponential Distribution
kbp3t2gc8wc9a8y9kxx0bl3qcfp76dz
Theorem: Inverse Image Mapping Induced by Projection

Let $\family {S_i}_{i \mathop \in I}$ be a family of sets.
Let $\ds S = \prod_{i \mathop \in I} S_i$ be the Cartesian product of $\family {S_i}_{i \mathop \in I}$.
For each $j \in I$, let $\pr_j: S \to S_j$ denote the $j$-th projection.
For each $j \in I$ let $\pr_j^\gets: \powerset {S_i} \to \powerset S$ denote the inverse image mapping induced by $\pr_j$
Then for all $j \in I$, $\pr_j^\gets$ is the mapping defined by:
:$\ds \forall T \subseteq S_i: \map {\pr_j^\gets} T = \prod_{i \mathop \in I} T_i$
where:
:$T_i = \begin {cases} T & i = j \\ S_i & i \ne j \end {cases}$

Proof:
Let $j \in I$.
Let $T \subseteq S_j$.
Let $\family {T_i}_{i \mathop \in I}$ be the family of sets defined by:
:$T_i = \begin {cases} T & : i = j \\ S_i & : i \ne j \end {cases}$
Then:
{{begin-eqn}}
{{eqn | l = \map {\pr_j^\gets} T
      | r = \set {x \in S: \map {\pr_j} x \in T}
      | c = {{Defof|Inverse Image Mapping of Mapping}}
}}
{{eqn | r = \set {x \in S: x_j \in T}
      | c = {{Defof|Projection on Family of Sets}}
}}
{{eqn | r = \set {x \in S: x_j \in T, \forall i \ne j: x_i \in S_i}
      | c = as $x \in S \implies \paren {\forall i \in I: x_i \in S_i}$
}}
{{eqn | r = \set {x \in S: \forall i \in I: x_i \in T_i}
      | c = Definition of $T_i$ for all $i \in I$
}}
{{eqn | r = \prod_{i \mathop \in I} T_i
      | c = {{Defof|Cartesian Product of Family}}
}}
{{end-eqn}}
{{qed}}
Category:Projections
Category:Inverse Image Mappings
fcz71o6oogocea47aacse0o0nvfgbof
Theorem: Identity Function is Odd Function

Let $I_\R: \R \to \R$ denote the identity function on $\R$.
Then $I_\R$ is an odd function.

Proof:
{{begin-eqn}}
{{eqn | l = \map {I_\R} {-x}
      | r = -x
      | c = {{Defof|Identity Function}}
}}
{{eqn | r = -\map {I_\R} x
      | c = 
}}
{{end-eqn}}
Hence the result by definition of odd function.
{{qed}}
Category:Identity Mappings
Category:Examples of Odd Functions
oxam7nnhno8vncvpprywkit3jqbco7m
Theorem: Half-Range Fourier Series/Identity Function/Sine

The half-range Fourier sine series for $\map f x$ can be expressed as:
{{begin-eqn}}
{{eqn | l = \map f x
      | o = \sim
      | r = \dfrac {2 \lambda} \pi \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } n \sin \frac {n \pi x} \lambda
      | c = 
}}
{{eqn | r = \dfrac {2 \lambda} \pi \paren {\sin \dfrac {\pi x} \lambda - \frac 1 2 \sin \dfrac {2 \pi x} \lambda + \frac 1 3 \sin \dfrac {3 \pi x} \lambda - \dotsb}
      | c = 
}}
{{end-eqn}}

Proof:
By definition of half-range Fourier sine series:
:$(1): \quad \map f x \sim \ds \sum_{n \mathop = 1}^\infty b_n \sin \dfrac {n \pi x} \lambda$
where for all $n \in \Z_{> 0}$:
{{begin-eqn}}
{{eqn | l = b_n
      | r = \frac 2 \lambda \int_0^\lambda \map f x \sin \dfrac {n \pi x} \lambda \rd x
      | c = 
}}
{{eqn | r = \frac 2 \lambda \int_0^\lambda x \sin \frac {n \pi x} \lambda \rd x
      | c = Definition of $\map f x$
}}
{{eqn | r = \frac 2 \lambda \intlimits {\frac {\lambda^2} {n^2 \pi^2} \sin \dfrac {n \pi x} \lambda - \frac \lambda {n \pi} x \cos \dfrac {n \pi x} \lambda} 0 \lambda
      | c = Primitive of $x \sin a x$, Fundamental Theorem of Calculus
}}
{{eqn | r = \frac 2 \lambda \paren {\paren {\frac {\lambda^2} {n^2 \pi^2} \sin n \pi - \frac {\lambda^2} {n \pi} \cos n \pi} - \paren {\frac {\lambda^2} {n^2 \pi^2} \sin 0 - \frac \lambda {n \pi} 0 \cos 0} }
      | c = 
}}
{{eqn | r = -\frac {2 \lambda} {n \pi} \cos n \pi
      | c = Sine of Multiple of Pi and simplification
}}
{{eqn | r = -\frac {2 \lambda} {n \pi} \paren {-1}^n
      | c = Cosine of Multiple of Pi
}}
{{eqn | r = \frac {2 \lambda} {n \pi} \paren {-1}^{n + 1}
}}
{{end-eqn}}
Substituting for $b_n$ in $(1)$: 
:$\ds \map f x = \dfrac {2 \lambda} \pi \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } n \sin \frac {n \pi x} \lambda$
as required.
{{Qed}}
Category:Half-Range Fourier Series for Identity Function
gwpeb1dmbkouijp76qo4qm5a0p3ne3d
Theorem: Absolute Value Function is Even Function

Let $\size {\, \cdot \,} : \R \to \R$ denote the absolute value function on $\R$:
Then $\size {\, \cdot \,}$ is an even function.

Proof:
Recall the definition of the absolute value function:
:<nowiki>$\size x = \begin{cases}
x & : x > 0 \\
0 & : x = 0 \\
-x & : x < 0
\end{cases}$</nowiki>
Testing the $3$ cases in turn:
{{begin-eqn}}
{{eqn | l = x
      | o = >
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = -x
      | o = <
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = \size {-x}
      | r = x
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = \size x
      | c = {{Defof|Absolute Value}}
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = x
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = -x
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = \size {-x}
      | r = 0
      | c = {{Defof|Absolute Value}}
}}
{{eqn | r = \size x
      | c = {{Defof|Absolute Value}}
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = x
      | o = <
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = -x
      | o = >
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = \size {-x}
      | r = -x
      | c = {{Defof|Absolute Value}}: as $-x > 0$
}}
{{eqn | r = \size x
      | c = {{Defof|Absolute Value}}: as $x < 0$
}}
{{end-eqn}}
{{qed|lemma}}
Hence the result by definition of even function.
{{qed}}
Category:Absolute Value Function
Category:Examples of Even Functions
rgsjxclr9v0ebcbj7fc2q25n1z96cpn
Theorem: Fourier Series/Absolute Value Function over Symmetric Range

Let $\lambda \in \R_{>0}$ be a strictly positive real number.
Let $\map f x: \openint {-\lambda} \lambda \to \R$ be the absolute value function on the open real interval $\openint {-\lambda} \lambda$:
:$\forall x \in \openint {-\lambda} \lambda: \map f x = \size x$
The Fourier series of $f$ over $\openint {-\lambda} \lambda$ can be given as:
{{begin-eqn}}
{{eqn | l = \map f x
      | o = \sim
      | r = \frac \lambda 2 - \frac {4 \lambda} {\pi^2} \sum_{n \mathop = 0}^\infty \frac 1 {\paren {2 n + 1}^2} \cos \dfrac {\paren {2 n + 1} \pi x} \lambda
      | c = 
}}
{{eqn | r = \frac \lambda 2 - \frac {4 \lambda} {\pi^2} \paren {\cos \dfrac {\pi x} \lambda + \frac 1 {3^2} \cos \dfrac {3 \pi x} \lambda + \frac 1 {5^2} \dfrac {5 \pi x} \lambda + \dotsb}
      | c = 
}}
{{end-eqn}}

Proof:
From Absolute Value Function is Even Function, $\map f x$ is an even function.
By Fourier Series for Even Function over Symmetric Range, we have:
:$\ds \map f x \sim \sum_{n \mathop = 1}^\infty a_n \cos \frac {n \pi x} \lambda$
where:
{{begin-eqn}}
{{eqn | l = a_n
      | r = \frac 2 \lambda \int_0^\pi \map f x \cos \frac {n \pi x} \lambda \rd x
      | c = 
}}
{{eqn | r = \frac 2 \lambda \int_0^\pi x \cos \frac {n \pi x} \lambda \rd x
      | c = Definition of $\map f x$
}}
{{end-eqn}}
Hence from Half-Range Fourier Cosine Series for Identity Function:
:$\map f x \sim \dfrac \lambda 2 - \ds \frac {4 \lambda} {\pi^2} \sum_{n \mathop = 0}^\infty \frac 1 {\paren {2 n + 1}^2} \cos \dfrac {\paren {2 n + 1} \pi x} \lambda$
Hence the result.
{{qed}}
Category:Absolute Value Function
Category:Fourier Series for Absolute Value Function
a25caf13gw8ycazokrahn9ahdqmetq3
Theorem: Versed Sine Function is Even

The versed sine is an even function:
:$\forall \theta \in \R: \map \vers {-\theta} = \vers \theta$

Proof:
{{begin-eqn}}
{{eqn | l = \map \vers {-\theta}
      | r = 1 - \map \cos {-\theta}
      | c = {{Defof|Versed Sine}}
}}
{{eqn | r = 1 - \cos \theta
      | c = Cosine Function is Even
}}
{{eqn | r = \vers \theta
      | c = {{Defof|Versed Sine}}
}}
{{end-eqn}}
{{qed}}
Category:Versed Sines
Category:Examples of Even Functions
g73g61r5fhzw1rsyohcg8mt45yih5e5
Theorem: Cartesian Product is Empty iff Factor is Empty/Family of Sets

Let $I$ be an indexing set.
Let $\family {S_i}_{i \mathop \in I}$ be a family of sets indexed by $I$.
Let $\ds S = \prod_{i \mathop \in I} S_i$ be the Cartesian product of $\family {S_i}_{i \mathop \in I}$.
Then:
:$S = \O$  {{iff}} $S_i = \O$ for some $i \in I$

Proof:
=== Necessary Condition ===
By the axiom of choice, the contrapositive statement holds:
:if $S_i \ne \O$ for all $i \in I$ then $S \ne \O$
By the Rule of Transposition, the converse holds:
:if $S = \O$  then $S_i = \O$ for some $i \in I$
{{qed|lemma}}
Theorem: Derivative of P-Norm wrt P

Let $p \ge 1$ be a real number.
Let $\ell^p$ denote the $p$-sequence space.
Let $\mathbf x = \sequence {x_n} \in \ell^p$.
Let $\norm {\mathbf x}_p$ be a $p$-norm.
Suppose, $\norm {\mathbf x}_p \ne 0$.
Then:
:$\ds \dfrac \d {\d p} \norm {\mathbf x}_p = \frac {\norm {\mathbf x}_p} p \paren { \frac {\sum_{n \mathop = 0}^\infty \size {x_n}^p \map \ln {\size {x_n} } } {\norm {\bf x}_p^p} - \map \ln {\norm {\bf x}_p} }$

Proof:
We begin with the natural logarithm of $\norm {\mathbf x}_p$:
{{begin-eqn}}
{{eqn | l = \dfrac \d {\d p} \map \ln {\norm {\bf x}_p}
      | r = \frac {\dfrac \d {\d p} \norm {\bf x}_p} {\norm {\bf x}_p}
}}
{{eqn | r = \map {\dfrac \d {\d p} } {\frac 1 p \map \ln {\sum_{n \mathop = 0}^\infty \size {x_n}^p} }
}}
{{eqn | r = -\frac 1 {p^2} \map \ln {\sum_{n \mathop = 0}^\infty \size {x_n}^p} + \frac 1 p \frac {\sum_{n \mathop = 0}^\infty \size {x_n}^p \map \ln {\size {x_n} } } {\sum_{n \mathop = 0}^\infty \size {x_n}^p}
      | c = Derivative of Power of Constant
}}
{{eqn | r = -\frac 1 {p^2} \map \ln {\norm {\bf x}_p^p} + \frac 1 p \frac {\sum_{n \mathop = 0}^\infty \size {x_n}^p \map \ln {\size {x_n} } } {\norm {\bf x}_p^p}
}}
{{eqn | r = \frac 1 p \paren {\frac {\sum_{n \mathop = 0}^\infty \size {x_n}^p \map {\ln} {\size {x_n} } } {\norm {\bf x}_p^p} - \map \ln {\norm {\bf x}_p} }
}}
{{end-eqn}}
Multiplication by $\norm {\mathbf x}_p$ completes the proof.
{{qed}}
Category:P-Norms
5knm6ibg8cexb6ea1046glcop0dc0no
Theorem: P-Norm of Real Sequence is Strictly Decreasing Function of P

Let $p \ge 1$ be a real number.
Let ${\ell^p}_\R$ denote the real $p$-sequence space.
Let $\mathbf x = \sequence {x_n} \in {\ell^p}_\R$.
Suppose $\mathbf x$ is not a sequence of zero elements.
Let $\norm {\mathbf x}_p$ denote the $p$-norm of $\mathbf x$ where $p \ge 1$.
Then the mapping $p \to \norm {\mathbf x}_p$ is strictly decreasing {{WRT}} $p$.

Proof:
{{begin-eqn}}
{{eqn | q = \forall i \in \N
      | l = \sum_{n \mathop = 0}^\infty {\size {x_n} }
      | o = \ge 
      | r = \size {x_i}
      | c = {{EuclidCommonNotionLink|5}}: the whole is greater than the part
}}
{{eqn | ll= \leadsto
      | q = \forall i \in \N
      | l = \paren {\sum_{n \mathop = 0}^\infty {\size {x_n} }^p }^{\frac 1 p}
      | o = \ge 
      | r = \paren { {\size {x_i}^p } }^{\frac 1 p}
      | c = 
}}
{{eqn | r = \size {x_i}
}}
{{end-eqn}}
Equality holds only for a sequence of zero elements.
Suppose $\mathbf x$ is not a sequence of zero elements.
Then:
{{begin-eqn}}
{{eqn | ll= \leadsto
      | q = \forall i \in \N
      | l = \paren {\sum_{n \mathop = 0}^\infty {\size {x_n} }^p }^{\frac 1 p}
      | o = > 
      | r = \size {x_i}
}}
{{eqn | ll= \leadsto
      | l = \frac 1 p \map \ln {\sum_{n \mathop = 0}^\infty {\size {x_n} }^p}
      | o = >
      | r = \map \ln {\size {x_i} }
}}
{{eqn | ll= \leadsto
      | l = \frac 1 p \map \ln {\sum_{n \mathop = 0}^\infty {\size {x_n} }^p} \sum_{i \mathop = 0}^\infty {\size {x_i} }^p
      | o = >
      | r = \sum_{i \mathop = 0}^\infty {\size {x_i} }^p \map \ln {\size {x_i} }
      | c = Multiply both sides by $\size {x_i}$ and sum over $i \in \N$
}}
{{eqn | ll = \leadsto
      | l = \sum_{i \mathop = 0}^\infty {\size {x_i} }^p \map \ln {\size {x_i} } - \frac 1 p \map \ln {\sum_{n \mathop = 0}^\infty {\size {x_n} }^p} \sum_{i \mathop = 0}^\infty {\size {x_i} }^p 
      | o = <
      | r = 0
}}
{{eqn | ll = \leadsto
      | l = \sum_{i \mathop = 0}^\infty {\size {x_i} }^p \map \ln {\size {x_i} } - \map \ln {\norm {\mathbf x}_p} \norm {\mathbf x}_p^p 
      | o = <
      | r = 0
      | c =  {{Defof|Real P-Norm}}; Denote this inequality as $\paren \star$
}}
{{end-eqn}}
By derivative of $p$-norm {{WRT}} $p$:
{{begin-eqn}}
{{eqn | l = \dfrac \d {\d p} \norm {\mathbf x}_p
      | r = \frac {\norm {\mathbf x}_p} p \paren {\frac {\sum_{i \mathop = 0}^\infty \size {x_i}^p \map \ln {\size {x_i} } } {\norm {\bf x}_p^p} - \map \ln {\norm {\bf x}_p} }
}}
{{eqn | r = \frac 1 {p \norm {\mathbf x}_p^{p \mathop - 1} } \paren {\sum_{i \mathop = 0}^\infty \size {x_i}^p \map \ln {\size {x_i} }  - \norm {\mathbf x}_p^p \map \ln {\norm {\bf x}_p} }
}}
{{end-eqn}}
By $\paren \star$, the term in parenthesis is negative.
By $p$-Norm is Norm:
:$\norm {\mathbf x}_p > 0$ for $\mathbf x \ne \sequence 0$.
Hence:
:$\forall p \ge 1 : \forall \mathbf x \ne \sequence 0 : \dfrac \d {\d p} \norm {\mathbf x}_p < 0$
{{qed}}
Category:P-Norms
4vwrnunj7uxcsmbqb6swuysttv18svu
Theorem: Extension of Half-Range Fourier Sine Function to Symmetric Range

Let $\map f x$ be a real function defined on the interval $\openint 0 \lambda$.
Let $\map f x$ be represented by the half-range Fourier sine series $\map S x$:
:$\map f x \sim \map S x = \ds \sum_{n \mathop = 1}^\infty b_n \sin \frac {n \pi x} \lambda$
where for all $n \in \Z_{> 0}$:
:$b_n = \ds \frac 2 \lambda \int_0^\lambda \map f x \sin \frac {n \pi x} \lambda \rd x$
Then $\map S x$ also represents the extension $g: \openint {-\lambda} \lambda \to \R$ of $f$, defined as:
:$\forall x \in \openint {-\lambda} \lambda: \map g x = \begin {cases} \map f x & : x > 0 \\ -\map f {-x} & : x < 0 \\ 0 & : x = 0 \end {cases}$

Proof:
It is apparent by inspection that:
:$(1): \quad g$ is an extension of $f$
:$(2): \quad g$ is an odd function.
Let $\map T x$ be the Fourier series representing $g$:
:$\map g x \sim \map T x = \dfrac {a_0} 2 + \ds \sum_{n \mathop = 1}^\infty \paren {a_n \cos \frac {n \pi x} \lambda + b_n \sin \frac {n \pi x} \lambda}$
where for all $n \in \Z_{> 0}$:
:$a_n = \ds \frac 1 \lambda \int_{-\lambda}^\lambda \map g x \cos \frac {n \pi x} \lambda \rd x$
:$b_n = \ds \frac 1 \lambda \int_{-\lambda}^\lambda \map g x \sin \frac {n \pi x} \lambda \rd x$
From Fourier Cosine Coefficients for Odd Function over Symmetric Range:
:$\forall n \in \Z_{\ge 0}: a_n = 0$
and from Fourier Sine Coefficients for Odd Function over Symmetric Range:
:$\forall n \in \Z_{>0}: b_n = \ds \frac 2 \lambda \int_0^\lambda \map g x \sin \frac {n \pi x} \lambda \rd x$
But on $\openint 0 \lambda$, by definition:
:$\forall x \in \openint 0 \lambda: \map g x = \map f x$
Hence:
:$\map T x = \ds \sum_{n \mathop = 1}^\infty \paren b_n \sin \frac {n \pi x} \lambda$
where:
:$b_n = \ds \frac 2 \lambda \int_0^\lambda \map f x \sin \frac {n \pi x} \lambda \rd x$
That is, $\map T x$ is the same as $\map S x$.
Hence the result.
{{qed}}
Category:Half-Range Fourier Series
staaqiq20we2nv12qt7w47cq1l35csp
Theorem: Extension of Half-Range Fourier Cosine Function to Symmetric Range

Let $\map f x$ be a real function defined on the interval $\openint 0 \lambda$.
Let $\map f x$ be represented by the half-range Fourier cosine series $\map S x$:
:$\map f x \sim \map S x = \dfrac {a_0} 2 + \ds \sum_{n \mathop = 1}^\infty a_n \cos \frac {n \pi x} \lambda$
where for all $n \in \Z_{> 0}$:
:$a_n = \ds \frac 2 \lambda \int_0^\lambda \map f x \cos \frac {n \pi x} \lambda \rd x$
Then $\map S x$ also represents the extension to the even function $g: \openint {-\lambda} \lambda \to \R$ of $f$, defined as:
:$\forall x \in \openint {-\lambda} \lambda: \map g x = \begin {cases} \map f x & : x > 0 \\ \map f {-x} & : x < 0 \\ \ds \lim_{x \mathop \to 0} \map g x & : x = 0 \end {cases}$

Proof:
It is apparent by inspection that:
:$(1): \quad g$ is an extension of $f$
:$(2): \quad g$ is an even function.
Let $\map T x$ be the Fourier series representing $g$:
:$\map g x \sim \map T x = \dfrac {a_0} 2 + \ds \sum_{n \mathop = 1}^\infty \paren {a_n \cos \frac {n \pi x} \lambda + b_n \sin \frac {n \pi x} \lambda}$
where for all $n \in \Z_{> 0}$:
:$a_n = \ds \frac 1 \lambda \int_{-\lambda}^\lambda \map g x \cos \frac {n \pi x} \lambda \rd x$
:$b_n = \ds \frac 1 \lambda \int_{-\lambda}^\lambda \map g x \sin \frac {n \pi x} \lambda \rd x$
From Fourier Sine Coefficients for Even Function over Symmetric Range:
:$\forall n \in \Z_{> 0}: b_n = 0$
and from Fourier Cosine Coefficients for Even Function over Symmetric Range:
:$\forall n \in \Z_{>0}: a_n = \ds \frac 2 \lambda \int_0^\lambda \map g x \cos \frac {n \pi x} \lambda \rd x$
But on $\openint 0 \lambda$, by definition:
:$\forall x \in \openint 0 \lambda: \map g x = \map f x$
Hence:
:$\map T x = \dfrac {a_0} 2 + \ds \sum_{n \mathop = 1}^\infty \paren a_n \cos \frac {n \pi x} \lambda$
where:
:$a_n = \ds \frac 2 \lambda \int_0^\lambda \map f x \cos \frac {n \pi x} \lambda \rd x$
That is, $\map T x$ is the same as $\map S x$.
Hence the result.
{{qed}}
Category:Half-Range Fourier Series
0hsivq396jatmi1bot9nntfaup6dgan
Theorem: Primitive of x by Logarithm of x squared plus a squared

:$\ds \int x \map \ln {x^2 + a^2} \rd x = \frac {\paren {x^2 + a^2} \map \ln {x^2 + a^2} - x^2} 2 + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int x \map \ln {x^2 + a^2} \rd x
      | r = \frac {x^2 \map \ln {x^2 + a^2} } 2 - \int \frac {x^3} {x^2 + a^2} \rd x + C
      | c = Primitive of $x^m \map \ln {x^2 + a^2}$ with $m = 1$
}}
{{eqn | r = \frac {x^2 \map \ln {x^2 + a^2} } 2 - \paren {\frac {x^2} 2 - \frac {a^2} 2 \map \ln {x^2 + a^2} } + C
      | c = Primitive of $\dfrac {x^3} {x^2 + a^2}$
}}
{{eqn | r = \frac {\paren {x^2 + a^2} \map \ln {x^2 + a^2} - x^2} 2 + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Sets Separated by Neighborhoods

Let $T = \struct {S, \tau}$ be a topological space.
{{TFAE|def = Separated by Neighborhoods/Sets|view = Sets Separated by Neighborhoods}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $A, B \subseteq S$ such that:
:$\exists N_A, N_B \subseteq S: \exists U, V \in \tau: A \subseteq U \subseteq N_A, B \subseteq V \subseteq N_B: N_A \cap N_B = \O$
From Subsets of Disjoint Sets are Disjoint then:
:$U \cap V = \O$
Thus:
:$\exists U, V \in \tau: A \subseteq U, B \subseteq V: U \cap V = \O$
{{qed|lemma}}
Theorem: Equivalence of Definitions of Points Separated by Neighborhoods

Let $T = \struct {S, \tau}$ be a topological space.
{{TFAE|def = Points Separated by Neighborhoods}}

Proof:
Let $x, y \in S$.
From Singleton of Element is Subset:
:$x$ and $y$ are separated as points by neighborhoods {{iff}} the singletons $\set x$ and $\set y$ are separated as sets by neighborhoods.
From Equivalence of Definitions of Sets Separated by Neighborhoods:
:the singletons $\set x$ and $\set y$ are separated as sets by neighborhoods {{iff}} the singletons $\set x$ and $\set y$ are separated as sets by open sets.
From Singleton of Element is Subset:
:the singletons $\set x$ and $\set y$ are separated as sets by open sets {{iff}} $x$ and $y$ are separated as points by open sets.
{{qed}}
Category:Separation Axioms
2cvik2cs1kk1t7a8q7a5rp4yotk6nln
Theorem: Product Space is T3 iff Factor Spaces are T3/Sufficient Condition

Let $\mathbb S = \family {\struct {S_\alpha, \tau_\alpha} }_{\alpha \mathop \in I}$ be an indexed family of non-empty topological spaces for $\alpha$ in some indexing set $I$.
Let $\ds T = \struct{S, \tau} = \prod_{\alpha \mathop \in I} \struct {S_\alpha, \tau_\alpha}$ be the product space of $\mathbb S$.
Let $T$ be a $T_3$ space.
Then for each $\alpha \in I$, $\struct {S_\alpha, \tau_\alpha}$ is a $T_3$ space.

Proof:
Let $T$ be a $T_3$ space.
As $S_\alpha \ne \O$ we also have $S \ne \O$ by the axiom of choice.
Let $\alpha \in I$.
From Subspace of Product Space is Homeomorphic to Factor Space, $\struct {S_\alpha, \tau_\alpha}$ is homeomorphic to a subspace $T_\alpha$ of $T$.
From $T_3$ property is hereditary, $T_\alpha$ is $T_3$.
From $T_3$ Property is Preserved under Homeomorphism, $\struct {S_\alpha, \tau_\alpha}$ is $T_3$.
As $\alpha \in I$ was arbitrary, it follows that each $\struct {S_\alpha, \tau_\alpha}$ is a $T_3$ space.