avewright/proofwiki-math huggingface dataset:
Theorem: Linear Second Order ODE/y'' + 4 y = 8 x^2 - 4 x

The second order ODE:
:$(1): \quad y'' + 4 y = 8 x^2 - 4 x$
has the general solution:
:$y = C_1 \sin 2 x + C_2 \cos 2 x - 1 - x + 2 x^2$

Proof:
Taking Laplace transforms: 
:$\laptrans {y'' + 4 y} = \laptrans {8 x^2 - 4 x}$
We have: 
{{begin-eqn}}
{{eqn	| l = \laptrans {y'' + 4 y}
	| r = \laptrans {y''} + 4 \laptrans y
	| c = Linear Combination of Laplace Transforms
}}
{{eqn	| r = s^2 \laptrans y - s \map y 0 - \map {y'} 0
	| c = Laplace Transform of Second Derivative
}}
{{end-eqn}}
We also have: 
{{begin-eqn}}
{{eqn	| l = \laptrans {8 x^2 - 4 x}
	| r = 8 \laptrans {x^2} - 4 \laptrans x
	| c = Linear Combination of Laplace Transforms
}}
{{eqn	| r = \frac {8 \cdot 2!} {s^3} - \frac {4} {s^2}
	| c = Laplace Transform of Power
}}
{{eqn	| r = \frac {16 - 4 s} {s^3}
}}
{{end-eqn}}
So:
:$\paren {s^2 + 4} \laptrans y = s \map y 0 + \map {y'} 0 + \dfrac {16 - 4 s} {s^3}$
Giving: 
{{begin-eqn}}
{{eqn	| l = \laptrans y
	| r = \map y 0 \frac s {s^2 + 4} + \map {y'} 0 \frac 1 {s^2 + 4} + \frac {16 - 4 s} {s^3 \paren {s^2 + 4} }
}}
{{eqn	| r = \map y 0 \frac s {s^2 + 4} + \map {y'} 0 \frac 1 {s^2 + 4} + \frac 4 {s^3} + \frac {s + 1} {s^2 + 4} - \frac 1 {s^2} - \frac 1 s
	| c = partial fraction expansion
}}
{{eqn	| r = \paren {\map y 0 + 1} \frac s {s^2 + 4} + \paren {\map {y'} 0 + 1} \frac 1 {s^2 + 4} + \frac 4 {s^3} - \frac 1 {s^2} - \frac 1 s
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn	| l = y
	| r = \invlaptrans {\paren {\map y 0 + 1} \frac s {s^2 + 4} + \paren {\map {y'} 0 + 1} \frac 1 {s^2 + 4} + \frac 4 {s^3} - \frac 1 {s^2} - \frac 1 s}
	| c = {{Defof|Inverse Laplace Transform}}
}}
{{eqn	| r = \paren {\map y 0 + 1} \invlaptrans {\frac s {s^2 + 2^2} } + \frac {\paren {\map {y'} 0 + 1} } 2 \invlaptrans {\frac 2 {s^2 + 2^2} } + 2 \invlaptrans {\frac {2!} {s^3} } - \invlaptrans {\frac {1!} {s^2} } - \invlaptrans {\frac {0!} s}
	| c = Linear Combination of Laplace Transforms
}}
{{eqn	| r = \paren {\map y 0 + 1} \invlaptrans {\laptrans {\cos 2 x} } + \frac {\paren {\map {y'} 0 + 1} } 2 \invlaptrans {\laptrans {\sin 2 x} } + 2 \invlaptrans {\laptrans {x^2} } - \invlaptrans {\laptrans x} - \invlaptrans {\laptrans 1}
	| c = Laplace Transform of Cosine, Laplace Transform of Sine, Laplace Transform of Power
}}
{{eqn	| r = \paren {\map y 0 + 1} \cos 2 x + \paren {\frac {\paren {\map {y'} 0 + 1} } 2 } \sin 2 x - 1 - x + 2 x^2
	| c = {{Defof|Inverse Laplace Transform}}
}}
{{end-eqn}}
Setting $C_1 = \dfrac {\paren {\map {y'} 0 + 1} } 2$ and $C_2 = \map y 0 + 1$ gives the result.
{{qed}}
Theorem: Linear Second Order ODE/y'' + y = cosecant x

The second order ODE:
:$(1): \quad y'' + y = \csc x$
has the general solution:
:$y = C_1 \sin x + C_2 \cos x - x \cos x + \sin x \map \ln {\sin x}$

Proof:
It can be seen that $\paren 1$ is a nonhomogeneous linear second order ODE with constant coefficients in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = 0$
:$q = 1$
:$\map R x = \csc x$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$\paren 2: \quad y'' + y = 0$
From Linear Second Order ODE: $y'' + y = 0$, this has the general solution:
:$y_g = C_1 \sin x + C_2 \cos x$
It remains to find a particular solution $y_p$ to $\paren 1$.
Expressing $y_g$ in the form:
:$y_g = C_1 \map {y_1} x + C_2 \map {y_2} x$
we have:
{{begin-eqn}}
{{eqn | l = \map {y_1} x
      | r = \sin x
      | c = 
}}
{{eqn | l = \map {y_2} x
      | r = \cos x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {y_1'} x
      | r = \cos x
      | c = Derivative of Sine Function
}}
{{eqn | l = \map {y_2'} x
      | r = -\sin x
      | c = Derivative of Cosine Function
}}
{{end-eqn}}
By the Method of Variation of Parameters, we have that:
:$y_p = v_1 y_1 + v_2 y_2$
where:
{{begin-eqn}}
{{eqn | l = v_1
      | r = -\int \frac {y_2 \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{eqn | l = v_2
      | r = \int \frac {y_1 \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{end-eqn}}
where $\map W {y_1, y_2}$ is the Wronskian of $y_1$ and $y_2$.
We have that:
{{begin-eqn}}
{{eqn | l = \map W {y_1, y_2}
      | r = y_1 {y_2}' - y_2 {y_1}'
      | c = {{Defof|Wronskian}}
}}
{{eqn | r = \sin x \paren {- \sin x} - \cos x \cos x
      | c = 
}}
{{eqn | r = -\paren {\sin^2 x + \cos^2 x}
      | c = 
}}
{{eqn | r = -1
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v_1
      | r = \int -\frac {y_2 \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{eqn | r = -\int \frac {\cos x \csc x} {-1} \rd x
      | c = 
}}
{{eqn | r = \int \frac {\cos x} {\sin x} \rd x
      | c = {{Defof|Cosecant}}
}}
{{eqn | r = \map \ln {\sin x}
      | c = Primitive of $\cot x$
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = v_2
      | r = \int \frac {y_1 \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{eqn | r = \int \frac {\sin x \csc x} {-1} \rd x
      | c = 
}}
{{eqn | r = -\int \frac {\sin x} {\sin x} \rd x
      | c = {{Defof|Cosecant}}
}}
{{eqn | r = -x
      | c = 
}}
{{end-eqn}}
It follows that:
:$y_p = \sin x \map \ln {\sin x} - x \cos x$
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 \sin x + C_2 \cos x + \sin x \map \ln {\sin x} - x \cos x$
is the general solution to $\paren 1$.
{{qed}}
Theorem: Linear Second Order ODE/y'' - 2 y' + y = 0

The second order ODE:
:$(1): \quad y' ' - 2 y' + y = 0$
has the general solution:
:$y = C_1 e^x + C_2 x e^x$

Proof:
It can be seen that $(1)$ is a constant coefficient homogeneous linear second order ODE.
Its auxiliary equation is:
:$(2): \quad: m^2 - 2 m + 1 = 0$
From Solution to Quadratic Equation with Real Coefficients, the roots of $(2)$ are:
:$m_1 = m_2 = 1$
These are real and equal.
So from Solution of Constant Coefficient Homogeneous LSOODE, the general solution of $(1)$ is:
:$y = C_1 e^x + C_2 x e^x$
{{qed}}
Category:Examples of Constant Coefficient Homogeneous LSOODEs
164431euvezjgdjeqyeu5yfjzzhn7pi
Theorem: Linear Second Order ODE/y'' - 2 y' + y = 2 x

The second order ODE:
:$(1): \quad y' ' - 2 y' + y = 2 x$
has the general solution:
:$y = C_1 e^x + C_2 x e^x + 2 x + 4$

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE in the form:
:$y' ' + p y' + q y = \map R x$
where:
:$p = -2$
:$q = 1$
:$\map R x = 2 x$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$(2): \quad y' ' - 2 y' + y = 0$
From Linear Second Order ODE: $y' ' - 2 y' + y = 0$, this has the general solution:
:$y_g = C_1 e^x + C_2 x e^x$
It remains to find a particular solution $y_p$ to $(1)$.
Taking the expression $\map R x = 2 x$ and differentiating twice {{WRT|Differentiation}} $x$:
{{begin-eqn}}
{{eqn | l = \map R x
      | r = 2 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {R'} x
      | r = 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {R' '} x
      | r = 0
      | c = 
}}
{{end-eqn}}
Trying out $y = 2 x$ in $(1)$:
:$0 - 4 + 2 x = 2 x - 4$
which is off by that constant of $4$.
But by Derivative of Constant:
:$4' = 0$
Hence setting $y = 2 x + 4$:
:$0 - 4 + \paren {2 x + 4} = 2 x$
and it can be seen that $y_p = 2 x + 4$ is indeed a particular solution to $(1)$.
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 e^x + C_2 x e^x + 2 x + 4$
is the general solution to $(1)$.
{{qed}}
Theorem: Linear Second Order ODE/y'' - 2 y' + y = 2 x

The second order ODE:
:$(1): \quad y' ' - 2 y' + y = 2 x$
has the general solution:
:$y = C_1 e^x + C_2 x e^x + 2 x + 4$

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE in the form:
:$y' ' + p y' + q y = \map R x$
where:
:$p = -2$
:$q = 1$
:$\map R x = 2 x$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$(2): \quad y' ' - 2 y' + y = 0$
From Linear Second Order ODE: $y' ' - 2 y' + y = 0$, this has the general solution:
:$y_g = C_1 e^x + C_2 x e^x$
It remains to find a particular solution $y_p$ to $(1)$.
Expressing $y_g$ in the form:
:$y_g = C_1 \, \map {y_1} x + C_2 \, \map {y_2} x$
we have:
{{begin-eqn}}
{{eqn | l = \map {y_1} x
      | r = e^x
      | c = 
}}
{{eqn | l = \map {y_2} x
      | r = x e^x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map { {y_1}'} x
      | r = e^x
      | c = Derivative of Exponential Function
}}
{{eqn | l = \map { {y_2}'} x
      | r = x e^x + e^x
      | c = Derivative of Exponential Function, Product Rule for Derivatives
}}
{{end-eqn}}
By the Method of Variation of Parameters, we have that:
:$y_p = v_1 y_1 + v_2 y_2$
where:
{{begin-eqn}}
{{eqn | l = v_1
      | r = \int -\frac {y_2 \, \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{eqn | l = v_2
      | r = \int \frac {y_1 \, \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{end-eqn}}
where $\map W {y_1, y_2}$ is the Wronskian of $y_1$ and $y_2$.
We have that:
{{begin-eqn}}
{{eqn | l = \map W {y_1, y_2}
      | r = y_1 {y_2}' - y_2 {y_1}'
      | c = {{Defof|Wronskian}}
}}
{{eqn | r = e^x \paren {x e^x + e^x} - x e^x e^x
      | c = 
}}
{{eqn | r = x e^{2 x} + e^{2 x} - x e^{2 x}
      | c = 
}}
{{eqn | r = e^{2 x}
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v_1
      | r = \int -\frac {y_2 \, \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{eqn | r = \int -\frac {x e^x 2 x} {e^{2 x} } \rd x
      | c = 
}}
{{eqn | r = \int -2 x^2 e^{- x} \rd x
      | c = 
}}
{{eqn | r = 2 e^{-x} \paren {x^2 + 2 x + 2}
      | c = Primitive of $x^2 e^{a x}$
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = v_2
      | r = \int \frac {y_1 \, \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{eqn | r = \int \frac {e^x 2 x} {e^{2 x} } \rd x
      | c = 
}}
{{eqn | r = \int 2 x e^{-x} \rd x
      | c = 
}}
{{eqn | r = -2 e^{- x} \paren {x + 1}
      | c = Primitive of $x e^{a x}$
}}
{{end-eqn}}
It follows that:
{{begin-eqn}}
{{eqn | l = y_p
      | r = 2 e^{-x} \paren {x^2 + 2 x + 2} e^x - 2 e^{-x} \paren {x + 1} x e^x
      | c = 
}}
{{eqn | r = 2 x^2 + 4 x + 4 - 2 x^2 - 2 x
      | c = simplifying
}}
{{eqn | r = 2 x + 4
      | c = further simplifying
}}
{{end-eqn}}
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 e^x + C_2 x e^x + 2 x + 4$
is the general solution to $(1)$.
{{qed}}
Theorem: Linear Second Order ODE/y'' - 2 y' + y = 2 x

The second order ODE:
:$(1): \quad y' ' - 2 y' + y = 2 x$
has the general solution:
:$y = C_1 e^x + C_2 x e^x + 2 x + 4$

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE with constant coefficients in the form:
:$y' ' + p y' + q y = \map R x$
where:
:$p = -2$
:$q = 1$
:$\map R x = 2 x$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$(2): \quad y' ' - 2 y' + y = 0$
From Linear Second Order ODE: $y'' - 2 y' + y = 0$, this has the general solution:
:$y_g = C_1 e^x + C_2 x e^x$
We have that:
:$R \left({x}\right) = 2 x$
So from the Method of Undetermined Coefficients for Polynomial:
:$y_p = A_0 + A_1 x$
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = A_0 + A_1 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_p}'
      | r = A_1
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = {y_p}''
      | r = 0
      | c = Derivative of Constant
}}
{{end-eqn}}
Substituting into $(1)$:
{{begin-eqn}}
{{eqn | l = 0 - 2 A_1 + \paren {A_0 + A_1 x}
      | r = 2 x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -2 A_1 + A_0
      | r = 0
      | c = equating coefficients
}}
{{eqn | ll= \leadsto
      | l = A_1
      | r = 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = A_0
      | r = 4
      | c = 
}}
{{end-eqn}}
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 e^x + C_2 x e^x + 2 x + 4$
is the general solution to $(1)$.
{{qed}}
Theorem: Linear Second Order ODE/y'' - y' - 6 y = exp -x

The second order ODE:
:$(1): \quad y'' - y' - 6 y = e^{-x}$
has the general solution:
:$y = C_1 e^{3 x} + C_2 e^{-2 x} - \dfrac {e^{-x} } 4$

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE with constant coefficients in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = -1$
:$q = -6$
:$\map R x = e^{-x}$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$y'' - y' - 6 y = 0$
From Linear Second Order ODE: $y'' - y' - 6 y = 0$, this has the general solution:
:$y_g = C_1 e^{3 x} + C_2 e^{-2 x}$
We have that:
:$\map R x = e^{-x}$
and so from the Method of Undetermined Coefficients for the Exponential function:
:$y_p = \dfrac {K e^{a x} } {a^2 + p a + q}$
where:
:$K = 1$
:$a = -1$
:$p = -1$
:$q = -6$
Hence:
{{begin-eqn}}
{{eqn | l = y_p
      | r = \dfrac {e^{-x} } {1 + 1 - 6}
      | c = 
}}
{{eqn | r = -\dfrac {e^{-x} } 4
      | c = 
}}
{{end-eqn}}
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 e^{3 x} + C_2 e^{-2 x} - \dfrac {e^{-x} } 4$
{{qed}}
Theorem: Linear Second Order ODE/y'' - y' - 6 y = exp -x

The second order ODE:
:$(1): \quad y'' - y' - 6 y = e^{-x}$
has the general solution:
:$y = C_1 e^{3 x} + C_2 e^{-2 x} - \dfrac {e^{-x} } 4$

Proof:
It can be seen that $(1)$ is a nonhomogeneous linear second order ODE in the form:
:$y'' + p y' + q y = \map R x$
where:
:$p = -1$
:$q = -6$
:$\map R x = e^{-x}$
First we establish the solution of the corresponding constant coefficient homogeneous linear second order ODE:
:$y'' - y' - 6 y = 0$
From Linear Second Order ODE: $y'' - y' - 6 y = 0$, this has the general solution:
:$y_g = C_1 e^{3 x} + C_2 e^{-2 x}$
It remains to find a particular solution $y_p$ to $(1)$.
Expressing $y_g$ in the form:
:$y_g = C_1 \, \map {y_1} x + C_2 \, \map {y_2} x$
we have:
{{begin-eqn}}
{{eqn | l = \map {y_1} x
      | r = e^{3 x}
      | c = 
}}
{{eqn | l = \map {y_2} x
      | r = e^{-2 x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map { {y_1}'} x
      | r = 3 e^{3 x}
      | c = Derivative of Exponential Function
}}
{{eqn | l = \map { {y_2}'} x
      | r = -2 e^{-2 x}
      | c = Derivative of Exponential Function
}}
{{end-eqn}}
By the Method of Variation of Parameters, we have that:
:$y_p = v_1 y_1 + v_2 y_2$
where:
{{begin-eqn}}
{{eqn | l = v_1
      | r = \int -\frac {y_2 \, \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{eqn | l = v_2
      | r = \int \frac {y_1 \, \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{end-eqn}}
where $\map W {y_1, y_2}$ is the Wronskian of $y_1$ and $y_2$.
We have that:
{{begin-eqn}}
{{eqn | l = \map W {y_1, y_2}
      | r = y_1 {y_2}' - y_2 {y_1}'
      | c = {{Defof|Wronskian}}
}}
{{eqn | r = e^{3 x} \paren {-2 e^{-2 x} } - e^{-2 x} \paren {3 e^{3 x} }
      | c = 
}}
{{eqn | r = -2 e^x - 3 e^x
      | c = 
}}
{{eqn | r = -5 e^x
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v_1
      | r = \int -\frac {y_2 \, \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{eqn | r = \int -\frac {e^{-2 x} \cdot e^{-x} } {-5 e^x} \rd x
      | c = 
}}
{{eqn | r = \int \frac {e^{-4 x} } 5 \rd x
      | c = 
}}
{{eqn | r = -\frac 1 {20} e^{-4 x}
      | c = Primitive of $e^{a x}$
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = v_2
      | r = \int \frac {y_1 \, \map R x} {\map W {y_1, y_2} } \rd x
      | c = 
}}
{{eqn | r = \int \frac {e^{3 x} \cdot e^{-x} } {-5 e^x} \rd x
      | c = 
}}
{{eqn | r = \int -\frac {e^x} 5 \rd x
      | c = 
}}
{{eqn | r = -\frac 1 5 e^x
      | c = Primitive of $e^{a x}$
}}
{{end-eqn}}
It follows that:
{{begin-eqn}}
{{eqn | l = y_p
      | r = -\frac 1 {20} e^{-4 x} e^{3 x} - \frac 1 5 e^x e^{-2 x}
      | c = 
}}
{{eqn | r = -\frac 1 {20} e^{-x} - \frac 1 5 e^{-x}
      | c = simplifying
}}
{{eqn | r = -\frac 1 4 e^{-x}
      | c = further simplifying
}}
{{end-eqn}}
So from General Solution of Linear 2nd Order ODE from Homogeneous 2nd Order ODE and Particular Solution:
:$y = y_g + y_p = C_1 e^{3 x} + C_2 e^{-2 x} - \dfrac {e^{-x} } 4$
is the general solution to $(1)$.
{{qed}}
Theorem: Filtered iff Finite Subsets have Lower Bounds

Let $\struct {S, \precsim}$ be a preordered set.
Let $H$ be a non-empty subset of $S$.
Then $H$ is filtered {{iff}}:
:for every finite subset $A$ of $H$:
::$\exists h \in H: \forall a \in A: h \precsim a$

Proof:
This follows by {{mutatis}} of the proof of Directed iff Finite Subsets have Upper Bounds.
{{qed}}
Theorem: Tangent of Half Angle plus Quarter Pi

:$\map \tan {\dfrac x 2 + \dfrac \pi 4} = \tan x + \sec x$

Proof:
Firstly, we have:
{{begin-eqn}}
{{eqn | n = 1
      | l = \tan x
      | r = \frac {2 \tan \frac x 2} {1 - \tan ^2 \frac x 2}
      | c = Double Angle Formula for Tangent
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \map \tan {\frac x 2 + \frac \pi 4}
      | r = \frac {\tan \frac x 2 + \tan \frac \pi 4} {1 - \tan \frac x 2 \tan \frac \pi 4}
      | c = Tangent of Sum
}}
{{eqn | r = \frac {\tan \frac x 2 + 1} {1 - \tan \frac x 2}
      | c = Tangent of $45 \degrees$
}}
{{eqn | r = \frac {\paren {\tan \frac x 2 + 1} \paren {\tan \frac x 2 + 1} } {\paren {1 - \tan \frac x 2} \paren {\tan \frac x 2 + 1} }
}}
{{eqn | r = \frac {\tan^2 \frac x 2 + 2 \tan \frac x 2 + 1} {1 - \tan^2 \frac x 2}
      | c = Difference of Two Squares, Square of Sum
}}
{{eqn | r = \frac {2 \tan \frac x 2} {1 - \tan^2 \frac x 2} + \frac {\tan^2 \frac x 2 + 1} {1 - \tan^2 \frac x 2}
}}
{{eqn | r = \tan x + \frac {\tan^2 \frac x 2 + 1} {1 - \tan^2 \frac x 2}
      | c = Double Angle Formula for Tangent: see $(1)$ above
}}
{{eqn | r = \tan x + \frac {\sin^2 \frac x 2 + \cos^2 \frac x 2} {\cos^2 \frac x 2 - \sin^2 \frac x 2}
      | c = multiplying Denominator and Numerator by $\cos^2 \frac x 2$
}}
{{eqn | r = \tan x + \frac {\sin^2 \frac x 2 + \cos^2 \frac x 2} {\cos 2 \frac x 2}
      | c = Double Angle Formula for Cosine
}}
{{eqn | r = \tan x + \frac 1 {\cos x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \tan x + \sec x
      | c = Secant is Reciprocal of Cosine
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
Category:Tangent Function
Category:Secant Function
0wwp1p2ickye49m0s6kfoq8lv5b8409
Theorem: Linear Second Order ODE/y'' - 2 y' - 3 y = 0

The second order ODE:
:$(1): \quad y' ' - 2 y' - 3 y = 0$
has the general solution:
:$y = C_1 e^{3 x} + C_2 e^{-x}$

Proof:
It can be seen that $(1)$ is a constant coefficient homogeneous linear second order ODE.
Its auxiliary equation is:
:$(2): \quad: m^2 - 2 m - 3 = 0$
From Solution to Quadratic Equation with Real Coefficients, the roots of $(2)$ are:
:$m_1 = 3$
:$m_2 = -1$
These are real and unequal.
So from Solution of Constant Coefficient Homogeneous LSOODE, the general solution of $(1)$ is:
:$y = C_1 e^{3 x} + C_2 e^{-x}$
{{qed}}
Category:Examples of Constant Coefficient Homogeneous LSOODEs
r4dp0gmjs5zhz7upaa8eqcwbetxjnek
Theorem: Linear Second Order ODE/y'' + 2 y' + 5 y = 0

The second order ODE:
:$(1): \quad y' ' + 2 y' + 5 y = 0$
has the general solution:
:$y = e^{-x} \paren {C_1 \cos 2 x + C_2 \sin 2 x}$

Proof:
It can be seen that $(1)$ is a constant coefficient homogeneous linear second order ODE.
Its auxiliary equation is:
:$(2): \quad m^2 + 2 m + 5 = 0$
From Solution to Quadratic Equation with Real Coefficients, the roots of $(2)$ are:
:$m_1 = -1 + 2 i$
:$m_2 = -1 - 2 i$
So from Solution of Constant Coefficient Homogeneous LSOODE, the general solution of $(1)$ is:
:$y = e^{-x} \paren {C_1 \cos 2 x + C_2 \sin 2 x}$
{{qed}}
Category:Examples of Constant Coefficient Homogeneous LSOODEs
of0mdf6rkdb9yk0uxu1ejz5ljkh7gfw
Theorem: Singleton is Directed and Filtered Subset

Let $\struct {S, \precsim}$ be a preordered set.
Let $x$ be an element of $S$.
Then $\set x$ is directed and filtered subset of $S$.

Proof:
Let $y, z \in \set x$.
By definition of singleton:
:$ y = x \land z = x$
By definition of reflexivity:
:$y \precsim x \land z \precsim x$
Thus:
:$\exists h \in \set x: y \precsim h \land z \precsim h$
Thus by definition:
:$\set x$ is a directed subset of $S$.
$\set x$ is a filtered subset of $S$ by {{mutatis}}.
{{qed}}
Theorem: Second Order ODE/(x^2 - 1) y'' - 2 x y' + 2 y = 0

The second order ODE:
:$(1): \quad \paren {x^2 - 1} y' ' - 2 x y' + 2 y = 0$
has the general solution:
:$y = C_1 x + C_2 \paren {x^2 + 1}$

Proof:
Note that:
{{begin-eqn}}
{{eqn | l = y_1
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {y_1}'
      | r = 1
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = {y_1}' '
      | r = 0
      | c = Derivative of Constant
}}
{{end-eqn}}
and so by inspection:
:$y_1 = x$
is a particular solution of $(1)$.
$(1)$ can be expressed as:
:$(2): \quad y' ' - \dfrac {2 x} {x^2 - 1} y' + \dfrac 2 {x^2 - 1} y = 0$
which is in the form:
:$y' ' + \map P x y' + \map Q x y = 0$
where:
:$\map P x = - \dfrac {2 x} {x^2 - 1}$
:$\map Q x = \dfrac 2 {x^2 - 1}$
From Particular Solution to Homogeneous Linear Second Order ODE gives rise to Another:
:$\map {y_2} x = \map v x \, \map {y_1} x$
where:
:$\ds v = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x$
is also a particular solution of $(1)$.
We have that:
{{begin-eqn}}
{{eqn | l = \int P \rd x
      | r = \int \paren {- \dfrac {2 x} {x^2 - 1} } \rd x
      | c = 
}}
{{eqn | r = -\map \ln {x^2 - 1}
      | c = Primitive of Function under its Derivative
}}
{{eqn | ll= \leadsto
      | l = e^{-\int P \rd x}
      | r = e^{\map \ln {x^2 - 1} }
      | c = 
}}
{{eqn | r = x^2 - 1
      | c =  
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = v
      | r = \int \dfrac 1 { {y_1}^2} e^{-\int P \rd x} \rd x
      | c = Definition of $v$
}}
{{eqn | r = \int \dfrac 1 {x^2} \paren {x^2 - 1} \rd x
      | c = 
}}
{{eqn | r = \int \paren {1 - \dfrac 1 {x^2} } \rd x
      | c = 
}}
{{eqn | r = x + \frac 1 x
      | c = Primitive of Power
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = y_2
      | r = v y_1
      | c = Definition of $y_2$
}}
{{eqn | r = \paren {x + \frac 1 x} x
      | c = 
}}
{{eqn | r = x^2 + 1
      | c = 
}}
{{end-eqn}}
From Two Linearly Independent Solutions of Homogeneous Linear Second Order ODE generate General Solution:
:$y = C_1 x + C_2 \paren {x^2 + 1}$
{{qed}}
Category:Examples of Homogeneous LSOODEs
mqax2wxdc8251m12bc5oc8vyu1zb2ea
Theorem: Directed iff Lower Closure Directed

Let $\struct {S, \precsim}$ be a preordered set.
Let $H$ be a non-empty subset of $S$.
Then $H$ is directed {{iff}}:
:$H^\precsim$ is directed
where $H^\precsim$ denotes the lower closure of $H$ with respect to $\precsim$.

Proof:
=== Sufficient Condition ===
Let us assume that $H$ is directed.
Let $x, y \in H^\precsim$.
By definition of lower closure:
:$\exists x' \in H: x \precsim x'$
and
:$\exists y' \in H: y \precsim y'$
By definition of directed subset:
:$\exists z \in H: x' \precsim z \land y' \precsim z$
By definition of reflexivity;
:$z \precsim z$
By definition of lower closure:
:$z \in H^\precsim$
Thus by definition of transitivity:
:$\exists z \in H^\precsim: x \precsim z \land y \precsim z$
Thus by definition:
:$H^\precsim$ is directed.
{{qed|lemma}}
Theorem: Filtered iff Upper Closure Filtered

Let $\struct {S, \precsim}$ be a preordered set.
Let $H$ be a non-empty subset of $S$.
Then $H$ is filtered {{iff}}
$H^\succsim$ is filtered
where $H^\succsim$ denotes the upper closure of $H$.

Proof:
This follows by {{mutatis}} of the proof of Directed iff Lower Closure Directed.
{{qed}}