Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sitg Structured version   Unicode version

Definition df-sitg 28023
Description: Define the integral of simple functions from a measurable space  dom  m to a generic space  w equipped with the right scalar product.  w will later be required to be a Banach space.

These simple functions are required to take finitely many different values: this is expressed by  ran  g  e.  Fin in the definition.

Moreover, for each  x, the pre-image  ( `' g " { x } ) is requested to be measurable, of finite measure.

In this definition,  (sigaGen `  ( TopOpen `  w
) ) is the Borel sigma-algebra on  w, and the functions  g range over the measurable functions over that Borel algebra.

Definition 2.4.1 of [Bogachev] p. 118. (Contributed by Thierry Arnoux, 21-Oct-2017.)

Assertion
Ref Expression
df-sitg  |- sitg  =  ( w  e.  _V ,  m  e.  U. ran measures  |->  ( f  e.  { g  e.  ( dom  mMblFnM (sigaGen `  ( TopOpen `  w )
) )  |  ( ran  g  e.  Fin  /\ 
A. x  e.  ( ran  g  \  {
( 0g `  w
) } ) ( m `  ( `' g " { x } ) )  e.  ( 0 [,) +oo ) ) }  |->  ( w  gsumg  ( x  e.  ( ran  f  \  {
( 0g `  w
) } )  |->  ( ( (RRHom `  (Scalar `  w ) ) `  ( m `  ( `' f " {
x } ) ) ) ( .s `  w ) x ) ) ) ) )
Distinct variable group:    f, g, m, w, x

Detailed syntax breakdown of Definition df-sitg
StepHypRef Expression
1 csitg 28022 . 2  class sitg
2 vw . . 3  setvar  w
3 vm . . 3  setvar  m
4 cvv 3113 . . 3  class  _V
5 cmeas 27917 . . . . 5  class measures
65crn 5000 . . . 4  class  ran measures
76cuni 4245 . . 3  class  U. ran measures
8 vf . . . 4  setvar  f
9 vg . . . . . . . . 9  setvar  g
109cv 1378 . . . . . . . 8  class  g
1110crn 5000 . . . . . . 7  class  ran  g
12 cfn 7517 . . . . . . 7  class  Fin
1311, 12wcel 1767 . . . . . 6  wff  ran  g  e.  Fin
1410ccnv 4998 . . . . . . . . . 10  class  `' g
15 vx . . . . . . . . . . . 12  setvar  x
1615cv 1378 . . . . . . . . . . 11  class  x
1716csn 4027 . . . . . . . . . 10  class  { x }
1814, 17cima 5002 . . . . . . . . 9  class  ( `' g " { x } )
193cv 1378 . . . . . . . . 9  class  m
2018, 19cfv 5588 . . . . . . . 8  class  ( m `
 ( `' g
" { x }
) )
21 cc0 9493 . . . . . . . . 9  class  0
22 cpnf 9626 . . . . . . . . 9  class +oo
23 cico 11532 . . . . . . . . 9  class  [,)
2421, 22, 23co 6285 . . . . . . . 8  class  ( 0 [,) +oo )
2520, 24wcel 1767 . . . . . . 7  wff  ( m `
 ( `' g
" { x }
) )  e.  ( 0 [,) +oo )
262cv 1378 . . . . . . . . . 10  class  w
27 c0g 14698 . . . . . . . . . 10  class  0g
2826, 27cfv 5588 . . . . . . . . 9  class  ( 0g
`  w )
2928csn 4027 . . . . . . . 8  class  { ( 0g `  w ) }
3011, 29cdif 3473 . . . . . . 7  class  ( ran  g  \  { ( 0g `  w ) } )
3125, 15, 30wral 2814 . . . . . 6  wff  A. x  e.  ( ran  g  \  { ( 0g `  w ) } ) ( m `  ( `' g " {
x } ) )  e.  ( 0 [,) +oo )
3213, 31wa 369 . . . . 5  wff  ( ran  g  e.  Fin  /\  A. x  e.  ( ran  g  \  { ( 0g `  w ) } ) ( m `
 ( `' g
" { x }
) )  e.  ( 0 [,) +oo )
)
3319cdm 4999 . . . . . 6  class  dom  m
34 ctopn 14680 . . . . . . . 8  class  TopOpen
3526, 34cfv 5588 . . . . . . 7  class  ( TopOpen `  w )
36 csigagen 27889 . . . . . . 7  class sigaGen
3735, 36cfv 5588 . . . . . 6  class  (sigaGen `  ( TopOpen
`  w ) )
38 cmbfm 27972 . . . . . 6  class MblFnM
3933, 37, 38co 6285 . . . . 5  class  ( dom  mMblFnM (sigaGen `  ( TopOpen `  w
) ) )
4032, 9, 39crab 2818 . . . 4  class  { g  e.  ( dom  mMblFnM (sigaGen `  ( TopOpen `  w
) ) )  |  ( ran  g  e. 
Fin  /\  A. x  e.  ( ran  g  \  { ( 0g `  w ) } ) ( m `  ( `' g " {
x } ) )  e.  ( 0 [,) +oo ) ) }
418cv 1378 . . . . . . . 8  class  f
4241crn 5000 . . . . . . 7  class  ran  f
4342, 29cdif 3473 . . . . . 6  class  ( ran  f  \  { ( 0g `  w ) } )
4441ccnv 4998 . . . . . . . . . 10  class  `' f
4544, 17cima 5002 . . . . . . . . 9  class  ( `' f " { x } )
4645, 19cfv 5588 . . . . . . . 8  class  ( m `
 ( `' f
" { x }
) )
47 csca 14561 . . . . . . . . . 10  class Scalar
4826, 47cfv 5588 . . . . . . . . 9  class  (Scalar `  w )
49 crrh 27725 . . . . . . . . 9  class RRHom
5048, 49cfv 5588 . . . . . . . 8  class  (RRHom `  (Scalar `  w ) )
5146, 50cfv 5588 . . . . . . 7  class  ( (RRHom `  (Scalar `  w )
) `  ( m `  ( `' f " { x } ) ) )
52 cvsca 14562 . . . . . . . 8  class  .s
5326, 52cfv 5588 . . . . . . 7  class  ( .s
`  w )
5451, 16, 53co 6285 . . . . . 6  class  ( ( (RRHom `  (Scalar `  w
) ) `  (
m `  ( `' f " { x }
) ) ) ( .s `  w ) x )
5515, 43, 54cmpt 4505 . . . . 5  class  ( x  e.  ( ran  f  \  { ( 0g `  w ) } ) 
|->  ( ( (RRHom `  (Scalar `  w ) ) `
 ( m `  ( `' f " {
x } ) ) ) ( .s `  w ) x ) )
56 cgsu 14699 . . . . 5  class  gsumg
5726, 55, 56co 6285 . . . 4  class  ( w 
gsumg  ( x  e.  ( ran  f  \  { ( 0g `  w ) } )  |->  ( ( (RRHom `  (Scalar `  w
) ) `  (
m `  ( `' f " { x }
) ) ) ( .s `  w ) x ) ) )
588, 40, 57cmpt 4505 . . 3  class  ( f  e.  { g  e.  ( dom  mMblFnM (sigaGen `  ( TopOpen `  w )
) )  |  ( ran  g  e.  Fin  /\ 
A. x  e.  ( ran  g  \  {
( 0g `  w
) } ) ( m `  ( `' g " { x } ) )  e.  ( 0 [,) +oo ) ) }  |->  ( w  gsumg  ( x  e.  ( ran  f  \  {
( 0g `  w
) } )  |->  ( ( (RRHom `  (Scalar `  w ) ) `  ( m `  ( `' f " {
x } ) ) ) ( .s `  w ) x ) ) ) )
592, 3, 4, 7, 58cmpt2 6287 . 2  class  ( w  e.  _V ,  m  e.  U. ran measures  |->  ( f  e.  { g  e.  ( dom  mMblFnM (sigaGen `  ( TopOpen
`  w ) ) )  |  ( ran  g  e.  Fin  /\  A. x  e.  ( ran  g  \  { ( 0g `  w ) } ) ( m `
 ( `' g
" { x }
) )  e.  ( 0 [,) +oo )
) }  |->  ( w 
gsumg  ( x  e.  ( ran  f  \  { ( 0g `  w ) } )  |->  ( ( (RRHom `  (Scalar `  w
) ) `  (
m `  ( `' f " { x }
) ) ) ( .s `  w ) x ) ) ) ) )
601, 59wceq 1379 1  wff sitg  =  ( w  e.  _V ,  m  e.  U. ran measures  |->  ( f  e.  { g  e.  ( dom  mMblFnM (sigaGen `  ( TopOpen `  w )
) )  |  ( ran  g  e.  Fin  /\ 
A. x  e.  ( ran  g  \  {
( 0g `  w
) } ) ( m `  ( `' g " { x } ) )  e.  ( 0 [,) +oo ) ) }  |->  ( w  gsumg  ( x  e.  ( ran  f  \  {
( 0g `  w
) } )  |->  ( ( (RRHom `  (Scalar `  w ) ) `  ( m `  ( `' f " {
x } ) ) ) ( .s `  w ) x ) ) ) ) )
Colors of variables: wff setvar class
This definition is referenced by:  sitgval  28025
  Copyright terms: Public domain W3C validator