:: Implicit Function Theorem -- Part {III } and Inverse Function Theorem --
:: Part {II}
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received September 30, 2022
:: Copyright (c) 2022-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NDIFF11, NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1,
FUNCT_1, NAT_1, FDIFF_1, SUBSET_1, RELAT_1, LOPBAN_1, RCOMP_1, SQUARE_1,
TARSKI, ARYTM_3, VALUED_1, ALGSTR_0, PRALG_1, FUNCT_2, ARYTM_1, SEQ_2,
ORDINAL2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1, XXREAL_0, XBOOLE_0,
FINSEQ_1, RLVECT_1, CFCONT_1, NDIFF_7, MCART_1, CARD_3, METRIC_1,
ORDINAL4, FINSEQ_2, COMPLEX1, RVSUM_1, RFINSEQ, VECTSP_1, MATRIX_1,
MATRIX_3, MATRLIN2, REAL_NS1, EUCLID, XCMPLX_0, FUNCOP_1, FUNCT_7,
MSSUBFAM, RLVECT_5, VALUED_0, QC_LANG1, FVSUM_1, INCSP_1, TREES_1,
MATRIXR1, PDIFF_1, BORSUK_1, AFINSQ_1, EUCLID_7, GROUP_1;
notations GCD_1, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, FINSEQ_1, FINSEQ_2,
VALUED_1, RVSUM_1, RFINSEQ, FINSEQ_7, MATRIX_0, STRUCT_0,
ALGSTR_0, PRE_TOPC, RLVECT_1, VECTSP_1, NORMSP_0, NORMSP_1,
MATRIX_1, FVSUM_1, MATRIX_3, RLVECT_5, EUCLID, LOPBAN_1, MATRIX_6,
NFCONT_1, NDIFF_1, NDIFF_2, REAL_NS1, PDIFF_1, LOPBAN_5, EUCLID_7,
PDIFF_7, PRVECT_3, MATRTOP1, NDIFF_7, MATRIX15, NDIFF_8, LOPBAN13;
constructors VECTSP_2, GCD_1, SQUARE_1, NDIFF_1, RELSET_1, NDIFF_2,
NDIFF_7, NDIFF_8, LOPBAN_5, LOPBAN13, RFINSEQ, MATRTOP1, MATRIX_3,
MATRIX_6, REAL_NS3, RSSPACE, FVSUM_1, MONOID_0, BINOP_2, FDIFF_1,
EUCLID_7, FINSEQ_7, FINSOP_1, PDIFF_1, PDIFF_7, LAPLACE, MATRIX15;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, XBOOLE_0, LOPBAN_1,
PRVECT_3, EUCLID, SQUARE_1, VALUED_0, NAT_1, VECTSP_1, REAL_NS1,
FINSEQ_2, CARD_1, ORDINAL1, FINSEQ_1, FINSEQ_9, FUNCT_1, FUNCT_2,
MONOID_0, NUMBERS, RELAT_1, VALUED_1, XXREAL_0, NDIFF_1, FUNCOP_1,
PDIFF_1, NORMSP_3, RING_2, GCD_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
equalities BINOP_1, SQUARE_1, PRVECT_3, FINSEQ_1, FINSEQ_2, EUCLID, VECTSP_1,
STRUCT_0, LOPBAN_1, RLVECT_1, RVSUM_1, FVSUM_1, MATRIX_0, PDIFF_1;
expansions VECTSP_1, FUNCT_2, TARSKI, NDIFF_1, PDIFF_1;
theorems TARSKI, XBOOLE_0, RLVECT_1, ZFMISC_1, RELAT_1, FUNCT_1, SQUARE_1,
FUNCT_2, LOPBAN_1, PARTFUN1, NFCONT_1, NDIFF_1, VECTSP_1, XXREAL_0,
PRVECT_3, NAT_1, NDIFF_7, VALUED_0, VALUED_1, RVSUM_1, JGRAPH_1,
FINSEQ_3, RFINSEQ, XREAL_1, LOPBAN13, NDIFF_9, ORDINAL1, MATRIX_0,
MATRIX_3, MATRTOP1, EUCLID, REAL_NS1, FINSEQ_1, REAL_NS2, FINSEQ_2,
XREAL_0, CARD_1, LAPLACE, NDIFF10, FVSUM_1, PDIFF_6, PDIFF_7, EUCLID_7,
EUCLID_4, PDIFF_8, NUMBERS, FUNCT_7, PDIFF_1, MATRIX15, LOPBAN15,
INTEGR23, TOPREAL7, STRUCT_0;
schemes NAT_1, BINOP_1, FINSEQ_1, FINSEQ_2, MATRIX_0;
begin :: Matrix and linear transformation on Euclidean spaces
registration
let n be Nat;
cluster REAL-NS n -> finite-dimensional;
correctness by REAL_NS2:62;
end;
theorem
for n be non zero Nat,
X be RealNormSpace,
f be LinearOperator of REAL-NS n,X
holds f is Lipschitzian
proof
let n be non zero Nat,
X be RealNormSpace,
f be LinearOperator of REAL-NS n,X;
REAL-NS n is finite-dimensional &
dim(REAL-NS n) = n by REAL_NS2:62;
hence thesis by LOPBAN15:2;
end;
theorem Th2:
for m be non zero Nat,
s,t be FinSequence of REAL m
st 1 <= len s & s = t | len(s)
holds
for i be Nat st 1 <= i <= len s
holds (accum t).i = (accum s).i
proof
let m be non zero Nat;
let s,t be FinSequence of REAL m;
assume
A1: 1 <= len s & s = t | ( len s );
defpred P[Nat] means
1 <= $1 <= len s implies (accum t).$1 = (accum s).$1;
A2: P[0];
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: P[n];
assume
A5: 1 <= n+1 <= len s; then
A6: n < len s by XXREAL_0:2,NAT_1:16;
A8: 1 in Seg len s by A1;
per cases;
suppose
A7: n=0;
hence (accum t).(n+1)
= t.1 by EUCLID_7:def 10
.= s.1 by A1,A8,FUNCT_1:49
.= (accum s).(n+1) by A7,EUCLID_7:def 10;
end;
suppose
A9: n <> 0;
then
A10: 1 <= n by NAT_1:14;
A11: len(accum t) = len t by EUCLID_7:def 10;
A12: len(accum s) = len s by EUCLID_7:def 10;
n in Seg len s by A6,A10;
then
A16: n in dom(accum s) by A12,FINSEQ_1:def 3;
A13: len s <= len t by A1,FINSEQ_1:79;
then
A14: n < len t by A6,XXREAL_0:2;
then n in Seg len t by A10; then
n in dom accum t by A11,FINSEQ_1:def 3; then
A17: (accum t)/.n
= (accum t).n by PARTFUN1:def 6
.= (accum s)/.n by A4,A5,A9,A16,PARTFUN1:def 6,XXREAL_0:2,NAT_1:14,16;
A18: n+1 in Seg len s by A5;
then
A19: n+1 in dom s by FINSEQ_1:def 3;
n+1 in Seg len t by A18,A13,FINSEQ_1:5,TARSKI:def 3;
then
n+1 in dom t by FINSEQ_1:def 3; then
A21: t/.(n+1)
= t.(n+1) by PARTFUN1:def 6
.= s.(n+1) by A1,A18,FUNCT_1:49
.= s/.(n+1) by A19,PARTFUN1:def 6;
thus
(accum t).(n+1)
= (accum s)/.n + t/.(n+1) by A9,A14,A17,NAT_1:14,EUCLID_7:def 10
.= (accum s).(n+1) by A6,A9,A21,NAT_1:14,EUCLID_7:def 10;
end;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th3:
for m be non zero Nat,
s,s1 be FinSequence of REAL m,
s0 be Element of REAL m
st s1 = s ^ <*s0*>
holds Sum s1 = Sum s + s0
proof
let m be non zero Nat,
s,s1 be FinSequence of REAL m,
s0 be Element of REAL m;
assume
A1: s1 = s ^ <*s0*>;
dom s = Seg(len s) by FINSEQ_1:def 3;
then
A2: s = s1 | len s by A1,FINSEQ_1:21;
per cases;
suppose
A3: len s = 0;
then s = {};
then
A4: s1 = <*s0*> by A1,FINSEQ_1:34;
len s1
= len s + len <*s0*> by A1,FINSEQ_1:22
.= 0 + 1 by A3,FINSEQ_1:40; then
A6: Sum s1
= (accum s1).1 by EUCLID_7:def 11
.= s1.1 by EUCLID_7:def 10
.= s0 by A4;
Sum s = 0* m by A3,EUCLID_7:def 11;
hence Sum s1 = Sum s + s0 by A6,EUCLID_4:1;
end;
suppose
A7: len s <> 0;
then
A8: 1 <= len s by NAT_1:14;
then len s in Seg(len s);
then len s in Seg len(accum s) by EUCLID_7:def 10;
then
A9: len s in dom(accum s) by FINSEQ_1:def 3;
A10: len s1
= len s + len <*s0*> by A1,FINSEQ_1:22
.= len s + 1 by FINSEQ_1:40;
A11: len s < len s1 by A10,NAT_1:13;
then len s in Seg len s1 by A8;
then len s in Seg len(accum s1) by EUCLID_7:def 10;
then
len s in dom(accum s1) by FINSEQ_1:def 3; then
A13: (accum s1)/.(len s)
= (accum s1).(len s) by PARTFUN1:def 6
.= (accum s).(len s) by A2,A8,Th2
.= (accum s)/.(len s) by A9,PARTFUN1:def 6;
A14: (accum s)/.(len s)
= (accum s).(len s) by A9,PARTFUN1:def 6
.= Sum s by A7,EUCLID_7:def 11;
len s + 1 in Seg(len s1) by A10,FINSEQ_1:4;
then len s + 1 in dom s1 by FINSEQ_1:def 3;
then
A15: s1/.(len s + 1)
= s1.(len s + 1) by PARTFUN1:def 6
.= s0 by A1,FINSEQ_1:42;
thus Sum s1
= (accum s1).(len s + 1) by A10,EUCLID_7:def 11
.= Sum s + s0 by A7,A11,A13,A14,A15,NAT_1:14,EUCLID_7:def 10;
end;
end;
theorem Th4:
for m be non zero Nat,
s be FinSequence of REAL m,
j be Nat
st 1 <= j <= m
holds
ex t be FinSequence of REAL
st len t = len s
& ( for i be Nat st 1 <= i <= len s
holds
ex si be Element of REAL m
st si = s.i & t.i = si.j )
& (Sum s).j = Sum t
proof
let m be non zero Nat;
defpred P[Nat] means
for s be FinSequence of REAL m,
j be Nat
st len s = $1 & 1 <= j <= m
holds
ex t be FinSequence of REAL
st len t = len s
& ( for i be Nat st 1 <= i <= len s
holds
ex si be Element of REAL m
st si = s.i & t.i = si.j )
& (Sum s).j = Sum t;
A1: P[0]
proof
let s be FinSequence of REAL m,
j be Nat;
assume
A2: len s = 0 & 1 <= j <= m;
reconsider t = <*>REAL as FinSequence of REAL;
take t;
thus len t = len s by A2;
thus
for i be Nat st 1 <= i <= len s
holds
ex si be Element of REAL m
st si = s.i & t.i = si.j by A2;
(Sum s).j
= (0* m).j by EUCLID_7:def 11,A2
.= 0;
hence thesis by RVSUM_1:72;
end;
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: P[n];
let s be FinSequence of REAL m,
j be Nat;
reconsider sn = s|n as FinSequence of REAL m;
assume
A5: len s = n+1 & 1 <= j <= m; then
A6: len sn = n by FINSEQ_1:59,NAT_1:11;
A7: s = sn ^ <*s.(n+1)*> by A5,FINSEQ_3:55;
n+1 in Seg (n+1) by FINSEQ_1:4;
then n+1 in dom s by A5,FINSEQ_1:def 3;
then s.(n+1) in rng s by FUNCT_1:3;
then reconsider sn1 = s.(n+1) as Element of REAL m;
A8: Sum s = Sum sn + sn1 by Th3,A7;
len(Sum sn) = m by CARD_1:def 7;
then dom(Sum sn) = Seg m by FINSEQ_1:def 3;
then j in dom (Sum sn) by A5;
then
A9: (Sum sn).j in rng (Sum sn) by FUNCT_1:3;
len sn1 = m by CARD_1:def 7;
then dom sn1 = Seg m by FINSEQ_1:def 3;
then j in dom sn1 by A5;
then sn1.j in rng sn1 by FUNCT_1:3;
then reconsider x = (Sum sn).j, y = sn1.j as Element of REAL by A9;
A10: (Sum s).j = x+y by A8,RVSUM_1:11;
consider tn be FinSequence of REAL such that
A11: len tn = len sn
& ( for i be Nat st 1 <= i & i <=len sn
holds
ex sni be Element of REAL m
st sni = sn.i & tn.i = sni.j )
& (Sum sn).j = Sum tn by A4,A5,A6;
reconsider t = tn ^ <*y*> as FinSequence of REAL;
take t;
thus len t
= len tn + len <*y*> by FINSEQ_1:22
.= n + len <*y*> by A5,A11,FINSEQ_1:59,NAT_1:11
.= len s by A5,FINSEQ_1:40;
thus
for i be Nat st 1 <= i <= len s
holds
ex si be Element of REAL m
st si = s.i & t.i = si.j
proof
let i be Nat;
assume
A12: 1 <= i <= len s;
per cases;
suppose
i <> len s;
then i < n+1 by A5,A12,XXREAL_0:1;
then
A13: i <= n by NAT_1:13;
then consider sni be Element of REAL m such that
A14: sni = sn.i & tn.i = sni.j by A6,A11,A12;
take sni;
i in Seg n by A12,A13;
hence sni = s.i by A14,FUNCT_1:49;
i in Seg len tn by A6,A11,A12,A13;
then i in dom tn by FINSEQ_1:def 3;
hence t.i = sni.j by A14,FINSEQ_1:def 7;
end;
suppose
A15: i = len s;
take sn1;
thus sn1 = s.i by A5,A15;
thus t.i = sn1.j by A5,A6,A11,A15,FINSEQ_1:42;
end;
end;
thus (Sum s).j = Sum t by RVSUM_1:74,A11,A10;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A1,A3);
hence thesis;
end;
theorem Th5:
for m be non zero Nat
for x be Element of REAL m
holds
ex s be FinSequence of REAL m
st dom s = Seg m
& (for i be Nat st 1 <= i <= m
holds
ex ei be Element of REAL m
st ei = reproj(i, 0* m).1
& s.i = proj(i,m).x * ei)
& Sum s = x
proof
let m be non zero Nat;
let x be Element of REAL m;
defpred P1[Nat, object] means
ex ei be Element of REAL m
st ei = reproj($1, 0* m).1
& $2 = proj($1,m).x * ei;
A1: for i be Nat st i in Seg m
holds ex y be Element of REAL m st P1[i,y]
proof
let i be Nat;
assume i in Seg m;
reconsider ei = reproj(i, 0* m).1 as
Element of REAL m by FUNCT_2:5,NUMBERS:19;
proj(i,m).x * ei is Element of REAL m;
hence thesis;
end;
consider s be FinSequence of REAL m such that
A2: dom s = Seg m
& for i be Nat st i in Seg m
holds P1[i, s.i] from FINSEQ_1:sch 5(A1);
take s;
thus dom s = Seg m by A2;
m is Element of NAT by ORDINAL1:def 12;
then
A3: len s = m by A2,FINSEQ_1:def 3;
thus
A4: for i be Nat st 1 <= i <= m
holds
ex ei be Element of REAL m
st ei = reproj(i, 0* m).1
& s.i = proj(i,m).x * ei
proof
let i be Nat;
assume 1 <= i <= m;
then i in Seg m;
hence thesis by A2;
end;
A5: len(Sum s) = m by CARD_1:def 7;
A6: len x = m by CARD_1:def 7;
for i be Nat st 1 <= i <= len(Sum s)
holds (Sum s).i = x.i
proof
let i be Nat;
assume
A7: 1 <= i <= len (Sum s);
then consider t be FinSequence of REAL such that
A8: len t = len s
& ( for j be Nat st 1 <= j <= len s
holds
ex sj be Element of REAL m
st sj = s.j & t.j = sj.i )
& (Sum s).i = Sum t by A5,Th4;
i in Seg m by A5,A7;
then
A9: i in dom t by A3,A8,FINSEQ_1:def 3;
consider si be Element of REAL m such that
A10: si = s.i & t.i = si.i by A3,A5,A7,A8;
consider ei be Element of REAL m such that
A11: ei = reproj(i, 0* m).1
& s.i = proj(i,m).x * ei by A4,A5,A7;
A12: proj(i,m).x = x.i by PDIFF_1:def 1;
1 is Element of REAL by NUMBERS:19;
then
A13: reproj(i, 0* m).1
= Replace(0* m,i,1) by PDIFF_1:def 5;
A14: i in dom(0*m) by A5,A7;
ei.i = 1 by A11,A13,A14,FUNCT_7:31;
then
A15: si.i = (x.i) * 1 by A10,A11,A12,RVSUM_1:45;
for j be Nat st j in dom t & j <> i holds t.j = 0
proof
let j be Nat;
assume
A16: j in dom t & j <> i;
then j in Seg len t by FINSEQ_1:def 3;
then
A17: 1 <= j <= len s by A8,FINSEQ_1:1;
then consider sj be Element of REAL m such that
A18: sj = s.j & t.j = sj.i by A8;
consider ei be Element of REAL m such that
A19: ei = reproj(j,0* m) . 1
& s.j = proj(j,m).x * ei by A3,A4,A17;
1 is Element of REAL by NUMBERS:19;
then reproj(j, 0* m).1 = Replace(0* m,j,1) by PDIFF_1:def 5;
then
A20: ei.i
= (0*m).i by A16,A19,FUNCT_7:32
.= 0;
thus t.j
= proj(j,m).x * ei.i by A18,A19,RVSUM_1:45
.= 0 by A20;
end;
hence thesis by A8,A9,A10,A15,INTEGR23:6;
end;
hence Sum s = x by A6,FINSEQ_1:14,CARD_1:def 7;
end;
theorem
for m,n be non zero Element of NAT,
M be Matrix of m,n,F_Real
holds
Mx2Tran(M) is Lipschitzian LinearOperator
of REAL-NS m,REAL-NS n
proof
let m,n be non zero Element of NAT,
M be Matrix of m,n, F_Real;
the carrier of (TOP-REAL n) = the carrier of (REAL-NS n)
& the carrier of (TOP-REAL m) = the carrier of (REAL-NS m) by REAL_NS2:4;
then reconsider f = Mx2Tran(M) as Function of REAL-NS m,REAL-NS n;
for x, y be Element of REAL-NS m
holds f.(x + y) = f.x + f.y
proof
let x, y be Element of REAL-NS m;
reconsider x0 = x, y0 = y as Element of TOP-REAL m by REAL_NS2:4;
thus f.(x + y)
= (Mx2Tran(M)).(x0 + y0) by REAL_NS2:7
.= (Mx2Tran(M)).x0 + (Mx2Tran(M)).y0 by MATRTOP1:22
.= f.x + f.y by REAL_NS2:7;
end;
then
A1: f is additive;
for x be VECTOR of REAL-NS m, a be Real
holds f.(a * x) = a * f.x
proof
let x be VECTOR of REAL-NS m, a be Real;
reconsider x0 = x as Element of TOP-REAL m by REAL_NS2:4;
thus f.(a * x)
= (Mx2Tran(M)).(a * x0) by REAL_NS2:8
.= a * (Mx2Tran(M)).x0 by MATRTOP1:23
.= a * f.x by REAL_NS2:8;
end;
then reconsider f as LinearOperator of REAL-NS m,REAL-NS n
by A1,LOPBAN_1:def 5;
REAL-NS m is finite-dimensional
& dim(REAL-NS m) = m by REAL_NS2:62;
then f is Lipschitzian by LOPBAN15:2;
hence thesis;
end;
theorem Th7:
for m be non zero Element of NAT,
f be LinearOperator of REAL-NS m,REAL-NS m
st f is bijective
holds
ex g be Lipschitzian LinearOperator of REAL-NS m,REAL-NS m
st g = f" & g is one-to-one onto
proof
let m be non zero Element of NAT,
f be LinearOperator of REAL-NS m,REAL-NS m;
assume f is bijective; then
consider g be LinearOperator of REAL-NS m,REAL-NS m
such that
A2: g = f" & g is one-to-one onto by REAL_NS2:85;
REAL-NS m is finite-dimensional
& dim(REAL-NS m) = m by REAL_NS2:62;
then g is Lipschitzian by LOPBAN15:2;
hence thesis by A2;
end;
theorem Th8:
for m be non zero Element of NAT,
f be LinearOperator of REAL-NS m,REAL-NS m
st f is bijective
holds
ex g be Point of R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS m)
st g = f & g is invertible
proof
let m be non zero Element of NAT,
f be LinearOperator of REAL-NS m,REAL-NS m;
assume
A1: f is bijective;
then consider h be Lipschitzian LinearOperator of REAL-NS m,REAL-NS m
such that
A2: h = f" & h is one-to-one onto by Th7;
REAL-NS m is finite-dimensional
& dim(REAL-NS m) = m by REAL_NS2:62;
then f is Lipschitzian by LOPBAN15:2;
then reconsider g = f as Point of
R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS m)
by LOPBAN_1:def 9;
take g;
thus g = f;
A3: rng g = the carrier of REAL-NS m by A1,FUNCT_2:def 3;
h in BoundedLinearOperators(REAL-NS m,REAL-NS m) by LOPBAN_1:def 9;
hence thesis by A1,A2,A3,LOPBAN13:def 1;
end;
theorem
for m,n be non zero Element of NAT,
M be Matrix of m, F_Real
holds
Mx2Tran(M) is bijective
iff
Det M <> 0.F_Real by MATRTOP1:40,MATRTOP1:42;
theorem Th10:
for m,n be non zero Element of NAT,
M be Matrix of m, F_Real
holds
Mx2Tran(M) is bijective
iff
M is invertible
proof
let m,n be non zero Element of NAT,
M be Matrix of m, F_Real;
Det M is unital iff Det M is non zero;
then M is invertible iff Det M <> 0. F_Real by LAPLACE:34, STRUCT_0:def 12;
hence thesis by MATRTOP1:40,42;
end;
theorem Th11:
for m be non zero Element of NAT,
f be 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
let m be non zero Element of NAT;
let f be Point of
R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS m);
assume
A1: f is one-to-one & rng f = the carrier of REAL-NS m;
reconsider g = f as Lipschitzian LinearOperator of REAL-NS m,REAL-NS m
by LOPBAN_1:def 9;
g is bijective by A1,FUNCT_2:def 3;
then
ex f be Point of R_NormSpace_of_BoundedLinearOperators(REAL-NS m,REAL-NS m)
st f = g & f is invertible by Th8;
hence thesis;
end;
theorem Th12:
for m be non zero Element of NAT,
f be Point of
R_NormSpace_of_BoundedLinearOperators(REAL-NS m, REAL-NS m),
M be Matrix of m, F_Real
st f = Mx2Tran(M)
holds
f is invertible
iff
M is invertible
proof
let m be non zero Element of NAT,
f be Point of
R_NormSpace_of_BoundedLinearOperators(REAL-NS m, REAL-NS m),
M be Matrix of m, F_Real;
assume
A1: f = Mx2Tran(M);
A2: the carrier of TOP-REAL m = REAL m by EUCLID:22;
A3: the carrier of REAL-NS m = REAL m by REAL_NS1:def 4;
hereby
assume f is invertible;
then Mx2Tran(M) is one-to-one
& rng(Mx2Tran(M)) = the carrier of REAL-NS m by A1,LOPBAN13:def 1;
then Mx2Tran(M) is bijective by A2,A3,FUNCT_2:def 3;
hence M is invertible by Th10;
end;
assume M is invertible;
then Mx2Tran(M) is bijective by Th10;
then f is one-to-one & rng f = the carrier of REAL-NS m
by A1,A2,A3,FUNCT_2:def 3;
hence f is invertible by Th11;
end;
theorem
for m be non zero Element of NAT,
f be Point of
R_NormSpace_of_BoundedLinearOperators(REAL-NS m, REAL-NS m),
M be Matrix of m, F_Real
st f = Mx2Tran(M)
holds
f is invertible
iff
Det M <> 0.F_Real
proof
let m be non zero Element of NAT,
f be Point of
R_NormSpace_of_BoundedLinearOperators (REAL-NS m, REAL-NS m),
M be Matrix of m, F_Real;
Det M is unital iff Det M is non zero;
then A1: Det M is unital iff Det M <> 0.F_Real by STRUCT_0:def 12;
assume f = Mx2Tran(M);
then
f is invertible
iff
M is invertible by Th12;
hence thesis by A1, LAPLACE:34;
end;
theorem Th14:
for m,n be non zero Element of NAT
ex f be Function of [:REAL m,REAL n:], REAL(m+n)
st ( for x be Element of REAL m, y be Element of REAL n
holds f.(x,y) = x ^ y )
& f is one-to-one & f is onto
proof
let m,n be non zero Element of NAT;
defpred S1[object, object, object] means
ex x be Element of REAL m,
y be Element of REAL n
st x = $1 & y = $2 & $3 = x ^ y;
A1: for x, y be object st x in REAL m & y in REAL n
holds ex z be object st z in REAL(m+n) & S1[x,y,z]
proof
let x, y be object;
assume
A2: x in REAL m & y in REAL n;
then
reconsider x0 = x as Element of REAL m;
reconsider y0 = y as Element of REAL n by A2;
set z0 = x0 ^ y0;
A4: len z0 = m + n by CARD_1:def 7;
z0 in REAL* by FINSEQ_1:def 11;
then z0 in (m+n) -tuples_on REAL by A4;
then reconsider z = z0 as Element of REAL(m+n);
take z;
thus thesis;
end;
consider f be Function of [:REAL m,REAL n:],REAL(m+n) such that
A5: for x, y be object st x in REAL m & y in REAL n
holds S1[x,y,f.(x,y)] from BINOP_1:sch 1(A1);
take f;
thus
A6: for x be Element of REAL m, y be Element of REAL n
holds f.(x,y) = x ^ y
proof
let x be Element of REAL m,
y be Element of REAL n;
ex x0 be Element of REAL m,
y0 be Element of REAL n
st x0 = x & y0 = y & f.(x,y) = x0 ^ y0 by A5;
hence thesis;
end;
now
let z1, z2 be object;
assume
A7: z1 in [:REAL m,REAL n:]
& z2 in [:REAL m,REAL n:]
& f.z1 = f.z2; then
consider x1, y1 be object such that
A8: x1 in REAL m & y1 in REAL n & z1 = [x1,y1] by ZFMISC_1:def 2;
consider x2, y2 be object such that
A9: x2 in REAL m & y2 in REAL n & z2 = [x2,y2] by A7,ZFMISC_1:def 2;
consider xx1 be Element of REAL m,
yy1 be Element of REAL n such that
A10: xx1 = x1 & yy1 = y1 & f.(x1,y1) = xx1 ^ yy1 by A5,A8;
consider xx2 be Element of REAL m,
yy2 be Element of REAL n such that
A11: xx2 = x2 & yy2 = y2 & f.(x2,y2) = xx2 ^ yy2 by A5,A9;
len xx1
= m by CARD_1:def 7
.= len xx2 by CARD_1:def 7;
then
A12: dom xx1 = dom xx2 by FINSEQ_3:29;
xx1
= (xx1 ^ yy1) | (dom xx1) by FINSEQ_1:21
.= xx2 by A7,A8,A9,A10,A11,A12,FINSEQ_1:21;
hence z1 = z2 by A7,A8,A9,A10,A11,FINSEQ_1:33;
end;
hence f is one-to-one by FUNCT_2:19;
now
let w be object;
assume w in REAL(m+n);
then
A13: ex s be Element of REAL * st w=s & len s = m+n;
then
reconsider w0 = w as FinSequence of REAL;
set x = w0 | m;
set y = w0 /^ m;
m <= m+n by NAT_1:11; then
A16: len y = m+n -m by A13,RFINSEQ:def 1;
A15: len x = m by A13,NAT_1:11,FINSEQ_1:59;
x in REAL* by FINSEQ_1:def 11;
then x in { s where s is Element of REAL * : len s = m } by A15;
then reconsider x0 = x as Element of REAL m;
y in REAL* by FINSEQ_1:def 11;
then y in { s where s is Element of REAL * : len s = n } by A16;
then reconsider y0 = y as Element of REAL n;
set z = [x0,y0];
A17: z in [:REAL m,REAL n:] by ZFMISC_1:87;
f.z
= f.(x0,y0)
.= x0 ^ y0 by A6
.= w by RFINSEQ:8;
hence w in rng f by FUNCT_2:4,A17;
end;
then REAL(m+n) c= rng f;
hence f is onto by XBOOLE_0:def 10;
end;
theorem
for m,n be non zero Element of NAT
ex f be Function of [:REAL-NS m,REAL-NS n:], REAL-NS(m+n)
st f is one-to-one & f is onto
& ( for x be Element of REAL m, y be Element of REAL n
holds f.(x, y) = x ^ y )
& ( for u,v be Point of [:REAL-NS m,REAL-NS n:]
holds f.(u + v) = f.u + f.v )
& ( for u be Point of [:REAL-NS m,REAL-NS n:], r be Real
holds f.(r * u) = r * f.u )
& f.(0.[:REAL-NS m,REAL-NS n:]) = 0.(REAL-NS(m+n))
& ( for u be Point of [:REAL-NS m,REAL-NS n:]
holds ||.f.u.|| = ||.u.|| )
proof
let m,n be non zero Element of NAT;
consider f be Function of [:REAL m,REAL n:],REAL(m+n)
such that
A1: ( for x be Element of REAL m, y be Element of REAL n
holds f.(x, y) = x ^ y )
& f is one-to-one & f is onto by Th14;
A2: the carrier of REAL-NS m = REAL m
& the carrier of REAL-NS n = REAL n
& the carrier of REAL-NS(m+n) = REAL(m+n) by REAL_NS1:def 4;
reconsider f as Function of [:REAL-NS m,REAL-NS n:], REAL-NS(m+n) by A2;
take f;
A3: for u,v be Point of [:REAL-NS m,REAL-NS n:] holds f.(u+v) = f.u + f.v
proof
let u,v be Point of [:REAL-NS m,REAL-NS n:];
consider x1 be Point of REAL-NS m, y1 be Point of REAL-NS n such that
A4: u = [x1,y1] by PRVECT_3:18;
consider x2 be Point of REAL-NS m, y2 be Point of REAL-NS n such that
A5: v = [x2,y2] by PRVECT_3:18;
reconsider px1 = x1, px2 = x2 as Element of REAL m by REAL_NS1:def 4;
reconsider py1 = y1, py2 = y2 as Element of REAL n by REAL_NS1:def 4;
reconsider px1x2 = x1 + x2 as Element of REAL m by REAL_NS1:def 4;
reconsider py1y2 = y1 + y2 as Element of REAL n by REAL_NS1:def 4;
A6: f.u
= f.(x1, y1) by A4
.= px1 ^ py1 by A1;
A7: f.v
= f.(x2, y2) by A5
.= px2 ^ py2 by A1;
A8: f.(u+v)
= f.(x1 + x2, y1 + y2) by A4,A5,PRVECT_3:18
.= px1x2 ^ py1y2 by A1;
reconsider fu = f.u, fv = f.v, fuv = f.(u + v)
as Element of REAL(m+n) by REAL_NS1:def 4;
A9: fu + fv = f.u + f.v by REAL_NS1:2;
A10: x1 + x2 = px1 + px2 by REAL_NS1:2;
A11: y1 + y2 = py1 + py2 by REAL_NS1:2;
A12: len(fu + fv) = m + n by CARD_1:def 7;
A13: len px1 = m & len px2 = m by CARD_1:def 7;
A14: len py1 = n & len py2 = n by CARD_1:def 7;
A15: len px1x2 = m by CARD_1:def 7;
A16: len py1y2 = n by CARD_1:def 7;
for i be Nat st 1 <= i & i <= len fuv
holds fuv.i = (fu + fv).i
proof
let i be Nat;
assume
A17: 1 <= i & i <= len fuv;
per cases;
suppose
A18: i <= m;
then i in Seg (len px1x2) by A15,A17;
then i in dom px1x2 by FINSEQ_1:def 3;
then
A19: fuv.i = px1x2.i by A8,FINSEQ_1:def 7;
A20: (fu + fv).i = fu.i + fv.i by RVSUM_1:11;
i in Seg len px1 by A13,A17,A18;
then i in dom px1 by FINSEQ_1:def 3;
then
A21: fu.i = px1.i by A6,FINSEQ_1:def 7;
i in Seg(len px2) by A13,A17,A18;
then i in dom px2 by FINSEQ_1:def 3;
then fv.i = px2.i by A7,FINSEQ_1:def 7;
hence fuv.i = (fu+fv).i by A10,A19,A20,A21,RVSUM_1:11;
end;
suppose
m < i;
then not i in Seg(len px1x2) by A15,FINSEQ_1:1;
then
A22: not i in dom px1x2 by FINSEQ_1:def 3;
i in Seg (len fuv) by A17;
then i in dom(px1x2 ^ py1y2) by A8,FINSEQ_1:def 3;
then consider j be Nat such that
A23: j in dom py1y2 & i = (len px1x2) + j by A22,FINSEQ_1:25;
A24: fuv.i = py1y2.j by A8,A23,FINSEQ_1:def 7;
A25: (fu + fv).i = fu.i + fv.i by RVSUM_1:11;
j in Seg len (py1y2) by A23,FINSEQ_1:def 3;
then j in dom py1 by A14,CARD_1:def 7,FINSEQ_1:def 3;
then
A26: fu.i = py1.j by A6,A13,A15,A23,FINSEQ_1:def 7;
j in Seg(len py2) by A16,A23,CARD_1:def 7,FINSEQ_1:def 3;
then j in dom py2 by FINSEQ_1:def 3;
then
fv.i = py2.j by A7,A23,A13,A15,FINSEQ_1:def 7;
hence fuv.i = (fu + fv).i by A11,A24,A25,A26,RVSUM_1:11;
end;
end;
hence thesis by A9,A12,FINSEQ_1:14,CARD_1:def 7;
end;
A28: for u be Point of [:REAL-NS m,REAL-NS n:],
r be Real
holds f.(r * u) = r * (f.u)
proof
let u be Point of [:REAL-NS m,REAL-NS n:],
r be Real;
consider x1 be Point of REAL-NS m,
y1 be Point of REAL-NS n such that
A29: u = [x1,y1] by PRVECT_3:18;
reconsider px1 = x1, prx1 = r * x1 as Element of REAL m
by REAL_NS1:def 4;
reconsider py1 = y1, pry1 = r * y1 as Element of REAL n
by REAL_NS1:def 4;
A30: f.u
= f.(x1, y1) by A29
.= px1 ^ py1 by A1;
A31: f.(r * u)
= f.(r * x1, r * y1) by A29,PRVECT_3:18
.= prx1 ^ pry1 by A1;
reconsider fu = f.u, fru = f.(r * u)
as Element of REAL(m+n) by REAL_NS1:def 4;
A32: r * fu = r * f.u by REAL_NS1:3;
A33: r * x1 = r * px1 by REAL_NS1:3;
A34: r * y1 = r * py1 by REAL_NS1:3;
A35: len(r * fu) = m+n by CARD_1:def 7;
A36: len px1 = m by CARD_1:def 7;
A37: len py1 = n by CARD_1:def 7;
A38: len prx1 = m by CARD_1:def 7;
for i be Nat st 1 <= i & i <= len fru
holds fru.i = (r * fu).i
proof
let i be Nat;
assume
A39: 1 <= i & i <= len fru;
per cases;
suppose
A40: i <= m;
then i in Seg(len prx1) by A38,A39;
then i in dom prx1 by FINSEQ_1:def 3;
then
A41: fru.i = prx1.i by A31,FINSEQ_1:def 7;
A42: (r * fu).i = r * fu.i by RVSUM_1:44;
i in Seg (len px1) by A36,A39,A40;
then i in dom px1 by FINSEQ_1:def 3;
then fu.i = px1.i by A30,FINSEQ_1:def 7;
hence fru.i = (r * fu).i by A33,A41,A42,RVSUM_1:44;
end;
suppose
m < i;
then not i in Seg len prx1 by A38,FINSEQ_1:1;
then
A43: not i in dom prx1 by FINSEQ_1:def 3;
i in Seg len fru by A39;
then i in dom(prx1 ^ pry1) by A31,FINSEQ_1:def 3;
then consider j be Nat such that
A44: j in dom pry1 & i = (len prx1) + j by A43,FINSEQ_1:25;
A45: fru.i = pry1.j by A44,A31,FINSEQ_1:def 7;
A46: (r * fu).i = r * fu.i by RVSUM_1:44;
j in Seg len (pry1) by A44,FINSEQ_1:def 3;
then j in dom py1 by A37,CARD_1:def 7,FINSEQ_1:def 3;
then fu.i = py1.j by A30,A36,A38,A44,FINSEQ_1:def 7;
hence fru.i = (r * fu).i by A34,A45,A46,RVSUM_1:44;
end;
end;
hence thesis by A32,A35,FINSEQ_1:14,CARD_1:def 7;
end;
0.[:REAL-NS m,REAL-NS n:]
= 0.[:REAL-NS m,REAL-NS n:] + 0.[:REAL-NS m,REAL-NS n:] by RLVECT_1:4;
then
A47: f.(0.[:REAL-NS m,REAL-NS n:]) + f.(0.[:REAL-NS m,REAL-NS n:])
- f.(0.[:REAL-NS m,REAL-NS n:])
= f.(0.[:REAL-NS m,REAL-NS n:]) - f.(0.[:REAL-NS m,REAL-NS n:]) by A3
.= 0.(REAL-NS (m+n)) by RLVECT_1:15;
A48: f.(0.[:REAL-NS m,REAL-NS n:]) + f.(0.[:REAL-NS m,REAL-NS n:])
- f.(0.[:REAL-NS m,REAL-NS n:])
= f.(0.[:REAL-NS m,REAL-NS n:]) +
(f.(0.[:REAL-NS m,REAL-NS n:] ) - f.(0.[:REAL-NS m,REAL-NS n:]))
by RLVECT_1:28
.= f.(0.[:REAL-NS m,REAL-NS n:]) + 0.(REAL-NS (m+n)) by RLVECT_1:15
.= f.(0.[:REAL-NS m,REAL-NS n:]) by RLVECT_1:4;
for u be Point of [:REAL-NS m,REAL-NS n:]
holds ||.f.u.|| = ||.u.||
proof
let u be Point of [:REAL-NS m,REAL-NS n:];
consider x1 be Point of REAL-NS m, y1 be Point of REAL-NS n
such that
A50: u = [x1,y1] by PRVECT_3:18;
reconsider px1 = x1 as Element of REAL m by REAL_NS1:def 4;
reconsider py1 = y1 as Element of REAL n by REAL_NS1:def 4;
A51: f.u
= f.(x1, y1) by A50
.= px1 ^ py1 by A1;
consider v be Element of REAL 2 such that
A52: v = <*||.x1.||,||.y1.||*> & ||.u.|| = |.v.| by A50,PRVECT_3:18;
reconsider fu = f.u as Element of REAL (m+n) by REAL_NS1:def 4;
A53: ||.f.u.|| = |.fu.| by REAL_NS1:1;
sqr px1 is Element of REAL m
& for k be Nat st k in Seg m holds 0 <= (sqr px1).k
proof
thus sqr px1 is Element of REAL m;
let k be Nat;
assume k in Seg m;
(sqr px1).k
= (px1.k) ^2 by VALUED_1:11
.= (px1.k) * (px1.k);
hence thesis by XREAL_1:63;
end;
then
A54: |.px1.| = sqrt(Sum(sqr px1)) & 0 <= Sum(sqr px1) by REAL_NS1:7;
sqr py1 is Element of REAL n
& for k be Nat st k in Seg n holds 0 <= (sqr py1).k
proof
thus sqr py1 is Element of REAL n;
let k be Nat;
(sqr py1).k
= (py1.k) ^2 by VALUED_1:11
.= (py1.k) * (py1.k);
hence thesis by XREAL_1:63;
end;
then |.py1.| = sqrt(Sum(sqr py1)) & 0 <= Sum(sqr py1) by REAL_NS1:7;
then
A55: |.py1.| ^2 = Sum(sqr py1) by SQUARE_1:def 2;
sqr(px1 ^ py1) is Element of REAL(m+n)
& for k be Nat st k in Seg(m+n) holds 0 <= (sqr(px1 ^ py1)).k
proof
sqr(fu) is Element of REAL(m+n);
hence sqr(px1 ^ py1) is Element of REAL(m+n) by A51;
let k be Nat;
(sqr(px1 ^ py1)).k
= ((px1 ^ py1).k) ^2 by VALUED_1:11
.= ((px1 ^ py1).k) * ((px1 ^ py1).k);
hence thesis by XREAL_1:63;
end;
then
A56: |.px1 ^ py1.| = sqrt(Sum sqr(px1 ^ py1))
& 0 <= Sum(sqr(px1 ^ py1)) by REAL_NS1:7;
reconsider ww = v as Point of TOP-REAL 2 by EUCLID:22;
A57: ww `1 = ||.x1.|| by A52;
A58: ww `2 = ||.y1.|| by A52;
|.fu.|^2
= Sum(sqr(px1 ^ py1) ) by A51,A56,SQUARE_1:def 2
.= Sum((sqr px1) ^ (sqr py1)) by TOPREAL7:10
.= Sum((sqr px1)) + Sum(sqr py1) by RVSUM_1:75
.= |.px1.| ^2 + |.py1.| ^2 by A54,A55,SQUARE_1:def 2
.= ||.x1.|| ^2 + |.py1.| ^2 by REAL_NS1:1
.= ||.x1.|| ^2 + ||.y1.|| ^2 by REAL_NS1:1
.= |.v.|^2 by A57,A58,JGRAPH_1:29;
then sqrt(|.fu.|^2) = |.v.| by SQUARE_1:22;
hence thesis by A52,A53,SQUARE_1:22;
end;
hence thesis by A1,A3,A28,A47,A48,REAL_NS1:def 4;
end;
begin :: Total derivative and partial derivative
theorem Th16:
for X,Y be RealNormSpace,
x be Point of X,
f be Lipschitzian LinearOperator of X,Y
holds f is_differentiable_in x
& f = diff(f,x)
proof
let X,Y be RealNormSpace,
x be Point of X,
f be Lipschitzian LinearOperator of X,Y;
set CX = [#]X;
A1: CX = dom f by FUNCT_2:def 1;
reconsider g = (the carrier of X) --> 0.Y as PartFunc of X,Y;
reconsider f0 = f as Element of BoundedLinearOperators(X,Y)
by LOPBAN_1:def 9;
A2: dom g = the carrier of X;
A3: for h be (0.X)-convergent sequence of X st h is non-zero
holds (||.h.||") (#) (g/*h) is convergent
& lim((||.h.||") (#) (g/*h)) = 0.Y
proof
let h be (0.X)-convergent sequence of X;
assume h is non-zero;
A4: for n be Nat holds ((||.h.||") (#) (g/*h)).n = 0.Y
proof
let n be Nat;
A5: g/.(h.n)
= g.(h.n) by A2,PARTFUN1:def 6
.= 0.Y;
A6: rng h c= dom g;
A7: n in NAT by ORDINAL1:def 12;
thus ((||.h.||") (#) (g/*h)).n
= (||.h.||".n) * ((g/*h).n) by NDIFF_1:def 2
.= (||.h.||".n) * (g/.(h.n)) by A6,A7,FUNCT_2:109
.= 0.Y by A5,RLVECT_1:10;
end;
then
A8: (||.h.||") (#) (g/*h) is constant by VALUED_0:def 18;
hence (||.h.||") (#) (g/*h) is convergent by NDIFF_1:18;
((||.h.||") (#) (g/*h)).0 = 0.Y by A4;
hence lim ((||.h.||") (#) (g/*h)) = 0.Y by A8,NDIFF_1:18;
end;
reconsider g as RestFunc of X,Y by A3,NDIFF_1:def 5;
ex g be Real
st 0 < g
& { y where y is Point of X : ||.(y - x).|| < g } c= CX
by NDIFF_1:3;
then reconsider CX as Neighbourhood of x by NFCONT_1:def 1;
A9: for x0 be Point of X st x0 in CX
holds f/.x0 - f/.x = f0.(x0-x) + g/.(x0-x)
proof
let x0 be Point of X;
A10: g/.(x0-x)
= g.(x0-x) by A2,PARTFUN1:def 6
.= 0.Y;
assume x0 in CX;
thus f/.x0 - f/.x
= f.x0 + (-1) * f.x by RLVECT_1:16
.= f.x0 + f.((-1) * x) by LOPBAN_1:def 5
.= f.(x0 + (-1) * x) by VECTSP_1:def 20
.= f.(x0 - x) by RLVECT_1:16
.= f0.(x0 - x) + g/.(x0 - x) by A10,RLVECT_1:4;
end;
hence f is_differentiable_in x by A1;
hence diff(f,x) = f by A1,A9,NDIFF_1:def 7;
end;
theorem
for n be non zero Nat,
i be Nat,
x be Point of REAL-NS n
st 1 <= i <= n
holds
Proj(i,n) is_differentiable_in x
&
diff(Proj(i,n),x) = Proj(i,n)
proof
let n be non zero Nat,
i be Nat,
x be Point of REAL-NS n;
assume
A1: 1 <= i <= n;
n is non zero Element of NAT by ORDINAL1:def 12;
then Proj(i,n) is Lipschitzian LinearOperator
of REAL-NS n,REAL-NS 1 by A1,PDIFF_8:6;
hence thesis by Th16;
end;
theorem Th18:
for m, n be non zero Nat
for f be PartFunc of REAL m,REAL n
for x be Element of REAL m
holds
f is_differentiable_in x
iff
for i be Nat st 1 <= i <= n
holds
ex fi be PartFunc of REAL m,REAL 1
st fi = Proj(i,n) * f
& fi is_differentiable_in x
proof
let m, n be non zero Nat;
let f be PartFunc of REAL m,REAL n;
let x be Element of REAL m;
A1: the carrier of REAL-NS m = REAL m
& the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
A2: the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
reconsider f0 = f as PartFunc of REAL-NS m,REAL-NS n by A1;
reconsider x0 = x as Point of REAL-NS m by REAL_NS1:def 4;
hereby
assume
A3: f is_differentiable_in x;
thus
for i be Nat st 1 <= i <= n
holds
ex fi be PartFunc of REAL m,REAL 1
st fi = Proj(i,n) * f
& fi is_differentiable_in x
proof
let i be Nat;
assume
A4: 1 <= i <= n;
reconsider fi = Proj(i,n) * f0 as PartFunc of REAL m,REAL 1
by A2,REAL_NS1:def 4;
take fi;
thus fi = Proj(i,n) * f;
thus fi is_differentiable_in x by A3,A4,PDIFF_6:29;
end;
end;
assume
A5: for i be Nat st 1 <= i <= n
holds
ex fi be PartFunc of REAL m,REAL 1
st fi = Proj(i,n) * f
& fi is_differentiable_in x;
for i be Nat st 1 <= i <= n
holds Proj(i,n) * f0 is_differentiable_in x0
proof
let i be Nat;
assume 1 <= i <= n;
then consider fi be PartFunc of REAL m,REAL 1 such that
A6: fi = Proj(i,n) * f
& fi is_differentiable_in x by A5;
thus Proj(i,n) * f0 is_differentiable_in x0 by A6;
end;
hence f is_differentiable_in x by PDIFF_6:29;
end;
theorem Th19:
for m, n be non zero Nat
for f be PartFunc of REAL m,REAL n
for x be Element of REAL m
holds
f is_differentiable_in x
iff
for i be Nat st 1 <= i <= n
holds
ex fi be PartFunc of REAL m,REAL
st fi = proj(i,n) * f
& fi is_differentiable_in x
proof
let m, n be non zero Nat;
let f be PartFunc of REAL m,REAL n;
let x be Element of REAL m;
reconsider y = x as Point of REAL-NS m by REAL_NS1:def 4;
A2: for i be Nat holds <>* (proj(i,n) * f) = Proj(i,n) * f
proof
let i be Nat;
reconsider fi = proj(i,n) * f as PartFunc of REAL m,REAL;
Proj(i,n) * f
= ((proj(1,1) qua Function)" * proj(i,n)) * f by PDIFF_1:11
.= <>* fi by RELAT_1:36;
hence thesis;
end;
hereby
assume
A3: f is_differentiable_in x;
thus
for i be Nat st 1 <= i <= n
holds
ex fi be PartFunc of REAL m,REAL
st fi = proj(i,n) * f
& fi is_differentiable_in x
proof
let i be Nat;
assume 1 <= i <= n;
then consider Fi be PartFunc of REAL m,REAL 1 such that
A4: Fi = Proj(i,n) * f
& Fi is_differentiable_in x by A3,Th18;
reconsider fi = proj(i,n) * f as PartFunc of REAL m,REAL;
take fi;
thus fi = proj(i,n) * f;
<>* fi = Fi by A4,A2;
hence fi is_differentiable_in x by A4,PDIFF_7:def 1;
end;
end;
assume
A5: for i be Nat st 1 <= i <= n
holds
ex fi be PartFunc of REAL m,REAL
st fi = proj(i,n) * f
& fi is_differentiable_in x;
for i be Nat st 1 <= i <= n
holds
ex Fi be PartFunc of REAL m,REAL 1
st Fi = Proj(i,n) * f
& Fi is_differentiable_in x
proof
let i be Nat;
assume 1 <= i <= n;
then consider fi be PartFunc of REAL m,REAL such that
A6: fi = proj(i,n) * f
& fi is_differentiable_in x by A5;
reconsider Fi = Proj(i,n) * f
as PartFunc of REAL m,REAL 1 by REAL_NS1:def 4;
take Fi;
thus Fi = Proj(i,n) * f;
Fi = <>* fi by A2,A6;
hence Fi is_differentiable_in x by A6,PDIFF_7:def 1;
end;
hence f is_differentiable_in x by Th18;
end;
theorem Th20:
for m, n be non zero Nat
for f be PartFunc of REAL m,REAL n
for x be Element of REAL m
st f is_differentiable_in x
holds
for i be Nat,
fi be PartFunc of REAL m,REAL
st 1 <= i <= n
& fi = proj(i,n) * f
holds
fi is_differentiable_in x
& diff(fi,x) = proj(i,n) * diff(f,x)
proof
let m, n be non zero Nat;
let f be PartFunc of REAL m,REAL n;
let x be Element of REAL m;
A1: the carrier of REAL-NS m = REAL m
& the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
assume
A2: f is_differentiable_in x;
let i be Nat,
fi be PartFunc of REAL m,REAL;
assume
A3: 1 <= i <= n
& fi = proj(i,n) * f; then
A4: ex fi be PartFunc of REAL m,REAL
st fi = proj(i,n) * f
& fi is_differentiable_in x by A2,Th19;
hence fi is_differentiable_in x by A3;
reconsider f0 = f as PartFunc of REAL-NS m,REAL-NS n by A1;
reconsider x0 = x as Point of REAL-NS m by REAL_NS1:def 4;
A5: Proj(i,n) * diff(f0,x0) = diff(Proj(i,n) * f0, x0) by A2,A3,PDIFF_6:28;
A6: Proj(i,n) * f0
= ((proj(1,1) qua Function)" * proj(i,n)) * f0 by PDIFF_1:11
.= <>* fi by A3,RELAT_1:36;
A7: Proj(i,n) * diff(f0,x0) = diff((<>* fi), x)
by A3,A4,A5,A6,PDIFF_6:3,PDIFF_7:def 1;
A8: diff(fi,x)
= proj(1,1) * diff(<>* fi, x) by PDIFF_7:def 2
.= proj(1,1) * (Proj(i,n) * diff(f,x)) by A2,A7,PDIFF_6:3
.= (proj(1,1) * Proj(i,n)) * diff(f,x) by RELAT_1:36;
1 in Seg 1;
then
A9: rng proj(1,1) = REAL by PDIFF_1:1;
proj(1,1) * Proj(i,n)
= proj(1,1) * ((proj(1,1) qua Function)" * proj(i,n)) by PDIFF_1:11
.= (proj(1,1) * (proj(1,1) qua Function)") * proj(i,n) by RELAT_1:36
.= (id REAL) * proj(i,n) by A9,FUNCT_1:39
.= proj(i,n) by FUNCT_2:17;
hence thesis by A8;
end;
theorem
for m,n be non zero Nat,
f be PartFunc of REAL m,REAL n,
x be Element of REAL m
st f is_differentiable_in x
holds
for i,j be Nat
st 1 <= i <= m
& 1 <= j <= n
holds f is_partial_differentiable_in x,i,j
proof
let m,n be non zero Nat;
let f be PartFunc of REAL m,REAL n;
let x be Element of REAL m;
assume
A1: f is_differentiable_in x;
let i,j be Nat;
assume
A2: 1 <= i <= m;
assume 1 <= j <= n; then
consider fj be PartFunc of REAL m,REAL such that
A4: fj = proj(j,n) * f
& fj is_differentiable_in x by A1,Th19;
fj is_partial_differentiable_in x,i by A2,A4,PDIFF_7:23;
hence thesis by A4;
end;
theorem
for m,n be non zero Nat,
f be PartFunc of REAL-NS m,REAL-NS n,
x be Element of REAL-NS m
st f is_differentiable_in x
holds
for i,j be Nat
st 1 <= i <= m
& 1 <= j <= n
holds f is_partial_differentiable_in x,i,j
proof
let m,n be non zero Nat;
let f be PartFunc of REAL-NS m,REAL-NS n;
let x be Element of REAL-NS m;
assume
A1: f is_differentiable_in x;
let i,j be Nat;
assume
A2: 1 <= i <= m;
assume
A3: 1 <= j <= n;
reconsider fj = Proj(j,n) * f as PartFunc of REAL-NS m,REAL-NS 1;
fj is_differentiable_in x by A1,A3,PDIFF_6:29;
then fj is_partial_differentiable_in x,i by A2,PDIFF_7:21;
hence thesis;
end;
theorem Th23:
for m be non zero Nat
for f be PartFunc of REAL m,REAL
for x be Element of REAL m
st f is_differentiable_in x
holds
for u,v be Element of REAL m
holds diff(f,x).(u+v) = diff(f,x).u + diff(f,x).v
proof
let m be non zero Nat;
let f be PartFunc of REAL m,REAL;
let x be Element of REAL m;
assume
A1: f is_differentiable_in x;
let u,v be Element of REAL m;
A3: diff(f,x) = proj(1,1) * diff(<>* f, x) by PDIFF_7:def 2;
<>* f is_differentiable_in x by A1,PDIFF_7:def 1; then
consider g be PartFunc of REAL-NS m,REAL-NS 1,
y be Point of REAL-NS m such that
A4: <>* f = g & x = y & diff(<>* f, x) = diff(g,y) by PDIFF_1:def 8;
reconsider DF = diff(g,y) as
Lipschitzian LinearOperator of REAL-NS m,REAL-NS 1 by LOPBAN_1:def 9;
A5: DF is additive;
A6: dom(diff(<>* f,x))
= dom DF by A4
.= the carrier of REAL-NS m by FUNCT_2:def 1;
A7: the carrier of REAL-NS m = REAL m by REAL_NS1:def 4;
reconsider u1 = u,v1 = v as Point of REAL-NS m by REAL_NS1:def 4;
thus diff(f,x).(u+v)
=(proj(1,1) * diff(<>* f, x)).(u+v) by PDIFF_7:def 2
.= proj(1,1).(diff(<>* f, x).(u+v)) by A6,A7,FUNCT_1:13
.= proj(1,1).(DF.(u1 + v1)) by A4,REAL_NS1:2
.= proj(1,1).(DF.u1 + DF.v1) by A5
.= proj(1,1).(DF.u1) + proj(1,1).(DF.v1) by PDIFF_1:4
.= (proj(1,1) * diff(<>* f, x)).u + proj(1,1).(diff(<>* f, x).v)
by A4,A6,FUNCT_1:13
.= diff(f,x).u + diff(f,x).v by A3,A6,A7,FUNCT_1:13;
end;
theorem Th24:
for m be non zero Nat
for f be PartFunc of REAL m,REAL
for x be Element of REAL m
st f is_differentiable_in x
holds
for u be Element of REAL m, a be Real
holds diff(f,x).(a*u) = a * diff(f,x).u
proof
let m be non zero Nat;
let f be PartFunc of (REAL m),REAL;
let x be Element of REAL m;
assume
A1: f is_differentiable_in x;
let u be Element of REAL m;
let a be Real;
A2: <>* f is_differentiable_in x by A1,PDIFF_7:def 1;
consider g be PartFunc of REAL-NS m,REAL-NS 1,
y be Point of REAL-NS m such that
A3: <>* f = g & x = y & diff(<>* f, x) = diff(g,y)
by A2,PDIFF_1:def 8;
reconsider DF = diff(g,y) as
Lipschitzian LinearOperator of REAL-NS m,REAL-NS 1
by LOPBAN_1:def 9;
A4: dom(diff(<>* f,x))
= dom DF by A3
.= the carrier of REAL-NS m by FUNCT_2:def 1;
A5: the carrier of REAL-NS m = REAL m by REAL_NS1:def 4;
reconsider u1 = u as Point of REAL-NS m by REAL_NS1:def 4;
thus diff(f,x).(a * u)
= (proj(1,1) * diff(<>* f, x)).(a * u) by PDIFF_7:def 2
.= proj(1,1).(diff(<>* f,x).(a * u)) by A4,A5,FUNCT_1:13
.= proj(1,1).(DF.(a * u1)) by REAL_NS1:3,A3
.= proj(1,1).(a * DF.u1) by LOPBAN_1:def 5
.= a * proj(1,1).(DF.u1) by PDIFF_1:4
.= a * (proj(1,1) * diff(<>* f,x)).u by A3,A4,FUNCT_1:13
.= a * diff(f,x).u by PDIFF_7:def 2;
end;
theorem Th25:
for m be non zero Nat
for f be PartFunc of REAL m,REAL
for x be Element of REAL m
st f is_differentiable_in x
holds
for s be FinSequence of REAL m,
t be FinSequence of REAL
st dom s = dom t
& for i be Nat st i in dom s
holds t.i = diff(f,x).(s.i)
holds diff(f,x).(Sum s) = Sum t
proof
let m be non zero Nat;
let f be PartFunc of REAL m,REAL;
let x be Element of REAL m;
assume
A1: f is_differentiable_in x;
defpred P[Nat] means
for s be FinSequence of REAL m,
t be FinSequence of REAL
st len s = $1 & dom s = dom t
& for i be Nat st i in dom s
holds t.i = diff(f,x).(s.i)
holds diff(f,x).(Sum s) = Sum t;
A2: P[0]
proof
let s be FinSequence of REAL m,
t be FinSequence of REAL;
assume
A3: len s = 0 & dom s =dom t
& for i be Nat st i in dom s
holds t.i = diff(f,x).(s.i); then
Sum s = 0*m by EUCLID_7:def 11;
then
A4: diff(f,x).(Sum s)
= diff(f,x).(0 * (Sum s)) by EUCLID_4:3
.= 0 * diff(f,x).(Sum s) by A1,Th24
.= 0;
dom t = Seg len s by A3,FINSEQ_1:def 3;
then t = <*>REAL by A3;
hence thesis by A4,RVSUM_1:72;
end;
A5: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A6: P[n];
let s be FinSequence of REAL m,
t be FinSequence of REAL;
assume
A7: len s = n+1 & dom s = dom t
& for i be Nat st i in dom s
holds t.i = diff(f,x).(s.i);
reconsider sn = s | n as FinSequence of REAL m;
reconsider tn = t | n as FinSequence of REAL;
A8: n <= n + 1 by NAT_1:11;
A9: len sn = n by A7,FINSEQ_1:59,NAT_1:11;
dom t = Seg len s by FINSEQ_1:def 3,A7;
then
A10: len t = n+1 by A7,FINSEQ_1:def 3;
then len tn = n by FINSEQ_1:59,NAT_1:11;
then
A11: dom tn
= Seg n by FINSEQ_1:def 3
.= dom sn by A9,FINSEQ_1:def 3;
A12: for i be Nat st i in dom sn
holds tn.i = diff(f,x).(sn.i)
proof
let i be Nat;
assume i in dom sn;
then
A13: i in Seg n by A9,FINSEQ_1:def 3;
then i in Seg(n+1) by A8,FINSEQ_1:5,TARSKI:def 3;
then i in dom s by A7,FINSEQ_1:def 3;
then
A14: t.i = diff(f,x).(s.i) by A7;
t.i = tn.i by A13,FUNCT_1:49;
hence thesis by A13,A14,FUNCT_1:49;
end;
A15: s = sn ^ <*s.(n+1)*> by A7,FINSEQ_3:55;
A16: t = tn ^ <*t.(n+1)*> by A10,FINSEQ_3:55;
n+1 in Seg(n+1) by FINSEQ_1:4;
then
A17: n+1 in dom s by A7,FINSEQ_1:def 3;
then s.(n+1) in rng s by FUNCT_1:3;
then reconsider sn1 = s.(n+1) as Element of REAL m;
t.(n+1) in rng t by A7,A17,FUNCT_1:3;
then reconsider tn1 = t.(n+1) as Element of REAL;
thus diff(f,x).(Sum s)
= diff(f,x).(Sum sn + sn1) by A15,Th3
.= diff(f,x).(Sum sn) + diff(f,x).sn1 by A1,Th23
.= Sum tn + diff(f,x).sn1 by A6,A9,A11,A12
.= Sum tn + tn1 by A7,A17
.= Sum t by A16,RVSUM_1:74;
end;
A18: for n be Nat holds P[n] from NAT_1:sch 2(A2,A5);
let s be FinSequence of REAL m,
t be FinSequence of REAL;
assume
A19: dom s = dom t
& for i be Nat st i in dom s
holds t.i = diff(f,x).(s.i);
len s is Nat & len s = len s;
hence diff(f,x).(Sum s) = Sum t by A18,A19;
end;
theorem Th26:
for m be non zero Nat
for f be PartFunc of REAL m,REAL
for x be Element of REAL m
st f is_differentiable_in x
holds
for dx be Element of REAL m
ex dy be FinSequence of REAL
st dom dy = Seg m
& ( for i be Nat st 1 <= i <= m
holds dy.i = proj(i,m).dx * partdiff(f,x,i) )
& diff(f,x).dx = Sum dy
proof
let m be non zero Nat;
let f be PartFunc of (REAL m),REAL;
let x be Element of REAL m;
assume
A1: f is_differentiable_in x;
let dx be Element of REAL m;
consider s be FinSequence of REAL m such that
A2: dom s = Seg m
& ( for i be Nat st 1 <= i <= m
holds
ex ei be Element of REAL m
st ei = reproj(i,0* m) . 1
& s.i = proj(i,m).dx * ei )
& Sum s = dx by Th5;
deffunc F1(Nat) = In(diff(f,x).(s.$1), REAL);
consider dy be FinSequence of REAL such that
A3: len dy = m
& for i be Nat st i in dom dy
holds dy.i = F1(i) from FINSEQ_2:sch 1;
A4: dom dy = Seg m by A3,FINSEQ_1:def 3;
A5: for i be Nat st i in dom dy
holds dy.i = diff(f,x).(s.i)
proof
let i be Nat;
assume i in dom dy;
then dy.i = In(diff(f,x).(s.i), REAL) by A3;
hence dy.i = diff(f,x).(s.i);
end;
take dy;
thus dom dy = Seg m by A3,FINSEQ_1:def 3;
thus for i be Nat st 1 <= i <= m
holds dy.i = proj(i,m).dx * partdiff(f,x,i)
proof
let i be Nat;
assume
A6: 1 <= i <= m;
then
A7: i in dom dy by A4;
consider ei be Element of REAL m such that
A8: ei = reproj(i,0* m).1
& s.i = proj(i,m).dx * ei by A2,A6;
thus dy.i
= diff(f,x).(s.i) by A5,A7
.= proj(i,m).dx * diff(f,x).ei by A1,A8,Th24
.= proj(i,m).dx * partdiff(f,x,i) by A1,A6,A8,PDIFF_7:23;
end;
thus diff(f,x).dx = Sum dy by A1,A2,A4,A5,Th25;
end;
theorem
for m,n be non zero Element of NAT,
X be Subset of REAL-NS m,
f be 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 be Nat st 1 <= i <= m & 1 <= 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
let m,n be non zero Element of NAT,
X be Subset of REAL-NS m,
f be PartFunc of REAL-NS m,REAL-NS n;
assume
A1: X is open & X c= dom f;
hereby
assume
A2: f is_differentiable_on X & f `| X is_continuous_on X;
let i,j be Nat;
assume
A3: 1 <= i <= m;
assume
A4: 1 <= j <= n;
f is_partial_differentiable_on X,i
& f `partial| (X,i) is_continuous_on X by A1,A2,A3,PDIFF_8:22;
hence
Proj(j,n) * f is_partial_differentiable_on X,i
& (Proj(j,n) * f) `partial| (X,i) is_continuous_on X
by A1,A3,A4,PDIFF_8:20;
end;
assume
A5: for i,j be Nat st 1 <= i <= m & 1 <= j <= n
holds
Proj(j,n) * f is_partial_differentiable_on X,i
& (Proj(j,n) * f) `partial| (X,i) is_continuous_on X;
for i be Nat st 1 <= i <= m
holds
f is_partial_differentiable_on X,i
& f `partial| (X,i) is_continuous_on X
proof
let i be Nat;
assume
A6: 1 <= i <= m; then
for j be Nat st 1 <= j <= n
holds
Proj(j,n) * f is_partial_differentiable_on X,i
& (Proj(j,n) * f) `partial| (X,i) is_continuous_on X by A5;
hence
f is_partial_differentiable_on X,i
& f `partial| (X,i) is_continuous_on X by A1,A6,PDIFF_8:20;
end;
hence f is_differentiable_on X & f `| X is_continuous_on X
by A1,PDIFF_8:22;
end;
begin :: Jacobian matrix
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:
for i,j be Nat st i in Seg m & j in Seg n
holds it * (i,j) = partdiff(f,x,i,j);
existence
proof
defpred P1[Nat, Nat, object] means
$3 = partdiff(f,x,$1,$2);
A1: for i,j be Nat st [i,j] in [:Seg m,Seg n:]
holds ex y be Element of F_Real st P1[i,j,y]
proof
let i,j be Nat;
partdiff (f,x,i,j) in REAL by XREAL_0:def 1;
hence thesis;
end;
consider M be Matrix of m,n,F_Real such that
A2: for i,j be Nat st [i,j] in Indices M
holds P1[i,j,M * (i,j)] from MATRIX_0:sch 2(A1);
take M;
thus for i,j be Nat st i in Seg m & j in Seg n
holds M * (i,j) = partdiff(f,x,i,j)
proof
let i,j be Nat;
assume i in Seg m & j in Seg n;
then [i,j] in [:Seg m,Seg n:] by ZFMISC_1:87;
then [i,j] in Indices M by MATRIX_0:23;
hence thesis by A2;
end;
end;
uniqueness
proof
let M1,M2 be Matrix of m,n,F_Real;
assume
A3: for i,j be Nat st i in Seg m & j in Seg n
holds M1 * (i,j) = partdiff(f,x,i,j);
assume
A4: for i,j be Nat st i in Seg m & j in Seg n
holds M2 * (i,j) = partdiff(f,x,i,j);
A5: len M1 = m & width M1 = n
& Indices M1 = [:Seg m,Seg n:] by MATRIX_0:23;
A6: len M2 = m & width M2 = n
& Indices M2 = [:Seg m,Seg n:] by MATRIX_0:23;
for i,j be Nat st [i,j] in Indices(M1)
holds M1 * (i,j) = M2 * (i,j)
proof
let i,j be Nat;
assume [i,j] in Indices(M1);
then
A7: i in Seg m & j in Seg n by A5,ZFMISC_1:87;
then M1 * (i,j) = partdiff(f,x,i,j) by A3;
hence M1 * (i,j) = M2 * (i,j) by A4,A7;
end;
hence M1 = M2 by A5,A6,MATRIX_0:21;
end;
end;
theorem Th28:
for m,n be non zero Nat
for f be PartFunc of REAL m,REAL n
for x be Element of REAL m
st f is_differentiable_in x
holds diff(f,x) = Mx2Tran(Jacobian(f,x))
proof
let m,n be non zero Nat;
let f be PartFunc of REAL m,REAL n;
let x be Element of REAL m;
assume
A1: f is_differentiable_in x;
set M = Jacobian(f,x);
A2: the carrier of TOP-REAL n = REAL n
& the carrier of TOP-REAL m = REAL m by EUCLID:22;
for dx be Element of REAL m
holds diff(f,x).dx = (Mx2Tran(Jacobian(f,x))).dx
proof
let dx be Element of REAL m;
reconsider fdx = diff(f,x).dx as Element of REAL n;
reconsider Mdx = (Mx2Tran(Jacobian(f,x))).dx
as Element of REAL n by A2,FUNCT_2:5;
A3: len fdx = n by CARD_1:def 7;
A4: len Mdx = n by CARD_1:def 7;
for j be Nat st 1 <= j <= len fdx
holds fdx.j = Mdx.j
proof
let j be Nat;
assume
A5: 1 <= j <= len fdx; then
consider fj be PartFunc of REAL m,REAL such that
A6: fj = proj(j,n) * f
& fj is_differentiable_in x by A1,A3,Th19;
consider dy be FinSequence of REAL such that
A7: dom dy = Seg m
& ( for i be Nat st 1 <= i <= m
holds dy.i = proj(i,m).dx * partdiff(fj,x,i) )
& diff(fj,x).dx = Sum dy by A6,Th26;
A8: j in Seg n by A3,A5;
A9: for i be Nat st i in Seg m
holds M * (i,j) = partdiff(fj,x,i)
proof
let i be Nat;
assume i in Seg m;
hence M * (i,j)
= partdiff(f,x,i,j) by A8,Def1
.= partdiff(fj,x,i) by A6;
end;
A10: for i be Nat st 1 <= i <= m
holds dy.i = proj(i,m).dx * (M * (i,j))
proof
let i be Nat;
assume
A11: 1 <= i <= m; then
A12: i in Seg m;
thus dy.i
= proj(i,m).dx * partdiff(fj,x,i) by A7,A11
.= proj(i,m).dx * (M * (i,j)) by A9,A12;
end;
set dxM = LineVec2Mx(@ dx) * M;
A13: len M = m & width M = n
& Indices M = [:Seg m, Seg n:] by MATRIX_0:23;
A14: LineVec2Mx @dx = <* @dx *>
& LineVec2Mx @dx is Matrix of 1, len(@dx), F_Real
by MATRIX15:def 1;
A15: len(@dx)
= len dx by MATRTOP1:def 1
.= m by CARD_1:def 7;
then
A16: len(LineVec2Mx @dx) = 1
& width(LineVec2Mx @dx) = m
& Indices(LineVec2Mx @dx) = [:Seg 1, Seg m:] by MATRIX_0:23;
then
A17: len dxM = len(LineVec2Mx @dx)
& width dxM = width M
& for i, j be Nat st [i,j] in Indices dxM
holds dxM * (i,j) = Line(LineVec2Mx(@ dx),i) "*" (Col(M,j))
by A13,MATRIX_3:def 4;
A18: Mdx = Line(dxM,1) by MATRTOP1:def 3;
A19: j in Seg(width dxM) by A3,A5,A13,A17;
then
A20: Mdx.j = dxM * (1,j) by A18,MATRIX_0:def 7;
len dxM = 1 by A16,MATRIX_3:def 4,A13;
then dom dxM = Seg 1 by FINSEQ_1:def 3;
then 1 in dom dxM; then
[1,j] in Indices dxM by A19,ZFMISC_1:87; then
A22: Mdx.j = Line(LineVec2Mx(@ dx),1) "*" (Col(M,j))
by A13,A16,A20,MATRIX_3:def 4;
set u = mlt(Line(LineVec2Mx(@ dx),1), Col(M,j));
len(Line(LineVec2Mx(@ dx),1))
= width(LineVec2Mx(@ dx)) by MATRIX_0:def 7
.= m by A15,MATRIX_0:23;
then reconsider a = Line(LineVec2Mx(@ dx),1) as
Element of m -tuples_on the carrier of F_Real by FINSEQ_2:92;
len(Col(M,j))
= len M by MATRIX_0:def 8
.= m by MATRIX_0:23;
then reconsider b = Col(M,j) as
Element of m -tuples_on the carrier of F_Real by FINSEQ_2:92;
u = mlt(a,b);
then u in { s where s is Element of (the carrier of F_Real) *
: len s = m };
then
A23: ex u0 be Element of (the carrier of F_Real)*
st u0 = u & len u0 = m;
m is Element of NAT by ORDINAL1:def 12;
then
A24: len dy = m by A7,FINSEQ_1:def 3;
A25: for i be Nat st 1 <= i <= len dy holds dy.i = u.i
proof
let i be Nat;
assume
A26: 1 <= i <= len dy; then
A27: i in Seg m by A24;
reconsider s = proj(i,m).dx as Element of F_Real;
reconsider t = M * (i,j) as Element of F_Real;
1 in Seg 1;
then [1,i] in Indices(LineVec2Mx(@ dx)) by A16,A27,ZFMISC_1:87;
then
A28: ex p be FinSequence of (the carrier of F_Real)
st p = (LineVec2Mx(@ dx)).1
& LineVec2Mx(@ dx) * (1,i) = p.i by MATRIX_0:def 5;
(LineVec2Mx(@ dx)).1 = @dx by A14
.= dx by MATRTOP1:def 1; then
a.i = dx.i by A16,A27,A28,MATRIX_0:def 7;
then
A30: a.i = proj(i,m).dx by PDIFF_1:def 1;
i in dom M by A13,A27,FINSEQ_1:def 3; then
b.i = M * (i,j) by MATRIX_0:def 8; then
u.i = s*t by A27,A30,FVSUM_1:61
.= (proj(i,m).dx) * (M * (i,j));
hence thesis by A10,A24,A26;
end;
A33: dom(diff(f,x)) = REAL m by FUNCT_2:def 1;
diff(fj,x).dx
= (proj(j,n) * diff(f,x)).dx by A1,A3,A5,A6,Th20
.= proj(j,n).(diff(f,x).dx) by A33,FUNCT_1:13
.= fdx.j by PDIFF_1:def 1;
hence thesis by A7,A22,A23,A24,A25,FINSEQ_1:14;
end;
hence thesis by A4,FINSEQ_1:14,CARD_1:def 7;
end;
hence diff(f,x) = Mx2Tran(Jacobian(f,x)) by EUCLID:22;
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:
ex g be PartFunc of REAL m,REAL n,
y be Element of REAL m
st g = f & y = x
& it = Jacobian(g,y);
existence
proof
the carrier of REAL-NS m = REAL m
& the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
then
reconsider g = f as PartFunc of REAL m,REAL n;
reconsider y = x as Element of REAL m by REAL_NS1:def 4;
take Jacobian(g,y);
thus thesis;
end;
uniqueness;
end;
theorem Th29:
for m,n be non zero Element of NAT,
x be Point of REAL-NS m,
f be PartFunc of REAL-NS m,REAL-NS n
st f is_differentiable_in x
holds diff(f,x) = Mx2Tran(Jacobian(f,x))
proof
let m,n be non zero Element of NAT,
x be Point of REAL-NS m,
f be PartFunc of REAL-NS m,REAL-NS n;
assume
A1: f is_differentiable_in x;
consider g be PartFunc of REAL m,REAL n,
y be Element of REAL m such that
A2: g = f & y = x
& Jacobian(f,x) = Jacobian(g,y) by Def2;
A3: g is_differentiable_in y by A1,A2;
thus diff(f,x)
= diff(g,y) by A1,A2,PDIFF_1:21
.= Mx2Tran(Jacobian(f,x)) by A2,A3,Th28;
end;
begin
theorem Th30:
for m be non zero Element of NAT,
f be PartFunc of REAL-NS m, REAL-NS m,
x be Point of REAL-NS m
st f is_differentiable_in x
holds
diff(f,x) is invertible
iff
Jacobian(f,x) is invertible
proof
let m be non zero Element of NAT,
f be PartFunc of REAL-NS m, REAL-NS m,
x be Point of REAL-NS m;
assume f is_differentiable_in x;
then diff(f,x) = Mx2Tran(Jacobian(f,x)) by Th29;
hence thesis by Th12;
end;
theorem Th31:
for m be non zero Element of NAT,
f be PartFunc of REAL-NS m, REAL-NS m,
x be 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
let m be non zero Element of NAT,
f be PartFunc of REAL-NS m, REAL-NS m,
x be Point of REAL-NS m;
Det(Jacobian(f,x)) is unital iff Det(Jacobian(f,x)) is non zero;
then A1: Det(Jacobian(f,x)) is unital iff Det(Jacobian(f,x)) <> 0.F_Real
by STRUCT_0:def 12;
assume f is_differentiable_in x;
then
diff(f,x) is invertible
iff
Jacobian(f,x) is invertible by Th30;
hence thesis by A1,LAPLACE:34;
end;
begin :: Implicit and inverse function theorems on Euclidean spaces
theorem
for l,m,n be non zero Element of NAT,
Z be Subset of [:REAL-NS l,REAL-NS m:],
f be PartFunc of [:REAL-NS l,REAL-NS m:], REAL-NS n,
a be Point of REAL-NS l,
b be Point of REAL-NS m,
c be Point of REAL-NS n,
z be 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 be Real
st 0 < r1 & 0 < r2
& [:Ball(a,r1),cl_Ball(b,r2):] c= Z
& ( for x be Point of REAL-NS l st x in Ball(a,r1) holds
ex y be Point of REAL-NS m
st y in Ball(b,r2) & f.(x,y) = c )
& ( for x be Point of REAL-NS l st x in Ball(a,r1) holds
for y1,y2 be 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 be 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 be 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 be Point of REAL-NS l,
z be 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 be Point of REAL-NS l,
z be 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 be PartFunc of REAL-NS l,REAL-NS m
st dom g1 = Ball(a,r1)
& rng g1 c= Ball(b,r2)
& ( for x be 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 be 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
for l,m be non zero Element of NAT,
Z be Subset of [:REAL-NS l,REAL-NS m:],
f be PartFunc of [:REAL-NS l,REAL-NS m:], REAL-NS m,
a be Point of REAL-NS l,
b,c be Point of REAL-NS m,
z be 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 be Real
st 0 < r1 & 0 < r2
& [:Ball(a,r1),cl_Ball(b,r2):] c= Z
& ( for x be Point of REAL-NS l st x in Ball(a,r1) holds
ex y be Point of REAL-NS m
st y in Ball(b,r2) & f.(x,y) = c )
& ( for x be Point of REAL-NS l st x in Ball(a,r1) holds
for y1,y2 be 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 be 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 be 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 be Point of REAL-NS l,
z be 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 be Point of REAL-NS l,
z be 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 be PartFunc of REAL-NS l,REAL-NS m
st dom g1 = Ball(a,r1)
& rng g1 c= Ball(b,r2)
& ( for x be 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 be Point of REAL-NS l st x in Ball(a,r1)
holds f.(x,g2.x) = c )
holds g1 = g2 )
proof
let l,m be non zero Element of NAT,
Z be Subset of [:REAL-NS l,REAL-NS m:],
f be PartFunc of [:REAL-NS l,REAL-NS m:], REAL-NS m,
a be Point of REAL-NS l,
b,c be Point of REAL-NS m,
z be Point of [:REAL-NS l,REAL-NS m:];
assume
A1: 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; then
A2: f is_differentiable_in z;
A3: partdiff`2 (f,z)
= diff(f * (reproj2 z),z`2) by NDIFF_7:def 7;
f * (reproj2 z) is_differentiable_in z`2 by A2,NDIFF_7:def 5,NDIFF_9:14;
then diff (f * (reproj2 z),z`2) is invertible by A1,Th31;
hence thesis by A1,A3,NDIFF_9:21;
end;
theorem
for m be non zero Element of NAT,
Z be Subset of REAL-NS m,
f be PartFunc of REAL-NS m,REAL-NS m,
a be Point of REAL-NS m,
b be 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 be Subset of REAL-NS m,B be Subset of REAL-NS m,
g be 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 be Point of REAL-NS m st y in B
holds diff(f,g/.y) is invertible )
& ( for y be Point of REAL-NS m st y in B
holds diff(g,y) = Inv diff(f,g/.y) )
proof
let m be non zero Element of NAT,
Z be Subset of REAL-NS m,
f be PartFunc of REAL-NS m,REAL-NS m,
a be Point of REAL-NS m,
b be Point of REAL-NS m;
assume
A1: 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; then
f is_differentiable_in a;
then diff(f,a) is invertible by A1,Th31;
hence thesis by A1,NDIFF10:17;
end;