diff --git a/.vscode/agda.code-snippets b/.vscode/agda.code-snippets index 817c4485b28..8b9bd16ade6 100644 --- a/.vscode/agda.code-snippets +++ b/.vscode/agda.code-snippets @@ -35,5 +35,10 @@ "body": ["retract-reasoning ? retract-of ? by ?"], "description": "Retract reasoning", "prefix": ["retract-reasoning"] + }, + "Inequality reasoning": { + "body": ["chain-of-inequalities ? ≤ ? by ?"], + "description": "Inequality reasoning", + "prefix": ["chain-of-inequalities"] } } diff --git a/src/commutative-algebra/powers-of-elements-large-commutative-rings.lagda.md b/src/commutative-algebra/powers-of-elements-large-commutative-rings.lagda.md index c4dfe1869c0..9c337440805 100644 --- a/src/commutative-algebra/powers-of-elements-large-commutative-rings.lagda.md +++ b/src/commutative-algebra/powers-of-elements-large-commutative-rings.lagda.md @@ -12,6 +12,7 @@ open import commutative-algebra.large-commutative-rings open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers open import foundation.identity-types open import foundation.universe-levels @@ -97,6 +98,25 @@ module _ power-one-Large-Ring (large-ring-Large-Commutative-Ring R) ``` +### `0ⁿ = 0` for nonzero `n` + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} + (R : Large-Commutative-Ring α β) + where + + nonzero-power-zero-Large-Commutative-Ring : + (n : ℕ⁺) → + ( power-Large-Commutative-Ring + ( R) + ( nat-nonzero-ℕ n) + ( zero-Large-Commutative-Ring R) ＝ + zero-Large-Commutative-Ring R) + nonzero-power-zero-Large-Commutative-Ring = + nonzero-power-zero-Large-Ring (large-ring-Large-Commutative-Ring R) +``` + ### `xⁿ⁺¹ = xⁿx` ```agda @@ -188,3 +208,20 @@ module _ distributive-power-mul-Large-Commutative-Monoid ( multiplicative-large-commutative-monoid-Large-Commutative-Ring R) ``` + +### Iterated powers commute + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} + (R : Large-Commutative-Ring α β) + where + + abstract + commute-power-Large-Commutative-Ring : + {l : Level} (m n : ℕ) (x : type-Large-Commutative-Ring R l) → + power-Large-Commutative-Ring R m (power-Large-Commutative-Ring R n x) ＝ + power-Large-Commutative-Ring R n (power-Large-Commutative-Ring R m x) + commute-power-Large-Commutative-Ring = + commute-power-Large-Ring (large-ring-Large-Commutative-Ring R) +``` diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 745734c2f2c..d94c2e216ab 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -58,6 +58,7 @@ open import elementary-number-theory.decidable-total-order-natural-numbers publi open import elementary-number-theory.decidable-total-order-rational-numbers public open import elementary-number-theory.decidable-total-order-standard-finite-types public open import elementary-number-theory.decidable-types public +open import elementary-number-theory.diagonal-integer-fractions public open import elementary-number-theory.difference-integers public open import elementary-number-theory.difference-rational-numbers public open import elementary-number-theory.dirichlet-convolution public diff --git a/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md b/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md index fd1909ddece..723cfd0b4c7 100644 --- a/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/addition-positive-rational-numbers.lagda.md @@ -12,6 +12,7 @@ module elementary-number-theory.addition-positive-rational-numbers where open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.difference-rational-numbers +open import elementary-number-theory.inequality-positive-rational-numbers open import elementary-number-theory.inequality-rational-numbers open import elementary-number-theory.minimum-positive-rational-numbers open import elementary-number-theory.positive-integer-fractions @@ -131,6 +132,37 @@ interchange-law-add-add-ℚ⁺ x y u v = ( rational-ℚ⁺ v)) ``` +### Addition with a positive rational number is a strictly increasing map + +```agda +abstract + le-left-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → le-ℚ x ((rational-ℚ⁺ d) +ℚ x) + le-left-add-rational-ℚ⁺ x d = + concatenate-leq-le-ℚ + ( x) + ( zero-ℚ +ℚ x) + ( (rational-ℚ⁺ d) +ℚ x) + ( inv-tr (leq-ℚ x) (left-unit-law-add-ℚ x) (refl-leq-ℚ x)) + ( preserves-le-left-add-ℚ + ( x) + ( zero-ℚ) + ( rational-ℚ⁺ d) + ( le-zero-is-positive-ℚ (is-positive-rational-ℚ⁺ d))) + + le-right-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → le-ℚ x (x +ℚ (rational-ℚ⁺ d)) + le-right-add-rational-ℚ⁺ x d = + inv-tr + ( le-ℚ x) + ( commutative-add-ℚ x (rational-ℚ⁺ d)) + ( le-left-add-rational-ℚ⁺ x d) + + leq-left-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → leq-ℚ x (rational-ℚ⁺ d +ℚ x) + leq-left-add-rational-ℚ⁺ x d = leq-le-ℚ (le-left-add-rational-ℚ⁺ x d) + + leq-right-add-rational-ℚ⁺ : (x : ℚ) (d : ℚ⁺) → leq-ℚ x (x +ℚ rational-ℚ⁺ d) + leq-right-add-rational-ℚ⁺ x d = leq-le-ℚ (le-right-add-rational-ℚ⁺ x d) +``` + ### The sum of two positive rational numbers is greater than each of them ```agda @@ -138,27 +170,13 @@ module _ (x y : ℚ⁺) where - le-left-add-ℚ⁺ : le-ℚ⁺ x (x +ℚ⁺ y) - le-left-add-ℚ⁺ = - tr - ( λ z → le-ℚ z ((rational-ℚ⁺ x) +ℚ (rational-ℚ⁺ y))) - ( right-unit-law-add-ℚ (rational-ℚ⁺ x)) - ( preserves-le-right-add-ℚ - ( rational-ℚ⁺ x) - ( zero-ℚ) - ( rational-ℚ⁺ y) - ( le-zero-is-positive-ℚ (is-positive-rational-ℚ⁺ y))) - - le-right-add-ℚ⁺ : le-ℚ⁺ y (x +ℚ⁺ y) + le-right-add-ℚ⁺ : le-ℚ⁺ x (x +ℚ⁺ y) le-right-add-ℚ⁺ = - tr - ( λ z → le-ℚ z ((rational-ℚ⁺ x) +ℚ (rational-ℚ⁺ y))) - ( left-unit-law-add-ℚ (rational-ℚ⁺ y)) - ( preserves-le-left-add-ℚ - ( rational-ℚ⁺ y) - ( zero-ℚ) - ( rational-ℚ⁺ x) - ( le-zero-is-positive-ℚ (is-positive-rational-ℚ⁺ x))) + le-right-add-rational-ℚ⁺ (rational-ℚ⁺ x) y + + le-left-add-ℚ⁺ : le-ℚ⁺ y (x +ℚ⁺ y) + le-left-add-ℚ⁺ = + le-left-add-rational-ℚ⁺ (rational-ℚ⁺ y) x ``` ### The positive difference of strictly inequal positive rational numbers @@ -196,7 +214,7 @@ module _ tr ( le-ℚ⁺ le-diff-ℚ⁺) ( left-diff-law-add-ℚ⁺) - ( le-left-add-ℚ⁺ le-diff-ℚ⁺ x) + ( le-right-add-ℚ⁺ le-diff-ℚ⁺ x) ``` ### Any positive rational number can be expressed as the sum of two positive rational numbers @@ -229,12 +247,18 @@ module _ le-left-summand-split-ℚ⁺ : le-ℚ⁺ left-summand-split-ℚ⁺ x le-left-summand-split-ℚ⁺ = le-mediant-zero-ℚ⁺ x + leq-left-summand-split-ℚ⁺ : leq-ℚ⁺ left-summand-split-ℚ⁺ x + leq-left-summand-split-ℚ⁺ = leq-le-ℚ le-left-summand-split-ℚ⁺ + le-right-summand-split-ℚ⁺ : le-ℚ⁺ right-summand-split-ℚ⁺ x le-right-summand-split-ℚ⁺ = tr ( le-ℚ⁺ right-summand-split-ℚ⁺) ( eq-add-split-ℚ⁺) - ( le-right-add-ℚ⁺ left-summand-split-ℚ⁺ right-summand-split-ℚ⁺) + ( le-left-add-ℚ⁺ left-summand-split-ℚ⁺ right-summand-split-ℚ⁺) + + leq-right-summand-split-ℚ⁺ : leq-ℚ⁺ right-summand-split-ℚ⁺ x + leq-right-summand-split-ℚ⁺ = leq-le-ℚ le-right-summand-split-ℚ⁺ le-add-split-ℚ⁺ : (p q r s : ℚ) → @@ -259,37 +283,6 @@ module _ ( rImports + +```agda +open import elementary-number-theory.integer-fractions +open import elementary-number-theory.integers +open import elementary-number-theory.multiplication-integer-fractions +open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.positive-integers + +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.propositions +open import foundation.sets +open import foundation.transport-along-identifications +open import foundation.universe-levels +``` + + + +## Idea + +{{#concept "Diagonal integer fractions" Agda=diagonal-fraction-ℤ}} are +[integer fractions](elementary-number-theory.integer-fractions.md) of the form +`k/k`. + +## Definition + +```agda +is-diagonal-prop-fraction-ℤ : fraction-ℤ → Prop lzero +is-diagonal-prop-fraction-ℤ (p , q , _) = Id-Prop ℤ-Set p q + +is-diagonal-fraction-ℤ : fraction-ℤ → UU lzero +is-diagonal-fraction-ℤ (p , q , _) = p ＝ q + +in-diagonal-fraction-ℤ : ℤ⁺ → fraction-ℤ +in-diagonal-fraction-ℤ k⁺@(k , _) = (k , k⁺) + +is-diagonal-in-diagonal-fraction-ℤ : + (k : ℤ⁺) → is-diagonal-fraction-ℤ (in-diagonal-fraction-ℤ k) +is-diagonal-in-diagonal-fraction-ℤ _ = refl +``` + +## Properties + +### A fraction is diagonal if and only if it is similar to 1 + +```agda +abstract + sim-one-is-diagonal-fraction-ℤ : + (p : fraction-ℤ) → + is-diagonal-fraction-ℤ p → sim-fraction-ℤ p one-fraction-ℤ + sim-one-is-diagonal-fraction-ℤ (p , _ , _) refl = + commutative-mul-ℤ p one-ℤ + + is-diagonal-sim-one-fraction-ℤ : + (p : fraction-ℤ) → + sim-fraction-ℤ p one-fraction-ℤ → + is-diagonal-fraction-ℤ p + is-diagonal-sim-one-fraction-ℤ (p , q , _) p~q = + equational-reasoning + p + ＝ p *ℤ one-ℤ + by inv (right-unit-law-mul-ℤ p) + ＝ one-ℤ *ℤ q + by p~q + ＝ q + by left-unit-law-mul-ℤ q +``` + +### Multiplying a fraction by a diagonal fraction results in a similar fraction + +```agda +abstract + sim-right-mul-diagonal-fraction-ℤ : + (p q : fraction-ℤ) → is-diagonal-fraction-ℤ q → + sim-fraction-ℤ (p *fraction-ℤ q) p + sim-right-mul-diagonal-fraction-ℤ p (q , .q , pos-q) refl = + transitive-sim-fraction-ℤ + ( p *fraction-ℤ (q , q , pos-q)) + ( p *fraction-ℤ one-fraction-ℤ) + ( p) + ( right-unit-law-mul-fraction-ℤ p) + ( sim-fraction-mul-fraction-ℤ + ( refl) + ( sim-one-is-diagonal-fraction-ℤ _ refl)) + + sim-left-mul-diagonal-fraction-ℤ : + (p q : fraction-ℤ) → is-diagonal-fraction-ℤ p → + sim-fraction-ℤ (p *fraction-ℤ q) q + sim-left-mul-diagonal-fraction-ℤ p q H = + transitive-sim-fraction-ℤ + ( p *fraction-ℤ q) + ( q *fraction-ℤ p) + ( q) + ( sim-right-mul-diagonal-fraction-ℤ q p H) + ( commutative-mul-fraction-ℤ p q) +``` diff --git a/src/elementary-number-theory/inequality-integer-fractions.lagda.md b/src/elementary-number-theory/inequality-integer-fractions.lagda.md index 4da09c34b85..0d14917b751 100644 --- a/src/elementary-number-theory/inequality-integer-fractions.lagda.md +++ b/src/elementary-number-theory/inequality-integer-fractions.lagda.md @@ -59,8 +59,9 @@ leq-fraction-ℤ-Prop (m , n , p) (m' , n' , p') = leq-fraction-ℤ : fraction-ℤ → fraction-ℤ → UU lzero leq-fraction-ℤ x y = type-Prop (leq-fraction-ℤ-Prop x y) -is-prop-leq-fraction-ℤ : (x y : fraction-ℤ) → is-prop (leq-fraction-ℤ x y) -is-prop-leq-fraction-ℤ x y = is-prop-type-Prop (leq-fraction-ℤ-Prop x y) +abstract + is-prop-leq-fraction-ℤ : (x y : fraction-ℤ) → is-prop (leq-fraction-ℤ x y) + is-prop-leq-fraction-ℤ x y = is-prop-type-Prop (leq-fraction-ℤ-Prop x y) ``` ## Properties @@ -89,42 +90,44 @@ module _ (x y : fraction-ℤ) where - is-sim-antisymmetric-leq-fraction-ℤ : - leq-fraction-ℤ x y → - leq-fraction-ℤ y x → - sim-fraction-ℤ x y - is-sim-antisymmetric-leq-fraction-ℤ H H' = - sim-is-zero-coss-mul-diff-fraction-ℤ x y - ( is-zero-is-nonnegative-is-nonpositive-ℤ - ( H) - ( is-nonpositive-eq-ℤ - ( skew-commutative-cross-mul-diff-fraction-ℤ y x) - ( is-nonpositive-neg-is-nonnegative-ℤ - ( H')))) + abstract + is-sim-antisymmetric-leq-fraction-ℤ : + leq-fraction-ℤ x y → + leq-fraction-ℤ y x → + sim-fraction-ℤ x y + is-sim-antisymmetric-leq-fraction-ℤ H H' = + sim-is-zero-coss-mul-diff-fraction-ℤ x y + ( is-zero-is-nonnegative-is-nonpositive-ℤ + ( H) + ( is-nonpositive-eq-ℤ + ( skew-commutative-cross-mul-diff-fraction-ℤ y x) + ( is-nonpositive-neg-is-nonnegative-ℤ + ( H')))) ``` ### Inequality on integer fractions is transitive ```agda -transitive-leq-fraction-ℤ : - (p q r : fraction-ℤ) → - leq-fraction-ℤ q r → - leq-fraction-ℤ p q → - leq-fraction-ℤ p r -transitive-leq-fraction-ℤ p q r H H' = - is-nonnegative-right-factor-mul-ℤ - ( is-nonnegative-eq-ℤ - ( lemma-add-cross-mul-diff-fraction-ℤ p q r) - ( is-nonnegative-add-ℤ - ( is-nonnegative-mul-ℤ - ( is-nonnegative-is-positive-ℤ - ( is-positive-denominator-fraction-ℤ p)) - ( H)) - ( is-nonnegative-mul-ℤ - ( is-nonnegative-is-positive-ℤ - ( is-positive-denominator-fraction-ℤ r)) - ( H')))) - ( is-positive-denominator-fraction-ℤ q) +abstract + transitive-leq-fraction-ℤ : + (p q r : fraction-ℤ) → + leq-fraction-ℤ q r → + leq-fraction-ℤ p q → + leq-fraction-ℤ p r + transitive-leq-fraction-ℤ p q r H H' = + is-nonnegative-right-factor-mul-ℤ + ( is-nonnegative-eq-ℤ + ( lemma-add-cross-mul-diff-fraction-ℤ p q r) + ( is-nonnegative-add-ℤ + ( is-nonnegative-mul-ℤ + ( is-nonnegative-is-positive-ℤ + ( is-positive-denominator-fraction-ℤ p)) + ( H)) + ( is-nonnegative-mul-ℤ + ( is-nonnegative-is-positive-ℤ + ( is-positive-denominator-fraction-ℤ r)) + ( H')))) + ( is-positive-denominator-fraction-ℤ q) ``` ### Chaining rules for similarity and inequality on the integer fractions @@ -134,31 +137,34 @@ module _ (p q r : fraction-ℤ) where - concatenate-sim-leq-fraction-ℤ : - sim-fraction-ℤ p q → - leq-fraction-ℤ q r → - leq-fraction-ℤ p r - concatenate-sim-leq-fraction-ℤ H H' = - is-nonnegative-right-factor-mul-ℤ - ( is-nonnegative-eq-ℤ - ( lemma-left-sim-cross-mul-diff-fraction-ℤ p q r H) - ( is-nonnegative-mul-ℤ - ( is-nonnegative-is-positive-ℤ (is-positive-denominator-fraction-ℤ p)) - ( H'))) - ( is-positive-denominator-fraction-ℤ q) - - concatenate-leq-sim-fraction-ℤ : - leq-fraction-ℤ p q → - sim-fraction-ℤ q r → - leq-fraction-ℤ p r - concatenate-leq-sim-fraction-ℤ H H' = - is-nonnegative-right-factor-mul-ℤ - ( is-nonnegative-eq-ℤ - ( inv (lemma-right-sim-cross-mul-diff-fraction-ℤ p q r H')) - ( is-nonnegative-mul-ℤ - ( is-nonnegative-is-positive-ℤ (is-positive-denominator-fraction-ℤ r)) - ( H))) - ( is-positive-denominator-fraction-ℤ q) + abstract + concatenate-sim-leq-fraction-ℤ : + sim-fraction-ℤ p q → + leq-fraction-ℤ q r → + leq-fraction-ℤ p r + concatenate-sim-leq-fraction-ℤ H H' = + is-nonnegative-right-factor-mul-ℤ + ( is-nonnegative-eq-ℤ + ( lemma-left-sim-cross-mul-diff-fraction-ℤ p q r H) + ( is-nonnegative-mul-ℤ + ( is-nonnegative-is-positive-ℤ + ( is-positive-denominator-fraction-ℤ p)) + ( H'))) + ( is-positive-denominator-fraction-ℤ q) + + concatenate-leq-sim-fraction-ℤ : + leq-fraction-ℤ p q → + sim-fraction-ℤ q r → + leq-fraction-ℤ p r + concatenate-leq-sim-fraction-ℤ H H' = + is-nonnegative-right-factor-mul-ℤ + ( is-nonnegative-eq-ℤ + ( inv (lemma-right-sim-cross-mul-diff-fraction-ℤ p q r H')) + ( is-nonnegative-mul-ℤ + ( is-nonnegative-is-positive-ℤ + ( is-positive-denominator-fraction-ℤ r)) + ( H))) + ( is-positive-denominator-fraction-ℤ q) ``` ### The similarity of integer fractions preserves inequality @@ -168,11 +174,12 @@ module _ (p q p' q' : fraction-ℤ) (H : sim-fraction-ℤ p p') (K : sim-fraction-ℤ q q') where - preserves-leq-sim-fraction-ℤ : leq-fraction-ℤ p q → leq-fraction-ℤ p' q' - preserves-leq-sim-fraction-ℤ I = - concatenate-sim-leq-fraction-ℤ p' p q' - ( symmetric-sim-fraction-ℤ p p' H) - ( concatenate-leq-sim-fraction-ℤ p q q' I K) + abstract + preserves-leq-sim-fraction-ℤ : leq-fraction-ℤ p q → leq-fraction-ℤ p' q' + preserves-leq-sim-fraction-ℤ I = + concatenate-sim-leq-fraction-ℤ p' p q' + ( symmetric-sim-fraction-ℤ p p' H) + ( concatenate-leq-sim-fraction-ℤ p q q' I K) ``` ### `x ≤ y` if and only if `0 ≤ y - x` @@ -182,31 +189,33 @@ module _ (x y : fraction-ℤ) where - eq-translate-diff-leq-zero-fraction-ℤ : - leq-fraction-ℤ zero-fraction-ℤ (y +fraction-ℤ (neg-fraction-ℤ x)) ＝ - leq-fraction-ℤ x y - eq-translate-diff-leq-zero-fraction-ℤ = - ap - ( is-nonnegative-ℤ) - ( ( cross-mul-diff-zero-fraction-ℤ (y +fraction-ℤ (neg-fraction-ℤ x))) ∙ - ( ap - ( add-ℤ ( (numerator-fraction-ℤ y) *ℤ (denominator-fraction-ℤ x))) - ( left-negative-law-mul-ℤ - ( numerator-fraction-ℤ x) - ( denominator-fraction-ℤ y)))) + abstract + eq-translate-diff-leq-zero-fraction-ℤ : + leq-fraction-ℤ zero-fraction-ℤ (y +fraction-ℤ (neg-fraction-ℤ x)) ＝ + leq-fraction-ℤ x y + eq-translate-diff-leq-zero-fraction-ℤ = + ap + ( is-nonnegative-ℤ) + ( ( cross-mul-diff-zero-fraction-ℤ (y +fraction-ℤ (neg-fraction-ℤ x))) ∙ + ( ap + ( add-ℤ ( (numerator-fraction-ℤ y) *ℤ (denominator-fraction-ℤ x))) + ( left-negative-law-mul-ℤ + ( numerator-fraction-ℤ x) + ( denominator-fraction-ℤ y)))) ``` ### Negation reverses the order of inequality on integer fractions ```agda -neg-leq-fraction-ℤ : - (x y : fraction-ℤ) → - leq-fraction-ℤ x y → - leq-fraction-ℤ (neg-fraction-ℤ y) (neg-fraction-ℤ x) -neg-leq-fraction-ℤ (m , n , p) (m' , n' , p') H = - binary-tr - ( leq-ℤ) - ( inv (left-negative-law-mul-ℤ m' n)) - ( inv (left-negative-law-mul-ℤ m n')) - ( neg-leq-ℤ (m *ℤ n') (m' *ℤ n) H) +abstract + neg-leq-fraction-ℤ : + (x y : fraction-ℤ) → + leq-fraction-ℤ x y → + leq-fraction-ℤ (neg-fraction-ℤ y) (neg-fraction-ℤ x) + neg-leq-fraction-ℤ (m , n , p) (m' , n' , p') H = + binary-tr + ( leq-ℤ) + ( inv (left-negative-law-mul-ℤ m' n)) + ( inv (left-negative-law-mul-ℤ m n')) + ( neg-leq-ℤ (m *ℤ n') (m' *ℤ n) H) ``` diff --git a/src/elementary-number-theory/integer-fractions.lagda.md b/src/elementary-number-theory/integer-fractions.lagda.md index 3ee08916360..2bdb4b8904e 100644 --- a/src/elementary-number-theory/integer-fractions.lagda.md +++ b/src/elementary-number-theory/integer-fractions.lagda.md @@ -20,6 +20,7 @@ open import foundation.binary-relations open import foundation.cartesian-product-types open import foundation.decidable-equality open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types open import foundation.equivalence-relations open import foundation.identity-types open import foundation.negation @@ -110,6 +111,19 @@ neg-fraction-ℤ (d , n) = (neg-ℤ d , n) ## Properties +### Equality of integer fractions + +```agda +abstract + eq-fraction-ℤ : + (x y : fraction-ℤ) → + numerator-fraction-ℤ x ＝ numerator-fraction-ℤ y → + denominator-fraction-ℤ x ＝ denominator-fraction-ℤ y → + x ＝ y + eq-fraction-ℤ (p , q , pos-q) (_ , _ , _) refl refl = + eq-pair-eq-fiber (eq-pair-eq-fiber (eq-is-prop (is-prop-is-positive-ℤ q))) +``` + ### The double negation of an integer fraction is the original fraction ```agda diff --git a/src/elementary-number-theory/multiplication-integer-fractions.lagda.md b/src/elementary-number-theory/multiplication-integer-fractions.lagda.md index f5ae8d1b34a..b1bb99e498d 100644 --- a/src/elementary-number-theory/multiplication-integer-fractions.lagda.md +++ b/src/elementary-number-theory/multiplication-integer-fractions.lagda.md @@ -62,93 +62,98 @@ ap-mul-fraction-ℤ p q = ap-binary mul-fraction-ℤ p q ### Multiplication on integer fractions respects the similarity relation ```agda -sim-fraction-mul-fraction-ℤ : - {x x' y y' : fraction-ℤ} → - sim-fraction-ℤ x x' → - sim-fraction-ℤ y y' → - sim-fraction-ℤ (x *fraction-ℤ y) (x' *fraction-ℤ y') -sim-fraction-mul-fraction-ℤ - {(nx , dx , dxp)} {(nx' , dx' , dx'p)} - {(ny , dy , dyp)} {(ny' , dy' , dy'p)} p q = - equational-reasoning - (nx *ℤ ny) *ℤ (dx' *ℤ dy') - ＝ (nx *ℤ dx') *ℤ (ny *ℤ dy') - by interchange-law-mul-mul-ℤ nx ny dx' dy' - ＝ (nx' *ℤ dx) *ℤ (ny' *ℤ dy) - by ap-mul-ℤ p q - ＝ (nx' *ℤ ny') *ℤ (dx *ℤ dy) - by interchange-law-mul-mul-ℤ nx' dx ny' dy +abstract + sim-fraction-mul-fraction-ℤ : + {x x' y y' : fraction-ℤ} → + sim-fraction-ℤ x x' → + sim-fraction-ℤ y y' → + sim-fraction-ℤ (x *fraction-ℤ y) (x' *fraction-ℤ y') + sim-fraction-mul-fraction-ℤ + {(nx , dx , dxp)} {(nx' , dx' , dx'p)} + {(ny , dy , dyp)} {(ny' , dy' , dy'p)} p q = + equational-reasoning + (nx *ℤ ny) *ℤ (dx' *ℤ dy') + ＝ (nx *ℤ dx') *ℤ (ny *ℤ dy') + by interchange-law-mul-mul-ℤ nx ny dx' dy' + ＝ (nx' *ℤ dx) *ℤ (ny' *ℤ dy) + by ap-mul-ℤ p q + ＝ (nx' *ℤ ny') *ℤ (dx *ℤ dy) + by interchange-law-mul-mul-ℤ nx' dx ny' dy ``` ### Unit laws for multiplication on integer fractions ```agda -left-unit-law-mul-fraction-ℤ : - (k : fraction-ℤ) → - sim-fraction-ℤ (mul-fraction-ℤ one-fraction-ℤ k) k -left-unit-law-mul-fraction-ℤ k = refl - -right-unit-law-mul-fraction-ℤ : - (k : fraction-ℤ) → - sim-fraction-ℤ (mul-fraction-ℤ k one-fraction-ℤ) k -right-unit-law-mul-fraction-ℤ (n , d , p) = - ap-mul-ℤ (right-unit-law-mul-ℤ n) (inv (right-unit-law-mul-ℤ d)) +abstract + left-unit-law-mul-fraction-ℤ : + (k : fraction-ℤ) → + sim-fraction-ℤ (mul-fraction-ℤ one-fraction-ℤ k) k + left-unit-law-mul-fraction-ℤ k = refl + + right-unit-law-mul-fraction-ℤ : + (k : fraction-ℤ) → + sim-fraction-ℤ (mul-fraction-ℤ k one-fraction-ℤ) k + right-unit-law-mul-fraction-ℤ (n , d , p) = + ap-mul-ℤ (right-unit-law-mul-ℤ n) (inv (right-unit-law-mul-ℤ d)) ``` ### Multiplication on integer fractions is associative ```agda -associative-mul-fraction-ℤ : - (x y z : fraction-ℤ) → - sim-fraction-ℤ - (mul-fraction-ℤ (mul-fraction-ℤ x y) z) - (mul-fraction-ℤ x (mul-fraction-ℤ y z)) -associative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) = - ap-mul-ℤ (associative-mul-ℤ nx ny nz) (inv (associative-mul-ℤ dx dy dz)) +abstract + associative-mul-fraction-ℤ : + (x y z : fraction-ℤ) → + sim-fraction-ℤ + (mul-fraction-ℤ (mul-fraction-ℤ x y) z) + (mul-fraction-ℤ x (mul-fraction-ℤ y z)) + associative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) = + ap-mul-ℤ (associative-mul-ℤ nx ny nz) (inv (associative-mul-ℤ dx dy dz)) ``` ### Multiplication on integer fractions is commutative ```agda -commutative-mul-fraction-ℤ : - (x y : fraction-ℤ) → sim-fraction-ℤ (x *fraction-ℤ y) (y *fraction-ℤ x) -commutative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) = - ap-mul-ℤ (commutative-mul-ℤ nx ny) (commutative-mul-ℤ dy dx) +abstract + commutative-mul-fraction-ℤ : + (x y : fraction-ℤ) → sim-fraction-ℤ (x *fraction-ℤ y) (y *fraction-ℤ x) + commutative-mul-fraction-ℤ (nx , dx , dxp) (ny , dy , dyp) = + ap-mul-ℤ (commutative-mul-ℤ nx ny) (commutative-mul-ℤ dy dx) ``` ### Multiplication on integer fractions distributes on the left over addition ```agda -left-distributive-mul-add-fraction-ℤ : - (x y z : fraction-ℤ) → - sim-fraction-ℤ - ( mul-fraction-ℤ x (add-fraction-ℤ y z)) - ( add-fraction-ℤ (mul-fraction-ℤ x y) (mul-fraction-ℤ x z)) -left-distributive-mul-add-fraction-ℤ - (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) = - ( ap - ( ( nx *ℤ (ny *ℤ dz +ℤ nz *ℤ dy)) *ℤ_) - ( ( interchange-law-mul-mul-ℤ dx dy dx dz) ∙ - ( associative-mul-ℤ dx dx (dy *ℤ dz)))) ∙ - ( interchange-law-mul-mul-ℤ - ( nx) - ( ny *ℤ dz +ℤ nz *ℤ dy) - ( dx) - ( dx *ℤ (dy *ℤ dz))) ∙ - ( inv - ( associative-mul-ℤ - ( nx *ℤ dx) +abstract + left-distributive-mul-add-fraction-ℤ : + (x y z : fraction-ℤ) → + sim-fraction-ℤ + ( mul-fraction-ℤ x (add-fraction-ℤ y z)) + ( add-fraction-ℤ (mul-fraction-ℤ x y) (mul-fraction-ℤ x z)) + left-distributive-mul-add-fraction-ℤ + (nx , dx , dxp) (ny , dy , dyp) (nz , dz , dzp) = + ( ap + ( ( nx *ℤ (ny *ℤ dz +ℤ nz *ℤ dy)) *ℤ_) + ( ( interchange-law-mul-mul-ℤ dx dy dx dz) ∙ + ( associative-mul-ℤ dx dx (dy *ℤ dz)))) ∙ + ( interchange-law-mul-mul-ℤ + ( nx) ( ny *ℤ dz +ℤ nz *ℤ dy) - ( dx *ℤ (dy *ℤ dz)))) ∙ - ( ap - ( _*ℤ (dx *ℤ (dy *ℤ dz))) - ( ( left-distributive-mul-add-ℤ + ( dx) + ( dx *ℤ (dy *ℤ dz))) ∙ + ( inv + ( associative-mul-ℤ ( nx *ℤ dx) - ( ny *ℤ dz) - ( nz *ℤ dy)) ∙ - ( ap-add-ℤ - ( interchange-law-mul-mul-ℤ nx dx ny dz)) - ( interchange-law-mul-mul-ℤ nx dx nz dy))) + ( ny *ℤ dz +ℤ nz *ℤ dy) + ( dx *ℤ (dy *ℤ dz)))) ∙ + ( ap + ( _*ℤ (dx *ℤ (dy *ℤ dz))) + ( ( left-distributive-mul-add-ℤ + ( nx *ℤ dx) + ( ny *ℤ dz) + ( nz *ℤ dy)) ∙ + ( ap-add-ℤ + ( interchange-law-mul-mul-ℤ nx dx ny dz)) + ( interchange-law-mul-mul-ℤ nx dx nz dy))) ``` ### The inclusion of integers preserves multiplication diff --git a/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md b/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md index c2f96f0721e..696d2c991f9 100644 --- a/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md +++ b/src/elementary-number-theory/multiplication-positive-and-negative-integers.lagda.md @@ -15,14 +15,17 @@ open import elementary-number-theory.natural-numbers open import elementary-number-theory.negative-integers open import elementary-number-theory.nonnegative-integers open import elementary-number-theory.nonpositive-integers +open import elementary-number-theory.nonzero-natural-numbers open import elementary-number-theory.positive-and-negative-integers open import elementary-number-theory.positive-integers open import elementary-number-theory.strict-inequality-integers +open import foundation.action-on-identifications-functions open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.empty-types open import foundation.identity-types +open import foundation.injective-maps open import foundation.transport-along-identifications open import foundation.unit-type ``` @@ -367,6 +370,10 @@ int-mul-nonpositive-ℤ' x y = y *ℤ int-nonpositive-ℤ x ```agda mul-positive-ℤ : positive-ℤ → positive-ℤ → positive-ℤ mul-positive-ℤ (x , H) (y , K) = (mul-ℤ x y , is-positive-mul-ℤ H K) + +infixl 40 _*ℤ⁺_ +_*ℤ⁺_ : ℤ⁺ → ℤ⁺ → ℤ⁺ +_*ℤ⁺_ = mul-positive-ℤ ``` ### Multiplication of nonnegative integers @@ -454,3 +461,43 @@ module _ ( right-distributive-mul-diff-ℤ y x (int-nonnegative-ℤ z)) ( is-nonnegative-mul-ℤ K (is-nonnegative-int-nonnegative-ℤ z)) ``` + +### The canonical embedding of positive integers in the nonzero natural numbers preserves multiplication + +```agda +abstract + mul-positive-nat-ℤ⁺ : + (k l : ℤ⁺) → + positive-nat-ℤ⁺ k *ℕ⁺ positive-nat-ℤ⁺ l ＝ positive-nat-ℤ⁺ (k *ℤ⁺ l) + mul-positive-nat-ℤ⁺ k⁺@(k , _) l⁺@(l , _) = + inv + ( is-injective-is-equiv + ( is-equiv-positive-int-ℕ⁺) + ( ( is-section-positive-nat-ℤ⁺ _) ∙ + ( eq-ℤ⁺ + ( k⁺ *ℤ⁺ l⁺) + ( positive-int-ℕ⁺ (positive-nat-ℤ⁺ k⁺ *ℕ⁺ positive-nat-ℤ⁺ l⁺)) + ( equational-reasoning + k *ℤ l + ＝ + int-ℕ (nat-ℕ⁺ (positive-nat-ℤ⁺ k⁺)) *ℤ + int-ℕ (nat-ℕ⁺ (positive-nat-ℤ⁺ l⁺)) + by + ap-mul-ℤ + ( inv (ap int-ℤ⁺ (is-section-positive-nat-ℤ⁺ k⁺))) + ( inv (ap int-ℤ⁺ (is-section-positive-nat-ℤ⁺ l⁺))) + ＝ + int-ℕ (nat-ℕ⁺ (positive-nat-ℤ⁺ k⁺ *ℕ⁺ positive-nat-ℤ⁺ l⁺)) + by + mul-int-ℕ + ( nat-ℕ⁺ (positive-nat-ℤ⁺ k⁺)) + ( nat-ℕ⁺ (positive-nat-ℤ⁺ l⁺)))))) +``` + +### Multiplication of positive integers is commutative + +```agda +abstract + commutative-mul-ℤ⁺ : (k l : ℤ⁺) → k *ℤ⁺ l ＝ l *ℤ⁺ k + commutative-mul-ℤ⁺ (k , _) (l , _) = eq-ℤ⁺ _ _ (commutative-mul-ℤ k l) +``` diff --git a/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md b/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md index 492703832cb..2996ffbd8ac 100644 --- a/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md +++ b/src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md @@ -348,6 +348,27 @@ abstract ( le-left-mul-greater-than-one-ℚ⁺ p 1

Imports diff --git a/src/metric-spaces/dense-subsets-metric-spaces.lagda.md b/src/metric-spaces/dense-subsets-metric-spaces.lagda.md index 307f1829908..5b8be946001 100644 --- a/src/metric-spaces/dense-subsets-metric-spaces.lagda.md +++ b/src/metric-spaces/dense-subsets-metric-spaces.lagda.md @@ -20,6 +20,7 @@ open import foundation.universe-levels open import metric-spaces.closure-subsets-metric-spaces open import metric-spaces.metric-spaces +open import metric-spaces.pointwise-continuous-functions-metric-spaces open import metric-spaces.subspaces-metric-spaces ``` @@ -46,6 +47,24 @@ module _ is-dense-subset-Metric-Space : UU (l1 ⊔ l2 ⊔ l3) is-dense-subset-Metric-Space = type-Prop is-dense-prop-subset-Metric-Space + +dense-subset-Metric-Space : + {l1 l2 : Level} (l3 : Level) (X : Metric-Space l1 l2) → UU (l1 ⊔ l2 ⊔ lsuc l3) +dense-subset-Metric-Space l3 X = + type-subtype (is-dense-prop-subset-Metric-Space {l3 = l3} X) + +module _ + {l1 l2 l3 : Level} + (X : Metric-Space l1 l2) + (S : dense-subset-Metric-Space l3 X) + where + + subset-dense-subset-Metric-Space : subset-Metric-Space l3 X + subset-dense-subset-Metric-Space = pr1 S + + is-dense-subset-dense-subset-Metric-Space : + is-dense-subset-Metric-Space X subset-dense-subset-Metric-Space + is-dense-subset-dense-subset-Metric-Space = pr2 S ``` ## Properties diff --git a/src/metric-spaces/limits-of-functions-metric-spaces.lagda.md b/src/metric-spaces/limits-of-functions-metric-spaces.lagda.md index 5e49e6ee82f..a574f273d93 100644 --- a/src/metric-spaces/limits-of-functions-metric-spaces.lagda.md +++ b/src/metric-spaces/limits-of-functions-metric-spaces.lagda.md @@ -9,11 +9,15 @@ module metric-spaces.limits-of-functions-metric-spaces where ```agda open import elementary-number-theory.positive-rational-numbers +open import foundation.axiom-of-countable-choice open import foundation.dependent-pair-types open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-propositional-truncation open import foundation.inhabited-subtypes open import foundation.propositional-truncations open import foundation.propositions +open import foundation.sets open import foundation.subtypes open import foundation.universe-levels @@ -71,3 +75,109 @@ module _ is-point-limit-function-Metric-Space = type-Prop is-point-limit-prop-function-Metric-Space ``` + +## The classical `(ε, δ)` definition of a limit + +The +{{#concept "classical definition of a limit" WDID=Q1042034 WD="(ε, δ)-definition of limit" Disambiguation="in a metric space" Agda=is-classical-limit-function-Metric-Space}} +states that the limit of `f x` as `x` approaches `x₀` is a `y` such that for any +`ε : ℚ⁺`, there [exists](foundation.existential-quantification.md) a `δ : ℚ⁺` +such that if `x` and `x₀` are in a `δ`-neighborhood of each other, `f x` and `y` +are in a `ε`-neighborhood of each other. + +The constructive definition implies the classical definition, but the other +direction requires the +[axiom of countable choice](foundation.axiom-of-countable-choice.md). + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + (x : type-Metric-Space X) + (y : type-Metric-Space Y) + where + + is-classical-limit-prop-function-Metric-Space : Prop (l1 ⊔ l2 ⊔ l4) + is-classical-limit-prop-function-Metric-Space = + Π-Prop + ( ℚ⁺) + ( λ ε → + ∃ ( ℚ⁺) + ( λ δ → + Π-Prop + ( type-Metric-Space X) + ( λ x' → + neighborhood-prop-Metric-Space X δ x x' ⇒ + neighborhood-prop-Metric-Space Y ε y (f x')))) + + is-classical-limit-function-Metric-Space : UU (l1 ⊔ l2 ⊔ l4) + is-classical-limit-function-Metric-Space = + type-Prop is-classical-limit-prop-function-Metric-Space +``` + +## Properties + +### Constructive limits are classical limits + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + (x : type-Metric-Space X) + (y : type-Metric-Space Y) + where + + abstract + is-classical-limit-is-limit-function-Metric-Space : + is-point-limit-function-Metric-Space X Y f x y → + is-classical-limit-function-Metric-Space X Y f x y + is-classical-limit-is-limit-function-Metric-Space H ε = + map-trunc-Prop (λ (μ , is-mod-μ) → (μ ε , is-mod-μ ε)) H +``` + +### Assuming countable choice, classical limits are constructive limits + +```agda +module _ + {l1 l2 l3 l4 : Level} + (acω : ACω) + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + (x : type-Metric-Space X) + (y : type-Metric-Space Y) + where + + abstract + is-limit-is-classical-limit-ACω-function-Metric-Space : + is-classical-limit-function-Metric-Space X Y f x y → + is-point-limit-function-Metric-Space X Y f x y + is-limit-is-classical-limit-ACω-function-Metric-Space H = + let + open + do-syntax-trunc-Prop + ( is-point-limit-prop-function-Metric-Space X Y f x y) + in do + μ ← + choice-countable-discrete-set-ACω + ( set-ℚ⁺) + ( is-countable-set-ℚ⁺) + ( has-decidable-equality-ℚ⁺) + ( acω) + ( λ ε → + Σ-Set + ( set-ℚ⁺) + ( λ δ → + set-Prop + ( Π-Prop + ( type-Metric-Space X) + ( λ x' → + neighborhood-prop-Metric-Space X δ x x' ⇒ + neighborhood-prop-Metric-Space Y ε y (f x'))))) + ( H) + intro-exists (pr1 ∘ μ) (pr2 ∘ μ) +``` diff --git a/src/metric-spaces/metric-space-of-rational-numbers.lagda.md b/src/metric-spaces/metric-space-of-rational-numbers.lagda.md index 6da9948861f..c90521d4ee2 100644 --- a/src/metric-spaces/metric-space-of-rational-numbers.lagda.md +++ b/src/metric-spaces/metric-space-of-rational-numbers.lagda.md @@ -12,6 +12,7 @@ module metric-spaces.metric-space-of-rational-numbers where open import elementary-number-theory.absolute-value-rational-numbers open import elementary-number-theory.addition-positive-rational-numbers open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.distance-rational-numbers open import elementary-number-theory.inequality-rational-numbers @@ -546,19 +547,19 @@ is-cauchy-approximation-rational-ℚ⁺ ε δ = ( rational-ℚ⁺ δ) ( rational-ℚ⁺ (ε +ℚ⁺ δ)) ( rational-ℚ⁺ ε +ℚ (rational-ℚ⁺ (ε +ℚ⁺ δ))) - ( le-right-add-ℚ⁺ + ( le-left-add-ℚ⁺ ( ε) ( ε +ℚ⁺ δ)) - ( le-right-add-ℚ⁺ ε δ))) , + ( le-left-add-ℚ⁺ ε δ))) , ( leq-le-ℚ ( transitive-le-ℚ ( rational-ℚ⁺ ε) ( rational-ℚ⁺ (ε +ℚ⁺ δ)) ( rational-ℚ⁺ δ +ℚ (rational-ℚ⁺ (ε +ℚ⁺ δ))) - ( le-right-add-ℚ⁺ + ( le-left-add-ℚ⁺ ( δ) ( ε +ℚ⁺ δ)) - ( le-left-add-ℚ⁺ ε δ))) + ( le-right-add-ℚ⁺ ε δ))) cauchy-approximation-rational-ℚ⁺ : cauchy-approximation-Metric-Space metric-space-ℚ @@ -582,7 +583,7 @@ is-zero-limit-rational-ℚ⁺ ε δ = ( inv-tr ( le-ℚ (rational-ℚ⁺ ε)) ( left-unit-law-add-ℚ (rational-ℚ⁺ (ε +ℚ⁺ δ))) - ( le-left-add-ℚ⁺ ε δ))) + ( le-right-add-ℚ⁺ ε δ))) convergent-rational-ℚ⁺ : convergent-cauchy-approximation-Metric-Space metric-space-ℚ @@ -591,3 +592,29 @@ convergent-rational-ℚ⁺ = zero-ℚ , is-zero-limit-rational-ℚ⁺ ``` + +### `x + d` is in a `d`-neighborhood of `x` + +```agda +abstract + neighborhood-add-ℚ : + (x : ℚ) (d : ℚ⁺) → neighborhood-ℚ d x (x +ℚ rational-ℚ⁺ d) + neighborhood-add-ℚ x d⁺@(d , _) = + ( refl-leq-ℚ (x +ℚ d) , + transitive-leq-ℚ x (x +ℚ d) (x +ℚ d +ℚ d) + ( leq-right-add-rational-ℚ⁺ (x +ℚ d) d⁺) + ( leq-right-add-rational-ℚ⁺ x d⁺)) +``` + +### `x - d` is in a `d`-neighborhood of `x` + +```agda +abstract + neighborhood-diff-ℚ : + (x : ℚ) (d : ℚ⁺) → neighborhood-ℚ d x (x -ℚ rational-ℚ⁺ d) + neighborhood-diff-ℚ x d⁺@(d , _) = + ( transitive-leq-ℚ (x -ℚ d) x (x +ℚ d) + ( leq-right-add-rational-ℚ⁺ x d⁺) + ( leq-transpose-right-add-ℚ _ _ _ (leq-right-add-rational-ℚ⁺ x d⁺)) , + inv-tr (leq-ℚ x) (is-section-diff-ℚ _ _) (refl-leq-ℚ x)) +``` diff --git a/src/metric-spaces/modulated-uniformly-continuous-functions-metric-spaces.lagda.md b/src/metric-spaces/modulated-uniformly-continuous-functions-metric-spaces.lagda.md index a505a4f9714..eb19b12fcf3 100644 --- a/src/metric-spaces/modulated-uniformly-continuous-functions-metric-spaces.lagda.md +++ b/src/metric-spaces/modulated-uniformly-continuous-functions-metric-spaces.lagda.md @@ -22,7 +22,7 @@ open import foundation.transport-along-identifications open import foundation.universe-levels open import metric-spaces.cartesian-products-metric-spaces -open import metric-spaces.continuous-functions-metric-spaces +open import metric-spaces.continuity-of-functions-at-points-in-metric-spaces open import metric-spaces.functions-metric-spaces open import metric-spaces.isometries-metric-spaces open import metric-spaces.metric-spaces diff --git a/src/metric-spaces/pointwise-continuous-functions-metric-spaces.lagda.md b/src/metric-spaces/pointwise-continuous-functions-metric-spaces.lagda.md new file mode 100644 index 00000000000..055c22e214f --- /dev/null +++ b/src/metric-spaces/pointwise-continuous-functions-metric-spaces.lagda.md @@ -0,0 +1,444 @@ +# Pointwise continuous functions in metric spaces + +```agda +module metric-spaces.pointwise-continuous-functions-metric-spaces where +``` + +
Imports + +```agda +open import elementary-number-theory.minimum-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers + +open import foundation.axiom-of-countable-choice +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.function-types +open import foundation.functoriality-cartesian-product-types +open import foundation.functoriality-propositional-truncation +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import metric-spaces.cartesian-products-metric-spaces +open import metric-spaces.continuity-of-functions-at-points-in-metric-spaces +open import metric-spaces.functions-metric-spaces +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.limits-of-functions-metric-spaces +open import metric-spaces.metric-spaces +open import metric-spaces.short-functions-metric-spaces +open import metric-spaces.uniformly-continuous-functions-metric-spaces +``` + +
+ +## Idea + +A +{{#concept "pointwise continuous function" Disambiguation="between metric spaces" Agda=pointwise-continuous-function-Metric-Space}} +from a [metric space](metric-spaces.metric-spaces.md) `X` to a metric space `Y` +is a function `f : X → Y` which is +[continuous at every point](metric-spaces.continuity-of-functions-at-points-in-metric-spaces.md) +in `X`. + +## Definition + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + where + + is-pointwise-continuous-prop-function-Metric-Space : Prop (l1 ⊔ l2 ⊔ l4) + is-pointwise-continuous-prop-function-Metric-Space = + Π-Prop + ( type-Metric-Space X) + ( is-continuous-at-point-prop-function-Metric-Space X Y f) + + is-pointwise-continuous-function-Metric-Space : UU (l1 ⊔ l2 ⊔ l4) + is-pointwise-continuous-function-Metric-Space = + type-Prop is-pointwise-continuous-prop-function-Metric-Space + +pointwise-continuous-function-Metric-Space : + {l1 l2 l3 l4 : Level} → Metric-Space l1 l2 → Metric-Space l3 l4 → + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) +pointwise-continuous-function-Metric-Space X Y = + type-subtype (is-pointwise-continuous-prop-function-Metric-Space X Y) + +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : pointwise-continuous-function-Metric-Space X Y) + where + + map-pointwise-continuous-function-Metric-Space : + type-function-Metric-Space X Y + map-pointwise-continuous-function-Metric-Space = pr1 f + + is-pointwise-continuous-map-pointwise-continuous-function-Metric-Space : + is-pointwise-continuous-function-Metric-Space + ( X) + ( Y) + ( map-pointwise-continuous-function-Metric-Space) + is-pointwise-continuous-map-pointwise-continuous-function-Metric-Space = pr2 f +``` + +### The classical definition of pointwise continuity + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + where + + is-classically-pointwise-continuous-prop-function-Metric-Space : + Prop (l1 ⊔ l2 ⊔ l4) + is-classically-pointwise-continuous-prop-function-Metric-Space = + Π-Prop + ( type-Metric-Space X) + ( λ x → is-classical-limit-prop-function-Metric-Space X Y f x (f x)) + + is-classically-pointwise-continuous-function-Metric-Space : UU (l1 ⊔ l2 ⊔ l4) + is-classically-pointwise-continuous-function-Metric-Space = + type-Prop is-classically-pointwise-continuous-prop-function-Metric-Space +``` + +## Properties + +### Constructively pointwise continuous functions are classically pointwise continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : pointwise-continuous-function-Metric-Space X Y) + where + + abstract + is-classically-pointwise-continuous-pointwise-continuous-function-Metric-Space : + is-classically-pointwise-continuous-function-Metric-Space + ( X) + ( Y) + ( map-pointwise-continuous-function-Metric-Space X Y f) + is-classically-pointwise-continuous-pointwise-continuous-function-Metric-Space + x = + is-classical-limit-is-limit-function-Metric-Space + ( X) + ( Y) + ( map-pointwise-continuous-function-Metric-Space X Y f) + ( x) + ( map-pointwise-continuous-function-Metric-Space X Y f x) + ( is-pointwise-continuous-map-pointwise-continuous-function-Metric-Space + ( X) + ( Y) + ( f) + ( x)) +``` + +### Assuming countable choice, classically pointwise continuous functions are continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (acω : ACω) + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (f : type-function-Metric-Space X Y) + where + + abstract + is-pointwise-continuous-is-classically-pointwise-continuous-ACω-function-Metric-Space : + is-classically-pointwise-continuous-function-Metric-Space X Y f → + is-pointwise-continuous-function-Metric-Space X Y f + is-pointwise-continuous-is-classically-pointwise-continuous-ACω-function-Metric-Space + H x = + is-limit-is-classical-limit-ACω-function-Metric-Space + ( acω) + ( X) + ( Y) + ( f) + ( x) + ( f x) + ( H x) +``` + +### The Cartesian product of pointwise continuous functions on metric spaces + +```agda +module _ + {l1 l2 l3 l4 l5 l6 l7 l8 : Level} + (A : Metric-Space l1 l2) (B : Metric-Space l3 l4) + (C : Metric-Space l5 l6) (D : Metric-Space l7 l8) + (f : pointwise-continuous-function-Metric-Space A B) + (g : pointwise-continuous-function-Metric-Space C D) + where + + map-product-pointwise-continuous-function-Metric-Space : + type-Metric-Space A × type-Metric-Space C → + type-Metric-Space B × type-Metric-Space D + map-product-pointwise-continuous-function-Metric-Space = + map-product + ( map-pointwise-continuous-function-Metric-Space A B f) + ( map-pointwise-continuous-function-Metric-Space C D g) + + abstract + is-pointwise-continuous-map-product-pointwise-continuous-function-Metric-Space : + is-pointwise-continuous-function-Metric-Space + ( product-Metric-Space A C) + ( product-Metric-Space B D) + ( map-product-pointwise-continuous-function-Metric-Space) + is-pointwise-continuous-map-product-pointwise-continuous-function-Metric-Space + ( a , c) = + let + open + do-syntax-trunc-Prop + ( is-point-limit-prop-function-Metric-Space + ( product-Metric-Space A C) + ( product-Metric-Space B D) + ( map-product-pointwise-continuous-function-Metric-Space) + ( a , c) + ( map-product-pointwise-continuous-function-Metric-Space (a , c))) + in do + (μf , is-mod-μf) ← + is-pointwise-continuous-map-pointwise-continuous-function-Metric-Space + ( A) + ( B) + ( f) + ( a) + (μg , is-mod-μg) ← + is-pointwise-continuous-map-pointwise-continuous-function-Metric-Space + ( C) + ( D) + ( g) + ( c) + intro-exists + ( λ ε → min-ℚ⁺ (μf ε) (μg ε)) + ( λ ε (a' , c') (Naa' , Ncc') → + ( is-mod-μf + ( ε) + ( a') + ( weakly-monotonic-neighborhood-Metric-Space + ( A) + ( a) + ( a') + ( min-ℚ⁺ (μf ε) (μg ε)) + ( μf ε) + ( leq-left-min-ℚ⁺ (μf ε) (μg ε)) + ( Naa')) , + is-mod-μg + ( ε) + ( c') + ( weakly-monotonic-neighborhood-Metric-Space + ( C) + ( c) + ( c') + ( min-ℚ⁺ (μf ε) (μg ε)) + ( μg ε) + ( leq-right-min-ℚ⁺ (μf ε) (μg ε)) + ( Ncc')))) + + product-pointwise-continuous-function-Metric-Space : + pointwise-continuous-function-Metric-Space + ( product-Metric-Space A C) + ( product-Metric-Space B D) + product-pointwise-continuous-function-Metric-Space = + ( map-product-pointwise-continuous-function-Metric-Space , + is-pointwise-continuous-map-product-pointwise-continuous-function-Metric-Space) +``` + +### The composition of pointwise continuous functions + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (Z : Metric-Space l5 l6) + (f : pointwise-continuous-function-Metric-Space Y Z) + (g : pointwise-continuous-function-Metric-Space X Y) + where + + map-comp-pointwise-continuous-function-Metric-Space : + type-function-Metric-Space X Z + map-comp-pointwise-continuous-function-Metric-Space = + map-pointwise-continuous-function-Metric-Space Y Z f ∘ + map-pointwise-continuous-function-Metric-Space X Y g + + abstract + is-pointwise-continuous-map-comp-pointwise-continuous-function-Metric-Space : + is-pointwise-continuous-function-Metric-Space X Z + ( map-comp-pointwise-continuous-function-Metric-Space) + is-pointwise-continuous-map-comp-pointwise-continuous-function-Metric-Space + x = + let + open + do-syntax-trunc-Prop + ( is-point-limit-prop-function-Metric-Space X Z + ( map-comp-pointwise-continuous-function-Metric-Space) + ( x) + ( map-comp-pointwise-continuous-function-Metric-Space x)) + in do + (μg , is-mod-μg) ← + is-pointwise-continuous-map-pointwise-continuous-function-Metric-Space + ( X) + ( Y) + ( g) + ( x) + (μf , is-mod-μf) ← + is-pointwise-continuous-map-pointwise-continuous-function-Metric-Space + ( Y) + ( Z) + ( f) + ( map-pointwise-continuous-function-Metric-Space X Y g x) + intro-exists + ( μg ∘ μf) + ( λ ε x' Nxx' → + is-mod-μf + ( ε) + ( map-pointwise-continuous-function-Metric-Space X Y g x') + ( is-mod-μg (μf ε) x' Nxx')) + + comp-pointwise-continuous-function-Metric-Space : + pointwise-continuous-function-Metric-Space X Z + comp-pointwise-continuous-function-Metric-Space = + ( map-comp-pointwise-continuous-function-Metric-Space , + is-pointwise-continuous-map-comp-pointwise-continuous-function-Metric-Space) +``` + +### Uniformly continuous functions are pointwise continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + where + + abstract + is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space : + (f : type-function-Metric-Space X Y) → + is-uniformly-continuous-function-Metric-Space X Y f → + is-pointwise-continuous-function-Metric-Space X Y f + is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space + f H x = map-trunc-Prop (λ (μ , is-mod-μ) → (μ , is-mod-μ x)) H + + pointwise-continuous-uniformly-continuous-function-Metric-Space : + uniformly-continuous-function-Metric-Space X Y → + pointwise-continuous-function-Metric-Space X Y + pointwise-continuous-uniformly-continuous-function-Metric-Space (f , H) = + ( f , + is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space f H) +``` + +### Short functions are pointwise continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + where + + abstract + is-pointwise-continuous-is-short-function-Metric-Space : + (f : type-function-Metric-Space X Y) → + is-short-function-Metric-Space X Y f → + is-pointwise-continuous-function-Metric-Space X Y f + is-pointwise-continuous-is-short-function-Metric-Space + f H = + is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space + ( X) + ( Y) + ( f) + ( is-uniformly-continuous-is-short-function-Metric-Space X Y f H) + + pointwise-continuous-short-function-Metric-Space : + short-function-Metric-Space X Y → + pointwise-continuous-function-Metric-Space X Y + pointwise-continuous-short-function-Metric-Space (f , H) = + ( f , + is-pointwise-continuous-is-short-function-Metric-Space f H) +``` + +### Isometries are pointwise continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + where + + abstract + is-pointwise-continuous-is-isometry-Metric-Space : + (f : type-function-Metric-Space X Y) → + is-isometry-Metric-Space X Y f → + is-pointwise-continuous-function-Metric-Space X Y f + is-pointwise-continuous-is-isometry-Metric-Space + f H = + is-pointwise-continuous-is-uniformly-continuous-function-Metric-Space + ( X) + ( Y) + ( f) + ( is-uniformly-continuous-is-isometry-Metric-Space X Y f H) + + pointwise-continuous-isometry-Metric-Space : + isometry-Metric-Space X Y → + pointwise-continuous-function-Metric-Space X Y + pointwise-continuous-isometry-Metric-Space (f , H) = + ( f , + is-pointwise-continuous-is-isometry-Metric-Space f H) +``` + +### Constant functions between metric spaces are pointwise continuous + +```agda +module _ + {l1 l2 l3 l4 : Level} + (X : Metric-Space l1 l2) + (Y : Metric-Space l3 l4) + (y : type-Metric-Space Y) + where + + abstract + is-pointwise-continuous-constant-function-Metric-Space : + is-pointwise-continuous-function-Metric-Space X Y (λ _ → y) + is-pointwise-continuous-constant-function-Metric-Space = + is-pointwise-continuous-is-short-function-Metric-Space X Y _ + ( is-short-constant-function-Metric-Space X Y y) + + pointwise-continuous-constant-function-Metric-Space : + pointwise-continuous-function-Metric-Space X Y + pointwise-continuous-constant-function-Metric-Space = + pointwise-continuous-short-function-Metric-Space X Y + ( short-constant-function-Metric-Space X Y y) +``` + +### The identity function is a pointwise continuous function on any metric space + +```agda +module _ + {l1 l2 : Level} + (X : Metric-Space l1 l2) + where + + abstract + is-pointwise-continuous-id-Metric-Space : + is-pointwise-continuous-function-Metric-Space X X id + is-pointwise-continuous-id-Metric-Space = + is-pointwise-continuous-is-isometry-Metric-Space X X id + ( is-isometry-id-Metric-Space X) + + pointwise-continuous-id-Metric-Space : + pointwise-continuous-function-Metric-Space X X + pointwise-continuous-id-Metric-Space = + ( id , is-pointwise-continuous-id-Metric-Space) +``` diff --git a/src/metric-spaces/rational-approximations-of-zero.lagda.md b/src/metric-spaces/rational-approximations-of-zero.lagda.md index 1af8b5b5d2a..c6ee20358a5 100644 --- a/src/metric-spaces/rational-approximations-of-zero.lagda.md +++ b/src/metric-spaces/rational-approximations-of-zero.lagda.md @@ -182,7 +182,7 @@ module _ ( f ε -ℚ zero-ℚ)) ( rational-ℚ⁺ ε) ( rational-ℚ⁺ (ε +ℚ⁺ δ)) - ( leq-le-ℚ⁺ {ε} {ε +ℚ⁺ δ} (le-left-add-ℚ⁺ ε δ)) + ( leq-le-ℚ⁺ {ε} {ε +ℚ⁺ δ} (le-right-add-ℚ⁺ ε δ)) ( inv-tr ( λ y → leq-ℚ (rational-ℚ⁰⁺ y) (rational-ℚ⁺ ε)) ( right-zero-law-dist-ℚ diff --git a/src/metric-spaces/saturated-rational-neighborhood-relations.lagda.md b/src/metric-spaces/saturated-rational-neighborhood-relations.lagda.md index 15a417ce7d2..3470843988f 100644 --- a/src/metric-spaces/saturated-rational-neighborhood-relations.lagda.md +++ b/src/metric-spaces/saturated-rational-neighborhood-relations.lagda.md @@ -209,5 +209,5 @@ module _ neighborhood-Rational-Neighborhood-Relation N δ x y) iff-le-neighborhood-saturated-monotonic-Rational-Neighborhood-Relation ε x y = ( λ Nxy δ ε<δ → monotonic-N x y ε δ ε<δ Nxy) , - ( λ H → saturated-N ε x y λ δ → H (ε +ℚ⁺ δ) (le-left-add-ℚ⁺ ε δ)) + ( λ H → saturated-N ε x y λ δ → H (ε +ℚ⁺ δ) (le-right-add-ℚ⁺ ε δ)) ``` diff --git a/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md b/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md index edbb096acc9..efdb75cd298 100644 --- a/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md +++ b/src/metric-spaces/uniformly-continuous-functions-metric-spaces.lagda.md @@ -23,7 +23,7 @@ open import foundation.universe-levels open import logic.functoriality-existential-quantification -open import metric-spaces.continuous-functions-metric-spaces +open import metric-spaces.continuity-of-functions-at-points-in-metric-spaces open import metric-spaces.functions-metric-spaces open import metric-spaces.isometries-metric-spaces open import metric-spaces.metric-spaces diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md index 243056dfe16..003c721677e 100644 --- a/src/real-numbers.lagda.md +++ b/src/real-numbers.lagda.md @@ -25,6 +25,7 @@ open import real-numbers.cauchy-sequences-real-numbers public open import real-numbers.closed-intervals-real-numbers public open import real-numbers.convergent-series-real-numbers public open import real-numbers.dedekind-real-numbers public +open import real-numbers.dense-subsets-real-numbers public open import real-numbers.difference-real-numbers public open import real-numbers.distance-real-numbers public open import real-numbers.enclosing-closed-rational-intervals-real-numbers public @@ -33,6 +34,7 @@ open import real-numbers.extensionality-multiplication-bilinear-form-real-number open import real-numbers.field-of-real-numbers public open import real-numbers.finitely-enumerable-subsets-real-numbers public open import real-numbers.geometric-sequences-real-numbers public +open import real-numbers.increasing-functions-real-numbers public open import real-numbers.inequalities-addition-and-subtraction-real-numbers public open import real-numbers.inequality-lower-dedekind-real-numbers public open import real-numbers.inequality-nonnegative-real-numbers public @@ -43,14 +45,19 @@ open import real-numbers.infima-and-suprema-families-real-numbers public open import real-numbers.infima-families-real-numbers public open import real-numbers.inhabited-finitely-enumerable-subsets-real-numbers public open import real-numbers.inhabited-totally-bounded-subsets-real-numbers public +open import real-numbers.integer-fraction-powers-positive-real-numbers public +open import real-numbers.integer-powers-positive-real-numbers public +open import real-numbers.invertibility-strictly-increasing-unbounded-continuous-functions-real-numbers public open import real-numbers.irrational-real-numbers public open import real-numbers.irrationality-square-root-of-two public open import real-numbers.isometry-addition-real-numbers public open import real-numbers.isometry-difference-real-numbers public open import real-numbers.isometry-negation-real-numbers public open import real-numbers.large-additive-group-of-real-numbers public +open import real-numbers.large-multiplicative-group-of-positive-real-numbers public open import real-numbers.large-multiplicative-monoid-of-real-numbers public open import real-numbers.large-ring-of-real-numbers public +open import real-numbers.limits-of-functions-real-numbers public open import real-numbers.limits-sequences-real-numbers public open import real-numbers.lipschitz-continuity-multiplication-real-numbers public open import real-numbers.local-ring-of-real-numbers public @@ -80,13 +87,21 @@ open import real-numbers.negation-lower-upper-dedekind-real-numbers public open import real-numbers.negation-real-numbers public open import real-numbers.negative-real-numbers public open import real-numbers.nonnegative-real-numbers public +open import real-numbers.nonzero-natural-roots-nonnegative-real-numbers public +open import real-numbers.nonzero-natural-roots-positive-real-numbers public open import real-numbers.nonzero-real-numbers public +open import real-numbers.odd-roots-nonnegative-real-numbers public +open import real-numbers.odd-roots-positive-real-numbers public +open import real-numbers.odd-roots-real-numbers public +open import real-numbers.pointwise-continuous-functions-real-numbers public open import real-numbers.positive-and-negative-real-numbers public open import real-numbers.positive-real-numbers public open import real-numbers.powers-real-numbers public open import real-numbers.proper-closed-intervals-real-numbers public open import real-numbers.raising-universe-levels-real-numbers public +open import real-numbers.rational-approximations-of-real-numbers public open import real-numbers.rational-lower-dedekind-real-numbers public +open import real-numbers.rational-powers-positive-real-numbers public open import real-numbers.rational-real-numbers public open import real-numbers.rational-upper-dedekind-real-numbers public open import real-numbers.real-numbers-from-lower-dedekind-real-numbers public @@ -106,10 +121,12 @@ open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbe open import real-numbers.strict-inequality-nonnegative-real-numbers public open import real-numbers.strict-inequality-positive-real-numbers public open import real-numbers.strict-inequality-real-numbers public +open import real-numbers.strictly-increasing-functions-real-numbers public open import real-numbers.subsets-real-numbers public open import real-numbers.suprema-families-real-numbers public open import real-numbers.totally-bounded-subsets-real-numbers public open import real-numbers.transposition-addition-subtraction-cuts-dedekind-real-numbers public +open import real-numbers.unbounded-functions-real-numbers public open import real-numbers.uniformly-continuous-functions-real-numbers public open import real-numbers.upper-dedekind-real-numbers public ``` diff --git a/src/real-numbers/addition-positive-real-numbers.lagda.md b/src/real-numbers/addition-positive-real-numbers.lagda.md index b56c02b5cb8..b24d21f5183 100644 --- a/src/real-numbers/addition-positive-real-numbers.lagda.md +++ b/src/real-numbers/addition-positive-real-numbers.lagda.md @@ -84,15 +84,19 @@ abstract opaque ( right-unit-law-add-ℝ x) ( preserves-le-left-add-ℝ x zero-ℝ d pos-d) -le-right-add-real-ℝ⁺ : - {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁺ l2) → le-ℝ x (real-ℝ⁺ d +ℝ x) -le-right-add-real-ℝ⁺ x d = - tr (le-ℝ x) (commutative-add-ℝ x (real-ℝ⁺ d)) (le-left-add-real-ℝ⁺ x d) - abstract + le-right-add-real-ℝ⁺ : + {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁺ l2) → le-ℝ x (real-ℝ⁺ d +ℝ x) + le-right-add-real-ℝ⁺ x d = + tr (le-ℝ x) (commutative-add-ℝ x (real-ℝ⁺ d)) (le-left-add-real-ℝ⁺ x d) + leq-left-add-real-ℝ⁺ : {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁺ l2) → leq-ℝ x (x +ℝ real-ℝ⁺ d) leq-left-add-real-ℝ⁺ x d = leq-le-ℝ (le-left-add-real-ℝ⁺ x d) + + leq-right-add-real-ℝ⁺ : + {l1 l2 : Level} → (x : ℝ l1) (d : ℝ⁺ l2) → leq-ℝ x (real-ℝ⁺ d +ℝ x) + leq-right-add-real-ℝ⁺ x d = leq-le-ℝ (le-right-add-real-ℝ⁺ x d) ``` ### Subtraction by a positive real number is a strictly deflationary map diff --git a/src/real-numbers/dense-subsets-real-numbers.lagda.md b/src/real-numbers/dense-subsets-real-numbers.lagda.md new file mode 100644 index 00000000000..45128bdbb33 --- /dev/null +++ b/src/real-numbers/dense-subsets-real-numbers.lagda.md @@ -0,0 +1,416 @@ +# Dense subsets of the real numbers + +```agda +module real-numbers.dense-subsets-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.minimum-positive-rational-numbers +open import elementary-number-theory.positive-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.dependent-pair-types +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.intersections-subtypes +open import foundation.propositional-truncations +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import logic.functoriality-existential-quantification + +open import metric-spaces.dense-subsets-metric-spaces + +open import order-theory.large-posets + +open import real-numbers.addition-positive-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.negation-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.rational-approximations-of-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers +open import real-numbers.strict-inequality-real-numbers +open import real-numbers.subsets-real-numbers +``` + +
+ +## Idea + +A {{#concept "dense subset" Disambiguation="of ℝ" Agda=dense-subset-ℝ}} of the +[real numbers](real-numbers.dedekind-real-numbers.md) `ℝ` is a +[dense subset](metric-spaces.dense-subsets-metric-spaces.md) of the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md), +which means that it is a [subset](real-numbers.subsets-real-numbers.md) `S ⊆ ℝ` +such that for any `x : ℝ` and any +[positive rational](elementary-number-theory.positive-rational-numbers.md) `ε`, +there is a `y` in an `ε`-neighborhood of `X` that is also in `S`. + +## Definition + +```agda +is-dense-subset-ℝ : {l1 l2 : Level} → subset-ℝ l1 l2 → UU (l1 ⊔ lsuc l2) +is-dense-subset-ℝ = is-dense-subset-Metric-Space (metric-space-ℝ _) + +dense-subset-ℝ : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +dense-subset-ℝ l1 l2 = dense-subset-Metric-Space l1 (metric-space-ℝ l2) + +subset-dense-subset-ℝ : {l1 l2 : Level} → dense-subset-ℝ l1 l2 → subset-ℝ l1 l2 +subset-dense-subset-ℝ = pr1 + +is-dense-subset-dense-subset-ℝ : + {l1 l2 : Level} (S : dense-subset-ℝ l1 l2) (x : ℝ l2) (ε : ℚ⁺) → + intersect-subtype (neighborhood-prop-ℝ l2 ε x) (subset-dense-subset-ℝ S) +is-dense-subset-dense-subset-ℝ = pr2 + +type-dense-subset-ℝ : {l1 l2 : Level} → dense-subset-ℝ l1 l2 → UU (l1 ⊔ lsuc l2) +type-dense-subset-ℝ S = type-subtype (subset-dense-subset-ℝ S) + +inclusion-dense-subset-ℝ : + {l1 l2 : Level} (S : dense-subset-ℝ l1 l2) → + type-dense-subset-ℝ S → ℝ l2 +inclusion-dense-subset-ℝ S = inclusion-subtype (subset-dense-subset-ℝ S) + +is-in-dense-subset-ℝ : {l1 l2 : Level} → dense-subset-ℝ l1 l2 → ℝ l2 → UU l1 +is-in-dense-subset-ℝ S = + is-in-subtype (subset-dense-subset-ℝ S) +``` + +## Properties + +### The rational reals are dense in `ℝ` + +```agda +abstract + is-dense-rational-real-ℝ : + (l : Level) → is-dense-subset-ℝ (subtype-rational-real {l}) + is-dense-rational-real-ℝ l x ε = + map-exists + ( _) + ( raise-real-ℚ l) + ( λ q Nεxq → ( Nεxq , q , is-rational-raise-real-ℚ l q)) + ( exists-rational-approximation-ℝ x ε) + +dense-subset-rational-real-ℝ : + (l : Level) → dense-subset-ℝ l l +dense-subset-rational-real-ℝ l = + ( subtype-rational-real , is-dense-rational-real-ℝ l) +``` + +### Given a dense subset `S ⊆ R`, two reals `x < y`, and positive rationals `δx`, `δy`, there are `x' < y'` with `x' ∈ S`, `y' ∈ S`, `x'` in a `δx`-neighborhood of `x` and correspondingly for `y` + +```agda +module _ + {l1 l2 : Level} + (S : dense-subset-ℝ l1 l2) + where + + abstract + exist-close-le-elements-dense-subset-ℝ : + {x y : ℝ l2} (δx δy : ℚ⁺) → le-ℝ x y → + exists + ( type-dense-subset-ℝ S × type-dense-subset-ℝ S) + ( λ ((x' , x'∈S) , (y' , y'∈S)) → + ( le-prop-ℝ x' y') ∧ + ( neighborhood-prop-ℝ l2 δx x x') ∧ + ( neighborhood-prop-ℝ l2 δy y y')) + exist-close-le-elements-dense-subset-ℝ {x = x} {y = y} δx δy xImports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.inequality-rational-numbers +open import elementary-number-theory.minimum-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.coproduct-types +open import foundation.dependent-pair-types +open import foundation.double-negation +open import foundation.empty-types +open import foundation.function-types +open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.universe-levels + +open import order-theory.large-posets +open import order-theory.order-preserving-maps-posets +open import order-theory.posets +open import order-theory.subposets + +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.dense-subsets-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.pointwise-continuous-functions-real-numbers +open import real-numbers.rational-approximations-of-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers +open import real-numbers.strict-inequality-real-numbers +open import real-numbers.subsets-real-numbers +``` + + + +## Idea + +A function `f` from the [real numbers](real-numbers.dedekind-real-numbers.md) to +themselves is +{{#concept "increasing" Disambiguation="function from ℝ to ℝ" Agda=is-increasing-function-ℝ}} +if for all `x ≤ y`, `f x ≤ f y`; in other words, it is an +[order-preserving map](order-theory.order-preserving-maps-posets.md) on the +[poset of real numbers](real-numbers.inequality-real-numbers.md). + +Several arguments on this page are due to +[Mark Saving](https://math.stackexchange.com/users/798694/mark-saving) in this +Mathematics Stack Exchange answer: . + +## Definition + +```agda +is-increasing-prop-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → Prop (lsuc l1 ⊔ l2) +is-increasing-prop-function-ℝ {l1} {l2} = + preserves-order-prop-Poset (ℝ-Poset l1) (ℝ-Poset l2) + +is-increasing-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → UU (lsuc l1 ⊔ l2) +is-increasing-function-ℝ f = type-Prop (is-increasing-prop-function-ℝ f) + +is-increasing-on-subset-function-ℝ : + {l1 l2 l3 : Level} (f : ℝ l1 → ℝ l2) (S : subset-ℝ l3 l1) → + UU (lsuc l1 ⊔ l2 ⊔ l3) +is-increasing-on-subset-function-ℝ f S = + preserves-order-Poset + ( poset-Subposet (ℝ-Poset _) S) + ( ℝ-Poset _) + ( f ∘ inclusion-subset-ℝ S) +``` + +## Properties + +### If `x < y` implies `f x ≤ f y`, then `f` is increasing + +```agda +module _ + {l1 l2 : Level} + (f : ℝ l1 → ℝ l2) + where + + abstract + is-increasing-leq-le-ℝ : + ((x y : ℝ l1) → le-ℝ x y → leq-ℝ (f x) (f y)) → + is-increasing-function-ℝ f + is-increasing-leq-le-ℝ H x y x≤y = + double-negation-elim-leq-ℝ + ( f x) + ( f y) + ( map-double-negation + ( rec-coproduct + ( λ x~y → leq-eq-ℝ (ap f (eq-sim-ℝ x~y))) + ( H x y)) + ( irrefutable-sim-or-le-leq-ℝ x y x≤y)) + +module _ + {l1 l2 l3 : Level} + (f : ℝ l1 → ℝ l2) + (S : subset-ℝ l3 l1) + where + + abstract + is-increasing-leq-le-on-subset-function-ℝ : + ( ((x y : type-subset-ℝ S) → + le-ℝ (pr1 x) (pr1 y) → leq-ℝ (f (pr1 x)) (f (pr1 y)))) → + is-increasing-on-subset-function-ℝ f S + is-increasing-leq-le-on-subset-function-ℝ H (x , x∈S) (y , y∈S) x≤y = + double-negation-elim-leq-ℝ + ( f x) + ( f y) + ( map-double-negation + ( rec-coproduct + ( λ x~y → leq-eq-ℝ (ap f (eq-sim-ℝ x~y))) + ( H (x , x∈S) (y , y∈S))) + ( irrefutable-sim-or-le-leq-ℝ x y x≤y)) +``` + +### If a pointwise continuous function `f` is increasing on a dense subset of `ℝ`, then it is increasing on `ℝ` + +```agda +module _ + {l1 l2 l3 : Level} + (f : pointwise-continuous-function-ℝ l1 l2) + (S : dense-subset-ℝ l3 l1) + where + + abstract + is-increasing-is-increasing-dense-subset-pointwise-continuous-function-ℝ : + is-increasing-on-subset-function-ℝ + ( map-pointwise-continuous-function-ℝ f) + ( subset-dense-subset-ℝ S) → + is-increasing-function-ℝ (map-pointwise-continuous-function-ℝ f) + is-increasing-is-increasing-dense-subset-pointwise-continuous-function-ℝ H = + let + f' = map-pointwise-continuous-function-ℝ f + open do-syntax-trunc-Prop empty-Prop + open inequality-reasoning-Large-Poset ℝ-Large-Poset + in + is-increasing-leq-le-ℝ + ( map-pointwise-continuous-function-ℝ f) + ( λ x y xImports + +```agda +open import elementary-number-theory.addition-integer-fractions +open import elementary-number-theory.addition-integers +open import elementary-number-theory.diagonal-integer-fractions +open import elementary-number-theory.integer-fractions +open import elementary-number-theory.integers +open import elementary-number-theory.multiplication-integer-fractions +open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.multiplication-positive-and-negative-integers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers +open import elementary-number-theory.positive-integers +open import elementary-number-theory.reduced-integer-fractions + +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.universe-levels + +open import real-numbers.integer-powers-positive-real-numbers +open import real-numbers.multiplication-positive-real-numbers +open import real-numbers.multiplicative-inverses-positive-real-numbers +open import real-numbers.nonzero-natural-roots-positive-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.powers-real-numbers +``` + + + +## Idea + +For any [positive](real-numbers.positive-real-numbers.md) +[real number](real-numbers.dedekind-real-numbers.md) `x` and any +[integer fraction](elementary-number-theory.integer-fractions.md) `p/q`, we can +define the +{{#concept "power operation" Disambiguation="positive real numbers to integer fraction powers" Agda=int-fraction-power-ℝ⁺}} +$x ↦ x^{p/q}$ to map `x` to the `q`th +[root](real-numbers.nonzero-natural-roots-positive-real-numbers.md) of the `p`th +[power](real-numbers.integer-powers-positive-real-numbers.md) of `x`. + +## Definition + +```agda +int-fraction-power-ℝ⁺ : {l : Level} → fraction-ℤ → ℝ⁺ l → ℝ⁺ l +int-fraction-power-ℝ⁺ (p , q⁺) x = + nonzero-nat-root-ℝ⁺ (positive-nat-ℤ⁺ q⁺) (int-power-ℝ⁺ p x) +``` + +## Properties + +### The canonical embedding of integers in the integer fractions preserves powers + +```agda +abstract + int-fraction-in-fraction-power-ℝ⁺ : + {l : Level} (k : ℤ) (x : ℝ⁺ l) → + int-fraction-power-ℝ⁺ (in-fraction-ℤ k) x ＝ int-power-ℝ⁺ k x + int-fraction-in-fraction-power-ℝ⁺ k x = + equational-reasoning + nonzero-nat-root-ℝ⁺ (positive-nat-ℤ⁺ one-ℤ⁺) (int-power-ℝ⁺ k x) + ＝ nonzero-nat-root-ℝ⁺ one-ℕ⁺ (int-power-ℝ⁺ k x) + by + ap + ( λ l → nonzero-nat-root-ℝ⁺ l (int-power-ℝ⁺ k x)) + ( eq-nonzero-ℕ (refl {x = 1})) + ＝ int-power-ℝ⁺ k x + by one-ℕ⁺-root-ℝ⁺ _ +``` + +### Powers by products of integer fractions are iterated integer fraction powers + +```agda +abstract + mul-int-fraction-power-ℝ⁺ : + {l : Level} (p q : fraction-ℤ) (x : ℝ⁺ l) → + int-fraction-power-ℝ⁺ (mul-fraction-ℤ p q) x ＝ + int-fraction-power-ℝ⁺ q (int-fraction-power-ℝ⁺ p x) + mul-int-fraction-power-ℝ⁺ (a , b⁺) (c , d⁺) x = + inv + ( equational-reasoning + nonzero-nat-root-ℝ⁺ + ( positive-nat-ℤ⁺ d⁺) + ( int-power-ℝ⁺ + ( c) + ( nonzero-nat-root-ℝ⁺ (positive-nat-ℤ⁺ b⁺) (int-power-ℝ⁺ a x))) + ＝ + nonzero-nat-root-ℝ⁺ + ( positive-nat-ℤ⁺ d⁺) + ( nonzero-nat-root-ℝ⁺ + ( positive-nat-ℤ⁺ b⁺) + ( int-power-ℝ⁺ c (int-power-ℝ⁺ a x))) + by + ap + ( nonzero-nat-root-ℝ⁺ (positive-nat-ℤ⁺ d⁺)) + ( inv (commute-root-int-power-ℝ⁺ (positive-nat-ℤ⁺ b⁺) c _)) + ＝ + nonzero-nat-root-ℝ⁺ + ( positive-nat-ℤ⁺ d⁺ *ℕ⁺ positive-nat-ℤ⁺ b⁺) + ( int-power-ℝ⁺ c (int-power-ℝ⁺ a x)) + by inv (mul-nonzero-nat-root-ℝ⁺ _ _ _) + ＝ + nonzero-nat-root-ℝ⁺ + ( positive-nat-ℤ⁺ (d⁺ *ℤ⁺ b⁺)) + ( int-power-ℝ⁺ c (int-power-ℝ⁺ a x)) + by + ap + ( λ k → nonzero-nat-root-ℝ⁺ k (int-power-ℝ⁺ c (int-power-ℝ⁺ a x))) + ( mul-positive-nat-ℤ⁺ d⁺ b⁺) + ＝ + nonzero-nat-root-ℝ⁺ + ( positive-nat-ℤ⁺ (d⁺ *ℤ⁺ b⁺)) + ( int-power-ℝ⁺ (a *ℤ c) x) + by + ap + ( nonzero-nat-root-ℝ⁺ _) + ( inv (int-power-mul-ℝ⁺ a c x)) + ＝ + nonzero-nat-root-ℝ⁺ + ( positive-nat-ℤ⁺ (b⁺ *ℤ⁺ d⁺)) + ( int-power-ℝ⁺ (a *ℤ c) x) + by + ap + ( λ k → + nonzero-nat-root-ℝ⁺ + ( positive-nat-ℤ⁺ k) + ( int-power-ℝ⁺ (a *ℤ c) x)) + ( commutative-mul-ℤ⁺ d⁺ b⁺)) +``` + +### Powers by diagonal integer fractions are the identity + +```agda +abstract + is-identity-power-diagonal-int-fraction-ℝ⁺ : + {l : Level} (k : fraction-ℤ) → is-diagonal-fraction-ℤ k → + (x : ℝ⁺ l) → int-fraction-power-ℝ⁺ k x ＝ x + is-identity-power-diagonal-int-fraction-ℝ⁺ (p , _ , pos-p) refl x = + let + n⁺@(n , _) = positive-nat-ℤ⁺ (p , pos-p) + in + equational-reasoning + nonzero-nat-root-ℝ⁺ n⁺ (int-power-ℝ⁺ p x) + ＝ nonzero-nat-root-ℝ⁺ n⁺ (int-power-ℝ⁺ (int-ℕ n) x) + by + ap + ( λ k → nonzero-nat-root-ℝ⁺ n⁺ (int-power-ℝ⁺ k x)) + ( inv (ap int-ℤ⁺ (is-section-positive-nat-ℤ⁺ (p , pos-p)))) + ＝ nonzero-nat-root-ℝ⁺ n⁺ (power-ℝ⁺ n x) + by ap (nonzero-nat-root-ℝ⁺ n⁺) (int-power-int-ℝ⁺ n x) + ＝ x + by is-retraction-nonzero-nat-power-ℝ⁺ n⁺ x +``` + +### Powers by integer fractions are equal to powers by reduced integer fractions + +```agda +abstract + reduce-int-fraction-power-ℝ⁺ : + {l : Level} (k : fraction-ℤ) (x : ℝ⁺ l) → + int-fraction-power-ℝ⁺ k x ＝ + int-fraction-power-ℝ⁺ (reduce-fraction-ℤ k) x + reduce-int-fraction-power-ℝ⁺ k x = + equational-reasoning + int-fraction-power-ℝ⁺ k x + ＝ + int-fraction-power-ℝ⁺ + ( reduce-fraction-ℤ k *fraction-ℤ diagonal-gcd-fraction-ℤ k) + ( x) + by + ap + ( λ p → int-fraction-power-ℝ⁺ p x) + ( eq-mul-reduce-diagonal-fraction-ℤ k) + ＝ + int-fraction-power-ℝ⁺ + ( diagonal-gcd-fraction-ℤ k) + ( int-fraction-power-ℝ⁺ (reduce-fraction-ℤ k) x) + by mul-int-fraction-power-ℝ⁺ _ _ _ + ＝ int-fraction-power-ℝ⁺ (reduce-fraction-ℤ k) x + by is-identity-power-diagonal-int-fraction-ℝ⁺ _ refl _ +``` + +### Powers by integer fractions are equal to powers by similar integer fractions + +```agda +abstract + sim-int-fraction-power-ℝ⁺ : + {l : Level} (p q : fraction-ℤ) → sim-fraction-ℤ p q → + (x : ℝ⁺ l) → int-fraction-power-ℝ⁺ p x ＝ int-fraction-power-ℝ⁺ q x + sim-int-fraction-power-ℝ⁺ p q p~q x = + equational-reasoning + int-fraction-power-ℝ⁺ p x + ＝ int-fraction-power-ℝ⁺ (reduce-fraction-ℤ p) x + by reduce-int-fraction-power-ℝ⁺ p x + ＝ int-fraction-power-ℝ⁺ (reduce-fraction-ℤ q) x + by + ap + ( λ k → int-fraction-power-ℝ⁺ k x) + ( unique-reduce-fraction-ℤ p q p~q) + ＝ int-fraction-power-ℝ⁺ q x + by inv (reduce-int-fraction-power-ℝ⁺ q x) +``` + +### `xᵃ⁺ᵇ = xᵃxᵇ` + +```agda +abstract + add-numerator-int-fraction-power-ℝ⁺ : + {l : Level} (p q : ℤ) (r : ℤ⁺) (x : ℝ⁺ l) → + int-fraction-power-ℝ⁺ (p +ℤ q , r) x ＝ + int-fraction-power-ℝ⁺ (p , r) x *ℝ⁺ int-fraction-power-ℝ⁺ (q , r) x + add-numerator-int-fraction-power-ℝ⁺ p q r x = + let + rℕ = positive-nat-ℤ⁺ r + in + equational-reasoning + nonzero-nat-root-ℝ⁺ rℕ (int-power-ℝ⁺ (p +ℤ q) x) + ＝ nonzero-nat-root-ℝ⁺ rℕ (int-power-ℝ⁺ p x *ℝ⁺ int-power-ℝ⁺ q x) + by + ap + ( nonzero-nat-root-ℝ⁺ rℕ) + ( distributive-int-power-add-ℝ⁺ p q x) + ＝ + ( nonzero-nat-root-ℝ⁺ rℕ (int-power-ℝ⁺ p x)) *ℝ⁺ + ( nonzero-nat-root-ℝ⁺ rℕ (int-power-ℝ⁺ q x)) + by + distributive-nonzero-nat-root-mul-ℝ⁺ rℕ _ _ + + distributive-add-integer-fraction-power-ℝ⁺ : + {l : Level} (p q : fraction-ℤ) (x : ℝ⁺ l) → + int-fraction-power-ℝ⁺ (p +fraction-ℤ q) x ＝ + int-fraction-power-ℝ⁺ p x *ℝ⁺ int-fraction-power-ℝ⁺ q x + distributive-add-integer-fraction-power-ℝ⁺ + (a , b⁺@(b , _)) (c , d⁺@(d , _)) x = + inv + ( equational-reasoning + int-fraction-power-ℝ⁺ (a , b⁺) x *ℝ⁺ int-fraction-power-ℝ⁺ (c , d⁺) x + ＝ + ( int-fraction-power-ℝ⁺ (a *ℤ d , b⁺ *ℤ⁺ d⁺) x) *ℝ⁺ + ( int-fraction-power-ℝ⁺ (b *ℤ c , b⁺ *ℤ⁺ d⁺) x) + by + ap-mul-ℝ⁺ + ( sim-int-fraction-power-ℝ⁺ _ _ + ( symmetric-sim-fraction-ℤ _ _ + ( sim-right-mul-diagonal-fraction-ℤ (a , b⁺) _ refl)) + ( x)) + ( sim-int-fraction-power-ℝ⁺ _ _ + ( symmetric-sim-fraction-ℤ _ _ + ( sim-left-mul-diagonal-fraction-ℤ _ (c , d⁺) refl)) + ( x)) + ＝ + ( int-fraction-power-ℝ⁺ (a *ℤ d , b⁺ *ℤ⁺ d⁺) x) *ℝ⁺ + ( int-fraction-power-ℝ⁺ (c *ℤ b , b⁺ *ℤ⁺ d⁺) x) + by + ap-mul-ℝ⁺ + ( refl) + ( ap + ( λ k → int-fraction-power-ℝ⁺ (k , b⁺ *ℤ⁺ d⁺) x) + ( commutative-mul-ℤ b c)) + ＝ int-fraction-power-ℝ⁺ (a *ℤ d +ℤ c *ℤ b , b⁺ *ℤ⁺ d⁺) x + by inv (add-numerator-int-fraction-power-ℝ⁺ _ _ _ _)) +``` + +### Integer fraction powers distribute over multiplication + +```agda +abstract + distributive-int-fraction-power-mul-ℝ⁺ : + {l1 l2 : Level} (q : fraction-ℤ) (x : ℝ⁺ l1) (y : ℝ⁺ l2) → + int-fraction-power-ℝ⁺ q (x *ℝ⁺ y) ＝ + int-fraction-power-ℝ⁺ q x *ℝ⁺ int-fraction-power-ℝ⁺ q y + distributive-int-fraction-power-mul-ℝ⁺ (p , q⁺) x y = + ( ap (nonzero-nat-root-ℝ⁺ _) (distributive-int-power-mul-ℝ⁺ p x y)) ∙ + ( distributive-nonzero-nat-root-mul-ℝ⁺ _ _ _) +``` + +### `x⁻ᵃ` is the multiplicative inverse of `xᵃ` + +```agda +abstract + neg-int-fraction-power-ℝ⁺ : + {l : Level} (q : fraction-ℤ) (x : ℝ⁺ l) → + int-fraction-power-ℝ⁺ (neg-fraction-ℤ q) x ＝ + inv-ℝ⁺ (int-fraction-power-ℝ⁺ q x) + neg-int-fraction-power-ℝ⁺ (p , q⁺) x = + equational-reasoning + nonzero-nat-root-ℝ⁺ (positive-nat-ℤ⁺ q⁺) (int-power-ℝ⁺ (neg-ℤ p) x) + ＝ nonzero-nat-root-ℝ⁺ (positive-nat-ℤ⁺ q⁺) (inv-ℝ⁺ (int-power-ℝ⁺ p x)) + by ap (nonzero-nat-root-ℝ⁺ _) (int-neg-power-ℝ⁺ p x) + ＝ inv-ℝ⁺ (nonzero-nat-root-ℝ⁺ (positive-nat-ℤ⁺ q⁺) (int-power-ℝ⁺ p x)) + by inv (commute-inv-nonzero-nat-root-ℝ⁺ _ _) +``` + +### `1ᵃ = 1` + +```agda +abstract + int-fraction-power-one-ℝ⁺ : + (q : fraction-ℤ) → int-fraction-power-ℝ⁺ q one-ℝ⁺ ＝ one-ℝ⁺ + int-fraction-power-one-ℝ⁺ (p , q⁺) = + ( ap (nonzero-nat-root-ℝ⁺ _) (int-power-one-ℝ⁺ _)) ∙ + ( nonzero-nat-root-one-ℝ⁺ _) +``` diff --git a/src/real-numbers/integer-powers-positive-real-numbers.lagda.md b/src/real-numbers/integer-powers-positive-real-numbers.lagda.md new file mode 100644 index 00000000000..2d10d4a7de5 --- /dev/null +++ b/src/real-numbers/integer-powers-positive-real-numbers.lagda.md @@ -0,0 +1,208 @@ +# Integer powers of positive real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.integer-powers-positive-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-integers +open import elementary-number-theory.integers +open import elementary-number-theory.multiplication-integers +open import elementary-number-theory.natural-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.binary-transport +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.universe-levels + +open import group-theory.integer-multiples-of-elements-large-abelian-groups +open import group-theory.integer-powers-of-elements-large-groups + +open import real-numbers.large-multiplicative-group-of-positive-real-numbers +open import real-numbers.multiplication-positive-real-numbers +open import real-numbers.multiplicative-inverses-positive-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.powers-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.rational-real-numbers +``` + +
+ +## Idea + +The +{{#concept "power operation" Disambiguation="raising an element of ℝ⁺ to an integer power" Agda=int-power-ℝ⁺}} +on the [positive real numbers](real-numbers.positive-real-numbers.md) `x ↦ xᵏ` +is defined by [iteratively](foundation.iterating-functions.md) +[multiplying](real-numbers.multiplication-positive-real-numbers.md) `x` with +itself `k` times. On this page we consider the case where `k` is an +[integer](elementary-number-theory.integers.md). + +## Definition + +```agda +int-power-ℝ⁺ : {l : Level} → ℤ → ℝ⁺ l → ℝ⁺ l +int-power-ℝ⁺ = int-multiple-Large-Ab large-ab-mul-ℝ⁺ +``` + +## Properties + +### `x¹ = x` + +```agda +abstract + int-one-power-ℝ⁺ : + {l : Level} (x : ℝ⁺ l) → int-power-ℝ⁺ one-ℤ x ＝ x + int-one-power-ℝ⁺ = int-multiple-one-Large-Ab large-ab-mul-ℝ⁺ +``` + +### `x⁻¹` is the multiplicative inverse of `x` + +```agda +abstract + int-neg-one-power-ℝ⁺ : + {l : Level} (x : ℝ⁺ l) → int-power-ℝ⁺ neg-one-ℤ x ＝ inv-ℝ⁺ x + int-neg-one-power-ℝ⁺ = int-multiple-neg-one-Large-Ab large-ab-mul-ℝ⁺ +``` + +### `x⁻ᵏ` is the multiplicative inverse of `xᵏ` + +```agda +abstract + int-neg-power-ℝ⁺ : + {l : Level} (k : ℤ) (x : ℝ⁺ l) → + int-power-ℝ⁺ (neg-ℤ k) x ＝ inv-ℝ⁺ (int-power-ℝ⁺ k x) + int-neg-power-ℝ⁺ = int-multiple-neg-Large-Ab large-ab-mul-ℝ⁺ +``` + +### Integer powers agree with natural powers + +```agda +abstract + int-power-int-ℝ⁺ : + {l : Level} (n : ℕ) (x : ℝ⁺ l) → int-power-ℝ⁺ (int-ℕ n) x ＝ power-ℝ⁺ n x + int-power-int-ℝ⁺ {l} 0 (x , _) = eq-ℝ⁺ _ _ (ap (raise-ℝ l) refl) + int-power-int-ℝ⁺ 1 x = eq-ℝ⁺ _ _ (ap real-ℝ⁺ (int-one-power-ℝ⁺ x)) + int-power-int-ℝ⁺ (succ-ℕ n@(succ-ℕ _)) x⁺@(x , _) = + equational-reasoning + int-power-ℝ⁺ (int-ℕ (succ-ℕ n)) x⁺ + ＝ int-power-ℝ⁺ (succ-ℤ (int-ℕ n)) x⁺ + by ap-binary int-power-ℝ⁺ (inv (succ-int-ℕ n)) refl + ＝ int-power-ℝ⁺ (int-ℕ n) x⁺ *ℝ⁺ x⁺ + by int-multiple-succ-Large-Ab large-ab-mul-ℝ⁺ (int-ℕ n) x⁺ + ＝ power-ℝ⁺ n x⁺ *ℝ⁺ x⁺ + by ap-mul-ℝ⁺ (int-power-int-ℝ⁺ n x⁺) (eq-ℝ⁺ _ _ refl) + ＝ power-ℝ⁺ (succ-ℕ n) x⁺ + by eq-ℝ⁺ _ _ (refl {x = power-ℝ (succ-ℕ n) x}) +``` + +### `1ⁿ = 1` + +```agda +abstract + int-power-raise-one-ℝ⁺ : + (l : Level) (k : ℤ) → + int-power-ℝ⁺ k (raise-ℝ⁺ l one-ℝ⁺) ＝ raise-ℝ⁺ l one-ℝ⁺ + int-power-raise-one-ℝ⁺ = + right-zero-law-int-multiple-Large-Ab large-ab-mul-ℝ⁺ + + int-power-one-ℝ⁺ : + (k : ℤ) → int-power-ℝ⁺ k one-ℝ⁺ ＝ one-ℝ⁺ + int-power-one-ℝ⁺ k = + ( ap (int-power-ℝ⁺ k) (eq-raise-ℝ⁺ one-ℝ⁺)) ∙ + ( int-power-raise-one-ℝ⁺ lzero k) ∙ + ( inv (eq-raise-ℝ⁺ one-ℝ⁺)) +``` + +### `xⁿ⁺¹ = xⁿx = xxⁿ` + +```agda +module _ + {l : Level} (k : ℤ) (x : ℝ⁺ l) + where + + abstract + int-power-succ-ℝ⁺ : + int-power-ℝ⁺ (succ-ℤ k) x ＝ int-power-ℝ⁺ k x *ℝ⁺ x + int-power-succ-ℝ⁺ = + int-multiple-succ-Large-Ab large-ab-mul-ℝ⁺ k x + + int-power-succ-ℝ⁺' : + int-power-ℝ⁺ (succ-ℤ k) x ＝ x *ℝ⁺ int-power-ℝ⁺ k x + int-power-succ-ℝ⁺' = + int-multiple-succ-Large-Ab' large-ab-mul-ℝ⁺ k x +``` + +### `xⁿ⁻¹ = xⁿx⁻¹ = x⁻¹x` + +```agda +module _ + {l : Level} (k : ℤ) (x : ℝ⁺ l) + where + + abstract + int-power-pred-ℝ⁺ : + int-power-ℝ⁺ (pred-ℤ k) x ＝ int-power-ℝ⁺ k x *ℝ⁺ inv-ℝ⁺ x + int-power-pred-ℝ⁺ = + int-multiple-pred-Large-Ab large-ab-mul-ℝ⁺ k x + + int-power-pred-ℝ⁺' : + int-power-ℝ⁺ (pred-ℤ k) x ＝ inv-ℝ⁺ x *ℝ⁺ int-power-ℝ⁺ k x + int-power-pred-ℝ⁺' = + int-multiple-pred-Large-Ab' large-ab-mul-ℝ⁺ k x +``` + +### `xᵐ⁺ⁿ = xᵐxⁿ` + +```agda +abstract + distributive-int-power-add-ℝ⁺ : + {l : Level} (m n : ℤ) (x : ℝ⁺ l) → + int-power-ℝ⁺ (m +ℤ n) x ＝ int-power-ℝ⁺ m x *ℝ⁺ int-power-ℝ⁺ n x + distributive-int-power-add-ℝ⁺ m n x = + right-distributive-int-multiple-add-Large-Ab large-ab-mul-ℝ⁺ x m n +``` + +### `xᵐⁿ = (xᵐ)ⁿ` + +```agda +abstract + int-power-mul-ℝ⁺ : + {l : Level} (m n : ℤ) (x : ℝ⁺ l) → + int-power-ℝ⁺ (m *ℤ n) x ＝ int-power-ℝ⁺ n (int-power-ℝ⁺ m x) + int-power-mul-ℝ⁺ = int-multiple-mul-Large-Ab large-ab-mul-ℝ⁺ +``` + +### `(xy)ᵏ = xᵏyᵏ` + +```agda +abstract + distributive-int-power-mul-ℝ⁺ : + {l1 l2 : Level} (k : ℤ) (x : ℝ⁺ l1) (y : ℝ⁺ l2) → + int-power-ℝ⁺ k (x *ℝ⁺ y) ＝ int-power-ℝ⁺ k x *ℝ⁺ int-power-ℝ⁺ k y + distributive-int-power-mul-ℝ⁺ = + left-distributive-int-multiple-add-Large-Ab large-ab-mul-ℝ⁺ +``` + +### `(xⁿ)ᵐ = (xᵐ)ⁿ` + +```agda +abstract + commute-int-power-ℝ⁺ : + {l : Level} (m n : ℤ) (x : ℝ⁺ l) → + int-power-ℝ⁺ m (int-power-ℝ⁺ n x) ＝ int-power-ℝ⁺ n (int-power-ℝ⁺ m x) + commute-int-power-ℝ⁺ = + commute-int-power-Large-Group large-group-mul-ℝ⁺ +``` + +## See also + +- [Natural powers of real numbers](real-numbers.powers-real-numbers.md) diff --git a/src/real-numbers/invertibility-strictly-increasing-unbounded-continuous-functions-real-numbers.lagda.md b/src/real-numbers/invertibility-strictly-increasing-unbounded-continuous-functions-real-numbers.lagda.md new file mode 100644 index 00000000000..fafab29d632 --- /dev/null +++ b/src/real-numbers/invertibility-strictly-increasing-unbounded-continuous-functions-real-numbers.lagda.md @@ -0,0 +1,862 @@ +# Invertibility of strictly increasing, unbounded, pointwise continuous functions on ℝ + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.invertibility-strictly-increasing-unbounded-continuous-functions-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.additive-group-of-rational-numbers +open import elementary-number-theory.difference-rational-numbers +open import elementary-number-theory.minimum-positive-rational-numbers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.strict-inequality-positive-rational-numbers +open import elementary-number-theory.strict-inequality-rational-numbers + +open import foundation.action-on-identifications-functions +open import foundation.automorphisms +open import foundation.axiom-of-countable-choice +open import foundation.binary-transport +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.disjoint-subtypes +open import foundation.disjunction +open import foundation.double-negation +open import foundation.empty-types +open import foundation.equivalences +open import foundation.existential-quantification +open import foundation.identity-types +open import foundation.inhabited-subtypes +open import foundation.injective-maps +open import foundation.logical-equivalences +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.retractions +open import foundation.subtypes +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import metric-spaces.isometries-metric-spaces +open import metric-spaces.metric-space-of-rational-numbers + +open import order-theory.large-posets + +open import real-numbers.addition-positive-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.dense-subsets-real-numbers +open import real-numbers.difference-real-numbers +open import real-numbers.increasing-functions-real-numbers +open import real-numbers.inequalities-addition-and-subtraction-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.limits-of-functions-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.pointwise-continuous-functions-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.rational-approximations-of-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.similarity-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers +open import real-numbers.strict-inequality-real-numbers +open import real-numbers.strictly-increasing-functions-real-numbers +open import real-numbers.transposition-addition-subtraction-cuts-dedekind-real-numbers +open import real-numbers.unbounded-functions-real-numbers +``` + +
+ +## Idea + +Any +[strictly increasing](real-numbers.strictly-increasing-functions-real-numbers.md), +[pointwise continuous](real-numbers.pointwise-continuous-functions-real-numbers.md), +[unbounded](real-numbers.unbounded-functions-real-numbers.md) function from the +[real numbers](real-numbers.dedekind-real-numbers.md) to themselves is an +[automorphism](foundation.automorphisms.md) of the real numbers. We abbreviate +these conditions as SIPCUB. + +## Definition + +```agda +module _ + {l1 l2 : Level} + (f : ℝ l1 → ℝ l2) + where + + is-SIPCUB-prop-function-ℝ : Prop (lsuc l1 ⊔ l2) + is-SIPCUB-prop-function-ℝ = + ( is-strictly-increasing-prop-function-ℝ f) ∧ + ( is-pointwise-continuous-prop-function-ℝ f) ∧ + ( is-unbounded-prop-function-ℝ f) + + is-SIPCUB-function-ℝ : UU (lsuc l1 ⊔ l2) + is-SIPCUB-function-ℝ = type-Prop is-SIPCUB-prop-function-ℝ + +SIPCUB-function-ℝ : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +SIPCUB-function-ℝ l1 l2 = type-subtype (is-SIPCUB-prop-function-ℝ {l1} {l2}) + +module _ + {l1 l2 : Level} + (f : SIPCUB-function-ℝ l1 l2) + where + + map-SIPCUB-function-ℝ : ℝ l1 → ℝ l2 + map-SIPCUB-function-ℝ = pr1 f + + abstract + is-strictly-increasing-SIPCUB-function-ℝ : + is-strictly-increasing-function-ℝ map-SIPCUB-function-ℝ + is-strictly-increasing-SIPCUB-function-ℝ = pr1 (pr2 f) + + is-increasing-SIPCUB-function-ℝ : + is-increasing-function-ℝ map-SIPCUB-function-ℝ + is-increasing-SIPCUB-function-ℝ = + is-increasing-is-strictly-increasing-function-ℝ + ( map-SIPCUB-function-ℝ) + ( is-strictly-increasing-SIPCUB-function-ℝ) + + is-pointwise-continuous-SIPCUB-function-ℝ : + is-pointwise-continuous-function-ℝ map-SIPCUB-function-ℝ + is-pointwise-continuous-SIPCUB-function-ℝ = pr1 (pr2 (pr2 f)) + + pointwise-continuous-SIPCUB-function-ℝ : + pointwise-continuous-function-ℝ l1 l2 + pointwise-continuous-SIPCUB-function-ℝ = + ( map-SIPCUB-function-ℝ , + is-pointwise-continuous-SIPCUB-function-ℝ) + + is-classically-pointwise-continuous-SIPCUB-function-ℝ : + (x : ℝ l1) → + is-classical-limit-function-ℝ + ( map-SIPCUB-function-ℝ) + ( x) + ( map-SIPCUB-function-ℝ x) + is-classically-pointwise-continuous-SIPCUB-function-ℝ = + is-classically-pointwise-continuous-pointwise-continuous-function-ℝ + ( pointwise-continuous-SIPCUB-function-ℝ) + + is-unbounded-below-SIPCUB-function-ℝ : + is-unbounded-below-function-ℝ map-SIPCUB-function-ℝ + is-unbounded-below-SIPCUB-function-ℝ = pr2 (pr2 (pr2 (pr2 f))) + + is-unbounded-above-SIPCUB-function-ℝ : + is-unbounded-above-function-ℝ map-SIPCUB-function-ℝ + is-unbounded-above-SIPCUB-function-ℝ = pr1 (pr2 (pr2 (pr2 f))) + + reflects-leq-SIPCUB-function-ℝ : + (x x' : ℝ l1) → + leq-ℝ (map-SIPCUB-function-ℝ x) (map-SIPCUB-function-ℝ x') → + leq-ℝ x x' + reflects-leq-SIPCUB-function-ℝ = + reflects-leq-is-strictly-increasing-function-ℝ + ( map-SIPCUB-function-ℝ) + ( is-strictly-increasing-SIPCUB-function-ℝ) + + reflects-le-SIPCUB-function-ℝ : + (x x' : ℝ l1) → + le-ℝ (map-SIPCUB-function-ℝ x) (map-SIPCUB-function-ℝ x') → + le-ℝ x x' + reflects-le-SIPCUB-function-ℝ = + reflects-le-is-strictly-increasing-pointwise-continuous-function-ℝ + ( pointwise-continuous-SIPCUB-function-ℝ) + ( is-strictly-increasing-SIPCUB-function-ℝ) + + is-injective-SIPCUB-function-ℝ : is-injective map-SIPCUB-function-ℝ + is-injective-SIPCUB-function-ℝ = + is-injective-is-strictly-increasing-function-ℝ + ( map-SIPCUB-function-ℝ) + ( is-strictly-increasing-SIPCUB-function-ℝ) +``` + +## Properties + +### Any SIPCUB function is invertible + +Note we cannot be any more universe-polymorphic. + +```agda +module _ + {l : Level} + (f : SIPCUB-function-ℝ l l) + (y : ℝ l) + where + + lower-cut-inv-SIPCUB-function-ℝ : subtype l ℚ + lower-cut-inv-SIPCUB-function-ℝ q = + le-prop-ℝ (map-SIPCUB-function-ℝ f (raise-real-ℚ l q)) y + + upper-cut-inv-SIPCUB-function-ℝ : subtype l ℚ + upper-cut-inv-SIPCUB-function-ℝ q = + le-prop-ℝ y (map-SIPCUB-function-ℝ f (raise-real-ℚ l q)) + + abstract + is-inhabited-lower-cut-inv-SIPCUB-function-ℝ : + is-inhabited-subtype lower-cut-inv-SIPCUB-function-ℝ + is-inhabited-lower-cut-inv-SIPCUB-function-ℝ = + let + open + do-syntax-trunc-Prop + ( is-inhabited-subtype-Prop lower-cut-inv-SIPCUB-function-ℝ) + in do + (q , qImports + +```agda +open import foundation.dependent-pair-types +open import foundation.universe-levels + +open import group-theory.large-abelian-groups +open import group-theory.large-groups +open import group-theory.large-monoids +open import group-theory.large-semigroups + +open import real-numbers.multiplication-positive-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.multiplicative-inverses-positive-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.similarity-positive-real-numbers +``` + + + +## Idea + +The [positive real numbers](real-numbers.positive-real-numbers.md) form a +[large abelian group](group-theory.large-abelian-groups.md) under +[multiplication](real-numbers.multiplication-positive-real-numbers.md). + +## Definition + +```agda +large-semigroup-mul-ℝ⁺ : Large-Semigroup lsuc +large-semigroup-mul-ℝ⁺ = + make-Large-Semigroup + ( ℝ⁺-Set) + ( mul-ℝ⁺) + ( associative-mul-ℝ⁺) + +large-monoid-mul-ℝ⁺ : Large-Monoid lsuc (_⊔_) +large-monoid-mul-ℝ⁺ = + make-Large-Monoid + ( large-semigroup-mul-ℝ⁺) + ( large-similarity-relation-sim-ℝ⁺) + ( raise-ℝ⁺) + ( λ l (x , _) → sim-raise-ℝ l x) + ( preserves-sim-mul-ℝ⁺) + ( one-ℝ⁺) + ( left-unit-law-mul-ℝ⁺) + ( right-unit-law-mul-ℝ⁺) + +large-group-mul-ℝ⁺ : Large-Group lsuc (_⊔_) +large-group-mul-ℝ⁺ = + make-Large-Group + ( large-monoid-mul-ℝ⁺) + ( inv-ℝ⁺) + ( preserves-sim-inv-ℝ⁺) + ( eq-left-inverse-law-mul-ℝ⁺) + ( eq-right-inverse-law-mul-ℝ⁺) + +large-ab-mul-ℝ⁺ : Large-Ab lsuc (_⊔_) +large-ab-mul-ℝ⁺ = + make-Large-Ab + ( large-group-mul-ℝ⁺) + ( commutative-mul-ℝ⁺) +``` diff --git a/src/real-numbers/limits-of-functions-real-numbers.lagda.md b/src/real-numbers/limits-of-functions-real-numbers.lagda.md new file mode 100644 index 00000000000..690da65c750 --- /dev/null +++ b/src/real-numbers/limits-of-functions-real-numbers.lagda.md @@ -0,0 +1,115 @@ +# Limits of functions on the real numbers + +```agda +module real-numbers.limits-of-functions-real-numbers where +``` + +
Imports + +```agda +open import foundation.axiom-of-countable-choice +open import foundation.propositions +open import foundation.universe-levels + +open import metric-spaces.limits-of-functions-metric-spaces + +open import real-numbers.dedekind-real-numbers +open import real-numbers.metric-space-of-real-numbers +``` + +
+ +## Idea + +A +{{#concept "limit" Disambiguation="of a function from ℝ to ℝ" Agda=is-limit-function-ℝ}} +of a function `f` from the [real numbers](real-numbers.dedekind-real-numbers.md) +to themselves at `x : ℝ` is the +[limit](metric-spaces.limits-of-functions-metric-spaces.md) of `f` at `x` in the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md). + +## Definition + +```agda +is-limit-prop-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → ℝ l1 → ℝ l2 → Prop (lsuc l1 ⊔ l2) +is-limit-prop-function-ℝ {l1} {l2} = + is-point-limit-prop-function-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + +is-limit-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → ℝ l1 → ℝ l2 → UU (lsuc l1 ⊔ l2) +is-limit-function-ℝ f x y = type-Prop (is-limit-prop-function-ℝ f x y) +``` + +### The classical epsilon-delta definition of limit + +The +{{#concept "classical definition of a limit" Disambiguation="in ℝ" Agda=is-classical-limit-function-ℝ}} +states that the limit of `f x` as `x` approaches `x₀` is a `y` such that for any +`ε : ℚ⁺`, there [exists](foundation.existential-quantification.md) a `δ : ℚ⁺` +such that if `x` and `x₀` are in a `δ`-neighborhood of each other, `f x` and `y` +are in a `ε`-neighborhood of each other. + +```agda +is-classical-limit-prop-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → ℝ l1 → ℝ l2 → Prop (lsuc l1 ⊔ l2) +is-classical-limit-prop-function-ℝ {l1} {l2} = + is-classical-limit-prop-function-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + +is-classical-limit-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → ℝ l1 → ℝ l2 → UU (lsuc l1 ⊔ l2) +is-classical-limit-function-ℝ f x y = + type-Prop (is-classical-limit-prop-function-ℝ f x y) +``` + +## Properties + +### Constructive limits are classical limits + +```agda +module _ + {l1 l2 : Level} + (f : ℝ l1 → ℝ l2) + (x : ℝ l1) + (y : ℝ l2) + where + + abstract + is-classical-limit-is-limit-function-ℝ : + is-limit-function-ℝ f x y → is-classical-limit-function-ℝ f x y + is-classical-limit-is-limit-function-ℝ = + is-classical-limit-is-limit-function-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + ( f) + ( x) + ( y) +``` + +### Assuming countable choice, classical limits are constructive limits + +```agda +module _ + {l1 l2 : Level} + (acω : ACω) + (f : ℝ l1 → ℝ l2) + (x : ℝ l1) + (y : ℝ l2) + where + + abstract + is-limit-is-classical-limit-ACω-function-ℝ : + is-classical-limit-function-ℝ f x y → is-limit-function-ℝ f x y + is-limit-is-classical-limit-ACω-function-ℝ = + is-limit-is-classical-limit-ACω-function-Metric-Space + ( acω) + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + ( f) + ( x) + ( y) +``` diff --git a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md index f33d4630f16..276f203c0c1 100644 --- a/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md +++ b/src/real-numbers/lipschitz-continuity-multiplication-real-numbers.lagda.md @@ -29,8 +29,9 @@ open import foundation.transport-along-identifications open import foundation.universe-levels open import metric-spaces.cartesian-products-metric-spaces -open import metric-spaces.continuous-functions-metric-spaces +open import metric-spaces.continuity-of-functions-at-points-in-metric-spaces open import metric-spaces.lipschitz-functions-metric-spaces +open import metric-spaces.pointwise-continuous-functions-metric-spaces open import metric-spaces.uniformly-continuous-functions-metric-spaces open import order-theory.large-posets diff --git a/src/real-numbers/metric-space-of-real-numbers.lagda.md b/src/real-numbers/metric-space-of-real-numbers.lagda.md index a5f9e1bc435..21e16b10ec5 100644 --- a/src/real-numbers/metric-space-of-real-numbers.lagda.md +++ b/src/real-numbers/metric-space-of-real-numbers.lagda.md @@ -12,6 +12,7 @@ module real-numbers.metric-space-of-real-numbers where open import elementary-number-theory.addition-positive-rational-numbers open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.difference-rational-numbers +open import elementary-number-theory.inequality-positive-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers @@ -386,6 +387,17 @@ module _ ( right-leq-real-bound-neighborhood-ℝ d x y H)) ``` +### The neighborhood relation on the real numbers is weakly monotonic + +```agda +abstract + weakly-monotonic-neighborhood-ℝ : + {l : Level} (x y : ℝ l) (d₁ d₂ : ℚ⁺) → leq-ℚ⁺ d₁ d₂ → + neighborhood-ℝ l d₁ x y → neighborhood-ℝ l d₂ x y + weakly-monotonic-neighborhood-ℝ {l} = + weakly-monotonic-neighborhood-Metric-Space (metric-space-ℝ l) +``` + ### The canonical embedding from rational to real numbers is an isometry between metric spaces ```agda diff --git a/src/real-numbers/multiplication-positive-real-numbers.lagda.md b/src/real-numbers/multiplication-positive-real-numbers.lagda.md index 25fc941ae1f..5faa887c8aa 100644 --- a/src/real-numbers/multiplication-positive-real-numbers.lagda.md +++ b/src/real-numbers/multiplication-positive-real-numbers.lagda.md @@ -16,6 +16,7 @@ open import elementary-number-theory.multiplication-positive-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers +open import foundation.action-on-identifications-binary-functions open import foundation.binary-transport open import foundation.dependent-pair-types open import foundation.existential-quantification @@ -37,7 +38,9 @@ open import real-numbers.multiplicative-inverses-positive-real-numbers open import real-numbers.nonnegative-real-numbers open import real-numbers.positive-and-negative-real-numbers open import real-numbers.positive-real-numbers +open import real-numbers.raising-universe-levels-real-numbers open import real-numbers.rational-real-numbers +open import real-numbers.similarity-positive-real-numbers open import real-numbers.similarity-real-numbers open import real-numbers.strict-inequality-real-numbers ``` @@ -98,11 +101,16 @@ mul-ℝ⁺ (x , is-pos-x) (y , is-pos-y) = infixl 40 _*ℝ⁺_ _*ℝ⁺_ : {l1 l2 : Level} → ℝ⁺ l1 → ℝ⁺ l2 → ℝ⁺ (l1 ⊔ l2) _*ℝ⁺_ = mul-ℝ⁺ + +ap-mul-ℝ⁺ : + {l1 l2 : Level} {x x' : ℝ⁺ l1} → x ＝ x' → {y y' : ℝ⁺ l2} → y ＝ y' → + x *ℝ⁺ y ＝ x' *ℝ⁺ y' +ap-mul-ℝ⁺ = ap-binary mul-ℝ⁺ ``` ## Properties -### Commutativity of multiplication of positive real numbers +### Commutativity of multiplication ```agda abstract @@ -112,6 +120,17 @@ abstract eq-ℝ⁺ (x⁺ *ℝ⁺ y⁺) (y⁺ *ℝ⁺ x⁺) (commutative-mul-ℝ x y) ``` +### Associativity of multiplication + +```agda +abstract + associative-mul-ℝ⁺ : + {l1 l2 l3 : Level} (x : ℝ⁺ l1) (y : ℝ⁺ l2) (z : ℝ⁺ l3) → + ((x *ℝ⁺ y) *ℝ⁺ z) ＝ (x *ℝ⁺ (y *ℝ⁺ z)) + associative-mul-ℝ⁺ (x , _) (y , _) (z , _) = + eq-ℝ⁺ _ _ (associative-mul-ℝ x y z) +``` + ### Multiplication by a positive real number preserves and reflects strict inequality ```agda @@ -193,6 +212,55 @@ abstract ( yx≤zx)) ``` +### Multiplication preserves similarity + +```agda +abstract + preserves-sim-mul-ℝ⁺ : + {l1 l2 l3 l4 : Level} → + (x : ℝ⁺ l1) (x' : ℝ⁺ l2) → sim-ℝ⁺ x x' → + (y : ℝ⁺ l3) (y' : ℝ⁺ l4) → sim-ℝ⁺ y y' → + sim-ℝ⁺ (x *ℝ⁺ y) (x' *ℝ⁺ y') + preserves-sim-mul-ℝ⁺ (x , _) (x' , _) x~x' (y , _) (y' , _) y~y' = + preserves-sim-mul-ℝ x~x' y~y' +``` + +### Unit laws + +```agda +abstract + left-unit-law-mul-ℝ⁺ : {l : Level} (x : ℝ⁺ l) → one-ℝ⁺ *ℝ⁺ x ＝ x + left-unit-law-mul-ℝ⁺ (x , _) = eq-ℝ⁺ _ _ (left-unit-law-mul-ℝ x) + + right-unit-law-mul-ℝ⁺ : {l : Level} (x : ℝ⁺ l) → x *ℝ⁺ one-ℝ⁺ ＝ x + right-unit-law-mul-ℝ⁺ (x , _) = eq-ℝ⁺ _ _ (right-unit-law-mul-ℝ x) +``` + +### Inverse laws + +```agda +module _ + {l : Level} (x : ℝ⁺ l) + where + + abstract + eq-right-inverse-law-mul-ℝ⁺ : + x *ℝ⁺ inv-ℝ⁺ x ＝ raise-ℝ⁺ l one-ℝ⁺ + eq-right-inverse-law-mul-ℝ⁺ = + eq-sim-ℝ⁺ _ _ + ( transitive-sim-ℝ _ _ _ + ( sim-raise-ℝ l one-ℝ) + ( right-inverse-law-mul-ℝ⁺ x)) + + eq-left-inverse-law-mul-ℝ⁺ : + inv-ℝ⁺ x *ℝ⁺ x ＝ raise-ℝ⁺ l one-ℝ⁺ + eq-left-inverse-law-mul-ℝ⁺ = + eq-sim-ℝ⁺ _ _ + ( transitive-sim-ℝ _ _ _ + ( sim-raise-ℝ l one-ℝ) + ( left-inverse-law-mul-ℝ⁺ x)) +``` + ### The multiplicative inverse is distributive over multiplication ```agda diff --git a/src/real-numbers/nonzero-natural-roots-nonnegative-real-numbers.lagda.md b/src/real-numbers/nonzero-natural-roots-nonnegative-real-numbers.lagda.md new file mode 100644 index 00000000000..a5d08c02851 --- /dev/null +++ b/src/real-numbers/nonzero-natural-roots-nonnegative-real-numbers.lagda.md @@ -0,0 +1,347 @@ +# Nonzero natural roots of nonnegative real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.nonzero-natural-roots-nonnegative-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.exponentiation-natural-numbers +open import elementary-number-theory.multiplication-natural-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers +open import elementary-number-theory.parity-natural-numbers +open import elementary-number-theory.powers-of-two + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.automorphisms +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.universe-levels + +open import real-numbers.dedekind-real-numbers +open import real-numbers.multiplication-nonnegative-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.odd-roots-nonnegative-real-numbers +open import real-numbers.odd-roots-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.powers-real-numbers +open import real-numbers.square-roots-nonnegative-real-numbers +open import real-numbers.squares-real-numbers +``` + +
+ +## Idea + +For any [nonzero](elementary-number-theory.nonzero-natural-numbers.md) +[natural number](elementary-number-theory.natural-numbers.md) `n`, there exists +an inverse to the [power function](real-numbers.powers-real-numbers.md) `x ↦ xⁿ` +on the [nonnegative](real-numbers.nonnegative-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md). + +## Definition + +```agda +root-pair-expansion-ℝ⁰⁺ : {l : Level} (u v : ℕ) (x : ℝ⁰⁺ l) → ℝ⁰⁺ l +root-pair-expansion-ℝ⁰⁺ 0 v x = + odd-root-ℝ⁰⁺ (succ-ℕ (v *ℕ 2)) (is-odd-has-odd-expansion _ (v , refl)) x +root-pair-expansion-ℝ⁰⁺ (succ-ℕ u) v x = + root-pair-expansion-ℝ⁰⁺ u v (sqrt-ℝ⁰⁺ x) + +real-root-pair-expansion-ℝ⁰⁺ : {l : Level} (u v : ℕ) (x : ℝ⁰⁺ l) → ℝ l +real-root-pair-expansion-ℝ⁰⁺ u v x = + real-ℝ⁰⁺ (root-pair-expansion-ℝ⁰⁺ u v x) + +nonzero-nat-root-ℝ⁰⁺ : {l : Level} → ℕ⁺ → ℝ⁰⁺ l → ℝ⁰⁺ l +nonzero-nat-root-ℝ⁰⁺ (succ-ℕ n , H) = + let + ((u , v) , _) = has-pair-expansion n + in root-pair-expansion-ℝ⁰⁺ u v +nonzero-nat-root-ℝ⁰⁺ (0 , H) = ex-falso (H refl) + +real-nonzero-nat-root-ℝ⁰⁺ : {l : Level} → ℕ⁺ → ℝ⁰⁺ l → ℝ l +real-nonzero-nat-root-ℝ⁰⁺ n x = real-ℝ⁰⁺ (nonzero-nat-root-ℝ⁰⁺ n x) +``` + +## Properties + +### The `n`th power of the `n`th root of `x` is `x` + +```agda +abstract + power-root-pair-expansion-ℝ⁰⁺ : + {l : Level} (u v : ℕ) (x : ℝ⁰⁺ l) → + power-ℝ + ( map-pair-expansion u v) + ( real-root-pair-expansion-ℝ⁰⁺ u v x) ＝ + real-ℝ⁰⁺ x + power-root-pair-expansion-ℝ⁰⁺ 0 v (x , _) = + equational-reasoning + power-ℝ (1 *ℕ succ-ℕ (v *ℕ 2)) _ + ＝ + power-ℝ + ( succ-ℕ (v *ℕ 2)) + ( odd-root-ℝ + ( succ-ℕ (v *ℕ 2)) + ( is-odd-has-odd-expansion _ (v , refl)) + ( x)) + by ap-binary power-ℝ (left-unit-law-mul-ℕ (succ-ℕ (v *ℕ 2))) refl + ＝ x + by + odd-power-odd-root-ℝ + ( succ-ℕ (v *ℕ 2)) + ( is-odd-has-odd-expansion _ (v , refl)) + ( x) + power-root-pair-expansion-ℝ⁰⁺ (succ-ℕ u) v x⁰⁺@(x , _) = + equational-reasoning + power-ℝ + ( map-pair-expansion (succ-ℕ u) v) + ( real-root-pair-expansion-ℝ⁰⁺ u v (sqrt-ℝ⁰⁺ x⁰⁺)) + ＝ + power-ℝ + ( map-pair-expansion u v *ℕ 2) + ( real-root-pair-expansion-ℝ⁰⁺ u v (sqrt-ℝ⁰⁺ x⁰⁺)) + by + ap-binary + ( power-ℝ) + ( map-pair-expansion-succ-ℕ u v) + ( refl) + ＝ + square-ℝ + ( power-ℝ + ( map-pair-expansion u v) + ( real-root-pair-expansion-ℝ⁰⁺ u v (sqrt-ℝ⁰⁺ x⁰⁺))) + by power-mul-ℝ (map-pair-expansion u v) 2 + ＝ square-ℝ (real-sqrt-ℝ⁰⁺ x⁰⁺) + by ap square-ℝ (power-root-pair-expansion-ℝ⁰⁺ u v (sqrt-ℝ⁰⁺ x⁰⁺)) + ＝ x + by eq-real-square-sqrt-ℝ⁰⁺ x⁰⁺ + +abstract + is-section-nonzero-nat-power-ℝ⁰⁺ : + {l : Level} (n : ℕ⁺) (x : ℝ⁰⁺ l) → + power-ℝ⁰⁺ (nat-nonzero-ℕ n) (nonzero-nat-root-ℝ⁰⁺ n x) ＝ x + is-section-nonzero-nat-power-ℝ⁰⁺ (succ-ℕ n , H) x = + let + ((u , v) , H) = has-pair-expansion n + in + eq-ℝ⁰⁺ _ _ + ( ( ap-binary power-ℝ (inv H) refl) ∙ + ( power-root-pair-expansion-ℝ⁰⁺ u v x)) + is-section-nonzero-nat-power-ℝ⁰⁺ (0 , H) x = ex-falso (H refl) +``` + +### The `n`th root of the `n`th power of `x` is `x` + +```agda +abstract + root-power-pair-expansion-ℝ⁰⁺ : + {l : Level} (u v : ℕ) (x : ℝ⁰⁺ l) → + real-ℝ⁰⁺ + ( root-pair-expansion-ℝ⁰⁺ u v (power-ℝ⁰⁺ (map-pair-expansion u v) x)) ＝ + real-ℝ⁰⁺ x + root-power-pair-expansion-ℝ⁰⁺ 0 v (x , _) = + equational-reasoning + odd-root-ℝ + ( succ-ℕ (v *ℕ 2)) + ( is-odd-has-odd-expansion _ (v , refl)) + ( power-ℝ (1 *ℕ succ-ℕ (v *ℕ 2)) x) + ＝ + odd-root-ℝ + ( succ-ℕ (v *ℕ 2)) + ( is-odd-has-odd-expansion _ (v , refl)) + ( power-ℝ (succ-ℕ (v *ℕ 2)) x) + by + ap + ( λ n → + odd-root-ℝ + ( succ-ℕ (v *ℕ 2)) + ( is-odd-has-odd-expansion _ (v , refl)) + ( power-ℝ n x)) + ( left-unit-law-mul-ℕ (succ-ℕ (v *ℕ 2))) + ＝ x + by + odd-root-odd-power-ℝ + ( succ-ℕ (v *ℕ 2)) + ( is-odd-has-odd-expansion _ (v , refl)) + ( x) + root-power-pair-expansion-ℝ⁰⁺ (succ-ℕ u) v x⁰⁺@(x , _) = + equational-reasoning + real-root-pair-expansion-ℝ⁰⁺ + ( u) + ( v) + ( sqrt-ℝ⁰⁺ + ( power-ℝ⁰⁺ (map-pair-expansion (succ-ℕ u) v) x⁰⁺)) + ＝ + real-root-pair-expansion-ℝ⁰⁺ + ( u) + ( v) + ( sqrt-ℝ⁰⁺ + ( power-ℝ⁰⁺ (map-pair-expansion u v *ℕ 2) x⁰⁺)) + by + ap + ( λ n → + real-root-pair-expansion-ℝ⁰⁺ u v (sqrt-ℝ⁰⁺ (power-ℝ⁰⁺ n x⁰⁺))) + ( map-pair-expansion-succ-ℕ u v) + ＝ + real-root-pair-expansion-ℝ⁰⁺ + ( u) + ( v) + ( sqrt-ℝ⁰⁺ (square-ℝ⁰⁺ (power-ℝ⁰⁺ (map-pair-expansion u v) x⁰⁺))) + by + ap + ( λ y → real-root-pair-expansion-ℝ⁰⁺ u v (sqrt-ℝ⁰⁺ y)) + ( eq-ℝ⁰⁺ _ _ (power-mul-ℝ (map-pair-expansion u v) 2)) + ＝ + real-root-pair-expansion-ℝ⁰⁺ + ( u) + ( v) + ( power-ℝ⁰⁺ (map-pair-expansion u v) x⁰⁺) + by + ap + ( real-root-pair-expansion-ℝ⁰⁺ u v) + ( is-retraction-square-ℝ⁰⁺ _) + ＝ x + by root-power-pair-expansion-ℝ⁰⁺ u v x⁰⁺ + + is-retraction-nonzero-nat-power-ℝ⁰⁺ : + {l : Level} (n : ℕ⁺) (x : ℝ⁰⁺ l) → + nonzero-nat-root-ℝ⁰⁺ n (power-ℝ⁰⁺ (nat-nonzero-ℕ n) x) ＝ x + is-retraction-nonzero-nat-power-ℝ⁰⁺ (succ-ℕ n , H) x = + let + ((u , v) , H) = has-pair-expansion n + in + eq-ℝ⁰⁺ _ _ + ( ( ap + ( λ k → real-root-pair-expansion-ℝ⁰⁺ u v (power-ℝ⁰⁺ k x)) + ( inv H)) ∙ + ( root-power-pair-expansion-ℝ⁰⁺ u v x)) + is-retraction-nonzero-nat-power-ℝ⁰⁺ (0 , H) x = ex-falso (H refl) +``` + +### For nonzero `n`, `power-ℝ⁰⁺ n` is an automorphism on the nonnegative real numbers + +```agda +is-equiv-nonzero-power-ℝ⁰⁺ : + {l : Level} (n : ℕ⁺) → is-equiv (power-ℝ⁰⁺ {l} (nat-nonzero-ℕ n)) +is-equiv-nonzero-power-ℝ⁰⁺ n = + is-equiv-is-invertible + ( nonzero-nat-root-ℝ⁰⁺ n) + ( is-section-nonzero-nat-power-ℝ⁰⁺ n) + ( is-retraction-nonzero-nat-power-ℝ⁰⁺ n) + +aut-nonzero-power-ℝ⁰⁺ : {l : Level} (n : ℕ⁺) → Aut (ℝ⁰⁺ l) +aut-nonzero-power-ℝ⁰⁺ n⁺@(n , _) = + ( power-ℝ⁰⁺ n , is-equiv-nonzero-power-ℝ⁰⁺ n⁺) + +abstract + is-injective-nonzero-power-ℝ⁰⁺ : + {l : Level} (n : ℕ⁺) → is-injective (power-ℝ⁰⁺ {l} (nat-nonzero-ℕ n)) + is-injective-nonzero-power-ℝ⁰⁺ n = + is-injective-is-equiv + ( is-equiv-nonzero-power-ℝ⁰⁺ n) +``` + +### The `1`st root of `x` is `x` + +```agda +abstract + root-one-ℝ⁰⁺ : {l : Level} (x : ℝ⁰⁺ l) → nonzero-nat-root-ℝ⁰⁺ one-ℕ⁺ x ＝ x + root-one-ℝ⁰⁺ x = + is-injective-nonzero-power-ℝ⁰⁺ + ( one-ℕ⁺) + ( ( is-section-nonzero-nat-power-ℝ⁰⁺ one-ℕ⁺ x) ∙ + ( eq-ℝ⁰⁺ _ _ (refl {x = real-ℝ⁰⁺ x}))) +``` + +### Roots by products of nonzero natural numbers are iterated roots + +```agda +abstract + mul-nonzero-nat-root-ℝ⁰⁺ : + {l : Level} (m n : ℕ⁺) (x : ℝ⁰⁺ l) → + nonzero-nat-root-ℝ⁰⁺ (m *ℕ⁺ n) x ＝ + nonzero-nat-root-ℝ⁰⁺ m (nonzero-nat-root-ℝ⁰⁺ n x) + mul-nonzero-nat-root-ℝ⁰⁺ m⁺@(m , _) n⁺@(n , _) x = + inv + ( is-injective-nonzero-power-ℝ⁰⁺ + ( m⁺ *ℕ⁺ n⁺) + ( equational-reasoning + power-ℝ⁰⁺ + ( m *ℕ n) + ( nonzero-nat-root-ℝ⁰⁺ m⁺ (nonzero-nat-root-ℝ⁰⁺ n⁺ x)) + ＝ + power-ℝ⁰⁺ + ( n) + ( power-ℝ⁰⁺ + ( m) + ( nonzero-nat-root-ℝ⁰⁺ m⁺ (nonzero-nat-root-ℝ⁰⁺ n⁺ x))) + by power-mul-ℝ⁰⁺ m n _ + ＝ + power-ℝ⁰⁺ + ( n) + ( nonzero-nat-root-ℝ⁰⁺ n⁺ x) + by ap (power-ℝ⁰⁺ n) (is-section-nonzero-nat-power-ℝ⁰⁺ m⁺ _) + ＝ x + by is-section-nonzero-nat-power-ℝ⁰⁺ n⁺ x + ＝ power-ℝ⁰⁺ (m *ℕ n) (nonzero-nat-root-ℝ⁰⁺ (m⁺ *ℕ⁺ n⁺) x) + by inv (is-section-nonzero-nat-power-ℝ⁰⁺ (m⁺ *ℕ⁺ n⁺) x))) +``` + +### Nonzero natural roots distribute over multiplication + +```agda +abstract + distributive-nonzero-nat-root-mul-ℝ⁰⁺ : + {l1 l2 : Level} (n : ℕ⁺) (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) → + nonzero-nat-root-ℝ⁰⁺ n (x *ℝ⁰⁺ y) ＝ + nonzero-nat-root-ℝ⁰⁺ n x *ℝ⁰⁺ nonzero-nat-root-ℝ⁰⁺ n y + distributive-nonzero-nat-root-mul-ℝ⁰⁺ n x y = + is-injective-nonzero-power-ℝ⁰⁺ n + ( equational-reasoning + power-ℝ⁰⁺ (nat-nonzero-ℕ n) (nonzero-nat-root-ℝ⁰⁺ n (x *ℝ⁰⁺ y)) + ＝ x *ℝ⁰⁺ y + by is-section-nonzero-nat-power-ℝ⁰⁺ n (x *ℝ⁰⁺ y) + ＝ + ( power-ℝ⁰⁺ (nat-nonzero-ℕ n) (nonzero-nat-root-ℝ⁰⁺ n x)) *ℝ⁰⁺ + ( power-ℝ⁰⁺ (nat-nonzero-ℕ n) (nonzero-nat-root-ℝ⁰⁺ n y)) + by + ap-mul-ℝ⁰⁺ + ( inv (is-section-nonzero-nat-power-ℝ⁰⁺ n x)) + ( inv (is-section-nonzero-nat-power-ℝ⁰⁺ n y)) + ＝ + power-ℝ⁰⁺ + ( nat-nonzero-ℕ n) + ( nonzero-nat-root-ℝ⁰⁺ n x *ℝ⁰⁺ nonzero-nat-root-ℝ⁰⁺ n y) + by inv (distributive-power-mul-ℝ⁰⁺ _ _ _)) +``` + +### Any root of 1 is 1 + +```agda +abstract + root-pair-expansion-one-ℝ⁰⁺ : + (u v : ℕ) → root-pair-expansion-ℝ⁰⁺ u v one-ℝ⁰⁺ ＝ one-ℝ⁰⁺ + root-pair-expansion-one-ℝ⁰⁺ 0 v = eq-ℝ⁰⁺ _ _ (odd-root-one-ℝ _ _) + root-pair-expansion-one-ℝ⁰⁺ (succ-ℕ u) v = + ( ap (root-pair-expansion-ℝ⁰⁺ u v) sqrt-one-ℝ⁰⁺) ∙ + ( root-pair-expansion-one-ℝ⁰⁺ u v) + + nonzero-nat-root-one-ℝ⁰⁺ : + (n : ℕ⁺) → nonzero-nat-root-ℝ⁰⁺ n one-ℝ⁰⁺ ＝ one-ℝ⁰⁺ + nonzero-nat-root-one-ℝ⁰⁺ (succ-ℕ n , H) = root-pair-expansion-one-ℝ⁰⁺ _ _ + nonzero-nat-root-one-ℝ⁰⁺ (0 , H) = ex-falso (H refl) +``` + +## See also + +- [Nonzero natural roots of positive real numbers](real-numbers.nonzero-natural-roots-positive-real-numbers.md) diff --git a/src/real-numbers/nonzero-natural-roots-positive-real-numbers.lagda.md b/src/real-numbers/nonzero-natural-roots-positive-real-numbers.lagda.md new file mode 100644 index 00000000000..ddcefb2cb6d --- /dev/null +++ b/src/real-numbers/nonzero-natural-roots-positive-real-numbers.lagda.md @@ -0,0 +1,245 @@ +# Nonzero natural roots of positive real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.nonzero-natural-roots-positive-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.integers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers + +open import foundation.action-on-identifications-functions +open import foundation.automorphisms +open import foundation.dependent-pair-types +open import foundation.empty-types +open import foundation.equivalences +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.retractions +open import foundation.sections +open import foundation.universe-levels + +open import real-numbers.integer-powers-positive-real-numbers +open import real-numbers.multiplication-positive-real-numbers +open import real-numbers.multiplication-real-numbers +open import real-numbers.multiplicative-inverses-positive-real-numbers +open import real-numbers.nonnegative-real-numbers +open import real-numbers.nonzero-natural-roots-nonnegative-real-numbers +open import real-numbers.odd-roots-positive-real-numbers +open import real-numbers.positive-and-negative-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.powers-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.square-roots-nonnegative-real-numbers +``` + +
+ +## Idea + +For any [nonzero](elementary-number-theory.nonzero-natural-numbers.md) +[natural number](elementary-number-theory.natural-numbers.md) `n`, there exists +an inverse to the [power function](real-numbers.powers-real-numbers.md) `x ↦ xⁿ` +on the [positive](real-numbers.positive-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md). + +## Definition + +```agda +abstract + preserves-is-positive-root-pair-expansion-ℝ⁰⁺ : + {l : Level} (u v : ℕ) (x : ℝ⁰⁺ l) → + is-positive-ℝ (real-ℝ⁰⁺ x) → + is-positive-ℝ (real-root-pair-expansion-ℝ⁰⁺ u v x) + preserves-is-positive-root-pair-expansion-ℝ⁰⁺ 0 v (x , _) 0Imports + +```agda +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.parity-natural-numbers + +open import foundation.dependent-pair-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.nonnegative-real-numbers +open import real-numbers.odd-roots-real-numbers +open import real-numbers.powers-real-numbers +``` + + + +## Idea + +[Odd roots](real-numbers.odd-roots-real-numbers.md) of +[nonnegative](real-numbers.nonnegative-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) are nonnegative. + +## Definition + +```agda +module _ + {l : Level} (n : ℕ) (odd-n : is-odd-ℕ n) + where + + abstract + is-nonnegative-odd-root-ℝ : + (x : ℝ l) → is-nonnegative-ℝ x → is-nonnegative-ℝ (odd-root-ℝ n odd-n x) + is-nonnegative-odd-root-ℝ x 0≤x = + tr + ( λ z → leq-ℝ z (odd-root-ℝ n odd-n x)) + ( odd-root-zero-ℝ n odd-n) + ( preserves-leq-odd-root-ℝ n odd-n 0≤x) + + odd-root-ℝ⁰⁺ : ℝ⁰⁺ l → ℝ⁰⁺ l + odd-root-ℝ⁰⁺ (x , 0≤x) = + ( odd-root-ℝ n odd-n x , is-nonnegative-odd-root-ℝ x 0≤x) + + odd-power-odd-root-ℝ⁰⁺ : + (x : ℝ⁰⁺ l) → power-ℝ n (real-ℝ⁰⁺ (odd-root-ℝ⁰⁺ x)) ＝ real-ℝ⁰⁺ x + odd-power-odd-root-ℝ⁰⁺ (x , _) = odd-power-odd-root-ℝ n odd-n x +``` diff --git a/src/real-numbers/odd-roots-positive-real-numbers.lagda.md b/src/real-numbers/odd-roots-positive-real-numbers.lagda.md new file mode 100644 index 00000000000..ea59bc7d398 --- /dev/null +++ b/src/real-numbers/odd-roots-positive-real-numbers.lagda.md @@ -0,0 +1,56 @@ +# Odd roots of positive real numbers + +```agda +module real-numbers.odd-roots-positive-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.parity-natural-numbers + +open import foundation.dependent-pair-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.odd-roots-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.powers-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + +
+ +## Idea + +[Odd roots](real-numbers.odd-roots-real-numbers.md) of +[positive](real-numbers.positive-real-numbers.md) +[real numbers](real-numbers.dedekind-real-numbers.md) are positive. + +## Definition + +```agda +module _ + {l : Level} (n : ℕ) (odd-n : is-odd-ℕ n) + where + + abstract + is-positive-odd-root-ℝ : + (x : ℝ l) → is-positive-ℝ x → is-positive-ℝ (odd-root-ℝ n odd-n x) + is-positive-odd-root-ℝ x 0≤x = + tr + ( λ z → le-ℝ z (odd-root-ℝ n odd-n x)) + ( odd-root-zero-ℝ n odd-n) + ( preserves-le-odd-root-ℝ n odd-n 0≤x) + + odd-root-ℝ⁺ : ℝ⁺ l → ℝ⁺ l + odd-root-ℝ⁺ (x , 0≤x) = + ( odd-root-ℝ n odd-n x , is-positive-odd-root-ℝ x 0≤x) + + odd-power-odd-root-ℝ⁺ : + (x : ℝ⁺ l) → power-ℝ n (real-ℝ⁺ (odd-root-ℝ⁺ x)) ＝ real-ℝ⁺ x + odd-power-odd-root-ℝ⁺ (x , _) = odd-power-odd-root-ℝ n odd-n x +``` diff --git a/src/real-numbers/odd-roots-real-numbers.lagda.md b/src/real-numbers/odd-roots-real-numbers.lagda.md new file mode 100644 index 00000000000..b93dbbe5e62 --- /dev/null +++ b/src/real-numbers/odd-roots-real-numbers.lagda.md @@ -0,0 +1,163 @@ +# Odd roots of real numbers + +```agda +{-# OPTIONS --lossy-unification #-} + +module real-numbers.odd-roots-real-numbers where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.parity-natural-numbers +open import elementary-number-theory.powers-rational-numbers + +open import foundation.binary-transport +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.universe-levels + +open import real-numbers.dedekind-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.invertibility-strictly-increasing-unbounded-continuous-functions-real-numbers +open import real-numbers.powers-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + +
+ +## Idea + +For any [odd](elementary-number-theory.parity-natural-numbers.md) +[natural number](elementary-number-theory.natural-numbers.md) `n`, the `n`th +{{#concept "root" Disambiguation="odd roots of real numbers" Agda=odd-root-ℝ}} +operation is a map from `ℝ` to `ℝ` that is the inverse operation to the `n`th +[power](real-numbers.powers-real-numbers.md). + +## Definition + +```agda +module _ + {l : Level} + (n : ℕ) + (odd-n : is-odd-ℕ n) + where + + opaque + odd-root-ℝ : ℝ l → ℝ l + odd-root-ℝ = map-inv-SIPCUB-function-ℝ (SIPCUB-odd-power-ℝ l n odd-n) + + abstract opaque + unfolding odd-root-ℝ + + odd-power-odd-root-ℝ : + (x : ℝ l) → power-ℝ n (odd-root-ℝ x) ＝ x + odd-power-odd-root-ℝ = + is-section-map-inv-SIPCUB-function-ℝ (SIPCUB-odd-power-ℝ l n odd-n) + + odd-root-odd-power-ℝ : + (x : ℝ l) → odd-root-ℝ (power-ℝ n x) ＝ x + odd-root-odd-power-ℝ = + is-retraction-map-inv-SIPCUB-function-ℝ (SIPCUB-odd-power-ℝ l n odd-n) +``` + +## Properties + +### Odd roots preserve strict inequality + +```agda +module _ + (n : ℕ) + (odd-n : is-odd-ℕ n) + where + + abstract + preserves-le-odd-root-ℝ : + {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → le-ℝ x y → + le-ℝ (odd-root-ℝ n odd-n x) (odd-root-ℝ n odd-n y) + preserves-le-odd-root-ℝ {x = x} {y = y} xImports + +```agda +open import elementary-number-theory.positive-rational-numbers + +open import foundation.axiom-of-countable-choice +open import foundation.dependent-pair-types +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import metric-spaces.pointwise-continuous-functions-metric-spaces + +open import real-numbers.dedekind-real-numbers +open import real-numbers.limits-of-functions-real-numbers +open import real-numbers.metric-space-of-real-numbers +``` + + + +## Idea + +A +{{#concept "pointwise continuous function" Disambiguation="from ℝ to ℝ" Agda=pointwise-continuous-function-ℝ}} +from the [real numbers](real-numbers.dedekind-real-numbers.md) to the real +numbers is a +[pointwise continuous function](metric-spaces.pointwise-continuous-functions-metric-spaces.md) +from the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md) to +itself. + +## Definition + +```agda +is-pointwise-continuous-prop-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → Prop (lsuc l1 ⊔ l2) +is-pointwise-continuous-prop-function-ℝ {l1} {l2} = + is-pointwise-continuous-prop-function-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + +is-pointwise-continuous-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → UU (lsuc l1 ⊔ l2) +is-pointwise-continuous-function-ℝ f = + type-Prop (is-pointwise-continuous-prop-function-ℝ f) + +pointwise-continuous-function-ℝ : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) +pointwise-continuous-function-ℝ l1 l2 = + type-subtype (is-pointwise-continuous-prop-function-ℝ {l1} {l2}) + +module _ + {l1 l2 : Level} + (f : pointwise-continuous-function-ℝ l1 l2) + where + + map-pointwise-continuous-function-ℝ : ℝ l1 → ℝ l2 + map-pointwise-continuous-function-ℝ = pr1 f + + is-pointwise-continuous-map-pointwise-continuous-function-ℝ : + is-pointwise-continuous-function-ℝ map-pointwise-continuous-function-ℝ + is-pointwise-continuous-map-pointwise-continuous-function-ℝ = pr2 f +``` + +### The classical definition of pointwise continuity + +```agda +module _ + {l1 l2 : Level} + (f : ℝ l1 → ℝ l2) + where + + is-classically-pointwise-continuous-prop-function-ℝ : Prop (lsuc l1 ⊔ l2) + is-classically-pointwise-continuous-prop-function-ℝ = + is-classically-pointwise-continuous-prop-function-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + ( f) + + is-classically-pointwise-continuous-function-ℝ : UU (lsuc l1 ⊔ l2) + is-classically-pointwise-continuous-function-ℝ = + type-Prop is-classically-pointwise-continuous-prop-function-ℝ +``` + +## Properties + +### Constructively pointwise continuous functions are classically pointwise continuous + +```agda +module _ + {l1 l2 : Level} + (f : pointwise-continuous-function-ℝ l1 l2) + where + + abstract + is-classically-pointwise-continuous-pointwise-continuous-function-ℝ : + is-classically-pointwise-continuous-function-ℝ + ( map-pointwise-continuous-function-ℝ f) + is-classically-pointwise-continuous-pointwise-continuous-function-ℝ = + is-classically-pointwise-continuous-pointwise-continuous-function-Metric-Space + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + ( f) +``` + +### Assuming countable choice, the classical definition of continuity implies the constructive definition + +```agda +module _ + {l1 l2 : Level} + (acω : ACω) + (f : ℝ l1 → ℝ l2) + where + + abstract + is-pointwise-continuous-is-classically-pointwise-continuous-ACω-function-ℝ : + is-classically-pointwise-continuous-function-ℝ f → + is-pointwise-continuous-function-ℝ f + is-pointwise-continuous-is-classically-pointwise-continuous-ACω-function-ℝ = + is-pointwise-continuous-is-classically-pointwise-continuous-ACω-function-Metric-Space + ( acω) + ( metric-space-ℝ l1) + ( metric-space-ℝ l2) + ( f) +``` diff --git a/src/real-numbers/positive-real-numbers.lagda.md b/src/real-numbers/positive-real-numbers.lagda.md index fb8e67e3f34..45a605a9855 100644 --- a/src/real-numbers/positive-real-numbers.lagda.md +++ b/src/real-numbers/positive-real-numbers.lagda.md @@ -29,6 +29,7 @@ open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions +open import foundation.sets open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.universe-levels @@ -83,6 +84,13 @@ is-positive-real-ℝ⁺ = pr2 ## Properties +### The positive real numbers form a set + +```agda +ℝ⁺-Set : (l : Level) → Set (lsuc l) +ℝ⁺-Set l = set-subset (ℝ-Set l) is-positive-prop-ℝ +``` + ### Positivity is preserved by similarity ```agda @@ -335,7 +343,22 @@ abstract ### Raising the universe level of positive real numbers ```agda +abstract + preserves-is-positive-raise-ℝ : + {l1 : Level} (l : Level) (x : ℝ l1) → is-positive-ℝ x → + is-positive-ℝ (raise-ℝ l x) + preserves-is-positive-raise-ℝ l x 0 @@ -75,6 +89,34 @@ power-ℝ = power-Large-Commutative-Ring large-commutative-ring-ℝ ## Properties +### The power operation preserves similarity + +```agda +abstract + preserves-sim-power-ℝ : + {l1 l2 : Level} (n : ℕ) {x : ℝ l1} {y : ℝ l2} → sim-ℝ x y → + sim-ℝ (power-ℝ n x) (power-ℝ n y) + preserves-sim-power-ℝ n = + preserves-sim-power-Large-Commutative-Ring large-commutative-ring-ℝ n _ _ +``` + +### The power operation commutes with raising universe level + +```agda +abstract + power-raise-ℝ : + {l0 : Level} (l : Level) (n : ℕ) (x : ℝ l0) → + power-ℝ n (raise-ℝ l x) ＝ raise-ℝ l (power-ℝ n x) + power-raise-ℝ l n x = + eq-sim-ℝ + ( similarity-reasoning-ℝ + power-ℝ n (raise-ℝ l x) + ~ℝ power-ℝ n x + by preserves-sim-power-ℝ n (sim-raise-ℝ' l x) + ~ℝ raise-ℝ l (power-ℝ n x) + by sim-raise-ℝ l _) +``` + ### The canonical embedding of rational numbers preserves powers ```agda @@ -88,6 +130,13 @@ abstract ( hom-ring-real-ℚ) ( n) ( q)) + + raise-power-real-ℚ : + (l : Level) (n : ℕ) (q : ℚ) → + power-ℝ n (raise-real-ℚ l q) ＝ raise-real-ℚ l (power-ℚ n q) + raise-power-real-ℚ l n q = + ( power-raise-ℝ l n (real-ℚ q)) ∙ + ( ap (raise-ℝ l) (power-real-ℚ n q)) ``` ### `1ⁿ ＝ 1` @@ -98,6 +147,16 @@ abstract power-one-ℝ = power-one-Large-Commutative-Ring large-commutative-ring-ℝ ``` +### `0ⁿ = 0` for nonzero `n` + +```agda +abstract + nonzero-power-zero-ℝ : + (n : ℕ⁺) → power-ℝ (nat-nonzero-ℕ n) zero-ℝ ＝ zero-ℝ + nonzero-power-zero-ℝ = + nonzero-power-zero-Large-Commutative-Ring large-commutative-ring-ℝ +``` + ### `xⁿ⁺¹ = xⁿx` ```agda @@ -116,15 +175,38 @@ abstract power-succ-ℝ' = power-succ-Large-Commutative-Ring' large-commutative-ring-ℝ ``` -### Powers by sums of natural numbers are products of powers +### Powers of positive real numbers are positive ```agda abstract - distributive-power-add-ℝ : - {l : Level} (m n : ℕ) {x : ℝ l} → - power-ℝ (m +ℕ n) x ＝ power-ℝ m x *ℝ power-ℝ n x - distributive-power-add-ℝ = - distributive-power-add-Large-Commutative-Ring large-commutative-ring-ℝ + is-positive-power-ℝ⁺ : + {l : Level} (n : ℕ) (x : ℝ⁺ l) → is-positive-ℝ (power-ℝ n (real-ℝ⁺ x)) + is-positive-power-ℝ⁺ 0 _ = + is-positive-sim-ℝ (sim-raise-ℝ _ _) (is-positive-real-ℝ⁺ one-ℝ⁺) + is-positive-power-ℝ⁺ 1 (_ , is-pos-x) = is-pos-x + is-positive-power-ℝ⁺ (succ-ℕ n@(succ-ℕ _)) x⁺@(x , is-pos-x) = + is-positive-mul-ℝ (is-positive-power-ℝ⁺ n x⁺) is-pos-x + +power-ℝ⁺ : {l : Level} → ℕ → ℝ⁺ l → ℝ⁺ l +power-ℝ⁺ n x⁺@(x , _) = (power-ℝ n x , is-positive-power-ℝ⁺ n x⁺) +``` + +### Powers of nonnegative real numbers are nonnegative + +```agda +abstract + is-nonnegative-power-ℝ⁰⁺ : + {l : Level} (n : ℕ) (x : ℝ⁰⁺ l) → is-nonnegative-ℝ (power-ℝ n (real-ℝ⁰⁺ x)) + is-nonnegative-power-ℝ⁰⁺ {l} 0 _ = + is-nonnegative-real-ℝ⁰⁺ (raise-ℝ⁰⁺ l one-ℝ⁰⁺) + is-nonnegative-power-ℝ⁰⁺ 1 (x , is-nonneg-x) = is-nonneg-x + is-nonnegative-power-ℝ⁰⁺ (succ-ℕ n@(succ-ℕ _)) x⁰⁺@(x , is-nonneg-x) = + is-nonnegative-mul-ℝ + ( is-nonnegative-power-ℝ⁰⁺ n x⁰⁺) + ( is-nonneg-x) + +power-ℝ⁰⁺ : {l : Level} → ℕ → ℝ⁰⁺ l → ℝ⁰⁺ l +power-ℝ⁰⁺ n x⁰⁺@(x , _) = (power-ℝ n x , is-nonnegative-power-ℝ⁰⁺ n x⁰⁺) ``` ### Powers by products of natural numbers are iterated powers @@ -147,6 +229,22 @@ abstract by ap (λ k → power-ℝ k x) (commutative-mul-ℕ m n) ＝ power-ℝ m (power-ℝ n x) by power-mul-ℝ n m + + power-mul-ℝ⁰⁺ : + {l : Level} (m n : ℕ) (x : ℝ⁰⁺ l) → + power-ℝ⁰⁺ (m *ℕ n) x ＝ power-ℝ⁰⁺ n (power-ℝ⁰⁺ m x) + power-mul-ℝ⁰⁺ m n x = eq-ℝ⁰⁺ _ _ (power-mul-ℝ m n) +``` + +### Powers by sums of natural numbers are products of powers + +```agda +abstract + distributive-power-add-ℝ : + {l : Level} (m n : ℕ) {x : ℝ l} → + power-ℝ (m +ℕ n) x ＝ power-ℝ m x *ℝ power-ℝ n x + distributive-power-add-ℝ = + distributive-power-add-Large-Commutative-Ring large-commutative-ring-ℝ ``` ### `(xy)ⁿ = xⁿyⁿ` @@ -158,6 +256,12 @@ abstract power-ℝ n (x *ℝ y) ＝ power-ℝ n x *ℝ power-ℝ n y distributive-power-mul-ℝ = distributive-power-mul-Large-Commutative-Ring large-commutative-ring-ℝ + + distributive-power-mul-ℝ⁰⁺ : + {l1 l2 : Level} (n : ℕ) (x : ℝ⁰⁺ l1) (y : ℝ⁰⁺ l2) → + power-ℝ⁰⁺ n (x *ℝ⁰⁺ y) ＝ power-ℝ⁰⁺ n x *ℝ⁰⁺ power-ℝ⁰⁺ n y + distributive-power-mul-ℝ⁰⁺ n _ _ = + eq-ℝ⁰⁺ _ _ (distributive-power-mul-ℝ n) ``` ### Even powers of real numbers are nonnegative @@ -177,40 +281,6 @@ nonnegative-even-power-ℝ n x even-n = ( power-ℝ n x , is-nonnegative-even-power-ℝ n x even-n) ``` -### Powers of positive real numbers are positive - -```agda -abstract - is-positive-power-ℝ⁺ : - {l : Level} (n : ℕ) (x : ℝ⁺ l) → is-positive-ℝ (power-ℝ n (real-ℝ⁺ x)) - is-positive-power-ℝ⁺ 0 _ = - is-positive-sim-ℝ (sim-raise-ℝ _ _) (is-positive-real-ℝ⁺ one-ℝ⁺) - is-positive-power-ℝ⁺ 1 (_ , is-pos-x) = is-pos-x - is-positive-power-ℝ⁺ (succ-ℕ n@(succ-ℕ _)) x⁺@(x , is-pos-x) = - is-positive-mul-ℝ (is-positive-power-ℝ⁺ n x⁺) is-pos-x - -power-ℝ⁺ : {l : Level} → ℕ → ℝ⁺ l → ℝ⁺ l -power-ℝ⁺ n x⁺@(x , _) = (power-ℝ n x , is-positive-power-ℝ⁺ n x⁺) -``` - -### Powers of nonnegative real numbers are nonnegative - -```agda -abstract - is-nonnegative-power-ℝ⁰⁺ : - {l : Level} (n : ℕ) (x : ℝ⁰⁺ l) → is-nonnegative-ℝ (power-ℝ n (real-ℝ⁰⁺ x)) - is-nonnegative-power-ℝ⁰⁺ {l} 0 _ = - is-nonnegative-real-ℝ⁰⁺ (raise-ℝ⁰⁺ l one-ℝ⁰⁺) - is-nonnegative-power-ℝ⁰⁺ 1 (x , is-nonneg-x) = is-nonneg-x - is-nonnegative-power-ℝ⁰⁺ (succ-ℕ n@(succ-ℕ _)) x⁰⁺@(x , is-nonneg-x) = - is-nonnegative-mul-ℝ - ( is-nonnegative-power-ℝ⁰⁺ n x⁰⁺) - ( is-nonneg-x) - -power-ℝ⁰⁺ : {l : Level} → ℕ → ℝ⁰⁺ l → ℝ⁰⁺ l -power-ℝ⁰⁺ n x⁰⁺@(x , _) = (power-ℝ n x , is-nonnegative-power-ℝ⁰⁺ n x⁰⁺) -``` - ### Even powers of negative real numbers are positive ```agda @@ -431,3 +501,253 @@ abstract ≤ real-ℚ⁺ (power-ℚ⁺ n ε⁺) by leq-eq-ℝ (ap real-ℚ (power-rational-ℚ⁺ n ε⁺))) ``` + +### For any `n`, `power-ℝ n` is pointwise continuous + +```agda +abstract + is-pointwise-continuous-power-ℝ : + {l : Level} (n : ℕ) → is-pointwise-continuous-function-ℝ {l} (power-ℝ n) + is-pointwise-continuous-power-ℝ 0 = + is-pointwise-continuous-constant-function-Metric-Space _ _ _ + is-pointwise-continuous-power-ℝ 1 = + is-pointwise-continuous-id-Metric-Space _ + is-pointwise-continuous-power-ℝ {l} (succ-ℕ n@(succ-ℕ _)) = + is-pointwise-continuous-map-comp-pointwise-continuous-function-Metric-Space + ( metric-space-ℝ l) + ( product-Metric-Space (metric-space-ℝ l) (metric-space-ℝ l)) + ( metric-space-ℝ l) + ( ind-Σ mul-ℝ , is-pointwise-continuous-mul-ℝ l l) + ( comp-pointwise-continuous-function-Metric-Space + ( metric-space-ℝ l) + ( product-Metric-Space (metric-space-ℝ l) (metric-space-ℝ l)) + ( product-Metric-Space (metric-space-ℝ l) (metric-space-ℝ l)) + ( product-pointwise-continuous-function-Metric-Space + ( metric-space-ℝ l) + ( metric-space-ℝ l) + ( metric-space-ℝ l) + ( metric-space-ℝ l) + ( power-ℝ n , is-pointwise-continuous-power-ℝ n) + ( pointwise-continuous-id-Metric-Space (metric-space-ℝ l))) + ( pointwise-continuous-isometry-Metric-Space + ( metric-space-ℝ l) + ( product-Metric-Space (metric-space-ℝ l) (metric-space-ℝ l)) + ( diagonal-isometry-product-Metric-Space (metric-space-ℝ l)))) + +pointwise-continuous-power-ℝ : + (l : Level) (n : ℕ) → pointwise-continuous-function-ℝ l l +pointwise-continuous-power-ℝ l n = + ( power-ℝ n , is-pointwise-continuous-power-ℝ n) +``` + +### Odd powers of real numbers preserve strict inequality + +```agda +abstract + is-strictly-increasing-odd-power-ℝ : + (l : Level) (n : ℕ) → is-odd-ℕ n → + is-strictly-increasing-function-ℝ (power-ℝ {l} n) + is-strictly-increasing-odd-power-ℝ l n odd-n = + is-strictly-increasing-is-strictly-increasing-rational-ℝ + ( pointwise-continuous-power-ℝ l n) + ( λ p q pImports + +```agda +open import elementary-number-theory.addition-positive-rational-numbers +open import elementary-number-theory.addition-rational-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.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.propositional-truncations +open import foundation.raising-universe-levels +open import foundation.universe-levels + +open import logic.functoriality-existential-quantification + +open import metric-spaces.dense-subsets-metric-spaces + +open import real-numbers.arithmetically-located-dedekind-cuts +open import real-numbers.dedekind-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.rational-real-numbers +``` + + + +## Idea + +A +{{#concept "rational approximation" Disambiguation="of a real number" Agda=rational-approximation-ℝ}} +of a [real number](real-numbers.dedekind-real-numbers.md) `x` to some +[positive rational](elementary-number-theory.positive-rational-numbers.md) `ε` +is a [rational number](elementary-number-theory.rational-numbers.md) whose +[canonical embedding](real-numbers.rational-real-numbers.md) in the real numbers +is within an `ε`-neighborhood of `x` in the +[metric space of real numbers](real-numbers.metric-space-of-real-numbers.md). + +## Definition + +```agda +rational-approximation-ℝ : {l : Level} → ℝ l → ℚ⁺ → UU l +rational-approximation-ℝ {l} x ε = + Σ ℚ (λ q → neighborhood-ℝ l ε x (raise-real-ℚ l q)) + +rational-approximation-above-ℝ : {l : Level} → ℝ l → ℚ⁺ → UU l +rational-approximation-above-ℝ {l} x ε = + Σ ℚ (λ q → is-in-upper-cut-ℝ x q × neighborhood-ℝ l ε x (raise-real-ℚ l q)) + +rational-approximation-below-ℝ : {l : Level} → ℝ l → ℚ⁺ → UU l +rational-approximation-below-ℝ {l} x ε = + Σ ℚ (λ q → is-in-lower-cut-ℝ x q × neighborhood-ℝ l ε x (raise-real-ℚ l q)) +``` + +## Properties + +### Any real number can be approximated below to any positive rational precision `ε` + +```agda +abstract opaque + unfolding neighborhood-ℝ real-ℚ + + exists-rational-approximation-below-ℝ : + {l : Level} (x : ℝ l) (ε : ℚ⁺) → + type-trunc-Prop (rational-approximation-below-ℝ x ε) + exists-rational-approximation-below-ℝ {l} x ε⁺@(ε , _) = + let + open + do-syntax-trunc-Prop + ( trunc-Prop (rational-approximation-below-ℝ x ε⁺)) + in do + ((p , q) , qImports + +```agda +open import elementary-number-theory.addition-integer-fractions +open import elementary-number-theory.addition-rational-numbers +open import elementary-number-theory.integers +open import elementary-number-theory.multiplication-integer-fractions +open import elementary-number-theory.multiplication-rational-numbers +open import elementary-number-theory.multiplicative-group-of-positive-rational-numbers +open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers +open import elementary-number-theory.positive-integers +open import elementary-number-theory.positive-rational-numbers +open import elementary-number-theory.rational-numbers +open import elementary-number-theory.reduced-integer-fractions +open import elementary-number-theory.unit-fractions-rational-numbers + +open import foundation.action-on-identifications-binary-functions +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.universe-levels + +open import real-numbers.integer-fraction-powers-positive-real-numbers +open import real-numbers.integer-powers-positive-real-numbers +open import real-numbers.multiplication-positive-real-numbers +open import real-numbers.multiplicative-inverses-positive-real-numbers +open import real-numbers.nonzero-natural-roots-positive-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.powers-real-numbers +open import real-numbers.raising-universe-levels-real-numbers +open import real-numbers.rational-real-numbers +``` + + + +## Idea + +We define the +{{#concept "power operation" Disambiguation="positive reals to rational powers" Agda=rational-power-ℝ⁺}} +raising [positive real numbers](real-numbers.positive-real-numbers.md) to +[rational](elementary-number-theory.rational-numbers.md) powers in terms of the +corresponding +[operation](real-numbers.integer-fraction-powers-positive-real-numbers.md) on +[integer fractions](elementary-number-theory.integer-fractions.md). + +## Definition + +```agda +rational-power-ℝ⁺ : {l : Level} → ℚ → ℝ⁺ l → ℝ⁺ l +rational-power-ℝ⁺ q = + int-fraction-power-ℝ⁺ (fraction-ℚ q) +``` + +## Properties + +### `xᵃ⁺ᵇ = xᵃxᵇ` + +```agda +abstract opaque + unfolding add-ℚ rational-fraction-ℤ + + distributive-power-add-rational-power-ℝ⁺ : + {l : Level} (p q : ℚ) (x : ℝ⁺ l) → + rational-power-ℝ⁺ (p +ℚ q) x ＝ + rational-power-ℝ⁺ p x *ℝ⁺ rational-power-ℝ⁺ q x + distributive-power-add-rational-power-ℝ⁺ p q x = + equational-reasoning + int-fraction-power-ℝ⁺ + ( reduce-fraction-ℤ (fraction-ℚ p +fraction-ℤ fraction-ℚ q)) + ( x) + ＝ int-fraction-power-ℝ⁺ (fraction-ℚ p +fraction-ℤ fraction-ℚ q) x + by inv (reduce-int-fraction-power-ℝ⁺ _ x) + ＝ + ( int-fraction-power-ℝ⁺ (fraction-ℚ p) x) *ℝ⁺ + ( int-fraction-power-ℝ⁺ (fraction-ℚ q) x) + by distributive-add-integer-fraction-power-ℝ⁺ _ _ x +``` + +### `xᵃᵇ = (xᵃ)ᵇ` + +```agda +abstract opaque + unfolding mul-ℚ rational-fraction-ℤ + + power-mul-rational-power-ℝ⁺ : + {l : Level} (p q : ℚ) (x : ℝ⁺ l) → + rational-power-ℝ⁺ (p *ℚ q) x ＝ rational-power-ℝ⁺ q (rational-power-ℝ⁺ p x) + power-mul-rational-power-ℝ⁺ p q x = + equational-reasoning + int-fraction-power-ℝ⁺ + ( reduce-fraction-ℤ (fraction-ℚ p *fraction-ℤ fraction-ℚ q)) + ( x) + ＝ int-fraction-power-ℝ⁺ (fraction-ℚ p *fraction-ℤ fraction-ℚ q) x + by inv (reduce-int-fraction-power-ℝ⁺ _ x) + ＝ rational-power-ℝ⁺ q (rational-power-ℝ⁺ p x) + by mul-int-fraction-power-ℝ⁺ _ _ x +``` + +### `(xy)ᵃ = xᵃyᵃ` + +```agda +abstract + distributive-rational-power-mul-ℝ⁺ : + {l1 l2 : Level} (q : ℚ) (x : ℝ⁺ l1) (y : ℝ⁺ l2) → + rational-power-ℝ⁺ q (x *ℝ⁺ y) ＝ + rational-power-ℝ⁺ q x *ℝ⁺ rational-power-ℝ⁺ q y + distributive-rational-power-mul-ℝ⁺ q = + distributive-int-fraction-power-mul-ℝ⁺ (fraction-ℚ q) +``` + +### `x⁻ᵃ` is the multiplicative inverse of `xᵃ` + +```agda +abstract opaque + unfolding neg-ℚ + + neg-rational-power-ℝ⁺ : + {l : Level} (q : ℚ) (x : ℝ⁺ l) → + rational-power-ℝ⁺ (neg-ℚ q) x ＝ inv-ℝ⁺ (rational-power-ℝ⁺ q x) + neg-rational-power-ℝ⁺ q = + neg-int-fraction-power-ℝ⁺ (fraction-ℚ q) +``` + +### The canonical embedding of integers in the rational numbers preserves powers of positive real numbers + +```agda +abstract + rational-ℤ-power-ℝ⁺ : + {l : Level} (k : ℤ) (x : ℝ⁺ l) → + rational-power-ℝ⁺ (rational-ℤ k) x ＝ int-power-ℝ⁺ k x + rational-ℤ-power-ℝ⁺ = int-fraction-in-fraction-power-ℝ⁺ +``` + +### The canonical embedding of natural numbers in the rational numbers preserves powers of positive real numbers + +```agda +abstract + rational-ℕ-power-ℝ⁺ : + {l : Level} (n : ℕ) (x : ℝ⁺ l) → + rational-power-ℝ⁺ (rational-ℕ n) x ＝ power-ℝ⁺ n x + rational-ℕ-power-ℝ⁺ n x = + rational-ℤ-power-ℝ⁺ (int-ℕ n) x ∙ int-power-int-ℝ⁺ n x +``` + +### `x¹ = x` + +```agda +abstract + one-ℚ-power-ℝ⁺ : + {l : Level} (x : ℝ⁺ l) → rational-power-ℝ⁺ one-ℚ x ＝ x + one-ℚ-power-ℝ⁺ x = + rational-ℕ-power-ℝ⁺ 1 x ∙ eq-ℝ⁺ _ _ (refl {x = real-ℝ⁺ x}) +``` + +### `x⁰ = 1` + +```agda +abstract + zero-ℚ-power-ℝ⁺ : + {l : Level} (x : ℝ⁺ l) → rational-power-ℝ⁺ zero-ℚ x ＝ raise-ℝ⁺ l one-ℝ⁺ + zero-ℚ-power-ℝ⁺ {l} x = + rational-ℕ-power-ℝ⁺ 0 x ∙ eq-ℝ⁺ _ _ (refl {x = raise-ℝ l one-ℝ}) +``` + +### `x⁻¹` is the multiplicative inverse of `x` + +```agda +abstract + neg-one-ℚ-power-ℝ⁺ : + {l : Level} (x : ℝ⁺ l) → rational-power-ℝ⁺ neg-one-ℚ x ＝ inv-ℝ⁺ x + neg-one-ℚ-power-ℝ⁺ x = + rational-ℤ-power-ℝ⁺ neg-one-ℤ x ∙ int-neg-one-power-ℝ⁺ x +``` + +### `x` to the `1/n` power is the `n`th root of `x` + +```agda +abstract opaque + unfolding is-positive-rational-ℤ inv-ℚ⁺ + + reciprocal-rational-ℕ⁺-power-ℝ⁺ : + {l : Level} (n : ℕ⁺) (x : ℝ⁺ l) → + rational-power-ℝ⁺ (reciprocal-rational-ℕ⁺ n) x ＝ + nonzero-nat-root-ℝ⁺ n x + reciprocal-rational-ℕ⁺-power-ℝ⁺ n x = + ap-binary + ( nonzero-nat-root-ℝ⁺) + ( is-retraction-positive-nat-ℤ⁺ n) + ( int-one-power-ℝ⁺ x) +``` + +### `1ᵃ = 1` + +```agda +abstract + rational-power-one-ℝ⁺ : + (q : ℚ) → rational-power-ℝ⁺ q one-ℝ⁺ ＝ one-ℝ⁺ + rational-power-one-ℝ⁺ q = int-fraction-power-one-ℝ⁺ (fraction-ℚ q) +``` diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index 3a435d07231..b72d292874f 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -28,6 +28,7 @@ open import foundation.injective-maps open import foundation.negated-equality open import foundation.negation open import foundation.propositions +open import foundation.raising-universe-levels open import foundation.retractions open import foundation.sections open import foundation.subtypes @@ -208,17 +209,33 @@ module _ ### The real embedding of a rational number is rational ```agda -opaque +abstract opaque unfolding real-ℚ is-rational-real-ℚ : (p : ℚ) → is-rational-ℝ (real-ℚ p) p is-rational-real-ℚ p = (irreflexive-le-ℚ p , irreflexive-le-ℚ p) ``` +### A rational real number raised to another universe level is rational + +```agda +abstract + is-rational-raise-ℝ : + {l0 : Level} (l : Level) (x : ℝ l0) {q : ℚ} → + is-rational-ℝ x q → is-rational-ℝ (raise-ℝ l x) q + is-rational-raise-ℝ l x (q≮x , x≮q) = + ( q≮x ∘ map-inv-raise , x≮q ∘ map-inv-raise) + + is-rational-raise-real-ℚ : + (l : Level) (p : ℚ) → is-rational-ℝ (raise-real-ℚ l p) p + is-rational-raise-real-ℚ l p = + is-rational-raise-ℝ l (real-ℚ p) (is-rational-real-ℚ p) +``` + ### Rational real numbers are embedded rationals ```agda -opaque +abstract opaque unfolding real-ℚ sim-ℝ sim-rational-ℝ : @@ -239,10 +256,22 @@ opaque ( ex-falso ∘ q∉ux) ( is-located-lower-upper-cut-ℝ x pImports + +```agda +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.dependent-pair-types +open import foundation.embeddings +open import foundation.function-types +open import foundation.identity-types +open import foundation.injective-maps +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.sets +open import foundation.subtypes +open import foundation.universe-levels + +open import order-theory.large-posets + +open import real-numbers.addition-positive-real-numbers +open import real-numbers.addition-real-numbers +open import real-numbers.dedekind-real-numbers +open import real-numbers.dense-subsets-real-numbers +open import real-numbers.increasing-functions-real-numbers +open import real-numbers.inequality-real-numbers +open import real-numbers.metric-space-of-real-numbers +open import real-numbers.pointwise-continuous-functions-real-numbers +open import real-numbers.positive-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequalities-addition-and-subtraction-real-numbers +open import real-numbers.strict-inequality-real-numbers +open import real-numbers.subsets-real-numbers +``` + + + +## Idea + +A function `f` from the [real numbers](real-numbers.dedekind-real-numbers.md) to +themselves is +{{#concept "strictly increasing" WDID=Q78055984 WD="strictly increasing function" Disambiguation="function from ℝ to ℝ" Agda=is-strictly-increasing-function-ℝ}} +if for all `x < y`, `f x < f y`. + +Several arguments on this page are due to +[Mark Saving](https://math.stackexchange.com/users/798694/mark-saving) in this +Mathematics Stack Exchange answer: . + +## Definition + +```agda +is-strictly-increasing-prop-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → Prop (lsuc l1 ⊔ l2) +is-strictly-increasing-prop-function-ℝ {l1} {l2} f = + Π-Prop + ( ℝ l1) + ( λ x → + Π-Prop + ( ℝ l1) + ( λ y → le-prop-ℝ x y ⇒ le-prop-ℝ (f x) (f y))) + +is-strictly-increasing-function-ℝ : + {l1 l2 : Level} → (ℝ l1 → ℝ l2) → UU (lsuc l1 ⊔ l2) +is-strictly-increasing-function-ℝ f = + type-Prop (is-strictly-increasing-prop-function-ℝ f) + +is-strictly-increasing-on-subset-function-ℝ : + {l1 l2 l3 : Level} → (ℝ l1 → ℝ l2) → subset-ℝ l3 l1 → UU (lsuc l1 ⊔ l2 ⊔ l3) +is-strictly-increasing-on-subset-function-ℝ f S = + (x y : type-subset-ℝ S) → le-ℝ (pr1 x) (pr1 y) → le-ℝ (f (pr1 x)) (f (pr1 y)) +``` + +## Properties + +### A strictly increasing function is increasing + +```agda +module _ + {l1 l2 : Level} + (f : ℝ l1 → ℝ l2) + where + + abstract + is-increasing-is-strictly-increasing-function-ℝ : + is-strictly-increasing-function-ℝ f → is-increasing-function-ℝ f + is-increasing-is-strictly-increasing-function-ℝ H = + is-increasing-leq-le-ℝ f (λ x y xImports + +```agda +open import elementary-number-theory.rational-numbers + +open import foundation.conjunction +open import foundation.existential-quantification +open import foundation.propositions +open import foundation.universe-levels + +open import real-numbers.dedekind-real-numbers +open import real-numbers.rational-real-numbers +open import real-numbers.strict-inequality-real-numbers +``` + + + +## Idea + +A function is: + +- unbounded below if for every + [rational](elementary-number-theory.rational-numbers.md) `q`, there + [exists](foundation.existential-quantification.md) `x : ℝ` such that `f x < q` +- unbounded above if for every + [rational](elementary-number-theory.rational-numbers.md) `q`, there + [exists](foundation.existential-quantification.md) `x : ℝ` such that `q < f x` +- {{#concept "unbounded" Agda=is-unbounded-function-ℝ Disambiguation="function on ℝ"}} + if it is both unbounded above and below + +## Definition + +```agda +module _ + {l1 l2 : Level} + (f : ℝ l1 → ℝ l2) + where + + is-unbounded-above-prop-function-ℝ : Prop (lsuc l1 ⊔ l2) + is-unbounded-above-prop-function-ℝ = + Π-Prop ℚ (λ q → ∃ (ℝ l1) (λ x → le-prop-ℝ (real-ℚ q) (f x))) + + is-unbounded-above-function-ℝ : UU (lsuc l1 ⊔ l2) + is-unbounded-above-function-ℝ = type-Prop is-unbounded-above-prop-function-ℝ + + is-unbounded-below-prop-function-ℝ : Prop (lsuc l1 ⊔ l2) + is-unbounded-below-prop-function-ℝ = + Π-Prop ℚ (λ q → ∃ (ℝ l1) (λ x → le-prop-ℝ (f x) (real-ℚ q))) + + is-unbounded-below-function-ℝ : UU (lsuc l1 ⊔ l2) + is-unbounded-below-function-ℝ = type-Prop is-unbounded-below-prop-function-ℝ + + is-unbounded-prop-function-ℝ : Prop (lsuc l1 ⊔ l2) + is-unbounded-prop-function-ℝ = + is-unbounded-above-prop-function-ℝ ∧ is-unbounded-below-prop-function-ℝ + + is-unbounded-function-ℝ : UU (lsuc l1 ⊔ l2) + is-unbounded-function-ℝ = type-Prop is-unbounded-prop-function-ℝ +``` diff --git a/src/ring-theory/large-rings.lagda.md b/src/ring-theory/large-rings.lagda.md index 9b8228761d3..9c5d1e4c156 100644 --- a/src/ring-theory/large-rings.lagda.md +++ b/src/ring-theory/large-rings.lagda.md @@ -7,6 +7,7 @@ module ring-theory.large-rings where
Imports ```agda +open import foundation.action-on-identifications-binary-functions open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.large-binary-relations @@ -114,6 +115,13 @@ record Large-Ring (α : Level → Level) (β : Level → Level → Level) : UUω mul-Large-Ring (add-Large-Ring a b) c ＝ add-Large-Ring (mul-Large-Ring a c) (mul-Large-Ring b c) + ap-mul-Large-Ring : + {l1 l2 : Level} + {x x' : type-Large-Ring l1} → x ＝ x' → + {y y' : type-Large-Ring l2} → y ＝ y' → + mul-Large-Ring x y ＝ mul-Large-Ring x' y' + ap-mul-Large-Ring = ap-binary mul-Large-Ring + open Large-Ring public ``` @@ -148,6 +156,11 @@ module _ sim-Large-Ring R y z → sim-Large-Ring R x y → sim-Large-Ring R x z transitive-sim-Large-Ring = transitive-sim-Large-Ab (large-ab-Large-Ring R) + + eq-sim-Large-Ring : + {l : Level} {x y : type-Large-Ring R l} → + sim-Large-Ring R x y → x ＝ y + eq-sim-Large-Ring = eq-sim-Large-Ab (large-ab-Large-Ring R) ``` ### Raising universe levels @@ -327,3 +340,25 @@ module _ ( _)) , raise-raise-Large-Ring R _) ``` + +### Zero laws of multiplication + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} (R : Large-Ring α β) + where + + abstract + sim-right-zero-law-Large-Ring : + {l : Level} (a : type-Large-Ring R l) → + sim-Large-Ring + ( R) + ( mul-Large-Ring R a (zero-Large-Ring R)) + ( zero-Large-Ring R) + sim-right-zero-law-Large-Ring a = + sim-zero-is-idempotent-add-Large-Ab + ( large-ab-Large-Ring R) + ( mul-Large-Ring R a (zero-Large-Ring R)) + ( ( inv (left-distributive-mul-add-Large-Ring R _ _ _)) ∙ + ( ap-mul-Large-Ring R refl (left-unit-law-add-Large-Ring R _))) +``` diff --git a/src/ring-theory/powers-of-elements-large-rings.lagda.md b/src/ring-theory/powers-of-elements-large-rings.lagda.md index 7552fe1a2a9..6a0c604c442 100644 --- a/src/ring-theory/powers-of-elements-large-rings.lagda.md +++ b/src/ring-theory/powers-of-elements-large-rings.lagda.md @@ -10,7 +10,10 @@ module ring-theory.powers-of-elements-large-rings where open import elementary-number-theory.addition-natural-numbers open import elementary-number-theory.multiplication-natural-numbers open import elementary-number-theory.natural-numbers +open import elementary-number-theory.nonzero-natural-numbers +open import foundation.dependent-pair-types +open import foundation.empty-types open import foundation.identity-types open import foundation.universe-levels @@ -85,6 +88,24 @@ module _ ( multiplicative-large-monoid-Large-Ring R) ``` +### `0ⁿ = 0` for nonzero `n` + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} (R : Large-Ring α β) + where + + abstract + nonzero-power-zero-Large-Ring : + (n : ℕ⁺) → + ( power-Large-Ring R (nat-nonzero-ℕ n) (zero-Large-Ring R) ＝ + zero-Large-Ring R) + nonzero-power-zero-Large-Ring (0 , H) = ex-falso (H refl) + nonzero-power-zero-Large-Ring (1 , H) = refl + nonzero-power-zero-Large-Ring (succ-ℕ n@(succ-ℕ _) , H) = + eq-sim-Large-Ring R (sim-right-zero-law-Large-Ring R _) +``` + ### `xⁿ⁺¹ = xⁿx` ```agda @@ -152,3 +173,20 @@ module _ power-mul-Large-Monoid ( multiplicative-large-monoid-Large-Ring R) ``` + +### Iterated powers commute + +```agda +module _ + {α : Level → Level} {β : Level → Level → Level} (R : Large-Ring α β) + where + + abstract + commute-power-Large-Ring : + {l : Level} (m n : ℕ) (x : type-Large-Ring R l) → + power-Large-Ring R m (power-Large-Ring R n x) ＝ + power-Large-Ring R n (power-Large-Ring R m x) + commute-power-Large-Ring = + commute-power-Large-Monoid + ( multiplicative-large-monoid-Large-Ring R) +```