Arithmetically located Dedekind cuts
Content created by Louis Wasserman and Fredrik Bakke.
Created on 2025-02-08.
Last modified on 2025-03-27.
{-# OPTIONS --lossy-unification #-} module real-numbers.arithmetically-located-dedekind-cuts where
Imports
open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.archimedean-property-rational-numbers open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.integers open import elementary-number-theory.multiplication-rational-numbers open import elementary-number-theory.natural-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.action-on-identifications-functions open import foundation.binary-transport open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.disjunction open import foundation.empty-types open import foundation.existential-quantification open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositional-truncations open import foundation.propositions open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels open import group-theory.abelian-groups open import real-numbers.dedekind-real-numbers open import real-numbers.lower-dedekind-real-numbers open import real-numbers.upper-dedekind-real-numbers
Definition
A pair of a lower Dedekind cut
L
and an upper Dedekind cut U
is
arithmetically located¶
if for any positive
rational number ε : ℚ⁺
, there
exists p, q : ℚ
where p ∈ L
and q ∈ U
, such that 0 < q - p < ε
.
Intuitively, when L , U
represent the cuts of a real number x
, p
and q
are rational approximations of x
to within ε
.
This follows parts of Section 11 in [BT09].
Definitions
The predicate of being arithmetically located on pairs of lower and upper Dedekind real numbers
module _ {l1 l2 : Level} (x : lower-ℝ l1) (y : upper-ℝ l2) where close-bounds-lower-upper-ℝ : ℚ⁺ → subtype (l1 ⊔ l2) (ℚ × ℚ) close-bounds-lower-upper-ℝ ε⁺ (p , q) = le-ℚ-Prop q (p +ℚ (rational-ℚ⁺ ε⁺)) ∧ cut-lower-ℝ x p ∧ cut-upper-ℝ y q is-arithmetically-located-prop-lower-upper-ℝ : Prop (l1 ⊔ l2) is-arithmetically-located-prop-lower-upper-ℝ = Π-Prop ℚ⁺ (λ ε⁺ → ∃ (ℚ × ℚ) (close-bounds-lower-upper-ℝ ε⁺)) is-arithmetically-located-lower-upper-ℝ : UU (l1 ⊔ l2) is-arithmetically-located-lower-upper-ℝ = type-Prop is-arithmetically-located-prop-lower-upper-ℝ
Properties
Arithmetically located cuts are located
If a pair of lower and upper Dedekind cuts is arithmetically located, it is also located.
module _ {l1 l2 : Level} (x : lower-ℝ l1) (y : upper-ℝ l2) where abstract is-located-is-arithmetically-located-lower-upper-ℝ : is-arithmetically-located-lower-upper-ℝ x y → is-located-lower-upper-ℝ x y is-located-is-arithmetically-located-lower-upper-ℝ arithmetically-located p q p<q = elim-exists ( cut-lower-ℝ x p ∨ cut-upper-ℝ y q) ( λ (p' , q') (q'<p'+q-p , p'∈L , q'∈U) → rec-coproduct ( λ p<p' → inl-disjunction ( is-in-cut-le-ℚ-lower-ℝ x p p' p<p' p'∈L)) ( λ p'≤p → inr-disjunction ( is-in-cut-le-ℚ-upper-ℝ ( y) ( q') ( q) ( concatenate-le-leq-ℚ ( q') ( p' +ℚ (q -ℚ p)) ( q) ( q'<p'+q-p) ( tr ( leq-ℚ (p' +ℚ (q -ℚ p))) ( is-identity-right-conjugation-Ab ( abelian-group-add-ℚ) ( p) ( q)) ( preserves-leq-left-add-ℚ (q -ℚ p) p' p p'≤p))) ( q'∈U))) ( decide-le-leq-ℚ p p')) ( arithmetically-located (positive-diff-le-ℚ p q p<q))
The cuts of Dedekind real numbers are arithmetically located
module _ {l : Level} (x : ℝ l) where abstract location-in-arithmetic-sequence-located-ℝ : (ε : ℚ⁺) (n : ℕ) (p : ℚ) → is-in-lower-cut-ℝ x p → is-in-upper-cut-ℝ x (p +ℚ (rational-ℤ (int-ℕ n) *ℚ rational-ℚ⁺ ε)) → exists ( ℚ) ( λ q → lower-cut-ℝ x q ∧ upper-cut-ℝ x (q +ℚ rational-ℚ⁺ (ε +ℚ⁺ ε))) location-in-arithmetic-sequence-located-ℝ ε⁺@(ε , _) zero-ℕ p p<x x<p+0ε = ex-falso ( is-disjoint-cut-ℝ ( x) ( p) ( p<x , tr ( is-in-upper-cut-ℝ x) ( ap (p +ℚ_) (left-zero-law-mul-ℚ ε) ∙ right-unit-law-add-ℚ p) ( x<p+0ε))) location-in-arithmetic-sequence-located-ℝ ε⁺@(ε , _) (succ-ℕ n) p p<x x<p+nε = elim-disjunction ( ∃ ℚ (λ q → lower-cut-ℝ x q ∧ upper-cut-ℝ x (q +ℚ (ε +ℚ ε)))) ( λ p+ε<x → location-in-arithmetic-sequence-located-ℝ ( ε⁺) ( n) ( p +ℚ ε) ( p+ε<x) ( tr ( is-in-upper-cut-ℝ x) ( equational-reasoning p +ℚ (rational-ℤ (int-ℕ (succ-ℕ n)) *ℚ ε) = p +ℚ (succ-ℚ (rational-ℤ (int-ℕ n)) *ℚ ε) by ap (p +ℚ_) (ap (_*ℚ ε) (inv (succ-rational-int-ℕ n))) = p +ℚ (ε +ℚ (rational-ℤ (int-ℕ n) *ℚ ε)) by ap (p +ℚ_) (mul-left-succ-ℚ _ _) = (p +ℚ ε) +ℚ rational-ℤ (int-ℕ n) *ℚ ε by inv (associative-add-ℚ _ _ _)) ( x<p+nε))) ( λ x<p+2ε → intro-exists ( p) ( p<x , tr ( is-in-upper-cut-ℝ x) ( associative-add-ℚ p ε ε) ( x<p+2ε))) ( is-located-lower-upper-cut-ℝ ( x) ( p +ℚ ε) ( (p +ℚ ε) +ℚ ε) ( le-right-add-rational-ℚ⁺ (p +ℚ ε) ε⁺)) is-arithmetically-located-ℝ : is-arithmetically-located-lower-upper-ℝ (lower-real-ℝ x) (upper-real-ℝ x) is-arithmetically-located-ℝ ε⁺@(ε , _) = let open do-syntax-trunc-Prop ( ∃ ( ℚ × ℚ) ( close-bounds-lower-upper-ℝ ( lower-real-ℝ x) ( upper-real-ℝ x) ( ε⁺))) in do ε'⁺@(ε' , pos-ε') , 2ε'<ε ← double-le-ℚ⁺ ε⁺ p , p<x ← is-inhabited-lower-cut-ℝ x q , x<q ← is-inhabited-upper-cut-ℝ x n , q-p<nε' ← archimedean-property-ℚ ε' (q -ℚ p) pos-ε' let nℚ = rational-ℤ (int-ℕ n) r , r<x , x<r+2ε' ← location-in-arithmetic-sequence-located-ℝ ( ε'⁺) ( n) ( p) ( p<x) ( le-upper-cut-ℝ ( x) ( q) ( p +ℚ (nℚ *ℚ ε')) ( tr ( le-ℚ q) ( commutative-add-ℚ (nℚ *ℚ ε') p) ( le-transpose-left-diff-ℚ q p (nℚ *ℚ ε') ( q-p<nε'))) ( x<q)) intro-exists ( r , r +ℚ (ε' +ℚ ε')) ( preserves-le-right-add-ℚ r (ε' +ℚ ε') ε 2ε'<ε , r<x , x<r+2ε')
References
- [BT09]
- Andrej Bauer and Paul Taylor. The Dedekind reals in abstract Stone duality. Mathematical Structures in Computer Science, 19:757–838, 2009. URL: PaulTaylor.EU/ASD/dedras/, doi:10.1017/S0960129509007695.
Recent changes
- 2025-03-27. Louis Wasserman. Addition on real numbers (#1336).
- 2025-02-16. Louis Wasserman. Break the Dedekind reals into lower and upper Dedekind reals (#1314).
- 2025-02-08. Fredrik Bakke. Functorial action of existential quantifications, and applications in
real-numbers
(#1298).