:: LP_SPACE semantic presentation

definition
let c1 be Real_Sequence;
let c2 be Real;
func c1 rto_power c2 -> Real_Sequence means :Def1: :: LP_SPACE:def 1
for b1 being Nat holds a3 . b1 = (abs (a1 . b1)) to_power a2;
existence
ex b1 being Real_Sequence st
for b2 being Nat holds b1 . b2 = (abs (c1 . b2)) to_power c2
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for b3 being Nat holds b1 . b3 = (abs (c1 . b3)) to_power c2 ) & ( for b3 being Nat holds b2 . b3 = (abs (c1 . b3)) to_power c2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines rto_power LP_SPACE:def 1 :
for b1 being Real_Sequence
for b2 being Real
for b3 being Real_Sequence holds
( b3 = b1 rto_power b2 iff for b4 being Nat holds b3 . b4 = (abs (b1 . b4)) to_power b2 );

definition
let c1 be Real;
assume E2: c1 >= 1 ;
func the_set_of_RealSequences_l^ c1 -> non empty Subset of Linear_Space_of_RealSequences means :Def2: :: LP_SPACE:def 2
for b1 being set holds
( b1 in a2 iff ( b1 in the_set_of_RealSequences & (seq_id b1) rto_power a1 is summable ) );
existence
ex b1 being non empty Subset of Linear_Space_of_RealSequences st
for b2 being set holds
( b2 in b1 iff ( b2 in the_set_of_RealSequences & (seq_id b2) rto_power c1 is summable ) )
proof end;
uniqueness
for b1, b2 being non empty Subset of Linear_Space_of_RealSequences st ( for b3 being set holds
( b3 in b1 iff ( b3 in the_set_of_RealSequences & (seq_id b3) rto_power c1 is summable ) ) ) & ( for b3 being set holds
( b3 in b2 iff ( b3 in the_set_of_RealSequences & (seq_id b3) rto_power c1 is summable ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines the_set_of_RealSequences_l^ LP_SPACE:def 2 :
for b1 being Real st b1 >= 1 holds
for b2 being non empty Subset of Linear_Space_of_RealSequences holds
( b2 = the_set_of_RealSequences_l^ b1 iff for b3 being set holds
( b3 in b2 iff ( b3 in the_set_of_RealSequences & (seq_id b3) rto_power b1 is summable ) ) );

Lemma3: for b1, b2 being Real st b1 >= 0 & b2 > 0 holds
b1 to_power b2 >= 0
proof end;

Lemma4: for b1, b2, b3 being Real st b1 > 0 & b2 >= 0 & b3 >= 0 holds
(b2 * b3) to_power b1 = (b2 to_power b1) * (b3 to_power b1)
proof end;

theorem Th1: :: LP_SPACE:1
for b1, b2, b3 being Real st b1 >= 0 & b1 < b2 & b3 > 0 holds
b1 to_power b3 < b2 to_power b3
proof end;

Lemma6: for b1 being Real st 1 = b1 holds
for b2, b3 being Real_Sequence
for b4 being Nat holds ((Partial_Sums ((b2 + b3) rto_power b1)) . b4) to_power (1 / b1) <= (((Partial_Sums (b2 rto_power b1)) . b4) to_power (1 / b1)) + (((Partial_Sums (b3 rto_power b1)) . b4) to_power (1 / b1))
proof end;

theorem Th2: :: LP_SPACE:2
for b1 being Real st 1 <= b1 holds
for b2, b3 being Real_Sequence
for b4 being Nat holds ((Partial_Sums ((b2 + b3) rto_power b1)) . b4) to_power (1 / b1) <= (((Partial_Sums (b2 rto_power b1)) . b4) to_power (1 / b1)) + (((Partial_Sums (b3 rto_power b1)) . b4) to_power (1 / b1))
proof end;

Lemma8: for b1, b2 being Real_Sequence
for b3 being Real st 1 = b3 & b1 rto_power b3 is summable & b2 rto_power b3 is summable holds
( (b1 + b2) rto_power b3 is summable & (Sum ((b1 + b2) rto_power b3)) to_power (1 / b3) <= ((Sum (b1 rto_power b3)) to_power (1 / b3)) + ((Sum (b2 rto_power b3)) to_power (1 / b3)) )
proof end;

theorem Th3: :: LP_SPACE:3
for b1, b2 being Real_Sequence
for b3 being Real st 1 <= b3 & b1 rto_power b3 is summable & b2 rto_power b3 is summable holds
( (b1 + b2) rto_power b3 is summable & (Sum ((b1 + b2) rto_power b3)) to_power (1 / b3) <= ((Sum (b1 rto_power b3)) to_power (1 / b3)) + ((Sum (b2 rto_power b3)) to_power (1 / b3)) )
proof end;

theorem Th4: :: LP_SPACE:4
for b1 being Real st 1 <= b1 holds
the_set_of_RealSequences_l^ b1 is lineary-closed
proof end;

theorem Th5: :: LP_SPACE:5
for b1 being Real st 1 <= b1 holds
RLSStruct(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ) #) is Subspace of Linear_Space_of_RealSequences
proof end;

theorem Th6: :: LP_SPACE:6
for b1 being Real st 1 <= b1 holds
( RLSStruct(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ) #) is Abelian & RLSStruct(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ) #) is add-associative & RLSStruct(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ) #) is right_zeroed & RLSStruct(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ) #) is right_complementable & RLSStruct(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ) #) is RealLinearSpace-like ) by Th5;

theorem Th7: :: LP_SPACE:7
for b1 being Real st 1 <= b1 holds
RLSStruct(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ) #) is RealLinearSpace by Th6;

Lemma14: for b1 being Real ex b2 being Function of the_set_of_RealSequences_l^ b1, REAL st
for b3 being set st b3 in the_set_of_RealSequences_l^ b1 holds
b2 . b3 = (Sum ((seq_id b3) rto_power b1)) to_power (1 / b1)
proof end;

definition
let c1 be Real;
func l_norm^ c1 -> Function of the_set_of_RealSequences_l^ a1, REAL means :Def3: :: LP_SPACE:def 3
for b1 being set st b1 in the_set_of_RealSequences_l^ a1 holds
a2 . b1 = (Sum ((seq_id b1) rto_power a1)) to_power (1 / a1);
existence
ex b1 being Function of the_set_of_RealSequences_l^ c1, REAL st
for b2 being set st b2 in the_set_of_RealSequences_l^ c1 holds
b1 . b2 = (Sum ((seq_id b2) rto_power c1)) to_power (1 / c1) by Lemma14;
uniqueness
for b1, b2 being Function of the_set_of_RealSequences_l^ c1, REAL st ( for b3 being set st b3 in the_set_of_RealSequences_l^ c1 holds
b1 . b3 = (Sum ((seq_id b3) rto_power c1)) to_power (1 / c1) ) & ( for b3 being set st b3 in the_set_of_RealSequences_l^ c1 holds
b2 . b3 = (Sum ((seq_id b3) rto_power c1)) to_power (1 / c1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines l_norm^ LP_SPACE:def 3 :
for b1 being Real
for b2 being Function of the_set_of_RealSequences_l^ b1, REAL holds
( b2 = l_norm^ b1 iff for b3 being set st b3 in the_set_of_RealSequences_l^ b1 holds
b2 . b3 = (Sum ((seq_id b3) rto_power b1)) to_power (1 / b1) );

theorem Th8: :: LP_SPACE:8
for b1 being Real st 1 <= b1 holds
NORMSTR(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(l_norm^ b1) #) is RealLinearSpace
proof end;

theorem Th9: :: LP_SPACE:9
for b1 being Real st b1 >= 1 holds
NORMSTR(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(l_norm^ b1) #) is Subspace of Linear_Space_of_RealSequences
proof end;

theorem Th10: :: LP_SPACE:10
for b1 being Real st 1 <= b1 holds
for b2 being non empty NORMSTR st b2 = NORMSTR(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(l_norm^ b1) #) holds
( the carrier of b2 = the_set_of_RealSequences_l^ b1 & ( for b3 being set holds
( b3 is VECTOR of b2 iff ( b3 is Real_Sequence & (seq_id b3) rto_power b1 is summable ) ) ) & 0. b2 = Zeroseq & ( for b3 being VECTOR of b2 holds b3 = seq_id b3 ) & ( for b3, b4 being VECTOR of b2 holds b3 + b4 = (seq_id b3) + (seq_id b4) ) & ( for b3 being Real
for b4 being VECTOR of b2 holds b3 * b4 = b3 (#) (seq_id b4) ) & ( for b3 being VECTOR of b2 holds
( - b3 = - (seq_id b3) & seq_id (- b3) = - (seq_id b3) ) ) & ( for b3, b4 being VECTOR of b2 holds b3 - b4 = (seq_id b3) - (seq_id b4) ) & ( for b3 being VECTOR of b2 holds (seq_id b3) rto_power b1 is summable ) & ( for b3 being VECTOR of b2 holds ||.b3.|| = (Sum ((seq_id b3) rto_power b1)) to_power (1 / b1) ) )
proof end;

theorem Th11: :: LP_SPACE:11
for b1 being Real st b1 >= 1 holds
for b2 being Real_Sequence st ( for b3 being Nat holds b2 . b3 = 0 ) holds
( b2 rto_power b1 is summable & (Sum (b2 rto_power b1)) to_power (1 / b1) = 0 )
proof end;

theorem Th12: :: LP_SPACE:12
for b1 being Real st 1 <= b1 holds
for b2 being Real_Sequence st b2 rto_power b1 is summable & (Sum (b2 rto_power b1)) to_power (1 / b1) = 0 holds
for b3 being Nat holds b2 . b3 = 0
proof end;

Lemma21: for b1 being Real st 1 <= b1 holds
for b2 being non empty NORMSTR st b2 = NORMSTR(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(l_norm^ b1) #) holds
for b3 being Point of b2
for b4 being Real holds (seq_id (b4 * b3)) rto_power b1 = ((abs b4) to_power b1) (#) ((seq_id b3) rto_power b1)
proof end;

Lemma22: for b1 being Real st 1 <= b1 holds
for b2 being non empty NORMSTR st b2 = NORMSTR(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(l_norm^ b1) #) holds
for b3 being Point of b2
for b4 being Real holds Sum ((seq_id (b4 * b3)) rto_power b1) = ((abs b4) to_power b1) * (Sum ((seq_id b3) rto_power b1))
proof end;

Lemma23: for b1 being Real st 1 <= b1 holds
for b2 being non empty NORMSTR st b2 = NORMSTR(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(l_norm^ b1) #) holds
for b3 being Point of b2
for b4 being Real holds (Sum ((seq_id (b4 * b3)) rto_power b1)) to_power (1 / b1) = (abs b4) * ((Sum ((seq_id b3) rto_power b1)) to_power (1 / b1))
proof end;

theorem Th13: :: LP_SPACE:13
for b1 being Real st 1 <= b1 holds
for b2 being non empty NORMSTR st b2 = NORMSTR(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(l_norm^ b1) #) holds
for b3, b4 being Point of b2
for b5 being Real holds
( ( ||.b3.|| = 0 implies b3 = 0. b2 ) & ( b3 = 0. b2 implies ||.b3.|| = 0 ) & 0 <= ||.b3.|| & ||.(b3 + b4).|| <= ||.b3.|| + ||.b4.|| & ||.(b5 * b3).|| = (abs b5) * ||.b3.|| )
proof end;

theorem Th14: :: LP_SPACE:14
for b1 being Real st b1 >= 1 holds
for b2 being non empty NORMSTR st b2 = NORMSTR(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(l_norm^ b1) #) holds
b2 is RealNormSpace-like
proof end;

theorem Th15: :: LP_SPACE:15
for b1 being Real st b1 >= 1 holds
for b2 being non empty NORMSTR st b2 = NORMSTR(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(l_norm^ b1) #) holds
b2 is RealNormSpace by Th9, Th14;

Lemma27: for b1 being Real
for b2 being Real_Sequence st b2 is convergent holds
for b3 being Real_Sequence st ( for b4 being Nat holds b3 . b4 = abs ((b2 . b4) - b1) ) holds
( b3 is convergent & lim b3 = abs ((lim b2) - b1) )
by RSSPACE3:1;

Lemma28: for b1 being Real st 0 < b1 holds
for b2 being Real
for b3 being Real_Sequence st b3 is convergent holds
for b4 being Real_Sequence st ( for b5 being Nat holds b4 . b5 = (abs ((b3 . b5) - b2)) to_power b1 ) holds
( b4 is convergent & lim b4 = (abs ((lim b3) - b2)) to_power b1 )
proof end;

Lemma29: for b1 being Real st 0 < b1 holds
for b2 being Real
for b3, b4 being Real_Sequence st b3 is convergent & b4 is convergent holds
for b5 being Real_Sequence st ( for b6 being Nat holds b5 . b6 = ((abs ((b3 . b6) - b2)) to_power b1) + (b4 . b6) ) holds
( b5 is convergent & lim b5 = ((abs ((lim b3) - b2)) to_power b1) + (lim b4) )
proof end;

Lemma30: for b1 being Real
for b2 being Real_Sequence st b2 is convergent & ex b3 being Nat st
for b4 being Nat st b3 <= b4 holds
b2 . b4 <= b1 holds
lim b2 <= b1
by RSSPACE2:6;

Lemma31: for b1, b2 being Real_Sequence holds b1 = (b1 + b2) - b2
proof end;

Lemma32: for b1 being Real st b1 >= 1 holds
for b2, b3 being Real_Sequence st b2 rto_power b1 is summable & b3 rto_power b1 is summable holds
(b2 + b3) rto_power b1 is summable
proof end;

theorem Th16: :: LP_SPACE:16
for b1 being Real st 1 <= b1 holds
for b2 being RealNormSpace st b2 = NORMSTR(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(l_norm^ b1) #) holds
for b3 being sequence of b2 st b3 is CCauchy holds
b3 is convergent
proof end;

definition
let c1 be Real;
assume E34: 1 <= c1 ;
func l_Space^ c1 -> RealBanachSpace equals :: LP_SPACE:def 4
 NORMSTR(# (the_set_of_RealSequences_l^ a1),(Zero_ (the_set_of_RealSequences_l^ a1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ a1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ a1),Linear_Space_of_RealSequences ),(l_norm^ a1) #);
coherence
NORMSTR(# (the_set_of_RealSequences_l^ c1),(Zero_ (the_set_of_RealSequences_l^ c1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ c1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ c1),Linear_Space_of_RealSequences ),(l_norm^ c1) #) is RealBanachSpace
proof end;
end;

:: deftheorem Def4 defines l_Space^ LP_SPACE:def 4 :
for b1 being Real st 1 <= b1 holds
l_Space^ b1 = NORMSTR(# (the_set_of_RealSequences_l^ b1),(Zero_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ b1),Linear_Space_of_RealSequences ),(l_norm^ b1) #);