:: BHSP_6 semantic presentation
:: deftheorem E1 defines setsum BHSP_6:def 1 :
theorem E2: :: BHSP_6:1
proof
let c
1 be
RealUnitarySpace;
assume E3:
( the
add of c
1 is
commutative & the
add of c
1 is
associative & the
add of c
1 is
has_a_unity )
;
let c
2 be
finite Subset of c
1;
let c
3 be
Function of the
carrier of c
1,the
carrier of c
1;
assume E4:
( c
2 c= dom c
3 & for b
1 being
set holds
( b
1 in dom c
3 implies c
3 . b
1 = b
1 ) )
;
consider c
4 being
FinSequence of the
carrier of c
1 such that
E5:
( c
4 is
one-to-one &
rng c
4 = c
2 &
setsum c
2 = the
add of c
1 "**" c
4 )
by E3, E1;
E6:
dom (Func_Seq c3,c4) = dom c
4
now
let c
5 be
set ;
assume E7:
c
5 in dom (Func_Seq c3,c4)
;
dom (Func_Seq c3,c4) is
Subset of
NAT
by RELSET_1:12;
then reconsider c
6 = c
5 as
Nat by E7;
E8:
c
4 . c
6 in rng c
4
by E6, E7, FUNCT_1:12;
(Func_Seq c3,c4) . c
5 =
(c3 * c4) . c
6
by BHSP_5:def 4
.=
c
3 . (c4 . c6)
by E6, E7, FUNCT_1:23
.=
c
4 . c
6
by E4, E5, E8
;
hence
(Func_Seq c3,c4) . c
5 = c
4 . c
5
;
end;
then
Func_Seq c
3,c
4 = c
4
by E6, FUNCT_1:9;
hence
setsum c
2 = setopfunc c
2,the
carrier of c
1,the
carrier of c
1,c
3,the
add of c
1
by E3, E4, E5, BHSP_5:def 5;
end;
theorem E3: :: BHSP_6:2
proof
let c
1 be
RealUnitarySpace;
assume E4:
( the
add of c
1 is
commutative & the
add of c
1 is
associative & the
add of c
1 is
has_a_unity )
;
let c
2, c
3 be
finite Subset of c
1;
assume E5:
c
2 misses c
3
;
let c
4 be
finite Subset of c
1;
assume E6:
c
4 = c
2 \/ c
3
;
reconsider c
5 =
id the
carrier of c
1 as
Function of the
carrier of c
1,the
carrier of c
1 ;
E7:
for b
1 being
set holds
( b
1 in the
carrier of c
1 implies c
5 . b
1 = b
1 )
by FUNCT_1:35;
E8:
dom c
5 = the
carrier of c
1
by FUNCT_2:def 1;
then E9:
setsum c
2 = setopfunc c
2,the
carrier of c
1,the
carrier of c
1,c
5,the
add of c
1
by E4, E7, E2;
E10:
setsum c
3 = setopfunc c
3,the
carrier of c
1,the
carrier of c
1,c
5,the
add of c
1
by E4, E7, E8, E2;
setopfunc c
4,the
carrier of c
1,the
carrier of c
1,c
5,the
add of c
1 =
the
add of c
1 . (setopfunc c2,the carrier of c1,the carrier of c1,c5,the add of c1),
(setopfunc c3,the carrier of c1,the carrier of c1,c5,the add of c1)
by E4, E5, E6, E8, BHSP_5:14
.=
(setopfunc c2,the carrier of c1,the carrier of c1,c5,the add of c1) + (setopfunc c3,the carrier of c1,the carrier of c1,c5,the add of c1)
by RLVECT_1:5
;
hence
setsum c
4 = (setsum c2) + (setsum c3)
by E4, E7, E8, E9, E10, E2;
end;
:: deftheorem E4 defines summable_set BHSP_6:def 2 :
definition
let c
1 be
RealUnitarySpace;
let c
2 be
Subset of c
1;
assume E5:
c
2 is
summable_set
;
func sum a
2 -> Point of a
1 means :: BHSP_6:def 3
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
finite Subset of a
1 holds
not ( not b
2 is
empty & b
2 c= a
2 & for b
3 being
finite Subset of a
1 holds
not ( b
2 c= b
3 & b
3 c= a
2 & not
||.(a3 - (setsum b3)).|| < b
1 ) ) );
existence
ex b1 being Point of c1 st
for b2 being Real holds
not ( b2 > 0 & for b3 being finite Subset of c1 holds
not ( not b3 is empty & b3 c= c2 & for b4 being finite Subset of c1 holds
not ( b3 c= b4 & b4 c= c2 & not ||.(b1 - (setsum b4)).|| < b2 ) ) )
by E5, E4;
uniqueness
for b1, b2 being Point of c1 holds
( ( for b3 being Real holds
not ( b3 > 0 & for b4 being finite Subset of c1 holds
not ( not b4 is empty & b4 c= c2 & for b5 being finite Subset of c1 holds
not ( b4 c= b5 & b5 c= c2 & not ||.(b1 - (setsum b5)).|| < b3 ) ) ) & for b3 being Real holds
not ( b3 > 0 & for b4 being finite Subset of c1 holds
not ( not b4 is empty & b4 c= c2 & for b5 being finite Subset of c1 holds
not ( b4 c= b5 & b5 c= c2 & not ||.(b2 - (setsum b5)).|| < b3 ) ) ) ) implies ( b1 = b2 ) )
proof
let c
3, c
4 be
Point of c
1;
assume that
E6:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( b
2 c= b
3 & b
3 c= c
2 & not
||.(c3 - (setsum b3)).|| < b
1 ) ) )
and
E7:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( b
2 c= b
3 & b
3 c= c
2 & not
||.(c4 - (setsum b3)).|| < b
1 ) ) )
;
E8:
now
let c
5 be
Real;
assume E9:
c
5 > 0
;
set c
6 = c
5 / 2;
E10:
( c
5 / 2 is
Real & c
5 / 2
> 0 )
by E9, REAL_2:127;
E11:
(c5 / 2) + (c5 / 2) = c
5
;
consider c
7 being
finite Subset of c
1 such that
E12:
( not c
7 is
empty & c
7 c= c
2 & for b
1 being
finite Subset of c
1 holds
not ( c
7 c= b
1 & b
1 c= c
2 & not
||.(c3 - (setsum b1)).|| < c
5 / 2 ) )
by E6, E10;
consider c
8 being
finite Subset of c
1 such that
E13:
( not c
8 is
empty & c
8 c= c
2 & for b
1 being
finite Subset of c
1 holds
not ( c
8 c= b
1 & b
1 c= c
2 & not
||.(c4 - (setsum b1)).|| < c
5 / 2 ) )
by E7, E10;
set c
9 = c
7 \/ c
8;
E14:
c
7 \/ c
8 c= c
2
by E12, E13, XBOOLE_1:8;
( c
7 \/ c
8 is
finite Subset of c
1 & c
7 c= c
7 \/ c
8 )
by XBOOLE_1:7;
then E15:
||.(c3 - (setsum (c7 \/ c8))).|| < c
5 / 2
by E12, E14;
( c
7 \/ c
8 is
finite Subset of c
1 & c
8 c= c
7 \/ c
8 )
by XBOOLE_1:7;
then
||.(c4 - (setsum (c7 \/ c8))).|| < c
5 / 2
by E13, E14;
then
||.(- (c4 - (setsum (c7 \/ c8)))).|| < c
5 / 2
by BHSP_1:37;
then E16:
||.(c3 - (setsum (c7 \/ c8))).|| + ||.(- (c4 - (setsum (c7 \/ c8)))).|| < c
5
by E11, E15, XREAL_1:10;
||.((c3 - (setsum (c7 \/ c8))) + (- (c4 - (setsum (c7 \/ c8))))).|| <= ||.(c3 - (setsum (c7 \/ c8))).|| + ||.(- (c4 - (setsum (c7 \/ c8)))).||
by BHSP_1:36;
then
||.((c3 - (setsum (c7 \/ c8))) + (- (c4 - (setsum (c7 \/ c8))))).|| + (||.(c3 - (setsum (c7 \/ c8))).|| + ||.(- (c4 - (setsum (c7 \/ c8)))).||) < (||.(c3 - (setsum (c7 \/ c8))).|| + ||.(- (c4 - (setsum (c7 \/ c8)))).||) + c
5
by E16, XREAL_1:10;
then E17:
(||.((c3 - (setsum (c7 \/ c8))) + (- (c4 - (setsum (c7 \/ c8))))).|| + (||.(c3 - (setsum (c7 \/ c8))).|| + ||.(- (c4 - (setsum (c7 \/ c8)))).||)) + (- (||.(c3 - (setsum (c7 \/ c8))).|| + ||.(- (c4 - (setsum (c7 \/ c8)))).||)) < (c5 + (||.(c3 - (setsum (c7 \/ c8))).|| + ||.(- (c4 - (setsum (c7 \/ c8)))).||)) + (- (||.(c3 - (setsum (c7 \/ c8))).|| + ||.(- (c4 - (setsum (c7 \/ c8)))).||))
by XREAL_1:10;
||.(c3 - c4).|| =
||.((c3 - c4) + (0. c1)).||
by RLVECT_1:def 7
.=
||.((c3 - c4) + ((setsum (c7 \/ c8)) + (- (setsum (c7 \/ c8))))).||
by RLVECT_1:16
.=
||.((c3 - c4) + ((setsum (c7 \/ c8)) - (setsum (c7 \/ c8)))).||
by RLVECT_1:def 11
.=
||.(((c3 - c4) + (setsum (c7 \/ c8))) - (setsum (c7 \/ c8))).||
by RLVECT_1:42
.=
||.((c3 - (c4 - (setsum (c7 \/ c8)))) - (setsum (c7 \/ c8))).||
by RLVECT_1:43
.=
||.(c3 - ((setsum (c7 \/ c8)) + (c4 - (setsum (c7 \/ c8))))).||
by RLVECT_1:41
.=
||.((c3 - (setsum (c7 \/ c8))) - (c4 - (setsum (c7 \/ c8)))).||
by RLVECT_1:41
.=
||.((c3 - (setsum (c7 \/ c8))) + (- (c4 - (setsum (c7 \/ c8))))).||
by RLVECT_1:def 11
;
hence
||.(c3 - c4).|| < c
5
by E17;
end;
c
3 = c
4
hence
c
3 = c
4
;
end;
end;
:: deftheorem defines sum BHSP_6:def 3 :
:: deftheorem E5 defines Bounded BHSP_6:def 4 :
:: deftheorem E6 defines weakly_summable_set BHSP_6:def 5 :
:: deftheorem E7 defines is_summable_set_by BHSP_6:def 6 :
definition
let c
1 be
RealUnitarySpace;
let c
2 be
Subset of c
1;
let c
3 be
Functional of c
1;
assume E8:
c
2 is_summable_set_by c
3
;
func sum_byfunc a
2,a
3 -> Real means :: BHSP_6:def 7
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
finite Subset of a
1 holds
not ( not b
2 is
empty & b
2 c= a
2 & for b
3 being
finite Subset of a
1 holds
not ( b
2 c= b
3 & b
3 c= a
2 & not
abs (a4 - (setopfunc b3,the carrier of a1,REAL ,a3,addreal )) < b
1 ) ) );
existence
ex b1 being Real st
for b2 being Real holds
not ( b2 > 0 & for b3 being finite Subset of c1 holds
not ( not b3 is empty & b3 c= c2 & for b4 being finite Subset of c1 holds
not ( b3 c= b4 & b4 c= c2 & not abs (b1 - (setopfunc b4,the carrier of c1,REAL ,c3,addreal )) < b2 ) ) )
by E8, E7;
uniqueness
for b1, b2 being Real holds
( ( for b3 being Real holds
not ( b3 > 0 & for b4 being finite Subset of c1 holds
not ( not b4 is empty & b4 c= c2 & for b5 being finite Subset of c1 holds
not ( b4 c= b5 & b5 c= c2 & not abs (b1 - (setopfunc b5,the carrier of c1,REAL ,c3,addreal )) < b3 ) ) ) & for b3 being Real holds
not ( b3 > 0 & for b4 being finite Subset of c1 holds
not ( not b4 is empty & b4 c= c2 & for b5 being finite Subset of c1 holds
not ( b4 c= b5 & b5 c= c2 & not abs (b2 - (setopfunc b5,the carrier of c1,REAL ,c3,addreal )) < b3 ) ) ) ) implies ( b1 = b2 ) )
proof
let c
4, c
5 be
Real;
assume that
E9:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( b
2 c= b
3 & b
3 c= c
2 & not
abs (c4 - (setopfunc b3,the carrier of c1,REAL ,c3,addreal )) < b
1 ) ) )
and
E10:
for b
1 being
Real holds
not ( b
1 > 0 & for b
2 being
finite Subset of c
1 holds
not ( not b
2 is
empty & b
2 c= c
2 & for b
3 being
finite Subset of c
1 holds
not ( b
2 c= b
3 & b
3 c= c
2 & not
abs (c5 - (setopfunc b3,the carrier of c1,REAL ,c3,addreal )) < b
1 ) ) )
;
E11:
now
let c
6 be
real number ;
assume E12:
c
6 > 0
;
set c
7 = c
6 / 2;
E13:
( c
6 / 2 is
Real & c
6 / 2
> 0 )
by E12, REAL_2:127, XREAL_0:def 1;
E14:
(c6 / 2) + (c6 / 2) = c
6
;
consider c
8 being
finite Subset of c
1 such that
E15:
( not c
8 is
empty & c
8 c= c
2 & for b
1 being
finite Subset of c
1 holds
not ( c
8 c= b
1 & b
1 c= c
2 & not
abs (c4 - (setopfunc b1,the carrier of c1,REAL ,c3,addreal )) < c
6 / 2 ) )
by E9, E13;
consider c
9 being
finite Subset of c
1 such that
E16:
( not c
9 is
empty & c
9 c= c
2 & for b
1 being
finite Subset of c
1 holds
not ( c
9 c= b
1 & b
1 c= c
2 & not
abs (c5 - (setopfunc b1,the carrier of c1,REAL ,c3,addreal )) < c
6 / 2 ) )
by E10, E13;
set c
10 = c
8 \/ c
9;
E17:
c
8 \/ c
9 c= c
2
by E15, E16, XBOOLE_1:8;
( c
8 \/ c
9 is
finite Subset of c
1 & c
8 c= c
8 \/ c
9 )
by XBOOLE_1:7;
then E18:
abs (c4 - (setopfunc (c8 \/ c9),the carrier of c1,REAL ,c3,addreal )) < c
6 / 2
by E15, E17;
( c
8 \/ c
9 is
finite Subset of c
1 & c
9 c= c
8 \/ c
9 )
by XBOOLE_1:7;
then E19:
abs (c5 - (setopfunc (c8 \/ c9),the carrier of c1,REAL ,c3,addreal )) < c
6 / 2
by E16, E17;
E20:
abs ((c4 - (setopfunc (c8 \/ c9),the carrier of c1,REAL ,c3,addreal )) - (c5 - (setopfunc (c8 \/ c9),the carrier of c1,REAL ,c3,addreal ))) <= (abs (c4 - (setopfunc (c8 \/ c9),the carrier of c1,REAL ,c3,addreal ))) + (abs (c5 - (setopfunc (c8 \/ c9),the carrier of c1,REAL ,c3,addreal )))
by COMPLEX1:143;
(abs (c4 - (setopfunc (c8 \/ c9),the carrier of c1,REAL ,c3,addreal ))) + (abs (c5 - (setopfunc (c8 \/ c9),the carrier of c1,REAL ,c3,addreal ))) < c
6
by E14, E18, E19, XREAL_1:10;
hence
abs (c4 - c5) < c
6
by E20, XREAL_1:2;
end;
c
4 = c
5
hence
c
4 = c
5
;
end;
end;
:: deftheorem defines sum_byfunc BHSP_6:def 7 :
theorem E8: :: BHSP_6:3
theorem E9: :: BHSP_6:4
proof
let c
1 be
RealUnitarySpace;
let c
2 be
linear-Functional of c
1;
let c
3 be
FinSequence of the
carrier of c
1;
assume E10:
len c
3 >= 1
;
let c
4 be
FinSequence of
REAL ;
assume E11:
(
dom c
3 = dom c
4 & for b
1 being
Nat holds
( b
1 in dom c
4 implies c
4 . b
1 = c
2 . (c3 . b1) ) )
;
consider c
5 being
Function of
NAT ,the
carrier of c
1 such that
E12:
c
5 . 1
= c
3 . 1
and
E13:
for b
1 being
Nat holds
( ( ) implies ( not 0
<> b
1 or not b
1 < len c
3 or c
5 . (b1 + 1) = the
add of c
1 . (c5 . b1),
(c3 . (b1 + 1)) ) )
and
E14:
the
add of c
1 "**" c
3 = c
5 . (len c3)
by E10, FINSOP_1:2;
Seg (len c4) =
dom c
3
by E11, FINSEQ_1:def 3
.=
Seg (len c3)
by FINSEQ_1:def 3
;
then E15:
len c
4 = len c
3
by FINSEQ_1:8;
then consider c
6 being
Function of
NAT ,
REAL such that
E16:
c
6 . 1
= c
4 . 1
and
E17:
for b
1 being
Nat holds
( ( ) implies ( not 0
<> b
1 or not b
1 < len c
4 or c
6 . (b1 + 1) = addreal . (c6 . b1),
(c4 . (b1 + 1)) ) )
and
E18:
addreal "**" c
4 = c
6 . (len c4)
by E10, FINSOP_1:2;
defpred S
1[
Nat] means ( ( 1
<= a
1 & a
1 <= len c
4 ) implies ( c
6 . a
1 = c
2 . (c5 . a1) ) );
for b
1 being
Nat holds
S
1[b
1]
proof
E19:
S
1[0]
;
E20:
now
let c
7 be
Nat;
assume E21:
S
1[c
7]
;
now
assume E22:
( 1
<= c
7 + 1 & c
7 + 1
<= len c
4 )
;
E23:
c
7 <= c
7 + 1
by NAT_1:29;
per cases
not ( not c
7 = 0 & not c
7 <> 0 )
;
suppose E24:
c
7 = 0
;
end;
suppose E24:
c
7 <> 0
;
then
0
< c
7
;
then E25:
0
+ 1
<= c
7
by INT_1:20;
E26:
(c7 + 1) - 1
< (len c4) - 0
by E22, REAL_1:92;
E27:
c
7 + 1
in dom c
4
by E22, FINSEQ_3:27;
reconsider c
8 = c
5 . c
7 as
Element of c
1 ;
c
3 . (c7 + 1) in rng c
3
by E11, E27, FUNCT_1:12;
then reconsider c
9 = c
3 . (c7 + 1) as
Element of c
1 ;
reconsider c
10 = c
8 as
VECTOR of c
1 ;
reconsider c
11 = c
9 as
VECTOR of c
1 ;
set c
12 = c
2 . c
10;
set c
13 = c
2 . c
11;
thus c
6 . (c7 + 1) =
addreal . (c6 . c7),
(c4 . (c7 + 1))
by E17, E24, E26
.=
addreal . (c2 . (c5 . c7)),
(c2 . c9)
by E11, E21, E22, E23, E25, E27, XREAL_1:2
.=
(c2 . c10) + (c2 . c11)
by BINOP_2:def 9
.=
c
2 . (c10 + c11)
by HAHNBAN:def 4
.=
c
2 . (the add of c1 . (c5 . c7),(c3 . (c7 + 1)))
by RLVECT_1:5
.=
c
2 . (c5 . (c7 + 1))
by E13, E15, E24, E26
;
end;
end;
end;
hence
S
1[c
7 + 1]
;
end;
thus
for b
1 being
Nat holds
S
1[b
1]
from NAT_1:sch 1(E19, E20);
end;
hence
c
2 . (the add of c1 "**" c3) = addreal "**" c
4
by E10, E14, E15, E18;
end;
theorem E10: :: BHSP_6:5