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 `( TopOpenw ) ) 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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-sitg | |- sitg = ( w e. _V , m e. U. ran measures |-> ( f e. { g e. ( dom m MblFnM ( sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( w gsum ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | csitg | |- sitg |
|
| 1 | vw | |- w |
|
| 2 | cvv | |- _V |
|
| 3 | vm | |- m |
|
| 4 | cmeas | |- measures |
|
| 5 | 4 | crn | |- ran measures |
| 6 | 5 | cuni | |- U. ran measures |
| 7 | vf | |- f |
|
| 8 | vg | |- g |
|
| 9 | 3 | cv | |- m |
| 10 | 9 | cdm | |- dom m |
| 11 | cmbfm | |- MblFnM |
|
| 12 | csigagen | |- sigaGen |
|
| 13 | ctopn | |- TopOpen |
|
| 14 | 1 | cv | |- w |
| 15 | 14 13 | cfv | |- ( TopOpen ` w ) |
| 16 | 15 12 | cfv | |- ( sigaGen ` ( TopOpen ` w ) ) |
| 17 | 10 16 11 | co | |- ( dom m MblFnM ( sigaGen ` ( TopOpen ` w ) ) ) |
| 18 | 8 | cv | |- g |
| 19 | 18 | crn | |- ran g |
| 20 | cfn | |- Fin |
|
| 21 | 19 20 | wcel | |- ran g e. Fin |
| 22 | vx | |- x |
|
| 23 | c0g | |- 0g |
|
| 24 | 14 23 | cfv | |- ( 0g ` w ) |
| 25 | 24 | csn | |- { ( 0g ` w ) } |
| 26 | 19 25 | cdif | |- ( ran g \ { ( 0g ` w ) } ) |
| 27 | 18 | ccnv | |- `' g |
| 28 | 22 | cv | |- x |
| 29 | 28 | csn | |- { x } |
| 30 | 27 29 | cima | |- ( `' g " { x } ) |
| 31 | 30 9 | cfv | |- ( m ` ( `' g " { x } ) ) |
| 32 | cc0 | |- 0 |
|
| 33 | cico | |- [,) |
|
| 34 | cpnf | |- +oo |
|
| 35 | 32 34 33 | co | |- ( 0 [,) +oo ) |
| 36 | 31 35 | wcel | |- ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) |
| 37 | 36 22 26 | wral | |- A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) |
| 38 | 21 37 | wa | |- ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) |
| 39 | 38 8 17 | crab | |- { g e. ( dom m MblFnM ( sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |
| 40 | cgsu | |- gsum |
|
| 41 | 7 | cv | |- f |
| 42 | 41 | crn | |- ran f |
| 43 | 42 25 | cdif | |- ( ran f \ { ( 0g ` w ) } ) |
| 44 | crrh | |- RRHom |
|
| 45 | csca | |- Scalar |
|
| 46 | 14 45 | cfv | |- ( Scalar ` w ) |
| 47 | 46 44 | cfv | |- ( RRHom ` ( Scalar ` w ) ) |
| 48 | 41 | ccnv | |- `' f |
| 49 | 48 29 | cima | |- ( `' f " { x } ) |
| 50 | 49 9 | cfv | |- ( m ` ( `' f " { x } ) ) |
| 51 | 50 47 | cfv | |- ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) |
| 52 | cvsca | |- .s |
|
| 53 | 14 52 | cfv | |- ( .s ` w ) |
| 54 | 51 28 53 | co | |- ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) |
| 55 | 22 43 54 | cmpt | |- ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) |
| 56 | 14 55 40 | co | |- ( w gsum ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) |
| 57 | 7 39 56 | cmpt | |- ( f e. { g e. ( dom m MblFnM ( sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( w gsum ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) ) |
| 58 | 1 3 2 6 57 | cmpo | |- ( w e. _V , m e. U. ran measures |-> ( f e. { g e. ( dom m MblFnM ( sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( w gsum ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) ) ) |
| 59 | 0 58 | wceq | |- sitg = ( w e. _V , m e. U. ran measures |-> ( f e. { g e. ( dom m MblFnM ( sigaGen ` ( TopOpen ` w ) ) ) | ( ran g e. Fin /\ A. x e. ( ran g \ { ( 0g ` w ) } ) ( m ` ( `' g " { x } ) ) e. ( 0 [,) +oo ) ) } |-> ( w gsum ( x e. ( ran f \ { ( 0g ` w ) } ) |-> ( ( ( RRHom ` ( Scalar ` w ) ) ` ( m ` ( `' f " { x } ) ) ) ( .s ` w ) x ) ) ) ) ) |