# Theory Measure

Up to index of Isabelle/HOL/Integration

theory Measure
imports Sigma_Algebra MonConv
header {*Preliminaries*}theory Measureimports Sigma_Algebra MonConvbegin(*We use a modified version of the simple Sigma_Algebra Theory byMarkus Wenzel here,  which does not need an explicit definition of countable,  changing the names according to Joe Hurd*)text {* Now we are already set for the central concept of  measure. The following definitions are translated as faithfully as possible  from those in Joe Hurd's thesis \cite{hurd2002}. *}definition  measurable:: "'a set set => 'b set set => ('a => 'b) set" where  "measurable F G = {f. ∀g∈G. f - g ∈ F}"text {*So a function is called $F$-$G$-measurable if and only if the inverse  image of any set in $G$ is in $F$. $F$ and $G$ are usually the sets of  measurable sets, the first component of a measure space\footnote{In  standard mathematical notation, the universe is first in a  measure space triple, but in our definitions, following Joe Hurd, it is always the  whole type universe and therefore omitted.}.*}definition  measurable_sets:: "('a set set * ('a set => real)) => 'a set set" where  "measurable_sets = fst"definition  measure:: "('a set set * ('a set => real)) => ('a set => real)" where  "measure = snd"text {*The other component is the measure itself. It is a function that  assigns a nonnegative real number to every measurable set and has  the property of being  countably additive for disjoint sets.*}definition  positive:: "('a set set * ('a set => real)) => bool" where  "positive M <-> measure M {} = 0 ∧   (∀A. A∈ measurable_sets M --> 0 ≤ measure M A)"  (*Remark: This definition of measure space is not minimal,  in the sense that the containment of the UNION in the measurable sets   is implied by the measurable sets being a sigma algebra*)definition  countably_additive:: "('a set set * ('a set => real)) => bool" where  "countably_additive M <-> (∀f::(nat => 'a set). range f ⊆ measurable_sets M  ∧ (∀m n. m ≠ n --> f m ∩ f n = {}) ∧  (\<Union>i. f i) ∈ measurable_sets M  --> (λn. measure M (f n)) sums  measure M (\<Union>i. f i))" text {*This last property deserves some comments. The conclusion is  usually --- also in the aforementioned source --- phrased as    @{text "measure M (\<Union>i. f i) = (∑n. measure M (f n))"}.  In our formal setting this is unsatisfactory, because the  sum operator\footnote{Which is merely syntactic sugar for the  \isa{suminf} functional from the \isa{Series} theory  \cite{Fleuriot:2000:MNR}.}, like any HOL function, is total, although  a series obviously need not converge. It is defined using the @{text ε} operator, and its  behavior is unspecified in the diverging case. Hence, the above assertion  would give no information about the convergence of the series.     Furthermore, the definition contains redundancy. Assuming that the  countable union of sets is measurable is unnecessary when the  measurable sets form a sigma algebra, which is postulated in the  final definition\footnote{Joe Hurd inherited this practice from a very  influential probability textbook \cite{Williams.mart}}.   *}definition  measure_space:: "('a set set * ('a set => real)) => bool" where  "measure_space M <-> sigma_algebra (measurable_sets M) ∧   positive M ∧ countably_additive M"text {*Note that our definition is restricted to finite measure  spaces --- that is, @{text "measure M UNIV < ∞"} --- since the measure  must be a real number for any measurable set. In probability, this  is naturally the case.      Two important theorems close this section. Both appear in  Hurd's work as well, but are shown anyway, owing to their central  role in measure theory. The first one is a mighty tool for proving measurability. It states  that for a function mapping one sigma algebra into another, it is  sufficient to be measurable regarding only a generator of the target  sigma algebra. Formalizing the interesting proof out of Bauer's  textbook \cite{Bauer} is relatively straightforward using rule  induction. *}theorem assumes sig: "sigma_algebra a" and meas: "f ∈ measurable a b" shows   measurable_lift: "f ∈ measurable a (sigma b)"proof -  def Q ≡ "{q. f - q ∈ a}"  with meas have 1: "b ⊆ Q" by (auto simp add: measurable_def)   { fix x assume "x∈sigma b"    hence "x∈Q"    proof (induct rule: sigma.induct)      case basic      from 1 show " !!a. a ∈ b ==> a ∈ Q" ..    next      case empty      from sig have "{}∈a"         by (simp only: sigma_algebra_def)           thus "{} ∈ Q"         by (simp add: Q_def)    next      case complement      fix r assume "r ∈ Q"      then obtain r1 where im: "r1 = f - r" and a: "r1 ∈ a"         by (simp add: Q_def)      with sig have "-r1 ∈ a"         by (simp only: sigma_algebra_def)      with im Q_def show "-r ∈ Q"         by (simp add: vimage_Compl)    next      case Union      fix r assume "!!i::nat. r i ∈ Q"      then obtain r1 where im: "!!i. r1 i =  f - r i" and a: "!!i. r1 i ∈        a"         by (simp add: Q_def)      from a sig have "UNION UNIV r1 ∈ a"         by (auto simp only: sigma_algebra_def)      with im Q_def show "UNION UNIV r ∈ Q"         by (auto simp add: vimage_UN)    qed }          hence "(sigma b) ⊆ Q" ..  thus "f ∈ measurable a (sigma b)"     by (auto simp add: measurable_def Q_def)qedtext {*The case is different for the second theorem. It is only five  lines in the book (ibid.), but almost 200 in formal text. Precision  still pays here, gaining a detailed view of a technique that  is often employed in measure theory --- making a sequence of sets  disjoint. Moreover, the necessity for the above-mentioned change in the  definition of countably additive was detected only in the  formalization of this proof.   To enable application of the additivity of measures, the following construction  yields disjoint sets. We skip the justification of the lemmata for  brevity. *} primrec mkdisjoint:: "(nat => 'a set) => (nat => 'a set)"where  "mkdisjoint A 0 = A 0"| "mkdisjoint A (Suc n) = A (Suc n) - A n"lemma mkdisjoint_un:   assumes up: "!!n. A n ⊆ A (Suc n)"  shows "A n = (\<Union>i∈{..n}. mkdisjoint A i)"(*<*)proof (induct n)  case 0 show ?case by simpnext  case (Suc n)  hence "A n = (\<Union>i∈{..n}. mkdisjoint A i)" .  moreover  have "(\<Union>i∈{..(Suc n)}. mkdisjoint A i) = mkdisjoint A (Suc n) ∪    (\<Union>i∈{..n}. mkdisjoint A i)" by (simp add: atMost_Suc)   moreover  have "mkdisjoint A (Suc n) ∪ A n = A (Suc n) ∪ A n" by simp  moreover  from up have "… = A (Suc n)" by auto  ultimately  show ?case by simpqed(*>*)lemma mkdisjoint_disj:   assumes up: "!!n. A n ⊆ A (Suc n)" and ne: "m ≠ n"  shows "mkdisjoint A m ∩ mkdisjoint A n = {}"(*<*)proof -  { fix m1 m2::nat assume less: "m1 < m2"    hence "0 < m2" by simp    then obtain n where eq: "m2 = Suc n" by (auto simp add: gr0_conv_Suc)    with less have less2: "m1 < Suc n" by simp        {      fix y assume y: "y ∈ mkdisjoint A m1"      fix x assume x: "x ∈ mkdisjoint A m2"      with eq have"x ∉ A n" by simp      also from up have "A n = (\<Union>i∈{..n}. mkdisjoint A i)"         by (rule mkdisjoint_un)       also       from less2 have "m1 ∈ {..n}" by simp      hence "mkdisjoint A m1 ⊆ (\<Union>i∈{..n}. mkdisjoint A i)" by auto      ultimately       have "x ∉ mkdisjoint A m1" by fast      with y have "y ≠ x" by fast    }    hence "mkdisjoint A m1 ∩ mkdisjoint A m2 = {}"       by (simp add: disjoint_iff_not_equal)  } hence 1: "!!m1 m2. m1 < m2 ==>  mkdisjoint A m1 ∩ mkdisjoint A m2 = {}" .    show ?thesis  proof (cases "m < n")    case True    thus ?thesis by (rule 1)  next    case False    with ne have "n < m" by arith    hence "mkdisjoint A n ∩ mkdisjoint A m = {}" by (rule 1)    thus ?thesis by fast  qedqed(*>*)   lemma mkdisjoint_mon_conv:  assumes mc: "A\<up>B"   shows "(\<Union>i. mkdisjoint A i) = B"(*<*)proof  { fix x assume "x ∈ (\<Union>i. mkdisjoint A i)"    then obtain i where "x ∈ mkdisjoint A i" by auto    hence "x ∈ A i" by (cases i) simp_all    with mc have "x ∈ B" by (auto simp add: set_mon_conv)  }  thus "(\<Union>i. mkdisjoint A i) ⊆ B" by fast       { fix x assume "x ∈ B"    with mc obtain i where "x ∈ A i" by (auto simp add: set_mon_conv)    also from mc have "!!n. A n ⊆ A (Suc n)" by (simp only: set_mon_conv)    hence "A i = (\<Union>r∈{..i}. mkdisjoint A r)" by (rule mkdisjoint_un)    also have "… ⊆ (\<Union>r. mkdisjoint A r)" by auto    finally have "x ∈ (\<Union>i. mkdisjoint A i)".  }  thus "B ⊆ (\<Union>i. mkdisjoint A i)" by fastqed(*>*)  (*This is in Joe Hurd's Thesis (p. 35) as Monotone Convergence theorem. Check the real name … .     Also, it's not as strong as it could be,    but we need no more.*)text {* Joe Hurd calls the following the Monotone Convergence Theorem,  though in mathematical literature this name is often reserved for a  similar fact  about integrals that we will prove in \ref{nnfis}, which depends on this  one. The claim made here is that the measures of monotonically convergent sets  approach the measure of their limit. A strengthened version would  imply monotone convergence of the measures, but is not needed in the  development.  *}theorem measure_mon_conv:   assumes ms: "measure_space M" and   Ams: "!!n. A n ∈ measurable_sets M" and AB: "A\<up>B"   shows "(λn. measure M (A n)) ----> measure M B"proof -    from AB have up: "!!n. A n ⊆ A (Suc n)"     by (simp only: set_mon_conv)    { fix i    have "mkdisjoint A i ∈ measurable_sets M"     proof (cases i)      case 0 with Ams show ?thesis by simp    next      case (Suc i)      have "A (Suc i) - A i = A (Suc i) ∩ - A i" by blast      with Suc ms Ams show ?thesis         by (auto simp add: measure_space_def sigma_algebra_def sigma_algebra_inter)    qed  }   hence i: "!!i. mkdisjoint A i ∈ measurable_sets M" .        with ms have un: "(\<Union>i. mkdisjoint A i) ∈ measurable_sets M"     by (simp add: measure_space_def sigma_algebra_def)  moreover  from i have range: "range (mkdisjoint A) ⊆ measurable_sets M"     by fast  moreover  from up have "∀i j. i ≠ j -->  mkdisjoint A i ∩ mkdisjoint A j = {}"     by (simp add: mkdisjoint_disj)  moreover note ms  ultimately  have sums:    "(λi. measure M (mkdisjoint A i)) sums (measure M (\<Union>i. mkdisjoint A i))"    by (simp add: measure_space_def countably_additive_def)  hence "(∑i. measure M (mkdisjoint A i)) = (measure M (\<Union>i. mkdisjoint A i))"     by (rule sums_unique[THEN sym])    also  from sums have "summable (λi. measure M (mkdisjoint A i))"     by (rule sums_summable)  hence "(λn. ∑i=0..<n. measure M (mkdisjoint A i))    ----> (∑i. measure M (mkdisjoint A i))"    by (rule summable_sumr_LIMSEQ_suminf)                                           hence "(λn. ∑i=0..<Suc n. measure M (mkdisjoint A i))    ----> (∑i. measure M (mkdisjoint A i))"    by (rule LIMSEQ_Suc)    ultimately have "(λn. ∑i=0..<Suc n. measure M (mkdisjoint A i))    ----> (measure M (\<Union>i. mkdisjoint A i))" by simp      also   { fix n     from up have "A n = (\<Union>i∈{..n}. mkdisjoint A i)"       by (rule mkdisjoint_un)    hence "measure M (A n) = measure M (\<Union>i∈{..n}. mkdisjoint A i)"      by simp        also have       "(\<Union>i∈{..n}. mkdisjoint A i) = (\<Union>i. if i≤n then mkdisjoint A i else {})"    proof -      have "UNIV = {..n} ∪ {n<..}" by auto      hence "(\<Union>i. if i≤n then mkdisjoint A i else {}) =         (\<Union>i∈{..n}. if i≤n then mkdisjoint A i else {})         ∪  (\<Union>i∈{n<..}. if i≤n then mkdisjoint A i else {})"         by (auto simp add: UN_Un)      moreover      { have "(\<Union>i∈{n<..}. if i≤n then mkdisjoint A i else {}) = {}"          by force }      hence "… = (\<Union>i∈{..n}. mkdisjoint A i)"         by auto      ultimately show         "(\<Union>i∈{..n}. mkdisjoint A i) = (\<Union>i. if i≤n then mkdisjoint A i else {})" by simp    qed        ultimately have       "measure M (A n) = measure M (\<Union>i. if i≤n then mkdisjoint A i else {})"       by simp    also     from i ms have       un: "(\<Union>i. if i≤n then mkdisjoint A i else {}) ∈ measurable_sets M"       by (simp add: measure_space_def sigma_algebra_def)    moreover    from i ms have       "range (λi. if i≤n then mkdisjoint A i else {}) ⊆ measurable_sets M"       by (auto simp add: measure_space_def sigma_algebra_def)    moreover    from up have "∀i j. i ≠ j -->       (if i≤n then mkdisjoint A i else {}) ∩       (if j≤n then mkdisjoint A j else {}) = {}"       by (simp add: mkdisjoint_disj)    moreover note ms    ultimately have       "measure M (A n) = (∑i. measure M (if i ≤ n then mkdisjoint A i else {}))"      by (simp add: measure_space_def countably_additive_def sums_unique)        also    from ms have       "∀i. (Suc n)≤i --> measure M (if i ≤ n then mkdisjoint A i else {}) = 0"      by (simp add: measure_space_def positive_def)    hence "(λi. measure M (if i ≤ n then mkdisjoint A i else {})) sums      (∑i=0..<Suc n. measure M (if i ≤ n then mkdisjoint A i else {}))"      by (rule series_zero)    hence "(∑i. measure M (if i ≤ n then mkdisjoint A i else {})) =       (∑i=0..<Suc n. measure M (if i ≤ n then mkdisjoint A i else {}))"      by (rule sums_unique[THEN sym])    also    have "… = (∑i=0..<Suc n. measure M (mkdisjoint A i))"      by (simp cong: setsum_ivl_cong)    finally have       "measure M (A n) = (∑i=0..<Suc n. measure M (mkdisjoint A i))" .  }    ultimately have     "(λn. measure M (A n)) ----> (measure M (\<Union>i. mkdisjoint A i))"     by simp    with AB show ?thesis     by (simp add: mkdisjoint_mon_conv)qed(*>*)(*<*)primrec trivial_series2:: "'a set => 'a set => (nat => 'a set)"where  "trivial_series2 a b 0 = a"| "trivial_series2 a b (Suc n) = (if (n=0) then b else {})"lemma measure_additive: assumes ms: "measure_space M"  and disj: "a ∩ b = {}" and a: "a ∈ measurable_sets M"  and b:"b ∈ measurable_sets M"  shows "measure M (a ∪ b) = measure M a + measure M b"(*<*)proof -  have "(a ∪ b) = (\<Union>i. trivial_series2 a b i)"  proof (rule set_eqI)    fix x    {      assume "x ∈ a ∪ b"      hence "∃i. x ∈ trivial_series2 a b i"      proof         assume "x ∈ a"        hence "x ∈ trivial_series2 a b 0"          by simp        thus "∃i. x ∈ trivial_series2 a b i"          by fast      next        assume "x ∈ b"        hence "x ∈ trivial_series2 a b 1"          by simp        thus "∃i. x ∈ trivial_series2 a b i"          by fast      qed    }    hence "(x ∈ a ∪ b) ==> (x ∈ (\<Union>i. trivial_series2 a b i))"      by simp    also    {       assume "x ∈ (\<Union>i. trivial_series2 a b i)"      then obtain i where x: "x ∈ trivial_series2 a b i"        by auto      hence "x ∈ a ∪ b"      proof (cases i)        case 0        with x show ?thesis by simp      next        case (Suc n)        with x show ?thesis          by (cases n) auto      qed    }    ultimately show "(x ∈ a ∪ b) = (x ∈ (\<Union>i. trivial_series2 a b i))"      by fast  qed  also   { fix i    from a b ms have "trivial_series2 a b i ∈ measurable_sets M"      by (cases i) (auto simp add: measure_space_def sigma_algebra_def)  }  hence m1: "range (trivial_series2 a b) ⊆ measurable_sets M"    and m2: "(\<Union>i. trivial_series2 a b i) ∈ measurable_sets M"    using ms    by (auto simp add: measure_space_def sigma_algebra_def)    { fix i j::nat    assume "i ≠ j"    hence "trivial_series2 a b i ∩ trivial_series2 a b j = {}"      using disj      by (cases i, cases j, auto)(cases j, auto)  }  with m1 m2 have "(λn. measure M (trivial_series2 a b n)) sums  measure M (\<Union>i. trivial_series2 a b i)"     using ms     by (simp add: measure_space_def countably_additive_def)  moreover  from ms have "∀m. Suc(Suc 0) ≤ m --> measure M (trivial_series2 a b m) = 0"  proof (clarify)    fix m     assume "Suc (Suc 0) ≤ m"    thus "measure M (trivial_series2 a b m) = 0"      using ms      by (cases m) (auto simp add: measure_space_def positive_def)   qed  hence "(λn. measure M (trivial_series2 a b n)) sums (∑n=0..<Suc(Suc 0). measure M (trivial_series2 a b n))"    by (rule series_zero)  moreover  have "(∑n=0..<Suc(Suc 0). measure M (trivial_series2 a b n)) =    measure M a + measure M b"    by simp  ultimately  have "measure M (a ∪ b) = (∑n. measure M (trivial_series2 a b n))"    and "Measure.measure M a + Measure.measure M b = (∑n. measure M (trivial_series2 a b n))"    by (simp_all add: sums_unique)  thus ?thesis by simpqed(*>*)end