nyuuzyou/wikis huggingface dataset:
Factorial as Product of Three Factorials/Examples/10

== Example of Factorial as Product of Three Factorials ==
:$10! = 7! \times 5! \times 3!$
== Proof ==
== Sources ==
* : $10$
* : $3,628,800$
* : $10$
* : $3,628,800$
Category:Factorial as Product of Three Factorials
Category:10
Category:3,628,800
Factorial as Product of Two Factorials

== Theorem ==
Apart from the general pattern, following directly from the definition of the factorial:
:$\paren {n!}! = n! \paren {n! - 1}!$
the only known factorial which is the product of two factorials is:
:$10! = 6! \, 7!$
== Proof ==
== Examples ==
== Sources ==
* : $10$
* : $10$
Category:Factorials
Category:10
Factorial as Sum of Series of Subfactorial by Falling Factorial over Factorial

== Theorem ==
Here, we have:
:$n^{\underline k}$ denotes the $k$th falling factorial of $n$
:$!k$ denotes the $k$th subfactorial
:$k!$ denotes the $k$th factorial.
== Proof ==
== Condition for Convergence ==
== Historical Note ==
== Sources ==
* : $\S 1.2.5$: Permutations and Factorials: $(11)$
Category:Factorials
Category:Falling Factorials
Category:Subfactorials
Category:Factorial as Sum of Series of Subfactorial by Falling Factorial over Factorial
Factorial as Sum of Series of Subfactorial by Falling Factorial over Factorial/Condition for Convergence

== Theorem ==
Consider the series:
This converges only when $n \in \Z_{\ge 0}$, that is, when $n$ is a non-negative integer.
== Proof ==
First we show that this series converges when $n \in \Z_{\ge 0}$.
Consider the coefficients:
:$1, \paren {1 - \dfrac 1 {1!} }, \paren {1 - \dfrac 1 {1!} + \dfrac 1 {2!} }, \ldots$
By Power Series Expansion for Exponential Function, they converge to $\dfrac 1 e$.
Starting from the $\paren {n + 1}$th term, there is a factor of $\paren {n - n}$.
In this case, all subsequent terms of the expansion equal $0$.
Therefore the series converges.
Then we show that this series diverges for $n \notin \Z_{\ge 0}$.
We do this via Divergence Test.
That is, we show that $\ds \lim_{k \mathop \to \infty} \frac { {!k} \, n^{\underline k} } {k!} \ne 0$.
 $\ds \lim_{k \mathop \to \infty} \frac { {!k} \, n^{\underline k} } {k!}$ exists.
By Power Series Expansion for Exponential Function, we have that $\ds \lim_{k \mathop \to \infty} \frac {k!} {!k} = e$.
Hence $\ds \lim_{k \mathop \to \infty} n^{\underline k}$ would exist as well.
For $k > \floor {n + 2}$:
Since $n - k \ne 0$, $\size {n^{\underline k} }$ increases without bound.
Hence its limit does not exist, a contradiction.
Therefore $\ds \lim_{k \mathop \to \infty} \frac { {!k} \, n^{\underline k} } {k!}$ does not exist for $n \notin \Z_{\ge 0}$.
By Divergence Test, our series diverges.
== Sources ==
* : $\S 1.2.5$: Permutations and Factorials: Exercise $16$
Category:Factorial as Sum of Series of Subfactorial by Falling Factorial over Factorial
Factorial as Sum of Series of Subfactorial by Falling Factorial over Factorial/Historical Note

== Historical Note on Factorial as Sum of Series of Subfactorial by Falling Factorial over Factorial ==
This result was established by during the course of his attempt extend the factorial to the real numbers.
While it provides an exact value for $n!$ when $n$ is a positive integer, the infinite sum exists only under this condition.
== Sources ==
* : $\S 1.2.5$: Permutations and Factorials
Category:Historical Notes
Factorial as Sum of Series of Subfactorial by Falling Factorial over Factorial/Proof

== Theorem ==
== Proof ==
Let $n$ be a non-negative integer.
We assume a solution of the form:
:$(1): \quad n! = a_0 + a_1 n + a_2 n \paren {n - 1} + a_3 n \paren {n - 1} \paren {n - 2} + \cdots$
We can express $(1)$ using binomial coefficients:
:$(2): \quad n! = \ds \sum_k \dbinom n k k! a_k$
Then:
== Sources ==
* : $\S 1.2.6$: Binomial Coefficients: Example $5$
Category:Factorial as Sum of Series of Subfactorial by Falling Factorial over Factorial
Factorial is Primitive Recursive

== Theorem ==
The factorial function $\operatorname{fac}: \N \to \N$ defined as:
:$\map {\operatorname{fac} } n = n!$
is primitive recursive.
== Proof ==
From the definition of the factorial, we have that:
:$\map {\operatorname{fac} } n = \begin{cases}
1 & : n = 0 \\
\map {\operatorname{mult} } {n, \map {\operatorname{fac} } {n - 1} } & : n > 0
\end{cases}$
Thus $\operatorname{fac}$ is obtained by primitive recursion from the constant $1$ and the primitive recursive function $\operatorname{mult}$.
Hence $\operatorname{fac}$ is primitive recursive.
Category:Primitive Recursive Functions
Factorial is not of Exponential Order

== Theorem ==
Let $\Gamma$ denote the gamma function.
Let $\map f t = \map \Gamma {t + 1} = t!$.
Then:
:$f$ is not of exponential order.
That is, it grows faster than any exponential.
== Proof ==
From Gamma Function is Continuous on Positive Reals, $f$ is continuous for $t \ge 0$.
Set $t > 0$.
From Stirling's Formula:
:$t! \sim \sqrt {2 \pi t} \paren {\dfrac t e}^t$
where $\sim$ denotes asymptotic equality.
That is, 
 $t^t \, e^{-t}$ is of exponential order $a$. 
Then, for $t$ sufficiently large, there exists a $K > 0$ such that:
This implies that $t^t$ is of exponential order, which is false.
From this contradiction it follows that $t!$ is also not of exponential order.
Category:Gamma Function
Category:Exponential Order
Factorial of Half

== Theorem ==
:$\left({\dfrac 1 2}\right)! = \dfrac {\sqrt \pi} 2$
where $x!$ denotes the extension of the factorial function to the real numbers.
== Proof 1 ==
== Proof 2 ==
== Historical Note ==
== Sources ==
* : $\S 1.2.5$: Permutations and Factorials
Category:Factorials/Examples
Category:Factorial of Half
Factorial of Half/Historical Note

== Historical Note on Factorial of Half ==
The factorial of $\dfrac 1 2$ was deduced by during the course of his attempt to extend the factorial to the real numbers.
However he was not able to prove that such an extension defined $n!$ for a general non-integer $n$.
== Sources ==
* : $\S 1.2.5$: Permutations and Factorials
Category:Historical Notes
Factorial of Half/Proof 2

== Theorem ==
== Proof ==
From Infinite Product of Product of Sequence of n plus alpha over Sequence of n plus beta:
Setting:
:$k = 2$
:$\alpha_1 = \alpha_2 = 0$
:$\beta_1 = -\dfrac 1 2, \beta_2 = \dfrac 1 2$
we see that:
:$\alpha_1 + \alpha_2 = \beta_1 + \beta_2$
So this reduces to:
We then note that by Wallis's Product:
:$\ds \prod_{n \mathop \ge 1} \dfrac n {n - \frac 1 2} \dfrac n {n + \frac 1 2} = \frac \pi 2$
Thus:
== Sources ==
* : $\S 1.2.5$: Permutations and Factorials: Exercise $18$
Category:Factorial of Half
Factorial of Integer plus Reciprocal of Integer

== Theorem ==
Let $x \in \Z$ be a positive integer.
Then:
:$\ds \lim_{n \mathop \to \infty} \dfrac {\paren {n + x}!} {n! n^x} = 1$
== Proof ==
We have that:
As $n \to \infty$, the quantity on the indeed tends to $1$.
== Sources ==
* : $\S 1.2.5$: Permutations and Factorials: Exercise $22$
Category:Factorials
Factorial which is Sum of Two Squares

== Theorem ==
The only factorial which can be expressed as the sum of two squares is:
== Proof ==
We show that for $n \ge 7$, $n!$ cannot be expressed as the sum of two squares.
By refining the result in Interval containing Prime Number of forms 4n - 1, 4n + 1, 6n - 1, 6n + 1, one can show that:
:There exists a prime of the form $4 k + 3$ strictly between $m$ and $2 m$ whenever $m \ge 4$.
Let $n \ge 7$. Then $\ceiling {\dfrac n 2} \ge 4$.
Using the result above, there is a prime $p$ of the form $4 k + 3$ such that:
:$\ceiling {\dfrac n 2} < p < 2 \ceiling {\dfrac n 2}$
We then have, by multiplying the inequality by $2$:
:$2 \ceiling {\dfrac n 2} < 2 p < 4 \ceiling {\dfrac n 2}$
This gives:
:$p < 2 \ceiling {\dfrac n 2} < 2 p$
Which implies:
:$p \le n < 2 p$
From Integer as Sum of Two Squares:
:$n!$ can be expressed as the sum of two squares each of its prime divisors of the form $4 k + 3$ (if any) occur to an even power.
The inequality above shows that there are no multiples of $p$ which are not greater than $n$ except $p$ itself.
Hence $p$ occurs to an odd power, $1$, in $n!$.
This shows that for $n \ge 7$, $n!$ cannot be expressed as the sum of two squares.
Checking the rest of the factorials we see that the only ones satisfying the criteria are:
Hence the result.
== Sources ==
* : $720$
Category:Factorials
Category:Square Numbers
Category:720
Factoring Mapping into Quotient and Injection

== Theorem ==
Let $f: S \to T$ be a mapping.
Then $f$ can be uniquely factored into a quotient mapping, followed by an injection.
Thus:
:$f = h \circ q_{\RR_f}$
where:
:$q_{\RR_f}: S \to S / \RR_f: \map {q_{\RR_f} } s = \eqclass s {\RR_f}$
:$h: S / \RR_f \to T: \map h {\eqclass s {\RR_f} } = \map f s$
:$\eqclass s {\RR_f}$ denotes the equivalence class of $s$ with respect to the equivalence relation $\RR$ induced on $S$ by $f$.
This can be illustrated using a commutative diagram as follows:
$\quad\quad \begin{xy}\xymatrix@L+2mu@+1em{
S \ar[r]^*{q_{\RR_f} }
\ar@{-->}[rd]_*{f = h \circ q_{\RR_f} }
&
S / \RR_f \ar[d]^*{h}
\\ &
T
}\end{xy}$
== Proof ==
The mapping $q_{\RR_f}: S \to S / \RR_f$ follows from the definition of quotient mapping.
The mapping $h$ is justified by Condition for Mapping from Quotient Set to be Well-Defined.
== Also see ==
* Factoring Mapping into Surjection and Inclusion
* Quotient Theorem for Surjections
* Quotient Theorem for Sets
== Sources ==
* : Chapter $\text{I}$: Sets and Functions: Factoring Functions
* : Chapter $4$: Mappings: Exercise $10 \ \text{(ii)}$
Category:Injections
Category:Quotient Mappings
Factoring Mapping into Surjection and Inclusion

== Theorem ==
Every mapping $f:S \to T$ can be uniquely factored into a surjection $g$ followed by the inclusion mapping $i_T$.
That is, $f = i_T \circ g$ where:
:$g: S \to \Img f: \map g x = \map f x$
:$i_T: \Img f \to T: \map {i_T} x = x$
This can be illustrated using a commutative diagram as follows:
$\quad\quad \begin{xy}\xymatrix@L+2mu@+1em {
S \ar@{-->}[r]^*{g}
\ar[rd]_*{f = i_T \circ g}
&
\Img f \ar@{-->}[d]^*{i_T}
\\
&
T
}\end{xy}$
== Proof ==
From Surjection by Restriction of Codomain, $f: S \to \Img f$ is a surjection.
The mapping $g: S \to \Img f$ where $\map g x = \map f x$ is therefore also clearly a surjection.
The mapping $g: S \to \Img f: \map g x = \map f x$ is clearly unique, by Equality of Mappings.
From Inclusion Mapping is Injection, $i_T: \Img f \to T$ is an injection.
Likewise, the mapping $i_T: \Img f \to T : \map {i_T} x = x$ is also unique, by its own definition.
== Also see ==
* Factoring Mapping into Quotient and Injection
* Quotient Theorem for Surjections
* Quotient Theorem for Sets
== Sources ==
* : Chapter $\text{I}$: Sets and Functions: Factoring Functions
Category:Surjections
Category:Inclusion Mappings
Factorions Base 10

== Theorem ==
The following positive integers are the only factorions base $10$:
:$1, 2, 145, 40 \, 585$
== Proof ==
From examples of factorials:
A computer search can verify solutions under $2540160 = 9! \times 7$ in seconds.
Let $n$ be a $7$-digit number with $n > 2540160$.
Then the sum of the factorials of its digits is not more than $9! \times 7 = 2540160$.
So $n$ cannot be a factorion base $10$.
Now let $n$ be a $k$-digit number, for $k \ge 8$.
Then the sum of the factorials of its digits is not more than $9! \times k$.
But we have:
So there are no more factorions base $10$.
== Historical Note ==
== Sources ==
* : $145$
* : $145$
Category:Factorions
Factorisation of Quintic x^5 - x + n into Irreducible Quadratic and Irreducible Cubic

== Theorem ==
The quintic $x^5 - x + n$ can be factorized into the product of an irreducible quadratic and an an irreducible cubic $n$ is in the set:
:$\set {\pm 15, \pm 22 \, 440, \pm 2 \, 759 \, 640}$
== Proof ==
We have that:
== Sources ==
* 
* : $2,759,640$
Category:Polynomial Theory
Factorisation of x^(2n)-1 in Real Domain

== Theorem ==
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
:$\ds z^{2 n} - 1 = \paren {z - 1} \paren {z + 1} \prod_{k \mathop = 1}^n \paren {z^2 - 2 \cos \dfrac {k \pi} n z + 1}$
== Proof ==
From Power of Complex Number minus 1:
:$\ds z^{2 n} - 1 = \prod_{k \mathop = 0}^{2 n - 1} \paren {z - \alpha^k}$
where:
From Complex Roots of Unity occur in Conjugate Pairs:
:$U_{2 n} = \set {1, \tuple {\alpha, \alpha^{2 n - 1} }, \tuple {\alpha^2, \alpha^{2 n - 2} }, \ldots, \tuple {\alpha^k, \alpha^{2 n - k} }, \ldots, \tuple {\alpha^{n - 1}, \alpha^{n + 1} }, -1}$
where $U_{2 n}$ denotes the complex $2 n$th roots of unity:
:$U_{2 n} = \set {z \in \C: z^{2 n} = 1}$
The case $k = 0$ is taken care of by setting $\alpha^0 = 1$, from whence we have the factor $z - 1$.
The case $k = n$ is taken care of by setting $\alpha^k = -1$, from whence we have the factor $z + 1$.
Taking the product of each of the remaining factors of $z^{2 n} - 1$:
Hence the result.
== Also see ==
* Factors of Difference of Two Even Powers
== Sources ==
* : $\S 3$. Roots of Unity: $(3.13)$
Category:Algebra
Category:Complex Roots
Factorisation of x^(2n+1)-1 in Real Domain

== Theorem ==
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
:$\ds z^{2 n + 1} - 1 = \paren {z - 1} \prod_{k \mathop = 1}^n \paren {z^2 - 2 z \cos \dfrac {2 \pi k} {2 n + 1} + 1}$
== Proof ==
From Power of Complex Number minus 1:
:$\ds z^{2 n + 1} - 1 = \prod_{k \mathop = 0}^{2 n} \paren {z - \alpha^k}$
where:
From Complex Roots of Unity occur in Conjugate Pairs:
:$U_{2 n + 1} = \set {1, \tuple {\alpha, \alpha^{2 n} }, \tuple {\alpha^2, \alpha^{2 n - 1} }, \ldots, \tuple {\alpha^k, \alpha^{2 n - k + 1} }, \ldots, \tuple {\alpha^n, \alpha^{n + 1} } }$
where $U_{2 n + 1}$ denotes the complex $2 n + 1$th roots of unity:
:$U_{2 n + 1} = \set {z \in \C: z^{2 n + 1} = 1}$
The case $n = 0$ is taken care of by setting $\alpha^0 = 1$, from whence we have the factor $z - 1$.
Taking the product of each of the remaining factors of $z^{2 n + 1} - 1$ in pairs:
Hence the result.
== Also see ==
* Factors of Difference of Two Odd Powers
== Sources ==
* : $\S 3$. Roots of Unity: $(3.13)$
Category:Algebra
Category:Complex Roots
Factorisation of z^(2n)+1 in Real Domain

== Theorem ==
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
:$\ds z^{2 n} + 1 = \prod_{k \mathop = 1}^n \paren {z^2 - 2 z \cos \dfrac {\paren {2 k + 1} \pi} {2 n} + 1}$
== Proof ==
From Factorisation of $z^n + 1$:
:$(1): \ds \quad z^{2 n} + 1 = \prod_{k \mathop = 0}^{2 n - 1} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n} }$
From Complex Roots of Polynomial with Real Coefficients occur in Conjugate Pairs, the roots of $(1)$ occur in conjugate pairs.
Hence we can express $(1)$ as:
Hence the result.
== Also see ==
* Factors of Sum of Two Even Powers
Category:Algebra
Category:Complex Roots
Factorisation of z^(2n+1)+1 in Real Domain

== Theorem ==
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
:$\ds z^{2 n + 1} + 1 = \paren {z + 1} \prod_{k \mathop = 0}^{n - 1} \paren {z^2 - 2 z \cos \dfrac {\paren {2 k + 1} \pi} {2 n + 1} + 1}$
== Proof ==
From Factorisation of $z^n + 1$:
:$(1): \quad \ds z^{2 n + 1} + 1 = \prod_{k \mathop = 0}^{2 n} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} }$
From Complex Roots of Polynomial with Real Coefficients occur in Conjugate Pairs, the roots of $(1)$ occur in conjugate pairs.
Hence we can express $(1)$ as:
== Also see ==
* Factors of Sum of Two Odd Powers
Category:Algebra
Category:Complex Roots
Factorisation of z^n+1

== Theorem ==
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
:$z^n + 1 = \ds \prod_{k \mathop = 0}^{n - 1} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} n}$
== Proof ==
From Factorisation of $z^n - a$, setting $a = -1$:
:$z^n + 1 = \ds \prod_{k \mathop = 0}^{n - 1} \paren {z - \alpha^k b}$
where:
:$\alpha$ is a primitive complex $n$th root of unity
:$b$ is any complex number such that $b^n = a$.
From Euler's Identity:
:$-1 = e^{i \pi}$
From Exponential of Product:
:$\paren {\exp \dfrac {i \pi} n}^n = e^{i \pi}$
and so:
:$b = \exp \dfrac {i \pi} n$
We also have by definition of the first complex $n$th root of unity, and from First Complex Root of Unity is Primitive:
:$\alpha = \exp \dfrac {2 i \pi} n$
Hence:
Category:Algebra
Category:Complex Roots
Factorisation of z^n+a

== Theorem ==
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $a \in \C$ be a complex number.
Then:
:$z^n + a = \ds \prod_{k \mathop = 0}^{n - 1} \paren {z - \alpha_k b}$
where:
:$\alpha_k$ are the complex $n$th roots of negative unity
:$b$ is any complex number such that $b^n = a$.
== Proof ==
From $z^n + a = 0$ we have that:
:$z^n = - a$
Let $b = a^{1 / n}$, hence $b^n = a$, with $a, b \in \C$.
From Roots of Complex Number:
and so each of $\alpha_k b = b e^{i \paren {2 k + 1} \pi / n}$ is a unique root of $z^n + a$ with $n \in \Z_{>0}$.
From the corollary to the Polynomial Factor Theorem:
If $\zeta_1, \zeta_2, \ldots, \zeta_n \in \C$ such that all are different, and $\map P {\zeta_1} = \map P {\zeta_2} = \cdots = \map P {\zeta_n} = 0$, then:
:$\ds \map P z = k \prod_{j \mathop = 1}^n \paren {z - \zeta_j}$
where $k \in \C$.
$z^n + a$ is a monic polynomial, hence $k = 1$ in the above product.
Choose $\zeta_j = \alpha_{j - 1} b$ and we have the desired result.
Category:Algebra
Category:Complex Roots
Factorisation of z^n-a

== Theorem ==
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $a \in \C$ be a complex number.
Then:
:$z^n - a = \ds \prod_{k \mathop = 0}^{n - 1} \paren {z - \alpha^k b}$
where:
:$\alpha$ is a primitive complex $n$th root of unity
:$b$ is any complex number such that $b^n = a$.
== Proof ==
From $z^n - a = 0$ we have that:
:$a = z^n$
Let $b = a^{1 / n}$, hence $b^n = a$, with $a, b \in \C$.
From Roots of Complex Number:
and so each of $b e^{2 i k \pi / n}$ is a root of $z^n - a$.
From First Complex Root of Unity is Primitive:
For each $n \in \Z_{>0}$ there exists at least one primitive complex $n$th root of unity, $\alpha$, hence each of $b \alpha^k$ is a unique root of $z^n - a$.
From the corollary to the Polynomial Factor Theorem:
If $\zeta_1, \zeta_2, \ldots, \zeta_n \in \C$ such that all are different, and $\map P {\zeta_1} = \map P {\zeta_2} = \cdots = \map P {\zeta_n} = 0$, then:
:$\ds \map P z = k \prod_{j \mathop = 1}^n \paren {z - \zeta_j}$
where $k \in \C$.
$z^n - a$ is a monic polynomial, hence $k = 1$ in the above product.
Choose $\zeta_j = b \alpha^{j - 1}$ and we have the desired result.
== Sources ==
* : $\S 3$. Roots of Unity
Category:Algebra
Category:Complex Roots
Factorization Lemma/Extended Real-Valued Function

== Theorem ==
Let $X$ be a set.
Let $\struct {Y, \Sigma}$ be a measurable space.
Let $f: X \to Y$ be a mapping.
An extended real-valued function $g: X \to \overline \R$ is $\map \sigma f$-measurable :
:There exists a $\Sigma$-measurable mapping $\tilde g: Y \to \overline \R$ such that $g = \tilde g \circ f$
where:
:$\map \sigma f$ denotes the $\sigma$-algebra generated by $f$
== Proof ==
=== Necessary Condition ===
Let $g$ be a $\map \sigma f \, / \, \overline \BB$-measurable function.
We need to construct a measurable $\tilde g$ such that $g = \tilde g \circ f$.
Let us proceed in the following fashion:
:Establish the result for $g$ a characteristic function;
:Establish the result for $g$ a simple function;
:Establish the result for all $g$
So let $g = \chi_E$ be a characteristic function.
By Characteristic Function Measurable iff Set Measurable, it follows that $E$ is $\map \sigma f$-measurable.
Thus there exists some $A \in \Sigma$ such that $E = \map {f^{-1} } A$.
Again by Characteristic Function Measurable iff Set Measurable, we have $\chi_A: Y \to \overline \R$ is measurable.
It follows that $\chi_E = \chi_A \circ f$, and $\tilde g := \chi_A$ works.
Now let $g = \ds \sum_{i \mathop = 1}^n a_i \chi_{E_i}$ be a simple function.
Let $A_i$ be associated to $E_i$ as above. Then we have:
Now $\ds \sum_{i \mathop = 1}^n a_i \chi_{A_i}$ is a simple function, hence measurable by Simple Function is Measurable.
Therefore, it suffices as a choice for $\tilde g$.
Next, let $g \ge 0$ be a measurable function.
By Measurable Function is Pointwise Limit of Simple Functions, we find simple functions $g_j$ such that:
:$\ds \lim_{j \mathop \to \infty} g_j = g$
Applying the previous step to each $g_j$, we find a sequence of $\tilde g_j$ satisfying:
:$\ds \lim_{j \mathop \to \infty} \tilde g_j \circ f = g$
From Composition with Pointwise Limit it follows that we have, putting $\tilde g := \ds \lim_{j \mathop \to \infty} \tilde g_j$:
:$\ds \lim_{j \mathop \to \infty} \tilde g_j \circ f = \tilde g \circ f$
An application of Pointwise Limit of Measurable Functions is Measurable yields $\tilde g$ measurable.
Thus we have provided a suitable $\tilde g$ for every $g$, such that:
:$g = \tilde g \circ f$
as desired.
=== Sufficient Condition ===
Suppose that such a $\tilde g$ exists.
Note that $f$ is $\map \sigma f \,/\, \Sigma$-measurable by definition of $\map \sigma f$.
The result follows immediately from Composition of Measurable Mappings is Measurable.
== Sources ==
* : $8.13$
Category:Measure Theory
Factorization Lemma/Real-Valued Function

== Theorem ==
Let $X$ be a set, and $\struct {Y, \Sigma}$ be a measurable space.
Let $f: X \to Y$ be a mapping.
Then a mapping $g: X \to \R$ is $\map \sigma f \, / \, \map \BB \R$-measurable :
:There exists a $\Sigma \, / \, \map \BB \R$-measurable mapping $\tilde g: Y \to \R$ such that $g = \tilde g \circ f$
where:
:$\map \sigma f$ denotes the $\sigma$-algebra generated by $f$
:$\map \BB \R$ denotes the Borel $\sigma$-algebra on $\R$
== Proof ==
=== Necessary Condition ===
Let $g$ be a $\map \sigma f \, / \, \map \BB \R$-measurable function.
We need to construct a measurable $\tilde g$ such that $g = \tilde g \circ f$.
Let us proceed in the following fashion:
:Establish the result for $g$ a characteristic function;
:Establish the result for $g$ a simple function;
:Establish the result for all $g$
So let $g = \chi_E$ be a characteristic function.
By Characteristic Function Measurable iff Set Measurable, it follows that $E$ is $\sigma \left({f}\right)$-measurable.
Thus there exists some $A \in \Sigma$ such that $E = \map {f^{-1} } A$.
Again by Characteristic Function Measurable iff Set Measurable, we have $\chi_A: Y \to \R$ is measurable.
It follows that $\chi_E = \chi_A \circ f$, and $\tilde g := \chi_A$ works.
Now let $g = \ds \sum_{i \mathop = 1}^n a_i \chi_{E_i}$ be a simple function.
Let $A_i$ be associated to $E_i$ as above. Then we have:
Now $\ds \sum_{i \mathop = 1}^n a_i \chi_{A_i}$ is a simple function, hence measurable by Simple Function is Measurable.
Therefore, it suffices as a choice for $\tilde g$.
Next, let $g \ge 0$ be a measurable function.
By Measurable Function is Pointwise Limit of Simple Functions, we find simple functions $g_j$ such that:
:$\ds \lim_{j \mathop \to \infty} g_j = g$
Applying the previous step to each $g_j$, we find a sequence of $\tilde g_j$ satisfying:
:$\ds \lim_{j \mathop \to \infty} \tilde g_j \circ f = g$
From Composition with Pointwise Limit it follows that we have, putting $\tilde g := \ds \lim_{j \mathop \to \infty} \tilde g_j$:
:$\ds \lim_{j \mathop \to \infty} \tilde g_j \circ f = \tilde g \circ f$
An application of Pointwise Limit of Measurable Functions is Measurable yields $\tilde g$ measurable.
Thus we have provided a suitable $\tilde g$ for every $g$, such that:
:$g = \tilde g \circ f$
as desired.
=== Sufficient Condition ===
Suppose that such a $\tilde g$ exists.
Note that $f$ is $\map \sigma f \, / \, \Sigma$-measurable by definition of $\map \sigma f$.
The result follows immediately from Composition of Measurable Mappings is Measurable.
== Sources ==
* : $\S 7$: Problem $11$
Category:Measure Theory