environ
vocabularies HIDDEN, NUMBERS, STRUCT_0, RSSPACE, RLVECT_1, SEQ_1, VALUED_1, SERIES_1, SUPINF_2, ARYTM_3, REAL_1, RELAT_1, ARYTM_1, PROB_2, CARD_3, COMPLEX1, SUBSET_1, CARD_1, XXREAL_0, FUNCT_1, SQUARE_1, BHSP_1, ALGSTR_0, ZFMISC_1, REALSET1, PRE_TOPC, VALUED_0, XXREAL_2, ORDINAL2, SEQ_2, NAT_1, BHSP_3, NORMSP_1, REWRITE1, RSSPACE2, ASYMPT_1;
notations HIDDEN, TARSKI, SUBSET_1, ZFMISC_1, ORDINAL1, BINOP_1, REALSET1, RELAT_1, PARTFUN1, FUNCT_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, COMPLEX1, REAL_1, NAT_1, VALUED_1, SQUARE_1, SEQ_1, SERIES_1, COMSEQ_2, SEQ_2, STRUCT_0, ALGSTR_0, XREAL_0, PRE_TOPC, RLVECT_1, BHSP_1, BHSP_2, BHSP_3, FUNCSDOM, RSSPACE;
definitions BHSP_3;
theorems RELAT_1, SQUARE_1, ZFMISC_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1, INT_1, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, RLSUB_1, BHSP_1, BHSP_2, BHSP_3, SEQ_4, RSSPACE, XREAL_0, XCMPLX_1, COMPLEX1, XREAL_1, XXREAL_0, ORDINAL1;
schemes NAT_1, SEQ_1, FUNCT_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, REALSET1, STRUCT_0, RSSPACE, VALUED_1, FUNCT_2, VALUED_0, NAT_1, SEQ_4, SERIES_1, SQUARE_1, SEQ_1, SEQ_2;
constructors HIDDEN, PARTFUN1, BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, NAT_D, SEQ_2, SERIES_1, REALSET1, RLSUB_1, BHSP_2, BHSP_3, RSSPACE, VALUED_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1, FUNCSDOM;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities SQUARE_1, BINOP_1, REALSET1, RLVECT_1, STRUCT_0, ALGSTR_0, RSSPACE, FUNCSDOM, SEQ_1;
expansions ;
Lm1:
for rseq being Real_Sequence st ( for n being Nat holds 0 <= rseq . n ) holds
( ( for n being Nat holds 0 <= (Partial_Sums rseq) . n ) & ( for n being Nat holds rseq . n <= (Partial_Sums rseq) . n ) & ( rseq is summable implies ( ( for n being Nat holds (Partial_Sums rseq) . n <= Sum rseq ) & ( for n being Nat holds rseq . n <= Sum rseq ) ) ) )
Lm2:
( ( for x, y being Real holds (x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y) ) & ( for x, y being Real holds x * x <= ((2 * (x - y)) * (x - y)) + ((2 * y) * y) ) )
Lm3:
for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e holds
lim seq <= e
Lm4:
for c being Real
for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = ((seq . i) - c) * ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = ((lim seq) - c) * ((lim seq) - c) )
Lm5:
for c being Real
for seq, seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Nat holds rseq . i = (((seq . i) - c) * ((seq . i) - c)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (((lim seq) - c) * ((lim seq) - c)) + (lim seq1) )
theorem
( ( for
x,
y being
Real holds
(x + y) * (x + y) <= ((2 * x) * x) + ((2 * y) * y) ) & ( for
x,
y being
Real holds
x * x <= ((2 * (x - y)) * (x - y)) + ((2 * y) * y) ) )
by Lm2;