Metamath Proof Explorer

Definition df-bigo

Description: Define the function "big-O", mapping a real function g to the set of real functions "of order g(x)". Definition in section 1.1 of AhoHopUll p. 2. This is a generalization of "big-O of one", see df-o1 and df-lo1 . As explained in the comment of df-o1 , any big-O can be represented in terms of O(1) and division, see elbigolo1 . (Contributed by AV, 15-May-2020)

Ref Expression
Assertion df-bigo 
|- _O = ( g e. ( RR ^pm RR ) |-> { f e. ( RR ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cbigo 
 |-  _O
1 vg 
 |-  g
2 cr 
 |-  RR
3 cpm 
 |-  ^pm
4 2 2 3 co 
 |-  ( RR ^pm RR )
5 vf 
 |-  f
6 vx 
 |-  x
7 vm 
 |-  m
8 vy 
 |-  y
9 5 cv 
 |-  f
10 9 cdm 
 |-  dom f
11 6 cv 
 |-  x
12 cico 
 |-  [,)
13 cpnf 
 |-  +oo
14 11 13 12 co 
 |-  ( x [,) +oo )
15 10 14 cin 
 |-  ( dom f i^i ( x [,) +oo ) )
16 8 cv 
 |-  y
17 16 9 cfv 
 |-  ( f ` y )
18 cle 
 |-  <_
19 7 cv 
 |-  m
20 cmul 
 |-  x.
21 1 cv 
 |-  g
22 16 21 cfv 
 |-  ( g ` y )
23 19 22 20 co 
 |-  ( m x. ( g ` y ) )
24 17 23 18 wbr 
 |-  ( f ` y ) <_ ( m x. ( g ` y ) )
25 24 8 15 wral 
 |-  A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) )
26 25 7 2 wrex 
 |-  E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) )
27 26 6 2 wrex 
 |-  E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) )
28 27 5 4 crab 
 |-  { f e. ( RR ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) ) }
29 1 4 28 cmpt 
 |-  ( g e. ( RR ^pm RR ) |-> { f e. ( RR ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) ) } )
30 0 29 wceq 
 |-  _O = ( g e. ( RR ^pm RR ) |-> { f e. ( RR ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) ) } )