The product rule for derivatives (#1771)

Depends on #1769 and #1758 (because it introduces the concept of a
uniform homeomorphism, though that could be extracted if necessary).

Author: lowasser

src/analysis.lagda.md

@@ -23,6 +23,7 @@ open import analysis.metric-abelian-groups public
 open import analysis.metric-abelian-groups-normed-real-vector-spaces public
 open import analysis.metric-abelian-groups-of-uniformly-continuous-maps-into-metric-abelian-groups public
 open import analysis.monotone-convergence-theorem-increasing-sequences-real-numbers 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.ratio-test-series-real-numbers public
 open import analysis.scalar-multiplication-differentiable-real-maps-on-proper-closed-intervals-real-numbers public

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

@@ -147,18 +147,6 @@ module _
               ( [c,d])
               ( g))
         gf = map-comp-differentiable-real-map-proper-closed-interval-ℝ
-        g'f x =
-          ( map-derivative-differentiable-real-map-proper-closed-interval-ℝ
-            ( [c,d])
-            ( g)
-            ( tot
-              ( f[a,b]⊆[c,d])
-              ( map-unit-im-uniformly-continuous-real-map-proper-closed-interval-ℝ
-                ( [a,b])
-                ( uniformly-continuous-map-differentiable-real-map-proper-closed-interval-ℝ
-                  ( [a,b])
-                  ( f))
-                ( x))))
         f' =
           map-derivative-differentiable-real-map-proper-closed-interval-ℝ
             ( [a,b])
@@ -178,6 +166,11 @@ module _
               ( [a,b])
               ( ucont-f)
               ( z))
+        g'∘f x =
+          ( map-derivative-differentiable-real-map-proper-closed-interval-ℝ
+            ( [c,d])
+            ( g)
+            ( tot-f x))
       in do
         (δf , is-mod-δf) ←
           is-derivative-map-derivative-differentiable-real-map-proper-closed-interval-ℝ
@@ -221,29 +214,29 @@ module _
                     ( Nδxy))
             in
               chain-of-inequalities
-                dist-ℝ (gf y -ℝ gf x) (g'f x *ℝ f' x *ℝ (pr1 y -ℝ pr1 x))
+                dist-ℝ (gf y -ℝ gf x) (g'∘f x *ℝ f' x *ℝ (pr1 y -ℝ pr1 x))
                 ≤ ( dist-ℝ
                     ( gf y -ℝ gf x)
-                    ( g'f x *ℝ (map-f y -ℝ map-f x))) +ℝ
+                    ( g'∘f x *ℝ (map-f y -ℝ map-f x))) +ℝ
                   ( dist-ℝ
-                    ( g'f x *ℝ (map-f y -ℝ map-f x))
-                    ( g'f x *ℝ f' x *ℝ (pr1 y -ℝ pr1 x)))
+                    ( g'∘f x *ℝ (map-f y -ℝ map-f x))
+                    ( g'∘f x *ℝ f' x *ℝ (pr1 y -ℝ pr1 x)))
                   by triangle-inequality-dist-ℝ _ _ _
                 ≤ ( dist-ℝ
                     ( gf y -ℝ gf x)
-                    ( g'f x *ℝ (map-f y -ℝ map-f x))) +ℝ
+                    ( g'∘f x *ℝ (map-f y -ℝ map-f x))) +ℝ
                   ( dist-ℝ
-                    ( g'f x *ℝ (map-f y -ℝ map-f x))
-                    ( g'f x *ℝ (f' x *ℝ (pr1 y -ℝ pr1 x))))
+                    ( g'∘f x *ℝ (map-f y -ℝ map-f x))
+                    ( g'∘f x *ℝ (f' x *ℝ (pr1 y -ℝ pr1 x))))
                   by
                     leq-eq-ℝ
                       ( ap-add-ℝ
                         ( refl)
                         ( ap-dist-ℝ refl (associative-mul-ℝ _ _ _)))
                 ≤ ( dist-ℝ
                     ( gf y -ℝ gf x)
-                    ( g'f x *ℝ (map-f y -ℝ map-f x))) +ℝ
-                  ( ( abs-ℝ (g'f x)) *ℝ
+                    ( g'∘f x *ℝ (map-f y -ℝ map-f x))) +ℝ
+                  ( ( abs-ℝ (g'∘f x)) *ℝ
                     ( dist-ℝ
                       ( map-f y -ℝ map-f x))
                       ( f' x *ℝ (pr1 y -ℝ pr1 x)))
@@ -270,7 +263,7 @@ module _
                             ( leq-left-min-ℚ⁺ (ωf (δg α)) (δf β))
                             ( Nδxy))))
                       ( preserves-leq-mul-ℝ⁰⁺
-                        ( nonnegative-abs-ℝ (g'f x))
+                        ( nonnegative-abs-ℝ (g'∘f x))
                         ( nonnegative-real-ℚ⁺ q⁺)
                         ( nonnegative-dist-ℝ _ _)
                         ( nonnegative-real-ℚ⁺ β *ℝ⁰⁺ nonnegative-dist-ℝ _ _)