Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sitg Structured version   Visualization version   GIF version

Definition df-sitg 31867
Description: Define the integral of simple functions from a measurable space dom 𝑚 to a generic space 𝑤 equipped with the right scalar product. 𝑤 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 𝑔 ∈ Fin in the definition.

Moreover, for each 𝑥, the pre-image (𝑔 “ {𝑥}) is requested to be measurable, of finite measure.

In this definition, (sigaGen‘(TopOpen‘𝑤)) is the Borel sigma-algebra on 𝑤, and the functions 𝑔 range over the measurable functions over that Borel algebra.

Definition 2.4.1 of [Bogachev] p. 118. (Contributed by Thierry Arnoux, 21-Oct-2017.)

Assertion
Ref Expression
df-sitg sitg = (𝑤 ∈ V, 𝑚 ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))))
Distinct variable group:   𝑓,𝑔,𝑚,𝑤,𝑥

Detailed syntax breakdown of Definition df-sitg
StepHypRef Expression
1 csitg 31866 . 2 class sitg
2 vw . . 3 setvar 𝑤
3 vm . . 3 setvar 𝑚
4 cvv 3398 . . 3 class V
5 cmeas 31733 . . . . 5 class measures
65crn 5526 . . . 4 class ran measures
76cuni 4796 . . 3 class ran measures
8 vf . . . 4 setvar 𝑓
9 vg . . . . . . . . 9 setvar 𝑔
109cv 1541 . . . . . . . 8 class 𝑔
1110crn 5526 . . . . . . 7 class ran 𝑔
12 cfn 8555 . . . . . . 7 class Fin
1311, 12wcel 2114 . . . . . 6 wff ran 𝑔 ∈ Fin
1410ccnv 5524 . . . . . . . . . 10 class 𝑔
15 vx . . . . . . . . . . . 12 setvar 𝑥
1615cv 1541 . . . . . . . . . . 11 class 𝑥
1716csn 4516 . . . . . . . . . 10 class {𝑥}
1814, 17cima 5528 . . . . . . . . 9 class (𝑔 “ {𝑥})
193cv 1541 . . . . . . . . 9 class 𝑚
2018, 19cfv 6339 . . . . . . . 8 class (𝑚‘(𝑔 “ {𝑥}))
21 cc0 10615 . . . . . . . . 9 class 0
22 cpnf 10750 . . . . . . . . 9 class +∞
23 cico 12823 . . . . . . . . 9 class [,)
2421, 22, 23co 7170 . . . . . . . 8 class (0[,)+∞)
2520, 24wcel 2114 . . . . . . 7 wff (𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)
262cv 1541 . . . . . . . . . 10 class 𝑤
27 c0g 16816 . . . . . . . . . 10 class 0g
2826, 27cfv 6339 . . . . . . . . 9 class (0g𝑤)
2928csn 4516 . . . . . . . 8 class {(0g𝑤)}
3011, 29cdif 3840 . . . . . . 7 class (ran 𝑔 ∖ {(0g𝑤)})
3125, 15, 30wral 3053 . . . . . 6 wff 𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)
3213, 31wa 399 . . . . 5 wff (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))
3319cdm 5525 . . . . . 6 class dom 𝑚
34 ctopn 16798 . . . . . . . 8 class TopOpen
3526, 34cfv 6339 . . . . . . 7 class (TopOpen‘𝑤)
36 csigagen 31676 . . . . . . 7 class sigaGen
3735, 36cfv 6339 . . . . . 6 class (sigaGen‘(TopOpen‘𝑤))
38 cmbfm 31787 . . . . . 6 class MblFnM
3933, 37, 38co 7170 . . . . 5 class (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤)))
4032, 9, 39crab 3057 . . . 4 class {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))}
418cv 1541 . . . . . . . 8 class 𝑓
4241crn 5526 . . . . . . 7 class ran 𝑓
4342, 29cdif 3840 . . . . . 6 class (ran 𝑓 ∖ {(0g𝑤)})
4441ccnv 5524 . . . . . . . . . 10 class 𝑓
4544, 17cima 5528 . . . . . . . . 9 class (𝑓 “ {𝑥})
4645, 19cfv 6339 . . . . . . . 8 class (𝑚‘(𝑓 “ {𝑥}))
47 csca 16671 . . . . . . . . . 10 class Scalar
4826, 47cfv 6339 . . . . . . . . 9 class (Scalar‘𝑤)
49 crrh 31513 . . . . . . . . 9 class ℝHom
5048, 49cfv 6339 . . . . . . . 8 class (ℝHom‘(Scalar‘𝑤))
5146, 50cfv 6339 . . . . . . 7 class ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))
52 cvsca 16672 . . . . . . . 8 class ·𝑠
5326, 52cfv 6339 . . . . . . 7 class ( ·𝑠𝑤)
5451, 16, 53co 7170 . . . . . 6 class (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)
5515, 43, 54cmpt 5110 . . . . 5 class (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥))
56 cgsu 16817 . . . . 5 class Σg
5726, 55, 56co 7170 . . . 4 class (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))
588, 40, 57cmpt 5110 . . 3 class (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥))))
592, 3, 4, 7, 58cmpo 7172 . 2 class (𝑤 ∈ V, 𝑚 ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))))
601, 59wceq 1542 1 wff sitg = (𝑤 ∈ V, 𝑚 ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))))
Colors of variables: wff setvar class
This definition is referenced by:  sitgval  31869
  Copyright terms: Public domain W3C validator