avewright/proofwiki-math huggingface dataset:
Theorem: Mean Ergodic Theorem

Let $\struct {X, \BB, \mu, T}$ be a measure-preserving dynamical system.
Let $\map {L^2_\C} \mu$ be the complex-valued $L^2$ space of $\mu$.
Let $U_T : \map {L^2_\C} \mu \to \map {L^2_\C} \mu$ of $T$ be the Koopman operator.
Let $I := \set {f \in \map {L^2_\C} \mu : \map {U_T} f = f}$.
Then for each $f \in \map {L^2_\C} \mu$:
:$\ds \lim_{N \mathop \to \infty} \dfrac 1 N \sum_{n \mathop = 0}^{N - 1} \map {U_T^n} f = \map {P_T} f$ converges in the $L^2$-norm
where:
:$U_T^n$ denotes the $n$ times composition of $U_T$
:$P_T: \map {L^2_\C} \mu \to \map {L^2_\C} \mu$ denotes the orthogonal projection on the closed linear subspace $I$.

Proof:
Recall $L^2$ space forms Hilbert space.
That is, $\map {L^2_\C} \mu$ is a Hilbert space with the $L^2$ inner product:
:$\ds \innerprod f g := \int f \; \overline g \rd \mu$
Let $\norm \cdot$ be the norm of $\map {L^2_\C} \mu$.
By Koopman Operator is Isometry:
:$\forall f \in \map {L^2_\C} \mu : \norm {\map U f} = \norm f$
Therefore, the result follows from Mean Ergodic Theorem (Hilbert Space).
{{qed}}
Theorem: Medians of Triangle Meet at Centroid/Corollary

Let $AA'$ be produced beyond $BC$ to $X$, where $A'X = A'G$.
Then the straight lines $BX$ and $CX$ are parallel to $CC'$ and $BB'$ respectively, and $\dfrac 2 3$ of their length.

Proof:
{{improve|modify the diagram to add $C'$ to it}}
:360px
Consider the quadrilateral $\Box BGCX$.
Its diagonals are $GX$ and $BC$.
By construction, they bisect each other.
From Quadrilateral with Bisecting Diagonals is Parallelogram, $\Box BGCX$ is a parallelogram.
From Position of Centroid of Triangle on Median:
:$BG$ is $\dfrac 2 3$ the length of $BB'$
:$GC$ is $\dfrac 2 3$ the length of $CC'$
But as $\Box BGCX$ is a parallelogram:
:$BG = CX$
and:
:$GC = BX$
Hence the result.
{{qed}}
Theorem: External Center of Similitude of Circles with respect to Radii

Let $A$ and $B$ be the centers of two circles $\bigcirc Ar$ and $\bigcirc BR$ whose radii are $r$ and $R$ respectively, $r \ne R$.
Let $\bigcirc Ar$ and $\bigcirc BR$ be such that neither is completely enclosed inside the other.
Let $T$ be the external center of similitude of $\bigcirc Ar$ and $\bigcirc BR$.
Let $P$ and $Q$ be points on the circumference of $\bigcirc Ar$ and $\bigcirc BR$ respectively.
Then:
:the radii $AP$ and $QR$ are parallel
{{iff}}:
:$T$, $P$ and $Q$ are collinear.

Proof:
:500px
Theorem: Area of Regular Hexagon

Let $H$ be a regular hexagon.
Let the length of one side of $H$ be $s$.
Let $\AA$ be the area of $H$.
Then:
:$\AA = \dfrac {3 \sqrt 3} 2 s^2$

Proof:
From Regular Hexagon is composed of Equilateral Triangles, it follows that a regular hexagon can be dissected into six congruent equilateral triangles:
:300px
Let $\AA_T$ be the area of the bottom triangle. 
Then by Area of Equilateral Triangle:
: $ \AA_T = \dfrac{\sqrt 3} 4 s^2 $
As $H$ consists of six congruent triangles, it follows that:
: $ \AA = 6\AA_T = \dfrac{6\sqrt 3} 4 s^2 = \dfrac{3\sqrt3} 2 s^2 $
{{qed}}
Theorem: Area of Regular Hexagon

Let $H$ be a regular hexagon.
Let the length of one side of $H$ be $s$.
Let $\AA$ be the area of $H$.
Then:
:$\AA = \dfrac {3 \sqrt 3} 2 s^2$

Proof:
A regular hexagon is a regular 6-sided polygon.
Therefore:
{{begin-eqn}}
{{eqn | l = \AA
      | r = \dfrac 1 4 \times 6 \times s^2 \times \cot \dfrac \pi 6
      | c = Area of Regular Polygon
}}
{{eqn | r = \dfrac 3 2 \times s^2 \times \sqrt 3
      | c = Cotangent of $30 \degrees$
}}
{{eqn | r = \dfrac {3 \sqrt 3} 2 s^2
}}
{{end-eqn}}
{{qed}}
Theorem: Product Rule for Derivatives/General Result/3 Factors

Let $\map u x$, $\map v x$ and $\map w x$ be real functions differentiable on the open interval $I$.
Then:
:$\forall x \in I: \map {\dfrac \d {\d x} } {u v w} = u v \dfrac {\d w} {\d x} + u w \dfrac {\d v} {\d x} + v w \dfrac {\d u} {\d x}$

Proof:
Let $y = u v w$.
Then:
{{begin-eqn}}
{{eqn | q = 
      | l = y
      | r = u \paren {v w}
      | c = 
}}
{{eqn | r = \dfrac {\d u} {\d x} \paren {v w} + u \map {\dfrac \d {\d x} } {v w}
      | c = Product Rule for Derivatives
}}
{{eqn | r = v w \dfrac {\d u} {\d x} + u \paren {w \dfrac {\d v} {\d x} + v \dfrac {\d w} {\d x} }
      | c = Product Rule for Derivatives
}}
{{eqn | r = u v \dfrac {\d w} {\d x} + u w \dfrac {\d v} {\d x} + v w \dfrac {\d u} {\d x}
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Median of Trapezium is Parallel to Bases/Sufficient Condition

Let $\Box ABCD$ be a trapezium such that $AB$ and $DC$ are the parallel sides.
:300px
Let $E$ be the midpoint of $AD$.
Let $F$ lie on $BC$.
Let $EF$ be parallel to both $AB$ and $DC$.
Then $F$ is the midpoint of $BC$.

Proof:
:300px
Let $DH$ be constructed parallel to $BC$ to cut $AB$ at $H$.
From the Parallel Transversal Theorem:
:$DG : GH = DE : EA$
and so $G$ is the midpoint of $AH$.
That is:
:$(1): \quad DG = GH$
Then we have that:
:$DC$ is parallel to $GF$
and:
:$DG$ is parallel to $CF$
so, by definition, $\Box GFCD$ is a parallelogram.
Similarly, we have:
:$GF$ is parallel to $HB$
and:
:$GH$ is parallel to $FB$
so, by definition, $\Box GFBH$ is also a parallelogram.
By Opposite Sides and Angles of Parallelogram are Equal we have that:
:$CF = DG$
and:
:$GH = FB$
But from $(1)$:
:$DG = GH$
and so:
:$CF = FB$
and so $F$ is the midpoint of $CB$.
Theorem: Median of Trapezium is Parallel to Bases

Let $\Box ABCD$ be a trapezium such that $AB$ and $DC$ are the bases.
:300px
Let $E$ be the midpoint of $AD$.
Let $F$ lie on $BC$.
Then:
:$EF$ is parallel to both $AB$ and $DC$
{{iff}}:
:$F$ is the midpoint of $BC$.
That is, the median of $\Box ABCD$ is parallel to the bases of $\Box ABCD$.

Proof:
=== Sufficient Condition ===
{{:Median of Trapezium is Parallel to Bases/Sufficient Condition}}{{qed|lemma}}
Theorem: Median of Trapezium is Parallel to Bases/Necessary Condition

Let $\Box ABCD$ be a trapezium such that $AB$ and $DC$ are the parallel sides.
:300px
Let $E$ be the midpoint of $AD$.
Let $F$ be the midpoint of $BC$.
Then $EF$ is parallel to both $AB$ and $DC$.

Proof:
:300px
{{AimForCont}} $EF$ is not parallel to $DC$.
By Playfair's axiom, there exists a unique straight line through $E$ which ''is'' parallel to $DC$.
Let $EF'$ be this line.
From Median of Trapezium is Parallel to Bases: Sufficient Condition, $F'$ is the midpoint of $BC$.
But {{hypothesis}} $F$ is also the midpoint of $BC$.
That is:
:$F = F'$
So:
:$EF = EF'$
and so $EF$ is parallel to $DC$.
This contradicts our assertion that $EF$ is not parallel to $DC$.
Hence, by Proof by Contradiction, $EF$ is parallel to $DC$.
By definition of base of trapezium, $AB$ is parallel to $DC$.
By Parallelism is Transitive Relation, $EF$ is parallel to $AB$.
That is, $EF$ is parallel to both $AB$ and $DC$.
Theorem: Probability Density Function of Exponential Distribution

Let $X$ be a continuous random variable with the exponential distribution with parameter $\beta$.
Then the probability density function of $X$ is given by:
:$\map {f_X} x = \begin{cases} \dfrac 1 \beta e^{-\frac x \beta} & : x \ge 0 \\ 0 & : \text{otherwise} \end{cases}$

Proof:
By definition of exponential distribution:
:$\map {F_X} \Omega = \R_{\ge 0}$
:$\map \Pr {X < x} = 1 - e^{-\frac x \beta}$
where $0 < \beta$.
By definition of probability density function:
:$\forall x \in \R: \map {f_X} x = \begin {cases} \map {F_X'} x & : x \in \Sigma \\ 0 & : x \notin \Sigma \end {cases}$
where $\map {F_X'} x$ denotes the derivative of $F_X$ at $x$.
Then:
{{begin-eqn}}
{{eqn | l = f_X
      | r = \map {\dfrac \d {\d x} } {1 - e^{-\frac x \beta} }
      | c = 
}}
{{eqn | r = \dfrac 1 \beta e^{-\frac x \beta}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Primitive of Reciprocal of Root of a minus x by Cube of Root of x minus b

:$\ds \int \dfrac {\d x} {\paren {a - x}^{1/2} \paren {x - b}^{3/2} } = \dfrac 2 {b - a} \sqrt {\dfrac {a - x} {x - b} } + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cos^2 \theta + b \sin^2 \theta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d x} {\d \theta}
      | r = 2 a \cos \theta \paren {-\sin \theta} + 2 b \sin \theta \cos \theta
      | c = Chain Rule for Derivatives, Derivative of Cosine Function, Derivative of Sine Function
}}
{{eqn | n = 1
      | r = 2 \paren {b - a} \cos \theta \sin \theta
      | c = 
}}
{{end-eqn}}
Then we have:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cos^2 \theta + b \sin^2 \theta
      | c = 
}}
{{eqn | r = a \paren {1 - \sin^2 \theta} + b \sin^2 \theta
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = a - x
      | r = \paren {a - b} \sin^2 \theta
      | c = after algebra
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = x
      | r = a \cos^2 \theta + b \sin^2 \theta
      | c = 
}}
{{eqn | r = a \cos^2 \theta + b \paren {1 - \cos^2 \theta}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = x - b
      | r = \paren {a - b} \cos^2 \theta
      | c = after algebra
}}
{{eqn | n = 4
      | ll= \leadsto
      | l = \dfrac {a - x} {x - b}
      | r = \dfrac {\paren {a - b} \sin^2 \theta} {\paren {a - b} \cos^2 \theta}
      | c = $(2)$ divided by $(3)$
}}
{{eqn | l = \dfrac {a - x} {x - b}
      | r = \tan^2 \theta
      | c = {{Defof|Real Tangent Function}}
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \int \dfrac {\d x} {\paren {a - x}^{1/2} \paren {x - b}^{3/2} }
      | r = \int \dfrac {2 \paren {b - a} \cos \theta \sin \theta \rd \theta} {\paren {a - b}^{1/2} \sin \theta \paren {a - b}^{3/2} \cos \theta}
      | c = substituting from $(1)$, $(2)$ and $(3)$
}}
{{eqn | r = \dfrac 2 {b - a} \int \sec^2 \theta \rd \theta
      | c = simplification, and {{Defof|Real Secant Function}}
}}
{{eqn | r = \dfrac 2 {b - a} \tan \theta + C
      | c = Primitive of Square of Secant Function
}}
{{eqn | r = \dfrac 2 {b - a} \sqrt {\dfrac {a - x} {x - b} } + C
      | c = substituting from $(4)$
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Simple Connectedness

Let $T = \struct{S, \tau}$ be a path-connected topological space.
{{TFAE| def = Simply Connected}}

Proof:
=== Definition by fundamental group implies Definition by path-homotopy of loops ===
Let $x \in S$.
From Fundamental Group is Independent of Base Point for Path-Connected Space, it follows that all fundamental groups $\map {\pi_1}{T, x}$ are isomorphic to one group denoted $\map {\pi_1}{ T }$.
By assumption, it follows that $\map {\pi_1}{ T }$ is trivial.
As the single element of $\map {\pi_1}{T, x}$ is a homotopy class of paths, it follows that all loops in $T$ with base point $x$ belong to the same homotopy class.
It follows that these loops are path-homotopic.
{{qed|lemma}}
Theorem: Primitive of x squared by Exponential of x

:$\ds \int x^2 e^x \rd x = e^x \paren {x^2 - 2 x + 2} + C$

Proof:
From Primitive of $x^2 e^{a x}$:
{{:Primitive of x squared by Exponential of a x}}
The result follows by setting $a = 1$.
{{qed}}
Theorem: Primitive of x squared by Exponential of x

:$\ds \int x^2 e^x \rd x = e^x \paren {x^2 - 2 x + 2} + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = x^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = 2 x
      | c = Derivative of Power
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = e^x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = e^x
      | c = Primitive of $e^x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^2 e^x \rd x
      | r = x^2 e^x - \int 2 x e^x \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = x^2 e^x - 2 \int x e^x \rd x + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = x^2 e^x - 2 \paren {e^x \paren {x - 1} } + C
      | c = Primitive of $x e^{a x}$ with $a = 1$
}}
{{eqn | r = e^x \paren {x^2 - 2 x + 2} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x by Arctangent of x

:$\ds \int x \arctan x \rd x = \frac {x^2 + 1} 2 \arctan x - \frac x 2 + C$

Proof:
From Primitive of $x \arctan \dfrac x a$:
{{:Primitive of x by Arctangent of x over a}}
The result follows on setting $a = 1$.
{{qed}}
Theorem: Primitive of x by Arctangent of x

:$\ds \int x \arctan x \rd x = \frac {x^2 + 1} 2 \arctan x - \frac x 2 + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arctan x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac 1 {x^2 + 1}
      | c = Derivative of $\arctan x$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^2} 2
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x \arctan x \rd x
      | r = \frac {x^2} 2 \arctan x - \int \frac {x^2} 2 \paren {\frac 1 {x^2 + 1} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^2} 2 \arctan x - \frac 1 2 \int \frac {x^2 \rd x} {x^2 + 1} + C
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac {x^2} 2 \arctan x - \frac 1 2 \paren {x - 1 \arctan x} + C
      | c = Primitive of $\dfrac {x^2} {x^2 + a^2}$ with $a = 1$
}}
{{eqn | r = \frac {x^2 + 1} 2 \arctan x - \frac x 2 + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cube of Secant Function

:$\ds \int \sec^3 x \rd x = \frac 1 2 \paren {\sec x \tan x + \ln \size {\sec x + \tan x} } + C$

Proof:
From Primitive of $\sec^3 a x$:
{{:Primitive of Cube of Secant of a x}}
The result follows on setting $a = 1$.
{{qed}}
Theorem: Primitive of Cube of Secant Function

:$\ds \int \sec^3 x \rd x = \frac 1 2 \paren {\sec x \tan x + \ln \size {\sec x + \tan x} } + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \sec a x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = a \sec a x \tan a x
      | c = Derivative of Function of Constant Multiple, Derivative of $\sec$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = \sec^2 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \tan x
      | c = Primitive of $\sec^2 x$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \sec^3 x \rd x
      | r = \int \sec x \sec^2 x \rd x
      | c = 
}}
{{eqn | r = \sec x \tan x - \int \tan x \paren {\sec x \tan x} \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \sec x \tan x - \int \tan^2 x \sec x \rd x + C
      | c = simplifying
}}
{{eqn | r = \sec x \tan x - \int \paren {\sec^2 x - 1} \sec x \rd x + C
      | c = Difference of $\sec^2$ and $\tan^2$
}}
{{eqn | r = \sec x \tan x - \int \sec^3 x \rd x + \int \sec x \rd x + C
      | c = Linear Combination of Primitives
}}
{{eqn | r = \sec x \tan x - \int \sec^3 x \rd x + \ln \size {\sec x + \tan x} + C
      | c = Primitive of $\sec x$
}}
{{eqn | ll= \leadsto
      | l = 2 \int \sec^3 a \rd x
      | r = \sec x \tan x + \ln \size {\sec x + \tan x} + C
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \int \sec^3 a \rd x
      | r = \dfrac 1 2 \paren {\sec x \tan x + \ln \size {\sec a x + \tan a x} } + C
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Composite Function/Corollary

Let $f$ and $g$ be a real functions which are integrable.
Let the composite function $g \circ f$ also be integrable.
Then:
{{begin-eqn}}
{{eqn | l = \int \map {\paren {g \circ f} } x \map {f'} x \rd x
      | r = \int \map g u \rd u
      | c = 
}}
{{end-eqn}}
where $u = \map f x$.

Proof:
{{begin-eqn}}
{{eqn | l = \map F x
      | r = \int \map {\paren {g \circ f} } x \map {f'} x \rd x
}}
{{eqn | r = \int \map g {\map f x} \map {f'} x \rd x
      | c = {{Defof|Composition of Mappings}}
}}
{{eqn | r = \int \map g u \map {f'} x \rd x
      | c = where $u = \map f x$
}}
{{eqn | ll= \leadsto
      | l = \frac {\d F} {\d x}
      | r = \map g u \map {f'} x
      | c = {{Defof|Primitive (Calculus)}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d F} {\d u} \frac {\d u} {\d x}
      | r = \map g u \map {f'} x
      | c = Chain Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \frac {\d F} {\d u} \frac \d {\d x} \map f x
      | r = \map g u \map {f'} x
      | c = Definition of $u$
}}
{{eqn | ll= \leadsto
      | l = \frac {\d F} {\d u} \map {f'} x
      | r = \map g u \map {f'} x
      | c = {{Defof|Derivative}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d F} {\d u}
      | r = \map g u
      | c = 
}}
{{eqn | ll= \leadsto
      | l = F
      | r = \int \map g u \rd u
      | c = {{Defof|Primitive (Calculus)}}
}}
{{end-eqn}}
{{qed}}
Category:Primitive of Composite Function
faefd9u2ukdcaoycxxuouulqkq9vav2
Theorem: Primitive of Cube of Sine Function

:$\ds \int \sin^3 x \rd x = \frac {\cos^3 x} 3 - \cos x + C$

Proof:
From Primitive of $\sin^3 a x$:
{{:Primitive of Cube of Sine of a x}}
The result follows by setting $a = 1$.
{{qed}}
Theorem: Primitive of Fourth Power of Cosine Function

:$\ds \int \cos^4 x \rd x = \frac {3 x} 8 + \frac {\sin 2 x} 4 + \frac {\sin 4 x} {32} + C$

Proof:
From Primitive of $\cos^4 a x$:
{{:Primitive of Fourth Power of Cosine of a x}}
The result follows by setting $a = 1$.
{{qed}}
Theorem: Sine of 22.5 Degrees

:$\sin 22.5 \degrees = \sin \dfrac \pi 8 = \dfrac 1 2 \sqrt {2 - \sqrt 2}$

Proof:
{{begin-eqn}}
{{eqn | l = \sin 22.5 \degrees
      | r = \sin \frac {45 \degrees} 2
      | c = 
}}
{{eqn | r = +\sqrt {\frac {1 - \cos 45 \degrees} 2}
      | c = Half Angle Formula for Sine
}}
{{eqn | r = \sqrt {\frac {1 - \frac {\sqrt 2} 2} 2}
      | c = {{cos|45}}
}}
{{eqn | r = \sqrt {\frac {2 - \sqrt 2} 4}
      | c = multiplying top and bottom by 2
}}
{{eqn | r = \frac 1 2 \sqrt {2 - \sqrt 2}
      | c = factoring $\dfrac 1 2$ out of the square root
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of 22.5 Degrees

:$\cos 22.5 \degrees = \cos \dfrac \pi 8 = \dfrac 1 2 \sqrt {2 + \sqrt 2}$

Proof:
{{begin-eqn}}
{{eqn | l = \cos 22.5 \degrees
      | r = \cos \frac {45 \degrees} 2
      | c = 
}}
{{eqn | r = +\sqrt {\frac {1 + \cos 45 \degrees} 2}
      | c = Half Angle Formula for Cosine
}}
{{eqn | r = \sqrt {\frac {1 + \frac {\sqrt 2} 2} 2}
      | c = {{cos|45}}
}}
{{eqn | r = \sqrt {\frac {2 + \sqrt 2} 4}
      | c = multiplying top and bottom by 2
}}
{{eqn | r = \frac 1 2 \sqrt {2 + \sqrt 2}
      | c = factoring $\dfrac 1 2$ out of the square root
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square Root

:$\ds \int \sqrt x \rd x = \dfrac {2 x^{3 / 2} } 3 = \dfrac {2 \sqrt x^3} 3$

Proof:
From Primitive of Power:
{{:Primitive of Power}}
Hence:
{{begin-eqn}}
{{eqn | l = \int \sqrt x \rd x
      | r = \int x^{1/2} \rd x
      | c = {{Defof|Square Root}}
}}
{{eqn | r = \dfrac {x^{1/2 + 1} } {1/2 + 1} + C
      | c = Primitive of Power
}}
{{eqn | r = \dfrac {x^{3/2} } {3/2} + C
      | c = simplification
}}
{{eqn | r = \dfrac {2 \sqrt x^3} 3 + C
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Category:Examples of Use of Primitive of Power
Category:Primitives
Category:Square Roots
qvaxtaw6c3mkyyep7rmfmz5l4rzvjbe
Theorem: Condition for Conditional Expectation to be Almost Surely Non-Negative

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $X$ be an integrable random variable on $\struct {\Omega, \Sigma, \Pr}$.
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra of $\Sigma$.
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ given $\GG$.
Then we have: 
:$\expect {X \mid \GG} \ge 0$ almost everywhere
{{iff}}:
:$\expect {X \cdot \chi_A} \ge 0$ for each $A \in \GG$
where $\chi_A$ is the characteristic function of $A$.

Proof:
=== Sufficient Condition ===
Suppose that:
:$\expect {X \chi_A} \ge 0$ for each $A \in \GG$.
Then we have, by the definition of the conditional expectation of $X$ given $\GG$:
:$\expect {\expect {X \mid \GG} \chi_A} \ge 0$ for each $A \in \GG$.
Set: 
:$A = \set {\omega \in \Omega : \map {\paren {\expect {X \mid \GG} } } \omega < 0}$
Since $\expect {X \mid \GG}$ is $\GG$-measurable, we have $A \in \GG$ from Characterization of Measurable Functions.
From Expectation is Monotone, we have:
:$\expect {\expect {X \mid \GG} \chi_A} \le 0$
So, we have:
:$\expect {\expect {X \mid \GG} \chi_A} = 0$
Then, from Measurable Function Zero A.E. iff Absolute Value has Zero Integral, we have:
:$\expect {X \mid \GG} \chi_A = 0$ almost everywhere.
But, for all $\omega \in A$, we have:
:$\expect {X \mid \GG} \chi_A < 0$ 
Hence we have $\map \Pr A = 0$. 
So $\expect {X \mid \GG} \ge 0$ almost everywhere.
{{qed|lemma}}
Theorem: Conditional Expectation is Monotone

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $X$ and $Y$ be integrable random variables on $\struct {\Omega, \Sigma, \Pr}$ such that:
:$X \le Y$ almost everywhere. 
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra of $\Sigma$.
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$.
Then we have:
:$\expect {X \mid \GG} \le \expect {Y \mid \GG}$ almost everywhere.

Proof:
We have:
:$Y - X \ge 0$ almost everywhere.
So, for each $A \in \GG$ we have:
:$\paren {Y - X} \cdot 1_A \ge 0$ almost everywhere.
So, from Expectation is Monotone:
:$\expect {\paren {Y - X} \cdot 1_A} \ge 0$
for each $A \in \GG$.
So, from Condition for Conditional Expectation to be Almost Surely Non-Negative, we have:
:$\expect {Y - X \mid \GG} \ge 0$ almost everywhere.
Then, from Conditional Expectation is Linear:
:$\expect {Y \mid \GG} - \expect {X \mid \GG} \ge 0$ almost everywhere.
So that:
:$\expect {X \mid \GG} \le \expect {Y \mid \GG}$ almost everywhere.
{{qed}}
Category:Conditional Expectation
2z9xy4nqzglha3qaoo87xtl3uc3rtrq
Theorem: Conditional Expectation Conditioned on Trivial Sigma-Algebra

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $X$ be an integrable random variable.
Let $\expect {X \mid \set {\O, \Omega} }$ be a version of the conditional expectation of $X$ given $\set {\O, \Omega}$.
Then:
:$\expect {X \mid \set {\O, \Omega} } = \expect X$ almost everywhere.

Proof:
We check that $\expect X$ is a version of the conditional expectation of $X$ given $\set {\O, \Omega}$, so that we get:
:$\expect {X \mid \set {\O, \Omega} } = \expect X$ almost everywhere.
from Existence and Essential Uniqueness of Conditional Expectation Conditioned on Sigma-Algebra.
Note that $\expect X$ is $\GG$-measurable from Constant Function is Measurable.
We certainly have:
:$\ds \int_\O \expect X \rd \Pr = \int_\O X \rd \Pr = 0$
from Integral of Integrable Function over Null Set.
We also have:
:$\ds \int_\Omega \expect X \rd \Pr = \expect X = \int_\Omega X \rd \Pr$
from Integral of Characteristic Function.
So $\expect X$ is a version of the conditional expectation of $X$ given $\set {\O, \Omega}$, and we have the result.
{{qed}}
Category:Conditional Expectation
1dbk3bax2m1t1thr6vj9l89b9wezk7m