nyuuzyou/wikis huggingface dataset:
Forced Vibration of Cart attached to Wall by Spring/Problem Definition

== Definition of Problem ==
:
Consider a cart $C$ of mass $m$ attached to a wall by means of a spring $S$.
Let $C$ be free to move along a straight line in a medium which applies a damping force $\mathbf F_d$ whose magnitude is proportional to the speed of $C$.
Let the force constant of $S$ be $k$.
Let the constant of proportion of the damping force $\mathbf F_d$ be $c$.
Let there be applied to $C$ an external force which varies as a function of time as:
:$\mathbf F_e = \mathbf F_0 \cos \omega t$
where $\mathbf F_0$ is constant.
Let the displacement of $C$ at time $t$ from the equilibrium position be $\mathbf x$.
== Sources ==
* : $\S 3.20$: Vibrations in Mechanical Systems$
Category:Mechanics
Forcing Frequency for Resonance of Cart attached to Wall by Spring

== Theorem ==
=== Problem Definition ===
Then the resonance frequency of $C$ is:
:$\nu_R = \dfrac 1 {2 \pi} \sqrt {\dfrac k m - \dfrac {c^2} {2 m^2} }$
== Proof ==
From Forced Vibration of Cart attached to Wall by Spring, the equation of motion of $C$ is:
:$(1): \quad m \dfrac {\d^2 \mathbf x} {\d t^2} + c \dfrac {\d \mathbf x} {\d t} + k \mathbf x = \mathbf F_0 \cos \omega t$
Let:
:$a^2 = \dfrac k m$
:$2 b = \dfrac c m$
:$K = \dfrac {\mathbf F_0} m$
This is in the form:
:$(2): \quad \dfrac {\d^2 y} {\d x^2} + 2 b \dfrac {\d y} {\d x} + a^2 x = K \cos \omega x$
where:
:$K \in \R: k > 0$
:$a, b \in \R_{>0}: b < a$
From Condition for Resonance in Forced Vibration of Underdamped System, $C$ is in resonance when:
:$\omega = \sqrt {a^2 - 2 b^2}$
Thus, substituting back for $a$ and $b$:
By definition of frequency of simple harmonic motion:
:$\nu_R = \dfrac 1 {2 \pi} \sqrt {\dfrac k m - \dfrac {c^2} {2 m^2} }$
== Sources ==
* : $\S 3.20$: Problem $1$
Category:Mechanics
Forking is Local

== Theorem ==
Let $T$ be a complete $\LL$-theory.
Let $\mathfrak C$ be a monster model for $T$.
Let $A\subseteq B$ be subsets of the universe of $\mathfrak C$.
Let $\map \pi {\bar x}$ be an $n$-type over $B$.
$\pi$ forks over $A$ a finite subset of $\pi$ forks over $A$.
== Proof ==
Suppose $\pi$ forks over $A$.
:By definition, $\pi$ implies a disjunction of formulas which each divide over $A$.
:Since proofs are finite, this means that there is a finite subset of $\pi$ which implies this disjunction, completing this direction of the proof.
Suppose a finite subset of $\pi$ forks over $A$.
:By definition, the finite subset implies a disjunction of formulas which each divide over $A$.
:But then $\pi$ clearly implies this disjunction as well, completing this direction of the proof.
Category:Model Theory for Predicate Logic
Form of Elements of Inductive Semigroup

== Theorem ==
Let $\struct {S, \circ}$ be an inductive semigroup.
Then the elements of $S$ are of the form:
:$\alpha \circ \beta \circ \beta \circ \cdots \circ \beta$
== Proof ==
Recall the definition of inductive semigroup:
It follows from the definition that all elements of the form:
:$\alpha \circ \beta \circ \beta \circ \cdots \circ \beta$
are indeed elements of $S$.
 $x \in S$ is not of the above form.
Let $A \subseteq S$ be such that $\alpha, x \in A$.
Then $A$ contains elements of the form:
:$x, x \circ \beta, x \circ \beta \circ \beta, \ldots$
Now let $B \subseteq S$ be such that $\alpha \in B$ but $x \notin B$.
Then $B$ is of the form:
:$\exists \alpha, \beta \in S: \paren {\alpha \in B \land \paren {\forall x \in B: x \circ \beta \in B} }$
but because $x \in S$ while $x \notin B$ it follows that:
:$B \ne S$
and so $S$ is not inductive.
From this contradiction it follows that all elements of $S$ are of the form:
:$\alpha \circ \beta \circ \beta \circ \cdots \circ \beta$
Category:Inductive Semigroups
Form of Geometric Sequence of Integers

== Theorem ==
Let $P = \sequence {a_j}_{0 \mathop \le j \mathop \le n}$ be a geometric sequence of length $n + 1$ consisting of integers only.
Then the $j$th term of $P$ is given by:
:$a_j = k p^{n - j} q^j$
where:
: the common ratio of $P$ expressed in canonical form is $\dfrac q p$
: $k$ is an integer.
=== Corollary ===
== Proof ==
Let $r$ be the common ratio of $P$.
From Common Ratio in Integer Geometric Sequence is Rational, $r$ is a rational number.
Let $r = \dfrac q p$ be in canonical form.
Thus, by definition:
:$p \perp q$
Let $a$ be the first term of $P$.
Then the sequence $P$ is:
:$P = \paren {a, a \dfrac q p, a \dfrac {q^2} {p^2}, \ldots, a \dfrac {q^n} {p^n} }$
All the elements of $P$ are integers, so, in particular:
:$a \dfrac {q^n} {p^n} \in \Z$
We have that: 
:$p \perp q$
From Powers of Coprime Numbers are Coprime:
:$q^n \perp p^n$
and so from Euclid's Lemma:
:$p^n \divides a$
Thus:
:$a = k p^n$
for some $k \in \Z$, and so:
:$P = \paren {k p^n, k q p^{n - 1}, k q^2 p^{n - 2}, \ldots, k q^{n - 1} p, k q^n}$
Category:Geometric Sequences of Integers
Form of Geometric Sequence of Integers/Corollary

== Corollary to Form of Geometric Sequence of Integers ==
Let $p$ and $q$ be integers.
Then the finite sequence $P = \sequence {a_j}_{0 \mathop \le j \mathop \le n}$ defined as:
:$a_j = p^j q^{n - j}$
is a geometric sequence whose common ratio is $\dfrac p q$.
== Proof ==
Let the greatest common divisor of $p$ and $q$ be $d$.
Then by Integers Divided by GCD are Coprime:
:$p = d r$
:$q = d s$
where $r$ and $s$ are coprime integers.
Thus:
:$a_j = p^j q^{n - j}$
and so by Form of Geometric Sequence of Integers it follows that $P$ is a geometric sequence whose common ratio is $\dfrac r s$.
Then:
Hence the result.
Category:Geometric Sequences of Integers
Form of Geometric Sequence of Integers from One

== Theorem ==
Let $Q_n = \sequence {a_j}_{0 \mathop \le j \mathop \le n}$ be a geometric sequence consisting of integers only.
Let $a_0 = 1$.
Then the $j$th term of $Q_n$ is given by:
:$a_j = a^j$
where:
:the common ratio of $Q_n$ is $a$
:$a = a_1$.
Thus:
:$Q_n = \tuple {1, a, a^2, \ldots, a^n}$
== Proof ==
From Form of Geometric Sequence of Integers, the $j$th term of $Q_n$ is given by:
:$a_j = k q^j p^{n - j}$
where:
:the common ratio of $Q_n$ expressed in canonical form is $\dfrac q p$
:$k$ is an integer.
As $a_0 = 1$ it follows that:
:$1 = k p^{n - j}$
from which it follows that:
:$k = 1$
:$p = 1$
and the common ratio of $Q_n$ is $q$.
Thus:
:$a_1 = q$
Setting $a = a_1$ yields the result as stated.
Category:Geometric Sequences of Integers
Form of Geometric Sequence of Integers in Lowest Terms

== Theorem ==
Let $G_n = \sequence {a_j}_{0 \mathop \le j \mathop \le n}$ be a geometric sequence of length $n$ consisting of positive integers only.
Let $r$ be the common ratio of $G_n$.
Let the elements of $G_n$ be the smallest positive integers such that $G_n$ has common ratio $r$.
Then the $j$th term of $G_n$ is given by:
:$a_j = p^{n - j} q^j$
where $r = \dfrac q p$.
That is:
:$G_n = \tuple {p^n, p^{n - 1} q, p^{n - 2} q^2, \ldots, p q^{n - 1}, q^n}$
== Proof ==
From Form of Geometric Sequence of Integers the $j$th term of $G_n$ is given by:
:$a_j = k p^{n - j} q^j$
where the common ratio is $\dfrac q p$.
Thus:
:$a_0 = k p^n$
:$a_n = k q^n$
From Geometric Sequence in Lowest Terms has Coprime Extremes it follows that $k = 1$.
Hence the result.
Category:Geometric Sequences of Integers
Form of Geometric Sequence of Integers with Coprime Extremes

== Theorem ==
Let $Q_n = \sequence {a_j}_{0 \mathop \le j \mathop \le n}$ be a geometric sequence of length $n$ consisting of positive integers only.
Let $a_1$ and $a_n$ be coprime.
Then the $j$th term of $Q_n$ is given by:
:$a_j = q^j p^{n - j}$
== Proof ==
Let $r$ be the common ratio of $Q_n$.
Let the elements of $Q_n$ be the smallest positive integers such that $Q_n$ has common ratio $r$.
From Geometric Sequence with Coprime Extremes is in Lowest Terms, the elements of $Q_n$ are the smallest positive integers such that $Q_n$ has common ratio $r$.
From Form of Geometric Sequence of Integers in Lowest Terms the $j$th term of $P$ is given by:
:$a_j = q^j p^{n - j}$
where $r = \dfrac p q$.
Hence the result.
Category:Geometric Sequences of Integers
Form of Logit for Logistic Curve

== Theorem ==
Let $p$ denote the probability of the occurrence of an event.
Let $p$ satisfy a logistic relationship with an explanatory variable $x$ of the form:
:$p = \dfrac 1 {1 + \map \exp {-\paren {\alpha + \beta x} } }$
Let $Y$ be the logit of $p$.
Then:
:$Y = \alpha + \beta x$
== Proof ==
By definition, the logit of $p$ is given by:
:$Y = \map \ln {\dfrac p {1 - p} }$
In order to simplify the algebra, let $c = -\paren {\alpha + \beta x}$.
Then we have:
== Sources ==
* 
* 
Category:Logit
Category:Logistic Curve
Form of Prime Sierpiński Number of the First Kind

== Theorem ==
Suppose $S_n = n^n + 1$ is a prime Sierpiński number of the first kind.
Then:
:$n = 2^{2^k}$
for some integer $k$.
== Proof ==
 $n$ has an odd divisor $d$.
By Sum of Two Odd Powers:
:$\paren {n^{n/d} + 1} \divides \paren {\paren {n^{n/d}}^d + 1^d} = S_n$
thus $S_n$ is composite, which is a contradiction.
Hence $n$ has no odd divisors.
That is, $n$ is a power of $2$.
Write $n = 2^m$.
 that $m$ has an odd divisor $f$.
By Sum of Two Odd Powers:
:$\paren {2^{n m/f} + 1} \divides \paren {\paren {2^{n m/f}}^f + 1^f} = 2^{m n} + 1 = S_n$
thus $S_n$ is composite, which is a contradiction.
Hence $m$ has no odd divisors.
That is, $m$ is a power of $2$.
Therefore we must have:
:$n = 2^{2^k}$
for some integer $k$.
== Also see ==
* Prime Sierpiński Numbers of the First Kind
Category:Sierpiński Numbers of the First Kind
Form of Spherical Harmonic

== Theorem ==
A spherical harmonic has the form:
:$r^n \paren {a_n \map {P_n} {\cos \theta} + \ds \sum_{m \mathop = 1}^n \paren { {a_n}^m \cos m \phi + {b_n}^m \sin m \phi} \map { {P_n}^m} {\cos \theta} }$
where:
:$P_n$ denotes a Legendre polynomial
:${P_n}^m$ denotes an associated Legendre function.
== Proof ==
== Sources ==
* 
* 
Category:Spherical Harmonics
Formal Derivative of Polynomials Satisfies Leibniz's Rule

== Theorem ==
Let $R$ be a commutative ring with unity.
Let $R \sqbrk X$ be the polynomial ring over $R$.
Let $f, g \in R \sqbrk X$ be polynomials.
Let $f'$ and $g'$ denote their formal derivatives.
Then:
:$\paren {f g}' = f g' + f' g$
== Proof ==
Both sides are bilinear functions of $f$ and $g$, so it suffices to verify the equality in the case where $\map f X = X^n$ and $\map g x = X^m$.
Then:
:$\paren {X^n X^m}' = \paren {n + m} X^{n + m - 1}$
and:
:$\paren {X^n}' X^m + X^n \paren {X^m}' = n X^{n - 1} X^m + m X^n X^{m - 1}$
Category:Polynomial Theory
Formation of Ordinary Differential Equation by Elimination/Examples

== Examples of Formation of Ordinary Differential Equation by Elimination ==
=== Simple Harmonic Motion ===
=== Parabolas whose Axes are $x$-Axis ===
=== Straight Line through Origin ===
=== Example: $y = A e^{2 x} + B e^{-2 x}$ ===
=== Example: $y = A \cos 3 x + B \sin 3 x$ ===
=== Example: $y = A e^{B x}$ ===
=== Example: $y = Ax + A^3$ ===
=== Example: $x^2 + y^2 = a^2$ ===
Category:Formation of Ordinary Differential Equations by Elimination
Formation of Ordinary Differential Equation by Elimination/Examples/Parabolas whose Axes are X Axis

== Examples of Formation of Ordinary Differential Equation by Elimination ==
Consider the set of all parabolas embedded in the Cartesian plane whose axis is the $x$ axis.
This set can be expressed as the ordinary differential equation of order $2$:
:$y \dfrac {\d^2 y} {\d x^2} + \paren {\dfrac {\d y} {\d x} }^2 = 0$
== Proof ==
Such a parabola has the equation:
:$y^2 = 4 a \paren {x - h}$
Differentiating twice $x$:
== Sources ==
* : Chapter $\text I$: Introduction and Definitions. Elimination. Graphical Representation: $5$. Examples
Category:Formation of Ordinary Differential Equations by Elimination
Formation of Ordinary Differential Equation by Elimination/Examples/Simple Harmonic Motion

== Examples of Formation of Ordinary Differential Equation by Elimination ==
Consider the equation governing simple harmonic motion:
:$(1): \quad y = A \map \cos {\omega x + \phi}$
This can be expressed as the ordinary differential equation of order $3$:
:$y \cdot \dfrac {\d^3 y} {\d x^3} = \dfrac {\d y} {\d x} \cdot \dfrac {\d^2 y} {\d x^2}$
== Proof ==
This equation has a dependent variable of $y$ and an independent variable of $x$.
It is required to eliminate the arbitrary constants $A$, $\phi$ and $\omega$.
Differentiating $2$ times $x$:
We have arrived at a ordinary differential equation of order $2$:
:$\dfrac {\d^2 y} {\d x^2} = -\omega^2 y$
Now we differentiate one further time $x$:
== Sources ==
* : Chapter $\text I$: Introduction and Definitions. Elimination. Graphical Representation: $5$. Examples
Category:Formation of Ordinary Differential Equations by Elimination
Category:Simple Harmonic Motion
Formation of Ordinary Differential Equation by Elimination/Examples/Straight Line through Origin

== Examples of Formation of Ordinary Differential Equation by Elimination ==
Consider the set of all straight lines embedded in the Cartesian plane which pass through the origin.
This set can be expressed as the ordinary differential equation of order $1$:
:$\dfrac y x = \dfrac {\d y} {\d x}$
That is, the tangent at any point on a straight line through the origin is the straight line itself.
== Proof ==
From Equation of Straight Line in Plane: Slope-Intercept Form, such a straight line has the equation:
:$y = m x$
Differentiating $x$:
Hence the result.
== Sources ==
* : Chapter $\text I$: Introduction and Definitions. Elimination. Graphical Representation: Examples for solution: $(6)$
Category:Formation of Ordinary Differential Equations by Elimination
Formation of Ordinary Differential Equation by Elimination/Examples/x^2 + y^2 equals a^2

== Examples of Formation of Ordinary Differential Equation by Elimination ==
Consider the equation:
:$(1): \quad x^2 + y^2 = a^2$
This can be expressed as the ordinary differential equation:
:$\dfrac {\d y} {\d x} = -\dfrac x y$
which demonstrates that the radius of a circle where it meets the circle is perpendicular to the tangent at that point.
== Proof ==
Differentiating $x$:
From Equation of Circle center Origin, $(1)$ is the equation of a circle whose center is at the origin.
The straight line $R$ from the origin to the point $\tuple {x, y}$ on the circle has slope $\dfrac y x$ by definition.
From Slope of Orthogonal Curves, a straight line $T$ through $\tuple {x, y}$ such that $\dfrac {\d y} {\d x} = -\dfrac x y$ is perpendicular to $R$.
But $T$ is by definition the tangent to the circle at $\tuple {x, y}$.
Hence we have shown that the radius of a circle where it meets the circle is perpendicular to the tangent at that point.
== Sources ==
* : Chapter $\text I$: Introduction and Definitions. Elimination. Graphical Representation: Examples for solution: $(5)$
Category:Formation of Ordinary Differential Equations by Elimination
Formation of Ordinary Differential Equation by Elimination/Examples/y equals A cos 3x + B sin 3x

== Examples of Formation of Ordinary Differential Equation by Elimination ==
Consider the equation:
:$(1): \quad y = A \cos 3 x + B \sin 3 x$
This can be expressed as the ordinary differential equation of order $2$:
:$\dfrac {\d^2 y} {\d x^2} + 9 y = 0$
== Proof ==
Differentiating twice $x$:
== Sources ==
* : Chapter $\text I$: Introduction and Definitions. Elimination. Graphical Representation: Examples for solution: $(2)$
Category:Formation of Ordinary Differential Equations by Elimination
Formation of Ordinary Differential Equation by Elimination/Examples/y equals A e^2x + B e^-2x

== Examples of Formation of Ordinary Differential Equation by Elimination ==
Consider the equation:
:$(1): \quad y = A e^{2 x} + B e^{-2 x}$
This can be expressed as the ordinary differential equation of order $2$:
:$\dfrac {\d^2 y} {\d x^2} = 4 y$
== Proof ==
Differentiating twice $x$:
== Sources ==
* : Chapter $\text I$: Introduction and Definitions. Elimination. Graphical Representation: Examples for solution: $(1)$
Category:Formation of Ordinary Differential Equations by Elimination
Formation of Ordinary Differential Equation by Elimination/Examples/y equals A e^Bx

== Examples of Formation of Ordinary Differential Equation by Elimination ==
Consider the equation:
:$(1): \quad y = A e^{B x}$
This can be expressed as the ordinary differential equation of order $2$:
:$\dfrac {\d^2 y} {\d x^2} + 9 y = 0$
== Proof ==
Differentiating twice $x$:
== Sources ==
* : Chapter $\text I$: Introduction and Definitions. Elimination. Graphical Representation: Examples for solution: $(3)$
Category:Formation of Ordinary Differential Equations by Elimination
Formation of Ordinary Differential Equation by Elimination/Examples/y equals Ax + A^3

== Examples of Formation of Ordinary Differential Equation by Elimination ==
Consider the equation:
:$(1): \quad y = A x + A^3$
This can be expressed as the ordinary differential equation:
:$y = x \dfrac {\d y} {\d x} + \paren {\dfrac {\d y} {\d x} }^3$
== Proof ==
Differentiating $x$:
== Sources ==
* : Chapter $\text I$: Introduction and Definitions. Elimination. Graphical Representation: Examples for solution: $(4)$
Category:Formation of Ordinary Differential Equations by Elimination
Formula and its Negation Cannot Both Cause Forking

== Theorem ==
Let $T$ be a complete $\LL$-theory.
Let $\mathfrak C$ be a monster model for $T$.
Let $A \subseteq B$ be subsets of the universe of $\mathfrak C$.
Let $\map \pi {\bar x}$ be an $n$-type over $B$.
If $\pi$ does not fork over $A$, then for any formula $\map \phi {\bar x, \bar b}$, either $\pi \cup \set \phi$ or $\pi \cup \set {\neg \phi}$ does not fork over $A$.
== Proof ==
We prove the contrapositive.
Suppose both $\pi \cup \set \phi$ and $\pi \cup \set {\neg \phi}$ fork over $A$.
By definition of forking:
:$\pi \cup \set \phi$ implies $\map {\phi_1} {\bar x, \bar c_1} \vee \cdots \vee \map {\phi_k} {\bar x, \bar c_k}$ and
:$\pi \cup \set {\neg \phi}$ implies $\map {\psi_1} {\bar x, \bar d_1} \vee \cdots \vee \map {\psi_k} {\bar x, \bar d_h}$,
where each $\phi_i$ and $\psi_j$ divide over $A$.
Then $\pi$ implies the disjunction
:$\ds \bigvee_i \map \phi {\bar x, \bar c_i} \vee \bigvee_j \map \psi {\bar x, \bar d_i}$
with each component formula dividing over $A$.
By definition, this means that $\pi$ forks over $A$.
Category:Model Theory for Predicate Logic
Formula for Aerodynamic Drag

== Theorem ==
The following formula can be used in aerodynamics to calculate an estimate of the aerodynamic drag on a body $B$ passing through a fluid $F$ (usually air):
:$D = \dfrac 1 2 k \rho A v^2$
where:
:$D$ is the drag on $B$
:$A$ is a representative area of cross-section of $B$
:$\rho$ is the density of $F$
:$v$ is the speed of $B$ through $F$
:$k$ is a coefficient which depends on the conditions, and is a function of the Reynolds number.
== Proof ==
== Sources ==
* 
* 
Category:Aerodynamic Drag
Formula for Compound Interest

== Theorem ==
Let $P$ be a principal.
Let $r$ be the interest rate for a given conversion period.
Let $n$ be the number of conversion periods.
The amount of compound interest paid on $P$ at the end of $n$ conversion periods is given by:
:$I = P \paren {\paren {1 + r}^n - 1}$
== Proof ==
== Sources ==
* 
* 
Category:Compound Interest
Formula for Hydrodynamic Lift

== Theorem ==
The following formula can be used in hydrodynamics to calculate an estimate of the lift on a body $B$ passing through a fluid $F$ (usually air):
:$L = c \rho A v^2$
where:
:$L$ is the lift on $B$
:$A$ is a representative area of $B$, such as the area of a wing or hydrofoil
:$\rho$ is the density of $F$
:$v$ is the speed of $B$ through $F$
:$c$ is a coefficient which depends on the circulation of $F$ around $B$, and is a function of the Reynolds number.
== Proof ==
== Sources ==
* 
* 
Category:Lift
Formula for Radiocarbon Dating

== Theorem ==
Let $Q$ be a quantity of a sample of dead organic material (usually wood) whose time of death is to be determined.
Let $t$ years be the age of $Q$ which is to be determined.
Let $r$ denote the ratio of the quantity of carbon-14 remaining in $Q$ after time $t$ to the quantity of carbon-14 in $Q$ at the time of its death.
Then the number of years that have elapsed since the death of $Q$ is given by:
:$t = -8060 \ln r$
== Proof ==
Let $x_0$ denote the ratio of carbon-14 to carbon-12 in $Q$ at the time of its death.
Let $x$ denote the ratio of carbon-14 to carbon-12 in $Q$ after time $t$.
Thus:
:$r = \dfrac x {x_0}$
It is assumed that the rate of decay of carbon-14 is a first-order reaction.
Hence we use:
Chemical analysis tells us that after $10$ years, $99.876 \%$ of the carbon-14 that was present in the organic matter still remains.
Thus at time $t = 10$, we have:
Hence the result.
== Sources ==
* : Chapter $1$: Basic Concepts: Lesson $1$: How Differential Equations Originate
Category:Radiometric Dating
Formula for Spearman's Rank Correlation Coefficient

== Theorem ==
Let $S$ be a set of entities.
Let $\sequence {x_i}$ and $\sequence {y_i}$ be rankings of $S$ based on an arbitrary property of the elements of $S$.
Let there be no tied ranks in either $\sequence {x_i}$ or $\sequence {y_i}$.
The Spearman's rank correlation coefficient may be calculated using the formula:
:$r_S = 1 - \dfrac {6 T} {n \paren {n^2 - 1} }$
where $T$ denotes the sum of squares of the differences between the ranks for each of the pairs $\tuple {x_1, y_1}$
== Proof ==
== Sources ==
* 
* 
* 
Category:Examples of Spearman's Rank Correlation Coefficient
Formula for Total Variation of Continuously Differentiable Function

== Theorem ==
Let $a, b$ be real numbers with $a < b$.
Let $f : \closedint a b \to \R$ be a continuously differentiable function.
Let $\map {V_} {\closedint a b}$ be the total variation of $f$ on $\closedint a b$.
Then:
:$\ds V_f = \int_a^b \size {\map {f'} x} \rd x$
== Proof ==
For each finite subdivision $P$ of $\closedint a b$, write: 
:$P = \set {x_0, x_1, \ldots, x_n }$
with:
:$a = x_0 < x_1 < x_2 < \cdots < x_{n - 1} < x_n = b$
We first show that: 
:$\ds \map {V_f} {\closedint a b} \le \int_a^b \size {\map {f'} x} \rd x$
We then show that: 
:$\ds \int_a^b \size {\map {f'} x} \rd x \le \map {V_f} {\closedint a b}$
from which the claim follows.
From Differentiable Function is Continuous: 
:$f$ is continuous on $\closedint a b$. 
From Restriction of Continuous Mapping is Continuous:
:$f$ is continuous on $\closedint {x_i} {x_{i + 1} }$ for each $i$.
Since $f'$ is continuous, we can apply the Fundamental Theorem of Calculus to obtain:
:$\ds \map f {x_{i + 1} } - \map f {x_i} = \int_{x_i}^{x_{i + 1} } \map {f'} x \rd x$
Then:
We therefore have, for each finite subdivisions $P$:
From the definition of total variation, it follows that: 
:$\ds \map {V_f} {\closedint a b} \le \int_a^b \size {\map {f'} x} \rd x$
We now turn attention to proving:
:$\ds \int_a^b \size {\map {f'} x} \rd x \le V_f$
For each $i$, there exists $c_i \in \openint {x_i} {x_{i + 1} }$ such that: 
:$\ds \map f {x_{i + 1} } - \map f {x_i} = \map f {c_i} \paren {x_{i + 1} - x_i}$
by the Mean Value Theorem.
We then have: 
:$\ds \map L {\size {f'}, P} = \sum_{i \mathop = 0}^n \paren {\inf_{\closedint {x_i} {x_{i + 1} } } \size {f'} } \paren {x_{i + 1} - x_i}$
From the definition of infinum, we have: 
:$\ds \inf_{\closedint {x_i} {x_{i + 1} } } \size {f'} \le \size {\map {f'} {c_i} }$
for each $i$. 
Then: 
That is:
:$\ds \map L {\size {f'}, P} \le \map {V_f} {P ; \closedint a b}$
Taking the supremum over all finite subdivisions $P$ of $\closedint a b$, we have: 
:$\ds \map L {\size {f'} } \le \map {V_f} {\closedint a b}$
Note that $f$ is continuously differentiable, so:
:$f'$ is continuous.
From Absolute Value of Continuous Real Function is Continuous:
:$\size {f'}$ is continuous.
From Continuous Real Function is Darboux Integrable, we have: 
:$\ds \map L {\size {f'} } = \int_a^b \size {\map {f'} x} \rd x$
So we obtain: 
:$\ds \int_a^b \size {\map {f'} x} \rd x \le \map {V_f} {\closedint a b}$
Hence the result.
Category:Total Variation of Real Function
Formulation 1 Rank Axioms Implies Rank Function of Matroid

== Theorem ==
Let $S$ be a finite set.
Let $\rho : \powerset S \to \Z$ be a mapping from the power set of $S$ to the integers.
Let $\rho$ satisfy formulation 1 of the rank axioms:
Then $\rho$ is the rank function of a matroid on $S$.
=== Lemma 1 ===
=== Lemma 2 ===
=== Lemma 3 ===
== Proof 1==
== Proof 2==
Category:Matroid Theory
Category:Matroid Rank Functions
Category:Formulation 1 Rank Axioms Implies Rank Function of Matroid