:: ASYMPT_1 semantic presentation

Lemma1: for b₁ being Nat st b₁ >= 2 holds
2 to_power b₁ > b₁ + 1

proof end;

theorem Th1: :: ASYMPT_1:1

for b₁, b₂ being Real_Sequence st b₁ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₁ . b₃ = ((((12 * (b₃ to_power 3)) * (log 2,b₃)) - (5 * (b₃ ^2 ))) + ((log 2,b₃) ^2 )) + 36 ) & b₂ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₂ . b₃ = (b₃ to_power 3) * (log 2,b₃) ) holds
ex b₃, b₄ being eventually-positive Real_Sequence st
( b₃ = b₁ & b₄ = b₂ & b₃ in Big_Oh b₄ )

proof end;

Lemma2: for b₁ being logbase Real
for b₂ being Real_Sequence st b₁ > 1 & b₂ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₂ . b₃ = log b₁,b₃ ) holds
b₂ is eventually-positive

proof end;

theorem Th2: :: ASYMPT_1:2

for b₁, b₂ being logbase Real
for b₃, b₄ being Real_Sequence st b₁ > 1 & b₂ > 1 & b₃ . 0 = 0 & ( for b₅ being Nat st b₅ > 0 holds
b₃ . b₅ = log b₁,b₅ ) & b₄ . 0 = 0 & ( for b₅ being Nat st b₅ > 0 holds
b₄ . b₅ = log b₂,b₅ ) holds
ex b₅, b₆ being eventually-positive Real_Sequence st
( b₅ = b₃ & b₆ = b₄ & Big_Oh b₅ = Big_Oh b₆ )

proof end;

definition

let c₁, c₂, c₃ be Real;
func seq_a^ c₁,c₂,c₃ -> Real_Sequence means :Def1: :: ASYMPT_1:def 1
for b₁ being Nat holds a₄ . b₁ = a₁ to_power ((a₂ * b₁) + a₃);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines seq_a^ ASYMPT_1:def 1 :

registration

let c₁ be positive Real;
let c₂, c₃ be Real;
cluster seq_a^ a₁,a₂,a₃ -> eventually-positive ;
coherence

proof end;

end;

Lemma4: for b₁, b₂, b₃ being Real st b₁ > 0 & b₃ > 0 & b₃ <> 1 holds
b₁ to_power b₂ = b₃ to_power (b₂ * (log b₃,b₁))

proof end;

theorem Th3: :: ASYMPT_1:3

for b₁, b₂ being positive Real st b₁ < b₂ holds
not seq_a^ b₂,1,0 in Big_Oh (seq_a^ b₁,1,0)

proof end;

definition

func seq_logn -> Real_Sequence means :Def2: :: ASYMPT_1:def 2
( a₁ . 0 = 0 & ( for b₁ being Nat st b₁ > 0 holds
a₁ . b₁ = log 2,b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines seq_logn ASYMPT_1:def 2 :

definition

let c₁ be Real;
func seq_n^ c₁ -> Real_Sequence means :Def3: :: ASYMPT_1:def 3
( a₂ . 0 = 0 & ( for b₁ being Nat st b₁ > 0 holds
a₂ . b₁ = b₁ to_power a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines seq_n^ ASYMPT_1:def 3 :

registration

cluster seq_logn -> eventually-positive ;
coherence

proof end;

end;

registration

let c₁ be Real;
cluster seq_n^ a₁ -> eventually-positive ;
coherence

proof end;

end;

Lemma7: for b₁, b₂ being Real_Sequence
for b₃ being Nat holds (b₁ /" b₂) . b₃ = (b₁ . b₃) / (b₂ . b₃)

proof end;

Lemma8: for b₁, b₂ being eventually-nonnegative Real_Sequence holds
( ( b₁ in Big_Oh b₂ & b₂ in Big_Oh b₁ ) iff Big_Oh b₁ = Big_Oh b₂ )

proof end;

theorem Th4: :: ASYMPT_1:4

for b₁, b₂ being eventually-nonnegative Real_Sequence holds
( Big_Oh b₁ c= Big_Oh b₂ & not Big_Oh b₁ = Big_Oh b₂ iff ( b₁ in Big_Oh b₂ & not b₁ in Big_Omega b₂ ) )

proof end;

Lemma10: for b₁, b₂, b₃ being real number st 0 < b₁ & b₁ <= b₂ & b₃ >= 0 holds
b₁ to_power b₃ <= b₂ to_power b₃

proof end;

Lemma11: 2 to_power 2 = 4

proof end;

Lemma12: 2 to_power 3 = 8

proof end;

Lemma13: 2 to_power 4 = 16

proof end;

Lemma14: 2 to_power 5 = 32

proof end;

Lemma15: 2 to_power 6 = 64

proof end;

Lemma16: for b₁ being Nat st b₁ >= 4 holds
(2 * b₁) + 3 < 2 to_power b₁

proof end;

Lemma17: for b₁ being Nat st b₁ >= 6 holds
(b₁ + 1) ^2 < 2 to_power b₁

proof end;

Lemma18: for b₁ being Real st b₁ > 6 holds
b₁ ^2 < 2 to_power b₁

proof end;

Lemma19: for b₁ being positive Real
for b₂ being Real_Sequence st b₂ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₂ . b₃ = log 2,(b₃ to_power b₁) ) holds
( b₂ /" (seq_n^ b₁) is convergent & lim (b₂ /" (seq_n^ b₁)) = 0 )

proof end;

Lemma20: for b₁ being Real st b₁ > 0 holds
( seq_logn /" (seq_n^ b₁) is convergent & lim (seq_logn /" (seq_n^ b₁)) = 0 )

proof end;

theorem Th5: :: ASYMPT_1:5

( Big_Oh seq_logn c= Big_Oh (seq_n^ (1 / 2)) & not Big_Oh seq_logn = Big_Oh (seq_n^ (1 / 2)) )

proof end;

theorem Th6: :: ASYMPT_1:6

( seq_n^ (1 / 2) in Big_Omega seq_logn & not seq_logn in Big_Omega (seq_n^ (1 / 2)) )

proof end;

Lemma22: for b₁ being Real_Sequence
for b₂ being Nat st ( for b₃ being Nat st b₃ <= b₂ holds
b₁ . b₃ >= 0 ) holds
Sum b₁,b₂ >= 0

proof end;

Lemma23: for b₁, b₂ being Real_Sequence
for b₃ being Nat st ( for b₄ being Nat st b₄ <= b₃ holds
b₁ . b₄ <= b₂ . b₄ ) holds
Sum b₁,b₃ <= Sum b₂,b₃

proof end;

Lemma24: for b₁ being Real_Sequence
for b₂ being Real st b₁ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₁ . b₃ = b₂ ) holds
for b₃ being Nat holds Sum b₁,b₃ = b₂ * b₃

proof end;

Lemma25: for b₁ being Real_Sequence
for b₂, b₃ being Nat holds (Sum b₁,b₂,b₃) + (b₁ . (b₂ + 1)) = Sum b₁,(b₂ + 1),b₃

proof end;

Lemma26: for b₁, b₂ being Real_Sequence
for b₃, b₄ being Nat st b₄ >= b₃ + 1 & ( for b₅ being Nat st b₃ + 1 <= b₅ & b₅ <= b₄ holds
b₁ . b₅ <= b₂ . b₅ ) holds
Sum b₁,b₄,b₃ <= Sum b₂,b₄,b₃

proof end;

Lemma27: for b₁ being Nat holds [/(b₁ / 2)\] <= b₁

proof end;

Lemma28: for b₁ being Real_Sequence
for b₂ being Real
for b₃ being Nat st b₁ . 0 = 0 & ( for b₄ being Nat st b₄ > 0 holds
b₁ . b₄ = b₂ ) holds
for b₄ being Nat holds Sum b₁,b₃,b₄ = b₂ * (b₃ - b₄)

proof end;

theorem Th7: :: ASYMPT_1:7

for b₁ being Real_Sequence
for b₂ being Nat st ( for b₃ being Nat holds b₁ . b₃ = Sum (seq_n^ b₂),b₃ ) holds
b₁ in Big_Theta (seq_n^ (b₂ + 1))

proof end;

theorem Th8: :: ASYMPT_1:8

for b₁ being Real_Sequence st b₁ . 0 = 0 & ( for b₂ being Nat st b₂ > 0 holds
b₁ . b₂ = b₂ to_power (log 2,b₂) ) holds
ex b₂ being eventually-positive Real_Sequence st
( b₂ = b₁ & not b₂ is smooth )

proof end;

definition

let c₁ be Real;
func seq_const c₁ -> Real_Sequence equals :: ASYMPT_1:def 4
NAT --> a₁;
coherence

proof end;

end;

:: deftheorem Def4 defines seq_const ASYMPT_1:def 4 :

registration

cluster seq_const 1 -> eventually-nonnegative ;
coherence

proof end;

end;

Lemma29: for b₁, b₂, b₃ being Real st b₁ > 1 & b₂ >= b₁ & b₃ >= 1 holds
log b₁,b₃ >= log b₂,b₃

proof end;

theorem Th9: :: ASYMPT_1:9

for b₁ being eventually-nonnegative Real_Sequence ex b₂ being FUNCTION_DOMAIN of NAT , REAL st
( b₂ = {(seq_n^ 1)} & ( b₁ in b₂ to_power (Big_Oh (seq_const 1)) implies ex b₃ being Natex b₄ being Realex b₅ being Nat st
( b₄ > 0 & ( for b₆ being Nat st b₆ >= b₃ holds
( 1 <= b₁ . b₆ & b₁ . b₆ <= b₄ * ((seq_n^ b₅) . b₆) ) ) ) ) & ( ex b₃ being Natex b₄ being Realex b₅ being Nat st
( b₄ > 0 & ( for b₆ being Nat st b₆ >= b₃ holds
( 1 <= b₁ . b₆ & b₁ . b₆ <= b₄ * ((seq_n^ b₅) . b₆) ) ) ) implies b₁ in b₂ to_power (Big_Oh (seq_const 1)) ) )

proof end;

theorem Th10: :: ASYMPT_1:10

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = ((3 * (10 to_power 6)) - ((18 * (10 to_power 3)) * b₂)) + (27 * (b₂ ^2 )) ) holds
b₁ in Big_Oh (seq_n^ 2)

proof end;

theorem Th11: :: ASYMPT_1:11

seq_n^ 2 in Big_Oh (seq_n^ 3)

proof end;

theorem Th12: :: ASYMPT_1:12

not seq_n^ 2 in Big_Omega (seq_n^ 3)

proof end;

Lemma31: for b₁ being positive Real
for b₂, b₃ being Real holds seq_a^ b₁,b₂,b₃ is eventually-positive
;

theorem Th13: :: ASYMPT_1:13

ex b₁ being eventually-positive Real_Sequence st
( b₁ = seq_a^ 2,1,1 & seq_a^ 2,1,0 in Big_Theta b₁ )

proof end;

definition

let c₁ be Nat;
func seq_n! c₁ -> Real_Sequence means :Def5: :: ASYMPT_1:def 5
for b₁ being Nat holds a₂ . b₁ = (b₁ + a₁) ! ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines seq_n! ASYMPT_1:def 5 :

registration

let c₁ be Nat;
cluster seq_n! a₁ -> eventually-positive ;
coherence

proof end;

end;

theorem Th14: :: ASYMPT_1:14

not seq_n! 0 in Big_Theta (seq_n! 1)

proof end;

E33: now

let c₁, c₂, c₃, c₄ be Real;
assume ( 0 <= c₂ & c₁ <= c₂ & 0 <= c₃ & c₃ <= c₄ ) ;
then ( c₁ * c₃ <= c₂ * c₃ & c₂ * c₃ <= c₂ * c₄ ) by XREAL_1:66;
hence c₁ * c₃ <= c₂ * c₄ by XREAL_1:2;

end;

theorem Th15: :: ASYMPT_1:15

for b₁ being Real_Sequence st b₁ in Big_Oh (seq_n^ 1) holds
b₁ (#) b₁ in Big_Oh (seq_n^ 2)

proof end;

theorem Th16: :: ASYMPT_1:16

ex b₁ being eventually-positive Real_Sequence st
( b₁ = seq_a^ 2,1,0 & 2 (#) (seq_n^ 1) in Big_Oh (seq_n^ 1) & not seq_a^ 2,2,0 in Big_Oh b₁ )

proof end;

theorem Th17: :: ASYMPT_1:17

( log 2,3 < 159 / 100 implies ( seq_n^ (log 2,3) in Big_Oh (seq_n^ (159 / 100)) & not seq_n^ (log 2,3) in Big_Omega (seq_n^ (159 / 100)) & not seq_n^ (log 2,3) in Big_Theta (seq_n^ (159 / 100)) ) )

proof end;

theorem Th18: :: ASYMPT_1:18

for b₁, b₂ being Real_Sequence st ( for b₃ being Nat holds b₁ . b₃ = b₃ mod 2 ) & ( for b₃ being Nat holds b₂ . b₃ = (b₃ + 1) mod 2 ) holds
ex b₃, b₄ being eventually-nonnegative Real_Sequence st
( b₃ = b₁ & b₄ = b₂ & not b₃ in Big_Oh b₄ & not b₄ in Big_Oh b₃ )

proof end;

theorem Th19: :: ASYMPT_1:19

for b₁, b₂ being eventually-nonnegative Real_Sequence holds
( Big_Oh b₁ = Big_Oh b₂ iff b₁ in Big_Theta b₂ )

proof end;

theorem Th20: :: ASYMPT_1:20

for b₁, b₂ being eventually-nonnegative Real_Sequence holds
( b₁ in Big_Theta b₂ iff Big_Theta b₁ = Big_Theta b₂ )

proof end;

Lemma34: for b₁ being Nat holds ((b₁ ^2 ) - b₁) + 1 > 0

proof end;

Lemma35: for b₁, b₂ being Real_Sequence
for b₃ being Nat
for b₄ being Real st b₁ is convergent & lim b₁ = b₄ & ( for b₅ being Nat st b₅ >= b₃ holds
b₁ . b₅ = b₂ . b₅ ) holds
( b₂ is convergent & lim b₂ = b₄ )

proof end;

Lemma36: for b₁ being Nat st b₁ >= 1 holds
((b₁ ^2 ) - b₁) + 1 <= b₁ ^2

proof end;

Lemma37: for b₁ being Nat st b₁ >= 1 holds
b₁ ^2 <= 2 * (((b₁ ^2 ) - b₁) + 1)

proof end;

Lemma38: for b₁ being Real st 0 < b₁ & b₁ < 1 holds
ex b₂ being Nat st
for b₃ being Nat st b₃ >= b₂ holds
(b₃ * (log 2,(1 + b₁))) - (8 * (log 2,b₃)) > 8 * (log 2,b₃)

proof end;

theorem Th21: :: ASYMPT_1:21

for b₁ being Real
for b₂ being Real_Sequence st 0 < b₁ & b₂ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₂ . b₃ = b₃ * (log 2,b₃) ) holds
ex b₃ being eventually-positive Real_Sequence st
( b₃ = b₂ & Big_Oh b₃ c= Big_Oh (seq_n^ (1 + b₁)) & not Big_Oh b₃ = Big_Oh (seq_n^ (1 + b₁)) )

proof end;

theorem Th22: :: ASYMPT_1:22

for b₁ being Real
for b₂ being Real_Sequence st 0 < b₁ & b₁ < 1 & b₂ . 0 = 0 & b₂ . 1 = 0 & ( for b₃ being Nat st b₃ > 1 holds
b₂ . b₃ = (b₃ to_power 2) / (log 2,b₃) ) holds
ex b₃ being eventually-positive Real_Sequence st
( b₃ = b₂ & Big_Oh (seq_n^ (1 + b₁)) c= Big_Oh b₃ & not Big_Oh (seq_n^ (1 + b₁)) = Big_Oh b₃ )

proof end;

theorem Th23: :: ASYMPT_1:23

for b₁ being Real_Sequence st b₁ . 0 = 0 & b₁ . 1 = 0 & ( for b₂ being Nat st b₂ > 1 holds
b₁ . b₂ = (b₂ to_power 2) / (log 2,b₂) ) holds
ex b₂ being eventually-positive Real_Sequence st
( b₂ = b₁ & Big_Oh b₂ c= Big_Oh (seq_n^ 8) & not Big_Oh b₂ = Big_Oh (seq_n^ 8) )

proof end;

theorem Th24: :: ASYMPT_1:24

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = (((b₂ ^2 ) - b₂) + 1) to_power 4 ) holds
ex b₂ being eventually-positive Real_Sequence st
( b₂ = b₁ & Big_Oh (seq_n^ 8) = Big_Oh b₂ )

proof end;

theorem Th25: :: ASYMPT_1:25

for b₁ being Real st 0 < b₁ & b₁ < 1 holds
ex b₂ being eventually-positive Real_Sequence st
( b₂ = seq_a^ (1 + b₁),1,0 & Big_Oh (seq_n^ 8) c= Big_Oh b₂ & not Big_Oh (seq_n^ 8) = Big_Oh b₂ )

proof end;

Lemma39: 2 to_power 12 = 4096

proof end;

Lemma40: for b₁ being Nat st b₁ >= 3 holds
b₁ ^2 > (2 * b₁) + 1

proof end;

Lemma41: for b₁ being Nat st b₁ >= 10 holds
2 to_power (b₁ - 1) > (2 * b₁) ^2

proof end;

Lemma42: for b₁ being Nat st b₁ >= 9 holds
(b₁ + 1) to_power 6 < 2 * (b₁ to_power 6)

proof end;

Lemma43: for b₁ being Nat st b₁ >= 30 holds
2 to_power b₁ > b₁ to_power 6

proof end;

Lemma44: for b₁ being Real st b₁ > 9 holds
2 to_power b₁ > (2 * b₁) ^2

proof end;

Lemma45: ex b₁ being Nat st
for b₂ being Nat st b₂ >= b₁ holds
(sqrt b₂) - (log 2,b₂) > 1

proof end;

Lemma46: (4 + 1) ! = 120

proof end;

Lemma47: for b₁ being Nat st b₁ >= 10 holds
(2 to_power (2 * b₁)) / (b₁ ! ) < 1 / (2 to_power (b₁ - 9))

proof end;

Lemma48: for b₁ being Nat st b₁ >= 3 holds
2 * (b₁ - 2) >= b₁ - 1

proof end;

Lemma49: 5 to_power 5 = 3125

proof end;

Lemma50: 4 to_power 4 = 256

proof end;

Lemma51: for b₁, b₂, b₃, b₄ being Real holds (b₁ / b₂) / (b₃ / b₄) = (b₁ / b₃) * (b₄ / b₂)

proof end;

Lemma52: for b₁ being real number st b₁ >= 0 holds
sqrt b₁ = b₁ to_power (1 / 2)

proof end;

Lemma53: ex b₁ being Nat st
for b₂ being Nat st b₂ >= b₁ holds
b₂ - ((sqrt b₂) * (log 2,b₂)) > b₂ / 2

proof end;

Lemma54: for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = (1 + (1 / (b₂ + 1))) to_power (b₂ + 1) ) holds
b₁ is non-decreasing

proof end;

Lemma55: for b₁ being Nat st b₁ >= 1 holds
((b₁ + 1) / b₁) to_power b₁ <= ((b₁ + 2) / (b₁ + 1)) to_power (b₁ + 1)

proof end;

theorem Th26: :: ASYMPT_1:26

for b₁, b₂ being Real_Sequence st b₁ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₁ . b₃ = b₃ to_power (log 2,b₃) ) & b₂ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₂ . b₃ = b₃ to_power (sqrt b₃) ) holds
ex b₃, b₄ being eventually-positive Real_Sequence st
( b₃ = b₁ & b₄ = b₂ & Big_Oh b₃ c= Big_Oh b₄ & not Big_Oh b₃ = Big_Oh b₄ )

proof end;

theorem Th27: :: ASYMPT_1:27

for b₁ being Real_Sequence st b₁ . 0 = 0 & ( for b₂ being Nat st b₂ > 0 holds
b₁ . b₂ = b₂ to_power (sqrt b₂) ) holds
ex b₂, b₃ being eventually-positive Real_Sequence st
( b₂ = b₁ & b₃ = seq_a^ 2,1,0 & Big_Oh b₂ c= Big_Oh b₃ & not Big_Oh b₂ = Big_Oh b₃ )

proof end;

theorem Th28: :: ASYMPT_1:28

ex b₁, b₂ being eventually-positive Real_Sequence st
( b₁ = seq_a^ 2,1,0 & b₂ = seq_a^ 2,1,1 & Big_Oh b₁ = Big_Oh b₂ )

proof end;

theorem Th29: :: ASYMPT_1:29

ex b₁, b₂ being eventually-positive Real_Sequence st
( b₁ = seq_a^ 2,1,0 & b₂ = seq_a^ 2,2,0 & Big_Oh b₁ c= Big_Oh b₂ & not Big_Oh b₁ = Big_Oh b₂ )

proof end;

theorem Th30: :: ASYMPT_1:30

ex b₁ being eventually-positive Real_Sequence st
( b₁ = seq_a^ 2,2,0 & Big_Oh b₁ c= Big_Oh (seq_n! 0) & not Big_Oh b₁ = Big_Oh (seq_n! 0) )

proof end;

theorem Th31: :: ASYMPT_1:31

( Big_Oh (seq_n! 0) c= Big_Oh (seq_n! 1) & not Big_Oh (seq_n! 0) = Big_Oh (seq_n! 1) )

proof end;

theorem Th32: :: ASYMPT_1:32

for b₁ being Real_Sequence st b₁ . 0 = 0 & ( for b₂ being Nat st b₂ > 0 holds
b₁ . b₂ = b₂ to_power b₂ ) holds
ex b₂ being eventually-positive Real_Sequence st
( b₂ = b₁ & Big_Oh (seq_n! 1) c= Big_Oh b₂ & not Big_Oh (seq_n! 1) = Big_Oh b₂ )

proof end;

Lemma56: for b₁, b₂ being Nat st b₁ <= b₂ holds
b₂ choose b₁ >= ((b₂ + 1) choose b₁) / (b₂ + 1)

proof end;

theorem Th33: :: ASYMPT_1:33

for b₁ being Nat st b₁ >= 1 holds
for b₂ being Real_Sequence
for b₃ being Nat st ( for b₄ being Nat holds b₂ . b₄ = Sum (seq_n^ b₃),b₄ ) holds
b₂ . b₁ >= (b₁ to_power (b₃ + 1)) / (b₃ + 1)

proof end;

Lemma57: for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = log 2,(b₂ ! ) ) holds
for b₂ being Nat holds b₁ . b₂ = Sum seq_logn ,b₂

proof end;

Lemma58: for b₁ being Nat st b₁ >= 4 holds
b₁ * (log 2,b₁) >= 2 * b₁

proof end;

theorem Th34: :: ASYMPT_1:34

for b₁, b₂ being Real_Sequence st b₂ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₂ . b₃ = b₃ * (log 2,b₃) ) & ( for b₃ being Nat holds b₁ . b₃ = log 2,(b₃ ! ) ) holds
ex b₃ being eventually-nonnegative Real_Sequence st
( b₃ = b₂ & b₁ in Big_Theta b₃ )

proof end;

theorem Th35: :: ASYMPT_1:35

for b₁ being eventually-nonnegative eventually-nondecreasing Real_Sequence
for b₂ being Real_Sequence st ( for b₃ being Nat holds
( ( b₃ mod 2 = 0 implies b₂ . b₃ = 1 ) & ( b₃ mod 2 = 1 implies b₂ . b₃ = b₃ ) ) ) holds
not b₂ in Big_Theta b₁

proof end;

definition

let c₁ be Function of NAT ,REAL * ;
let c₂ be Nat;
redefine func . as c₁ . c₂ -> FinSequence of REAL ;
coherence

proof end;

end;

E59: now

let c₁, c₂ be positive Real;
reconsider c₃ = <*c₁*> as Element of REAL * by FINSEQ_1:def 11;
defpred S₁[ Nat, FinSequence of REAL , set ] means ex b₁ being Nat st
( b₁ = [/(((a₁ + 1) + 1) / 2)\] & a₃ = a₂ ^ <*((4 * (a₂ /. b₁)) + (c₂ * ((a₁ + 1) + 1)))*> );

E60: now

let c₄ be Nat;
let c₅ be Element of REAL * ;
reconsider c₆ = [/(((c₄ + 1) + 1) / 2)\] as Nat by INT_1:80;
consider c₇ being FinSequence of REAL such that
E61: c₇ = c₅ ^ <*((4 * (c₅ /. c₆)) + (c₂ * ((c₄ + 1) + 1)))*> ;
reconsider c₈ = c₇ as Element of REAL * by FINSEQ_1:def 11;
take c₉ = c₈;
thus S₁[c₄,c₅,c₉] by E61;

end;

consider c₄ being Function of NAT ,REAL * such that
E61: c₄ . 0 = c₃ and
E62: for b₁ being Nat holds S₁[b₁,c₄ . b₁,c₄ . (b₁ + 1)] from RECDEF_1:sch 2(E60);
take c₅ = c₄;
thus ( c₅ . 0 = <*c₁*> & ( for b₁ being Nat ex b₂ being Nat st
( b₂ = [/(((b₁ + 1) + 1) / 2)\] & c₅ . (b₁ + 1) = (c₅ . b₁) ^ <*((4 * ((c₅ . b₁) /. b₂)) + (c₂ * ((b₁ + 1) + 1)))*> ) ) ) by E61, E62;

end;

definition

let c₁ be Nat;
let c₂, c₃ be positive Real;
defpred S₁[ Nat, FinSequence of REAL , set ] means ex b₁ being Nat st
( b₁ = [/(((a₁ + 1) + 1) / 2)\] & a₃ = a₂ ^ <*((4 * (a₂ /. b₁)) + (c₃ * ((a₁ + 1) + 1)))*> );
E60: for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL * st S₁[b₁,b₂,b₃] & S₁[b₁,b₂,b₄] holds
b₃ = b₄ ;
func Prob28 c₁,c₂,c₃ -> Real means :Def6: :: ASYMPT_1:def 6
a₄ = 0 if a₁ = 0
otherwise ex b₁ being Natex b₂ being Function of NAT ,REAL * st
( b₁ + 1 = a₁ & a₄ = (b₂ . b₁) /. a₁ & b₂ . 0 = <*a₂*> & ( for b₃ being Nat ex b₄ being Nat st
( b₄ = [/(((b₃ + 1) + 1) / 2)\] & b₂ . (b₃ + 1) = (b₂ . b₃) ^ <*((4 * ((b₂ . b₃) /. b₄)) + (a₃ * ((b₃ + 1) + 1)))*> ) ) );
consistency ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Prob28 ASYMPT_1:def 6 :

definition

let c₁, c₂ be positive Real;
func seq_prob28 c₁,c₂ -> Real_Sequence means :Def7: :: ASYMPT_1:def 7
for b₁ being Nat holds a₃ . b₁ = Prob28 b₁,a₁,a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines seq_prob28 ASYMPT_1:def 7 :

Lemma62: for b₁ being Nat st b₁ >= 2 holds
[/(b₁ / 2)\] < b₁

proof end;

Lemma63: for b₁, b₂ being positive Real holds
( Prob28 0,b₁,b₂ = 0 & Prob28 1,b₁,b₂ = b₁ & ( for b₃ being Nat st b₃ >= 2 holds
ex b₄ being Nat st
( b₄ = [/(b₃ / 2)\] & Prob28 b₃,b₁,b₂ = (4 * (Prob28 b₄,b₁,b₂)) + (b₂ * b₃) ) ) )

proof end;

theorem Th36: :: ASYMPT_1:36

for b₁, b₂ being positive Real holds seq_prob28 b₁,b₂ is eventually-nondecreasing

proof end;

definition

func POWEROF2SET -> non empty Subset of NAT equals :: ASYMPT_1:def 8
{ (2 to_power b₁) where B is Nat : verum } ;
coherence

proof end;

end;

:: deftheorem Def8 defines POWEROF2SET ASYMPT_1:def 8 :

Lemma64: for b₁ being Nat st b₁ >= 2 holds
b₁ ^2 > b₁ + 1

proof end;

Lemma65: for b₁ being Nat st b₁ >= 1 holds
(2 to_power (b₁ + 1)) - (2 to_power b₁) > 1

proof end;

Lemma66: for b₁ being Nat st b₁ >= 2 holds
not (2 to_power b₁) - 1 in POWEROF2SET

proof end;

theorem Th37: :: ASYMPT_1:37

for b₁ being Real_Sequence st ( for b₂ being Nat holds
( ( b₂ in POWEROF2SET implies b₁ . b₂ = b₂ ) & ( not b₂ in POWEROF2SET implies b₁ . b₂ = 2 to_power b₂ ) ) ) holds
( b₁ in Big_Theta (seq_n^ 1),POWEROF2SET & not b₁ in Big_Theta (seq_n^ 1) & seq_n^ 1 is smooth & not b₁ is eventually-nondecreasing )

proof end;

theorem Th38: :: ASYMPT_1:38

for b₁, b₂ being Real_Sequence st b₁ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₁ . b₃ = b₃ to_power (2 to_power [\(log 2,b₃)/]) ) & b₂ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₂ . b₃ = b₃ to_power b₃ ) holds
ex b₃ being eventually-positive Real_Sequence st
( b₃ = b₂ & b₁ in Big_Theta b₃,POWEROF2SET & not b₁ in Big_Theta b₃ & b₁ is eventually-nondecreasing & b₃ is eventually-nondecreasing & not b₃ is_smooth_wrt 2 )

proof end;

theorem Th39: :: ASYMPT_1:39

for b₁ being Real_Sequence st ( for b₂ being Nat holds
( ( b₂ in POWEROF2SET implies b₁ . b₂ = b₂ ) & ( not b₂ in POWEROF2SET implies b₁ . b₂ = b₂ to_power 2 ) ) ) holds
ex b₂ being eventually-positive Real_Sequence st
( b₂ = b₁ & seq_n^ 1 in Big_Theta b₂,POWEROF2SET & not seq_n^ 1 in Big_Theta b₂ & b₂ taken_every 2 in Big_Oh b₂ & seq_n^ 1 is eventually-nondecreasing & not b₂ is eventually-nondecreasing )

proof end;

Lemma67: for b₁ being Nat st b₁ >= 2 holds
b₁ ! > 1

proof end;

Lemma68: for b₁, b₂ being Nat st b₂ <= b₁ holds
b₂ ! <= b₁ !

proof end;

Lemma69: for b₁ being Nat st b₁ >= 1 holds
ex b₂ being Nat st
( b₂ ! <= b₁ & b₁ < (b₂ + 1) ! & ( for b₃ being Nat st b₃ ! <= b₁ & b₁ < (b₃ + 1) ! holds
b₃ = b₂ ) )

proof end;

definition

let c₁ be Nat;
func Step1 c₁ -> Nat means :Def9: :: ASYMPT_1:def 9
ex b₁ being Nat st
( b₁ ! <= a₁ & a₁ < (b₁ + 1) ! & a₂ = b₁ ! ) if a₁ <> 0
otherwise a₂ = 0;
consistency ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Step1 ASYMPT_1:def 9 :

Lemma71: for b₁ being Nat st b₁ >= 3 holds
b₁ ! > b₁

proof end;

theorem Th40: :: ASYMPT_1:40

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = Step1 b₂ ) holds
ex b₂ being eventually-positive Real_Sequence st
( b₂ = b₁ & b₁ is eventually-nondecreasing & ( for b₃ being Nat holds b₁ . b₃ <= (seq_n^ 1) . b₃ ) & not b₂ is smooth )

proof end;

Lemma72: (seq_n^ 1) - (seq_const 1) is eventually-positive

proof end;

theorem Th41: :: ASYMPT_1:41

for b₁ being eventually-nonnegative Real_Sequence st b₁ = (seq_n^ 1) - (seq_const 1) holds
(Big_Theta b₁) + (Big_Theta (seq_n^ 1)) = Big_Theta (seq_n^ 1)

proof end;

theorem Th42: :: ASYMPT_1:42

ex b₁ being FUNCTION_DOMAIN of NAT , REAL st
( b₁ = {(seq_n^ 1)} & ( for b₂ being Nat holds (seq_n^ (- 1)) . b₂ <= (seq_n^ 1) . b₂ ) & not seq_n^ (- 1) in b₁ to_power (Big_Oh (seq_const 1)) )

proof end;

theorem Th43: :: ASYMPT_1:43

for b₁ being non negative Real
for b₂, b₃ being eventually-nonnegative Real_Sequence st ex b₄ being Realex b₅ being Nat st
( b₄ > 0 & ( for b₆ being Nat st b₆ >= b₅ holds
b₃ . b₆ >= b₄ ) ) & b₂ in Big_Oh (b₁ + b₃) holds
b₂ in Big_Oh b₃

proof end;

theorem Th44: :: ASYMPT_1:44

2 to_power 2 = 4 by Lemma11;

theorem Th45: :: ASYMPT_1:45

2 to_power 3 = 8 by Lemma12;

theorem Th46: :: ASYMPT_1:46

2 to_power 4 = 16 by Lemma13;

theorem Th47: :: ASYMPT_1:47

2 to_power 5 = 32 by Lemma14;

theorem Th48: :: ASYMPT_1:48

2 to_power 6 = 64 by Lemma15;

theorem Th49: :: ASYMPT_1:49

2 to_power 12 = 4096 by Lemma39;

theorem Th50: :: ASYMPT_1:50

for b₁ being Nat st b₁ >= 3 holds
b₁ ^2 > (2 * b₁) + 1 by Lemma40;

theorem Th51: :: ASYMPT_1:51

for b₁ being Nat st b₁ >= 10 holds
2 to_power (b₁ - 1) > (2 * b₁) ^2 by Lemma41;

theorem Th52: :: ASYMPT_1:52

for b₁ being Nat st b₁ >= 9 holds
(b₁ + 1) to_power 6 < 2 * (b₁ to_power 6) by Lemma42;

theorem Th53: :: ASYMPT_1:53

for b₁ being Nat st b₁ >= 30 holds
2 to_power b₁ > b₁ to_power 6 by Lemma43;

theorem Th54: :: ASYMPT_1:54

for b₁ being Real st b₁ > 9 holds
2 to_power b₁ > (2 * b₁) ^2 by Lemma44;

theorem Th55: :: ASYMPT_1:55

ex b₁ being Nat st
for b₂ being Nat st b₂ >= b₁ holds
(sqrt b₂) - (log 2,b₂) > 1 by Lemma45;

theorem Th56: :: ASYMPT_1:56

for b₁, b₂, b₃ being Real st b₁ > 0 & b₃ > 0 & b₃ <> 1 holds
b₁ to_power b₂ = b₃ to_power (b₂ * (log b₃,b₁)) by Lemma4;

theorem Th57: :: ASYMPT_1:57

(4 + 1) ! = 120 by Lemma46;

theorem Th58: :: ASYMPT_1:58

5 to_power 5 = 3125 by Lemma49;

theorem Th59: :: ASYMPT_1:59

4 to_power 4 = 256 by Lemma50;

theorem Th60: :: ASYMPT_1:60

for b₁ being Nat holds ((b₁ ^2 ) - b₁) + 1 > 0 by Lemma34;

theorem Th61: :: ASYMPT_1:61

for b₁ being Nat st b₁ >= 2 holds
b₁ ! > 1 by Lemma67;

theorem Th62: :: ASYMPT_1:62

for b₁, b₂ being Nat st b₂ <= b₁ holds
b₂ ! <= b₁ ! by Lemma68;

theorem Th63: :: ASYMPT_1:63

for b₁ being Nat st b₁ >= 1 holds
ex b₂ being Nat st
( b₂ ! <= b₁ & b₁ < (b₂ + 1) ! & ( for b₃ being Nat st b₃ ! <= b₁ & b₁ < (b₃ + 1) ! holds
b₃ = b₂ ) ) by Lemma69;

theorem Th64: :: ASYMPT_1:64

for b₁ being Nat st b₁ >= 2 holds
[/(b₁ / 2)\] < b₁ by Lemma62;

theorem Th65: :: ASYMPT_1:65

for b₁ being Nat st b₁ >= 3 holds
b₁ ! > b₁ by Lemma71;

theorem Th66: :: ASYMPT_1:66

(seq_n^ 1) - (seq_const 1) is eventually-positive by Lemma72;

theorem Th67: :: ASYMPT_1:67

for b₁ being Nat st b₁ >= 2 holds
2 to_power b₁ > b₁ + 1 by Lemma1;

theorem Th68: :: ASYMPT_1:68

for b₁ being logbase Real
for b₂ being Real_Sequence st b₁ > 1 & b₂ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₂ . b₃ = log b₁,b₃ ) holds
b₂ is eventually-positive by Lemma2;

theorem Th69: :: ASYMPT_1:69

for b₁, b₂ being eventually-nonnegative Real_Sequence holds
( ( b₁ in Big_Oh b₂ & b₂ in Big_Oh b₁ ) iff Big_Oh b₁ = Big_Oh b₂ ) by Lemma8;

theorem Th70: :: ASYMPT_1:70

for b₁, b₂, b₃ being Real st 0 < b₁ & b₁ <= b₂ & b₃ >= 0 holds
b₁ to_power b₃ <= b₂ to_power b₃ by Lemma10;

theorem Th71: :: ASYMPT_1:71

for b₁ being Nat st b₁ >= 4 holds
(2 * b₁) + 3 < 2 to_power b₁ by Lemma16;

theorem Th72: :: ASYMPT_1:72

for b₁ being Nat st b₁ >= 6 holds
(b₁ + 1) ^2 < 2 to_power b₁ by Lemma17;

theorem Th73: :: ASYMPT_1:73

for b₁ being Real st b₁ > 6 holds
b₁ ^2 < 2 to_power b₁ by Lemma18;

theorem Th74: :: ASYMPT_1:74

for b₁ being positive Real
for b₂ being Real_Sequence st b₂ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₂ . b₃ = log 2,(b₃ to_power b₁) ) holds
( b₂ /" (seq_n^ b₁) is convergent & lim (b₂ /" (seq_n^ b₁)) = 0 ) by Lemma19;

theorem Th75: :: ASYMPT_1:75

for b₁ being Real st b₁ > 0 holds
( seq_logn /" (seq_n^ b₁) is convergent & lim (seq_logn /" (seq_n^ b₁)) = 0 ) by Lemma20;

theorem Th76: :: ASYMPT_1:76

for b₁ being Real_Sequence
for b₂ being Nat st ( for b₃ being Nat st b₃ <= b₂ holds
b₁ . b₃ >= 0 ) holds
Sum b₁,b₂ >= 0 by Lemma22;

theorem Th77: :: ASYMPT_1:77

for b₁, b₂ being Real_Sequence
for b₃ being Nat st ( for b₄ being Nat st b₄ <= b₃ holds
b₁ . b₄ <= b₂ . b₄ ) holds
Sum b₁,b₃ <= Sum b₂,b₃ by Lemma23;

theorem Th78: :: ASYMPT_1:78

for b₁ being Real_Sequence
for b₂ being Real st b₁ . 0 = 0 & ( for b₃ being Nat st b₃ > 0 holds
b₁ . b₃ = b₂ ) holds
for b₃ being Nat holds Sum b₁,b₃ = b₂ * b₃ by Lemma24;

theorem Th79: :: ASYMPT_1:79

for b₁ being Real_Sequence
for b₂, b₃ being Nat holds (Sum b₁,b₂,b₃) + (b₁ . (b₂ + 1)) = Sum b₁,(b₂ + 1),b₃ by Lemma25;

theorem Th80: :: ASYMPT_1:80

for b₁, b₂ being Real_Sequence
for b₃, b₄ being Nat st b₄ >= b₃ + 1 & ( for b₅ being Nat st b₃ + 1 <= b₅ & b₅ <= b₄ holds
b₁ . b₅ <= b₂ . b₅ ) holds
Sum b₁,b₄,b₃ <= Sum b₂,b₄,b₃ by Lemma26;

theorem Th81: :: ASYMPT_1:81

for b₁ being Nat holds [/(b₁ / 2)\] <= b₁ by Lemma27;

theorem Th82: :: ASYMPT_1:82

for b₁ being Real_Sequence
for b₂ being Real
for b₃ being Nat st b₁ . 0 = 0 & ( for b₄ being Nat st b₄ > 0 holds
b₁ . b₄ = b₂ ) holds
for b₄ being Nat holds Sum b₁,b₃,b₄ = b₂ * (b₃ - b₄) by Lemma28;

theorem Th83: :: ASYMPT_1:83

for b₁, b₂ being Real_Sequence
for b₃ being Nat
for b₄ being Real st b₁ is convergent & lim b₁ = b₄ & ( for b₅ being Nat st b₅ >= b₃ holds
b₁ . b₅ = b₂ . b₅ ) holds
( b₂ is convergent & lim b₂ = b₄ ) by Lemma35;

theorem Th84: :: ASYMPT_1:84

for b₁ being Nat st b₁ >= 1 holds
((b₁ ^2 ) - b₁) + 1 <= b₁ ^2 by Lemma36;

theorem Th85: :: ASYMPT_1:85

for b₁ being Nat st b₁ >= 1 holds
b₁ ^2 <= 2 * (((b₁ ^2 ) - b₁) + 1) by Lemma37;

theorem Th86: :: ASYMPT_1:86

for b₁ being Real st 0 < b₁ & b₁ < 1 holds
ex b₂ being Nat st
for b₃ being Nat st b₃ >= b₂ holds
(b₃ * (log 2,(1 + b₁))) - (8 * (log 2,b₃)) > 8 * (log 2,b₃) by Lemma38;

theorem Th87: :: ASYMPT_1:87

for b₁ being Nat st b₁ >= 10 holds
(2 to_power (2 * b₁)) / (b₁ ! ) < 1 / (2 to_power (b₁ - 9)) by Lemma47;

theorem Th88: :: ASYMPT_1:88

for b₁ being Nat st b₁ >= 3 holds
2 * (b₁ - 2) >= b₁ - 1 by Lemma48;

theorem Th89: :: ASYMPT_1:89

for b₁ being real number st b₁ >= 0 holds
b₁ to_power (1 / 2) = sqrt b₁ by Lemma52;

theorem Th90: :: ASYMPT_1:90

ex b₁ being Nat st
for b₂ being Nat st b₂ >= b₁ holds
b₂ - ((sqrt b₂) * (log 2,b₂)) > b₂ / 2 by Lemma53;

theorem Th91: :: ASYMPT_1:91

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = (1 + (1 / (b₂ + 1))) to_power (b₂ + 1) ) holds
b₁ is non-decreasing by Lemma54;

theorem Th92: :: ASYMPT_1:92

for b₁ being Nat st b₁ >= 1 holds
((b₁ + 1) / b₁) to_power b₁ <= ((b₁ + 2) / (b₁ + 1)) to_power (b₁ + 1) by Lemma55;

theorem Th93: :: ASYMPT_1:93

for b₁, b₂ being Nat st b₁ <= b₂ holds
b₂ choose b₁ >= ((b₂ + 1) choose b₁) / (b₂ + 1) by Lemma56;

theorem Th94: :: ASYMPT_1:94

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = log 2,(b₂ ! ) ) holds
for b₂ being Nat holds b₁ . b₂ = Sum seq_logn ,b₂ by Lemma57;

theorem Th95: :: ASYMPT_1:95

for b₁ being Nat st b₁ >= 4 holds
b₁ * (log 2,b₁) >= 2 * b₁ by Lemma58;

theorem Th96: :: ASYMPT_1:96

for b₁, b₂ being positive Real holds
( Prob28 0,b₁,b₂ = 0 & Prob28 1,b₁,b₂ = b₁ & ( for b₃ being Nat st b₃ >= 2 holds
ex b₄ being Nat st
( b₄ = [/(b₃ / 2)\] & Prob28 b₃,b₁,b₂ = (4 * (Prob28 b₄,b₁,b₂)) + (b₂ * b₃) ) ) ) by Lemma63;

theorem Th97: :: ASYMPT_1:97

for b₁ being Nat st b₁ >= 2 holds
b₁ ^2 > b₁ + 1 by Lemma64;

theorem Th98: :: ASYMPT_1:98

for b₁ being Nat st b₁ >= 1 holds
(2 to_power (b₁ + 1)) - (2 to_power b₁) > 1 by Lemma65;

theorem Th99: :: ASYMPT_1:99

for b₁ being Nat st b₁ >= 2 holds
not (2 to_power b₁) - 1 in POWEROF2SET by Lemma66;

theorem Th100: :: ASYMPT_1:100

for b₁, b₂ being Nat st b₂ >= 1 & b₁ ! <= b₂ & b₂ < (b₁ + 1) ! holds
Step1 b₂ = b₁ ! by Def9;

theorem Th101: :: ASYMPT_1:101

for b₁, b₂, b₃ being Real st b₁ > 1 & b₂ >= b₁ & b₃ >= 1 holds
log b₁,b₃ >= log b₂,b₃ by Lemma29;