avewright/proofwiki-math huggingface dataset:
Theorem: Space of Somewhere Differentiable Continuous Functions on Closed Interval is Meager in Space of Continuous Functions on Closed Interval/Lemma 2/Lemma 2.1

:for each $\tuple {n, m} \in \N^2$, $A_{n, m}$ is closed in $\tuple {\map \CC I, d}$.

Proof:
Fix $\tuple {n, m} \in \N^2$. 
From Space of Continuous on Closed Interval Real-Valued Functions with Supremum Norm forms Banach Space:
:$\tuple {\map \CC I, d}$ is complete.
Hence, from Subspace of Complete Metric Space is Closed iff Complete:
:$A_{n, m}$ is closed {{iff}} $\tuple {A_{n, m}, d}$ is complete.
Let $\sequence {f_i}_{i \mathop \in \N}$ be a Cauchy sequence in $\tuple {A_{n, m}, d}$.
Since $\tuple {\map \CC I, d}$ is complete, $\sequence {f_i}_{i \mathop \in \N}$ converges some $f \in \map \CC I$.
We aim to show that $f \in A_{n, m}$.
Since $f_i \in A_{n, m}$ for each $i \in \N$, there exists $x_i \in I$ such that: 
:$\ds \size {\frac {\map {f_i} t - \map {f_i} {x_i} } {t - x_i} } \le n$ for each $t$ with $0 < \size {t - x_i} < \dfrac 1 m$.
Note that since $I$ is bounded, $\sequence {x_i}_{i \mathop \in \N}$ is bounded.
Therefore, by the Bolzano-Weierstrass Theorem:
:there exists a convergent subsequence of $\sequence {x_i}_{i \mathop \in \N}$, $\sequence {x_{i_k} }_{k \mathop \in \N}$.
Let: 
:$\ds x = \lim_{k \mathop \to \infty} x_{i_k}$
Note that we also have: 
:$\ds f = \lim_{k \mathop \to \infty} f_{i_k}$
From Subset of Metric Space contains Limits of Sequences iff Closed, since $I$ is closed, $x \in I$.
From Necessary Condition for Uniform Convergence:
:the sequence $\sequence {\map {f_{i_k} } {x_{i_k} } }_{k \mathop \in \N}$ converges to $\map f x$.
We therefore have: 
{{begin-eqn}}
{{eqn | l = \size {\frac {\map f t - \map f x} {t - x} }
      | r = \lim_{k \mathop \to \infty} \size {\frac {\map {f_{i_k} } t - \map {f_{i_k} } {x_{i_k} } } {t - x_{i_k} } }
}}
{{eqn | o = \le
      | r = n
}}
{{end-eqn}}
for all $t$ with $0 < \size {t - x} < \dfrac 1 m$. 
That is, $f \in A_{n, m}$.
{{qed}}
Category:Space of Somewhere Differentiable Continuous Functions on Closed Interval is Meager in Space of Continuous Functions on Closed Interval
in0j024c1fl7t54v438cx5waw963aik
Theorem: Decomposition of Mean Squared Error

<onlyinclude>
Let $\theta$ be a population parameter of some stochastic model.
Let $\hat \theta$ be an estimator of $\theta$.
We then have:
:$\map {\operatorname {MSE} } {\hat \theta} = \var {\hat \theta} + \paren {\map {\operatorname {bias}} {\hat \theta} }^2 $
where:
:$\map {\operatorname {MSE} } {\hat \theta}$ denotes the Mean Squared Error of $\hat \theta$.
:$\var {\hat \theta}$ denotes the variance of $\hat \theta$.
:$\map {\operatorname {bias} } {\hat \theta}$ denotes the bias of $\hat \theta$.

Proof:
Let $\delta = \hat \theta - \theta$.
By {{Defof|Mean Squared Error of Estimator}}:
:$\expect {\delta ^2} = \map {\operatorname {MSE} } {\hat \theta}$
and:
{{begin-eqn}}
{{eqn | l = \expect \delta
      | r = \expect {\paren {\hat \theta} - \theta}
}}
{{eqn | r = \expect {\hat \theta} - \theta
      | c = Expectation of Linear Transformation of Random Variable
}}
{{eqn | r = \map{\operatorname{bias} } {\hat \theta}
      | c = {{Defof|Bias in Estimator}}
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \var {\hat \theta}
      | r = \var \delta
      | c = Variance of Linear Transformation of Random Variable
}}
{{eqn | r = \expect {\delta^2} - \paren {\expect \delta}^2
      | c = Variance as Expectation of Square minus Square of Expectation
}}
{{eqn | r = \map {\operatorname {MSE} } {\hat \theta} - \paren {\map {\operatorname {bias} } {\hat \theta} }^2
}}
{{end-eqn}}
Or, equivalently:
:$\map {\operatorname {MSE} } {\hat \theta} = \var {\hat \theta} + \paren {\map {\operatorname {bias} } {\hat \theta} }^2$
{{qed}}
Category:Inductive Statistics
Category:Variance
372tc7z8wwnbhxvjm8gr26pvjhqculs
Theorem: Subset of Nowhere Dense Subset is Nowhere Dense

Let $T = \struct {S, \tau}$ be a topological space.
Let $A \subseteq S$ be nowhere dense in $T$.
Let $B \subseteq A$. 
Then $B$ is nowhere dense in $T$.

Proof:
{{AimForCont}} it is not the case that $B$ is nowhere dense in $T$.
Then by definition of nowhere dense:
:$B^-$ contains some open set of $T$ which is non-empty.
From Set Closure Preserves Set Inclusion, we have:
:$B^- \subseteq A^-$
So:
:$A^-$ contains some open set of $T$ which is non-empty.
So $A$ is not nowhere dense in $T$.
This contradicts our assertion that $A$ is nowhere dense in $T$:
The result follows by Proof by Contradiction.
{{qed}}
Category:Nowhere Dense
2kam5sfl8c400cxsomjcx7387m7ykag
Theorem: Derived Set Preserves Set Inclusion

Let $T = \struct {S, \tau}$ be a topological space.
Let $B \subseteq A \subseteq S$.
Then:
:$B' \subseteq A'$
where $A'$ and $B'$ are the derived sets in $T$ of $A$ and $B$ respectively.

Proof:
Let: 
:$x \in B'$
By the definition of derived set:
:$x$ is a limit point of $B$.
Note that $B \subseteq A$.
From Limit Point of Subset is Limit Point of Set:
:$x$ is a limit point of $A$.
So, $x \in A'$.
That is:
:$B' \subseteq A'$
{{qed}}
Category:Limit Points
bsp2iqal0g2yrhqr0u89brrzwg4vfjq
Theorem: Set Closure Preserves Set Inclusion

Let $T = \struct {S, \tau}$ be a topological space.
Let $B \subseteq A \subseteq S$.
Then:
:$B^- \subseteq A^-$
where $A^-$ and $B^-$ are the set closures in $T$ of $A$ and $B$ respectively.

Proof:
By definition 1 of set closure:
:$B^- = B \cup B'$
where $B'$ is the derived set of $B$ in $T$. 
Similarly:
:$A^- = A \cup A'$
where $A'$ is the derived set of $A$ in $T$.
From Derived Set Preserves Set Inclusion:
:$B' \subseteq A'$
So, by Set Union Preserves Subsets:
:$B \cup B' \subseteq A \cup A'$
That is:
:$B^- \subseteq A^-$
{{qed}}
Category:Set Closures
tks9y6fgpie70rbwaskjlse8ovtpuii
Theorem: Subset of Meager Set is Meager Set

Let $T = \struct {S, \tau}$ be a topological space.
Let $A$ be meager in $T$.
Let $B \subseteq A$.
Then $B$ is meager in $T$.

Proof:
Since $A$ is meager in $T$:
:there exists a countable collection of sets $\set {U_n: n \in \N}$ nowhere dense in $T$ such that $\ds A = \bigcup_{n \mathop \in \N} U_n$.
Then, we have: 
{{begin-eqn}}
{{eqn | l = B
      | r = A \cap B
      | c = Intersection with Subset is Subset
}}
{{eqn | r = \paren {\bigcup_{n \mathop \in \N} U_n} \cap B
}}
{{eqn | r = \bigcup_{n \mathop \in \N} \paren {U_n \cap B}
      | c = Union Distributes over Intersection
}}
{{end-eqn}}
From Intersection is Subset:
:$U_n \cap B \subseteq U_n$
From Subset of Nowhere Dense Subset is Nowhere Dense:
:$U_n \cap B$ is nowhere dense in $T$.
Then, we see that:
:$B$ can be written as the union of nowhere dense sets in $T$.
That is:
:$B$ is meager in $T$.
{{qed}}
Category:Meager Spaces
8auzqspv1s22avzxiqqop0pky06m3vk
Theorem: Functions in Vector Space of Real-Valued Functions Continuously Differentiable on Closed Interval vanish at Endpoints

Let $I := \closedint a b$ be a closed real interval.
Let $\struct {\map {C^1} I, +, \, \cdot \,}_\R$ be the continuously differentiable on closed interval real function vector space.
Let $S := \set {x \in \map {C^1} I : \map x a = y_a, \map x b = y_b}$.
Then $S$ is a vector subspace of $\struct {\map {C^1} I, +, \, \cdot \,}_\R$ {{iff}} $y_a = y_b = 0$.

Proof:
=== Necessary Condition ===
Suppose $y_a = y_b = 0$.
Theorem: Union of Meager Sets is Meager Set

Let $T = \struct {S, \tau}$ be a topological space.
Let $A$ and $B$ be meager in $T$.
Then $A \cup B$ is meager in $T$.

Proof:
Since $A$ is meager in $T$:
:there exists a countable collection of sets $\set {U_n: n \in \N}$ nowhere dense in $T$ such that $\ds A = \bigcup_{n \mathop \in \N} U_n$.
Since $B$ is meager in $T$:
:there exists a countable collection of sets $\set {V_m: m \in \N}$ nowhere dense in $T$ such that $\ds B = \bigcup_{m \mathop \in \N} V_m$.
Then:
:$\ds A \cup B = \paren {\bigcup_{n \mathop \in \N} U_n} \cup \paren {\bigcup_{m \mathop \in \N} V_m}$
The {{RHS}} is a countable union of sets nowhere dense in $T$, so:
:$A \cup B$ is meager in $T$.
{{qed}}
Category:Meager Spaces
Category:Set Union
akyxmrpe9z44sqlh3q94dagut14xknx
Theorem: Primitive of Reciprocal of p squared plus Square of q by Hyperbolic Cosine of a x/Inverse Hyperbolic Tangent Form

:$\ds \int \frac {\d x} {p^2 + q^2 \cosh^2 a x} = \dfrac 1 {a p \sqrt {p^2 + q^2} } \tanh^{-1} \dfrac {p \tanh a x} {\sqrt {p^2 + q^2} } + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\d x} {p^2 + q^2 \cosh^2 a x}
      | r = \frac 1 {2 a p \sqrt {p^2 + q^2} } \ln \size {\frac {p \tanh a x + \sqrt {p^2 + q^2} } {p \tanh a x - \sqrt {p^2 + q^2} } } + C
      | c = Primitive of $\dfrac {\d x} {p^2 + q^2 \cosh^2 a x}$: Logarithm Form
}}
{{eqn | r = \frac 1 {a p \sqrt {p^2 + q^2} } \tanh^{-1} \dfrac {p \tanh a x} {\sqrt {p^2 + q^2} } + C
      | c = {{Defof|Inverse Hyperbolic Tangent|subdef = Real|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Weierstrass Function is Continuous

Let $a \in \openint 0 1$. 
Let $b$ be a strictly positive odd integer such that: 
:$\ds a b > 1 + \frac 3 2 \pi$
Let $f: \R \to \R$ be a real function defined by: 
:$\ds \map f x = \sum_{n \mathop = 0}^\infty a^n \map \cos {b^n \pi x}$
for each $x \in \R$.
Then $f$ is well-defined and continuous.

Proof:
Note that: 
:$\ds \sup_{x \mathop \in \R} \size {a^n \map \cos {b^n \pi x} } = a^n$
Since $a \in \openint 0 1$:
:$\ds \sum_{n \mathop = 0}^\infty a^n$ converges.
So, by the Weierstrass M-Test:
:$\ds \sum_{n \mathop = 0}^\infty a^n \map \cos {b^n \pi x}$ converges uniformly on $\R$. 
That is, $f$ is well-defined.
Further, from Uniformly Convergent Series of Continuous Functions Converges to Continuous Function: Corollary:
:$f$ is continuous.
{{qed}}
Category:Weierstrass Functions
lefd9f7wkxv4tea7lgqws656hdm0t18
Theorem: Real Inverse Hyperbolic Sine Function is Bijection

The real inverse hyperbolic sine is a bijection.

Proof:
From Hyperbolic Sine is Bijection over Reals and by definition of bijection, we have that $\sinh$ admits an inverse function over $\R$.
From:
:Domain of Bijection is Codomain of Inverse
:Codomain of Bijection is Domain of Inverse
the domain and image of hyperbolic sine over $\R$, is $\R$.
{{qed}}
Category:Inverse Hyperbolic Sine
h7ao7rgfmqmsnkmr9n2kpgw0zf8t36t
Theorem: Power Series Expansion for Real Area Hyperbolic Sine

The (real) area hyperbolic sine function has a Taylor series expansion:
{{begin-eqn}}
{{eqn | l = \arsinh x
      | r = <nowiki>\begin {cases}
\ds \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n \paren {2 n}!} {2^{2 n} \paren {n!}^2} \frac {x^{2 n + 1} } {2 n + 1} & : \size x < 1 \\ \\
\ds \ln 2 x + \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n \paren {2 n}!} {2^{2 n} \paren {n!}^2 \paren {2 n} x^{2 n} } } & : x \ge 1 \\ \\
\ds -\ln \paren {-2 x} - \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^n \paren {2 n}!} {2^{2 n} \paren {n!}^2 \paren {2 n} x^{2 n} } } & : x \le -1
\end {cases}</nowiki>
      | c = 
}}
{{eqn | o =
}}
{{eqn | r = <nowiki>\begin {cases}
x - \dfrac {x^3} {2 \times 3} + \dfrac {1 \times 3 x^5} {2 \times 4 \times 5} - \dfrac {1 \times 3 \times 5 x^7} {2 \times 4 \times 6 \times 7} + \cdots & : \size x < 1 \\ \\
\ln 2 x + \dfrac 1 {2 \times 2 x^2} - \dfrac {1 \times 3} {2 \times 4 \times 4 x^4} + \dfrac {1 \times 3 \times 5} {2 \times 4 \times 6 \times 6 x^6} + \cdots & : x \ge 1 \\ \\
-\ln \paren {-2 x} - \paren {\dfrac 1 {2 \times 2 x^2} - \dfrac {1 \times 3} {2 \times 4 \times 4 x^4} + \dfrac {1 \times 3 \times 5} {2 \times 4 \times 6 \times 6 x^6} + \cdots} & : x \le -1
\end {cases} </nowiki>
      | c = 
}}
{{end-eqn}}

Proof:
=== Lemma 1 ===
{{:Power Series Expansion for Real Area Hyperbolic Sine/Lemma 1}}{{qed|lemma}}
From Power Series is Termwise Integrable within Radius of Convergence, $(1)$ can be integrated term by term:
{{begin-eqn}}
{{eqn | l = \int_0^x \frac 1 {\sqrt {t^2 + 1} } \rd t
      | r = \sum_{n \mathop = 0}^\infty \int_0^x \frac {\paren {-1}^n \paren {2 n}!} {2^{2 n} \paren {n!}^2} t^{2 n} \rd t
      | c =
}}
{{eqn | ll= \leadsto
      | l = \arsinh x
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n \paren {2 n}!} {2^{2 n} \paren {n!}^2} \frac {x^{2 n + 1} } {2 n + 1}
      | c = Derivative of Inverse Hyperbolic Sine
}}
{{end-eqn}}
{{qed|lemma}}
We will now prove that the series converges for $-1 < x < 1$.
By Stirling's Formula:
{{begin-eqn}}
{{eqn | l = \frac {\paren {-1}^n \paren {2 n}!} {2^{2 n} \paren {n!}^2} \frac {x^{2 n + 1} } {2 n + 1} 
      | o = \sim
      | r = \frac {\paren {-1}^n \paren {2 n}^{2 n} e^{-2 n} \sqrt {4 \pi n} } {2^{2 n} n^{2 n} e^{-2 n} 2 \pi n} \frac {x^{2 n + 1} } {2 n + 1}
      | c =
}}
{{eqn | r = \frac {\paren {-1}^n}  {\sqrt {\pi n} } \frac {x^{2 n + 1} } {2 n + 1}
      | c =
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \size {\frac 1 {\sqrt {\pi n} } \frac {x^{2 n + 1} } {2 n + 1} }
      | o = <
      | r = \size {\frac {x^{2 n + 1} } {n^{3/2} } }
      | c = 
}}
{{eqn | o = \le
      | r = \frac 1 {n^{3/2} }
      | c = 
}}
{{end-eqn}}
Hence by Convergence of P-Series:
:$\ds \sum_{n \mathop = 1}^\infty \frac 1 {n^{3/2} }$
is convergent.
So by the Comparison Test, the Taylor series is convergent for $-1 \le x \le 1$.
{{qed|lemma}}
Another lemma:
Theorem: Power Series Expansion for Real Area Hyperbolic Secant

The (real) area hyperbolic secant function has a Taylor series expansion:
{{begin-eqn}}
{{eqn | l = \arsech x
      | r = \ln \frac 2 x - \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {2 n}! x^{2 n} } {2^{2 n} \paren {n!}^2 \paren {2 n} } }
      | c = 
}}
{{eqn | r = \ln \frac 2 x - \paren {\dfrac 1 2 \dfrac {x^2} 2 + \dfrac {1 \times 3} {2 \times 4} \dfrac {x^4} 4 + \dfrac {1 \times 3 \times 5} {2 \times 4 \times 6} \dfrac {x^6} 6 + \cdots}
      | c = 
}}
{{end-eqn}}
for $0 < x \le 1$.

Proof:
From Power Series Expansion for Real Area Hyperbolic Cosine:
{{begin-eqn}}
{{eqn | l = \arcosh x
      | r = \ln 2 x - \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2 \paren {2 n} x^{2 n} } }
      | c = 
}}
{{eqn | r = \ln 2 x - \paren {\dfrac 1 2 \dfrac 1 {2 x^2} + \dfrac {1 \times 3} {2 \times 4} \dfrac 1 {4 x^4} + \dfrac {1 \times 3 \times 5} {2 \times 4 \times 6} \dfrac 1 {6 x^6} + \cdots}
      | c = 
}}
{{end-eqn}}
for $x \ge 1$.
From Real Area Hyperbolic Cosine of Reciprocal equals Real Area Hyperbolic Secant:
:$\map \arcosh {\dfrac 1 x} = \arsech x$
So:
{{begin-eqn}}
{{eqn | l = \arsech x
      | r = \ln \frac 2 x - \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {2 n}! x^{2 n} } {2^{2 n} \paren {n!}^2 \paren {2 n} } }
      | c = 
}}
{{eqn | r = \ln \frac 2 x - \paren {\dfrac 1 2 \dfrac {x^2} 2 + \dfrac {1 \times 3} {2 \times 4} \dfrac {x^4} 4 + \dfrac {1 \times 3 \times 5} {2 \times 4 \times 6} \dfrac {x^6} 6 + \cdots}
      | c = 
}}
{{end-eqn}}
For $1 \le \dfrac 1 x$ we have that $0 < x \le 1$.
Hence the result.
{{qed}}
Theorem: Primitive of Inverse Hyperbolic Cosine of x over a/Corollary

:$\ds \int -\cosh^{-1} \frac x a \rd x = x \paren {-\cosh^{-1} \dfrac x a} + \sqrt {x^2 - a^2} + C$
where $-\cosh^{-1}$ denotes the negative branch of the real inverse hyperbolic cosine multifunction.

Proof:
{{begin-eqn}}
{{eqn | l = -\cosh^{-1} \frac x a
      | r = -\arcosh \frac x a
      | c = {{Defof|Real Inverse Hyperbolic Cosine}}
}}
{{eqn | ll= \leadsto
      | l = \int -\cosh^{-1} \frac x a \rd x
      | r = -\int \arcosh \frac x a \rd x
      | c = 
}}
{{eqn | r = -\paren {x \arcosh \dfrac x a - \sqrt {x^2 - a^2} + C}
      | c = Primitive of $\arcosh \dfrac x a$
}}
{{eqn | r = \paren {-\cosh^{-1} \dfrac x a} + \sqrt {x^2 - a^2} + C
      | c = {{Defof|Real Inverse Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Inverse Hyperbolic Cosine of x over a/Corollary

:$\ds \int x \paren {-\cosh^{-1} \frac x a} \rd x = \paren {\dfrac {x^2} 2 - \dfrac {a^2} 4} \paren {-\cosh^{-1} \frac x a} + \dfrac {x \sqrt {x^2 - a^2} } 4 + C$
where $-\cosh^{-1}$ denotes the negative branch of the real inverse hyperbolic cosine multifunction.

Proof:
{{begin-eqn}}
{{eqn | l = -\cosh^{-1} \frac x a
      | r = -\arcosh \frac x a
      | c = {{Defof|Real Inverse Hyperbolic Cosine}}
}}
{{eqn | ll= \leadsto
      | l = \int x \paren {-\cosh^{-1} \frac x a} \rd x
      | r = -\int x \arcosh \frac x a \rd x
      | c = 
}}
{{eqn | r = -\paren {\dfrac {x^2} 2 - \dfrac {a^2} 4} \arcosh \dfrac x a - \dfrac {x \sqrt {x^2 - a^2} } 4 + C
      | c = Primitive of $x \arcosh \dfrac x a$
}}
{{eqn | r = \paren {\dfrac {x^2} 2 - \dfrac {a^2} 4} \paren {-\cosh^{-1} \frac x a} + \dfrac {x \sqrt {x^2 - a^2} } 4
      | c = {{Defof|Real Inverse Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Inverse Hyperbolic Cosine of x over a over x/Corollary

{{begin-eqn}}
{{eqn | l = \int \dfrac 1 x \paren {-\cosh^{-1} \dfrac x a} \rd x
      | r = -\dfrac 1 2 \ln^2 \paren {\dfrac {2 x} a} - \sum_{n \mathop \ge 1} \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2 \paren {2 n}^2} \paren {\frac a x}^{2 n} + C
      | c = 
}}
{{eqn | r = -\dfrac 1 2 \ln^2 \paren {\dfrac {2 x} a} - \dfrac 1 {2 \times 2^2} \paren {\dfrac a x}^2 - \dfrac {1 \times 3} {2 \times 4 \times 4^2} \paren {\dfrac a x}^4 - \dfrac {1 \times 3 \times 5} {2 \times 4 \times 6 \times 6^2} \paren {\dfrac a x}^6 + \dotsb + C
      | c = 
}}
{{end-eqn}}
where $-\cosh^{-1}$ denotes the negative branch of the real inverse hyperbolic cosine multifunction.

Proof:
{{begin-eqn}}
{{eqn | l = -\cosh^{-1} \frac x a
      | r = -\arcosh \frac x a
      | c = {{Defof|Real Inverse Hyperbolic Cosine}}
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac 1 x \paren {-\cosh^{-1} \dfrac x a} \rd x
      | r = -\int \dfrac 1 x \arcosh \dfrac x a \rd x
      | c = 
}}
{{eqn | r = -\paren {\dfrac 1 2 \ln^2 \paren {\dfrac {2 x} a} + \sum_{n \mathop \ge 1} \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2 \paren {2 n}^2} \paren {\frac a x}^{2 n} + C}
      | c = Primitive of $\arcosh \dfrac x a$
}}
{{eqn | r = -\dfrac 1 2 \ln^2 \paren {\dfrac {2 x} a} - \sum_{n \mathop \ge 1} \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2 \paren {2 n}^2} \paren {\frac a x}^{2 n} + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Inverse Hyperbolic Secant of x over a/Corollary

:$\ds \int \sech^{-1} \frac x a \rd x = -x \paren {-\sech^{-1} \dfrac x a} - a \arcsin \dfrac x a + C$
where $-\sech^{-1}$ denotes the negative branch of the real inverse hyperbolic secant multifunction.

Proof:
{{begin-eqn}}
{{eqn | l = -\sech^{-1} \frac x a
      | r = -\arsech \frac x a
      | c = {{Defof|Real Inverse Hyperbolic Secant}}
}}
{{eqn | ll= \leadsto
      | l = \int -\sech^{-1} \frac x a \rd x
      | r = -\int \arsech \frac x a \rd x
      | c = 
}}
{{eqn | r = -\paren {x \arsech \dfrac x a + a \arcsin \dfrac x a + C}
      | c = Primitive of $\arsech \dfrac x a$
}}
{{eqn | r = -x \paren {-\sech^{-1} \dfrac x a} - a \arcsin \dfrac x a + C
      | c = {{Defof|Real Inverse Hyperbolic Secant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of x by Inverse Hyperbolic Cosine of x over a/Corollary

:$\ds \int x^m \paren {-\cosh^{-1} \frac x a} \rd x = \dfrac {x^{m + 1} } {m + 1} \paren {-\cosh^{-1} \frac x a} + \dfrac 1 {m + 1} \int \dfrac {x^{m + 1} } {\sqrt {x^2 - a^2} } \rd x + C$
where $-\cosh^{-1}$ denotes the negative branch of the real inverse hyperbolic cosine multifunction.

Proof:
{{begin-eqn}}
{{eqn | l = -\cosh^{-1} \frac x a
      | r = -\arcosh \frac x a
      | c = {{Defof|Real Inverse Hyperbolic Cosine}}
}}
{{eqn | ll= \leadsto
      | l = \int x^m \paren {-\cosh^{-1} \frac x a} \rd x
      | r = -\int x^m \arcosh \frac x a \rd x
      | c = 
}}
{{eqn | r = -\paren {\dfrac {x^{m + 1} } {m + 1} \arcosh \dfrac x a - \dfrac 1 {m + 1} \int \dfrac {x^{m + 1} } {\sqrt {x^2 - a^2} } \rd x + C}
      | c = Primitive of $x^m \arcosh \dfrac x a$
}}
{{eqn | r = \dfrac {x^{m + 1} } {m + 1} \paren {-\cosh^{-1} \frac x a} + \dfrac 1 {m + 1} \int \dfrac {x^{m + 1} } {\sqrt {x^2 - a^2} } \rd x + C
      | c = {{Defof|Real Inverse Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Inverse Hyperbolic Secant of x over a/Corollary

:$\ds \int x \paren {-\sech^{-1} \frac x a} \rd x = -\dfrac {x^2} 2 \paren {-\sech^{-1} \frac x a} + \dfrac {a \sqrt {a^2 - x^2} } 2 + C$
where $-\sech^{-1}$ denotes the negative branch of the real inverse hyperbolic secant multifunction.

Proof:
{{begin-eqn}}
{{eqn | l = -\sech^{-1} \frac x a
      | r = -\arsech \frac x a
      | c = {{Defof|Real Inverse Hyperbolic Secant}}
}}
{{eqn | ll= \leadsto
      | l = \int x \paren {-\sech^{-1} \frac x a} \rd x
      | r = -\int x \arsech \frac x a \rd x
      | c = 
}}
{{eqn | r = -\paren {\dfrac {x^2} 2 \arsech \dfrac x a - \dfrac {a \sqrt {a^2 - x^2} } 2 + C}
      | c = Primitive of $x \arsech \dfrac x a$
}}
{{eqn | r = -\dfrac {x^2} 2 \paren {-\sech^{-1} \frac x a} + \dfrac {a \sqrt {a^2 - x^2} } 2 + C
      | c = {{Defof|Real Inverse Hyperbolic Secant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Inverse Hyperbolic Secant of x over a over x/Corollary

{{begin-eqn}}
{{eqn | l = \int \dfrac 1 x \paren {-\sech^{-1} \dfrac x a} \rd x
      | r = \frac 1 2 \map \ln {\dfrac a x} \map \ln {\dfrac {4 a} x} + \sum_{n \mathop \ge 1} \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2 \paren {2 n}^2} \paren {\frac x a}^{2 n} + C
      | c = 
}}
{{eqn | r = \dfrac 1 2 \map \ln {\dfrac a x} \map \ln {\dfrac {4 a} x} + \dfrac 1 {2 \times 2^2} \paren {\dfrac x a}^2 - \dfrac {1 \times 3} {2 \times 4 \times 4^2} \paren {\dfrac x a}^4 - \dfrac {1 \times 3 \times 5} {2 \times 4 \times 6 \times 6^2} \paren {\dfrac x a}^6 + C
      | c = 
}}
{{end-eqn}}
where $-\sech^{-1}$ denotes the negative branch of the real inverse hyperbolic secant multifunction.

Proof:
{{begin-eqn}}
{{eqn | l = -\sech^{-1} \frac x a
      | r = -\arsech \frac x a
      | c = {{Defof|Real Inverse Hyperbolic Secant}}
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac 1 x \paren {-\sech^{-1} \dfrac x a} \rd x
      | r = -\int \dfrac 1 x \arsech \dfrac x a \rd x
      | c = 
}}
{{eqn | r = -\paren {-\frac 1 2 \map \ln {\dfrac a x} \map \ln {\dfrac {4 a} x} - \sum_{n \mathop \ge 1} \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2 \paren {2 n}^2} \paren {\frac x a}^{2 n} + C}
      | c = Primitive of $\dfrac 1 x \arsech \dfrac x a$
}}
{{eqn | r = \frac 1 2 \map \ln {\dfrac a x} \map \ln {\dfrac {4 a} x} + \sum_{n \mathop \ge 1} \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2 \paren {2 n}^2} \paren {\frac x a}^{2 n} + C
      | c = {{Defof|Real Inverse Hyperbolic Secant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of x by Inverse Hyperbolic Secant of x over a/Corollary

:$\ds \int x^m \paren {-\sech^{-1} \frac x a} \rd x = \dfrac {x^{m + 1} } {m + 1} \paren {-\sech^{-1} \frac x a} - \dfrac a {m + 1} \int \dfrac {x^m} {\sqrt {a^2 - x^2} } \rd x + C$
where $-\sech^{-1}$ denotes the negative branch of the real inverse hyperbolic secant multifunction.

Proof:
{{begin-eqn}}
{{eqn | l = -\sech^{-1} \frac x a
      | r = -\arsech \frac x a
      | c = {{Defof|Real Inverse Hyperbolic Secant}}
}}
{{eqn | ll= \leadsto
      | l = \int x^m \paren {-\sech^{-1} \frac x a} \rd x
      | r = -\int x^m \arsech \frac x a \rd x
      | c = 
}}
{{eqn | r = -\paren {\dfrac {x^{m + 1} } {m + 1} \arsech \dfrac x a + \dfrac a {m + 1} \int \dfrac {x^m} {\sqrt {a^2 - x^2} } \rd x + C}
      | c = Primitive of $x^m \arsech \dfrac x a$
}}
{{eqn | r = \dfrac {x^{m + 1} } {m + 1} \paren {-\sech^{-1} \frac x a} - \dfrac a {m + 1} \int \dfrac {x^m} {\sqrt {a^2 - x^2} } \rd x + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}