Displaying similar documents to “Integral representation of Gaussian measures.”

Product Pre-Measure

Noboru Endou (2016)

Formalized Mathematics

Similarity:

In this article we formalize in Mizar [5] product pre-measure on product sets of measurable sets. Although there are some approaches to construct product measure [22], [6], [9], [21], [25], we start it from σ-measure because existence of σ-measure on any semialgebras has been proved in [15]. In this approach, we use some theorems for integrals.

On the extension of measures.

Baltasar Rodríguez-Salinas (2001)

RACSAM

Similarity:

We give necessary and sufficient conditions for a totally ordered by extension family (Ω, Σ, μ) of spaces of probability to have a measure μ which is an extension of all the measures μ. As an application we study when a probability measure on Ω has an extension defined on all the subsets of Ω.

Fubini’s Theorem on Measure

Noboru Endou (2017)

Formalized Mathematics

Similarity:

The purpose of this article is to show Fubini’s theorem on measure [16], [4], [7], [15], [18]. Some theorems have the possibility of slight generalization, but we have priority to avoid the complexity of the description. First of all, for the product measure constructed in [14], we show some theorems. Then we introduce the section which plays an important role in Fubini’s theorem, and prove the relevant proposition. Finally we show Fubini’s theorem on measure.

Hopf Extension Theorem of Measure

Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama (2009)

Formalized Mathematics

Similarity:

The authors have presented some articles about Lebesgue type integration theory. In our previous articles [12, 13, 26], we assumed that some σ-additive measure existed and that a function was measurable on that measure. However the existence of such a measure is not trivial. In general, because the construction of a finite additive measure is comparatively easy, to induce a σ-additive measure a finite additive measure is used. This is known as an E. Hopf's extension theorem of measure...