avewright/proofwiki-math huggingface dataset:
Theorem: Conditions for Ordering in Ordered Group to be Directed

Let $\struct {G, \odot, \preccurlyeq}$ be an ordered group whose identity element is $e$.
Then:
:$\preccurlyeq$ is a directed ordering
{{iff}}:
:for every $x \in G$ there exist $y, z \in G$ such that $e \preccurlyeq y$, $e \preccurlyeq z$ and $x = y \odot z^{-1}$.

Proof:
=== Sufficient Condition ===
Let $\preccurlyeq$ be a directed ordering.
By definition of directed ordering:
:$\forall x, z \in G: \exists y \in G: x \preccurlyeq y$ and $z \preccurlyeq y$
Let $x \in G$ be arbitrary.
{{begin-eqn}}
{{eqn | q = \exists y \in G
      | l = x
      | o = \preccurlyeq
      | r = y
      | c = {{Defof|Directed Ordering}}
}}
{{eqn | lo= \land
      | l = e
      | o = \preccurlyeq
      | r = y
      | c = as it holds for all $z$, it definitely holds for $e$
}}
{{eqn | ll= \leadsto
      | l = x \odot y^{-1}
      | o = \preccurlyeq
      | r = y \odot y^{-1}
      | c = {{Defof|Relation Compatible with Operation}}
}}
{{eqn | lo= \land
      | l = e
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \odot y^{-1} \odot z
      | o = \preccurlyeq
      | r = e \odot z
      | c = 
}}
{{eqn | lo= \land
      | l = e
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {y \odot x^{-1} }^{-1} \odot z
      | o = \preccurlyeq
      | r = z
      | c = Inverse of Group Product
}}
{{eqn | lo= \land
      | l = e
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{end-eqn}}
Let $e = \paren {y \odot x^{-1}  }^{-1} \odot z$.
Then:
{{begin-eqn}}
{{eqn | l = z
      | r = y \odot x^{-1} 
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \odot z
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y \odot z^{-1}
      | c = 
}}
{{end-eqn}}
Then from:
{{begin-eqn}}
{{eqn | l = \paren {y \odot x^{-1} }^{-1} \odot z
      | o = \preccurlyeq
      | r = z
      | c = 
}}
{{eqn | lo= \land
      | l = e
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{end-eqn}}
we get:
{{begin-eqn}}
{{eqn | l = e
      | o = \preccurlyeq
      | r = z
      | c = {{Group-axiom|3}}
}}
{{eqn | lo= \land
      | l = e
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{end-eqn}}
and we see that:
:$\exists y, z \in G: e \preccurlyeq y, e \preccurlyeq z, x = y \odot z^{-1}$
{{qed}}
Theorem: Raw Moment of Log Normal Distribution

Let $X$ be a continuous random variable with the Log Normal distribution with $\mu \in \R, \sigma \in \R_{>0}$.
Let $n$ be a strictly positive integer. 
Then the $n$th raw moment $\expect {X^n}$ of $X$ is given by: 
:$\expect {X^n} = \exp {\paren {n\mu + \dfrac {\sigma^2 n^2} 2} }$

Proof:
From the definition of the Log Normal distribution, $X$ has probability density function:
:$\map {f_X} x = \dfrac 1 {\sigma \sqrt {2 \pi} x} \map \exp {-\dfrac {\paren {\map \ln x - \mu}^2} {2 \sigma^2} }$
where $\Img X = \R_{>0}$.
From the definition of the expected value of a continuous random variable: 
:$\ds \expect {X^n} = \int_0^\infty x^n \map {f_X} x \rd x$
Therefore:
{{begin-eqn}}
{{eqn	| l = \expect {X^n}
	    | r = \int_0^\infty x^n \dfrac 1 {\sigma \sqrt {2 \pi} x} \map \exp {-\dfrac {\paren {\map \ln x - \mu}^2} {2 \sigma^2} } \rd x
}}
{{eqn	| r = \dfrac 1 {\sigma \sqrt {2 \pi} } \int_0^\infty x^{n - 1} \map \exp {-\dfrac {\paren {\map \ln x - \mu}^2} {2 \sigma^2} } \rd x
	    | c = rewriting
}}
{{end-eqn}}
Let: 
:$u = \dfrac {\paren {\map \ln x - \mu}} {\sqrt 2 \sigma}$
Then by Chain Rule for Derivatives, we have:
:$\dfrac {\d u} {\d x} = \dfrac 1 {x \sqrt 2 \sigma}$
and also:
:$\exp {\paren {\sqrt 2 \sigma nu + n \mu} } = x^n$
We can see that:
:$u \to -\infty$ as $x \to 0$
and
:$u \to \infty$ as $x \to \infty$
Plugging these results back into our integral above, we have:
{{begin-eqn}}
{{eqn	| l = \expect {X^n}
	    | r = \dfrac {\exp {\paren {n \mu} } } {\sqrt \pi} \int_{-\infty}^\infty \exp {\paren {-u^2 + \sqrt 2 \sigma nu} } \rd u
}}
{{eqn	| r = \dfrac {\exp {\paren {n \mu} } } {\sqrt \pi} \int_{-\infty}^\infty \exp {\paren {-u^2 + \sqrt 2 \sigma nu - \dfrac {\sigma^2 n^2 } 2 + \dfrac {\sigma^2 n^2} 2} } \rd u
        | c = adding $0$
}}
{{eqn	| r = \dfrac {\exp {\paren {n \mu + \dfrac {\sigma^2 n^2} 2} } } {\sqrt \pi} \int_{-\infty}^\infty \exp {\paren {-u^2 + \sqrt 2 \sigma nu - \dfrac {\sigma^2 n^2} 2} } \rd u
        | c = Linear Combination of Definite Integrals
}}
{{eqn	| r = \dfrac {\exp {\paren {n \mu + \dfrac {\sigma^2 n^2} 2} } } {\sqrt \pi} \int_{-\infty}^\infty \exp {\paren {-\paren {u - \dfrac {\sqrt 2 \sigma n} 2}^2} } \rd u
        | c = Square of Sum
}}
{{eqn	| r = \dfrac {\exp {\paren {n \mu + \dfrac {\sigma^2 n^2} 2} } } {\sqrt \pi} \int_{-\infty}^\infty \exp {\paren {-y^2} } \rd y
        | c = setting $y = u - \dfrac {\sqrt 2 \sigma n} 2$ and hence $\d y = \d u$
}}
{{eqn	| r = \dfrac {\exp {\paren {n \mu + \dfrac {\sigma^2 n^2} 2} } } {\sqrt \pi} \sqrt \pi
        | c = Gaussian Integral
}}
{{eqn	| r = \exp {\paren {n \mu + \dfrac {\sigma^2 n^2} 2} }
        | c = 
}}
{{end-eqn}}
{{qed}}
Category:Log Normal Distribution
Category:Raw Moments
pfbrw6htxieybogb7rownl7vuh9kkij
Theorem: Expectation of Log Normal Distribution

Let $X$ be a continuous random variable with the Log Normal distribution with $\mu \in \R, \sigma \in \R_{> 0}$.
The expectation of $X$ is given by:
:$\expect X = \exp {\paren {\mu + \dfrac {\sigma^2 } 2 } }$

Proof:
From Raw Moment of Log Normal Distribution, we have:
The $n$th raw moment $\expect {X^n}$ of $X$ is given by: 
:$\expect {X^n} = \exp {\paren {n\mu + \dfrac {\sigma^2 n^2 } 2 } }$
Therefore, for $n = 1$ we have:
:$\expect X = \exp {\paren {\mu + \dfrac {\sigma^2 } 2 } }$
Hence the result.
{{qed}}
Category:Log Normal Distribution
Category:Expectation
hlnt0xza3utb6zyvm8stk9yq8enll2k
Theorem: Variance of Log Normal Distribution

Let $X$ be a continuous random variable with the Log Normal distribution with $\mu \in \R, \sigma \in \R_{> 0}$.
Then the variance of $X$ is given by: 
:$\var X = \map \exp {2 \mu + \sigma^2} \paren {\map \exp {\sigma^2} - 1}$

Proof:
By Variance as Expectation of Square minus Square of Expectation:
:$\var X = \expect {X^2} - \paren {\expect X}^2$
By Expectation of Log Normal Distribution:
:$\expect X = \map \exp {\mu + \dfrac {\sigma^2} 2}$
From Raw Moment of Log Normal Distribution:
The $n$th raw moment $\expect {X^n}$ of $X$ is given by: 
:$\expect {X^n} = \map \exp {n \mu + \dfrac {\sigma^2 n^2} 2}$
Therefore, for $n = 2$ we have:
:$\expect {X^2} = \map \exp {2 \mu + 2 \sigma^2}$
So:
{{begin-eqn}}
{{eqn | l = \var X
      | r = \map \exp {2 \mu + 2 \sigma^2} - \paren {\map \exp {\mu + \dfrac {\sigma^2} 2} }^2
}}
{{eqn | r = \map \exp {2 \mu + 2 \sigma^2} - \map \exp {2 \mu + \sigma^2}
      | c = Power of Power
}}
{{eqn | r = \map \exp {2 \mu + \sigma^2} \paren {\map \exp {\sigma^2} - 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Variance
Category:Log Normal Distribution
6sgzbeo2p362zowaizcs5e9ckud26i2
Theorem: Composition of Dirac Delta Distribution with Function with Simple Zero

Let $\delta \in \map {\DD'} \R$ be the Dirac delta distribution.
Let $\sequence {\map {\delta_n} x}_{n \mathop \in \N}$ be a delta sequence.
Let $f : \R \to \R$ be a real function with a simple zero at $x_0$.
Let $f$ be strictly monotone.
Let $\phi \in \map \DD \R$ be a test function.
Then in the distributional sense it holds that:
:$\map \delta {\map f x} = \dfrac {\map \delta {x - x_0} } {\size {\map {f'} {x_0} } }$
which can be interpreted as:
:$\ds \int_{-\infty}^\infty \map \delta {\map f x} \map \phi x \rd x = \dfrac {\map \phi {x_0} } {\size {\map {f'} {x_0} } }$
which more strictly means that:
:$\ds \lim_{n \mathop \to \infty} \int_{-\infty}^\infty \map {\delta_n} {\map f x} \map \phi x \rd x = \dfrac {\map \phi {x_0} } {\size {\map {f'} {x_0} } }$

Proof:
Suppose $\map {f'} {x_0} > 0$.
Then:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \int_{-\infty}^{\infty} \map {\delta_n} {\map f x} \map \phi x \rd x
      | r = \lim_{n \mathop \to \infty} \int_{-\infty}^{\infty} \map {\delta_n} y \frac {\map \phi {\map x y} } {\map {f'} {\map x y} } \rd y
      | c = Derivative of Inverse Function, Integration by Substitution, $y = \map f x$
}}
{{eqn | r = \frac {\map \phi {x_0} }{\map {f'} {x_0} }
      | c = {{Defof|Delta Sequence}}, $\map x 0 = x_0$
}}
{{eqn | r = \lim_{n \mathop \to \infty} \int_{-\infty}^\infty \frac {\map \phi x \map {\delta_n} {x - x_0} } {\map {f'} {x_0} } \rd x
}}
{{end-eqn}}
Suppose $\map {f'} {x_0} < 0$.
Then:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \int_{-\infty}^{\infty} \map {\delta_n} {\map f x} \map \phi x \rd x
      | r = \lim_{n \mathop \to \infty} \int_{\infty}^{-\infty} \map {\delta_n} y \frac {\map \phi {\map x y} } {\map {f'} {\map x y} } \rd y
      | c = Derivative of Inverse Function, Integration by Substitution, $y = \map f x$
}}
{{eqn | r = \lim_{n \mathop \to \infty} \int_{-\infty}^{\infty} \map {\delta_n} y \frac {\map \phi {\map x y} } {-\map {f'} {\map x y} } \rd y
}}
{{eqn | r = \frac {\map \phi {x_0} }{- \map {f'} {x_0} }
      | c = {{Defof|Delta Sequence}}, $\map x 0 = x_0$
}}
{{eqn | r = \lim_{n \mathop \to \infty} \int_{-\infty}^\infty \frac {\map \phi x \map {\delta_n} {x - x_0} } {-\map {f'} {x_0} } \rd x
}}
{{end-eqn}}
Altogether:
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \int_{-\infty}^{\infty} \map {\delta_n} {\map f x} \map \phi x \rd x
      | r = \frac {\map \phi {x_0} } {\size { \map {f'} {x_0} } }
      | c = {{Defof|Delta Sequence}}, $\map x 0 = x_0$
}}
{{eqn | r = \lim_{n \mathop \to \infty} \int_{-\infty}^\infty \frac {\map \phi x \map {\delta_n} {x - x_0} } {\size {\map {f'} {x_0 } } } \rd x
}}
{{end-eqn}}
{{Research|Theorem conditions here are stronger than usually found in literature to keep us on the safe side. The situtation may change as we learn more.}}
{{qed}}
Theorem: D'Ocagne's Identity

:$\forall m, n \in \Z: \paren {-1}^n F_{m - n} = F_m F_{n + 1} - F_n F_{n - 1}$

Proof:
{{begin-eqn}}
{{eqn | q = 
      | l = \paren {-1}^n F_i F_j
      | r = F_{n + i} F_{n + j} - F_n F_{n + i + j}
      | c = Vajda's Identity
}}
{{eqn | ll= \leadsto
      | l = \paren {-1}^n F_{m - n} F_1
      | r = F_{n + \paren {m - n} } F_{n + 1} - F_n F_{n + \paren {m - n} + 1}
      | c = setting $i \gets m - n$ and $j \gets 1$
}}
{{eqn | ll= \leadsto
      | l = \paren {-1}^n F_{m - n}
      | r = F_m F_{n + 1} - F_n F_{m + 1}
      | c = {{Defof|Fibonacci Numbers}}: $F_1 = 1$
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Philbert Maurice d'Ocagne|cat = d'Ocagne}}
Category:Fibonacci Numbers
0ypprivv60sgztw3nr1jxc4ra8sa7vg
Theorem: Dipper Relation is Equivalence Relation

Let $m \in \N$ be a natural number.
Let $n \in \N_{>0}$ be a non-zero natural number.
Let $\RR_{m, n}$ be the dipper relation on $\N$:
:$\forall x, y \in \N: x \mathrel {\RR_{m, n} } y \iff \begin {cases} x = y \\ m \le x < y \text { and } n \divides \paren {y - x} \\  m \le y < x \text { and } n \divides \paren {x - y} \end {cases}$
Then $\RR_{m, n}$ is an equivalence relation.

Proof:
First let it be noted that $\RR_{m, n}$ can be written as:
:$\forall x, y \in \N: x \mathrel {\RR_{m, n} } y \iff \begin {cases} x = y \\ m \le x, y \text { and } n \divides \size {x - y} \end {cases}$
where $\size {x - y}$ denotes the absolute value of $x - y$.
Checking in turn each of the criteria for equivalence:
Theorem: Dipper Relation is Congruence for Addition

Let $m \in \N$ be a natural number.
Let $n \in \N_{>0}$ be a non-zero natural number.
Let $\RR_{m, n}$ be the dipper relation on $\N$:
:$\forall x, y \in \N: x \mathrel {\RR_{m, n} } y \iff \begin {cases} x = y \\ m \le x < y \text { and } n \divides \paren {y - x} \\  m \le y < x \text { and } n \divides \paren {x - y} \end {cases}$
Then $\RR_{m, n}$ is a congruence relation for addition.

Proof:
From Dipper Relation is Equivalence Relation we have that $\RR_{m, n}$ is an equivalence relation.
From Equivalence Relation is Congruence iff Compatible with Operation, it is sufficient to show that:
:$\forall x, y, z \in \N: x \mathrel {\RR_{m, n} } y \implies \paren {x + z} \mathrel {\RR_{m, n} } \paren {y + z}$
and:
:$\forall x, y, z \in \N: x \mathrel {\RR_{m, n} } y \implies \paren {z + x} \mathrel {\RR_{m, n} } \paren {z + y}$
Furthermore, because Natural Number Addition is Commutative, it is sufficient to demonstrate the first of these only.
So, let $x, y \in \N$ be such that:
:$x \mathrel {\RR_{m, n} } y$
First let $x = y$.
We have that:
:$x = y \implies x + z = y + z$
and so:
:$\paren {x + z} \mathrel {\RR_{m, n} } \paren {y + z}$
Otherwise, we have that:
:$x \ne y$ and $x, y \ge m$
{{WLOG}}, let $x < y$.
If not, then as $\RR_{m, n}$ is symmetric we can rename $x$ and $y$ as necessary.
{{begin-eqn}}
{{eqn | l = x
      | o = \RR_{m, n}
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \divides
      | r = \paren {y - x}
      | c = Definition of $\RR_{m, n}$
}}
{{eqn | ll= \leadsto
      | q = \exists k \in \N_{>0}
      | l = k n
      | r = \paren {y - x}
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | ll= \leadsto
      | l = k n
      | r = \paren {y + z - x - z}
      | c = as $\paren {y + z - x - z} = y - x$
}}
{{eqn | r = \paren {\paren {y + z} - \paren {x + z} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \divides
      | r = \paren {\paren {y + z} - \paren {x + z} }
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | l = \paren {x + z}
      | o = \RR_{m, n}
      | r = \paren {y + z}
      | c = Definition of $\RR_{m, n}$, as both $x + z \ge m$ and $y + z \ge m$
}}
{{end-eqn}}
{{qed}}
Theorem: Dipper Relation is Congruence for Multiplication

Let $m \in \N$ be a natural number.
Let $n \in \N_{>0}$ be a non-zero natural number.
Let $\RR_{m, n}$ be the dipper relation on $\N$:
:$\forall x, y \in \N: x \mathrel {\RR_{m, n} } y \iff \begin {cases} x = y \\ m \le x < y \text { and } n \divides \paren {y - x} \\  m \le y < x \text { and } n \divides \paren {x - y} \end {cases}$
Then $\RR_{m, n}$ is a congruence relation for multiplication.

Proof:
From Dipper Relation is Equivalence Relation we have that $\RR_{m, n}$ is an equivalence relation.
From Equivalence Relation is Congruence iff Compatible with Operation, it is sufficient to show that:
:$\forall x, y, z \in \N: x \mathrel {\RR_{m, n} } y \implies \paren {x z} \mathrel {\RR_{m, n} } \paren {y z}$
and:
:$\forall x, y, z \in \N: x \mathrel {\RR_{m, n} } y \implies \paren {z x} \mathrel {\RR_{m, n} } \paren {z y}$
Furthermore, because Natural Number Addition is Commutative, it is sufficient to demonstrate the first of these only.
First let $x = y$.
We have that:
:$x = y \implies x z = y z$
and so:
:$\paren {x z} \mathrel {\RR_{m, n} } \paren {y z}$
Otherwise, we have that:
:$x \ne y$ and $x, y \ge m$
{{WLOG}}, let $x < y$.
If not, then as $\RR_{m, n}$ is symmetric we can rename $x$ and $y$ as necessary.
First note that if $z = 0$, then:
:$\paren {x z} = \paren {y z}=  0$
and so:
:$\paren {x z} \mathrel {\RR_{m, n} } \paren {y z}$
Otherwise we have that $z \ge 1$ and so both $x z \ge m$ and $y  z \ge m$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \RR_{m, n}
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \divides
      | r = \paren {y - x}
      | c = Definition of $\RR_{m, n}$
}}
{{eqn | ll= \leadsto
      | q = \exists k \in \N_{>0}
      | l = k n
      | r = \paren {y - x}
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | ll= \leadsto
      | q = \exists k \in \N_{>0}
      | l = k z n
      | r = \paren {y z - x z}
      | c = as $z \in \N_{>0}$
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \divides
      | r = \paren {y z - x z}
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | l = \paren {x z}
      | o = \RR_{m, n}
      | r = \paren {y z}
      | c = Definition of $\RR_{m, n}$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Restricted Dipper Relation is Equivalence Relation

Let $m, n \in \N_{>0}$ be non-zero natural numbers.
Let $\RR^*_{m, n}$ be the restricted dipper relation on $\N$:
:$\forall x, y \in \N_{>0}: x \mathrel {\RR^*_{m, n} } y \iff \begin {cases} x = y \\ m \le x < y \text { and } n \divides \paren {y - x} \\  m \le y < x \text { and } n \divides \paren {x - y} \end {cases}$
Then $\RR^*_{m, n}$ is an equivalence relation.

Proof:
By definition, $\RR^*_{m, n}$ is the restriction of the dipper relation $\RR_{m, n}$ to $\N_{>0}$.
We have from Dipper Relation is Equivalence Relation that $\RR_{m, n}$ is an equivalence relation.
The result follows from Restriction of Equivalence Relation is Equivalence.
{{qed}}
Theorem: Restricted Dipper Relation is Congruence for Multiplication

Let $m, n \in \N_{>0}$ be non-zero natural numbers.
Let $\RR^*_{m, n}$ be the restricted dipper relation on $\N$:
:$\forall x, y \in \N_{>0}: x \mathrel {\RR^*_{m, n} } y \iff \begin {cases} x = y \\ m \le x < y \text { and } n \divides \paren {y - x} \\  m \le y < x \text { and } n \divides \paren {x - y} \end {cases}$
Then $\RR^*_{m, n}$ is a congruence relation for multiplication.

Proof:
By definition, $\RR^*_{m, n}$ is the restriction of the dipper relation $\RR_{m, n}$ to $\N_{>0}$.
We have from Dipper Relation is Congruence for Multiplication that $\RR_{m, n}$ is a congruence relation for multiplication.
The result follows from Restriction of Congruence Relation is Congruence.
{{qed}}
Theorem: Dipper Operation is Closed on Initial Segment

Let $m \in \N$ be a natural number.
Let $n \in \N_{>0}$ be a non-zero natural number.
Let $\N_{< \paren {m \mathop + n} }$ denote the initial segment of the natural numbers:
:$\N_{< \paren {m \mathop + n} } := \set {0, 1, \ldots, m + n - 1}$
Let $+_{m, n}$ denote the '''dipper operation''' on $\N_{< \paren {m \mathop + n} }$:
:$\forall a, b \in \N_{< \paren {m \mathop + n} }: a +_{m, n} b = \begin{cases} a + b & : a + b < m \\ a + b - k n & : a + b \ge m \end{cases}$
where $k$ is the largest integer satisfying:
:$m + k n \le a + b$
Then $+_{m, n}$ is closed on $\N_{< \paren {m \mathop + n} }$.

Proof:
Let $a + b < m$.
Then:
:$0 \le a +_{m, n} b < m$
and so:
:$a +_{m, n} b \in \N_{< \paren {m \mathop + n} }$
Let $a + b > m$.
Then:
:$a +_{m, n} b = a + b - k n$
where $k$ is the largest such that $m + k n < a + b$
Hence:
{{begin-eqn}}
{{eqn | q = 
      | l = m + k n
      | o = \le
      | m = a + b
      | mo= <
      | r = m + \paren {k + 1} n
      | c = Definition of $k$
}}
{{eqn | ll= \leadsto
      | l = m
      | o = \le
      | m = a + b - k n
      | mo= <
      | r = m + n
      | c = subtracting $k n$ from all parts
}}
{{eqn | ll= \leadsto
      | l = m
      | o = \le
      | m = a +_{m, n} b
      | mo= <
      | r = m + n
      | c = Definition of $+_{m, n}$
}}
{{end-eqn}}
That is:
:$a +_{m, n} b \in \N_{< \paren {m \mathop + n} }$
That is, $+_{m, n}$ is closed on $\N_{< \paren {m \mathop + n} }$.
{{qed}}
Category:Dipper Operations
Category:Algebraic Closure
6ru53m97mwaprifkl2cft2tee5rcnnb
Theorem: Restriction of Dipper Operation to Non-Zero Initial Segment is Closed

Let $m, n \in \N_{>0}$ be non-zero natural numbers.
Let $\N_{< \paren {m \mathop + n} }$ denote the initial segment of the natural numbers:
:$\N_{< \paren {m \mathop + n} } := \set {0, 1, \ldots, m + n - 1}$
Let $+_{m, n}$ denote the '''dipper operation''' on $\N_{< \paren {m \mathop + n} }$:
:$\forall a, b \in \N_{< \paren {m \mathop + n} }: a +_{m, n} b = \begin{cases} a + b & : a + b < m \\ a + b - k n & : a + b \ge m \end{cases}$
where $k$ is the largest integer satisfying:
:$m + k n \le a + b$
Let $\N^*_{< \paren {m \mathop + n} }$ denote the set defined as $\N_{< \paren {m \mathop + n} } \setminus \set 0$:
:$\N^*_{< \paren {m \mathop + n} } := \set {1, 2, \ldots, m + n - 1}$
Then $+_{m, n}$ is closed on $\N^*_{< \paren {m \mathop + n} }$.

Proof:
From Dipper Operation is Closed on Initial Segment, $+_{m, n}$ is closed on $\N_{< \paren {m \mathop + n} }$.
That is:
:$\forall a, b \in \N_{< \paren {m \mathop + n} }: a +_{m, n} b < m + n$
It remains to be shown that:
:$\forall a, b \in \N^*_{< \paren {m \mathop + n} }: a +_{m, n} b > 0$
Let $a + b < m$.
Then as $a > 0$ and $b > 0$ it follows that $a + b < 0$.
That is:
:$a +_{m, n} b > 0$
Let $a + b > m$.
Then:
:$a +_{m, n} b = a + b - k n$
where $k$ is the largest integer satisfying $m + k n \le a + b$.
That is:
:$m < a + b - k n$
But as $m > 0$ we must have that:
:$0 < a +_{m, n} b$
and the result follows.
{{qed}}
Theorem: Equivalence Classes of Dipper Relation

Let $m \in \N$ be a natural number.
Let $n \in \N_{>0}$ be a non-zero natural number.
Let $\RR_{m, n}$ be the dipper relation on $\N$:
:$\forall x, y \in \N: x \mathrel {\RR_{m, n} } y \iff \begin {cases} x = y \\ m \le x < y \text { and } n \divides \paren {y - x} \\  m \le y < x \text { and } n \divides \paren {x - y} \end {cases}$
The equivalence classes of $\RR_{m, n}$ are:
:$\eqclass x {\RR_{m, n} } = \begin {cases} \set x & : x < m \\ \set {y \in \N: \paren {m \le y} \land \paren {\exists k \in \Z: x = y + k n} } & : x \ge m \end {cases}$

Proof:
From Dipper Relation is Equivalence Relation we have that $\RR_{m, n}$ is indeed an equivalence relation.
Let $x < m$.
Then by definition:
:$y \in \eqclass x {\RR_{m, n} } \iff x = y$
and so:
:$\eqclass x {\RR_{m, n} } = \set x$
Let $m \le x$.
Let $x \mathrel {\RR_{m, n} } y$.
First we note that $m \le y$.
Let $x = y$.
Then $y \in \eqclass x {\RR_{m, n} }$ immediately, and:
:$x = y + 0 \times n$
That is:
:$\exists k \in \Z: x = y + k n$
where in this instance $k = 0$.
Let $x > y$.
We have that:
{{begin-eqn}}
{{eqn | l = n
      | o = \divides
      | r = \paren {x - y}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists k \in \Z
      | l = k n
      | r = x - y
      | c = 
}}
{{eqn | l = x
      | r = y + k n
      | c = 
}}
{{end-eqn}}
Let $x < y$.
We have that:
{{begin-eqn}}
{{eqn | l = n
      | o = \divides
      | r = \paren {y - x}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists k' \in \Z
      | l = k' n
      | r = y - x
      | c = 
}}
{{eqn | l = x
      | r = y - k' n
      | c = 
}}
{{eqn | l = x
      | r = y + k n
      | c = where $k = -k'$
}}
{{end-eqn}}
Hence when $m \le x$, we have that:
:$\eqclass x {\RR_{m, n} } = \set {y \in \N: \paren {m \le y} \land \paren {\exists k \in \Z: x = y + k n} }$
{{qed}}
Category:Dipper Relations
Category:Examples of Equivalence Classes
lbdrlsv15z7q0cno95bvqjumdxd1khs
Theorem: Restricted Dipper Operation is Associative

Let $m, n \in \N_{>0}$ be non-zero natural numbers.
Let $\N_{< \paren {m \mathop + n} }$ denote the initial segment of the natural numbers:
:$\N_{< \paren {m \mathop + n} } := \set {0, 1, \ldots, m + n - 1}$
Let $\N^*_{< \paren {m \mathop + n} }$ denote the set defined as $\N_{< \paren {m \mathop + n} } \setminus \set 0$:
:$\N^*_{< \paren {m \mathop + n} } := \set {1, 2, \ldots, m + n - 1}$
The '''restricted dipper operation''' $+^*_{m, n}$ on $\N^*_{< \paren {m \mathop + n} }$ is associative.

Proof:
By definition, $+^*_{m, n}$ is the restriction of the dipper relation $+_{m, n}$ to $\N_{>0}$.
We have from Dipper Operation is Associative that $+_{m, n}$ is an associative operation.
The result follows from Restriction of Associative Operation is Associative.
{{qed}}
Theorem: Restricted Dipper Operation is Commutative

Let $m, n \in \N_{>0}$ be non-zero natural numbers.
Let $\N_{< \paren {m \mathop + n} }$ denote the initial segment of the natural numbers:
:$\N_{< \paren {m \mathop + n} } := \set {0, 1, \ldots, m + n - 1}$
Let $\N^*_{< \paren {m \mathop + n} }$ denote the set defined as $\N_{< \paren {m \mathop + n} } \setminus \set 0$:
:$\N^*_{< \paren {m \mathop + n} } := \set {1, 2, \ldots, m + n - 1}$
The '''restricted dipper operation''' $+^*_{m, n}$ on $\N^*_{< \paren {m \mathop + n} }$ is commutative.

Proof:
By definition, $+^*_{m, n}$ is the restriction of the dipper relation $+_{m, n}$ to $\N_{>0}$.
We have from Dipper Operation is Associative that $+_{m, n}$ is a commutative operation.
The result follows from Restriction of Commutative Operation is Commutative.
{{qed}}