Homotopy Type Theory
Cauchy approximation > history (Rev #7, changes)
Showing changes from revision #6 to #7:
Added | Removed | Changed
Definition
Let T A T A directed abelian type group and with a point codirected type 1 : A 1:A , where a the directed type operation⊕ \oplus strict order is associative, and letS < S \lt , be a term T ζ : 0 < 1 T \zeta: 0 \lt 1 - and a family of dependent terms premetric space . We define the predicate
isCauchyApproximation a : A , b : A ⊢ α ( x a , b ) ≔ : ∏ δ : T ( ∏ η : T 0 x δ < ∼ δ ⊕ η a x η ) × ( 0 < b ) → ( 0 < a + b ) isCauchyApproximation(x) a:A, \coloneqq b:A \prod_{\delta:T} \vdash \prod_{\eta:T} \alpha(a, x_\delta b):(0 \sim_{\delta \lt \oplus a) \eta} \times x_\eta (0 \lt b) \to (0 \lt a + b) x x Let is a A + ≔ ∑ a : A ( 0 < a ) A_{+} \coloneqq \sum_{a:A} (0 \lt a) T T be the ifpositive cone? of A A .
x : T → S ⊢ c ( x ) : isCauchyApproximation ( x ) x:T \to S \vdash c(x): isCauchyApproximation(x) Let S S A + A_{+} premetric space . We define the predicate
The type of T T S S
isCauchyApproximation ( x ) ≔ ∏ δ : A + ∏ η : A + x δ ∼ δ ⊕ η x η isCauchyApproximation(x) \coloneqq \prod_{\delta:A_{+}} \prod_{\eta:A_{+}} x_\delta \sim_{\delta \oplus \eta} x_\eta C ( S , T ) ≔ ∑ x : T → S isCauchyApproximation ( x ) C(S, T) \coloneqq \sum_{x:T \to S} isCauchyApproximation(x) x x A + A_{+}
x : A + → S ⊢ c ( x ) : isCauchyApproximation ( x ) x:A_{+} \to S \vdash c(x): isCauchyApproximation(x)
The type of A + A_{+} S S
C ( S , A + ) ≔ ∑ x : A + → S isCauchyApproximation ( x ) C(S, A_{+}) \coloneqq \sum_{x:A_{+} \to S} isCauchyApproximation(x)
Properties
Every T A + T A_{+} Cauchy net indexed by T A + T A_{+} T A + T A_{+} is a strictly ordered type, and thus a directed type and a strictly codirected type, with N : T A + N:T N:A_{+} N ≔ δ ⊗ η N \coloneqq \delta \otimes \eta δ : T A + \delta:T \delta:A_{+} η : T A + \eta:T \eta:A_{+} ϵ : R + \epsilon:R_{+} ϵ ≔ + δ ⊕ η \epsilon \coloneqq + \delta \oplus \eta
Thus, there is a family of dependent terms
x : T A + → S ⊢ n ( x ) : isCauchyApproximation ( x ) → isCauchyNet ( x ) x:T x:A_{+} \to S \vdash n(x): isCauchyApproximation(x) \to isCauchyNet(x)A T A + T A_{+} x ∘ M x \circ M x x T A + T A_{+} modulus of Cauchy convergence M M
See also
References
Revision on March 12, 2022 at 21:31:00 by
Anonymous? .
See the history of this page for a list of all contributions to it.