IsarMathLib

In this theory file we consider the properties of integers that are needed for the real numbers construction in Real_ZF series.

In this section we study basic properties of slopes - the integer almost homomorphisms. The general definition of an almost homomorphism \(f\) on a group \(G\) written in additive notation requires the set \(\{f(m+n) - f(m) - f(n): m,n\in G\}\) to be finite. In this section we establish a definition that is equivalent for integers: that for all integer \(m,n\) we have \(|f(m+n) - f(m) - f(n)| \leq L\) for some \(L\).

First we extend the standard notation for integers with notation related to slopes. We define slopes as almost homomorphisms on the additive group of integers. The set of slopes is denoted \( \mathcal{S} \). We also define "positive" slopes as those that take infinite number of positive values on positive integers. We write \( \delta (s,m,n) \) to denote the homomorphism difference of \(s\) at \(m,n\) (i.e the expression \(s(m+n) - s(m) - s(n)\)). We denote \( \text{ max}\delta (s) \) the maximum absolute value of homomorphism difference of \(s\) as \(m,n\) range over integers. If \(s\) is a slope, then the set of homomorphism differences is finite and this maximum exists. In Group_ZF_3 we define the equivalence relation on almost homomorphisms using the notion of a quotient group relation and use "\( \approx \)" to denote it. As here this symbol seems to be hogged by the standard Isabelle, we will use "\( \sim \)" instead "\( \approx \)". We show in this section that \(s\sim r\) iff for some \(L\) we have \(|s(m)-r(m)| \leq L\) for all integer \(m\). The "\( + \)" denotes the first operation on almost homomorphisms. For slopes this is addition of functions defined in the natural way. The "\( \circ \)" symbol denotes the second operation on almost homomorphisms (see Group_ZF_3 for definition), defined for the group of integers. In short "\( \circ \)" is the composition of slopes. The "\( ^{-1} \)" symbol acts as an infix operator that assigns the value \(\min\{n\in Z_+: p\leq f(n)\}\) to a pair (of sets) \(f\) and \(p\). In application \(f\) represents a function defined on \(Z_+\) and \(p\) is a positive integer. We choose this notation because we use it to construct the right inverse in the ring of classes of slopes and show that this ring is in fact a field. To study the homomorphism difference of the function defined by \(p\mapsto f^{-1}(p)\) we introduce the symbol \( \varepsilon \) defined as \(\varepsilon(f,\langle m,n \rangle ) = f^{-1}(m+n)-f^{-1}(m)-f^{-1}(n)\). Of course the intention is to use the fact that \(\varepsilon(f,\langle m,n \rangle )\) is the homomorphism difference of the function \(g\) defined as \(g(m) = f^{-1}(m)\). We also define \(\gamma (s,m,n)\) as the expression \(\delta(f,m,-n)+s(0)-\delta (f,n,-n)\). This is useful because of the identity \(f(m-n) = \gamma (m,n) + f(m)-f(n)\) that allows to obtain bounds on the value of a slope at the difference of of two integers. For every integer \(m\) we introduce notation \(m^S\) defined by \(m^E(n)=m\cdot n\). The mapping \(q\mapsto q^S\) embeds integers into \( \mathcal{S} \) preserving the order, (that is, maps positive integers into \( \mathcal{S} _+ \)).

We can use theorems proven in the group1 context.

Type information related to the homomorphism difference expression.

Type information related to the homomorphism difference expression.

Slopes map integers into integers.

The homomorphism difference in multiplicative notation is defined as the expression \(s(m\cdot n)\cdot(s(m)\cdot s(n))^{-1}\). The next lemma shows that in the additive notation used for integers the homomorphism difference is \(f(m+n) - f(m) - f(n)\) which we denote as \( \delta (f,m,n) \).

The next formula restates the definition of the homomorphism difference to express the value an almost homomorphism on a sum.

The homomorphism difference of any integer function is integer.

The value of an integer function at a sum expressed in terms of \( \delta \).

The next lemma presents two ways the set of homomorphism differences can be written.

If \(f\) maps integers into integers and for all \(m,n\in Z\) we have \(|f(m+n) - f(m) - f(n)| \leq L\) for some \(L\), then \(f\) is a slope.

The absolute value of homomorphism difference of a slope \(s\) does not exceed \( \text{ max}\delta (s) \).

A useful estimate for the value of a slope at \(0\), plus some type information for slopes.

Int Group_ZF_3.thy we show that finite range functions valued in an abelian group form a normal subgroup of almost homomorphisms. This allows to define the equivalence relation between almost homomorphisms as the relation resulting from dividing by that normal subgroup. Then we show in Group_ZF_3_4_L12 that if the difference of \(f\) and \(g\) has finite range (actually \(f(n)\cdot g(n)^{-1}\) as we use multiplicative notation in Group_ZF_3.thy), then \(f\) and \(g\) are equivalent. The next lemma translates that fact into the notation used in int1 context.

A neccessary condition for two slopes to be almost equal. For slopes the definition postulates the set \(\{f(m)-g(m): m\in Z\}\) to be finite. This lemma shows that this implies that \(|f(m)-g(m)|\) is bounded (by some integer) as \(m\) varies over integers. We also mention here that in this context \( s \sim r \) implies that both \(s\) and \(r\) are slopes.

Let's recall that the relation of almost equality is an equivalence relation on the set of slopes.

Another version of sufficient condition for two slopes to be almost equal: if the difference of two slopes is a finite range function, then they are almost equal.

If two slopes are almost equal, then the difference has finite range. This is the inverse of Int_ZF_2_1_L9C.

What is the value of a composition of slopes?

Composition of slopes is a slope.

Negative of a slope is a slope.

What is the value of a negative of a slope?

What are the values of a sum of slopes?

Sum of slopes is a slope.

A simple but useful identity.

Some estimates for the absolute value of a slope at the opposite integer.

An identity that expresses the value of an integer function at the opposite integer in terms of the value of that function at the integer, zero, and the homomorphism difference. We have a similar identity in Int_ZF_2_1_L14, but over there we assume that \(f\) is a slope.

The next lemma allows to use the expression \( maxf(f, 0 .\ .\ M-1) \). Recall that \( maxf(f,A) \) is the maximum of (function) \(f\) on (the set) \(A\).

A lower estimate for the value of a slope at \(nM+k\).

Identity is a slope.

Simple identities about (absolute value of) homomorphism differences.

Some identities about the homomorphism difference of odd functions.

Recall that \(f\) is a slope iff \(f(m+n)-f(m)-f(n)\) is bounded as \(m,n\) ranges over integers. The next lemma is the first step in showing that we only need to check this condition as \(m,n\) ranges over positive intergers. Namely we show that if the condition holds for positive integers, then it holds if one integer is positive and the second one is nonnegative.

If the slope condition holds for all pairs of integers such that one integer is positive and the second one is nonnegative, then it holds when both integers are nonnegative.

If the homomorphism difference is bounded on \( \mathbb{Z} _+\times \mathbb{Z} _+ \), then it is bounded on \( \mathbb{Z} ^+\times \mathbb{Z} ^+ \).

For odd functions we can do better than in Int_ZF_2_1_L22: if the homomorphism difference of \(f\) is bounded on \( \mathbb{Z} ^+\times \mathbb{Z} ^+ \), then it is bounded on \( \mathbb{Z} \times \mathbb{Z} \), hence \(f\) is a slope. Loong prof by splitting the \( \mathbb{Z} \times \mathbb{Z} \) into six subsets.

If the homomorphism difference of a function defined on positive integers is bounded, then the odd extension of this function is a slope.

Type information related to \(\gamma\).

A couple of formulae involving \(f(m-n)\) and \(\gamma(f,m,n)\).

A formula expressing the difference between \(f(m-n-k)\) and \(f(m)-f(n)-f(k)\) in terms of \(\gamma\).

If \(s\) is a slope, then \(\gamma (s,m,n)\) is uniformly bounded.

If \(s\) is a slope, then \(s(m) \leq s(m-1) + M\), where \(L\) does not depend on \(m\).

If \(s\) is a slope, then the difference between \(s(m-n-k)\) and \(s(m)-s(n)-s(k)\) is uniformly bounded.

If \(s\) is a slope, then we can find integers \(M,K\) such that \(s(m-n-k) \leq s(m)-s(n)-s(k) + M\) and \(s(m)-s(n)-s(k) + K \leq s(m-n-k)\), for all integer \(m,n,k\).

By definition functions \(f,g\) are almost equal if \(f-g\)* is bounded. In the next lemma we show it is sufficient to check the boundedness on positive integers.

A sufficient condition for an odd slope to be almost equal to identity: If for all positive integers the value of the slope at \(m\) is between \(m\) and \(m\) plus some constant independent of \(m\), then the slope is almost identity.

A lemma about adding a constant to slopes. This is actually proven in Group_ZF_3_5_L1, in Group_ZF_3.thy here we just refer to that lemma to show it in notation used for integers. Unfortunately we have to use raw set notation in the proof.

Composition of slopes is not commutative. However, as we show in this section if \(f\) and \(g\) are slopes then the range of \(f\circ g - g\circ f\) is bounded. This allows to show that the multiplication of real numbers is commutative.

Two useful estimates.

If \(f\) is a slope, then \(|f(p\cdot q)-p\cdot f(q)|\leq (|p|+1)\cdot\)\( \text{ max}\delta (f) \). The proof is by induction on \(p\) and the next lemma is the induction step for the case when \(0\leq p\).

If \(f\) is a slope, then \(|f(p\cdot q)-p\cdot f(q)|\leq (|p|+1)\cdot\)\( \text{ max}\delta \). The proof is by induction on \(p\) and the next lemma is the induction step for the case when \(p\leq 0\).

If \(f\) is a slope, then \(|f(p\cdot q)-p\cdot f(q)|\leq (|p|+1)\cdot\)\( \text{ max}\delta \)\((f)\). Proof by cases on \(0 \leq p\).

The next elegant result is Lemma 7 in the Arthan's paper \cite{Arthan2004}.

This is Lemma 8 in the Arthan's paper.

If \(f\) and \(g\) are slopes, then \(f\circ g\) is equivalent (almost equal) to \(g\circ f\). This is Theorem 9 in Arthan's paper \cite{Arthan2004}.