avewright/proofwiki-math huggingface dataset:
Theorem: Volume of Circular Cylinder/Slant Height

Let $\CC$ be a circular cylinder such that:
:the bases of $\CC$ are circles of radius $r$
:the slant height of $\CC$ is $l$
:the inclination of the generatrices of $\CC$ to the base of $\CC$ is $\theta$.
The volume $\VV$ of $\CC$ is given by the formula:
:$\VV = \pi r^2 l \sin \theta$

Proof:
Let $h$ denote the height of $\CC$.
From Relation between Slant Height and Height of Cylinder:
:$h = l \sin \theta$
From Volume of Circular Cylinder in terms of Height:
:$\VV = \pi r^2 h$
The result follows.
{{qed}}
Theorem: Volume of Frustum of Right Circular Cone

Let $F$ be a frustum of a right circular cone.
The volume $\VV$ of $F$ is given as:
:$\VV = \dfrac {\pi h \paren {a^2 + a b + b^2} } 3$
where:
:$a$ and $b$ are the radii of the bases of $F$
:$h$ is the altitude of $F$.

Proof:
From Volume of Frustum of Cone or Pyramid:
:$\VV = \dfrac {h \paren {A_1 + A_2 + \sqrt {A_1 A_2} } } 3$
where:
:$A_1$ and $A_2$ are the areas of the bases of $F$
:$h$ is the altitude of $F$.
Here we have that $F$ be a frustum of a right circular cone.
Hence the bases of $F$ are circles.
From Area of Circle, the areas of the bases of $F$ are therefore:
:$A_1 = \pi a^2$
:$A_2 = \pi b^2$
Hence:
{{begin-eqn}}
{{eqn | l = \VV
      | r = \dfrac {h \paren {A_1 + A_2 + \sqrt {A_1 A_2} } } 3
      | c = Volume of Frustum of Cone or Pyramid: see above
}}
{{eqn | r = \dfrac {h \paren {\pi a^2 + \pi b^2 + \sqrt {\pi a^2 \pi b^2} } } 3
      | c = 
}}
{{eqn | r = \dfrac {\pi h \paren {a^2 + b^2 + a b} } 3
      | c = after simplification
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Power Reduction Formulas/Cosine to 6th

:$\cos^6 x = \dfrac {10 + 15 \cos 2 x + 6 \cos 4 x + \cos 6 x} {32}$

Proof:
{{begin-eqn}}
{{eqn | l = \cos 6 x
      | r = 32 \cos^6 x - 48 \cos^4 x + 18 \cos^2 x - 1
      | c = Sextuple Angle Formula for Cosine
}}
{{eqn | ll= \leadsto
      | l = 32 \cos^6 x
      | r = \cos 6 x + 48 \cos^4 x - 18 \cos^2 x + 1
      | c = rearranging
}}
{{eqn | r = \cos 6 x + 48 \paren {\dfrac {3 + 4 \cos 2 x + \cos 4 x} 8} - 18 \paren {\dfrac {1 + \cos 2 x} 2} + 1
      | c = Fourth Power of Cosine, Square of Cosine
}}
{{eqn | r = \cos 6 x + \paren {18 + 24 \cos 2 x + 6 \cos 4 x} - \paren {9 + 9 \cos 2 x} + 1
      | c = multipying out
}}
{{eqn | r = 10 + 15 \cos 2 x + 6 \cos 4 x + \cos 6 x
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \cos^6 x
      | r = \frac {10 + 15 \cos 2 x + 6 \cos 4 x + \cos 6 x} {32}
      | c = dividing both sides by $32$
}}
{{end-eqn}}
{{qed}}
Category:Cosine Function
mwigx9yuwzm88do1iq2h1qm9b0m8epw
Theorem: Septuple Angle Formulas/Cosine

:$\cos 7 \theta = 64 \cos^7 \theta - 112 \cos^5 \theta + 56 \cos^3 \theta - 7 \cos \theta$

Proof:
{{begin-eqn}}
{{eqn | l = \cos 7 \theta + i \sin 7 \theta
      | r = \paren {\cos \theta + i \sin \theta}^7
      | c = De Moivre's Formula
}}
{{eqn | r = \paren {\cos \theta}^7 + \binom 7 1 \paren {\cos \theta}^6 \paren {i \sin \theta} + \binom 7 2 \paren {\cos \theta}^5 \paren {i \sin \theta}^2 + \binom 7 3 \paren {\cos \theta}^4 \paren {i \sin \theta}^3
      | c = Binomial Theorem
}}
{{eqn | o = 
      | ro= +
      | r = \binom 7 4 \paren {\cos \theta}^3 \paren {i \sin \theta}^4 + \binom 7 5 \paren {\cos \theta}^2 \paren {i \sin \theta}^5 + \binom 7 6 \paren {\cos \theta} \paren {i \sin \theta}^6 + \paren {i \sin \theta}^7
}}
{{eqn | r = \cos^7 \theta + 7 i \cos^6 \theta \sin \theta - 21 \cos^5 \sin^2 \theta - 35 i \cos^4 \theta \sin^3 \theta
      | c = substituting for binomial coefficients
}}
{{eqn | o = 
      | ro= +
      | r = 35 \cos^3 \theta \sin^4 \theta + 21 i \cos^2 \theta \sin^5 \theta - 7 \cos \theta \sin^6 \theta - i \sin^7 \theta
      | c = and using $i^2 = -1$
}}
{{eqn | n = 1
      | r = \cos^7 \theta - 21 \cos^5 \sin^2 \theta + 35 \cos^3 \theta \sin^4 \theta - 7 \cos \theta \sin^6 \theta
}}
{{eqn | o = 
      | ro=+
      | r = i \paren {7 \cos^6 \theta \sin \theta - 35 \cos^4 \theta \sin^3 \theta + 21 \cos^2 \theta \sin^5 \theta - \sin^7 \theta}
      | c = rearranging
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \cos 7 \theta
      | r = \cos^7 \theta - 21 \cos^5 \sin^2 \theta + 35 \cos^3 \theta \sin^4 \theta - 7 \cos \theta \sin^6 \theta
      | c = equating real parts in $(1)$
}}
{{eqn | r = \cos^7 \theta - 21 \cos^5 \paren {1 - \cos^2 \theta} + 35 \cos^3 \theta \paren {1 - \cos^2 \theta}^2 - 7 \cos \theta \paren {1 - \cos^2 \theta}^3
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = 64 \cos^7 \theta - 112 \cos^5 \theta + 56 \cos^3 \theta - 7 \cos \theta
      | c = multiplying out and gathering terms
}}
{{end-eqn}}
{{qed}}
Category:Cosine Function
Category:Septuple Angle Formulas
Category:Septuple Angle Formula for Cosine
e8u07h4uxsxq7hck63elit5fa7y3ss8
Theorem: Power Reduction Formulas/Cosine to 7th

:$\cos^7 x = \dfrac {35 \cos x + 21 \cos 3 x + 7 \cos 5 x + \cos 7 x} {64}$

Proof:
{{begin-eqn}}
{{eqn | l = \cos 7 x
      | r = 64 \cos^7 x - 112 \cos^5 x + 56 \cos^3 x - 7 \cos x
      | c = Septuple Angle Formula for Cosine
}}
{{eqn | ll= \leadsto
      | l = 64 \cos^7 x
      | r = \cos 7 x + 112 \cos^5 x - 56 \cos^3 x + 7 \cos x
      | c = rearranging
}}
{{eqn | r = \cos 7 x + 112 \paren {\dfrac {10 \cos x + 5 \cos 3 x + \cos 5 x} {16} } - 56 \paren {\frac {3 \cos x + \cos 3 x} 4} + 7 \cos x
      | c = Fifth Power of Cosine, Cube of Cosine
}}
{{eqn | r = \cos 7 x + 70 \cos x + 35 \cos 3 x + 7 \cos 5 x - 42 \cos x - 14 \cos 3 x + 7 \cos x
      | c = multipying out
}}
{{eqn | r = 35 \cos x + 21 \cos 3 x + 7 \cos 5 x + \cos 7 x
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \cos^7 x
      | r = \frac {35 \cos x + 21 \cos 3 x + 7 \cos 5 x + \cos 7 x} {64}
      | c = dividing both sides by $64$
}}
{{end-eqn}}
{{qed}}
Category:Cosine Function
5qgyhy5n6op7zx226nazyysni4gtobg
Theorem: Extension of Continuous Mapping is Continuous

Let $T_1 = \struct {S_1, \tau_1}$ and $T_2 = \struct {S_2, \tau_2}$ be topological spaces.
Let $T_H = \struct{H, \tau_H}$ be a topological subspace of $T_2$ where $H \subseteq S_2$.
Let $f: S_1 \to H$ be a $\tuple { \tau_1 , \tau_H}$-continuous mapping.
Define a mapping $g: S_1 \to S_2$ by:
:$\forall x \in S_1 : \map g x = \map f x$
Then $g$ is $\tuple { \tau_1 , \tau_2}$-continuous.

Proof:
Let $i_H$ be the inclusion mapping of $H$ in $S_2$.
Then:
:$g = i_H \circ f$
From Continuity of Composite with Inclusion: Inclusion on Mapping, it follows that $f$ is $\tuple { \tau_1 , \tau_H}$-continuous mapping {{iff}} $i_H \circ f = g$ is $\tuple { \tau_1 , \tau_2}$-continuous.
Since $f$ is continuous by assumption, $g$ is continuous.
{{qed}}
Theorem: Open Continuous Injection is Embedding

Let $T_1 = \struct{S_1, \tau_1}$ and $T_2 = \struct{S_2, \tau_2}$ be topological spaces.
Let $f: S_1 \to S_2$ be an open and continuous injection.
Then $f$ is an embedding of $T_1$ into $T_2$.

Proof:
Let $g: S_1 \to f \sqbrk {S_1}$ be the restriction of $f$ to $S_1 \times f \sqbrk {S_1}$.
It must be shown that $g$ is a homeomorphism.
Theorem: Closed Continuous Injection is Embedding

Let $T_1 = \struct{S_1, \tau_1}$ and $T_2 = \struct{S_2, \tau_2}$ be topological spaces.
Let $f: S_1 \to S_2$ be a closed and continuous injection.
Then $f$ is an embedding of $T_1$ into $T_2$.

Proof:
Let $g: S_1 \to f \sqbrk {S_1}$ be the restriction of $f$ to $S_1 \times f \sqbrk {S_1}$.
It must be shown that $g$ is a homeomorphism.
Theorem: Surjective Embedding is Homeomorphism

Let $T_1 = \struct{S_1, \tau_1}$ and $T_2 = \struct{S_2, \tau_2}$ be topological spaces.
Let $f: S_1 \to S_2$ be a surjective embedding.
Then $f$ is a homeomorphism.

Proof:
Let $f {\restriction_{S_1 \times f\sqbrk {S_1} }}$ be the restriction of $f$ to its image.
By definition of surjection, $f \sqbrk {S_1} = S_2$.
Therefore, $f {\restriction_{S_1 \times f\sqbrk {S_1} }} = f$
By definition of embedding, $f {\restriction_{S_1 \times f\sqbrk {S_1} }}$ of $f$ to its image is a homeomorphism.
Therefore, $f$ is a homeomorphism.
{{qed}}
Theorem: Locally Euclidean Subspace of Euclidean Space is Manifold

Let $\R^n$ be an Euclidean space for $n \in \N$.
Let $M = \struct{H, \tau_H}$ be a subspace of $\R^n$, where $H \subseteq \R^n$.
Let $M$ be locally Euclidean of dimension $d$.
Then $M$ is a $d$-manifold.

Proof:
From Metric Space is Hausdorff, $\R^n$ is a Hausdorff space.
From Subspace of Hausdorff Space is Hausdorff, $M$ is a Hausdorff space.
From Euclidean Space is Second-Countable, $\R^n$ is second-countable.
From Second-Countability is Hereditary, $M$ is second-countable.
Therefore, $M$ is a $d$-manifold.
{{qed}}
Theorem: Graph of Continuous Real Function is Manifold

Let $U \subseteq \R^n$ be an open subset of $n$-dimensional Euclidean space.
Let $f : U \to \R^k$ be a  continuous mapping.
Let $\map \Gamma f$ be the graph of $f$ equipped with the subspace topology.
Then $\map \Gamma f$ is a $n$-manifold.

Proof:
Let $\gamma_f : U \to \R^{n + k}$ be the graph parametrization of $\map \Gamma f$.
From Graph Parametrization of Continuous Mapping is Embedding, $\gamma_f$ is an embedding.
The image of $\gamma_f$ is $\map \Gamma f$.
Therefore, $U$ and $\map \Gamma f$ are homeomorphic.
In other words, for each point in $\map \Gamma f$, $\map \Gamma f$ is a open neighborhood that is homeomorphic to an open subset of $\R^n$.
So $\map \Gamma f$ is locally Euclidean of dimension $n$ by definition.
From Locally Euclidean Subspace of Euclidean Space is Manifold, $\map \Gamma f$ is a $n$-manifold.
{{qed}}
Theorem: Particular Values of Legendre Polynomials/1

:$\map {P_n} 1 = 1$

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\map {P_n} 1 = 1$
Theorem: Particular Values of Legendre Polynomials/-1

:$\map {P_n} {-1} = \paren {-1}^n$

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\map {P_n} {-1} = \paren {-1}^n$
Theorem: Particular Values of Legendre Polynomials/-x

:$\map {P_n} x = \paren {-1}^n \map {P_n} {-x}$

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\map {P_n} x = \paren {-1}^n \map {P_n} {-x}$
First we note that:
{{begin-eqn}}
{{eqn | l = \map {P_n} x
      | r = \paren {-1}^n \map {P_n} {-x}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \dfrac 1 {\paren {-1}^n} \map {P_n} x
      | r = \map {P_n} {-x}
      | c = dividing both sides by $\paren {-1}^n$
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {-1}^n \map {P_n} x
      | r = \map {P_n} {-x}
      | c = as $\paren {-1}^n = \dfrac 1 {\paren {-1}^n}$
}}
{{end-eqn}}
That is:
:$(1): \quad \map {P_n} x = \paren {-1}^n \map {P_n} {-x} \iff \map {P_n} {-x} = \paren {-1}^n \map {P_n} x$
Theorem: Legendre Polynomial of Even Index is Even Function

Let $n \in \N$ be an even natural number: $n \in \set {0, 2, 4, \ldots}$
Let $\map {P_n} x$ denote the Legendre polynomial of order $n$.
Then $\map {P_n} x$ is an even function.

Proof:
From Legendre Polynomial of $-x$:
:$\map {P_n} x = \paren {-1}^n \map {P_n} {-x}$
When $n$ is even we have:
:$\paren {-1}^n = 1$
and so:
:$\map {P_n} x = \map {P_n} {-x}$
Hence the result by definition of even function.
{{qed}}
Theorem: Legendre Polynomial of Odd Index is Odd Function

Let $n \in \N$ be an odd natural number: $n \in \set {1, 3, 5, \ldots}$
Let $\map {P_n} x$ denote the Legendre polynomial of order $n$.
Then $\map {P_n} x$ is an odd function.

Proof:
From Legendre Polynomial of $-x$:
:$\map {P_n} x = \paren {-1}^n \map {P_n} {-x}$
When $n$ is odd we have:
:$\paren {-1}^n = -1$
and so:
:$\map {P_n} x = -\map {P_n} {-x}$
Hence the result by definition of odd function.
{{qed}}
Theorem: Generating Function for Associated Legendre Function of the First Kind

Let $\map { {P_n}^m} x$ denote an '''associated Legendre function of the first kind'''.
Then the generating function for ${P_n}^m$ is:
:$\ds \frac {\paren {2 m}! \paren {1 - x^2}^{m / 2} t^m} {2^m m! \paren {1 - 2 t x + t^2}^{m + 1/2} } = \sum_{n \mathop = m}^\infty \map { {P_n}^m} x t^n$

Proof:
{{ProofWanted|Proof at https://www.phys.ksu.edu/personal/wysin/notes/legendre.pdf}}
Theorem: Stirling's Formula/Refinement

A refinement of Stirling's Formula is:
:$n! = \sqrt {2 \pi n} \paren {\dfrac n e}^n \paren {1 + \dfrac 1 {12 n} + \map \OO  {\dfrac 1 {n^2} } }$

Proof:
Let:
:$\ds \map f n := \dfrac {n!} {\sqrt {2 \pi n} n^n e^{-n} } - \paren {1 + \frac 1 {12 n} }$
We need to show:
:$\ds \map f n = \map \OO {\dfrac 1 {n^2} }$
Recall Limit of Error in Stirling's Formula:
:$e^{1 / \paren {12 n + 1} } \le \dfrac {n!} {\sqrt {2 \pi n} n^n e^{-n} } \le e^{1 / 12 n}$
Furthermore, observe:
{{begin-eqn}}
{{eqn | l = e^{1 / {12 n + 1} }
      | o = \ge
      | r = 1 + \frac 1 {12 n + 1}
      | c = Exponential Function Inequality
}}
{{eqn | r = 1 + \frac 1 {12 n} - \frac 1 {12 n \paren {12 n + 1} }
}}
{{eqn | o = \ge
      | r = \paren {1 + \frac 1 {12 n} } - \frac 1 {n^2}
}}
{{end-eqn}}
On the other hand:
{{begin-eqn}}
{{eqn | l = e^{1 / {12 n} }
      | r = 1 + \frac 1 {12 n} + \frac {e^\xi}{2!} \paren {\frac 1 {12 n} }^2
      | c = for a $\xi \in \closedint 0 {\frac 1 {12n} }$ by Taylor's Theorem
}}
{{eqn | o = \le
      | r = 1 + \frac 1 {12 n} + \frac {e^1} {2!} \paren {\frac 1 {12 n} }^2
      | c = Exponential is Strictly Increasing
}}
{{eqn | o = \le
      | r = \paren {1 + \frac 1 {12 n} } + \frac 1 {n^2}
      | c = $e=2.71\ldots$
}}
{{end-eqn}}
Altogether we have:
:$-\dfrac 1 {n^2} \le e^{1 / \paren {12 n + 1} } - \paren {1 + \dfrac 1 {12 n} } \le \map f n \le e^{1 / \paren {12 n} } - \paren {1 + \dfrac 1 {12 n} } \le \dfrac 1 {n^2}$
Therefore:
:$ \size {\map f n} \le \dfrac 1 {n^2}$
{{qed}}
Theorem: Rodrigues' Formula for Hermite Polynomials

:$\map {H_n} x = \paren {-1}^n \map \exp {x^2} \map {\dfrac {\d^n} {\d x^n} } {\map \exp {-x^2} }$
where:
:$n \in \N$ is a natural number
:$H_n$ is the $n$th Hermite polynomial.

Proof:
{{ProofWanted}}
{{Namedfor|Olinde Rodrigues|cat = Rodrigues}}
Theorem: Generating Function for Hermite Polynomials

Let $\map {H_n} x$ denote the $n$th Hermite polynomial.
Then the generating function for $H_n$ is:
:$\ds e^{2 t x - t^2} = \sum_{n \mathop = 0}^\infty \dfrac {\map {H_n} x t^n} {n!}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {H_n} x
      | r = \paren {-1}^n \map \exp {x^2} \map {\dfrac {\d^n} {\d x^n} } {\map \exp {-x^2} }
      | c = Rodrigues' Formula for Hermite Polynomials
}}
{{eqn | r = \paren {-1}^n \dfrac {n!} {2 i n} \oint_C \dfrac {\map \exp {x^2 - \xi^2} } { {\xi - x}^{n + 1} } \rd \xi
      | c = Cauchy Integral Formula: $C$ is an arbitrary contour around $x$ going anticlockwise
}}
{{eqn | r = \paren {-1}^n \dfrac {n!} {2 i n} \oint_C \dfrac {\map \exp {x^2 - \paren {x - t}^2} } {t^{n + 1} } \rd t
      | c = substituting $t$ for $x - \xi$
}}
{{eqn | r = \intlimits {\dfrac {\d^n} {\d t^n} \map \exp {x^2 - \paren {x - t}^2} } {t \mathop = 0} {}
      | c = 
}}
{{end-eqn}}
and the result follows.
{{qed}}
Theorem: Recurrence Formula for Hermite Polynomials

Let $\map {H_n} x$ denote the Hermite polynomial of order $n$.
Then:
:$\map {H_{n + 1} } x = 2 x \map {H_n} x - 2 n \map {H_{n - 1} } x$

Proof:
From Generating Function for Hermite Polynomials, the generating function for $H_n$ is:
:$(1): \quad \ds e^{2 t x - t^2} = \sum_{n \mathop = 0}^\infty \dfrac {\map {H_n} x t^n} {n!}$
Differentiating both sides of $(1)$ {{WRT|Differentiation}} $t$:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d t} } {e^{2 t x - t^2} }
      | r = \map {\dfrac \d {\d t} } {\sum_{n \mathop = 0}^\infty \dfrac {\map {H_n} x t^n} {n!} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {2 x - 2 t} e^{2 t x - t^2}
      | r = \sum_{n \mathop = 0}^\infty \map {\dfrac \d {\d t} } {\dfrac {\map {H_n} x t^n} {n!} }
      | c = Derivative of Exponential Function, Derivative of Power, Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \paren {2 x - 2 t} e^{2 t x - t^2}
      | r = \sum_{n \mathop = 1}^\infty {\dfrac {n \map {H_n} x t^{n - 1} } {n!} }
      | c = Derivative of Power
}}
{{eqn | ll= \leadsto
      | l = \paren {2 x - 2 t} \sum_{n \mathop = 0}^\infty \dfrac {\map {H_n} x t^n} {n!}
      | r = \sum_{n \mathop = 1}^\infty {\dfrac {n \map {H_n} x t^{n - 1} } {n!} }
      | c = substituting $\ds \sum_{n \mathop = 0}^\infty \dfrac {\map {H_n} x t^n} {n!}$ for $e^{2 t x - t^2}$ from $(1)$
}}
{{eqn | ll= \leadsto
      | l = \paren {2 x - 2 t} \sum_{n \mathop = 0}^\infty \dfrac {\map {H_n} x t^n} {n!}
      | r = \sum_{n \mathop = 0}^\infty {\dfrac {\paren {n + 1} \map {H_{n + 1} } x t^n} {\paren {n + 1}!} }
      | c = Translation of Index Variable of Summation in {{RHS}}
}}
{{end-eqn}}
Equating coefficients of $t^n$:
{{begin-eqn}}
{{eqn | l = 2 x \dfrac {\map {H_n} x} {n!} - 2 \dfrac {\map {H_{n - 1} } x} {\paren {n - 1}!}
      | r = \paren {n + 1} \dfrac {\map {H_{n + 1} } x} {\paren {n + 1}!}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {H_{n + 1} } x
      | r = 2 x \map {H_n} x - 2 n \map {H_{n - 1} } x
      | c = simplifying
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Recurrence Formula for Hermite Polynomials using Derivative

Let $\map {H_n} x$ denote the Hermite polynomial of order $n$.
Then:
:$\dfrac \d {\d x} \map {H_n} x = 2 n \map {H_{n - 1} } x$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac \d {\d x} \map {H_n} x
      | r = \map {\dfrac \d {\d x} } {\paren {-1}^n \map \exp {x^2} \map {\dfrac {\d^n} {\d x^n} } {\map \exp {-x^2} } }
      | c = Rodrigues' Formula for Hermite Polynomials
}}
{{eqn | r = \paren {-1}^n \paren {2 x \map \exp {x^2} \map {\dfrac {\d^n} {\d x^n} } {\map \exp {-x^2} } + \map \exp {x^2} \map {\dfrac {\d^{n + 1} } {\d x^{n + 1} } } {\map \exp {-x^2} } }
      | c = Derivative of Exponential Function, Derivative of Power, Chain Rule for Derivatives, Product Rule for Derivatives
}}
{{eqn | r = 2 x \paren {\paren {-1}^n \map \exp {x^2} \map {\dfrac {\d^n} {\d x^n} } {\map \exp {-x^2} } } - \paren {-1}^{n + 1} \map \exp {x^2} \map {\dfrac {\d^{n + 1} } {\d x^{n + 1} } } {\map \exp {-x^2} }
      | c = rearranging
}}
{{eqn | r = 2 x \map {H_n} x - \map {H_{n + 1} } x
      | c = Rodrigues' Formula for Hermite Polynomials
}}
{{eqn | r = 2 x \map {H_n} x - \paren {2 x \map {H_n} x - 2 n \map {H_{n - 1} } x}
      | c = Recurrence Formula for Hermite Polynomials
}}
{{eqn | r = 2 n \map {H_{n - 1} } x
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Closed Form for Hermite Polynomials

{{begin-eqn}}
{{eqn | l = \map {H_n} x
      | r = \paren {2 x}^n - \dfrac {n \paren {n - 1} } {1!} \paren {2 x}^{n - 2} + \dfrac {n \paren {n - 1} \paren {n - 2} \paren {n - 3} } {2!} \paren {2 x}^{n - 4} \cdots
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^{\floor {n / 2} } \paren {-1}^k \dfrac {n^\underline {2 k} } {k!} \paren {2 x}^{n - 2 k}
      | c = where $n^\underline {2 k}$ denotes the falling factorial operator
}}
{{end-eqn}}

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\map {H_n} x = \ds \sum_{k \mathop = 0}^{\floor {n / 2} } \paren {-1}^k \dfrac {n^\underline {2 k} } {k!} \paren {2 x}^{n - 2 k}$
Theorem: Rodrigues' Formula for Laguerre Polynomials

:$\map {L_n} x = e^x \map {\dfrac {\d^n} {\d x^n} } {x^n e^{-x} }$
where:
:$n \in \N$ is a natural number
:$L_n$ is the $n$th Laguerre polynomial.

Proof:
{{ProofWanted}}
{{Namedfor|Olinde Rodrigues|cat = Rodrigues}}
Theorem: Power Series Expansion for Chebyshev Polynomial of the First Kind

The $n$th '''Chebyshev polynomial of the first kind''' can be expressed as a power series expansion in the form:
{{begin-eqn}}
{{eqn | l = \map {T_n} x
      | r = \sum_{k \mathop = 0}^\infty \paren {-1}^k \dbinom n {2 k} x^{n - 2 k} \paren {1 - x^2}^k
}}
{{eqn | r = x^n - \dbinom n 2 x^{n - 2} \paren {1 - x^2} + \dbinom n 4 x^{n - 4} \paren {1 - x^2}^2 - \dbinom n 6 x^{n - 6} \paren {1 - x^2}^3 + \cdots
}}
{{end-eqn}}
where $n \in \N$.

Proof:
From the Definition of Chebyshev Polynomial of the First Kind, we have:
:$\map {T_n} {\cos \theta} = \map \cos {n \theta}$
From De Moivre's Formula, we have:
:$\cos n \theta + i \sin n \theta = \paren {\cos \theta + i \sin \theta}^n$
As $n \in \Z_{>0}$, we use the Binomial Theorem on the {{RHS}}, resulting in:
:$\ds \cos n \theta + i \sin n \theta = \sum_{k \mathop \ge 0} \binom n k \paren {\cos^{n - k} \theta} \paren {i \sin \theta}^k$
When $k$ is even, the expression being summed is real.
Equating the real parts of both sides of the equation, replacing $k$ with $2 k$ to make $k$ even, gives:
{{begin-eqn}}
{{eqn | l = \cos n \theta
      | r = \sum_{k \mathop \ge 0} \paren {-1}^k \dbinom n {2 k } \paren {\cos^{n - \paren {2 k } } \theta} \paren {\sin^{2 k } \theta}
      | c = 
}}
{{eqn | r = \sum_{k \mathop \ge 0} \paren {-1}^k \dbinom n {2 k } \paren {\cos^{n - \paren {2 k } } \theta} \paren {\sin^2 \theta}^k
      | c = 
}}
{{eqn | r = \sum_{k \mathop \ge 0} \paren {-1}^k \dbinom n {2 k } \paren {\cos^{n - \paren {2 k } } \theta} \paren {1 - \cos^2 \theta}^k
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \sum_{k \mathop = 0}^\infty \paren {-1}^k \dbinom n {2 k} x^{n - 2 k} \paren {1 - x^2}^k
      | c = $\cos \theta \to x$
}}
{{eqn | ll = \leadsto
      | l = \map {T_n} x
      | r = \sum_{k \mathop = 0}^\infty \paren {-1}^k \dbinom n {2 k} x^{n - 2 k} \paren {1 - x^2}^k
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Particular Values of Chebyshev Polynomials of the First Kind/-x

:$\map {T_n} {-x} = \paren {-1}^n \map {T_n} x$

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\map {T_n} {-x} = \paren {-1}^n \map {T_n} x$
First we note that:
{{begin-eqn}}
{{eqn | l = \map {T_n} {-x}
      | r = \paren {-1}^n \map {T_n} x
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \dfrac 1 {\paren {-1}^n} \map {T_n} {-x}
      | r = \map {T_n} x
      | c = dividing both sides by $\paren {-1}^n$
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {-1}^n \map {T_n} {-x}
      | r = \map {T_n} x
      | c = as $\paren {-1}^n = \dfrac 1 {\paren {-1}^n}$
}}
{{end-eqn}}
That is:
:$(1): \quad \map {T_n} {-x} = \paren {-1}^n \map {T_n} x \iff \map {T_n} x = \paren {-1}^n \map {T_n} {-x}$
Theorem: Particular Values of Chebyshev Polynomials of the First Kind/1

:$\map {T_n} 1 = 1$

Proof:
The proof proceeds by strong induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\map {T_n} 1 = 1$
Theorem: Particular Values of Chebyshev Polynomials of the First Kind/-1

:$\map {T_n} {-1} = \paren {-1}^n$

Proof:
{{begin-eqn}}
{{eqn | l = \map {T_n} {-x}
      | r = \paren {-1}^n \map {T_n} x
      | c = Particular Values of Chebyshev Polynomials of the First Kind: $-x$
}}
{{eqn | ll= \leadsto
      | l = \map {T_n} {-1}
      | r = \paren {-1}^n \map {T_n} 1
      | c = setting $x = 1$
}}
{{eqn | r = \paren {-1}^n
      | c = Particular Values of Chebyshev Polynomials of the First Kind: $1$
}}
{{end-eqn}}
{{qed}}
Theorem: Particular Values of Chebyshev Polynomials of the First Kind/0

:$\map {T_n} 0 = \begin {cases} \paren {-1}^{n / 2} & : \text {$n$ even} \\ 0 & : \text {$n$ odd} \end {cases}$

Proof:
=== Even Order ===
{{:Particular Values of Chebyshev Polynomials of the First Kind/0/Even Order}}