nyuuzyou/wikis huggingface dataset:
Definite Integral from 0 to Quarter Pi of Logarithm of One plus Tan x

== Theorem ==
:$\ds \int_0^{\pi/4} \map \ln {1 + \tan x} \rd x = \frac \pi 8 \ln 2$
== Proof ==
Therefore: 
:$\ds 2 \int_0^{\pi/4} \map \ln {1 + \tan x} \rd x = \frac \pi 4 \ln 2$
giving: 
:$\ds \int_0^{\pi/4} \map \ln {1 + \tan x} \rd x = \frac \pi 8 \ln 2$
== Sources ==
* : $\S 15$: Definite Integrals involving Logarithmic Functions: $15.109$
Category:Definite Integrals involving Logarithm Function
Category:Definite Integrals involving Tangent Function
Definite Integral from 0 to a of Reciprocal of Root of a Squared minus x Squared

== Theorem ==
:$\ds \int_0^a \dfrac {\d x} {\sqrt {a^2 - x^2} } = \frac \pi 2$
for $a > 0$. 
== Proof 1 == 
 
== Proof 2 ==
== Sources ==
* : $\S 15$: Definite Integrals involving Rational or Irrational expressions: $15.22$
Category:Definite Integral from 0 to a of Reciprocal of Root of a Squared minus x Squared
Category:Examples of Definite Integrals
Definite Integral from 0 to a of Root of a Squared minus x Squared

== Theorem ==
:$\ds \int_0^a \sqrt {a^2 - x^2} \rd x = \frac {\pi a^2} 4$
for $a > 0$. 
== Proof 1 ==
== Proof 2 == 
== Sources ==
* : $\S 15$: Definite Integrals involving Rational or Irrational expressions: $15.23$
Category:Definite Integral from 0 to a of Root of a Squared minus x Squared
Category:Examples of Definite Integrals
Definite Integral from 0 to a of x^m by (a^n - x^n)^p

== Theorem ==
:$\ds \int_0^a x^m \paren {a^n - x^n}^p \rd x = \frac {a^{m + 1 + n p} \, \map \Gamma {\frac {m + 1} n} \map \Gamma {p + 1} } {n \map \Gamma {\frac {m + 1} n + p + 1} }$
== Proof ==
== Sources ==
* : $\S 15$: Definite Integrals involving Rational or Irrational expressions: $15.24$
Category:Examples of Definite Integrals
Definite Integral is Area

== Theorem ==
Let $f : \closedint a b \to \R$ be Darboux integrable over $\closedint a b$.
Let $A$ be the total signed area between $\map f x$ and the $x$-axis, and between the lines $x = a$ and $x = b$.
Then $A$ equals the Darboux integral of $f$ over $\closedint a b$.
== Proof ==
=== Lemma ===
Define $f^+$ and $f^-$ to be the positive and negative parts of $f$, respectively.
Let $A^+$ be the area under $\map {f^+} x$ on $\closedint a b$.
Let $A^-$ be the area under $\map {f^-} x$ on the same interval.
By Positive Part of Darboux Integrable Function is Integrable and its corollary for the negative part,
$f^+$ and $f^-$ are Darboux integrable over $\closedint a b$.
By the lemma, $A^+$ and $A^-$ are equal to the Darboux integral over their respective parts.
Therefore:
Category:Definite Integral is Area
Category:Definite Integrals
Definite Integral is Area/Lemma

== Lemma for Definite Integral is Area ==
Let $f : \closedint a b \to \R_{\mathop \ge 0}$ be non-negative and Darboux integrable over $\closedint a b$.
Let $G$ be the point set of $\tuple {x, y}$ such that $a \le x \le b$ and $0 \le y \le \map f x$.
Let $A$ be the area of $G$, which is colloquially called the area under the curve.
Then $A$ equals the Darboux integral of $f$ over $\closedint a b$.
== Proof ==
Let $\ds P = \sequence {x_i}_{0 \mathop \le i \mathop \le n}$ be a finite subdivision of $\closedint a b$.
For each $i$ from $1$ to $n$, the $R_i$ be the rectangle $x_{i - 1} \le x \le x_i$ and $\ds 0 \le y \le \sup_{\closedint {x_{i - 1} } {x_i} } \map f x$.
Then all the points $0 \le y \le \map f x$ for $x \in \closedint {x_{i - 1} } {x_i}$ are in $R_i$.
But $P$ is a subdivision of $\closedint a b$, so $\ds \bigcup R_i \supseteq G$.
Therefore, $\set {R_i}_{1 \mathop \le i \mathop \le n}$ is a finite covering of $G$.
By Area of Rectangle, $\map A {R_i} = \paren {x_i - x_{i - 1} } \sup_{\closedint {x_{i - 1} } {x_i} } \map f x$.
Thus:
Therefore, by the definitions of Outer Jordan Content and Upper Darboux Integral:
:$\ds \map {m^*} G \le \overline {\int_a^b} \map f x \rd x$
Now, let $\ds y' = \sup_{\closedint a b} \map f x$.
Let $B$ be the rectangle with $a \le x \le b$ and $0 \le y \le y'$.
Then, $G \subseteq B$.
Consider again $\ds P = \sequence {x_i}_{0 \mathop \le i \mathop \le n}$, a finite subdivision of $\closedint a b$.
Let $S_i$ be the rectangle $x_{i - 1} \le x \le x_i$ and $\inf_{\closedint {x_{i - 1} } {x_i} } \map f x \le y \le y'$.
In a similar manner to before, $\set {S_i}_{1 \mathop \le i \mathop \le n}$ is a finite covering of $B \setminus G$.
And like before, it follows that:
:$\ds \map {m^*} {B \setminus G} \le \map A B - \underline {\int_a^b} \map f x \rd x$
But then:
:$\ds \underline {\int_a^b} \map f x \rd x \le \map A B - \map {m^*} {B \setminus G}$
Also, by Outer Jordan Content Never Smaller than Inner Jordan Content:
:$\map A B - \map {m^*} {B \setminus G} \le \map {m^*} G$
So the following inequalities hold:
:$\ds \underline {\int_a^b} \map f x \rd x \le \map A B - \map {m^*} {B \setminus G} \le \map {m^*} G \le \overline {\int_a^b} \map f x \rd x$
By hypothesis:
:$\ds \underline {\int_a^b} \map f x \rd x = \overline {\int_a^b} \map f x \rd x$
Therefore:
:$\ds \map {m^*} G = \map A B - \map {m^*} {B \setminus G} = \map m G = \int_a^b \map f x \rd x$
By Well-Defined Jordan Content Equals Content:
:$\ds A = \map m G = \int_a^b \map f x \rd x$
Category:Definite Integral is Area
Definite Integral of Constant/Corollary

== Corollary to Definite Integral of Constant ==
:$\ds \int_a^b \rd x = b - a$
== Proof ==
From Definite Integral of Constant:
:$\ds \int_a^b c \rd x = c \paren {b - a}$
where $c$ is a constant.
Setting $c = 1$:
:$\ds \int_a^b \rd x = b - a$
== Sources ==
* 
* 
Category:Definite Integrals
Definite Integral of Constant Multiple of Real Function

== Theorem ==
Let $f$ be a real function which is integrable on the closed interval $\closedint a b$.
Let $c \in \R$ be a real number.
Then:
:$\ds \int_a^b c \map f x \rd x = c \int_a^b \map f x \rd x$
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $\S 15$: General Formulas involving Definite Integrals: $15.8$
* : $6$. Integral Calculus: Appendix: Rules and Techniques of Integration: $1.2$
* 
* 
* : $\S 18$: Definite Integrals: General Formulas involving Definite Integrals: $18.8$
Category:Definite Integral of Constant Multiple of Real Function
Category:Definite Integrals
Definite Integral of Constant Multiple of Real Function/Proof 1

== Theorem ==
== Proof ==
Let $F$ be a primitive of $f$ on $\closedint a b$.
By Primitive of Constant Multiple of Function, $H = c F$ is a primitive of $c f$ on $\closedint a b$.
Hence by the Fundamental Theorem of Calculus:
Category:Definite Integral of Constant Multiple of Real Function
Definite Integral of Constant Multiple of Real Function/Proof 2

== Theorem ==
== Proof ==
Let $F$ be a primitive of $f$ on $\closedint a b$.
By Linear Combination of Definite Integrals:
:$\ds \int_a^b \paren {\lambda \map f t + \mu \map g t} \rd t = \lambda \int_a^b \map f t \rd t + \mu \int_a^b \map g t \rd t$
for real functions $f$ and $g$ which are integrable on the closed interval $\closedint a b$, where $\lambda$ and $\mu$ be real numbers.
The result follows by setting $\lambda = c$ and $\mu = 0$.
Category:Definite Integral of Constant Multiple of Real Function
Definite Integral of Even Function

== Theorem ==
Let $f$ be an even function with a primitive on the closedinterval $\closedint {-a} a$, where $a > 0$.
Then:
:$\ds \int_{-a}^a \map f x \rd x = 2 \int_0^a \map f x \rd x$
=== Corollary ===
== Proof ==
Let $F$ be a primitive for $f$ on the interval $\closedint {-a} a$.
Then, by Sum of Integrals on Adjacent Intervals for Integrable Functions, we have:
Therefore, it suffices to prove that:
:$\ds \int_{-a}^0 \map f x \rd x = \int_0^a \map f x \rd x$
To this end, let $\phi: \R \to \R$ be defined by $x \mapsto -x$. 
From Derivative of Identity Function and Derivative of Constant Multiple, for all $x \in \R$, we have $\map {\phi'} x = -1$.
Then, by means of Integration by Substitution, we compute:
This concludes the proof.
== Also see ==
* Definite Integral of Odd Function
== Sources ==
* : $\S 4.5$
Category:Integral Calculus
Category:Even Functions
Category:Definite Integrals
Definite Integral of Even Function/Corollary

== Corollary to Definite Integral of Even Function ==
Let $f$ be an even function with a primitive on the open interval $\openint {-a} a$, where $a > 0$.
Then the improper integral of $f$ on $\openint {-a} a$ is:
:$\ds \int_{\mathop \to -a}^{\mathop \to a} \map f x \rd x = 2 \int_0^{\mathop \to a} \map f x \rd x$
== Proof ==
Category:Integral Calculus
Category:Even Functions
Category:Improper Integrals
Definite Integral of Exponential of minus a x squared from 0 to Infinity

== Theorem ==
:$\ds \int_0^\infty \map \exp {-a x^2} \rd x = \dfrac 1 2 \sqrt {\dfrac \pi a}$
for $a > 0$.
== Proof ==
Recall Integral to Infinity of $\map \exp {-x^2}$:
:$\ds \int_0^\infty \map \exp {-x^2} \rd x = \dfrac {\sqrt \pi} 2$
Then:
== Sources ==
* : Back endpapers: A Brief Table of Integrals: $140$.
Category:Integral to Infinity of Exponential of -t^2
Category:Error Function
Category:Definite Integrals involving Exponential Function
Definite Integral of Fourier Series at Ends of Interval

== Theorem ==
Let $f: \R \to \R$ be a real function defined in the open interval $\openint {-\pi} \pi$.
Let $f$ fulfil the Dirichlet conditions in $\openint {-\pi} \pi$.
Let $a_0, a_1, \dotsc; b_1, \dotsc$ be the Fourier coefficients of $f$ in $\openint {-\pi} \pi$.
Consider the real function:
:$\map F x = \ds \int_{-\pi}^x \map f t \rd t - \dfrac {a_0} 2 x$
Then:
:$\map F \pi = \map F {-\pi} = \dfrac {a_0 \pi} 2$
== Proof ==
From Definite Integral on Zero Interval:
Then:
== Sources ==
* : Chapter Three: Properties of Fourier Series: $1$. Integration of Fourier Series
Category:Definite Integrals
Category:Fourier Analysis
Definite Integral of Function plus Constant

== Theorem ==
Let $f$ be a real function which is continuous on the closed interval $\closedint a b$.
Let $c$ be a constant.
Then:
:$\ds \int_a^b \paren {\map f t + c} \rd t = \int_a^b \map f t \rd t + c \paren {b - a}$
== Proof ==
Let $P = \set {x_0, x_1, x_2, \ldots, x_n}$ be a finite subdivision of $\closedint a b$.
Let $\map {L^{\paren {f + c} } } P$ be the lower Darboux sum of $\map f x + c$ on $\closedint a b$ belonging to $P$.
Let:
:$\ds m_k^{\paren {f + c} } = \map {\inf_{x \mathop \in \closedint {x_{k - 1} } {x_k} } } {\map f x + c}$
where $k \in \set {0, 1, \ldots, n}$.
So:
It follows that:
So from the definition of definite integral, it follows that:
== Sources ==
* : $\S 13.7$
* : Appendix: $\S 18.8$: Integration
Category:Integral Calculus
Definite Integral of Function satisfying Dirichlet Conditions is Continuous

== Theorem ==
Let $f: \R \to \R$ be a real function defined in the open interval $\openint {-\pi} \pi$.
Let $f$ fulfil the Dirichlet conditions in $\openint {-\pi} \pi$.
Let $a_0, a_1, \dotsc; b_1, \dotsc$ be the Fourier coefficients of $f$ in $\openint {-\pi} \pi$.
Then the real function:
:$\map F x = \ds \int_{-\pi}^x \map f t \rd t - \dfrac {a_0} 2 x$
is continuous on $\openint {-\pi} \pi$.
== Proof ==
== Sources ==
* : Chapter Three: Properties of Fourier Series: $1$. Integration of Fourier Series
Category:Continuity
Category:Definite Integrals
Definite Integral of Limit of Uniformly Convergent Sequence of Integrable Functions

== Theorem ==
Let $a, b \in \R$ with $a < b$. 
Let $\sequence {f_n}$ be a sequence of Riemann integrable real functions $\closedint a b \to \R$ converging uniformly to $f : \closedint a b \to \R$.
Then $f$ is integrable, and: 
:$\ds \int_a^b \map f x \rd x = \lim_{n \mathop \to \infty} \int_a^b \map {f_n} x \rd x$
== Proof ==
By Limit of Uniformly Convergent Sequence of Integrable Functions is Integrable, $f$ is integrable.
We have:
Let $\epsilon \in \R_{> 0}$.
Since $f_n \to f$ uniformly, we can find $N \in \N$ such that for $n > N$ we have:
:$\ds \sup_{x \mathop \in \closedint a b} \size {\map f x - \map {f_n} x} < \frac \epsilon {b - a}$
by the definition of uniform convergence.
So, for $n > N$ we have: 
:$\ds \paren {b - a} \sup_{x \mathop \in \closedint a b} \size {\map f x - \map {f_n} x} < \epsilon$
and hence:
:$\ds \size {\int_a^b \map f x \rd x - \int_a^b \map {f_n} x \rd x} < \epsilon$ 
Since $\epsilon$ was arbitrary it follows that: 
:$\ds \lim_{n \mathop \to \infty} \int_a^b \map {f_n} x \rd x = \int_a^b \map f x \rd x$
as required.
Category:Integral Calculus
Category:Uniform Convergence
Definite Integral of Odd Function

== Theorem ==
Let $f$ be an odd function with a primitive on the open interval $\closedint {-a} a$, where $a > 0$.
Then:
:$\ds \int_{-a}^a \map f x \rd x = 0$
=== Corollary ===
== Proof ==
Let $F$ be a primitive for $f$ on the interval $\closedint {-a} a$.
Then, by Sum of Integrals on Adjacent Intervals for Integrable Functions, we have:
Therefore, it suffices to prove that:
:$\ds \int_{-a}^0 \map f x \rd x = -\int_0^a \map f x \rd x$
To this end, let $\phi: \R \to \R$ be defined by $x \mapsto -x$. 
From Derivative of Identity Function and Derivative of Constant Multiple, for all $x \in \R$, we have $\map {\phi'} x = -1$.
Then, by means of Integration by Substitution, we compute:
This concludes the proof.
== Also see ==
* Definite Integral of Even Function
== Sources ==
* : $\S 4.5$
Category:Integral Calculus
Category:Odd Functions
Category:Definite Integrals
Definite Integral of Odd Function/Corollary

== Corollary to Definite Integral of Odd Function ==
Let $f$ be an odd function with a primitive on the open interval $\openint {-a} a$, where $a > 0$.
Then the improper integral of $f$ on $\openint {-a} a$ is:
:$\ds \int_{\mathop \to -a}^{\mathop \to a} \map f x \rd x = 0$
== Proof ==
Category:Integral Calculus
Category:Odd Functions
Category:Improper Integrals
Definite Integral of Partial Derivative

== Theorem ==
Let $\map f {x, y}$ and $\map {\dfrac {\partial f} {\partial x} } {x, y}$ be continuous functions of $x$ and $y$ on $D = \closedint {x_1} {x_2} \times \closedint a b$.
Then:
:$\ds \frac \d {\d x} \int_a^b \map f {x, y} \rd y = \int_a^b \map {\frac {\partial f} {\partial x} } {x, y} \rd y$
for $x \in \closedint {x_1} {x_2}$.
== Proof 1 ==
== Proof 2 ==
Category:Partial Differentiation
Category:Definite Integrals
Category:Definite Integral of Partial Derivative
Definite Integral of Partial Derivative/Proof 1

== Theorem ==
== Proof ==
From Leibniz's Integral Rule:
:$\ds \frac \d {\d y} \int_{\map a y}^{\map b y} \map f {x, y} \rd x = \map f {y, \map b y} \frac {\d b} {\d y} - \map f {y, \map a y} \frac {\d a} {\d y} + \int_{\map a y}^{\map b y} \frac {\partial} {\partial y} \map f {x, y} \rd x$
where $\map a y$, $\map b y$ are continuously differentiable.
Setting $\map a y$ and $\map b y$ constant, so that $\exists a, b \in \R: \map a y = a, \map b y = b$:
:$\dfrac {\d a} {\d y} = \dfrac {\d b} {\d y} = 0$
from which the result follows immediately.
Category:Definite Integral of Partial Derivative
Definite Integral of Partial Derivative/Proof 2

== Theorem ==
== Proof ==
Define $\ds \map G x = \int_a^b \map f {x, y} \rd y$.
The continuity of $f$ ensures that $G$ exists.
Then by linearity of the integral:
:$\dfrac {\Delta G} {\Delta x} = \dfrac {\map G {x + \Delta x} - \map G x} {\Delta x} = \ds \int_a^b \frac {\map f {x + \Delta x, y} - \map f {x, y} } {\Delta x} \rd y$
We want to find the limit of this quantity as $\Delta x$ approaches zero.
For each $y \in \closedint a b$, we can consider $\map {f_y} x = \map f {x, y}$ as a separate function of the single variable $x$, with $\dfrac {\d f_y} {\d x} = \dfrac {\partial f} {\partial x}$.
Thus by the Mean Value Theorem, there is a number $c_y \in \openint x {x + \Delta x}$ such that:
:$\map {f_y} {x + \Delta x} - \map {f_y} x = \map {\dfrac {\d f_y} {\d x} } {c_y} \Delta x$
That is:
:$\map f {x + \Delta x, y} - \map f {x, y} = \map {\dfrac {\partial f} {\partial x} } {c_y, y} \Delta x$
Therefore:
:$\dfrac {\Delta G} {\Delta x} = \ds \int_a^b \map {\frac {\partial f} {\partial x} } {c_y, y} \rd y$
Now, pick any $\epsilon > 0$ and set $\epsilon_0 = \dfrac {\epsilon} {b - a}$.
Since $\dfrac {\partial f} {\partial x}$ is continuous on the compact set $D$, it is uniformly continuous on $D$.
Hence for each $x$ and $y$:
:$\size {\map {\dfrac {\partial f} {\partial x} } {x + h, y} - \map {\dfrac {\partial f} {\partial x} } {x, y} } < \epsilon_0$
whenever $h$ is sufficiently small.
Since $x < c_y < x + \Delta x$, it follows that for sufficiently small $\Delta x$:
:$\size {\map {\dfrac {\partial f} {\partial x} } {c_y, y} - \map {\dfrac {\partial f} {\partial x} } {x, y} } < \epsilon_0$
regardless of our choice of $y$.
So we can say:
But since $\epsilon$ was arbitrary, it follows that:
:$\ds \lim_{\Delta x \mathop \to 0} \frac {\Delta G} {\Delta x} = \int_a^b \map {\frac {\partial f} {\partial x} } {x, y} \rd y$
and the theorem is proved.
Category:Definite Integral of Partial Derivative
Definite Integral of Periodic Function

== Theorem ==
Let $f$ be a Darboux integrable periodic function with period $L$.
Let $\alpha \in \R$ and $n \in \Z$.
Then:
:$\ds \int_\alpha^{\alpha + n L} \map f x \d x = n \int_0^L \map f x \d x$
== Proof ==
For $n \ge 0$:
For $n < 0$:
Hence the result.
Category:Definite Integrals
Category:Periodic Functions
Definite Integral of Reciprocal of Root of a Squared minus x Squared

== Theorem ==
:$\ds \int_0^x \frac {\d t} {\sqrt{1 - t^2} } = \arcsin x$
== Proof ==
== Sources ==
* : Chapter $\text {A}.33$: Weierstrass ()
Category:Definite Integrals
Category:Arcsine Function
Category:Reciprocals
Definite Integral of Step Function

== Theorem ==
Let $\alpha, \beta \in \R$ be a real numbers such that $\alpha < \beta$.
Let $\map f x$ be a step function defined on the interval $\closedint \alpha \beta$:
:$\map f x = \lambda_1 \chi_{\mathbb I_1} + \lambda_2 \chi_{\mathbb I_2} + \cdots + \lambda_n \chi_{\mathbb I_n}$
where:
:$\lambda_1, \lambda_2, \ldots, \lambda_n$ are real constants
:$\mathbb I_1, \mathbb I_2, \ldots, \mathbb I_n$ are intervals, where these intervals partition $\closedint \alpha \beta$
:$\chi_{\mathbb I_1}, \chi_{\mathbb I_2}, \ldots, \chi_{\mathbb I_n}$ are characteristic functions of $\mathbb I_1, \mathbb I_2, \ldots, \mathbb I_n$.
Then the definite integral of $f$ { $x$ over $\closedint \alpha \beta$ is given by:
:$\ds \int_\alpha^\beta \map f x \rd x = \sum_{k \mathop = 1}^n \lambda_k \paren {\beta_k - \alpha_k}$
where $\alpha_k, \beta_k$ are the endpoints of $\mathbb I_k$ for $1 \le k \le n$.
== Proof ==
Each of the intervals $\mathbb I_k$ is such that $f \sqbrk {\mathbb I_k}$ is a constant function:
:$\forall x \in \mathbb I_k: \map f x = \lambda_k$
Thus:
From the corollary to Sum of Integrals on Adjacent Intervals for Integrable Functions:
Category:Step Functions
Category:Definite Integrals
Definite Integral of Uniformly Convergent Series of Continuous Functions

== Theorem ==
Let $\sequence {f_n}$ be a sequence of real functions.
Let each of $\sequence {f_n}$ be continuous on the interval $\hointr a b$.
Let the series:
:$\ds \map f x := \sum_{n \mathop = 1}^\infty \map {f_n} x$
be uniformly convergent for all $x \in \closedint a b$.
Then:
:$\ds \int_a^b \map f x \rd x = \sum_{n \mathop = 1}^\infty \int_a^b \map {f_n} x \rd x$
== Proof ==
Define $\map {S_N} x = \ds \sum_{n \mathop = 1}^N \map {f_n} x$.
We have:
== Sources ==
* : $\S 1.3.1$: Properties of uniformly convergent series: Theorem $1.9 \ \text{(b)}$
Category:Integral Calculus
Category:Convergence
Category:Continuity
Category:Series
Definite Integral on Zero Interval

== Theorem ==
Let $f$ be a real function which is defined on the closed interval $\Bbb I := \closedint a b$, where $a < b$.
Then:
:$\ds \forall c \in \Bbb I: \int_c^c \map f t \rd t = 0$
== Proof ==
Follows directly from the definition of definite integral.
There is only one finite subdivision of $\closedint c c$ and that is $\set c$.
Both the lower Darboux sum and upper Darboux sum of $\map f x$ on $\closedint c c$ belonging to the finite subdivision $\set c$ are equal to zero.
Hence the result.
== Sources ==
* : $\S 15$: General Formulas involving Definite Integrals: $15.9$
* : $6$. Integral Calculus: Appendix: Rules and Techniques of Integration: $1.4$
* : $\S 18$: Definite Integrals: General Formulas involving Definite Integrals: $18.9$
Category:Definite Integrals
Definite Integral over Reals of Exponential of -(a x^2 plus b x plus c)

== Theorem ==
:$\ds \int_{-\infty}^\infty \map \exp {-\paren {a x^2 + b x + c} } \rd x = \sqrt {\frac \pi a} \map \exp {\frac {b^2 - 4 a c} {4 a} }$
where $a$, $b$ and $c$ are real numbers with $a > 0$.
== Proof ==
== Sources ==
* : $\S 15$: Definite Integrals involving Exponential Functions: $15.75$
Category:Definite Integrals involving Exponential Function
Definite Integral over Unit Square of Logarithm of x minus Logarithm of y over x minus y

== Theorem ==
:$\ds \int_0^1 \int_0^1 \frac {\ln x - \ln y} {x - y} \rd x \rd y = 2 \map \zeta 2$
== Proof ==
== Sources ==
* https://www.instagram.com/p/C0BtTejRdDW/
Category:Definite Integrals involving Logarithm Function
Category:Riemann Zeta Function
Category:Spence's Function
Definite Integral to Infinity of Arctangent of p x minus Arctangent of q x over x

== Theorem ==
:$\ds \int_0^\infty \frac {\arctan p x - \arctan q x} x \rd x = \frac \pi 2 \ln \frac p q$
where $p$ and $q$ are strictly positive real numbers.
== Proof ==
Note that the integrand is of the form: 
:$\ds \int_0^\infty \frac {\map f {p x} - \map f {q x} } x \rd x$
where:
:$\map f x = \arctan x$
We have, by Derivative of Arctangent Function:
:$\map {f'} x = \dfrac 1 {1 + x^2}$
which is continuous on $\R$. 
By Limit to Infinity of Arctangent Function: 
:$\ds \lim_{x \mathop \to \infty} \map f x = \lim_{x \mathop \to \infty} \arctan x = \frac \pi 2$
As $f$ is continuously differentiable and $\ds \lim_{x \mathop \to \infty} \map f x$ exists and is finite, we may apply Frullani's Integral, giving:
== Sources ==
* : $\S 15$: Definite Integrals involving Trigonometric Functions: $15.67$
Category:Definite Integrals involving Arctangent Function
Definite Integral to Infinity of Cosine m x over x Squared plus a Squared

== Theorem ==
:$\ds \int_0^\infty \frac {\cos m x} {x^2 + a^2} \rd x = \frac \pi {2 a} e^{-m a}$
where $m$ and $a$ are positive real numbers. 
== Proof ==
From Definite Integral of Even Function:
:$\ds \frac 1 2 \int_{-\infty}^\infty \frac {\cos m x} {x^2 + a^2} \rd x = \int_0^\infty \frac {\cos m x} {x^2 + a^2} \rd x$
Let $R$ be a positive real number with $R > a$.
Let $C_1$ be the straight line segment from $-R$ to $R$.
Let $C_2$ be the arc of the circle of radius $R$ centred at the origin connecting $R$ and $-R$ anticlockwise.
Let $\Gamma = C_1 \cup C_2$. 
Let: 
:$\map f z = \dfrac {e^{i m z} } {z^2 + a^2}$
From Euler's Formula, we have: 
:$\map f z = \dfrac {\cos m z} {z^2 + a^2} + i \dfrac {\sin m z} {z^2 + a^2}$
So: 
Note that the integrand is meromorphic with simple poles where $z^2 + a^2 = 0$. 
That is, at $z = a i$ and $z = -a i$. 
As our semi-circular contour lies in the upper half-plane, the only pole of concern is $a i$.
As $R > a$, these poles do not lie on $C_2$, but are enclosed by the curve $\Gamma$.
We have: 
The integral over $C_2$ can be shown to vanish as $R \to \infty$:
Taking $R \to \infty$, we have: 
So: 
:$\ds \int_{-\infty}^\infty \frac {\cos m x} {x^2 + a^2} \rd x = \frac \pi a e^{-m a}$
giving:
:$\ds \int_0^\infty \frac {\cos m x} {x^2 + a^2} \rd x = \frac \pi {2 a} e^{-m a}$
== Sources ==
* : $\S 15$: Definite Integrals involving Trigonometric Functions: $15.40$
Category:Definite Integrals involving Cosine Function
Definite Integral to Infinity of Cosine of a x^2

== Theorem ==
:$\ds \int_0^\infty \map \cos {a x^2} \rd x = \frac 1 2 \sqrt {\frac \pi {2 a} }$
where $a$ is a positive real number. 
== Proof ==
We have, by Euler's Formula: Corollary:
:$\map \exp {-i a x^2} = -i \map \sin {a x^2} + \map \cos {a x^2}$
As $\map \sin {a x^2}$ and $\map \cos {a x^2}$ are both real for real $a, x$, we therefore have:
== Sources ==
* : $\S 15$: Definite Integrals involving Trigonometric Functions: $15.50$
Category:Definite Integrals involving Sine Function