:: LOPBAN_3 semantic presentation
begin
theorem Th1: :: LOPBAN_3:1
for X being non empty right_complementable add-associative right_zeroed NORMSTR
for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds
for m being Element of NAT holds (Partial_Sums seq) . m = 0. X
proof
let X be non empty right_complementable add-associative right_zeroed NORMSTR ; ::_thesis: for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds
for m being Element of NAT holds (Partial_Sums seq) . m = 0. X
let seq be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0. X ) implies for m being Element of NAT holds (Partial_Sums seq) . m = 0. X )
assume A1: for n being Element of NAT holds seq . n = 0. X ; ::_thesis: for m being Element of NAT holds (Partial_Sums seq) . m = 0. X
let m be Element of NAT ; ::_thesis: (Partial_Sums seq) . m = 0. X
defpred S1[ Element of NAT ] means seq . $1 = (Partial_Sums seq) . $1;
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
thus seq . (k + 1) = (0. X) + (seq . (k + 1)) by RLVECT_1:4
.= ((Partial_Sums seq) . k) + (seq . (k + 1)) by A1, A3
.= (Partial_Sums seq) . (k + 1) by BHSP_4:def_1 ; ::_thesis: verum
end;
A4: S1[ 0 ] by BHSP_4:def_1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
then seq = Partial_Sums seq by FUNCT_2:63;
hence (Partial_Sums seq) . m = 0. X by A1; ::_thesis: verum
end;
definition
let X be RealNormSpace;
let seq be sequence of X;
attrseq is summable means :Def1: :: LOPBAN_3:def 1
Partial_Sums seq is convergent ;
end;
:: deftheorem Def1 defines summable LOPBAN_3:def_1_:_
for X being RealNormSpace
for seq being sequence of X holds
( seq is summable iff Partial_Sums seq is convergent );
registration
let X be RealNormSpace;
clusterV4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) summable for Element of K32(K33(NAT, the carrier of X));
existence
ex b1 being sequence of X st b1 is summable
proof
reconsider C = NAT --> (0. X) as sequence of X ;
take C ; ::_thesis: C is summable
take 0. X ; :: according to NORMSP_1:def_6,LOPBAN_3:def_1 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= ||.(((Partial_Sums C) . b3) - (0. X)).|| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.(((Partial_Sums C) . b2) - (0. X)).|| ) )
assume A1: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.(((Partial_Sums C) . b2) - (0. X)).|| )
take 0 ; ::_thesis: for b1 being Element of NAT holds
( not 0 <= b1 or not p <= ||.(((Partial_Sums C) . b1) - (0. X)).|| )
let m be Element of NAT ; ::_thesis: ( not 0 <= m or not p <= ||.(((Partial_Sums C) . m) - (0. X)).|| )
assume 0 <= m ; ::_thesis: not p <= ||.(((Partial_Sums C) . m) - (0. X)).||
for n being Element of NAT holds C . n = 0. X by FUNCOP_1:7;
then ||.(((Partial_Sums C) . m) - (0. X)).|| = ||.((0. X) - (0. X)).|| by Th1
.= 0 by NORMSP_1:6 ;
hence not p <= ||.(((Partial_Sums C) . m) - (0. X)).|| by A1; ::_thesis: verum
end;
end;
definition
let X be RealNormSpace;
let seq be sequence of X;
func Sum seq -> Element of X equals :: LOPBAN_3:def 2
lim (Partial_Sums seq);
correctness
coherence
lim (Partial_Sums seq) is Element of X;
;
end;
:: deftheorem defines Sum LOPBAN_3:def_2_:_
for X being RealNormSpace
for seq being sequence of X holds Sum seq = lim (Partial_Sums seq);
definition
let X be RealNormSpace;
let seq be sequence of X;
attrseq is norm_summable means :Def3: :: LOPBAN_3:def 3
||.seq.|| is summable ;
end;
:: deftheorem Def3 defines norm_summable LOPBAN_3:def_3_:_
for X being RealNormSpace
for seq being sequence of X holds
( seq is norm_summable iff ||.seq.|| is summable );
theorem Th2: :: LOPBAN_3:2
for X being RealNormSpace
for seq being sequence of X
for m being Element of NAT holds 0 <= ||.seq.|| . m
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X
for m being Element of NAT holds 0 <= ||.seq.|| . m
let seq be sequence of X; ::_thesis: for m being Element of NAT holds 0 <= ||.seq.|| . m
let m be Element of NAT ; ::_thesis: 0 <= ||.seq.|| . m
||.seq.|| . m = ||.(seq . m).|| by NORMSP_0:def_4;
hence 0 <= ||.seq.|| . m ; ::_thesis: verum
end;
theorem Th3: :: LOPBAN_3:3
for X being RealNormSpace
for x, y, z being Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).||
proof
let X be RealNormSpace; ::_thesis: for x, y, z being Element of X holds ||.(x - y).|| = ||.((x - z) + (z - y)).||
let x, y, z be Element of X; ::_thesis: ||.(x - y).|| = ||.((x - z) + (z - y)).||
thus ||.(x - y).|| = ||.((x - (0. X)) - y).|| by RLVECT_1:13
.= ||.((x - (z - z)) - y).|| by RLVECT_1:5
.= ||.(((x - z) + z) - y).|| by RLVECT_1:29
.= ||.((x - z) + (z - y)).|| by RLVECT_1:def_3 ; ::_thesis: verum
end;
theorem Th4: :: LOPBAN_3:4
for X being RealNormSpace
for seq being sequence of X st seq is convergent holds
for s being Real st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < s
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X st seq is convergent holds
for s being Real st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < s
let seq be sequence of X; ::_thesis: ( seq is convergent implies for s being Real st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < s )
assume seq is convergent ; ::_thesis: for s being Real st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < s
then consider g1 being Element of X such that
A1: for s being Real st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - g1).|| < s by NORMSP_1:def_6;
let s be Real; ::_thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < s )
assume 0 < s ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < s
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
||.((seq . m) - g1).|| < s / 2 by A1, XREAL_1:215;
now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((seq_._m)_-_(seq_._n)).||_<_s
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq . m) - (seq . n)).|| < s )
assume n <= m ; ::_thesis: ||.((seq . m) - (seq . n)).|| < s
then A3: ||.((seq . m) - g1).|| < s / 2 by A2;
A4: ( ||.(((seq . m) - g1) + (g1 - (seq . n))).|| <= ||.((seq . m) - g1).|| + ||.(g1 - (seq . n)).|| & ||.(((seq . m) - g1) + (g1 - (seq . n))).|| = ||.((seq . m) - (seq . n)).|| ) by Th3, NORMSP_1:def_1;
||.((seq . n) - g1).|| < s / 2 by A2;
then ||.(g1 - (seq . n)).|| < s / 2 by NORMSP_1:7;
then ||.((seq . m) - g1).|| + ||.(g1 - (seq . n)).|| < (s / 2) + (s / 2) by A3, XREAL_1:8;
hence ||.((seq . m) - (seq . n)).|| < s by A4, XXREAL_0:2; ::_thesis: verum
end;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < s ; ::_thesis: verum
end;
theorem Th5: :: LOPBAN_3:5
for X being RealNormSpace
for seq being sequence of X holds
( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p )
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X holds
( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p )
let seq be sequence of X; ::_thesis: ( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p )
A1: now__::_thesis:_(_(_for_p_being_Real_st_p_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((seq_._m)_-_(seq_._n)).||_<_p_)_implies_seq_is_Cauchy_sequence_by_Norm_)
assume A2: for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p ; ::_thesis: seq is Cauchy_sequence_by_Norm
now__::_thesis:_for_s_being_Real_st_0_<_s_holds_
ex_k_being_Element_of_NAT_st_
for_m,_n_being_Element_of_NAT_st_k_<=_m_&_k_<=_n_holds_
||.((seq_._m)_-_(seq_._n)).||_<_s
let s be Real; ::_thesis: ( 0 < s implies ex k being Element of NAT st
for m, n being Element of NAT st k <= m & k <= n holds
||.((seq . m) - (seq . n)).|| < s )
assume 0 < s ; ::_thesis: ex k being Element of NAT st
for m, n being Element of NAT st k <= m & k <= n holds
||.((seq . m) - (seq . n)).|| < s
then consider k being Element of NAT such that
A3: for m being Element of NAT st k <= m holds
||.((seq . m) - (seq . k)).|| < s / 2 by A2, XREAL_1:215;
now__::_thesis:_for_m,_n_being_Element_of_NAT_st_k_<=_m_&_k_<=_n_holds_
||.((seq_._m)_-_(seq_._n)).||_<_s
let m, n be Element of NAT ; ::_thesis: ( k <= m & k <= n implies ||.((seq . m) - (seq . n)).|| < s )
assume that
A4: k <= m and
A5: k <= n ; ::_thesis: ||.((seq . m) - (seq . n)).|| < s
||.((seq . n) - (seq . k)).|| < s / 2 by A3, A5;
then A6: ||.((seq . k) - (seq . n)).|| < s / 2 by NORMSP_1:7;
||.((seq . m) - (seq . k)).|| < s / 2 by A3, A4;
then A7: ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).|| < (s / 2) + (s / 2) by A6, XREAL_1:8;
( ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| <= ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).|| & ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| = ||.((seq . m) - (seq . n)).|| ) by Th3, NORMSP_1:def_1;
hence ||.((seq . m) - (seq . n)).|| < s by A7, XXREAL_0:2; ::_thesis: verum
end;
hence ex k being Element of NAT st
for m, n being Element of NAT st k <= m & k <= n holds
||.((seq . m) - (seq . n)).|| < s ; ::_thesis: verum
end;
hence seq is Cauchy_sequence_by_Norm by RSSPACE3:8; ::_thesis: verum
end;
now__::_thesis:_(_seq_is_Cauchy_sequence_by_Norm_implies_for_p_being_Real_st_p_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((seq_._m)_-_(seq_._n)).||_<_p_)
assume A8: seq is Cauchy_sequence_by_Norm ; ::_thesis: for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p
thus for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p ::_thesis: verum
proof
let p be Real; ::_thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p )
assume p > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p
then consider n being Element of NAT such that
A9: for m, k being Element of NAT st n <= m & n <= k holds
||.((seq . m) - (seq . k)).|| < p by A8, RSSPACE3:8;
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p by A9;
hence ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p ; ::_thesis: verum
end;
end;
hence ( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < p ) by A1; ::_thesis: verum
end;
theorem Th6: :: LOPBAN_3:6
for X being RealNormSpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds
for m being Element of NAT holds (Partial_Sums ||.seq.||) . m = 0
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds
for m being Element of NAT holds (Partial_Sums ||.seq.||) . m = 0
let seq be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0. X ) implies for m being Element of NAT holds (Partial_Sums ||.seq.||) . m = 0 )
assume A1: for n being Element of NAT holds seq . n = 0. X ; ::_thesis: for m being Element of NAT holds (Partial_Sums ||.seq.||) . m = 0
let m be Element of NAT ; ::_thesis: (Partial_Sums ||.seq.||) . m = 0
defpred S1[ Element of NAT ] means ||.seq.|| . $1 = (Partial_Sums ||.seq.||) . $1;
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
thus ||.seq.|| . (k + 1) = ||.(0. X).|| + (||.seq.|| . (k + 1))
.= ||.(seq . k).|| + (||.seq.|| . (k + 1)) by A1
.= ((Partial_Sums ||.seq.||) . k) + (||.seq.|| . (k + 1)) by A3, NORMSP_0:def_4
.= (Partial_Sums ||.seq.||) . (k + 1) by SERIES_1:def_1 ; ::_thesis: verum
end;
A4: S1[ 0 ] by SERIES_1:def_1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
hence (Partial_Sums ||.seq.||) . m = ||.seq.|| . m
.= ||.(seq . m).|| by NORMSP_0:def_4
.= ||.(0. X).|| by A1
.= 0 ;
::_thesis: verum
end;
theorem Th7: :: LOPBAN_3:7
for X being RealNormSpace
for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent
proof
let X be RealNormSpace; ::_thesis: for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent
let seq, seq1 be sequence of X; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies seq1 is convergent )
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent ; ::_thesis: seq1 is convergent
consider g1 being Element of X such that
A3: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - g1).|| < p by A2, NORMSP_1:def_6;
take g1 ; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= ||.((seq1 . b3) - g1).|| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.((seq1 . b2) - g1).|| ) )
assume 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.((seq1 . b2) - g1).|| )
then consider n1 being Element of NAT such that
A4: for m being Element of NAT st n1 <= m holds
||.((seq . m) - g1).|| < p by A3;
take n = n1; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= ||.((seq1 . b1) - g1).|| )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.((seq1 . m) - g1).|| )
assume A5: n <= m ; ::_thesis: not p <= ||.((seq1 . m) - g1).||
consider Nseq being increasing sequence of NAT such that
A6: seq1 = seq * Nseq by A1, VALUED_0:def_17;
m <= Nseq . m by SEQM_3:14;
then A7: n <= Nseq . m by A5, XXREAL_0:2;
seq1 . m = seq . (Nseq . m) by A6, FUNCT_2:15;
hence not p <= ||.((seq1 . m) - g1).|| by A4, A7; ::_thesis: verum
end;
theorem Th8: :: LOPBAN_3:8
for X being RealNormSpace
for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
proof
let X be RealNormSpace; ::_thesis: for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
let seq, seq1 be sequence of X; ::_thesis: ( seq1 is subsequence of seq & seq is convergent implies lim seq1 = lim seq )
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent ; ::_thesis: lim seq1 = lim seq
consider Nseq being increasing sequence of NAT such that
A3: seq1 = seq * Nseq by A1, VALUED_0:def_17;
A4: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((seq1_._m)_-_(lim_seq)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p )
assume 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
||.((seq . m) - (lim seq)).|| < p by A2, NORMSP_1:def_7;
take n = n1; ::_thesis: for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq1 . m) - (lim seq)).|| < p )
assume A6: n <= m ; ::_thesis: ||.((seq1 . m) - (lim seq)).|| < p
m <= Nseq . m by SEQM_3:14;
then A7: n <= Nseq . m by A6, XXREAL_0:2;
seq1 . m = seq . (Nseq . m) by A3, FUNCT_2:15;
hence ||.((seq1 . m) - (lim seq)).|| < p by A5, A7; ::_thesis: verum
end;
seq1 is convergent by A1, A2, Th7;
hence lim seq1 = lim seq by A4, NORMSP_1:def_7; ::_thesis: verum
end;
theorem :: LOPBAN_3:9
for X being RealNormSpace
for seq, seq1 being sequence of X
for k being Element of NAT st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th7, Th8;
theorem Th10: :: LOPBAN_3:10
for X being RealNormSpace
for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is convergent
proof
let X be RealNormSpace; ::_thesis: for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds
seq1 is convergent
let seq, seq1 be sequence of X; ::_thesis: ( seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st seq = seq1 ^\ k ; ::_thesis: seq1 is convergent
consider k being Element of NAT such that
A3: seq = seq1 ^\ k by A2;
consider g1 being Element of X such that
A4: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - g1).|| < p by A1, NORMSP_1:def_6;
take g1 ; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= ||.((seq1 . b3) - g1).|| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.((seq1 . b2) - g1).|| ) )
assume 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.((seq1 . b2) - g1).|| )
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
||.((seq . m) - g1).|| < p by A4;
take n = n1 + k; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= ||.((seq1 . b1) - g1).|| )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.((seq1 . m) - g1).|| )
assume A6: n <= m ; ::_thesis: not p <= ||.((seq1 . m) - g1).||
then consider l being Nat such that
A7: m = (n1 + k) + l by NAT_1:10;
reconsider l = l as Element of NAT by ORDINAL1:def_12;
m - k = ((n1 + l) + k) + (- k) by A7;
then reconsider m1 = m - k as Element of NAT ;
now__::_thesis:_n1_<=_m1
assume not n1 <= m1 ; ::_thesis: contradiction
then m1 + k < n1 + k by XREAL_1:6;
hence contradiction by A6; ::_thesis: verum
end;
then ( m1 + k = m & ||.((seq . m1) - g1).|| < p ) by A5;
hence not p <= ||.((seq1 . m) - g1).|| by A3, NAT_1:def_3; ::_thesis: verum
end;
theorem Th11: :: LOPBAN_3:11
for X being RealNormSpace
for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds
lim seq1 = lim seq
proof
let X be RealNormSpace; ::_thesis: for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds
lim seq1 = lim seq
let seq, seq1 be sequence of X; ::_thesis: ( seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k implies lim seq1 = lim seq )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st seq = seq1 ^\ k ; ::_thesis: lim seq1 = lim seq
consider k being Element of NAT such that
A3: seq = seq1 ^\ k by A2;
A4: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((seq1_._m)_-_(lim_seq)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p )
assume 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
||.((seq . m) - (lim seq)).|| < p by A1, NORMSP_1:def_7;
take n = n1 + k; ::_thesis: for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((seq1 . m) - (lim seq)).|| < p )
assume A6: n <= m ; ::_thesis: ||.((seq1 . m) - (lim seq)).|| < p
then consider l being Nat such that
A7: m = (n1 + k) + l by NAT_1:10;
reconsider l = l as Element of NAT by ORDINAL1:def_12;
m - k = ((n1 + l) + k) + (- k) by A7;
then reconsider m1 = m - k as Element of NAT ;
now__::_thesis:_n1_<=_m1
assume not n1 <= m1 ; ::_thesis: contradiction
then m1 + k < n1 + k by XREAL_1:6;
hence contradiction by A6; ::_thesis: verum
end;
then ( m1 + k = m & ||.((seq . m1) - (lim seq)).|| < p ) by A5;
hence ||.((seq1 . m) - (lim seq)).|| < p by A3, NAT_1:def_3; ::_thesis: verum
end;
seq1 is convergent by A1, A2, Th10;
hence lim seq1 = lim seq by A4, NORMSP_1:def_7; ::_thesis: verum
end;
theorem Th12: :: LOPBAN_3:12
for X being RealNormSpace
for seq being sequence of X st seq is constant holds
seq is convergent
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X st seq is constant holds
seq is convergent
let seq be sequence of X; ::_thesis: ( seq is constant implies seq is convergent )
assume seq is constant ; ::_thesis: seq is convergent
then consider r being Element of X such that
A1: for n being Nat holds seq . n = r by VALUED_0:def_18;
take g = r; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= ||.((seq . b3) - g).|| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.((seq . b2) - g).|| ) )
assume A2: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= ||.((seq . b2) - g).|| )
take n = 0 ; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= ||.((seq . b1) - g).|| )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= ||.((seq . m) - g).|| )
assume n <= m ; ::_thesis: not p <= ||.((seq . m) - g).||
||.((seq . m) - g).|| = ||.(r - g).|| by A1
.= ||.(0. X).|| by RLVECT_1:15
.= 0 ;
hence not p <= ||.((seq . m) - g).|| by A2; ::_thesis: verum
end;
theorem Th13: :: LOPBAN_3:13
for X being RealNormSpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds
seq is norm_summable
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X st ( for n being Element of NAT holds seq . n = 0. X ) holds
seq is norm_summable
let seq be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0. X ) implies seq is norm_summable )
assume A1: for n being Element of NAT holds seq . n = 0. X ; ::_thesis: seq is norm_summable
take 0 ; :: according to SEQ_2:def_6,SERIES_1:def_2,LOPBAN_3:def_3 ::_thesis: for b1 being set holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= abs (((Partial_Sums ||.seq.||) . b3) - 0) ) )
let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs (((Partial_Sums ||.seq.||) . b2) - 0) ) )
assume A2: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= abs (((Partial_Sums ||.seq.||) . b2) - 0) )
take 0 ; ::_thesis: for b1 being Element of NAT holds
( not 0 <= b1 or not p <= abs (((Partial_Sums ||.seq.||) . b1) - 0) )
let m be Element of NAT ; ::_thesis: ( not 0 <= m or not p <= abs (((Partial_Sums ||.seq.||) . m) - 0) )
assume 0 <= m ; ::_thesis: not p <= abs (((Partial_Sums ||.seq.||) . m) - 0)
abs (((Partial_Sums ||.seq.||) . m) - 0) = abs (0 - 0) by A1, Th6
.= 0 by ABSVALUE:def_1 ;
hence not p <= abs (((Partial_Sums ||.seq.||) . m) - 0) by A2; ::_thesis: verum
end;
registration
let X be RealNormSpace;
clusterV4() Relation-like NAT -defined the carrier of X -valued Function-like V29( NAT ) V30( NAT , the carrier of X) norm_summable for Element of K32(K33(NAT, the carrier of X));
existence
ex b1 being sequence of X st b1 is norm_summable
proof
reconsider C = NAT --> (0. X) as sequence of X ;
take C ; ::_thesis: C is norm_summable
for n being Element of NAT holds C . n = 0. X by FUNCOP_1:7;
hence C is norm_summable by Th13; ::_thesis: verum
end;
end;
theorem Th14: :: LOPBAN_3:14
for X being RealNormSpace
for s being sequence of X st s is summable holds
( s is convergent & lim s = 0. X )
proof
let X be RealNormSpace; ::_thesis: for s being sequence of X st s is summable holds
( s is convergent & lim s = 0. X )
let s be sequence of X; ::_thesis: ( s is summable implies ( s is convergent & lim s = 0. X ) )
assume s is summable ; ::_thesis: ( s is convergent & lim s = 0. X )
then A1: Partial_Sums s is convergent by Def1;
then A2: (Partial_Sums s) ^\ 1 is convergent by Th7;
lim ((Partial_Sums s) ^\ 1) = lim (Partial_Sums s) by A1, Th8;
then A3: lim (((Partial_Sums s) ^\ 1) - (Partial_Sums s)) = (lim (Partial_Sums s)) - (lim (Partial_Sums s)) by A1, A2, NORMSP_1:26
.= 0. X by RLVECT_1:15 ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(((Partial_Sums_s)_^\_1)_._n)_-_((Partial_Sums_s)_._n)_=_(s_^\_1)_._n
let n be Element of NAT ; ::_thesis: (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = (s ^\ 1) . n
(Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by BHSP_4:def_1;
then (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + ((s ^\ 1) . n) by NAT_1:def_3;
then ((Partial_Sums s) ^\ 1) . n = ((s ^\ 1) . n) + ((Partial_Sums s) . n) by NAT_1:def_3;
then (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = ((s ^\ 1) . n) + (((Partial_Sums s) . n) - ((Partial_Sums s) . n)) by RLVECT_1:def_3;
then (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = ((s ^\ 1) . n) + (0. X) by RLVECT_1:15;
hence (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = (s ^\ 1) . n by RLVECT_1:4; ::_thesis: verum
end;
then A4: s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s) by NORMSP_1:def_3;
then s ^\ 1 is convergent by A1, A2, NORMSP_1:20;
hence ( s is convergent & lim s = 0. X ) by A3, A4, Th10, Th11; ::_thesis: verum
end;
theorem Th15: :: LOPBAN_3:15
for X being RealNormSpace
for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)
proof
let X be RealNormSpace; ::_thesis: for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)
let s1, s2 be sequence of X; ::_thesis: (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2)
A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_s1)_+_(Partial_Sums_s2))_._(n_+_1)_=_(((Partial_Sums_s1)_+_(Partial_Sums_s2))_._n)_+_((s1_+_s2)_._(n_+_1))
let n be Element of NAT ; ::_thesis: ((Partial_Sums s1) + (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) + (Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1))
thus ((Partial_Sums s1) + (Partial_Sums s2)) . (n + 1) = ((Partial_Sums s1) . (n + 1)) + ((Partial_Sums s2) . (n + 1)) by NORMSP_1:def_2
.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) + ((Partial_Sums s2) . (n + 1)) by BHSP_4:def_1
.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) + ((s2 . (n + 1)) + ((Partial_Sums s2) . n)) by BHSP_4:def_1
.= ((((Partial_Sums s1) . n) + (s1 . (n + 1))) + (s2 . (n + 1))) + ((Partial_Sums s2) . n) by RLVECT_1:def_3
.= (((Partial_Sums s1) . n) + ((s1 . (n + 1)) + (s2 . (n + 1)))) + ((Partial_Sums s2) . n) by RLVECT_1:def_3
.= (((Partial_Sums s1) . n) + ((s1 + s2) . (n + 1))) + ((Partial_Sums s2) . n) by NORMSP_1:def_2
.= (((Partial_Sums s1) . n) + ((Partial_Sums s2) . n)) + ((s1 + s2) . (n + 1)) by RLVECT_1:def_3
.= (((Partial_Sums s1) + (Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1)) by NORMSP_1:def_2 ; ::_thesis: verum
end;
((Partial_Sums s1) + (Partial_Sums s2)) . 0 = ((Partial_Sums s1) . 0) + ((Partial_Sums s2) . 0) by NORMSP_1:def_2
.= (s1 . 0) + ((Partial_Sums s2) . 0) by BHSP_4:def_1
.= (s1 . 0) + (s2 . 0) by BHSP_4:def_1
.= (s1 + s2) . 0 by NORMSP_1:def_2 ;
hence (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) by A1, BHSP_4:def_1; ::_thesis: verum
end;
theorem Th16: :: LOPBAN_3:16
for X being RealNormSpace
for s1, s2 being sequence of X holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)
proof
let X be RealNormSpace; ::_thesis: for s1, s2 being sequence of X holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)
let s1, s2 be sequence of X; ::_thesis: (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2)
A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_s1)_-_(Partial_Sums_s2))_._(n_+_1)_=_(((Partial_Sums_s1)_-_(Partial_Sums_s2))_._n)_+_((s1_-_s2)_._(n_+_1))
let n be Element of NAT ; ::_thesis: ((Partial_Sums s1) - (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) - (Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1))
thus ((Partial_Sums s1) - (Partial_Sums s2)) . (n + 1) = ((Partial_Sums s1) . (n + 1)) - ((Partial_Sums s2) . (n + 1)) by NORMSP_1:def_3
.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) - ((Partial_Sums s2) . (n + 1)) by BHSP_4:def_1
.= (((Partial_Sums s1) . n) + (s1 . (n + 1))) - ((s2 . (n + 1)) + ((Partial_Sums s2) . n)) by BHSP_4:def_1
.= ((((Partial_Sums s1) . n) + (s1 . (n + 1))) - (s2 . (n + 1))) - ((Partial_Sums s2) . n) by RLVECT_1:27
.= (((Partial_Sums s1) . n) + ((s1 . (n + 1)) - (s2 . (n + 1)))) - ((Partial_Sums s2) . n) by RLVECT_1:def_3
.= (((s1 - s2) . (n + 1)) + ((Partial_Sums s1) . n)) - ((Partial_Sums s2) . n) by NORMSP_1:def_3
.= ((s1 - s2) . (n + 1)) + (((Partial_Sums s1) . n) - ((Partial_Sums s2) . n)) by RLVECT_1:def_3
.= (((Partial_Sums s1) - (Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1)) by NORMSP_1:def_3 ; ::_thesis: verum
end;
((Partial_Sums s1) - (Partial_Sums s2)) . 0 = ((Partial_Sums s1) . 0) - ((Partial_Sums s2) . 0) by NORMSP_1:def_3
.= (s1 . 0) - ((Partial_Sums s2) . 0) by BHSP_4:def_1
.= (s1 . 0) - (s2 . 0) by BHSP_4:def_1
.= (s1 - s2) . 0 by NORMSP_1:def_3 ;
hence (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) by A1, BHSP_4:def_1; ::_thesis: verum
end;
registration
let X be RealNormSpace;
let seq be norm_summable sequence of X;
cluster||.seq.|| -> summable for Real_Sequence;
coherence
for b1 being Real_Sequence st b1 = ||.seq.|| holds
b1 is summable by Def3;
end;
registration
let X be RealNormSpace;
cluster Function-like V30( NAT , the carrier of X) summable -> convergent for Element of K32(K33(NAT, the carrier of X));
coherence
for b1 being sequence of X st b1 is summable holds
b1 is convergent by Th14;
end;
theorem Th17: :: LOPBAN_3:17
for X being RealNormSpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
proof
let X be RealNormSpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is summable & seq2 is summable implies ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) )
assume ( seq1 is summable & seq2 is summable ) ; ::_thesis: ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) )
then A1: ( Partial_Sums seq1 is convergent & Partial_Sums seq2 is convergent ) by Def1;
then A2: (Partial_Sums seq1) + (Partial_Sums seq2) is convergent by NORMSP_1:19;
A3: (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by Th15;
Sum (seq1 + seq2) = lim ((Partial_Sums seq1) + (Partial_Sums seq2)) by Th15
.= (lim (Partial_Sums seq1)) + (lim (Partial_Sums seq2)) by A1, NORMSP_1:25 ;
hence ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) by A2, A3, Def1; ::_thesis: verum
end;
theorem Th18: :: LOPBAN_3:18
for X being RealNormSpace
for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
proof
let X be RealNormSpace; ::_thesis: for seq1, seq2 being sequence of X st seq1 is summable & seq2 is summable holds
( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 is summable & seq2 is summable implies ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) )
assume ( seq1 is summable & seq2 is summable ) ; ::_thesis: ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) )
then A1: ( Partial_Sums seq1 is convergent & Partial_Sums seq2 is convergent ) by Def1;
then A2: (Partial_Sums seq1) - (Partial_Sums seq2) is convergent by NORMSP_1:20;
A3: (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) by Th16;
Sum (seq1 - seq2) = lim ((Partial_Sums seq1) - (Partial_Sums seq2)) by Th16
.= (lim (Partial_Sums seq1)) - (lim (Partial_Sums seq2)) by A1, NORMSP_1:26 ;
hence ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) by A2, A3, Def1; ::_thesis: verum
end;
registration
let X be RealNormSpace;
let seq1, seq2 be summable sequence of X;
clusterseq1 + seq2 -> summable ;
coherence
seq1 + seq2 is summable by Th17;
clusterseq1 - seq2 -> summable ;
coherence
seq1 - seq2 is summable by Th18;
end;
theorem Th19: :: LOPBAN_3:19
for X being RealNormSpace
for seq being sequence of X
for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X
for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
let seq be sequence of X; ::_thesis: for z being Real holds Partial_Sums (z * seq) = z * (Partial_Sums seq)
let z be Real; ::_thesis: Partial_Sums (z * seq) = z * (Partial_Sums seq)
defpred S1[ Element of NAT ] means (Partial_Sums (z * seq)) . $1 = (z * (Partial_Sums seq)) . $1;
A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_
S1[n_+_1]
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
(Partial_Sums (z * seq)) . (n + 1) = ((Partial_Sums (z * seq)) . n) + ((z * seq) . (n + 1)) by BHSP_4:def_1
.= (z * ((Partial_Sums seq) . n)) + ((z * seq) . (n + 1)) by A2, NORMSP_1:def_5
.= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by NORMSP_1:def_5
.= z * (((Partial_Sums seq) . n) + (seq . (n + 1))) by RLVECT_1:def_5
.= z * ((Partial_Sums seq) . (n + 1)) by BHSP_4:def_1
.= (z * (Partial_Sums seq)) . (n + 1) by NORMSP_1:def_5 ;
hence S1[n + 1] ; ::_thesis: verum
end;
(Partial_Sums (z * seq)) . 0 = (z * seq) . 0 by BHSP_4:def_1
.= z * (seq . 0) by NORMSP_1:def_5
.= z * ((Partial_Sums seq) . 0) by BHSP_4:def_1
.= (z * (Partial_Sums seq)) . 0 by NORMSP_1:def_5 ;
then A3: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence Partial_Sums (z * seq) = z * (Partial_Sums seq) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th20: :: LOPBAN_3:20
for X being RealNormSpace
for seq being summable sequence of X
for z being Real holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
proof
let X be RealNormSpace; ::_thesis: for seq being summable sequence of X
for z being Real holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
let seq be summable sequence of X; ::_thesis: for z being Real holds
( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
let z be Real; ::_thesis: ( z * seq is summable & Sum (z * seq) = z * (Sum seq) )
A1: Partial_Sums (z * seq) = z * (Partial_Sums seq) by Th19;
A2: Partial_Sums seq is convergent by Def1;
then A3: z * (Partial_Sums seq) is convergent by NORMSP_1:22;
Sum (z * seq) = lim (z * (Partial_Sums seq)) by Th19
.= z * (Sum seq) by A2, NORMSP_1:28 ;
hence ( z * seq is summable & Sum (z * seq) = z * (Sum seq) ) by A3, A1, Def1; ::_thesis: verum
end;
registration
let X be RealNormSpace;
let z be Real;
let seq be summable sequence of X;
clusterz * seq -> summable ;
coherence
z * seq is summable by Th20;
end;
theorem Th21: :: LOPBAN_3:21
for X being RealNormSpace
for s, s1 being sequence of X st ( for n being Element of NAT holds s1 . n = s . 0 ) holds
Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1
proof
let X be RealNormSpace; ::_thesis: for s, s1 being sequence of X st ( for n being Element of NAT holds s1 . n = s . 0 ) holds
Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1
let s, s1 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds s1 . n = s . 0 ) implies Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 )
assume A1: for n being Element of NAT holds s1 . n = s . 0 ; ::_thesis: Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1
A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_(((Partial_Sums_s)_^\_1)_-_s1)_._(k_+_1)_=_((((Partial_Sums_s)_^\_1)_-_s1)_._k)_+_((s_^\_1)_._(k_+_1))
let k be Element of NAT ; ::_thesis: (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1))
thus (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = (((Partial_Sums s) ^\ 1) . (k + 1)) - (s1 . (k + 1)) by NORMSP_1:def_3
.= (((Partial_Sums s) ^\ 1) . (k + 1)) - (s . 0) by A1
.= ((Partial_Sums s) . ((k + 1) + 1)) - (s . 0) by NAT_1:def_3
.= ((s . ((k + 1) + 1)) + ((Partial_Sums s) . (k + 1))) - (s . 0) by BHSP_4:def_1
.= ((s . ((k + 1) + 1)) + ((Partial_Sums s) . (k + 1))) - (s1 . k) by A1
.= (s . ((k + 1) + 1)) + (((Partial_Sums s) . (k + 1)) - (s1 . k)) by RLVECT_1:def_3
.= (s . ((k + 1) + 1)) + ((((Partial_Sums s) ^\ 1) . k) - (s1 . k)) by NAT_1:def_3
.= (s . ((k + 1) + 1)) + ((((Partial_Sums s) ^\ 1) - s1) . k) by NORMSP_1:def_3
.= ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1)) by NAT_1:def_3 ; ::_thesis: verum
end;
(((Partial_Sums s) ^\ 1) - s1) . 0 = (((Partial_Sums s) ^\ 1) . 0) - (s1 . 0) by NORMSP_1:def_3
.= (((Partial_Sums s) ^\ 1) . 0) - (s . 0) by A1
.= ((Partial_Sums s) . (0 + 1)) - (s . 0) by NAT_1:def_3
.= (((Partial_Sums s) . 0) + (s . (0 + 1))) - (s . 0) by BHSP_4:def_1
.= ((s . (0 + 1)) + (s . 0)) - (s . 0) by BHSP_4:def_1
.= (s . (0 + 1)) + ((s . 0) - (s . 0)) by RLVECT_1:def_3
.= (s . (0 + 1)) + (0. X) by RLVECT_1:15
.= s . (0 + 1) by RLVECT_1:4
.= (s ^\ 1) . 0 by NAT_1:def_3 ;
hence Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 by A2, BHSP_4:def_1; ::_thesis: verum
end;
theorem Th22: :: LOPBAN_3:22
for X being RealNormSpace
for s being sequence of X st s is summable holds
for n being Element of NAT holds s ^\ n is summable
proof
let X be RealNormSpace; ::_thesis: for s being sequence of X st s is summable holds
for n being Element of NAT holds s ^\ n is summable
let s be sequence of X; ::_thesis: ( s is summable implies for n being Element of NAT holds s ^\ n is summable )
defpred S1[ Element of NAT ] means s ^\ $1 is summable ;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
reconsider s1 = NAT --> ((s ^\ n) . 0) as sequence of X ;
for k being Element of NAT holds s1 . k = (s ^\ n) . 0 by FUNCOP_1:7;
then A2: Partial_Sums ((s ^\ n) ^\ 1) = ((Partial_Sums (s ^\ n)) ^\ 1) - s1 by Th21;
assume s ^\ n is summable ; ::_thesis: S1[n + 1]
then Partial_Sums (s ^\ n) is convergent by Def1;
then A3: (Partial_Sums (s ^\ n)) ^\ 1 is convergent by Th7;
s1 is convergent by Th12;
then ( s ^\ (n + 1) = (s ^\ n) ^\ 1 & Partial_Sums ((s ^\ n) ^\ 1) is convergent ) by A3, A2, NAT_1:48, NORMSP_1:20;
hence S1[n + 1] by Def1; ::_thesis: verum
end;
assume s is summable ; ::_thesis: for n being Element of NAT holds s ^\ n is summable
then A4: S1[ 0 ] by NAT_1:47;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A1); ::_thesis: verum
end;
registration
let X be RealNormSpace;
let seq be summable sequence of X;
let n be Element of NAT ;
clusterseq ^\ n -> summable for sequence of X;
coherence
for b1 being sequence of X st b1 = seq ^\ n holds
b1 is summable by Th22;
end;
theorem Th23: :: LOPBAN_3:23
for X being RealNormSpace
for seq being sequence of X holds
( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable )
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X holds
( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable )
let seq be sequence of X; ::_thesis: ( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable )
for n being Element of NAT holds 0 <= ||.seq.|| . n by Th2;
then ( Partial_Sums ||.seq.|| is bounded_above iff ||.seq.|| is summable ) by SERIES_1:17;
hence ( Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable ) by Def3; ::_thesis: verum
end;
registration
let X be RealNormSpace;
let seq be norm_summable sequence of X;
cluster Partial_Sums ||.seq.|| -> bounded_above for Real_Sequence;
coherence
for b1 being Real_Sequence st b1 = Partial_Sums ||.seq.|| holds
b1 is bounded_above by Th23;
end;
theorem Th24: :: LOPBAN_3:24
for X being RealBanachSpace
for seq being sequence of X holds
( seq is summable iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p )
proof
let X be RealBanachSpace; ::_thesis: for seq being sequence of X holds
( seq is summable iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p )
let seq be sequence of X; ::_thesis: ( seq is summable iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p )
A1: now__::_thesis:_(_(_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).||_<_p_)_implies_seq_is_summable_)
assume for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p ; ::_thesis: seq is summable
then Partial_Sums seq is Cauchy_sequence_by_Norm by Th5;
then Partial_Sums seq is convergent by LOPBAN_1:def_15;
hence seq is summable by Def1; ::_thesis: verum
end;
now__::_thesis:_(_seq_is_summable_implies_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).||_<_p_)
assume seq is summable ; ::_thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p
then Partial_Sums seq is convergent by Def1;
hence for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p by Th4; ::_thesis: verum
end;
hence ( seq is summable iff for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p ) by A1; ::_thesis: verum
end;
theorem Th25: :: LOPBAN_3:25
for X being RealNormSpace
for s being sequence of X
for n, m being Element of NAT st n <= m holds
||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n))
proof
let X be RealNormSpace; ::_thesis: for s being sequence of X
for n, m being Element of NAT st n <= m holds
||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n))
let s be sequence of X; ::_thesis: for n, m being Element of NAT st n <= m holds
||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n))
set s1 = Partial_Sums s;
set s2 = Partial_Sums ||.s.||;
let n, m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)) )
assume n <= m ; ::_thesis: ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n))
then reconsider k = m - n as Element of NAT by INT_1:5;
defpred S1[ Element of NAT ] means ||.(((Partial_Sums s) . (n + $1)) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . (n + $1)) - ((Partial_Sums ||.s.||) . n));
A1: n + k = m ;
now__::_thesis:_for_k_being_Element_of_NAT_holds_||.s.||_._k_>=_0
let k be Element of NAT ; ::_thesis: ||.s.|| . k >= 0
||.(s . k).|| >= 0 ;
hence ||.s.|| . k >= 0 by NORMSP_0:def_4; ::_thesis: verum
end;
then A2: Partial_Sums ||.s.|| is non-decreasing by SERIES_1:16;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
A4: abs (((Partial_Sums ||.s.||) . (n + (k + 1))) - ((Partial_Sums ||.s.||) . n)) = abs ((((Partial_Sums ||.s.||) . (n + k)) + (||.s.|| . ((n + k) + 1))) - ((Partial_Sums ||.s.||) . n)) by SERIES_1:def_1
.= abs ((((Partial_Sums ||.s.||) . (n + k)) + ||.(s . ((n + k) + 1)).||) - ((Partial_Sums ||.s.||) . n)) by NORMSP_0:def_4
.= abs (||.(s . ((n + k) + 1)).|| + (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n))) ;
||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| = ||.(((s . ((n + k) + 1)) + ((Partial_Sums s) . (n + k))) - ((Partial_Sums s) . n)).|| by BHSP_4:def_1
.= ||.((s . ((n + k) + 1)) + (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))).|| by RLVECT_1:def_3 ;
then A5: ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + ||.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).|| by NORMSP_1:def_1;
(Partial_Sums ||.s.||) . (n + k) >= (Partial_Sums ||.s.||) . n by A2, SEQM_3:5;
then A6: ((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n) >= 0 by XREAL_1:48;
assume ||.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n)) ; ::_thesis: S1[k + 1]
then ||.(s . ((n + k) + 1)).|| + ||.(((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n))) by XREAL_1:7;
then ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + (abs (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n))) by A5, XXREAL_0:2;
then ||.(((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)).|| <= ||.(s . ((n + k) + 1)).|| + (((Partial_Sums ||.s.||) . (n + k)) - ((Partial_Sums ||.s.||) . n)) by A6, ABSVALUE:def_1;
hence S1[k + 1] by A4, ABSVALUE:def_1; ::_thesis: verum
end;
||.(((Partial_Sums s) . (n + 0)) - ((Partial_Sums s) . n)).|| = ||.(0. X).|| by RLVECT_1:15
.= 0 ;
then A7: S1[ 0 ] by COMPLEX1:46;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A7, A3);
hence ||.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).|| <= abs (((Partial_Sums ||.s.||) . m) - ((Partial_Sums ||.s.||) . n)) by A1; ::_thesis: verum
end;
theorem Th26: :: LOPBAN_3:26
for X being RealBanachSpace
for seq being sequence of X st seq is norm_summable holds
seq is summable
proof
let X be RealBanachSpace; ::_thesis: for seq being sequence of X st seq is norm_summable holds
seq is summable
let seq be sequence of X; ::_thesis: ( seq is norm_summable implies seq is summable )
assume seq is norm_summable ; ::_thesis: seq is summable
then A1: Partial_Sums ||.seq.|| is convergent by SERIES_1:def_2;
now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p )
assume 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) < p by A1, SEQ_4:41;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p )
assume A3: n <= m ; ::_thesis: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p
then A4: ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| <= abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) by Th25;
abs (((Partial_Sums ||.seq.||) . m) - ((Partial_Sums ||.seq.||) . n)) < p by A2, A3;
hence ||.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).|| < p by A4, XXREAL_0:2; ::_thesis: verum
end;
hence seq is summable by Th24; ::_thesis: verum
end;
theorem :: LOPBAN_3:27
for X being RealNormSpace
for rseq1 being Real_Sequence
for seq2 being sequence of X st rseq1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n holds
seq2 is norm_summable
proof
let X be RealNormSpace; ::_thesis: for rseq1 being Real_Sequence
for seq2 being sequence of X st rseq1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n holds
seq2 is norm_summable
let rseq1 be Real_Sequence; ::_thesis: for seq2 being sequence of X st rseq1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n holds
seq2 is norm_summable
let seq2 be sequence of X; ::_thesis: ( rseq1 is summable & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n implies seq2 is norm_summable )
assume that
A1: rseq1 is summable and
A2: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n ; ::_thesis: seq2 is norm_summable
consider m being Element of NAT such that
A3: for n being Element of NAT st m <= n holds
||.(seq2 . n).|| <= rseq1 . n by A2;
A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_||.seq2.||_._n
let n be Element of NAT ; ::_thesis: 0 <= ||.seq2.|| . n
||.(seq2 . n).|| = ||.seq2.|| . n by NORMSP_0:def_4;
hence 0 <= ||.seq2.|| . n ; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
||.seq2.||_._n_<=_rseq1_._n
let n be Element of NAT ; ::_thesis: ( m <= n implies ||.seq2.|| . n <= rseq1 . n )
assume m <= n ; ::_thesis: ||.seq2.|| . n <= rseq1 . n
then ||.(seq2 . n).|| <= rseq1 . n by A3;
hence ||.seq2.|| . n <= rseq1 . n by NORMSP_0:def_4; ::_thesis: verum
end;
hence ||.seq2.|| is summable by A1, A4, SERIES_1:19; :: according to LOPBAN_3:def_3 ::_thesis: verum
end;
theorem :: LOPBAN_3:28
for X being RealNormSpace
for seq1, seq2 being sequence of X st ( for n being Element of NAT holds
( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable holds
( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| )
proof
let X be RealNormSpace; ::_thesis: for seq1, seq2 being sequence of X st ( for n being Element of NAT holds
( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable holds
( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| )
let seq1, seq2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds
( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable implies ( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| ) )
assume ( ( for n being Element of NAT holds
( 0 <= ||.seq1.|| . n & ||.seq1.|| . n <= ||.seq2.|| . n ) ) & seq2 is norm_summable ) ; ::_thesis: ( seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2.|| )
hence ( ||.seq1.|| is summable & Sum ||.seq1.|| <= Sum ||.seq2.|| ) by SERIES_1:20; :: according to LOPBAN_3:def_3 ::_thesis: verum
end;
theorem :: LOPBAN_3:29
for X being RealNormSpace
for seq being sequence of X st ( for n being Element of NAT holds ||.seq.|| . n > 0 ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 holds
not seq is norm_summable by SERIES_1:27;
theorem :: LOPBAN_3:30
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable
let seq be sequence of X; ::_thesis: for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable
let rseq1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is norm_summable )
assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 ) ; ::_thesis: seq is norm_summable
for n being Element of NAT holds ||.seq.|| . n >= 0 by Th2;
hence ||.seq.|| is summable by A1, SERIES_1:28; :: according to LOPBAN_3:def_3 ::_thesis: verum
end;
theorem :: LOPBAN_3:31
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 holds
not ||.seq.|| is summable
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 holds
not ||.seq.|| is summable
let seq be sequence of X; ::_thesis: for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 holds
not ||.seq.|| is summable
let rseq1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 implies not ||.seq.|| is summable )
assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & ex m being Element of NAT st
for n being Element of NAT st m <= n holds
rseq1 . n >= 1 ) ; ::_thesis: not ||.seq.|| is summable
for n being Element of NAT holds ||.seq.|| . n >= 0 by Th2;
hence not ||.seq.|| is summable by A1, SERIES_1:29; ::_thesis: verum
end;
theorem :: LOPBAN_3:32
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds
not seq is norm_summable
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds
not seq is norm_summable
let seq be sequence of X; ::_thesis: for rseq1 being Real_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds
not seq is norm_summable
let rseq1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 implies not seq is norm_summable )
assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 > 1 ) ; ::_thesis: not seq is norm_summable
for n being Element of NAT holds ||.seq.|| . n >= 0 by Th2;
hence not ||.seq.|| is summable by A1, SERIES_1:30; :: according to LOPBAN_3:def_3 ::_thesis: verum
end;
theorem :: LOPBAN_3:33
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ||.seq.|| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) holds
( seq is norm_summable iff rseq1 is summable )
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X
for rseq1 being Real_Sequence st ||.seq.|| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) holds
( seq is norm_summable iff rseq1 is summable )
let seq be sequence of X; ::_thesis: for rseq1 being Real_Sequence st ||.seq.|| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) holds
( seq is norm_summable iff rseq1 is summable )
let rseq1 be Real_Sequence; ::_thesis: ( ||.seq.|| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) implies ( seq is norm_summable iff rseq1 is summable ) )
assume ( ||.seq.|| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) ) ; ::_thesis: ( seq is norm_summable iff rseq1 is summable )
then for n being Element of NAT holds
( ||.seq.|| is non-increasing & ||.seq.|| . n >= 0 & rseq1 . n = (2 to_power n) * (||.seq.|| . (2 to_power n)) ) by Th2;
then ( ||.seq.|| is summable iff rseq1 is summable ) by SERIES_1:31;
hence ( seq is norm_summable iff rseq1 is summable ) by Def3; ::_thesis: verum
end;
theorem :: LOPBAN_3:34
for X being RealNormSpace
for seq being sequence of X
for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
seq is norm_summable
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X
for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
seq is norm_summable
let seq be sequence of X; ::_thesis: for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
seq is norm_summable
let p be Real; ::_thesis: ( p > 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) implies seq is norm_summable )
assume ( p > 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) ) ; ::_thesis: seq is norm_summable
then ||.seq.|| is summable by SERIES_1:32;
hence seq is norm_summable by Def3; ::_thesis: verum
end;
theorem :: LOPBAN_3:35
for X being RealNormSpace
for seq being sequence of X
for p being Real st p <= 1 & ( for n being Element of NAT st n >= 1 holds
||.seq.|| . n = 1 / (n to_power p) ) holds
not seq is norm_summable by SERIES_1:33;
theorem :: LOPBAN_3:36
for X being RealNormSpace
for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds
( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds
( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable
let seq be sequence of X; ::_thesis: for rseq1 being Real_Sequence st ( for n being Element of NAT holds
( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable
let rseq1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds
( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is norm_summable )
assume that
A1: for n being Element of NAT holds
( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) and
A2: ( rseq1 is convergent & lim rseq1 < 1 ) ; ::_thesis: seq is norm_summable
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_||.seq.||_._n_<>_0_&_rseq1_._n_=_((abs_||.seq.||)_._(n_+_1))_/_((abs_||.seq.||)_._n)_)
let n be Element of NAT ; ::_thesis: ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) )
A3: 0 <= ||.seq.|| . n by Th2;
A4: 0 <= ||.seq.|| . (n + 1) by Th2;
A5: (abs ||.seq.||) . (n + 1) = abs (||.seq.|| . (n + 1)) by SEQ_1:12
.= ||.seq.|| . (n + 1) by A4, ABSVALUE:def_1 ;
A6: ( seq . n <> 0. X & ||.seq.|| . n = ||.(seq . n).|| ) by A1, NORMSP_0:def_4;
(abs ||.seq.||) . n = abs (||.seq.|| . n) by SEQ_1:12
.= ||.seq.|| . n by A3, ABSVALUE:def_1 ;
hence ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) ) by A1, A5, A6, NORMSP_0:def_5; ::_thesis: verum
end;
then ||.seq.|| is absolutely_summable by A2, SERIES_1:37;
then A7: abs ||.seq.|| is summable by SERIES_1:def_4;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_||.seq.||)_._n_=_||.seq.||_._n
let n be Element of NAT ; ::_thesis: (abs ||.seq.||) . n = ||.seq.|| . n
A8: 0 <= ||.seq.|| . n by Th2;
thus (abs ||.seq.||) . n = abs (||.seq.|| . n) by SEQ_1:12
.= ||.seq.|| . n by A8, ABSVALUE:def_1 ; ::_thesis: verum
end;
then abs ||.seq.|| = ||.seq.|| by FUNCT_2:63;
hence seq is norm_summable by A7, Def3; ::_thesis: verum
end;
theorem :: LOPBAN_3:37
for X being RealNormSpace
for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 holds
not seq is norm_summable
proof
let X be RealNormSpace; ::_thesis: for seq being sequence of X st ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 holds
not seq is norm_summable
let seq be sequence of X; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0. X ) & ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 implies not seq is norm_summable )
assume that
A1: for n being Element of NAT holds seq . n <> 0. X and
A2: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 ; ::_thesis: not seq is norm_summable
consider m being Element of NAT such that
A3: for n being Element of NAT st n >= m holds
(||.seq.|| . (n + 1)) / (||.seq.|| . n) >= 1 by A2;
A4: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
((abs_||.seq.||)_._(n_+_1))_/_((abs_||.seq.||)_._n)_>=_1
let n be Element of NAT ; ::_thesis: ( n >= m implies ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 )
assume A5: n >= m ; ::_thesis: ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1
A6: 0 <= ||.seq.|| . n by Th2;
A7: 0 <= ||.seq.|| . (n + 1) by Th2;
A8: (abs ||.seq.||) . (n + 1) = abs (||.seq.|| . (n + 1)) by SEQ_1:12
.= ||.seq.|| . (n + 1) by A7, ABSVALUE:def_1 ;
(abs ||.seq.||) . n = abs (||.seq.|| . n) by SEQ_1:12
.= ||.seq.|| . n by A6, ABSVALUE:def_1 ;
hence ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) >= 1 by A3, A5, A8; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.seq.||_._n_<>_0
let n be Element of NAT ; ::_thesis: ||.seq.|| . n <> 0
seq . n <> 0. X by A1;
then ||.(seq . n).|| <> 0 by NORMSP_0:def_5;
hence ||.seq.|| . n <> 0 by NORMSP_0:def_4; ::_thesis: verum
end;
hence not ||.seq.|| is summable by A4, SERIES_1:39; :: according to LOPBAN_3:def_3 ::_thesis: verum
end;
registration
let X be RealBanachSpace;
cluster Function-like V30( NAT , the carrier of X) norm_summable -> summable for Element of K32(K33(NAT, the carrier of X));
coherence
for b1 being sequence of X st b1 is norm_summable holds
b1 is summable by Th26;
end;
begin
theorem Th38: :: LOPBAN_3:38
for X being Banach_Algebra
for x, y, z being Element of X
for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
proof
let X be Banach_Algebra; ::_thesis: for x, y, z being Element of X
for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
let x, y, z be Element of X; ::_thesis: for a, b being Real holds
( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
let a, b be Real; ::_thesis: ( x + y = y + x & (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus x + y = y + x ; ::_thesis: ( (x + y) + z = x + (y + z) & x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus (x + y) + z = x + (y + z) by RLVECT_1:def_3; ::_thesis: ( x + (0. X) = x & ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus x + (0. X) = x by RLVECT_1:def_4; ::_thesis: ( ex t being Element of X st x + t = 0. X & (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus ex t being Element of X st x + t = 0. X by ALGSTR_0:def_11; ::_thesis: ( (x * y) * z = x * (y * z) & 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus (x * y) * z = x * (y * z) by GROUP_1:def_3; ::_thesis: ( 1 * x = x & 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus 1 * x = x by RLVECT_1:def_8; ::_thesis: ( 0 * x = 0. X & a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus 0 * x = 0. X by RLVECT_1:10; ::_thesis: ( a * (0. X) = 0. X & (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus a * (0. X) = 0. X by RLVECT_1:10; ::_thesis: ( (- 1) * x = - x & x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus (- 1) * x = - x by RLVECT_1:16; ::_thesis: ( x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) & (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus ( x * (1. X) = x & (1. X) * x = x & x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) & a * (x * y) = (a * x) * y & a * (x + y) = (a * x) + (a * y) & (a + b) * x = (a * x) + (b * x) & (a * b) * x = a * (b * x) ) by FUNCSDOM:def_9, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, VECTSP_1:def_2, VECTSP_1:def_3, VECTSP_1:def_4, VECTSP_1:def_8; ::_thesis: ( (a * b) * (x * y) = (a * x) * (b * y) & a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus (a * b) * (x * y) = a * (b * (x * y)) by RLVECT_1:def_7
.= a * (x * (b * y)) by LOPBAN_2:def_11
.= (a * x) * (b * y) by FUNCSDOM:def_9 ; ::_thesis: ( a * (x * y) = x * (a * y) & (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus a * (x * y) = x * (a * y) by LOPBAN_2:def_11; ::_thesis: ( (0. X) * x = 0. X & x * (0. X) = 0. X & x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
A1: (x * (y - z)) + (x * z) = x * ((y - z) + z) by VECTSP_1:def_2
.= x * (y - (z - z)) by RLVECT_1:29
.= x * (y - (0. X)) by RLVECT_1:15
.= x * y by RLVECT_1:13 ;
x * (0. X) = x * ((0. X) + (0. X)) by RLVECT_1:def_4
.= (x * (0. X)) + (x * (0. X)) by VECTSP_1:def_2 ;
then 0. X = ((x * (0. X)) + (x * (0. X))) - (x * (0. X)) by RLVECT_1:15;
then 0. X = (x * (0. X)) + ((x * (0. X)) - (x * (0. X))) by RLVECT_1:def_3;
then A2: 0. X = (x * (0. X)) + (0. X) by RLVECT_1:15;
(0. X) * x = ((0. X) + (0. X)) * x by RLVECT_1:def_4
.= ((0. X) * x) + ((0. X) * x) by VECTSP_1:def_3 ;
then 0. X = (((0. X) * x) + ((0. X) * x)) - ((0. X) * x) by RLVECT_1:15;
then 0. X = ((0. X) * x) + (((0. X) * x) - ((0. X) * x)) by RLVECT_1:def_3;
then 0. X = ((0. X) * x) + (0. X) by RLVECT_1:15;
hence ( (0. X) * x = 0. X & x * (0. X) = 0. X ) by A2, RLVECT_1:def_4; ::_thesis: ( x * (y - z) = (x * y) - (x * z) & (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus x * (y - z) = (x * (y - z)) + (0. X) by RLVECT_1:4
.= (x * (y - z)) + ((x * z) - (x * z)) by RLVECT_1:15
.= (x * y) - (x * z) by A1, RLVECT_1:def_3 ; ::_thesis: ( (y - z) * x = (y * x) - (z * x) & (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
A3: ((y - z) * x) + (z * x) = ((y - z) + z) * x by VECTSP_1:def_3
.= (y - (z - z)) * x by RLVECT_1:29
.= (y - (0. X)) * x by RLVECT_1:15
.= y * x by RLVECT_1:13 ;
thus (y - z) * x = ((y - z) * x) + (0. X) by RLVECT_1:4
.= ((y - z) * x) + ((z * x) - (z * x)) by RLVECT_1:15
.= (y * x) - (z * x) by A3, RLVECT_1:def_3 ; ::_thesis: ( (x + y) - z = x + (y - z) & (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus (x + y) - z = x + (y - z) by RLVECT_1:def_3; ::_thesis: ( (x - y) + z = x - (y - z) & (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus (x - y) + z = x - (y - z) by RLVECT_1:29; ::_thesis: ( (x - y) - z = x - (y + z) & x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus (x - y) - z = x - (y + z) by RLVECT_1:27; ::_thesis: ( x + y = (x - z) + (z + y) & x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus (x - z) + (z + y) = ((x - z) + z) + y by RLVECT_1:def_3
.= (x - (z - z)) + y by RLVECT_1:29
.= (x - (0. X)) + y by RLVECT_1:15
.= x + y by RLVECT_1:13 ; ::_thesis: ( x - y = (x - z) + (z - y) & x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus (x - z) + (z - y) = ((x - z) + z) - y by RLVECT_1:def_3
.= (x - (z - z)) - y by RLVECT_1:29
.= (x - (0. X)) - y by RLVECT_1:15
.= x - y by RLVECT_1:13 ; ::_thesis: ( x = (x - y) + y & x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus (x - y) + y = x - (y - y) by RLVECT_1:29
.= x - (0. X) by RLVECT_1:15
.= x by RLVECT_1:13 ; ::_thesis: ( x = y - (y - x) & ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus y - (y - x) = (y - y) + x by RLVECT_1:29
.= (0. X) + x by RLVECT_1:15
.= x by RLVECT_1:4 ; ::_thesis: ( ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| & ||.(1. X).|| = 1 & X is complete )
thus ( ( ||.x.|| = 0 implies x = 0. X ) & ( x = 0. X implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(x * y).|| <= ||.x.|| * ||.y.|| ) by LOPBAN_2:def_9, NORMSP_0:def_5, NORMSP_1:def_1; ::_thesis: ( ||.(1. X).|| = 1 & X is complete )
thus ( ||.(1. X).|| = 1 & X is complete ) by LOPBAN_2:def_10; ::_thesis: verum
end;
registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V133() V134() RealNormSpace-like V150() associative right-distributive right_unital Banach_Algebra-like -> well-unital for Normed_AlgebraStr ;
coherence
for b1 being Banach_Algebra holds b1 is well-unital
proof
let X be Banach_Algebra; ::_thesis: X is well-unital
let x be Element of X; :: according to VECTSP_1:def_6 ::_thesis: ( x * (1. X) = x & (1. X) * x = x )
thus ( x * (1. X) = x & (1. X) * x = x ) by Th38; ::_thesis: verum
end;
end;
definition
let X be non empty associative well-unital multLoopStr ;
let v be Element of X;
redefine attr v is invertible means :Def4: :: LOPBAN_3:def 4
ex w being Element of X st
( v * w = 1. X & w * v = 1. X );
compatibility
( v is invertible iff ex w being Element of X st
( v * w = 1. X & w * v = 1. X ) )
proof
thus ( v is invertible implies ex w being Element of X st
( v * w = 1. X & w * v = 1. X ) ) ::_thesis: ( ex w being Element of X st
( v * w = 1. X & w * v = 1. X ) implies v is invertible )
proof
assume A1: v is invertible ; ::_thesis: ex w being Element of X st
( v * w = 1. X & w * v = 1. X )
then consider y being Element of X such that
A2: v * y = 1. X by ALGSTR_0:def_28;
take y ; ::_thesis: ( v * y = 1. X & y * v = 1. X )
thus v * y = 1. X by A2; ::_thesis: y * v = 1. X
consider x being Element of X such that
A3: x * v = 1. X by A1, ALGSTR_0:def_27;
x = x * (1. X) by VECTSP_1:def_6
.= (1. X) * y by A2, A3, GROUP_1:def_3
.= y by VECTSP_1:def_6 ;
hence y * v = 1. X by A3; ::_thesis: verum
end;
given w being Element of X such that A4: ( v * w = 1. X & w * v = 1. X ) ; ::_thesis: v is invertible
thus ( v is right_invertible & v is left_invertible ) by A4, ALGSTR_0:def_27, ALGSTR_0:def_28; :: according to ALGSTR_0:def_29 ::_thesis: verum
end;
end;
:: deftheorem Def4 defines invertible LOPBAN_3:def_4_:_
for X being non empty associative well-unital multLoopStr
for v being Element of X holds
( v is invertible iff ex w being Element of X st
( v * w = 1. X & w * v = 1. X ) );
definition
let X be non empty Normed_AlgebraStr ;
let S be sequence of X;
let a be Element of X;
funca * S -> sequence of X means :: LOPBAN_3:def 5
for n being Element of NAT holds it . n = a * (S . n);
existence
ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = a * (S . n)
proof
deffunc H1( Element of NAT ) -> Element of the carrier of X = a * (S . $1);
ex S being sequence of X st
for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_4();
hence ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = a * (S . n) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = a * (S . n) ) & ( for n being Element of NAT holds b2 . n = a * (S . n) ) holds
b1 = b2
proof
let S1, S2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds S1 . n = a * (S . n) ) & ( for n being Element of NAT holds S2 . n = a * (S . n) ) implies S1 = S2 )
assume that
A1: for n being Element of NAT holds S1 . n = a * (S . n) and
A2: for n being Element of NAT holds S2 . n = a * (S . n) ; ::_thesis: S1 = S2
for n being Element of NAT holds S1 . n = S2 . n
proof
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
S1 . n = a * (S . n) by A1;
hence S1 . n = S2 . n by A2; ::_thesis: verum
end;
hence S1 = S2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem defines * LOPBAN_3:def_5_:_
for X being non empty Normed_AlgebraStr
for S being sequence of X
for a being Element of X
for b4 being sequence of X holds
( b4 = a * S iff for n being Element of NAT holds b4 . n = a * (S . n) );
definition
let X be non empty Normed_AlgebraStr ;
let S be sequence of X;
let a be Element of X;
funcS * a -> sequence of X means :: LOPBAN_3:def 6
for n being Element of NAT holds it . n = (S . n) * a;
existence
ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (S . n) * a
proof
deffunc H1( Element of NAT ) -> Element of the carrier of X = (S . $1) * a;
ex S being sequence of X st
for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_4();
hence ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (S . n) * a ; ::_thesis: verum
end;
uniqueness
for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (S . n) * a ) & ( for n being Element of NAT holds b2 . n = (S . n) * a ) holds
b1 = b2
proof
let S1, S2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (S . n) * a ) & ( for n being Element of NAT holds S2 . n = (S . n) * a ) implies S1 = S2 )
assume that
A1: for n being Element of NAT holds S1 . n = (S . n) * a and
A2: for n being Element of NAT holds S2 . n = (S . n) * a ; ::_thesis: S1 = S2
for n being Element of NAT holds S1 . n = S2 . n
proof
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
S1 . n = (S . n) * a by A1;
hence S1 . n = S2 . n by A2; ::_thesis: verum
end;
hence S1 = S2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem defines * LOPBAN_3:def_6_:_
for X being non empty Normed_AlgebraStr
for S being sequence of X
for a being Element of X
for b4 being sequence of X holds
( b4 = S * a iff for n being Element of NAT holds b4 . n = (S . n) * a );
definition
let X be non empty Normed_AlgebraStr ;
let seq1, seq2 be sequence of X;
funcseq1 * seq2 -> sequence of X means :: LOPBAN_3:def 7
for n being Element of NAT holds it . n = (seq1 . n) * (seq2 . n);
existence
ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (seq1 . n) * (seq2 . n)
proof
deffunc H1( Element of NAT ) -> Element of the carrier of X = (seq1 . $1) * (seq2 . $1);
ex S being sequence of X st
for n being Element of NAT holds S . n = H1(n) from FUNCT_2:sch_4();
hence ex b1 being sequence of X st
for n being Element of NAT holds b1 . n = (seq1 . n) * (seq2 . n) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being sequence of X st ( for n being Element of NAT holds b1 . n = (seq1 . n) * (seq2 . n) ) & ( for n being Element of NAT holds b2 . n = (seq1 . n) * (seq2 . n) ) holds
b1 = b2
proof
let S1, S2 be sequence of X; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (seq1 . n) * (seq2 . n) ) & ( for n being Element of NAT holds S2 . n = (seq1 . n) * (seq2 . n) ) implies S1 = S2 )
assume that
A1: for n being Element of NAT holds S1 . n = (seq1 . n) * (seq2 . n) and
A2: for n being Element of NAT holds S2 . n = (seq1 . n) * (seq2 . n) ; ::_thesis: S1 = S2
for n being Element of NAT holds S1 . n = S2 . n
proof
let n be Element of NAT ; ::_thesis: S1 . n = S2 . n
S1 . n = (seq1 . n) * (seq2 . n) by A1;
hence S1 . n = S2 . n by A2; ::_thesis: verum
end;
hence S1 = S2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem defines * LOPBAN_3:def_7_:_
for X being non empty Normed_AlgebraStr
for seq1, seq2, b4 being sequence of X holds
( b4 = seq1 * seq2 iff for n being Element of NAT holds b4 . n = (seq1 . n) * (seq2 . n) );
notation
let X be non empty associative well-unital multLoopStr ;
let x be Element of X;
synonym x " for / x;
end;
definition
let X be non empty associative well-unital multLoopStr ;
let x be Element of X;
assume B1: x is invertible ;
redefine func / x means :Def8: :: LOPBAN_3:def 8
( x * it = 1. X & it * x = 1. X );
compatibility
for b1 being Element of the carrier of X holds
( b1 = x " iff ( x * b1 = 1. X & b1 * x = 1. X ) )
proof
let y be Element of X; ::_thesis: ( y = x " iff ( x * y = 1. X & y * x = 1. X ) )
consider x1 being Element of X such that
A1: x * x1 = 1. X by B1, ALGSTR_0:def_28;
A2: x is right_mult-cancelable
proof
let y, z be Element of X; :: according to ALGSTR_0:def_21 ::_thesis: ( not y * x = z * x or y = z )
assume A3: y * x = z * x ; ::_thesis: y = z
thus y = y * (1. X) by VECTSP_1:def_6
.= (z * x) * x1 by A1, A3, GROUP_1:def_3
.= z * (1. X) by A1, GROUP_1:def_3
.= z by VECTSP_1:def_6 ; ::_thesis: verum
end;
thus ( y = x " implies ( x * y = 1. X & y * x = 1. X ) ) ::_thesis: ( x * y = 1. X & y * x = 1. X implies y = x " )
proof
assume A4: y = x " ; ::_thesis: ( x * y = 1. X & y * x = 1. X )
y = y * (1. X) by VECTSP_1:def_6
.= (y * x) * x1 by A1, GROUP_1:def_3
.= (1. X) * x1 by B1, A2, A4, ALGSTR_0:def_30
.= x1 by VECTSP_1:def_6 ;
hence x * y = 1. X by A1; ::_thesis: y * x = 1. X
thus y * x = 1. X by B1, A2, A4, ALGSTR_0:def_30; ::_thesis: verum
end;
thus ( x * y = 1. X & y * x = 1. X implies y = x " ) by B1, A2, ALGSTR_0:def_30; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines " LOPBAN_3:def_8_:_
for X being non empty associative well-unital multLoopStr
for x being Element of X st x is invertible holds
for b3 being Element of the carrier of X holds
( b3 = x " iff ( x * b3 = 1. X & b3 * x = 1. X ) );
definition
let X be Banach_Algebra;
let z be Element of X;
funcz GeoSeq -> sequence of X means :Def9: :: LOPBAN_3:def 9
( it . 0 = 1. X & ( for n being Element of NAT holds it . (n + 1) = (it . n) * z ) );
existence
ex b1 being sequence of X st
( b1 . 0 = 1. X & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) )
proof
deffunc H1( set , set ) -> set = the multF of X . [$2,z];
consider g being Function such that
A1: ( dom g = NAT & g . 0 = 1. X & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) ) from NAT_1:sch_11();
defpred S1[ Element of NAT ] means g . $1 in the carrier of X;
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
then reconsider gk = g . k as Element of X ;
g . (k + 1) = the multF of X . [gk,z] by A1;
hence S1[k + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] by A1;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2);
then for n being set st n in NAT holds
g . n in the carrier of X ;
then reconsider g0 = g as sequence of X by A1, FUNCT_2:3;
take g0 ; ::_thesis: ( g0 . 0 = 1. X & ( for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * z ) )
thus ( g0 . 0 = 1. X & ( for n being Element of NAT holds g0 . (n + 1) = (g0 . n) * z ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being sequence of X st b1 . 0 = 1. X & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) & b2 . 0 = 1. X & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * z ) holds
b1 = b2
proof
let seq1, seq2 be sequence of X; ::_thesis: ( seq1 . 0 = 1. X & ( for n being Element of NAT holds seq1 . (n + 1) = (seq1 . n) * z ) & seq2 . 0 = 1. X & ( for n being Element of NAT holds seq2 . (n + 1) = (seq2 . n) * z ) implies seq1 = seq2 )
assume that
A4: seq1 . 0 = 1. X and
A5: for n being Element of NAT holds seq1 . (n + 1) = (seq1 . n) * z and
A6: seq2 . 0 = 1. X and
A7: for n being Element of NAT holds seq2 . (n + 1) = (seq2 . n) * z ; ::_thesis: seq1 = seq2
defpred S1[ Element of NAT ] means seq1 . $1 = seq2 . $1;
A8: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
hence seq1 . (k + 1) = (seq2 . k) * z by A5
.= seq2 . (k + 1) by A7 ;
::_thesis: verum
end;
A9: S1[ 0 ] by A4, A6;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A8);
hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines GeoSeq LOPBAN_3:def_9_:_
for X being Banach_Algebra
for z being Element of X
for b3 being sequence of X holds
( b3 = z GeoSeq iff ( b3 . 0 = 1. X & ( for n being Element of NAT holds b3 . (n + 1) = (b3 . n) * z ) ) );
definition
let X be Banach_Algebra;
let z be Element of X;
let n be Element of NAT ;
funcz #N n -> Element of X equals :: LOPBAN_3:def 10
(z GeoSeq) . n;
correctness
coherence
(z GeoSeq) . n is Element of X;
;
end;
:: deftheorem defines #N LOPBAN_3:def_10_:_
for X being Banach_Algebra
for z being Element of X
for n being Element of NAT holds z #N n = (z GeoSeq) . n;
theorem :: LOPBAN_3:39
for X being Banach_Algebra
for z being Element of X holds z #N 0 = 1. X by Def9;
theorem Th40: :: LOPBAN_3:40
for X being Banach_Algebra
for z being Element of X st ||.z.|| < 1 holds
( z GeoSeq is summable & z GeoSeq is norm_summable )
proof
let X be Banach_Algebra; ::_thesis: for z being Element of X st ||.z.|| < 1 holds
( z GeoSeq is summable & z GeoSeq is norm_summable )
let z be Element of X; ::_thesis: ( ||.z.|| < 1 implies ( z GeoSeq is summable & z GeoSeq is norm_summable ) )
A1: for n being Element of NAT holds
( 0 <= ||.(z GeoSeq).|| . n & ||.(z GeoSeq).|| . n <= (||.z.|| GeoSeq) . n )
proof
defpred S1[ Element of NAT ] means ( 0 <= ||.(z GeoSeq).|| . $1 & ||.(z GeoSeq).|| . $1 <= (||.z.|| GeoSeq) . $1 );
A2: ||.(z GeoSeq).|| . 0 = ||.((z GeoSeq) . 0).|| by NORMSP_0:def_4;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
||.(((z GeoSeq) . k) * z).|| <= ||.((z GeoSeq) . k).|| * ||.z.|| by LOPBAN_2:def_9;
then A4: ||.(((z GeoSeq) . k) * z).|| <= (||.(z GeoSeq).|| . k) * ||.z.|| by NORMSP_0:def_4;
assume S1[k] ; ::_thesis: S1[k + 1]
then (||.(z GeoSeq).|| . k) * ||.z.|| <= ((||.z.|| GeoSeq) . k) * ||.z.|| by XREAL_1:64;
then A5: ||.(((z GeoSeq) . k) * z).|| <= ((||.z.|| GeoSeq) . k) * ||.z.|| by A4, XXREAL_0:2;
||.(z GeoSeq).|| . (k + 1) = ||.((z GeoSeq) . (k + 1)).|| by NORMSP_0:def_4
.= ||.(((z GeoSeq) . k) * z).|| by Def9 ;
hence S1[k + 1] by A5, PREPOWER:3; ::_thesis: verum
end;
||.((z GeoSeq) . 0).|| = ||.(1. X).|| by Def9
.= 1 by LOPBAN_2:def_10
.= (||.z.|| GeoSeq) . 0 by PREPOWER:3 ;
then A6: S1[ 0 ] by A2;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A3);
hence for n being Element of NAT holds
( 0 <= ||.(z GeoSeq).|| . n & ||.(z GeoSeq).|| . n <= (||.z.|| GeoSeq) . n ) ; ::_thesis: verum
end;
assume ||.z.|| < 1 ; ::_thesis: ( z GeoSeq is summable & z GeoSeq is norm_summable )
then abs ||.z.|| < 1 by ABSVALUE:def_1;
then ||.z.|| GeoSeq is summable by SERIES_1:24;
then ||.(z GeoSeq).|| is summable by A1, SERIES_1:20;
then z GeoSeq is norm_summable by Def3;
hence ( z GeoSeq is summable & z GeoSeq is norm_summable ) ; ::_thesis: verum
end;
theorem :: LOPBAN_3:41
for X being Banach_Algebra
for x being Point of X st ||.((1. X) - x).|| < 1 holds
( ((1. X) - x) GeoSeq is summable & ((1. X) - x) GeoSeq is norm_summable ) by Th40;
Lm1: 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
let X be RealNormSpace; ::_thesis: for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
let x be Point of X; ::_thesis: ( ( for e being Real st e > 0 holds
||.x.|| < e ) implies x = 0. X )
assume A1: for e being Real st e > 0 holds
||.x.|| < e ; ::_thesis: x = 0. X
now__::_thesis:_not_x_<>_0._X
assume x <> 0. X ; ::_thesis: contradiction
then 0 <> ||.x.|| by NORMSP_0:def_5;
then 0 < ||.x.|| ;
hence contradiction by A1; ::_thesis: verum
end;
hence x = 0. X ; ::_thesis: verum
end;
Lm2: 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
let X be RealNormSpace; ::_thesis: for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
let x, y be Point of X; ::_thesis: ( ( for e being Real st e > 0 holds
||.(x - y).|| < e ) implies x = y )
assume for e being Real st e > 0 holds
||.(x - y).|| < e ; ::_thesis: x = y
then x - y = 0. X by Lm1;
hence x = y by RLVECT_1:21; ::_thesis: verum
end;
Lm3: for X being RealNormSpace
for x, y being Point of X
for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) holds
x = y
proof
let X be RealNormSpace; ::_thesis: for x, y being Point of X
for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) holds
x = y
let x, y be Point of X; ::_thesis: for seq being Real_Sequence st seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) holds
x = y
let seq be Real_Sequence; ::_thesis: ( seq is convergent & lim seq = 0 & ( for n being Element of NAT holds ||.(x - y).|| <= seq . n ) implies x = y )
assume that
A1: ( seq is convergent & lim seq = 0 ) and
A2: for n being Element of NAT holds ||.(x - y).|| <= seq . n ; ::_thesis: x = y
now__::_thesis:_for_e_being_Real_st_0_<_e_holds_
||.(x_-_y).||_<_e
let e be Real; ::_thesis: ( 0 < e implies ||.(x - y).|| < e )
assume 0 < e ; ::_thesis: ||.(x - y).|| < e
then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < e by A1, SEQ_2:def_7;
A4: seq . n <= abs (seq . n) by ABSVALUE:4;
A5: ||.(x - y).|| <= seq . n by A2;
abs ((seq . n) - 0) < e by A3;
then seq . n < e by A4, XXREAL_0:2;
hence ||.(x - y).|| < e by A5, XXREAL_0:2; ::_thesis: verum
end;
hence x = y by Lm2; ::_thesis: verum
end;
theorem :: LOPBAN_3:42
for X being Banach_Algebra
for x being Point of X st ||.((1. X) - x).|| < 1 holds
( x is invertible & x " = Sum (((1. X) - x) GeoSeq) )
proof
let X be Banach_Algebra; ::_thesis: for x being Point of X st ||.((1. X) - x).|| < 1 holds
( x is invertible & x " = Sum (((1. X) - x) GeoSeq) )
let x be Point of X; ::_thesis: ( ||.((1. X) - x).|| < 1 implies ( x is invertible & x " = Sum (((1. X) - x) GeoSeq) ) )
assume A1: ||.((1. X) - x).|| < 1 ; ::_thesis: ( x is invertible & x " = Sum (((1. X) - x) GeoSeq) )
set seq = ((1. X) - x) GeoSeq ;
A2: ((1. X) - x) GeoSeq is summable by A1, Th40;
then A3: ||.((((1. X) - x) GeoSeq) ^\ 1).|| is convergent by LOPBAN_1:41;
reconsider y = Sum (((1. X) - x) GeoSeq) as Element of X ;
A4: Partial_Sums (((1. X) - x) GeoSeq) is convergent by A2, Def1;
then lim ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| = 0 by NORMSP_1:24;
then A5: lim (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) = ||.x.|| * 0 by A4, NORMSP_1:24, SEQ_2:8
.= 0 ;
lim ((((1. X) - x) GeoSeq) ^\ 1) = 0. X by A2, Th14;
then A6: lim ||.((((1. X) - x) GeoSeq) ^\ 1).|| = ||.(0. X).|| by A2, LOPBAN_1:41;
A7: ||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| is convergent by A4, NORMSP_1:24, SEQ_2:7;
then A8: ||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) is convergent by A3, SEQ_2:5;
A9: lim (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) = (lim ||.((((1. X) - x) GeoSeq) ^\ 1).||) + (lim (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) by A7, A3, SEQ_2:6
.= 0 by A5, A6 ;
A10: for n being Element of NAT holds ((1. X) - x) * ((((1. X) - x) GeoSeq) . n) = (((1. X) - x) GeoSeq) . (n + 1)
proof
defpred S1[ Element of NAT ] means ((1. X) - x) * ((((1. X) - x) GeoSeq) . $1) = (((1. X) - x) GeoSeq) . ($1 + 1);
A11: ((1. X) - x) * ((((1. X) - x) GeoSeq) . 0) = ((1. X) - x) * (1. X) by Def9
.= (1. X) - x by Th38 ;
A12: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A13: S1[k] ; ::_thesis: S1[k + 1]
thus ((1. X) - x) * ((((1. X) - x) GeoSeq) . (k + 1)) = ((1. X) - x) * (((((1. X) - x) GeoSeq) . k) * ((1. X) - x)) by Def9
.= (((1. X) - x) * ((((1. X) - x) GeoSeq) . k)) * ((1. X) - x) by Th38
.= (((1. X) - x) GeoSeq) . ((k + 1) + 1) by A13, Def9 ; ::_thesis: verum
end;
(((1. X) - x) GeoSeq) . (0 + 1) = ((((1. X) - x) GeoSeq) . 0) * ((1. X) - x) by Def9
.= (1. X) * ((1. X) - x) by Def9
.= (1. X) - x by Th38 ;
then A14: S1[ 0 ] by A11;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A14, A12);
hence for n being Element of NAT holds ((1. X) - x) * ((((1. X) - x) GeoSeq) . n) = (((1. X) - x) GeoSeq) . (n + 1) ; ::_thesis: verum
end;
A15: for n being Element of NAT holds ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . n) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)
proof
defpred S1[ Element of NAT ] means ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . $1) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . $1) - ((((1. X) - x) GeoSeq) . 0);
A16: ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . 0) = ((1. X) - x) * ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1
.= ((1. X) - x) * (1. X) by Def9
.= (1. X) - x by Th38 ;
A17: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A18: S1[k] ; ::_thesis: S1[k + 1]
A19: (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . (k + 1)) - ((((1. X) - x) GeoSeq) . 0) = ((Partial_Sums (((1. X) - x) GeoSeq)) . ((k + 1) + 1)) - ((((1. X) - x) GeoSeq) . 0) by NAT_1:def_3
.= (((Partial_Sums (((1. X) - x) GeoSeq)) . (k + 1)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1))) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1
.= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1))) + (- ((((1. X) - x) GeoSeq) . 0)) by NAT_1:def_3
.= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) - ((((1. X) - x) GeoSeq) . 0)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1)) by RLVECT_1:def_3 ;
((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . (k + 1)) = ((1. X) - x) * (((Partial_Sums (((1. X) - x) GeoSeq)) . k) + ((((1. X) - x) GeoSeq) . (k + 1))) by BHSP_4:def_1
.= (((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . k)) + (((1. X) - x) * ((((1. X) - x) GeoSeq) . (k + 1))) by Th38
.= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) - ((((1. X) - x) GeoSeq) . 0)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1)) by A10, A18 ;
hence S1[k + 1] by A19; ::_thesis: verum
end;
(((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . 0) - ((((1. X) - x) GeoSeq) . 0) = ((Partial_Sums (((1. X) - x) GeoSeq)) . (0 + 1)) - ((((1. X) - x) GeoSeq) . 0) by NAT_1:def_3
.= (((Partial_Sums (((1. X) - x) GeoSeq)) . 0) + ((((1. X) - x) GeoSeq) . 1)) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1
.= (((((1. X) - x) GeoSeq) . 0) + ((((1. X) - x) GeoSeq) . 1)) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1
.= ((((1. X) - x) GeoSeq) . 1) + (((((1. X) - x) GeoSeq) . 0) - ((((1. X) - x) GeoSeq) . 0)) by Th38
.= ((((1. X) - x) GeoSeq) . 1) + (0. X) by RLVECT_1:15
.= (((1. X) - x) GeoSeq) . (0 + 1) by RLVECT_1:4
.= ((((1. X) - x) GeoSeq) . 0) * ((1. X) - x) by Def9
.= (1. X) * ((1. X) - x) by Def9
.= (1. X) - x by Th38 ;
then A20: S1[ 0 ] by A16;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A20, A17);
hence for n being Element of NAT holds ((1. X) - x) * ((Partial_Sums (((1. X) - x) GeoSeq)) . n) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0) ; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((1._X)_-_(x_*_y)).||_<=_(||.((((1._X)_-_x)_GeoSeq)_^\_1).||_+_(||.x.||_(#)_||.((Partial_Sums_(((1._X)_-_x)_GeoSeq))_-_y).||))_._n
let n be Element of NAT ; ::_thesis: ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n
reconsider yn = (Partial_Sums (((1. X) - x) GeoSeq)) . n as Element of X ;
(Partial_Sums (((1. X) - x) GeoSeq)) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq)) . n) + ((((1. X) - x) GeoSeq) . (n + 1)) by BHSP_4:def_1;
then A21: (Partial_Sums (((1. X) - x) GeoSeq)) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq)) . n) + (((((1. X) - x) GeoSeq) ^\ 1) . n) by NAT_1:def_3;
((1. X) - ((1. X) - x)) * yn = ((1. X) * yn) - (((1. X) - x) * yn) by Th38
.= yn - (((1. X) - x) * yn) by Th38
.= ((Partial_Sums (((1. X) - x) GeoSeq)) . n) - ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by A15
.= (((Partial_Sums (((1. X) - x) GeoSeq)) . n) - (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by Th38 ;
then ((1. X) - ((1. X) - x)) * yn = (((Partial_Sums (((1. X) - x) GeoSeq)) . n) - (((Partial_Sums (((1. X) - x) GeoSeq)) . n) + (((((1. X) - x) GeoSeq) ^\ 1) . n))) + ((((1. X) - x) GeoSeq) . 0) by A21, NAT_1:def_3
.= ((((Partial_Sums (((1. X) - x) GeoSeq)) . n) - ((Partial_Sums (((1. X) - x) GeoSeq)) . n)) - (((((1. X) - x) GeoSeq) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by Th38
.= ((0. X) - (((((1. X) - x) GeoSeq) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by RLVECT_1:15
.= (0. X) - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:29
.= - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:14
.= ((((1. X) - x) GeoSeq) . 0) - (((((1. X) - x) GeoSeq) ^\ 1) . n) by RLVECT_1:33
.= ((((1. X) - x) GeoSeq) . 0) - ((((1. X) - x) GeoSeq) . (n + 1)) by NAT_1:def_3
.= (1. X) - ((((1. X) - x) GeoSeq) . (n + 1)) by Def9 ;
then A22: (1. X) - (x * yn) = (1. X) - ((1. X) - ((((1. X) - x) GeoSeq) . (n + 1))) by Th38
.= (((1. X) - x) GeoSeq) . (n + 1) by Th38
.= ((((1. X) - x) GeoSeq) ^\ 1) . n by NAT_1:def_3 ;
||.(x * (yn - y)).|| <= ||.x.|| * ||.(yn - y).|| by Th38;
then A23: (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ||.(x * (yn - y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.x.|| * ||.(yn - y).||) by XREAL_1:7;
( ||.((((((1. X) - x) GeoSeq) ^\ 1) . n) + (x * (yn - y))).|| <= ||.(((((1. X) - x) GeoSeq) ^\ 1) . n).|| + ||.(x * (yn - y)).|| & ||.(((((1. X) - x) GeoSeq) ^\ 1) . n).|| + ||.(x * (yn - y)).|| = (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ||.(x * (yn - y)).|| ) by NORMSP_0:def_4, NORMSP_1:def_1;
then A24: ||.((((((1. X) - x) GeoSeq) ^\ 1) . n) + (x * (yn - y))).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.x.|| * ||.(yn - y).||) by A23, XXREAL_0:2;
(1. X) - (x * y) = ((1. X) - (0. X)) - (x * y) by RLVECT_1:13
.= ((1. X) - ((x * yn) - (x * yn))) - (x * y) by RLVECT_1:15
.= (((1. X) - (x * yn)) + (x * yn)) - (x * y) by RLVECT_1:29
.= ((1. X) - (x * yn)) + ((x * yn) - (x * y)) by RLVECT_1:def_3
.= ((1. X) - (x * yn)) + (x * (yn - y)) by Th38 ;
then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.x.|| * ||.(((Partial_Sums (((1. X) - x) GeoSeq)) - y) . n).||) by A22, A24, NORMSP_1:def_4;
then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.x.|| * (||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| . n)) by NORMSP_0:def_4;
then ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ((||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) . n) by SEQ_1:9;
hence ||.((1. X) - (x * y)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n by SEQ_1:7; ::_thesis: verum
end;
then A25: 1. X = x * y by A8, A9, Lm3;
A26: for n being Element of NAT holds ((Partial_Sums (((1. X) - x) GeoSeq)) . n) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)
proof
defpred S1[ Element of NAT ] means ((Partial_Sums (((1. X) - x) GeoSeq)) . $1) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . $1) - ((((1. X) - x) GeoSeq) . 0);
A27: ((Partial_Sums (((1. X) - x) GeoSeq)) . 0) * ((1. X) - x) = ((((1. X) - x) GeoSeq) . 0) * ((1. X) - x) by BHSP_4:def_1
.= (1. X) * ((1. X) - x) by Def9
.= (1. X) - x by Th38 ;
A28: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A29: S1[k] ; ::_thesis: S1[k + 1]
A30: (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . (k + 1)) - ((((1. X) - x) GeoSeq) . 0) = ((Partial_Sums (((1. X) - x) GeoSeq)) . ((k + 1) + 1)) - ((((1. X) - x) GeoSeq) . 0) by NAT_1:def_3
.= (((Partial_Sums (((1. X) - x) GeoSeq)) . (k + 1)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1))) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1
.= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1))) + (- ((((1. X) - x) GeoSeq) . 0)) by NAT_1:def_3
.= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) - ((((1. X) - x) GeoSeq) . 0)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1)) by RLVECT_1:def_3 ;
((Partial_Sums (((1. X) - x) GeoSeq)) . (k + 1)) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq)) . k) + ((((1. X) - x) GeoSeq) . (k + 1))) * ((1. X) - x) by BHSP_4:def_1
.= (((Partial_Sums (((1. X) - x) GeoSeq)) . k) * ((1. X) - x)) + (((((1. X) - x) GeoSeq) . (k + 1)) * ((1. X) - x)) by Th38
.= ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . k) - ((((1. X) - x) GeoSeq) . 0)) + ((((1. X) - x) GeoSeq) . ((k + 1) + 1)) by A29, Def9 ;
hence S1[k + 1] by A30; ::_thesis: verum
end;
(((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . 0) - ((((1. X) - x) GeoSeq) . 0) = ((Partial_Sums (((1. X) - x) GeoSeq)) . (0 + 1)) - ((((1. X) - x) GeoSeq) . 0) by NAT_1:def_3
.= (((Partial_Sums (((1. X) - x) GeoSeq)) . 0) + ((((1. X) - x) GeoSeq) . 1)) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1
.= (((((1. X) - x) GeoSeq) . 0) + ((((1. X) - x) GeoSeq) . 1)) - ((((1. X) - x) GeoSeq) . 0) by BHSP_4:def_1
.= ((((1. X) - x) GeoSeq) . 1) + (((((1. X) - x) GeoSeq) . 0) - ((((1. X) - x) GeoSeq) . 0)) by Th38
.= ((((1. X) - x) GeoSeq) . 1) + (0. X) by RLVECT_1:15
.= (((1. X) - x) GeoSeq) . (0 + 1) by RLVECT_1:4
.= ((((1. X) - x) GeoSeq) . 0) * ((1. X) - x) by Def9
.= (1. X) * ((1. X) - x) by Def9
.= (1. X) - x by Th38 ;
then A31: S1[ 0 ] by A27;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A31, A28);
hence for n being Element of NAT holds ((Partial_Sums (((1. X) - x) GeoSeq)) . n) * ((1. X) - x) = (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0) ; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((1._X)_-_(y_*_x)).||_<=_(||.((((1._X)_-_x)_GeoSeq)_^\_1).||_+_(||.x.||_(#)_||.((Partial_Sums_(((1._X)_-_x)_GeoSeq))_-_y).||))_._n
let n be Element of NAT ; ::_thesis: ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n
reconsider yn = (Partial_Sums (((1. X) - x) GeoSeq)) . n as Element of X ;
(Partial_Sums (((1. X) - x) GeoSeq)) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq)) . n) + ((((1. X) - x) GeoSeq) . (n + 1)) by BHSP_4:def_1;
then A32: (Partial_Sums (((1. X) - x) GeoSeq)) . (n + 1) = ((Partial_Sums (((1. X) - x) GeoSeq)) . n) + (((((1. X) - x) GeoSeq) ^\ 1) . n) by NAT_1:def_3;
yn * ((1. X) - ((1. X) - x)) = (yn * (1. X)) - (yn * ((1. X) - x)) by Th38
.= yn - (yn * ((1. X) - x)) by Th38
.= ((Partial_Sums (((1. X) - x) GeoSeq)) . n) - ((((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by A26
.= (((Partial_Sums (((1. X) - x) GeoSeq)) . n) - (((Partial_Sums (((1. X) - x) GeoSeq)) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by Th38 ;
then yn * ((1. X) - ((1. X) - x)) = (((Partial_Sums (((1. X) - x) GeoSeq)) . n) - (((Partial_Sums (((1. X) - x) GeoSeq)) . n) + (((((1. X) - x) GeoSeq) ^\ 1) . n))) + ((((1. X) - x) GeoSeq) . 0) by A32, NAT_1:def_3
.= ((((Partial_Sums (((1. X) - x) GeoSeq)) . n) - ((Partial_Sums (((1. X) - x) GeoSeq)) . n)) - (((((1. X) - x) GeoSeq) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by Th38
.= ((0. X) - (((((1. X) - x) GeoSeq) ^\ 1) . n)) + ((((1. X) - x) GeoSeq) . 0) by RLVECT_1:15
.= (0. X) - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:29
.= - ((((((1. X) - x) GeoSeq) ^\ 1) . n) - ((((1. X) - x) GeoSeq) . 0)) by RLVECT_1:14
.= ((((1. X) - x) GeoSeq) . 0) - (((((1. X) - x) GeoSeq) ^\ 1) . n) by RLVECT_1:33
.= ((((1. X) - x) GeoSeq) . 0) - ((((1. X) - x) GeoSeq) . (n + 1)) by NAT_1:def_3
.= (1. X) - ((((1. X) - x) GeoSeq) . (n + 1)) by Def9 ;
then A33: (1. X) - (yn * x) = (1. X) - ((1. X) - ((((1. X) - x) GeoSeq) . (n + 1))) by Th38
.= (((1. X) - x) GeoSeq) . (n + 1) by Th38
.= ((((1. X) - x) GeoSeq) ^\ 1) . n by NAT_1:def_3 ;
||.((yn - y) * x).|| <= ||.(yn - y).|| * ||.x.|| by Th38;
then A34: (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ||.((yn - y) * x).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.(yn - y).|| * ||.x.||) by XREAL_1:7;
( ||.((((((1. X) - x) GeoSeq) ^\ 1) . n) + ((yn - y) * x)).|| <= ||.(((((1. X) - x) GeoSeq) ^\ 1) . n).|| + ||.((yn - y) * x).|| & ||.(((((1. X) - x) GeoSeq) ^\ 1) . n).|| + ||.((yn - y) * x).|| = (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ||.((yn - y) * x).|| ) by NORMSP_0:def_4, NORMSP_1:def_1;
then A35: ||.((((((1. X) - x) GeoSeq) ^\ 1) . n) + ((yn - y) * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.(yn - y).|| * ||.x.||) by A34, XXREAL_0:2;
(1. X) - (y * x) = ((1. X) - (0. X)) - (y * x) by RLVECT_1:13
.= ((1. X) - ((yn * x) - (yn * x))) - (y * x) by RLVECT_1:15
.= (((1. X) - (yn * x)) + (yn * x)) - (y * x) by RLVECT_1:29
.= ((1. X) - (yn * x)) + ((yn * x) - (y * x)) by RLVECT_1:def_3
.= ((1. X) - (yn * x)) + ((yn - y) * x) by Th38 ;
then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + (||.(((Partial_Sums (((1. X) - x) GeoSeq)) - y) . n).|| * ||.x.||) by A33, A35, NORMSP_1:def_4;
then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ((||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).|| . n) * ||.x.||) by NORMSP_0:def_4;
then ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| . n) + ((||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||) . n) by SEQ_1:9;
hence ||.((1. X) - (y * x)).|| <= (||.((((1. X) - x) GeoSeq) ^\ 1).|| + (||.x.|| (#) ||.((Partial_Sums (((1. X) - x) GeoSeq)) - y).||)) . n by SEQ_1:7; ::_thesis: verum
end;
then A36: 1. X = y * x by A8, A9, Lm3;
hence x is invertible by A25, Def4; ::_thesis: x " = Sum (((1. X) - x) GeoSeq)
hence x " = Sum (((1. X) - x) GeoSeq) by A36, A25, Def8; ::_thesis: verum
end;