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 }