Definition df-sitm 30393

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.)

Assertion

Ref	Expression
df-sitm	|- sitm = ( w e. _V , m e. U. ran measures |-> ( f e. dom ( wsitg m ) , g e. dom ( wsitg m ) |-> ( ( ( RR*s ↾s ( 0 [,] +oo ) )sitg m ) ` ( f oF ( dist ` w ) g ) ) ) )

Distinct variable group:   f, g, m, w

Detailed syntax breakdown of Definition df-sitm

Step	Hyp	Ref	Expression
1		csitm 30390	. 2 class sitm
2		vw	. . 3 setvar w
3		vm	. . 3 setvar m
4		cvv 3200	. . 3 class _V
5		cmeas 30258	. . . . 5 class measures
6	5	crn 5115	. . . 4 class ran measures
7	6	cuni 4436	. . 3 class U. ran measures
8		vf	. . . 4 setvar f
9		vg	. . . 4 setvar g
10	2	cv 1482	. . . . . 6 class w
11	3	cv 1482	. . . . . 6 class m
12		csitg 30391	. . . . . 6 class sitg
13	10, 11, 12	co 6650	. . . . 5 class ( wsitg m )
14	13	cdm 5114	. . . 4 class dom ( wsitg m )
15	8	cv 1482	. . . . . 6 class f
16	9	cv 1482	. . . . . 6 class g
17		cds 15950	. . . . . . . 8 class dist
18	10, 17	cfv 5888	. . . . . . 7 class ( dist ` w )
19	18	cof 6895	. . . . . 6 class oF ( dist ` w )
20	15, 16, 19	co 6650	. . . . 5 class ( f oF ( dist ` w ) g )
21		cxrs 16160	. . . . . . 7 class RR*s
22		cc0 9936	. . . . . . . 8 class 0
23		cpnf 10071	. . . . . . . 8 class +oo
24		cicc 12178	. . . . . . . 8 class [,]
25	22, 23, 24	co 6650	. . . . . . 7 class ( 0 [,] +oo )
26		cress 15858	. . . . . . 7 class ↾s
27	21, 25, 26	co 6650	. . . . . 6 class ( RR*s ↾s ( 0 [,] +oo ) )
28	27, 11, 12	co 6650	. . . . 5 class ( ( RR*s ↾s ( 0 [,] +oo ) )sitg m )
29	20, 28	cfv 5888	. . . 4 class ( ( ( RR*s ↾s ( 0 [,] +oo ) )sitg m ) ` ( f oF ( dist ` w ) g ) )
30	8, 9, 14, 14, 29	cmpt2 6652	. . 3 class ( f e. dom ( wsitg m ) , g e. dom ( wsitg m ) |-> ( ( ( RR*s ↾s ( 0 [,] +oo ) )sitg m ) ` ( f oF ( dist ` w ) g ) ) )
31	2, 3, 4, 7, 30	cmpt2 6652	. 2 class ( w e. _V , m e. U. ran measures |-> ( f e. dom ( wsitg m ) , g e. dom ( wsitg m ) |-> ( ( ( RR*s ↾s ( 0 [,] +oo ) )sitg m ) ` ( f oF ( dist ` w ) g ) ) ) )
32	1, 31	wceq 1483	1 wff sitm = ( w e. _V , m e. U. ran measures |-> ( f e. dom ( wsitg m ) , g e. dom ( wsitg m ) |-> ( ( ( RR*s ↾s ( 0 [,] +oo ) )sitg m ) ` ( f oF ( dist ` w ) g ) ) ) )

This definition is referenced by:  sitmval  30411