avewright/proofwiki-math huggingface dataset:
Theorem: Orientation of Simple Closed Contour is with Respect to Interior

Let $C$ be a simple closed contour in the complex plane $\C$.
Let $\Int C$ denote the interior of $C$.
$C$ is positively oriented, {{iff}} $C$ is positively oriented with respect to $\Int C$.
$C$ is negatively oriented, {{iff}} $C$ is negatively oriented with respect to $\Int C$.

Proof:
=== Sufficient condition ===
Suppose $C$ is positively oriented.
Let $\gamma : \closedint a b$ be a parameterization of $C$.
Set $K := \set { t \in \closedint a b : \textrm{ $\gamma$ is not differentiable at $t$ } }$.
By definition of positive orientation, it follows that for all $t \in \openint a b \setminus K$, there exists $r_0 \in \R_{>0}$ such that:
:for all $\epsilon \in \openint 0 {r_0}$ : $\map \gamma t + \epsilon i \map {\gamma'} t \in \Int C$
Complex Plane is Homeomorphic to Real Plane shows that we can identify the complex plane $\C$ with the real plane $\R^2$ by the homeomorphism $\map \phi {x, y} = x + i y$.
Interior of Simple Closed Contour is Well-Defined shows that the image $\Img C$ can be identified with the image of a Jordan curve $g: \R^2 \to \R^2$.
From the same theorem, it follows that $\Int C$ can be identified with the interior of $g$.
From the Jordan Curve Theorem, it follows that $\Int C$ is an open connected set with $\Img C$ as its boundary.
It follows that $\Int C$ is a connected domain with $\Img C \subseteq \partial \Int C$, which is the first requirement for $C$ to be positively oriented with respect to $\Int C$.
The next requirement is that for all $t \in \openint a b \setminus K$, we need to find $r \in \R_{>0}$ such that:
:for all $\epsilon \in \openint 0 r$ : $\map \gamma t + \epsilon i \map {\gamma'} t \in \Int C$, and $\map \gamma t - \epsilon i \map {\gamma'} t \notin \Int C$
From All Normal Vectors of Simple Closed Contour Cannot Point into Interior, it follows that there exists $r_1 \in \R_{>0}$ such that $\map \gamma t - \epsilon i \map {\gamma'} t \notin \Int C$ for all $\epsilon \in \openint 0 {r_1}$.
Then $r := \map \min {r_0 , r_1}$ fulfils the criteria.
When $C$ is negatively oriented, the proof is similar.
{{qed|lemma}}
Theorem: Supremum Operator Norm of Cesàro Summation Operator

Let $A : \ell^\infty \to \ell^\infty$ be the Cesàro summation operator.
Let $\norm {\, \cdot \,}$ be the supremum operator norm.
Then $\norm A = 1$.

Proof:
By Cesàro Summation Operator is Continuous Linear Transformation:
:$\norm {A \mathbf x}_\infty \le \norm {\mathbf x}_\infty$
where $\norm {\, \cdot \,}_\infty$ denotes the supremum norm.
By Universal Upper Bound greater than Supremum Operator Norm:
:$\norm A \le 1$
Let $\mathbf 1 := \tuple {1, 1, \ldots} \in \ell^\infty$
Then:
{{begin-eqn}}
{{eqn | l = \norm A
      | r = \norm A \cdot 1
}}
{{eqn | r = \norm A \norm {\mathbf 1}_\infty
      | c = {{Defof|Supremum Norm}}
}}
{{eqn | o = \ge
      | r = \norm {A \mathbf 1}_\infty
      | c = Supremum Operator Norm as Universal Upper Bound
}}
{{eqn | r = \norm {\tuple {1, 1, \ldots} }_\infty
}}
{{eqn | r = 1
}}
{{end-eqn}}
Altogether, $\norm A = 1$.
{{qed}}
Theorem: Integral of Positive Measurable Function with respect to Restricted Measure

Let $\struct {X, \Sigma, \mu}$ be a measure space. 
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra of $\Sigma$.
Let $\mu \restriction_\GG$ be the restriction of $\mu$ to $\GG$.
Let $f : X \to \overline \R$ be a positive $\GG$-measurable function.
Then: 
:$\ds \int f \rd \mu = \int f \rd \mu \restriction_\GG$

Proof:
We first prove the result for positive simple functions.
Let $f : X \to \R$ be a positive simple function that is $\GG$-measurable.
From  Simple Function has Standard Representation there exists:
:a finite sequence $a_1, \ldots, a_n$ of real numbers
:a partition $E_1, \ldots, E_n$ of $\GG$-measurable sets
such that: 
:$f = \ds \sum_{j \mathop = 1}^n a_j \chi_{E_j}$
Then we have: 
{{begin-eqn}}
{{eqn	| l = \int f \rd \mu \restriction_G
		| r = \sum_{j \mathop = 1}^n a_j \map {\paren {\mu \restriction_G} } {E_j}
		| c = Integral of Positive Measurable Function Extends Integral of Positive Simple Function, {{Defof|Integral of Positive Simple Function}}
}}
{{eqn	| r = \sum_{j \mathop = 1}^n a_j \map \mu {E_j}
		| c = {{Defof|Restricted Measure}}
}}
{{eqn	| r = \int f \rd \mu
		| c = Integral of Positive Measurable Function Extends Integral of Positive Simple Function, {{Defof|Integral of Positive Simple Function}}
}}
{{end-eqn}}
So we get the theorem for positive simple functions.
Now let $f$ be a general positive $\GG$-measurable function.
From Measurable Function is Pointwise Limit of Simple Functions, there exists an increasing sequence $\sequence {f_n}_{n \mathop \in \N}$ of positive simple functions such that: 
:$\ds \map f x = \lim_{n \mathop \to \infty} \map {f_n} x$
for each $x \in X$.
Then for each $n \in \N$ we have: 
:$\ds \int f_n \rd \mu = \int f_n \rd \mu \restriction_\GG$
From Integral of Positive Measurable Function as Limit of Integrals of Positive Simple Functions, taking $n \to \infty$ we obtain: 
:$\ds \int f \rd \mu = \int f \rd \mu \restriction_\GG$
{{qed}}
Category:Restricted Measures
Category:Integral of Positive Measurable Function
qnnpgvdvqw40hu9qrgdz860c6s30ta6
Theorem: Inner Product with Vector is Linear Functional

Let $\GF$ be a subfield of $\C$.
Let $\struct{ V, \innerprod \cdot \cdot }$ be an inner product space over $\GF$.
Let $v_0 \in V$.
Then the mapping $L: V \to \GF$ defined by:
:$\map L v := \innerprod v {v_0}$
is a linear functional.

Proof:
Let us directly check the definition of linear functional:
{{begin-eqn}}
{{eqn|l = \map L {\alpha v + \beta w}
     |r = \innerprod { \alpha v + \beta w } {v_0}
}}
{{eqn|r = \innerprod {\alpha v} {v_0} + \innerprod {\beta w} {v_0}
}}
{{eqn|r = \alpha \innerprod v {v_0} + \beta \innerprod w {w_0}
}}
{{eqn|r = \alpha \map L v + \beta \map L w
}}
{{end-eqn}}
{{qed}}
Theorem: Inner Product with Vector is Bounded Linear Functional

Let $\GF$ be a subfield of $\C$.
Let $\struct {V, \innerprod \cdot \cdot}$ be an inner product space over $\GF$.
Let $v_0 \in V$.
Then the mapping $L: V \to \GF$ defined by:
:$\map L v := \innerprod v {v_0}$
is a bounded linear functional with norm equal to $\norm {v_0}$.

Proof:
By Inner Product with Vector is Linear Functional, $L$ is a linear functional.
To check that $L$ is bounded:
{{begin-eqn}}
{{eqn | l = \cmod {\map L v}
      | r = \cmod {\innerprod v {v_0} }
}}
{{eqn | o = \le
      | r = \norm v \norm {v_0}
      | c = Cauchy-Bunyakovsky-Schwarz Inequality for Inner Product Spaces
}}
{{end-eqn}}
Thus $L$ is bounded by $\norm {v_0}$.
Furthermore, note:
:$\map L {v_0} = \innerprod {v_0} {v_0} = \norm {v_0}^2$
so that indeed $\norm {v_0}$ is the norm of $L$.
{{qed}}
Theorem: Kernel of Bounded Linear Transformation is Closed Linear Subspace

Let $V, W$ be normed vector spaces.
Let $f: V \to W$ be a bounded linear transformation.
Then $\ker f$, the kernel of $f$, is a closed linear subspace of $V$.

Proof:
By Kernel of Linear Transformation is Linear Subspace, $\ker f$ is a subspace of $V$.
By Continuity of Linear Transformations, $f$ is continuous.
Since $\ker f = f^{-1} \sqbrk{ \set{ \mathbf 0_W } }$, it follows from Continuity Defined from Closed Sets that $\ker f$ is closed.
Hence the result by definition of closed linear subspace.
{{qed}}
Category:Bounded Linear Transformations
2e02q17b7nhby588bo3qued65euglon
Theorem: Sufficient Condition for Weak Convergence of Bounded Sequence in Hilbert Space in terms of Everywhere Dense Set

Let $\struct {\HH, \innerprod \cdot \cdot_\HH}$ be a Hilbert space.
Let $\sequence {x_n}_{n \mathop \in \N}$ be a bounded sequence in $\HH$.
Let $D$ be an everywhere dense set in $\HH$ such that: 
:$\innerprod {x_n} v \to \innerprod x v$
for all $v \in D$, for some $x \in \HH$.
Then: 
:$x_n \weakconv x$
where $\weakconv$ denotes weak convergence.

Proof:
We show the theorem in the case $x = 0$ first for neatness.
From Weak Convergence in Hilbert Space, we want to show that: 
:$\innerprod {x_n} z \to \innerprod x z$ 
for all $z \in \HH$.
Let $\epsilon > 0$. 
Since $D$ is everywhere dense in $\HH$, for each $n \in \N$ we can pick $z_n \in D$ such that: 
:$\norm {z - z_n}_\HH < \dfrac 1 n$
We now have, for each $n \in \N$ and $m \in \N$:
:$\cmod {\innerprod {x_n} z} = \cmod {\innerprod {x_n} {z - z_m} - \innerprod {x_n} {z_m} }$
due to the conjugate linearity of the inner product in its second argument.
Pick $M > 0$ such that: 
:$\norm {x_n}_\HH \le M$ 
for each $n \in \N$. 
We can then bound:
{{begin-eqn}}
{{eqn	| l = \cmod {\innerprod {x_n} {z - z_m}_\HH - \innerprod {x_n} {z_m}_\HH}
		| o = \le
		| r = \cmod {\innerprod {x_n} {z - z_m}_\HH } + \cmod {\innerprod {x_n} {z_m}_\HH}
		| c = Triangle Inequality for Complex Numbers
}}
{{eqn	| o = \le
		| r = \norm {x_n}_\HH \norm {z - z_m}_\HH + \cmod {\innerprod {x_n} {z_m}_\HH}
		| c = Cauchy-Bunyakovsky-Schwarz Inequality for Inner Product Spaces
}}
{{eqn	| o = \le
		| r = \frac M m + \cmod {\innerprod {x_n} {z_m}_\HH}
		| c = since $\norm {x_n}_\HH \le M$ and $\norm {z - z_m}_\HH < 1/m$
}}
{{end-eqn}}
Fix $m \in \N$ such that: 
:$m > \dfrac {2 M} \epsilon$
Since we have: 
:$\innerprod {x_n} {z_m}_\HH \to 0$ 
for this fixed $m$, we can pick $N$ such that: 
:$\cmod {\innerprod {x_n} {z_m}_\HH} < \dfrac \epsilon 2$
for $n \ge N$.
Then for $n \ge N$ we have: 
:$\cmod {\innerprod {x_n} z_\HH} < \epsilon$
So:
:$\innerprod {x_n} z_\HH \to 0 = \innerprod 0 z$
giving:
:$x_n \weakconv 0 = x$ 
Now we show the theorem for general $x$. 
Suppose that:
:$\innerprod {x_n} v \to \innerprod x v$
for all $v \in D$.
Then, using the linearity of the inner product in the first argument, we have: 
:$\innerprod {x_n - x} v \to 0$ 
Then by our previous calculations: 
:$x_n - x \weakconv 0$
so:
:$x_n \weakconv x$
from Linear Combination of Weakly Convergent Sequences is Weakly Convergent.
{{qed}}
Category:Hilbert Spaces
Category:Weak Convergence (Normed Vector Spaces)
hvaib9daothj7xxpk9hmgfq3qku7a9j
Theorem: Expectation of Conditional Expectation

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra.
Let $X$ be a integrable random variable.
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ given $\GG$.
Then: 
:$\expect {\expect {X \mid \GG} } = \expect X$

Proof:
We have: 
{{begin-eqn}}
{{eqn	| l = \expect {\expect {X \mid \GG} }
		| r = \int_\Omega \expect {X \mid \GG} \rd \Pr
		| c = {{Defof|Expectation|subdef = General Definition}}
}}
{{eqn	| r = \int_\Omega X \rd \Pr
		| c = {{Defof|Conditional Expectation on Sigma-Algebra}}
}}
{{eqn	| r = \expect X
		| c = {{Defof|Expectation|subdef = General Definition}}
}}
{{end-eqn}}
{{qed}}
Theorem: Conditional Expectation of Measurable Random Variable

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra.
Let $X$ be a integrable random variable that is $\GG$-measurable.
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ given $\GG$.
Then:
:$\expect {X \mid \GG} = X$ almost everywhere.

Proof:
We show that $X$ is a version of $\expect {X \mid \GG}$.
Then since conditional expectation is essentially unique by Existence and Essential Uniqueness of Conditional Expectation Conditioned on Sigma-Algebra, we will obtain:
:$\expect {X \mid \GG} = X$ almost everywhere.
Note that $X$ is integrable and $\GG$-measurable {{hypothesis}}, with: 
:$\ds \int_A X \rd \Pr = \int_A X \rd \Pr$
So $X$ satisfies the conditions of conditional expectation, and so:
:$\expect {X \mid \GG} = X$ almost everywhere.
{{qed}}
Theorem: Tower Property of Conditional Expectation

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\HH \subseteq \GG$ be sub-$\sigma$-algebras of $\Sigma$.
Let $X$ be a integrable random variable. 
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ given $\GG$.
Let $\expect {X \mid \HH}$ be a version of the conditional expectation of $X$ given $\HH$.
Let $\expect {\expect {X \mid \GG} \mid \HH}$ be a a version of the conditional expectation of $\expect {X \mid \GG}$ given $\HH$.
Then:
:$\expect {\expect {X \mid \GG} \mid \HH} = \expect {X \mid \HH}$ almost everywhere.

Proof:
We show that $\expect {X \mid \HH}$ is a version of $\expect {\expect {X \mid \GG} \mid \HH}$.
Let $A \in \HH$. 
Then:
{{begin-eqn}}
{{eqn	| l = \int_A \expect {X \mid \HH} \rd \Pr
		| r = \int_A X \rd \Pr
		| c = {{Defof|Conditional Expectation on Sigma-Algebra}}
}}
{{eqn	| r = \int_A \expect {X \mid \GG} \rd \Pr
		| c = {{Defof|Conditional Expectation on Sigma-Algebra}}, since $\HH \subseteq \GG$
}}
{{end-eqn}}
Since $\expect {X \mid \HH}$ is $\HH$-measurable, we have that $\expect {X \mid \HH}$ is a version of $\expect {\expect {X \mid \GG} \mid \HH}$.
So by Existence and Essential Uniqueness of Conditional Expectation Conditioned on Sigma-Algebra:
:$\expect {\expect {X \mid \GG} \mid \HH} = \expect {X \mid \HH}$ almost everywhere.
{{qed}}
Theorem: Conditional Expectation is Linear

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra.
Let $X$ and $Y$ be integrable random variables.
Let $\alpha, \beta \in \R$. 
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ given $\GG$.
Let $\expect {Y \mid \GG}$ be a version of the conditional expectation of $Y$ given $\GG$.
Let $\expect {\alpha X + \beta Y \mid \GG}$ be a version of the conditional expectation of $\alpha x + \beta Y$ given $\GG$.
Then:
:$\expect {\alpha X + \beta Y \mid \GG} = \alpha \expect {X \mid \GG} + \beta \expect {Y \mid \GG}$ almost everywhere.

Proof:
We show that $\alpha \expect {X \mid \GG} + \beta \expect {Y \mid \GG}$ is a version of the conditional expectation of $\alpha x + \beta Y$ given $\GG$.
From Linear Combination of Real-Valued Random Variables is Real-Valued Random Variable, we have that $\alpha \expect {X \mid \GG} + \beta \expect {Y \mid \GG}$ is a $\GG$-measurable random variable.
Let $A \in \GG$.
Then:
{{begin-eqn}}
{{eqn	| l = \int_A \paren {\alpha \expect {X \mid \GG} + \beta \expect {Y \mid \GG} } \rd \Pr
		| r = \alpha \int_A \expect {X \mid \GG} \rd \Pr + \beta \int_A \expect {Y \mid \GG} \rd \Pr
		| c = Integral of Integrable Function is Additive, Integral of Integrable Function is Homogeneous
}}
{{eqn	| r = \alpha \int_A X \rd \Pr + \beta \int_A Y \rd \Pr
		| c = {{Defof|Conditional Expectation on Sigma-Algebra}}
}}
{{eqn	| r = \int_A \paren {\alpha X + \beta Y} \rd \Pr
		| c = Integral of Integrable Function is Additive, Integral of Integrable Function is Homogeneous
}}
{{end-eqn}}
So $\alpha \expect {X \mid \GG} + \beta \expect {Y \mid \GG}$ is a version of the conditional expectation of $\alpha x + \beta Y$ given $\GG$, and from Existence and Essential Uniqueness of Conditional Expectation Conditioned on Sigma-Algebra we have:
:$\expect {\alpha X + \beta Y \mid \GG} = \alpha \expect {X \mid \GG} + \beta \expect {Y \mid \GG}$ almost everywhere.
{{qed}}
Theorem: Conditional Monotone Convergence Theorem

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $X$ be an non-negative integrable random variable.
Let $\sequence {X_n}_{n \in \N}$ be an sequence of non-negative integrable random variables converging almost surely to $X$, such that: 
:$X_n \le X_{n + 1}$ almost everywhere for each $n \in \N$.
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra. 
For each $n \in \N$, let $\expect {X_n \mid \GG}$ be a version of the conditional expectation of $X_n$ conditioned on $\GG$.
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ conditioned on $\GG$.
Then:
:$\ds \lim_{n \mathop \to \infty} \expect {X_n \mid \GG} = \expect {X \mid \GG}$ almost everywhere.

Proof:
Note that for almost all $\omega \in \Omega$, $\sequence {\map {X_n} \omega}_{n \mathop \in \N}$ is an increasing real sequence with $\map {X_n} \omega \to \map X \omega$. 
From Monotone Convergence Theorem (Real Analysis), we then have that: 
:$\map {X_n} \omega \le \map X \omega$
for almost all $\omega \in \Omega$.
From Conditional Expectation is Monotone, we then have: 
:$\expect {X_n \mid \GG} \le \expect {X \mid \GG}$
Also: 
:$X_n \le X_{n + 1}$ almost everywhere
by hypothesis, so again applying Conditional Expectation is Monotone we have: 
:$\expect {X_n \mid \GG} \le \expect {X_{n + 1} \mid \GG}$
So for almost all $\omega \in \Omega$, $\sequence {\map {\paren {\expect {X_n \mid \GG} } } \omega}_{n \mathop \in \N}$ is an increasing real sequence bounded above by $\map {\paren {\expect {X \mid \GG} } } \omega$.
So by Monotone Convergence Theorem (Real Analysis):
:$\ds \lim_{n \mathop \to \infty} \map {\paren {\expect {X_n \mid \GG} } } \omega$ exists for almost all $\omega \in \Omega$.
So define: 
:$\ds Y = \lim_{n \mathop \to \infty} \expect {X_n \mid \GG}$
Then from Pointwise Limit of Measurable Functions is Measurable, $Y$ is a real-valued random variable. 
We want to show that $Y$ is a version of the conditional expectation of $X$ conditioned on $\GG$.
We just need to check that: 
:$\ds \int_A Y \rd \Pr = \int_A X \rd \Pr$
for each $A \in \GG$.
We have: 
{{begin-eqn}}
{{eqn	| l = \int_A Y \rd \Pr
		| r = \int_A \paren {\lim_{n \mathop \to \infty} \expect {X_n \mid \GG} } \rd \Pr
}}
{{eqn	| r = \lim_{n \mathop \to \infty} \int_A \expect {X_n \mid \GG} \rd \Pr
		| c = Monotone Convergence Theorem (Measure Theory)
}}
{{eqn	| r = \lim_{n \mathop \to \infty} \int_A X_n \rd \Pr
		| c = {{Defof|Conditional Expectation on Sigma-Algebra}}
}}
{{eqn	| r = \int_A X \rd \Pr
		| c = Monotone Convergence Theorem (Measure Theory)
}}
{{end-eqn}}
and hence $Y$ is a version of the conditional expectation of $X$ conditioned on $\GG$ and hence we have: 
:$\ds Y = \lim_{n \mathop \to \infty} \expect {X_n \mid \GG} = \expect {X \mid \GG}$ almost everywhere.
{{qed}}
Theorem: Tangent of Sum of Three Angles

:$\map \tan {A + B + C} = \dfrac {\tan A + \tan B + \tan C - \tan A \tan B \tan C} {1 - \tan B \tan C - \tan C \tan A - \tan A \tan B}$

Proof:
{{begin-eqn}}
{{eqn | l = \map \tan {A + B + C}
      | r = \dfrac {\tan A + \map \tan {B + C} } {1 - \tan A \tan {B + C} }
      | c = Tangent of Sum
}}
{{eqn | r = \dfrac {\tan A + \frac {\tan B + \tan C} {1 - \tan B \tan C} } {1 - \tan A \frac {\tan B + \tan C} {1 - \tan B \tan C} }
      | c = Tangent of Sum
}}
{{eqn | r = \dfrac {\tan A \paren {1 - \tan B \tan C} + \tan B + \tan C} {\paren {1 - \tan B \tan C} - \tan A \paren {\tan B + \tan C} }
      | c = multiplying top and bottom by $1 - \tan B \tan C$
}}
{{eqn | r = \dfrac {\tan A + \tan B + \tan C - \tan A \tan B \tan C} {1 - \tan B \tan C - \tan C \tan A - \tan A \tan B}
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent of Sum of Three Angles

:$\map \tan {A + B + C} = \dfrac {\tan A + \tan B + \tan C - \tan A \tan B \tan C} {1 - \tan B \tan C - \tan C \tan A - \tan A \tan B}$

Proof:
This is a special case of Tangent of Sum of Series of Angles, for $n = 3$.
{{qed}}
Theorem: Sine of Sum of Three Angles

:$\map \sin {A + B + C} = \sin A \cos B \cos C + \cos A \sin B \cos C + \cos A \cos B \sin C - \sin A \sin B \sin C$

Proof:
{{begin-eqn}}
{{eqn | l = \map \sin {A + B + C}
      | r = \map \sin {A + B} \cos C + \map \cos {A + B} \sin C
      | c = Sine of Sum
}}
{{eqn | r = \paren {\sin A \cos B + \cos A \sin B} \cos C + \paren {\cos A \cos B - \sin A \sin B} \sin C
      | c = Sine of Sum, Cosine of Sum
}}
{{eqn | r = \sin A \cos B \cos C + \cos A \sin B \cos C + \cos A \cos B \sin C - \sin A \sin B \sin C
      | c = multiplying out
}}
{{end-eqn}}
{{qed}}
Category:Sine Function
2nxttg53otx3ccrcyvnt4e0chid7txk
Theorem: Cosine of Sum of Three Angles

:$\map \cos {A + B + C} = \cos A \cos B \cos C - \sin A \sin B \cos C - \sin A \cos B \sin C - \cos A \sin B \sin C$

Proof:
{{begin-eqn}}
{{eqn | l = \map \cos {A + B + C}
      | r = \map \cos {A + B} \cos C - \map \sin {A + B} \sin C
      | c = Cosine of Sum
}}
{{eqn | r = \paren {\cos A \cos B - \sin A \sin B} \cos C - \paren {\sin A \cos B + \cos A \sin B} \sin C
      | c = Cosine of Sum, Sine of Sum
}}
{{eqn | r = \cos A \cos B \cos C - \sin A \sin B \cos C - \sin A \cos B \sin C - \cos A \sin B \sin C
      | c = multiplying out
}}
{{end-eqn}}
{{qed}}
Category:Cosine Function
l15bsjhbkzuiopk9yig9m23un22mm76
Theorem: Tangent of Sum of Series of Angles

Let $\theta_1, \theta_2, \ldots, \theta_n$ be angles.
For all $k \in \set {1, 2, 3, \ldots, n}$, let $s_k$ be defined as the sum of the product of $\map \tan {\theta_1}, \map \tan {\theta_2}, \ldots, \map \tan {\theta_n}$ taken $k$ at a time:
{{begin-eqn}}
{{eqn | l = s_1
      | r = \sum_{i \mathop = 1}^n \map \tan {\theta_i}
      | c = 
}}
{{eqn | l = s_2
      | r = \sum_{i \mathop = 1}^{n - 1} \sum_{j \mathop = i + 1}^n \map \tan {\theta_i} \map \tan {\theta_j}
      | c = 
}}
{{eqn | l = s_3
      | r = \sum_{i \mathop = 1}^{n - 2} \sum_{j \mathop = i + 1}^{n - 1} \sum_{k \mathop = j + 1}^n \map \tan {\theta_i} \map \tan {\theta_j} \map \tan {\theta_k}
      | c = 
}}
{{eqn | o = \vdots
      | c = 
}}
{{eqn | l = s_k
      | r = \sum_{\substack {S \mathop \in \set {1, 2, \ldots, n} \\ \size S \mathop = k} } \paren {\prod_{j \mathop \in S} \tan \theta_j}
      | c = 
}}
{{end-eqn}}
Then:
:$\map \tan {\theta_1 + \theta_2 + \theta_3 + \cdots + \theta_n} = \dfrac {s_1 - s_3 + s_5 - \cdots} {1 - s_2 + s_4 - \cdots}$

Proof:
First we note:
{{begin-eqn}}
{{eqn | l = \cos \sum_j \theta_j + i \sin \sum_j \theta_j
      | r = \prod_j \paren {\cos \theta_j + i \sin \theta_j}
      | c = Product of Complex Numbers in Polar Form
}}
{{eqn | r = \prod_j \cos \theta_j \prod_j \paren {1 + i \tan \theta_j}
      | c = 
}}
{{eqn | r = \prod_j \cos \theta_j \paren {1 + i \tan \theta_1} \times \paren {1 + i \tan \theta_2} \times \cdots \times \paren {1 + i \tan \theta_n}
      | c = expanding the product
}}
{{eqn | r = \prod_j \cos \theta_j \leftparen {1 + i \paren {\tan \theta_1 + \tan \theta_2 + \cdots + \tan \theta_n} }
      | c = multiplying out
}}
{{eqn | o = 
      | ro= +
      | r = i^2 \paren {\tan \theta_1 \tan \theta_2 + \tan \theta_1 \tan \theta_3 + \cdots + \tan \theta_{n - 1} \tan \theta_n}
}}
{{eqn | o = 
      | ro= +
      | r = \cdots
}}
{{eqn | o = 
      | ro= +
      | r = \rightparen {i^n \tan \theta_1 \tan \theta_2 \ldots \tan \theta_n}
}}
{{eqn | r = \prod_j \cos \theta_j \sum_{k \mathop = 0}^n i^k s_k
      | c = $s_0 = 1$
}}
{{eqn | r = \prod_j \cos \theta_j \paren {1 - s_2 + s_4 - s_6 + \cdots} + \prod_j \cos \theta_j \paren {i s_1 - i s_3 + i s_5 - \cdots}
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \cos \sum_j \theta_j
      | r = \prod_j \cos \theta_j \paren {1 - s_2 + s_4 - s_6 + \cdots}
      | c = equating real parts
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \sin \sum_j \theta_j
      | r = \prod_j \cos \theta_j \paren {s_1 - s_3 + s_5 - \cdots }
      | c = equating imaginary parts
}}
{{eqn | ll= \leadsto
      | l = \tan \sum_j \theta_j
      | r = \frac {\paren {s_1 - s_3 + s_5 - \cdots} } {1 - s_2 + s_4 - \cdots}
      | c = $\dfrac {\paren 2} {\paren 1}$
}}
{{end-eqn}}
{{qed}}