let T be non empty TopSpace; for FS1 being Functional_Sequence of the carrier of T,REAL st ( for n being Element of NAT ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) ) ) & ex seq being Real_Sequence st
( seq is summable & ( for n being Element of NAT
for p being Point of T holds (FS1 # p) . n <= seq . n ) ) holds
for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous
let FS1 be Functional_Sequence of the carrier of T,REAL; ( ( for n being Element of NAT ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) ) ) & ex seq being Real_Sequence st
( seq is summable & ( for n being Element of NAT
for p being Point of T holds (FS1 # p) . n <= seq . n ) ) implies for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous )
assume that
A1:
for n being Element of NAT ex f being RealMap of T st
( FS1 . n = f & f is continuous & ( for p being Point of T holds f . p >= 0 ) )
and
A2:
ex seq being Real_Sequence st
( seq is summable & ( for n being Element of NAT
for p being Point of T holds (FS1 # p) . n <= seq . n ) )
; for f being RealMap of T st ( for p being Point of T holds f . p = Sum (FS1 # p) ) holds
f is continuous
let f be RealMap of T; ( ( for p being Point of T holds f . p = Sum (FS1 # p) ) implies f is continuous )
assume A3:
for p being Point of T holds f . p = Sum (FS1 # p)
; f is continuous
reconsider fR = f as Function of T,R^1 by TOPMETR:17;
now let p be
Point of
T;
fR is_continuous_at p
for
R being
Subset of
R^1 st
R is
open &
fR . p in R holds
ex
U being
Subset of
T st
(
U is
open &
p in U &
fR .: U c= R )
proof
reconsider fRp =
fR . p as
Point of
RealSpace by METRIC_1:def 13;
let R be
Subset of
R^1;
( R is open & fR . p in R implies ex U being Subset of T st
( U is open & p in U & fR .: U c= R ) )
assume
(
R is
open &
fR . p in R )
;
ex U being Subset of T st
( U is open & p in U & fR .: U c= R )
then consider rn being
real number such that A4:
rn > 0
and A5:
Ball (
fRp,
rn)
c= R
by TOPMETR:15, TOPMETR:def 6;
set r2 =
rn / 2;
set r4 =
rn / 4;
reconsider r2 =
rn / 2,
r4 =
rn / 4 as
Real ;
A6:
r4 > 0
by A4, XREAL_1:224;
consider seq being
Real_Sequence such that A7:
seq is
summable
and A8:
for
n being
Element of
NAT for
q being
Point of
T holds
(FS1 # q) . n <= seq . n
by A2;
Partial_Sums seq is
convergent
by A7, SERIES_1:def 2;
then consider n being
Element of
NAT such that A9:
for
m being
Element of
NAT st
n <= m holds
abs (((Partial_Sums seq) . m) - (lim (Partial_Sums seq))) < r4
by A6, SEQ_2:def 7;
defpred S1[
set ,
set ]
means ex
SS being
Subset of
T st
(
SS = $2 &
SS is
open &
p in SS & ( for
f1 being
RealMap of
T st
FS1 . $1
= f1 holds
for
f1p being
Point of
RealSpace st
f1p = f1 . p holds
f1 .: SS c= Ball (
f1p,
(r2 / (n + 1))) ) );
A10:
for
k being
set st
k in {0} \/ (Seg n) holds
ex
U being
set st
(
U in bool the
carrier of
T &
S1[
k,
U] )
proof
let k be
set ;
( k in {0} \/ (Seg n) implies ex U being set st
( U in bool the carrier of T & S1[k,U] ) )
assume
k in {0} \/ (Seg n)
;
ex U being set st
( U in bool the carrier of T & S1[k,U] )
then
(
k in Seg n or
k in {0} )
by XBOOLE_0:def 3;
then reconsider k =
k as
Element of
NAT by TARSKI:def 1;
consider f1 being
RealMap of
T such that A11:
FS1 . k = f1
and A12:
f1 is
continuous
and
for
p being
Point of
T holds
f1 . p >= 0
by A1;
reconsider f19 =
f1 as
Function of
T,
R^1 by TOPMETR:17;
reconsider f1p =
f19 . p as
Point of
RealSpace by METRIC_1:def 13;
set B =
Ball (
f1p,
(r2 / (n + 1)));
reconsider B =
Ball (
f1p,
(r2 / (n + 1))) as
Subset of
R^1 by METRIC_1:def 13, TOPMETR:17;
(
dist (
f1p,
f1p)
= 0 &
r2 > 0 )
by A4, METRIC_1:1, XREAL_1:215;
then
dist (
f1p,
f1p)
< r2 / (n + 1)
by XREAL_1:139;
then A13:
f1p in B
by METRIC_1:11;
f19 is
continuous
by A12, TOPREAL6:74;
then
(
B is
open &
f19 is_continuous_at p )
by TMAP_1:50, TOPMETR:14, TOPMETR:def 6;
then consider U being
Subset of
T such that A14:
(
U is
open &
p in U )
and A15:
f19 .: U c= B
by A13, TMAP_1:43;
for
f1 being
RealMap of
T st
FS1 . k = f1 holds
for
f1p being
Point of
RealSpace st
f1p = f1 . p holds
f1 .: U c= Ball (
f1p,
(r2 / (n + 1)))
by A11, A15;
hence
ex
U being
set st
(
U in bool the
carrier of
T &
S1[
k,
U] )
by A14;
verum
end;
consider FSn being
Function of
({0} \/ (Seg n)),
(bool the carrier of T) such that A16:
for
k being
set st
k in {0} \/ (Seg n) holds
S1[
k,
FSn . k]
from FUNCT_2:sch 1(A10);
A17:
for
k being
Element of
NAT for
q being
Point of
T holds
(FS1 # q) . k >= 0
A18:
for
k being
Element of
NAT holds
(seq ^\ (n + 1)) . k >= 0
reconsider RNG =
rng FSn as
Subset-Family of
T ;
A19:
RNG is
open
0 in {0}
by TARSKI:def 1;
then
0 in {0} \/ (Seg n)
by XBOOLE_0:def 3;
then reconsider RNG =
RNG as non
empty Subset-Family of
T by FUNCT_2:4;
A22:
(
lim (Partial_Sums seq) = Sum seq &
Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) )
by A7, SERIES_1:15, SERIES_1:def 3;
abs (((Partial_Sums seq) . n) - (lim (Partial_Sums seq))) < r4
by A9;
then
abs (- (Sum (seq ^\ (n + 1)))) < r4
by A22;
then A23:
abs (Sum (seq ^\ (n + 1))) < r4
by COMPLEX1:52;
seq ^\ (n + 1) is
summable
by A7, SERIES_1:12;
then
Sum (seq ^\ (n + 1)) >= 0
by A18, SERIES_1:18;
then A24:
Sum (seq ^\ (n + 1)) < r4
by A23, ABSVALUE:def 1;
A25:
for
q being
Point of
T holds
(
FS1 # q is
summable &
0 <= Sum ((FS1 # q) ^\ (n + 1)) &
Sum ((FS1 # q) ^\ (n + 1)) < r4 )
proof
let q be
Point of
T;
( FS1 # q is summable & 0 <= Sum ((FS1 # q) ^\ (n + 1)) & Sum ((FS1 # q) ^\ (n + 1)) < r4 )
set F =
FS1 # q;
A28:
for
k being
Element of
NAT holds
(
0 <= (FS1 # q) . k &
(FS1 # q) . k <= seq . k )
by A8, A17;
then
FS1 # q is
summable
by A7, SERIES_1:20;
then A29:
(FS1 # q) ^\ (n + 1) is
summable
by SERIES_1:12;
seq ^\ (n + 1) is
summable
by A7, SERIES_1:12;
then
Sum ((FS1 # q) ^\ (n + 1)) <= Sum (seq ^\ (n + 1))
by A26, SERIES_1:20;
hence
(
FS1 # q is
summable &
0 <= Sum ((FS1 # q) ^\ (n + 1)) &
Sum ((FS1 # q) ^\ (n + 1)) < r4 )
by A7, A24, A28, A26, A29, SERIES_1:18, SERIES_1:20, XXREAL_0:2;
verum
end;
A30:
fR .: (meet RNG) c= R
proof
let fRq be
set ;
TARSKI:def 3 ( not fRq in fR .: (meet RNG) or fRq in R )
assume
fRq in fR .: (meet RNG)
;
fRq in R
then consider q being
set such that A31:
q in dom fR
and A32:
q in meet RNG
and A33:
fRq = fR . q
by FUNCT_1:def 6;
reconsider q =
q as
Point of
T by A31;
set sp =
FS1 # p;
set sq =
FS1 # q;
set spn =
(FS1 # p) ^\ (n + 1);
set sqn =
(FS1 # q) ^\ (n + 1);
set absPSpq =
Partial_Sums (abs ((FS1 # p) - (FS1 # q)));
for
k being
Element of
NAT st
k <= n holds
(abs ((FS1 # p) - (FS1 # q))) . k <= r2 / (n + 1)
proof
let k be
Element of
NAT ;
( k <= n implies (abs ((FS1 # p) - (FS1 # q))) . k <= r2 / (n + 1) )
assume A34:
k <= n
;
(abs ((FS1 # p) - (FS1 # q))) . k <= r2 / (n + 1)
(
k = 0 or
k >= 1 )
by NAT_1:14;
then
(
k in {0} or
k in Seg n )
by A34, FINSEQ_1:1, TARSKI:def 1;
then A35:
k in {0} \/ (Seg n)
by XBOOLE_0:def 3;
then
FSn . k in RNG
by FUNCT_2:4;
then A36:
q in FSn . k
by A32, SETFAM_1:def 1;
dom ((FS1 # p) - (FS1 # q)) = NAT
by FUNCT_2:def 1;
then A37:
((FS1 # p) - (FS1 # q)) . k = ((FS1 # p) . k) - ((FS1 # q) . k)
by VALUED_1:13;
consider f1 being
RealMap of
T such that A38:
FS1 . k = f1
and
f1 is
continuous
and
for
p being
Point of
T holds
f1 . p >= 0
by A1;
reconsider f1p =
f1 . p,
f1q =
f1 . q as
Point of
RealSpace by METRIC_1:def 13;
ex
SS being
Subset of
T st
(
SS = FSn . k &
SS is
open &
p in SS & ( for
f1 being
RealMap of
T st
FS1 . k = f1 holds
for
f1p being
Point of
RealSpace st
f1p = f1 . p holds
f1 .: SS c= Ball (
f1p,
(r2 / (n + 1))) ) )
by A16, A35;
then A39:
f1 .: (FSn . k) c= Ball (
f1p,
(r2 / (n + 1)))
by A38;
dom f1 = the
carrier of
T
by FUNCT_2:def 1;
then
f1q in f1 .: (FSn . k)
by A36, FUNCT_1:def 6;
then
dist (
f1p,
f1q)
< r2 / (n + 1)
by A39, METRIC_1:11;
then A40:
abs ((f1 . p) - (f1 . q)) < r2 / (n + 1)
by TOPMETR:11;
f1 . p = (FS1 # p) . k
by A38, SEQFUNC:def 10;
then
abs (((FS1 # p) . k) - ((FS1 # q) . k)) < r2 / (n + 1)
by A38, A40, SEQFUNC:def 10;
hence
(abs ((FS1 # p) - (FS1 # q))) . k <= r2 / (n + 1)
by A37, SEQ_1:12;
verum
end;
then A41:
(Partial_Sums (abs ((FS1 # p) - (FS1 # q)))) . n <= (r2 / (n + 1)) * (n + 1)
by Th12;
set PSp =
Partial_Sums (FS1 # p);
set PSq =
Partial_Sums (FS1 # q);
set PSpq =
Partial_Sums ((FS1 # p) - (FS1 # q));
(
(Partial_Sums (FS1 # p)) - (Partial_Sums (FS1 # q)) = Partial_Sums ((FS1 # p) - (FS1 # q)) &
dom ((Partial_Sums (FS1 # p)) - (Partial_Sums (FS1 # q))) = NAT )
by SEQ_1:1, SERIES_1:6;
then A42:
abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) = abs ((Partial_Sums ((FS1 # p) - (FS1 # q))) . n)
by VALUED_1:13;
abs ((Partial_Sums ((FS1 # p) - (FS1 # q))) . n) <= (Partial_Sums (abs ((FS1 # p) - (FS1 # q)))) . n
by Th13;
then
abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) <= (r2 / (n + 1)) * (n + 1)
by A42, A41, XXREAL_0:2;
then A43:
abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) <= r2
by XCMPLX_1:87;
0 <= Sum ((FS1 # p) ^\ (n + 1))
by A25;
then A44:
abs (Sum ((FS1 # p) ^\ (n + 1))) = Sum ((FS1 # p) ^\ (n + 1))
by ABSVALUE:def 1;
0 <= Sum ((FS1 # q) ^\ (n + 1))
by A25;
then A45:
abs (Sum ((FS1 # q) ^\ (n + 1))) = Sum ((FS1 # q) ^\ (n + 1))
by ABSVALUE:def 1;
reconsider fRq =
fR . q as
Point of
RealSpace by METRIC_1:def 13;
A46:
abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))) <= (abs (Sum ((FS1 # p) ^\ (n + 1)))) + (abs (Sum ((FS1 # q) ^\ (n + 1))))
by COMPLEX1:57;
A47:
(
fRp = Sum (FS1 # p) &
fRq = Sum (FS1 # q) )
by A3;
(
Sum (FS1 # p) = ((Partial_Sums (FS1 # p)) . n) + (Sum ((FS1 # p) ^\ (n + 1))) &
Sum (FS1 # q) = ((Partial_Sums (FS1 # q)) . n) + (Sum ((FS1 # q) ^\ (n + 1))) )
by A25, SERIES_1:15;
then
abs ((fR . p) - (fR . q)) = abs ((((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n)) + ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))))
by A47;
then A48:
abs ((fR . p) - (fR . q)) <= (abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n))) + (abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))))
by COMPLEX1:56;
(
Sum ((FS1 # p) ^\ (n + 1)) < r4 &
Sum ((FS1 # q) ^\ (n + 1)) < r4 )
by A25;
then
(abs (Sum ((FS1 # p) ^\ (n + 1)))) + (abs (Sum ((FS1 # q) ^\ (n + 1)))) < r4 + r4
by A44, A45, XREAL_1:8;
then
abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1)))) < r2
by A46, XXREAL_0:2;
then
(abs (((Partial_Sums (FS1 # p)) . n) - ((Partial_Sums (FS1 # q)) . n))) + (abs ((Sum ((FS1 # p) ^\ (n + 1))) - (Sum ((FS1 # q) ^\ (n + 1))))) < r2 + r2
by A43, XREAL_1:8;
then
abs ((fR . p) - (fR . q)) < rn
by A48, XXREAL_0:2;
then
dist (
fRp,
fRq)
< rn
by TOPMETR:11;
then
fRq in Ball (
fRp,
rn)
by METRIC_1:11;
hence
fRq in R
by A5, A33;
verum
end;
then
p in meet RNG
by SETFAM_1:def 1;
hence
ex
U being
Subset of
T st
(
U is
open &
p in U &
fR .: U c= R )
by A19, A30, TOPS_2:20;
verum
end; hence
fR is_continuous_at p
by TMAP_1:43;
verum end;
then
fR is continuous
by TMAP_1:50;
hence
f is continuous
by TOPREAL6:74; verum