nyuuzyou/wikis huggingface dataset:
Reductio ad Absurdum/Variant 2

== Theorem ==
If, by making an assumption $\neg p$, we can infer a contradiction as a consequence, then we may infer $p$:
:$\neg p \implies \paren {q \land \neg q} \vdash p$
== Proof 1 ==
== Proof by Truth Table ==
== Linguistic Note ==
== Sources ==
* : $\S 1.12$: Valid Arguments
Category:Reductio ad Absurdum
Reductio ad Absurdum/Variant 2/Proof by Truth Table

== Theorem ==
== Proof==
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccccc||c|} \hline
\neg & p & \implies & (q & \land & \neg & q) & p \\
\hline
\T & \F & \F & \F & \F & \T & \F & \F \\
\T & \F & \F & \T & \F & \F & \T & \F \\
\F & \T & \T & \F & \F & \T & \F & \T \\
\F & \T & \T & \T & \F & \F & \T & \T \\
\hline
\end{array}$
Category:Truth Table Proofs
Category:Reductio ad Absurdum
Reductio ad Absurdum for Hilbert Proof System Instance 1 for Predicate Logic

== Theorem ==
Let $\LL$ be the language of predicate logic.
Let $\mathscr H$ be instance 1 of a Hilbert proof system for predicate logic.
Then Reductio ad Absurdum is a derived rule of $\mathscr H$:
== Proof ==
Suppose that $\Sigma, \neg \phi \vdash_{\mathscr H} \bot$.
By Contradictory Antecedent, $\bot \implies \phi$ is a tautology.
Therefore, $\bot \implies \phi$ is an axiom of $\mathscr H$, so that by Modus Ponendo Ponens:
:$\Sigma, \neg \phi \vdash_{\mathscr H} \phi$
By Deduction Theorem for Hilbert Proof System for Predicate Logic, it follows that:
:$\Sigma \vdash_{\mathscr H} \neg \phi \implies \phi$
Next, note that $\paren{ \neg \phi \implies \phi } \implies \phi$ is a tautology and so an axiom of $\mathscr H$.
Hence by Modus Ponendo Ponens:
:$\Sigma \vdash_{\mathscr H} \phi$
== Sources ==
* : $\text{II}.11$ Some Strategies for Constructing Proofs: Lemma $\text{II}.11.4$
Category:Reductio ad Absurdum
Category:Hilbert Proof System Instance 1 for Predicate Logic
Reduction Formula (Trigonometry)/Examples

== Examples of Reduction Formulae in context of Trigonometry ==
=== Tangent of $90 \degrees \pm \theta$ ===
=== Sine of $90 \degrees \pm \theta$ ===
=== Cosine of $90 \degrees \pm \theta$ ===
=== Tangent of $180 \degrees \pm \theta$ ===
=== Sine of $180 \degrees \pm \theta$ ===
=== Cosine of $180 \degrees \pm \theta$ ===
=== Tangent of $270 \degrees \pm \theta$ ===
=== Sine of $270 \degrees \pm \theta$ ===
=== Cosine of $270 \degrees \pm \theta$ ===
Category:Examples of Reduction Formulae (Trigonometry)
Reduction Formula (Trigonometry)/Examples/Cosine of Right Angle plus or minus Angle

== Example of Reduction Formula in context of Trigonometry ==
:$\map \cos {90 \degrees \pm \theta} = \mp \sin \theta$
== Proof ==
From Cosine of Angle plus Right Angle:
:$\map \cos {90 \degrees + \theta} = -\sin \theta$
From Cosine of Complement equals Sine:
:$\map \cos {90 \degrees - \theta} = \sin \theta$
== Sources ==
* 
* 
Category:Examples of Reduction Formulae (Trigonometry)
Category:Cosine Function
Reduction Formula (Trigonometry)/Examples/Cosine of Straight Angle plus or minus Angle

== Example of Reduction Formula in context of Trigonometry ==
:$\map \cos {180 \degrees \pm \theta} = -\cos \theta$
== Proof ==
From Cosine of Angle plus Straight Angle:
:$\map \cos {180 \degrees + \theta} = -\cos \theta$
From Cosine of Supplementary Angle:
:$\map \cos {180 \degrees - \theta} = -\cos \theta$
== Sources ==
* 
* 
Category:Examples of Reduction Formulae (Trigonometry)
Category:Cosine Function
Reduction Formula (Trigonometry)/Examples/Cosine of Three Right Angles plus or minus Angle

== Example of Reduction Formula in context of Trigonometry ==
:$\map \cos {270 \degrees \pm \theta} = \pm \sin \theta$
== Proof ==
From Cosine of Angle plus Three Right Angles:
:$\map \cos {270 \degrees + \theta} = \sin \theta$
From Cosine of Three Right Angles minus Angle:
:$\map \cos {270 \degrees - \theta} = -\sin \theta$
== Sources ==
* 
* 
Category:Examples of Reduction Formulae (Trigonometry)
Category:Cosine Function
Reduction Formula (Trigonometry)/Examples/Sine of Right Angle plus or minus Angle

== Example of Reduction Formula in context of Trigonometry ==
:$\map \sin {90 \degrees \pm \theta} = \cos \theta$
== Proof ==
From Sine of Angle plus Right Angle:
:$\map \sin {90 \degrees + \theta} = \cos \theta$
From Sine of Complement equals Cosine:
:$\map \sin {90 \degrees - \theta} = \cos \theta$
== Sources ==
* 
* 
Category:Examples of Reduction Formulae (Trigonometry)
Category:Sine Function
Reduction Formula (Trigonometry)/Examples/Sine of Straight Angle plus or minus Angle

== Example of Reduction Formula in context of Trigonometry ==
:$\map \sin {180 \degrees \pm \theta} = \mp \sin \theta$
== Proof ==
From Sine of Angle plus Straight Angle:
:$\map \sin {180 \degrees + \theta} = -\sin \theta$
From Sine of Supplementary Angle:
:$\map \sin {180 \degrees - \theta} = \sin \theta$
== Sources ==
* 
* 
Category:Examples of Reduction Formulae (Trigonometry)
Category:Sine Function
Reduction Formula (Trigonometry)/Examples/Sine of Three Right Angles plus or minus Angle

== Example of Reduction Formula in context of Trigonometry ==
:$\map \sin {270 \degrees \pm \theta} = -\cos \theta$
== Proof ==
From Sine of Angle plus Three Right Angles:
:$\map \sin {270 \degrees + \theta} = -\cos \theta$
From Sine of Three Right Angles minus Angle:
:$\map \sin {270 \degrees - \theta} = -\cos \theta$
== Sources ==
* 
* 
Category:Examples of Reduction Formulae (Trigonometry)
Category:Sine Function
Reduction Formula (Trigonometry)/Examples/Tangent of Right Angle plus or minus Angle

== Example of Reduction Formula in context of Trigonometry ==
:$\map \tan {90 \degrees \pm \theta} = \mp \cot \theta$
== Proof ==
From Tangent of Angle plus Right Angle:
:$\map \tan {90 \degrees + \theta} = -\cot \theta$
From Tangent of Complement equals Cotangent:
:$\map \tan {90 \degrees - \theta} = \cot \theta$
== Sources ==
* 
* 
Category:Examples of Reduction Formulae (Trigonometry)
Category:Tangent Function
Reduction Formula (Trigonometry)/Examples/Tangent of Straight Angle plus or minus Angle

== Example of Reduction Formula in context of Trigonometry ==
:$\map \tan {180 \degrees \pm \theta} = \pm \tan \theta$
== Proof ==
From Tangent of Angle plus Straight Angle:
:$\map \tan {180 \degrees + \theta} = \tan \theta$
From Tangent of Supplementary Angle:
:$\map \tan {180 \degrees - \theta} = -\tan \theta$
== Sources ==
* 
* 
Category:Examples of Reduction Formulae (Trigonometry)
Category:Tangent Function
Reduction Formula (Trigonometry)/Examples/Tangent of Three Right Angles plus or minus Angle

== Example of Reduction Formula in context of Trigonometry ==
:$\map \tan {270 \degrees \pm \theta} = \mp \cot \theta$
== Proof ==
From Tangent of Angle plus Three Right Angles:
:$\map \tan {270 \degrees + \theta} = -\cot \theta$
From Tangent of Three Right Angles minus Angle:
:$\map \tan {270 \degrees - \theta} = \cot \theta$
== Sources ==
* 
* 
Category:Examples of Reduction Formulae (Trigonometry)
Category:Tangent Function
Reduction Formula for Definite Integral of Power of Cosine

== Theorem ==
Let $n \in \Z_{> 0}$ be a positive integer.
Let $I_n$ be defined as:
:$\ds I_n = \int_0^{\frac \pi 2} \cos^n x \rd x$
Then $\sequence {I_n}$ is a decreasing sequence of real numbers which satisfies:
:$n I_n = \paren {n - 1} I_{n - 2}$
Thus:
:$I_n = \dfrac {n - 1} n I_{n - 2}$
is a reduction formula for $I_n$.
=== Corollary 1 ===
=== Corollary 2 ===
== Proof ==
From Shape of Cosine Function:
:$\forall x \in \closedint 0 {\dfrac \pi 2}: 0 \le \cos x \le 1$
So, on the same interval:
:$0 \le \cos^{n + 1} x \le \cos^n x$
Therefore:
:$\forall n \in \N: 0 < I_{n + 1} < I_n$
From Reduction Formula for Integral of Power of Cosine:
:$\ds \int \cos^n x \rd x = \dfrac {\cos^{n - 1} x \sin x} n + \dfrac {n - 1} n \int \cos^{n - 2} x \rd x$
Thus:
== Also see ==
* Reduction Formula for Definite Integral of Power of Sine
Category:Reduction Formula for Definite Integral of Power of Cosine
Category:Reduction Formulae (Calculus)
Category:Definite Integrals involving Cosine Function
Reduction Formula for Definite Integral of Power of Sine

== Theorem ==
Let $n \in \Z_{> 0}$ be a positive integer.
Let $I_n$ be defined as:
:$\ds I_n = \int_0^{\frac \pi 2} \sin^n x \rd x$
Then $\sequence {I_n}$ is a decreasing sequence of real numbers which satisfies:
:$n I_n = \paren {n - 1} I_{n - 2}$
Thus:
:$I_n = \dfrac {n - 1} n I_{n - 2}$
is a reduction formula for $I_n$.
=== Corollary 1 ===
=== Corollary 2 ===
== Proof ==
From Shape of Sine Function:
:$\forall x \in \closedint 0 {\dfrac \pi 2}: 0 \le \sin x \le 1$
and so on the same interval:
:$0 \le \sin^{n + 1} x \le \sin^n x$
therefore:
:$\forall n \in \N: 0 < I_{n + 1} < I_n$
From Reduction Formula for Integral of Power of Sine:
:$\ds \int \sin^n x \rd x = \dfrac {n - 1} n \int \sin^{n - 2} x \rd x - \dfrac {\sin^{n - 1} x \cos x} n$
Thus:
== Also see ==
* Reduction Formula for Definite Integral of Power of Cosine
== Sources ==
* : $\S 17.4 \ (1)$
Category:Reduction Formula for Definite Integral of Power of Sine
Category:Reduction Formulae (Calculus)
Category:Definite Integrals involving Sine Function
Reduction Formula for Integral of Power of Cosine

== Theorem ==
Let $n \in \Z_{> 0}$ be a (strictly) positive integer.
Let:
:$I_n := \ds \int \cos^n x \rd x$
Then:
:$I_n = \dfrac {\cos^{n - 1} x \sin x} n + \dfrac {n - 1} n I_{n - 2}$
is a reduction formula for $\ds \int \cos^n x \rd x$.
=== Corollary ===
== Proof ==
With a view to expressing the problem in the form:
:$\ds \int u \frac {\rd v} {\rd x} \rd x = u v - \int v \frac {\rd u} {\rd x} \rd x$
let:
and let:
Then:
== Also see ==
* Reduction Formula for Integral of Power of Sine
* Reduction Formula for Integral of Power of Tangent
== Sources ==
* : Appendix $8$: Integrals: Reduction Formulae
Category:Reduction Formula for Integral of Power of Cosine
Category:Reduction Formulae (Calculus)
Category:Primitives involving Cosine Function
Reduction Formula for Integral of Power of Cosine/Corollary

== Corollary to Reduction Formula for Integral of Power of Cosine ==
Let $n \in \Z_{> 0}$ be a (strictly) positive integer.
Let $a \in \R_{\ne 0}$ be a non-zero real number
Then:
:$\ds \int \cos^n a x \rd x = \dfrac {\cos^{n - 1} a x \sin a x} {a n} + \dfrac {n - 1} n \int \cos^{n - 2} a x \rd x$
is a reduction formula for $\ds \int \cos^n a x \rd x$.
== Proof ==
== Also see ==
* Primitive of $\sin^n a x$
* Primitive of $\tan^n a x$
* Primitive of $\cot^n a x$
* Primitive of $\sec^n a x$
* Primitive of $\csc^n a x$
== Sources ==
* : $\S 14$: Integrals involving $\sin a x$: $14.396$
* : Front endpapers: A Brief Table of Integrals: $61$.
* : Appendix: Table $3$: Reduction formulae
* : Appendix: Table $3$: Reduction formulae
Category:Reduction Formula for Integral of Power of Cosine
Category:Primitives involving Cosine Function
Reduction Formula for Integral of Power of Cosine/Mistake

== Source Work ==
:
:Appendix $8$: Integrals
::Reduction Formulae
== Mistake ==
:For $I_n = \int \cos^n x \rd x$, where $n \ge 2$, then
:::::$I_n = \dfrac {\cos^n x \sin x} n + \dfrac {n - 1} n I_{n - 2}$.''
== Correction ==
The correct expression is:
:::::$I_n = \dfrac {\cos^{n - 1} x \sin x} n + \dfrac {n - 1} n I_{n - 2}$
== Sources ==
* : Appendix $8$: Integrals: Reduction Formulae
Category:Mistakes/The Concise Oxford Dictionary of Mathematics
Reduction Formula for Integral of Power of Sine

== Theorem ==
Let $n \in \Z_{> 0}$ be a (strictly) positive integer.
Let:
:$I_n := \ds \int \sin^n x \rd x$
Then:
:$I_n = \dfrac {n - 1} n I_{n - 2} - \dfrac {\sin^{n - 1} x \cos x} n$
is a reduction formula for $\ds \int \sin^n x \rd x$.
=== Corollary ===
== Proof 1 ==
== Proof 2 ==
== Also see ==
* Reduction Formula for Integral of Power of Cosine
* Reduction Formula for Integral of Power of Tangent
== Sources ==
* : Chapter $\text {B}.12$: Wallis's Product
* : Appendix $8$: Integrals: Reduction Formulae
Category:Reduction Formula for Integral of Power of Sine
Category:Reduction Formulae (Calculus)
Category:Primitives involving Sine Function
Reduction Formula for Integral of Power of Sine/Corollary

== Corollary to Reduction Formula for Integral of Power of Sine ==
Let $n \in \Z_{> 0}$ be a (strictly) positive integer.
Let $a \in \R_{\ne 0}$ be a non-zero real number
Then:
:$\ds \int \sin^n a x \rd x = \dfrac {n - 1} n \int \sin^{n - 2} a x \rd x - \dfrac {\sin^{n - 1} a x \cos a x} {a n}$
is a reduction formula for $\ds \int \sin^n a x \rd x$.
== Proof ==
== Also see ==
* Primitive of $\cos^n a x$
* Primitive of $\tan^n a x$
* Primitive of $\cot^n a x$
* Primitive of $\sec^n a x$
* Primitive of $\csc^n a x$
== Sources ==
* : $\S 14$: Integrals involving $\sin a x$: $14.366$
* : Front endpapers: A Brief Table of Integrals: $60$.
* : Appendix: Table $3$: Reduction formulae
* : Appendix: Table $3$: Reduction formulae
Category:Reduction Formula for Integral of Power of Sine
Reduction Formula for Integral of Power of Sine/Mistake

== Source Work ==
:
:Appendix $8$: Integrals
::Reduction Formulae
== Mistake ==
:For $I_n = \int \sin^n x \rd x$, where $n \ge 2$, then
:::::$I_n = -\dfrac {\sin^n x \cos x} n + \dfrac {n - 1} n I_{n - 2}$.''
== Correction ==
The correct expression is:
:::::$I_n = -\dfrac {\sin^{n - 1} x \cos x} n + \dfrac {n - 1} n I_{n - 2}$
== Sources ==
* : Appendix $8$: Integrals: Reduction Formulae
Category:Mistakes/The Concise Oxford Dictionary of Mathematics
Reduction Formula for Integral of Power of Sine/Proof 1

== Theorem ==
== Proof ==
Let $n \ge 2$.
Let:
:$\ds I_n := \int \sin^n x \rd x$
Then:
thus demonstrating the identity for all $n \ge 2$.
When $n = 1$ this degenerates to:
From Primitive of Sine Function this shows that the identity still holds for $n = 1$.
Category:Reduction Formula for Integral of Power of Sine
Reduction Formula for Integral of Power of Sine/Proof 2

== Theorem ==
== Proof ==
With a view to expressing the problem in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
and let:
Then:
Category:Reduction Formula for Integral of Power of Sine
Reduction Formula for Integral of Power of Tangent

== Theorem ==
For all $n \in \Z_{> 1}$:
Let:
:$I_n := \ds \int \tan^n x \rd x$
Then:
:$I_n = \dfrac {\tan^{n - 1} x} {n - 1} - I_{n - 2}$
is a reduction formula for $\ds \int \tan^n x \rd x$.
== Proof ==
Let:
Then:
 
Hence the result.
== Also see ==
* Reduction Formula for Integral of Power of Sine
* Reduction Formula for Integral of Power of Cosine
== Sources ==
* : Appendix $8$: Integrals: Reduction Formulae
Category:Primitives involving Tangent Function
Category:Reduction Formulae (Calculus)
Reduction Formula for Power of x by Exponential of a x

== Theorem ==
:$\ds \int x^n e^{a x} \rd x = \frac {x^n e^{a x} } a - \dfrac n a \int x^{n - 1} e^{a x} \rd x$
for $n \in \Z_{>0}$, $a \in \R_{\ne 0}$.
== Proof ==
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
and let:
Then:
== Sources ==
* : $\S 14$: Integrals involving $e^{a x}$: $14.512$
* : Back endpapers: A Brief Table of Integrals: $105$.
* : Appendix: Table $3$: Reduction formulae
* : Appendix: Table $3$: Reduction formulae
Category:Primitive of Power of x by Exponential of a x
Category:Primitives involving Exponential Function
Reduction Formula for Power of x by General Exponential of a x

== Theorem ==
:$\ds \int x^n b^{a x} \rd x = \frac {x^n b^{a x} } {a \ln b} - \dfrac n {a \ln b} \int x^{n - 1} b^{a x} \rd x$
for $n \in \Z_{>0}$, $a \in \R_{\ne 0}$, $b > 0$, $b \ne 1$
== Proof ==
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
and let:
Then:
== Sources ==
* : Back endpapers: A Brief Table of Integrals: $106$.
Category:Primitives involving Exponential Function
Reduction Formula for Primitive of Product of Power with Exponential

== Theorem ==
Let $n \in \Z_{> 0}$ be a (strictly) positive integer.
Let:
:$I_n := \ds \int x^n e^x \rd x$
Then:
:$I_n = x^n e^x - n I_{n - 1}$
is a reduction formula for $\ds \int x^n e^x \rd x$.
== Proof ==
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
and let:
Then:
== Sources ==
* : Appendix $8$: Integrals: Reduction Formulae
Category:Reduction Formulae (Calculus)
Category:Primitives involving Exponential Function
Reduction Formula for Primitive of Product of Power with Power of Quadratic

== Theorem ==
Let $n \in \Z_{\ge 0}$ and $k \in \Z_{\ge 2}$.
Let:
:$I_{n, k} := \ds \int x^k \paren {x^2 + A x + B}^n \rd x$
Then:
:$I_{n, k} = \dfrac {x^{k - 1} \paren {x^2 + A x + B}^{n + 1} } {k + 2 n + 1} - \dfrac {B \paren {k - 1} } {k + 2 n + 1} I_{n, k - 2} - \dfrac {A \paren {k + n} } {k + 2 n + 1} I_{n, k - 1}$
is a reduction formula for $\ds \int x^k \paren {x^2 + A x + B}^n \rd x$.
== Proof ==
Let $h$ be the real function defined as:
:$\forall x \in \R: \map h x = x^2 + A x + B$
Thus we have:
:$I_{n, k} := \ds \int x^k \paren {\map h x}^n \rd x$
Then we have:
== Sources ==
* : Appendix $8$: Integrals: Reduction Formulae
* 
Category:Primitives involving a x squared plus b x plus c
Category:Reduction Formulae (Calculus)
Reduction Formula for Primitive of a x + b over Power of Quadratic

== Theorem ==
Let $n \in \Z_{\ge 2}$.
Let:
:$\map {I_n} {a, b} := \ds \int \dfrac {a x + b} {\paren {x^2 + A x + B}^n} \rd x$
Then:
:$\map {I_n} {a, b} = \dfrac {b A - 2 a B + \paren {2 b - a A} x} {\paren {n - 1} \paren {4 B - A^2} \paren {x^2 + A x + B}^n} + \dfrac {\paren {2 n - 3} \paren {2 b - a A} } {\paren {n - 1} \paren {4 B - A^2} } \map {I_{n - 1} }{0, 1}$
is a reduction formula for $\ds \int \dfrac {a x + b} {\paren {x^2 + A x + B}^n} \rd x$.
== Proof ==
We observe that:
:$(1): \quad \map {\dfrac \d {\d x} } {x^2 + A x + B} = 2 x + A$
Hence we obtain:
and so express:
Let $z = x^2 + A x + B$.
Then:
Hence we have:
Now let $h$ be the real function defined as:
:$\forall x \in \R: \map h x = x^2 + A x + B$
Thus we have:
:$\map {I_n} {a, b} := \ds \int \dfrac {a x + b} {\paren {\map h x}^n} \rd x$
Using Power Rule for Derivatives:
:$\map {\dfrac \d {\d x} } {\map h x} = 2 x + A$
and so:
The result follows after algebra.
== Sources ==
* : Appendix $8$: Integrals: Reduction Formulae
* 
Category:Primitives involving a x squared plus b x plus c
Category:Reduction Formulae (Calculus)
Reduction of Explicit ODE to First Order System

== Theorem ==
Let $\map {x^{\paren n} } t = \map F {t, x, x', \ldots, x^{\paren {n - 1} } }$, $\map x {t_0} = x_0$ be an explicit ODE with $x \in \R^m$.
Let there exist $I \subseteq \R$ such that there exists a unique particular solution:
:$x: I \to \R^m$
to this ODE.
Then there exists a system of first order ODEs:
:$y' = \map {\tilde F} {t, y}$
with $y = \tuple {y_1, \ldots, y_{m n} }^T \in \R^{m n}$ such that:
:$\tuple {\map {y_1} t, \ldots, \map {y_m} t} = \map x t$
for all $t \in I$ and $\map y {t_0} = x_0$.
== Proof ==
Define the mappings:
:$z_1, \ldots, z_n: I \to \R^m$
by:
:$z_j = x^{\paren {j - 1} }$, $j = 1, \ldots, n$
Then:
This is a system of $m n$ first order ODEs.
By construction:
:$\map {z_1} t = \map x t$
for all $t \in I$ and $\map {z_1} {t_0} = x_0$.
Therefore we can take:
:$y = \begin {pmatrix} z_1 \\ \vdots \\ z_{n - 1} \\ z_n \end {pmatrix}, \quad \tilde F: \begin {pmatrix} z_1 \\ \vdots \\ z_n \end{pmatrix} \mapsto \begin {pmatrix} z_2 \\ \vdots \\ z_n \\ \map F {t, z_1, \ldots, z_n} \end {pmatrix}$
== Historical Note ==
== Sources ==
* : Chapter $\text I$: Introductory: $\S 1.2$ Genesis of an Ordinary Differential Equation
Category:Ordinary Differential Equations
Reduction of Riemann-Stieltjes Integral to Identity Integrator

== Theorem ==
Let $f, \alpha$ be real functions that are bounded on $\closedint a b$.
Suppose that $f$ is Riemann-Stieltjes integrable with respect to $\alpha$ on $\closedint a b$.
Also suppose that $\alpha$ is continuously differentiable on $\closedint a b$.
Then, let $\alpha'$ be the derivative of $\alpha$ on $\closedint a b$.
Let $g : \closedint a b \to \R$ be defined as:
:$\map g x = \map f x \map {\alpha'} x$
Let $\iota$ be the identity mapping on $\closedint a b$.
Then, $g$ is Riemann-Stieltjes integrable with respect to $\iota$ on $\closedint a b$ and:
:$\ds \int_a^b g \rd \iota = \int_a^b f \rd \alpha$
== Proof ==
As $f$ is bounded on $\closedint a b$, let $M \in \R$ such that:
:$\forall x \in \closedint a b: \size {\map f x} \le M$
, let $M > 0$.
Let $\epsilon > 0$ be arbitrary.
By Continuous Function on Closed Real Interval is Uniformly Continuous:
:$\alpha'$ is uniformly continuous on $\closedint a b$
Therefore, there exists some $\delta_\epsilon$ such that, for all $x, y \in \closedint a b$ such that $\size {x - y} < \delta$:
:$\map {\alpha'} x - \map {\alpha'} y < \dfrac \epsilon {2 M \paren {b - a}}$
By Existence of Subdivision with Small Norm, let $P'_\epsilon$ be a subdivision of $\closedint a b$ such that:
:$\norm {P'_\epsilon} < \delta_\epsilon$
where $\norm {P'_\epsilon}$ denotes the norm of $P'_\epsilon$.
By definition of Riemann-Stieltjes integral, there is a subdivision $P' '_\epsilon$ such that:
:For any $P$ finer than $P' '_\epsilon$, $\ds \size {\map S {P, f, \alpha} - \int_a^b f \rd \alpha} < \frac \epsilon 2$
Define $P_\epsilon := P'_\epsilon \cup P' '_\epsilon$.
Then, $P_\epsilon$ is a subdivision of $\closedint a b$ that is finer than both $P'_\epsilon$ and $P' '_\epsilon$.
Let $P = \set {x_0, x_1, \dotsc, x_{n - 1}, x_n}$ be an arbitrary subdivision of $\closedint a b$ that is finer than $P_\epsilon$.
Then, $P$ is also finer than $P'_\epsilon$ and $P' '_\epsilon$.
For every $k \in \set {1, 2, \dotsc, x_{n - 1}, x_n}$, it follows from the Mean Value Theorem that:
:$\paren 1 \quad \map {\alpha'} {v_k} = \dfrac {\map \alpha {x_k} - \map \alpha {x_{k - 1}}} {x_k - x_{k - 1}}$
for some $v_k \in \openint {x_{k - 1}} {x_k}$.
Let $t_1, t_2, \dotsc, t_{n - 1}, t_n$ be fixed such that:
:$t_k \in \closedint {x_{k - 1}} {x_k}$
Let $\map S {P, f, \alpha}$ denote the Riemann-Stieltjes sum of $f$ with respect to $\alpha$ for $P$, using $\paren {t_k}_k$.
Let $\map S {P, g, \iota}$ denote the Riemann-Stieltjes sum of $g$ with respect to $\iota$ for $P$, using $\paren {t_k}_k$.
For every $k \in \set {1, \dotsc, n}$, we have:
Therefore:
Finally:
As $t_1, \dotsc, t_n$, $P$, and $\epsilon$ were all arbitrary in their respective domains, it follows from the definition of the Riemann-Stieltjes integral that:
:$\ds \int_a^b g \rd \iota = \int_a^b f \rd \alpha$
== Sources ==
* : Chapter $7$ The Riemann-Stieltjes Integral: $\S 7.7$: Theorem $7.8$
Category:Riemann-Stieltjes Integral
Refinement of Open Cover has Greater Entropy

== Theorem ==
Let $X$ be a compact topological space.
Let $\alpha, \beta$ be open covers of $X$.
Let $\map H \alpha$ and $\map H \beta$ be their entropies.
Suppose that $\beta$ is a refinement of $\alpha$.
Then:
:$\map H \alpha \le \map H \beta$
== Proof ==
By definition of entropy of open cover, there is a finite subcover $\beta' \subseteq \beta$ such that:
:$\map H \beta = \map \ln k$
with $k = \size {\beta '}$.
We write:
:$\beta' = \set {B_1, \ldots, B_k}$
:$\forall i \in \set {1, \ldots ,k} \; \exists A_i \in \alpha : B_i \subseteq A_i$
Then:
:$\alpha' = \set {A_1, \ldots, A_k}$
is a subcover of $\alpha$.
Thus, by definition of entropy of open cover:
:$\map H \alpha \le \map \ln k = \map H \beta$
== Sources ==
* Chapter $7$: Topological Entropy
Category:Ergodic Theory
Category:Topology
Refinement of a Refinement is Refinement of Cover

== Theorem ==
Let $S$ be a set.
Let $\UU = \set {U_\alpha}$, $\VV = \set {V_\beta}$ and $\WW = \set {W_\gamma}$ be covers of $S$.
Let $\VV$ be a refinement of $\UU$.
Let $\WW$ be a refinement of $\VV$.
Then:
:$\WW$ is a refinement of $\UU$
== Proof ==
Let $W \in \WW$.
By definition of refinement:
:$\exists V \in \VV : W \subseteq V$
Similarly:
:$\exists U \in \UU : V \subseteq U$
From Subset Relation is Transitive:
:$W \subseteq U$
Since $W$ was arbitrary:
:$\forall W \in \WW : \exists U \in \UU : W \subseteq U$
It follows that $\WW$ is a refinement of $\UU$ by definition.
Category:Covers