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 30726
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 30725 . 2 class sitg
2 vw . . 3 setvar 𝑤
3 vm . . 3 setvar 𝑚
4 cvv 3349 . . 3 class V
5 cmeas 30592 . . . . 5 class measures
65crn 5250 . . . 4 class ran measures
76cuni 4572 . . 3 class ran measures
8 vf . . . 4 setvar 𝑓
9 vg . . . . . . . . 9 setvar 𝑔
109cv 1629 . . . . . . . 8 class 𝑔
1110crn 5250 . . . . . . 7 class ran 𝑔
12 cfn 8108 . . . . . . 7 class Fin
1311, 12wcel 2144 . . . . . 6 wff ran 𝑔 ∈ Fin
1410ccnv 5248 . . . . . . . . . 10 class 𝑔
15 vx . . . . . . . . . . . 12 setvar 𝑥
1615cv 1629 . . . . . . . . . . 11 class 𝑥
1716csn 4314 . . . . . . . . . 10 class {𝑥}
1814, 17cima 5252 . . . . . . . . 9 class (𝑔 “ {𝑥})
193cv 1629 . . . . . . . . 9 class 𝑚
2018, 19cfv 6031 . . . . . . . 8 class (𝑚‘(𝑔 “ {𝑥}))
21 cc0 10137 . . . . . . . . 9 class 0
22 cpnf 10272 . . . . . . . . 9 class +∞
23 cico 12381 . . . . . . . . 9 class [,)
2421, 22, 23co 6792 . . . . . . . 8 class (0[,)+∞)
2520, 24wcel 2144 . . . . . . 7 wff (𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)
262cv 1629 . . . . . . . . . 10 class 𝑤
27 c0g 16307 . . . . . . . . . 10 class 0g
2826, 27cfv 6031 . . . . . . . . 9 class (0g𝑤)
2928csn 4314 . . . . . . . 8 class {(0g𝑤)}
3011, 29cdif 3718 . . . . . . 7 class (ran 𝑔 ∖ {(0g𝑤)})
3125, 15, 30wral 3060 . . . . . 6 wff 𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)
3213, 31wa 382 . . . . 5 wff (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))
3319cdm 5249 . . . . . 6 class dom 𝑚
34 ctopn 16289 . . . . . . . 8 class TopOpen
3526, 34cfv 6031 . . . . . . 7 class (TopOpen‘𝑤)
36 csigagen 30535 . . . . . . 7 class sigaGen
3735, 36cfv 6031 . . . . . 6 class (sigaGen‘(TopOpen‘𝑤))
38 cmbfm 30646 . . . . . 6 class MblFnM
3933, 37, 38co 6792 . . . . 5 class (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤)))
4032, 9, 39crab 3064 . . . 4 class {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))}
418cv 1629 . . . . . . . 8 class 𝑓
4241crn 5250 . . . . . . 7 class ran 𝑓
4342, 29cdif 3718 . . . . . 6 class (ran 𝑓 ∖ {(0g𝑤)})
4441ccnv 5248 . . . . . . . . . 10 class 𝑓
4544, 17cima 5252 . . . . . . . . 9 class (𝑓 “ {𝑥})
4645, 19cfv 6031 . . . . . . . 8 class (𝑚‘(𝑓 “ {𝑥}))
47 csca 16151 . . . . . . . . . 10 class Scalar
4826, 47cfv 6031 . . . . . . . . 9 class (Scalar‘𝑤)
49 crrh 30371 . . . . . . . . 9 class ℝHom
5048, 49cfv 6031 . . . . . . . 8 class (ℝHom‘(Scalar‘𝑤))
5146, 50cfv 6031 . . . . . . 7 class ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))
52 cvsca 16152 . . . . . . . 8 class ·𝑠
5326, 52cfv 6031 . . . . . . 7 class ( ·𝑠𝑤)
5451, 16, 53co 6792 . . . . . 6 class (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)
5515, 43, 54cmpt 4861 . . . . 5 class (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥))
56 cgsu 16308 . . . . 5 class Σg
5726, 55, 56co 6792 . . . 4 class (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))
588, 40, 57cmpt 4861 . . 3 class (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥))))
592, 3, 4, 7, 58cmpt2 6794 . 2 class (𝑤 ∈ V, 𝑚 ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))))
601, 59wceq 1630 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  30728
  Copyright terms: Public domain W3C validator