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 29525
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 29524 . 2 class sitg
2 vw . . 3 setvar 𝑤
3 vm . . 3 setvar 𝑚
4 cvv 3172 . . 3 class V
5 cmeas 29391 . . . . 5 class measures
65crn 5029 . . . 4 class ran measures
76cuni 4366 . . 3 class ran measures
8 vf . . . 4 setvar 𝑓
9 vg . . . . . . . . 9 setvar 𝑔
109cv 1473 . . . . . . . 8 class 𝑔
1110crn 5029 . . . . . . 7 class ran 𝑔
12 cfn 7818 . . . . . . 7 class Fin
1311, 12wcel 1976 . . . . . 6 wff ran 𝑔 ∈ Fin
1410ccnv 5027 . . . . . . . . . 10 class 𝑔
15 vx . . . . . . . . . . . 12 setvar 𝑥
1615cv 1473 . . . . . . . . . . 11 class 𝑥
1716csn 4124 . . . . . . . . . 10 class {𝑥}
1814, 17cima 5031 . . . . . . . . 9 class (𝑔 “ {𝑥})
193cv 1473 . . . . . . . . 9 class 𝑚
2018, 19cfv 5790 . . . . . . . 8 class (𝑚‘(𝑔 “ {𝑥}))
21 cc0 9792 . . . . . . . . 9 class 0
22 cpnf 9927 . . . . . . . . 9 class +∞
23 cico 12004 . . . . . . . . 9 class [,)
2421, 22, 23co 6527 . . . . . . . 8 class (0[,)+∞)
2520, 24wcel 1976 . . . . . . 7 wff (𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)
262cv 1473 . . . . . . . . . 10 class 𝑤
27 c0g 15869 . . . . . . . . . 10 class 0g
2826, 27cfv 5790 . . . . . . . . 9 class (0g𝑤)
2928csn 4124 . . . . . . . 8 class {(0g𝑤)}
3011, 29cdif 3536 . . . . . . 7 class (ran 𝑔 ∖ {(0g𝑤)})
3125, 15, 30wral 2895 . . . . . 6 wff 𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞)
3213, 31wa 382 . . . . 5 wff (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))
3319cdm 5028 . . . . . 6 class dom 𝑚
34 ctopn 15851 . . . . . . . 8 class TopOpen
3526, 34cfv 5790 . . . . . . 7 class (TopOpen‘𝑤)
36 csigagen 29334 . . . . . . 7 class sigaGen
3735, 36cfv 5790 . . . . . 6 class (sigaGen‘(TopOpen‘𝑤))
38 cmbfm 29445 . . . . . 6 class MblFnM
3933, 37, 38co 6527 . . . . 5 class (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤)))
4032, 9, 39crab 2899 . . . 4 class {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))}
418cv 1473 . . . . . . . 8 class 𝑓
4241crn 5029 . . . . . . 7 class ran 𝑓
4342, 29cdif 3536 . . . . . 6 class (ran 𝑓 ∖ {(0g𝑤)})
4441ccnv 5027 . . . . . . . . . 10 class 𝑓
4544, 17cima 5031 . . . . . . . . 9 class (𝑓 “ {𝑥})
4645, 19cfv 5790 . . . . . . . 8 class (𝑚‘(𝑓 “ {𝑥}))
47 csca 15717 . . . . . . . . . 10 class Scalar
4826, 47cfv 5790 . . . . . . . . 9 class (Scalar‘𝑤)
49 crrh 29171 . . . . . . . . 9 class ℝHom
5048, 49cfv 5790 . . . . . . . 8 class (ℝHom‘(Scalar‘𝑤))
5146, 50cfv 5790 . . . . . . 7 class ((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))
52 cvsca 15718 . . . . . . . 8 class ·𝑠
5326, 52cfv 5790 . . . . . . 7 class ( ·𝑠𝑤)
5451, 16, 53co 6527 . . . . . 6 class (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)
5515, 43, 54cmpt 4637 . . . . 5 class (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥))
56 cgsu 15870 . . . . 5 class Σg
5726, 55, 56co 6527 . . . 4 class (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))
588, 40, 57cmpt 4637 . . 3 class (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥))))
592, 3, 4, 7, 58cmpt2 6529 . 2 class (𝑤 ∈ V, 𝑚 ran measures ↦ (𝑓 ∈ {𝑔 ∈ (dom 𝑚MblFnM(sigaGen‘(TopOpen‘𝑤))) ∣ (ran 𝑔 ∈ Fin ∧ ∀𝑥 ∈ (ran 𝑔 ∖ {(0g𝑤)})(𝑚‘(𝑔 “ {𝑥})) ∈ (0[,)+∞))} ↦ (𝑤 Σg (𝑥 ∈ (ran 𝑓 ∖ {(0g𝑤)}) ↦ (((ℝHom‘(Scalar‘𝑤))‘(𝑚‘(𝑓 “ {𝑥})))( ·𝑠𝑤)𝑥)))))
601, 59wceq 1474 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  29527
  Copyright terms: Public domain W3C validator