ORDEQ_01: Contracting Mapping on Normed Linear Space

:: Contracting Mapping on Normed Linear Space
:: by Keiichi Miyajima , Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received August 19, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users

definition

let f be Function;

attr f is with_unique_fixpoint means :: ORDEQ_01:def 1
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;

:: deftheorem defines with_unique_fixpoint ORDEQ_01:def 1 :

theorem :: ORDEQ_01:1

for x being set holds x is_a_fixpoint_of {[x,x]}

proof end;

theorem Th2: :: ORDEQ_01:2

for x, y, z being set st x is_a_fixpoint_of {[y,z]} holds
x = y

proof end;

registration

let x be set ;

cluster {[x,x]} -> with_unique_fixpoint ;

coherence

proof end;

end;

theorem Th3: :: ORDEQ_01:3

for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X

proof end;

theorem :: ORDEQ_01:4

for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y

proof end;

theorem :: ORDEQ_01:5

for K, L, e being Real st 0 < K & K < 1 & 0 < e holds
ex n being Nat st |.(L * (K to_power n)).| < e

proof end;

registration

let X be RealNormSpace;

cluster Function-like V22() quasi_total -> contraction for Element of K16(K17( the carrier of X, the carrier of X));

coherence

proof end;

end;

registration

let X be RealBanachSpace;

cluster Function-like quasi_total contraction -> with_unique_fixpoint for Element of K16(K17( the carrier of X, the carrier of X));

coherence

proof end;

end;

theorem :: ORDEQ_01:6

canceled;

::$CT

theorem Th7: :: ORDEQ_01:7

for X being RealBanachSpace
for f being Function of X,X st ex n0 being Nat st iter (f,n0) is contraction holds
f is with_unique_fixpoint

proof end;

theorem :: ORDEQ_01:8

for X being RealBanachSpace
for 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 end;

theorem Th9: :: ORDEQ_01:9

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being continuous PartFunc of REAL,Y st dom f = X holds
f is bounded Function of X,Y

proof 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: :: ORDEQ_01:def 2
for x being set holds
( x in it iff ex f being continuous PartFunc of REAL,Y st
( x = f & dom f = X ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ContinuousFunctions ORDEQ_01:def 2 :

registration

let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;

cluster ContinuousFunctions (X,Y) -> non empty ;

coherence

proof end;

end;

registration

let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;

cluster ContinuousFunctions (X,Y) -> linearly-closed ;

coherence

proof 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 :: ORDEQ_01:def 3
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;

:: deftheorem defines R_VectorSpace_of_ContinuousFunctions ORDEQ_01:def 3 :

registration

let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;

cluster R_VectorSpace_of_ContinuousFunctions (X,Y) -> strict ;

coherence ;

end;

theorem Th10: :: ORDEQ_01:10

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g, h being VECTOR of (R_VectorSpace_of_ContinuousFunctions (X,Y))
for f9, g9, h9 being 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 being Element of X holds h9 /. x = (f9 /. x) + (g9 /. x) )

proof end;

theorem Th11: :: ORDEQ_01:11

for a being Real
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, h being VECTOR of (R_VectorSpace_of_ContinuousFunctions (X,Y))
for f9, h9 being continuous PartFunc of REAL,Y st f9 = f & h9 = h & dom f9 = X & dom h9 = X holds
( h = a * f iff for x being Element of X holds h9 /. x = a * (f9 /. x) )

proof end;

theorem Th12: :: ORDEQ_01:12

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds 0. (R_VectorSpace_of_ContinuousFunctions (X,Y)) = X --> (0. Y)

proof 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 :: ORDEQ_01:def 4
(BoundedFunctionsNorm (X,Y)) | (ContinuousFunctions (X,Y));

correctness by FUNCT_2:32;

end;

:: deftheorem defines ContinuousFunctionsNorm ORDEQ_01:def 4 :

definition

let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;
let f be set ;
assume A1: f in ContinuousFunctions (X,Y) ;

func modetrans (f,X,Y) -> continuous PartFunc of REAL,Y means :Def5: :: ORDEQ_01:def 5
( it = f & dom it = X );

correctness by A1, Def2;

end;

:: deftheorem Def5 defines modetrans ORDEQ_01:def 5 :

definition

let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;

func R_NormSpace_of_ContinuousFunctions (X,Y) -> non empty strict NORMSTR equals :: ORDEQ_01:def 6
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;

:: deftheorem defines R_NormSpace_of_ContinuousFunctions ORDEQ_01:def 6 :

theorem :: ORDEQ_01:13

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being continuous PartFunc of REAL,Y st dom f = X holds
modetrans (f,X,Y) = f

proof end;

theorem Th14: :: ORDEQ_01:14

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds X --> (0. Y) = 0. (R_NormSpace_of_ContinuousFunctions (X,Y))

proof end;

theorem Th15: :: ORDEQ_01:15

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f9, g9, h9 being 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 being Element of X holds h9 /. x = (f9 /. x) + (g9 /. x) )

proof end;

theorem :: ORDEQ_01:16

for a being Real
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, h being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f9, h9 being continuous PartFunc of REAL,Y st f9 = f & h9 = h & dom f9 = X & dom h9 = X holds
( h = a * f iff for x being Element of X holds h9 /. x = a * (f9 /. x) )

proof end;

theorem Th17: :: ORDEQ_01:17

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f = g holds
||.f.|| = ||.g.|| by FUNCT_1:49;

theorem Th18: :: ORDEQ_01:18

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f1, g1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f & g1 = g holds
f + g = f1 + g1

proof end;

theorem Th19: :: ORDEQ_01:19

for a being Real
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f1 being Point of (R_NormSpace_of_BoundedFunctions (X,Y)) st f1 = f holds
a * f = a * f1

proof end;

Lm2: for a being Real
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g being Point of (R_NormSpace_of_ContinuousFunctions (X,Y)) holds
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) ) & ( f = 0. (R_NormSpace_of_ContinuousFunctions (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

proof end;

Lm3: for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds
( R_NormSpace_of_ContinuousFunctions (X,Y) is reflexive & R_NormSpace_of_ContinuousFunctions (X,Y) is discerning & R_NormSpace_of_ContinuousFunctions (X,Y) is RealNormSpace-like )

proof end;

Lm4: for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds R_NormSpace_of_ContinuousFunctions (X,Y) is RealNormSpace

proof end;

registration

let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;

cluster R_NormSpace_of_ContinuousFunctions (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like ;

coherence by Lm4;

end;

theorem Th20: :: ORDEQ_01:20

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for f, g, h being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for f9, g9, h9 being 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 being Element of X holds h9 /. x = (f9 /. x) - (g9 /. x) )

proof end;

theorem Th21: :: ORDEQ_01:21

proof end;

Lm5: for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for C being Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) st C = ContinuousFunctions (X,Y) holds
C is closed

proof end;

registration

let X be non empty closed_interval Subset of REAL;
let Y be RealNormSpace;

cluster closed for Element of K16( the carrier of (R_NormSpace_of_BoundedFunctions (X,Y)));

existence

proof end;

end;

theorem Th22: :: ORDEQ_01:22

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds ContinuousFunctions (X,Y) is closed Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) by Lm5;

theorem Th23: :: ORDEQ_01:23

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for seq being sequence of (R_NormSpace_of_ContinuousFunctions (X,Y)) st Y is complete & seq is Cauchy_sequence_by_Norm holds
seq is convergent

proof end;

Lm6: for X being non empty closed_interval Subset of REAL
for Y being RealBanachSpace holds R_NormSpace_of_ContinuousFunctions (X,Y) is RealBanachSpace

proof end;

registration

let X be non empty closed_interval Subset of REAL;
let Y be RealBanachSpace;

cluster R_NormSpace_of_ContinuousFunctions (X,Y) -> non empty strict complete ;

coherence by Lm6;

end;

theorem Th24: :: ORDEQ_01:24

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for v being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g being PartFunc of REAL,Y st g = v holds
for t being Real st t in X holds
||.(g /. t).|| <= ||.v.||

proof end;

theorem Th25: :: ORDEQ_01:25

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for K being Real
for v being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g being PartFunc of REAL,Y st g = v & ( for t being Real st t in X holds
||.(g /. t).|| <= K ) holds
||.v.|| <= K

proof end;

theorem Th26: :: ORDEQ_01:26

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for v1, v2 being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g1, g2 being PartFunc of REAL,Y st g1 = v1 & g2 = v2 holds
for t being Real st t in X holds
||.((g1 /. t) - (g2 /. t)).|| <= ||.(v1 - v2).||

proof end;

theorem Th27: :: ORDEQ_01:27

for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace
for K being Real
for v1, v2 being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g1, g2 being PartFunc of REAL,Y st g1 = v1 & g2 = v2 & ( for t being Real st t in X holds
||.((g1 /. t) - (g2 /. t)).|| <= K ) holds
||.(v1 - v2).|| <= K

proof end;

theorem Th28: :: ORDEQ_01:28

for n, i being Nat
for f being PartFunc of REAL,(REAL n)
for A being Subset of REAL holds (proj (i,n)) * (f | A) = ((proj (i,n)) * f) | A

proof end;

theorem Th29: :: ORDEQ_01:29

for n being non zero Element of NAT
for a, b being Real
for g being continuous PartFunc of REAL,(REAL n) st dom g = ['a,b'] holds
g | ['a,b'] is bounded

proof end;

theorem Th30: :: ORDEQ_01:30

for n being non zero Element of NAT
for a, b being Real
for g being continuous PartFunc of REAL,(REAL n) st dom g = ['a,b'] holds
g is_integrable_on ['a,b']

proof end;

theorem Th31: :: ORDEQ_01:31

for n being non zero Element of NAT
for a, b being Real
for f, F being PartFunc of REAL,(REAL n) st a <= b & dom f = ['a,b'] & dom F = ['a,b'] & f is continuous & ( for t being Real st t in [.a,b.] holds
F . t = integral (f,a,t) ) holds
for x being Real st x in [.a,b.] holds
F is_continuous_in x

proof end;

theorem Th32: :: ORDEQ_01:32

for n being non zero Element of NAT
for a, b being Real
for f being continuous PartFunc of REAL,(REAL-NS n) st dom f = ['a,b'] holds
f | ['a,b'] is bounded

proof end;

theorem Th33: :: ORDEQ_01:33

for n being non zero Element of NAT
for a, b being Real
for f being continuous PartFunc of REAL,(REAL-NS n) st dom f = ['a,b'] holds
f is_integrable_on ['a,b']

proof end;

theorem Th34: :: ORDEQ_01:34

for n being non zero Element of NAT
for a, b being Real
for f being continuous PartFunc of REAL,(REAL-NS n)
for F being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom F = ['a,b'] & ( for t being Real st t in [.a,b.] holds
F . t = integral (f,a,t) ) holds
for x being Real st x in [.a,b.] holds
F is_continuous_in x

proof end;

theorem Th35: :: ORDEQ_01:35

for R being PartFunc of REAL,REAL st R is total holds
( R is RestFunc-like iff for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Real st z <> 0 & |.z.| < d holds
(|.z.| ") * |.(R /. z).| < r ) ) )

proof end;

theorem Th36: :: ORDEQ_01:36

for n being non zero Element of NAT
for a, b being Real
for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for f being continuous PartFunc of REAL,(REAL-NS n)
for g being PartFunc of REAL,(REAL-NS n) st a <= b & dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & ( for t being 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 being Real st t in Z holds
diff (g,t) = f /. t ) )

proof end;

theorem :: ORDEQ_01:37

for n being non zero Element of NAT
for i being Nat
for y1, y2 being Point of (REAL-NS n) holds (proj (i,n)) . (y1 + y2) = ((proj (i,n)) . y1) + ((proj (i,n)) . y2)

proof end;

theorem Th38: :: ORDEQ_01:38

for n being non zero Element of NAT
for i being Nat
for y1 being Point of (REAL-NS n)
for r being Real holds (proj (i,n)) . (r * y1) = r * ((proj (i,n)) . y1)

proof end;

theorem Th39: :: ORDEQ_01:39

for n being non zero Element of NAT
for g being PartFunc of REAL,(REAL-NS n)
for x0 being Real
for i being 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 end;

Lm7: for n being non zero Element of NAT
for i being Nat holds (proj (i,n)) . (0. (REAL-NS n)) = 0

proof end;

theorem Th40: :: ORDEQ_01:40

for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL-NS n)
for X being set st ( for i being Nat st 1 <= i & i <= n holds
((proj (i,n)) * f) | X is V22() ) holds
f | X is V22()

proof end;

theorem Th41: :: ORDEQ_01:41

for n being non zero Element of NAT
for a, b being Real
for f being PartFunc of REAL,(REAL-NS n) st ].a,b.[ c= dom f & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (f,x) = 0. (REAL-NS n) ) holds
f | ].a,b.[ is V22()

proof end;

theorem Th42: :: ORDEQ_01:42

for n being non zero Element of NAT
for a, b being Real
for f being continuous PartFunc of REAL,(REAL-NS n) st a < b & [.a,b.] = dom f & f | ].a,b.[ is V22() holds
for x being Real st x in [.a,b.] holds
f . x = f . a

proof end;

theorem Th43: :: ORDEQ_01:43

for n being non zero Element of NAT
for a, b being Real
for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for y, Gf being continuous PartFunc of REAL,(REAL-NS n)
for g being 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 being Real st t in Z holds
diff (y,t) = Gf /. t ) & ( for t being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) holds
y = g

proof end;

theorem Th44: :: ORDEQ_01:44

for n being non zero Element of NAT
for a, b, c, d being Real
for f being 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 end;

theorem Th45: :: ORDEQ_01:45

for n being non zero Element of NAT
for a, b, c, d, e being Real
for f being 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 being 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 end;

Lm8: for a being Real
for g being Function of REAL,REAL st ( for x being Real holds g . x = x - a ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = 1 )

proof end;

theorem Th46: :: ORDEQ_01:46

for a being Real
for n being Nat
for g being Function of REAL,REAL st ( for x being Real holds g . x = (x - a) |^ (n + 1) ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = (n + 1) * ((x - a) |^ n) )

proof end;

theorem Th47: :: ORDEQ_01:47

for a being Real
for n being Nat
for g being Function of REAL,REAL st ( for x being Real holds g . x = ((x - a) |^ (n + 1)) / ((n + 1) !) ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = ((x - a) |^ n) / (n !) )

proof end;

Lm9: for n being Nat
for a, r, L being Real
for g being Function of REAL,REAL st ( for x being Real holds g . x = (((r * (x - a)) |^ (n + 1)) / ((n + 1) !)) * L ) holds
for x being Real holds
( g is_differentiable_in x & diff (g,x) = r * ((((r * (x - a)) |^ n) / (n !)) * L) )

proof end;

Lm10: for m being non zero Element of NAT
for a, r, L being Real
for g being Function of REAL,REAL st ( for x being Real holds g . x = r * ((((r * (x - a)) |^ m) / (m !)) * L) ) holds
for x being Real holds g is_differentiable_in x

proof end;

Lm11: for n being non zero Element of NAT
for a, r, t, L being Real
for f0 being Function of REAL,REAL st a <= t & ( for x being 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 end;

Lm12: for a, t, L, r being Real
for k being non zero Element of NAT st a <= t holds
ex rg being PartFunc of REAL,REAL st
( dom rg = ['a,t'] & ( for x being 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 end;

theorem Th48: :: ORDEQ_01:48

for a, t being Real
for f, g being 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 being Real st x in ['a,t'] holds
f . x <= g . x ) holds
integral (f,a,t) <= integral (g,a,t)

proof end;

definition

let n be non zero Element of NAT ;
let y0 be VECTOR of (REAL-NS n);
let G be Function of (REAL-NS n),(REAL-NS n);
let 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: :: ORDEQ_01:def 7
for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],(REAL-NS n))) ex f, g, Gf being 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 being Real st t in ['a,b'] holds
g . t = y0 + (integral (Gf,a,t)) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Fredholm ORDEQ_01:def 7 :

theorem Th49: :: ORDEQ_01:49

for n being 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 g, h being 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 being Real st t in ['a,b'] holds
||.((g /. t) - (h /. t)).|| <= (r * (t - a)) * ||.(u - v).||

proof end;

theorem Th50: :: ORDEQ_01:50

for n being 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).||

proof end;

Lm13: for r, L, a, b, t being Real
for m being 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 end;

Lm14: for a, b, r being Real st a < b & 0 < r holds
ex m being Element of NAT st
( ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) < 1 & 0 < ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) )

proof end;

theorem Th51: :: ORDEQ_01:51

for n being 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)
for m being Nat 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))) 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 end;

theorem Th52: :: ORDEQ_01:52

for n being non zero Element of NAT
for a, b being Real
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n) st a < b & G is_Lipschitzian_on the carrier of (REAL-NS n) holds
ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction

proof end;

theorem Th53: :: ORDEQ_01:53

proof end;

theorem Th54: :: ORDEQ_01:54

for n being non zero Element of NAT
for a, b being Real
for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for f, g being 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 being Real st t in Z holds
diff (g,t) = (G * f) /. t ) )

proof end;

theorem Th55: :: ORDEQ_01:55

for n being non zero Element of NAT
for a, b being Real
for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for y being 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 being Real st t in Z holds
diff (y,t) = G . (y /. t) ) holds
y is_a_fixpoint_of Fredholm (G,a,b,y0)

proof end;

theorem :: ORDEQ_01:56

for n being non zero Element of NAT
for a, b being Real
for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n)
for y1, y2 being 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 being 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 being Real st t in Z holds
diff (y2,t) = G . (y2 /. t) ) holds
y1 = y2

proof end;

theorem :: ORDEQ_01:57

for n being non zero Element of NAT
for a, b being Real
for Z being open Subset of REAL
for y0 being VECTOR of (REAL-NS n)
for G being Function of (REAL-NS n),(REAL-NS n) st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of (REAL-NS n) holds
ex y being continuous PartFunc of REAL,(REAL-NS n) st
( dom y = ['a,b'] & y is_differentiable_on Z & y /. a = y0 & ( for t being Real st t in Z holds
diff (y,t) = G . (y /. t) ) )

proof end;