:: HOLDER_1 semantic presentation

registration

let c₁ be real number ;
cluster right_closed_halfline a₁ -> non empty ;
coherence

proof end;

end;

theorem Th1: :: HOLDER_1:1

for b₁, b₂ being Real st 0 < b₁ & 0 < b₂ holds
for b₃ being Real st 0 <= b₃ holds
(b₃ to_power b₁) * (b₃ to_power b₂) = b₃ to_power (b₁ + b₂)

proof end;

theorem Th2: :: HOLDER_1:2

for b₁, b₂ being Real st 0 < b₁ & 0 < b₂ holds
for b₃ being Real st 0 <= b₃ holds
(b₃ to_power b₁) to_power b₂ = b₃ to_power (b₁ * b₂)

proof end;

theorem Th3: :: HOLDER_1:3

for b₁ being Real st 0 < b₁ holds
for b₂, b₃ being Real st 0 <= b₂ & b₂ <= b₃ holds
b₂ to_power b₁ <= b₃ to_power b₁

proof end;

theorem Th4: :: HOLDER_1:4

for b₁, b₂, b₃, b₄ being Real st 1 < b₁ & (1 / b₁) + (1 / b₂) = 1 & 0 < b₃ & 0 < b₄ holds
( b₃ * b₄ <= ((b₃ #R b₁) / b₁) + ((b₄ #R b₂) / b₂) & ( b₃ * b₄ = ((b₃ #R b₁) / b₁) + ((b₄ #R b₂) / b₂) implies b₃ #R b₁ = b₄ #R b₂ ) & ( b₃ #R b₁ = b₄ #R b₂ implies b₃ * b₄ = ((b₃ #R b₁) / b₁) + ((b₄ #R b₂) / b₂) ) )

proof end;

theorem Th5: :: HOLDER_1:5

for b₁, b₂, b₃, b₄ being Real st 1 < b₁ & (1 / b₁) + (1 / b₂) = 1 & 0 <= b₃ & 0 <= b₄ holds
( b₃ * b₄ <= ((b₃ to_power b₁) / b₁) + ((b₄ to_power b₂) / b₂) & ( b₃ * b₄ = ((b₃ to_power b₁) / b₁) + ((b₄ to_power b₂) / b₂) implies b₃ to_power b₁ = b₄ to_power b₂ ) & ( b₃ to_power b₁ = b₄ to_power b₂ implies b₃ * b₄ = ((b₃ to_power b₁) / b₁) + ((b₄ to_power b₂) / b₂) ) )

proof end;

Lemma4: for b₁ being Real_Sequence st ( for b₂ being Nat holds 0 <= b₁ . b₂ ) holds
for b₂ being Nat holds b₁ . b₂ <= (Partial_Sums b₁) . b₂

proof end;

Lemma5: for b₁ being Real_Sequence st ( for b₂ being Nat holds 0 <= b₁ . b₂ ) holds
for b₂ being Nat holds 0 <= (Partial_Sums b₁) . b₂

proof end;

Lemma6: for b₁ being Real_Sequence st ( for b₂ being Nat holds 0 <= b₁ . b₂ ) holds
for b₂ being Nat st (Partial_Sums b₁) . b₂ = 0 holds
for b₃ being Nat st b₃ <= b₂ holds
b₁ . b₃ = 0

proof end;

Lemma7: for b₁ being Real_Sequence
for b₂ being Nat st ( for b₃ being Nat st b₃ <= b₂ holds
b₁ . b₃ = 0 ) holds
(Partial_Sums b₁) . b₂ = 0

proof end;

theorem Th6: :: HOLDER_1:6

for b₁, b₂ being Real st 1 < b₁ & (1 / b₁) + (1 / b₂) = 1 holds
for b₃, b₄, b₅, b₆, b₇ being Real_Sequence st ( for b₈ being Nat holds
( b₅ . b₈ = (abs (b₃ . b₈)) to_power b₁ & b₆ . b₈ = (abs (b₄ . b₈)) to_power b₂ & b₇ . b₈ = abs ((b₃ . b₈) * (b₄ . b₈)) ) ) holds
for b₈ being Nat holds (Partial_Sums b₇) . b₈ <= (((Partial_Sums b₅) . b₈) to_power (1 / b₁)) * (((Partial_Sums b₆) . b₈) to_power (1 / b₂))

proof end;

theorem Th7: :: HOLDER_1:7

for b₁ being Real st 1 < b₁ holds
for b₂, b₃, b₄, b₅, b₆ being Real_Sequence st ( for b₇ being Nat holds
( b₄ . b₇ = (abs (b₂ . b₇)) to_power b₁ & b₅ . b₇ = (abs (b₃ . b₇)) to_power b₁ & b₆ . b₇ = (abs ((b₂ . b₇) + (b₃ . b₇))) to_power b₁ ) ) holds
for b₇ being Nat holds ((Partial_Sums b₆) . b₇) to_power (1 / b₁) <= (((Partial_Sums b₄) . b₇) to_power (1 / b₁)) + (((Partial_Sums b₅) . b₇) to_power (1 / b₁))

proof end;

theorem Th8: :: HOLDER_1:8

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds b₁ . b₃ <= b₂ . b₃ ) & b₂ is convergent & b₁ is non-decreasing holds
( b₁ is convergent & lim b₁ <= lim b₂ )

proof end;

theorem Th9: :: HOLDER_1:9

for b₁, b₂, b₃ being Real_Sequence st ( for b₄ being Nat holds b₁ . b₄ <= (b₂ . b₄) + (b₃ . b₄) ) & b₂ is convergent & b₃ is convergent & b₁ is non-decreasing holds
( b₁ is convergent & lim b₁ <= (lim b₂) + (lim b₃) )

proof end;

theorem Th10: :: HOLDER_1:10

for b₁ being Real st 0 < b₁ holds
for b₂, b₃ being Real_Sequence st b₂ is convergent & ( for b₄ being Nat holds 0 <= b₂ . b₄ ) & ( for b₄ being Nat holds b₃ . b₄ = (b₂ . b₄) to_power b₁ ) holds
( b₃ is convergent & lim b₃ = (lim b₂) to_power b₁ )

proof end;

theorem Th11: :: HOLDER_1:11

for b₁ being Real st 0 < b₁ holds
for b₂, b₃ being Real_Sequence st b₂ is summable & ( for b₄ being Nat holds 0 <= b₂ . b₄ ) & ( for b₄ being Nat holds b₃ . b₄ = ((Partial_Sums b₂) . b₄) to_power b₁ ) holds
( b₃ is convergent & lim b₃ = (Sum b₂) to_power b₁ & b₃ is non-decreasing & ( for b₄ being Nat holds b₃ . b₄ <= (Sum b₂) to_power b₁ ) )

proof end;

theorem Th12: :: HOLDER_1:12

for b₁, b₂ being Real st 1 < b₁ & (1 / b₁) + (1 / b₂) = 1 holds
for b₃, b₄, b₅, b₆, b₇ being Real_Sequence st ( for b₈ being Nat holds
( b₅ . b₈ = (abs (b₃ . b₈)) to_power b₁ & b₆ . b₈ = (abs (b₄ . b₈)) to_power b₂ & b₇ . b₈ = abs ((b₃ . b₈) * (b₄ . b₈)) ) ) & b₅ is summable & b₆ is summable holds
( b₇ is summable & Sum b₇ <= ((Sum b₅) to_power (1 / b₁)) * ((Sum b₆) to_power (1 / b₂)) )

proof end;

theorem Th13: :: HOLDER_1:13

for b₁ being Real st 1 < b₁ holds
for b₂, b₃, b₄, b₅, b₆ being Real_Sequence st ( for b₇ being Nat holds
( b₄ . b₇ = (abs (b₂ . b₇)) to_power b₁ & b₅ . b₇ = (abs (b₃ . b₇)) to_power b₁ & b₆ . b₇ = (abs ((b₂ . b₇) + (b₃ . b₇))) to_power b₁ ) ) & b₄ is summable & b₅ is summable holds
( b₆ is summable & (Sum b₆) to_power (1 / b₁) <= ((Sum b₄) to_power (1 / b₁)) + ((Sum b₅) to_power (1 / b₁)) )

proof end;