Homotopy Type Theory
modulated Cauchy real numbers > history (Rev #6)
Definition
Let R R be a dense integral subdomain of the rational numbers ℚ \mathbb{Q} and let R + R_{+} be the positive terms of R R .
The Cauchy real numbers ℝ C \mathbb{R}_C are inductively generated by the following:
a function inj : C ( R , R + ) → ℝ C inj: C(R, R_{+}) \to \mathbb{R}_C , where C ( R , R + ) C(R, R_{+}) is the type of R + R_{+} -indexed net s in R R that are R + R_{+} -Cauchy approximation s.
a dependent family of terms
a : C ( R , R + ) , b : C ( R , R + ) ⊢ eq ℝ C ( a , b ) : ( ∏ ϵ : R + a ϵ ∼ ϵ b ϵ ) → ( inj ( a ) = ℝ C inj ( b ) ) a:C(R, R_{+}), b:C(R, R_{+}) \vdash eq_{\mathbb{R}_C}(a, b): \left( \prod_{\epsilon:R_{+}} a_\epsilon \sim_{\epsilon} b_\epsilon \right) \to (inj(a) =_{\mathbb{R}_C} inj(b))
where the R + R_{+} -premetric for ϵ : R + \epsilon:R_{+} is defined as
a ∼ ϵ b ≔ | a ϵ − b ϵ | < 4 ϵ a \sim_{\epsilon} b \coloneqq \vert a_\epsilon - b_\epsilon \vert \lt 4 \epsilon
a family of dependent terms
a : ℝ C , b : ℝ C ⊢ τ ( a , b ) : isProp ( a = ℝ C b ) a:\mathbb{R}_C, b:\mathbb{R}_C \vdash \tau(a, b): isProp(a =_{\mathbb{R}_C} b)
The Cauchy real numbers are sometimes defined using sequence s x : ℕ → R x:\mathbb{N} \to R , y : ℕ → R y:\mathbb{N} \to R with modulus of Cauchy convergence M : R + → ℕ M:R_{+} \to \mathbb{N} , N : R + → ℕ N:R_{+} \to \mathbb{N} respectively. However, the composition of a sequence and a modulus of Cauchy convergence yields a Cauchy approximation, so one could define Cauchy approximations a : R + → R a:R_{+} \to R as a ≔ x ∘ M a \coloneqq x \circ M and b : R + → R b:R_{+} \to R as b ≔ y ∘ N b \coloneqq y \circ N , with x M ( ϵ ) = a ϵ x_{M(\epsilon)} = a_\epsilon and y N ( ϵ ) = b ϵ y_{N(\epsilon)} = b_\epsilon following from function evaluation. In fact, Cauchy approximations and sequences with a modulus of Cauchy convergence are inter-definable.
See also
References
Revision on March 21, 2022 at 02:12:16 by
Anonymous? .
See the history of this page for a list of all contributions to it.