Description: Define the Bochner integral as the extension by continuity of the Bochnel integral for simple functions.
Bogachev first defines 'fundamental in the mean' sequences, in definition 2.3.1 of Bogachev p. 116, and notes that those are actually Cauchy sequences for the pseudometric ( w sitm m ) .
He then defines the Bochner integral in chapter 2.4.4 in Bogachev p. 118. The definition of the Lebesgue integral, df-itg .
(Contributed by Thierry Arnoux, 13-Feb-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-itgm | ⊢ itgm = ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( ( ( metUnif ‘ ( 𝑤 sitm 𝑚 ) ) CnExt ( UnifSt ‘ 𝑤 ) ) ‘ ( 𝑤 sitg 𝑚 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | citgm | ⊢ itgm | |
| 1 | vw | ⊢ 𝑤 | |
| 2 | cvv | ⊢ V | |
| 3 | vm | ⊢ 𝑚 | |
| 4 | cmeas | ⊢ measures | |
| 5 | 4 | crn | ⊢ ran measures |
| 6 | 5 | cuni | ⊢ ∪ ran measures |
| 7 | cmetu | ⊢ metUnif | |
| 8 | 1 | cv | ⊢ 𝑤 |
| 9 | csitm | ⊢ sitm | |
| 10 | 3 | cv | ⊢ 𝑚 |
| 11 | 8 10 9 | co | ⊢ ( 𝑤 sitm 𝑚 ) |
| 12 | 11 7 | cfv | ⊢ ( metUnif ‘ ( 𝑤 sitm 𝑚 ) ) |
| 13 | ccnext | ⊢ CnExt | |
| 14 | cuss | ⊢ UnifSt | |
| 15 | 8 14 | cfv | ⊢ ( UnifSt ‘ 𝑤 ) |
| 16 | 12 15 13 | co | ⊢ ( ( metUnif ‘ ( 𝑤 sitm 𝑚 ) ) CnExt ( UnifSt ‘ 𝑤 ) ) |
| 17 | csitg | ⊢ sitg | |
| 18 | 8 10 17 | co | ⊢ ( 𝑤 sitg 𝑚 ) |
| 19 | 18 16 | cfv | ⊢ ( ( ( metUnif ‘ ( 𝑤 sitm 𝑚 ) ) CnExt ( UnifSt ‘ 𝑤 ) ) ‘ ( 𝑤 sitg 𝑚 ) ) |
| 20 | 1 3 2 6 19 | cmpo | ⊢ ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( ( ( metUnif ‘ ( 𝑤 sitm 𝑚 ) ) CnExt ( UnifSt ‘ 𝑤 ) ) ‘ ( 𝑤 sitg 𝑚 ) ) ) |
| 21 | 0 20 | wceq | ⊢ itgm = ( 𝑤 ∈ V , 𝑚 ∈ ∪ ran measures ↦ ( ( ( metUnif ‘ ( 𝑤 sitm 𝑚 ) ) CnExt ( UnifSt ‘ 𝑤 ) ) ‘ ( 𝑤 sitg 𝑚 ) ) ) |