nyuuzyou/wikis huggingface dataset:
Conditional is Equivalent to Negation of Conjunction with Negative/Formulation 2/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
$\begin{array}{|ccc|c|ccccc|} \hline
(p & \implies & q) & \iff & (\neg & (p & \land & \neg & q)) \\
\hline
\F & \T & \F & \T & \T & \F & \F & \T & \F \\
\F & \T & \T & \T & \T & \F & \F & \F & \T \\
\T & \F & \F & \T & \F & \T & \T & \T & \F \\
\T & \T & \T & \T & \T & \T & \F & \F & \T \\
\hline
\end{array}$
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 6$
* : $\S \text{I}: 13$: Logical Equivalences: Exercise $\text{(A)} \ 1$
Category:Conditional is Equivalent to Negation of Conjunction with Negative
Category:Truth Table Proofs
Conditional is Left Distributive over Conjunction/Formulation 1

== Theorem ==
:$p \implies \paren {q \land r} \dashv \vdash \paren {p \implies q} \land \paren {p \implies r}$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof 1 ==
== Proof by Truth Table ==
Category:Conditional is Left Distributive over Conjunction
Conditional is Left Distributive over Conjunction/Formulation 1/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connectives match for all boolean interpretations.
$\begin{array}{|ccccc||ccccccc|} \hline
p & \implies & (q & \land & r) & (p & \implies & q) & \land & (p & \implies & r) \\
\hline
\F & \T & \F & \F & \F & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \F & \T & \F & \T & \F & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \F & \T & \T & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \F & \T & \F & \F & \F & \T & \F & \F \\
\T & \F & \F & \F & \T & \T & \F & \F & \F & \T & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
Category:Conditional is Left Distributive over Conjunction
Category:Truth Table Proofs
Conditional is Left Distributive over Conjunction/Formulation 2

== Theorem ==
:$\vdash \paren {p \implies \paren {q \land r} } \iff \paren {\paren {p \implies q} \land \paren {p \implies r} }$
This can be expressed as two separate theorems:
=== Forward Implication ===
=== Reverse Implication ===
== Proof 1 ==
== Proof by Truth Table ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 3$: Theorem $\text{T29}$
Category:Conditional is Left Distributive over Conjunction
Conditional is Left Distributive over Conjunction/Formulation 2/Proof by Truth Table

== Theorem ==
== Proof ==
We apply the Method of Truth Tables.
As can be seen by inspection, the truth values under the main connective is true for all boolean interpretations.
$\begin{array}{|ccccc|c|ccccccc|} \hline
(p & \implies & (q & \land & r)) & \iff & ((p & \implies & q) & \land & (p & \implies & r)) \\
\hline
\F & \T & \F & \F & \F & \T & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \F & \T & \T & \F & \T & \F & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \T & \F & \T & \T & \T & \F & \T & \F \\
\F & \T & \T & \T & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\T & \F & \F & \F & \F & \T & \T & \F & \F & \F & \T & \F & \F \\
\T & \F & \F & \F & \T & \T & \T & \F & \F & \F & \T & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \T & \F & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
Category:Conditional is Left Distributive over Conjunction
Category:Truth Table Proofs
Conditional is Left Distributive over Conjunction/Forward Implication/Formulation 1

== Theorem ==
:$p \implies \paren {q \land r} \vdash \paren {p \implies q} \land \paren {p \implies r}$
== Proof ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction: Exercise $1 \ \text{(i)}$
* : $\S 1.2.1$: Rules for natural deduction: Exercises $1.4: \ 2 \ \text{(j)}$
Category:Conditional is Left Distributive over Conjunction
Conditional is Left Distributive over Conjunction/Forward Implication/Formulation 2/Proof

== Theorem ==
== Proof ==
Let us use the following abbreviations
Expanding the abbreviations leads us back to:
:$\paren {p \implies \paren {q \land r} } \implies \paren {\paren {p \implies q} \land \paren {p \implies r} }$
Category:Conditional is Left Distributive over Conjunction
Conditional is Left Distributive over Conjunction/Reverse Implication/Formulation 1

== Theorem ==
:$\paren {p \implies q} \land \paren {p \implies r} \vdash p \implies \paren {q \land r}$
== Proof ==
== Sources ==
* : Chapter $1$: The Propositional Calculus $1$: $3$ Conjunction and Disjunction: Exercise $1 \ \text{(c)}$
* : $\S 1.2.1$: Rules for natural deduction: Exercises $1.4: \ 2 \ \text{(k)}$
Category:Conditional is Left Distributive over Conjunction
Conditional is Left Distributive over Conjunction/Reverse Implication/Formulation 2/Proof

== Theorem ==
== Proof ==
Let us use the following abbreviations
Expanding the abbreviations leads us back to:
:$\paren {\paren {p \implies q} \land \paren {p \implies r} } \implies \paren {p \implies \paren {q \land r} }$
Category:Conditional is Left Distributive over Conjunction
Conditional is Left Distributive over Disjunction/Formulation 1

== Theorem ==
:$p \implies \paren {q \lor r} \dashv \vdash \paren {p \implies q} \lor \paren {p \implies r}$
This can be split into two parts:
=== Forward Implication ===
=== Reverse Implication ===
Category:Conditional is Left Distributive over Disjunction
Conditional is Left Distributive over Disjunction/Formulation 2

== Theorem ==
:$\vdash \paren {p \implies \paren {q \lor r} } \iff \paren {\paren {p \implies q} \lor \paren{p \implies r} }$
== Proof ==
== Sources ==
* : $\text{II}$: 'AND', 'OR', 'IF AND ONLY IF': $\S 5$: Theorem $\text{T55}$
Category:Conditional is Left Distributive over Disjunction
Conditional is not Associative

== Theorem ==
There exist propositions $p, q, r$ such that:
:$p \implies \paren {q \implies r} \not \vdash \paren {p \implies q} \implies r$
That is, the conditional is not associative.
== Proof ==
<onlyinclude>
We apply the Method of Truth Tables:
:$\begin{array}{|ccccc||ccccc|} \hline
p & \implies & (q & \implies & r) & (p & \implies & q) & \implies & r \\
\hline
\F & \T & \F & \T & \F & \F & \T & \F & \F & \F \\
\F & \T & \F & \T & \T & \F & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \F & \T & \T & \F & \F \\
\F & \T & \T & \T & \T & \F & \T & \T & \T & \T \\
\T & \T & \F & \T & \F & \T & \F & \F & \T & \F \\
\T & \T & \F & \T & \T & \T & \F & \F & \T & \T \\
\T & \F & \T & \F & \F & \T & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
As can be seen by inspection, the truth values under the main connectives do not match for all boolean interpretations.
Category:Conditional
Conditional is not Right Self-Distributive/Formulation 1

== Theorem ==
While this holds:
:$\paren {p \implies q} \implies r \vdash \paren {p \implies r} \implies \paren {q \implies r}$
its converse does not:
:$\paren {p \implies r} \implies \paren {q \implies r} \not \vdash \paren {p \implies q} \implies r$
== Proof ==
We apply the Method of Truth Tables to the proposition:
:$\paren {p \implies q} \implies r \vdash \paren {p \implies r} \implies \paren {q \implies r}$
As can be seen for all boolean interpretations by inspection, where the truth value under the main connective on the is $\T$, that under the one on the is also $\T$:
$\begin{array}{|ccccc||ccccccc|} \hline
(p & \implies & q) & \implies & r & (p & \implies & r) & \implies & (q & \implies & r) \\
\hline
\F & \T & \F & \F & \F & \F & \T & \F & \T & \F & \T & \F \\
\F & \T & \F & \T & \T & \F & \T & \T & \T & \F & \T & \T \\
\F & \T & \T & \F & \F & \F & \T & \F & \F & \T & \F & \F \\
\F & \T & \T & \T & \T & \F & \T & \T & \T & \T & \T & \T \\
\T & \F & \F & \T & \F & \T & \F & \F & \T & \F & \F & \F \\
\T & \F & \F & \T & \T & \T & \T & \T & \T & \F & \T & \T \\
\T & \T & \T & \F & \F & \T & \F & \F & \T & \T & \F & \F \\
\T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
The two formulas are not equivalent, as the relevant columns do not match exactly.
For example, when $p = q = r = \F$ we have that:
:$\paren {p \implies q} \implies r = \F$
but:
:$\paren {p \implies r} \implies \paren {q \implies r} = \T$
Hence the result:
:$\paren {p \implies q} \implies r \vdash \paren {p \implies r} \implies \paren {q \implies r}$
but:
:$\paren {p \implies r} \implies \paren {q \implies r} \not \vdash \paren {p \implies q} \implies r$
Category:Truth Table Proofs
Category:Conditional is not Right Self-Distributive
Conditional is not Right Self-Distributive/Formulation 2

== Theorem ==
While this holds:
:$\vdash \paren {\paren {p \implies q} \implies r} \implies \paren {\paren {p \implies r} \implies \paren {q \implies r} }$
its converse does not:
:$\not \vdash \paren {\paren {p \implies r} \implies \paren {q \implies r} } \implies \paren {\paren {p \implies q} \implies r}$
== Proof ==
== Sources ==
Category:Conditional is not Right Self-Distributive
Conditions Satisfied by Linear Code

== Theorem ==
Let $p$ be a prime number.
Let $\Z_p$ be the set of residue classes modulo $p$.
Let $C := \tuple {n, k}$ be a linear code of a master code $\map V {n, p}$.
Then $C$ satisfies the following conditions:
:$(C \, 1): \quad \forall \mathbf x, \mathbf y \in C: \mathbf x + \paren {-\mathbf y} \in C$
:$(C \, 2): \quad \forall \mathbf x \in C, m \in \Z_p: m \times \mathbf x \in C$
where $+$ and $\times$ are the operations of codeword addition and codeword multiplication respectively.
== Proof ==
From Master Code forms Vector Space, $\map V {n, p}$ is a vector space.
By definition, $\tuple {n, k}$ is a subspace of $\map V {n, p}$.
The result follows by the fact that a subspace is itself a vector space.
== Sources ==
* : Chapter $6$: Error-correcting codes: Definition $6.2$
Category:Linear Codes
Conditions for C^1 Smooth Solution of Euler's Equation to have Second Derivative

== Theorem ==
Let $\map y x:\R \to \R$ be a real function.
Let $\map F {x, y, y'}:\R^3 \to \R$ be a real function.
Suppose $\map F {x, y, y'}$ has continuous first and second derivatives all its arguments.
Suppose $y$ has a continuous first derivative and satisfies Euler's equation: 
:$F_y - \dfrac \d {\d x} F_{y'} = 0$
Suppose:
:$\map {F_{y' y'} } {x, \map y x, \map y x'} \ne 0$
Then $\map y x$ has continuous second derivatives.
== Proof ==
Consider the difference
Overbar indicates that derivatives are evaluated along certain intermediate curves.
Divide $\Delta F_{y'} $ by $\Delta x$ and consider the limit $\Delta x \to 0$:
:$\ds \lim_{\Delta x \mathop \to 0} \frac {\Delta F_{y'} } {\Delta x} = \lim_{\Delta x \mathop \to 0} \paren {\overline F_{y'x} + \frac {\Delta y} {\Delta x} \overline F_{y' y} + \frac {\Delta y'} {\Delta x} \overline F_{y'y'} }$
Existence of second derivatives and continuity of $F$ is guaranteed by conditions of the theorem:
:$\ds \lim_{\Delta x \mathop \to 0} \frac {\Delta F_{y'} } {\Delta x} = F_{y' x}$
:$\ds \lim_{\Delta x \mathop \to 0} \overline F_{y' x} = F_{y' x}$
:$\ds \lim_{\Delta x \mathop \to 0} \overline F_{y' y} = F_{y' y}$
:$\ds \lim_{\Delta x \mathop \to 0} \overline F_{y' y} = F_{y'y'}$
Similarly:
:$\ds \lim_{\Delta x \mathop \to 0} \frac {\Delta y} {\Delta x} = y'$
By Product Rule for Limits of Real Functions, it follows that:
:$\ds \lim_{\Delta x \mathop \to 0} \frac {\Delta y'} {\Delta x} = y$
Hence $y$ exists wherever $F_{y' y'} \ne 0$.
Euler's equation and continuity of necessary derivatives of $F$ and $y$ implies that $y$ is continuous.
== Sources ==
* : $\S 1.4$: The Simplest Variational Problem. Euler's Equation
Category:Calculus of Variations
Conditions for Commutative Diagram on Quotient Mappings between Mappings

== Theorem ==
Let $A$ and $B$ be sets.
Let $\RR_S$ and $\RR_T$ be equivalence relations on $S$ and $T$ respectively.
Let $f: S \to T$ be a mapping from $S$ to $T$.
Let $S / \RR_S$ and $T / \RR_T$ be the quotient sets of $S$ and $T$ induced by $\RR_S$ and $\RR_T$ respectively.
Let $q_S: S \to S / \RR_S$ and $q_T: T \to T / \RR_T$ be the quotient mappings induced by $\RR_S$ and $\RR_T$ respectively.
Then a mapping $g: S / \RR_S \to T / \RR_T$ exists such that:
:$q_T \circ f = g \circ q_S$
:
:$\forall x, y \in S: x \mathrel {\RR_S} y \implies \map f x \mathrel {\RR_T} \map f y$
::$\begin {xy} \xymatrix@L + 2mu@ + 1em {
 S \ar[r]^*{f}
 \ar[d]_*{q_S}
& T \ar[d]^*{q_T} \\
S / \RR_S \ar@{-->}[r]_*{g} & T / \RR_T } \end {xy}$
== Proof ==
Consider the commutative diagram:
::$\begin {xy} \xymatrix@L + 2mu@ + 1em {
 S \ar[rr]^*{f}
 \ar[dd]_*{q_S}
 \ar[ddrr]^*{q_T \circ f}
& & T \ar[dd]^*{q_T} \\
& & \\
S / \RR_S \ar@{-->}[rr]_*{g} & & T / \RR_T } \end {xy}$
We consider the mapping $q_T \circ f: S \to T / \RR_T$.
From Condition for Mapping from Quotient Set to be Well-Defined:
:there exists a mapping $g: S / \RR_S \to T / \RR_T$ such that $g \circ q_S = q_T \circ f$
:
:$\forall x, y \in S: \tuple {x, y} \in \RR_S \implies \map {\paren {q_T \circ f} } x = \map {\paren {q_T \circ f} } y$
Hence:
== Sources ==
* : Chapter $\text{I}$: Sets and Functions: Problem $\text{CC}$: Factoring through Quotients
Category:Quotient Mappings
Conditions for Connected Riemannian Manifold to be Isometric to Quotient of Connected Riemannian Manifold by Covering Automorphism Group

== Theorem ==
Let $\struct {M, g}$ and $\struct {\tilde M, \tilde g}$ be connected Riemannian manifolds.
Let $\pi : \tilde M \to M$ be a normal Riemannian covering map.
Let $\Gamma = \map {\operatorname {Aut}_\pi} {\tilde M}$ be the covering automorphism group.
Then $M$ is isometric to $\tilde M ~/~\Gamma$.
== Proof ==
== Sources ==
* : $\S 2$: Riemannian Metrics. Methods for Constructing Riemannian Metrics
Category:Riemannian Geometry
Conditions for Diameter to be Perpendicular Bisector

== Theorem ==
If in a circle a diameter bisects a chord (which is itself not a diameter), then it cuts it at right angles, and if it cuts it at right angles then it bisects it.
== Proof ==
:
Let $ABC$ be a circle, in which $AB$ is a chord which is not a diameter (i.e. it does not pass through the center).
=== First part ===
Let $CD$ be a diameter which bisects $AB$ at the point $F$.
Find the center $E$ of circle $ABC$, and join $EA$ and $EB$.
Because $E$ is the center, $EA = EB$.
Because $F$ bisects $AB$, $FA = FB$.
Also, $FE$ is common, so from Triangle Side-Side-Side Congruence $\triangle AFE = \triangle BFE$.
From :
:
So $\angle AFE$ and $\angle BFE$ are both right angles.
Therefore the diameter $CD$ cuts $AB$ at right angles.
=== Second part ===
Let $CD$ be a diameter which cuts $AB$ at right angles at point $F$.
We using the same construction as above.
Because $E$ is the center, $EA = EB$.
From Isosceles Triangle has Two Equal Angles, $\angle EAF = \angle EBF$.
But $\angle AFE = \angle BFE$ because both are right angles.
As $EF$ is common, it follows from Triangle Side-Angle-Angle Congruence that $\triangle AFE = \triangle BFE$.
Therefore $AF = FB$.
Hence the result.
== Sources ==
* : Book $\text{III}$. Propositions
Category:Circles
Conditions for Extremal Embedding in Field of Functional

== Theorem ==
Let $J$ be a functional such that:
:$\ds J \sqbrk {\mathbf y} = \int_a^b \map F {x, \mathbf y, \mathbf y'} \rd x$
Let $\gamma$ be an extremal of $J$, defined by $\mathbf y = \map {\mathbf y} x$ for $x \in \closedint a b$.
Suppose:
:$\forall x \in \closedint a b: \map \det {F_{\mathbf y' \mathbf y'} } \ne 0$
Suppose no points conjugate to $\paren {a, \map {\mathbf y} a}$ lie on $\gamma$.
Then $\gamma$ can be embedded in a field.
== Proof ==
Let $c \in \R$ be conjugate to $a$, such that $c < a$.
By assumption:
:$c \notin \closedint a b$
Hence, there exists a set $\closedint c b$ such that:
:$\closedint c b = \closedint c a \cup \closedint a b$
where $\size {c - a} > 0$.
By there exists a real point between two real points:
:$\exists \epsilon: \size {c - a} > \epsilon > 0$
Therefore, there exists $\epsilon > 0$ such that:
:$\gamma$ can be extended onto the whole interval $\closedint {a - \epsilon} b$, where extension means definition of some mapping in $\hointr {a - \epsilon} a$
:the interval $\closedint {a - \epsilon} b$ contains no points conjugate to $a$.
Consider a family of extremals leaving the point $\tuple {a - \epsilon, \map {\mathbf y} {a - \epsilon} }$.
There are no points conjugate to $a - \epsilon$ in $\closedint {a - \epsilon} b$.
Hence, for $x \in \closedint a b$ no two extremals in this family which are sufficiently close to the original extremal $\gamma$ can intersect.
Since all the functions are extremals, they satisfy same differential equations.
Lack of intersection implies different boundary conditions.
Denote these conditions collectively as $\map {\boldsymbol \psi} {x, \mathbf y} = \map {\mathbf y'} x$.
Thus, in some region $R$ containing $\gamma$ extremals sufficiently close to $\gamma$ define a central field in which $\gamma$ is embedded.
By Central Field is Field of Functional, $\gamma$ can be embedded in the field of functional.
== Sources ==
* : $\S 6.32$: The Field of a Functional
Category:Calculus of Variations
Conditions for Floor of Log base b of x to equal Floor of Log base b of Floor of x

== Theorem ==
Let $b \in \R$ be a real number.
:$\forall x \in \R_{\ge 1}: \floor {\log_b x} = \floor {\log_b \floor x} \iff b \in \Z_{> 1}$
where $\floor x$ denotes the floor of $x$.
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $\S 1.2.4$: Integer Functions and Elementary Number Theory: Exercise $34$
Category:Logarithms
Category:Floor Function
Category:Conditions for Floor of Log base b of x to equal Floor of Log base b of Floor of x
Conditions for Floor of Log base b of x to equal Floor of Log base b of Floor of x/Proof 1

== Theorem ==
== Proof ==
=== Necessary Condition ===
Let:
:$\forall x \in \R_{\ge 1}: \floor {\log_b x} = \floor {\log_b \floor x}$
Let $x = b$.
Then:
:$\floor {\log_b b} = \floor {\log_b \floor b}$
 $b \notin \Z$.
Thus by Proof by Contradiction:
:$b \in \Z$
But for $\log_b$ to be defined, $b > 0$ and $b \ne 1$.
Hence:
:$b \in \Z_{> 1}$
=== Sufficient Condition ===
Let $b \in \Z_{> 1}$.
Let $\floor {\log_b x} = n$.
Then:
== Sources ==
* : $\S 1.2.4$: Integer Functions and Elementary Number Theory: Exercise $34$
Category:Conditions for Floor of Log base b of x to equal Floor of Log base b of Floor of x
Conditions for Floor of Log base b of x to equal Floor of Log base b of Floor of x/Proof 2

== Theorem ==
== Proof ==
We have that:
:Logarithm is Strictly Increasing
and:
:Real Natural Logarithm Function is Continuous
Suppose that $\log_b x \in \Z$: let $\log_b x = n$, say.
Then:
:$x = b^n$
It follows that:
:$x \in \Z \iff b \in \Z$
Thus by McEliece's Theorem (Integer Functions):
:$\forall x \in \R_{\ge 1}: \floor {\log_b x} = \floor {\log_b \floor x} \iff b \in \Z_{>1}$
== Sources ==
* : $\S 1.2.4$: Integer Functions and Elementary Number Theory: Exercise $34$
Category:Conditions for Floor of Log base b of x to equal Floor of Log base b of Floor of x
Conditions for Function to be First Integral of Euler's Equations for Vanishing Variation

== Theorem ==
Let $\Phi = \map {\Phi} {x, \family {y_i}_{1 \mathop \le i \mathop \le n}, \family {p_i}_{1 \mathop \le i \mathop \le n} }$ be a real function.
Let $H$ be Hamiltonian.
Then a necessary and sufficient condition for $\Phi$ to be the first integral of Euler's Equations is
:$\dfrac {\partial \Phi} {\partial x} + \sqbrk{\Phi, H} = 0$
=== Corollary 1 ===
=== Corollary 2 ===
== Proof ==
For $\Phi$ to be the first integral:
:$\dfrac {\d \Phi} {\d x} = 0$
Hence the result.
== Sources ==
* : $\S 4.16$: The Canonical Form of the Euler's Equations
Category:Calculus of Variations
Conditions for Function to be First Integral of Euler's Equations for Vanishing Variation/Corollary 1

== Corollary to Conditions for Function to be First Integral of Euler's Equations for Vanishing Variation ==
Consider the Conditions for Function to be First Integral of Euler's Equations for Vanishing Variation.
Let $\dfrac {\partial\Phi} {\partial x}=0$.
Then $\Phi$ is the first integral if its Poisson Bracket with the Hamiltonian vanishes.
== Proof ==
Set $\dfrac {\partial \Phi} {\partial x} = 0$ in Conditions for Function to be First Integral of Euler's Equations for Vanishing Variation.
== Sources ==
* : $\S 4.17$: First Integrals of the Euler Equations
Category:Calculus of Variations
Conditions for Function to be First Integral of Euler's Equations for Vanishing Variation/Corollary 2

== Corollary to Conditions for Function to be First Integral of Euler's Equations for Vanishing Variation ==
Consider the Conditions for Function to be First Integral of Euler's Equations for Vanishing Variation.
Let $\Phi = H$.
Let $\dfrac {\partial H} {\partial x} = 0$.
Then $H$ is the first integral of Euler's Equations.
== Proof ==
The statment is proven from Conditions for Function to be First Integral of Euler's Equations for Vanishing Variation
by setting $\Phi = H$ and $\dfrac {\partial H} {\partial x} = 0$, and noticing that $\sqbrk{H, H} = 0$.
== Sources ==
* : $\S 4.17$: First Integrals of the Euler Equations
Category:Calculus of Variations
Conditions for Function to be Maximum of its Legendre Transform Two-variable Equivalent

== Theorem ==
Let $x, p \in \R$.
Let $\map f x$ be a strictly convex real function.
Let $f^*$ be a Legendre transformed $f$.
Let $\map g {x, p} = - \map {f^*} p + x p$
Then:
:$\ds \map f x = \max_p \paren {-\map {f^*} p + x p}$
where $\ds \max_p$ maximises the function with respect to a variable $p$.
== Proof ==
Function $g$ acquires an extremum along $p$, when its first derivative along $p$ vanishes:
To check if the extremum is a global maximum, consider the second derivative:
:$\dfrac {\partial^2 g} {\partial p^2} = - \dfrac {\partial^2 f^*} {\partial p^2}$
By Legendre Transform of Strictly Convex Real Function is Strictly Convex and Real Function is Strictly Convex iff Derivative is Strictly Increasing, it holds that:
Negative second derivative at the extremum implies extremum being a global maximum.
Therefore:
:$\ds \max_p \paren{-\map {f^*} p + x p} = \bigvalueat {\paren {-\map {f^*} p + x p} } {x \mathop = \map { {f^*}'} p}$
The is the Legendre Transform of $f^*$.
However, $f^*$ is a Legendre transformed $f$.
By Legendre Transform is Involution, this equals $f$.
== Sources ==
* : $\S 4.18$: The Legendre Tranformation
Category:Calculus of Variations
Conditions for Functional to be Extremum of Two-variable Functional over Canonical Variable p

== Theorem ==
Let $y = \map y x$ and $\map F {x, y, y'}$ be real functions.
Let $\dfrac {\partial^2 F} {\partial {y'}^2} \ne 0$.
Let $\ds J \sqbrk y = \int_a^b \map F {x, y, y'} \rd x$
Let $\ds J \sqbrk {y, p} = \int_a^b \paren {-\map H {x, y, p} + p y'} \rd x$, where $H$ is the Hamiltonian of $J \sqbrk y$.
Then $\ds J \sqbrk y = \bigvalueat {J \sqbrk {y, p} } {\frac {\delta J \sqbrk{y, p} } {\delta p} \mathop = 0}$
== Proof ==
Euler's equation for $J \sqbrk {y, p}$:
Substitute this result back into the functional $J \sqbrk {y, p}$:
== Sources ==
* : $\S 4.18$: The Legendre Tranformation
Category:Calculus of Variations
Conditions for Homogeneity/Plane

== Theorem ==
The plane $P = \alpha_1 x_1 + \alpha_2 x_2 + \alpha_3 x_3 = \gamma$ is homogeneous $\gamma = 0$.
== Proof ==
=== Sufficient Condition ===
Let the plane $P = \alpha_1 x_1 + \alpha_2 x_2 + \alpha_3 x_3 = \gamma$ be homogeneous.
Then the origin $\tuple {0, 0, 0}$ lies on $P$.
Hence:
=== Necessary Condition ===
Let the equation of $P$ be $\alpha_1 x_1 + \alpha_2 x_2 + \alpha_3 x_3 = 0$.
Then:
:$0 = \alpha_1 0 + \alpha_2 0 + \alpha_3 0 \in P$
and so:
:$\tuple {0, 0, 0}$ lies on $P$
Hence $P$ is homogeneous.
== Sources ==
* : Chapter $\text {V}$: Vector Spaces: $\S 28$. Linear Transformations
Category:Linear Algebra
Category:Solid Analytic Geometry