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 30722
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 30721 . 2 class sitg
2 vw . . 3 setvar 𝑤
3 vm . . 3 setvar 𝑚
4 cvv 3340 . . 3 class V
5 cmeas 30588 . . . . 5 class measures
65crn 5267 . . . 4 class ran measures
76cuni 4588 . . 3 class ran measures
8 vf . . . 4 setvar 𝑓
9 vg . . . . . . . . 9 setvar 𝑔
109cv 1631 . . . . . . . 8 class 𝑔
1110crn 5267 . . . . . . 7 class ran 𝑔
12 cfn 8123 . . . . . . 7 class Fin
1311, 12wcel 2139 . . . . . 6 wff ran 𝑔 ∈ Fin
1410ccnv 5265 . . . . . . . . . 10 class 𝑔
15 vx . . . . . . . . . . . 12 setvar 𝑥
1615cv 1631 . . . . . . . . . . 11 class 𝑥
1716csn 4321 . . . . . . . . . 10 class {𝑥}
1814, 17cima 5269 . . . . . . . . 9 class (𝑔 “ {𝑥})
193cv 1631 . . . . . . . . 9 class 𝑚
2018, 19cfv 6049 . . . . . . . 8 class (𝑚‘(𝑔 “ {𝑥}))
21 cc0 10148 . . . . . . . . 9 class 0
22 cpnf 10283 . . . . . . . . 9 class +∞
23 cico 12390 . . . . . . . . 9 class [,)
2421, 22, 23co 6814 . . . . . . . 8 class (0[,)+∞)
2520, 24wcel 2139 . . . . . . 7 wff (𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)
262cv 1631 . . . . . . . . . 10 class 𝑤
27 c0g 16322 . . . . . . . . . 10 class 0g
2826, 27cfv 6049 . . . . . . . . 9 class (0g𝑤)
2928csn 4321 . . . . . . . 8 class {(0g𝑤)}
3011, 29cdif 3712 . . . . . . 7 class (ran 𝑔 ∖ {(0g𝑤)})
3125, 15, 30wral 3050 . . . . . 6 wff 𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)
3213, 31wa 383 . . . . 5 wff (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))
3319cdm 5266 . . . . . 6 class dom 𝑚
34 ctopn 16304 . . . . . . . 8 class TopOpen
3526, 34cfv 6049 . . . . . . 7 class (TopOpen‘𝑤)
36 csigagen 30531 . . . . . . 7 class sigaGen
3735, 36cfv 6049 . . . . . 6 class (sigaGen‘(TopOpen‘𝑤))
38 cmbfm 30642 . . . . . 6 class MblFnM
3933, 37, 38co 6814 . . . . 5 class (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤)))
4032, 9, 39crab 3054 . . . 4 class {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))}
418cv 1631 . . . . . . . 8 class 𝑓
4241crn 5267 . . . . . . 7 class ran 𝑓
4342, 29cdif 3712 . . . . . 6 class (ran 𝑓 ∖ {(0g𝑤)})
4441ccnv 5265 . . . . . . . . . 10 class 𝑓
4544, 17cima 5269 . . . . . . . . 9 class (𝑓 “ {𝑥})
4645, 19cfv 6049 . . . . . . . 8 class (𝑚‘(𝑓 “ {𝑥}))
47 csca 16166 . . . . . . . . . 10 class Scalar
4826, 47cfv 6049 . . . . . . . . 9 class (Scalar‘𝑤)
49 crrh 30367 . . . . . . . . 9 class ℝHom
5048, 49cfv 6049 . . . . . . . 8 class (ℝHom‘(Scalar‘𝑤))
5146, 50cfv 6049 . . . . . . 7 class ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))
52 cvsca 16167 . . . . . . . 8 class ·𝑠
5326, 52cfv 6049 . . . . . . 7 class ( ·𝑠𝑤)
5451, 16, 53co 6814 . . . . . 6 class (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)
5515, 43, 54cmpt 4881 . . . . 5 class (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥))
56 cgsu 16323 . . . . 5 class Σg
5726, 55, 56co 6814 . . . 4 class (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))
588, 40, 57cmpt 4881 . . 3 class (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥))))
592, 3, 4, 7, 58cmpt2 6816 . 2 class (𝑤 ∈ V, 𝑚 ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))))
601, 59wceq 1632 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  30724
  Copyright terms: Public domain W3C validator