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 32970
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 32969 . 2 class sitg
2 vw . . 3 setvar 𝑀
3 vm . . 3 setvar π‘š
4 cvv 3448 . . 3 class V
5 cmeas 32834 . . . . 5 class measures
65crn 5639 . . . 4 class ran measures
76cuni 4870 . . 3 class βˆͺ ran measures
8 vf . . . 4 setvar 𝑓
9 vg . . . . . . . . 9 setvar 𝑔
109cv 1541 . . . . . . . 8 class 𝑔
1110crn 5639 . . . . . . 7 class ran 𝑔
12 cfn 8890 . . . . . . 7 class Fin
1311, 12wcel 2107 . . . . . 6 wff ran 𝑔 ∈ Fin
1410ccnv 5637 . . . . . . . . . 10 class ◑𝑔
15 vx . . . . . . . . . . . 12 setvar π‘₯
1615cv 1541 . . . . . . . . . . 11 class π‘₯
1716csn 4591 . . . . . . . . . 10 class {π‘₯}
1814, 17cima 5641 . . . . . . . . 9 class (◑𝑔 β€œ {π‘₯})
193cv 1541 . . . . . . . . 9 class π‘š
2018, 19cfv 6501 . . . . . . . 8 class (π‘šβ€˜(◑𝑔 β€œ {π‘₯}))
21 cc0 11058 . . . . . . . . 9 class 0
22 cpnf 11193 . . . . . . . . 9 class +∞
23 cico 13273 . . . . . . . . 9 class [,)
2421, 22, 23co 7362 . . . . . . . 8 class (0[,)+∞)
2520, 24wcel 2107 . . . . . . 7 wff (π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞)
262cv 1541 . . . . . . . . . 10 class 𝑀
27 c0g 17328 . . . . . . . . . 10 class 0g
2826, 27cfv 6501 . . . . . . . . 9 class (0gβ€˜π‘€)
2928csn 4591 . . . . . . . 8 class {(0gβ€˜π‘€)}
3011, 29cdif 3912 . . . . . . 7 class (ran 𝑔 βˆ– {(0gβ€˜π‘€)})
3125, 15, 30wral 3065 . . . . . 6 wff βˆ€π‘₯ ∈ (ran 𝑔 βˆ– {(0gβ€˜π‘€)})(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞)
3213, 31wa 397 . . . . 5 wff (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– {(0gβ€˜π‘€)})(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))
3319cdm 5638 . . . . . 6 class dom π‘š
34 ctopn 17310 . . . . . . . 8 class TopOpen
3526, 34cfv 6501 . . . . . . 7 class (TopOpenβ€˜π‘€)
36 csigagen 32777 . . . . . . 7 class sigaGen
3735, 36cfv 6501 . . . . . 6 class (sigaGenβ€˜(TopOpenβ€˜π‘€))
38 cmbfm 32888 . . . . . 6 class MblFnM
3933, 37, 38co 7362 . . . . 5 class (dom π‘šMblFnM(sigaGenβ€˜(TopOpenβ€˜π‘€)))
4032, 9, 39crab 3410 . . . 4 class {𝑔 ∈ (dom π‘šMblFnM(sigaGenβ€˜(TopOpenβ€˜π‘€))) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– {(0gβ€˜π‘€)})(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))}
418cv 1541 . . . . . . . 8 class 𝑓
4241crn 5639 . . . . . . 7 class ran 𝑓
4342, 29cdif 3912 . . . . . 6 class (ran 𝑓 βˆ– {(0gβ€˜π‘€)})
4441ccnv 5637 . . . . . . . . . 10 class ◑𝑓
4544, 17cima 5641 . . . . . . . . 9 class (◑𝑓 β€œ {π‘₯})
4645, 19cfv 6501 . . . . . . . 8 class (π‘šβ€˜(◑𝑓 β€œ {π‘₯}))
47 csca 17143 . . . . . . . . . 10 class Scalar
4826, 47cfv 6501 . . . . . . . . 9 class (Scalarβ€˜π‘€)
49 crrh 32614 . . . . . . . . 9 class ℝHom
5048, 49cfv 6501 . . . . . . . 8 class (ℝHomβ€˜(Scalarβ€˜π‘€))
5146, 50cfv 6501 . . . . . . 7 class ((ℝHomβ€˜(Scalarβ€˜π‘€))β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯})))
52 cvsca 17144 . . . . . . . 8 class ·𝑠
5326, 52cfv 6501 . . . . . . 7 class ( ·𝑠 β€˜π‘€)
5451, 16, 53co 7362 . . . . . 6 class (((ℝHomβ€˜(Scalarβ€˜π‘€))β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯})))( ·𝑠 β€˜π‘€)π‘₯)
5515, 43, 54cmpt 5193 . . . . 5 class (π‘₯ ∈ (ran 𝑓 βˆ– {(0gβ€˜π‘€)}) ↦ (((ℝHomβ€˜(Scalarβ€˜π‘€))β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯})))( ·𝑠 β€˜π‘€)π‘₯))
56 cgsu 17329 . . . . 5 class Ξ£g
5726, 55, 56co 7362 . . . 4 class (𝑀 Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– {(0gβ€˜π‘€)}) ↦ (((ℝHomβ€˜(Scalarβ€˜π‘€))β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯})))( ·𝑠 β€˜π‘€)π‘₯)))
588, 40, 57cmpt 5193 . . 3 class (𝑓 ∈ {𝑔 ∈ (dom π‘šMblFnM(sigaGenβ€˜(TopOpenβ€˜π‘€))) ∣ (ran 𝑔 ∈ Fin ∧ βˆ€π‘₯ ∈ (ran 𝑔 βˆ– {(0gβ€˜π‘€)})(π‘šβ€˜(◑𝑔 β€œ {π‘₯})) ∈ (0[,)+∞))} ↦ (𝑀 Ξ£g (π‘₯ ∈ (ran 𝑓 βˆ– {(0gβ€˜π‘€)}) ↦ (((ℝHomβ€˜(Scalarβ€˜π‘€))β€˜(π‘šβ€˜(◑𝑓 β€œ {π‘₯})))( ·𝑠 β€˜π‘€)π‘₯))))
592, 3, 4, 7, 58cmpo 7364 . 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  32972
  Copyright terms: Public domain W3C validator