:: Higher Order Partial Differentiable Functions
:: by Kazuhisa Nakasho and Yasunari Shidama
::
:: Received December 2, 2025
:: Copyright (c) 2025-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 4.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/4.0/.
environ
vocabularies NDIFF14, NUMBERS, REAL_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1,
NAT_1, FDIFF_1, SUBSET_1, RELAT_1, LOPBAN_1, RCOMP_1, TARSKI, ARYTM_3,
ARYTM_1, CARD_1, XXREAL_0, XBOOLE_0, CFCONT_1, FUNCT_7, VALUED_1,
RSSPACE, PRVECT_2, FINSEQ_1, ORDINAL4, PDIFF_1, CARD_3, PDIFF_9,
STRUCT_0, ZFMISC_1, RFINSEQ, FUNCT_2, SUPINF_2, FCONT_1, FUNCOP_1,
RLVECT_1, ALGSTR_0, MONOID_0, LOPBAN_8, MSSUBFAM, NDIFF_6, RLSUB_1,
FUNCSDOM, XXREAL_2, SEQ_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, FUNCT_3, FUNCOP_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, XXREAL_2, XREAL_0, NAT_1, FINSEQ_1, RFINSEQ, STRUCT_0,
ALGSTR_0, MONOID_0, PRE_TOPC, RLVECT_1, VECTSP_1, RLSUB_1, NORMSP_0,
NORMSP_1, VFUNCT_1, NDIFF_6, RSSPACE, SEQ_4, LOPBAN_1, NFCONT_1, NDIFF_1,
NDIFF_2, PRVECT_2, PRVECT_3, NDIFF_5, LOPBAN_8, LOPBAN_9;
constructors VFUNCT_1, RELSET_1, NDIFF_6, LOPBAN13, NDIFF_1, NDIFF_5, RLSUB_1,
SEQ_4, RSSPACE, FUNCT_3, MONOID_0, NDIFF_2, LOPBAN_9, RFINSEQ;
registrations RELSET_1, STRUCT_0, XREAL_0, NAT_1, INT_1, LOPBAN_1, RELAT_1,
XBOOLE_0, ORDINAL1, XXREAL_0, FINSEQ_1, CARD_1, PRVECT_2, FUNCT_1,
NORMSP_3, MEMBERED, RLVECT_1, MONOID_0, LOPBAN_9;
requirements SUBSET, REAL, BOOLE, ARITHM, NUMERALS;
definitions FUNCT_1;
equalities LOPBAN_1, PRVECT_3, STRUCT_0, BINOP_1, NDIFF_6, NDIFF_2, NORMSP_0;
expansions VECTSP_1, NDIFF_1, MONOID_0, NDIFF_6, RLSUB_1, FUNCT_1, XXREAL_2;
theorems XBOOLE_1, RELAT_1, FUNCT_1, FINSEQ_1, PRVECT_2, FINSEQ_3, RLSUB_1,
SUBSET_1, NAT_1, INT_1, VFUNCT_1, PARTFUN1, XXREAL_0, ORDINAL1, XREAL_1,
FUNCOP_1, ZFMISC_1, RELSET_1, NDIFF_1, NDIFF_5, NDIFF_6, FUNCT_2,
FUNCT_3, NDIFF13, LOPBAN_1, TARSKI, RLVECT_1, RFINSEQ, FINSEQ_5, SEQ_4,
NFCONT_1, RSSPACE, FINSEQ_2, XXREAL_2;
schemes NAT_1, FINSEQ_1, RECDEF_1, FUNCT_2;
begin :: Vector Space of Continuously Differentiable Functions
theorem
for S,T be RealNormSpace,
f be PartFunc of S,T,
Z be Subset of S
holds
f|Z is_differentiable_on Z iff f is_differentiable_on Z
proof
let S,T be RealNormSpace,
f be PartFunc of S,T,
Z be Subset of S;
hereby
assume A1: f|Z is_differentiable_on Z;
dom(f|Z) c= dom f by RELAT_1:60;
hence f is_differentiable_on Z by A1,XBOOLE_1:1;
end;
thus f is_differentiable_on Z implies f|Z is_differentiable_on Z
by RELAT_1:62;
end;
theorem Th2:
for L,M be RealNormSpace,
s be Point of L,
w be FinSequence of M,
X be FinSequence of R_NormSpace_of_BoundedLinearOperators(L,M)
st dom w = dom X & for i be Nat st i in dom w holds w.i = (X/.i).s
holds Sum w = (Sum X).s
proof
let L,M be RealNormSpace, s be Point of L;
set LM = R_NormSpace_of_BoundedLinearOperators(L,M);
defpred P[Nat] means
for w be FinSequence of M,
X be FinSequence of R_NormSpace_of_BoundedLinearOperators(L,M)
st len w = $1 & dom w = dom X
& for i be Nat st i in dom w holds w.i = (X/.i).s
holds Sum w = (Sum X).s;
A1: P[0]
proof
let w be FinSequence of M,
X be FinSequence of R_NormSpace_of_BoundedLinearOperators(L,M);
assume A2: len w = 0 & dom w = dom X
& for i be Nat st i in dom w holds w.i = (X/.i).s;
A3: w = <*> the carrier of M by A2;
then A4: Sum w = 0.M by RLVECT_1:43;
X = <*> the carrier of LM by A2,A3;
then Sum X = 0.LM by RLVECT_1:43
.= (the carrier of L) --> 0.M
by LOPBAN_1:31;
hence thesis by A4,FUNCOP_1:7;
end;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6: P[k];
let w be FinSequence of M,
X be FinSequence of R_NormSpace_of_BoundedLinearOperators(L,M);
assume A7: len w = k+1 & dom w = dom X
& for i be Nat st i in dom w holds w.i = (X/.i).s;
set w1 = w | k;
set X1 = X | k;
A9: dom X = Seg (k+1) by A7,FINSEQ_1:def 3;
then A10: len X = k+1 by FINSEQ_1:def 3; then
A11: len X1 = k by FINSEQ_1:59,NAT_1:11;
A12: X1 = X | Seg k by FINSEQ_1:def 16;
then A13: X1 = X | dom X1 by A11,FINSEQ_1:def 3;
X/.len X = X.(len X) by A9,A10,FINSEQ_1:4,PARTFUN1:def 6;
then A14: Sum X = Sum X1 + X/.len X by A10,A11,A13,RLVECT_1:38;
A15: dom w = Seg (k+1) by A7,FINSEQ_1:def 3;
A17: len w1 = k by A7,FINSEQ_1:59,NAT_1:11;
A18: w1 = w | Seg k by FINSEQ_1:def 16;
then A19: w1 = w | dom w1 by A17,FINSEQ_1:def 3;
w/.len w = w.(len w) by A15,A7,FINSEQ_1:4,PARTFUN1:def 6;
then A20: Sum w = Sum w1 + w/.len w
by A7,A17,A19,RLVECT_1:38;
A21: dom w1 = Seg k by A17,FINSEQ_1:def 3
.= dom X1 by A11,FINSEQ_1:def 3;
for i be Nat st i in dom w1 holds w1.i = (X1/.i).s
proof
let i be Nat;
assume A22: i in dom w1;
then A23: i in Seg len w1 by FINSEQ_1:def 3;
Seg len w1 c= Seg len w by A7,A17,FINSEQ_1:5,NAT_1:11;
then A24: Seg len w1 c= dom w by FINSEQ_1:def 3;
A25: w1.i = w.i by FUNCT_1:49,A23,A17,A18
.= (X/.i).s by A7,A23,A24;
X1/.i = X1.i by A21,A22,PARTFUN1:def 6
.= X.i by A12,A17,A23,FUNCT_1:49
.= X/.i by A7,A23,A24,PARTFUN1:def 6;
hence w1.i = (X1/.i).s by A25;
end;
then A26: Sum w1 = (Sum X1).s by A6,A21,A17;
1 <= len w by A7,NAT_1:11;
then A27: len w in dom w by FINSEQ_3:25;
then w.(len w) = (X/.(len w)).s by A7;
then w/.(len w) = (X/.(len w)).s by A27,PARTFUN1:def 6;
hence Sum w = (Sum X).s by A7,A10,A14,A20,A26,LOPBAN_1:35;
end;
A29: for k be Nat holds P[k] from NAT_1:sch 2(A1,A5);
let w be FinSequence of M,
X be FinSequence of R_NormSpace_of_BoundedLinearOperators(L,M);
assume A30: dom w = dom X & for i be Nat st i in dom w holds w.i = (X/.i).s;
len w = len w;
hence Sum w = (Sum X).s by A29,A30;
end;
registration
let X be RealNormSpace;
cluster non empty open for Subset of X;
correctness
proof
take G = [#]X;
thus thesis;
end;
end;
theorem Th3:
for X,Y be RealNormSpace,
Z be non empty Subset of X,
v,u be VECTOR of RealVectSpace(Z, Y),
f,g be PartFunc of X,Y,
a be Real
st dom f = Z & dom g = Z & v = f & u = g
holds v+u = f+g & a*v = a(#)f
proof
let X, Y be RealNormSpace,
Z be non empty Subset of X,
v,u be VECTOR of RealVectSpace(Z, Y),
f,g be PartFunc of X,Y,
a be Real;
assume that
A1: dom f = Z and
A2: dom g = Z and
A3: v = f and
A4: u = g;
A5: dom (f+g) = dom f /\ dom g by VFUNCT_1:def 1
.= Z by A1,A2;
rng (f+g) c= the carrier of Y;
then f+g is Function of Z,the carrier of Y by A5,FUNCT_2:2;
then reconsider vu = f+g as Element of Funcs (Z, the carrier of Y)
by FUNCT_2:8;
for x being Element of Z holds vu.x = v.x+u.x
proof
let x be Element of Z;
A6: f/.x = v.x by A1,A3,PARTFUN1:def 6;
A7: g/.x = u.x by A2,A4,PARTFUN1:def 6;
thus vu.x = (f+g)/.x by A5,PARTFUN1:def 6
.= v.x + u.x by A5,A6,A7,VFUNCT_1:def 1;
end;
hence v+u = f + g by LOPBAN_1:11;
A8: dom (a(#)f) = Z by A1,VFUNCT_1:def 4;
rng (a(#)f) c= the carrier of Y;
then a(#)f is Function of Z,the carrier of Y by A8,FUNCT_2:2;
then reconsider av = a(#)f as Element of Funcs (Z, the carrier of Y)
by FUNCT_2:8;
for x being Element of Z holds av.x = a*v.x
proof
let x be Element of Z;
A9: f/.x = v.x by A1,A3,PARTFUN1:def 6;
thus av.x = (a(#)f)/.x by A8,PARTFUN1:def 6
.= a*v.x by A8,A9,VFUNCT_1:def 4;
end;
hence a*v = a(#)f by LOPBAN_1:12;
end;
definition
let X, Y be RealNormSpace, Z be non empty open Subset of X, n be Nat;
func Continuously_differentiable_Functions(Z,Y,n)
-> Subset of RealVectSpace(Z, Y) equals
{f where f is PartFunc of X,Y:
dom f = Z & f is_differentiable_on n,Z & diff(f,n,Z) is_continuous_on Z};
correctness
proof
set S = {f where f is PartFunc of X,Y:
dom f = Z & f is_differentiable_on n,Z
& diff(f,n,Z) is_continuous_on Z};
for x be object st x in S holds x in Funcs(Z,the carrier of Y)
proof
let x be object;
assume x in S;
then consider f be PartFunc of X,Y such that
A1: x = f & dom f = Z & f is_differentiable_on n,Z
& diff(f,n,Z) is_continuous_on Z;
rng f c= the carrier of Y;
then f is Function of Z,the carrier of Y by A1,FUNCT_2:2;
hence x in Funcs(Z,the carrier of Y) by FUNCT_2:8,A1;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem
for X,Y be RealNormSpace,
Z be non empty open Subset of X,
n be Nat,
f be PartFunc of X,Y
holds
f in Continuously_differentiable_Functions(Z,Y,n)
iff
dom f = Z & f is_differentiable_on n,Z
& diff(f,n,Z) is_continuous_on Z
proof
let X, Y be RealNormSpace,
Z be non empty open Subset of X,
n be Nat,
f be PartFunc of X,Y;
hereby
assume f in Continuously_differentiable_Functions(Z,Y,n);
then ex f1 be PartFunc of X,Y st f = f1
& dom f1 = Z & f1 is_differentiable_on n,Z
& diff(f1,n,Z) is_continuous_on Z;
hence dom f = Z & f is_differentiable_on n,Z
& diff(f,n,Z) is_continuous_on Z;
end;
assume dom f = Z & f is_differentiable_on n,Z
& diff(f,n,Z) is_continuous_on Z;
hence f in Continuously_differentiable_Functions(Z,Y,n);
end;
registration
let X, Y be RealNormSpace,
Z be non empty open Subset of X,
n be Nat;
cluster Continuously_differentiable_Functions(Z,Y,n) -> non empty functional;
coherence
proof
set Li = the Point of Y;
A1: dom (Z --> Li) = Z & rng (Z --> Li) c= {Li} by FUNCOP_1:13;
reconsider L = Z --> Li as PartFunc of X,Y by RELSET_1:4,A1;
A2: L is_differentiable_on n,Z by NDIFF13:49;
L is_differentiable_on n+1,Z by NDIFF13:49;
then diff(L,n,Z) is_continuous_on Z by NDIFF_1:45,NDIFF_6:14;
then L in Continuously_differentiable_Functions(Z,Y,n) by A1,A2;
hence Continuously_differentiable_Functions(Z,Y,n) is non empty;
let x be object;
assume x in Continuously_differentiable_Functions(Z,Y,n);
hence thesis;
end;
end;
theorem Th5:
for X,Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat
holds Continuously_differentiable_Functions(Z,Y,n) is linearly-closed
proof
let X,Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat;
set W = Continuously_differentiable_Functions(Z,Y,n);
A0: n <> {};
then A1: 1 <= n by NAT_1:14;
A2: for v,u be VECTOR of RealVectSpace(Z, Y) st v in W & u in W
holds v + u in W
proof
let v,u be VECTOR of RealVectSpace(Z,Y) such that
A3: v in W and
A4: u in W;
consider f be PartFunc of X,Y such that
A5: f = v & dom f = Z & f is_differentiable_on n,Z
& diff(f,n,Z) is_continuous_on Z by A3;
consider g be PartFunc of X,Y such that
A6: g = u & dom g = Z & g is_differentiable_on n,Z
& diff(g,n,Z) is_continuous_on Z by A4;
A7: dom (f+g) = dom f /\ dom g by VFUNCT_1:def 1
.= Z by A5,A6;
A8: v+u = f + g by A5,A6,Th3;
A9: f+g is_differentiable_on n,Z by A0,A5,A6,NAT_1:14,NDIFF_6:21;
diff(f+g,n,Z) = diff(f,n,Z) + diff(g,n,Z) by A1,A5,A6,NDIFF_6:20;
then diff(f+g,n,Z) is_continuous_on Z by A5,A6,NFCONT_1:25;
hence v+u in W by A7,A8,A9;
end;
for a be Real
for v be VECTOR of RealVectSpace(Z,Y) st v in W holds a * v in W
proof
let a be Real;
let v be VECTOR of RealVectSpace(Z,Y) such that
A10: v in W;
consider f be PartFunc of X,Y such that
A11: f = v & dom f = Z & f is_differentiable_on n,Z
& diff(f,n,Z) is_continuous_on Z by A10;
A12: dom (a(#)f) = Z by A11,VFUNCT_1:def 4;
A13: a*v = a(#)f by Th3,A11;
A14: a(#)f is_differentiable_on n,Z by A0,A11,NAT_1:14,NDIFF_6:25;
diff(a(#)f,n,Z) = a(#)diff(f,n,Z) by A1,A11,NDIFF_6:24;
then diff(a(#)f,n,Z) is_continuous_on Z by NFCONT_1:27,A11;
hence a*v in W by A12,A13,A14;
end;
hence thesis by A2;
end;
theorem
for X,Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat
holds
RLSStruct(# Continuously_differentiable_Functions(Z,Y,n),
Zero_(Continuously_differentiable_Functions(Z,Y,n),
RealVectSpace(Z,Y)),
Add_(Continuously_differentiable_Functions(Z,Y,n),
RealVectSpace(Z,Y)),
Mult_(Continuously_differentiable_Functions(Z,Y,n),
RealVectSpace(Z,Y)) #)
is Subspace of RealVectSpace(Z,Y) by Th5,RSSPACE:11;
registration
let X,Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat;
cluster RLSStruct(# Continuously_differentiable_Functions(Z,Y,n),
Zero_(Continuously_differentiable_Functions(Z,Y,n),
RealVectSpace(Z,Y)),
Add_(Continuously_differentiable_Functions(Z,Y,n),
RealVectSpace(Z,Y)),
Mult_(Continuously_differentiable_Functions(Z,Y,n),
RealVectSpace(Z,Y)) #)
-> Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence by Th5,RSSPACE:11;
end;
definition
let X,Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat;
func RVectSp_Continuously_differentiable_Funcs(Z,Y,n)
-> strict RealLinearSpace equals
RLSStruct(# Continuously_differentiable_Functions(Z,Y,n),
Zero_(Continuously_differentiable_Functions(Z,Y,n),
RealVectSpace(Z,Y)),
Add_(Continuously_differentiable_Functions(Z,Y,n),
RealVectSpace(Z,Y)),
Mult_(Continuously_differentiable_Functions(Z,Y,n),
RealVectSpace(Z,Y)) #);
coherence;
end;
registration
let X,Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat;
cluster RVectSp_Continuously_differentiable_Funcs(Z,Y,n)
-> constituted-Functions;
coherence;
end;
theorem Th7:
for X,Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat,
v,u be VECTOR of RVectSp_Continuously_differentiable_Funcs(Z,Y,n),
f,g be PartFunc of X,Y,
a be Real
st dom f = Z & dom g = Z & v = f & u = g
holds v+u = f+g & a*v = a(#)f
proof
let X, Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat,
v,u be VECTOR of RVectSp_Continuously_differentiable_Funcs(Z,Y,n),
f,g be PartFunc of X,Y,
a be Real;
assume A1: dom f = Z & dom g = Z & v = f & u = g;
A2: RVectSp_Continuously_differentiable_Funcs(Z,Y,n)
is Subspace of RealVectSpace(Z,Y) by Th5,RSSPACE:11;
reconsider v1=v,u1=u as VECTOR of RealVectSpace(Z, Y)
by TARSKI:def 3;
thus v+u = v1+u1 by RLSUB_1:13,A2
.= f+g by Th3,A1;
thus a*v = a*v1 by RLSUB_1:14,A2
.= a(#)f by Th3,A1;
end;
definition
let X, Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat;
let f be Element of RVectSp_Continuously_differentiable_Funcs(Z,Y,n);
let v be Element of Z;
redefine func f.v -> VECTOR of Y; :: redefines . (FUNCT_1, definition)
coherence
proof
f in Continuously_differentiable_Functions(Z,Y,n);
then consider g be PartFunc of X,Y such that
A1: f = g & dom g = Z & g is_differentiable_on n,Z
& diff(g,n,Z) is_continuous_on Z;
f.v = g/.v by A1,PARTFUN1:def 6;
hence thesis;
end;
end;
theorem
for X,Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat
holds for f,g,h be VECTOR of RVectSp_Continuously_differentiable_Funcs(Z,Y,n)
holds h = f+g iff for x be Element of Z holds h.x = f.x + g.x
proof
let X, Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat;
let f,g,h be VECTOR of RVectSp_Continuously_differentiable_Funcs(Z,Y,n);
A1: RVectSp_Continuously_differentiable_Funcs(Z,Y,n)
is Subspace of RealVectSpace(Z,Y) by Th5,RSSPACE:11;
then reconsider f1 = f as VECTOR of RealVectSpace(Z,Y) by RLSUB_1:10;
reconsider h1 = h as VECTOR of RealVectSpace(Z,Y) by A1, RLSUB_1:10;
reconsider g1 = g as VECTOR of RealVectSpace(Z,Y) by A1, RLSUB_1:10;
A2: now
assume A3: h = f+g;
let x be Element of Z;
h1 = f1+g1 by A1,A3,RLSUB_1:13;
hence h.x = f.x+g.x by LOPBAN_1:11;
end;
now
assume for x be Element of Z holds h.x = f.x+g.x;
then h1 = f1+g1 by LOPBAN_1:11;
hence h = f+g by A1,RLSUB_1:13;
end;
hence thesis by A2;
end;
theorem
for X, Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat
holds for f,h be VECTOR of RVectSp_Continuously_differentiable_Funcs(Z,Y,n)
for a be Real holds h = a*f iff
for x be Element of Z holds h.x = a * f.x
proof
let X, Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat;
let f,h be VECTOR of RVectSp_Continuously_differentiable_Funcs(Z,Y,n);
let a be Real;
A1: RVectSp_Continuously_differentiable_Funcs(Z,Y,n)
is Subspace of RealVectSpace(Z,Y) by Th5,RSSPACE:11;
then reconsider f1 = f as VECTOR of RealVectSpace(Z,Y) by RLSUB_1:10;
reconsider h1 = h as VECTOR of RealVectSpace(Z,Y) by A1,RLSUB_1:10;
A2: now
assume A3: h = a*f;
let x be Element of Z;
h1 = a*f1 by A1,A3,RLSUB_1:14;
hence h.x = a*f.x by LOPBAN_1:12;
end;
now
assume for x be Element of Z holds h.x = a*f.x;
then h1 = a*f1 by LOPBAN_1:12;
hence h = a*f by A1,RLSUB_1:14;
end;
hence thesis by A2;
end;
theorem Th10:
for X,Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat
holds
0.RVectSp_Continuously_differentiable_Funcs(Z,Y,n) = Z --> 0.Y
proof
let X,Y be RealNormSpace,
Z be non empty open Subset of X,
n be non empty Nat;
A1: 0.RealVectSpace(Z,Y) = Z --> 0.Y;
RVectSp_Continuously_differentiable_Funcs(Z,Y,n)
is Subspace of RealVectSpace(Z,Y) by Th5,RSSPACE:11;
hence thesis by A1,RLSUB_1:11;
end;
theorem Th11:
for G0,F be RealNormSpace,
X be non empty open Subset of G0,
n be non empty Nat,
x be Point of G0
st x in X
holds
for W0 be FinSequence of the carrier of
RVectSp_Continuously_differentiable_Funcs(X,
R_NormSpace_of_BoundedLinearOperators(G0,F),n),
Wx be FinSequence of R_NormSpace_of_BoundedLinearOperators(G0,F)
st dom Wx = dom W0
& for i be Nat st i in dom Wx
holds
ex Wi be PartFunc of G0,R_NormSpace_of_BoundedLinearOperators(G0,F)
st Wi = W0.i & Wx/.i = Wi/.x
holds Sum Wx = (Sum W0).x
proof
let G0,F be RealNormSpace,
X be non empty open Subset of G0,
n be non empty Nat,
x be Point of G0;
assume A1: x in X;
set G0F = R_NormSpace_of_BoundedLinearOperators(G0,F);
set XG0Fn = RVectSp_Continuously_differentiable_Funcs(X,G0F,n);
defpred P[Nat] means
for W0 being FinSequence of the carrier of XG0Fn,
Wx be FinSequence of G0F
st len Wx = $1 & dom Wx = dom W0
& for i be Nat st i in dom Wx
ex Wi be PartFunc of G0, G0F
st Wi = W0.i & Wx/.i = Wi/.x
holds Sum Wx = (Sum W0).x;
A2: P[0]
proof
let W0 be FinSequence of the carrier of XG0Fn,
Wx be FinSequence of G0F;
assume A3: len Wx = 0 & dom Wx = dom W0
& for i be Nat st i in dom Wx
ex Wi be PartFunc of G0, G0F
st Wi = W0.i & Wx/.i = Wi/.x;
A4: Wx = <*> the carrier of G0F by A3;
then A5: Sum Wx = 0.G0F by RLVECT_1:43;
W0 = <*> the carrier of XG0Fn by A3,A4;
then Sum W0 = 0.XG0Fn by RLVECT_1:43
.= X --> 0.G0F by Th10;
hence thesis by A1,A5,FUNCOP_1:7;
end;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A7: P[k];
let W0 be FinSequence of the carrier of XG0Fn,
Wx be FinSequence of G0F;
assume A8: len Wx = k+1 & dom Wx = dom W0
& for i be Nat st i in dom Wx
ex Wi be PartFunc of G0, G0F
st Wi = W0.i & Wx/.i = Wi/.x;
set Wx1 = Wx | k;
set W01 = W0 | k;
A10: dom W0 = Seg (k+1) by A8,FINSEQ_1:def 3;
then A11: len W0 = k+1 by FINSEQ_1:def 3; then
A12: len W01 = k by FINSEQ_1:59,NAT_1:11;
A13: W01 = W0 | Seg k by FINSEQ_1:def 16;
then A14: W01 = W0 | dom W01 by A12,FINSEQ_1:def 3;
W0/.len W0 = W0.(len W0) by A10,A11,FINSEQ_1:4,PARTFUN1:def 6;
then A15: Sum W0 = Sum W01 + W0/.len W0 by A11,A12,A14,RLVECT_1:38;
A16: dom Wx = Seg (k+1) by A8,FINSEQ_1:def 3;
A18: len Wx1 = k by A8,FINSEQ_1:59,NAT_1:11;
A19: Wx1 = Wx | Seg k by FINSEQ_1:def 16;
then A20: Wx1 = Wx | dom Wx1 by A18,FINSEQ_1:def 3;
Wx/.len Wx = Wx.(len Wx) by A8,A16,FINSEQ_1:4,PARTFUN1:def 6;
then A22: Sum Wx = Sum Wx1 + Wx/.len Wx by A8,A18,A20,RLVECT_1:38;
A23: dom Wx1 = Seg k by A18,FINSEQ_1:def 3
.= dom W01 by A12,FINSEQ_1:def 3;
for i be Nat st i in dom Wx1
holds ex Wi be PartFunc of G0, G0F st Wi = W01.i & Wx1/.i = Wi/.x
proof
let i be Nat;
assume A24: i in dom Wx1;
then A25: i in Seg len Wx1 by FINSEQ_1:def 3;
Seg len Wx1 c= Seg len Wx by A8,A18,FINSEQ_1:5,NAT_1:11;
then A26: Seg len Wx1 c= dom Wx by FINSEQ_1:def 3;
A27: Wx1/.i = Wx1.i by A24,PARTFUN1:def 6
.= Wx.i by FUNCT_1:49,A25,A18,A19
.= Wx/.i by A25,A26,PARTFUN1:def 6;
consider Wi be PartFunc of G0, G0F such that
A28: Wi = W0.i & Wx/.i = Wi/.x by A8,A25,A26;
take Wi;
thus Wi = W01.i & Wx1/.i = Wi/.x by A13,A18,A25,A27,A28,FUNCT_1:49;
end;
then A29: Sum Wx1 = (Sum W01).x by A7,A23,A18;
1 <= len Wx by A8,NAT_1:11;
then consider Wi be PartFunc of G0, G0F such that
A30: Wi = W0.(len Wx) & Wx/.(len Wx) = Wi/.x by A8,FINSEQ_3:25;
Sum W01 in Continuously_differentiable_Functions(X,G0F,n);
then consider SS be PartFunc of G0, G0F such that
A31: SS = Sum W01 & dom SS = X
& SS is_differentiable_on n,X
& diff(SS,n,X) is_continuous_on X;
W0.(len Wx) = W0/.(len Wx) by A8,A16,FINSEQ_1:4,PARTFUN1:def 6;
then W0.(len Wx) in Continuously_differentiable_Functions(X,G0F,n);
then A32: ex f be PartFunc of G0, G0F
st f = W0.(len Wx) & dom f = X
& f is_differentiable_on n,X
& diff(f,n,X) is_continuous_on X;
A33: dom (SS+Wi) = dom SS /\ dom Wi by VFUNCT_1:def 1
.= X by A30,A31,A32;
A34: Wi = W0/.(len Wx) by A8,A16,A30,FINSEQ_1:4,PARTFUN1:def 6;
(Sum W01).x = SS/.x by A1,A31,PARTFUN1:def 6;
hence Sum Wx
= (SS+Wi)/.x by A1,A22,A29,A30,A33,VFUNCT_1:def 1
.= (SS+Wi).x by A1,A33,PARTFUN1:def 6
.= (Sum W0).x by A8,A11,A15,A30,A31,A32,A34,Th7;
end;
A36: for k be Nat holds P[k] from NAT_1:sch 2(A2,A6);
let W0 be FinSequence of the carrier of XG0Fn,
Wx be FinSequence of G0F;
assume A37: dom Wx = dom W0
& for i be Nat st i in dom Wx
ex Wi be PartFunc of G0, G0F
st Wi = W0.i & Wx/.i = Wi/.x;
len Wx = len Wx;
hence Sum Wx = (Sum W0).x by A36,A37;
end;
begin :: High Order Partial Differentiable Functions
reserve E,F,G,S,T,W,Y for RealNormSpace;
reserve f,f1,f2 for PartFunc of S,T;
reserve Z for Subset of S;
reserve i,n for Nat;
definition
let S be RealNormSpace-Sequence,
T be RealNormSpace,
I be non empty FinSequence of dom S;
func Partdiff_SP(S,T,I) -> RealNormSpace-Sequence means
:Def3:
dom it = dom I
& it.1 = R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T)
& for i be Nat st 1 <= i < len I holds
it.(i+1) = R_NormSpace_of_BoundedLinearOperators(
S.(In(I.(i+1),dom S)),modetrans(it.i));
existence
proof
defpred P[Nat,set,set] means
$3 = R_NormSpace_of_BoundedLinearOperators(
S.(In(I.($1+1),dom S)),modetrans($2));
A1: for n being Nat st 1 <= n < len I
for x being set ex y being set st P[n,x,y]
proof
let n be Nat;
assume 1 <= n < len I;
let x be set;
take y = R_NormSpace_of_BoundedLinearOperators(
S.(In(I.(n+1),dom S)),modetrans(x));
thus thesis;
end;
consider p being FinSequence such that
A2: len p = len I
& (p.1 = R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T)
or len I = 0)
& for n st 1 <= n < len I holds P[n,p.n,p.(n+1)]
from RECDEF_1:sch 3(A1);
for x being set st x in rng p holds x is RealNormSpace
proof
let x be set;
assume x in rng p;
then consider i be object such that
A5: i in dom p & x = p.i by FUNCT_1:def 3;
reconsider i as Nat by A5;
A6: 1 <= i <= len p by A5,FINSEQ_3:25;
per cases;
suppose i = 1;
hence x is RealNormSpace by A2,A5;
end;
suppose i <> 1;
then 1 < i by A6,XXREAL_0:1;
then 1+1 <= i by NAT_1:13;
then A7: 2-1 <= i-1 by XREAL_1:9;
then reconsider j = i-1 as Nat by INT_1:3,ORDINAL1:def 12;
i-1 < i-0 by XREAL_1:15;
then j < len I by A2,A6,XXREAL_0:2; then
p.i = R_NormSpace_of_BoundedLinearOperators(
S.(In(I.(j+1),dom S)),modetrans(p.j)) by A2,A7;
hence x is RealNormSpace by A5;
end;
end;
then reconsider p as RealNormSpace-Sequence by A2,PRVECT_2:def 10;
take p;
thus thesis by A2,FINSEQ_3:29;
end;
uniqueness
proof
defpred P[Nat,set,set] means
$3 = R_NormSpace_of_BoundedLinearOperators(
S.(In(I.($1+1),dom S)),modetrans($2));
let p1,p2 be RealNormSpace-Sequence;
assume A9: dom p1 = dom I
& p1.1 = R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T)
& for i be Nat st 1 <= i < len I holds P[i,p1.i,p1.(i+1)];
assume A10: dom p2 = dom I
& p2.1 = R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T)
& for i be Nat st 1 <= i < len I holds P[i,p2.i,p2.(i+1)];
A11: dom p1 = Seg len I by A9,FINSEQ_1:def 3;
A12: dom p2 = Seg len I by A10,FINSEQ_1:def 3;
A13: for n st 1 <= n < len I
for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2;
A14: len p1 = len I
& (p1.1 = R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T)
or len I = 0)
& for n st 1 <= n < len I holds P[n,p1.n,p1.(n+1)]
by A9,A11,FINSEQ_1:def 3;
A15: len p2 = len I
& (p2.1 = R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T)
or len I = 0)
& for n st 1 <= n < len I holds P[n,p2.n,p2.(n+1)]
by A10,A12,FINSEQ_1:def 3;
thus p1 = p2 from RECDEF_1:sch 7(A13,A14,A15);
end;
end;
definition
let S be RealNormSpace-Sequence,
T be RealNormSpace,
I be non empty FinSequence of dom S,
i be Nat;
assume A1: 1 <= i <= len I;
func Partdiff_SP(S,T,I,i) -> RealNormSpace equals
:Def4:
Partdiff_SP(S,T,I).i;
correctness
proof
reconsider i0 = In(i,dom I) as Element of dom Partdiff_SP(S,T,I) by Def3;
Partdiff_SP(S,T,I).i0 is RealNormSpace;
hence thesis by SUBSET_1:def 8,A1,FINSEQ_3:25;
end;
end;
theorem Th12:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
I be non empty FinSequence of dom S
holds
Partdiff_SP(S,T,I,1)
= R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T)
& for i be Nat st 1 <= i < len I holds
Partdiff_SP(S,T,I,i+1) = R_NormSpace_of_BoundedLinearOperators
(S.(In(I.(i+1),dom S)),Partdiff_SP(S,T,I,i))
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
I be non empty FinSequence of dom S;
1 <= len I by FINSEQ_1:20;
hence Partdiff_SP(S,T,I,1) = Partdiff_SP(S,T,I).1 by Def4
.= R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T) by Def3;
let i be Nat;
assume A1: 1 <= i < len I; then
A2: 1 <= i+1 <= len I by NAT_1:13;
A3: Partdiff_SP(S,T,I,i) = Partdiff_SP(S,T,I).i by A1,Def4;
thus Partdiff_SP(S,T,I,i+1) = Partdiff_SP(S,T,I).(i+1) by A2,Def4
.= R_NormSpace_of_BoundedLinearOperators
(S.(In(I.(i+1),dom S)),modetrans(Partdiff_SP(S,T,I).i)) by A1,Def3
.= R_NormSpace_of_BoundedLinearOperators
(S.(In(I.(i+1),dom S)),Partdiff_SP(S,T,I,i)) by A3,NDIFF_6:def 1;
end;
definition
let S be RealNormSpace-Sequence,
T be RealNormSpace,
I be non empty FinSequence of dom S;
func PartdiffSP(S,T,I) -> RealNormSpace equals
(Partdiff_SP(S,T,I)).(len I);
correctness
proof
len I in Seg len I by FINSEQ_1:3;
then len I in dom I by FINSEQ_1:def 3;
then reconsider i0 = len I as Element of dom(Partdiff_SP(S,T,I)) by Def3;
Partdiff_SP(S,T,I).i0 is RealNormSpace;
hence thesis;
end;
end;
definition
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f be PartFunc of product S,T;
func PartDiffSeq(f,Z,I) -> FinSequence means
:Def6:
dom it = dom I & it.1 = f`partial|(Z,I.1)
& for i be Nat st 1 <= i < len I holds
ex g be PartFunc of product S, Partdiff_SP(S,T,I,i)
st it.i = g & it.(i+1) = g`partial|(Z,I.(i+1));
existence
proof
defpred P[Nat,set,set] means
$2 is PartFunc of product S, Partdiff_SP(S,T,I,$1) implies
ex g be PartFunc of product S, Partdiff_SP(S,T,I,$1)
st $2 = g & $3 = g`partial|(Z,I.($1+1));
A1: for n being Nat st 1 <= n & n < len I
for x being set ex y being set st P[n,x,y]
proof
let n be Nat;
assume 1 <= n < len I;
let x be set;
x is PartFunc of product S, Partdiff_SP(S,T,I,n) implies
ex y being set st
ex g be PartFunc of product S, Partdiff_SP(S,T,I,n)
st x = g & y = g`partial|(Z,I.(n+1))
proof
assume x is PartFunc of product S, Partdiff_SP(S,T,I,n);
then reconsider g = x as PartFunc of product S, Partdiff_SP(S,T,I,n);
take y = g`partial|(Z,I.(n+1));
thus thesis;
end;
hence thesis;
end;
consider p being FinSequence such that
A2: len p = len I
& (p.1 = f`partial|(Z,I.1) or len I = 0)
& for n st 1 <= n < len I holds P[n,p.n,p.(n+1)]
from RECDEF_1:sch 3(A1);
defpred Q[Nat] means
1 <= $1 <= len I implies
p.$1 is PartFunc of product S, Partdiff_SP(S,T,I,$1);
A4: Q[0];
A5: for i be Nat st Q[i] holds Q[i+1]
proof
let i be Nat;
assume A6: Q[i];
assume A7: 1 <= i+1 <= len I;
per cases;
suppose A8: i = 0;
Partdiff_SP(S,T,I,i+1)
= Partdiff_SP(S,T,I).(i+1) by A7,Def4
.= R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T)
by A8,Def3;
hence p.(i+1) is PartFunc of product S,
Partdiff_SP(S,T,I,i+1) by A2,A8;
end;
suppose A9: i <> 0;
then A10: 1 <= i by NAT_1:14;
i < i+1 by NAT_1:19;
then A11: i < len I by A7,XXREAL_0:2;
then consider g be PartFunc of product S, Partdiff_SP(S,T,I,i)
such that
A12: p.i = g & p.(i+1) = g`partial|(Z,I.(i+1)) by A2,A6,A9,NAT_1:14;
A13: Partdiff_SP(S,T,I).i = Partdiff_SP(S,T,I,i) by A10,A11,Def4;
Partdiff_SP(S,T,I,i+1) = Partdiff_SP(S,T,I).(i+1) by A7,Def4
.= R_NormSpace_of_BoundedLinearOperators(
S.(In(I.(i+1),dom S)),modetrans(Partdiff_SP(S,T,I).i))
by A9,A11,Def3,NAT_1:14
.= R_NormSpace_of_BoundedLinearOperators(
S.(In(I.(i+1),dom S)),Partdiff_SP(S,T,I,i))
by A13,NDIFF_6:def 1;
hence p.(i+1) is PartFunc of product S, Partdiff_SP(S,T,I,i+1) by A12;
end;
end;
A14: for i be Nat holds Q[i] from NAT_1:sch 2(A4,A5);
A15: for i be Nat st 1 <= i < len I holds
ex g be PartFunc of product S, Partdiff_SP(S,T,I,i)
st p.i = g & p.(i+1) = g`partial|(Z,I.(i+1))
proof
let i be Nat;
assume A16: 1 <= i < len I;
then p.i is PartFunc of product S, Partdiff_SP(S,T,I,i) by A14;
hence ex g be PartFunc of product S, Partdiff_SP(S,T,I,i)
st p.i = g & p.(i+1) = g`partial|(Z,I.(i+1)) by A2,A16;
end;
take p;
thus dom p = dom I by A2,FINSEQ_3:29;
thus p.1 = f`partial|(Z,I.1) by A2;
thus thesis by A15;
end;
uniqueness
proof
defpred P[Nat,set,set] means
ex g be PartFunc of product S, Partdiff_SP(S,T,I,$1)
st $2 = g & $3 = g`partial|(Z,I.($1+1));
let p1,p2 be FinSequence;
assume A17: dom p1 = dom I & p1.1 = f`partial|(Z,I.1)
& for i be Nat st 1 <= i < len I holds
ex g be PartFunc of product S, Partdiff_SP(S,T,I,i)
st p1.i = g & p1.(i+1) = g`partial|(Z,I.(i+1));
assume A18: dom p2 = dom I & p2.1 = f`partial|(Z,I.1)
& for i be Nat st 1 <= i < len I holds
ex g be PartFunc of product S, Partdiff_SP(S,T,I,i)
st p2.i = g & p2.(i+1) = g`partial|(Z,I.(i+1));
A19: dom p1 = Seg len I by A17,FINSEQ_1:def 3;
A20: dom p2 = Seg len I by A18,FINSEQ_1:def 3;
A21: for n st 1 <= n < len I
for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2;
A22: len p1 = len I & (p1.1 = f`partial|(Z,I.1) or len I = 0)
& for n be Nat st 1 <= n & n < len I holds P[n,p1.n,p1.(n+1)]
by A17,A19,FINSEQ_1:def 3;
A23: len p2 = len I & (p2.1 = f`partial|(Z,I.1) or len I = 0)
& for n be Nat st 1 <= n < len I holds P[n,p2.n,p2.(n+1)]
by A18,A20,FINSEQ_1:def 3;
thus p1 = p2 from RECDEF_1:sch 7(A21,A22,A23);
end;
end;
definition
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f be PartFunc of product S,T;
let i be Nat;
assume A1: 1 <= i <= len I;
func PartDiffSeq(f,Z,I,i) -> PartFunc of product S, Partdiff_SP(S,T,I,i)
equals
:Def7:
PartDiffSeq(f,Z,I).i;
correctness
proof
per cases;
suppose A2: i = 1;
then A3: PartDiffSeq(f,Z,I).i = f`partial|(Z,I.i) by Def6;
Partdiff_SP(S,T,I,i) = Partdiff_SP(S,T,I).i by Def4,A1
.= R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T) by Def3,A2;
hence PartDiffSeq(f,Z,I).i is PartFunc of product S, Partdiff_SP(S,T,I,i)
by A3,A2;
end;
suppose i <> 1;
then 1 < i by A1,XXREAL_0:1;
then 1+1 <= i by NAT_1:13;
then A4: 2-1 <= i-1 by XREAL_1:9;
then reconsider j = i-1 as Nat by INT_1:3,ORDINAL1:def 12;
i-1 < i-0 by XREAL_1:15;
then A5: j < len I by A1,XXREAL_0:2;
consider g be PartFunc of product S, Partdiff_SP(S,T,I,j)
such that A6: PartDiffSeq(f,Z,I).j = g
& PartDiffSeq(f,Z,I).(j+1) = g`partial|(Z,I.(j+1)) by Def6,A5,A4;
A7: Partdiff_SP(S,T,I).j = Partdiff_SP(S,T,I,j) by Def4,A4,A5;
Partdiff_SP(S,T,I,i)
= Partdiff_SP(S,T,I).(j+1) by Def4,A1
.= R_NormSpace_of_BoundedLinearOperators(
S.(In(I.(j+1),dom S)),modetrans(Partdiff_SP(S,T,I).j))
by Def3,A5,A4
.= R_NormSpace_of_BoundedLinearOperators(
S.(In(I.(j+1),dom S)),Partdiff_SP(S,T,I,j))
by A7,NDIFF_6:def 1;
hence PartDiffSeq(f,Z,I).i is PartFunc of product S, Partdiff_SP(S,T,I,i)
by A6;
end;
end;
end;
theorem Th13:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f be PartFunc of product S,T
holds
PartDiffSeq(f,Z,I,1) = f`partial|(Z,I.1)
& for i be Nat st 1 <= i < len I holds
PartDiffSeq(f,Z,I,i+1) = PartDiffSeq(f,Z,I,i)`partial|(Z,I.(i+1))
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f be PartFunc of product S,T;
1 <= len I by FINSEQ_1:20;
hence PartDiffSeq(f,Z,I,1) = PartDiffSeq(f,Z,I).1 by Def7
.= f`partial|(Z,I.1) by Def6;
let i be Nat;
assume A1: 1 <= i < len I;
then 1 <= i+1 <= len I by NAT_1:13;
then A2: PartDiffSeq(f,Z,I,i+1) = PartDiffSeq(f,Z,I).(i+1) by Def7;
ex g be PartFunc of product S, Partdiff_SP(S,T,I,i)
st PartDiffSeq(f,Z,I).i = g
& PartDiffSeq(f,Z,I).(i+1) = g`partial|(Z,I.(i+1))
by Def6,A1;
hence PartDiffSeq(f,Z,I,i+1) = PartDiffSeq(f,Z,I,i)`partial|(Z,I.(i+1))
by A1,A2,Def7;
end;
definition
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f be PartFunc of product S,T;
pred f is_partial_differentiable_on Z,I means
f is_partial_differentiable_on Z,I.1
& for i be Nat st 1 <= i < len I
holds PartDiffSeq(f,Z,I,i) is_partial_differentiable_on Z,I.(i+1);
end;
definition
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f be PartFunc of product S,T;
func f `partial| (Z,I) -> PartFunc of product S,Partdiff_SP(S,T,I,len I)
equals
PartDiffSeq(f,Z,I,len I);
coherence;
end;
theorem
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
k be Element of dom S,
f be PartFunc of product S,T
holds
f is_partial_differentiable_on Z,<*k*>
iff f is_partial_differentiable_on Z,k
by FINSEQ_1:40;
theorem Th15:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
k be Element of dom S,
f be PartFunc of product S,T
holds
f `partial|(Z,<*k*>) = f`partial|(Z,k)
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
k be Element of dom S,
f be PartFunc of product S,T;
set I = <*k*>;
A1: len I = 1 & I.1 = k by FINSEQ_1:40;
then f`partial|(Z,I) = (PartDiffSeq (f,Z,I)).(len I) by Def7
.= f`partial|(Z,k) by A1,Def6;
hence thesis;
end;
theorem Th16:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I,G be non empty FinSequence of dom S,
f be PartFunc of product S,T
holds
(for n being Nat st 1 <= n <= len G holds
Partdiff_SP(S,T,G^I,n) = Partdiff_SP(S,T,G,n)
& PartDiffSeq(f,Z,G^I,n) = PartDiffSeq(f,Z,G,n))
& (for n being Nat st 1 <= n <= len I holds
Partdiff_SP(S, Partdiff_SP(S,T,G,len G),I,n)
= Partdiff_SP(S,T,G^I,len G + n)
& PartDiffSeq((f `partial| (Z,G)),Z,I,n)
= PartDiffSeq(f,Z,G^I,len G + n))
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I,G be non empty FinSequence of dom S,
f be PartFunc of product S,T;
A1: for i being Nat st i < len G holds
(G^I).(i+1) = G.(i+1)
proof
let i be Nat;
assume i < len G;
then 1 <= i+1 <= len G by NAT_1:11,13;
then i+1 in dom G by FINSEQ_3:25;
hence (G^I).(i+1) = G.(i+1) by FINSEQ_1:def 7;
end;
A2: for i being Nat st i < len I holds
(G^I).(len G + (i+1)) = I.(i+1)
proof
let i be Nat;
assume i < len I;
then i+1 <= len I by NAT_1:13;
then A3: i+1 in dom I by NAT_1:11,FINSEQ_3:25;
thus (G^I).(len G + (i+1)) = I.(i+1) by A3,FINSEQ_1:def 7;
end;
defpred S1[Nat] means 1 <= $1 <= len G implies
Partdiff_SP(S,T,G^I,$1) = Partdiff_SP(S,T,G,$1)
& PartDiffSeq(f,Z,G^I,$1) = PartDiffSeq(f,Z,G,$1);
A4: S1[0];
A5: for k being Nat st S1[k] holds S1[k+1]
proof
let k be Nat;
assume A6: S1[k];
assume A7: 1 <= k+1 <= len G;
k < k+1 by NAT_1:19;
then A8: k < len G by A7,XXREAL_0:2;
per cases;
suppose A9: k = 0;
hence Partdiff_SP(S,T,G^I,k+1)
= R_NormSpace_of_BoundedLinearOperators(S.(In((G^I).(k+1),dom S)),T)
by Th12
.= R_NormSpace_of_BoundedLinearOperators(S.(In(G.(k+1),dom S)),T)
by A8,A1
.= Partdiff_SP(S,T,G,k+1) by A9,Th12;
thus PartDiffSeq(f,Z,G^I,k+1)
= f`partial|(Z,(G^I).(k+1)) by Th13,A9
.= f`partial|(Z,G.(k+1)) by A8,A1
.= PartDiffSeq(f,Z,G,k+1) by Th13,A9;
end;
suppose A10: k <> 0;
len (G^I) = len G + len I by FINSEQ_1:22;
then len G <= len (G^I) by NAT_1:11;
then A11: 1 <= k < len (G^I) by A8,A10,NAT_1:14,XXREAL_0:2;
hence Partdiff_SP(S,T,G^I,k+1)
= R_NormSpace_of_BoundedLinearOperators(
S.(In((G^I).(k+1),dom S)),Partdiff_SP(S,T,G^I,k))
by Th12
.= R_NormSpace_of_BoundedLinearOperators(
S.(In(G.(k+1),dom S)),Partdiff_SP(S,T,G,k))
by A1,A6,A8,A10,NAT_1:14
.= Partdiff_SP(S,T,G,k+1) by A8,A10,Th12,NAT_1:14;
thus PartDiffSeq(f,Z,G^I,k+1)
= PartDiffSeq(f,Z,G^I,k)`partial|(Z,(G^I).(k+1))
by A11,Th13
.= PartDiffSeq(f,Z,G,k)`partial|(Z,G.(k+1)) by A1,A6,A8,A10,NAT_1:14
.= PartDiffSeq(f,Z,G,k+1) by A8,A10,Th13,NAT_1:14;
end;
end;
A12: for n being Nat holds S1[n] from NAT_1:sch 2(A4,A5);
hence for n being Nat st 1 <= n <= len G holds
Partdiff_SP(S,T,G^I,n) = Partdiff_SP(S,T,G,n)
& PartDiffSeq(f,Z,G^I,n) = PartDiffSeq(f,Z,G,n);
1 <= len G by FINSEQ_1:20;
then A13: Partdiff_SP(S,T,G^I,len G) = Partdiff_SP(S,T,G,len G)
& PartDiffSeq(f,Z,G^I,len G) = PartDiffSeq(f,Z,G,len G)
by A12;
defpred S2[Nat] means 1 <= $1 <= len I implies
Partdiff_SP(S,T,G^I,len G + $1)
= Partdiff_SP(S,Partdiff_SP(S,T,G,len G),I,$1)
& PartDiffSeq(f,Z,G^I,len G + $1)
= PartDiffSeq(f`partial|(Z,G),Z,I,$1);
A14: S2[0];
A15: for k being Nat st S2[k] holds S2[k+1]
proof
let k be Nat;
assume A16: S2[k];
set i = len G + k;
assume A17: 1 <= k+1 <= len I;
per cases;
suppose A18: k = 0;
set i = len G;
A19: 1 <= len G & 1 <= len I by FINSEQ_1:20;
0 + len G < len I + len G by XREAL_1:8;
then A20: 1 <= i < len(G^I) by FINSEQ_1:20,22;
1 in dom I by A19,FINSEQ_3:25;
then A21: (G^I).(i+1) = I.1 by FINSEQ_1:def 7;
thus Partdiff_SP(S,T,G^I,len G + (k+1))
= R_NormSpace_of_BoundedLinearOperators(
S.In((G^I).(i+1),dom S),Partdiff_SP(S,T,G^I,i))
by A18,A20,Th12
.= Partdiff_SP(S,Partdiff_SP(S,T,G,len G),I,k+1) by A13,A18,A21,Th12;
thus PartDiffSeq(f,Z,G^I,len G + (k+1))
= PartDiffSeq(f,Z,G^I,i)`partial|(Z,(G^I).(i+1)) by A18,A20,Th13
.= PartDiffSeq(f`partial|(Z,G),Z,I,k+1) by A13,A18,A21,Th13;
end;
suppose A22: k <> 0;
k < k+1 by NAT_1:19;
then A23: k < len I by A17,XXREAL_0:2;
A24: (G^I).(i+1) = (G^I).(len G + (k+1))
.= I.(k+1) by A2,A23;
len (G^I) = len G + len I by FINSEQ_1:22;
then A27: 1 <= i < len (G^I) by A23,NAT_1:14,XREAL_1:8;
hence Partdiff_SP(S,T,G^I,len G + (k+1))
= R_NormSpace_of_BoundedLinearOperators(
S.In((G^I).(i+1),dom S),Partdiff_SP(S,T,G^I,i))
by Th12
.= Partdiff_SP(S,Partdiff_SP(S,T,G,len G),I,k+1)
by A16,A22,A23,A24,Th12,NAT_1:14;
thus PartDiffSeq(f,Z,G^I,len G + (k+1))
= PartDiffSeq(f,Z,G^I,i)`partial|(Z,(G^I).(i+1)) by Th13,A27
.= PartDiffSeq(f`partial|(Z,G),Z,I,k+1)
by A16,A22,A23,A24,Th13,NAT_1:14;
end;
end;
for n being Nat holds S2[n] from NAT_1:sch 2(A14,A15);
hence for n being Nat st 1 <= n <= len I holds
Partdiff_SP(S,Partdiff_SP(S,T,G,len G),I,n)
= Partdiff_SP(S,T,G^I,len G + n)
& PartDiffSeq(f`partial|(Z,G),Z,I,n)
= PartDiffSeq(f,Z,G^I,len G + n);
end;
theorem Th17:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I,G be non empty FinSequence of dom S,
f be PartFunc of product S,T
holds
Partdiff_SP(S,T,G^I,len G) = Partdiff_SP(S,T,G,len G)
& PartDiffSeq(f,Z,G^I,len G) = PartDiffSeq(f,Z,G,len G)
& Partdiff_SP(S,Partdiff_SP(S,T,G,len G),I,len I)
= Partdiff_SP(S,T,G^I,len G + len I)
& PartDiffSeq(f`partial|(Z,G),Z,I,len I)
= PartDiffSeq(f,Z,G^I,len G + len I)
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I,G be non empty FinSequence of dom S,
f be PartFunc of product S,T;
1 <= len G by FINSEQ_1:20;
hence Partdiff_SP(S,T,G^I,len G) = Partdiff_SP(S,T,G,len G)
& PartDiffSeq(f,Z,G^I,len G) = PartDiffSeq(f,Z,G,len G) by Th16;
1 <= len I by FINSEQ_1:20;
hence Partdiff_SP(S,Partdiff_SP(S,T,G,len G),I,len I)
= Partdiff_SP(S,T,G^I,len G + len I)
& PartDiffSeq(f`partial|(Z,G),Z,I,len I)
= PartDiffSeq(f,Z,G^I,len G + len I) by Th16;
end;
theorem Th18:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I,G be non empty FinSequence of dom S,
f be PartFunc of product S,T
holds
f`partial|(Z,G)`partial|(Z,I) = f`partial|(Z,G^I)
& Partdiff_SP(S,Partdiff_SP(S,T,G,len G),I,len I)
= Partdiff_SP(S,T,G^I,len(G^I))
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I,G be non empty FinSequence of dom S,
f be PartFunc of product S,T;
thus f`partial|(Z,G)`partial|(Z,I)
= PartDiffSeq(f,Z,G^I,len G + len I) by Th17
.= f`partial|(Z,G^I) by FINSEQ_1:22;
thus Partdiff_SP(S,Partdiff_SP(S,T,G,len G),I,len I)
= Partdiff_SP(S,T,G^I,len G + len I) by Th17
.= Partdiff_SP(S,T,G^I,len(G^I)) by FINSEQ_1:22;
end;
theorem
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
G be non empty FinSequence of dom S,
s be Element of dom S,
f be PartFunc of product S,T
holds
Partdiff_SP(S,Partdiff_SP(S,T,G,len G),<*s*>,1)
= Partdiff_SP(S,T,G^<*s*>,len G + 1)
& f`partial|(Z,G)`partial|(Z,s)
= PartDiffSeq(f,Z,G^<*s*>,len G + 1)
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
G be non empty FinSequence of dom S,
s be Element of dom S,
f be PartFunc of product S,T;
set I = <*s*>;
A1: len I = 1 by FINSEQ_1:39;
hence Partdiff_SP(S,Partdiff_SP(S,T,G,len G),<*s*>,1)
= Partdiff_SP(S,T,G^<*s*>,len G + 1) by Th17;
PartDiffSeq(f`partial|(Z,G),Z,I,len I)
= f`partial|(Z,G)`partial|(Z,I.1) by A1,Th13
.= f`partial|(Z,G)`partial|(Z,s);
hence thesis by A1,Th17;
end;
theorem Th20:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I,G be non empty FinSequence of dom S,
f be PartFunc of product S,T
holds
f is_partial_differentiable_on Z,I^G
iff
f is_partial_differentiable_on Z,I
& f`partial|(Z,I) is_partial_differentiable_on Z,G
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I,G be non empty FinSequence of dom S,
f be PartFunc of product S,T;
A1: for i being Nat st i < len I holds
(I^G).(i+1) = I.(i+1)
proof
let i be Nat;
assume i < len I;
then 1 <= i+1 <= len I by NAT_1:11,13;
then i+1 in dom I by FINSEQ_3:25;
hence (I^G).(i+1) = I.(i+1) by FINSEQ_1:def 7;
end;
A2: len(I^G) = len I + len G by FINSEQ_1:22;
A3: for i being Nat st i < len G holds
(I^G).(len I + (i+1)) = G.(i+1)
proof
let i be Nat;
assume i < len G;
then i+1 <= len G by NAT_1:13;
then i+1 in dom G by NAT_1:11,FINSEQ_3:25;
hence (I^G).(len I + (i+1)) = G.(i+1) by FINSEQ_1:def 7;
end;
0 + len I < len G + len I by XREAL_1:8;
then A6: len I < len(I^G) by FINSEQ_1:22;
A5: 1 <= len I & 1 <= len G by FINSEQ_1:20; then
1 in dom G by FINSEQ_3:25;
then A7: (I^G).(len I+1) = G.1 by FINSEQ_1:def 7;
A8: 1 <= len I by FINSEQ_1:20;
A9: 1 in dom I by A5,FINSEQ_3:25;
hereby
assume A11: f is_partial_differentiable_on Z,I^G;
for i be Nat st 1 <= i < len I
holds PartDiffSeq(f,Z,I,i) is_partial_differentiable_on Z,I.(i+1)
proof
let i be Nat;
assume A13: 1 <= i < len I;
then i < len(I^G) by A6,XXREAL_0:2;
then A14: PartDiffSeq(f,Z,I^G,i)
is_partial_differentiable_on Z,(I^G).(i+1) by A11,A13;
A15: (I^G).(i+1) = I.(i+1) by A1,A13;
Partdiff_SP(S,T,I^G,i) = Partdiff_SP(S,T,I,i) by A13,Th16;
hence PartDiffSeq(f,Z,I,i) is_partial_differentiable_on Z,I.(i+1)
by A13,A14,A15,Th16;
end;
hence f is_partial_differentiable_on Z,I by A9,A11,FINSEQ_1:def 7;
A17: PartDiffSeq(f,Z,I^G,len I)
is_partial_differentiable_on Z,(I^G).(len I+1) by A6,A11,FINSEQ_1:20;
A18: PartDiffSeq(f,Z,I^G,len I) = f`partial|(Z,I) by A8,Th16;
for i be Nat st 1 <= i < len G holds
PartDiffSeq(f`partial|(Z,I),Z,G,i)
is_partial_differentiable_on Z,G.(i+1)
proof
let i be Nat;
assume A20: 1 <= i < len G;
then A21: len I + i < len(I^G) by A2,XREAL_1:8;
A22: 1 + 0 <= len I + i by A20,XREAL_1:7;
A23: Partdiff_SP(S,Partdiff_SP(S,T,I,len I),G,i)
= Partdiff_SP(S,T,I^G,len I + i) by A20,Th16;
A24: PartDiffSeq(f`partial|(Z,I),Z,G,i)
= PartDiffSeq(f,Z,I^G,len I + i) by A20,Th16;
(I^G).(len I + i+1) = (I^G).(len I + (i+1))
.= G.(i+1) by A3,A20;
hence
PartDiffSeq(f`partial|(Z,I),Z,G,i)
is_partial_differentiable_on Z,G.(i+1) by A11,A21,A22,A23,A24;
end;
hence f`partial|(Z,I) is_partial_differentiable_on Z,G
by A7,A8,A17,A18,Th16;
end;
assume that
A25: f is_partial_differentiable_on Z,I and
A26: f`partial|(Z,I) is_partial_differentiable_on Z,G;
A29: (I^G).(0+1) = I.(0+1) by A1;
for i be Nat st 1 <= i < len(I^G) holds
PartDiffSeq(f,Z,I^G,i)
is_partial_differentiable_on Z,(I^G).(i+1)
proof
let i be Nat;
assume A30: 1 <= i < len(I^G);
per cases;
suppose A31: i < len I; then
A32: PartDiffSeq(f,Z,I^G,i) = PartDiffSeq(f,Z,I,i) by A30,Th16;
A33: Partdiff_SP(S,T,I^G,i) = Partdiff_SP(S,T,I,i) by A30,A31,Th16;
PartDiffSeq(f,Z,I,i) is_partial_differentiable_on Z,I.(i+1)
by A25,A30,A31;
hence PartDiffSeq(f,Z,I^G,i) is_partial_differentiable_on Z,(I^G).(i+1)
by A1,A31,A32,A33;
end;
suppose len I <= i;
then len I - len I <= i - len I by XREAL_1:9;
then i - len I in NAT by INT_1:3;
then reconsider j = i - len I as Nat;
A35: j < len I + len G - len I by A2,A30,XREAL_1:14;
per cases;
suppose A36: j = 0; then
PartDiffSeq(f,Z,I^G,i) = f`partial|(Z,I) by A30,Th16;
hence PartDiffSeq(f,Z,I^G,i)
is_partial_differentiable_on Z,(I^G).(i+1) by A7,A26,A30,A36,Th16;
end;
suppose A38: j <> 0; then
A39: 1 <= j by NAT_1:14;
A40: PartDiffSeq(f`partial|(Z,I),Z,G,j)
is_partial_differentiable_on Z,G.(j+1) by A26,A35,A38,NAT_1:14;
A41: (I^G).(i+1) = (I^G).(len I + (j+1))
.= G.(j+1) by A3,A35;
Partdiff_SP(S,Partdiff_SP(S,T,I,len I),G,j)
= Partdiff_SP(S,T,I^G,len I + j) by A35,A39,Th16;
hence PartDiffSeq(f,Z,I^G,i) is_partial_differentiable_on Z,(I^G).(i+1)
by A35,A39,A40,A41,Th16;
end;
end;
end;
hence f is_partial_differentiable_on Z,I^G by A25,A29;
end;
begin :: Properties of Partial Derivatives and Fundamental Operations
theorem Th21:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
f,g be PartFunc of product S,T,
i be set
st Z is open & i in dom S
& f is_partial_differentiable_on Z,i
& g is_partial_differentiable_on Z,i
holds
f+g is_partial_differentiable_on Z,i
& (f+g)`partial|(Z,i) = f`partial|(Z,i) + g`partial|(Z,i)
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
f,g be PartFunc of product S,T,
i be set;
assume that
A1: Z is open & i in dom S and
A2: f is_partial_differentiable_on Z,i and
A3: g is_partial_differentiable_on Z,i;
A4: Z c= dom f & Z c= dom g by A2,A3,NDIFF_5:def 8;
then Z c= dom f /\ dom g by XBOOLE_1:19;
then A5: Z c= dom(f+g) by VFUNCT_1:def 1; then
A9: dom((f+g)|Z) = Z by RELAT_1:62;
for x being Point of product S st x in Z holds
(f+g)|Z is_partial_differentiable_in x,i
proof
let x be Point of product S;
assume x in Z;
then f|Z is_partial_differentiable_in x,i
& g|Z is_partial_differentiable_in x,i by A2,A3,NDIFF_5:def 8;
then A6: f|Z + g|Z is_partial_differentiable_in x,i by A1,NDIFF_5:28;
A7: dom(f|Z) = Z & dom(g|Z) = Z by A4,RELAT_1:62;
then A8: dom(f|Z) /\ dom(g|Z) = Z;
for x be Element of product S st x in dom((f+g)|Z)
holds ((f+g)|Z)/.x = (f|Z)/.x + (g|Z)/.x
proof
let x be Element of product S;
assume A10: x in dom((f+g)|Z);
hence ((f+g)|Z)/.x = (f+g)/.x by PARTFUN1:80
.= f/.x + g/.x by A5,A9,A10,VFUNCT_1:def 1
.= (f|Z)/.x + g/.x by A7,A10,PARTFUN1:80
.= (f|Z)/.x + (g|Z)/.x by A7,A10,PARTFUN1:80;
end;
hence (f+g)|Z is_partial_differentiable_in x,i
by A5,A6,A8,RELAT_1:62,VFUNCT_1:def 1;
end;
hence A11: f+g is_partial_differentiable_on Z,i by A5,NDIFF_5:def 8;
set pfg = f`partial|(Z,i) + g`partial|(Z,i);
dom(f`partial|(Z,i)) = Z & dom(g`partial|(Z,i)) = Z by A2,A3,NDIFF_5:def 9;
then dom(f`partial|(Z,i)) /\ dom(g`partial|(Z,i)) = Z;
then A12: dom pfg = Z by VFUNCT_1:def 1;
for x being Point of product S st x in Z holds pfg/.x = partdiff(f+g,x,i)
proof
let x be Point of product S;
assume A13: x in Z; then
A14: f is_partial_differentiable_in x,i
& g is_partial_differentiable_in x,i by A1,A2,A3,NDIFF_5:32;
thus pfg/.x = (f`partial|(Z,i))/.x + (g`partial|(Z,i))/.x
by A12,A13,VFUNCT_1:def 1
.= partdiff(f,x,i) + (g`partial|(Z,i))/.x
by A2,A13,NDIFF_5:def 9
.= partdiff(f,x,i) + partdiff(g,x,i) by A3,A13,NDIFF_5:def 9
.= partdiff(f+g,x,i) by A1,A14,NDIFF_5:28;
end;
hence (f+g)`partial|(Z,i) = f`partial|(Z,i) + g`partial|(Z,i)
by A11,A12,NDIFF_5:def 9;
end;
theorem Th22:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
f be PartFunc of product S,T,
i be set
st Z is open & f is_differentiable_on Z
holds
f is_partial_differentiable_on Z,i
& for x being Point of product S st x in Z holds
(f`partial|(Z,i))/.x = ((f`|Z)/.x) * (reproj(In(i,dom S),0.(product S)))
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
f be PartFunc of product S,T,
i be set;
assume that
A1: Z is open and
A2: f is_differentiable_on Z;
A4: for x being Point of product S st x in Z holds
f is_partial_differentiable_in x,i
& partdiff(f,x,i) = (diff(f,x)) * (reproj(In(i,dom S),0.(product S)))
proof
let x be Point of product S;
assume x in Z;
then f is_differentiable_in x by A1,A2,NDIFF_1:31;
hence f is_partial_differentiable_in x,i
& partdiff(f,x,i) = (diff(f,x)) * (reproj(In(i,dom S),0.(product S)))
by NDIFF_5:41;
end;
then for x being Point of product S st x in Z holds
f is_partial_differentiable_in x,i;
hence
A5: f is_partial_differentiable_on Z,i by A1,A2,NDIFF_5:24;
let x be Point of product S;
assume A6: x in Z;
hence (f`partial|(Z,i))/.x = partdiff(f,x,i) by A5,NDIFF_5:def 9
.= (diff(f,x)) * (reproj(In(i,dom S),0.(product S))) by A4,A6
.= ((f`|Z)/.x) * (reproj(In(i,dom S),0.(product S)))
by A2,A6,NDIFF_1:def 9;
end;
theorem Th23:
for S be RealNormSpace-Sequence,
s be set
holds
reproj(In(s,dom S),0.(product S))
is Lipschitzian LinearOperator of S.In(s,dom S),product S
proof
let S be RealNormSpace-Sequence,
s be set;
set L1 = reproj(In(s,dom S),0.(product S));
set E = S.In(s,dom S);
set F = product S;
A1: L1 is additive by NDIFF_5:34;
for x be VECTOR of E, a be Real holds L1.(a*x) = a*L1.x by NDIFF_5:39;
then reconsider L1 as LinearOperator of E, F by A1,LOPBAN_1:def 5;
set K = 1;
for x being VECTOR of E holds ||.L1.x.|| <= K * ||.x.|| by NDIFF_5:21;
hence thesis by LOPBAN_1:def 8;
end;
theorem Th24:
for S be RealNormSpace-Sequence,
s be set
holds
proj(In(s,dom S)) is Lipschitzian LinearOperator of product S,S.In(s,dom S)
& ex LP be Point of
R_NormSpace_of_BoundedLinearOperators(product S,S.In(s,dom S))
st LP = proj(In(s,dom S)) & ||.LP.|| <= 1
proof
let S be RealNormSpace-Sequence,
s be set;
set L1 = proj(In(s,dom S));
set F = S.In(s,dom S);
set E = product S;
A1: L1 is additive by NDIFF_5:35;
for x be VECTOR of E, a be Real holds L1.(a*x) = a*L1.x by NDIFF_5:40;
then reconsider L1 as LinearOperator of E, F by A1,LOPBAN_1:def 5;
set K = 1;
for x being VECTOR of E holds ||.L1.x.|| <= K * ||.x.|| by NDIFF_5:31;
hence
A3: proj(In(s,dom S)) is Lipschitzian LinearOperator of E,F
by LOPBAN_1:def 8;
then reconsider LP = L1 as Point of
R_NormSpace_of_BoundedLinearOperators(E,F) by LOPBAN_1:def 9;
take LP;
thus LP = proj(In(s,dom S));
A5: for x being Real st x in PreNorms(modetrans(LP,E,F)) holds x <= 1
proof
let x be Real;
assume x in PreNorms(modetrans(LP,E,F));
then consider y being VECTOR of product S such that
A6: (x = ||.(modetrans(LP,E,F)).y.|| & ||.y.|| <= 1);
A7: ||.L1.y.|| <= K * ||.y.|| by NDIFF_5:31;
LP = modetrans(LP,E,F) by A3,LOPBAN_1:29;
hence x <= 1 by A6,A7,XXREAL_0:2;
end;
reconsider LP0 = LP as Element of BoundedLinearOperators(E,F);
A8: PreNorms modetrans(LP,E,F) is bounded_above
proof
for x being ExtReal st x in PreNorms modetrans(LP,E,F) holds x <= 1 by A5;
then 1 is UpperBound of PreNorms modetrans(LP,E,F) by XXREAL_2:def 1;
hence PreNorms modetrans(LP,E,F) is bounded_above;
end;
now
assume A9: upper_bound(PreNorms(modetrans(LP,E,F))) > 1;
set dif = upper_bound(PreNorms(modetrans(LP,E,F))) - 1;
upper_bound(PreNorms(modetrans(LP,E,F))) - 1 > 0 by A9,XREAL_1:50;
then ex w being Real st w in PreNorms(modetrans(LP,E,F))
& upper_bound(PreNorms(modetrans(LP,E,F)))
- (upper_bound(PreNorms(modetrans(LP,E,F))) - 1) < w
by A8,SEQ_4:def 1;
hence contradiction by A5;
end;
hence thesis by LOPBAN_1:def 13;
end;
theorem Th25:
for S be RealNormSpace-Sequence,
G be RealNormSpace,
Z be non empty Subset of product S,
f be PartFunc of product S,G,
s be set,
i be Nat
st f is_differentiable_on i+1,Z
holds f`partial|(Z,s) is_differentiable_on i,Z
proof
let S be RealNormSpace-Sequence,
G be RealNormSpace,
Z be non empty Subset of product S,
f be PartFunc of product S,G,
s be set,
i be Nat;
assume A1: f is_differentiable_on i+1,Z;
then f is_differentiable_on 0+1,Z;
then A2: f is_differentiable_on Z by NDIFF_6:15,NDIFF13:2;
then A3: Z is open by NDIFF_1:32; then
A4: f is_partial_differentiable_on Z,s
& for z being Point of product S st z in Z holds
(f`partial|(Z,s))/.z = ((f`|Z)/.z) * (reproj(In(s,dom S),0.(product S)))
by A2,Th22;
set PD1 = f`partial|(Z,s);
A5: dom PD1 = Z by A4,NDIFF_5:def 9;
reconsider L10 = reproj(In(s,dom S),0.(product S))
as Lipschitzian LinearOperator of S.In(s,dom S),product S by Th23;
set BL1 = R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),product S);
A6: dom(Z --> L10) = Z & rng(Z --> L10) c= {L10} by FUNCOP_1:13;
L10 in the carrier of
R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),product S)
by LOPBAN_1:def 9; then
{L10} c= the carrier of
R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),product S)
by ZFMISC_1:31; then
A7: rng(Z --> L10) c= the carrier of
R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),product S)
by XBOOLE_1:1; then
reconsider L1 = Z --> L10 as PartFunc of product S,BL1
by A6,RELSET_1:4;
reconsider L100 = L10
as Point of R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),product S)
by LOPBAN_1:def 9;
L1 = Z --> L100;
then A8: L1 is_differentiable_on i,Z by A3,NDIFF13:49;
A9: for z be Point of product S st z in Z holds
(f`partial|(Z,s))/.z = ((f`|Z)/.z) * L1/.z
proof
let z be Point of product S;
assume A10: z in Z;
then A11: L1/.z = L1.z by A6,PARTFUN1:def 6
.= L10 by A10,FUNCOP_1:7;
reconsider H1 = (f`|Z)/.z as Lipschitzian LinearOperator of product S,G
by LOPBAN_1:def 9;
reconsider H2 = L1/.z as Lipschitzian LinearOperator
of S.In(s,dom S),product S by A11;
A13: modetrans(L1/.z,S.In(s,dom S),product S) = H2 by LOPBAN_1:def 11;
(f`partial|(Z,s))/.z = H1*H2 by A2,A3,A10,A11,Th22;
hence (f`partial|(Z,s))/.z = ((f`|Z)/.z) * (L1/.z) by A13,LOPBAN_1:def 11;
end;
A16: f`|Z is_differentiable_on i,Z by A1,NDIFF13:35;
consider B be Lipschitzian BilinearOperator of
R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),product S),
R_NormSpace_of_BoundedLinearOperators(product S,G),
R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),G)
such that
A17: for u be Point of
R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),product S),
v be Point of R_NormSpace_of_BoundedLinearOperators(product S,G)
holds B.(u,v) = v*u by NDIFF13:37;
set w2 = <:L1,f`|Z:>;
A18: dom w2 = dom(f`|Z) /\ dom L1 by FUNCT_3:def 7
.= Z /\ dom L1 by A2,NDIFF_1:def 9
.= Z by A6;
A19: rng w2 c= [:rng L1,rng(f`|Z):] by FUNCT_3:51;
[:rng L1,rng(f`|Z):] c= [:the carrier of
R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),product S),
the carrier of R_NormSpace_of_BoundedLinearOperators(product S,G):]
by ZFMISC_1:96;
then rng w2 c= the carrier of
[:R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),product S),
R_NormSpace_of_BoundedLinearOperators(product S,G):]
by A19,XBOOLE_1:1;
then reconsider w2 as PartFunc of product S,
[:R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),product S),
R_NormSpace_of_BoundedLinearOperators(product S,G):]
by A18,RELSET_1:4;
reconsider W = B*w2 as PartFunc of product S,
R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),G);
A20: W is_differentiable_on i,Z by A8,A16,NDIFF13:38;
dom B = the carrier of
[:R_NormSpace_of_BoundedLinearOperators(S.In(s,dom S),product S),
R_NormSpace_of_BoundedLinearOperators(product S,G):]
by FUNCT_2:def 1;
then rng w2 c= dom B;
then A21: dom W = Z by A18,RELAT_1:27;
for x0 be object st x0 in dom(PD1) holds PD1.x0 = W.x0
proof
let x0 be object;
assume A22: x0 in dom(PD1);
then reconsider x = x0 as Point of product S;
A23: PD1.x0 = PD1/.x by A22,PARTFUN1:def 6
.= ((f`|Z)/.x) * L1/.x by A5,A9,A22
.= B.(L1/.x,(f`|Z)/.x) by A17
.= B.([L1/.x,(f`|Z)/.x]);
A24: dom(f`|Z) = Z by A2,NDIFF_1:def 9;
A25: dom(<:L1,f`|Z:>) = dom L1 /\ dom(f`|Z) by FUNCT_3:def 7
.= Z by A6,A24;
[L1/.x,(f`|Z)/.x] = [L1.x,(f`|Z)/.x] by A5,A6,A22,PARTFUN1:def 6
.= [L1.x,(f`|Z).x] by A5,A22,A24,PARTFUN1:def 6
.= w2.x by A5,A22,A25,FUNCT_3:def 7;
hence PD1.x0 = W.x0 by A5,A22,A23,A25,FUNCT_1:13;
end;
hence PD1 is_differentiable_on i,Z by A5,A20,A21,FUNCT_1:2;
end;
theorem Th26:
for S be RealNormSpace-Sequence,
G be RealNormSpace,
Z be non empty Subset of product S,
f be PartFunc of product S,G,
s be set,
i be Nat
st f is_differentiable_on i+1,Z
& diff(f,i+1,Z) is_continuous_on Z
holds
f`partial|(Z,s) is_differentiable_on i,Z
& diff(f`partial|(Z,s),i,Z) is_continuous_on Z
proof
let S be RealNormSpace-Sequence,
G be RealNormSpace,
Z be non empty Subset of product S,
f be PartFunc of product S,G,
s be set,
i be Nat;
assume A1: f is_differentiable_on i+1,Z
& diff(f,i+1,Z) is_continuous_on Z; then
f is_differentiable_on 0+1,Z;
then A2: f is_differentiable_on Z by NDIFF_6:15,NDIFF13:2;
then A3: Z is open by NDIFF_1:32; then
A4: f is_partial_differentiable_on Z,s
& for z being Point of product S st z in Z holds
(f`partial|(Z,s))/.z = ((f`|Z)/.z) * (reproj(In(s,dom S),0.(product S)))
by A2,Th22;
set PD1 = f`partial|(Z,s);
set E = S.In(s,dom S);
A5: dom PD1 = Z by A4,NDIFF_5:def 9;
reconsider L10 = reproj(In(s,dom S),0.(product S))
as Lipschitzian LinearOperator of S.In(s,dom S),product S by Th23;
set BL1 = R_NormSpace_of_BoundedLinearOperators(E,product S);
A6: dom(Z --> L10) = Z & rng(Z --> L10) c= {L10} by FUNCOP_1:13;
L10 in the carrier of R_NormSpace_of_BoundedLinearOperators(E,product S)
by LOPBAN_1:def 9; then
{L10} c= the carrier of R_NormSpace_of_BoundedLinearOperators(E,product S)
by ZFMISC_1:31; then
A7: rng(Z --> L10) c= the carrier of
R_NormSpace_of_BoundedLinearOperators(E,product S) by XBOOLE_1:1;
reconsider L1 = Z --> L10 as PartFunc of product S,BL1
by RELSET_1:4,A6,A7;
reconsider L100 = L10
as Point of R_NormSpace_of_BoundedLinearOperators(E,product S)
by LOPBAN_1:def 9;
A8: L1 = Z --> L100;
then A9: L1 is_differentiable_on i,Z by A3,NDIFF13:49;
A10: L1 is_differentiable_on i+1,Z by A3,A8,NDIFF13:49; then
A11: diff(L1,i,Z) is_continuous_on Z by NDIFF_1:45,NDIFF_6:14;
A12: for z be Point of product S st z in Z holds
(f`partial|(Z,s))/.z = ((f`|Z)/.z) * L1/.z
proof
let z be Point of product S;
assume A13: z in Z; then
A14: L1/.z = L1.z by A6,PARTFUN1:def 6
.= L10 by FUNCOP_1:7,A13;
reconsider H1 = (f`|Z)/.z as Lipschitzian LinearOperator of product S,G
by LOPBAN_1:def 9;
reconsider H2 = L1/.z as Lipschitzian LinearOperator of
S.In(s,dom S),product S by A14;
A16: modetrans(L1/.z,S.In(s,dom S),product S) = H2 by LOPBAN_1:def 11;
(f`partial|(Z,s))/.z = H1*H2 by A2,A3,A13,A14,Th22;
hence (f`partial|(Z,s))/.z = ((f`|Z)/.z) * (L1/.z)
by A16,LOPBAN_1:def 11;
end;
A19: f`|Z is_differentiable_on i,Z
& diff(f`|Z,i,Z) is_continuous_on Z by A1,NDIFF13:36;
consider B be Lipschitzian BilinearOperator of
R_NormSpace_of_BoundedLinearOperators(E,product S),
R_NormSpace_of_BoundedLinearOperators(product S,G),
R_NormSpace_of_BoundedLinearOperators(E,G)
such that
A20: for u be Point of R_NormSpace_of_BoundedLinearOperators(E,product S),
v be Point of R_NormSpace_of_BoundedLinearOperators(product S,G)
holds B.(u,v) = v*u by NDIFF13:37;
set w2 = <:L1,f`|Z:>;
A21: dom w2 = dom(f`|Z) /\ dom L1 by FUNCT_3:def 7
.= Z /\ dom L1 by A2,NDIFF_1:def 9
.= Z by A6;
A22: rng w2 c= [:rng L1,rng(f`|Z):] by FUNCT_3:51;
[:rng L1,rng(f`|Z):] c= [:the carrier of
R_NormSpace_of_BoundedLinearOperators(E,product S),
the carrier of R_NormSpace_of_BoundedLinearOperators(product S,G):]
by ZFMISC_1:96; then
rng w2 c= the carrier of
[:R_NormSpace_of_BoundedLinearOperators(E,product S),
R_NormSpace_of_BoundedLinearOperators(product S,G):]
by A22,XBOOLE_1:1;
then reconsider w2 as PartFunc of product S,
[:R_NormSpace_of_BoundedLinearOperators(E,product S),
R_NormSpace_of_BoundedLinearOperators(product S,G):]
by RELSET_1:4,A21;
reconsider W = B*w2 as
PartFunc of product S,R_NormSpace_of_BoundedLinearOperators(E,G);
A23: W is_differentiable_on i,Z
& diff(W,i,Z) is_continuous_on Z by NDIFF13:41,A9,A11,A19;
dom B = the carrier of
[:R_NormSpace_of_BoundedLinearOperators(E,product S),
R_NormSpace_of_BoundedLinearOperators(product S,G):]
by FUNCT_2:def 1;
then rng w2 c= dom B;
then A24: dom W = Z by A21,RELAT_1:27;
for x0 be object st x0 in dom(PD1) holds PD1.x0 = W.x0
proof
let x0 be object;
assume A25: x0 in dom(PD1);
then reconsider x = x0 as Point of product S;
A26: PD1.x0 = PD1/.x by A25,PARTFUN1:def 6
.= ((f`|Z)/.x) * L1/.x by A12,A25,A5
.= B.(L1/.x,(f`|Z)/.x) by A20
.= B.([L1/.x,(f`|Z)/.x]);
A27: dom(f`|Z) = Z by A2,NDIFF_1:def 9;
A28: dom(<:L1,f`|Z:>) = dom L1 /\ dom(f`|Z) by FUNCT_3:def 7
.= Z by A6,A27;
[L1/.x,(f`|Z)/.x] = [L1.x,(f`|Z)/.x] by A6,PARTFUN1:def 6,A25,A5
.= [L1.x,(f`|Z).x] by PARTFUN1:def 6,A27,A25,A5
.= w2.x by A5,A25,A28,FUNCT_3:def 7;
hence PD1.x0 = W.x0 by A5,A25,A26,A28,FUNCT_1:13;
end;
hence PD1 is_differentiable_on i,Z
& diff(PD1,i,Z) is_continuous_on Z by A23,FUNCT_1:2,A5,A24;
end;
theorem Th27:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
f be PartFunc of product S,T,
a be Real,
i be set
st Z is open & i in dom S
& f is_partial_differentiable_on Z,i
holds
a(#)f is_partial_differentiable_on Z,i
& (a(#)f)`partial|(Z,i) = a(#)(f`partial|(Z,i))
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
f be PartFunc of product S,T,
a be Real,
i be set;
assume that
A1: Z is open & i in dom S and
A2: f is_partial_differentiable_on Z,i;
A3: Z c= dom f by A2,NDIFF_5:def 8;
then A4: Z c= dom(a(#)f) by VFUNCT_1:def 4;
for x being Point of product S st x in Z holds
(a(#)f)|Z is_partial_differentiable_in x,i
proof
let x be Point of product S;
assume x in Z;
then f|Z is_partial_differentiable_in x,i by A2,NDIFF_5:def 8;
then A5: a(#)(f|Z) is_partial_differentiable_in x,i by A1,NDIFF_5:30;
A6: dom(f|Z) = Z by A3,RELAT_1:62;
A7: dom((a(#)f)|Z) = Z by A4,RELAT_1:62;
for x be Element of product S st x in dom((a(#)f)|Z) holds
((a(#)f)|Z)/.x = a*(f|Z)/.x
proof
let x be Element of product S;
assume A8: x in dom((a(#)f)|Z);
hence ((a(#)f)|Z)/.x = (a(#)f)/.x by PARTFUN1:80
.= a*f/.x by A4,A7,A8,VFUNCT_1:def 4
.= a*(f|Z)/.x by A6,A8,PARTFUN1:80;
end;
hence (a(#)f)|Z is_partial_differentiable_in x,i
by A4,A5,A6,RELAT_1:62,VFUNCT_1:def 4;
end;
hence
A9: a(#)f is_partial_differentiable_on Z,i by A4,NDIFF_5:def 8;
set pfg = a(#)(f`partial|(Z,i));
dom(f`partial|(Z,i)) = Z by A2,NDIFF_5:def 9;
then A10: dom pfg = Z by VFUNCT_1:def 4;
for x being Point of product S st x in Z holds
pfg/.x = partdiff(a(#)f,x,i)
proof
let x be Point of product S;
assume A11: x in Z; then
A12: f is_partial_differentiable_in x,i by A1,A2,NDIFF_5:32;
thus pfg/.x = a*(f`partial|(Z,i))/.x by A10,A11,VFUNCT_1:def 4
.= a*partdiff(f,x,i) by A2,A11,NDIFF_5:def 9
.= partdiff(a(#)f,x,i) by A1,A12,NDIFF_5:30;
end;
hence (a(#)f)`partial|(Z,i) = a(#)(f`partial|(Z,i))
by A9,A10,NDIFF_5:def 9;
end;
theorem Th28:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
f be PartFunc of product S,T,
a be Real,
i be set
st Z is open & i in dom S
& f is_partial_differentiable_on Z,i
holds
-f is_partial_differentiable_on Z,i
& (-f)`partial|(Z,i) = -f`partial|(Z,i)
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
f be PartFunc of product S,T,
a be Real,
i be set;
assume that
A1: Z is open & i in dom S and
A2: f is_partial_differentiable_on Z,i;
A3: -f = (-1)(#)f by VFUNCT_1:23;
hence -f is_partial_differentiable_on Z,i by A1,A2,Th27;
(-1)(#)f is_partial_differentiable_on Z,i
& ((-1)(#)f)`partial|(Z,i) = (-1)(#)(f`partial|(Z,i)) by A1,A2,Th27;
hence (-f)`partial|(Z,i) = -(f`partial|(Z,i)) by A3,VFUNCT_1:23;
end;
theorem
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
f,g be PartFunc of product S,T,
i be set
st Z is open & i in dom S
& f is_partial_differentiable_on Z,i
& g is_partial_differentiable_on Z,i
holds
f-g is_partial_differentiable_on Z,i
& (f-g)`partial|(Z,i) = f`partial|(Z,i) - g`partial|(Z,i)
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
f,g be PartFunc of product S,T,
i be set;
assume that
A1: Z is open & i in dom S and
A2: f is_partial_differentiable_on Z,i and
A3: g is_partial_differentiable_on Z,i;
A4: -g is_partial_differentiable_on Z,i
& (-g)`partial|(Z,i) = -g`partial|(Z,i) by A1,A3,Th28;
A5: f - g = f + -g by VFUNCT_1:25;
hence f-g is_partial_differentiable_on Z,i by A1,A2,A4,Th21;
thus (f-g)`partial|(Z,i)
= f`partial|(Z,i) + -g`partial|(Z,i) by A1,A2,A4,A5,Th21
.= f`partial|(Z,i) - g`partial|(Z,i) by VFUNCT_1:25;
end;
begin :: Higher Order Partial and Total Differentiability
theorem Th30:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f,g be PartFunc of product S,T
st Z is open
& f is_partial_differentiable_on Z,I
& g is_partial_differentiable_on Z,I
holds
f+g is_partial_differentiable_on Z,I
& for i be Nat st 1 <= i <= len I holds
PartDiffSeq(f+g,Z,I,i) = PartDiffSeq(f,Z,I,i) + PartDiffSeq(g,Z,I,i)
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f,g be PartFunc of product S,T;
assume that
A1: Z is open and
A2: f is_partial_differentiable_on Z,I and
A3: g is_partial_differentiable_on Z,I;
1 <= len I by FINSEQ_1:20;
then 1 in dom I by FINSEQ_3:25;
then A6: I.1 in rng I by FUNCT_1:3;
A8: f`partial|(Z,I.1) = PartDiffSeq(f,Z,I,1) by Th13;
A9: g`partial|(Z,I.1) = PartDiffSeq(g,Z,I,1) by Th13;
A10: Partdiff_SP(S,T,I,1)
= R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T) by Th12;
A11: PartDiffSeq(f+g,Z,I,1) = (f+g)`partial|(Z,I.1) by Th13
.= PartDiffSeq(f,Z,I,1) + PartDiffSeq(g,Z,I,1)
by A1,A2,A3,A6,A8,A9,A10,Th21;
defpred P[Nat] means
1 <= $1 & $1 < len I implies
PartDiffSeq(f+g,Z,I,$1) is_partial_differentiable_on Z,I.($1+1)
& PartDiffSeq(f+g,Z,I,$1+1)
= PartDiffSeq(f,Z,I,$1+1) + PartDiffSeq(g,Z,I,$1+1);
A12: P[0];
A13: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A14: P[k];
assume A15: 1 <= k+1 < len I; then
A16: PartDiffSeq(f,Z,I,k+1) is_partial_differentiable_on Z,I.((k+1)+1)
by A2;
A17: PartDiffSeq(g,Z,I,k+1) is_partial_differentiable_on Z,I.((k+1)+1)
by A3,A15;
1 <= (k+1)+1 <= len I by A15,NAT_1:13;
then (k+1)+1 in dom I by FINSEQ_3:25;
then A18: I.((k+1)+1) in rng I by FUNCT_1:3;
then
A19: PartDiffSeq(f,Z,I,k+1) + PartDiffSeq(g,Z,I,k+1)
is_partial_differentiable_on Z,I.((k+1)+1)
& (PartDiffSeq(f,Z,I,k+1) + PartDiffSeq(g,Z,I,k+1))
`partial|(Z,I.((k+1)+1))
= PartDiffSeq(f,Z,I,k+1)`partial|(Z,I.((k+1)+1))
+ PartDiffSeq(g,Z,I,k+1)`partial|(Z,I.((k+1)+1))
by A1,A16,A17,Th21;
A20: Partdiff_SP(S,T,I,(k+1)+1)
= R_NormSpace_of_BoundedLinearOperators(
S.(In(I.((k+1)+1),dom S)),Partdiff_SP(S,T,I,(k+1)))
by A15,Th12;
A21: PartDiffSeq(f,Z,I,k+1)`partial|(Z,I.((k+1)+1))
= PartDiffSeq(f,Z,I,(k+1)+1) by A15,Th13;
A23: (PartDiffSeq(f,Z,I,k+1) + PartDiffSeq(g,Z,I,k+1))
`partial|(Z,I.((k+1)+1))
= PartDiffSeq(f,Z,I,(k+1)+1) + PartDiffSeq(g,Z,I,(k+1)+1)
by A15,A19,A20,A21,Th13;
per cases;
suppose A24: k = 0;
hence PartDiffSeq(f+g,Z,I,k+1)
is_partial_differentiable_on Z,I.((k+1)+1) by A1,A11,A16,A17,A18,Th21;
thus PartDiffSeq(f+g,Z,I,(k+1)+1)
= PartDiffSeq(f,Z,I,(k+1)+1) + PartDiffSeq(g,Z,I,(k+1)+1)
by A11,A15,A23,A24,Th13;
end;
suppose A26: k <> 0;
hence PartDiffSeq(f+g,Z,I,k+1)
is_partial_differentiable_on Z,I.((k+1)+1)
by A1,A14,A15,A16,A17,A18,Th21,NAT_1:13,14;
thus PartDiffSeq(f+g,Z,I,(k+1)+1)
= PartDiffSeq(f,Z,I,(k+1)+1) + PartDiffSeq(g,Z,I,(k+1)+1)
by A14,A15,A23,A26,Th13,NAT_1:13,14;
end;
end;
A27: for k be Nat holds P[k] from NAT_1:sch 2(A12,A13);
hence f+g is_partial_differentiable_on Z,I by A1,A2,A3,A6,Th21;
thus for i be Nat st 1 <= i <= len I holds
PartDiffSeq(f+g,Z,I,i) = PartDiffSeq(f,Z,I,i) + PartDiffSeq(g,Z,I,i)
proof
let i be Nat;
assume A28: 1 <= i <= len I;
per cases;
suppose i = 1;
hence PartDiffSeq(f+g,Z,I,i)
= PartDiffSeq(f,Z,I,i) + PartDiffSeq(g,Z,I,i) by A11;
end;
suppose i <> 1;
then 1 < i by XXREAL_0:1,A28;
then 1+1 <= i by NAT_1:13;
then A29: 2-1 <= i-1 by XREAL_1:9;
then i-1 in NAT by INT_1:3;
then reconsider j = i-1 as Nat;
j < j+1 by NAT_1:16;
then j < len I by A28,XXREAL_0:2;
then PartDiffSeq(f+g,Z,I,j+1)
= PartDiffSeq(f,Z,I,j+1) + PartDiffSeq(g,Z,I,j+1) by A27,A29;
hence PartDiffSeq(f+g,Z,I,i)
= PartDiffSeq(f,Z,I,i) + PartDiffSeq(g,Z,I,i);
end;
end;
end;
theorem Th31:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f be PartFunc of product S,T,
a be Real
st Z is open & f is_partial_differentiable_on Z,I
holds
a(#)f is_partial_differentiable_on Z,I
& for i be Nat st 1 <= i <= len I holds
PartDiffSeq(a(#)f,Z,I,i) = a(#)PartDiffSeq(f,Z,I,i)
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f be PartFunc of product S,T,
a be Real;
assume that
A1: Z is open and
A2: f is_partial_differentiable_on Z,I;
1 <= len I by FINSEQ_1:20;
then 1 in dom I by FINSEQ_3:25;
then A4: I.1 in rng I by FUNCT_1:3;
A6: f`partial|(Z,I.1) = PartDiffSeq(f,Z,I,1) by Th13;
A7: Partdiff_SP(S,T,I,1)
= R_NormSpace_of_BoundedLinearOperators(S.(In(I.1,dom S)),T) by Th12;
A8: PartDiffSeq(a(#)f,Z,I,1) = (a(#)f)`partial|(Z,I.1) by Th13
.= a(#)PartDiffSeq(f,Z,I,1) by A1,A2,A4,A6,A7,Th27;
defpred P[Nat] means
1 <= $1 & $1 < len I implies
PartDiffSeq(a(#)f,Z,I,$1) is_partial_differentiable_on Z,I.($1+1)
& PartDiffSeq(a(#)f,Z,I,$1+1) = a(#)PartDiffSeq(f,Z,I,$1+1);
A9: P[0];
A10: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A11: P[k];
assume A12: 1 <= k+1 < len I; then
A13: PartDiffSeq(f,Z,I,k+1)
is_partial_differentiable_on Z,I.((k+1)+1) by A2;
1 <= (k+1)+1 <= len I by A12,NAT_1:13;
then (k+1)+1 in dom I by FINSEQ_3:25;
then A14: I.((k+1)+1) in rng I by FUNCT_1:3;
then
A15: a(#)PartDiffSeq(f,Z,I,k+1) is_partial_differentiable_on Z,I.((k+1)+1)
& (a(#)(PartDiffSeq(f,Z,I,k+1)))`partial|(Z,I.((k+1)+1))
= a(#)(PartDiffSeq(f,Z,I,k+1)`partial|(Z,I.((k+1)+1)))
by A1,A13,Th27;
A16: Partdiff_SP(S,T,I,(k+1)+1)
= R_NormSpace_of_BoundedLinearOperators(
S.(In(I.((k+1)+1),dom S)),Partdiff_SP(S,T,I,(k+1))) by A12,Th12;
A18: (a(#)PartDiffSeq(f,Z,I,k+1))`partial|(Z,I.((k+1)+1))
= a(#)PartDiffSeq(f,Z,I,(k+1)+1) by A12,A15,A16,Th13;
per cases;
suppose A19: k = 0;
hence PartDiffSeq(a(#)f,Z,I,k+1)
is_partial_differentiable_on Z,I.((k+1)+1) by A1,A8,A13,A14,Th27;
thus PartDiffSeq(a(#)f,Z,I,(k+1)+1)
= a(#)PartDiffSeq(f,Z,I,(k+1)+1) by A8,A12,A18,A19,Th13;
end;
suppose A20: k <> 0;
hence PartDiffSeq(a(#)f,Z,I,k+1)
is_partial_differentiable_on Z,I.((k+1)+1)
by A1,A11,A12,A13,A14,Th27,NAT_1:13,14;
thus PartDiffSeq(a(#)f,Z,I,(k+1)+1)
= a(#)PartDiffSeq(f,Z,I,(k+1)+1) by A11,A12,A18,A20,Th13,NAT_1:13,14;
end;
end;
A22: for k be Nat holds P[k] from NAT_1:sch 2(A9,A10);
hence a(#)f is_partial_differentiable_on Z,I by A1,A2,A4,Th27;
thus for i be Nat st 1 <= i <= len I holds
PartDiffSeq(a(#)f,Z,I,i) = a(#)PartDiffSeq(f,Z,I,i)
proof
let i be Nat;
assume A23: 1 <= i <= len I;
per cases;
suppose i = 1;
hence PartDiffSeq(a(#)f,Z,I,i) = a(#)PartDiffSeq(f,Z,I,i) by A8;
end;
suppose i <> 1;
then 1 < i by XXREAL_0:1,A23;
then 1+1 <= i by NAT_1:13;
then A24: 2-1 <= i-1 by XREAL_1:9;
then i-1 in NAT by INT_1:3;
then reconsider j = i-1 as Nat;
j < j+1 by NAT_1:16;
then j < len I by A23,XXREAL_0:2;
then PartDiffSeq(a(#)f,Z,I,j+1) = a(#)PartDiffSeq(f,Z,I,j+1) by A22,A24;
hence PartDiffSeq(a(#)f,Z,I,i) = a(#)PartDiffSeq(f,Z,I,i);
end;
end;
end;
theorem Th32:
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f be PartFunc of product S,T
st Z is open & f is_partial_differentiable_on Z,I
holds
-f is_partial_differentiable_on Z,I
& for i be Nat st 1 <= i <= len I holds
PartDiffSeq(-f,Z,I,i) = -PartDiffSeq(f,Z,I,i)
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f be PartFunc of product S,T;
assume that
A1: Z is open and
A2: f is_partial_differentiable_on Z,I;
A3: (-1)(#)f = -f by VFUNCT_1:23;
hence -f is_partial_differentiable_on Z,I by A1,A2,Th31;
let i be Nat;
assume 1 <= i <= len I;
hence PartDiffSeq(-f,Z,I,i)
= (-1)(#)PartDiffSeq(f,Z,I,i) by A1,A2,A3,Th31
.= -PartDiffSeq(f,Z,I,i) by VFUNCT_1:23;
end;
theorem
for S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f,g be PartFunc of product S,T
st Z is open
& f is_partial_differentiable_on Z,I
& g is_partial_differentiable_on Z,I
holds
f-g is_partial_differentiable_on Z,I
& for i be Nat st 1 <= i <= len I holds
PartDiffSeq(f-g,Z,I,i) = PartDiffSeq(f,Z,I,i) - PartDiffSeq(g,Z,I,i)
proof
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
I be non empty FinSequence of dom S,
f,g be PartFunc of product S,T;
assume that
A1: Z is open and
A2: f is_partial_differentiable_on Z,I and
A3: g is_partial_differentiable_on Z,I;
A4: f-g = f + -g by VFUNCT_1:25;
A5: -g is_partial_differentiable_on Z,I
& for i be Nat st 1 <= i <= len I holds
PartDiffSeq(-g,Z,I,i) = -PartDiffSeq(g,Z,I,i) by A1,A3,Th32;
hence f-g is_partial_differentiable_on Z,I by A1,A2,A4,Th30;
let i be Nat;
assume A6: 1 <= i <= len I;
hence PartDiffSeq(f-g,Z,I,i)
= PartDiffSeq(f,Z,I,i) + PartDiffSeq(-g,Z,I,i) by A1,A2,A4,A5,Th30
.= PartDiffSeq(f,Z,I,i) + -PartDiffSeq(g,Z,I,i) by A1,A3,A6,Th32
.= PartDiffSeq(f,Z,I,i) - PartDiffSeq(g,Z,I,i) by VFUNCT_1:25;
end;
definition
let S be RealNormSpace-Sequence,
T be RealNormSpace,
Z be Subset of product S,
f be PartFunc of product S,T;
let k be Nat;
pred f is_partial_differentiable_up_to_order k,Z means
for I being non empty FinSequence of dom S
st len I <= k holds f is_partial_differentiable_on Z,I;
end;
theorem
for G being RealNormSpace-Sequence,
X being non empty Subset of product G
st X is open
holds for n being Nat,
F being RealNormSpace,
f being PartFunc of product G,F
st f is_differentiable_on n,X
holds for I being non empty FinSequence of dom G
st len I <= n holds f is_partial_differentiable_on X,I
proof
let G be RealNormSpace-Sequence,
X be non empty Subset of product G;
assume A1: X is open;
defpred P[Nat] means
for F being RealNormSpace,
f being PartFunc of product G,F
st f is_differentiable_on $1,X
holds for I being non empty FinSequence of dom G
st len I <= $1 holds f is_partial_differentiable_on X,I;
A2: P[0];
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A4: P[n];
let F be RealNormSpace,
f be PartFunc of product G,F;
assume A5: f is_differentiable_on n+1,X;
per cases;
suppose A6: n = 0;
then A7: f is_differentiable_on X by A5,NDIFF13:2,NDIFF_6:15;
thus for I being non empty FinSequence of dom G
st len I <= n+1 holds f is_partial_differentiable_on X,I
proof
let I be non empty FinSequence of dom G;
assume A8: len I <= n+1;
1 <= len I by NAT_1:14;
hence f is_partial_differentiable_on X,I
by A1,A6,A7,A8,Th22,XXREAL_0:1;
end;
end;
suppose A11: n <> 0;
A12: f is_differentiable_on n,X by A5,NAT_1:11,NDIFF_6:17;
thus for I being non empty FinSequence of dom G
st len I <= n+1 holds f is_partial_differentiable_on X,I
proof
let I be non empty FinSequence of dom G;
assume A13: len I <= n+1;
per cases;
suppose len I <> n+1;
then len I < n+1 by A13,XXREAL_0:1;
hence f is_partial_differentiable_on X,I by A4,A12,NAT_1:13;
end;
suppose A14: len I = n+1;
then 1 <= len I by NAT_1:11;
then A15: 1 in dom I by FINSEQ_3:25;
then I.1 in rng I by FUNCT_1:3;
then reconsider I1 = I.1 as Element of dom G;
set J1 = <*(I/.1)*>;
set Jn = I /^ 1;
A16: I = J1^Jn by FINSEQ_5:29;
A17: J1 = <*I1*> by A15,PARTFUN1:def 6;
1 <= len I by A14,NAT_1:11;
then A18: len Jn = n+1 - 1 by A14,RFINSEQ:def 1
.= n;
then reconsider Jn as non empty FinSequence of dom G by A11;
A19: J1.1 = I1 & len J1 = 1 by A15,FINSEQ_1:40,PARTFUN1:def 6;
reconsider J1 as non empty FinSequence of dom G;
A20: f`partial|(X,I1) is_differentiable_on n,X by A5,Th25;
Partdiff_SP(G,F,J1,len J1)
= R_NormSpace_of_BoundedLinearOperators((G.(In(I1,dom G))),F)
by A19,Th12;
then f`partial|(X,J1) is_differentiable_on n,X by A17,A20,Th15;
then A22: f`partial|(X,J1) is_partial_differentiable_on X,Jn
by A4,A18;
f is_differentiable_on 1,X by A5,NAT_1:11,NDIFF_6:17;
then f is_differentiable_on X by NDIFF13:2,NDIFF_6:15;
then f is_partial_differentiable_on X,J1
by A1,Th22,FINSEQ_1:40;
hence f is_partial_differentiable_on X,I by A16,A22,Th20;
end;
end;
end;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th35:
for G being RealNormSpace-Sequence,
X being non empty Subset of product G
st X is open
holds for n being Nat,
F being RealNormSpace,
f being PartFunc of product G,F
st f is_differentiable_on n,X
& diff(f,n,X) is_continuous_on X
holds for I being non empty FinSequence of dom G
st len I <= n holds
f is_partial_differentiable_on X,I
& f`partial|(X,I) is_continuous_on X
proof
let G be RealNormSpace-Sequence,
X be non empty Subset of product G;
assume A1: X is open;
defpred P[Nat] means
for F being RealNormSpace,
f being PartFunc of product G,F
st f is_differentiable_on $1,X
& diff(f,$1,X) is_continuous_on X
holds for I being non empty FinSequence of dom G
st len I <= $1 holds
f is_partial_differentiable_on X,I
& f`partial|(X,I) is_continuous_on X;
A2: P[0];
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A4: P[n];
let F be RealNormSpace,
f be PartFunc of product G,F;
assume A5: f is_differentiable_on n+1,X
& diff(f,n+1,X) is_continuous_on X;
per cases;
suppose A6: n = 0; then
A8: f is_differentiable_on X by A5,NDIFF13:2,NDIFF_6:15;
A9: diff(f,n+1,X) = (f|X)`|X by A6,NDIFF_6:11
.= f`|X by A8,NDIFF13:3;
A10: diff_SP(n+1,product G,F)
= R_NormSpace_of_BoundedLinearOperators(product G,F) by A6,NDIFF_6:7;
let I be non empty FinSequence of dom G;
assume A11: len I <= n+1;
A12: 1 <= len I by NAT_1:14;
then A13: len I = 1 by A6,A11,XXREAL_0:1;
A14: I = <*I.1*> by A6,A11,A12,FINSEQ_1:40,XXREAL_0:1;
1 in dom I by A12,FINSEQ_3:25;
then I.1 in rng I by FUNCT_1:3;
then reconsider I1 = I.1 as Element of dom G;
A15: f is_partial_differentiable_on X,I1
& f`partial|(X,I1) is_continuous_on X
by A1,A5,A8,A9,A10,NDIFF_5:57;
hence f is_partial_differentiable_on X,I
by A6,A11,A12,XXREAL_0:1;
Partdiff_SP(G,F,I,len I)
= R_NormSpace_of_BoundedLinearOperators((G.(In(I1,dom G))),F)
by A13,Th12;
hence f`partial|(X,I) is_continuous_on X by A14,A15,Th15;
end;
suppose A16: n <> 0;
A17: f is_differentiable_on n,X by A5,NAT_1:11,NDIFF_6:17;
A18: diff(f,n,X) is_continuous_on X by A5,NDIFF_1:45,NDIFF_6:14;
thus for I being non empty FinSequence of dom G
st len I <= n+1 holds
f is_partial_differentiable_on X,I
& f`partial|(X,I) is_continuous_on X
proof
let I be non empty FinSequence of dom G;
assume A19: len I <= n+1;
per cases;
suppose len I <> n+1;
then len I < n+1 by A19,XXREAL_0:1;
then len I <= n by NAT_1:13;
hence f is_partial_differentiable_on X,I
& f`partial|(X,I) is_continuous_on X by A4,A17,A18;
end;
suppose A20: len I = n+1;
then 1 <= len I by NAT_1:11;
then A21: 1 in dom I by FINSEQ_3:25;
then I.1 in rng I by FUNCT_1:3;
then reconsider I1 = I.1 as Element of dom G;
set J1 = <*(I/.1)*>;
set Jn = I /^ 1;
A22: I = J1^Jn by FINSEQ_5:29;
A23: J1 = <*I1*> by A21,PARTFUN1:def 6;
1 <= len I by A20,NAT_1:11;
then A24: len Jn = n+1 - 1 by A20,RFINSEQ:def 1
.= n;
then reconsider Jn as non empty FinSequence of dom G by A16;
A25: J1.1 = I1 & len J1 = 1 by A21,FINSEQ_1:40,PARTFUN1:def 6;
reconsider J1 as non empty FinSequence of dom G;
A26: f`partial|(X,I1) is_differentiable_on n,X
& diff(f`partial|(X,I1),n,X) is_continuous_on X by A5,Th26;
A27: Partdiff_SP(G,F,J1,len J1)
= R_NormSpace_of_BoundedLinearOperators((G.(In(I1,dom G))),F)
by A25,Th12;
then
A28: f`partial|(X,J1) is_differentiable_on n,X by A23,A26,Th15;
B28: diff(f`partial|(X,J1),n,X) is_continuous_on X
by A23,A26,A27,Th15;
then
A29: f`partial|(X,J1) is_partial_differentiable_on X,Jn
& f`partial|(X,J1)`partial|(X,Jn) is_continuous_on X
by A4,A24,A28;
f is_differentiable_on 1,X by A5,NAT_1:11,NDIFF_6:17;
then f is_differentiable_on X by NDIFF13:2,NDIFF_6:15;
then f is_partial_differentiable_on X,J1
by A1,Th22,FINSEQ_1:40;
hence f is_partial_differentiable_on X,I by A22,A29,Th20;
f`partial|(X,J1)`partial|(X,Jn) = f`partial|(X,I)
& Partdiff_SP(G,Partdiff_SP(G,F,J1,len J1),Jn,len Jn)
= Partdiff_SP(G,F,I,len I) by A22,Th18;
hence f`partial|(X,I) is_continuous_on X by A4,A24,A28,B28;
end;
end;
end;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem
for G being RealNormSpace-Sequence,
X being non empty open Subset of product G,
F being RealNormSpace,
f being PartFunc of product G,F
for n being Nat st 1 <= n
holds
(f is_differentiable_on n,X & diff(f,n,X) is_continuous_on X)
iff
for I being non empty FinSequence of dom G st len I <= n holds
f is_partial_differentiable_on X,I
& f`partial|(X,I) is_continuous_on X
proof
let G be RealNormSpace-Sequence,
X be non empty open Subset of product G,
F be RealNormSpace,
f be PartFunc of product G,F;
defpred P[Nat] means
for F being RealNormSpace,
f being PartFunc of product G,F
st 1 <= $1
& for I being non empty FinSequence of dom G st len I <= $1 holds
f is_partial_differentiable_on X,I
& f`partial|(X,I) is_continuous_on X
holds
f is_differentiable_on $1,X & diff(f,$1,X) is_continuous_on X;
A2: P[0];
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A4: P[n];
let F be RealNormSpace,
f be PartFunc of product G,F;
assume A5: 1 <= n+1
& for I being non empty FinSequence of dom G st len I <= n+1 holds
f is_partial_differentiable_on X,I
& f`partial|(X,I) is_continuous_on X;
A6: for i being set st i in dom G holds
f is_partial_differentiable_on X,i
& f`partial|(X,i) is_continuous_on X
proof
let i be set;
assume i in dom G;
then reconsider i0 = i as Element of dom G;
set I = <*i0*>;
A7: len I = 1 & I.1 = i0 by FINSEQ_1:40;
reconsider I as non empty FinSequence of dom G;
A8: f is_partial_differentiable_on X,I
& f`partial|(X,I) is_continuous_on X by A5,A7;
hence f is_partial_differentiable_on X,i;
Partdiff_SP(G,F,I,len I)
= R_NormSpace_of_BoundedLinearOperators((G.(In(i0,dom G))),F)
by A7,Th12;
hence f`partial|(X,i) is_continuous_on X by A8,Th15;
end;
then A10: f is_differentiable_on X & f`|X is_continuous_on X
by NDIFF_5:57;
per cases;
suppose A11: n = 0;
hence f is_differentiable_on n+1,X by A10,NDIFF_6:15,NDIFF13:2;
diff(f,(n+1),X) = (f|X)`|X by A11,NDIFF_6:11
.= f`|X by A10,NDIFF13:3;
hence diff(f,n+1,X) is_continuous_on X by A10,A11,NDIFF_6:7;
end;
suppose A14: n <> 0;
then A15: 1 <= n by NAT_1:14;
A16: for i be set st i in dom G holds
f`partial|(X,i) is_differentiable_on n,X
& diff(f`partial|(X,i),n,X) is_continuous_on X
proof
let i be set;
assume i in dom G;
then reconsider i0 = i as Element of dom G;
set J1 = <*i0*>;
A17: J1.1 = i0 & len J1 = 1 by FINSEQ_1:40;
reconsider J1 as non empty FinSequence of dom G;
for J2 being non empty FinSequence of dom G st len J2 <= n holds
f`partial|(X,i) is_partial_differentiable_on X,J2
& (f`partial|(X,i))`partial|(X,J2) is_continuous_on X
proof
let J2 be non empty FinSequence of dom G;
assume A18: len J2 <= n;
set I = J1^J2;
len I = len J1 + len J2 by FINSEQ_1:22;
then len I <= n+1 by A17,A18,XREAL_1:7;
then A19: f is_partial_differentiable_on X,I
& f`partial|(X,I) is_continuous_on X by A5;
A20: f is_partial_differentiable_on X,J1
& f`partial|(X,J1) is_partial_differentiable_on X,J2 by A19,Th20;
A21: f`partial|(X,J1)`partial|(X,J2) = f`partial|(X,I)
& Partdiff_SP(G,Partdiff_SP(G,F,J1,len J1),J2,len J2)
= Partdiff_SP(G,F,I,len I) by Th18;
A22: Partdiff_SP(G,F,J1,len J1)
= R_NormSpace_of_BoundedLinearOperators((G.(In(i,dom G))),F)
by A17,Th12;
hence f`partial|(X,i) is_partial_differentiable_on X,J2
by A20,Th15;
thus (f`partial|(X,i))`partial|(X,J2) is_continuous_on X
by A19,A21,A22,Th15;
end;
hence f`partial|(X,i) is_differentiable_on n,X
& diff(f`partial|(X,i),n,X) is_continuous_on X by A4,A15;
end;
A25: for x be Point of product G st x in X holds
for dx be Point of product G
ex w being FinSequence of F st dom w = dom G
& (for i being set st i in dom G holds
w.i = (f`partial|(X,i)/.x).((proj(In(i,dom G)).dx)))
& ((f`|X)/.x).dx = Sum w
proof
let x be Point of product G;
assume A26: x in X;
let dx be Point of product G;
consider w being FinSequence of F such that
A27: (dom w = dom G
& (for i being set st i in dom G holds
w.i = (partdiff(f,x,i)).((proj(In(i,dom G))).dx))
& (diff(f,x)).dx = Sum w) by A6,A26,NDIFF_5:56;
take w;
thus dom w = dom G by A27;
thus for i being set st i in dom G holds
w.i = (f`partial|(X,i)/.x).((proj(In(i,dom G)).dx))
proof
let i be set;
assume A28: i in dom G;
then A29: w.i = (partdiff(f,x,i)).((proj(In(i,dom G))).dx) by A27;
f is_partial_differentiable_on X,i by A6,A28;
hence thesis by A26,A29,NDIFF_5:def 9;
end;
thus ((f`|X)/.x).dx = Sum w by A10,A26,A27,NDIFF_1:def 9;
end;
set GF = R_NormSpace_of_BoundedLinearOperators(product G,F);
A30: for i being set st i in dom G
ex Wi be PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(product G,F)
st Wi is_differentiable_on n,X
& diff(Wi,n,X) is_continuous_on X
& dom Wi = X
& for x be Point of product G st x in X holds
Wi.x = (f`partial|(X,i)/.x)*proj(In(i,dom G))
proof
let i be set;
assume A31: i in dom G;
set Gi = R_NormSpace_of_BoundedLinearOperators(
product G,G.(In(i,dom G)));
set GiF = R_NormSpace_of_BoundedLinearOperators(G.(In(i,dom G)),F);
proj(In(i,dom G))
is Lipschitzian LinearOperator of product G,G.In(i,dom G) by Th24;
then reconsider Li = proj(In(i,dom G)) as Point of Gi
by LOPBAN_1:def 9;
A32: dom(X --> Li) = X & rng(X --> Li) c= {Li} by FUNCOP_1:13;
reconsider L = X --> Li as PartFunc of product G,Gi by A32,RELSET_1:4;
consider B be Lipschitzian BilinearOperator of Gi,GiF,GF such that
A33: for u be Point of Gi, v be Point of GiF holds
B.(u,v) = v*u by NDIFF13:37;
set w = <:L,f`partial|(X,i):>;
f is_partial_differentiable_on X,i by A6,A31;
then A34: dom(f`partial|(X,i)) = X by NDIFF_5:def 9;
A35: dom w = dom L /\ (dom(f`partial|(X,i))) by FUNCT_3:def 7
.= X by A32,A34;
A36: rng w c= [:rng L,rng(f`partial|(X,i)):] by FUNCT_3:51;
A37: [:rng L,rng(f`partial|(X,i)):]
c= [:[#]Gi,[#]GiF:] by ZFMISC_1:96;
then rng w c= the carrier of [:Gi,GiF:] by A36,XBOOLE_1:1;
then reconsider w as PartFunc of product G,[:Gi,GiF:]
by A35,RELSET_1:4;
reconsider W = B*w as PartFunc of product G,GF;
A38: L is_differentiable_on n,X by NDIFF13:49;
L is_differentiable_on n+1,X by NDIFF13:49;
then A39: diff(L,n,X) is_continuous_on X by NDIFF_1:45,NDIFF_6:14;
A40: f`partial|(X,i) is_differentiable_on n,X by A16,A31;
A41: diff(f`partial|(X,i),n,X) is_continuous_on X by A16,A31;
take W;
A42: the carrier of [:Gi,GiF:] = dom B by FUNCT_2:def 1;
then A43: dom W = X by A35,A36,A37,RELAT_1:27,XBOOLE_1:1;
for x be Point of product G st x in X holds
W.x = (f`partial|(X,i)/.x)*proj(In(i,dom G))
proof
let x be Point of product G;
assume A44: x in X;
reconsider fpi = (f`partial|(X,i))/.x
as Lipschitzian LinearOperator of G.(In(i,dom G)),F
by LOPBAN_1:def 9;
reconsider fLi = Li as Lipschitzian LinearOperator of
product G,G.(In(i,dom G)) by LOPBAN_1:def 9;
A45: modetrans(fpi,G.(In(i,dom G)),F)
= (f`partial|(X,i))/.x by LOPBAN_1:def 11;
thus W.x = B.(w.x) by A43,A44,FUNCT_1:12
.= B.([L.x,f`partial|(X,i).x])
by A32,A34,A44,FUNCT_3:49
.= B.([Li,f`partial|(X,i).x]) by A44,FUNCOP_1:7
.= B.(Li,f`partial|(X,i)/.x) by A34,A44,PARTFUN1:def 6
.= (f`partial|(X,i)/.x)*Li by A33
.= (f`partial|(X,i)/.x)*proj(In(i,dom G))
by A45,LOPBAN_1:def 11;
end;
hence thesis by A35,A36,A37,A38,A39,A40,A41,A42,
NDIFF13:41,RELAT_1:27,XBOOLE_1:1;
end;
set PGF = R_NormSpace_of_BoundedLinearOperators(product G,F);
defpred P1[object,object] means
ex Wi be PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(product G,F)
st $2 = Wi
& Wi is_differentiable_on n,X
& diff(Wi,n,X) is_continuous_on X
& dom Wi = X
& for x be Point of product G st x in X holds
Wi.x = (f`partial|(X,In($1,dom G))/.x)*proj(In($1,dom G));
A47: for i being object st i in dom G holds
ex y being object st
(y in PFuncs(the carrier of product G,the carrier of PGF) & P1[i,y])
proof
let i be object;
assume A48: i in dom G;
reconsider i0 = i as set by TARSKI:1;
consider Wi be PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(product G,F)
such that
A49: Wi is_differentiable_on n,X
& diff(Wi,n,X) is_continuous_on X
& dom Wi = X
& for x be Point of product G st x in X holds
Wi.x = (f`partial|(X,i0)/.x)*proj(In(i,dom G)) by A30,A48;
take y = Wi;
In(i,dom G) = i by A48,SUBSET_1:def 8;
hence thesis by A49,PARTFUN1:45;
end;
A51: (the carrier of product G) --> 0.PGF
in PFuncs(the carrier of product G,the carrier of PGF)
by PARTFUN1:45;
consider W being Function of dom G,
PFuncs(the carrier of product G,the carrier of PGF)
such that
A52: for i being object st i in dom G holds P1[i,W.i]
from FUNCT_2:sch 1(A47);
A53: for i being set st i in dom G
ex Wi be PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(product G,F)
st W.i = Wi
& Wi is_differentiable_on n,X
& diff(Wi,n,X) is_continuous_on X
& dom Wi = X
& for x be Point of product G st x in X holds
(W.i).x = (f`partial|(X,i)/.x)*proj(In(i,dom G))
proof
let i be set;
assume A54: i in dom G;
then consider Wi be PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(product G,F)
such that
A55: W.i = Wi
& Wi is_differentiable_on n,X
& diff(Wi,n,X) is_continuous_on X
& dom Wi = X
& for x be Point of product G st x in X holds
Wi.x = (f`partial|(X,In(i,dom G))/.x)*proj(In(i,dom G))
by A52;
take Wi;
In(i,dom G) = i by A54,SUBSET_1:def 8;
hence thesis by A55;
end;
reconsider nn = n as non empty Nat by A14;
A56: dom W = dom G by A51,FUNCT_2:def 1
.= Seg len G by FINSEQ_1:def 3;
then reconsider W0 = W as FinSequence by FINSEQ_1:def 2;
for i being Nat st i in dom W0 holds
W0.i in the carrier of
RVectSp_Continuously_differentiable_Funcs(X,GF,nn)
proof
let i be Nat;
assume i in dom W0;
then consider Wi be PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(product G,F)
such that
A57: W.i = Wi
& Wi is_differentiable_on n,X
& diff(Wi,n,X) is_continuous_on X
& dom Wi = X
& for x be Point of product G st x in X holds
Wi.x = (f`partial|(X,In(i,dom G))/.x)*proj(In(i,dom G))
by A52,A56;
thus W0.i in the carrier of
RVectSp_Continuously_differentiable_Funcs(X,GF,nn) by A57;
end;
then reconsider W0 as FinSequence of
the carrier of RVectSp_Continuously_differentiable_Funcs(X,GF,nn)
by FINSEQ_2:12;
Sum W0 in the carrier of
RVectSp_Continuously_differentiable_Funcs(X,GF,nn);
then
A58: ex f be PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(product G,F)
st Sum W0 = f & dom f = X & f is_differentiable_on nn,X
& diff(f,nn,X) is_continuous_on X;
then reconsider Sw = Sum W0 as PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(product G,F);
for x be Point of product G st x in dom(f`|X) holds (f`|X).x = Sw.x
proof
let x be Point of product G;
assume A59: x in dom(f`|X);
then A60: x in X by A10,NDIFF_1:def 9;
then Sw.x = Sw/.x by A58,PARTFUN1:def 6;
then reconsider Swx = Sw.x as Lipschitzian LinearOperator of
product G,F by LOPBAN_1:def 9;
reconsider Fx = (f`|X)/.x as Lipschitzian LinearOperator of
product G,F by LOPBAN_1:def 9;
defpred PF1[Nat,object] means $2 = (W.$1)/.x;
A61: for k being Nat st k in Seg len G holds
ex x being Element of the carrier of
R_NormSpace_of_BoundedLinearOperators(product G,F) st PF1[k,x];
consider Wx be FinSequence of
the carrier of R_NormSpace_of_BoundedLinearOperators(product G,F)
such that
A62: dom Wx = Seg len G
& for k being Nat st k in Seg len G holds PF1[k,Wx.k]
from FINSEQ_1:sch 5(A61);
A63: dom Wx = dom G by A62,FINSEQ_1:def 3;
A64: for i be Nat st i in dom Wx holds Wx/.i = (W.i)/.x
proof
let i be Nat;
assume A65: i in dom Wx;
then Wx.i = (W.i)/.x by A62;
hence thesis by A65,PARTFUN1:def 6;
end;
A66: dom Wx = dom W0 by A51,A63,FUNCT_2:def 1;
B66: for i be Nat st i in dom Wx holds
ex Wi be PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(product G,F)
st Wi = W0.i & Wx/.i = Wi/.x
proof
let i be Nat;
assume A67: i in dom Wx;
consider Wi be PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(product G,F)
such that A68: Wi = W.i;
take Wi;
thus thesis by A64,A67,A68;
end;
B69: for dx be Point of product G holds Fx.dx = Swx.dx
proof
let dx be Point of product G;
consider w being FinSequence of F such that
A70: dom w = dom G
& (for i being set st i in dom G holds
w.i = (f`partial|(X,i)/.x).((proj(In(i,dom G)).dx)))
& ((f`|X)/.x).dx = Sum w by A25,A60;
for i be Nat st i in dom w holds w.i = (Wx/.i).dx
proof
let i be Nat;
assume A71: i in dom w;
then A72: w.i = (f`partial|(X,i)/.x).((proj(In(i,dom G)).dx))
by A70;
consider Wi be PartFunc of product G,
R_NormSpace_of_BoundedLinearOperators(product G,F)
such that
A73: W.i = Wi
& Wi is_differentiable_on n,X
& diff(Wi,n,X) is_continuous_on X
& dom Wi = X
& for x be Point of product G st x in X holds
(W.i).x = (f`partial|(X,i)/.x)*proj(In(i,dom G))
by A53,A70,A71;
A74: (W.i).x = (f`partial|(X,i)/.x)*proj(In(i,dom G))
by A60,A73;
A75: (W.i).x = (W.i)/.x by A60,A73,PARTFUN1:def 6;
dom proj(In(i,dom G)) = the carrier of product G
by FUNCT_2:def 1;
hence w.i = ((W.i)/.x).dx by A72,A74,A75,FUNCT_1:13
.= (Wx/.i).dx by A63,A64,A70,A71;
end;
then Sum w = (Sum Wx).dx by A63,A70,Th2;
hence Fx.dx = Swx.dx by A60,A66,B66,A70,Th11;
end;
thus (f`|X).x = (f`|X)/.x
by A59,PARTFUN1:def 6
.= Sw.x by B69,FUNCT_2:63;
end;
then f`|X = Sum W0 by A10,A58,NDIFF_1:def 9;
then f`|X in the carrier of
RVectSp_Continuously_differentiable_Funcs(X,GF,nn);
then
ex g be PartFunc of product G,GF
st g = f`|X & dom g = X & g is_differentiable_on nn,X
& diff(g,nn,X) is_continuous_on X;
hence f is_differentiable_on n+1,X
& diff(f,n+1,X) is_continuous_on X by A10,NDIFF13:32;
end;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis by Th35;
end;