Metamath Proof Explorer

Definition df-ibl

Description: Define the class of integrable functions on the reals. A function is integrable if it is measurable and the integrals of the pieces of the function are all finite. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion df-ibl 
|- L^1 = { f e. MblFn | A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cibl 
 |-  L^1
1 vf 
 |-  f
2 cmbf 
 |-  MblFn
3 vk 
 |-  k
4 cc0 
 |-  0
5 cfz 
 |-  ...
6 c3 
 |-  3
7 4 6 5 co 
 |-  ( 0 ... 3 )
8 citg2 
 |-  S.2
9 vx 
 |-  x
10 cr 
 |-  RR
11 cre 
 |-  Re
12 1 cv 
 |-  f
13 9 cv 
 |-  x
14 13 12 cfv 
 |-  ( f ` x )
15 cdiv 
 |-  /
16 ci 
 |-  _i
17 cexp 
 |-  ^
18 3 cv 
 |-  k
19 16 18 17 co 
 |-  ( _i ^ k )
20 14 19 15 co 
 |-  ( ( f ` x ) / ( _i ^ k ) )
21 20 11 cfv 
 |-  ( Re ` ( ( f ` x ) / ( _i ^ k ) ) )
22 vy 
 |-  y
23 12 cdm 
 |-  dom f
24 13 23 wcel 
 |-  x e. dom f
25 cle 
 |-  <_
26 22 cv 
 |-  y
27 4 26 25 wbr 
 |-  0 <_ y
28 24 27 wa 
 |-  ( x e. dom f /\ 0 <_ y )
29 28 26 4 cif 
 |-  if ( ( x e. dom f /\ 0 <_ y ) , y , 0 )
30 22 21 29 csb 
 |-  [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 )
31 9 10 30 cmpt 
 |-  ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) )
32 31 8 cfv 
 |-  ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) )
33 32 10 wcel 
 |-  ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR
34 33 3 7 wral 
 |-  A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR
35 34 1 2 crab 
 |-  { f e. MblFn | A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR }
36 0 35 wceq 
 |-  L^1 = { f e. MblFn | A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR }