avewright/proofwiki-math huggingface dataset:
Theorem: Set is Subset of Union/Family of Sets

Let $\family {S_\alpha}_{\alpha \mathop \in I}$ be a family of sets indexed by $I$.
Then:
:$\ds \forall \beta \in I: S_\beta \subseteq \bigcup_{\alpha \mathop \in I} S_\alpha$
where $\ds \bigcup_{\alpha \mathop \in I} S_\alpha$ is the union of $\family {S_\alpha}$.

Proof:
Let $x \in S_\beta$ for some $\beta \in I$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = S_\beta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \set {x: \exists \alpha \in I: x \in S_\alpha}
      | c = {{Defof|Indexed Family of Sets}}
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \bigcup_{\alpha \mathop \in I} S_\alpha
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadsto
      | l = S_\beta
      | o = \subseteq
      | r = \bigcup_{\alpha \mathop \in I} S_\alpha
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
As $\beta$ was arbitrary, it follows that:
:$\ds \forall \beta \in I: S_\beta \subseteq \bigcup_{\alpha \mathop \in I} S_\alpha$
{{qed}}
Theorem: Set is Subset of Union/Family of Sets

Let $\family {S_\alpha}_{\alpha \mathop \in I}$ be a family of sets indexed by $I$.
Then:
:$\ds \forall \beta \in I: S_\beta \subseteq \bigcup_{\alpha \mathop \in I} S_\alpha$
where $\ds \bigcup_{\alpha \mathop \in I} S_\alpha$ is the union of $\family {S_\alpha}$.

Proof:
Let $\beta \in I$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = \beta
      | o = \in
      | r = I
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \set \beta
      | o = \subseteq
      | r = I
      | c = Singleton of Element is Subset
}}
{{eqn | ll= \leadsto
      | l = \bigcup \set {S_\beta}
      | o = \subseteq
      | r = \bigcup_{\alpha \mathop \in I} S_\alpha
      | c = Union of Subset of Family is Subset of Union of Family
}}
{{eqn | ll= \leadsto
      | l = S_\beta
      | o = \subseteq
      | r = \bigcup_{\alpha \mathop \in I} S_\alpha
      | c = {{Defof|Set Union|subentry = Family of Sets}}
}}
{{end-eqn}}
So it follows that:
:$\ds \forall \beta \in I: S_\beta \subseteq \bigcup_{\alpha \mathop \in I} S_\alpha$
{{qed}}
Theorem: Reverse Fatou's Lemma/Positive Measurable Functions

Let $\sequence {f_n}_{n \mathop \in \N} \in \MM_{\overline \R}^+$, $f_n: X \to \overline \R$ be a sequence of positive measurable functions.
Suppose that there exists a positive measurable function $f: X \to \overline \R$ such that:
:$\ds \int f \rd \mu < +\infty$
:$\forall n \in \N: f_n \le f$
where $\le$ signifies a pointwise inequality.
Let $\ds \limsup_{n \mathop \to \infty} f_n: X \to \overline \R$ be the pointwise limit superior of the $f_n$.
Then:
:$\ds \limsup_{n \mathop \to \infty} \int f_n \rd \mu \le \int \limsup_{n \mathop \to \infty} f_n \rd \mu$
where:
:the integral sign denotes $\mu$-integration
:the {{LHS}} limit superior is taken in the extended real numbers $\overline \R$.

Proof:
{{ProofWanted}}
{{Namedfor|Pierre Joseph Louis Fatou|cat = Fatou}}
Theorem: Monotone Convergence Theorem (Measure Theory)

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $u : X \to \overline \R_{\ge 0}$ be a positive $\Sigma$-measurable function. 
Let $\sequence {u_n}_{n \mathop \in \N}$ be an sequence of positive $\Sigma$-measurable functions $u_n : X \to \overline \R_{\ge 0}$ such that: 
:$\map {u_i} x \le \map {u_j} x$ for all $i \le j$
and:
:$\ds \map u x = \lim_{n \mathop \to \infty} \map {u_n} x$
hold for $\mu$-almost all $x \in X$. 
Then:
:$\ds \int u \rd \mu = \lim_{n \mathop \to \infty} \int u_n \rd \mu$

Proof:
First suppose that: 
:$\map {u_i} x \le \map {u_j} x$ for all $i \le j$
and:
:$\ds \map u x = \lim_{n \mathop \to \infty} \map {u_n} x$
for all $x \in X$.
From Integral of Positive Measurable Function is Monotone, we have that: 
:$\ds \int u_i \rd \mu \le \int u_j \rd \mu$ for all $i \le j$.
From Monotone Convergence Theorem (Real Analysis): Increasing Sequence, we have: 
:$u_i \le u$ for each $i$.
So, applying Integral of Positive Measurable Function is Monotone again we have: 
:$\ds \int u_i \rd \mu \le \int u \rd \mu$ for each $i$.
So: 
:the sequence $\ds \sequence {\int u_i \rd \mu}_{i \in \N}$ is increasing.
So, from Monotone Convergence Theorem (Real Analysis): Increasing Sequence and Unbounded Monotone Sequence Diverges to Infinity: Increasing, we have: 
:$\ds \sequence {\int u_i \rd \mu}_{i \in \N}$ converges, possibly to $+\infty$.
From Lower and Upper Bounds for Sequences, we also have: 
:$\ds \lim_{n \mathop \to \infty} \int u_n \rd \mu \le \int u \rd \mu$ 
We now aim to prove: 
:$\ds \int u \rd \mu \le \lim_{n \mathop \to \infty} \int u_n \rd \mu$
From Measurable Function is Pointwise Limit of Simple Functions, for each $n$ there exists a increasing sequence of positive simple functions $\sequence {u_{n, k} }_{k \mathop \in \N}$ such that: 
:$\ds u_n = \lim_{k \mathop \to \infty} u_{n, k}$
From Monotone Convergence Theorem (Real Analysis): Increasing Sequence, this is equivalent to: 
:$\ds u_n = \sup_{k \in \N} u_{n, k}$ 
Let: 
:$\ds g_n = \max \set {u_{1, n}, u_{2, n}, \ldots, u_{n, n} }$ 
for each $n$.
From Pointwise Maximum of Simple Functions is Simple, $g_n$ is a positive simple function for each $n \in \N$.
With a view to apply Integral of Positive Measurable Function as Limit of Integrals of Positive Simple Functions, we show that: 
:$\sequence {g_n}_{n \mathop \in \N}$ is increasing
and:
:$\ds \map u x = \lim_{n \to \infty} \map {g_n} x$ 
for each $x \in X$.
We also show that: 
:$\map {g_n} x \le \map {u_n} x$
for each $n \in \N$ and $x \in X$.
Theorem: Intersection is Associative/Family of Sets

Let $\family {S_i}_{i \mathop \in I}$ and $\family {I_\lambda}_{\lambda \mathop \in \Lambda}$ be indexed families of sets.
Let $\ds I = \bigcap_{\lambda \mathop \in \Lambda} I_\lambda$.
Then:
:$\ds \bigcap_{i \mathop \in I} S_i = \bigcap_{\lambda \mathop \in \Lambda} \paren {\bigcap_{i \mathop \in I_\lambda} S_i}$

Proof:
For every $\lambda \in \Lambda$, let $\ds T_\lambda = \bigcap_{i \mathop \in I_\lambda} S_i$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcap_{i \mathop \in I} S_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall i \in I
      | l = x
      | o = \in
      | r = S_i
      | c = {{Defof|Intersection of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall \lambda \in \Lambda: \forall i \in I_\lambda
      | l = x
      | o = \in
      | r = S_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall \lambda \in \Lambda
      | l = x
      | o = \in
      | r = \bigcap_{i \mathop \in I_\lambda} S_i = T_\lambda
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{\lambda \mathop \in \Lambda} T_\lambda
      | c = 
}}
{{end-eqn}}
Thus:
:$\ds \bigcap_{i \mathop \in I} S_i = \bigcap_{\lambda \mathop \in \Lambda} T_\lambda = \bigcap_{\lambda \mathop \in \Lambda} \paren {\bigcap_{i \mathop \in I_\lambda} S_i}$
{{qed}}
Theorem: Intersection is Associative/Family of Sets

Let $\family {S_i}_{i \mathop \in I}$ and $\family {I_\lambda}_{\lambda \mathop \in \Lambda}$ be indexed families of sets.
Let $\ds I = \bigcap_{\lambda \mathop \in \Lambda} I_\lambda$.
Then:
:$\ds \bigcap_{i \mathop \in I} S_i = \bigcap_{\lambda \mathop \in \Lambda} \paren {\bigcap_{i \mathop \in I_\lambda} S_i}$

Proof:
{{begin-eqn}}
{{eqn | l = \bigcap_{i \mathop \in I} S_i
      | r = \map \complement {\map \complement {\bigcap_{i \mathop \in I} S_i} }
      | c = Complement of Complement
}}
{{eqn | r = \map \complement {\bigcup_{i \mathop \in I} \map \complement {S_i} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Intersection
}}
{{eqn | r = \map \complement {\bigcup_{\lambda \mathop \in \Lambda} \paren {\bigcup_{i \mathop \in I_\lambda} \map \complement {S_i} } }
      | c = General Associativity of Set Union
}}
{{eqn | r = \map \complement {\bigcup_{\lambda \mathop \in \Lambda} \paren {\map \complement {\bigcap_{i \mathop \in I_\lambda} S_i} } }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Intersection
}}
{{eqn | r = \bigcap_{\lambda \mathop \in \Lambda} \paren {\map \complement {\map \complement {\bigcap_{i \mathop \in I_\lambda} S_i} } }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Union
}}
{{eqn | r = \bigcap_{\lambda \mathop \in \Lambda} \paren {\bigcap_{i \mathop \in I_\lambda} S_i}
      | c = Complement of Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Union is Associative/Family of Sets

Let $\family {S_i}_{i \mathop \in I}$ and $\family {I_\lambda}_{\lambda \mathop \in \Lambda}$ be indexed families of sets.
Let $\ds I = \bigcup_{\lambda \mathop \in \Lambda} I_\lambda$ denote the union of  $\family {I_\lambda}_{\lambda \mathop \in \Lambda}$.
Then:
:$\ds \bigcup_{i \mathop \in I} S_i = \bigcup_{\lambda \mathop \in \Lambda} \paren {\bigcup_{i \mathop \in I_\lambda} S_i}$

Proof:
For every $\lambda \in \Lambda$, let $\ds T_\lambda = \bigcup_{i \mathop \in I_\lambda} S_i$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcup_{i \mathop \in I} S_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists i \in I
      | l = x
      | o = \in
      | r = S_i
      | c = {{Defof|Union of Family}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists \lambda \in \Lambda: \exists i \in I_\lambda
      | l = x
      | o = \in
      | r = S_i
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \exists \lambda \in \Lambda
      | l = x
      | o = \in
      | r = \bigcup_{i \mathop \in I_\lambda} S_i = T_\lambda
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcup_{\lambda \mathop \in \Lambda} T_\lambda
      | c = 
}}
{{end-eqn}}
Thus:
:$\ds \bigcup_{i \mathop \in I} S_i = \bigcup_{\lambda \mathop \in \Lambda} T_\lambda = \bigcup_{\lambda \mathop \in \Lambda} \paren {\bigcup_{i \mathop \in I_\lambda} S_i}$
{{qed}}
Theorem: Continuity under Integral Sign

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $U$ be a non-empty open set of a metric space.
Let $f: U \times X \to \R$ be a mapping satisfying:
:$(1): \quad$ For all $\lambda \in U$, the mapping $x \mapsto \map f {\lambda, x}$ is $\mu$-integrable
:$(2): \quad$ For $\mu$-almost all $x \in X$, the mapping $\lambda \mapsto \map f {\lambda, x}$ is continuous
:$(3): \quad$ There exists a $\mu$-integrable $g: X \to \R$ such that:
::::$\forall \tuple {\lambda, x} \in U \times X: \size {\map f {\lambda, x} } \le \map g x$
Then the mapping $h: U \to \R$ defined by:
:$\ds \map h \lambda := \int \map f {\lambda, x} \map {\rd \mu} x$
is continuous.

Proof:
Let $\lambda_0 \in U$ be arbitrary.
Let $\sequence {\lambda_n}_{n \mathop \ge 1}$ be a sequence in $U$ which converges to $\lambda_0$.
Define the sequence of functions $f_n: X \to \R$, for $n = 0$ and $n \ge 1$ by $\map {f_n} x = \map f {\lambda_n, x}$.
By hypothesis $(1)$, for each $n \ge 1$, the function $f_n$ is $\mu$-integrable.
By hypothesis $(2)$, and by Sequential Continuity is Equivalent to Continuity in Metric Space, we have:
:$\ds \map {f_0} x = \lim_{n \mathop \to \infty} \map {f_n} x$
for $\mu$-almost all $x \in X$.
By hypothesis $(3)$, we have:
:$\size {\map {f_n} x} \le \map g x$
for all $x \in X$ and all $n \ge 1$.
Therefore by Lebesgue's Dominated Convergence Theorem:
:$\ds \lim_{n \mathop \to \infty} \int f_n \rd \mu = \int f_0 \rd \mu$
That is:
:$\ds \lim_{n \mathop \to \infty} \int \map f {\lambda_n, x} \rd \mu = \int \map f {\lambda_0, x} \rd \mu$
or in terms of $h$:
:$\ds \lim_{n \mathop \to \infty} \map h {\lambda_n} = \map h {\lambda_0}$
Since the sequence $\sequence {\lambda_n}_{n \mathop \ge 1}$ was arbitrary, by Sequential Continuity is Equivalent to Continuity in Metric Space this shows that $h$ is continuous at $\lambda_0 \in U$.
But $\lambda_0 \in U$ was arbitrary, so $h$ is continuous in $U$.
{{qed}}
Theorem: Gamma Function is Continuous on Positive Reals

Let $\Gamma: \R_{>0} \to \R$ be the Gamma function, restricted to the strictly positive real numbers.
Then $\Gamma$ is continuous.

Proof:
Let $0 < \alpha < a \le x \le y \le b < \beta$.
Let $0 < \delta < \Delta$.
Then:
:$(1): \quad \ds \size {\int_\delta^\Delta t^{x - 1} e^{-t} \rd t - \int_\delta^\Delta t^{y - 1} e^{-t} } \le \int_\delta^\Delta \paren {t^{x - 1} - t^{y - 1} }e^{-t} \rd t$
{{explain|why?}}
From the Mean Value Theorem:
:$(2): \quad \dfrac {t^{x - 1} - t^{y - 1} }{x - y} = \paren {\ln t} t^{\xi - 1}$
for some $\xi \in \R$ such that $x \le \xi \le y$.
Let $r \in \R_{>0}$.
Then:
:$t^{-r} \ln t \to 0$ as $t \to \infty$
:$t^r \ln t \to 0$ as $t \to 0^+$
From $(2)$ it follows that:
:$\exists H \in \R: \size {t^{x - 1} - t^{y - 1} } \le H \paren {t^{\alpha - 1} + t^{\beta - 1} } \size {x - y}$
From $(1)$ it follows that:
:$\size {\map \Gamma x - \map \Gamma y} \le H \size {x - y} \paren {\map \Gamma \alpha - \map \Gamma \beta}$
The result follows from the Squeeze Theorem.
{{qed}}
{{explain|Quite a few steps in the above need to be filled in and/or justified with links to results}}
Theorem: Log of Gamma Function is Convex on Positive Reals

Let $\Gamma: \R_{>0} \to \R$ be the Gamma function, restricted to the strictly positive real numbers.
Let $\ln$ denote the natural logarithm function.
Then the composite mapping $\ln \circ \operatorname \Gamma$ is a convex function.

Proof:
By definition, the Gamma function $\Gamma: \R_{> 0} \to \R$ is defined as:
:$\ds \map \Gamma z = \int_0^{\infty} t^{z - 1} e^{-t} \rd t$
:$\forall z > 0: \map \Gamma z > 0$, as an integral of a strictly positive function in $t$.
{{explain|A separate page is needed for the above statement}}
The function is smooth according to Gamma Function is Smooth on Positive Reals, and
:$\ds \forall k \in \N: \map {\Gamma^{\paren k} } z = \int_0^{\infty} \map \ln t^k t^{z - 1} e^{-t} \rd t$
{{explain|Prove the above}}
Let $\map f z := \map \ln {\map \Gamma z}$.
:$f$ is smooth because $\Gamma$ is smooth and positive.
{{explain|A link to why this follows}}
Then:
:$\map {f'} z = \dfrac {\map {\Gamma'} z} {\map \Gamma z}$
:$\map {f^{\paren 2} } z = \dfrac {\map {\Gamma^{\paren 2} } z \map \Gamma z - \map {\Gamma'} z^2} {\map \Gamma z^2} > 0$
{{explain|Invoke the result that this comes from: Derivative of Quotient or whatever it is}}
The numerator is positive due to the Cauchy-Bunyakovsky-Schwarz Inequality for Inner Product Spaces applied to the scalar products:
:$\ds \innerprod g h = \int_0^\infty \map g t \map h t t^{z - 1} e^{-t} \rd t \quad \forall z \gt 0$
applied to $g = \ln$ and $h = 1$.
:$\forall z \in \R_{>0}: \map {f^{\paren 2} } z > 0 \implies f$ is convex.
{{qed}}
Theorem: Log of Gamma Function is Convex on Positive Reals

Let $\Gamma: \R_{>0} \to \R$ be the Gamma function, restricted to the strictly positive real numbers.
Let $\ln$ denote the natural logarithm function.
Then the composite mapping $\ln \circ \operatorname \Gamma$ is a convex function.

Proof:
The strategy is to show that:
:$\map \ln {\map \Gamma {\dfrac x 2 + \dfrac y 2} } \le \dfrac 1 2 \map \ln {\map \Gamma x} + \dfrac 1 2 \map \ln {\map \Gamma y}$
Let $0 < \delta < \Delta$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {\int_\delta^\Delta t^{\paren {x + y - 2} / 2} e^{-t} \rd t}^2
      | r = \paren {\int_\delta^\Delta \paren {t^{\paren {x - 1} / 2} e^{-t/2} } \paren {t^{\paren {y - 1} / 2} e^{-t/2} } \rd t}^2
      | c = 
}}
{{eqn | n = 1
      | o = \le
      | r = \paren {\int_\delta^\Delta t^{x - 1} e^{-t} \rd t} \paren {\int_\delta^\Delta t^{y - 1} e^{-t} \rd t}
      | c = Cauchy-Bunyakovsky-Schwarz Inequality for Definite Integrals
}}
{{end-eqn}}
Letting $\delta \to 0$ and $\Delta \to \infty$, $(1)$ becomes equivalent to:
:$\paren {\map \Gamma {\dfrac {x + y} 2} }^2 \le \paren {\map \Gamma x} \paren {\map \Gamma y}$
{{begin-eqn}}
{{eqn | l = \paren {\map \Gamma {\dfrac {x + y} 2} }^2
      | o = \le
      | r = \paren {\map \Gamma x} \paren {\map \Gamma y}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\paren {\map \Gamma {\dfrac {x + y} 2} }^2}
      | o = \le
      | r = \map \ln {\paren {\map \Gamma x} \paren {\map \Gamma y} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 \map \ln {\map \Gamma {\dfrac {x + y} 2} }
      | o = \le
      | r = \map \ln {\map \Gamma x} + \map \ln {\map \Gamma y}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\map \Gamma {\dfrac x 2 + \dfrac y 2} }
      | o = \le
      | r = \frac 1 2 \map \ln {\map \Gamma x} + \frac 1 2 \map \ln {\map \Gamma y}
      | c = 
}}
{{end-eqn}}
The result follows by definition of convex function.
{{qed}}
Theorem: Log of Gamma Function is Convex on Positive Reals

Let $\Gamma: \R_{>0} \to \R$ be the Gamma function, restricted to the strictly positive real numbers.
Let $\ln$ denote the natural logarithm function.
Then the composite mapping $\ln \circ \operatorname \Gamma$ is a convex function.

Proof:
The strategy is to use the Euler Form of the Gamma function and directly calculate the second derivative of $\ln \map \Gamma z$.
{{begin-eqn}}
{{eqn | l = \map \Gamma z
      | r = \lim_{m \mathop \to \infty} \frac {m^z m!} {z \paren {z + 1} \paren {z + 2} \dotsm \paren {z + m} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d^2 \ln \map \Gamma z} {\d z^2} 
      | r = \dfrac {\d^2} {\d z^2} \map \ln {\lim_{m \mathop \to \infty} \frac {m^z m!} {z \paren {z + 1} \paren {z + 2} \dotsm \paren {z + m} } }
      | c = 
}}
{{eqn | r = \lim_{m \mathop \to \infty} \dfrac {\d^2} {\d z^2} \map \ln {\frac {m^z m!} {z \paren {z + 1} \paren {z + 2} \dotsm \paren {z + m} } }
      | c = 
}}
{{end-eqn}}
The limit interchange is justified because Gamma Function is Smooth on Positive Reals.
{{begin-eqn}}
{{eqn | l = \lim_{m \mathop \to \infty} \dfrac {\d^2} {\d z^2} \paren {z \map \ln m + \map \ln {m!} - \sum_{n \mathop = 0}^m \map \ln {z + n} }
      | r = \lim_{m \mathop \to \infty} \sum_{n \mathop = 0}^m \dfrac 1 {\paren {z + n}^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d^2 \ln \map \Gamma z} {\d z^2}
      | r = \sum_{n \mathop = 0}^\infty \dfrac 1 {\paren {z + n}^2} > 0
      | c = 
}}
{{end-eqn}}
Logarithmic convexity then follows from Real Function with Strictly Positive Second Derivative is Strictly Convex.
{{qed}}
Theorem: Pratt's Lemma

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let:
:$\sequence {g_n}_{n \mathop \in \N}$
:$\sequence {G_n}_{n \mathop \in \N}$
:$\sequence {f_n}_{n \mathop \in \N}$
be sequences of $\mu$-integrable functions.
Let the pointwise limits:
:$\ds f := \lim_{n \mathop \to \infty} f_n$
:$\ds g := \lim_{n \mathop \to \infty} g_n$
:$\ds G := \lim_{n \mathop \to \infty} G_n$
exist.
Let $g$ and $G$ be $\mu$-integrable.
Suppose that, for all $x \in X$ and $n \in \N$:
:$\map {g_n} x \le \map {f_n} x \le \map {G_n} x$
Finally, suppose the following hold:
:$\ds \lim_{n \mathop \to \infty} \int g_n \rd \mu = \int g \rd \mu$
:$\ds \lim_{n \mathop \to \infty} \int G_n \rd \mu = \int G \rd \mu$
Then:
:$\ds \lim_{n \mathop \to \infty} \int f_n \rd \mu = \int f \rd \mu$
and the latter is finite.

Proof:
{{ProofWanted}}
{{Namedfor|John Winsor Pratt|cat = Pratt}}
Theorem: Hölder's Inequality for Integrals

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $p, q \in \R_{>0}$ such that $\dfrac 1 p + \dfrac 1 q = 1$.
{{improve|the assumption should read $p,q\in\R_{>0}\cup\set{+\infty}$.<br/>Suggestion: make a page for defining $p,q$ as satisfying this relation, including the pair $\tuple{1,\infty}$}}
Let $f \in \map {\LL^p} \mu, f: X \to \R$, and $g \in \map {\LL^q} \mu, g: X \to \R$, where $\LL$ denotes Lebesgue space.
Then their pointwise product $f g$ is $\mu$-integrable, that is:
:$f g \in \map {\LL^1} \mu$
and:
{{begin-eqn}}
{{eqn | l = \norm {f g}_1
      | r = \int \size {f g} \rd \mu
      | c = 
}}
{{eqn | o = \le
      | r = \paren {\int \size f^p \rd \mu}^{1 / p} \paren {\int \size g^q \rd \mu}^{1 / q}
      | c = 
}}
{{eqn | r = \norm f_p \cdot \norm g_q
      | c = 
}}
{{end-eqn}}
where:
:$\size {f g}$ denotes the absolute value function applied to the pointwise product of $f$ and $g$
:the $\norm {\, \cdot \,}_p$ signify $p$-seminorms.

Proof:
Let $x \in X$.
Let:
:$a_x := \dfrac {\size {\map f x} } {\norm f_p}$
and:
:$b_x := \dfrac {\size {\map g x} } {\norm g_q}$
Applying Young's Inequality for Products to $a_x$ and $b_x$:
:$\dfrac {\size {\map f x \map g x} } {\norm f_p \cdot \norm g_q} \le \dfrac {\size {\map f x}^p} {p \norm f_p^p} + \dfrac {\size {\map g x}^q} { q \norm g_q^q}$
By Integral of Positive Measurable Function is Monotone, integrating both sides of this inequality over x yields:
:$\ds \dfrac {\int \size {\map f x \map g x} \map \mu {\d x} } {\norm f_p \cdot \norm g_q} \le \frac {\norm f_p^p} {p \norm f_p^p} + \frac {\norm g_p^q} {q \norm g_q^q} = \frac 1 p + \frac 1 q = 1$
so:
:$\ds \int \size {\map f x \map g x} \map \mu {\d x} \le \norm f_p \cdot \norm g_q$
If we have equality, then:
:$\ds \int \paren {\frac {\size {\map f x}^p} {p \norm f_p^p} + \frac {\size {\map g x}^q} {q \norm g_q^q} - \frac {\size {\map f x \map g x} } {\norm f_p \cdot \norm g_q} } \map \mu {\d x} = 0$
As:
:$\dfrac {\size {\map f x}^p} {p \norm f_p^p} + \dfrac {\size {\map g x}^q} {q \norm g_q^q} - \dfrac {\size {\map f x \map g x} } {\norm f_p \cdot \norm g_q} \ge 0$
it follows from Measurable Function Zero A.E. iff Absolute Value has Zero Integral that:
:$\dfrac {\size {\map g x}^p} {p \norm f_p^p} + \dfrac {\size {\map g x}^q} {q \norm g_q^q} = \dfrac {\size {\map f x \map g x} } {\norm f_p \cdot \norm g_q}$ a.e.
By Young's Inequality for Products, we have equality {{iff}} $b_x = {a_x}^{p - 1}$.
Raising both sides to the $q$th power gives:
:$\dfrac {\size {\map g x}^p} {\norm f_p^p} = \dfrac {\size {\map g x}^q} {\norm g_q^q}$
as $\paren {p - 1} q = p$. 
{{qed}}
Theorem: Hölder's Inequality for Integrals/Equality

:$\ds \int \size {f g} \rd \mu = \norm f_p \cdot \norm g_q$
holds {{iff}}, for $\mu$-almost all $x \in X$:
:$\dfrac {\size {\map f x}^p} {\norm f_p^p} = \dfrac {\size {\map g x}^q} {\norm g_q^q}$
{{questionable|What if e.g. $f{{=}}0$ and $g{{=}}1$? The equality holds, trivially, but how to read the necessary condition?}}
{{help|Whoever is on the case, note that the equality condition as given in both Abramowitz & Stegun and Spiegel is as follows, but then they don't go into that fancy-pants $\norm f_p$ notation either, they specifically use the notation $\ds \paren {\int_a^b {\size {\map f x} }^p \rd x}^{1 / p}$ which is more accessible, although admittedly in the context of a Riemann integral rather than a Lebesgue one. Input needed from someone who a) is familiar with the theorem in the general Lebesgue space and b) is motivated to bring the exposition back down to earth by explaining what $\norm f_p$ actually means in undergrad language.}}
:$\dfrac {\size {\map f x}^{p - 1} } {\size {\map g x} } = c$
for some $c \in \R$.

Proof:
{{ProofWanted}}
{{Namedfor|Otto Ludwig Hölder|cat = Hölder}}
Theorem: Condition for Membership of Equivalence Class

Let $\RR$ be an equivalence relation on a set $S$.
Let $\eqclass x \RR$ denote the $\RR$-equivalence class of $x$.
Then:
:$\forall y \in S: y \in \eqclass x \RR \iff \tuple {x, y} \in \RR$

Proof:
From the definition of an equivalence class:
:$\eqclass x \RR = \set {y \in S: \tuple {x, y} \in \RR}$
Let $y \in S$ such that $y \in \eqclass x \RR$.
Then by definition $\tuple {x, y} \in \RR$.
Similarly, let $\tuple {x, y} \in \RR$.
Again by definition, $y \in \eqclass x \RR$.
{{qed}}
Theorem: Linearly Ordered Space is Normal

Let $T = \struct {S, \preceq, \tau}$ be a linearly ordered space.
Then $\struct {S, \tau}$ is normal.

Proof:
From Linearly Ordered Space is Completely Normal, $\struct {S, \tau}$ is a completely normal space.
The result follows from Completely Normal Space is Normal.
{{qed}}
Category:Linearly Ordered Spaces
Category:Examples of Normal Spaces
j3o46fu7v2jy4y4a5ro1pxdq3n8ub2c