:: Partial Differentiation of Real Ternary Functions
:: by Takao Inou\'e , Bing Xie and Xiquan Liang
::
:: Received November 7, 2009
:: Copyright (c) 2009 Association of Mizar Users

begin

theorem Th1: :: PDIFF_4:1

( dom (proj 1,3) = REAL 3 & rng (proj 1,3) = REAL & ( for x, y, z being Element of REAL holds (proj 1,3) . <*x,y,z*> = x ) )

proof end;

theorem Th2: :: PDIFF_4:2

( dom (proj 2,3) = REAL 3 & rng (proj 2,3) = REAL & ( for x, y, z being Element of REAL holds (proj 2,3) . <*x,y,z*> = y ) )

proof end;

theorem Th3: :: PDIFF_4:3

( dom (proj 3,3) = REAL 3 & rng (proj 3,3) = REAL & ( for x, y, z being Element of REAL holds (proj 3,3) . <*x,y,z*> = z ) )

proof end;

begin

theorem Lem1: :: PDIFF_4:4

for x, y, z being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,1 holds
SVF1 1,f,u is_differentiable_in x

proof end;

theorem Lem2: :: PDIFF_4:5

for x, y, z being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,2 holds
SVF1 2,f,u is_differentiable_in y

proof end;

theorem Lem3: :: PDIFF_4:6

for x, y, z being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,3 holds
SVF1 3,f,u is_differentiable_in z

proof end;

theorem BXXLXSDef6: :: PDIFF_4:7

for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 1,f,u is_differentiable_in x0 ) iff f is_partial_differentiable_in u,1 )

proof end;

theorem BXXLXSDef7: :: PDIFF_4:8

for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 2,f,u is_differentiable_in y0 ) iff f is_partial_differentiable_in u,2 )

proof end;

theorem BXXLXSDef7ForZ: :: PDIFF_4:9

for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & SVF1 3,f,u is_differentiable_in z0 ) iff f is_partial_differentiable_in u,3 )

proof end;

theorem :: PDIFF_4:10

for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,f,u) & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
((SVF1 1,f,u) . x) - ((SVF1 1,f,u) . x0) = (L . (x - x0)) + (R . (x - x0)) )

proof end;

theorem :: PDIFF_4:11

for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,f,u) & ex L being LINEAR ex R being REST st
for y being Real st y in N holds
((SVF1 2,f,u) . y) - ((SVF1 2,f,u) . y0) = (L . (y - y0)) + (R . (y - y0)) )

proof end;

theorem :: PDIFF_4:12

for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,f,u) & ex L being LINEAR ex R being REST st
for z being Real st z in N holds
((SVF1 3,f,u) . z) - ((SVF1 3,f,u) . z0) = (L . (z - z0)) + (R . (z - z0)) )

proof end;

theorem BXXLXSDef10: :: PDIFF_4:13

for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( f is_partial_differentiable_in u,1 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,f,u) & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
((SVF1 1,f,u) . x) - ((SVF1 1,f,u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )

proof end;

theorem BXXLXSDef11: :: PDIFF_4:14

for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( f is_partial_differentiable_in u,2 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,f,u) & ex L being LINEAR ex R being REST st
for y being Real st y in N holds
((SVF1 2,f,u) . y) - ((SVF1 2,f,u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )

proof end;

theorem BXXLXSDef11ForZ: :: PDIFF_4:15

for f being PartFunc of (REAL 3),REAL
for u being Element of REAL 3 holds
( f is_partial_differentiable_in u,3 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,f,u) & ex L being LINEAR ex R being REST st
for z being Real st z in N holds
((SVF1 3,f,u) . z) - ((SVF1 3,f,u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) )

proof end;

BXXLXSdef12: for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
( r = diff (SVF1 1,f,u),x0 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,f,u) & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 1,f,u) . x) - ((SVF1 1,f,u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )

proof end;

BXXLXSdef13: for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
( r = diff (SVF1 2,f,u),y0 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,f,u) & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 2,f,u) . y) - ((SVF1 2,f,u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )

proof end;

BXXLXSdef13ForZ: for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
( r = diff (SVF1 3,f,u),z0 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,f,u) & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 3,f,u) . z) - ((SVF1 3,f,u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )

proof end;

theorem BXXLXSDef12: :: PDIFF_4:16

for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 holds
( r = partdiff f,u,1 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of x0 st
( N c= dom (SVF1 1,f,u) & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for x being Real st x in N holds
((SVF1 1,f,u) . x) - ((SVF1 1,f,u) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) ) )

proof end;

theorem BXXLXSDef13: :: PDIFF_4:17

for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 holds
( r = partdiff f,u,2 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,f,u) & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for y being Real st y in N holds
((SVF1 2,f,u) . y) - ((SVF1 2,f,u) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) ) ) )

proof end;

theorem BXXLXSDef13ForZ: :: PDIFF_4:18

for x0, y0, z0, r being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 holds
( r = partdiff f,u,3 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of z0 st
( N c= dom (SVF1 3,f,u) & ex L being LINEAR ex R being REST st
( r = L . 1 & ( for z being Real st z in N holds
((SVF1 3,f,u) . z) - ((SVF1 3,f,u) . z0) = (L . (z - z0)) + (R . (z - z0)) ) ) ) ) )

proof end;

theorem :: PDIFF_4:19

for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> holds
partdiff f,u,1 = diff (SVF1 1,f,u),x0 by Th1;

theorem :: PDIFF_4:20

for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> holds
partdiff f,u,2 = diff (SVF1 2,f,u),y0 by Th2;

theorem :: PDIFF_4:21

for x0, y0, z0 being Real
for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x0,y0,z0*> holds
partdiff f,u,3 = diff (SVF1 3,f,u),z0 by Th3;

definition

let f be PartFunc of (REAL 3),REAL ;
let D be set ;
pred f is_partial_differentiable`1_on D means :Def16: :: PDIFF_4:def 1
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,1 ) );
pred f is_partial_differentiable`2_on D means :Def17: :: PDIFF_4:def 2
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,2 ) );
pred f is_partial_differentiable`3_on D means :Def17ForZ: :: PDIFF_4:def 3
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,3 ) );

end;

:: deftheorem Def16 defines is_partial_differentiable`1_on PDIFF_4:def 1 :

for f being PartFunc of (REAL 3),REAL
for D being set holds
( f is_partial_differentiable`1_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,1 ) ) );

:: deftheorem Def17 defines is_partial_differentiable`2_on PDIFF_4:def 2 :

for f being PartFunc of (REAL 3),REAL
for D being set holds
( f is_partial_differentiable`2_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,2 ) ) );

:: deftheorem Def17ForZ defines is_partial_differentiable`3_on PDIFF_4:def 3 :

for f being PartFunc of (REAL 3),REAL
for D being set holds
( f is_partial_differentiable`3_on D iff ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f | D is_partial_differentiable_in u,3 ) ) );

theorem :: PDIFF_4:22

for D being set
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`1_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,1 ) )

proof end;

theorem :: PDIFF_4:23

for D being set
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`2_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,2 ) )

proof end;

theorem :: PDIFF_4:24

for D being set
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`3_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,3 ) )

proof end;

definition

let f be PartFunc of (REAL 3),REAL ;
let D be set ;
assume A1: f is_partial_differentiable`1_on D ;
func f `partial1| D -> PartFunc of (REAL 3),REAL means :: PDIFF_4:def 4
( dom it = D & ( for u being Element of REAL 3 st u in D holds
it . u = partdiff f,u,1 ) );
existence
ex b₁ being PartFunc of (REAL 3),REAL st
( dom b₁ = D & ( for u being Element of REAL 3 st u in D holds
b₁ . u = partdiff f,u,1 ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of (REAL 3),REAL st dom b₁ = D & ( for u being Element of REAL 3 st u in D holds
b₁ . u = partdiff f,u,1 ) & dom b₂ = D & ( for u being Element of REAL 3 st u in D holds
b₂ . u = partdiff f,u,1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines `partial1| PDIFF_4:def 4 :

for f being PartFunc of (REAL 3),REAL
for D being set st f is_partial_differentiable`1_on D holds
for b<sub>3</sub> being PartFunc of (REAL 3),REAL holds
( b<sub>3</sub> = f `partial1| D iff ( dom b₃ = D & ( for u being Element of REAL 3 st u in D holds
b₃ . u = partdiff f,u,1 ) ) );

definition

let f be PartFunc of (REAL 3),REAL ;
let D be set ;
assume A1: f is_partial_differentiable`2_on D ;
func f `partial2| D -> PartFunc of (REAL 3),REAL means :: PDIFF_4:def 5
( dom it = D & ( for u being Element of REAL 3 st u in D holds
it . u = partdiff f,u,2 ) );
existence
ex b₁ being PartFunc of (REAL 3),REAL st
( dom b₁ = D & ( for u being Element of REAL 3 st u in D holds
b₁ . u = partdiff f,u,2 ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of (REAL 3),REAL st dom b₁ = D & ( for u being Element of REAL 3 st u in D holds
b₁ . u = partdiff f,u,2 ) & dom b₂ = D & ( for u being Element of REAL 3 st u in D holds
b₂ . u = partdiff f,u,2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines `partial2| PDIFF_4:def 5 :

for f being PartFunc of (REAL 3),REAL
for D being set st f is_partial_differentiable`2_on D holds
for b<sub>3</sub> being PartFunc of (REAL 3),REAL holds
( b<sub>3</sub> = f `partial2| D iff ( dom b₃ = D & ( for u being Element of REAL 3 st u in D holds
b₃ . u = partdiff f,u,2 ) ) );

definition

let f be PartFunc of (REAL 3),REAL ;
let D be set ;
assume A1: f is_partial_differentiable`3_on D ;
func f `partial3| D -> PartFunc of (REAL 3),REAL means :: PDIFF_4:def 6
( dom it = D & ( for u being Element of REAL 3 st u in D holds
it . u = partdiff f,u,3 ) );
existence
ex b₁ being PartFunc of (REAL 3),REAL st
( dom b₁ = D & ( for u being Element of REAL 3 st u in D holds
b₁ . u = partdiff f,u,3 ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of (REAL 3),REAL st dom b₁ = D & ( for u being Element of REAL 3 st u in D holds
b₁ . u = partdiff f,u,3 ) & dom b₂ = D & ( for u being Element of REAL 3 st u in D holds
b₂ . u = partdiff f,u,3 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines `partial3| PDIFF_4:def 6 :

for f being PartFunc of (REAL 3),REAL
for D being set st f is_partial_differentiable`3_on D holds
for b<sub>3</sub> being PartFunc of (REAL 3),REAL holds
( b<sub>3</sub> = f `partial3| D iff ( dom b₃ = D & ( for u being Element of REAL 3 st u in D holds
b₃ . u = partdiff f,u,3 ) ) );

begin

theorem :: PDIFF_4:25

for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3
for N being Neighbourhood of (proj 1,3) . u0 st f is_partial_differentiable_in u0,1 & N c= dom (SVF1 1,f,u0) holds
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {((proj 1,3) . u0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 1,f,u0) /* (h + c)) - ((SVF1 1,f,u0) /* c)) is convergent & partdiff f,u0,1 = lim ((h " ) (#) (((SVF1 1,f,u0) /* (h + c)) - ((SVF1 1,f,u0) /* c))) )

proof end;

theorem :: PDIFF_4:26

for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3
for N being Neighbourhood of (proj 2,3) . u0 st f is_partial_differentiable_in u0,2 & N c= dom (SVF1 2,f,u0) holds
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {((proj 2,3) . u0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 2,f,u0) /* (h + c)) - ((SVF1 2,f,u0) /* c)) is convergent & partdiff f,u0,2 = lim ((h " ) (#) (((SVF1 2,f,u0) /* (h + c)) - ((SVF1 2,f,u0) /* c))) )

proof end;

theorem :: PDIFF_4:27

for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3
for N being Neighbourhood of (proj 3,3) . u0 st f is_partial_differentiable_in u0,3 & N c= dom (SVF1 3,f,u0) holds
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {((proj 3,3) . u0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 3,f,u0) /* (h + c)) - ((SVF1 3,f,u0) /* c)) is convergent & partdiff f,u0,3 = lim ((h " ) (#) (((SVF1 3,f,u0) /* (h + c)) - ((SVF1 3,f,u0) /* c))) )

proof end;

theorem :: PDIFF_4:28

for u0 being Element of REAL 3
for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,1 & f2 is_partial_differentiable_in u0,1 holds
f1 (#) f2 is_partial_differentiable_in u0,1

proof end;

theorem :: PDIFF_4:29

for u0 being Element of REAL 3
for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,2 & f2 is_partial_differentiable_in u0,2 holds
f1 (#) f2 is_partial_differentiable_in u0,2

proof end;

theorem :: PDIFF_4:30

for u0 being Element of REAL 3
for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_partial_differentiable_in u0,3 & f2 is_partial_differentiable_in u0,3 holds
f1 (#) f2 is_partial_differentiable_in u0,3

proof end;

theorem :: PDIFF_4:31

for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,1 holds
SVF1 1,f,u0 is_continuous_in (proj 1,3) . u0

proof end;

theorem :: PDIFF_4:32

for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,2 holds
SVF1 2,f,u0 is_continuous_in (proj 2,3) . u0

proof end;

theorem :: PDIFF_4:33

for f being PartFunc of (REAL 3),REAL
for u0 being Element of REAL 3 st f is_partial_differentiable_in u0,3 holds
SVF1 3,f,u0 is_continuous_in (proj 3,3) . u0

proof end;

theorem :: PDIFF_4:34

for u0 being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in u0,1 holds
ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )

proof end;

theorem :: PDIFF_4:35

for u0 being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in u0,2 holds
ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )

proof end;

theorem :: PDIFF_4:36

for u0 being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in u0,3 holds
ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )

proof end;

begin

Lm6: for x1, y1, z1, x2, y2, z2 being Real holds |[x1,y1,z1]| + |[x2,y2,z2]| = |[(x1 + x2),(y1 + y2),(z1 + z2)]|

proof end;

definition

let f be PartFunc of (REAL 3),REAL ;
let p be Element of REAL 3;
func grad f,p -> Element of REAL 3 equals :: PDIFF_4:def 7
(((partdiff f,p,1) * <e1> ) + ((partdiff f,p,2) * <e2> )) + ((partdiff f,p,3) * <e3> );
coherence
(((partdiff f,p,1) * <e1> ) + ((partdiff f,p,2) * <e2> )) + ((partdiff f,p,3) * <e3> ) is Element of REAL 3 ;

end;

:: deftheorem defines grad PDIFF_4:def 7 :

for f being PartFunc of (REAL 3),REAL
for p being Element of REAL 3 holds grad f,p = (((partdiff f,p,1) * <e1> ) + ((partdiff f,p,2) * <e2> )) + ((partdiff f,p,3) * <e3> );

theorem Th43: :: PDIFF_4:37

for p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL holds grad f,p = |[(partdiff f,p,1),(partdiff f,p,2),(partdiff f,p,3)]|

proof end;

theorem Th45: :: PDIFF_4:38

for p being Element of REAL 3
for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad (f + g),p = (grad f,p) + (grad g,p)

proof end;

theorem Th46: :: PDIFF_4:39

for p being Element of REAL 3
for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad (f - g),p = (grad f,p) - (grad g,p)

proof end;

theorem Th47: :: PDIFF_4:40

for r being Real
for p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 holds
grad (r (#) f),p = r * (grad f,p)

proof end;

theorem :: PDIFF_4:41

for s, t being Real
for p being Element of REAL 3
for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad ((s (#) f) + (t (#) g)),p = (s * (grad f,p)) + (t * (grad g,p))

proof end;

theorem :: PDIFF_4:42

for s, t being Real
for p being Element of REAL 3
for f, g being PartFunc of (REAL 3),REAL st f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 & f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3 holds
grad ((s (#) f) - (t (#) g)),p = (s * (grad f,p)) - (t * (grad g,p))

proof end;

theorem :: PDIFF_4:43

for p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st f is total & f is constant holds
grad f,p = 0.REAL 3

proof end;

definition

let a be Element of REAL 3;
func unitvector a -> Element of REAL 3 equals :: PDIFF_4:def 8
|[((a . 1) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))),((a . 2) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))),((a . 3) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))]|;
coherence
|[((a . 1) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))),((a . 2) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))),((a . 3) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))]| is Element of REAL 3 ;

end;

:: deftheorem defines unitvector PDIFF_4:def 8 :

for a being Element of REAL 3 holds unitvector a = |[((a . 1) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))),((a . 2) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 )))),((a . 3) / (sqrt ((((a . 1) ^2 ) + ((a . 2) ^2 )) + ((a . 3) ^2 ))))]|;

definition

let f be PartFunc of (REAL 3),REAL ;
let p, a be Element of REAL 3;
func Directiondiff f,p,a -> Real equals :: PDIFF_4:def 9
(((partdiff f,p,1) * ((unitvector a) . 1)) + ((partdiff f,p,2) * ((unitvector a) . 2))) + ((partdiff f,p,3) * ((unitvector a) . 3));
coherence
(((partdiff f,p,1) * ((unitvector a) . 1)) + ((partdiff f,p,2) * ((unitvector a) . 2))) + ((partdiff f,p,3) * ((unitvector a) . 3)) is Real ;

end;

:: deftheorem defines Directiondiff PDIFF_4:def 9 :

for f being PartFunc of (REAL 3),REAL
for p, a being Element of REAL 3 holds Directiondiff f,p,a = (((partdiff f,p,1) * ((unitvector a) . 1)) + ((partdiff f,p,2) * ((unitvector a) . 2))) + ((partdiff f,p,3) * ((unitvector a) . 3));

theorem :: PDIFF_4:44

for x0, y0, z0 being Real
for a, p being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st a = <*x0,y0,z0*> holds
Directiondiff f,p,a = ((((partdiff f,p,1) * x0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 )))) + (((partdiff f,p,2) * y0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))) + (((partdiff f,p,3) * z0) / (sqrt (((x0 ^2 ) + (y0 ^2 )) + (z0 ^2 ))))

proof end;

theorem :: PDIFF_4:45

for p, a being Element of REAL 3
for f being PartFunc of (REAL 3),REAL holds Directiondiff f,p,a = |((grad f,p),(unitvector a))|

proof end;

definition

let f1, f2, f3 be PartFunc of (REAL 3),REAL ;
let p be Element of REAL 3;
func curl f1,f2,f3,p -> Element of REAL 3 equals :: PDIFF_4:def 10
((((partdiff f3,p,2) - (partdiff f2,p,3)) * <e1> ) + (((partdiff f1,p,3) - (partdiff f3,p,1)) * <e2> )) + (((partdiff f2,p,1) - (partdiff f1,p,2)) * <e3> );
coherence
((((partdiff f3,p,2) - (partdiff f2,p,3)) * <e1> ) + (((partdiff f1,p,3) - (partdiff f3,p,1)) * <e2> )) + (((partdiff f2,p,1) - (partdiff f1,p,2)) * <e3> ) is Element of REAL 3 ;

end;

:: deftheorem defines curl PDIFF_4:def 10 :

for f1, f2, f3 being PartFunc of (REAL 3),REAL
for p being Element of REAL 3 holds curl f1,f2,f3,p = ((((partdiff f3,p,2) - (partdiff f2,p,3)) * <e1> ) + (((partdiff f1,p,3) - (partdiff f3,p,1)) * <e2> )) + (((partdiff f2,p,1) - (partdiff f1,p,2)) * <e3> );

theorem :: PDIFF_4:46

for p being Element of REAL 3
for f1, f2, f3 being PartFunc of (REAL 3),REAL holds curl f1,f2,f3,p = |[((partdiff f3,p,2) - (partdiff f2,p,3)),((partdiff f1,p,3) - (partdiff f3,p,1)),((partdiff f2,p,1) - (partdiff f1,p,2))]|

proof end;