:: by Yasumasa Suzuki

::

:: Received September 25, 2004

:: Copyright (c) 2004-2016 Association of Mizar Users

definition

let x be Real_Sequence;

let p be Real;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = |.(x . n).| to_power p

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = |.(x . n).| to_power p ) & ( for n being Nat holds b_{2} . n = |.(x . n).| to_power p ) holds

b_{1} = b_{2}

end;
let p be Real;

func x rto_power p -> Real_Sequence means :Def1: :: LP_SPACE:def 1

for n being Nat holds it . n = |.(x . n).| to_power p;

existence for n being Nat holds it . n = |.(x . n).| to_power p;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines rto_power LP_SPACE:def 1 :

for x being Real_Sequence

for p being Real

for b_{3} being Real_Sequence holds

( b_{3} = x rto_power p iff for n being Nat holds b_{3} . n = |.(x . n).| to_power p );

for x being Real_Sequence

for p being Real

for b

( b

definition

let p be Real;

assume A1: p >= 1 ;

ex b_{1} being non empty Subset of Linear_Space_of_RealSequences st

for x being set holds

( x in b_{1} iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) )

for b_{1}, b_{2} being non empty Subset of Linear_Space_of_RealSequences st ( for x being set holds

( x in b_{1} iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) ) holds

b_{1} = b_{2}

end;
assume A1: p >= 1 ;

func the_set_of_RealSequences_l^ p -> non empty Subset of Linear_Space_of_RealSequences means :Def2: :: LP_SPACE:def 2

for x being set holds

( x in it iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) );

existence for x being set holds

( x in it iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def2 defines the_set_of_RealSequences_l^ LP_SPACE:def 2 :

for p being Real st p >= 1 holds

for b_{2} being non empty Subset of Linear_Space_of_RealSequences holds

( b_{2} = the_set_of_RealSequences_l^ p iff for x being set holds

( x in b_{2} iff ( x in the_set_of_RealSequences & (seq_id x) rto_power p is summable ) ) );

for p being Real st p >= 1 holds

for b

( b

( x in b

Lm1: for x1, y1 being Real st x1 >= 0 & y1 > 0 holds

x1 to_power y1 >= 0

proof end;

Lm2: for x1, x2, y1 being Real st y1 > 0 & x1 >= 0 & x2 >= 0 holds

(x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)

proof end;

Lm3: for p being Real st 1 = p holds

for a, b being Real_Sequence

for n being Nat holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))

proof end;

theorem Th2: :: LP_SPACE:2

for p being Real st 1 <= p holds

for a, b being Real_Sequence

for n being Nat holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))

for a, b being Real_Sequence

for n being Nat holds ((Partial_Sums ((a + b) rto_power p)) . n) to_power (1 / p) <= (((Partial_Sums (a rto_power p)) . n) to_power (1 / p)) + (((Partial_Sums (b rto_power p)) . n) to_power (1 / p))

proof end;

Lm4: for a, b being Real_Sequence

for p being Real st 1 = p & a rto_power p is summable & b rto_power p is summable holds

( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )

proof end;

theorem Th3: :: LP_SPACE:3

for a, b being Real_Sequence

for p being Real st 1 <= p & a rto_power p is summable & b rto_power p is summable holds

( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )

for p being Real st 1 <= p & a rto_power p is summable & b rto_power p is summable holds

( (a + b) rto_power p is summable & (Sum ((a + b) rto_power p)) to_power (1 / p) <= ((Sum (a rto_power p)) to_power (1 / p)) + ((Sum (b rto_power p)) to_power (1 / p)) )

proof end;

theorem Th5: :: LP_SPACE:5

for p being Real st 1 <= p holds

RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is Subspace of Linear_Space_of_RealSequences

RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is Subspace of Linear_Space_of_RealSequences

proof end;

theorem :: LP_SPACE:6

for p being Real st 1 <= p holds

( RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is Abelian & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is add-associative & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is right_zeroed & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is right_complementable & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is vector-distributive & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is scalar-distributive & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is scalar-associative & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is scalar-unital ) by Th5;

( RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is Abelian & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is add-associative & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is right_zeroed & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is right_complementable & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is vector-distributive & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is scalar-distributive & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is scalar-associative & RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is scalar-unital ) by Th5;

theorem :: LP_SPACE:7

for p being Real st 1 <= p holds

RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is RealLinearSpace by Th5;

RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)) #) is RealLinearSpace by Th5;

definition

let p be Real;

ex b_{1} being Function of (the_set_of_RealSequences_l^ p),REAL st

for x being object st x in the_set_of_RealSequences_l^ p holds

b_{1} . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p)

for b_{1}, b_{2} being Function of (the_set_of_RealSequences_l^ p),REAL st ( for x being object st x in the_set_of_RealSequences_l^ p holds

b_{1} . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) & ( for x being object st x in the_set_of_RealSequences_l^ p holds

b_{2} . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) holds

b_{1} = b_{2}

end;
func l_norm^ p -> Function of (the_set_of_RealSequences_l^ p),REAL means :Def3: :: LP_SPACE:def 3

for x being object st x in the_set_of_RealSequences_l^ p holds

it . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p);

existence for x being object st x in the_set_of_RealSequences_l^ p holds

it . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p);

ex b

for x being object st x in the_set_of_RealSequences_l^ p holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines l_norm^ LP_SPACE:def 3 :

for p being Real

for b_{2} being Function of (the_set_of_RealSequences_l^ p),REAL holds

( b_{2} = l_norm^ p iff for x being object st x in the_set_of_RealSequences_l^ p holds

b_{2} . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) );

for p being Real

for b

( b

b

theorem Th8: :: LP_SPACE:8

for p being Real st 1 <= p holds

NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) is RealLinearSpace

NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) is RealLinearSpace

proof end;

theorem Th9: :: LP_SPACE:9

for p being Real st p >= 1 holds

NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) is Subspace of Linear_Space_of_RealSequences

NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) is Subspace of Linear_Space_of_RealSequences

proof end;

theorem Th10: :: LP_SPACE:10

for p being Real st 1 <= p holds

for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) )

for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds

( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real

for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds

( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) )

proof end;

theorem Th11: :: LP_SPACE:11

for p being Real st p >= 1 holds

for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds

( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 )

for rseq being Real_Sequence st ( for n being Nat holds rseq . n = 0 ) holds

( rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 )

proof end;

theorem Th12: :: LP_SPACE:12

for p being Real st 1 <= p holds

for rseq being Real_Sequence st rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 holds

for n being Nat holds rseq . n = 0

for rseq being Real_Sequence st rseq rto_power p is summable & (Sum (rseq rto_power p)) to_power (1 / p) = 0 holds

for n being Nat holds rseq . n = 0

proof end;

Lm5: for p being Real st 1 <= p holds

for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

for x being Point of lp

for a being Real holds (seq_id (a * x)) rto_power p = (|.a.| to_power p) (#) ((seq_id x) rto_power p)

proof end;

Lm6: for p being Real st 1 <= p holds

for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

for x being Point of lp

for a being Real holds Sum ((seq_id (a * x)) rto_power p) = (|.a.| to_power p) * (Sum ((seq_id x) rto_power p))

proof end;

Lm7: for p being Real st 1 <= p holds

for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

for x being Point of lp

for a being Real holds (Sum ((seq_id (a * x)) rto_power p)) to_power (1 / p) = |.a.| * ((Sum ((seq_id x) rto_power p)) to_power (1 / p))

proof end;

theorem Th13: :: LP_SPACE:13

for p being Real st 1 <= p holds

for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

for x, y being Point of lp

for a being Real holds

( ( ||.x.|| = 0 implies x = 0. lp ) & ( x = 0. lp implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

for x, y being Point of lp

for a being Real holds

( ( ||.x.|| = 0 implies x = 0. lp ) & ( x = 0. lp implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.a.| * ||.x.|| )

proof end;

theorem Th14: :: LP_SPACE:14

for p being Real st p >= 1 holds

for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

( lp is reflexive & lp is discerning & lp is RealNormSpace-like )

for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

( lp is reflexive & lp is discerning & lp is RealNormSpace-like )

proof end;

theorem :: LP_SPACE:15

for p being Real st p >= 1 holds

for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

lp is RealNormSpace by Th9, Th14;

for lp being non empty NORMSTR st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

lp is RealNormSpace by Th9, Th14;

Lm8: for p being Real st 0 < p holds

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).| to_power p ) holds

( rseq is convergent & lim rseq = |.((lim seq) - c).| to_power p )

proof end;

Lm9: for p being Real st 0 < p holds

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).| to_power p) + (seq1 . i) ) holds

( rseq is convergent & lim rseq = (|.((lim seq) - c).| to_power p) + (lim seq1) )

proof end;

Lm10: for a, b being Real_Sequence holds a = (a + b) - b

proof end;

Lm11: for p being Real st p >= 1 holds

for a, b being Real_Sequence st a rto_power p is summable & b rto_power p is summable holds

(a + b) rto_power p is summable

proof end;

theorem Th16: :: LP_SPACE:16

for p being Real st 1 <= p holds

for lp being RealNormSpace st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

for vseq being sequence of lp st vseq is Cauchy_sequence_by_Norm holds

vseq is convergent

for lp being RealNormSpace st lp = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) holds

for vseq being sequence of lp st vseq is Cauchy_sequence_by_Norm holds

vseq is convergent

proof end;

definition

let p be Real;

assume A1: 1 <= p ;

NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) is RealBanachSpace

end;
assume A1: 1 <= p ;

func l_Space^ p -> RealBanachSpace equals :: LP_SPACE:def 4

NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #);

coherence NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #);

NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #) is RealBanachSpace

proof end;

:: deftheorem defines l_Space^ LP_SPACE:def 4 :

for p being Real st 1 <= p holds

l_Space^ p = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #);

for p being Real st 1 <= p holds

l_Space^ p = NORMSTR(# (the_set_of_RealSequences_l^ p),(Zero_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Add_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(Mult_ ((the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences)),(l_norm^ p) #);