avewright/proofwiki-math huggingface dataset:
Theorem: Sum of nth Fibonacci Number over nth Power of 2

:$\ds \sum_{n \mathop = 0}^\infty \frac {F_n} {2^n} = 2$
where $F_n$ is the $n$th Fibonacci number.

Proof:
Let us define a sample space which satisfies the Kolmogorov Axioms such that it is the set of all combinations of flipping a fair coin  until you receive two heads in a row.
Let $X_n$ be the event of some outcome from flipping $n$ fair coins in a row, then $\map \Pr {X_n} = \dfrac 1 {2^n}$.
In the sample space defined above, we now demonstrate that for a given number of flips $n$, there are exactly $F_{n - 1}$ outcomes contained in the sample space.
=== Illustration ===
:<nowiki>$\begin{array}{c|c|cc}
n & \map f n & \text {Sample Space}: \Omega \\
\hline
1 & 0 & \text {impossible} \\
2 & 1 & HH \\
3 & 1 & THH \\
4 & 2 & (HTHH), (TTHH) \\
5 & 3 & (THTHH), (HTTHH), (TTTHH) \\
6 & 5 & (HTHTHH), (TTHTHH), (THTTHH), (HTTTHH), (TTTTHH) \\
\hline
\cdots & \cdots & \cdots \\
\hline
n & F_{n - 1} & \cdots \\
\hline
\end{array}$</nowiki>
Reviewing the illustration above, for any given value of $n$:
For '''ALL''' combinations displayed in row $n$ (that is $\map f n$) , we can place a $T$ in front and that new combination would exist in the sample space for $\paren {n + 1}$.
For example:
:$\paren {HTHH}, \paren {TTHH} \to \paren {THTHH}, \paren {TTTHH}$
However, we also see that for only those combinations starting with a $T$ (that is $\map f {n - 1}$), can we place an $H$ in front and that new combination will also exist in the sample space for $\paren {n + 1}$.
For example:
:$\paren {TTHH} \to \paren {HTTHH}$
Therefore, we have:
{{begin-eqn}}
{{eqn | l = \map f n
      | r = F_{n - 1}
      | c = 
}}
{{eqn | l = \map f {n + 1}
      | r = \map f n + \map f {n - 1}
      | c = $\map f n$ is adding a $T$ in front and $\map f {n - 1}$ is adding an $H$ in front 
}}
{{eqn | r = F_{n - 1} + F_{n - 2}
      | c = 
}}
{{eqn | r = F_n
      | c = 
}}
{{end-eqn}}
The sum of the probabilities of outcomes in a sample space is one by the second Kolmogorov Axiom.  
{{begin-axiom}}
{{axiom | n = \text {II}
        | ml= \map \Pr \Omega
        | mo= =
        | mr= 1
}}
{{end-axiom}}
Hence:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^\infty \frac {F_{n - 1} } {2^n}
      | r = 1
      | c = $2$nd Kolmogorov Axiom
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 0}^\infty \frac {F_n} {2^{n + 1} }
      | r = 1
      | c = reindexing the sum
}}
{{eqn | ll= \leadsto
      | l = \sum_{n \mathop = 0}^\infty \frac {F_n} {2^n}
      | r = 2
      | c = multiplying both sides by $2$
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of nth Fibonacci Number over nth Power of 2

:$\ds \sum_{n \mathop = 0}^\infty \frac {F_n} {2^n} = 2$
where $F_n$ is the $n$th Fibonacci number.

Proof:
From the Euler-Binet Formula, we have:
:$F_n = \dfrac {\phi^n - \paren {1 - \phi}^n} {\sqrt 5}$
Therefore:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 0}^\infty \frac{F_n} {2^n}
      | r = \sum_{n \mathop = 0}^\infty \dfrac {\phi^n - \paren {1 - \phi}^n} {\sqrt 5 \times 2^n}
      | c = Euler-Binet Formula
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \dfrac {\paren {\dfrac {1 + \sqrt 5} 2}^n - \paren {1 - \paren {\dfrac {1 + \sqrt 5} 2 } }^n} {\sqrt 5 \times 2^n}
      | c = {{Defof|Golden Mean}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \dfrac {\paren {\dfrac {1 + \sqrt 5} 2}^n - \paren {\dfrac {1 - \sqrt 5} 2 }^n} {\sqrt 5 \times 2^n}
      | c = 
}}
{{eqn | r = \dfrac 1 {\sqrt 5} \sum_{n \mathop = 0}^\infty \paren {\dfrac {1 + \sqrt 5} 4}^n - \dfrac 1 {\sqrt 5} \sum_{n \mathop = 0}^\infty \paren {\dfrac {1 - \sqrt 5} 4}^n
      | c = Product of Powers and $2^2 = 4$
}}
{{eqn | r = \dfrac 1 {\sqrt 5} \paren {\dfrac 1 {1 - \dfrac {1 + \sqrt 5 } 4} } - \dfrac 1 {\sqrt 5} \paren {\dfrac 1 {1 - \dfrac {1 - \sqrt 5} 4} }
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \dfrac 1 {\sqrt 5} \paren {\dfrac 1 {1 - \dfrac {1 + \sqrt 5} 4} } \times \dfrac 4 4 - \dfrac 1 {\sqrt 5} \paren {\dfrac 1 {1 - \dfrac {1 - \sqrt 5} 4} } \times \dfrac 4 4
      | c = multiplying top and bottom by $4$
}}
{{eqn | r = \dfrac 4 {\sqrt 5} \paren {\dfrac 1 {3 - \sqrt 5} } - \dfrac 4 {\sqrt 5} \paren {\dfrac 1 {3 + \sqrt 5} }
      | c = 
}}
{{eqn | r = \dfrac 4 {\sqrt 5} \paren {\dfrac 1 {3 - \sqrt 5} } \times \paren {\dfrac {3 + \sqrt 5} {3 + \sqrt 5} } - \dfrac 4 {\sqrt 5} \paren {\dfrac 1 {3 + \sqrt 5} } \times \paren {\dfrac {3 - \sqrt 5} {3 - \sqrt 5} }
      | c = multiplying top and bottom by $\paren {3 + \sqrt 5}$ and by $\paren {3 - \sqrt 5}$
}}
{{eqn | r = \dfrac 4 {\sqrt 5} \paren {\dfrac {3 + \sqrt 5} 4} - \dfrac 4 {\sqrt 5} \paren {\dfrac {3 - \sqrt 5} 4}
      | c = 
}}
{{eqn | r = \paren {\dfrac {3 + \sqrt 5} {\sqrt 5} } - \paren {\dfrac {3 - \sqrt 5} {\sqrt 5} }
      | c = 
}}
{{eqn | r = 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of nth Fibonacci Number over nth Power of 2

:$\ds \sum_{n \mathop = 0}^\infty \frac {F_n} {2^n} = 2$
where $F_n$ is the $n$th Fibonacci number.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^{\infty} F_k z^k
      | r = \dfrac z {1 - z - z^2}
      | c = Generating Function for Fibonacci Numbers holds for all $\cmod {z} < \dfrac 1 {\phi} \approx 0.62$
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 0}^{\infty} \frac {F_k} {2^k}
      | r = \dfrac {\dfrac 1 2} {1 - \dfrac 1 2 - \paren {\dfrac 1 2}^2}
      | c = substituting $z = \dfrac 1 2$
}}
{{eqn | r = \dfrac {1 / 2} {1 / 4}
      | c = 
}}
{{eqn | r = 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Second Order ODE/y'' = f(x)

The second order ODE:
:$\dfrac {\d^2 y} {\d x^2} = \map f x$
has the general solution:
:$\ds y = \iint \map f x \rd x \rd x + C_1 x + C_2$
where $C_1$ and $C_2$ are arbitrary constants.

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\d^2 y} {\d x^2}
      | r = \map f x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d^2 y} {\d x^2} \rd y
      | r = \int \map f x \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d y} {\d x}
      | r = \int \map f x \rd x + C_1
      | c = where $C_1$ is an arbitrary constant
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d y} {\d x} \rd y
      | r = \int \paren {\int \map f x \rd x + C_1} \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | r = \int \paren {\int \map f x \rd x} \rd x + \int C_1 \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \iint \map f x \rd x \rd x + C_1 x + C_2
      | c = Primitive of Power: $C_2$ is another arbitrary constant
}}
{{end-eqn}}
{{qed}}
Theorem: Recurrence Relation for Polygamma Function

:$\map {\psi_n} {z + 1} = \map {\psi_n} z + \paren {-1}^n n! z^{-n - 1}$
where:
:$\psi_n$ denote the $n$th polygamma function
:$z \in \C \setminus \Z_{\le 0}$.

Proof:
{{begin-eqn}}
{{eqn | l = \map \Gamma {z + 1}
	  | r = z \map \Gamma z 
      | c = Gamma Difference Equation
}}
{{eqn | ll= \leadsto
	  | l = \map \ln {\map \Gamma {z + 1} }
	  | r = \map \ln {z \map \Gamma z}
      | c = applying $\ln$ on both sides
}}
{{eqn | r = \ln z + \map \ln {\map \Gamma z}
      | c = Sum of Logarithms
}}
{{eqn | ll= \leadsto
	  | l = \dfrac \d {\d z} \map \ln {\map \Gamma {z + 1} }
	  | r = \dfrac \d {\d z} \ln z + \dfrac \d {\d z} \map \ln {\map \Gamma z}
      | c = differentiation {{WRT|Differentiation}} $z$
}}
{{eqn | ll= \leadsto
	  | l = \dfrac {\map {\Gamma'} {z + 1} } {\map \Gamma {z + 1} }
	  | r = z^{-1} + \dfrac {\map {\Gamma'} z} {\map \Gamma z}
      | c = Derivative of Natural Logarithm Function, Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
	  | l = \map \psi {z + 1}
	  | r = \map \psi z + z^{-1}
      | c = {{Defof|Digamma Function}}
}}
{{eqn | ll= \leadsto
	  | l = \dfrac {\d^n} {\d z^n} \map \psi {z + 1}
	  | r = \dfrac {\d^n} {\d z^n} \map \psi z + \dfrac {\d^n} {\d z^n} {z^{-1} }
      | c = taking $n$th derivative
}}
{{eqn | ll= \leadsto
	  | l = \map {\psi_n} {z + 1}
	  | r = \map {\psi_n} z + \paren {-1}^n n! z^{-n - 1}
      | c = {{Defof|Polygamma Function}} and {{Corollary|Nth Derivative of Reciprocal of Mth Power}}
}}
{{end-eqn}}
{{qed}}
Theorem: Second Order ODE/y'' = f(y)

The second order ODE:
:$\dfrac {\d^2 y} {\d x^2} = \map f y$
has the general solution:
:$\dfrac {\sqrt 2} 2 \ds \int \dfrac {\d y} {\sqrt {\ds \int \map f y \rd y + C_1} } = x + C_2$
where $C_1$ and $C_2$ are arbitrary constants.

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {\d^2 y} {\d x^2}
      | r = \map f y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 \dfrac {\d y} {\d x} \dfrac {\d^2 y} {\d x^2}
      | r = 2 \map f y \dfrac {\d y} {\d x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int 2 \dfrac {\d y} {\d x} \dfrac {\d^2 y} {\d x^2} \rd x
      | r = \int 2 \map f y \dfrac {\d y} {\d x} \rd x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {\dfrac {\d y} {\d x} }^2
      | r = 2 \int \map f y \rd y + C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d y} {\d x}
      | r = \sqrt {2 \int \map f y \rd y + C_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d y} {\sqrt {2 \ds \int \map f y \rd y + C_1} }
      | r = \int \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\sqrt 2} 2 \int \dfrac {\d y} {\sqrt {\ds \int \map f y \rd y + C_1} }
      | r = x + C_2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Lie Algebra is Anticommutative

Let $L$ be a Lie algebra.
Then $L$ is anticommutative:
:$\forall a, b \in L: \sqbrk {a, b} = -\sqbrk {b, a}$
where $\sqbrk {\, \cdot, \cdot \,}$ denotes the bilinear mapping over $L$.

Proof:
{{begin-eqn}}
{{eqn | l = \sqbrk {a + b, a + b}
      | r = \sqbrk {a, a + b} + \sqbrk {b, a + b}
      | c = {{Defof|Bilinear Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \sqbrk {a + b, a + b}
      | r = \sqbrk {a, a} + \sqbrk {a, b} + \sqbrk{b, a} + \sqbrk {b, b}
      | c = {{Defof|Bilinear Mapping}}
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = \sqbrk {a, b} + \sqbrk {b, a}
      | c = {{Lie-algebra-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = \sqbrk {a, b}
      | r = -\sqbrk {b, a}
}}
{{end-eqn}}
{{qed}}
Theorem: Two Planes have Line in Common/Hilbert's Axioms

Two planes $\alpha, \beta$ have no point in common or a straight line $a$ in common.

Proof:
{{tidy}}
{{MissingLinks}}
By Law of Excluded Middle, $\alpha$ and $\beta$ have no point in common, or some point $A$ in common.
In the former case, the theorem holds trivially.
In the latter, by Axiom $\text I, 6$, there is a second point $B$ lying on both $\alpha$ and $\beta$.
By Axiom $I, 1$, there is a straight line $a$ containing both $A$ and $B$.
Then, by Axiom $I, 5$, every point of $a$ lies on both $\alpha$ and $\beta$.
{{qed}}
Theorem: Relation between Direction Cosines

Let $\LL$ be a line embedded in a Cartesian $3$-space.
Let $l$, $m$ and $n$ be the direction cosines of $\LL$ {{WRT}} the $x$-axis, $y$-axis and $z$-axis respectively.
Then:
:$l^2 + m^2 + n^2 = 1$

Proof:
Let $\mathbf r$ be a vector quantity embedded in a Cartesian $3$-space that is parallel to $\LL$.
Let the direction angles which $\mathbf r$ makes with the $x$-axis, $y$-axis and $z$-axis be $\alpha$, $\beta$ and $\gamma$ respectively.
From Components of Vector in terms of Direction Cosines:
:$l = \cos \alpha = \dfrac {r_x} r$
:$m = \cos \beta = \dfrac {r_y} r$
:$n = \cos \gamma = \dfrac {r_z} r$
where $r = \size {\mathbf r}$ and $r_x$ is the component of $\mathbf r$ along the $x$-axis (and similarly for $r_y$ and $r_z$).
Therefore:
{{begin-eqn}}
{{eqn | l = l^2 + m^2 + n^2
      | r = \paren {\frac {r_x} r}^2 + \paren {\frac {r_y} r}^2 + \paren {\frac {r_z} r}^2
}}
{{eqn | r = \frac {r_x^2 + r_y^2 + r_z^2} {r^2}
}}
{{eqn | r = \frac {r^2} {r^2}
      | c = {{Defof|Vector Length|subdef = Real Vector Space}}
}}
{{eqn | r = 1
}}
{{end-eqn}}
{{qed}}
Theorem: Integral Form of Polygamma Function

Let $z$ be a complex number with a positive real part.
Then: 
:$\ds \map {\psi_n} z = \paren {-1}^{n + 1} \int_0^\infty \frac {t^n e^{-z t} } {1 - e^{-t} } \rd t$
where $\map {\psi_n} z$ denotes the $n$th polygamma function.

Proof:
From Gauss's Integral Form of Digamma Function, we have:
:$\ds \map \psi z = \int_0^\infty \paren {\frac {e^{-t} } t - \frac {e^{-z t} } {1 - e^{-t} } } \rd t$
Therefore:
{{begin-eqn}}
{{eqn | l = \map \psi z 
      | r = \int_0^\infty \paren {\frac {e^{-t} } t - \frac {e^{-z t} } {1 - e^{-t} } } \rd t
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \dfrac {\d^n} {\d z^n} \map \psi z
      | r = \dfrac {\d^n} {\d z^n} \paren {\int_0^\infty \paren {\frac {e^{-t} } t - \frac {e^{-z t} } {1 - e^{-t} } } \rd t }
      | c = taking $n$th derivative
}}
{{eqn | r = \paren {-1}^{n + 1} \int_0^\infty \frac {t^n e^{-z t} } {1 - e^{-t} } \rd t
      | c = {{Corollary|Derivative of Exponential Function|1}}
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Disconnected Space

{{TFAE|def = Disconnected Space}}
Let $T = \struct {S, \tau}$ be a topological space.

Proof:
By definition $1$, $T$ is '''disconnected''' {{iff}} $T$ is not connected.
{{Recall|Connected Topological Space|connected topological space}}
{{:Definition:Connected Topological Space/Definition 7}}
Hence precisely a '''disconnected space''' by definition $2$.
{{qed}}
Category:Disconnected Spaces
oko18c2v3q9n2m9u8zo4x5sjowq29e0
Theorem: Sum of Trigamma of n plus 3 over n plus 2

{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 0}^\infty  \dfrac {\map {\psi_1} {n + 3} } {\paren {n + 2} }
      | r = \dfrac {\map {\psi_1} 3} 2 + \dfrac {\map {\psi_1} 4} 3 + \dfrac {\map {\psi_1} 5} 4 + \dfrac {\map {\psi_1} 6} 5 + \cdots
      | c = 
}}
{{eqn | r = \map \zeta 3 - \map \zeta 2 + 1
      | c = 
}}
{{end-eqn}}
where:
:$\map {\psi_1} n$ is the trigamma function of $n$
:$\map \zeta 2$ is the Riemann $\zeta$ function of $2$
:$\map \zeta 3$ is Apéry's constant: the Riemann $\zeta$ function of $3$.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 0}^\infty  \dfrac {\map {\psi_1} {n + 3} } {\paren {n + 2} }
      | r = \sum_{n \mathop = 1}^\infty  \dfrac {\map {\psi_1} {n + 1} } n - \map {\psi_1} 2
      | c = $n \to n - 2$
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty  \dfrac {\map {\psi_1} {n + 1} } n - \paren {\map {\psi_1} 1 - 1}
      | c = Recurrence Relation for Polygamma Function: $\map {\psi_1} 2 = \map {\psi_1} 1 - 1$
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty  \dfrac {\map {\psi_1} {n + 1} } n - \map \zeta 2 + 1
      | c = Polygamma Function in terms of Hurwitz Zeta Function: $\map {\psi_1} 1 = \map \Gamma 2 \map \zeta {2, 1}$
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \paren {-\int_0^1 \frac {x^{\paren {n + 1} - 1} \ln x} {n \paren {1 - x} } \rd x} - \map \zeta 2 + 1
      | c = Integral Form of Polygamma Function: $\ds \map {\psi_1} z = -\int_0^1 \frac {u^{z - 1} \ln u} {1 - u} \rd u$
}}
{{eqn | r = \int_0^1 \paren {-\sum_{n \mathop = 1}^\infty \frac {x^n} n} \frac {\ln x} {\paren {1 - x} } \rd x  - \map \zeta 2 + 1
      | c = Tonelli's Theorem
}}
{{eqn | r = \int_0^1 \frac {\map \ln {1 - x} \ln x} {\paren {1 - x} } \rd x  - \map \zeta {2} + 1
      | c = Power Series Expansion for Logarithm of $1 - x$: $\ds \map \ln {1 - x} = -\sum_{n \mathop = 1}^\infty \frac {x^n} n$
}}
{{eqn | r = \map \zeta 3 - \map \zeta 2 + 1
      | c = Definite Integral: $\ds \int_0^1 \dfrac {\ln x \map \ln {1 - x} } {\paren {1 - x} } \rd x$
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One minus x over One minus x

:$\ds \int_0^1 \dfrac {\ln x \map \ln {1 - x} } {\paren {1 - x} } \rd x = \map \zeta 3$
where $\map \zeta 3$ is Apéry's constant: the Riemann $\zeta$ function of $3$.

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^1 \dfrac {\ln x \map \ln {1 - x} } {\paren {1 - x} } \rd x
	    | r = \int_1^0 \dfrac {\map \ln {1 - u} \ln u } u \paren {-\rd u}
	    | c = $x \to \paren {1 - u}$ and $\rd x \to -\rd u$
}}
{{eqn	| r = \int_0^1 \dfrac {\map \ln {1 - u} \ln u } u \rd u
	    | c = reversing limits of integration
}}
{{eqn	| r = -\int_0^1 \frac {\ln u} u \paren {\sum_{n \mathop = 1}^\infty \frac {u^n} n}
	    | c = Power Series Expansion for $\map \ln {1 - x}$
}}
{{eqn	| r = -\int_0^1 \ln u \paren {\sum_{n \mathop = 1}^\infty \frac {u^{n - 1} } n}
	    | c = 
}}
{{eqn	| r = -\sum_{n \mathop = 1}^\infty \frac 1 n \paren {\int_0^1 u^{n - 1} \ln u \rd u}
	    | c = Fubini's Theorem
}}
{{eqn	| r = \paren {-1}^2 \sum_{n \mathop = 1}^\infty \frac 1 n \paren {\frac {\map \Gamma 2} {\paren {\paren {n - 1} + 1}^2} }
	    | c = Definite Integral from $0$ to $1$ of $x^m \paren {\ln x}^n$
}}
{{eqn	| r = 1! \sum_{n \mathop = 1}^\infty \frac 1 {n^3}
	    | c = Gamma Function Extends Factorial
}}
{{eqn	| r = \map \zeta {3}
	    | c = {{Defof|Apéry's Constant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to 1 of Logarithm of x by Logarithm of One minus x over One minus x

:$\ds \int_0^1 \dfrac {\ln x \map \ln {1 - x} } {\paren {1 - x} } \rd x = \map \zeta 3$
where $\map \zeta 3$ is Apéry's constant: the Riemann $\zeta$ function of $3$.

Proof:
With a view to expressing the primitive in the form:
{{begin-eqn}}
{{eqn | l = \int u \frac {\d v} {\d x} \rd x
      | r = u v - \int v \frac {\d u} {\d x} \rd x
      | c = Integration by Parts
}}
{{end-eqn}}
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \ln x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac 1 x
      | c = Derivative of $\ln x$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \frac {\map \ln {1 - x} } {\paren {1 - x} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = - \frac 1 2 \paren {\map \ln {1 - x} }^2
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int_0^1 \frac {\map \ln {1 - x} \ln x } {\paren {1 - x} } \rd x 
      | r = \intlimits {\ln x \paren {-\frac 1 2 \paren {\map \ln {1 - x} }^2} } 0 1 + \frac 1 2 \int_0^1 \frac {\paren {\map \ln {1 - x} }^2} x \rd x 
      | c = Integration by Parts
}}
{{eqn | r = 0 + \frac 1 2 \int_0^1 \frac {\paren {\map \ln {1 - x} }^2} x \rd x 
      | c = 
}}
{{eqn | r = \frac 1 2 \int_1^0 \frac {\paren {\map \ln u}^2} {1 - u} \paren {-\d u} 
      | c = $x \to \paren {1 - u}$ and $\rd x \to -\rd u$
}}
{{eqn | r = \frac 1 2 \int_0^1 \frac {\paren {-\map \ln u} \paren {-\map \ln u} } {1 - u} \rd u  
      | c = reversing limits of integration
}}
{{eqn | r = \frac 1 2 \int_0^1 \frac {\paren {\map \ln {\dfrac 1 u} }^{3 - 1} } {1 - u} \rd u 
      | c = Logarithm of Reciprocal
}}
{{eqn | r = \frac {\map \zeta 3 \map \Gamma 3} 2 
      | c = Integral Representation of Riemann Zeta Function in terms of Gamma Function: $\ds \map \zeta s \map \Gamma s = \int_0^1 \frac {\paren {\map \ln {\frac 1 u} }^{s - 1} } {1 - u} \rd u$
}}
{{eqn | r = \map \zeta 3 
      | c = Gamma Function of 3
}}
{{end-eqn}}
{{qed}}
Theorem: Discriminant of Quadratic Equation

Let $\QQ$ be the quadratic equation:
:$a x^2 + b x + c$
The discriminant of $\QQ$ is given by:
:$\map \Delta \QQ = b^2 - 4 a c$

Proof:
Let $\alpha_1$ and $\alpha_2$ be the roots of $\QQ$.
We have:
{{begin-eqn}}
{{eqn | l = \map \Delta \QQ
      | r = a^2 \paren {\alpha_1 - \alpha_2}^2
      | c = Discriminant Example: Quadratic
}}
{{eqn | r = a^2 \paren { {\alpha_1}^2 - 2 \alpha_1 \alpha_2 + {\alpha_2}^2}
      | c = Square of Difference
}}
{{eqn | r = a^2 \paren { {\alpha_1}^2 + 2 \alpha_1 \alpha_2 + {\alpha_2}^2 - 4 \alpha_1 \alpha_2}
      | c = adding and subtracting $2 \alpha_1 \alpha_2$
}}
{{eqn | r = a^2 \paren { \paren {\alpha_1 + \alpha_2}^2 - 4 \alpha_1 \alpha_2}
      | c = Square of Sum
}}
{{eqn | r = a^2 \paren { \paren {-\dfrac b a}^2 - 4 \dfrac c a}
      | c = Sum of Roots of Quadratic Equation, Product of Roots of Quadratic Equation
}}
{{eqn | r = b^2 - 4 a c
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Digamma Function of One

:$\map \psi 1 = -\gamma$

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi z
      | r = \dfrac {\map {\Gamma'} z} {\map \Gamma z} 
      | c = {{Defof|Digamma Function}}
}}
{{eqn | r = -\gamma + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {z + n - 1} }
      | c = Reciprocal times Derivative of Gamma Function
}}
{{eqn | ll = \leadsto
      | l = \map \psi 1
      | r = -\gamma + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {1 + n - 1} }
      | c = $z \gets 1$
}}
{{eqn | r = -\gamma + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 n}
      | c = 
}}
{{eqn | r = -\gamma
      | c = noting that the summation is an empty sum
}}
{{end-eqn}}
{{qed}}
Category:Examples of Digamma Function
Category:Euler-Mascheroni Constant
kt9y7fch4fj3ewea9ijagbivg5lakro
Theorem: Digamma Function of One

:$\map \psi 1 = -\gamma$

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi {\frac 1 4}
      | r = -\gamma - \ln 8 - \frac \pi 2 \map \cot {\frac 1 4 \pi} + 2 \sum_{n \mathop = 1}^{\ceiling {4 / 2} - 1} \map \cos {\frac {2 \pi n} 4} \map \ln {\map \sin {\frac {\pi n} 4} }
      | c = Gauss's Digamma Theorem
}}
{{eqn | r = -\gamma - 3 \ln 2 - \frac \pi 2 \times 1 + 2 \times 0 \times \map \ln {\frac {\sqrt 2} 2}
      | c = {{cot|45}}, {{cos|90}}, {{sin|45}} and Sum of Logarithms
}}
{{eqn | r = -\gamma - 3 \ln 2 - \dfrac \pi 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Digamma Function of One

:$\map \psi 1 = -\gamma$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^{n - 1} \map \psi {\frac k n}
      | r = -\paren {n - 1} \gamma - n \ln n
      | c = {{Corollary|Digamma Additive Formula}}
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^{4 - 1} \map \psi {\frac k 4}
      | r = -\paren {4 - 1} \gamma - 4 \ln 4
      | c = 
}}
{{eqn | ll= \leadsto
      | n = 1
      | l = \map \psi {\frac 1 4} + \map \psi {\frac 2 4} + \map \psi {\frac 3 4}
      | r = -3 \gamma - 4 \ln 4
      | c = 
}}
{{eqn | n = 2
      | l = \map \psi {\frac 1 4} - \map \psi {\frac 3 4}
      | r = -\pi \map \cot {\frac \pi 4}
      | c = Digamma Reflection Formula
}}
{{eqn | ll= \leadsto
      | l = 2 \map \psi {\frac 1 4} + \map \psi {\frac 1 2}
      | r = -3 \gamma - 4 \ln 4 - \pi \map \cot {\frac \pi 4}
      | c = adding lines $1$ and $2$
}}
{{eqn | ll= \leadsto
      | l = 2 \map \psi {\frac 1 4}
      | r = -3 \gamma - 4 \ln 4 - \pi \map \cot {\frac \pi 4} - \map \psi {\frac 1 2}
      | c = subtracting $\map \psi {\frac 1 2}$ from both sides
}}
{{eqn | r = -3 \gamma - 8 \ln 2 - \pi \paren 1 - \paren {-\gamma - 2 \ln 2}
      | c = Digamma Function of One Half, Logarithm of Power and {{cot|45}}
}}
{{eqn | r = -2 \gamma - 6 \ln 2 -\pi
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \map \psi {\frac 1 4}
      | r = -\gamma - 3 \ln 2 - \dfrac \pi 2
      | c = dividing by $2$
}}
{{end-eqn}}
{{qed}}
Theorem: Digamma Function of One

:$\map \psi 1 = -\gamma$

Proof:
{{begin-eqn}}
{{eqn | l = \map \psi {\frac 1 2}
      | r = -\gamma - \ln 4 - \frac \pi 2 \map \cot {\frac 1 2 \pi} + 2 \sum_{n \mathop = 1}^0 \map \cos {\frac {2 \pi n} 2} \map \ln {\map \sin {\frac {\pi n} 2} }
      | c = Gauss's Digamma Theorem
}}
{{eqn | r = -\gamma - \ln 4
      | c = Cotangent of Right Angle, noting also that the summation is an empty sum
}}
{{eqn | r = -\gamma - 2 \ln 2
      | c = Logarithm of Power
}}
{{end-eqn}}
{{qed}}