The product rule

Author: lowasser

references.bib

@@ -158,6 +158,16 @@ @misc{BH25
   primaryclass  = {math.LO},
 }
 
+@book{BishopFoundations,
+  title         = {Foundations of constructive analysis},
+  author        = {Bishop, Errett},
+  year          = 2012,
+  publisher     = {Ishi Press International},
+  address       = {New York ; Tokyo},
+  isbn          = 9784871877145,
+  language      = {eng},
+}
+
 @phdthesis{Booij20PhD,
   title         = {Analysis in univalent type theory},
   author        = {Booij, Auke Bart},

src/analysis.lagda.md

@@ -14,6 +14,7 @@ open import analysis.differentiability-identity-function-on-proper-closed-interv
 open import analysis.differentiable-real-functions-on-proper-closed-intervals-real-numbers public
 open import analysis.metric-abelian-groups public
 open import analysis.metric-abelian-groups-normed-real-vector-spaces public
+open import analysis.multiplication-differentiable-real-functions-on-proper-closed-intervals-real-numbers public
 open import analysis.nonnegative-series-real-numbers public
 open import analysis.scalar-multiplication-differentiable-functions-on-proper-closed-intervals-real-numbers public
 open import analysis.series-complete-metric-abelian-groups public

src/analysis/multiplication-differentiable-real-functions-on-proper-closed-intervals-real-numbers.lagda.md

@@ -360,3 +360,20 @@ abstract
       ( λ p=1 → leq-eq-ℚ (ap-mul-ℚ p=1 refl ∙ left-unit-law-mul-ℚ q))
       ( λ 1<p → ex-falso (not-leq-le-ℚ one-ℚ p 1<p p≤1))
 ```
+
+### Swapping laws for multiplication of positive rational numbers
+
+```agda
+abstract
+  right-swap-mul-ℚ⁺ :
+    (a b c : ℚ⁺) → (a *ℚ⁺ b) *ℚ⁺ c ＝ (a *ℚ⁺ c) *ℚ⁺ b
+  right-swap-mul-ℚ⁺ a b c =
+    equational-reasoning
+      (a *ℚ⁺ b) *ℚ⁺ c
+      ＝ a *ℚ⁺ (b *ℚ⁺ c)
+        by associative-mul-ℚ⁺ a b c
+      ＝ a *ℚ⁺ (c *ℚ⁺ b)
+        by ap-mul-ℚ⁺ refl (commutative-mul-ℚ⁺ b c)
+      ＝ (a *ℚ⁺ c) *ℚ⁺ b
+        by inv (associative-mul-ℚ⁺ a c b)
+```

src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md

@@ -85,6 +85,14 @@ pr1 two-ℕ⁺ = 2
 pr2 two-ℕ⁺ ()
 ```
 
+### The nonzero natural number `3`
+
+```agda
+three-ℕ⁺ : ℕ⁺
+pr1 three-ℕ⁺ = 3
+pr2 three-ℕ⁺ ()
+```
+
 ### The successor function on the nonzero natural numbers
 
 ```agda

src/elementary-number-theory/nonzero-natural-numbers.lagda.md

@@ -10,6 +10,7 @@ module metric-spaces.cartesian-products-metric-spaces where
 open import foundation.cartesian-product-types
 open import foundation.conjunction
 open import foundation.dependent-pair-types
+open import foundation.diagonal-maps-cartesian-products-of-types
 open import foundation.equality-cartesian-product-types
 open import foundation.evaluation-functions
 open import foundation.function-extensionality
@@ -20,6 +21,7 @@ open import foundation.sets
 open import foundation.universe-levels
 
 open import metric-spaces.extensionality-pseudometric-spaces
+open import metric-spaces.isometries-metric-spaces
 open import metric-spaces.metric-spaces
 open import metric-spaces.monotonic-rational-neighborhood-relations
 open import metric-spaces.pseudometric-spaces
@@ -144,3 +146,18 @@ module _
       ( pr2)
   is-short-pr2-product-Metric-Space _ _ _ = pr2
 ```
+
+### The diagonal isometry from `X` to `X × X`
+
+```agda
+module _
+  {l1 l2 : Level}
+  (X : Metric-Space l1 l2)
+  where
+
+  diagonal-product-isometry-Metric-Space :
+    isometry-Metric-Space X (product-Metric-Space X X)
+  diagonal-product-isometry-Metric-Space =
+    ( diagonal-product (type-Metric-Space X) ,
+      ( λ _ _ _ → ((λ N → (N , N)) , pr1)))
+```

src/metric-spaces/cartesian-products-metric-spaces.lagda.md

@@ -79,19 +79,19 @@ module _
   (f : uniformly-continuous-function-Metric-Space X Y)
   where
 
-  is-uniformly-continuous-map-unit-im-uniformly-continuous-function-Metric-Space :
+  is-uniformly-continuous-map-unit-im-Metric-Space :
     is-uniformly-continuous-function-Metric-Space
       ( X)
       ( im-uniformly-continuous-function-Metric-Space X Y f)
       ( map-unit-im-uniformly-continuous-function-Metric-Space X Y f)
-  is-uniformly-continuous-map-unit-im-uniformly-continuous-function-Metric-Space =
+  is-uniformly-continuous-map-unit-im-Metric-Space =
     is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space X Y f
 
-  uniformly-continuous-map-unit-im-uniformly-continuous-function-Metric-Space :
+  uniformly-continuous-map-unit-im-Metric-Space :
     uniformly-continuous-function-Metric-Space
       ( X)
       ( im-uniformly-continuous-function-Metric-Space X Y f)
-  uniformly-continuous-map-unit-im-uniformly-continuous-function-Metric-Space =
+  uniformly-continuous-map-unit-im-Metric-Space =
     ( map-unit-im-uniformly-continuous-function-Metric-Space X Y f ,
-      is-uniformly-continuous-map-unit-im-uniformly-continuous-function-Metric-Space)
+      is-uniformly-continuous-map-unit-im-Metric-Space)
 ```

src/metric-spaces/images-uniformly-continuous-functions-metric-spaces.lagda.md

@@ -76,6 +76,7 @@ open import real-numbers.multiplication-nonzero-real-numbers public
 open import real-numbers.multiplication-positive-and-negative-real-numbers public
 open import real-numbers.multiplication-positive-real-numbers public
 open import real-numbers.multiplication-real-numbers public
+open import real-numbers.multiplication-uniformly-continuous-functions-proper-closed-intervals-real-numbers public
 open import real-numbers.multiplicative-inverses-negative-real-numbers public
 open import real-numbers.multiplicative-inverses-nonzero-real-numbers public
 open import real-numbers.multiplicative-inverses-positive-real-numbers public

src/real-numbers.lagda.md

@@ -0,0 +1,107 @@
+# Multiplication of uniformly continuous functions on proper closed intervals in the real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.multiplication-uniformly-continuous-functions-proper-closed-intervals-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.universe-levels
+
+open import metric-spaces.cartesian-products-metric-spaces
+open import metric-spaces.images-uniformly-continuous-functions-metric-spaces
+open import metric-spaces.lipschitz-functions-metric-spaces
+open import metric-spaces.uniformly-continuous-functions-metric-spaces
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.lipschitz-continuity-multiplication-real-numbers
+open import real-numbers.metric-space-of-real-numbers
+open import real-numbers.multiplication-real-numbers
+open import real-numbers.proper-closed-intervals-real-numbers
+open import real-numbers.uniformly-continuous-functions-proper-closed-intervals-real-numbers
+```
+
+</details>
+
+## Idea
+
+Given two
+[uniformly continuous maps](real-numbers.uniformly-continuous-functions-proper-closed-intervals-real-numbers.md)
+`f` and `g` on the
+[proper closed interval](real-numbers.proper-closed-intervals-real-numbers.md)
+of [real numbers](real-numbers.dedekind-real-numbers.md) `[a, b]`, the map
+`x ↦ f x * g x` is uniformly continuous.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  ([a,b] : proper-closed-interval-ℝ l1 l1)
+  (f : ucont-map-proper-closed-interval-ℝ l1 l2 [a,b])
+  (g : ucont-map-proper-closed-interval-ℝ l1 l3 [a,b])
+  where
+
+  map-mul-ucont-map-proper-closed-interval-ℝ :
+    type-proper-closed-interval-ℝ l1 [a,b] → ℝ (l2 ⊔ l3)
+  map-mul-ucont-map-proper-closed-interval-ℝ x =
+    pr1 f x *ℝ pr1 g x
+
+  abstract
+    is-ucont-map-mul-ucont-map-proper-closed-interval-ℝ :
+      is-ucont-map-proper-closed-interval-ℝ
+        ( [a,b])
+        ( map-mul-ucont-map-proper-closed-interval-ℝ)
+    is-ucont-map-mul-ucont-map-proper-closed-interval-ℝ =
+      is-uniformly-continuous-comp-function-Metric-Space
+        ( metric-space-proper-closed-interval-ℝ l1 [a,b])
+        ( product-Metric-Space
+          ( subspace-im-ucont-map-proper-closed-interval-ℝ
+            ( [a,b])
+            ( f))
+          ( subspace-im-ucont-map-proper-closed-interval-ℝ
+            ( [a,b])
+            ( g)))
+        ( metric-space-ℝ (l2 ⊔ l3))
+        ( _)
+        ( _)
+        ( is-uniformly-continuous-is-lipschitz-function-Metric-Space
+          ( product-Metric-Space
+            ( subspace-im-ucont-map-proper-closed-interval-ℝ
+              ( [a,b])
+              ( f))
+            ( subspace-im-ucont-map-proper-closed-interval-ℝ
+              ( [a,b])
+              ( g)))
+          ( metric-space-ℝ (l2 ⊔ l3))
+          ( _)
+          ( is-lipschitz-mul-inhabited-totally-bounded-subset-ℝ
+            ( inhabited-totally-bounded-subset-im-ucont-map-proper-closed-interval-ℝ
+              ( [a,b])
+              ( f))
+            ( inhabited-totally-bounded-subset-im-ucont-map-proper-closed-interval-ℝ
+              ( [a,b])
+              ( g))))
+        ( is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space
+          ( _)
+          ( _)
+          ( comp-uniformly-continuous-function-Metric-Space _ _ _
+            ( product-uniformly-continuous-function-Metric-Space _ _ _ _
+              ( uniformly-continuous-map-unit-im-Metric-Space _ _ f)
+              ( uniformly-continuous-map-unit-im-Metric-Space _ _ g))
+            ( uniformly-continuous-isometry-Metric-Space
+              ( _)
+              ( _)
+              ( diagonal-product-isometry-Metric-Space
+                ( metric-space-proper-closed-interval-ℝ l1 [a,b])))))
+
+  mul-ucont-map-proper-closed-interval-ℝ :
+    ucont-map-proper-closed-interval-ℝ l1 (l2 ⊔ l3) [a,b]
+  mul-ucont-map-proper-closed-interval-ℝ =
+    ( map-mul-ucont-map-proper-closed-interval-ℝ ,
+      is-ucont-map-mul-ucont-map-proper-closed-interval-ℝ)
+```