environ
vocabularies HIDDEN, 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, LOPBAN_1, ORDEQ_01, STRUCT_0, COMPLEX1, VALUED_1, ALI2, SUPINF_2, XBOOLE_0, ABIAN, INTEGRA1, FINSEQ_1, TARSKI, INTEGRA5, MEASURE7, CARD_3, XXREAL_1, PARTFUN1, RLVECT_1, SEQ_4, FUNCT_2, RCOMP_1, VALUED_0, XXREAL_2, FCONT_1, CFCONT_1, MEASURE5, NFCONT_1, FUNCOP_1, REALSET1, FDIFF_1, INTEGRA7, SERIES_1, SIN_COS, REAL_NS1, NEWTON, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2, VALUED_1, SEQ_1, SEQ_2, RVSUM_1, NEWTON, SEQ_4, RCOMP_1, FCONT_1, FDIFF_1, ABIAN, POWER, SERIES_1, MEASURE5, SIN_COS, INTEGRA1, INTEGRA5, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, EUCLID, LOPBAN_1, NFCONT_1, NFCONT_2, NDIFF_1, REAL_NS1, INTEGRA7, PDIFF_1, INTEGR18, NFCONT_3, NDIFF_3, NDIFF_5, INTEGR19, ORDEQ_01;
definitions TARSKI;
theorems TARSKI, ABSVALUE, RLVECT_1, NORMSP_0, XCMPLX_1, SEQ_1, SEQ_2, SERIES_1, PARTFUN1, PARTFUN2, INTEGRA7, FUNCT_1, POWER, FUNCT_2, NORMSP_1, XREAL_1, LOPBAN_1, FUNCT_7, XXREAL_0, XREAL_0, ORDINAL1, RELAT_1, NFCONT_1, NFCONT_3, FCONT_1, SEQ_4, VFUNCT_1, NEWTON, XBOOLE_0, RCOMP_1, FUNCOP_1, FINSEQ_1, NDIFF_3, SIN_COS, COMSEQ_2, INTEGRA2, XXREAL_1, RVSUM_1, COMPLEX1, NDIFF_4, PDIFF_1, FDIFF_1, VALUED_1, XBOOLE_1, INTEGR19, REAL_NS1, INTEGRA4, INTEGRA5, HOLDER_1, INT_1, RELSET_1, ORDEQ_01, NDIFF_1, INTEGRA6, FINSEQ_2, XXREAL_2, FRECHET, RLTOPSP1, NDIFF_5, ZFMISC_1, VECTSP_1, INTEGR18, INTEGR21;
schemes SEQ_1, NAT_1, FUNCT_2, PARTFUN1;
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, ORDINAL1, FUNCOP_1, NEWTON, NFCONT_3, XXREAL_2, RCOMP_1, RLVECT_1, REAL_NS1, VALUED_0, FDIFF_1, FCONT_1, MEASURE5, POWER, PREPOWER, LOPBAN_1, ORDEQ_01, NDIFF_1, INT_1, PDIFF_1;
constructors HIDDEN, ABIAN, SEQ_2, RELSET_1, SEQ_4, VFUNCT_1, PDIFF_1, RLSUB_1, FCONT_1, NFCONT_1, INTEGRA3, INTEGRA4, NDIFF_1, NDIFF_3, INTEGR18, RVSUM_1, INTEGR19, INTEGR15, COMSEQ_2, VALUED_2, FDIFF_1, INTEGRA7, COMSEQ_3, SIN_COS, NFCONT_2, C0SP2, ORDEQ_01, RFUNCT_1, RFINSEQ2, SQUARE_1, PDIFF_7, NDIFF_5, INTEGR20;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RCOMP_1, RVSUM_1, ORDEQ_01, ABIAN, SUBSET_1, STRUCT_0, ALGSTR_0, NORMSP_0, RSSPACE4, FDIFF_1, RLVECT_1, FINSEQ_1, EUCLID, RLSUB_1, INTEGRA5, ORDINAL1, INTEGRA1, INTEGRA3, INTEGRA2, VALUED_2, NDIFF_1, NDIFF_3, NORMSP_1, XCMPLX_0, NDIFF_5, LOPBAN_1, PDIFF_1, SQUARE_1, VALUED_1, INTEGR20;
expansions RCOMP_1, RVSUM_1, ORDEQ_01, ABIAN, SUBSET_1, STRUCT_0, ALGSTR_0, NORMSP_0, RSSPACE4, FDIFF_1, RLVECT_1, FINSEQ_1, EUCLID, RLSUB_1, INTEGRA5, INTEGRA1, INTEGRA2, NFCONT_2, NFCONT_3, VALUED_2, NDIFF_1, NDIFF_3, NORMSP_1, INTEGR19, FUNCT_3, TARSKI, ORDINAL1, NDIFF_5, PDIFF_7, NFCONT_1, INTEGR20;
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*> ) ) )
LM519A:
for x being Point of (REAL-NS 1) ex z being Real st x = <*z*>
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).|
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)
Lm17:
for a being Real
for X being RealNormSpace
for x being Point of X holds ||.((a ") * x).|| = ||.x.|| / |.a.|
theorem Th1955:
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 )
theorem Th40:
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 ) )
theorem Th47:
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
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) )
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
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 )
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 )
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:
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
ex b1 being Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)),(R_NormSpace_of_ContinuousFunctions (['a,b'],X)) st
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 & b1 . 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)) ) )
uniqueness
for b1, b2 being Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)),(R_NormSpace_of_ContinuousFunctions (['a,b'],X)) st ( 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 & b1 . 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)) ) ) ) & ( 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 & b2 . 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)) ) ) ) holds
b1 = b2
end;
::
deftheorem Def8 defines
Fredholm ORDEQ_02:def 1 :
for X being RealBanachSpace
for y0 being VECTOR of X
for G being Function of X,X
for a, b being Real st a <= b & G is_continuous_on dom G holds
for b6 being Function of (R_NormSpace_of_ContinuousFunctions (['a,b'],X)),(R_NormSpace_of_ContinuousFunctions (['a,b'],X)) holds
( b6 = Fredholm (G,a,b,y0) iff 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 & b6 . 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)) ) ) );
theorem Th53:
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).||
theorem Th54:
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).||
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
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) !) )
theorem Th55:
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).||
theorem Th58:
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 ) )