avewright/proofwiki-math huggingface dataset:
Theorem: Dilation of Compact Set in Topological Vector Space is Compact

Let $k$ be a topological field.
Let $X$ be a topological vector space over $X$. 
Let $K$ be a compact subset of $X$. 
Let $t \in k \setminus \set {0_k}$. 
Then $t K$ is compact.

Proof:
Let $\family {U_\alpha : \alpha \in I}$ be open sets such that: 
:$\ds t K \subseteq \bigcup_{\alpha \mathop \in I} U_\alpha$
From Dilation of Union of Subsets of Vector Space, we have: 
:$\ds K \subseteq \bigcup_{\alpha \mathop \in I} \paren {t^{-1} U_\alpha}$ 
From Dilation of Open Set in Topological Vector Space is Open, we have that $t^{-1} U_\alpha$ is open.
Since $K$ is compact, there exists $t^{-1} U_1, t^{-1} U_2, \ldots, t^{-1} U_n$ such that: 
:$\ds K \subseteq \bigcup_{i \mathop = 1}^n \paren {t^{-1} U_i}$ 
Then, using Dilation of Union of Subsets of Vector Space again we have: 
:$\ds t K \subseteq \bigcup_{i \mathop = 1}^n U_i$ 
So every open cover of $t K$ has a finite subcover.
So $t K$ is compact.
{{qed}}
Theorem: Dilation of Compact Set in Topological Vector Space is Compact

Let $k$ be a topological field.
Let $X$ be a topological vector space over $X$. 
Let $K$ be a compact subset of $X$. 
Let $t \in k \setminus \set {0_k}$. 
Then $t K$ is compact.

Proof:
From Dilation Mapping on Topological Vector Space is Continuous, the mapping $c_t : X \to X$ defined by:
:$\map {c_t} x = t x$
for each $x \in X$ is continuous.
From Continuous Image of Compact Space is Compact:
:$\map {c_t} K = t K$ is compact.
{{qed}}
Theorem: Topological Dual Space of Hausdorff Locally Convex Space Separates Points

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \PP}$ be a Hausdorff locally convex space over $\GF$.
Let $X^\ast$ be the topological dual of $X$. 
Let $x \in X$. 
Then $X^\ast$ separates points.
That is, if $x, y \in X$ are such that: 
:$\map f x = \map f y$ for all $f \in X^\ast$
we have that $x = y$.

Proof:
Suppose $x \ne y$. 
It suffices to find $f \in X^\ast$ such that $\map f x \ne \map f y$. 
From Finite Topological Space is Compact, $\set {\mathbf 0_X}$ is compact. 
From Compact Subspace of Hausdorff Space is Closed, $\set {\mathbf 0_X}$ is closed.
Since $x \ne y$, we have: 
:$x - y \not \in X \setminus \set {\mathbf 0_X}$
From Existence of Non-Zero Continuous Linear Functional vanishing on Proper Closed Subspace of Locally Convex Space, there exists $f \in X^\ast$ such that: 
:$\map f {x - y} \ne 0$
That is: 
:$\map f x \ne \map f y$
{{qed}}
Category:Locally Convex Spaces
Category:Topological Dual Spaces
cfbdp306hcmjf3ycc5kxqcajxr3jj19
Theorem: Characterization of von Neumann-Boundedness in Hausdorff Locally Convex Space

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \PP}$ be a Hausdorff locally convex space over $\GF$.
Let $U \subseteq X$.
Then $U$ is von Neumann-bounded {{iff}}:
:for each $p \in \PP$ there exists $C_p > 0$ such that: 
::$\map p x < C_p$
:for each $x \in U$.

Proof:
For each $p \in \PP$, let: 
:$B_p = \set {y \in X : \map p y < 1}$
Note that by the definition of the standard topology, $B_p$ is an open neighborhood of $\mathbf 0_X$. 
Let $r > 0$. 
From {{SeminormAxiom|2}}, for $y \in X$ we have: 
:$\map p y < 1$ 
{{iff}}:
:$\map p {r y} < r$ 
So, we have: 
:$r B_p = \set {y \in X : \map p y < r}$
Theorem: Normed Vector Space is Hausdorff Locally Convex Space

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space.
Then $\struct {X, \norm {\, \cdot \,} }$ is a Hausdorff locally convex space.

Proof:
From Normed Vector Space is Locally Convex Space, $\struct {X, \norm {\, \cdot \,} }$ can be viewed as the locally convex space $\struct {X, \norm {\, \cdot \,} }$.
Now for $x \ne \mathbf 0_X$, we have: 
:$\norm x \ne 0$ 
from {{NormAxiomVector|1}}. 
So $\struct {X, \norm {\, \cdot \,} }$ is a Hausdorff locally convex space.
{{qed}}
Category:Locally Convex Spaces
Category:Normed Vector Spaces
34bwapj2ixayshnb475s1pjs64s2jm9
Theorem: Characterization of von Neumann-Boundedness in Normed Vector Space

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space.
Let $U \subseteq X$.
Then $U$ is von Neumann-bounded {{iff}} it is bounded as a subset of a normed vector space.

Proof:
From Normed Vector Space is Hausdorff Locally Convex Space, $\struct {X, \norm {\, \cdot \,} }$ can be viewed as the Hausdorff locally convex space $\struct {X, \norm {\, \cdot \,} }$. 
The result is then immediate from Characterization of von Neumann-Boundedness in Hausdorff Locally Convex Space.
{{qed}}
Category:Von Neumann-Bounded Subsets of Topological Vector Spaces
Category:Normed Vector Spaces
fwtjp4dgjgakjg8tu4ofdh15xpy4557
Theorem: Initial Topology on Normed Vector Space is Weak Topology

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be a normed vector space over $\GF$. 
Let $X^\ast$ be the normed dual space of $X$. 
Let $w$ be the initial topology on $X$ with respect to $X^\ast$.
Then $w$ is the weak topology on $X$.

Proof:
From Normed Dual Space Separates Points, if $x \ne y$ then there exists $f \in X^\ast$ such that $\map f x \ne \map f y$.
That is, if $x \ne \mathbf 0_X$, there exists $f \in X^\ast$ such that $\map f x \ne 0$.
{{qed}}
Category:Weak Topologies on Topological Vector Spaces
Category:Normed Vector Spaces
fs598imvc8zv7xhcr4kmkgcnsawapmy
Theorem: Weak Topology on Topological Vector Space over Hausdorff Topological Field is Hausdorff

Let $K$ be a Hausdorff topological field. 
Let $X$ be a topological vector space over $K$ with weak topology $w$.
Then $\struct {X, w}$ is Hausdorff.

Proof:
From the definition of the weak topology, if $x, y \in X$ have $x \ne y$, then $x - y \ne \mathbf 0_X$: 
:there exists $f \in X^\ast$ such that $\map f {x - y} \ne 0$. 
Since $f$ is linear, we then have $\map f x \ne \map f y$.
Since $K$ is Hausdorff, we therefore obtain that $\struct {X, w}$ is Hausdorff from Initial Topology with respect to Point-Separating Family of Mappings onto Hausdorff Spaces is Hausdorff.
{{qed}}
Category:Weak Topologies on Topological Vector Spaces
Category:Hausdorff Spaces
hp2x1ayu9z2nwfnpjclbek6lhi0xsws
Theorem: Equation of Wave with Constant Velocity

Let $\phi$ be a wave which is propagated along the $x$-axis in the positive direction with constant velocity $c$ and without change of shape.
Let $\paren {\map \phi x}_{t \mathop = 0} = \map f x$ be the '''wave profile''' of $\phi$.
Then the '''disturbance''' of $\phi$ at point $x$ and time $t$ can be expressed using the equation:
:$\map \phi {x, t} = \map f {x - c t}$
where:
:$x$ denotes the displacement from the origin along the $x$-axis
:$t$ denotes the time.

Proof:
Let us imagine a snapshot of $\phi$ at the time $t = 0$.
Then, {{hypothesis}}, the wave $\phi$ is described by the equation:
:$\phi = \map f x$
Also {{hypothesis}}, $\phi$ is propagated with no change of shape.
Hence, an imagined snapshot of $\phi$ at the general time $t$ will be:
:identical with that at $t = 0$
:moved along the $x$-axis a distance $s$.
By SUVAT:
:$s = c t$
in the positive direction along the $x$-axis.
Let us set the origin at the point $x = c t$.
Let the displacement measured from this new origin be $X$.
Then we have:
:$X = x + c t$
Hence the new equation for the wave profile of $\phi$ is:
:$\phi = \map f X$
But referred to that original fixed origin, this means:
:$\phi = \map f {x - c t}$
{{qed}}
Theorem: Equation of Wave with Constant Velocity/Corollary

Let $\phi$ be a wave which is propagated along the $x$-axis in the negative direction with constant velocity $c$ and without change of shape.
Let $\paren {\map \phi x}_{t \mathop = 0} = \map f x$ be the '''wave profile''' of $\phi$.
Then the '''disturbance''' of $\phi$ at point $x$ and time $t$ can be expressed using the equation:
:$\map \phi {x, t} = \map f {x + c t}$

Proof:
We have {{hypothesis}} that the velocity of $\phi$ in the negative direction is $c$.
Hence the velocity of $\phi$ in the positive direction is $-c$.
By Equation of Wave with Constant Velocity:
:$\phi = \map f {x - \paren {-c} t}$
Hence the result.
{{qed}}
Theorem: Characterization of Continuity of Linear Functional in Weak Topology

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a topological vector space over $\GF$ with weak topology $w$. 
Let $X^\ast$ be the topological dual space of $X$.
Let $f : X \to \GF$ be a linear functional.
Then $f$ is $w$-continuous {{iff}} $f \in X^\ast$. 
That is: 
:$\struct {X, w}^\ast = X^\ast$
{{explain|Better to introduce the $\struct {X, w}$ notation earlier in the page -- as it stands the reader is left wondering what it means}}

Proof:
This is precisely Continuity of Linear Functionals in Initial Topology on Vector Space Generated by Linear Functionals, taking $F = X^\ast$. 
{{qed}}
Category:Weak Topologies on Topological Vector Spaces
n7q6ziw6u8e8gpvaz2rzc2qfjlfaxeq
Theorem: Equivalence of Definitions of Weak Convergence on Topological Vector Space

Let $\GF \in \set {\R, \C}$. 
Let $X$ be a topological vector space over $\GF$. 
Let $X^\ast$ be the topological dual space of $X$.
Suppose that: 
:for each $x, y \in X$ with $x \ne y$, there exists $f \in X^\ast$ such that $\map f x \ne \map f y$. 
Let $\sequence {x_n}_{n \mathop \in \N}$ be a sequence in $X$. 
Let $x \in X$. 
{{TFAE|def = Weak Convergence (Topological Vector Space)|view = weak convergence on topological vector space}}

Proof:
=== Definition 1 implies Definition 2 ===
Suppose that $\sequence {x_n}_{n \mathop \in \N}$ converges in $\struct {X, w}$.
Let $f \in X^\ast$ and $\epsilon > 0$. 
We want to show that: 
:$\map f {x_n} \to \map f x$ in $\GF$. 
Let $\map {B_r} {\lambda, \GF}$ be the open ball in $\GF$ of radius $r$ and Centre $\lambda$.
From Characterization of Continuity of Linear Functional in Weak Topology, we have that $f$ is continuous in $\struct {X, w}$.
From the definition of the initial topology, we then have: 
:$f^{-1} \sqbrk {\map {B_r} {\map f x, \GF} }$ is weakly open for each $r > 0$ and $x \in X$.
So by the definition of convergence in $\struct {X, w}$, there exists $N \in \N$ such that: 
:$x_n \in f^{-1} \sqbrk {\map {B_r} {\map f x, \GF} }$ for $n \ge N$. 
Then: 
:$\map f {x_n} \in \map {B_r} {\map f x, \GF}$ for $n \ge N$
so that: 
:$\cmod {\map f {x_n} - \map f x} < \epsilon$
Since $\epsilon$ was arbitrary, we have: 
:$\map f {x_n} \to \map f x$ in $\GF$.
{{qed|lemma}}
Theorem: Wave Profile of Harmonic Wave

Let $\phi$ be a harmonic wave which is propagated along the $x$-axis in the positive direction with constant velocity $c$.
Then the '''wave profile''' of $\phi$ can be expressed as:
:$\paren {\map \phi x}_{t \mathop = 0} = a \cos \omega x$

Proof:
By definition, a '''harmonic wave''' is a wave whose wave profile can be expressed as a sine curve.
By definition, a sine curve can be expressed in the form:
:$\map \phi x = a \map \sin {\omega x + \epsilon}$
where $a$, $\omega$ and $\epsilon$ are arbitrary constants.
We select $\epsilon$ so as to set:
:$\epsilon = \dfrac \pi 2$
We then have:
{{begin-eqn}}
{{eqn | l = \map \phi x
      | r = a \map \sin {\omega x + \dfrac \pi 2}
      | c = 
}}
{{eqn | r = a \cos \omega x
      | c = 
}}
{{end-eqn}}
Hence at time $t = 0$ the equation expressing a wave in the form of a sine curve is:
:$\paren {\map \phi x}_{t \mathop = 0} = a \cos \omega x$
Hence the result by definition of wave profile.
{{qed}}
Theorem: Equation of Harmonic Wave

Let $\phi$ be a harmonic wave which is propagated along the $x$-axis in the positive direction with constant velocity $c$.
Then the '''disturbance''' of $\phi$ at point $x$ and time $t$ can be expressed using the equation:
:$\map \phi {x, t} = a \map \cos {\omega \paren {x - c t} }$

Proof:
From Wave Profile of Harmonic Wave:
:$\forall x \in \R: \paren {\map \phi x}_{t \mathop = 0} = a \cos \omega x$
From Equation of Wave with Constant Velocity:
:$\forall x, t \in \R: \map \phi {x, t} = a \map \cos {\omega \paren {x - c t} }$
Hence the result.
{{qed}}
Theorem: Wavelength of Harmonic Wave

Let $\phi$ be a harmonic wave expressed as:
:$\forall x, t \in \R: \map \phi {x, t} = a \map \cos {\omega \paren {x - c t} }$
The '''wavelength''' $\lambda$ of $\phi$ can be expressed as:
:$\lambda = \dfrac {2 \pi} \omega$

Proof:
By definition, $\lambda$ is the period of the wave profile of $\phi$.
From Wave Profile of Harmonic Wave, the wave profile of $\phi$ is given by:
:$\paren {\map \phi x}_{t \mathop = 0} = a \cos \omega x$
From Period of Real Cosine Function:
:$\paren {\map \phi x}_{t \mathop = 0} = a \cos {\omega x + 2 \pi}$
So the period of $\paren {\map \phi x}_{t \mathop = 0}$ is $\dfrac {2 \pi} \omega$.
Hence the result by definition of wavelength.
{{qed}}
Theorem: Period of Real Cosine Function

The period of the real cosine function is $2 \pi$.
That is, $2 \pi$ is the smallest value $L \in \R_{>0}$ such that:
:$\forall x \in \R: \cos x = \map \cos {x + L}$

Proof:
From Sine and Cosine are Periodic on Reals, we have that $\cos$ is a periodic real function.
Let $L$ be that period.
From Cosine of Angle plus Full Angle:
:$\map \cos {x + 2 \pi} = \cos x$
So $L = 2 \pi$ satisfies:
:$\forall x \in \R: \cos x = \map \cos {x + L}$
It remains to be shown that $2 \pi$ is the smallest such $L \in \R_{>0}$ with this property.
We have that:
{{begin-eqn}}
{{eqn | l = \cos \dfrac \pi 2
      | r = 0
      | c = Cosine of Right Angle
}}
{{eqn | l = \map \cos {\dfrac \pi 2 + \pi}
      | r = 0
      | c = Cosine of Three Right Angles
}}
{{eqn | l = \map \cos {\dfrac \pi 2 + 2 \pi}
      | r = 0
      | c = Cosine of Angle plus Full Angle
}}
{{end-eqn}}
and for no other $x \in \closedint 0 {2 \pi}$ is $\cos x = 0$.
Hence if there is another smaller $L \in \R_{>0}$ with the property that classifies it as the period of the real cosine function, it can only be $\pi$.
But then we note:
{{begin-eqn}}
{{eqn | l = \cos 0
      | r = 1
      | c = Cosine of Zero is One
}}
{{eqn | l = \map \cos {0 + \pi}
      | r = -1
      | c = Cosine of Straight Angle
}}
{{eqn | o = \ne
      | r = \cos 0
}}
{{end-eqn}}
Hence $\pi$ is not the period of the real cosine function.
Thus $2 \pi$ is the smallest value $L \in \R_{>0}$ such that:
:$\forall x \in \R: \cos x = \map \cos {x + L}$
and the result follows.
{{qed}}
Category:Cosine Function
Category:Periodic Functions
bgdcnizh0mrjz9hfhy6rfeimlnbcz74
Theorem: Period of Real Sine Function

The period of the real sine function is $2 \pi$.
That is, $2 \pi$ is the smallest value $L \in \R_{>0}$ such that:
:$\forall x \in \R: \sin x = \map \sin {x + L}$

Proof:
From Sine and Cosine are Periodic on Reals, we have that $\sin$ is a periodic real function.
Let $L$ be that period.
From Sine of Angle plus Full Angle:
:$\map \sin {x + 2 \pi} = \sin x$
So $L = 2 \pi$ satisfies:
:$\forall x \in \R: \sin x = \map \sin {x + L}$
It remains to be shown that $2 \pi$ is the smallest such $L \in \R_{>0}$ with this property.
We have that:
{{begin-eqn}}
{{eqn | l = \sin 0
      | r = 0
      | c = Sine of Zero is Zero
}}
{{eqn | l = \map \sin {0 + \pi}
      | r = 0
      | c = Sine of Straight Angle
}}
{{eqn | l = \cos \map \cos {0 + 2 \pi}
      | r = 0
      | c = Sine of Angle plus Full Angle
}}
{{end-eqn}}
and for no other $x \in \closedint 0 {2 \pi}$ is $\sin x = 0$.
Hence if there is another smaller $L \in \R_{>0}$ with the property that classifies it as the period of the real sine function, it can only be $\pi$.
But then we note:
{{begin-eqn}}
{{eqn | l = \sin \dfrac \pi 2
      | r = 1
      | c = Sine of Right Angle
}}
{{eqn | l = \map \sin {\dfrac \pi 2 + \pi}
      | r = -1
      | c = Sine of Three Right Angles
}}
{{eqn | o = \ne
      | r = \sin \dfrac \pi 2
}}
{{end-eqn}}
Hence $\pi$ is not the period of the real sine function.
Thus $2 \pi$ is the smallest value $L \in \R_{>0}$ such that:
:$\forall x \in \R: \sin x = \map \sin {x + L}$
and the result follows.
{{qed}}
Theorem: Period of Harmonic Wave

Let $\phi$ be a harmonic wave expressed as:
:$\forall x, t \in \R: \map \phi {x, t} = a \map \cos {\omega \paren {x - c t} }$
The '''period''' $\tau$ of $\phi$ can be expressed as:
:$\tau = \dfrac \lambda c$
where $\lambda$ is the wavelength of $\phi$.

Proof:
By definition, a harmonic wave is an instance of a periodic wave.
Hence Period of Periodic Wave can be used directly.
{{qed}}
Theorem: Period of Harmonic Wave

Let $\phi$ be a harmonic wave expressed as:
:$\forall x, t \in \R: \map \phi {x, t} = a \map \cos {\omega \paren {x - c t} }$
The '''period''' $\tau$ of $\phi$ can be expressed as:
:$\tau = \dfrac \lambda c$
where $\lambda$ is the wavelength of $\phi$.

Proof:
By definition, $\tau$ is the time taken for one complete wavelength of $\phi$ to pass an arbitrary point on the $x$-axis.
From Equation of Harmonic Wave, we have:
:$(1): \quad \map \phi {x, t} = a \map \cos {\omega \paren {x - c t} }$
From Wavelength of Harmonic Wave:
:$\lambda = \dfrac {2 \pi} \omega$
Hence:
:$\omega = \dfrac {2 \pi} \lambda$
and we can express $(1)$ in the form:
:$(2): \quad \map \phi {x, t} = a \map \cos {\dfrac {2 \pi} \lambda \paren {x - c t} }$
From $(2)$ it follows that $\dfrac {2 \pi} \lambda \paren {x - c t}$ must pass through a complete cycle of values as $t$ is increased by $\tau$.
Thus:
:$\dfrac {2 \pi c \tau} \lambda = 2 \pi$
and so:
:$\tau = \dfrac \lambda c$
Hence the result.
{{qed}}
Theorem: Frequency of Harmonic Wave

Let $\phi$ be a harmonic wave expressed as:
:$\forall x, t \in \R: \map \phi {x, t} = a \map \cos {\omega \paren {x - c t} }$
The '''frequency''' $\nu$ of $\phi$ can be expressed as:
:$\nu = \dfrac 1 \tau$
where $\tau$ is the period of $\phi$.

Proof:
By definition, a harmonic wave is an instance of a periodic wave.
Hence Frequency of Periodic Wave can be used directly.
{{qed}}
Theorem: Velocity of Harmonic Wave is Wavelength times Frequency

Let $\phi$ be a harmonic wave expressed as:
:$\forall x, t \in \R: \map \phi {x, t} = a \map \cos {\omega \paren {x - c t} }$
where $c$ is the velocity of $\phi$.
Then:
:$c = \nu \lambda$
where:
:$\nu$ is the frequency of $\phi$
:$\lambda$ is the wavelength of $\phi$.

Proof:
By definition, a harmonic wave is an instance of a periodic wave.
Hence Velocity of Periodic Wave is Wavelength times Frequency can be used directly.
Theorem: Equation of Harmonic Wave/Wavelength and Period

:$\map \phi {x, t} = a \map \cos {2 \pi \paren {\dfrac x \lambda - \dfrac t \tau} }$
where:
:$\lambda$ is the wavelength of $\phi$
:$\tau$ is the period of $\phi$.

Proof:
{{begin-eqn}}
{{eqn | l = \map \phi {x, t}
      | r = a \map \cos {\dfrac {2 \pi} \lambda \paren {x - c t} }
      | c = Equation of Harmonic Wave in terms of Wavelength and Velocity
}}
{{eqn | r = a \map \cos {\dfrac {2 \pi} \lambda \paren {x - \dfrac \lambda \tau t} }
      | c = Period of Harmonic Wave: $\tau = \dfrac \lambda c$
}}
{{eqn | r = a \map \cos {2 \pi \paren {\dfrac x \lambda - \dfrac t \tau} }
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Harmonic Wave/Wavelength and Frequency

:$\map \phi {x, t} = a \map \cos {2 \pi \paren {\dfrac x \lambda - \nu t} }$
where:
:$\lambda$ is the wavelength of $\phi$
:$\nu$ is the frequency of $\phi$.

Proof:
{{begin-eqn}}
{{eqn | l = \map \phi {x, t}
      | r = a \map \cos {2 \pi \paren {\dfrac x \lambda - \dfrac t \tau} }
      | c = Equation of Harmonic Wave in terms of Wavelength and Period: $\tau$ is the period of $\phi$
}}
{{eqn | r = a \map \cos {2 \pi \paren {\dfrac x \lambda - \dfrac 1 \tau t} }
      | c = rearranging
}}
{{eqn | r = a \map \cos {2 \pi \paren {\dfrac x \lambda - \nu t} }
      | c = Frequency of Harmonic Wave
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Harmonic Wave/Wavelength and Velocity

:$\map \phi {x, t} = a \map \cos {\dfrac {2 \pi} \lambda \paren {x - c t} }$
where $\lambda$ is the wavelength of $\phi$

Proof:
{{begin-eqn}}
{{eqn | l = \map \phi {x, t}
      | r = a \map \cos {\omega \paren {x - c t} }
      | c = Equation of Harmonic Wave
}}
{{eqn | r = a \map \cos {\dfrac {2 \pi} \lambda \paren {x - c t} }
      | c = Wavelength of Harmonic Wave: $\lambda = \dfrac {2 \pi} \omega$
}}
{{end-eqn}}
{{qed}}
Theorem: Wave Number of Harmonic Wave

Let $\phi$ be a harmonic wave expressed as:
:$\forall x, t \in \R: \map \phi {x, t} = a \map \cos {\omega \paren {x - c t} }$
The '''wave number''' $k$ of $\phi$ can be expressed as:
:$k = \dfrac 1 \lambda$
where $\lambda$ is the wavelength of $\phi$.

Proof:
By definition, a harmonic wave is an instance of a periodic wave.
Hence Wave Number of Periodic Wave can be used directly.
{{qed}}
Theorem: Wave Number of Harmonic Wave

Let $\phi$ be a harmonic wave expressed as:
:$\forall x, t \in \R: \map \phi {x, t} = a \map \cos {\omega \paren {x - c t} }$
The '''wave number''' $k$ of $\phi$ can be expressed as:
:$k = \dfrac 1 \lambda$
where $\lambda$ is the wavelength of $\phi$.

Proof:
By definition, $k$ is the number of complete wavelengths of $\phi$ per unit displacement along the $x$-axis.
By definition, $\lambda$ is the period of the wave profile of $\phi$.
So between two points at unit distance apart, there are $\dfrac 1 \lambda$ wavelengths of $\phi$.
The result follows by definition of wave number.
{{qed}}
Theorem: Equation of Harmonic Wave/Wave Number and Frequency

:$\map \phi {x, t} = a \map \cos {2 \pi \paren {k x - \nu t} }$
where:
:$k$ is the wave number of $\phi$
:$\nu$ is the frequency of $\phi$.

Proof:
{{begin-eqn}}
{{eqn | l = \map \phi {x, t}
      | r = a \map \cos {2 \pi \paren {\dfrac x \lambda - \nu t} }
      | c = Equation of Harmonic Wave in terms of Wavelength and Frequency: $\lambda$ is the wavelength of $\phi$
}}
{{eqn | r = a \map \cos {2 \pi \paren {\dfrac 1 \lambda x - \nu t} }
      | c = rearranging
}}
{{eqn | r = a \map \cos {2 \pi \paren {k x - \nu t} }
      | c = Wave Number of Harmonic Wave
}}
{{end-eqn}}
{{qed}}
Theorem: Period of Periodic Wave

Let $\phi$ be a periodic wave expressed as:
:$\forall x, t \in \R: \map \phi {x, t} = \map f {x - c t}$
The '''period''' $\tau$ of $\phi$ can be expressed as:
:$\tau = \dfrac \lambda c$
where $\lambda$ is the wavelength of $\phi$.

Proof:
By definition, $\tau$ is the time taken for one complete wavelength of $\phi$ to pass an arbitrary point on the $x$-axis.
We have:
:$\map \phi {x, t} = \map f {x - c t} = \map f {x - c t + \lambda}$
It follows that $x - c t$ must pass through a complete cycle of values as $t$ is increased by $\tau$.
Thus:
:$\lambda = c \tau$
and so:
:$\tau = \dfrac \lambda c$
Hence the result.
{{qed}}
Theorem: Frequency of Periodic Wave

Let $\phi$ be a periodic wave expressed as:
:$\forall x, t \in \R: \map \phi {x, t} = \map f {x - c t}$
The '''frequency''' $\nu$ of $\phi$ can be expressed as:
:$\nu = \dfrac 1 \tau$
where $\tau$ is the period of $\phi$.

Proof:
By definition, $\nu$ is the number of complete '''wavelengths''' of $\phi$ to pass an arbitrary point on the $x$-axis in unit time.
Let $x_0$ be that arbitrary point.
By definition, $\tau$ is the time taken for one complete wavelength of $\phi$ to pass $x_0$.
So after unit time, $\dfrac 1 \tau$ wavelengths of $\phi$ pass $x_0$.
Hence the result.
{{qed}}
Theorem: Velocity of Periodic Wave is Wavelength times Frequency

Let $\phi$ be a periodic wave expressed as:
:$\forall x, t \in \R: \map \phi {x, t} = \map f {x - c t}$
where $c$ is the velocity of $\phi$.
Then:
:$c = \nu \lambda$
where:
:$\nu$ is the frequency of $\phi$
:$\lambda$ is the wavelength of $\phi$.

Proof:
{{begin-eqn}}
{{eqn | l = \tau
      | r = \dfrac \lambda c
      | c = Period of Periodic Wave, where $\tau$ is the period of $\phi$
}}
{{eqn | ll= \leadsto
      | l = c
      | r = \dfrac 1 \tau \times \lambda
      | c = algebra
}}
{{eqn | r = \nu \lambda
      | c = Frequency of Periodic Wave
}}
{{end-eqn}}
{{qed}}
Theorem: Wave Number of Periodic Wave

Let $\phi$ be a periodic wave expressed as:
:$\forall x, t \in \R: \map \phi {x, t} = \map f {x - c t}$
The '''wave number''' $k$ of $\phi$ can be expressed as:
:$k = \dfrac 1 \lambda$
where $\lambda$ is the wavelength of $\phi$.

Proof:
By definition, $k$ is the number of complete wavelengths of $\phi$ per unit displacement along the $x$-axis.
By definition, $\lambda$ is the period of the wave profile of $\phi$.
So between two points at unit distance apart, there are $\dfrac 1 \lambda$ wavelengths of $\phi$.
The result follows by definition of wave number.
{{qed}}