ORDEQ_02: Differential Equations on Functions from $\mathbbR$ into Real {B}anach Space

:: Differential Equations on Functions from $\mathbbR$ into Real {B}anach Space
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received December 31, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

Lm1: the carrier of (REAL-NS 1) = REAL 1
by REAL_NS1:def 4;

Lm2: ( dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) )

proof end;

theorem NDIFF435: :: ORDEQ_02:1

for Y being RealNormSpace
for J being Function of (REAL-NS 1),REAL
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,Y
for f being PartFunc of (REAL-NS 1),Y st J = proj (1,1) & x0 in dom f & y0 in dom g & x0 = <*y0*> & f = g * J holds
( f is_continuous_in x0 iff g is_continuous_in y0 )

proof end;

theorem :: ORDEQ_02:2

for Y being RealNormSpace
for I being Function of REAL,(REAL-NS 1)
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,Y
for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_continuous_in x0 iff g is_continuous_in y0 )

proof end;

theorem FTh40: :: ORDEQ_02:3

for Y being RealNormSpace
for I being Function of REAL,(REAL-NS 1) st I = (proj (1,1)) " holds
( ( for R being RestFunc of (REAL-NS 1),Y holds R * I is RestFunc of Y ) & ( for L being LinearOperator of (REAL-NS 1),Y holds L * I is LinearFunc of Y ) )

proof end;

theorem FTh41: :: ORDEQ_02:4

for Y being RealNormSpace
for J being Function of (REAL-NS 1),REAL st J = proj (1,1) holds
( ( for R being RestFunc of Y holds R * J is RestFunc of (REAL-NS 1),Y ) & ( for L being LinearFunc of Y holds L * J is Lipschitzian LinearOperator of (REAL-NS 1),Y ) )

proof end;

theorem FTh42: :: ORDEQ_02:5

for Y being RealNormSpace
for I being Function of REAL,(REAL-NS 1)
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,Y
for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
( g is_differentiable_in y0 & diff (g,y0) = (diff (f,x0)) . <*1*> & ( for r being Element of REAL holds (diff (f,x0)) . <*r*> = r * (diff (g,y0)) ) )

proof end;

theorem FTh43: :: ORDEQ_02:6

for Y being RealNormSpace
for I being Function of REAL,(REAL-NS 1)
for x0 being Point of (REAL-NS 1)
for y0 being Real
for g being PartFunc of REAL,Y
for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g holds
( f is_differentiable_in x0 iff g is_differentiable_in y0 )

proof end;

theorem FTh44: :: ORDEQ_02:7

proof end;

LM519A: for x being Point of (REAL-NS 1) ex z being Real st x = <*z*>

proof end;

theorem FTh42A: :: ORDEQ_02:8

for Y being RealNormSpace
for I being Function of REAL,(REAL-NS 1)
for x0 being Point of (REAL-NS 1)
for y0 being Element of REAL
for g being PartFunc of REAL,Y
for f being PartFunc of (REAL-NS 1),Y st I = (proj (1,1)) " & x0 in dom f & y0 in dom g & x0 = <*y0*> & f * I = g & f is_differentiable_in x0 holds
||.(diff (g,y0)).|| = ||.(diff (f,x0)).||

proof end;

theorem LM519B1: :: ORDEQ_02:9

for a, b, z being Real
for p, q, x being Point of (REAL-NS 1) st p = <*a*> & q = <*b*> & x = <*z*> holds
( ( z in ].a,b.[ implies x in ].p,q.[ ) & ( x in ].p,q.[ implies ( a <> b & ( a < b implies z in ].a,b.[ ) & ( a > b implies z in ].b,a.[ ) ) ) )

proof end;

theorem LM519C1: :: ORDEQ_02:10

for a, b, z being Real
for p, q, x being Point of (REAL-NS 1) st p = <*a*> & q = <*b*> & x = <*z*> holds
( ( z in [.a,b.] implies x in [.p,q.] ) & ( x in [.p,q.] implies ( ( a <= b implies z in [.a,b.] ) & ( a >= b implies z in [.b,a.] ) ) ) )

proof end;

theorem LM519D: :: ORDEQ_02:11

for a, b being Real
for p, q being Point of (REAL-NS 1)
for I being Function of REAL,(REAL-NS 1) st p = <*a*> & q = <*b*> & I = (proj (1,1)) " holds
( ( a <= b implies I .: [.a,b.] = [.p,q.] ) & ( a < b implies I .: ].a,b.[ = ].p,q.[ ) )

proof end;

theorem Th519: :: ORDEQ_02:12

for Y being RealNormSpace
for g being PartFunc of REAL, the carrier of Y
for a, b, M being Real st a <= b & [.a,b.] c= dom g & ( for x being Real st x in [.a,b.] holds
g is_continuous_in x ) & ( for x being Real st x in ].a,b.[ holds
g is_differentiable_in x ) & ( for x being Real st x in ].a,b.[ holds
||.(diff (g,x)).|| <= M ) holds
||.((g /. b) - (g /. a)).|| <= M * |.(b - a).|

proof end;

Lm13a: for Y being RealBanachSpace
for a, b, c, d, e being Real
for f being continuous PartFunc of REAL, the carrier of Y st [.a,b.] c= dom f & c in [.a,b.] & d in [.a,b.] & ( for x being Real st x in [.(min (c,d)),(max (c,d)).] holds
||.(f /. x).|| <= e ) holds
||.(integral (f,c,d)).|| <= e * |.(d - c).|

proof end;

Lm14a: for Y being RealBanachSpace
for a, b, c, d, e being Real
for f being continuous PartFunc of REAL, the carrier of Y st c <= d & [.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)

proof end;

Lm17: for a being Real
for X being RealNormSpace
for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / |.a.|

proof end;

theorem Th1955: :: ORDEQ_02:13

for a, b, x0 being Real
for X being RealBanachSpace
for F being PartFunc of REAL, the carrier of X
for f being continuous PartFunc of REAL, the carrier of X st [.a,b.] c= dom f & ].a,b.[ c= dom F & ( for x being Real st x in ].a,b.[ holds
F /. x = integral (f,a,x) ) & x0 in ].a,b.[ & f is_continuous_in x0 holds
( F is_differentiable_in x0 & diff (F,x0) = f /. x0 )

proof end;

theorem Th35: :: ORDEQ_02:14

for X being RealBanachSpace
for a, b being Real
for F being PartFunc of REAL, the carrier of X
for f being continuous PartFunc of REAL, the carrier of X st 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 Lm00: :: ORDEQ_02:15

for X being RealBanachSpace
for a being Real
for f being continuous PartFunc of REAL, the carrier of X st a in dom f holds
integral (f,a,a) = 0. X

proof end;

theorem Th40a: :: ORDEQ_02:16

for X being RealBanachSpace
for a, b being Real
for y0 being VECTOR of X
for f being continuous PartFunc of REAL, the carrier of X
for g being PartFunc of REAL, the carrier of X st a <= b & dom f = [.a,b.] & ( for t being Real st t in [.a,b.] holds
g /. t = y0 + (integral (f,a,t)) ) holds
g /. a = y0

proof end;

theorem Th40: :: ORDEQ_02:17

for X being RealBanachSpace
for Z being open Subset of REAL
for a, b being Real
for y0 being VECTOR of X
for f being continuous PartFunc of REAL, the carrier of X
for g being PartFunc of REAL, the carrier of X st 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 is_differentiable_on Z & ( for t being Real st t in Z holds
diff (g,t) = f /. t ) )

proof end;

theorem Th45a: :: ORDEQ_02:18

for X being RealBanachSpace
for a, b being Real
for f being PartFunc of REAL, the carrier of X st a <= b & [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds
f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (f,x) = 0. X ) holds
f /. b = f /. a

proof end;

theorem Th45: :: ORDEQ_02:19

for X being RealBanachSpace
for a, b being Real
for f being PartFunc of REAL, the carrier of X st [.a,b.] c= dom f & ( for x being Real st x in [.a,b.] holds
f is_continuous_in x ) & f is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (f,x) = 0. X ) holds
f | ].a,b.[ is constant

proof end;

theorem Th46: :: ORDEQ_02:20

for X being RealBanachSpace
for a, b being Real
for f being continuous PartFunc of REAL, the carrier of X st [.a,b.] = dom f & f | ].a,b.[ is constant holds
for x being Real st x in [.a,b.] holds
f /. x = f /. a

proof end;

theorem Th47: :: ORDEQ_02:21

for X being RealBanachSpace
for Z being open Subset of REAL
for a, b being Real
for y0 being VECTOR of X
for y, Gf being continuous PartFunc of REAL, the carrier of X
for g being PartFunc of REAL, the carrier of X 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;

Lm4: 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;

Lm5: 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;

Lm6: 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;

Lm7: 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;

definition

let X be RealBanachSpace;
let y0 be VECTOR of X;
let G be Function of X,X;
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'],X)),(R_NormSpace_of_ContinuousFunctions (['a,b'],X)) means :Def8: :: ORDEQ_02:def 1
for x being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) ex f, g, Gf being continuous PartFunc of REAL, the carrier of X 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 Def8 defines Fredholm ORDEQ_02:def 1 :

theorem Th53: :: ORDEQ_02:22

for X being RealBanachSpace
for a, b, r being Real
for y0 being VECTOR of X
for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))
for g, h being continuous PartFunc of REAL, the carrier of X 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 Th54: :: ORDEQ_02:23

for X being RealBanachSpace
for a, b, r being Real
for y0 being VECTOR of X
for G being Function of X,X st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X))
for m being Element of NAT
for g, h being continuous PartFunc of REAL, the carrier of X 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;

Lm8: 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;

Lm9: 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 Th55: :: ORDEQ_02:24

for X being RealBanachSpace
for a, b, r being Real
for y0 being VECTOR of X
for G being Function of X,X
for m being Nat st a <= b & 0 < r & ( for y1, y2 being VECTOR of X holds ||.((G /. y1) - (G /. y2)).|| <= r * ||.(y1 - y2).|| ) holds
for u, v being VECTOR of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)) 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 Th56: :: ORDEQ_02:25

for X being RealBanachSpace
for a, b being Real
for y0 being VECTOR of X
for G being Function of X,X st a < b & G is_Lipschitzian_on the carrier of X holds
ex m being Nat st iter ((Fredholm (G,a,b,y0)),(m + 1)) is contraction

proof end;

theorem Th57: :: ORDEQ_02:26

for X being RealBanachSpace
for a, b being Real
for y0 being VECTOR of X
for G being Function of X,X st a < b & G is_Lipschitzian_on the carrier of X holds
Fredholm (G,a,b,y0) is with_unique_fixpoint

proof end;

theorem Th58: :: ORDEQ_02:27

for X being RealBanachSpace
for Z being open Subset of REAL
for a, b being Real
for y0 being VECTOR of X
for G being Function of X,X
for f, g being continuous PartFunc of REAL, the carrier of X st dom f = ['a,b'] & dom g = ['a,b'] & Z = ].a,b.[ & a < b & G is_Lipschitzian_on the carrier of X & 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 Th59: :: ORDEQ_02:28

for X being RealBanachSpace
for Z being open Subset of REAL
for a, b being Real
for y0 being VECTOR of X
for G being Function of X,X
for y being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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_02:29

for X being RealBanachSpace
for Z being open Subset of REAL
for a, b being Real
for y0 being VECTOR of X
for G being Function of X,X
for y1, y2 being continuous PartFunc of REAL, the carrier of X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X & 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_02:30

for X being RealBanachSpace
for Z being open Subset of REAL
for a, b being Real
for y0 being VECTOR of X
for G being Function of X,X st a < b & Z = ].a,b.[ & G is_Lipschitzian_on the carrier of X holds
ex y being continuous PartFunc of REAL, the carrier of X 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;