let n be non zero Element of NAT ; for a, b, r being Real
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n) st a <= b & 0 < r & ( for y1, y2 being VECTOR of (REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n)))
for m being Element of NAT
for g, h being 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 being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
let a, b, r be Real; for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n) st a <= b & 0 < r & ( for y1, y2 being VECTOR of (REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n)))
for m being Element of NAT
for g, h being 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 being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
let y0 be VECTOR of (REAL-NS n); for G being Function of (REAL-NS n),(REAL-NS n) st a <= b & 0 < r & ( for y1, y2 being VECTOR of (REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n)))
for m being Element of NAT
for g, h being 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 being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
let G be Function of (REAL-NS n),(REAL-NS n); ( a <= b & 0 < r & ( for y1, y2 being VECTOR of (REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) implies for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n)))
for m being Element of NAT
for g, h being 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 being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).|| )
assume A1:
( a <= b & 0 < r & ( for y1, y2 being VECTOR of (REAL-NS n) holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) )
; for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n)))
for m being Element of NAT
for g, h being 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 being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u - v).||
set F = Fredholm (G,a,b,y0);
A2:
dom G = the carrier of (REAL-NS n)
by FUNCT_2:def 1;
for x1, x2 being 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))); for m being Element of NAT
for g, h being continuous PartFunc of REAL,(REAL-NS n) st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v1 holds
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u1 - v1).||
defpred S1[ Nat] means for g, h being continuous PartFunc of REAL,(REAL-NS n) st g = (iter ((Fredholm (G,a,b,y0)),($1 + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),($1 + 1))) . v1 holds
for t being 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:
S1[ 0 ]
proof
let g,
h be
continuous PartFunc of
REAL,
(REAL-NS n);
( g = (iter ((Fredholm (G,a,b,y0)),(0 + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),(0 + 1))) . v1 implies for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (0 + 1)) / ((0 + 1) !)) * ||.(u1 - v1).|| )
assume A5:
(
g = (iter ((Fredholm (G,a,b,y0)),(0 + 1))) . u1 &
h = (iter ((Fredholm (G,a,b,y0)),(0 + 1))) . v1 )
;
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (0 + 1)) / ((0 + 1) !)) * ||.(u1 - v1).||
A6:
g = (Fredholm (G,a,b,y0)) . u1
by A5, FUNCT_7:70;
A7:
h = (Fredholm (G,a,b,y0)) . v1
by A5, FUNCT_7:70;
for
t being
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
for
t being
Real st
t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (0 + 1)) / ((0 + 1) !)) * ||.(u1 - v1).||
;
verum
end;
A8:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A9:
S1[
k]
;
S1[k + 1]
let g,
h be
continuous PartFunc of
REAL,
(REAL-NS n);
( g = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . v1 implies for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).|| )
assume A10:
(
g = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . u1 &
h = (iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . v1 )
;
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).||
reconsider u =
(iter ((Fredholm (G,a,b,y0)),(k + 1))) . u1 as
VECTOR of
(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ;
reconsider v =
(iter ((Fredholm (G,a,b,y0)),(k + 1))) . v1 as
VECTOR of
(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ;
A11:
dom (iter ((Fredholm (G,a,b,y0)),(k + 1))) = the
carrier of
(R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n)))
by FUNCT_2:def 1;
A12:
(iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . u1 =
((Fredholm (G,a,b,y0)) * (iter ((Fredholm (G,a,b,y0)),(k + 1)))) . u1
by FUNCT_7:71
.=
(Fredholm (G,a,b,y0)) . u
by A11, FUNCT_1:13
;
A13:
(iter ((Fredholm (G,a,b,y0)),((k + 1) + 1))) . v1 =
((Fredholm (G,a,b,y0)) * (iter ((Fredholm (G,a,b,y0)),(k + 1)))) . v1
by FUNCT_7:71
.=
(Fredholm (G,a,b,y0)) . v
by A11, FUNCT_1:13
;
consider f1,
g1,
Gf1 being
continuous PartFunc of
REAL,
(REAL-NS n) such that A14:
(
u = f1 &
(Fredholm (G,a,b,y0)) . u = g1 &
dom f1 = ['a,b'] &
dom g1 = ['a,b'] &
Gf1 = G * f1 & ( for
t being
Real st
t in ['a,b'] holds
g1 . t = y0 + (integral (Gf1,a,t)) ) )
by Def7, A1, A3;
consider f2,
g2,
Gf2 being
continuous PartFunc of
REAL,
(REAL-NS n) such that A15:
(
v = f2 &
(Fredholm (G,a,b,y0)) . v = g2 &
dom f2 = ['a,b'] &
dom g2 = ['a,b'] &
Gf2 = G * f2 & ( for
t being
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 being
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 =
Gf1 - Gf2 as
continuous PartFunc of
REAL,
(REAL-NS n) ;
A20:
['a,b'] = [.a,b.]
by A1, INTEGRA5:def 3;
let t be
Real;
( t in ['a,b'] implies ||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).|| )
assume A21:
t in ['a,b']
;
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).||
then A22:
ex
g being
Real st
(
t = g &
a <= g &
g <= b )
by A20;
A23:
ex
g being
Element of
REAL st
(
t = g &
a <= g &
g <= b )
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, XXREAL_0: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 being
PartFunc of
REAL,
REAL such that A34:
(
dom rg = ['a,t'] & ( for
x being
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 being
Real st
x in ['a,t'] holds
||.Gf12.|| . x <= rg . x
proof
let x be
Real;
( x in ['a,t'] implies ||.Gf12.|| . x <= rg . x )
assume A36:
x in ['a,t']
;
||.Gf12.|| . x <= rg . x
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
||.Gf12.|| . x <= rg . x
by A26, A35, A36, NORMSP_0:def 2, A37;
verum
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
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ ((k + 1) + 1)) / (((k + 1) + 1) !)) * ||.(u1 - v1).||
by A41, A32, XXREAL_0:2, A34;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A4, A8);
hence
for m being Element of NAT
for g, h being continuous PartFunc of REAL,(REAL-NS n) st g = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . u1 & h = (iter ((Fredholm (G,a,b,y0)),(m + 1))) . v1 holds
for t being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (((r * (t - a)) |^ (m + 1)) / ((m + 1) !)) * ||.(u1 - v1).||
; verum