avewright/proofwiki-math huggingface dataset:
Theorem: Definite Integral from -a to a of Power of a plus x by Power of a minus x

:$\ds \int_{-a}^a \paren {a + x}^{m - 1} \paren {a - x}^{n - 1} \rd x = \paren {2 a}^{m + n - 1} \frac {\map \Gamma m \map \Gamma n} {\map \Gamma {m + n} }$

Proof:
Note the resemblance of this result to the integral defining the beta function.
In view of this, we apply the substitution: 
:$u = \dfrac {a + x} {2 a}$
We then have, by Derivative of Power: 
:$\dfrac {\d u} {\d x} = \dfrac 1 {2 a}$
and:
{{begin-eqn}}
{{eqn | l = 1 - u
      | r = 1 - \frac {a + x} {2 a}
}}
{{eqn | r = \frac {2 a - a - x} {2 a}
}}
{{eqn | r = \frac {a - x} {2 a}
}}
{{end-eqn}}
so that: 
:$a + x = 2 a u$
and:
:$a - x = \paren {2 a} \paren {1 - u}$
and:
:$\dfrac {\d x} {\d u} = 2 a$
We therefore have: 
{{begin-eqn}}
{{eqn | l = \int_{-a}^a \paren {a + x}^{m - 1} \paren {a - x}^{n - 1} \rd x
      | r = 2 a \int_0^1 \paren {2a u}^{m - 1} \paren {2 a \paren {1 - u} }^{n - 1} \rd u
      | c = Integration by Substitution
}}
{{eqn | r = \paren {2 a}^{m + n - 2 + 1} \int_0^1 u^{m - 1} \paren {1 - u}^{n - 1} \rd u
}}
{{eqn | r = \paren {2 a}^{m + n - 1} \map \Beta {m, n}
      | c = {{Defof|Beta Function|index = 1}}
}}
{{eqn | r = \paren {2 a}^{m + n - 1} \frac {\map \Gamma m \map \Gamma n} {\map \Gamma {m + n} }
      | c = {{Defof|Beta Function|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Arccosine in terms of Arctangent

:$\arccos x = 2 \map \arctan {\sqrt {\dfrac {1 - x} {1 + x} } }$

Proof:
Let: 
:$\theta = \arccos x$
Then by the definition of arccosine:
:$x = \cos \theta$
and: 
:$0 \le \theta < \pi$
Then: 
{{begin-eqn}}
{{eqn | l = 2 \map \arctan {\sqrt {\frac {1 - x} {1 + x} } }
      | r = 2 \map \arctan {\sqrt {\frac {1 - \cos \theta} {1 + \cos \theta} } }
}}
{{eqn | r = 2 \map \arctan {\sqrt {\frac {2 \sin^2 \frac \theta 2} {2 \cos^2 \frac \theta 2} } }
      | c = {{Corollary|Double Angle Formula for Cosine|1}}, {{Corollary|Double Angle Formula for Cosine|2}}
}}
{{eqn | r = 2 \map \arctan {\tan \frac \theta 2}
      | c = for $0 \le \theta < \dfrac \pi 2$ we have $\sin \theta \ge 0$ and $\cos \theta > 0$
}}
{{eqn | r = \theta
      | c = {{Defof|Real Arctangent}}
}}
{{eqn | r = \arccos x
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Reciprocal of a plus b Cosine x

:$\ds \int_0^{\pi/2} \frac 1 {a + b \cos x} \rd x = \frac 1 {\sqrt {a^2 - b^2} } \map \arccos {\frac b a}$

Proof:
Since $a > b > 0$, we have $a^2 > b^2$.
So:
{{begin-eqn}}
{{eqn	| l = \int_0^{\pi/2} \frac 1 {a + b \cos x} \rd x
	| r = \intlimits {\frac 2 {\sqrt {a^2 - b^2} } \map \arctan {\sqrt {\frac {a - b} {a + b} } \tan \frac x 2} } 0 1
	| c = Primitive of $\dfrac 1 {p + q \cos x}$
}}
{{eqn	| r = \frac 1 {\sqrt {a^2 - b^2} } \paren {2 \map \arctan {\sqrt {\frac {a - b} {a + b} } } }
}}
{{eqn	| r = \frac 1 {\sqrt {a^2 - b^2} } \paren {2 \map \arctan {\sqrt {\frac {1 - \frac b a} {1 + \frac b a} } } }
}}
{{eqn	| r = \frac 1 {\sqrt {a^2 - b^2} } \map \arccos {\frac b a}
	| c = Arccosine in terms of Arctangent
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -a x by Sine of b x over x

:$\ds \int_0^\infty \frac {e^{-a x} \sin b x} x \rd x = \map \arctan {\frac b a}$

Proof:
Take $a$ constant and define: 
:$\ds \map I b = \int_0^\infty \frac {e^{-a x} \sin b x} x \rd x$
We have: 
{{begin-eqn}}
{{eqn	| l = \map {I'} b
	| r = \frac \d {\d b} \int_0^\infty \frac {e^{-a x} \sin b x} x \rd x
}}
{{eqn	| r = \int_0^\infty \frac \partial {\partial b} \paren {\frac {e^{-a x} \sin b x} x} \rd x
	| c = Definite Integral of Partial Derivative
}}
{{eqn	| r = \int_0^\infty e^{-a x} \cos b x \rd x
	| c = Derivative of $\cos a x$
}}
{{eqn	| r = \frac a {a^2 + b^2}
	| c = Definite Integral to Infinity of $e^{-a x} \cos b x$
}}
{{end-eqn}}
so:
{{begin-eqn}}
{{eqn	| l = \map I b
	| r = a \int \frac 1 {b^2 + a^2} \rd b
}}
{{eqn	| r = \frac a a \arctan \frac b a + C
	| c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{eqn	| r = \arctan \frac b a + C
}}
{{end-eqn}}
for some constant $C \in \R$.
We have: 
{{begin-eqn}}
{{eqn	| l = \map I 0
	| r = \int_0^\infty \frac {e^{-a x} \sin 0} x \rd x
}}
{{eqn	| r = \int_0^\infty 0 \rd x
}}
{{eqn	| r = 0
}}
{{end-eqn}}
on the other hand:
{{begin-eqn}}
{{eqn	| l = \map I 0
	| r = \arctan 0 + C
}}
{{eqn	| r = C
}}
{{end-eqn}}
so:
:$C = 0$
So we have: 
:$\ds \int_0^\infty \frac {e^{-a x} \sin b x} x \rd x = \map \arctan {\frac b a}$
as required.
{{qed}}
Theorem: Definite Integral to Infinity of Sine of m x over Exponential of 2 Pi x minus One

:$\ds \int_0^\infty \frac {\sin m x} {e^{2 \pi x} - 1} \rd x = \frac 1 4 \coth \frac m 2 - \frac 1 {2 m}$

Proof:
We have:
{{begin-eqn}}
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {\sin m x} {e^{2 \pi x} - 1} \rd x
	| r = \int_0^\infty \frac {e^{-2 \pi x} \sin m x} {1 - e^{-2 \pi x} } \rd x
}}
{{eqn	| r = \int_0^\infty e^{-2 \pi x} \sin m x \paren {\sum_{k = 0}^\infty e^{-2 \pi k x} } \rd x
	| c = Sum of Infinite Geometric Sequence
}}
{{eqn	| r = \sum_{k = 0}^\infty \paren {\int_0^\infty e^{-x \paren {2 \pi \paren {1 + k} } } \sin m x \rd x}
}}
{{eqn	| r = \sum_{k = 0}^\infty \frac m {\paren {2 \pi \paren {1 + k} }^2 + m^2}
	| c = Definite Integral to Infinity of $e^{-a x} \sin b x$
}}
{{eqn	| r = \frac 1 {2 \pi} \sum_{k = 0}^\infty \frac {\frac m {2 \pi} } {\paren {k + 1}^2 + \paren {\frac m {2 \pi} }^2}
	| c = dividing by $\paren {2 \pi}^2$
}}
{{eqn	| r = \frac 1 {2 \pi} \sum_{k = 1}^\infty \frac {\frac m {2 \pi} } {k^2 + \paren {\frac m {2 \pi} }^2}
	| c = shifting the index
}}
{{end-eqn}}
By Mittag-Leffler Expansion for Hyperbolic Cotangent Function we have: 
:$\ds \sum_{k \mathop = 1}^\infty \frac z {k^2 + z^2} = \frac \pi 2 \map \coth {\pi z} - \frac 1 {2 z}$
for all $z \in \C$ where $z$ is not an integer multiple of $i$. 
Since all variables concerned in this instance all real-valued, we can apply this identity. 
Setting $z = \dfrac m {2 \pi}$ in the above we obtain:
{{begin-eqn}}
{{eqn	| l = \sum_{k = 1}^\infty \frac {\frac m {2 \pi} } {k^2 + \paren {\frac m {2 \pi} }^2}
	| r = \frac \pi 2 \map \coth {\pi \times \frac m {2 \pi} } - \frac 1 {2 \times \frac m {2 \pi} }
}}
{{eqn	| r = \frac \pi 2 \coth \frac m 2 - \frac \pi m
}}
{{end-eqn}}
So:
:$\ds \int_0^\infty \frac {\sin m x} {e^{2 \pi x} - 1} \rd x = \frac 1 {2 \pi} \paren {\frac \pi 2 \coth \frac m 2 - \frac \pi m} = \frac 1 4 \coth \frac m 2 - \frac 1 {2 m}$
as required.
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -a x^2 by Cosine of b x

:$\ds \int_0^\infty e^{-a x^2} \cos b x \rd x = \frac 1 2 \sqrt {\frac \pi a} \map \exp {-\frac {b^2} {4 a} }$

Proof:
Fix $a$ and define: 
:$\ds \map I b = \int_0^\infty e^{-a x^2} \cos b x \rd x$
for all $b \in \R$. 
Then, we have: 
{{begin-eqn}}
{{eqn	| l = \map {I'} b
	| r = \frac \d {\d b} \paren {\int_0^\infty e^{-a x^2} \cos b x \rd x}
}}
{{eqn	| r = \int_0^\infty \frac \partial {\partial b} \paren {e^{-a x^2} \cos b x} \rd x
	| c = Definite Integral of Partial Derivative
}}
{{eqn	| r = -\int_0^\infty \paren {x e^{-a x^2} } \sin b x \rd x
	| c = Derivative of $\cos a x$
}}
{{eqn	| r = -\paren {\intlimits {-\frac 1 {2 a} e^{-a x^2} \sin b x} 0 \infty - b \int_0^\infty \paren {-\frac 1 {2 a} e^{-a x^2} } \cos b x \rd x}
	| c = Integration by Parts
}}
{{end-eqn}}
Note that: 
{{begin-eqn}}
{{eqn	| l = \size {\frac 1 {2 a} e^{-a x^2} \sin b x}
	| o = \le
	| r = \frac 1 {2 a} e^{-a x^2}
	| c = noting that $\size {\sin x} \le 1$
}}
{{eqn	| o = \to
	| r = 0
	| c = Exponential Tends to Zero and Infinity
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn	| l = -\paren {\intlimits {-\frac 1 {2 a} e^{-a x^2} \sin b x} 0 \infty - b \int_0^\infty \paren {-\frac 1 {2 a} e^{-a x^2} } \cos b x \rd x}
	| r = -\frac b {2 a} \int_0^\infty e^{-a x^2} \cos b x \rd x
}}
{{eqn	| r = -\frac b {2 a} \map I b
}}
{{end-eqn}}
We then have: 
:$\dfrac {\map {I'} b} {\map I b} = -\dfrac b {2 a}$
Integrating, by Primitive of Function under its Derivative and Primitive of Constant:
:$\ln \size {\map I b} = -\dfrac {b^2} {4 a} + C$
for some $C \in \R$.
{{finish|This obviously only gives us an expression for $\ln \size {\map I b}$, we then need to determine that $\map I b > 0$ which seems nontrivial}}
So: 
:$\map I b = A \map \exp {-\dfrac {b^2} {4 a} }$
for some $A \in \R$.
We have: 
{{begin-eqn}}
{{eqn	| l = \map I 0
	| r = \int_0^\infty e^{-a x^2} \rd x
}}
{{eqn	| r = \frac 1 2 \sqrt {\frac \pi a}
	| c = Definite Integral to Infinity of $e^{-a x^2}$
}}
{{end-eqn}}
on the other hand we have: 
{{begin-eqn}}
{{eqn	| l = \map I 0
	| r = A \map \exp 0
}}
{{eqn	| r = A
	| c = Exponential of Zero
}}
{{end-eqn}}
So we have: 
:$\ds\map I b = \int_0^\infty e^{-a x^2} \cos b x \rd x = \frac 1 2 \sqrt {\frac \pi a} \map \exp {-\frac {b^2} {4 a} }$
for all $b \in \R$ as required.
{{qed}}
Theorem: Fourier Series for Logarithm of Sine of x over 0 to Pi

:$\ds \map \ln {\sin x} = -\ln 2 - \sum_{n \mathop = 1}^\infty \frac {\cos 2 n x} n$
where $0 < x < \pi$.

Proof:
We find the Half-Range Fourier Cosine Series over $\openint 0 {\dfrac \pi 2}$ for $\map \ln {\sin x}$.
By definition:
:$\ds \map \ln {\sin x} \sim \frac {a_0} 2 + \sum_{n \mathop = 1}^\infty a_n \cos 2 n x$
where for all $n \in \Z_{\ge 0}$:
:$\ds a_n = \frac 4 \pi \int_0^{\pi/2} \map \ln {\sin x} \cos 2 n x \ \d x$
By Definite Integral from 0 to Half Pi of Logarithm of Sine x:
:$a_0 = \dfrac 4 \pi \paren {-\dfrac \pi 2 \ln 2} = -2 \ln 2$
By Definite Integral from 0 to Half Pi of Logarithm of Sine x by Cosine of 2nx:
:$a_n = \dfrac 4 \pi \paren {-\dfrac \pi {4 n} } = -\dfrac 1 n$
Therefore:
{{begin-eqn}}
{{eqn | l = \map \ln {\sin x}
      | o = \sim
      | r = \frac {a_0} 2 + \sum_{n \mathop = 1}^\infty a_n \cos 2 n x
}}
{{eqn | r = -\ln 2 - \sum_{n \mathop = 1}^\infty \frac {\cos 2 n x} n
}}
{{end-eqn}}
{{qed}}
Theorem: Fourier Series for Logarithm of Sine of x over 0 to Pi

:$\ds \map \ln {\sin x} = -\ln 2 - \sum_{n \mathop = 1}^\infty \frac {\cos 2 n x} n$
where $0 < x < \pi$.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^\infty \dfrac {\cos 2 n x} n
      | r = \sum_{n \mathop = 1}^\infty \dfrac {\map \exp {2 i n x} + \map \exp {-2 i n x} } {2 n}
      | c = Euler's Cosine Identity: $\cos z = \dfrac {\map \exp {i z} + \map \exp {-i z} } 2$
}}
{{eqn | r = \frac 1 2 \sum_{n \mathop = 1}^\infty \paren {\frac {\paren {\map \exp {2 i x} }^n} n + \frac {\paren {\map \exp {-2 i x} }^n} n}
      | c = Power of Power
}}
{{eqn | r = -\frac 1 2 \paren {\map \ln {1 - \map \exp {2 i x} } + \map \ln {1 - \map \exp {-2 i x} } }
      | c = Power Series Expansion for $\map \ln {1 - x}$: $-\map \ln {1 - x} = \ds \sum_{n \mathop = 1}^\infty \dfrac {x^n} n$
}}
{{eqn | r = -\frac 1 2 \paren {\map \ln {1 - \map \exp {-2 i x} - \map \exp {2 i x} + 1} }
      | c = Sum of Logarithms
}}
{{eqn | r = -\frac 1 2 \paren {\map \ln {2 - 2 \paren {\frac {\map \exp {-2 i x} + \map \exp {2 i x} } 2} } }
      | c = simplifying and multiplying top and bottom by $2$
}}
{{eqn | r = -\frac 1 2 \paren {\map \ln {2 - 2 \map \cos {2 x} } }
      | c = Euler's Cosine Identity: $\cos z = \dfrac {\map \exp {i z} + \map \exp {-i z} } 2$
}}
{{eqn | r = -\frac 1 2 \paren {\map \ln {4 \sin^2 x} }
      | c = {{Corollary|Double Angle Formula for Cosine|2}}: $1 - \cos 2 \theta = 2 \sin^2 \theta$
}}
{{eqn | r = -\paren {\map \ln {4 \sin^2 x }^{\frac 1 2} }
      | c = Logarithm of Power
}}
{{eqn | r = -\paren {\map \ln {2 \sin x} }
      | c = 
}}
{{eqn | r = -\paren {\ln 2 + \map \ln {\sin x} }
      | c = Sum of Logarithms
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 1}^\infty \dfrac {\cos 2 n x} n
      | r = -\ln 2 - \map \ln {\sin x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\sin x}
      | r = -\ln 2 - \sum_{n \mathop = 1}^\infty \dfrac {\cos 2 n x} n
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Subset of Set Difference iff Disjoint Set

Let $S, T$ be sets.
Let $A \subseteq S$
Then:
:$A \cap T = \O \iff A \subseteq S \setminus T$
where:
:$A \cap T$ denotes set intersection
:$\O$ denotes the empty set
:$S \setminus T$ denotes set difference.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = A \cap \paren {S \setminus T} 
      | r = \paren {A \cap S} \setminus T
      | c = Intersection with Set Difference is Set Difference with Intersection
}}
{{eqn | r = A \setminus T
      | c = Intersection with Subset is Subset
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = A
      | o = \subseteq
      | r = S \setminus T
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = A
      | r = A \cap \paren {S \setminus T}
      | c = Intersection with Subset is Subset
}}
{{eqn | ll= \leadstoandfrom
      | l = A
      | r = A \setminus T
      | c = As $A \cap \paren {S \setminus T} = A \setminus T$
}}
{{eqn | ll = \leadstoandfrom
      | l = A \cap T
      | r = \O
      | c = Set Difference with Disjoint Set
}}
{{end-eqn}}
{{qed}}
Category:Set Difference
Category:Disjoint Sets
q6dxws2h8938ofa7dgk459wk4cpfr1o
Theorem: Set Difference of Doubleton and Singleton is Singleton

Let $x, y$ be distinct objects.
Then:
:$\set{x, y} \setminus \set x = \set y$

Proof:
{{begin-eqn}}
{{eqn | l = \set {x, y} \setminus \set x
      | r = \set {z: z \in \set {x, y} \land z \notin \set x}
      | c = {{Defof|Set Difference}}
}}
{{eqn | r = \set {z: \paren {z = x \lor z = y} \land z \notin \set x}
      | c = {{Defof|Doubleton}}
}}
{{eqn | r = \set {z: \paren {z = x \lor z = y} \land z \ne x}
      | c = {{Defof|Singleton}}
}}
{{eqn | r = \set {z: \paren {z = x \land z \ne x} \lor \paren {z = y \land z \ne x} }
      | c = Conjunction Distributes over Disjunction
}}
{{eqn | r = \set {z: \bot \lor \paren {z = y \land z \ne x} }
      | c = {{Defof|Contradiction}}
}}
{{eqn | r = \set {z: \paren {z = y \land z \ne x} }
      | c = Disjunction with Contradiction
}}
{{eqn | r = \set {z : z = y}
      | c = Rule of Simplification
}}
{{eqn | r = \set y
      | c = {{Defof|Singleton}}
}}
{{end-eqn}}
{{qed}}
Category:Singletons
Category:Doubletons
2yo0ngrwag2fj31y5wrsadxaq7rpwic
Theorem: 1 plus Perfect Power is not Power of 2

The equation:
:$1 + a^n = 2^m$
has no solutions in the integers for $n, m > 1$.
This is an elementary special case of Catalan's Conjecture.

Proof:
{{AimForCont}} there is a solution.
Then:
{{begin-eqn}}
{{eqn | l = a^n
      | r = 2^m - 1
}}
{{eqn | o = \equiv
      | r = -1
      | rr = \pmod 4
      | c = as $m > 1$
}}
{{end-eqn}}
$a$ is immediately seen to be odd.
By Square Modulo 4, $n$ must also be odd.
Now:
{{begin-eqn}}
{{eqn | l = 2^m
      | r = a^n + 1
}}
{{eqn | r = \paren {a + 1} \sum_{k \mathop = 0}^{n - 1} \paren {-1}^k a^{n - k - 1}
      | c = Sum of Two Odd Powers
}}
{{end-eqn}}
The latter sum has $n$ powers of $a$, which sums to an odd number.
The only odd divisor of $2^m$ is $1$.
However, if the sum is $1$, we have:
:$a^n + 1 = a + 1$
giving $n = 1$, contradicting our constraint $n > 1$.
Hence the result by Proof by Contradiction.
{{qed}}
Category:Number Theory
ex9a8rtweepg9xdh7umpt71f6nn8kuk
Theorem: Definite Integral from 0 to Half Pi of Logarithm of Sine x by Cosine of 2nx

For $n \in \N_{>0}$:
:$\ds \int_0^{\pi/2} \map \ln {\sin x} \cos 2 n x \rd x = -\frac \pi {4 n}$

Proof:
First we have:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to 0} \map \ln {\sin x} \sin 2 n x
      | r = \lim_{x \mathop \to 0} \frac {\map \ln {\sin x} } {\csc 2 n x}
      | c = {{Defof|Cosecant}}
}}
{{eqn | r = \lim_{x \mathop \to 0} \frac {\cot x} {- 2 n \cot 2 n x \csc 2 n x}
      | c = L'Hôpital's Rule: Corollary $2$
}}
{{eqn | r = \lim_{x \mathop \to 0} \frac {\cos x} {- 2 n \cos 2 n x} \frac {\sin^2 2 n x} {\sin x}
      | c = {{Defof|Cosecant}}, {{Defof|Cotangent}}
}}
{{eqn | l = \lim_{x \mathop \to 0} \frac {\sin^2 2 n x} {\sin x}
      | r = \lim_{x \mathop \to 0} \frac {4 n \sin 2 n x \cos 2 n x} {\cos x}
      | c = L'Hôpital's Rule
}}
{{eqn | r = 0
}}
{{end-eqn}}
hence $\ds \lim_{x \mathop \to 0} \map \ln {\sin x} \sin 2 n x = 0$.
Thus:
{{begin-eqn}}
{{eqn | l = \int_0^{\pi/2} \map \ln {\sin x} \cos 2 n x \rd x
      | r = \frac 1 {2 n} \int_0^{\pi/2} \map \ln {\sin x} \map \rd {\sin 2 n x}
      | c = Primitive of $\cos a x$
}}
{{eqn | r = \frac 1 {2 n} \paren {\bigintlimits {\map \ln {\sin x} \sin 2 n x} 0 {\pi/2} - \int_0^{\pi/2} \sin n x \map \rd {\map \ln {\sin x} } }
      | c = Integration by Parts
}}
{{eqn | r = -\frac 1 {2 n} \int_0^{\pi/2} \sin n x \map \rd {\map \ln {\sin x} }
      | c = From above
}}
{{eqn | r = -\frac 1 {2 n} \int_0^{\pi/2} \sin 2 n x \frac {\cos x} {\sin x} \rd x
      | c = Primitive of Cotangent Function
}}
{{eqn | r = -\frac 1 {2 n} \int_0^{\pi/2} \frac {\sin \paren {2 n + 1} x + \sin \paren {2 n - 1} x} {2 \sin x} \rd x
      | c = Werner Formula for Sine by Cosine
}}
{{eqn | r = -\frac 1 {4 n} \int_0^{\pi} \frac {\sin \paren {\paren {2 n + 1} u/2} + \sin \paren {\paren {2 n - 1} u/2} } {2 \sin \paren {u/2} } \rd u
      | c = substituting $u = 2 x$
}}
{{eqn | r = -\frac 1 {4 n} \int_0^{\pi} \paren {\frac 1 2 + \sum_{k \mathop = 1}^n \map \cos {k u} + \frac 1 2 + \sum_{k \mathop = 1}^{n - 1} \map \cos {k u} } \rd u
      | c = Lagrange's Cosine Identity
}}
{{eqn | r = -\frac 1 {4 n} \int_0^{\pi} 1 \rd u
      | c = All integrals involving $\cos k u$ evaluate to $0$
}}
{{eqn | r = -\frac \pi {4 n}
      | c = Definite Integral of Constant
}}
{{end-eqn}}
{{qed}}
Category:Definite Integrals involving Logarithm Function
Category:Definite Integrals involving Sine Function
5ixqrx7rin2tm7zqtgehza0lnpq8tqo
Theorem: Distinct Matroid Elements are Parallel iff Each is in Closure of Other/Lemma

Let $a, b \in S$.
Let $\set a$ and $\set b$ be independent.
Then $\set {a, b}$ is dependent {{iff}}:
:$a \in \map \sigma {\set b}$
and
:$b \in \map \sigma {\set a}$

Proof:
{{begin-eqn}}
{{eqn | l = \set {a, b}
      | o = \notin
      | r = \mathscr I
}}
{{eqn | ll= \leadstoandfrom
      | l = \set a \cup \set b
      | o = \notin
      | r = \mathscr I
      | c = Union of Disjoint Singletons is Doubleton
}}
{{eqn | ll= \leadstoandfrom
      | l = a
      | o = \in
      | r = \map \sigma {\set b}
      | c = Element Depends on Independent Set iff Union with Singleton is Dependent
}}
{{eqn | lo= \land
      | l = b
      | o = \in
      | r = \map \sigma {\set a}
      | c = Element Depends on Independent Set iff Union with Singleton is Dependent
}}
{{end-eqn}}
{{qed}}
Category:Distinct Matroid Elements are Parallel iff Each is in Closure of Other
a3szsfqgb984wsvqqb2yy8i472rnz2j
Theorem: Definite Integral to Infinity of Sine m x over x by x Squared plus a Squared

:$\ds \int_0^\infty \frac {\sin m x} {x \paren {x^2 + a^2} } \rd x = \frac \pi {2 a^2} \paren {1 - e^{-m a} }$

Proof:
Fix $a$ and set: 
:$\ds \map I m = \int_0^\infty \frac {\sin m x} {x \paren {x^2 + a^2} } \rd x$
for $m \ge 0$. 
We have:
{{begin-eqn}}
{{eqn	| l = \map {I'} m
	| r = \frac \d {\d m} \int_0^\infty \frac {\sin m x} {x \paren {x^2 + a^2} } \rd x
}}
{{eqn	| r = \int_0^\infty \frac \partial {\partial m} \paren {\frac {\sin m x} {x \paren {x^2 + a^2} } } \rd x
	| c = Definite Integral of Partial Derivative
}}
{{eqn	| r = \int_0^\infty \frac {\cos m x} {x^2 + a^2} \rd x
	| c = Derivative of $\sin a x$
}}
{{eqn	| r = \frac \pi {2 a} e^{-m a}
	| c = Definite Integral to Infinity of $\dfrac {\cos m x} {x^2 + a^2}$
}}
{{end-eqn}}
So by Primitive of $e^{a x}$:
:$\map I m = -\dfrac \pi {2 a^2} e^{-m a} + C$
for some constant $C \in \R$.
We have: 
{{begin-eqn}}
{{eqn	| l = \map I 0
	| r = \int_0^\infty \frac {\sin 0 x} {x^2 + a^2} \rd x
}}
{{eqn	| r = \int_0^\infty 0 \rd x
	| c = Sine of Zero is Zero
}}
{{eqn	| r = 0
}}
{{end-eqn}}
On the other hand: 
{{begin-eqn}}
{{eqn	| l = \map I 0
	| r = -\frac \pi {2 a^2} e^0 + C
}}
{{eqn	| r = -\frac \pi {2 a^2} + C
	| c = Exponential of Zero
}}
{{end-eqn}}
So:
:$C = \dfrac \pi {2 a^2}$
giving: 
:$\ds \map I m = \int_0^\infty \frac {\sin m x} {x \paren {x^2 + a^2} } \rd x = \frac \pi {2 a^2} \paren {1 - e^{-m a} }$
{{qed}}
Theorem: Definite Integral from 0 to Pi of a Squared minus 2 a b Cosine x plus b Squared

:$\ds \int_0^\pi \map \ln {a^2 - 2 a b \cos x + b^2} \rd x = \begin{cases}2 \pi \ln a & a \ge b > 0 \\ 2 \pi \ln b & b \ge a > 0\end{cases}$

Proof:
Note that: 
:$\paren {a - b}^2 \ge 0$
so by Square of Sum:
:$a^2 - 2 a b + b^2 \ge 0$
So:
:$a^2 + b^2 \ge 2 a b = \size {-2 a b}$
so we may apply Definite Integral from $0$ to $\pi$ of $\map \ln {a + b \cos x}$.
We then have:
{{begin-eqn}}
{{eqn	| l = \int_0^\pi \map \ln {a^2 - 2 a b \cos x + b^2} \rd x
	| r = \pi \map \ln {\frac {a^2 + b^2 + \sqrt {\paren {a^2 + b^2}^2 - \paren {2 a b}^2} } 2}
}}
{{eqn	| r = \pi \map \ln {\frac {a^2 + b^2 + \sqrt {a^4 + 2 a^2 b^2 + b^4 - 4 a^2 b^2} } 2}
}}
{{eqn	| r = \pi \map \ln {\frac {a^2 + b^2 + \sqrt {a^4 - 2 a^2 b^2 + b^4} } 2}
}}
{{eqn	| r = \pi \map \ln {\frac {a^2 + b^2 + \sqrt {\paren {a^2 - b^2}^2} } 2}
}}
{{eqn	| r = \pi \map \ln {\frac {a^2 + b^2 + \size {a^2 - b^2} } 2}
	| c = {{Defof|Absolute Value/Definition 2|Absolute Value}}
}}
{{end-eqn}}
Note that if $a \ge b > 0$ we have:
{{begin-eqn}}
{{eqn	| l = \pi \map \ln {\frac {a^2 + b^2 + \size {a^2 - b^2} } 2}
	| r = \pi \map \ln {\frac {a^2 + b^2 + a^2 - b^2} 2}
	| c = since $a \ge b > 0$, we have $a^2 \ge b^2$ and $\size {a^2 - b^2} = a^2 - b^2$
}}
{{eqn	| r = \pi \map \ln {a^2}
}}
{{eqn	| r = 2 \pi \ln a
	| c = Logarithm of Power
}}
{{end-eqn}}
Note that if $b \ge a > 0$ we have: 
{{begin-eqn}}
{{eqn	| l = \pi \map \ln {\frac {a^2 + b^2 + \size {a^2 - b^2} } 2}
	| r = \pi \map \ln {\frac {a^2 + b^2 + b^2 - a^2} 2}
	| c = since $a \ge b > 0$, we have $a^2 \ge b^2$ and $\size {a^2 - b^2} = b^2 - a^2$
}}
{{eqn	| r = \pi \map \ln {b^2}
}}
{{eqn	| r = 2 \pi \ln b
	| c = Logarithm of Power
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Square of Logarithm of Sine x

:$\ds \int_0^{\pi/2} \paren {\map \ln {\sin x} }^2 \rd x = \frac \pi 2 \paren {\ln 2}^2 + \frac {\pi^3} {24}$

Proof:
From Fourier Series for $\map \ln {\sin x}$ from $0$ to $\pi$:
:$\ds \map \ln {\sin x} = -\ln 2 - \sum_{n \mathop = 1}^\infty \frac {\cos 2 n x} n$
Then, by Parseval's Theorem:
{{begin-eqn}}
{{eqn | l = \frac 2 \pi \int_0^\pi \paren {\map \ln {\sin x} }^2 \rd x
      | r = 2 \paren {\ln 2}^2 + \sum_{n = 1}^\infty \frac 1 {n^2}
}}
{{eqn | r = 2 \paren {\ln 2}^2 + \frac {\pi^2} 6
      | c = Basel Problem
}}
{{end-eqn}}
We then have: 
{{begin-eqn}}
{{eqn | l = \int_0^\pi \paren {\map \ln {\sin x} }^2 \rd x
      | r = \int_0^{\pi/2} \paren {\map \ln {\sin x} }^2 \rd x + \int_{\pi/2}^\pi \paren {\map \ln {\sin x} }^2 \rd x
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions
}}
{{eqn | r = \int_0^{\pi/2} \paren {\map \ln {\sin x} }^2 \rd x + \int_0^{\pi/2} \paren {\map \ln {\map \sin {\pi - x} } }^2 \rd x
}}
{{eqn | r = 2 \int_0^{\pi/2} \paren {\map \ln {\sin x} }^2 \rd x
      | c = Sine of Supplementary Angle
}}
{{end-eqn}}
So: 
:$\ds \frac 4 \pi \int_0^{\pi/2} \paren {\map \ln {\sin x} }^2 \rd x = 2 \paren {\ln 2}^2 + \frac {\pi^2} 6$
Multiplying by $\dfrac \pi 4$: 
:$\ds \int_0^{\pi/2} \paren {\map \ln {\sin x} }^2 \rd x = \frac \pi 2 \paren {\ln 2}^2 + \frac {\pi^3} {24}$
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Square of Logarithm of Cosine x

:$\ds \int_0^{\pi/2} \paren {\map \ln {\cos x} }^2 \rd x = \frac \pi 2 \paren {\ln 2}^2 + \frac {\pi^3} {24}$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^{\pi/2} \paren {\map \ln {\cos x} }^2 \rd x
	| r = \int_0^{\pi/2} \paren {\map \ln {\map \cos {\frac \pi 2 - x} } }^2 \rd x
}}
{{eqn	| r = \int_0^{\pi/2} \paren {\map \ln {\sin x} }^2 \rd x
	| c = Cosine of Complement equals Sine
}}
{{eqn	| r = \frac \pi 2 \paren {\ln 2}^2 + \frac {\pi^3} {24}
	| c = Definite Integral from $0$ to $\dfrac \pi 2$ of $\paren {\map \ln {\sin x} }^2$
}}
{{end-eqn}}
{{qed}}