src/HOL/Analysis/Sigma_Algebra.thy
changeset 68607 67bb59e49834
parent 68403 223172b97d0b
child 69164 74f1b0f10b2b
     1.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Mon Jul 09 21:55:40 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jul 10 09:38:35 2018 +0200
     1.3 @@ -146,13 +146,13 @@
     1.4    "a \<in> M \<Longrightarrow> \<Omega> - a \<in> M"
     1.5    by auto
     1.6  
     1.7 -lemma%important algebra_iff_Un:
     1.8 +proposition algebra_iff_Un:
     1.9    "algebra \<Omega> M \<longleftrightarrow>
    1.10      M \<subseteq> Pow \<Omega> \<and>
    1.11      {} \<in> M \<and>
    1.12      (\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
    1.13      (\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un")
    1.14 -proof%unimportant
    1.15 +proof
    1.16    assume "algebra \<Omega> M"
    1.17    then interpret algebra \<Omega> M .
    1.18    show ?Un using sets_into_space by auto
    1.19 @@ -173,12 +173,12 @@
    1.20    show "algebra \<Omega> M" proof qed fact
    1.21  qed
    1.22  
    1.23 -lemma%important algebra_iff_Int:
    1.24 +proposition algebra_iff_Int:
    1.25       "algebra \<Omega> M \<longleftrightarrow>
    1.26         M \<subseteq> Pow \<Omega> & {} \<in> M &
    1.27         (\<forall>a \<in> M. \<Omega> - a \<in> M) &
    1.28         (\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int")
    1.29 -proof%unimportant
    1.30 +proof
    1.31    assume "algebra \<Omega> M"
    1.32    then interpret algebra \<Omega> M .
    1.33    show ?Int using sets_into_space by auto
    1.34 @@ -1433,7 +1433,7 @@
    1.35  text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
    1.36  generated by a generator closed under intersection.\<close>
    1.37  
    1.38 -lemma%important sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
    1.39 +proposition sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
    1.40    assumes "Int_stable G"
    1.41      and closed: "G \<subseteq> Pow \<Omega>"
    1.42      and A: "A \<in> sigma_sets \<Omega> G"
    1.43 @@ -1442,7 +1442,7 @@
    1.44      and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
    1.45      and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)"
    1.46    shows "P A"
    1.47 -proof%unimportant -
    1.48 +proof -
    1.49    let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
    1.50    interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
    1.51      using closed by (rule sigma_algebra_sigma_sets)
    1.52 @@ -1633,12 +1633,12 @@
    1.53  
    1.54  subsubsection \<open>Constructing simple @{typ "'a measure"}\<close>
    1.55  
    1.56 -lemma%important emeasure_measure_of:
    1.57 +proposition emeasure_measure_of:
    1.58    assumes M: "M = measure_of \<Omega> A \<mu>"
    1.59    assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
    1.60    assumes X: "X \<in> sets M"
    1.61    shows "emeasure M X = \<mu> X"
    1.62 -proof%unimportant -
    1.63 +proof -
    1.64    interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
    1.65    have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
    1.66      using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)