Skip to content

Absolute value of real numbers #1385

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 100 commits into from
Mar 27, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
100 commits
Select commit Hold shift + click to select a range
68ffc45
Associativity of min and max
lowasser Feb 8, 2025
4ac4f7d
Merge branch 'master' into min-max-associative
lowasser Feb 8, 2025
4a8b5c5
Formatting
lowasser Feb 8, 2025
6a9f837
Define lower Dedekind cuts/reals
lowasser Feb 9, 2025
ef39dd3
make pre-commit
lowasser Feb 9, 2025
59195c9
Define upper Dedekind reals
lowasser Feb 9, 2025
4233e28
make pre-commit
lowasser Feb 9, 2025
6ad62d5
Rename things
lowasser Feb 9, 2025
6bfb619
Formatting
lowasser Feb 9, 2025
fd8f384
Add new file
lowasser Feb 9, 2025
fb0d5d3
Fix line length
lowasser Feb 9, 2025
efaf647
Merge branch 'lower-upper-dedekind' into lower-upper-rational-dedekind
lowasser Feb 9, 2025
f21b948
Add rational upper reals
lowasser Feb 9, 2025
a3d3af9
Progress
lowasser Feb 9, 2025
ba687cd
Merge branch 'lower-upper-rational-dedekind' into lower-upper-inequality
lowasser Feb 9, 2025
fb18a45
Preservation of inequality
lowasser Feb 9, 2025
0aa663c
Define normal Dedekind reals in terms of lower and upper cuts
lowasser Feb 9, 2025
1f9f502
Merge branch 'lower-upper-inequality' into lower-upper-dedekind
lowasser Feb 9, 2025
7499c7c
Start negation
lowasser Feb 9, 2025
2185e18
Inequality on upper reals
lowasser Feb 9, 2025
f2da896
overhaul
lowasser Feb 10, 2025
70f181c
make pre-commit
lowasser Feb 10, 2025
9268779
a -> an
lowasser Feb 10, 2025
e40e90b
Merge branch 'master' into lower-upper-neg
lowasser Feb 10, 2025
1b9d81b
Rename some things
lowasser Feb 10, 2025
d40a43a
Merge branch 'master' into lower-upper-neg
lowasser Feb 10, 2025
f75209b
Some more theorems
lowasser Feb 11, 2025
6d17056
Merge branch 'master' into lower-upper-neg
lowasser Feb 11, 2025
098d4e8
Finish gaps
lowasser Feb 11, 2025
b3b72b2
Progress
lowasser Feb 11, 2025
56c4fe3
Merge remote-tracking branch 'origin/lower-upper-neg' into lower-uppe…
lowasser Feb 11, 2025
faaa937
Merge branch 'master' into lower-upper-neg
lowasser Feb 11, 2025
1f9d73a
Recover all the previous results
lowasser Feb 11, 2025
7857a80
Merge branch 'master' into lower-upper-neg
lowasser Feb 11, 2025
263f367
make pre-commit
lowasser Feb 11, 2025
a3da42d
Merge remote-tracking branch 'origin/lower-upper-neg' into lower-uppe…
lowasser Feb 11, 2025
3669840
Merge branch 'master' into lower-upper-neg
lowasser Feb 11, 2025
f235570
Remove empty bibliography
lowasser Feb 11, 2025
827111e
Review changes
lowasser Feb 11, 2025
f734874
Fix names
lowasser Feb 12, 2025
327479d
Progress
lowasser Feb 12, 2025
3a4c279
Merge branch 'master' into min-max-associative
lowasser Feb 12, 2025
80e1863
Merge
lowasser Feb 12, 2025
6eeef9a
Fix syntax
lowasser Feb 12, 2025
53e54d8
Fix links
lowasser Feb 12, 2025
71479ca
Fix naming
lowasser Feb 12, 2025
e535435
make pre-commit
lowasser Feb 12, 2025
bd83f7b
Start
lowasser Feb 12, 2025
fbbfe5e
Progress
lowasser Feb 12, 2025
c100494
Merge branch 'min-max-associative' into lower-upper-max-min
lowasser Feb 12, 2025
9444d9e
Progress
lowasser Feb 12, 2025
c62e125
Progress
lowasser Feb 12, 2025
ba7600c
Progress
lowasser Feb 12, 2025
178808f
Merge branch 'master' into lower-upper-neg
lowasser Feb 13, 2025
b524ba8
max-lower-R
lowasser Feb 13, 2025
0d68a13
make pre-commit
lowasser Feb 13, 2025
8c076b1
Progress
lowasser Feb 13, 2025
0f4ab58
Progress
lowasser Feb 13, 2025
4c342b2
Progress
lowasser Feb 13, 2025
a903440
More imports
lowasser Feb 13, 2025
42ad0b8
Merge branch 'min-max-associative' into inflattice
lowasser Feb 13, 2025
8df9c15
Merge branch 'master' into min-max-associative
lowasser Feb 13, 2025
f9e99ef
Merge branch 'min-max-associative' into inflattice
lowasser Feb 13, 2025
8aa85c0
Fix symbols in docs
lowasser Feb 13, 2025
24b6f2f
Merge branch 'add-rational-reals' into add-reals
lowasser Feb 13, 2025
6095330
Back off the hard bits
lowasser Feb 13, 2025
9a2c3d6
Merge branch 'master' into lower-upper-neg
lowasser Feb 13, 2025
7ad5d5f
Merge remote-tracking branch 'origin/lower-upper-neg' into lower-uppe…
lowasser Feb 13, 2025
23a33d3
Apply suggestions from code review
lowasser Feb 13, 2025
f2c3f76
renaming
lowasser Feb 13, 2025
b9f1d27
Fix formatting
lowasser Feb 13, 2025
3673163
make pre-commit
lowasser Feb 13, 2025
324595a
Respond to review comments
lowasser Feb 14, 2025
10a0a36
Inline explanations of lower and upper cuts
lowasser Feb 14, 2025
6430f86
Reword
lowasser Feb 14, 2025
73a9e40
Merge branch 'master' into inflattice
lowasser Feb 14, 2025
e64c537
Merge branch 'master' into lower-upper-neg
lowasser Feb 14, 2025
d35cc9a
Merge branch 'inflattice' into min-max-lower-upper
lowasser Feb 14, 2025
eb516ee
Merge branch 'lower-upper-neg' into min-max-lower-upper
lowasser Feb 14, 2025
02e1fdc
Typo fix
lowasser Feb 14, 2025
c213682
Progress
lowasser Feb 18, 2025
2276510
Define minimum and maximum on real numbers
lowasser Feb 19, 2025
fff4eda
make pre-commit
lowasser Feb 19, 2025
e5861c3
Begin defining the absolute value.
lowasser Feb 19, 2025
89e5a16
Merge branch 'master' into min-max-lower-upper
lowasser Feb 19, 2025
e4ef49b
make pre-commit
lowasser Feb 19, 2025
7a1164e
Merge branch 'min-max-lower-upper' into abs-real
lowasser Feb 19, 2025
8e9b4c5
Prove the absolute value is nonnegative
lowasser Feb 19, 2025
f04c6fd
Fix links
lowasser Feb 19, 2025
73a6953
Merge branch 'min-max-lower-upper' into abs-real
lowasser Feb 19, 2025
ef02378
Merge branch 'master' into abs-real
lowasser Mar 26, 2025
5db467d
Progress
lowasser Mar 26, 2025
5b103eb
make pre-commit
lowasser Mar 26, 2025
759bf61
Revert
lowasser Mar 26, 2025
872c07e
Update src/order-theory/least-upper-bounds-large-posets.lagda.md
lowasser Mar 26, 2025
1760b08
Review comments
lowasser Mar 26, 2025
d6b5608
Review comments
lowasser Mar 26, 2025
cef6c75
Apply suggestions from code review
lowasser Mar 27, 2025
4078ef9
Review coments
lowasser Mar 27, 2025
40877b9
Fix
lowasser Mar 27, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/elementary-number-theory/absolute-value-integers.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,9 @@ open import foundation.unit-type

## Idea

The {{#concept "absolute value" Disambiguation="of an integer" Agda=abs-ℤ}} of
an integer is the natural number with the same distance from `0`.
The
{{#concept "absolute value" Disambiguation="of an integer" Agda=abs-ℤ WD="absolute value" WDID=Q120812}}
of an integer is the natural number with the same distance from `0`.

## Definition

Expand Down
29 changes: 29 additions & 0 deletions src/order-theory/least-upper-bounds-large-posets.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,9 @@ module order-theory.least-upper-bounds-large-posets where

```agda
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.logical-equivalences
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.universe-levels

open import order-theory.dependent-products-large-posets
Expand Down Expand Up @@ -39,6 +41,15 @@ Similarly, a
of a family of elements `a : I → P` in a large poset `P` is an element `x` in
`P` such that the logical equivalence

```text
is-binary-upper-bound-Large-Poset P a b y ↔ (x ≤ y)
```

holds for every `y` in `P`.

Similarly, a least upper bound of a family of elements `a : I → P` in a large
poset `P` is an element `x` in `P` such that the logical equivalence

```text
is-upper-bound-family-of-elements-Large-Poset P a y ↔ (x ≤ y)
```
Expand Down Expand Up @@ -130,6 +141,24 @@ module _
backward-implication (H _) (refl-leq-Large-Poset P _)
```

### The least upper bound of `x` and `y` is the least upper bound of `y` and `x`

```agda
module _
{α : Level → Level} {β : Level → Level → Level}
(P : Large-Poset α β)
{l1 l2 : Level} (a : type-Large-Poset P l1) (b : type-Large-Poset P l2)
where

abstract
is-binary-least-upper-bound-swap-Large-Poset :
{l3 : Level} (y : type-Large-Poset P l3) →
is-least-binary-upper-bound-Large-Poset P a b y →
is-least-binary-upper-bound-Large-Poset P b a y
is-binary-least-upper-bound-swap-Large-Poset _ H z =
H z ∘iff iff-equiv commutative-product
```

### Binary least upper bounds are unique up to similarity of elements

```agda
Expand Down
2 changes: 2 additions & 0 deletions src/real-numbers.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
```agda
module real-numbers where

open import real-numbers.absolute-value-real-numbers public
open import real-numbers.addition-lower-dedekind-real-numbers public
open import real-numbers.addition-upper-dedekind-real-numbers public
open import real-numbers.apartness-real-numbers public
Expand All @@ -23,6 +24,7 @@ open import real-numbers.minimum-real-numbers public
open import real-numbers.minimum-upper-dedekind-real-numbers public
open import real-numbers.negation-lower-upper-dedekind-real-numbers public
open import real-numbers.negation-real-numbers public
open import real-numbers.nonnegative-real-numbers public
open import real-numbers.raising-universe-levels-real-numbers public
open import real-numbers.rational-lower-dedekind-real-numbers public
open import real-numbers.rational-real-numbers public
Expand Down
92 changes: 92 additions & 0 deletions src/real-numbers/absolute-value-real-numbers.lagda.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,92 @@
# The absolute value of real numbers

```agda
{-# OPTIONS --lossy-unification #-}

module real-numbers.absolute-value-real-numbers where
```

<details><summary>Imports</summary>

```agda
open import elementary-number-theory.rational-numbers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.empty-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import real-numbers.dedekind-real-numbers
open import real-numbers.inequality-real-numbers
open import real-numbers.maximum-real-numbers
open import real-numbers.negation-real-numbers
open import real-numbers.nonnegative-real-numbers
```

</details>

## Idea

The
{{#concept "absolute value" Disambiguation="of a real number" Agda=abs-ℝ WD="absolute value" WDID=Q120812}}
of a [real number](real-numbers.dedekind-real-numbers.md) is the
[maximum](real-numbers.maximum-real-numbers.md) of it and its
[negation](real-numbers.negation-real-numbers.md).

```agda
abs-ℝ : {l : Level} → ℝ l → ℝ l
abs-ℝ x = binary-max-ℝ x (neg-ℝ x)
```

## Properties

### The absolute value of a real number is nonnegative

```agda
abstract
is-nonnegative-abs-ℝ : {l : Level} → (x : ℝ l) → is-nonnegative-ℝ (abs-ℝ x)
is-nonnegative-abs-ℝ x q q<0 =
elim-disjunction
( lower-cut-ℝ (abs-ℝ x) q)
( id)
( λ (x<0 , 0<x) → ex-falso (is-disjoint-cut-ℝ x zero-ℚ (0<x , x<0)))
( is-located-lower-upper-cut-ℝ (abs-ℝ x) q zero-ℚ q<0)
```

### The absolute value of the negation of a real number is its absolute value

```agda
abstract
abs-neg-ℝ : {l : Level} → (x : ℝ l) → abs-ℝ (neg-ℝ x) = abs-ℝ x
abs-neg-ℝ x =
ap (binary-max-ℝ (neg-ℝ x)) (neg-neg-ℝ x) ∙ commutative-binary-max-ℝ _ _
```

### `x` is between `-|x|` and `|x|`

```agda
module _
{l : Level} (x : ℝ l)
where

abstract
leq-abs-ℝ : leq-ℝ x (abs-ℝ x)
leq-abs-ℝ = leq-left-binary-max-ℝ x (neg-ℝ x)

neg-leq-abs-ℝ : leq-ℝ (neg-ℝ x) (abs-ℝ x)
neg-leq-abs-ℝ = leq-right-binary-max-ℝ x (neg-ℝ x)

leq-neg-abs-ℝ : leq-ℝ (neg-ℝ (abs-ℝ x)) x
leq-neg-abs-ℝ =
tr
( leq-ℝ (neg-ℝ (abs-ℝ x)))
( neg-neg-ℝ x)
( neg-leq-ℝ (neg-ℝ x) (abs-ℝ x) neg-leq-abs-ℝ)

neg-leq-neg-abs-ℝ : leq-ℝ (neg-ℝ (abs-ℝ x)) (neg-ℝ x)
neg-leq-neg-abs-ℝ = neg-leq-ℝ x (abs-ℝ x) leq-abs-ℝ
```
86 changes: 52 additions & 34 deletions src/real-numbers/inequality-real-numbers.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
Expand Down Expand Up @@ -75,41 +76,47 @@ module _
leq-ℝ' : UU (l1 ⊔ l2)
leq-ℝ' = type-Prop leq-ℝ-Prop'

leq-iff-ℝ' : leq-ℝ x y ↔ leq-ℝ'
pr1 (leq-iff-ℝ') lx⊆ly q q-in-uy =
elim-exists
( upper-cut-ℝ x q)
( λ p (p<q , p≮y) →
subset-upper-cut-upper-complement-lower-cut-ℝ
( x)
( q)
( intro-exists
( p)
( p<q ,
reverses-order-complement-subtype
( lower-cut-ℝ x)
( lower-cut-ℝ y)
( lx⊆ly)
( p)
( p≮y))))
( subset-upper-complement-lower-cut-upper-cut-ℝ y q q-in-uy)
pr2 leq-iff-ℝ' uy⊆ux p p-in-lx =
elim-exists
( lower-cut-ℝ y p)
( λ q (p<q , x≮q) →
subset-lower-cut-lower-complement-upper-cut-ℝ
( y)
( p)
( intro-exists
abstract
leq'-leq-ℝ : leq-ℝ x y → leq-ℝ'
leq'-leq-ℝ lx⊆ly q y<q =
elim-exists
( upper-cut-ℝ x q)
( λ p (p<q , p≮y) →
subset-upper-cut-upper-complement-lower-cut-ℝ
( x)
( q)
( p<q ,
reverses-order-complement-subtype
( upper-cut-ℝ y)
( upper-cut-ℝ x)
( uy⊆ux)
( q)
( x≮q))))
( subset-lower-complement-upper-cut-lower-cut-ℝ x p p-in-lx)
( intro-exists
( p)
( p<q ,
reverses-order-complement-subtype
( lower-cut-ℝ x)
( lower-cut-ℝ y)
( lx⊆ly)
( p)
( p≮y))))
( subset-upper-complement-lower-cut-upper-cut-ℝ y q y<q)

leq-leq'-ℝ : leq-ℝ' → leq-ℝ x y
leq-leq'-ℝ uy⊆ux p p<x =
elim-exists
( lower-cut-ℝ y p)
( λ q (p<q , x≮q) →
subset-lower-cut-lower-complement-upper-cut-ℝ
( y)
( p)
( intro-exists
( q)
( p<q ,
reverses-order-complement-subtype
( upper-cut-ℝ y)
( upper-cut-ℝ x)
( uy⊆ux)
( q)
( x≮q))))
( subset-lower-complement-upper-cut-lower-cut-ℝ x p p<x)

leq-iff-ℝ' : leq-ℝ x y ↔ leq-ℝ'
leq-iff-ℝ' = (leq'-leq-ℝ , leq-leq'-ℝ)
```

### Inequality on the real numbers is reflexive
Expand Down Expand Up @@ -186,6 +193,17 @@ iff-leq-real-ℚ : (x y : ℚ) → leq-ℚ x y ↔ leq-ℝ (real-ℚ x) (real-
iff-leq-real-ℚ = iff-leq-lower-real-ℚ
```

### Negation reverses inequality on the real numbers

```agda
module _
{l1 l2 : Level} (x : ℝ l1) (y : ℝ l2)
where

neg-leq-ℝ : leq-ℝ x y → leq-ℝ (neg-ℝ y) (neg-ℝ x)
neg-leq-ℝ x≤y = leq-leq'-ℝ (neg-ℝ y) (neg-ℝ x) (x≤y ∘ neg-ℚ)
```

## References

{{#bibliography}}
57 changes: 57 additions & 0 deletions src/real-numbers/maximum-real-numbers.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ module real-numbers.maximum-real-numbers where
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.empty-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.universe-levels

Expand All @@ -23,6 +24,7 @@ open import real-numbers.inequality-real-numbers
open import real-numbers.lower-dedekind-real-numbers
open import real-numbers.maximum-lower-dedekind-real-numbers
open import real-numbers.maximum-upper-dedekind-real-numbers
open import real-numbers.similarity-real-numbers
open import real-numbers.upper-dedekind-real-numbers
```

Expand Down Expand Up @@ -111,6 +113,61 @@ module _
( lower-real-ℝ z)
```

### The binary maximum is a binary upper bound

```agda
module _
{l1 l2 : Level}
(x : ℝ l1) (y : ℝ l2)
where

abstract
leq-left-binary-max-ℝ : leq-ℝ x (binary-max-ℝ x y)
leq-left-binary-max-ℝ =
pr1
( is-binary-upper-bound-is-least-binary-upper-bound-Large-Poset
( ℝ-Large-Poset)
( x)
( y)
( is-least-binary-upper-bound-binary-max-ℝ x y))

leq-right-binary-max-ℝ : leq-ℝ y (binary-max-ℝ x y)
leq-right-binary-max-ℝ =
pr2
( is-binary-upper-bound-is-least-binary-upper-bound-Large-Poset
( ℝ-Large-Poset)
( x)
( y)
( is-least-binary-upper-bound-binary-max-ℝ x y))
```

### The binary maximum is commutative

```agda
module _
{l1 l2 : Level}
(x : ℝ l1) (y : ℝ l2)
where

opaque
unfolding sim-ℝ

commutative-binary-max-ℝ : binary-max-ℝ x y = binary-max-ℝ y x
commutative-binary-max-ℝ =
eq-sim-ℝ
( sim-is-least-binary-upper-bound-Large-Poset
( ℝ-Large-Poset)
( x)
( y)
( is-least-binary-upper-bound-binary-max-ℝ x y)
( is-binary-least-upper-bound-swap-Large-Poset
( ℝ-Large-Poset)
( y)
( x)
( binary-max-ℝ y x)
( is-least-binary-upper-bound-binary-max-ℝ y x)))
```

### The large poset of real numbers has joins

```agda
Expand Down
40 changes: 40 additions & 0 deletions src/real-numbers/nonnegative-real-numbers.lagda.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
# Nonnegative real numbers

```agda
{-# OPTIONS --lossy-unification #-}

module real-numbers.nonnegative-real-numbers where
```

<details><summary>Imports</summary>

```agda
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import real-numbers.dedekind-real-numbers
open import real-numbers.inequality-real-numbers
open import real-numbers.rational-real-numbers
```

</details>

## Idea

A real number `x` is
{{#concept "nonnegative" Disambiguation="real number" Agda=is-nonnegative-ℝ}} if
`0 ≤ x`.

## Definitions

```agda
is-nonnegative-ℝ : {l : Level} → ℝ l → UU l
is-nonnegative-ℝ = leq-ℝ zero-ℝ

is-nonnegative-prop-ℝ : {l : Level} → ℝ l → Prop l
is-nonnegative-prop-ℝ = leq-ℝ-Prop zero-ℝ

nonnegative-ℝ : (l : Level) → UU (lsuc l)
nonnegative-ℝ l = type-subtype (is-nonnegative-prop-ℝ {l})
```
Loading