kill(all)$

calculus, proof :Leibniz's rule for differentiation under the integral sign (two variable),version 1.0
peter.vlasschaert@gmail.com,16/08/2019

load : packages
=============

load(lrats);

example : 'see website'
calculus, Leibniz's rule for differentiation under the integral sign (two variable),version 1.0

representation: leibnizrule2
=====================

process of evaluation  =>
f(x,t) = sin(x*t)
[g(x)=x,h(x)=x^2]

p1:'diff('integrate(f(x,t),t,h(x),g(x)) ,x)= diff('integrate(f(x,t),t,h(x),g(x)) ,x);

rem : FTC = Fundamental Theorema Calculus
FTC = {FTC1,FTC2}
see website:
=========

2e)First & Second Fundamental Theorem of Calculus.

example 3: youtube
example 4: youtube
new: 12/08/2019:Calculus : First Fundamental Theorem of Calculus(proof),part 1,version 1.0
download  (Maxima,code)       :Fundamentaltheoremcalculuspart1version1final
download  (Maxima,png)         :Fundamentaltheoremcalculuspart1version1finaloutp
new: 12/08/2019:Calculus : Second Fundamental Theorem of Calculus(proof),part 2 ,version 1.0
download  (Maxima,code)       :Fundamentaltheoremcalculuspart2version1final
download  (Maxima,png)         :Fundamentaltheoremcalculuspart2version1finaloutp

proof, 'p1'
========
lhs → rhs

1e)  data (lhs)
-------------------

p1a:args(lhs(p1));

p1b:args(p1a[1]);

p1b1:p1b[1]; /* function with two ariables */
p1b2:p1b[2]; /*integration variable */
p1b3:p1b[3];  /*lower limit for integration */
p1b4:p1b[4];  /*upper limit for integration */

rem : find all elements for the proof.

2e)  FTC
-------------

p2:M(x)=p1a[1];

rule1 : integration:point between
=========================

p2a:integrate(f(x,t),t,h(x),g(x)) =integrate(f(x,t),t,h(x),a)+integrate(f(x,t),t,a,g(x));

rule2 : integration :interchange upper with lower limit
========================================

p2b:integrate(f(x,t),t,h(x),a) = -integrate(f(x,t),t,a,h(x)) ;

combine : two rules
===============

p2c:lhs(p2a) = lratsubst([p2b],rhs(p2a));

use FT:  F(x) =integrate(f(t),t,a,x)  <> F'(x) = f(x)

p2d:lhs(p2) = F(x,g(x))  - F(x,h(x));

3e) definition total differential: general  : F(x,y),two variables
---------------------------------------------------------------------------------
M(x)  => M'(x)   →   diff(M(x),x)

p3:'diff(F(x,y)) =diff(F(x,y));

p3a:[del(y)='diff(y,x),del(x)='diff(x,x)];

p3b:'diff(F(x,y),x) = lratsubst(p3a,rhs(p3));

differentation : p2d with respect to x
-------------------------------------------------
use : p3b

p3c:diff(p2d,x);

first part:F(x,g(x))
------------------------
here  :y=g(x)

p3d:F(x,y) = F(x,g(x));

p3d1:lratsubst([p3d],p3b);

p3d2:args(rhs(p3d1));

p3d2a:p3d2[1];
p3d2a1:part(p3d2a,1)= f(x,g(x));
p3d2a2:part(p3d2a,2) =lratsubst([y=g(x)],part(p3d2a,2));
p3d2a3:p3d2[2] =integrate(diff(f(x,t),x),t,a,g(x));

p3e:lhs(p3d1)=lratsubst([p3d2a1,p3d2a2,p3d2a3],rhs(p3d1));

second part:F(x,h(x))
------------------------
here  :y=h(x)

p4d:F(x,y) = F(x,h(x));

p4d1:lratsubst([p4d],p3b);

p4d2:args(rhs(p4d1));

p4d2a:p4d2[1];
p4d2a1:part(p4d2a,1)= f(x,h(x));
p4d2a2:part(p4d2a,2) =lratsubst([y=h(x)],part(p3d2a,2));
p4d2a3:p4d2[2] =integrate(diff(f(x,t),x),t,a,h(x));

p4e:lhs(p4d1)=lratsubst([p4d2a1,p4d2a2,p4d2a3],rhs(p4d1));

combine : first & second part
=======================
use :p3c & p3e & p4e

p5:lhs(p3c) = lratsubst([p3e,p4e],rhs(p3c));

rule2 : integration :interchange upper with lower limit
rule1 : to combine the integrals

p5a:integrate('diff(f(x,t),x,1),t,a,h(x)) = -integrate('diff(f(x,t),x,1),t,h(x),a);

p5b:integrate('diff(f(x,t),x,1),t,h(x),g(x))=integrate('diff(f(x,t),x,1),t,h(x),a)+integrate('diff(f(x,t),x,1),t,a,g(x));

p5b1:[rhs(p5b)=lhs(p5b)];

final result :proof
=============

p6:lratsubst([p5a],p5);

p6a:lratsubst(p5b1,p6);

leibniz(rule,two variables).
====================

p6b:lhs(p1)=rhs(p6a);