MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ibl Unicode version

Definition df-ibl 18978
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.)
Assertion
Ref Expression
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 }
Distinct variable group:    y, k, f, x

Detailed syntax breakdown of Definition df-ibl
StepHypRef Expression
1 cibl 18972 . 2  class  L ^1
2 vx . . . . . . 7  set  x
3 cr 8736 . . . . . . 7  class  RR
4 vy . . . . . . . 8  set  y
52cv 1622 . . . . . . . . . . 11  class  x
6 vf . . . . . . . . . . . 12  set  f
76cv 1622 . . . . . . . . . . 11  class  f
85, 7cfv 5255 . . . . . . . . . 10  class  ( f `
 x )
9 ci 8739 . . . . . . . . . . 11  class  _i
10 vk . . . . . . . . . . . 12  set  k
1110cv 1622 . . . . . . . . . . 11  class  k
12 cexp 11104 . . . . . . . . . . 11  class  ^
139, 11, 12co 5858 . . . . . . . . . 10  class  ( _i
^ k )
14 cdiv 9423 . . . . . . . . . 10  class  /
158, 13, 14co 5858 . . . . . . . . 9  class  ( ( f `  x )  /  ( _i ^
k ) )
16 cre 11582 . . . . . . . . 9  class  Re
1715, 16cfv 5255 . . . . . . . 8  class  ( Re
`  ( ( f `
 x )  / 
( _i ^ k
) ) )
187cdm 4689 . . . . . . . . . . 11  class  dom  f
195, 18wcel 1684 . . . . . . . . . 10  wff  x  e. 
dom  f
20 cc0 8737 . . . . . . . . . . 11  class  0
214cv 1622 . . . . . . . . . . 11  class  y
22 cle 8868 . . . . . . . . . . 11  class  <_
2320, 21, 22wbr 4023 . . . . . . . . . 10  wff  0  <_  y
2419, 23wa 358 . . . . . . . . 9  wff  ( x  e.  dom  f  /\  0  <_  y )
2524, 21, 20cif 3565 . . . . . . . 8  class  if ( ( x  e.  dom  f  /\  0  <_  y
) ,  y ,  0 )
264, 17, 25csb 3081 . . . . . . 7  class  [_ (
Re `  ( (
f `  x )  /  ( _i ^
k ) ) )  /  y ]_ if ( ( x  e. 
dom  f  /\  0  <_  y ) ,  y ,  0 )
272, 3, 26cmpt 4077 . . . . . 6  class  ( x  e.  RR  |->  [_ (
Re `  ( (
f `  x )  /  ( _i ^
k ) ) )  /  y ]_ if ( ( x  e. 
dom  f  /\  0  <_  y ) ,  y ,  0 ) )
28 citg2 18971 . . . . . 6  class  S.2
2927, 28cfv 5255 . . . . 5  class  ( S.2 `  ( x  e.  RR  |->  [_ ( Re `  (
( f `  x
)  /  ( _i
^ k ) ) )  /  y ]_ if ( ( x  e. 
dom  f  /\  0  <_  y ) ,  y ,  0 ) ) )
3029, 3wcel 1684 . . . 4  wff  ( S.2 `  ( x  e.  RR  |->  [_ ( Re `  (
( f `  x
)  /  ( _i
^ k ) ) )  /  y ]_ if ( ( x  e. 
dom  f  /\  0  <_  y ) ,  y ,  0 ) ) )  e.  RR
31 c3 9796 . . . . 5  class  3
32 cfz 10782 . . . . 5  class  ...
3320, 31, 32co 5858 . . . 4  class  ( 0 ... 3 )
3430, 10, 33wral 2543 . . 3  wff  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 cmbf 18969 . . 3  class MblFn
3634, 6, 35crab 2547 . 2  class  { 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 }
371, 36wceq 1623 1  wff  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 }
Colors of variables: wff set class
This definition is referenced by:  isibl  19120  iblmbf  19122
  Copyright terms: Public domain W3C validator