Homotopy Type Theory Eudoxus real numbers > history (Rev #2, changes)

Skip the Navigation Links | Home Page | All Pages | Latest Revisions | Authors |

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

Let the proposition that an endofunction f:ℤ→ℤf:\mathbb{Z} \to \mathbb{Z} over the integers is bounded be defined as follows:

In set theory

isBounded(f)≔‖∑ C:ℤ∏ m:ℤ|f(m)|<C‖isBounded(f) \coloneqq \left\Vert \sum_{C:\mathbb{Z}} \prod_{m:\mathbb{Z}} \vert f(m) \vert \lt C \ \right\Vert

An endofunction f:ℤ ℤf:\mathbb{Z}^\mathbb{Z} over the integers is bounded if

and let the proposition that ff is almost linear be defined as follows:

∃C∈ℤ.∀m∈ℤ.|f(m)|<C\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \vert f(m) \vert \lt C
isAlmostLinear(f)≔‖∑ C:ℤ∏ m:ℤ∏ n:ℤ|f(m+n)−f(m)−f(n)|<C‖isAlmostLinear(f) \coloneqq \left\Vert \sum_{C:\mathbb{Z}} \prod_{m:\mathbb{Z}} \prod_{n:\mathbb{Z}} \vert f(m + n) - f(m) - f(n) \vert \lt C \ \right\Vert

and ff is almost linear if
∃C∈ℤ.∀m∈ℤ.∀n∈ℤ.|f(m+n)−f(m)−f(n)|<C\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \forall n \in \mathbb{Z}. \vert f(m + n) - f(m) - f(n) \vert \lt C

Let the set of almost linear endofunctions over the integers be defined as
AL(ℤ)≔{f∈ℤ ℤ|∃C∈ℤ.∀m∈ℤ.∀n∈ℤ.|f(m+n)−f(m)−f(n)|<C}AL(\mathbb{Z}) \coloneqq \{f\in \mathbb{Z}^\mathbb{Z} \vert \exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \forall n \in \mathbb{Z}. \vert f(m + n) - f(m) - f(n) \vert \lt C \}

The set of Eudoxus real numbers is a set ℝ\mathbb{R} with a function ι∈ℝ AL(ℤ)\iota \in \mathbb{R}^{AL(\mathbb{Z})} such that
∀f∈AL(ℤ).∀g∈AL(ℤ).(∃C∈ℤ.∀m∈ℤ.|f(m)−g(m)|<C)⇒(ι(f)=ι(g))\forall f \in AL(\mathbb{Z}). \forall g \in AL(\mathbb{Z}). (\exists C \in \mathbb{Z}. \forall m \in \mathbb{Z}. \vert f(m) - g(m) \vert \lt C) \implies (\iota(f) = \iota(g))

In homotopy type theory

Let the proposition that an endofunction f:ℤ→ℤf:\mathbb{Z} \to \mathbb{Z} over the integers is bounded be defined as follows:
isBounded(f)≔‖∑ C:ℤ∏ m:ℤ|f(m)|<C‖isBounded(f) \coloneqq \left\Vert \sum_{C:\mathbb{Z}} \prod_{m:\mathbb{Z}} \vert f(m) \vert \lt C \ \right\Vert

and let the proposition that ff is almost linear be defined as follows:
isAlmostLinear(f)≔‖∑ C:ℤ∏ m:ℤ∏ n:ℤ|f(m+n)−f(m)−f(n)|<C‖isAlmostLinear(f) \coloneqq \left\Vert \sum_{C:\mathbb{Z}} \prod_{m:\mathbb{Z}} \prod_{n:\mathbb{Z}} \vert f(m + n) - f(m) - f(n) \vert \lt C \ \right\Vert

Let the type of almost linear endofunctions over the integers be defined as

AL(ℤ)≔∑ f:ℤ→ℤisAlmostLinear(f)AL(\mathbb{Z}) \coloneqq \sum_{f:\mathbb{Z} \to \mathbb{Z}} isAlmostLinear(f)

The type of Eudoxus real numbers, denoted as ℝ\mathbb{R}, is a higher inductive type generated by:

  • a function inj ι:AL(ℤ)→ℝ inj: \iota: AL(\mathbb{Z}) \to \mathbb{R}

  • a dependent product of functions from propositions to identities:

η:∏ f:AL(ℤ)∏ g:AL(ℤ)isBounded(f−g)→( inj ι(f)= inj ι(g)) \eta : \prod_{f:AL(\mathbb{Z})} \prod_{g:AL(\mathbb{Z})} isBounded(f - g) \to (inj(f) (\iota(f) = inj(g)) \iota(g))
  • A set-truncator
    τ 0:∏ a:ℝ∏ b:ℝisProp(a=b)\tau_0: \prod_{a:\mathbb{R}} \prod_{b:\mathbb{R}} isProp(a=b)

See also

References

Revision on April 13, 2022 at 23:42:51 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (2 more)Previous revision (1 more)Current version of pageHide changesHistory (3 revisions)Rollback Source