:: Implicit Function Theorem -- Part {III } and Inverse Function Theorem -- Part {II}
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received September 30, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

registration

let n be Nat;

cluster REAL-NS n -> finite-dimensional ;

correctness
coherence
REAL-NS n is finite-dimensional ;
by REAL_NS2:62;

end;

theorem :: NDIFF11:1

for n being non zero Nat
for X being RealNormSpace
for f being LinearOperator of (REAL-NS n),X holds f is Lipschitzian

proof end;

theorem Th2: :: NDIFF11:2

for m being non zero Nat
for s, t being FinSequence of REAL m st 1 <= len s & s = t | (len s) holds
for i being Nat st 1 <= i & i <= len s holds
(accum t) . i = (accum s) . i

proof end;

theorem Th3: :: NDIFF11:3

for m being non zero Nat
for s, s1 being FinSequence of REAL m
for s0 being Element of REAL m st s1 = s ^ <*s0*> holds
Sum s1 = (Sum s) + s0

proof end;

theorem Th4: :: NDIFF11:4

for m being non zero Nat
for s being FinSequence of REAL m
for j being Nat st 1 <= j & j <= m holds
ex t being FinSequence of REAL st
( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t )

proof end;

theorem Th5: :: NDIFF11:5

for m being non zero Nat
for x being Element of REAL m ex s being FinSequence of REAL m st
( dom s = Seg m & ( for i being Nat st 1 <= i & i <= m holds
ex ei being Element of REAL m st
( ei = (reproj (i,(0* m))) . 1 & s . i = ((proj (i,m)) . x) * ei ) ) & Sum s = x )

proof end;

theorem :: NDIFF11:6

for m, n being non zero Element of NAT
for M being Matrix of m,n,F_Real holds Mx2Tran M is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n)

proof end;

theorem Th7: :: NDIFF11:7

for m being non zero Element of NAT
for f being LinearOperator of (REAL-NS m),(REAL-NS m) st f is bijective holds
ex g being Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS m) st
( g = f " & g is one-to-one & g is onto )

proof end;

theorem Th8: :: NDIFF11:8

for m being non zero Element of NAT
for f being LinearOperator of (REAL-NS m),(REAL-NS m) st f is bijective holds
ex g being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m))) st
( g = f & g is invertible )

proof end;

theorem :: NDIFF11:9

for m, n being non zero Element of NAT
for M being Matrix of m,F_Real holds
( Mx2Tran M is bijective iff Det M <> 0. F_Real ) by MATRTOP1:40, MATRTOP1:42;

theorem Th10: :: NDIFF11:10

for m, n being non zero Element of NAT
for M being Matrix of m,F_Real holds
( Mx2Tran M is bijective iff M is invertible )

proof end;

theorem Th11: :: NDIFF11:11

for m being non zero Element of NAT
for f being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m))) st f is one-to-one & rng f = the carrier of (REAL-NS m) holds
f is invertible

proof end;

theorem Th12: :: NDIFF11:12

for m being non zero Element of NAT
for f being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m)))
for M being Matrix of m,F_Real st f = Mx2Tran M holds
( f is invertible iff M is invertible )

proof end;

theorem :: NDIFF11:13

for m being non zero Element of NAT
for f being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS m)))
for M being Matrix of m,F_Real st f = Mx2Tran M holds
( f is invertible iff Det M <> 0. F_Real )

proof end;

theorem Th14: :: NDIFF11:14

for m, n being non zero Element of NAT ex f being Function of [:(REAL m),(REAL n):],(REAL (m + n)) st
( ( for x being Element of REAL m
for y being Element of REAL n holds f . (x,y) = x ^ y ) & f is one-to-one & f is onto )

proof end;

theorem :: NDIFF11:15

for m, n being non zero Element of NAT ex f being Function of [:(REAL-NS m),(REAL-NS n):],(REAL-NS (m + n)) st
( f is one-to-one & f is onto & ( for x being Element of REAL m
for y being Element of REAL n holds f . (x,y) = x ^ y ) & ( for u, v being Point of [:(REAL-NS m),(REAL-NS n):] holds f . (u + v) = (f . u) + (f . v) ) & ( for u being Point of [:(REAL-NS m),(REAL-NS n):]
for r being Real holds f . (r * u) = r * (f . u) ) & f . (0. [:(REAL-NS m),(REAL-NS n):]) = 0. (REAL-NS (m + n)) & ( for u being Point of [:(REAL-NS m),(REAL-NS n):] holds ||.(f . u).|| = ||.u.|| ) )

proof end;

theorem Th16: :: NDIFF11:16

for X, Y being RealNormSpace
for x being Point of X
for f being Lipschitzian LinearOperator of X,Y holds
( f is_differentiable_in x & f = diff (f,x) )

proof end;

theorem :: NDIFF11:17

for n being non zero Nat
for i being Nat
for x being Point of (REAL-NS n) st 1 <= i & i <= n holds
( Proj (i,n) is_differentiable_in x & diff ((Proj (i,n)),x) = Proj (i,n) )

proof end;

theorem Th18: :: NDIFF11:18

for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m holds
( f is_differentiable_in x iff for i being Nat st 1 <= i & i <= n holds
ex fi being PartFunc of (REAL m),(REAL 1) st
( fi = (Proj (i,n)) * f & fi is_differentiable_in x ) )

proof end;

theorem Th19: :: NDIFF11:19

for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m holds
( f is_differentiable_in x iff for i being Nat st 1 <= i & i <= n holds
ex fi being PartFunc of (REAL m),REAL st
( fi = (proj (i,n)) * f & fi is_differentiable_in x ) )

proof end;

theorem Th20: :: NDIFF11:20

for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
for i being Nat
for fi being PartFunc of (REAL m),REAL st 1 <= i & i <= n & fi = (proj (i,n)) * f holds
( fi is_differentiable_in x & diff (fi,x) = (proj (i,n)) * (diff (f,x)) )

proof end;

theorem :: NDIFF11:21

for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
f is_partial_differentiable_in x,i,j

proof end;

theorem :: NDIFF11:22

for m, n being non zero Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Element of (REAL-NS m) st f is_differentiable_in x holds
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
f is_partial_differentiable_in x,i,j

proof end;

theorem Th23: :: NDIFF11:23

for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x holds
for u, v being Element of REAL m holds (diff (f,x)) . (u + v) = ((diff (f,x)) . u) + ((diff (f,x)) . v)

proof end;

theorem Th24: :: NDIFF11:24

for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x holds
for u being Element of REAL m
for a being Real holds (diff (f,x)) . (a * u) = a * ((diff (f,x)) . u)

proof end;

theorem Th25: :: NDIFF11:25

for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x holds
for s being FinSequence of REAL m
for t being FinSequence of REAL st dom s = dom t & ( for i being Nat st i in dom s holds
t . i = (diff (f,x)) . (s . i) ) holds
(diff (f,x)) . (Sum s) = Sum t

proof end;

theorem Th26: :: NDIFF11:26

for m being non zero Nat
for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st f is_differentiable_in x holds
for dx being Element of REAL m ex dy being FinSequence of REAL st
( dom dy = Seg m & ( for i being Nat st 1 <= i & i <= m holds
dy . i = ((proj (i,m)) . dx) * (partdiff (f,x,i)) ) & (diff (f,x)) . dx = Sum dy )

proof end;

theorem :: NDIFF11:27

for m, n being non zero Element of NAT
for X being Subset of (REAL-NS m)
for f being PartFunc of (REAL-NS m),(REAL-NS n) st X is open & X c= dom f holds
( ( f is_differentiable_on X & f `| X is_continuous_on X ) iff for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= n holds
( (Proj (j,n)) * f is_partial_differentiable_on X,i & ((Proj (j,n)) * f) `partial| (X,i) is_continuous_on X ) )

proof end;

definition

let m, n be non zero Nat;
let f be PartFunc of (REAL m),(REAL n);
let x be Element of REAL m;

func Jacobian (f,x) -> Matrix of m,n,F_Real means :Def1: :: NDIFF11:def 1
for i, j being Nat st i in Seg m & j in Seg n holds
it * (i,j) = partdiff (f,x,i,j);

existence
ex b₁ being Matrix of m,n,F_Real st
for i, j being Nat st i in Seg m & j in Seg n holds
b₁ * (i,j) = partdiff (f,x,i,j)

proof end;

uniqueness
for b₁, b₂ being Matrix of m,n,F_Real st ( for i, j being Nat st i in Seg m & j in Seg n holds
b₁ * (i,j) = partdiff (f,x,i,j) ) & ( for i, j being Nat st i in Seg m & j in Seg n holds
b₂ * (i,j) = partdiff (f,x,i,j) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Jacobian NDIFF11:def 1 :
for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m
for b₅ being Matrix of m,n,F_Real holds
( b₅ = Jacobian (f,x) iff for i, j being Nat st i in Seg m & j in Seg n holds
b₅ * (i,j) = partdiff (f,x,i,j) );

theorem Th28: :: NDIFF11:28

for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) = Mx2Tran (Jacobian (f,x))

proof end;

definition

let m, n be non zero Nat;
let f be PartFunc of (REAL-NS m),(REAL-NS n);
let x be Point of (REAL-NS m);

func Jacobian (f,x) -> Matrix of m,n,F_Real means :Def2: :: NDIFF11:def 2
ex g being PartFunc of (REAL m),(REAL n) ex y being Element of REAL m st
( g = f & y = x & it = Jacobian (g,y) );

existence
ex b₁ being Matrix of m,n,F_Real ex g being PartFunc of (REAL m),(REAL n) ex y being Element of REAL m st
( g = f & y = x & b₁ = Jacobian (g,y) )

proof end;

uniqueness
for b₁, b₂ being Matrix of m,n,F_Real st ex g being PartFunc of (REAL m),(REAL n) ex y being Element of REAL m st
( g = f & y = x & b₁ = Jacobian (g,y) ) & ex g being PartFunc of (REAL m),(REAL n) ex y being Element of REAL m st
( g = f & y = x & b₂ = Jacobian (g,y) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def2 defines Jacobian NDIFF11:def 2 :
for m, n being non zero Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m)
for b₅ being Matrix of m,n,F_Real holds
( b₅ = Jacobian (f,x) iff ex g being PartFunc of (REAL m),(REAL n) ex y being Element of REAL m st
( g = f & y = x & b₅ = Jacobian (g,y) ) );

theorem Th29: :: NDIFF11:29

for m, n being non zero Element of NAT
for x being Point of (REAL-NS m)
for f being PartFunc of (REAL-NS m),(REAL-NS n) st f is_differentiable_in x holds
diff (f,x) = Mx2Tran (Jacobian (f,x))

proof end;

theorem Th30: :: NDIFF11:30

for m being non zero Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS m)
for x being Point of (REAL-NS m) st f is_differentiable_in x holds
( diff (f,x) is invertible iff Jacobian (f,x) is invertible )

proof end;

theorem Th31: :: NDIFF11:31

for m being non zero Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS m)
for x being Point of (REAL-NS m) st f is_differentiable_in x holds
( diff (f,x) is invertible iff Det (Jacobian (f,x)) <> 0. F_Real )

proof end;

theorem :: NDIFF11:32

for l, m, n being non zero Element of NAT
for Z being Subset of [:(REAL-NS l),(REAL-NS m):]
for f being PartFunc of [:(REAL-NS l),(REAL-NS m):],(REAL-NS n)
for a being Point of (REAL-NS l)
for b being Point of (REAL-NS m)
for c being Point of (REAL-NS n)
for z being Point of [:(REAL-NS l),(REAL-NS m):] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`2 (f,z) is invertible holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of (REAL-NS l) st x in Ball (a,r1) holds
ex y being Point of (REAL-NS m) st
( y in Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of (REAL-NS l) st x in Ball (a,r1) holds
for y1, y2 being Point of (REAL-NS m) st y1 in Ball (b,r2) & y2 in Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of (REAL-NS l),(REAL-NS m) st
( dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g is_continuous_on Ball (a,r1) & g . a = b & ( for x being Point of (REAL-NS l) st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & g is_differentiable_on Ball (a,r1) & g `| (Ball (a,r1)) is_continuous_on Ball (a,r1) & ( for x being Point of (REAL-NS l)
for z being Point of [:(REAL-NS l),(REAL-NS m):] st x in Ball (a,r1) & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) & ( for x being Point of (REAL-NS l)
for z being Point of [:(REAL-NS l),(REAL-NS m):] st x in Ball (a,r1) & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) ) & ( for g1, g2 being PartFunc of (REAL-NS l),(REAL-NS m) st dom g1 = Ball (a,r1) & rng g1 c= Ball (b,r2) & ( for x being Point of (REAL-NS l) st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= Ball (b,r2) & ( for x being Point of (REAL-NS l) st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) ) by NDIFF_9:21;

theorem :: NDIFF11:33

for l, m being non zero Element of NAT
for Z being Subset of [:(REAL-NS l),(REAL-NS m):]
for f being PartFunc of [:(REAL-NS l),(REAL-NS m):],(REAL-NS m)
for a being Point of (REAL-NS l)
for b, c being Point of (REAL-NS m)
for z being Point of [:(REAL-NS l),(REAL-NS m):] st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & Det (Jacobian ((f * (reproj2 z)),(z `2))) <> 0. F_Real holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of (REAL-NS l) st x in Ball (a,r1) holds
ex y being Point of (REAL-NS m) st
( y in Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of (REAL-NS l) st x in Ball (a,r1) holds
for y1, y2 being Point of (REAL-NS m) st y1 in Ball (b,r2) & y2 in Ball (b,r2) & f . (x,y1) = c & f . (x,y2) = c holds
y1 = y2 ) & ex g being PartFunc of (REAL-NS l),(REAL-NS m) st
( dom g = Ball (a,r1) & rng g c= Ball (b,r2) & g is_continuous_on Ball (a,r1) & g . a = b & ( for x being Point of (REAL-NS l) st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) & g is_differentiable_on Ball (a,r1) & g `| (Ball (a,r1)) is_continuous_on Ball (a,r1) & ( for x being Point of (REAL-NS l)
for z being Point of [:(REAL-NS l),(REAL-NS m):] st x in Ball (a,r1) & z = [x,(g . x)] holds
diff (g,x) = - ((Inv (partdiff`2 (f,z))) * (partdiff`1 (f,z))) ) & ( for x being Point of (REAL-NS l)
for z being Point of [:(REAL-NS l),(REAL-NS m):] st x in Ball (a,r1) & z = [x,(g . x)] holds
partdiff`2 (f,z) is invertible ) ) & ( for g1, g2 being PartFunc of (REAL-NS l),(REAL-NS m) st dom g1 = Ball (a,r1) & rng g1 c= Ball (b,r2) & ( for x being Point of (REAL-NS l) st x in Ball (a,r1) holds
f . (x,(g1 . x)) = c ) & dom g2 = Ball (a,r1) & rng g2 c= Ball (b,r2) & ( for x being Point of (REAL-NS l) st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )

proof end;

theorem :: NDIFF11:34

for m being non zero Element of NAT
for Z being Subset of (REAL-NS m)
for f being PartFunc of (REAL-NS m),(REAL-NS m)
for a, b being Point of (REAL-NS m) st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & a in Z & f . a = b & Det (Jacobian (f,a)) <> 0. F_Real holds
ex A, B being Subset of (REAL-NS m) ex g being PartFunc of (REAL-NS m),(REAL-NS m) st
( A is open & B is open & A c= dom f & a in A & b in B & f .: A = B & dom g = B & rng g = A & dom (f | A) = A & rng (f | A) = B & f | A is one-to-one & g is one-to-one & g = (f | A) " & f | A = g " & g . b = a & g is_continuous_on B & g is_differentiable_on B & g `| B is_continuous_on B & ( for y being Point of (REAL-NS m) st y in B holds
diff (f,(g /. y)) is invertible ) & ( for y being Point of (REAL-NS m) st y in B holds
diff (g,y) = Inv (diff (f,(g /. y))) ) )

proof end;