avewright/proofwiki-math huggingface dataset:
Theorem: Continuous Lattice and Way Below implies Preceding implies Preceding

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a continuous complete lattice.
Let $a, b \in S$.
Let:
:$\forall c \in S: c \ll a \implies c \preceq b$
Then $a \preceq b$

Proof:
By definition of way below closure:
:$\forall c \in a^\ll: c \preceq b$
By definition:
:$b$ is an upper bound for $a^\ll$
By definition of supremum:
:$\map \sup {a^\ll} \preceq b$
By definition of continuous:
:$L$ satisfies the axiom of approximation.
Thus by the axiom of approximation:
:$a = \map \sup {a^\ll} \preceq b$
{{qed}}
Theorem: Sum over k of Floor of Log base b of k

Let $n \in \Z_{> 0}$ be a strictly positive integer.
Let $b \in \Z$ such that $b \ge 2$.
Then:
:$\ds \sum_{k \mathop = 1}^n \floor {\log_b k} = \paren {n + 1} \floor {\log_b n} - \dfrac {b^{\floor {\log_b n} + 1} - b} {b - 1}$

Proof:
From Sum of Sequence as Summation of Difference of Adjacent Terms:
:$(1): \quad \ds \sum_{k \mathop = 1}^n \floor {\log_b k} = n \floor {\log_b n} - \sum_{k \mathop = 1}^{n - 1} k \paren {\floor {\map {\log_b} {k + 1} } - \floor {\log_b k} }$
Let $S$ be defined as:
:$\ds S := \sum_{k \mathop = 1}^{n - 1} k \paren {\floor {\map {\log_b} {k + 1} } - \floor {\log_b k} }$
As $b \ge 2$, we have that:
:$\map {\log_b} {k + 1} - \log_b k < 1$
As $b$ is an integer:
:$\lfloor {\map {\log_b} {k + 1} } - \floor {\log_b k} = 1$
{{iff}} $k + 1$ is a power of $b$.
So:
{{begin-eqn}}
{{eqn | l = S
      | r = \sum_{k \mathop = 1}^{n - 1} k \sqbrk {k + 1 \text{ is a power of } b}
      | c = where $\sqbrk {\, \cdot \,}$ is Iverson's convention
}}
{{eqn | r = \sum_{1 \mathop \le t \mathop \le \log_b n} \paren {b^t - 1}
      | c = 
}}
{{eqn | r = \sum_{t \mathop = 1}^{\floor {\log_b n} } \paren {b^t - 1}
      | c = 
}}
{{eqn | r = \sum_{t \mathop = 1}^{\floor {\log_b n} } b^t - \sum_{t \mathop = 1}^{\floor {\log_b n} } 1
      | c = 
}}
{{eqn | r = \sum_{t \mathop = 1}^{\floor {\log_b n} } b^t - \floor {\log_b n}
      | c = 
}}
{{eqn | r = b \sum_{t \mathop = 0}^{\floor {\log_b n} - 1} b^t - \floor {\log_b n}
      | c = extracting $b$ as a factor
}}
{{eqn | r = b \frac {b^{\floor {\log_b n} } - 1} {b - 1} - \floor {\log_b n}
      | c = Sum of Geometric Progression
}}
{{eqn | r = \frac {b^{\floor {\log_b n} + 1} - b} {b - 1} - \floor {\log_b n}
      | c = 
}}
{{end-eqn}}
The result follows by substituting $S$ back into $(1)$ and factoring out $\floor {\log_b n}$.
{{qed}}
Theorem: Sum over k of Floor of Root k

Let $n \in \Z_{> 0}$ be a strictly positive integer.
Let $b \in \Z$ such that $b \ge 2$.
Then:
:$\ds \sum_{k \mathop = 1}^n \floor {\sqrt k} = \floor {\sqrt n} \paren {n - \dfrac {\paren {2 \floor {\sqrt n} + 5} \paren {\floor {\sqrt n} - 1} } 6}$

Proof:
From Sum of Sequence as Summation of Difference of Adjacent Terms:
:$\ds \sum_{k \mathop = 1}^n \floor {\sqrt k} = n \floor {\sqrt n} - \sum_{k \mathop = 1}^{n - 1} k \paren {\floor {\sqrt {k + 1} } - \floor {\sqrt k} }$
Let $S$ be defined as:
:$\ds S := \sum_{k \mathop = 1}^{n - 1} k \paren {\floor {\sqrt {k + 1} } - \floor {\sqrt k} }$
We have that:
:$\sqrt {k + 1} - \sqrt k < 1$
and so:
:$\floor {\sqrt {k + 1} } - \floor {\sqrt k} = 1$
{{iff}} $k + 1$ is a square number.
So:
{{begin-eqn}}
{{eqn | l = S
      | r = \sum_{k \mathop = 1}^{n - 1} k \sqbrk {\text {$k + 1$ is a square number} }
      | c = 
}}
{{eqn | l = S
      | r = \sum_{k \mathop = 2}^n (k - 1) \sqbrk {\text {$k$ is a square number} }
      | c = 
}}
{{eqn | r = \sum_{t \mathop = 2}^{\floor {\sqrt n} } \paren {t^2 - 1}
      | c = $1$ is not included in this summation
}}
{{eqn | r = \sum_{t \mathop = 1}^{\floor {\sqrt n} } t^2 - 1 - \sum_{t \mathop = 2}^{\floor {\sqrt n} } 1
      | c = 
}}
{{eqn | r = \sum_{t \mathop = 1}^{\floor {\sqrt n} } t^2 - \sum_{t \mathop = 1}^{\floor {\sqrt n} } 1
      | c = 
}}
{{eqn | r = \frac {\floor {\sqrt n} \paren {\floor {\sqrt n} + 1} \paren {2 \floor {\sqrt n} + 1} } 6 - \floor {\sqrt n}
      | c = Sum of Sequence of Squares 
}}
{{eqn | r = \frac {\floor {\sqrt n} \paren {\floor {\sqrt n} + 1} \paren {2 \floor {\sqrt n} + 1} - 6 \floor {\sqrt n} } 6
      | c = 
}}
{{eqn | r = \floor {\sqrt n} \frac {\paren {\floor {\sqrt n} + 1} \paren {2 \floor {\sqrt n} + 1} - 6} 6
      | c = 
}}
{{eqn | r = \floor {\sqrt n} \frac {2 \floor {\sqrt n}^2 + 3 \floor {\sqrt n} - 5} 6
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^n \floor {\sqrt k}
      | r = n \floor {\sqrt n} - \floor {\sqrt n} \frac {\paren {2 \floor {\sqrt n} + 5} \paren {\floor {\sqrt n} - 1} } 6
      | c = 
}}
{{eqn | r = \floor {\sqrt n} \paren {n - \dfrac {\paren {2 \floor {\sqrt n} + 5} \paren {\floor {\sqrt n} - 1} } 6}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Top is Meet Irreducible

Let $\left({S, \wedge, \preceq}\right)$ be a bounded above meet semilattice.
Then $\top$ is meet irreducible
where $\top$ denotes the greatest element in $S$.

Proof:
Let $x, y \in S$ such that
:$\top = x \wedge y$
By Meet Precedes Operands
:$\top \preceq x$ and $\top \preceq y$
By definition of greatest element:
:$x \preceq \top$
Thus by definition of antisymmetry:
:$\top = x$
{{qed}}
Theorem: Meet Irreducible iff Finite Infimum equals Element

Let $L = \left({S, \wedge, \preceq}\right)$ be a meet semilattice.
Let $x \in S$.
Then
:$x$ is meet irreducible
{{iff}}
:for every non-empty finite subset $A$ of $S$: $x = \inf A \implies x \in A$

Proof:
=== Sufficient Condition ===
Let $x$ be meet irreducible.
We will prove the result by induction on cardinality of $A$.
Theorem: Sum over k of Sum over j of Floor of n + jb^k over b^k+1

Let $n, b \in \Z$ such that $n \ge 0$ and $b \ge 2$.
Then:
:$\ds \sum_{k \mathop \ge 0} \sum_{1 \mathop \le j \mathop < b} \floor {\dfrac {n + j b^k} {b^{k + 1} } } = n$
where $\floor {\, \cdot \,}$ denotes the floor function.

Proof:
We have that $\floor {\dfrac {n + j b^k} {b^{k + 1} } }$ is in the form $\floor {\dfrac {m k + x} n}$ so that:
{{begin-eqn}}
{{eqn | l = \sum_{1 \mathop \le j \mathop < b} \floor {\dfrac {n + j b^k} {b^{k + 1} } }
      | r = \sum_{1 \mathop \le j \mathop < b} \floor {\dfrac {j + \frac n {b^k} } b}
      | c = 
}}
{{eqn | r = \sum_{0 \mathop \le j \mathop < b} \floor {\dfrac {j + \frac n {b^k} } b} - \floor {\dfrac n {b^{k + 1} } }
      | c = 
}}
{{eqn | r = \dfrac {\paren {1 - 1} \paren {b - 1} } 2 + \dfrac {\paren {1 - 1} } 2 + 1 \floor {\dfrac n {b^k} } - \floor {\dfrac n {b^{k + 1} } }
      | c = Summation over k of Floor of mk+x over n
}}
{{eqn | r = \floor {\dfrac n {b^k} } - \floor {\dfrac n {b^{k + 1} } }
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop \ge 0} \sum_{1 \mathop \le j \mathop < b} \floor {\dfrac {n + j b^k} {b^{k + 1} } }
      | r = \sum_{k \mathop \ge 0} \paren {\floor {\dfrac n {b^k} } - \floor {\dfrac n {b^{k + 1} } } }
      | c = 
}}
{{eqn | r = \lim_{k \mathop \to \infty} \floor {\dfrac n 1} - \floor {\dfrac n {b^{k + 1} } }
      | c = {{Defof|Telescoping Series}}
}}
{{eqn | r = n
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum over j of Function of Floor of mj over n

Let $f$ be a real function.
Then:
:$\ds \sum_{0 \mathop \le j \mathop < n} \map f {\floor {\dfrac {m j} n} } = \sum_{0 \mathop \le r \mathop < m} \ceiling {\dfrac {r n} m} \paren {\map f {r - 1} - \map f r} + n \map f {m - 1}$

Proof:
{{begin-eqn}}
{{eqn | l = r
      | m = \floor {\dfrac {m j} n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r
      | o = \le
      | m = \dfrac {m j} n
      | mo= <
      | r = r + 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {r n} m
      | o = \le
      | m = j
      | mo= <
      | r = \dfrac {\paren {r + 1} n} m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \ceiling {\dfrac {r n} m}
      | o = \le
      | m = j
      | mo= <
      | r = \ceiling {\dfrac {\paren {r + 1} n} m}
      | c = as $j$ is an integer
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_{0 \mathop \le j \mathop < n} \map f {\floor {\dfrac {m j} n} }
      | c = 
}}
{{eqn | r = \sum_{0 \mathop \le \ceiling {\frac {r n} m} \mathop < n} \map f r
      | c = 
}}
{{eqn | r = \sum_{0 \mathop \le r \mathop < m} \map f r \paren {\ceiling {\dfrac {\paren {r + 1} n} m} - \ceiling {\dfrac {r n} m} }
      | c = 
}}
{{eqn | r = \map f 0 \ceiling {\dfrac n m} + \map f 1 \paren {\ceiling {\dfrac {2 n} m} - \ceiling {\dfrac n m} } + \cdots + \map f {m - 1} \paren {\ceiling {\dfrac {m n} m} - \ceiling {\dfrac {\paren {m - 1} n} m} }
      | c = 
}}
{{eqn | r = \ceiling {\dfrac n m} \paren {\map f 0 + \map f 1} + \ceiling {\dfrac {2 n} m} \paren {\map f 0 + \map f 1} + \cdots + \ceiling {\dfrac {\paren {m - 1} n} m} \paren {\map f {m - 2} + \map f {m - 1} } + n \map f {m - 1}
      | c = 
}}
{{eqn | r = \sum_{0 \mathop \le r \mathop < m} \ceiling {\dfrac {r n} m} \paren {\map f {r - 1} + \map f r} + n \map f {m - 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Legendre Symbol

Let $p$ be an odd prime.
Let $a \in \Z$.
{{TFAE|def = Legendre Symbol}}

Proof:
{{ProofWanted}}
Category:Legendre Symbol
0mcyc6lpkl926gdog8ux9xww3otz0x4
Theorem: Upper Closure of Element without Element is Filter implies Element is Meet Irreducible

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a lattice.
Let $x \in S$.
Let
:$x^\succeq \setminus \set x$ be a filter in $L$.
Then $x$ is meet irreducible.

Proof:
Let $a, b \in S$.
{{AimForCont}}:
:$x = a \wedge b$ and $x \ne a$ and $x \ne b$
By Meet Precedes Operands:
:$x \preceq b$ and $x \preceq a$
By definition of upper closure of element:
:$b, a \in x^\succeq$
By definitions of singleton and difference:
:$b, a \in x^\succeq \setminus \set x$
By definition of filtered:
:$\exists z \in x^\succeq \setminus \set x: z \preceq a \land z \preceq b$
By definition of infimum:
:$z \preceq x$
By definition of upper section:
:$x \in x^\succeq \setminus \set x$
Thus this contradicts $x \in \set x$ by definition of singleton.
{{qed}}
Theorem: Maximal Element of Complement of Filter is Meet Irreducible

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a lattice.
Let $F$ be a filter in $L$.
Let $p \in S$.
Let $p = \map \max {\relcomp S F}$.
Then $p$ is meet irreducible.

Proof:
Let $x, y \in S$.
{{AimForCont}}
:$p = x \wedge y$ and $p \ne x$ and $p \ne y$
By Meet Precedes Operands:
:$p \preceq x$ and $p \preceq y$
By definition of $\prec$:
:$p \prec x$ and $p \prec y$
We will prove that
:$x \notin F$ or $y \notin F$
{{AimForCont}}
:$x \in F \land y \in F$
By definition of filtered:
:$\exists z \in F: z \preceq x \land z \preceq y$
By definition of infimum:
:$z \preceq p$
By definition of upper section:
:$p \in F$
Thus this contradicts $p \in \relcomp S F$ by definition of greatest element.
{{qed|lemma}}
By definition of relative complement:
:$x \in \relcomp S F$ or $y \in \relcomp S F$
Thus by definition of greatest element:
this contradicts $p \prec x$ and $p \prec y$
{{qed}}
Theorem: De Polignac's Formula/Technique

When calculating $\mu$, the easiest way to calculate the next term is simply to divide the previous term by $p$ and discard the remainder:
:$\floor {\dfrac n {p^{k + 1} } } = \floor {\floor {\dfrac n {p^k} } / p}$

Proof:
From Floor of $\dfrac {x + m} n$: Corollary:
:$\floor {\dfrac {x + m} n} = \floor {\dfrac {\floor x + m} n}$
which is valid for all integers $m, n$ such that $n > 0$.
In this instance, $m = 0$ and $n = p$, while $x = \dfrac n {p^k}$.
{{qed}}
Theorem: Not Preceding implies There Exists Meet Irreducible Element Not Preceding

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice.
Let $x, y \in S$ such that
:$y \npreceq x$
Then
:$\exists p \in S: p$ is meet irreducible and $x \preceq p$ and $y \npreceq p$

Proof:
By definition of continuous:
:$L$ satisfies the axiom of approximation
and
:$\forall x \in S: x^\ll$ is directed.
By Axiom of Approximation in Up-Complete Semilattice
:$\exists u \in S: u \ll y \land u \npreceq x$
By Way Below implies There Exists Way Below Open Filter Subset of Way Above Closure:
:there exists way below open filter $F$ in $L$: $y \in F \subseteq u^\gg$
By Way Above Closure is Subset of Upper Closure of Element:
:$u^\gg \subseteq u^\succeq$
By definition of upper section:
:$x \notin F$
By definition of relative complement:
:$x \in \relcomp S F$
By Upper Way Below Open Subset Complement is Non Empty implies There Exists Maximal Element of Complement:
:$\exists m \in \relcomp S F: x \preceq m \land m = \max \relcomp S F$
Thus by Maximal Element of Complement of Filter is Meet Irreducible:
:$m$ is meet irreducible.
Thus
:$x \preceq m$
{{AimForCont}}
:$y \preceq m$
By definition of upper section:
:$m \in F$
This contradicts $m \in \relcomp S F$ by definition of greatest element.
{{qed}}
Theorem: Termial on Real Numbers is Extension of Integers

The termial function as defined on the real numbers is an extension of its definition on the integers $\Z$.

Proof:
From the definition of the termial function on the integers:
:$\ds n? = \sum_{k \mathop = 1}^n k = 1 + 2 + \cdots + n$
From Closed Form for Triangular Numbers, we have that:
:$\ds \forall n \in \Z_{> 0}: \sum_{k \mathop = 1}^n k = \dfrac {n \paren {n + 1} } 2$
This agrees with the definition of the termial function on the real numbers.
Hence the result, by definition of extension.
{{qed}}
Theorem: Floor of m+n-1 over n

Let $m, n \in \Z$ such that $n > 0$.
Then:
:$\floor {\dfrac {m + n - 1} n} = \ceiling {\dfrac m n}$
The identity does not necessarily apply for $n < 0$.

Proof:
First let $n > 0$ as stated.
Suppose $n \divides m$. 
Then $m = k n$ for some $k \in \Z$.
It follows that:
:$\floor {\dfrac {m + n - 1} n} = \floor {k + 1 - \dfrac 1 n} = k$
and:
:$\ceiling {\dfrac m n} = k$
Now suppose $n \nmid m$.
Since $n > 0$, we have $m = k n + r$ for some $k \in\Z$ and $r \in \N$, $0 < r < n$.
Therefore:
:$\floor {\dfrac {m + n - 1} n} = \floor {k + 1 + \dfrac {r - 1} n} = k + 1$
and:
:$\ceiling {\dfrac m n} = k + 1$
{{qed|lemma}}
Setting $m = 1, n = -2$ we have:
{{begin-eqn}}
{{eqn | l = \floor {\dfrac {m + n - 1} n}
      | r = \floor {\dfrac {1 + \paren {-2} - 1} {\paren {-2} } }
      | c = 
}}
{{eqn | r = \ceiling 1
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{eqn | o = \ne
      | r = 0
      | c = 
}}
{{eqn | r = \ceiling {\dfrac 1 {\paren {-2} } }
      | c = 
}}
{{eqn | r = \ceiling {\dfrac m n}
      | c = 
}}
{{end-eqn}}
Thus, as stated, it is confirmed that the identity does not hold for $n < 0$.
It is noted that when $n = 0$ the expressions on either side are not defined.
{{qed}}
Theorem: Characteristics of Floor and Ceiling Function

Let $f: \R \to \Z$ be an integer-valued function which satisfies both of the following:
:$(1): \quad \map f {x + 1} = \map f x + 1$
:$(2): \quad \forall n \in \Z_{> 0}: \map f x = \map f {\dfrac {\map f {n x} } n}$
Then either:
:$\forall x \in \Q: \map f x = \floor x$
or:
:$\forall x \in \Q: \map f x = \ceiling x$

Proof:
From $(1)$, by induction we have:
:$\forall n \in \N: \map f {x + n} = \map f x + n$
and
:$\forall n \in\N: \map f {x - n} = \map f x - n$
and therefore, in particular:
:$(3): \quad \forall n \in \Z: \map f n = \map f 0 + n$
From $(2)$, we get
{{begin-eqn}}
{{eqn | l = \map f 0
      | r = \map f {\map f 0}
}}
{{eqn | r = \map f 0 + \map f 0
      | c = using $(3)$ and $f$ being integer valued
}}
{{end-eqn}}
Hence
:$\map f 0 = 0$
Thus from $(3)$ it follows that:
:$\forall n \in \Z: \map f n = n$
Suppose that $\map f {\dfrac 1 2} = k \le 0$.
Then:
{{begin-eqn}}
{{eqn | l = k
      | r = \map f {\dfrac 1 {1 - 2 k} \map f {\dfrac 1 2 - k} }
      | c = 
}}
{{eqn | r = \map f {\dfrac 1 {1 - 2 k} \paren {\map f {\dfrac 1 2} - k} }
      | c = 
}}
{{eqn | r = \map f 0
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
We show that in this case, by induction:
:$\map f {\dfrac 1 n} = 0$ for all $n \in \N$
Induction hypothesis:
:$\map f {\dfrac 1 {n - 1} } = 0$
Then from $(1)$:
:$\map f {\dfrac n {n - 1} } = \map f {\dfrac 1 {n - 1} + 1} = 0 + 1 = 1$
so:
{{begin-eqn}}
{{eqn | l = \map f {\dfrac 1 n}
      | r = \map f {\dfrac 1 n \map f {\dfrac n {n - 1} } }
      | c = 
}}
{{eqn | r = \map f {\dfrac 1 {n - 1} }
      | c = using $(2)$
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
Finally, we show by induction on $m$ that even:
:$\map f {\dfrac m n} = 0$
for $m \in \set {1, \ldots, n - 1}$.
Above we have shown this for $m = 1$.
Let $1 \le m < n$. 
If $m \divides n$, then
:$\map f {\dfrac m n} = \map f {\dfrac 1 {n / m} } = 0$
Otherwise, write:
:$n = \paren {k - 1} m + r$
Then:
:$k > 1$
and:
:$1 \le r \le m - 1$
We therefore have:
:$k m = n + m - r$
so by the induction hypothesis:
:$\map f {\dfrac {k m} n} = \map f {1 + \dfrac {m - r} n} = 1 + \map f {\dfrac {m - r} n} = 1$
Then:
{{begin-eqn}}
{{eqn | l = \map f {\dfrac m n}
      | r = \map f {\dfrac 1 m \map f {\dfrac {m k} n} }
      | c = 
}}
{{eqn | r = \map f {\dfrac 1 m}
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
By $(1)$, this shows that
:$\map f {\dfrac 1 2} \le 0 \implies \map f x = \floor x$
for all rational $x$.
Suppose that $\map f {\dfrac 1 2} = k > 0$.
Then the integer-valued function $g: \R \to \Z$ satisfies:
:$\map g x = -\map f {-x}$
satisfies $(1)$ and $(2)$, and also:
{{begin-eqn}}
{{eqn | l = \map g {\dfrac 1 2}
      | r = 1 - \map f {\dfrac 1 2}
      | c = 
}}
{{eqn | o = \ge
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map f x
      | r = -\map g {-x}
      | c = 
}}
{{eqn | r = -\floor {-x}
      | c = 
}}
{{eqn | r = \ceiling x
      | c = Floor of Negative equals Negative of Ceiling
}}
{{end-eqn}}
Thus:
:$\map f {\dfrac 1 2} > 0 \implies \map f x = \ceiling x$
for all rational $x$.
{{qed}}
Theorem: Continuous Replicative Function

Let $f: \R \to \R$ be a real function.
Let $f$ be continuous on $\R$.
Let $f$ also be a replicative function.
Then $f$ is of the form:
:$\map f x = \paren {x - \dfrac 1 2} a$
where $a \in \R$.

Proof:
Let $f$ be a replicative function.
Then:
:$\forall n > 0: \map f {n x + 1} - \map f {n x} = \map f {x + 1} - \map f x$
If $f$ is then also continuous:
:$\forall x \in \R: \map f {x + 1} - \map f x$
and so:
:$\map g x = \map f x - c \floor x$
is both replicative and periodic.
We have:
:$\ds \int_0^1 e^{2 \pi i n x} \map g x \rd x = \dfrac 1 n \int_0^1 e^{2 \pi y} \map g y \rd y$
Expanding in a Fourier series shows:
:$\map g x = \paren {x - \dfrac 1 2} a$
for $0 < x < 1$.
Thus it follows that:
:$\map f x = \paren {x - \dfrac 1 2} a$
{{qed}}
{{MissingLinks|The above needs to be linked to the results used.}}
Theorem: Sum over k to p over 2 of Floor of 2kq over p

Let $p \in \Z$ be an odd prime.
Let $q \in \Z$ be an odd integer and $p \nmid q$.
Then:
:$\ds \sum_{0 \mathop \le k \mathop < p / 2} \floor {\dfrac {2 k q} p} \equiv \sum_{0 \mathop \le k \mathop < p / 2} \floor {\dfrac {k q} p} \pmod 2$

Proof:
When $k < \dfrac p 4$ we have:
{{begin-eqn}}
{{eqn | l = \floor {\dfrac {\paren {p - 1 - 2 k} q} p}
      | r = \floor {q - \dfrac {\paren {2 k + 1} q} p}
}}
{{eqn | r = q + \floor {-\dfrac {\paren {2 k + 1} q} p}
      | c = Floor of Number plus Integer
}}
{{eqn | r = q - \ceiling {\dfrac {\paren {2 k + 1} q} p}
      | c = Floor of Negative equals Negative of Ceiling
}}
{{eqn | r = q - 1 - \floor {\dfrac {\paren {2 k + 1} q} p}
      | c = Floor equals Ceiling iff Integer
}}
{{eqn | o = \equiv
      | r = \floor {\dfrac {\paren {2 k + 1} q} p}
      | rr= \pmod 2
      | c = 
}}
{{end-eqn}}
Here it is noted that $\dfrac {\paren {2 k + 1} q} p$ is not an integer, since we have:
:$p \nmid q$
:$p > \dfrac p 2 + 1 > 2 k + 1$
Thus it is possible to replace the last terms:
:$\floor {\dfrac {\paren {p - 1} q} p}, \floor {\dfrac {\paren {p - 3} q} p}, \ldots$
by:
:$\floor {\dfrac q p}, \floor {\dfrac {3 q} p}, \ldots$
The result follows.
{{qed}}
Theorem: Powers of Group Elements/Sum of Indices/Additive Notation

:$\forall m, n \in \Z: \paren {m \cdot g} + \paren {n \cdot g} = \paren {m + n} \cdot g$

Proof:
All elements of a group are invertible, so we can directly use the result from Index Laws for Monoids: Sum of Indices:
:$\forall m, n \in \Z: g^m \circ g^n = g^{m + n}$
where in this context the group operation is $+$ and $n$th power of $g$ is denoted $n g$.
{{qed}}
Theorem: Powers of Group Elements/Negative Index/Additive Notation

:$\forall n \in \Z: -\paren {n g} = \paren {-n} g = n \paren {-g}$

Proof:
All elements of a group are invertible, so we can directly use the result from Index Laws for Monoids: Sum of Indices:
:$\forall n \in \Z: \paren {g^n}^{-1} = g^{-n} = \paren {g^{-1} }^n$
where in this context:
:the group operation is $+$
:the $n$th power of $g$ is denoted $n g$
:the inverse of $g$ is $-g$.
{{qed}}
Theorem: Powers of Group Elements/Product of Indices/Additive Notation

:$\forall m, n \in \Z: n \cdot \paren {m \cdot g} = \paren {m \times n} \cdot g = m \cdot \paren {n \cdot g}$

Proof:
All elements of a group are invertible, so we can directly use the result from Index Laws for Monoids: Product of Indices:
:$\forall m, n \in \Z: g^{m n} = \paren {g^m}^n = \paren {g^n}^m$
where in this context:
:the group operation is $+$
:the $n$th power of $g$ is denoted $n \cdot g$
{{qed}}
Theorem: Power of Product in Abelian Group/Additive Notation

:$\forall x, y \in G: \forall k \in \Z: k \cdot \paren {x + y} = \paren {k \cdot x} + \paren {k \cdot y}$

Proof:
By definition of abelian group, $x$ and $y$ commute.
That is:
:$x + y = y + x$
The result follows from Power of Product of Commutative Elements in Group.
{{qed}}
Theorem: Power of Idempotent Element

Let $\struct {S, \circ}$ be an algebraic structure.
Let $s \in S$ be an idempotent element with respect to $\circ$.
Then:
:$\forall n \in \Z_{> 0}: s^n = s$
where $s^n$ is defined as:
:$s^n = \begin{cases} s & : n = 1 \\
s^{n - 1} \circ s & : n > 1 \end{cases}$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{> 0}$, let $\map P n$ be the proposition:
:$s^n = s$
$\map P 1$ is the case:
:$s^1 = s$
which holds by definition.
Thus $\map P 1$ is seen to hold.
Theorem: Powers of Group Element Commute

Let $\struct {G, \circ}$ be a group.
Let $g \in G$.
Let $m, n \in \N_{>0}$.
Then:
:$\forall m, n \in \N_{>0}: g^n \circ g^m = g^m \circ g^n$

Proof:
By definition, a group is also a semigroup.
The result follows as a special case of Powers of Semigroup Element Commute
{{Qed}}
Theorem: Strictly Positive Real Numbers under Multiplication form Subgroup of Non-Zero Real Numbers

Let $\R_{>0}$ be the set of strictly positive real numbers, that is:
:$\R_{>0} = \set {x \in \R: x > 0}$
The structure $\struct {\R_{>0}, \times}$ forms a subgroup of $\struct {\R_{\ne 0}, \times}$, where $\R_{\ne 0}$ is the set of real numbers without zero, that is:
:$\R_{\ne 0} = \R \setminus \set 0$

Proof:
From Non-Zero Real Numbers under Multiplication form Abelian Group we have that $\struct {\R_{\ne 0}, \times}$ is a group.
We know that $\R_{>0} \ne \O$, as (for example) $1 \in \R_{>0}$.
Now, verify that the conditions for Two-Step Subgroup Test are satisfied:
Theorem: Strictly Positive Rational Numbers under Multiplication form Subgroup of Non-Zero Rational Numbers

Let $\Q_{> 0}$ be the set of strictly positive rational numbers, that is $\Q_{> 0} = \set { x \in \Q: x > 0}$.
The structure $\struct {\Q_{> 0}, \times}$ is a subgroup of $\struct {\Q_{\ne 0}, \times}$, where $\Q_{\ne 0}$ is the set of rational numbers without zero: $\Q_{\ne 0} = \Q \setminus \set 0$.

Proof:
From Non-Zero Rational Numbers under Multiplication form Infinite Abelian Group we have that $\struct {\Q_{\ne 0}, \times}$ is a group.
We know that $\Q_{> 0} \ne \O$, as (for example) $1 \in \Q_{> 0}$.
Let $a, b \in \Q_{> 0}$.
Then:
:$a b \in \Q_{\ne 0}$ and $ab > 0$
Hence:
:$a b \in \Q_{> 0}$
Let $a \in \Q_{> 0}$.
Then:
:$a^{-1} = \dfrac 1 a \in \Q_{> 0}$
So, by the Two-Step Subgroup Test, $\struct {\Q_{> 0}, \times}$ is a subgroup of $\struct {\Q_{\ne 0}, \times}$.
{{qed}}
Category:Rational Multiplication
Category:Subgroups
hosydfksvcrtu0v4mxpr0xfx1w3225y