Homotopy Type Theory
Cauchy approximation > history (Rev #6, changes)
Showing changes from revision #5 to #6:
Added | Removed | Changed
Definition
Let R T R T Archimedean directed ordered type integral domain with and a dense codirected type where the directed type operation strict order ⊕ \oplus , is associative, and letR + S R_{+} S be the a semiring? T T - of positive terms inR R premetric space . We define the predicate
Suppose S S R + R_{+} premetric space , and let x : R + → S x:R_{+} \to S net with index type R + R_{+}
isCauchyApproximation ( x ) ≔ ∏ δ : T ∏ η : T x δ ∼ δ ⊕ η x η isCauchyApproximation(x) \coloneqq \prod_{\delta:T} \prod_{\eta:T} x_\delta \sim_{\delta \oplus \eta} x_\eta isCauchyApproximation ( x ) ≔ ∏ δ : R + ∏ η : R + x δ ∼ δ + η x η isCauchyApproximation(x) \coloneqq \prod_{\delta:R_{+}} \prod_{\eta:R_{+}} x_\delta \sim_{\delta + \eta} x_\eta x x T T
x x R + R_{+}
x : T → S ⊢ c ( x ) : isCauchyApproximation ( x ) x:T \to S \vdash c(x): isCauchyApproximation(x) x : R + → S ⊢ c ( x ) : isCauchyApproximation ( x ) x:R_{+} \to S \vdash c(x): isCauchyApproximation(x) The type of T T S S
The type of R + R_{+} S S
C ( S , T ) ≔ ∑ x : T → S isCauchyApproximation ( x ) C(S, T) \coloneqq \sum_{x:T \to S} isCauchyApproximation(x) C ( S , R + ) ≔ ∑ x : R + → S isCauchyApproximation ( x ) C(S, R_{+}) \coloneqq \sum_{x:R_{+} \to S} isCauchyApproximation(x)
Properties
Every R + T R_{+} T Cauchy net indexed by R + T R_{+} T R + T R_{+} T is a codirected type, with linear order N : T N:T , and defined thus as a meet-pseudosemilattice, withN : ≔ R + δ ⊗ η N:R_{+} N \coloneqq \delta \otimes \eta defined for as N ≔ min ( δ , : η T ) N \delta:T \coloneqq \min(\delta, \eta) for and δ η : R + T \delta:R_{+} \eta:T , . η ϵ : R + \eta:R_{+} \epsilon:R_{+} , and is meet defined operation as min ϵ : ≔ R + δ × ⊕ R + η → R + \min:R_{+} \epsilon \times \coloneqq R_{+} \delta \to \oplus R_{+} \eta . ϵ : R + \epsilon:R_{+} is defined as ϵ ≔ δ + η \epsilon \coloneqq \delta + \eta
Thus, there is a family of dependent terms
x : R + T → S ⊢ n ( x ) : isCauchyApproximation ( x ) → isCauchyNet ( x ) x:R_{+} x:T \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)A R + T R_{+} T x ∘ M x \circ M x x R + T R_{+} T modulus of Cauchy convergence M M
See also
References
Revision on March 12, 2022 at 09:35:07 by
Anonymous? .
See the history of this page for a list of all contributions to it.