Homotopy Type Theory limit of a function > history (Rev #9, changes)

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

Showing changes from revision #8 to #9: Added | Removed | Changed

Contents

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

Definition

In rational set numbers theory

Let ℚ\mathbb{Q} be the rational numbers and let ℚ +\mathbb{Q}_{+} be the positive rational numbers. The limit of a function f:ℚ→ℚf:\mathbb{Q} \to \mathbb{Q} approaching a term c:ℚc:\mathbb{Q} is a term L:ℚL:\mathbb{Q} such that for all directed types II and nets x:I→ℚx:I \to \mathbb{Q} where cc is the limit of xx, LL is the limit of f∘xf \circ x, or written in type theory:

In Archimedean ordered fields

∏ I:𝒰isDirected(I)×∏ x:I→ℚisLimit(c,x)×isLimit(L,f∘x)\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to \mathbb{Q}} isLimit(c, x) \times isLimit(L, f \circ x)

Let FF be an Archimedean ordered field and let

where

F +≔{a∈F|0<aF_{+} \coloneqq \{a \in F \vert 0 \lt a
isLimit(c,x)≔∏ ϵ:ℚ +‖∑ N:I∏ i:I(i≥N)→(|x i−c|<ϵ)‖isLimit(c,x) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - c \vert \lt \epsilon) \Vert

be the positive elements in FF. The limit of a function f∈F Ff \in F^F approaching an element c∈Fc \in F is an element L∈FL \in F such that for all directed sets II and nets x∈F Ix \in F^I where cc is the limit of xx, LL is the limit of f∘xf \circ x, or written in type theory:

isLimit(L,f∘x)≔∏ ϵ:ℚ +‖∑ N:I∏ i:I(i≥N)→(|f(x i)−L|<ϵ)‖isLimit(L,f \circ x) \coloneqq \prod_{\epsilon:\mathbb{Q}_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert f(x_i) - L \vert \lt \epsilon) \Vert
∀I∈DirectedSet 𝒰.∀x∈F IisLimit(c,x)∧isLimit(L,f∘x)\forall I \in DirectedSet_\mathcal{U}. \forall x \in F^I isLimit(c, x) \wedge isLimit(L, f \circ x)

where the predicates
isLimit(c,x)≔∀ϵ∈F +.∃N∈I.∀i∈I.(i≥N)⇒(|x i−c|<ϵ)isLimit(c,x) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i\in I. (i \geq N) \implies (\vert x_i - c \vert \lt \epsilon)
isLimit(L,f∘x)≔∀ϵ∈F +.∃N∈I.∀i∈I.(i≥N)→(|f(x i)−L|<ϵ)isLimit(L,f \circ x) \coloneqq \forall \epsilon \in F_{+}. \exists N \in I. \forall i\in I. (i \geq N) \to (\vert f(x_i) - L \vert \lt \epsilon)

The limit is usually written as

L≔lim x→cf(x)L \coloneqq \lim_{x \to c} f(x)

In Archimedean ordered fields

In preconvergence spaces

Let F S F S be and anArchimedean ordered fieldTT and be letF +F_{+}preconvergence space s. be The the positive terms ofFF. The limit of a function f : ∈FT S→F f:\F f \to \in F T^S approaching a an term elementc : ∈ F S c:F c \in S is a an term elementL : ∈ F T L:F L \in T such that for all directed setsdirected typeII s andII and nets x : ∈IS I→F x:I x \to \in F S^I where cc is the alimit of xx, LL is the a limit off∘xf \circ x, or written in type theory:

∏ I:𝒰∀isDirected(I ) ∈×DirectedSet 𝒰∏ x:I→F.isLimit∀x∈S I.isLimit S(c,x,c)×isLimitisLimit T(L,f∘x,L) \prod_{I:\mathcal{U}} \forall isDirected(I) I \in DirectedSet_\mathcal{U}. \forall x \in S^I. isLimit_S(x, c) \times \prod_{x:I isLimit_T(f \to F} isLimit(c, x) \times isLimit(L, f \circ x) x, L)

In homotopy type theory

In Archimedean ordered fields

Let FF be an Archimedean ordered field and let
F +≔∑a:F0<aF_{+} \coloneqq \sum{a:F} 0 \lt a

be the positive elements in FF. The limit of a function f:F→Ff:\F \to F approaching a term c:Fc:F is a term L:FL:F such that for all directed types II and nets x:I→Fx:I \to F where cc is the limit of xx, LL is the limit of f∘xf \circ x, or written in type theory:
∏ I:𝒰isDirected(I)×∏ x:I→FisLimit(c,x)×isLimit(L,f∘x)\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to F} isLimit(c, x) \times isLimit(L, f \circ x)

where

isLimit(c,x)≔∏ ϵ:F +‖∑ N:I∏ i:I(i≥N)→(|x i−c|<ϵ)‖isLimit(c,x) \coloneqq \prod_{\epsilon:F_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert x_i - c \vert \lt \epsilon) \Vert
isLimit(L,f∘x)≔∏ ϵ:F +‖∑ N:I∏ i:I(i≥N)→(|f(x i)−L|<ϵ)‖isLimit(L,f \circ x) \coloneqq \prod_{\epsilon:F_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (\vert f(x_i) - L \vert \lt \epsilon) \Vert

The limit is usually written as

L≔lim x→cf(x)L \coloneqq \lim_{x \to c} f(x)

Most general definition

In preconvergence spaces

Let SS be and a type with apredicateTT beisLimit SisLimit_Spreconvergence space s. between The the type of all nets inSSlimit of a function f:S→Tf:S \to T approaching a term c:Sc:S is a term L:TL:T such that for all directed types II and nets x:I→Sx:I \to S where cc is a limit of xx, LL is a limit of f∘xf \circ x, or written in type theory:

∑ ∏ I:𝒰isDirected(I)×∏ x:I→SisLimit S( I x → , S c)×isLimit T(f∘x,L) \sum_{I:\mathcal{U}} \prod_{I:\mathcal{U}} isDirected(I) \times (I \prod_{x:I \to S) S} isLimit_S(x, c) \times isLimit_T(f \circ x, L)

and SS itself, and let TT be a type with a predicate isLimit TisLimit_T between the type of all nets in TT
∑ I:𝒰isDirected(I)×(I→T)\sum_{I:\mathcal{U}} isDirected(I) \times (I \to T)

and TT itself.

The limit of a function f:S→Tf:S \to T approaching a term c:Sc:S is a term L:TL:T such that for all directed types II and nets x:I→Sx:I \to S where cc is a limit of xx, LL is a limit of f∘xf \circ x, or written in type theory:
∏ I:𝒰isDirected(I)×∏ x:I→SisLimit S(x,c)×isLimit T(f∘x,L)\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isLimit_S(x, c) \times isLimit_T(f \circ x, L)

See also

Revision on April 14, 2022 at 05:08:58 by Anonymous?. See the history of this page for a list of all contributions to it.

DiscussNext revision (4 more)Previous revision (8 more)Current version of pageHide changesHistory (12 revisions)Rollback Source