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

Showing changes from revision #5 to #6: Added | Removed | Changed

Contents

Definition

In rational numbers

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:Ix:I \to \mathbb{Q} where cc is the limit of xx, LL is the limit of fxf \circ x, or written in type theory:

I:𝒰isDirected(I)× x:IisLimit(c,x)×isLimit(L,fx)\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to \mathbb{R}} isLimit(c, x) \times isLimit(L, f \circ x)

where

isLimit(c,x) ϵ: + N:I i:I(iN)(|x ic|<ϵ)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
isLimit(L,fx) ϵ: + N:I i:I(iN)(|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

The limit is usually written as

Llim xcf(x)L \coloneqq \lim_{x \to c} f(x)

In premetric spaces

Let T R T R be a dense integral subdomain of the type rational numbers and let S S \mathbb{Q} be and aTR + T R_{+} - be the positive terms ofpremetric spaceRR . andUU be a VV-premetric space. The limit of a function f:SUf:S \to U approaching a term c:Sc:S is a term L:UL:U such that for all directed types II and nets x:ISx:I \to S where cc is the limit of xx, LL is the limit of fxf \circ x, or written in type theory:

I:𝒰isDirected(I)× x:ISisLimit(c,x)×isLimit(L,fx)\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isLimit(c, x) \times isLimit(L, f \circ x)

Let SS and TT be R +R_{+}-premetric spaces. The limit of a function f:STf: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:ISx:I \to S where cc is the limit of xx, LL is the limit of fxf \circ x, or written in type theory:

I:𝒰isDirected(I)× x:ISisLimit(c,x)×isLimit(L,fx)\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} isLimit(c, x) \times isLimit(L, f \circ x)

where

isLimit(c,x) ϵ:TR + N:I i:I(iN)(x i ϵc) isLimit(c,x) \coloneqq \prod_{\epsilon:T} \prod_{\epsilon:R_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (x_i \sim_\epsilon c) \Vert
isLimit(L,fx) ϵ:VR + N:I i:I(iN)(f(x i) ϵL) isLimit(L,f \circ x) \coloneqq \prod_{\epsilon:V} \prod_{\epsilon:R_{+}} \Vert \sum_{N:I} \prod_{i:I} (i \geq N) \to (f(x_i) \sim_\epsilon L) \Vert

The limit is usually written as

Llim xcf(x)L \coloneqq \lim_{x \to c} f(x)

In Most convergence general spaces definition

LetSS be a type with a predicate S\to_S between the type of all nets in SS

I:𝒰isDirected(I)×(IS)\sum_{I:\mathcal{U}} isDirected(I) \times (I \to S)

and SS itself, and let TT be a type with a predicate T\to_T between the type of all nets in TT

I:𝒰isDirected(I)×(IT)\sum_{I:\mathcal{U}} isDirected(I) \times (I \to T)

and TT itself.

The limit of a function f:STf: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:ISx:I \to S where cc is a limit of xx, LL is a limit of fxf \circ x, or written in type theory:

I:𝒰isDirected(I)× x:IS(x Sc)×(fx TL)\prod_{I:\mathcal{U}} isDirected(I) \times \prod_{x:I \to S} (x \to_S c) \times (f \circ x \to_T L)

See also

Revision on March 31, 2022 at 06:56:59 by Anonymous?. See the history of this page for a list of all contributions to it.