:: Contracting Mapping on Normed Linear Space
:: by Keiichi Miyajima , Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received August 19, 2012
:: Copyright (c) 2012-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PRE_TOPC, NORMSP_1, FUNCT_1, ARYTM_1, NAT_1, SUBSET_1, NUMBERS,
CARD_1, XXREAL_0, FUNCT_7, REAL_1, ARYTM_3, RELAT_1, ORDINAL2, SEQ_1,
SEQ_2, POWER, RSSPACE3, LOPBAN_1, ORDEQ_01, STRUCT_0, COMPLEX1, VALUED_1,
ALI2, SUPINF_2, XBOOLE_0, ABIAN, INTEGRA1, FINSEQ_1, TARSKI, INTEGRA5,
CARD_3, XXREAL_1, PARTFUN1, RLVECT_1, SEQ_4, FUNCT_2, RCOMP_1, VALUED_0,
XXREAL_2, FCONT_1, ALGSTR_0, CFCONT_1, MEASURE5, RLSUB_1, RELAT_2,
REWRITE1, NFCONT_1, C0SP2, RSSPACE, RSSPACE4, FUNCOP_1, REALSET1,
FDIFF_1, PREPOWER, INTEGRA7, METRIC_1, SERIES_1, SIN_COS, SEQFUNC,
REAL_NS1, FINSEQ_2, EUCLID, NEWTON, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, PARTFUN2, NUMBERS, XXREAL_0, XREAL_0, REAL_1, NAT_1,
VALUED_0, COMPLEX1, XCMPLX_0, XXREAL_2, FUNCOP_1, FINSEQ_1, VALUED_1,
FINSEQ_2, SEQ_1, SEQ_2, NEWTON, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1,
FUNCT_7, ABIAN, PREPOWER, POWER, SERIES_1, SEQFUNC, MEASURE5, SIN_COS,
TAYLOR_1, INTEGRA1, INTEGRA5, INTEGRA7, STRUCT_0, ALGSTR_0, PRE_TOPC,
RLVECT_1, RLSUB_1, NORMSP_0, NORMSP_1, VFUNCT_1, RSSPACE, EUCLID,
RSSPACE3, LOPBAN_1, NFCONT_1, INTEGR19, RSSPACE4, REAL_NS1, PDIFF_1,
INTEGR15, INTEGR18, NFCONT_3, NDIFF_3, NFCONT_2, NFCONT_4;
constructors REAL_1, ABIAN, SEQ_1, SEQ_2, RSSPACE3, RELSET_1, SEQ_4, VFUNCT_1,
PDIFF_1, INTEGRA5, NFCONT_3, RLSUB_1, PARTFUN2, FCONT_1, NFCONT_1,
NDIFF_1, NDIFF_3, RSSPACE4, SEQFUNC, INTEGR18, RVSUM_1, BINOP_2,
INTEGR19, INTEGR15, NFCONT_4, FDIFF_1, VALUED_2, PREPOWER, INTEGRA7,
COMSEQ_2, COMSEQ_3, SIN_COS, TAYLOR_1, NFCONT_2, C0SP2;
registrations STRUCT_0, NAT_1, VALUED_1, NORMSP_0, XXREAL_0, NUMBERS,
XBOOLE_0, FUNCT_1, FUNCT_2, XREAL_0, MEMBERED, NORMSP_1, RELAT_1,
FINSEQ_2, RELSET_1, INTEGRA1, ORDINAL1, FUNCOP_1, NEWTON, NFCONT_3,
XXREAL_2, RSSPACE4, RCOMP_1, RLVECT_1, REAL_NS1, VALUED_0, FINSEQ_1,
FDIFF_1, FCONT_1, EUCLID, MEASURE5, VALUED_2, FCONT_3, POWER, NFCONT_4,
PREPOWER;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions ABIAN, NORMSP_0, FDIFF_1, RLSUB_1, INTEGR15, NFCONT_2;
equalities SUBSET_1, STRUCT_0, ALGSTR_0, NORMSP_0, RSSPACE4, RLVECT_1,
FINSEQ_1, RCOMP_1, EUCLID, INTEGRA5;
expansions ABIAN, NORMSP_0, FDIFF_1, FINSEQ_1, INTEGRA5, NFCONT_2;
theorems ABSVALUE, RLVECT_1, NORMSP_0, XCMPLX_1, SEQ_1, SEQ_2, SERIES_1,
TAYLOR_1, PARTFUN1, PARTFUN2, FDIFF_2, INTEGRA7, FUNCT_1, NAT_1, POWER,
FUNCT_2, NORMSP_1, XREAL_1, RSSPACE3, LOPBAN_1, FUNCT_7, XXREAL_0,
XREAL_0, ORDINAL1, RELAT_1, TARSKI, RSSPACE4, RSSPACE, NFCONT_1,
NFCONT_3, RLSUB_1, FCONT_1, SEQ_4, VFUNCT_1, NEWTON, XBOOLE_0, RCOMP_1,
FUNCOP_1, CARD_1, NDIFF_3, SIN_COS, COMSEQ_2, INTEGRA2, XXREAL_1,
RVSUM_1, COMPLEX1, NDIFF_4, PDIFF_1, FDIFF_1, ROLLE, VALUED_1, XBOOLE_1,
INTEGR19, REAL_NS1, INTEGRA5, PREPOWER, NFCONT_4, HOLDER_1, INT_1,
RELSET_1, NFCONT_2;
schemes SEQ_1, NAT_1, XBOOLE_0, FUNCT_2, PARTFUN2;
begin :: The Principle of Contracting Mapping on Normed Linear Space
reserve n for non zero Element of NAT;
reserve a,b,r,t for Real;
definition
let f be Function;
attr f is with_unique_fixpoint means
ex x being set st x is_a_fixpoint_of f &
for y being set st y is_a_fixpoint_of f holds x = y;
end;
theorem
for x being set holds x is_a_fixpoint_of {[x,x]}
proof
let x be set;
A1: [x,x] in {[x,x]} by TARSKI:def 1;
dom {[x,x]} = {x} by RELAT_1:9;
hence x in dom {[x,x]} by TARSKI:def 1;
hence x = {[x,x]}.x by A1,FUNCT_1:def 2;
end;
theorem Th2:
for x,y,z being set st x is_a_fixpoint_of {[y,z]} holds x = y
proof
let x,y,z be set;
assume
A1: x in dom {[y,z]};
dom {[y,z]} = {y} by RELAT_1:9;
hence thesis by A1,TARSKI:def 1;
end;
registration
let x be set;
cluster {[x,x]} -> with_unique_fixpoint;
coherence
proof
set f = {[x,x]};
A1: dom f = {x} by RELAT_1:9;
take x;
thus x is_a_fixpoint_of f
proof
thus
A2: x in dom f by A1,TARSKI:def 1;
[x,x] in f by TARSKI:def 1;
hence x = f.x by A2,FUNCT_1:def 2;
end;
let b be set;
assume b is_a_fixpoint_of f;
then b = x by Th2;
hence thesis;
end;
end;
theorem Th3:
for X being RealNormSpace, x being Point of X holds
(for e being Real st e > 0 holds ||.x.|| < e) implies x = 0.X
proof
let X be RealNormSpace, x be Point of X;
assume
A1: for e being Real st e > 0 holds ||.x.|| < e;
assume x <> 0.X;
then 0 <> ||.x.|| by NORMSP_0:def 5;
hence contradiction by A1;
end;
theorem
for X being RealNormSpace, x,y being Point of X holds
(for e being Real st e > 0 holds ||.x-y.|| < e) implies x = y
proof
let X be RealNormSpace, x,y be Point of X;
assume for e being Real st e > 0 holds ||.x-y.|| <e;
then x-y = 0.X by Th3;
hence thesis by RLVECT_1:21;
end;
theorem
for K, L, e being Real st 0 < K & K < 1 & 0 < e
ex n being Nat st |. L*(K to_power n) .| < e
proof
let K, L, e be Real such that
A1: 0 < K and
A2: K < 1 and
A3: 0 < e;
deffunc P(Nat) = K to_power ($1+1);
consider rseq be Real_Sequence such that
A4: for n be Nat holds rseq.n=P(n) from SEQ_1:sch 1;
A5: L(#)rseq is convergent by A1,A2,A4,SEQ_2:7,SERIES_1:1;
A6: lim (L(#)rseq) = L* lim rseq by A1,A2,A4,SEQ_2:8,SERIES_1:1
.=L * (0 qua Real) by A1,A2,A4,SERIES_1:1;
consider n be Nat such that
A7: for m be Nat st n<=m holds
|.((L(#)rseq).m-(0 qua Real)).| < e by A5,A6,A3,SEQ_2:def 7;
|.((L(#)rseq).n-(0 qua Real)).| < e by A7;
then |. L*rseq.n .| < e by SEQ_1:9;
then |. L*(K to_power (n+1)) .| < e by A4;
hence thesis;
end;
registration
let X be RealNormSpace;
cluster constant -> contraction for Function of X,X;
coherence
proof
let f be Function of X,X such that
A1: f is constant;
set K = 1/2;
take K;
thus 0 < K & K < 1;
let x,y be Point of X;
dom f = the carrier of X by FUNCT_2:def 1;
hence thesis by NORMSP_1:6,A1,FUNCT_1:def 10;
end;
end;
registration
let X be RealBanachSpace;
cluster contraction -> with_unique_fixpoint for Function of X,X;
coherence
proof
let f be Function of X,X;
assume f is contraction;
then consider xp being Point of X such that
A1: f.xp = xp and
A2: for x be Point of X st f.x = x holds xp = x by NFCONT_2:14;
take xp;
thus f.xp = xp by A1;
let y be set;
assume y is_a_fixpoint_of f;
then y in dom f & f.y = y;
hence thesis by A2;
end;
end;
::$CT
theorem Th7:
for X being RealBanachSpace, f being Function of X,X st
ex n0 being Nat st iter(f,n0) is contraction holds
f is with_unique_fixpoint
proof
let X be RealBanachSpace;
let f be Function of X, X;
given n0 be Nat such that
A1: iter(f,n0) is contraction;
consider xp be Point of X such that
A2: (iter(f,n0)).xp = xp and
A3: for x be Point of X st iter(f,n0).x = x holds xp = x by A1,NFCONT_2:14;
take xp;
thus A4: xp is_a_fixpoint_of f
proof
A5: (iter(f,n0)).(f.xp) = (iter(f,n0)*f).xp by FUNCT_2:15
.=(iter(f,n0+1)).xp by FUNCT_7:69
.=(f*iter(f,n0)).xp by FUNCT_7:71
.=f.xp by A2,FUNCT_2:15;
thus f.xp = xp by A5,A3;
end;
A6: now
let x be Point of X such that
A7: f.x = x;
for n be Nat holds (iter(f,n)).x = x
proof
defpred P[Nat] means (iter(f,$1)).x = x;
(iter(f,0)).x=(id the carrier of X).x by FUNCT_7:84
.=x;
then
A8: P[ 0 ];
A9: now let n be Nat such that
A10: P[n];
reconsider m = n as Element of NAT by ORDINAL1:def 12;
(iter(f,n+1)).x = (f*iter(f,m)).x by FUNCT_7:71
.= x by A7,A10,FUNCT_2:15;
hence P[n+1];
end;
for n be Nat holds P[n] from NAT_1:sch 2(A8,A9);
hence thesis;
end;
then (iter(f,n0)).x = x;
hence xp = x by A3;
end;
let y be set;
A11: dom f = the carrier of X by FUNCT_2:def 1;
assume
A12: y is_a_fixpoint_of f;
then reconsider x1 = xp, y1 = y as Point of X by A11;
A13: f.x1 = x1 & f.y1 = y1 by A12,A4;
thus xp = y by A6,A13;
end;
theorem
for X being RealBanachSpace, f being Function of X,X st
ex n0 being Element of NAT st iter(f,n0) is contraction holds
ex xp being Point of X st f.xp = xp &
for x being Point of X st f.x = x holds xp = x
proof
let X be RealBanachSpace;
let f be Function of X,X;
assume ex n0 be Element of NAT st iter(f,n0) is contraction;
then f is with_unique_fixpoint by Th7;
then consider xp being set such that
A1: xp is_a_fixpoint_of f & for y being set st y is_a_fixpoint_of f holds
xp = y;
xp in dom f by A1;
then reconsider xp as Point of X;
take xp;
thus f.xp = xp by A1;
let x be Point of X;
assume f.x = x;
then x is_a_fixpoint_of f;
hence xp = x by A1;
end;
begin :: The Real Banach Space C([a,b],X)
theorem Th9:
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
f be continuous PartFunc of REAL,Y
st dom f = X holds
f is bounded Function of X,Y
proof
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
let f be continuous PartFunc of REAL,Y;
assume A1:dom f = X;
rng f c= the carrier of Y; then
reconsider g=f as Function of X,Y by A1,FUNCT_2:2;
f|X = f by A1; then
A2: (||.f .||) |X is continuous by A1,NFCONT_3:22;
A3:dom (||.f .||) = X by A1,NORMSP_0:def 2; then
consider x1,x2 be Real such that A4:
x1 in dom (||.f .||) & x2 in dom (||.f .||)
& (||.f .||).x1 = upper_bound (rng (||.f .||))
& (||.f .||).x2 = lower_bound (rng (||.f .||)) by A2,FCONT_1:30;
A5:(||.f .||).x1 =||.f/.x1 .|| by A4,NORMSP_0:def 2;
reconsider K = (||.f .||).x1 as Real;
now let x be Element of X;
A6: ||. g.x .|| =||. g/.x .||
.=(||.f.||).x by A3,NORMSP_0:def 2
.=(||.f.||)/.x by A3,PARTFUN1:def 6;
A7: rng (||.f .||) is real-bounded by A2,A3,FCONT_1:28,RCOMP_1:10;
(||.f .||).x in rng (||.f .||) by A3,FUNCT_1:3;
then
(||.f .||)/.x in rng (||.f .||) by A3,PARTFUN1:def 6;
hence ||. g.x .|| <= K by A4,A6,A7,SEQ_4:def 1;
end;
hence thesis by A5,RSSPACE4:def 4;
end;
definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
func ContinuousFunctions(X,Y)
-> Subset of R_VectorSpace_of_BoundedFunctions(X,Y) means :Def2:
for x being set holds x in it iff
ex f be continuous PartFunc of REAL,Y st x = f & dom f = X;
existence
proof
defpred P[object] means
ex f be continuous PartFunc of REAL,Y st $1=f & dom f = X;
consider IT being set such that
A1: for x being object holds x in IT iff x in BoundedFunctions(X,Y) &
P[x] from XBOOLE_0:sch 1;
take IT;
for x be object st x in IT holds x in BoundedFunctions(X,Y) by A1;
hence IT is Subset of R_VectorSpace_of_BoundedFunctions (X,Y)
by TARSKI:def 3;
let x be set;
thus x in IT implies
ex f be continuous PartFunc of REAL,Y st x=f & dom f = X by A1;
assume
A2: ex f be continuous PartFunc of REAL,Y st x=f & dom f = X;
then consider f be continuous PartFunc of REAL,Y such that
A3: x=f & dom f = X;
f is bounded Function of X,Y by A3,Th9;
then x in BoundedFunctions(X,Y) by A3,RSSPACE4:def 5;
hence thesis by A1,A2;
end;
uniqueness
proof
let X1,X2 be Subset of R_VectorSpace_of_BoundedFunctions (X,Y);
assume that
A4: for x being set holds x in X1 iff ex f be
continuous PartFunc of REAL,Y st x=f & dom f = X and
A5: for x being set holds x in X2 iff ex f be
continuous PartFunc of REAL,Y st x=f & dom f = X;
for x being object st x in X2 holds x in X1
proof
let x be object;
assume x in X2;
then ex f be continuous PartFunc of REAL,Y st x=f & dom f = X by A5;
hence thesis by A4;
end;
then
A6: X2 c= X1 by TARSKI:def 3;
for x being object st x in X1 holds x in X2
proof
let x be object;
assume x in X1;
then ex f be continuous PartFunc of REAL,Y st x=f & dom f = X by A4;
hence thesis by A5;
end;
then X1 c= X2 by TARSKI:def 3;
hence thesis by A6,XBOOLE_0:def 10;
end;
end;
registration
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
cluster ContinuousFunctions(X,Y) -> non empty;
coherence
proof
set f = X --> 0.Y;
reconsider f as Function of X,Y;
dom f = X;
then reconsider g = f as PartFunc of REAL,Y by RELSET_1:5;
dom g = X;
hence thesis by Def2;
end;
end;
registration
let X be non empty closed_interval Subset of REAL, Y be RealNormSpace;
cluster ContinuousFunctions(X,Y) -> linearly-closed;
coherence
proof
set W = ContinuousFunctions(X,Y);
thus for v,u be VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y)
st v in W & u in W holds v + u in W
proof
let v,u be VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y) such that
A1: v in W and
A2: u in W;
reconsider f=v+u,v0=v,u0=u as bounded Function of X,Y by RSSPACE4:def 5;
consider v1 be continuous PartFunc of REAL,Y such that
A3: v1=v & dom v1 = X by A1,Def2;
consider u1 be continuous PartFunc of REAL,Y such that
A4: u1=u & dom u1 = X by A2,Def2;
A5: dom f = (dom v1)/\ (dom u1) by A3,A4,FUNCT_2:def 1;
A6: now let x0 be Element of REAL;
assume A7:x0 in dom f;
then reconsider x=x0 as Element of X;
thus f/.x0 = f.x by A7,PARTFUN1:def 6
.=v0/.x+u0/.x by RSSPACE4:8
.=v1/.x0+u1/.x0 by A3,A4;
end;
dom f = X by FUNCT_2:def 1;
then dom f c= REAL & rng f c= the carrier of Y;
then f in PFuncs(REAL,the carrier of Y) by PARTFUN1:def 3;
then f is PartFunc of REAL,Y by PARTFUN1:46;
then
A8: f = v1+u1 by A5,A6,VFUNCT_1:def 1;
then dom (v1+u1) = X by FUNCT_2:def 1;
hence thesis by Def2,A8;
end;
let a be Real;
let v be VECTOR of R_VectorSpace_of_BoundedFunctions (X,Y) such that
A9: v in W;
reconsider f=a*v,v0=v as bounded Function of X,Y by RSSPACE4:def 5;
consider v1 be continuous PartFunc of REAL,Y such that
A10: v1=v & dom v1 = X by A9,Def2;
A11: dom f = dom v1 by A10,FUNCT_2:def 1;
A12: now let x0 be Element of REAL;
assume A13:x0 in dom f;
then reconsider x=x0 as Element of X;
thus f/.x0 = f.x by A13,PARTFUN1:def 6
.=a*v0/.x by RSSPACE4:9
.=a*v1/.x0 by A10;
end;
dom f = X by FUNCT_2:def 1;
then dom f c= REAL & rng f c= the carrier of Y;
then f in PFuncs(REAL,the carrier of Y) by PARTFUN1:def 3;
then f is PartFunc of REAL,Y by PARTFUN1:46;
then
A14: f = a(#)v1 by A11,A12,VFUNCT_1:def 4;
then dom (a(#)v1) = X by FUNCT_2:def 1;
hence thesis by Def2,A14;
end;
end;
definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
func R_VectorSpace_of_ContinuousFunctions(X,Y) -> strict RealLinearSpace
equals
RLSStruct (# ContinuousFunctions(X,Y), Zero_(ContinuousFunctions(X,Y),
R_VectorSpace_of_BoundedFunctions (X,Y)), Add_(ContinuousFunctions(X,Y),
R_VectorSpace_of_BoundedFunctions (X,Y)), Mult_(ContinuousFunctions(X,Y),
R_VectorSpace_of_BoundedFunctions(X,Y)) #);
coherence by RSSPACE:11;
end;
registration
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
cluster R_VectorSpace_of_ContinuousFunctions(X,Y) ->
Abelian add-associative
right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence;
end;
theorem Th10:
for X be non empty closed_interval Subset of REAL, Y be RealNormSpace,
f,g,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(X,Y),
f9,g9,h9 be continuous PartFunc of REAL,Y
st f9=f & g9=g & h9=h & dom f9=X & dom g9=X & dom h9=X
holds (h = f+g iff for x
be Element of X holds h9/.x = f9/.x + g9/.x )
proof
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
let f,g,h be VECTOR
of R_VectorSpace_of_ContinuousFunctions(X,Y);
A1: R_VectorSpace_of_ContinuousFunctions(X,Y)
is Subspace of R_VectorSpace_of_BoundedFunctions(X,Y) by RSSPACE:11;
then reconsider f1=f as VECTOR
of R_VectorSpace_of_BoundedFunctions(X,Y) by RLSUB_1:10;
reconsider h1=h as VECTOR
of R_VectorSpace_of_BoundedFunctions(X,Y) by A1,RLSUB_1:10;
reconsider g1=g as VECTOR
of R_VectorSpace_of_BoundedFunctions(X,Y) by A1,RLSUB_1:10;
let f9,g9,h9 be continuous PartFunc of REAL,Y such that
A2: f9=f & g9=g & h9=h & dom f9=X & dom g9=X & dom h9=X;
reconsider f90=f1, g90=g1, h90=h1 as bounded Function of X,Y
by RSSPACE4:def 5;
A3: now
assume
A4: h = f+g;
let x be Element of X;
A5: h1=f1+g1 by A1,A4,RLSUB_1:13;
thus h9/.x =h90.x by A2,PARTFUN1:def 6
.=f90/.x+g90/.x by A5,RSSPACE4:8
.=f9/.x+g9/.x by A2;
end;
now
assume A6: for x be Element of X holds h9/.x=f9/.x+g9/.x;
now let x be Element of X;
thus h90.x = h9/.x by A2,PARTFUN1:def 6
.= f90/.x+g90/.x by A2,A6
.= f90.x+g90.x;
end;
then h1=f1+g1 by RSSPACE4:8;
hence h =f+g by A1,RLSUB_1:13;
end;
hence thesis by A3;
end;
theorem Th11:
for X be non empty closed_interval Subset of REAL, Y be RealNormSpace,
f,h be VECTOR of R_VectorSpace_of_ContinuousFunctions(X,Y),
f9,h9 be continuous PartFunc of REAL,Y
st f9=f & h9=h & dom f9=X & dom h9=X
holds h = a*f iff for x be Element of X holds h9/.x = a*f9/.x
proof
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
let f,h be VECTOR
of R_VectorSpace_of_ContinuousFunctions(X,Y);
A1: R_VectorSpace_of_ContinuousFunctions(X,Y)
is Subspace of R_VectorSpace_of_BoundedFunctions(X,Y) by RSSPACE:11;
then reconsider f1=f as VECTOR
of R_VectorSpace_of_BoundedFunctions(X,Y) by RLSUB_1:10;
reconsider h1=h as VECTOR
of R_VectorSpace_of_BoundedFunctions(X,Y) by A1,RLSUB_1:10;
let f9,h9 be continuous PartFunc of REAL,Y such that
A2: f9=f & h9=h & dom f9=X & dom h9=X;
reconsider f90=f1 as bounded Function of X,Y by RSSPACE4:def 5;
reconsider h90=h1 as bounded Function of X,Y by RSSPACE4:def 5;
A3: now
assume
A4: h = a*f;
let x be Element of X;
A5: h1=a*f1 by A1,A4,RLSUB_1:14;
thus h9/.x =h90.x by A2,PARTFUN1:def 6
.=a*f90/.x by A5,RSSPACE4:9
.=a*f9/.x by A2;
end;
now
assume A6: for x be Element of X holds h9/.x=a*f9/.x;
now let x be Element of X;
thus h90.x = h9/.x by A2,PARTFUN1:def 6
.= a*f90/.x by A2,A6
.= a*f90.x;
end;
then h1=a*f1 by RSSPACE4:9;
hence h =a*f by A1,RLSUB_1:14;
end;
hence thesis by A3;
end;
theorem Th12:
for X be non empty closed_interval Subset of REAL, Y be RealNormSpace holds
0. R_VectorSpace_of_ContinuousFunctions(X,Y) = X -->0.Y
proof
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
R_VectorSpace_of_ContinuousFunctions(X,Y) is Subspace of
R_VectorSpace_of_BoundedFunctions(X,Y)
& 0.R_VectorSpace_of_BoundedFunctions(X,Y) =(X -->0.Y)
by RSSPACE4:10,RSSPACE:11;
hence thesis by RLSUB_1:11;
end;
definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
func ContinuousFunctionsNorm(X,Y) ->
Function of ContinuousFunctions(X,Y),REAL equals
(BoundedFunctionsNorm(X,Y)) | (ContinuousFunctions(X,Y));
correctness by FUNCT_2:32;
end;
definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
let f be set such that
A1: f in ContinuousFunctions(X,Y);
func modetrans(f,X,Y) -> continuous PartFunc of REAL,Y means :Def5:
it = f & dom it = X;
correctness by A1,Def2;
end;
definition
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
func R_NormSpace_of_ContinuousFunctions(X,Y) -> strict non empty NORMSTR
equals
NORMSTR (# ContinuousFunctions(X,Y),
Zero_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y)),
Add_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y)),
Mult_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y)),
ContinuousFunctionsNorm(X,Y) #);
coherence;
end;
theorem
for X be non empty closed_interval Subset of REAL,Y be RealNormSpace,
f be continuous PartFunc of REAL,Y
st dom f=X holds modetrans(f,X,Y)=f
proof
let X be non empty closed_interval Subset of REAL,Y be RealNormSpace,
f be continuous PartFunc of REAL,Y;
assume dom f = X; then
f in ContinuousFunctions(X,Y) by Def2;
hence thesis by Def5;
end;
theorem Th14:
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace holds (X --> 0.Y)
= 0.R_NormSpace_of_ContinuousFunctions(X,Y)
proof
let X be non empty closed_interval Subset of REAL,
Y be RealNormSpace;
(X --> 0.Y) =0.R_VectorSpace_of_ContinuousFunctions(X,Y) by Th12
.=0.R_NormSpace_of_ContinuousFunctions(X,Y);
hence thesis;
end;
theorem Th15:
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace, f,g,h be Point of
R_NormSpace_of_ContinuousFunctions(X,Y),
f9,g9,h9 be continuous PartFunc of REAL,Y
st f9=f & g9=g & h9=h & dom f9=X & dom g9=X & dom h9=X
holds (h = f+g iff for x be Element of X
holds h9/.x = f9/.x + g9/.x)
proof
let X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
f,g,h be Point of R_NormSpace_of_ContinuousFunctions(X,Y);
reconsider f1=f, g1=g, h1=h
as VECTOR of R_VectorSpace_of_ContinuousFunctions(X,Y);
A1: h=f+g iff h1=f1 + g1;
let f9,g9,h9 be continuous PartFunc of REAL,Y;
thus thesis by A1,Th10;
end;
theorem
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
f,h be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
f9,h9 be continuous PartFunc of REAL,Y
st f9=f & h9=h & dom f9=X & dom h9=X
holds (h = a*f iff for x be Element of X
holds h9/.x = a*f9/.x)
proof
let X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
f,h be Point of R_NormSpace_of_ContinuousFunctions(X,Y);
reconsider f1=f, h1=h as VECTOR of R_VectorSpace_of_ContinuousFunctions(X,Y);
let f9,h9 be continuous PartFunc of REAL,Y;
assume
A1: f9=f & h9=h & dom f9=X & dom h9=X;
h=a*f iff h1=a*f1;
hence thesis by A1,Th11;
end;
theorem Th17:
for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
f be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g be Point of R_NormSpace_of_BoundedFunctions(X,Y)
st f=g holds ||.f.|| = ||.g.|| by FUNCT_1:49;
theorem Th18:
for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
f,g be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
f1,g1 be Point of R_NormSpace_of_BoundedFunctions(X,Y)
st f1=f & g1=g holds f+g = f1+g1
proof
let X be non empty closed_interval Subset of REAL,Y be RealNormSpace,
f,g be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
f1,g1 be Point of R_NormSpace_of_BoundedFunctions(X,Y);
assume A1: f1=f & g1=g;
reconsider f2=f,g2=g as Point of R_VectorSpace_of_ContinuousFunctions(X,Y);
reconsider f3=f2,g3=g2 as Point of R_VectorSpace_of_BoundedFunctions(X,Y)
by TARSKI:def 3;
A2: R_VectorSpace_of_ContinuousFunctions(X,Y) is Subspace of
R_VectorSpace_of_BoundedFunctions(X,Y) by RSSPACE:11;
thus f+g = f2+g2
.= f3+g3 by A2,RLSUB_1:13
.= f1 + g1 by A1;
end;
theorem Th19:
for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
f be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
f1 be Point of R_NormSpace_of_BoundedFunctions(X,Y) st f1=f
holds a*f = a*f1
proof
let X be non empty closed_interval Subset of REAL,Y be RealNormSpace,
f be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
f1 be Point of R_NormSpace_of_BoundedFunctions(X,Y);
assume A1: f1=f;
reconsider f2=f as Point of R_VectorSpace_of_ContinuousFunctions(X,Y);
reconsider f3=f2 as Point of R_VectorSpace_of_BoundedFunctions(X,Y)
by TARSKI:def 3;
A2: R_VectorSpace_of_ContinuousFunctions(X,Y)
is Subspace of R_VectorSpace_of_BoundedFunctions(X,Y) by RSSPACE:11;
thus a*f = a*f2
.= a*f3 by A2,RLSUB_1:14
.= a*f1 by A1;
end;
Lm2: for X be non empty closed_interval Subset of REAL
for Y be RealNormSpace for f, g being
Point of R_NormSpace_of_ContinuousFunctions(X,Y)
holds ( ||.f.|| = 0
iff f = 0.R_NormSpace_of_ContinuousFunctions(X,Y) )
& ||.a*f.|| = |.(a).| * ||.f.||
& ||.f+g.|| <= ||.f.|| + ||.g.||
proof
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
let f, g being Point of R_NormSpace_of_ContinuousFunctions(X,Y);
reconsider f1=f as VECTOR
of R_NormSpace_of_BoundedFunctions(X,Y) by TARSKI:def 3;
reconsider g1=g as VECTOR of R_NormSpace_of_BoundedFunctions(X,Y)
by TARSKI:def 3;
A1:0.R_NormSpace_of_ContinuousFunctions(X,Y)
= (X --> 0.Y) by Th14
.= 0.R_NormSpace_of_BoundedFunctions(X,Y) by RSSPACE4:15;
A2: ||.f1+g1.|| <= ||.f1.|| + ||.g1.|| by RSSPACE4:21;
A3: ||.f1+g1.|| = ||.f+g.|| by Th18,Th17;
A4: ||.f1.|| = ||.f.|| by FUNCT_1:49;
||.a*f1.|| = ||.a*f.|| by Th19,Th17;
hence thesis by RSSPACE4:21,A1,FUNCT_1:49,A2,A3,A4;
end;
Lm3:
for X be non empty closed_interval Subset of REAL
for Y be RealNormSpace holds
R_NormSpace_of_ContinuousFunctions(X,Y) is
reflexive discerning RealNormSpace-like
proof
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
thus ||.0.R_NormSpace_of_ContinuousFunctions(X,Y).|| = 0 by Lm2;
for x, y being Point of R_NormSpace_of_ContinuousFunctions(X,Y)
for a be Real holds
( ||.x.|| = 0
iff x = 0.R_NormSpace_of_ContinuousFunctions(X,Y) )
& ||. a*x.|| = |.(a).| * ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| by Lm2;
hence thesis by NORMSP_1:def 1;
end;
Lm4:
for X be non empty closed_interval Subset of REAL
for Y be RealNormSpace holds
R_NormSpace_of_ContinuousFunctions(X,Y) is RealNormSpace
proof
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
RLSStruct (# ContinuousFunctions(X,Y),
Zero_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y)),
Add_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y)),
Mult_(ContinuousFunctions(X,Y),R_VectorSpace_of_BoundedFunctions (X,Y))
#) is RealLinearSpace by RSSPACE:11;
hence thesis by Lm3,RSSPACE3:2;
end;
registration
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
cluster R_NormSpace_of_ContinuousFunctions(X,Y) ->
reflexive discerning RealNormSpace-like vector-distributive
scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence by Lm4;
end;
theorem Th20:
for X be non empty closed_interval Subset of REAL
for Y be RealNormSpace
for f,g,h be Point of R_NormSpace_of_ContinuousFunctions(X,Y)
for f9,g9,h9 be continuous PartFunc of REAL,Y
st f9=f & g9=g & h9=h & dom f9=X & dom g9=X & dom h9=X
holds (h = f-g iff for x be Element of X holds h9/.x = f9/.x - g9/.x )
proof
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
let f,g,h be Point of R_NormSpace_of_ContinuousFunctions(X,Y);
let f9,g9,h9 be continuous PartFunc of REAL,Y such that
A1: f9=f & g9=g & h9=h & dom f9=X & dom g9=X & dom h9=X;
A2: now
assume
A3: for x be Element of X holds h9/.x = f9/.x - g9/.x;
now
let x be Element of X;
h9/.x = f9/.x - g9/.x by A3;
then h9/.x + g9/.x= f9/.x - (g9/.x- g9/.x) by RLVECT_1:29;
then h9/.x + g9/.x= f9/.x - 0.Y by RLVECT_1:15;
hence h9/.x + g9/.x= f9/.x;
end;
then f=h+g by A1,Th15;
then f-g=h+(g-g) by RLVECT_1:def 3;
then f-g=h+0.R_NormSpace_of_ContinuousFunctions(X,Y) by RLVECT_1:5;
hence f-g=h;
end;
now
assume h=f-g;
then h+g=f-(g-g) by RLVECT_1:29;
then
A4: h+g=f-0.R_NormSpace_of_ContinuousFunctions(X,Y) by RLVECT_1:5;
now
let x be Element of X;
f9/.x=h9/.x + g9/.x by A1,A4,Th15;
then f9/.x-g9/.x=h9/.x + (g9/.x-g9/.x) by RLVECT_1:def 3;
then f9/.x-g9/.x=h9/.x + 0.Y by RLVECT_1:15;
hence f9/.x-g9/.x=h9/.x;
end;
hence for x be Element of X holds h9/.x = f9/.x - g9/.x;
end;
hence thesis by A2;
end;
theorem Th21:
for X be non empty closed_interval Subset of REAL for Y be RealNormSpace,
f,g be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
f1,g1 be Point of R_NormSpace_of_BoundedFunctions(X,Y)
st f1=f & g1=g
holds f-g = f1-g1
proof
let X be non empty closed_interval Subset of REAL,Y be RealNormSpace,
f,g be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
f1,g1 be Point of R_NormSpace_of_BoundedFunctions(X,Y);
assume A1: f1=f & g1=g;
A2: -g1 = (-1)*g1 by RLVECT_1:16
.= (-1)*g by A1,Th19
.= -g by RLVECT_1:16;
thus f-g = f1 - g1 by A1,A2,Th18;
end;
Lm5:
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
C being Subset of R_NormSpace_of_BoundedFunctions(X,Y) st
C = ContinuousFunctions(X,Y) holds
C is closed
proof
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
let C be Subset of R_NormSpace_of_BoundedFunctions(X,Y);
assume A1: C = ContinuousFunctions(X,Y);
now let seq be sequence of
R_NormSpace_of_BoundedFunctions(X,Y);
assume A2: rng seq c= C & seq is convergent;
reconsider f = lim seq as bounded Function of X,Y by RSSPACE4:def 5;
A3: dom f = X by FUNCT_2:def 1;
now let z be object;
assume z in BoundedFunctions (X,Y); then
z is bounded Function of X,Y by RSSPACE4:def 5;
hence z in PFuncs(X,the carrier of Y) by PARTFUN1:45;
end;
then BoundedFunctions (X,Y) c= PFuncs(X,the carrier of Y)
by TARSKI:def 3; then
reconsider H = seq as Functional_Sequence of X,the carrier of Y
by FUNCT_2:7;
A4: for p be Real st p>0 ex k be Nat st
for n be Nat, x be set st
n>=k & x in X holds ||. (H.n)/.x - f/.x .|| < p
proof
let p be Real;
assume p>0; then
consider k be Nat such that
A5: for n be Nat st n >= k holds
||.seq.n - lim seq.|| < p by A2,NORMSP_1:def 7;
take k;
hereby let n be Nat, x be set;
assume A6: n>=k & x in X; then
A7: ||.seq.n - lim seq.|| < p by A5;
reconsider g = seq.n - lim seq, s = seq.n
as bounded Function of X,Y by RSSPACE4:def 5;
reconsider x0 = x as Element of X by A6;
A8: g.x0=s/.x0-f/.x0 by RSSPACE4:24;
||.g.x0.|| <= ||.seq.n - lim seq.|| by RSSPACE4:16;
hence ||.(H.n)/.x - f/.x.|| < p by A8,A7,XXREAL_0:2;
end;
end;
dom f = X by FUNCT_2:def 1;
then dom f c= REAL & rng f c= the carrier of Y;
then f in PFuncs(REAL,the carrier of Y) by PARTFUN1:def 3;
then reconsider f as PartFunc of REAL,Y by PARTFUN1:46;
for x0 be Real st x0 in dom f holds f is_continuous_in x0
proof
let x be Real;
assume A9: x in dom f;
now let r0 be Real;
assume A10:0 < r0; then
consider k being Nat such that
A11: for n be Nat,x be set st n>=k & x in X holds
||.(H.n)/.x - f/.x .|| < r0/3 by A4,XREAL_1:222;
A12: ||.(H.k)/.x - f/.x .|| < r0/3 by A11,A3,A9;
k in NAT by ORDINAL1:def 12; then
k in dom seq by NORMSP_1:12; then
H.k in rng seq by FUNCT_1:def 3; then
consider h be continuous PartFunc of REAL,Y such that
A13: H.k=h & dom h= X by A2,Def2,A1;
A14: 0 <r0/3 & r0/3 is Real by A10,XREAL_1:222;
x in dom h by A9,A13,FUNCT_2:def 1;
then h is_continuous_in x by NFCONT_3:def 2;
then consider w1 be Real such that
A15: 0 < w1 & for x0 be Real
st x0 in dom h & |.(x0-x).| < w1
holds ||. h/.x0 - h/.x .||<r0/3 by A14,NFCONT_3:8;
take w1;
thus 0 < w1 by A15;
thus for z0 be Real st z0 in dom f & |.(z0 - x).|< w1
holds ||. f/.z0 -f/.x .|| <r0
proof
let z0 be Real;
assume A16: z0 in dom f & |.(z0 - x).|< w1; then
A17: z0 in dom h by FUNCT_2:def 1,A13; then
A18: ||.h/.z0 - h/.x.|| < r0/3 by A16,A15;
A19: ||.f/.x - h/.x.|| < r0/3 by A12,A13,NORMSP_1:7;
||.h/.z0 - f/.z0 .|| < r0/3 by A17,A11,A13; then
||.f/.z0 - h/.z0.|| < r0/3 by NORMSP_1:7; then
||.f/.z0 - h/.z0.||+||.f/.x - h/.x.|| < r0/3 + r0/3
by A19,XREAL_1:8; then
A20: ||.f/.z0 - h/.z0.|| +||.f/.x - h/.x.||+ ||.h/.z0 - h/.x.||
< r0/3 + r0/3 + r0/3 by A18,XREAL_1:8;
(f/.z0 - h/.z0)- (f/.x - h/.x) +(h/.z0-h/.x)
= (f/.z0 - h/.z0) -((f/.x - h/.x) - (h/.z0-h/.x)) by RLVECT_1:29
.= (f/.z0 - h/.z0) -(f/.x - (h/.x + (h/.z0-h/.x))) by RLVECT_1:27
.= (f/.z0 - h/.z0) -(f/.x - (h/.z0 - (h/.x -h/.x))) by RLVECT_1:29
.= (f/.z0 - h/.z0) -(f/.x - (h/.z0 - 0.Y)) by RLVECT_1:15
.= f/.z0 - (h/.z0 + (f/.x - h/.z0)) by RLVECT_1:27
.= f/.z0 - (f/.x -(h/.z0-h/.z0)) by RLVECT_1:29
.= f/.z0 - (f/.x -0.Y) by RLVECT_1:15
.= f/.z0 - f/.x; then
A21: ||. f/.z0 -f/.x .|| <= ||.(f/.z0 - h/.z0)- (f/.x - h/.x) .||
+||.h/.z0-h/.x .|| by NORMSP_1:def 1;
||.(f/.z0 - h/.z0)- (f/.x - h/.x).||+||.h/.z0-h/.x .||
<= ||. f/.z0 - h/.z0 .|| + ||.f/.x - h/.x.||
+||.h/.z0-h/.x.|| by XREAL_1:6,NORMSP_1:3; then
||. f/.z0 -f/.x .|| <= ||.f/.z0 - h/.z0.||+||.f/.x - h/.x.||
+||.h/.z0-h/.x.|| by A21,XXREAL_0:2;
hence ||. f/.z0 -f/.x .|| <r0 by A20,XXREAL_0:2;
end;
end;
hence f is_continuous_in x by A9,NFCONT_3:8;
end; then
f is continuous by NFCONT_3:def 2;
hence lim seq in C by A3,Def2,A1;
end;
hence thesis by NFCONT_1:def 3;
end;
registration
let X be non empty closed_interval Subset of REAL,
Y be RealNormSpace;
cluster closed for Subset of R_NormSpace_of_BoundedFunctions(X,Y);
existence
proof
reconsider C = ContinuousFunctions(X,Y)
as Subset of R_NormSpace_of_BoundedFunctions(X,Y);
C is closed by Lm5;
hence thesis;
end;
end;
theorem Th22:
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace holds
ContinuousFunctions(X,Y)
is closed Subset of R_NormSpace_of_BoundedFunctions(X,Y)
by Lm5;
theorem Th23:
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
seq be sequence of R_NormSpace_of_ContinuousFunctions(X,Y)
st Y is complete &
seq is Cauchy_sequence_by_Norm holds seq is convergent
proof
let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
let vseq be sequence of R_NormSpace_of_ContinuousFunctions(X,Y);
assume A1: Y is complete & vseq is Cauchy_sequence_by_Norm;
rng vseq c= BoundedFunctions(X,Y) by XBOOLE_1:1; then
reconsider vseq1=vseq as sequence of
R_NormSpace_of_BoundedFunctions(X,Y) by FUNCT_2:6;
now let e be Real such that
A2: e >0;
consider k be Nat such that
A3: for n,m be Nat st n >= k & m >= k holds
||. vseq.n - vseq.m .|| < e by A1,A2,RSSPACE3:8;
take k;
now let n,m be Nat;
assume n >= k & m >= k; then
||. vseq.n - vseq.m .|| < e by A3;
hence ||. vseq1.n - vseq1.m .|| < e by Th17,Th21;
end;
hence for n,m be Nat st n >= k & m >= k holds
||. vseq1.n - vseq1.m .|| < e;
end; then
A4:vseq1 is convergent by A1,LOPBAN_1:def 15,RSSPACE3:8;
reconsider Z = ContinuousFunctions(X,Y) as Subset of
R_NormSpace_of_BoundedFunctions(X,Y);
rng vseq c= ContinuousFunctions(X,Y); then
reconsider tv=lim vseq1 as Point of
R_NormSpace_of_ContinuousFunctions(X,Y) by A4,NFCONT_1:def 3,Th22;
for e be Real st e > 0 ex k be Nat
st for n be Nat st
n >= k holds ||.vseq.n - tv.|| < e
proof
let e be Real;
assume e > 0; then
consider k be Nat such that
A5: for n be Nat st n >= k holds
||.vseq1.n - lim vseq1.|| < e by A4,NORMSP_1:def 7;
take k;
now let n be Nat;
assume n >= k; then
||.vseq1.n-lim vseq1.|| < e by A5;
hence ||.vseq.n-tv.|| < e by Th17,Th21;
end;
hence for n be Nat st n >= k holds ||.vseq.n - tv.|| < e;
end;
hence thesis by NORMSP_1:def 6;
end;
Lm6:
for X be non empty closed_interval Subset of REAL,
Y be RealBanachSpace holds
R_NormSpace_of_ContinuousFunctions(X,Y) is RealBanachSpace
proof
let X be non empty closed_interval Subset of REAL;
let Y be RealBanachSpace;
for seq be sequence of R_NormSpace_of_ContinuousFunctions(X,Y)
st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th23;
hence thesis by LOPBAN_1:def 15;
end;
registration
let X be non empty closed_interval Subset of REAL;
let Y be RealBanachSpace;
cluster R_NormSpace_of_ContinuousFunctions(X,Y) -> complete;
coherence by Lm6;
end;
theorem Th24:
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
v be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g be PartFunc of REAL,Y st g=v
holds for t be Real st t in X holds ||.g/.t.|| <= ||.v.||
proof
let X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
v be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g be PartFunc of REAL,Y;
assume A1:g=v;
consider f be continuous PartFunc of REAL,Y such that
A2: v=f & dom f = X by Def2;
reconsider g1=g as bounded Function of X,Y by A1,Th9,A2;
reconsider v1=v as VECTOR of R_NormSpace_of_BoundedFunctions(X,Y)
by TARSKI:def 3;
A3: ||.v1.|| = ||.v.|| by FUNCT_1:49;
let t be Real;
assume t in X; then
reconsider t1=t as Element of X;
||.g1.t1.|| <= ||.v1.|| by A1,RSSPACE4:16;
hence thesis by A2,A1,PARTFUN1:def 6,A3;
end;
theorem Th25:
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
K be Real,
v being Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g be PartFunc of REAL,Y st g=v &
for t be Real st t in X holds ||.g/.t.|| <= K
holds ||.v.|| <= K
proof
let X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
K be Real,
v be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g be PartFunc of REAL,Y;
assume A1:g=v & for t be Real st t in X holds ||.g/.t.|| <= K;
consider f be continuous PartFunc of REAL,Y such that
A2: v=f & dom f = X by Def2;
reconsider g1=g as bounded Function of X,Y by A1,Th9,A2;
reconsider v1=v as VECTOR of R_NormSpace_of_BoundedFunctions(X,Y)
by TARSKI:def 3;
A3: for t be Element of X holds ||.g1.t.|| <= K
proof
let t be Element of X;
reconsider t1=t as Real;
||.g/.t1.|| <= K by A1;
hence ||.g1.t.|| <= K by A2,A1,PARTFUN1:def 6;
end;
A4: for x be Element of REAL st x in PreNorms(g1) holds x <= K
proof
let x be Element of REAL;
assume x in PreNorms(g1); then
consider t be Element of X such that
A5: x= ||.g1.t.||;
thus thesis by A3,A5;
end;
upper_bound PreNorms(g1) <= K
proof
assume A6: not upper_bound PreNorms(g1) <= K;
reconsider s = upper_bound PreNorms(g1) - K as Real;
A7: 0 < s by A6,XREAL_1:50;
PreNorms(g1) is non empty bounded_above by RSSPACE4:11; then
consider r be Real such that
A8: r in PreNorms(g1) & (upper_bound PreNorms(g1))-s<r by A7,SEQ_4:def 1;
thus contradiction by A8,A4;
end;
then ||.v1.|| <= K by A1,RSSPACE4:14;
hence thesis by FUNCT_1:49;
end;
theorem Th26:
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
v1,v2 be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g1,g2 be PartFunc of REAL,Y
st g1=v1 & g2=v2
holds for t be Real st t in X holds
||.g1/.t - g2/.t .|| <= ||.v1-v2.||
proof
let X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
v1,v2 be Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g1,g2 be PartFunc of REAL,Y;
assume A1:g1=v1 & g2=v2;
consider f1 be continuous PartFunc of REAL,Y such that
A2: v1=f1 & dom f1 = X by Def2;
consider f2 be continuous PartFunc of REAL,Y such that
A3: v2=f2 & dom f2 = X by Def2;
consider f12 be continuous PartFunc of REAL,Y such that
A4: v1-v2=f12 & dom f12 = X by Def2;
let t be Real;
assume t in X;
then reconsider t1=t as Element of X;
f12/.t1 = f1/.t1 - f2/.t1 by A2,A3,A4,Th20;
hence ||.g1/.t - g2/.t .|| <= ||.v1-v2.|| by A1,A2,A3,A4,Th24;
end;
theorem Th27:
for X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
K be Real,
v1,v2 being Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g1,g2 be PartFunc of REAL,Y
st g1=v1 & g2=v2 &
for t be Real st t in X holds
||.g1/.t - g2/.t .|| <= K
holds ||.v1-v2.|| <= K
proof
let X be non empty closed_interval Subset of REAL,
Y be RealNormSpace,
K be Real,
v1,v2 being Point of R_NormSpace_of_ContinuousFunctions(X,Y),
g1,g2 be PartFunc of REAL,Y;
assume A1:g1=v1 & g2=v2 &
for t be Real st t in X holds ||.g1/.t - g2/.t .|| <= K;
consider f1 be continuous PartFunc of REAL,Y such that
A2: v1=f1 & dom f1 = X by Def2;
consider f2 be continuous PartFunc of REAL,Y such that
A3: v2=f2 & dom f2 = X by Def2;
consider f12 be continuous PartFunc of REAL,Y such that
A4: v1-v2=f12 & dom f12 = X by Def2;
for t be Real st t in X holds ||.f12/.t .|| <= K
proof
let t be Real;
assume t in X;
then reconsider t1=t as Element of X;
f12/.t1 = g1/.t - g2/.t by A1,A2,A3,A4,Th20;
hence ||.f12/.t .|| <= K by A1;
end;
hence thesis by Th25,A4;
end;
begin :: Differential Equations
theorem Th28:
for n,i be Nat, f be PartFunc of REAL,REAL n,
A be Subset of REAL holds proj(i,n)*(f|A) = (proj(i,n)*f)|A
proof
let n,i be Nat, f be PartFunc of REAL,REAL n, A be Subset of REAL;
A1: dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then
A2: rng f c= dom(proj(i,n));
A3: rng (f|A) c= dom (proj(i,n)) by A1;
A4: now
let c be object;
assume
A5: c in dom ((proj(i,n)*f)|A); then
A6: c in dom (proj(i,n)*f) /\ A by RELAT_1:61;
A7: c in dom (proj(i,n)*f) by A6,XBOOLE_0:def 4;
then c in dom f by A2,RELAT_1:27;
then c in dom f /\ A by A5,XBOOLE_0:def 4;then
A8: c in dom (f|A) by RELAT_1:61;
then c in dom (proj(i,n)*(f|A)) by A3,RELAT_1:27;
then (proj(i,n)*(f|A)).c = (proj(i,n)).((f|A).c) by FUNCT_1:12
.= (proj(i,n)).(f.c) by A8,FUNCT_1:47
.= (proj(i,n)*f).c by A7,FUNCT_1:12;
hence ((proj(i,n)*f)|A).c = (proj(i,n)*(f|A)).c by A5,FUNCT_1:47;
end;
dom ((proj(i,n)*f)|A) = dom (proj(i,n)*f) /\ A by RELAT_1:61
.= dom f /\ A by A2,RELAT_1:27
.= dom (f|A) by RELAT_1:61
.= dom (proj(i,n)*(f|A)) by A3,RELAT_1:27;
hence thesis by A4,FUNCT_1:2;
end;
theorem Th29:
for g be continuous PartFunc of REAL, REAL n st dom g = [' a,b ']
holds g | [' a,b '] is bounded
proof
let g be continuous PartFunc of REAL, REAL n;
assume A1: dom g =[' a,b '];
A2: for i be Element of NAT st i in Seg n holds
(proj(i,n)*g) | [' a,b '] is continuous
proof
let i be Element of NAT;
assume i in Seg n; then
proj(i,n)*g is continuous by NFCONT_4:44;
hence (proj(i,n)*g) | [' a,b '] is continuous;
end;
let i be Element of NAT;
assume A3: i in Seg n;
dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then rng g c= dom(proj(i,n));
then [' a,b '] c= dom (proj(i,n)*g) by A1,RELAT_1:27;
then (proj(i,n)*g) | [' a,b '] is bounded by A3,A2,INTEGRA5:10;
hence thesis by Th28;
end;
theorem Th30:
for g be continuous PartFunc of REAL,REAL n
st dom g =[' a,b ']
holds g is_integrable_on [' a,b ']
proof
let g be continuous PartFunc of REAL,REAL n;
assume A1: dom g =[' a,b '];
let i be Element of NAT;
assume i in Seg n; then
A2: proj(i,n)*g is continuous by NFCONT_4:44;
dom (proj(i,n))=REAL n by FUNCT_2:def 1;
then rng g c= dom(proj(i,n));
then
A3: [' a,b '] c= dom (proj(i,n)*g) by A1,RELAT_1:27;
(proj(i,n)*g) | [' a,b '] is continuous by A2;
hence thesis by A3,INTEGRA5:11;
end;
theorem Th31:
for f,F be PartFunc of REAL,REAL n
st a <= b
& dom f =[' a,b '] & dom F =[' a,b ']
& f is continuous
& for t be Real st t in [.a,b.] holds F.t = integral(f,a,t)
holds
for x be Real st x in [.a,b.] holds F is_continuous_in x
proof
let f,F be PartFunc of REAL,REAL n;
assume A1: a <= b
& dom f =[' a,b '] & dom F =[' a,b '] & f is continuous
& for t be Real st t in [.a,b.]
holds F.t = integral(f,a,t);
A2: f|([' a,b ']) is bounded by A1,Th29;
dom f = dom (|.f.|) by NFCONT_4:def 2; then
(|.f.|) | ([' a,b ']) = |.f.| by A1; then
|.f.| is bounded by A1,A2,INTEGR19:19; then
consider K be Real such that
A3: for y be set st y in dom (|.f.|)
holds |. (|.f.| . y).| < K by COMSEQ_2:def 3;
a in [.a,b.] by A1; then
a in ['a,b'] by A1,INTEGRA5:def 3; then
a in dom (|.f.|) by A1,NFCONT_4:def 2; then
A4: |. (|.f.| . a) .| < K by A3;
A5: 0 < K by A4,COMPLEX1:46;
A6:
now let c,d be Real;
assume A7:c in ['a,b'] & d in ['a,b'];
let y be Real;
assume A8: y in ['min(c,d),max(c,d)'];
['min(c,d),max(c,d)'] c= ['a,b'] by A7,A1,INTEGR19:3;
then y in ['a,b'] by A8;
then
A9: y in dom |.f.| by NFCONT_4:def 2,A1; then
|. (|.f.| .y) .|< K by A3; then
|.(|.f.| /.y).| < K by A9,PARTFUN1:def 6; then
|.(|.f/.y .|).| < K by A9,NFCONT_4:def 2;
hence |. f/.y .| <= K by ABSVALUE:def 1;
end;
A10:
now let c,d be Real;
assume A11:c in ['a,b'] & d in ['a,b'];
then for y be Real st y in ['min(c,d),max(c,d)']
holds |. f/.y .| <= K by A6;
hence |. integral(f,c,d) .| <= n*K * |.d-c.|
by A1,A2,Th30,A11,INTEGR19:32;
end;
let x0 be Real;
assume A12: x0 in [.a,b.]; then
A13: x0 in dom F by INTEGRA5:def 3,A1;
for r be Real st 0<r ex s be Real
st 0<s & for x1 be Real st
x1 in dom F & |.(x1-x0).|<s
holds |. F/.x1 - F/.x0 .|<r
proof
let r be Real;
assume A14:0<r;
A15: 0 < (n*K) by A5,XREAL_1:129;
then consider s be Real such that
A16: 0 < s & s < r/(n*K) by XREAL_1:5,A14,XREAL_1:139;
s*(n*K ) < (r/(n*K))*(n*K ) by A15,A16,XREAL_1:68;
then
A17: 0<s & n*K *s < r by A15,XCMPLX_1:87,A16;
take s;
thus 0 < s by A16;
let x1 be Real;
assume A18: x1 in dom F & |.(x1-x0).|<s; then
A19: x0 in ['a,b'] & x1 in ['a,b'] by A1,A12,INTEGRA5:def 3;
then
A20: |. integral(f,x0,x1) .| <= n*K * |.x1-x0.| by A10;
n*K * |.x1-x0.| <= n*K *s by A5,A18,XREAL_1:64;
then
A21: n*K * |.x1-x0.| < r by A17,XXREAL_0:2;
A22: x0 in [.a,b.] & x1 in [.a,b.] by A1,A12,INTEGRA5:def 3,A18;
A23: F/.x0 = F.x0 by A19,A1,PARTFUN1:def 6
.= integral(f,a,x0) by A1,A12;
A24: F/.x1 = F.x1 by A18,PARTFUN1:def 6
.=integral(f,a,x1) by A22,A1;
reconsider R1= F/.x0 as Element of n-tuples_on REAL;
reconsider R2= integral(f,x0,x1) as Element of n-tuples_on REAL;
F/.x0 + integral(f,x0,x1) - F/.x0
= integral(f,x0,x1) by RVSUM_1:42;
then |. F/.x1 - F/.x0 .| <= n*K * |.x1-x0.|
by A24,A23,A2,Th30,A19,A1,INTEGR19:31,A20;
hence thesis by A21,XXREAL_0:2;
end;
hence F is_continuous_in x0 by A13,NFCONT_4:3;
end;
theorem Th32:
for f be continuous PartFunc of REAL,REAL-NS n st dom f = [' a,b ']
holds f|([' a,b ']) is bounded
proof
let f be continuous PartFunc of REAL,REAL-NS n;
assume A1: dom f =[' a,b '];
reconsider g = f as PartFunc of REAL, REAL n by REAL_NS1:def 4;
g is continuous by NFCONT_4:23;
then g|([' a,b ']) is bounded by A1,Th29;
hence f|([' a,b ']) is bounded by INTEGR19:34;
end;
theorem Th33:
for f be continuous PartFunc of REAL,REAL-NS n st dom f = [' a,b ']
holds f is_integrable_on [' a,b ']
proof
let f be continuous PartFunc of REAL,REAL-NS n;
assume A1: dom f =[' a,b '];
reconsider g = f as PartFunc of REAL, REAL n by REAL_NS1:def 4;
A2: g is continuous by NFCONT_4:23; then
A3: g is_integrable_on [' a,b '] by A1,Th30;
g|([' a,b ']) is bounded by A2,A1,Th29;
hence thesis by A1,A3,INTEGR19:44;
end;
theorem Th34:
for f be continuous PartFunc of REAL,REAL-NS n,
F be PartFunc of REAL,REAL-NS n
st a <= b
& dom f =[' a,b '] & dom F =[' a,b ']
& for t be Real st t in [.a,b.] holds F.t = integral(f,a,t)
holds
for x be Real st x in [.a,b.] holds F is_continuous_in x
proof
let f be continuous PartFunc of REAL,REAL-NS n,
F be PartFunc of REAL,REAL-NS n;
assume A1: a <= b & dom f =[' a,b '] & dom F =[' a,b ']
& for t be Real st t in [.a,b.]
holds F.t = integral(f,a,t);
reconsider f0= f,F0= F as PartFunc of REAL, REAL n by REAL_NS1:def 4;
A2: f | ['a,b'] is bounded by A1,Th32;
a in [.a,b.] by A1; then
A3: a in ['a,b'] by A1,INTEGRA5:def 3;
A4: f0 is continuous by NFCONT_4:23;
A5: now let t be Real;
assume A6:t in [.a,b.];then
A7:t in ['a,b'] by A1,INTEGRA5:def 3;
thus F0.t = integral(f,a,t) by A1,A6
.= integral(f0,a,t) by A1,A7,A2,Th33,A3,INTEGR19:48;
end;
now let x be Real;
assume x in [.a,b.]; then
F0 is_continuous_in x by A4,A5,A1,Th31;
hence F is_continuous_in x by NFCONT_4:1;
end;
hence thesis;
end;
theorem Th35:
for R be PartFunc of REAL, REAL
st R is total holds R is RestFunc-like iff
for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
st z <> 0 & |. z .| < d holds |.z.|"* |. R/.z .| < r
proof
let R be PartFunc of REAL,REAL such that
A1: R is total;
thus R is RestFunc-like implies
for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
st z <> 0 & |. z .| < d holds |.z.|"* |. R/.z .| < r
proof
assume
A2: R is RestFunc-like;
given r be Real such that
A3: r > 0 and
A4: for d be Real st d > 0 holds ex z be Real st z <> 0 & |. z .| < d
& not ( |. z .|"* |. R/.z .|) < r;
defpred P[Nat,Real] means $2 <> 0
& |. $2 .| < (1/($1+1 )) & not ( ( |. $2 .|"* |. R/.$2 .|) < r );
A5: for n be Element of NAT ex z be Element of REAL st P[n,z]
proof
let n be Element of NAT;
reconsider d = 1/(n + 1) as Element of REAL by XREAL_0:def 1;
d <> 0 by XCMPLX_1:50; then
consider z be Real such that A6: z <> 0 & |. z .| < d
& not ( |. z .|"* |. R/.z .|) < r by A4;
reconsider z as Element of REAL by XREAL_0:def 1;
take z;
thus thesis by A6;
end;
consider s be Real_Sequence such that
A7: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A5);
A8: for n being Nat holds P[n,s.n]
proof
let n be Nat; n in NAT by ORDINAL1:def 12;
hence thesis by A7;
end;
A9: now
let p be Real;
assume
A10: 0<p;
consider n be Nat such that
A11: p"<n by SEQ_4:3;
reconsider q0=0,q1=1 as Real;
p" + q0 < n + q1 by A11,XREAL_1:8; then
A12: 1/(n+1) < 1/p" by A10,XREAL_1:76;
take n;
let m be Nat;
A13: m in NAT by ORDINAL1:def 12;
assume n<=m; then
A14: n + 1 <= m + 1 by XREAL_1:6;
1/(m+1) <= 1/(n+1) by A14,XREAL_1:118; then
A15: |. s.m - 0 .| < 1/(n+1) by A7,XXREAL_0:2,A13;
1/p" = p by XCMPLX_1:216;
hence |. s.m - 0 .| <p by A12,A15,XXREAL_0:2;
end;
A16: s is convergent by A9,SEQ_2:def 6;
then lim s = 0 by A9,SEQ_2:def 7;
then reconsider s as non-zero 0-convergent Real_Sequence
by A16,A8,SEQ_1:5,FDIFF_1:def 1;
(s")(#)(R/*s) is convergent & lim ((s")(#)(R/*s)) = 0
by A2;
then consider n0 be Nat such that
A17: for m be Nat st n0 <=m holds |. ((s")(#)(R/*s)).
m- 0 .| < r by A3,SEQ_2:def 7;
reconsider n0 as Element of NAT by ORDINAL1:def 12;
A18: |.(s.n0)"*(R/.(s.n0)).| = |.((s.n0)").| * |.(R/.(s.n0)).| by COMPLEX1:65
.=|. s.n0 .|" * |.(R/.(s.n0)).| by COMPLEX1:66;
dom R = REAL by A1,PARTFUN1:def 2; then
A19: rng s c= dom R;
|. ((s")(#)(R/*s)).n0- 0 .|
= |.(s".n0)*((R/*s).n0).| by SEQ_1:8
.= |.(s.n0)"*((R/*s).n0).| by VALUED_1:10
.= |.(s.n0)"*(R/.(s.n0)).| by A19,FUNCT_2:109;
hence contradiction by A7,A17,A18;
end;
assume
A20: for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
st z <> 0 & |. z .| < d holds ( |. z .|"* |. R/.z .|) < r;
thus R is total by A1;
let s be non-zero 0-convergent Real_Sequence;
A21: s is convergent & lim s = 0;
A22: now
let r be Real;
assume r > 0;
then consider d be Real such that
A23: d > 0 and
A24: for z be Real st z <> 0 & |. z .| < d holds
( |. z .| "* |. R/.z .|) < r by A20;
consider n0 be Nat such that
A25: for m be Nat st n0 <=m holds |. s.m-0 .| < d by A21,A23,SEQ_2:def 7;
take n0;
thus for m be Nat st n0 <=m holds |. ((s")(#)(R/*s)).m- 0 .| < r
proof
dom R = REAL by A1,PARTFUN1:def 2; then
A26: rng s c= dom R;
let m be Nat;
A27: m in NAT by ORDINAL1:def 12;
assume n0 <= m; then
A28: |. s.m-0 .| < d by A25;
|. s.m .|" * |.(R/.(s.m)).| = |.((s.m)").| * |.(R/.(s.m)).|
by COMPLEX1:66
.= |.(s.m)"*(R/.(s.m)).| by COMPLEX1:65
.= |.(s.m)"*((R/*s).m).| by A26,FUNCT_2:109,A27
.= |.(s".m)*((R/*s).m).| by VALUED_1:10
.= |. ((s")(#)(R/*s)).m- 0 .| by SEQ_1:8;
hence thesis by A24,A28,SEQ_1:5;
end;
end;
hence (s")(#)(R/*s) is convergent by SEQ_2:def 6;
hence lim ((s")(#)(R/*s)) = 0 by A22,SEQ_2:def 7;
end;
reserve
Z for open Subset of REAL,
y0 for VECTOR of REAL-NS n,
G for Function of REAL-NS n,REAL-NS n;
theorem Th36:
for f be continuous PartFunc of REAL,REAL-NS n,
g be PartFunc of REAL,REAL-NS n st a <= b
& dom f = [' a,b '] & dom g = [' a,b '] & Z = ]. a,b .[
& for t be Real st t in [' a,b ']
holds g.t = y0+ integral(f,a,t) holds
g is continuous & g/.a=y0 &
g is_differentiable_on Z
& for t be Real st t in Z holds diff(g,t) = f/.t
proof
let f be continuous PartFunc of REAL,REAL-NS n,
g be PartFunc of REAL,REAL-NS n;
assume A1:a <= b & dom f = [' a,b '] & dom g = [' a,b '] & Z = ]. a,b .[
& for t be Real st t in [' a,b '] holds g.t = y0+ integral(f,a,t);
A2: f is_integrable_on ['a,b'] by A1,Th33;
A3: f| ['a,b'] is bounded by A1,Th32;
A4: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
deffunc FX(Element of REAL) = integral(f,a,$1);
consider F0 be Function of REAL,REAL-NS n such that
A5: for x be Element of REAL
holds F0.x = FX(x) from FUNCT_2:sch 4;
set F = F0| ['a,b'];
A6: dom F = dom F0 /\ ['a,b'] by RELAT_1:61
.= REAL /\ ['a,b'] by FUNCT_2:def 1
.= ['a,b'] by XBOOLE_1:28;
A7: now let x be Real;
assume x in [.a,b.]; then
A8: x in ['a,b'] by A1,INTEGRA5:def 3;
A9: x in REAL by XREAL_0:def 1;
thus F.x = F0.x by A8,A6,FUNCT_1:47
.= integral(f,a,x) by A5,A9;
end;
A10: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
A11: for x be Real st x in [.a,b.]
holds F is_continuous_in x by Th34,A1,A6,A7;
A12: for x be Real st x in ].a,b.[
holds F.x = integral(f,a,x) by A7,A10;
A13: Z c= dom F by A1,A6,A10,INTEGRA5:def 3;
A14: now let x be Real;
assume A15: x in Z;
then f is_continuous_in x by A10,A4,A1,NFCONT_3:def 2;
hence F is_differentiable_in x & diff(F,x)=f/.x
by A15,A1,A2,A3,A12,A13,INTEGR19:55;
end;
then for x be Real st x in Z holds F is_differentiable_in x;
then
A16: F is_differentiable_on Z by A13,NDIFF_3:10;
set G0 = REAL --> y0;
set G = G0| ['a,b'];
A17: dom G = dom G0 /\ ['a,b'] by RELAT_1:61
.= REAL /\ ['a,b']
.= ['a,b'] by XBOOLE_1:28;
A18: now let x be Real;
assume x in [.a,b.]; then
A19: x in ['a,b'] by A1,INTEGRA5:def 3;
thus G.x = G0.x by A19,A17,FUNCT_1:47
.= y0 by XREAL_0:def 1,FUNCOP_1:7;
end;
A20: F is continuous by A4,A6,A11,NFCONT_3:def 2;
A21: G|Z is constant; then
A22: G is_differentiable_on Z &
for x be Real st x in Z holds (G`|Z).x = 0.(REAL-NS n)
by A17,A1,A10,A4,NDIFF_3:20;
A23: dom g = dom F /\ dom G by A6,A17,A1;
now let x be Element of REAL;
assume A24: x in dom g;
A25: x in [.a,b.] by A24,A1,INTEGRA5:def 3;
A26: G/.x = G.x by A24,A1,A17,PARTFUN1:def 6
.= y0 by A25,A18;
A27: F/.x = F.x by A24,A1,A6,PARTFUN1:def 6
.= integral(f,a,x) by A25,A7;
thus g/.x = g.x by A24,PARTFUN1:def 6
.= G/.x + F/.x by A26,A27,A1,A24;
end; then
A28: g = G + F by A23,VFUNCT_1:def 1;
thus g is continuous by A20,A28;
A29: a in ['a,b'] by A1,A4;
A30: 0.(REAL-NS n)
=integral(f,a,a) - integral(f,a,a) by RLVECT_1:15
.= integral(f,a,a) + integral(f,a,a) - integral(f,a,a)
by A29,A1,Th33,A3,INTEGR19:53
.= integral(f,a,a) + ( integral(f,a,a) - integral(f,a,a) )
by RLVECT_1:28
.= integral(f,a,a) + 0.(REAL-NS n) by RLVECT_1:15
.= integral(f,a,a);
thus g/.a = g.a by A1,A29,PARTFUN1:def 6
.= y0+ integral(f,a,a) by A1,A29
.= y0 by A30;
A31: g is_differentiable_on Z &
for x be Real st x in Z holds
(g`|Z).x = diff(G,x) + diff(F,x) by A28,A16,A22,A1,A10,A4,NDIFF_3:17;
thus g is_differentiable_on Z by A28,A16,A22,A1,A10,A4,NDIFF_3:17;
thus for t be Real st t in Z holds diff(g,t) = f/.t
proof
let t be Real;
assume A32: t in Z;
A33: diff(g,t) =(g`|Z).t by A31,A32,NDIFF_3:def 6
.=diff(G,t) + diff(F,t)
by A28,A16,A22,A1,A10,A4,NDIFF_3:17,A32;
A34: diff(G,t) = (G`|Z).t by A22,A32,NDIFF_3:def 6
.= 0.(REAL-NS n) by A21,A17,A1,A10,A4,NDIFF_3:20,A32;
thus diff(g,t) = 0.(REAL-NS n) + f/.t by A33,A34,A14,A32
.= f/.t;
end;
end;
theorem
for i be Nat,
y1,y2 be Point of REAL-NS n holds
proj(i,n).(y1 + y2) = proj(i,n).y1 + proj(i,n).y2
proof
let i be Nat,
y1,y2 be Point of REAL-NS n;
reconsider yy1 = y1, yy2 = y2 as Element of REAL n by REAL_NS1:def 4;
reconsider ry1 = yy1.i as Real;
reconsider ry2 = yy2.i as Real;
A1: proj(i,n).y1 = ry1 & proj(i,n).y2 = ry2 by PDIFF_1:def 1;
proj(i,n).(y1 + y2) = proj(i,n).(yy1 + yy2) by REAL_NS1:2
.= (yy1 + yy2).i by PDIFF_1:def 1
.= ry1 + ry2 by RVSUM_1:11;
hence thesis by A1;
end;
theorem Th38:
for i be Nat,
y1 be Point of REAL-NS n, r being Real holds
proj(i,n).(r*y1) = r*(proj(i,n).y1)
proof
let i be Nat,
y1 be Point of REAL-NS n, r be Real;
reconsider yy1 = y1 as Element of REAL n by REAL_NS1:def 4;
reconsider y1i = yy1.i as Element of REAL by XREAL_0:def 1;
proj(i,n).(r*y1) = proj(i,n).(r*yy1) by REAL_NS1:3
.= (r*yy1).i by PDIFF_1:def 1
.= r* y1i by RVSUM_1:44;
hence thesis by PDIFF_1:def 1;
end;
theorem Th39:
for g be PartFunc of REAL,REAL-NS n,
x0 be Real,
i be Nat st
1 <= i & i <= n & g is_differentiable_in x0 holds
(proj(i,n)*g) is_differentiable_in x0 &
proj(i,n).(diff(g,x0)) = diff((proj(i,n)*g),x0)
proof
let g be PartFunc of REAL,REAL-NS n,
x0 be Real,
i be Nat;
assume A1: 1 <= i & i <= n & g is_differentiable_in x0; then
consider N being Neighbourhood of x0 such that
A2: N c= dom g & ex DFG be LinearFunc of REAL-NS n,
GR be RestFunc of REAL-NS n st diff(g,x0) = DFG/.1 &
for x be Real st x in N holds
g/.x - g/.x0 = DFG/.(x-x0) + GR/.(x-x0) by NDIFF_3:def 4;
consider DFG be LinearFunc of REAL-NS n,
GR be RestFunc of REAL-NS n such that
A3: diff(g,x0) = DFG/.1 &
for x be Real st x in N holds
g/.x - g/.x0 = DFG/.(x-x0) + GR/.(x-x0) by A2;
consider LP be Point of REAL-NS n such that
A4: for p be Real holds DFG/.p = p*LP by NDIFF_3:def 2;
A5: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
reconsider PG = proj(i,n) as Function of REAL-NS n,REAL;
the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
reconsider L = proj(i,n)*DFG as Function of REAL,REAL;
A6: for r being Real holds L.r = (proj(i,n).LP)*r
proof
let r be Real;
A7: dom L = REAL by FUNCT_2:def 1;
dom DFG = REAL by FUNCT_2:def 1; then
DFG.r = DFG/.r by XREAL_0:def 1,PARTFUN1:def 6 .= r*LP by A4; then
proj(i,n).(DFG.r) = r*(proj(i,n).LP) by Th38;
hence L.r = (proj(i,n).LP)*r by A7,FUNCT_1:12,XREAL_0:def 1;
end;
reconsider L as LinearFunc by A6,FDIFF_1:def 3;
A8: GR is total by NDIFF_3:def 1; then
reconsider FGR = GR as Function of REAL,REAL-NS n;
A9: proj(i,n)*FGR is Function of REAL,REAL by A5;
proj(i,n)*GR is RestFunc
proof
A10: dom GR = REAL by A8,PARTFUN1:def 2;
reconsider R = proj(i,n)*GR as PartFunc of REAL,REAL;
for r be Real st r > 0 ex d be Real st d > 0 &
(for z be Real st z <> 0 & |.z.| < d
holds (|.z.|" * |. R/.z .|) < r)
proof
let r be Real;
assume r > 0; then
consider d be Real such that
A11: d > 0 & (for z be Real st z <> 0 & |.z.| < d holds
(|.z.|"* ||. GR/.z .||) < r) by A8,NDIFF_4:23;
take d;
thus d> 0 by A11;
let z be Real;
assume A12: z <> 0 & |.z.| < d;
A13: z in REAL by XREAL_0:def 1;
A14: GR/.z = GR.z by A10,PARTFUN1:def 6,XREAL_0:def 1;
A15: i in Seg n by A1;
reconsider GRz = GR/.z as Point of REAL-NS n;
reconsider GRz1 = GRz as Element of REAL n by REAL_NS1:def 4;
reconsider GRzi = GRz1.i as Real;
the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
dom proj(i,n) = the carrier of REAL-NS n by PARTFUN1:def 2; then
A16: z in dom (proj(i,n)*GR) by A10,A14,FUNCT_1:11,A13; then
A17: (proj(i,n)*GR).z = proj(i,n).(GR.z) by FUNCT_1:12
.= proj(i,n).(GRz1) by A10,A13,PARTFUN1:def 6;
A18: |.GRzi.| <= ||. GR/.z .|| by A15,REAL_NS1:9;
A19: 0 <= |.z.| by COMPLEX1:46;
0 <= |.GRzi.| by COMPLEX1:46; then
A20: |.z.|"* |.GRzi.| <= |.z.|"* ||. GR/.z .|| by A18,A19,XREAL_1:66;
|.z.|"* ||. GR/.z .|| < r by A11,A12; then
A21: |.z.|"* |.GRzi.| < r by A20,XXREAL_0:2;
reconsider Rz = (proj(i,n)*GR).z as Element of REAL by XREAL_0:def 1;
|.z.|"* |. Rz .| < r by A21,PDIFF_1:def 1,A17;
hence thesis by A16,PARTFUN1:def 6;
end;
hence thesis by A9,Th35;
end; then
reconsider R = proj(i,n)*GR as RestFunc;
set pg = proj(i,n)*g;
the carrier of REAL-NS n = REAL n by REAL_NS1:def 4; then
dom proj(i,n) = the carrier of REAL-NS n by FUNCT_2:def 1; then
rng g c= dom proj(i,n); then
A22: dom g = dom (proj(i,n)*g) by RELAT_1:27;
A23: for x be Real st x in N holds
pg.x - pg.x0 = L.(x-x0) + R.(x-x0)
proof
let x be Real;
reconsider xx = x as Element of REAL by XREAL_0:def 1;
now assume A24: x in N; then
A25: g/.x - g/.x0 = DFG/.(xx-x0) + GR/.(xx-x0) by A3;
A26: x0 in N by RCOMP_1:16;
A27: g/.x = g.x & g/.x0 = g.x0 by A2,A24,A26,PARTFUN1:def 6;
reconsider PGSx = pg.x - pg.x0 as Element of REAL by XREAL_0:def 1;
reconsider PGdx = pg.x as Element of REAL by XREAL_0:def 1;
reconsider PGdx0 = pg.x0 as Element of REAL by XREAL_0:def 1;
g.x in rng g by A2,A24,FUNCT_1:3; then
reconsider Gx = g.x as Element of REAL n by REAL_NS1:def 4;
g.x0 in rng g by A2,A26,FUNCT_1:3; then
reconsider Gx0 = g.x0 as Element of REAL n by REAL_NS1:def 4;
set projGx = proj(i,n).(g.x);
reconsider projGx as Element of REAL by XREAL_0:def 1;
set projGx0 = proj(i,n).(g.x0);
reconsider projGx0 as Element of REAL by XREAL_0:def 1;
reconsider Gx1 = Gx as Element of REAL-NS n by REAL_NS1:def 4;
reconsider Gx01 = Gx0 as Element of REAL-NS n by REAL_NS1:def 4;
reconsider Gsx = g/.x as Element of REAL n by REAL_NS1:def 4;
reconsider Gsx0 = g/.x0 as Element of REAL n by REAL_NS1:def 4;
reconsider dxx0 = x-x0 as Element of REAL by XREAL_0:def 1;
reconsider Ldxx0 = L.(x-x0) as Element of REAL by XREAL_0:def 1;
A28: dom R = REAL by A9,PARTFUN1:def 2;
reconsider Rdxx0 = R.(x-x0) as Element of REAL by XREAL_0:def 1;
reconsider Lxx0Rxx0 = L.(x-x0) + R.(x-x0) as Element of REAL
by XREAL_0:def 1;
reconsider Ldiff = DFG/.(x-x0) as Element of REAL n by REAL_NS1:def 4;
set projLdiff = proj(i,n).Ldiff;
reconsider projLdiff as Element of REAL;
A29: dom GR = REAL by A8,PARTFUN1:def 2; then
GR.dxx0 in rng GR by FUNCT_1:3; then
reconsider Rdiff = GR.dxx0 as Element of REAL n by REAL_NS1:def 4;
set projRdiff = proj(i,n).Rdiff;
reconsider projRdiff as Element of REAL;
dom DFG = REAL by FUNCT_2:def 1; then
A30: Ldiff = DFG.(x-x0) by PARTFUN1:def 6,XREAL_0:def 1;
dom L = REAL by FUNCT_2:def 1; then
A31: L.(x-x0) = proj(i,n).Ldiff by FUNCT_1:12,XREAL_0:def 1,A30;
A32: R.(x-x0) = proj(i,n).Rdiff by A28,FUNCT_1:12;
A33: proj(i,n).Ldiff = Ldiff.i by PDIFF_1:def 1;
A34: proj(i,n).Rdiff = Rdiff.i by PDIFF_1:def 1;
reconsider diffGR = DFG/.(x-x0) + GR/.(x-x0)
as Element of REAL n by REAL_NS1:def 4;
reconsider Rsdiff = GR/.(x-x0) as Element of REAL n by REAL_NS1:def 4;
PGSx = projGx - PGdx0 by A2,A22,A24,FUNCT_1:12
.= proj(i,n).Gx1 - proj(i,n).Gx01 by A2,A22,A26,FUNCT_1:12
.= Gx.i - proj(i,n).Gx01 by PDIFF_1:def 1
.= Gx.i - Gx0.i by PDIFF_1:def 1
.= (Gsx - Gsx0).i by A27,RVSUM_1:27
.= diffGR.i by A25,REAL_NS1:5
.= (Ldiff + Rsdiff).i by REAL_NS1:2
.= Ldiff.i + Rsdiff.i by RVSUM_1:11;
hence thesis by A31,A33,A34,A29,PARTFUN1:def 6,A32;
end;
hence thesis;
end;
hence A35: proj(i,n)*g is_differentiable_in x0 by A2,A22;
L.1 = 1*(proj(i,n).LP) by A6
.= proj(i,n).((1 qua Real) * LP) by RLVECT_1:def 8
.= proj(i,n).diff(g,x0) by A3,A4;
hence proj(i,n).diff(g,x0) = diff((proj(i,n)*g),x0)
by A35,A2,A22,A23,FDIFF_1:def 5;
end;
Lm7:
for i be Nat holds proj(i,n).(0.(REAL-NS n)) = 0
proof
let i be Nat;
thus proj(i,n).(0.(REAL-NS n)) = proj(i,n).(0*n) by REAL_NS1:def 4
.= (0*n).i by PDIFF_1:def 1
.= 0;
end;
theorem Th40:
for f be PartFunc of REAL,REAL-NS n,
X be set st
for i be Nat st 1 <= i & i <= n
holds (proj(i,n)*f) | X is constant
holds
f| X is constant
proof
let f be PartFunc of REAL,REAL-NS n, X be set;
assume A1: for i be Nat st 1 <= i & i <= n
holds (proj(i,n)*f) | X is constant;
A2: the carrier of (REAL-NS n) = REAL n by REAL_NS1:def 4;
now let x,y be object;
assume A3: x in dom (f| X) & y in dom (f| X); then
A4: x in dom f & x in X & y in dom f & y in X by RELAT_1:57;
f.x in rng f by A4,FUNCT_1:3; then
reconsider fx=f.x as Element of REAL n by REAL_NS1:def 4;
f.y in rng f by A4,FUNCT_1:3; then
reconsider fy=f.y as Element of REAL n by REAL_NS1:def 4;
A5: len fy =n by CARD_1:def 7;
A6: len fx =n by CARD_1:def 7;
now let i be Nat;
assume
A7: 1 <= i & i <= len fx;
dom proj(i,n) = the carrier of REAL-NS n by A2,FUNCT_2:def 1; then
rng f c= dom proj(i,n); then
A8: dom f = dom (proj(i,n)*f) by RELAT_1:27;
A9: ((proj(i,n)*f) | X).x
=((proj(i,n)*f)).x by A3,FUNCT_1:49
.= proj(i,n).(f.x) by A4,FUNCT_1:13
.= fx.i by PDIFF_1:def 1;
A10: ((proj(i,n)*f) | X).y
=((proj(i,n)*f)).y by A3,FUNCT_1:49
.= proj(i,n).(f.y) by A4,FUNCT_1:13
.= fy.i by PDIFF_1:def 1;
A11: (proj(i,n)*f) | X is constant by A1,A7,A6;
x in dom ((proj(i,n)*f) | X) & y in dom ((proj(i,n)*f) | X)
by A8,A4,RELAT_1:57;
hence fx.i = fy.i by A9,A10,A11,FUNCT_1:def 10;
end; then
A12: fx=fy by A5,CARD_1:def 7;
thus (f| X).x = f.x by A3,FUNCT_1:49
.=(f| X).y by A3,A12,FUNCT_1:49;
end;
hence thesis by FUNCT_1:def 10;
end;
theorem Th41:
for f be PartFunc of REAL,REAL-NS n
st ].a,b.[ c= dom f
& f is_differentiable_on ].a,b.[
& for x be Real
st x in ].a,b.[ holds diff(f,x) = 0.(REAL-NS n)
holds f| (].a,b.[) is constant
proof
let f be PartFunc of REAL,REAL-NS n;
assume A1: ].a,b.[ c= dom f & f is_differentiable_on ].a,b.[
& for x be Real st x in ].a,b.[ holds diff(f,x) = 0.(REAL-NS n);
reconsider Z = ].a,b.[ as open Subset of REAL;
now let i be Nat;
assume A2: 1 <= i & i <= n;
A3: now let x be Real;
assume x in Z; then
f is_differentiable_in x by A1,NDIFF_3:10;
hence (proj(i,n)*f) is_differentiable_in x &
proj(i,n).(diff(f,x)) = diff((proj(i,n)*f),x) by A2,Th39;
end;
A4: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
dom (proj(i,n)) = REAL n by FUNCT_2:def 1; then
rng f c= dom (proj(i,n)) by A4; then
A5: Z c= dom (proj(i,n)*f) by A1,RELAT_1:27;
for x be Real st x in Z holds
(proj(i,n)*f) is_differentiable_in x by A3; then
A6: (proj(i,n)*f) is_differentiable_on ].a,b.[ by A5,FDIFF_1:9;
for x be Real st x in ].a,b.[ holds diff((proj(i,n)*f),x) = 0
proof
let x be Real;
assume A7: x in ].a,b.[; then
A8: proj(i,n).(diff(f,x)) = diff((proj(i,n)*f),x) by A3;
diff(f,x) = 0.(REAL-NS n) by A1,A7;
hence diff((proj(i,n)*f),x) = 0 by Lm7,A8;
end;
hence (proj(i,n)*f) | ].a,b.[ is constant by A6,ROLLE:7;
end;
hence thesis by Th40;
end;
theorem Th42:
for f be continuous PartFunc of REAL,REAL-NS n st a < b
& [.a,b.] = dom f & f | ].a,b.[ is constant holds
for x be Real st x in [.a,b.] holds f.x = f.a
proof
let f be continuous PartFunc of REAL,REAL-NS n;
assume A1: a < b & [.a,b.] = dom f & f| (].a,b.[) is constant;
A2: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
reconsider d = (b-a)/2 as Real;
A3: 0 < b-a by A1,XREAL_1:50; then
A4: 0 < d by XREAL_1:215;
a+(b-a)/2 = (a+b) / 2; then
A5: a < a+d & a+d < b by A1,XREAL_1:226; then
a+d in ].a,b.[; then
f.(a+d) in rng f by A2,A1,FUNCT_1:3; then
reconsider f0=f.(a+d) as Point of REAL-NS n;
A6: dom (f| (].a,b.[) ) = dom f /\ (].a,b.[) by RELAT_1:61
.= ].a,b.[ by A1,XXREAL_1:25,XBOOLE_1:28;
A7: now let x be Real;
assume A8: x in ].a,b.[;
A9: a+d in dom (f| (].a,b.[) ) by A5,A6;
thus f/.x = f.x by A8,A2,A1,PARTFUN1:def 6
.= (f| (].a,b.[) ).x by A6,A8,FUNCT_1:47
.= (f| (].a,b.[) ).(a+d) by A1,A6,A8,A9,FUNCT_1:def 10
.=f0 by A9,FUNCT_1:47;
end;
A10: a in dom f by A1;
A11: b in dom f by A1;
deffunc F1(Nat) = a+d/($1+1);
A12: for x being Element of NAT holds F1(x) is Element of REAL
by XREAL_0:def 1;
consider s1 be Real_Sequence such that
A13: for x being Element of NAT holds s1.x = F1(x) from FUNCT_2:sch 9(A12);
A14: f is_continuous_in a by A10,NFCONT_3:def 2;
A15: now let y be object;
assume y in rng s1; then
consider x be object such that
A16: x in dom s1 & y=s1.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A16;
A17: y = a+d/(x+1) by A13,A16;
A18: 0 < d/(x+1) by A4,XREAL_1:139;
1 + (0 qua Real) <= 1 + x by XREAL_1:7; then
A19: d/(x+1) <= d / 1 by XREAL_1:118,A3;
A20: a + (0 qua Real) < a + d/(x+1) by A18,XREAL_1:8;
a + d/(x+1) <= a + d by A19,XREAL_1:7; then
a + d/(x+1) < b by A5,XXREAL_0:2;
hence y in ].a,b.[ by A17,A20;
end; then
A21: rng s1 c= ].a,b.[ by TARSKI:def 3; then
A22: rng s1 c= dom f by A2,A1,XBOOLE_1:1;
A23: now let p be Real;
assume A24: 0<p;
consider n be Nat such that
A25: d/p < n by SEQ_4:3;
n + (0 qua Real) < n + 1 by XREAL_1:8; then
d/p < n + 1 by XXREAL_0:2,A25; then
(d/p)*p < (n + 1)*p by A24,XREAL_1:68; then
A26: d < (n + 1)*p by A24,XCMPLX_1:87;
A27: d/(n+1) < p by A26,XREAL_1:83;
A28: |.(d/(n+1)).| = d/(n+1) by A3,ABSVALUE:def 1;
A29: |.(d/(n+1)).| < p by A27,A3,ABSVALUE:def 1;
take n;
thus for m be Nat st n<=m holds |.(s1.m-a).| < p
proof
let m be Nat;
A30: m in NAT by ORDINAL1:def 12;
assume n<=m; then
A31: n+1 <= m+1 by XREAL_1:7;
d/(m+1) <= d/(n+1) by A3,A31,XREAL_1:118; then
A32: |.(d/(m+1)).| <= |.(d/(n+1)).| by A28,A3,ABSVALUE:def 1;
|.(s1.m-a).| = |.(a+d/(m+1) -a ).| by A13,A30
.= |.(d/(m+1)).|;
hence |.(s1.m-a).| < p by A32,A29,XXREAL_0:2;
end;
end; then
A33: s1 is convergent by SEQ_2:def 6; then
A34: lim s1 = a by A23,SEQ_2:def 7;
A35: f/*s1 is convergent & f/.a = lim (f/*s1)
by A14,A22,A33,A34,NFCONT_3:def 1;
A36: for i be Nat holds (f/*s1).i = f0
proof
let i be Nat;
A37: i in NAT by ORDINAL1:def 12; then
A38: s1.i in rng s1 by FUNCT_2:4;
thus (f/*s1).i = f/.(s1.i) by A21,FUNCT_2:109,XBOOLE_1:1,A1,A2,A37
.= f0 by A7,A38,A15;
end;
now let r be Real;
assume A39: 0 < r;
reconsider m = the Element of NAT as Nat;
take m;
thus for k be Nat st m <= k holds ||.(f/*s1).k - f0.|| < r
proof
let k be Nat;
assume m <= k;
||.(f/*s1).k - f0.|| = ||.f0 - f0.|| by A36
.= ||. 0.(REAL-NS n) .|| by RLVECT_1:15
.= 0;
hence thesis by A39;
end;
end; then
lim (f/*s1) =f0 by A35,NORMSP_1:def 7; then
A40: f.a = f0 by A35,A10,PARTFUN1:def 6;
deffunc F2(Nat) = b-d/($1+1);
A41: for x being Element of NAT holds F2(x) is Element of REAL
by XREAL_0:def 1;
consider s2 be Real_Sequence such that
A42: for x being Element of NAT holds s2.x = F2(x) from FUNCT_2:sch 9(A41);
A43: f is_continuous_in b by A11,NFCONT_3:def 2;
A44: now let y be object;
assume y in rng s2; then
consider x be object such that
A45: x in dom s2 & y=s2.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A45;
A46: y = b-d/(x+1) by A42,A45;
A47: 0 < d/(x+1) by A4,XREAL_1:139;
1 + (0 qua Real) <= 1 + x by XREAL_1:7; then
A48: d/(x+1) <= d / 1 by XREAL_1:118,A3;
A49: b - d/(x+1) < b - (0 qua Real) by A47,XREAL_1:15;
b - d <= b - d/(x+1) by A48,XREAL_1:13; then
a < b - d/(x+1) by A5,XXREAL_0:2;
hence y in ].a,b.[ by A46,A49;
end; then
A50: rng s2 c= ].a,b.[ by TARSKI:def 3; then
A51: rng s2 c= dom f by A2,A1,XBOOLE_1:1;
A52: now let p be Real;
assume A53: 0<p;
consider n be Nat such that
A54: d/p < n by SEQ_4:3;
n + (0 qua Real) < n + 1 by XREAL_1:8; then
d/p < n + 1 by XXREAL_0:2,A54; then
(d/p)*p < (n + 1)*p by A53,XREAL_1:68; then
A55: d < (n + 1)*p by A53,XCMPLX_1:87;
A56: d/(n+1) < p by A55,XREAL_1:83;
take n;
thus for m be Nat st n<=m holds |.(s2.m-b).| < p
proof
let m be Nat;
A57: m in NAT by ORDINAL1:def 12;
assume n<=m; then
A58: n+1 <= m+1 by XREAL_1:7;
A59: d/(m+1) <= d/(n+1) by A3,A58,XREAL_1:118;
A60: |.(d/(m+1)).| = d/(m+1) by A3,ABSVALUE:def 1;
|.(s2.m-b).| = |.(b-d/(m+1) -b ).| by A42,A57
.= |.(-d/(m+1)).|
.= |.(d/(m+1)).| by COMPLEX1:52;
hence |.(s2.m-b).| < p by A60,XXREAL_0:2,A59,A56;
end;
end; then
A61: s2 is convergent by SEQ_2:def 6; then
A62: lim s2 = b by A52,SEQ_2:def 7;
A63: f/*s2 is convergent & f/.b = lim (f/*s2)
by A43,A51,A61,A62,NFCONT_3:def 1;
A64: for i be Element of NAT holds (f/*s2).i = f0
proof
let i be Element of NAT;
A65: s2.i in rng s2 by FUNCT_2:4;
thus (f/*s2).i = f/.(s2.i) by A2,A1,XBOOLE_1:1,A50,FUNCT_2:109
.= f0 by A7,A65,A44;
end;
now let r be Real;
assume A66: 0 < r;
reconsider m = the Element of NAT as Nat;
take m;
thus for k be Nat st m <= k holds ||.(f/*s2).k - f0.|| < r
proof
let k be Nat;
assume m <= k;
k in NAT by ORDINAL1:def 12; then
||.(f/*s2).k - f0.|| = ||.f0 - f0.|| by A64
.= ||. 0.(REAL-NS n) .|| by RLVECT_1:15
.= 0;
hence thesis by A66;
end;
end; then
lim (f/*s2) = f0 by A63,NORMSP_1:def 7; then
A67: f.b = f0 by A63,A11,PARTFUN1:def 6;
let x be Real;
assume x in [.a,b.]; then
A68: ex r be Real st x=r & a <=r & r <= b;
per cases;
suppose A69: x in ].a,b.[;
hence f.x = f/.x by A1,A2,PARTFUN1:def 6
.= f.a by A40,A69,A7;
end;
suppose not x in ].a,b.[; then
x <=a or b <= x;
hence f.x =f.a by A40,A67,A68,XXREAL_0:1;
end;
end;
theorem Th43:
for y,Gf be continuous PartFunc of REAL,REAL-NS n,
g be PartFunc of REAL,REAL-NS n st a<b
& Z = ]. a,b .[
& dom y = [' a,b '] & dom g = [' a,b '] & dom Gf = [' a,b ']
& y is_differentiable_on Z
& y/.a = y0
& (for t be Real st t in Z holds diff(y,t) = Gf/.t)
& (for t be Real st t in [' a,b ']
holds g.t = y0 + integral(Gf,a,t) )
holds y=g
proof
let y,Gf be continuous PartFunc of REAL,REAL-NS n,
g be PartFunc of REAL,REAL-NS n;
assume A1: a<b & Z = ]. a,b .[
& dom y = [' a,b '] & dom g =[' a,b '] & dom Gf =[' a,b ']
& y is_differentiable_on Z
& y/.a = y0
& (for t be Real st t in Z holds diff(y,t) = Gf/.t)
& (for t be Real st t in [' a,b '] holds g.t = y0+ integral(Gf,a,t));
then
A2: g is continuous & g/.a=y0 & g is_differentiable_on Z
& for t be Real st t in Z holds diff(g,t) = Gf/.t by Th36;
A3: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
A4: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
reconsider h=y-g as continuous PartFunc of REAL,REAL-NS n by A2;
A5: dom h = [' a,b '] /\ [' a,b '] by A1,VFUNCT_1:def 2
.= [' a,b ']; then
A6: ].a,b.[ c= dom h by A3,XXREAL_1:25;
A7: h is_differentiable_on ].a,b.[ by A1,A2,NDIFF_3:18,A4,A3,A5;
A8: now let x be Real;
assume A9: x in ].a,b.[; then
A10: diff(y,x) = Gf/.x by A1;
A11: diff(g,x) = Gf/.x by A1,A9,Th36;
thus diff(h,x) = ((y-g)`|(].a,b.[)).x by A9,A7,NDIFF_3:def 6
.= Gf/.x - Gf/.x by A10,A11,A1,A2,A6,A9,NDIFF_3:18
.= 0.(REAL-NS n) by RLVECT_1:15;
end;
A12: h| (].a,b.[) is constant by Th41,A5,A7,A8,A3,XXREAL_1:25;
A13: for x being Real st x in dom h holds h.x = 0.(REAL-NS n)
proof
let x be Real;
assume A14: x in dom h;
A15: a in dom h by A5,A1,A3;
thus h.x = h.a by A14,Th42,A1,A12,A3,A5
.= h/.a by A15,PARTFUN1:def 6
.= y0-y0 by A2,A1,A15,VFUNCT_1:def 2
.= 0.(REAL-NS n) by RLVECT_1:15;
end;
for x being Element of REAL st x in dom y holds y.x = g.x
proof
let x be Element of REAL;
assume A16: x in dom y; then
0.(REAL-NS n) = h.x by A13,A1,A5
.= h/.x by A16,A1,A5,PARTFUN1:def 6
.= y/.x -g/.x by A16,A1,A5,VFUNCT_1:def 2; then
A17: y/.x = g/.x by RLVECT_1:21;
thus y.x = g/.x by A17,A16,PARTFUN1:def 6
.= g.x by A16,A1,PARTFUN1:def 6;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th44:
for a,b,c,d be Real,
f be PartFunc of REAL,REAL-NS n
st a <= b & f is_integrable_on ['a,b']
& ||. f .|| is_integrable_on ['a,b']
& f| ['a,b'] is bounded & ['a,b'] c= dom f
& c in ['a,b'] & d in ['a,b']
holds ||. f .|| is_integrable_on ['min(c,d),max(c,d)'] &
(||. f .||) | ['min(c,d),max(c,d)'] is bounded &
||. integral(f,c,d) .|| <= integral((||. f .||),min(c,d),max(c,d))
proof
let a,b,c,d be Real,
f be PartFunc of REAL,REAL-NS n;
assume A1: a <= b & f is_integrable_on ['a,b']
& ||. f .|| is_integrable_on ['a,b']
& f| ['a,b'] is bounded & ['a,b'] c= dom f
& c in ['a,b'] & d in ['a,b'];
reconsider f1=f as PartFunc of REAL,REAL n by REAL_NS1:def 4;
A2: f1 | ['a,b'] is bounded by A1,INTEGR19:34;
A3: f1 is_integrable_on ['a,b'] by A2,A1,INTEGR19:43;
A4: ||. f .|| = |. f1 .| by NFCONT_4:9;
A5: |. f1 .| is_integrable_on ['a,b'] by A1,NFCONT_4:9;
|. f1 .| is_integrable_on ['min(c,d),max(c,d)'] &
(|. f1 .|) | ['min(c,d),max(c,d)'] is bounded &
|. integral(f1,c,d) .| <= integral((|. f1 .|),min(c,d),max(c,d))
by A1,A2,A3,A5,INTEGR19:22;
hence thesis by A4,REAL_NS1:1,A1,INTEGR19:48;
end;
theorem Th45:
for a,b,c,d,e be Real,
f be PartFunc of REAL,REAL-NS n
st (a<=b & c <= d & f is_integrable_on ['a,b']
& ||. f .|| is_integrable_on ['a,b'] & f| ['a,b'] is bounded &
['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] &
for x be Real st x in ['c,d'] holds ||. f/.x .|| <= e)
holds
||. integral(f,c,d) .|| <= e * (d-c) &
||. integral(f,d,c).|| <= e * (d-c)
proof
let a,b,c,d,e be Real,
f be PartFunc of REAL,REAL-NS n;
assume
A1: a<=b & c <= d & f is_integrable_on ['a,b']
& ||. f .|| is_integrable_on ['a,b']
& f| ['a,b'] is bounded
& ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b']
& for x be Real st x in ['c,d'] holds ||. f/.x .|| <= e;
A2: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3; then
A3: ex g be Real st c = g & a<=g & g <= b by A1;
A4: ex g be Real st d=g & a<=g & g <= b by A2,A1;
reconsider f1=f as PartFunc of REAL,REAL n by REAL_NS1:def 4;
A5: f1 | ['a,b'] is bounded by A1,INTEGR19:34;
A6: f1 is_integrable_on ['a,b'] by A5,A1,INTEGR19:43;
A7: |. f1 .| is_integrable_on ['a,b'] by A1,NFCONT_4:9;
now let x be Real;
assume A8: x in ['c,d']; then
A9: ||. f/.x .|| <= e by A1;
A10: ['c,d'] c= dom f by A1,INTEGR19:2,A3,A4; then
f/.x = f.x by A8,PARTFUN1:def 6
.= f1/.x by A8,A10,PARTFUN1:def 6;
hence |. f1/.x .| <= e by A9,REAL_NS1:1;
end; then
|. integral(f1,c,d) .| <= e * (d-c) & |. integral(f1,d,c).| <= e * (d-c)
by A1,A5,A6,A7,INTEGR19:24;
hence
||. integral(f,c,d) .|| <= e * (d-c) & ||. integral(f,d,c).|| <= e * (d-c)
by REAL_NS1:1,A1,INTEGR19:48;
end;
Lm8:
for g be Function of REAL,REAL
st for x be Real holds g.x=x-a holds
for x be Real holds g is_differentiable_in x & diff(g,x)=1
proof
let g be Function of REAL,REAL;
A1: dom(g)=[#]REAL by FUNCT_2:def 1;
assume
A2: for x be Real holds g.x=x-a;
A3: for d be Real st d in [#]REAL holds g.d = 1*d + (-1*a)
proof
let d be Real such that
d in [#]REAL;
thus g.d = d-a by A2
.= 1*d +(-1*a);
end; then
A4: g is_differentiable_on dom(g) by A1,FDIFF_1:23;
for x be Real holds g is_differentiable_in x & diff(g,x)=1
proof
let d be Real;
thus g is_differentiable_in d by A1,A4,XREAL_0:def 1;
d in REAL by XREAL_0:def 1;
hence diff(g,d) = (g`|dom(g)).d by A1,A4,FDIFF_1:def 7
.= 1 by A1,A3,FDIFF_1:23,XREAL_0:def 1;
end;
hence thesis;
end;
theorem Th46:
for n be Nat, g be Function of REAL,REAL
st for x be Real holds g.x= (x-a) |^ (n+1)
holds
for x be Real holds g is_differentiable_in x
& diff(g,x)= (n+1)* ((x-a) |^ n)
proof
let n be Nat;
let g be Function of REAL,REAL;
A1: dom(g)=REAL by FUNCT_2:def 1;
assume A2: for x be Real holds g.x= (x-a) |^ (n+1);
defpred X[set] means $1 in REAL;
deffunc U(Real) = In($1-a,REAL);
consider f being PartFunc of REAL,REAL such that
A3: for d be Element of REAL holds d in dom f iff X[d] and
A4: for d be Element of REAL st d in dom f holds f/.d = U(d)
from PARTFUN2:sch 2;
for x be object st x in REAL holds x in dom f by A3; then
REAL c=dom(f) by TARSKI:def 3; then
A5: dom(f)=REAL by XBOOLE_0:def 10;
A6: for d be Element of REAL holds f.d = d-a
proof
let d be Element of REAL;
f/.d = In(d-a,REAL) by A4,A5;
hence thesis by A5,PARTFUN1:def 6;
end;
A7: for d be Real holds f.d = d-a
proof
let d be Real;
d in REAL by XREAL_0:def 1;
hence thesis by A6;
end;
reconsider n1 = n + 1 as Element of NAT by ORDINAL1:def 12;
A8: f is Function of REAL,REAL by A5,FUNCT_2:67;
A9: dom( #Z (n1) ) = REAL & rng (f) c= REAL by FUNCT_2:def 1; then
A10: dom ( #Z (n1) *f ) = dom(f) by RELAT_1:27;
A11: now
let x be Element of REAL;
assume x in dom ( ( #Z (n1)) *f );
hence ( #Z (n1) *f ).x = ( #Z (n1) *f )/.x by PARTFUN1:def 6
.= #Z (n1) /.(f/.x) by A5,A10,PARTFUN2:3
.= ( #Z (n1) ).(f.x) by A5,PARTFUN1:def 6
.= (f.x) #Z (n1) by TAYLOR_1:def 1
.= (f.x) |^ (n+1) by PREPOWER:36
.= (x-a) |^ (n+1) by A6
.= g.x by A2;
end;
reconsider n1 = n+1, nn=n,n0=(n+1)-1 as Element of NAT by ORDINAL1:def 12;
A12: for x be Real holds ( #Z (n1)) *f is_differentiable_in x
& diff(( #Z (n1)) *f,x) = (n+1)* ((x-a) |^ n)
proof
let x be Real;
A13: f is_differentiable_in x
& #Z (n1) is_differentiable_in f.x by A8,Lm8,A7,TAYLOR_1:2;
hence ( #Z (n1)) *f is_differentiable_in x by FDIFF_2:13;
reconsider pp = (f.x) #Z (n0) as Real;
reconsider px = (x-a) #Z nn as Real;
diff(( #Z (n1) ),f.x) = (n1) * pp by TAYLOR_1:2;
hence diff(( #Z (n1)) *f,x)
= (n1) * pp * diff(f,x) by A13,FDIFF_2:13
.= (n1) * pp * 1 by A8,Lm8,A7
.= (n1) * px by A7
.= (n+1) * (x-a) |^ n by PREPOWER:36;
end;
( #Z (n1) *f) = g by A11,PARTFUN1:5,A1,A5,A9,RELAT_1:27;
hence thesis by A12;
end;
theorem Th47:
for n be Nat, g be Function of REAL,REAL
st for x be Real holds g.x = ((x-a) |^ (n+1)) / ((n+1)! ) holds
for x be Real holds g is_differentiable_in x
& diff(g,x) = ((x-a) |^ n) / (n!)
proof
let n be Nat;
let g be Function of REAL,REAL;
A1: dom(g)=REAL by FUNCT_2:def 1;
assume A2: for x be Real holds g.x = ((x-a) |^ (n+1)) / ((n+1)! );
defpred X[set] means $1 in REAL;
deffunc U(Real) = In(($1-a)|^ (n+1),REAL);
consider f being PartFunc of REAL,REAL such that
A3: for d be Element of REAL holds d in dom f iff X[d] and
A4: for d be Element of REAL st d in dom f holds f/.d = U(d)
from PARTFUN2:sch 2;
for x be object st x in REAL holds x in dom f by A3; then
REAL c=dom(f) by TARSKI:def 3; then
A5: dom(f)=REAL by XBOOLE_0:def 10;
A6: for d be Real holds f.d = (d-a) |^ (n+1)
proof
let d be Real;
A7: d in REAL by XREAL_0:def 1;
f/.d = In((d-a) |^ (n+1),REAL) by A4,A5,A7;
hence thesis by A5,PARTFUN1:def 6,A7;
end;
A8: f is Function of REAL,REAL by A5,FUNCT_2:67;
A9: dom ( ( 1 /( (n+1)!) ) (#) f ) = dom(f) by VALUED_1:def 5;
A10: now
let x be Element of REAL;
assume x in dom ((1/((n+1)!)) (#) f);
hence (( 1/((n+1)!)) (#) f ).x = (1/((n+1)!)) * f.x by VALUED_1:def 5
.= 1/((n+1)!)*( (x-a) |^ (n+1) ) by A6
.= ((x-a) |^ (n+1))/((n+1)!) * 1 by XCMPLX_1:75
.= g.x by A2;
end;
A11: for x be Real holds (1/((n+1)!)) (#) f is_differentiable_in x
& diff((1/((n+1)!)) (#) f,x) = ((x-a) |^ n)/(n!)
proof
let x be Real;
A12: (n+1) / ((n+1)!) = (1*(n+1))/ (n! * (n+1)) by NEWTON:15
.= 1/(n!) by XCMPLX_1:91;
A13: f is_differentiable_in x by A8,A6,Th46;
hence ( 1/((n+1)!) ) (#) f is_differentiable_in x by FDIFF_1:15;
thus diff((1/((n+1)!)) (#) f,x) = (1/((n+1)!)) *diff(f,x) by A13,FDIFF_1:15
.= diff(f,x)/((n+1)!)*1 by XCMPLX_1:75
.=1 *( (n+1)* ((x-a) |^ n) )/ ((n+1)!) by A8,A6,Th46
.=1*( (x-a) |^ n * ((n+1) / ((n+1)!)) ) by XCMPLX_1:74
.=(x-a) |^ n / (n!) by A12,XCMPLX_1:99;
end;
( (1/((n+1)!)) (#) f) =g by A10,PARTFUN1:5,A1,A5,A9;
hence thesis by A11;
end;
Lm9:
for n be Nat for a,r,L be Real,
g be Function of REAL,REAL
st for x be Real holds
g.x = ( (r*(x-a))|^(n+1) )/ ((n+1)!) * L
holds for x be Real holds g is_differentiable_in x
& diff(g,x) = r*( ( (r*(x-a))|^n )/ (n!) * L)
proof
let n be Nat,
a,r,L be Real,
g be Function of REAL,REAL;
assume A1: for x be Real holds g.x = ( (r*(x-a))|^(n+1) )/ ((n+1)!) * L;
A2: dom g = REAL by FUNCT_2:def 1;
deffunc F(Real) = In((($1-a) |^ (n+1)) / ((n+1) !),REAL);
consider f be Function of REAL,REAL such that
A3: for x be Element of REAL holds f.x = F(x) from FUNCT_2:sch 4;
A4: for x be Real holds f.x = ((x-a) |^ (n+1)) / ((n+1) !)
proof
let x be Real; x in REAL by XREAL_0:def 1; then
f.x = F(x) by A3;
hence thesis;
end;
A5: dom f = REAL by FUNCT_2:def 1;
A6: dom ( ( r |^ (n+1) * L ) (#) f ) = dom(f) by VALUED_1:def 5;
A7: now
let x be Element of REAL;
assume x in dom ( (r |^ (n+1) * L) (#) f );
hence ( (r |^ (n+1) * L) (#) f ).x = ((r |^ (n+1) * L))* f.x
by VALUED_1:def 5
.= ( r |^ (n+1) * L )*( ((x-a) |^ (n+1)) / ((n+1) !) ) by A4
.= ( (r |^ (n+1)) * (((x-a) |^ (n+1)) / ((n+1) !)) ) *L
.= ( ((r |^ (n+1)) * ((x-a) |^ (n+1))) / ((n+1) !) ) *L by XCMPLX_1:74
.= ( ( (r*(x-a))|^(n+1) )/ ((n+1)!) ) * L by NEWTON:7
.= g.x by A1;
end;
A8: for x be Real holds ( r |^ (n+1) * L ) (#) f is_differentiable_in x
& diff(( r |^ (n+1) * L ) (#) f,x) = r*( ( (r*(x-a))|^n)/ (n!) * L )
proof
let x be Real;
A9: f is_differentiable_in x & diff(f,x) = ((x-a) |^ n) / (n!) by Th47,A4;
hence ( r |^ (n+1) * L ) (#) f is_differentiable_in x by FDIFF_1:15;
thus diff(( r |^ (n+1) * L ) (#) f,x) = ( r |^ (n+1) * L ) * diff(f,x)
by A9,FDIFF_1:15
.= ( r |^ (n+1) ) * ( ( (x-a) |^ n) / (n!) ) * L by A9
.= ( ( r |^ (n+1) ) * ((x-a) |^ n) ) / (n!) * L by XCMPLX_1:74
.= ( ( r * r |^ n ) * ((x-a) |^ n) ) / (n!) * L by NEWTON:6
.= ( r * (( r |^ n ) * ((x-a) |^ n)) ) / (n!) * L
.= ( r * ( (r*(x-a))|^n ) ) / (n!) * L by NEWTON:7
.= r*( ( (r*(x-a))|^n )/ (n!) )* L by XCMPLX_1:74
.= r*( ( (r*(x-a))|^n )/ (n!) * L );
end;
(( r |^ (n+1) * L ) (#) f) = g by A7,PARTFUN1:5,A2,A5,A6;
hence thesis by A8;
end;
Lm10:
for m be non zero Element of NAT
for a,r,L be Real,
g be Function of REAL,REAL
st for x be Real holds
g.x = r*( ( (r*(x-a))|^m)/ (m!) * L )
holds for x be Real holds g is_differentiable_in x
proof
let m be non zero Element of NAT,
a,r,L be Real,
g be Function of REAL,REAL;
assume A1: for x be Real holds g.x = r*( ( (r*(x-a))|^m)/ (m!) * L );
A2: dom g = REAL by FUNCT_2:def 1;
1 <= m by NAT_1:14; then
reconsider n = m - 1 as Nat by INT_1:5,ORDINAL1:def 12;
reconsider n as Element of NAT by ORDINAL1:def 12;
deffunc F(Real) = In((($1-a) |^ (n+1)) / ((n+1) !),REAL);
consider f be Function of REAL,REAL such that
A3: for x be Element of REAL holds f.x = F(x) from FUNCT_2:sch 4;
A4: for x be Real holds f.x = ((x-a) |^ (n+1)) / ((n+1) !)
proof
let x be Real;
x in REAL by XREAL_0:def 1; then
f.x = F(x) by A3;
hence thesis;
end;
A5: dom f = REAL by FUNCT_2:def 1;
A6: dom ( ( r |^ (n+2) * L ) (#) f ) = dom(f) by VALUED_1:def 5;
A7: now
let x be Element of REAL;
assume x in dom ( ( r |^ (n+2) * L ) (#) f );
hence (( r |^ (n+2) * L ) (#) f ).x = (( r |^ (n+2) * L ))* f.x
by VALUED_1:def 5
.= ( r |^ (n+2) * L )*( ((x-a) |^ (n+1)) / ((n+1) !) ) by A4
.= ( r |^ ((n+1)+1) )*( ((x-a) |^ (n+1)) / ((n+1) !) ) *L
.= ( r * r |^ (n+1) )*( ((x-a) |^ (n+1)) / ((n+1) !) ) *L by NEWTON:6
.= r * ( (r |^ (n+1))* (((x-a) |^ (n+1)) / ((n+1) !)) ) *L
.= r * ( ((r |^ (n+1))* ((x-a) |^ (n+1)))/ ((n+1) !) ) *L by XCMPLX_1:74
.= r * ( ( (r*(x-a))|^(n+1) )/ ((n+1)!) ) * L by NEWTON:7
.= r * ( ( (r*(x-a))|^m)/ (m!) * L )
.= g.x by A1;
end;
A8: for x be Real holds ( r |^ (n+2) * L ) (#) f is_differentiable_in x
proof
let x be Real;
f is_differentiable_in x by Th47,A4;
hence ( r |^ (n+2) * L ) (#) f is_differentiable_in x by FDIFF_1:15;
end;
(( r |^ (n+2) * L ) (#) f) = g by A7,A2,A5,A6,PARTFUN1:5;
hence thesis by A8;
end;
Lm11:
for a,r,t,L be Real,
f0 be Function of REAL,REAL st a <= t &
for x be Real holds f0.x = r*( ( (r*(x-a))|^n )/ (n!) * L )
holds
f0| ['a,t'] is continuous &
f0| [' a,t '] is bounded &
f0 is_integrable_on [' a,t '] &
integral(f0,a,t) = ( (r*(t-a))|^(n+1) ) /((n+1)!) * L
proof
let a,r,t,L be Real, f0 be Function of REAL,REAL;
A1: a in REAL by XREAL_0:def 1;
assume A2: a <= t;
assume A3: for x be Real holds
f0.x = r*( ( (r*(x-a))|^n )/ (n!) * L );
A4: dom f0 = REAL by FUNCT_2:def 1;
A5: dom f0 = REAL by FUNCT_2:def 1;
for x be Real st x in dom f0
holds f0 is_continuous_in x by A3,Lm10,FDIFF_1:24; then
reconsider f0 as continuous PartFunc of REAL,REAL by FCONT_1:def 2;
deffunc F(Real) = In(( (r*($1-a))|^(n+1))/ ((n+1)!) * L,REAL);
consider g be Function of REAL,REAL such that
A6: for x be Element of REAL holds g.x = F(x) from FUNCT_2:sch 4;
A7: for x be Real holds g.x = ( (r*(x-a))|^(n+1))/ ((n+1)!) * L
proof
let x be Real;
x in REAL by XREAL_0:def 1; then
g.x = In(( (r*(x-a))|^(n+1))/ ((n+1)!) * L,REAL) by A6;
hence thesis;
end;
A8: dom g = [#]REAL by FUNCT_2:def 1;
for x be Real st x in [#]REAL holds g is_differentiable_in x
by A7,Lm9; then
A9: g is_differentiable_on REAL by A8;
A10: now let x be Element of REAL;
assume x in dom (g`| [#]REAL );
thus (g`| [#]REAL ).x = diff(g,x) by A9,FDIFF_1:def 7
.= r*( ( (r*(x-a))|^n )/ (n!) * L ) by Lm9,A7
.= f0.x by A3
.= (f0 | [#]REAL).x;
end;
dom (g`| [#]REAL ) = [#]REAL by A9,FDIFF_1:def 7
.= dom (f0 | [#]REAL) by A4; then
g`| [#]REAL = f0 | [#]REAL by A10,PARTFUN1:5; then
g in IntegralFuncs(f0,[#]REAL ) by A9,INTEGRA7:def 1; then
A11: g is_integral_of f0,[#]REAL by INTEGRA7:def 2;
A12: f0 | [' a,t '] is bounded by INTEGRA5:10,A5;
A13: g.t = integral(f0,a,t) + g.a by A2,INTEGRA7:18,A5,INTEGRA5:11,A12,A11;
A14: (0 qua Real) + 1 <= n +1 by XREAL_1:6;
g.a = In(( (r*(a-a))|^(n+1))/((n+1)!) * L,REAL) by A6,A1
.= ( 0 qua Real )/ ((n+1)!) * L by A14,NEWTON:11
.= (0 qua Real);
hence thesis by A12,A13,A5,INTEGRA5:11,A7;
end;
Lm12:
for a,t,L,r be Real, k be non zero Element of NAT st a <= t
ex rg be PartFunc of REAL,REAL
st dom rg = ['a,t'] &
(for x be Real st x in ['a,t']
holds rg.x =r*( ( (r*(x-a))|^k)/ (k!) * L) ) &
rg is continuous &
rg is_integrable_on ['a,t'] & rg| ['a,t'] is bounded &
integral(rg,a,t) = ( (r*(t-a))|^(k+1) ) /((k+1)!) * L
proof
let a,t,L,r be Real, k be non zero Element of NAT;
assume A1: a <= t;
deffunc F(Real) = In(r*( ( (r*($1-a))|^k )/ (k!) * L ),REAL);
consider f0 be Function of REAL,REAL such that
A2: for x be Element of REAL holds f0.x = F(x) from FUNCT_2:sch 4;
A3: for x be Real holds f0.x = r*( ( (r*(x-a))|^k )/ (k!) * L )
proof
let x be Real; x in REAL by XREAL_0:def 1; then
f0.x = In(r*( ( (r*(x-a))|^k )/ (k!) * L ),REAL) by A2;
hence thesis;
end;
A4: dom f0 = REAL by FUNCT_2:def 1;
A5: f0| ['a,t'] is continuous & f0| [' a,t '] is bounded
& f0 is_integrable_on [' a,t ']
& integral(f0,a,t) = ( (r*(t-a)) |^ ( k + 1) ) /((k+1)!) * L
by Lm11,A1,A3;
set f = f0| ['a,t'];
A6: dom (f0| ['a,t']) = ['a,t'] by A4,RELAT_1:62;
reconsider f as continuous PartFunc of REAL,REAL by Lm11,A1,A3;
A7: now let x be Real;
assume A8: x in ['a,t'];
A9: x in REAL by XREAL_0:def 1;
thus f.x = f0.x by A8,FUNCT_1:49
.= In(r*( ( (r*(x-a))|^k )/ (k!) * L ),REAL) by A2,A9
.= r*( ( (r*(x-a))|^k )/ (k!) * L );
end;
A10: integral(f0,a,t) = integral(f0,[' a,t ']) by INTEGRA5:def 4,A1
.= integral(f0 || [' a,t '] );
A11: integral(f,a,t) = integral(f,[' a,t ']) by INTEGRA5:def 4,A1
.= integral(f|| [' a,t '] );
take f;
thus thesis by A7,A11,A10,A5,A6;
end;
theorem Th48:
for f,g be PartFunc of REAL,REAL st a <= t &
['a,t'] c= dom f & f is_integrable_on ['a,t'] &
f| ['a,t'] is bounded &
['a,t'] c= dom g & g is_integrable_on ['a,t'] &
g| ['a,t'] is bounded &
for x be Real st x in ['a,t'] holds f.x <= g.x holds
integral(f,a,t) <= integral(g,a,t)
proof
let f,g be PartFunc of REAL,REAL;
assume A1: a <= t &
['a,t'] c= dom f & f is_integrable_on ['a,t'] &
f| ['a,t'] is bounded &
['a,t'] c= dom g & g is_integrable_on ['a,t'] &
g| ['a,t'] is bounded &
for x be Real st x in ['a,t'] holds f.x <= g.x;
set f0 = f| ['a,t'];
set g0 = g| ['a,t'];
A2: dom f0 = ['a,t'] by A1,RELAT_1:62;
rng f0 c= REAL; then
reconsider f0 as Function of ['a,t'],REAL by A2,FUNCT_2:2;
A3: dom g0 = ['a,t'] by A1,RELAT_1:62;
rng g0 c= REAL; then
reconsider g0 as Function of ['a,t'],REAL by A3,FUNCT_2:2;
A4: f0| ['a,t'] is bounded by A1;
A5: f0 is integrable by A1;
A6: g0| ['a,t'] is bounded by A1;
A7: g0 is integrable by A1;
now let x be Real;
assume A8: x in ['a,t'];
A9: f0.x = f.x by A8,FUNCT_1:49;
g0.x = g.x by A8,FUNCT_1:49;
hence f0.x <= g0.x by A9,A1,A8;
end; then
A10: integral(f,['a,t']) <= integral(g,['a,t']) by A4,A5,A6,A7,INTEGRA2:34;
integral(f,['a,t']) = integral(f,a,t) by A1,INTEGRA5:def 4;
hence integral(f,a,t) <= integral(g,a,t) by A10,A1,INTEGRA5:def 4;
end;
definition
let n be non zero Element of NAT;
let y0 be VECTOR of REAL-NS n,
G be Function of REAL-NS n,REAL-NS n,
a,b be Real;
assume A1: a<=b & G is_continuous_on dom G;
func Fredholm(G,a,b,y0) -> Function of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n),
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) means
:Def7:
for x be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n)
ex f,g,Gf be continuous PartFunc of REAL,REAL-NS n
st x=f & it.x = g & dom f =[' a,b '] & dom g =[' a,b '] & Gf = G*f
& for t be Real st t in [' a,b '] holds g.t = y0 + integral(Gf,a,t);
existence
proof
defpred P[set,set] means
ex f,g,Gf be continuous PartFunc of REAL,REAL-NS n
st $1=f & $2=g & dom f =[' a,b '] & dom g =[' a,b '] & Gf=G*f
& for t be Real st t in [' a,b '] holds g.t = y0+ integral(Gf,a,t);
set D = the carrier of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n);
A2: for x being Element of D ex y being Element of D st P[x,y]
proof
let x be Element of D;
consider f0 be continuous PartFunc of REAL,REAL-NS n such that
A3: x=f0 & dom f0 = [' a,b '] by Def2;
now let x0 be Real;
assume A4: x0 in dom(G*f0); then
x0 in dom f0 by FUNCT_1:11; then
A5: f0 is_continuous_in x0 by NFCONT_3:def 2;
the carrier of REAL-NS n = dom G by FUNCT_2:def 1; then
G | (dom G ) is_continuous_in f0/.x0 by A1,NFCONT_1:def 7;
hence G*f0 is_continuous_in x0 by A4,A5,NFCONT_3:15;
end; then
reconsider Gf = G*f0 as continuous PartFunc of REAL,REAL-NS n
by NFCONT_3:def 2;
dom G = the carrier of REAL-NS n by FUNCT_2:def 1; then
rng f0 c= dom G; then
A6: dom Gf = [' a,b '] by A3,RELAT_1:27;
A7: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
deffunc FX(Element of REAL) = integral(Gf,a,$1);
consider F0 be Function of REAL,REAL-NS n such that
A8: for x be Element of REAL holds F0.x = FX(x) from FUNCT_2:sch 4;
set F = F0| ['a,b'];
A9: dom F = dom F0 /\ ['a,b'] by RELAT_1:61
.= REAL /\ ['a,b'] by FUNCT_2:def 1
.= ['a,b'] by XBOOLE_1:28;
A10: now let t be Real;
assume A11: t in [.a,b.];
A12: t in REAL by XREAL_0:def 1;
thus F.t = F0.t by A11,A9,A7,FUNCT_1:47
.= integral(Gf,a,t) by A8,A12;
end;
A13: for t be Real st t in [.a,b.]
holds F is_continuous_in t by Th34,A6,A1,A9,A10;
set G0 = REAL --> y0;
set G1 = G0| ['a,b'];
A14: dom G1 = dom G0 /\ ['a,b'] by RELAT_1:61
.= REAL /\ ['a,b']
.= ['a,b'] by XBOOLE_1:28;
A15: now let t be Real;
assume A16: t in [.a,b.];
thus G1.t = G0.t by A16,A14,A7,FUNCT_1:47
.= y0 by XREAL_0:def 1,FUNCOP_1:7;
end;
A17: F is continuous by A7,A9,A13,NFCONT_3:def 2;
set g=G1+F;
A18: dom g = dom F /\ dom G1 by VFUNCT_1:def 1
.= ['a,b'] by A9,A14;
reconsider g as continuous PartFunc of REAL,REAL-NS n by A17;
reconsider y=g as Element of D by A18,Def2;
take y;
now let t be Real;
assume A19:t in ['a,b'];
A20: G1/.t = G1.t by A19,A14,PARTFUN1:def 6
.= y0 by A19,A7,A15;
A21: F/.t = F.t by A19,A9,PARTFUN1:def 6
.= integral(Gf,a,t) by A19,A7,A10;
thus g.t = g/.t by A18,A19,PARTFUN1:def 6
.= y0 + integral(Gf,a,t) by A20,A21,A18,A19,VFUNCT_1:def 1;
end;
hence thesis by A18,A3;
end;
consider F being Function of D,D such that
A22: for x being Element of D holds P[x,F.x] from FUNCT_2:sch 3 (A2);
take F;
thus thesis by A22;
end;
uniqueness
proof
let F1,F2 be Function of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n),
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n);
assume
A23: for x be VECTOR of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) holds
ex f,g,Gf be continuous PartFunc of REAL,REAL-NS n
st x=f & F1.x = g & dom f =[' a,b '] & dom g =[' a,b '] & Gf = G*f
& for t be Real st t in [' a,b ']
holds g.t = y0+ integral(Gf,a,t);
assume
A24: for x be VECTOR of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) holds
ex f,g,Gf be continuous PartFunc of REAL,REAL-NS n
st x=f & F2.x = g & dom f =[' a,b '] & dom g =[' a,b '] & Gf = G*f
& for t be Real st t in [' a,b ']
holds g.t = y0+ integral(Gf,a,t);
now let x be Element of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n);
consider f1,g1,Gf1 be continuous PartFunc of REAL,REAL-NS n such that
A25: x=f1 & F1.x = g1 & dom f1 =[' a,b '] & dom g1 =[' a,b '] & Gf1 = G*f1
& for t be Real st t in [' a,b ']
holds g1.t = y0+ integral(Gf1,a,t) by A23;
consider f2,g2,Gf2 be continuous PartFunc of REAL,REAL-NS n such that
A26: x=f2 & F2.x = g2 & dom f2 =[' a,b '] & dom g2 =[' a,b '] & Gf2 = G*f2
& for t be Real st t in [' a,b ']
holds g2.t = y0+ integral(Gf2,a,t) by A24;
now let t be object;
assume A27: t in dom g1; then
reconsider t0=t as Real;
thus g1.t = y0+ integral(Gf2,a,t0) by A26,A27,A25
.= g2.t by A27,A26,A25;
end;
hence F1.x = F2.x by A25,A26,FUNCT_1:2;
end;
hence F1=F2 by FUNCT_2:def 8;
end;
end;
theorem Th49:
a <= b & 0 < r &
(for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||)
implies
for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n),
g,h be continuous PartFunc of REAL,REAL-NS n
st g= Fredholm(G,a,b,y0).u & h= Fredholm(G,a,b,y0).v holds
for t be Real st t in [' a,b '] holds
||. g/.t - h/.t .|| <= r*(t-a) * ||.u-v.||
proof
assume A1: a<=b & 0 < r &
for y1, y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||;
A2: dom G = the carrier of REAL-NS n by FUNCT_2:def 1;
for x1,x2 be Point of REAL-NS n
st x1 in (the carrier of REAL-NS n)
& x2 in (the carrier of REAL-NS n) holds
||.G/.x1-G/.x2.||<=r*||.x1-x2.|| by A1; then
G is_Lipschitzian_on the carrier of (REAL-NS n) by A1,A2,NFCONT_1:def 9; then
A3: G is_continuous_on dom G by A2,NFCONT_1:45;
let u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n),
g,h be continuous PartFunc of REAL,REAL-NS n;
assume A4: g= Fredholm(G,a,b,y0).u & h= Fredholm(G,a,b,y0).v;
set F= Fredholm(G,a,b,y0);
consider f1,g1,Gf1 be continuous PartFunc of REAL,REAL-NS n such that
A5: u=f1 & F.u = g1 & dom f1 =[' a,b '] & dom g1 =[' a,b '] & Gf1 = G*f1
& for t be Real st t in [' a,b ']
holds g1.t = y0+ integral(Gf1,a,t) by Def7,A1,A3;
consider f2,g2,Gf2 be continuous PartFunc of REAL,REAL-NS n such that
A6: v=f2 & F.v = g2 & dom f2 =[' a,b '] & dom g2 =[' a,b '] & Gf2 = G*f2
& for t be Real
st t in [' a,b ']
holds g2.t = y0+ integral(Gf2,a,t) by Def7,A1,A3;
set Gf12= Gf1 - Gf2;
A7: dom G = the carrier of REAL-NS n by FUNCT_2:def 1; then
rng f1 c= dom G; then
A8: dom Gf1 =[' a,b '] by A5,RELAT_1:27;
rng f2 c= dom G by A7; then
A9: dom Gf2 =[' a,b '] by A6,RELAT_1:27;
reconsider Gf12 as continuous PartFunc of REAL,REAL-NS n;
A10: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
let t be Real;
assume A11: t in [' a,b ']; then
A12: ex g be Real st t=g & a<=g & g <= b by A10;
A13: dom Gf12 = dom Gf1 /\ dom Gf2 by VFUNCT_1:def 2
.= ['a,b'] by A8,A9;
A14: Gf12 is_integrable_on ['a,b'] by A13,Th33;
A15: Gf12| ['a,b'] is bounded by A13,Th32;
Gf12| (['a,b']) is continuous; then
A16: (||. Gf12 .||) | [' a,b '] is continuous by A13,NFCONT_3:22;
[' a,b '] = dom (||. Gf12 .||) by A13,NORMSP_0:def 2; then
A17: (||. Gf12 .||) is_integrable_on [' a,b '] by A16,INTEGRA5:11;
A18: a in ['a,b'] by A10,A1;
for x be Real st x in ['a,t'] holds ||. Gf12/.x .|| <= r*||.u-v.||
proof
let x be Real;
assume A19: x in ['a,t'];
A20: ['a,t'] c= [' a,b '] by A12,INTEGR19:1;
A21: Gf12/.x =Gf1/.x -Gf2/.x by A13,A20,A19,VFUNCT_1:def 2;
A22: Gf1/.x = (Gf1).x by A8,A20,A19,PARTFUN1:def 6
.= G.(f1.x) by A20,A19,A8,A5,FUNCT_1:12
.= G/.(f1/.x) by A20,A19,A5,PARTFUN1:def 6;
A23: Gf2/.x = (Gf2).x by A9,A20,A19,PARTFUN1:def 6
.= G.(f2.x) by A20,A19,A9,A6,FUNCT_1:12
.= G/.(f2/.x) by A20,A19,A6,PARTFUN1:def 6;
A24: ||. Gf1/.x -Gf2/.x .||<=r*||.(f1/.x)-(f2/.x).|| by A22,A23,A1;
||.(f1/.x)-(f2/.x).|| <=||.u-v.|| by A20,A19,A5,A6,Th26; then
r*||.(f1/.x)-(f2/.x).|| <=r*||.u-v.|| by A1,XREAL_1:64;
hence thesis by A21,A24,XXREAL_0:2;
end; then
A25: ||. integral(Gf12,a,t) .||<= ((r*||.u-v.|| ))* (t-a)
by Th45,A1,A17,A14,A15,A13,A18,A11,A12;
A26: Gf1 is_integrable_on ['a,b'] by A8,Th33;
A27: Gf1| ['a,b'] is bounded by A8,Th32;
A28: Gf2 is_integrable_on ['a,b'] by A9,Th33;
A29: Gf2| ['a,b'] is bounded by A9,Th32;
A30: integral(Gf12,a,t) = integral(Gf1,a,t) - integral(Gf2,a,t)
by A8,A9,A26,A27,A28,A29,A18,A11,A1,INTEGR19:50;
A31: g/.t = g1.t by A4,A11,A5,PARTFUN1:def 6
.= y0 + integral(Gf1,a,t) by A5,A11;
A32: h/.t = g2.t by A4,A11,A6,PARTFUN1:def 6
.= y0 + integral(Gf2,a,t) by A6,A11;
g/.t - h/.t = (y0+ integral(Gf1,a,t) - y0 ) -integral(Gf2,a,t)
by A31,A32,RLVECT_1:27
.= ( integral(Gf1,a,t) + (y0 - y0) ) -integral(Gf2,a,t)
by RLVECT_1:28
.= ( integral(Gf1,a,t) + 0.(REAL-NS n) ) -integral(Gf2,a,t)
by RLVECT_1:15
.= integral(Gf12,a,t) by A30;
hence thesis by A25;
end;
theorem Th50:
a <= b & 0 < r &
(for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||)
implies
for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n),
m be Element of NAT,
g,h be continuous PartFunc of REAL,REAL-NS n
st g = iter(Fredholm(G,a,b,y0),(m+1)).u
& h = iter(Fredholm(G,a,b,y0),(m+1)).v holds
for t be Real st t in [' a,b ']
holds ||. g/.t - h/.t .|| <= ((r*(t-a))|^(m+1) )/((m+1)!) * ||.u-v.||
proof
assume A1: a<=b & 0 < r &
for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||;
set F = Fredholm(G,a,b,y0);
A2: dom G = the carrier of REAL-NS n by FUNCT_2:def 1;
for x1,x2 be Point of REAL-NS n
st x1 in (the carrier of REAL-NS n)
& x2 in (the carrier of REAL-NS n) holds
||.G/.x1-G/.x2.||<=r*||.x1-x2.|| by A1; then
G is_Lipschitzian_on the carrier of (REAL-NS n) by A1,A2,NFCONT_1:def 9; then
A3: G is_continuous_on dom G by A2,NFCONT_1:45;
let u1,v1 be VECTOR of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n);
defpred P[Nat] means
for g,h be continuous PartFunc of REAL,REAL-NS n
st g = iter(F,($1+1)).u1
& h = iter(F,($1+1)).v1 holds
for t be Real st t in [' a,b ']
holds ||. g/.t - h/.t .||
<= ( (r*(t-a))|^($1+1) )/(($1+1)!) * ||.u1-v1.||;
reconsider Z0 = 0 as Element of NAT;
A4: P[0]
proof
let g,h be continuous PartFunc of REAL,REAL-NS n;
assume A5: g = iter(F,( (0 qua Element of NAT ) + 1)).u1
& h = iter(F,( (0 qua Element of NAT ) + 1)).v1;
A6: g= F.u1 by A5,FUNCT_7:70;
A7: h= F.v1 by A5,FUNCT_7:70;
for t be Real st t in [' a,b '] holds
||. g/.t - h/.t .|| <= ((r*(t-a))|^(Z0 + 1) )
/((Z0 + 1)!) * ||.u1-v1.|| by NEWTON:13,Th49,A1,A6,A7;
hence thesis;
end;
A8:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A9: P[k];
let g,h be continuous PartFunc of REAL,REAL-NS n;
assume A10:
g = iter(F,((k+1)+1)).u1 & h = iter(F,((k+1)+1)).v1;
reconsider u=iter(F,(k+1)).u1 as
VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n);
reconsider v=iter(F,(k+1)).v1 as
VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n);
A11: dom(iter(F,k+1)) = the carrier of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) by FUNCT_2:def 1;
A12: iter(F,((k+1)+1)).u1 = (F*iter(F,k+1)).u1 by FUNCT_7:71
.= F.u by A11,FUNCT_1:13;
A13: iter(F,((k+1)+1)).v1 = (F*iter(F,k+1)).v1 by FUNCT_7:71
.= F.v by A11,FUNCT_1:13;
consider f1,g1,Gf1 be continuous PartFunc of REAL,REAL-NS n such that
A14: u=f1 & F.u = g1 & dom f1 =[' a,b '] & dom g1 =[' a,b '] & Gf1 = G*f1
& for t be Real st t in [' a,b ']
holds g1.t = y0+ integral(Gf1,a,t) by Def7,A1,A3;
consider f2,g2,Gf2 be continuous PartFunc of REAL,REAL-NS n such that
A15: v=f2 & F.v = g2 & dom f2 =[' a,b '] & dom g2 =[' a,b '] & Gf2 = G*f2
& for t be Real st t in [' a,b ']
holds g2.t = y0+ integral(Gf2,a,t) by Def7,A1,A3;
set Gf12= Gf1 - Gf2;
A16: for t be Real st t in [' a,b ']
holds ||. f1/.t - f2/.t .||
<= ( (r*(t-a))|^(k+1) )/((k+1)!) * ||.u1-v1.|| by A9,A14,A15;
A17: dom G = the carrier of REAL-NS n by FUNCT_2:def 1; then
rng f1 c= dom G; then
A18: dom Gf1 =[' a,b '] by A14,RELAT_1:27;
rng f2 c= dom G by A17; then
A19: dom Gf2 =[' a,b '] by A15,RELAT_1:27;
reconsider Gf12 as continuous PartFunc of REAL,REAL-NS n;
A20: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
let t be Real;
assume A21: t in [' a,b ']; then
A22: ex g be Real st t=g & a<=g & g <= b by A20;
A23: ex g be Element of REAL st t=g & a<=g & g <= b
proof
consider g be Real such that A24: t=g & a<=g & g <= b by A21,A20;
reconsider g as Element of REAL by XREAL_0:def 1;
take g;
thus thesis by A24;
end;
A25: dom Gf12 = dom Gf1 /\ dom Gf2 by VFUNCT_1:def 2
.= ['a,b'] by A18,A19; then
A26: dom (||. Gf12 .||) = ['a,b'] by NORMSP_0:def 2;
A27: Gf12 is_integrable_on ['a,b'] by A25,Th33;
A28: Gf12| ['a,b'] is bounded by A25,Th32;
A29: a in ['a,b'] by A20,A1;
Gf12 | ['a,b'] is continuous; then
A30: (||. Gf12 .||) | [' a,b '] is continuous by A25,NFCONT_3:22;
[' a,b '] = dom (||. Gf12 .||) by A25,NORMSP_0:def 2; then
A31: ||. Gf12 .|| is_integrable_on [' a,b '] by A30,INTEGRA5:11;
min(a,t) = a & max(a,t) = t by A22,XXREAL_0:def 9,def 10; then
A32: ||. Gf12 .|| is_integrable_on ['a,t'] &
(||. Gf12 .||) | ['a,t'] is bounded &
||. integral(Gf12,a,t) .||
<= integral((||. Gf12 .||),a,t) by A1,A27,A28,A25,A29,A21,A31,Th44;
A33: k+1 is non zero Element of NAT by ORDINAL1:def 12;
consider rg be PartFunc of REAL,REAL such that
A34: dom rg = ['a,t'] &
(for x be Real st x in ['a,t']
holds rg.x = r*(( (r*(x-a))|^(k+1) )/((k+1)!) * ||.u1-v1.|| ))
& rg is continuous
& rg is_integrable_on ['a,t'] & rg| ['a,t'] is bounded
& integral(rg,a,t) = ( (r*(t-a))|^((k+1)+1) )
/ (((k+1)+1)!) * ||.u1-v1.|| by Lm12,A23,A33;
A35: ['a,t'] c= [' a,b '] by A22,INTEGR19:1;
for x be Real st x in ['a,t'] holds ||. Gf12 .||.x <= rg.x
proof
let x be Real;
assume A36: x in ['a,t'];
A37: Gf12/.x =Gf1/.x -Gf2/.x by A25,A35,A36,VFUNCT_1:def 2;
A38: Gf1/.x = (Gf1).x by A18,A35,A36,PARTFUN1:def 6
.= G.(f1.x) by A35,A36,A18,A14,FUNCT_1:12
.= G/.(f1/.x) by A35,A36,A14,PARTFUN1:def 6;
A39: Gf2/.x = (Gf2).x by A19,A35,A36,PARTFUN1:def 6
.= G.(f2.x) by A35,A36,A19,A15,FUNCT_1:12
.= G/.(f2/.x) by A35,A36,A15,PARTFUN1:def 6;
A40: ||. Gf1/.x -Gf2/.x .|| <= r*||.(f1/.x)-(f2/.x).|| by A38,A39,A1;
r*||.(f1/.x)-(f2/.x).||
<=r*(( (r*(x-a))|^(k+1) )/((k+1)!) * ||.u1-v1.||)
by A1,XREAL_1:64,A16,A35,A36; then
r*||.(f1/.x)-(f2/.x).|| <=rg.x by A36,A34; then
||. Gf1/.x -Gf2/.x .|| <=rg.x by A40,XXREAL_0:2;
hence thesis by A26,A35,A36,NORMSP_0:def 2,A37;
end; then
A41: integral((||. Gf12 .||),a,t) <= integral(rg,a,t)
by A32,A22,A26,A35,A34,Th48;
A42: Gf1 is_integrable_on ['a,b'] by A18,Th33;
A43: Gf1| ['a,b'] is bounded by A18,Th32;
A44: Gf2 is_integrable_on ['a,b'] by A19,Th33;
A45: Gf2| ['a,b'] is bounded by A19,Th32;
A46: integral(Gf12,a,t) = integral(Gf1,a,t) - integral(Gf2,a,t)
by A18,A19,A42,A43,A44,A45,A29,A21,A1,INTEGR19:50;
A47: g/.t = g1.t by A12,A10,A21,A14,PARTFUN1:def 6
.= y0+ integral(Gf1,a,t) by A14,A21;
A48: h/.t = g2.t by A13,A10,A21,A15,PARTFUN1:def 6
.= y0+ integral(Gf2,a,t) by A15,A21;
g/.t - h/.t = (y0+ integral(Gf1,a,t) - y0 ) -integral(Gf2,a,t)
by RLVECT_1:27,A47,A48
.= ( integral(Gf1,a,t) + (y0 - y0) ) -integral(Gf2,a,t)
by RLVECT_1:28
.= ( integral(Gf1,a,t) + 0.(REAL-NS n) ) -integral(Gf2,a,t)
by RLVECT_1:15
.= integral(Gf12,a,t) by A46;
hence thesis by A41,A32,XXREAL_0:2,A34;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A8);
hence thesis;
end;
Lm13:
for r,L,a,b,t be Real,m be Nat
st a<=t & t <= b & 0 <= L & 0<=r holds
((r*(t-a))|^(m+1) )/((m+1)!) * L
<= ((r*(b-a))|^(m+1) )/((m+1)!) * L
proof
let r,L,a,b,t be Real, m be Nat;
assume A1: a<=t & t <= b & 0 <= L & 0<=r; then
(t-a) <= (b-a) by XREAL_1:13; then
A2: (r*(t-a)) <= (r*(b-a)) by A1,XREAL_1:64;
0 <= t - a by A1,XREAL_1:48; then
A3: (r*(t-a)) to_power (m+1) <= (r*(b-a)) to_power (m+1) by A1,HOLDER_1:3,A2;
((r*(t-a))|^(m+1))/((m+1)!) <= ((r*(b-a))|^(m+1))/((m+1)!) by A3,XREAL_1:72;
hence thesis by A1,XREAL_1:64;
end;
Lm14:
a < b & 0 < r implies
ex m be Element of NAT st ((r*(b-a))|^(m+1) )/((m+1)!) < 1
& 0 < ((r*(b-a))|^(m+1) )/((m+1)!)
proof
assume A1: a < b & 0 < r;
set z=r*(b-a);
set s = z rExpSeq;
s is summable by SIN_COS:45; then
A2: s is convergent & lim s = 0 by SERIES_1:4;
consider n be Nat such that
A3: for m be Nat st n<=m holds |.s.m- 0 .| < 1 by A2,SEQ_2:def 7;
reconsider m0 = max(n,1) as Element of NAT by ORDINAL1:def 12;
reconsider m = m0 - 1 as Element of NAT by INT_1:5,XXREAL_0:25;
take m;
|.s.(m+1) - 0 .| < 1 by A3,XXREAL_0:25; then
A4: |.( ((r*(b-a))|^(m+1) )/((m+1)!) ).| < 1 by SIN_COS:def 5;
0 < b - a by A1,XREAL_1:50; then
(0 qua Real) *r < r*(b-a) by A1,XREAL_1:68; then
0 < (r*(b-a)) to_power (m+1) by POWER:34;
hence thesis by A4,ABSVALUE:def 1,XREAL_1:139;
end;
theorem Th51:
for m be Nat st a <= b & 0 < r &
(for y1,y2 be VECTOR of REAL-NS n holds ||.G/.y1-G/.y2.|| <= r*||.y1-y2.||)
holds
for u,v be VECTOR of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n)
holds ||. iter(Fredholm(G,a,b,y0),(m+1)).u
- iter(Fredholm(G,a,b,y0),(m+1)).v .||
<= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.||
proof
let m be Nat;
assume A1: a<=b & 0 < r & for y1,y2 be VECTOR of REAL-NS n
holds ||.G/.y1-G/.y2.||<=r*||.y1-y2.||;
let u,v be VECTOR of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n);
reconsider u1=iter(Fredholm(G,a,b,y0),(m+1)).u as VECTOR of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n);
reconsider v1=iter(Fredholm(G,a,b,y0),(m+1)).v as VECTOR of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n);
consider g be continuous PartFunc of REAL,REAL-NS n such that
A2: u1=g & dom g = [' a,b '] by Def2;
consider h be continuous PartFunc of REAL,REAL-NS n such that
A3: v1=h & dom h = [' a,b '] by Def2;
now let t be Real;
A4: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
assume A5: t in [' a,b ']; then
A6: ex g be Real st t=g & a<=g & g <= b by A4;
m in NAT by ORDINAL1:def 12; then
A7: ||. g/.t - h/.t .||
<= ((r*(t-a))|^(m+1) )/((m+1)!) * ||.u-v.|| by A5,Th50,A1,A2,A3;
((r*(t-a))|^(m+1) )/((m+1)!) * ||.u-v.||
<= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.|| by A6,A1,Lm13;
hence ||. g/.t - h/.t .|| <= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.||
by A7,XXREAL_0:2;
end;
hence thesis by Th27,A2,A3;
end;
theorem Th52:
a<b & G is_Lipschitzian_on the carrier of REAL-NS n implies
ex m be Nat st iter(Fredholm(G,a,b,y0),(m+1)) is contraction
proof
assume A1: a<b & G is_Lipschitzian_on the carrier of REAL-NS n; then
consider r be Real such that
A2: 0<r & for x1,x2 be Point of REAL-NS n
st x1 in (the carrier of REAL-NS n)
& x2 in (the carrier of REAL-NS n) holds
||.G/.x1-G/.x2.||<=r*||.x1-x2.|| by NFCONT_1:def 9;
A3: for x1,x2 be Point of REAL-NS n holds
||.G/.x1-G/.x2.||<=r*||.x1-x2.|| by A2;
consider m be Element of NAT such that
A4: ((r*(b-a))|^(m+1) )/((m+1)!) < 1 &
0 < ((r*(b-a))|^(m+1) )/((m+1)!) by Lm14,A1,A2;
take m;
for u,v be VECTOR of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n)
holds ||. iter(Fredholm(G,a,b,y0),(m+1)).u
- iter(Fredholm(G,a,b,y0),(m+1)).v .||
<= ((r*(b-a))|^(m+1) )/((m+1)!) * ||.u-v.|| by Th51,A3,A2,A1;
hence thesis by A4;
end;
theorem Th53:
a<b & G is_Lipschitzian_on the carrier of REAL-NS n implies
Fredholm(G,a,b,y0) is with_unique_fixpoint
proof
assume a<b & G is_Lipschitzian_on the carrier of REAL-NS n; then
ex m be Nat st iter(Fredholm(G,a,b,y0),(m+1)) is contraction by Th52;
hence thesis by Th7;
end;
theorem Th54:
for f,g be continuous PartFunc of REAL,REAL-NS n
st dom f =[' a,b '] & dom g =[' a,b '] & Z = ]. a,b .[
& a<b
& G is_Lipschitzian_on the carrier of REAL-NS n
& g=Fredholm(G,a,b,y0).f holds g/.a=y0
& g is_differentiable_on Z
& for t be Real st t in Z holds diff(g,t) = (G*f)/.t
proof
let f,g be continuous PartFunc of REAL,REAL-NS n;
assume A1: dom f =[' a,b '] & dom g =[' a,b '] & Z = ]. a,b .[
& a<b
& G is_Lipschitzian_on the carrier of REAL-NS n
& g=Fredholm(G,a,b,y0).f;
set D = R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n);
dom G = the carrier of REAL-NS n by FUNCT_2:def 1; then
A2: G is_continuous_on dom G by A1,NFCONT_1:45;
f is Element of D by Def2,A1; then
consider f0,g0,Gf0 be continuous PartFunc of REAL,REAL-NS n such that
A3: f=f0 & Fredholm(G,a,b,y0).f = g0
& dom f0 = [' a,b '] & dom g0 =[' a,b '] & Gf0 = G*f0
& for t be Real st t in [' a,b ']
holds g0.t = y0+ integral(Gf0,a,t) by A1,A2,Def7;
reconsider Gf=G*f as continuous PartFunc of REAL,REAL-NS n by A3;
dom G = the carrier of REAL-NS n by FUNCT_2:def 1; then
rng f c= dom G; then
dom Gf =[' a,b '] by A1,RELAT_1:27;
hence thesis by A1,Th36,A3;
end;
theorem Th55:
for y be continuous PartFunc of REAL,REAL-NS n st a<b
& Z = ]. a,b .[
& G is_Lipschitzian_on the carrier of REAL-NS n
& dom y = [' a,b ']
& y is_differentiable_on Z
& y/.a = y0
& (for t be Real st t in Z holds diff(y,t) = G.(y/.t))
holds y is_a_fixpoint_of (Fredholm(G,a,b,y0))
proof
let y be continuous PartFunc of REAL,REAL-NS n;
assume A1: a<b & Z = ]. a,b .[
& G is_Lipschitzian_on the carrier of REAL-NS n
& dom y = [' a,b ']
& y is_differentiable_on Z
& y/.a = y0
& (for t be Real st t in Z holds diff(y,t) = G.(y/.t));
A2: dom (Fredholm(G,a,b,y0))
= the carrier of R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n)
by FUNCT_2:def 1;
A3: y is Element of the carrier of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) by Def2,A1;
A4: y in dom (Fredholm(G,a,b,y0)) by A2,Def2,A1;
dom G = the carrier of REAL-NS n by FUNCT_2:def 1; then
G is_continuous_on dom G by A1,NFCONT_1:45; then
consider f,g,Gf be continuous PartFunc of REAL,REAL-NS n such that
A5: y=f & (Fredholm(G,a,b,y0)).y = g
& dom f =[' a,b '] & dom g =[' a,b '] & Gf = G*f
& for t be Real st t in [' a,b ']
holds g.t = y0+ integral(Gf,a,t) by Def7,A1,A3;
dom G = the carrier of REAL-NS n by FUNCT_2:def 1; then
rng f c= dom G; then
A6: dom (G*f) = [' a,b '] by A5,RELAT_1:27;
for t be Real st t in Z holds diff(y,t) = (Gf)/.t
proof
let t be Real;
assume A7:t in Z;
A8: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
A9: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
thus diff(y,t) = G.(y/.t) by A1,A7
.= G.(y.t) by A8,A1,A7,A9,PARTFUN1:def 6
.= (Gf).t by A5,A8,A1,A7,A9,FUNCT_1:13
.= (Gf)/.t by A5,A8,A1,A7,A9,A6,PARTFUN1:def 6;
end;
hence thesis by A4,A5,Th43,A1,A6;
end;
theorem
for y1,y2 be continuous PartFunc of REAL,REAL-NS n
st a<b & Z = ]. a,b .[ & G is_Lipschitzian_on the carrier of REAL-NS n
& dom y1 = [' a,b ']
& y1 is_differentiable_on Z
& y1/.a = y0
& (for t be Real st t in Z holds diff(y1,t) = G.(y1/.t))
& dom y2 = [' a,b ']
& y2 is_differentiable_on Z
& y2/.a = y0
& (for t be Real st t in Z holds diff(y2,t) = G.(y2/.t))
holds y1=y2
proof
let y1,y2 be continuous PartFunc of REAL,REAL-NS n;
assume A1:
a<b & Z = ]. a,b .[ & G is_Lipschitzian_on the carrier of REAL-NS n
& dom y1 = [' a,b ']
& y1 is_differentiable_on Z
& y1/.a = y0
& (for t be Real st t in Z holds diff(y1,t) = G.(y1/.t))
& dom y2 = [' a,b ']
& y2 is_differentiable_on Z
& y2/.a = y0
& (for t be Real st t in Z holds diff(y2,t) = G.(y2/.t)); then
Fredholm(G,a,b,y0) is with_unique_fixpoint by Th53; then
consider y being set such that
A2: y is_a_fixpoint_of (Fredholm(G,a,b,y0)) & for z being set
st z is_a_fixpoint_of (Fredholm(G,a,b,y0)) holds y = z;
A3: y1 is_a_fixpoint_of (Fredholm(G,a,b,y0)) by Th55,A1;
A4: y2 is_a_fixpoint_of (Fredholm(G,a,b,y0)) by Th55,A1;
y1 = y by A3,A2 .= y2 by A4,A2;
hence thesis;
end;
theorem
a<b & Z = ]. a,b .[ & G is_Lipschitzian_on the carrier of REAL-NS n implies
ex y be continuous PartFunc of REAL,REAL-NS n st
dom y = [' a,b ']
& y is_differentiable_on Z
& y/.a = y0
& for t be Real st t in Z holds diff(y,t) = G.(y/.t)
proof
assume A1: a<b & Z = ]. a,b .[
& G is_Lipschitzian_on the carrier of REAL-NS n; then
Fredholm(G,a,b,y0) is with_unique_fixpoint by Th53; then
consider x be set such that
A2: x is_a_fixpoint_of (Fredholm(G,a,b,y0)) & for y being set st
y is_a_fixpoint_of (Fredholm(G,a,b,y0)) holds x = y;
A3: x in dom (Fredholm(G,a,b,y0)) & x = (Fredholm(G,a,b,y0)).x
by A2;
reconsider x as Element of the carrier of
R_NormSpace_of_ContinuousFunctions([' a,b '],REAL-NS n) by A3;
consider f be continuous PartFunc of REAL,REAL-NS n such that
A4: x=f & dom f = [' a,b '] by Def2;
take f;
thus dom f = [' a,b '] & f is_differentiable_on Z & f/.a = y0
by Th54,A4,A1,A3;
A5: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
A6: ['a,b'] = [.a,b.] by A1,INTEGRA5:def 3;
let t be Real;
assume A7:t in Z;
dom G = the carrier of REAL-NS n by FUNCT_2:def 1; then
rng f c= dom G; then
A8: dom (G*f) = [' a,b '] by A4,RELAT_1:27;
thus diff(f,t) = (G*f)/.t by A7,Th54,A4,A1,A3
.= (G*f).t by A8,A5,A1,A7,A6,PARTFUN1:def 6
.= G.(f.t) by A8,A5,A1,A7,A6,FUNCT_1:12
.= G.(f/.t) by A5,A1,A7,A6,A4,PARTFUN1:def 6;
end;