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 = ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | csitg | ⊢ sitg | |
1 | vw | ⊢ 𝑤 | |
2 | cvv | ⊢ V | |
3 | vm | ⊢ 𝑚 | |
4 | cmeas | ⊢ measures | |
5 | 4 | crn | ⊢ ran measures |
6 | 5 | cuni | ⊢ ∪ ran measures |
7 | vf | ⊢ 𝑓 | |
8 | vg | ⊢ 𝑔 | |
9 | 3 | cv | ⊢ 𝑚 |
10 | 9 | cdm | ⊢ dom 𝑚 |
11 | cmbfm | ⊢ MblFnM | |
12 | csigagen | ⊢ sigaGen | |
13 | ctopn | ⊢ TopOpen | |
14 | 1 | cv | ⊢ 𝑤 |
15 | 14 13 | cfv | ⊢ ( TopOpen ‘ 𝑤 ) |
16 | 15 12 | cfv | ⊢ ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) |
17 | 10 16 11 | co | ⊢ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) |
18 | 8 | cv | ⊢ 𝑔 |
19 | 18 | crn | ⊢ ran 𝑔 |
20 | cfn | ⊢ Fin | |
21 | 19 20 | wcel | ⊢ ran 𝑔 ∈ Fin |
22 | vx | ⊢ 𝑥 | |
23 | c0g | ⊢ 0g | |
24 | 14 23 | cfv | ⊢ ( 0g ‘ 𝑤 ) |
25 | 24 | csn | ⊢ { ( 0g ‘ 𝑤 ) } |
26 | 19 25 | cdif | ⊢ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) |
27 | 18 | ccnv | ⊢ ◡ 𝑔 |
28 | 22 | cv | ⊢ 𝑥 |
29 | 28 | csn | ⊢ { 𝑥 } |
30 | 27 29 | cima | ⊢ ( ◡ 𝑔 “ { 𝑥 } ) |
31 | 30 9 | cfv | ⊢ ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) |
32 | cc0 | ⊢ 0 | |
33 | cico | ⊢ [,) | |
34 | cpnf | ⊢ +∞ | |
35 | 32 34 33 | co | ⊢ ( 0 [,) +∞ ) |
36 | 31 35 | wcel | ⊢ ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) |
37 | 36 22 26 | wral | ⊢ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) |
38 | 21 37 | wa | ⊢ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) |
39 | 38 8 17 | crab | ⊢ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } |
40 | cgsu | ⊢ Σg | |
41 | 7 | cv | ⊢ 𝑓 |
42 | 41 | crn | ⊢ ran 𝑓 |
43 | 42 25 | cdif | ⊢ ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) |
44 | crrh | ⊢ ℝHom | |
45 | csca | ⊢ Scalar | |
46 | 14 45 | cfv | ⊢ ( Scalar ‘ 𝑤 ) |
47 | 46 44 | cfv | ⊢ ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) |
48 | 41 | ccnv | ⊢ ◡ 𝑓 |
49 | 48 29 | cima | ⊢ ( ◡ 𝑓 “ { 𝑥 } ) |
50 | 49 9 | cfv | ⊢ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) |
51 | 50 47 | cfv | ⊢ ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) |
52 | cvsca | ⊢ ·𝑠 | |
53 | 14 52 | cfv | ⊢ ( ·𝑠 ‘ 𝑤 ) |
54 | 51 28 53 | co | ⊢ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) |
55 | 22 43 54 | cmpt | ⊢ ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ) |
56 | 14 55 40 | co | ⊢ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ) ) |
57 | 7 39 56 | cmpt | ⊢ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ) ) ) |
58 | 1 3 2 6 57 | cmpo | ⊢ ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ) ) ) ) |
59 | 0 58 | wceq | ⊢ sitg = ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( 𝑓 ∈ { 𝑔 ∈ ( dom 𝑚 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝑤 ) ) ) ∣ ( ran 𝑔 ∈ Fin ∧ ∀ 𝑥 ∈ ( ran 𝑔 ∖ { ( 0g ‘ 𝑤 ) } ) ( 𝑚 ‘ ( ◡ 𝑔 “ { 𝑥 } ) ) ∈ ( 0 [,) +∞ ) ) } ↦ ( 𝑤 Σg ( 𝑥 ∈ ( ran 𝑓 ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( ( ℝHom ‘ ( Scalar ‘ 𝑤 ) ) ‘ ( 𝑚 ‘ ( ◡ 𝑓 “ { 𝑥 } ) ) ) ( ·𝑠 ‘ 𝑤 ) 𝑥 ) ) ) ) ) |