Metamath Proof Explorer

Definition df-sitm

Description: Define the integral metric for simple functions, as the integral of the distances between the function values. Since distances take nonnegative values in RR* , the range structure for this integral is ` ( RR*s |``s ( 0 , +oo ) ) ` . See definition 2.3.1 of Bogachev p. 116. (Contributed by Thierry Arnoux, 22-Oct-2017)

Ref Expression
Assertion df-sitm ⊢ sitm = w ∈ V , m ∈ ⋃ ran ⁡ measures ⟼ f ∈ ℑ m w , g ∈ ℑ m w ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ w f g dm

Detailed syntax breakdown

Step Hyp Ref Expression
0 csitm class sitm
1 vw setvar w
2 cvv class V
3 vm setvar m
4 cmeas class measures
5 4 crn class ran ⁡ measures
6 5 cuni class ⋃ ran ⁡ measures
7 vf setvar f
8 1 cv setvar w
9 csitg class sitg
10 3 cv setvar m
11 8 10 9 co class w sitg m
12 11 cdm class ℑ m w
13 vg setvar g
14 cxrs class ℝ 𝑠 *
15 cress class ↾ 𝑠
16 cc0 class 0
17 cicc class .
18 cpnf class +∞
19 16 18 17 co class 0 +∞
20 14 19 15 co class ℝ 𝑠 * ↾ 𝑠 0 +∞
21 20 10 9 co class ℝ 𝑠 * ↾ 𝑠 0 +∞ sitg m
22 7 cv setvar f
23 cds class dist
24 8 23 cfv class dist ⁡ w
25 24 cof class ∘ f ⁡ dist ⁡ w
26 13 cv setvar g
27 22 26 25 co class f dist ⁡ w f g
28 27 21 cfv class ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ w f g dm
29 7 13 12 12 28 cmpo class f ∈ ℑ m w , g ∈ ℑ m w ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ w f g dm
30 1 3 2 6 29 cmpo class w ∈ V , m ∈ ⋃ ran ⁡ measures ⟼ f ∈ ℑ m w , g ∈ ℑ m w ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ w f g dm
31 0 30 wceq wff sitm = w ∈ V , m ∈ ⋃ ran ⁡ measures ⟼ f ∈ ℑ m w , g ∈ ℑ m w ⟼ ∫ ℑ ℝ 𝑠 * ↾ 𝑠 0 +∞ f dist ⁡ w f g dm