#import "../notation/main.typ": inverse, preimage, half-open-rectangle, symmetric-difference
#import "../topology/main.typ": topological-space
#import "../theme.typ":  proof, proposition, theorem, definition, example, comment

== Introduction

#let set-algebra = (
    tag : link(<set-algebra>)[set algebra]
)
#definition("Set algebra")[
    Let $X$ be a set, and $cal(A) subset.eq 2^X$ such that:
    1. $X in cal(A)$. #comment[Unit].
    2. $A,B in cal(A) ==> A union B in cal(A)$. #comment[Closed under union].
    3. $A in cal(A) ==> X without A in cal(A)$. #comment[Closed under complement].
    Then $(X,cal(A))$ is called a *set algebra*.
]<set-algebra>

#let set-ring = (
    tag : link(<set-ring>)[set ring]
)
#definition("Set ring")[
    Let $X$ be a set, and $cal(R) subset.eq 2^X$ such that:
    1. $cal(R) != nothing$. #comment[Non-empty].
    2. $A,B in cal(R) ==> A sect B in cal(R)$. #comment[Closed under intersection].
    3. $A,B in cal(R) ==> A #symmetric-difference.sym B in cal(R)$. #comment[Closed under symmetric difference].
    Then $(X, cal(R))$ is called a *set ring*
]<set-ring>

#proposition(text[intersection of #text[#set-ring.tag]s is a #set-ring.tag])[
    Let $(X,cal(R_0))$ and $(X,cal(R_1))$ be two #text[#set-ring.tag]s. Then $(X, cal(R_0) sect cal(R_1))$ is a #set-ring.tag.
]<insersection-of-set-ring-is-a-set-ring>

#proof(text[of @insersection-of-set-ring-is-a-set-ring])[
    Given two #text[#set-ring.tag]s $(X,cal(R_0))$ and $(X,cal(R_1))$. We need to show that $(X,cal(R) = cal(R_0) sect cal(R_1))$ is a #set-ring.tag:
    1. Suppose $A_0 in cal(R_0)$ and $A_1 in cal(R_1)$ #comment[(such $A_0$ and $A_1$ exists since $cal(R_0)$ and $cal(R_1)$ are non-empty)]. Then $nothing in cal(R_0)$ since $nothing = A_0 #symmetric-difference.sym A_1 in cal(R_0)$. Similarly, $nothing in cal(R_1)$. Therefore $nothing in cal(R_0) sect cal(R_1)$
    2. Suppose $A,B in cal(R)$. Then $A,B in cal(R_0)$ and $A,B in cal(R_1)$. Then $A sect B in cal(R_0)$ and $cal(R_1)$. Therefore $A sect B in cal(R)$.
    3. Suppose $A,B in cal(R)$. Then $A,B in cal(R_0)$ and $A,B in cal(R_1)$. Then $A #symmetric-difference.sym B in cal(R_0)$ and $cal(R_1)$. Therefore $A #symmetric-difference.sym B in cal(R)$.
]

#let sigma-algebra = (
    tag : link(<sigma-algebra>)[$sigma$-algebra]
)
#definition(text[$sigma$-algebra])[
    Let $X$ be a set. $Sigma subset.eq 2^X$ is said a *sigma algebra of X* iff.:
    1. $X in Sigma$
    2. $E in Sigma ==> X without E in Sigma$. #comment[close under complement].
    3. ${A_n in Sigma}_(n=1)^(oo) ==> union.big_(i=1)^(oo) A_i in Sigma$. #comment[close under infinite unions].
]<sigma-algebra>

#proposition(text[a #sigma-algebra.tag is a #set-ring.tag])[
    Let $(X,Sigma)$ be a #sigma-algebra.tag, then $(X,Sigma)$ is a #set-ring.tag
]<sigma-algebra-is-a-set-ring>

#proof(text[of @sigma-algebra-is-a-set-ring])[
    We need to show that, given a #sigma-algebra.tag $(X,Sigma)$ the axioms of #text[#set-ring.tag]s hold:
    1. $Sigma != nothing$. This is true since $X in Sigma$.
    2. $A,B in Sigma ==> A sect B in Sigma$. This is true since $A sect B = (X without A) union (X without B)$ #comment[(a #sigma-algebra.tag is closed under $union$ and $without$)].
    3. $A,B in Sigma ==> A #symmetric-difference.sym B in Sigma$. This is true since $A #symmetric-difference.sym B = (A without B) union (B without A)$ #comment[(a #sigma-algebra.tag is closed under $union$ and $without$)].
]

#let generated-sigma-algebra = (
    tag : link(<generated-sigma-algebra>)[generated $sigma$-algebra],
    sym : (universe,content) => link(<generated-sigma-algebra>)[$sigma_(#universe)(#content)$]
)
#definition(text[generate $sigma$-algebra])[
    Let $X$ be a set and $G subset.eq 2^X$. The *$sigma$-algebra generated by $G$*, denoted #(generated-sigma-algebra.sym)("X","G"), is the smallest #link(<sigma-algebra>)[$sigma$-algebra] such that:
    1. $G subset.eq #(generated-sigma-algebra.sym)("X","G")$.
    2. $forall Sigma " "#text[#sigma-algebra.tag]: G subset.eq Sigma ==> sigma_(X)(G) subset.eq Sigma$. #comment[Every other #sigma-algebra.tag that contains $G$ contains also the generated one, #(generated-sigma-algebra.sym)("X","G")].
]<generated-sigma-algebra>

#let borel-sigma-algebra = (
    tag : link(<borel-sigma-algebra>)[Borel sigma algebra],
    sym : (universe, topology) => link(<borel-sigma-algebra>)[$cal(B)(#universe, #topology)$]
)
#definition(text[borel $sigma$-algebra])[
    Let $(X,G)$ be a #topological-space.tag. We refer to $#(generated-sigma-algebra.sym)("X","G")=#(borel-sigma-algebra.sym)("X","G")$ as a *Borel $sigma$-algebra*.
]<borel-sigma-algebra>

#let sigma-algebra-product = (
    tag : link(<sigma-algebra-product>)[$sigma$-algebra product],
    sym : link(<sigma-algebra-product>)[#sym.times.circle]
)
#definition(text[$sigma$-algebra product])[
    Let $Sigma_1$ and $Sigma_2$ be #sigma-algebra.tag on $X_1$ and $X_2$ respectively. The *product $sigma$-algebra* denoted $Sigma_1 #sigma-algebra-product.sym Sigma_2$ is defined as #(generated-sigma-algebra.sym)($X_1 times X_2$,${S_1 times S_2 | S_1 in Sigma_1, S_2 in Sigma_2}$) 
]<sigma-algebra-product>

#let measurable-space = (
    tag : link(<measurable-space>)[measurable space]
)
#definition("measurable space")[
    $(X,Sigma)$ is said *measurable* iff. #sym.Sigma is a #sigma-algebra.tag of $X$.
]<measurable-space>

#let measure = (
    tag : link(<measure>)[measure],
    ax1 : measure => text[$#measure (nothing) = 0$],
    ax2 : measure => text[$E in Sigma ==> #measure (E)>=0$],
    ax3 : measure => text[${E_n in Sigma}_(n in NN) " pairwise disjoint " ==> #measure (union_(n in NN) E_b) = sum_(n in NN) #measure (E_n)$]
)
#definition("measure")[
    Given $(X,Sigma)$ #measurable-space.tag. $mu:Sigma --> RR union {+oo,-oo}$ is said a *measure* iff.
    1. $mu(nothing)=0$ #comment[Empty set].
    2. $E in Sigma ==> mu(E)>=0$. #comment[Positiveness].
    3. ${E_n in Sigma}_(n in NN) " pairwise disjoint " ==> mu(union_(n in NN) E_b) = sum_(n in NN) mu(E_n)$. #comment[Countable additivity].
]<measure>

#let measure-space = (
    tag : link(<measure-space>)[measure space]

)
#definition("measure space")[
    $(X,Sigma,mu)$ is said a *measure space* iff. $(X,Sigma)$ is a #sigma-algebra.tag and #sym.mu is a #measure.tag of $(X,Sigma)$.
]<measure-space>

#let measurable-function = (
    tag : link(<measurable-function>)[measurable function]
)
#definition("measurable function")[
    Let $(X_1, Sigma_1)$ and $(X_2, Sigma_2)$ be #text[#measurable-space.tag]s. $f:X_1 --> X_2$ is said a *measurable function* iff. $forall E in Sigma_2: #(inverse.sym)("f") (E) in Sigma_1$. #comment[The #preimage.tag of each measurable set is again measurable].
]<measurable-function>

#let pushforward = (
    tag : link(<pushforward>)[pushforward],
    sym : (fname,measure) => link(<pushforward>)[$#(fname)_(hash) #measure$]
)
#definition("pushforward")[
    Let $(X_1,Sigma_1,mu)$ be a #measure-space.tag. Let $(X_2,Sigma_2)$ be a #measurable-space.tag. Let $f:X_1 --> X_2$ be a #measurable-function.tag. The *pushforwad of $mu$ under $f$* is the mapping $#(pushforward.sym)("f",sym.mu): Sigma_2 --> RR_(>=0) union {oo}$ defined as: $ forall E in Sigma_2 : #(pushforward.sym)("f", sym.mu) = mu(#(inverse.sym)("f") (E)) $
]<pushforward>

The pushforward is simply a function that generates a measure for a measurable space starting from a different measure space and a measurable function acting as bridge between the two spaces. 

#proposition("pushforward of a measure is a measure")[
    Let $(X_1,Sigma_1,mu)$ be a #measure-space.tag. Let $(X_2,Sigma_2)$ be a #measurable-space.tag. Let $f:X_1 --> X_2$ be a #measurable-function.tag. Then $(X_2,Sigma_2,#(pushforward.sym)("f",sym.mu))$ is a #measure-space.tag.
]<pushforward-of-a-measure-is-a-measure>

#proof(text[of @pushforward-of-a-measure-is-a-measure])[
    To prove that statement, we need to prove only the axioms of a #measure.tag.
    1. Let $E in Sigma_2$, we need to show that $f_(\#)mu(E) >= 0$. This is trivial by definition of #pushforward.tag and #measure.tag.
    2. Let $[E_n in Sigma_2]_(n=1)^(oo)$ be a sequence of pairwise disjoint sets. We need to show that: $#(pushforward.sym)("f",sym.mu) (union.big_(n=1)^(oo)E_n)=sum_(n=1)^(oo) #(pushforward.sym)("f",sym.mu) (E_n)$.
        $ #(pushforward.sym)("f",sym.mu) (union.big_(n=1)^(oo)E_n) &= mu(#(inverse.sym)("f") (union.big_(n=1)^(oo) E_n)) #comment[definition of #pushforward.tag] \
                                                                   &= mu(union.big_(n=1)^(oo) #(inverse.sym)("f") (E_n)) \
                                                                   &= sum_(n=1)^(oo) mu(#(inverse.sym)("f") (E_n)) #comment[definition of #measure.tag] \
                                                                   &= sum_(n=1)^(oo) #(pushforward.sym)("f",sym.mu) (E_n) #comment[definition of #pushforward.tag]
        $
    3. We need to show that $exists E in Sigma_1$ such that $#(pushforward.sym)("f",sym.mu) (E) >= 0$. Let $E' in Sigma_1$ such that $mu(E') >= 0$ (such $E'$ exists by defintion of measure). Then, $f(E')$ is a set that meets the requirements, that is 
        $ #(pushforward.sym)("f",sym.mu) (f(E')) = mu(#(inverse.sym)("f") (f(E'))) = mu(E') >= 0 $
]

#example("pushforward example")[
    Consider the #measure-space.tag $(NN,2^NN,mu(E)=|E|)$. Consider the #measurable-space.tag $(RR, #(generated-sigma-algebra.sym)(sym.RR,(half-open-rectangle.sym)("n")))$. Consider the #measurable-function.tag $f:NN --> RR$ such that f(x) = x. Consider #pushforward.tag $#(pushforward.sym)("f",sym.mu):RR --> RR_(>=0) union {oo}$. Then $#(pushforward.sym)("f",sym.mu)$ is a #measure.tag for the #measurable-space.tag $(RR, #(generated-sigma-algebra.sym)(sym.RR,(half-open-rectangle.sym)("n")))$ since:
    1. $#(pushforward.sym)("f",sym.mu) (E in #(generated-sigma-algebra.sym)(sym.RR,(half-open-rectangle.sym)("n"))) = |{n in NN | n in E}| >= 0$.
    2. Let ${E_n}_(n=1)^(oo)$ pairwise disjoint, then $#(pushforward.sym)("f",sym.mu) (union.big_(n=1)^(oo) E_n) = mu(#(inverse.sym)("f") (union.big_(n=1)^(oo) E_n)) = mu(union.big_(n=1)^(oo) #(inverse.sym)("f") (E_n)) = sum_(n=1)^(oo) mu(#(inverse.sym)("f") (E_n)) = sum_(n=1)^(oo) #(pushforward.sym)("f",sym.mu) (E_n)$.
    3. $#(pushforward.sym)("f",sym.mu) (nothing) = mu(#(inverse.sym)("f") (nothing)) = mu(nothing) = 0$
]

#let pre-measure = (
    tag : link(<pre-measure>)[pre-measure]
)
#definition("pre-measure")[
    Let $(X, Sigma)$ be a #set-algebra.tag. Let $mu:S --> R_(>=0) union {+oo}$. $mu$ is said a *pre-measure* iff.
    1. $mu(nothing) = 0$. #comment[Empty set].
    2. Given a collection of pairwise disjoint sets ${A_n in S}_(n in NN)$ such that $union.big_(n in NN) A_n in S ==> mu(union.big_(n in NN) A_n) = sum_(n in NN) mu(A_n)$. #comment[Countable additivity].
    3. $forall A in S: mu(A) >= 0$. #comment[Positiveness].
]<pre-measure>

A #pre-measure.tag is a precursor of a full-fledge #measure.tag. The main difference is that a #measure.tag is defined on #text[#sigma-algebra.tag]s, meanwhile the #pre-measure.tag is defined on a simple collection of subsets. Further, given that this collection is not necessarily closed under unions as a #sigma-algebra.tag does, we also need to check that, in the second requirement, the union of $A_n$ is indeed contained in the collection.

#let outer-measure = (
    tag : link(<outer-measure>)[outer measure],
    ax1 : measure => text[$#measure (nothing) = 0$],
    ax2 : measure => text[$forall A,B: A subset.eq B ==> #measure (A) <= #measure (B)$],
    ax3 : measure => text[$forall {A_n}_(n in NN): #measure (union.big_(n in NN) A_n) <= sum_(n in NN) #measure (A_n)$]
)
#definition("Outer measure")[
    Let $X$ be a set. An *outer measure* $mu: 2^X --> RR_(>=0) union {oo}$ such that:
    1. #(outer-measure.ax1)($mu$). #comment[empty set].
    2. #(outer-measure.ax2)($mu$). #comment[Monotonicity].
    3. #(outer-measure.ax3)($mu$). #comment[Countable subadditivity].
]<outer-measure>

An #text[#outer-measure.tag]s are weaker wrt. #text[#measure.tag]s as they are only countably subadditive rather than countably additive. However, they are able to measure all subset of $X$ rather than only a #text[#sigma-algebra.tag]s.


