The product rule for derivatives #1771

New issue

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

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

Already on GitHub? Sign in to your account

Open

lowasser wants to merge 63 commits into UniMath:master from lowasser:tb-proper-intervals

src/analysis.lagda.md

-Original file line number
+Diff line change
@@ Expand Up @@
     open import analysis.limits-of-sequences-metric-abelian-groups 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.ratio-test-series-real-numbers public
     open import analysis.scalar-multiplication-differentiable-real-maps-on-proper-closed-intervals-real-numbers public
@@ Expand Down @@

...-differentiable-real-functions-on-proper-closed-intervals-real-numbers.lagda.md

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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-ℝ _ _)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

The product rule for derivatives #1771

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

The product rule for derivatives #1771

Are you sure you want to change the base?

Uh oh!

The product rule for derivatives #1771

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!