src/HOL/Analysis/Measure_Space.thy
changeset 67962 0acdcd8f4ba1
parent 67673 c8caefb20564
child 67982 7643b005b29a
     1.1 --- a/src/HOL/Analysis/Measure_Space.thy	Thu Apr 05 06:15:02 2018 +0000
     1.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Fri Apr 06 17:34:50 2018 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    Measurable "HOL-Library.Extended_Nonnegative_Real"
     1.5  begin
     1.6  
     1.7 -subsection "Relate extended reals and the indicator function"
     1.8 +subsection%unimportant "Relate extended reals and the indicator function"
     1.9  
    1.10  lemma suminf_cmult_indicator:
    1.11    fixes f :: "nat \<Rightarrow> ennreal"
    1.12 @@ -59,7 +59,7 @@
    1.13    represent sigma algebras (with an arbitrary emeasure).
    1.14  \<close>
    1.15  
    1.16 -subsection "Extend binary sets"
    1.17 +subsection%unimportant "Extend binary sets"
    1.18  
    1.19  lemma LIMSEQ_binaryset:
    1.20    assumes f: "f {} = 0"
    1.21 @@ -91,7 +91,7 @@
    1.22    shows "f {} = 0 \<Longrightarrow> (\<Sum>n. f (binaryset A B n)) = f A + f B"
    1.23    by (metis binaryset_sums sums_unique)
    1.24  
    1.25 -subsection \<open>Properties of a premeasure @{term \<mu>}\<close>
    1.26 +subsection%unimportant \<open>Properties of a premeasure @{term \<mu>}\<close>
    1.27  
    1.28  text \<open>
    1.29    The definitions for @{const positive} and @{const countably_additive} should be here, by they are
    1.30 @@ -442,7 +442,7 @@
    1.31    using empty_continuous_imp_continuous_from_below[OF f fin] cont
    1.32    by blast
    1.33  
    1.34 -subsection \<open>Properties of @{const emeasure}\<close>
    1.35 +subsection%unimportant \<open>Properties of @{const emeasure}\<close>
    1.36  
    1.37  lemma emeasure_positive: "positive (sets M) (emeasure M)"
    1.38    by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)
    1.39 @@ -881,7 +881,7 @@
    1.40  
    1.41  subsection \<open>\<open>\<mu>\<close>-null sets\<close>
    1.42  
    1.43 -definition null_sets :: "'a measure \<Rightarrow> 'a set set" where
    1.44 +definition%important null_sets :: "'a measure \<Rightarrow> 'a set set" where
    1.45    "null_sets M = {N\<in>sets M. emeasure M N = 0}"
    1.46  
    1.47  lemma null_setsD1[dest]: "A \<in> null_sets M \<Longrightarrow> emeasure M A = 0"
    1.48 @@ -989,7 +989,7 @@
    1.49  
    1.50  subsection \<open>The almost everywhere filter (i.e.\ quantifier)\<close>
    1.51  
    1.52 -definition ae_filter :: "'a measure \<Rightarrow> 'a filter" where
    1.53 +definition%important ae_filter :: "'a measure \<Rightarrow> 'a filter" where
    1.54    "ae_filter M = (INF N:null_sets M. principal (space M - N))"
    1.55  
    1.56  abbreviation almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
    1.57 @@ -1265,7 +1265,7 @@
    1.58  
    1.59  subsection \<open>\<open>\<sigma>\<close>-finite Measures\<close>
    1.60  
    1.61 -locale sigma_finite_measure =
    1.62 +locale%important sigma_finite_measure =
    1.63    fixes M :: "'a measure"
    1.64    assumes sigma_finite_countable:
    1.65      "\<exists>A::'a set set. countable A \<and> A \<subseteq> sets M \<and> (\<Union>A) = space M \<and> (\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>)"
    1.66 @@ -1387,7 +1387,7 @@
    1.67  
    1.68  subsection \<open>Measure space induced by distribution of @{const measurable}-functions\<close>
    1.69  
    1.70 -definition distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
    1.71 +definition%important distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
    1.72    "distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
    1.73  
    1.74  lemma
    1.75 @@ -1513,12 +1513,12 @@
    1.76    "f \<in> measurable M N \<Longrightarrow> A \<in> null_sets (distr M N f) \<longleftrightarrow> f -` A \<inter> space M \<in> null_sets M \<and> A \<in> sets N"
    1.77    by (auto simp add: null_sets_def emeasure_distr)
    1.78  
    1.79 -lemma distr_distr:
    1.80 +lemma%important distr_distr:
    1.81    "g \<in> measurable N L \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> distr (distr M N f) L g = distr M L (g \<circ> f)"
    1.82    by (auto simp add: emeasure_distr measurable_space
    1.83             intro!: arg_cong[where f="emeasure M"] measure_eqI)
    1.84  
    1.85 -subsection \<open>Real measure values\<close>
    1.86 +subsection%unimportant \<open>Real measure values\<close>
    1.87  
    1.88  lemma ring_of_finite_sets: "ring_of_sets (space M) {A\<in>sets M. emeasure M A \<noteq> top}"
    1.89  proof (rule ring_of_setsI)
    1.90 @@ -1705,7 +1705,7 @@
    1.91  
    1.92  subsection \<open>Set of measurable sets with finite measure\<close>
    1.93  
    1.94 -definition fmeasurable :: "'a measure \<Rightarrow> 'a set set"
    1.95 +definition%important fmeasurable :: "'a measure \<Rightarrow> 'a set set"
    1.96  where
    1.97    "fmeasurable M = {A\<in>sets M. emeasure M A < \<infinity>}"
    1.98  
    1.99 @@ -1972,7 +1972,7 @@
   1.100  
   1.101  subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
   1.102  
   1.103 -locale finite_measure = sigma_finite_measure M for M +
   1.104 +locale%important finite_measure = sigma_finite_measure M for M +
   1.105    assumes finite_emeasure_space: "emeasure M (space M) \<noteq> top"
   1.106  
   1.107  lemma finite_measureI[Pure.intro!]:
   1.108 @@ -2194,7 +2194,7 @@
   1.109      using bound[of x] sets_eq_imp_space_eq[OF sets] by (simp add: iter)
   1.110  qed (auto simp add: iter le_fun_def INF_apply[abs_def] intro!: meas cont)
   1.111  
   1.112 -subsection \<open>Counting space\<close>
   1.113 +subsection%unimportant \<open>Counting space\<close>
   1.114  
   1.115  lemma strict_monoI_Suc:
   1.116    assumes ord [simp]: "(\<And>n. f n < f (Suc n))" shows "strict_mono f"
   1.117 @@ -2343,7 +2343,7 @@
   1.118    show "sigma_finite_measure (count_space A)" ..
   1.119  qed
   1.120  
   1.121 -subsection \<open>Measure restricted to space\<close>
   1.122 +subsection%unimportant \<open>Measure restricted to space\<close>
   1.123  
   1.124  lemma emeasure_restrict_space:
   1.125    assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
   1.126 @@ -2502,7 +2502,7 @@
   1.127    finally show "emeasure M X = emeasure N X" .
   1.128  qed fact
   1.129  
   1.130 -subsection \<open>Null measure\<close>
   1.131 +subsection%unimportant \<open>Null measure\<close>
   1.132  
   1.133  definition "null_measure M = sigma (space M) (sets M)"
   1.134  
   1.135 @@ -2525,7 +2525,7 @@
   1.136  
   1.137  subsection \<open>Scaling a measure\<close>
   1.138  
   1.139 -definition scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
   1.140 +definition%important scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
   1.141  where
   1.142    "scale_measure r M = measure_of (space M) (sets M) (\<lambda>A. r * emeasure M A)"
   1.143  
   1.144 @@ -2703,11 +2703,11 @@
   1.145    qed auto
   1.146  qed
   1.147  
   1.148 -lemma unsigned_Hahn_decomposition:
   1.149 +lemma%important unsigned_Hahn_decomposition:
   1.150    assumes [simp]: "sets N = sets M" and [measurable]: "A \<in> sets M"
   1.151      and [simp]: "emeasure M A \<noteq> top" "emeasure N A \<noteq> top"
   1.152    shows "\<exists>Y\<in>sets M. Y \<subseteq> A \<and> (\<forall>X\<in>sets M. X \<subseteq> Y \<longrightarrow> N X \<le> M X) \<and> (\<forall>X\<in>sets M. X \<subseteq> A \<longrightarrow> X \<inter> Y = {} \<longrightarrow> M X \<le> N X)"
   1.153 -proof -
   1.154 +proof%unimportant -
   1.155    have "\<exists>Y\<in>sets (restrict_space M A).
   1.156      (\<forall>X\<in>sets (restrict_space M A). X \<subseteq> Y \<longrightarrow> (restrict_space N A) X \<le> (restrict_space M A) X) \<and>
   1.157      (\<forall>X\<in>sets (restrict_space M A). X \<inter> Y = {} \<longrightarrow> (restrict_space M A) X \<le> (restrict_space N A) X)"
   1.158 @@ -2728,12 +2728,12 @@
   1.159      done
   1.160  qed
   1.161  
   1.162 -text \<open>
   1.163 +text%important \<open>
   1.164    Define a lexicographical order on @{type measure}, in the order space, sets and measure. The parts
   1.165    of the lexicographical order are point-wise ordered.
   1.166  \<close>
   1.167  
   1.168 -instantiation measure :: (type) order_bot
   1.169 +instantiation%important measure :: (type) order_bot
   1.170  begin
   1.171  
   1.172  inductive less_eq_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
   1.173 @@ -2746,10 +2746,10 @@
   1.174      if sets M = sets N then emeasure M \<le> emeasure N else sets M \<subseteq> sets N else space M \<subseteq> space N)"
   1.175    by (auto elim: less_eq_measure.cases intro: less_eq_measure.intros)
   1.176  
   1.177 -definition less_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
   1.178 +definition%important less_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
   1.179    "less_measure M N \<longleftrightarrow> (M \<le> N \<and> \<not> N \<le> M)"
   1.180  
   1.181 -definition bot_measure :: "'a measure" where
   1.182 +definition%important bot_measure :: "'a measure" where
   1.183    "bot_measure = sigma {} {}"
   1.184  
   1.185  lemma
   1.186 @@ -2766,13 +2766,14 @@
   1.187  
   1.188  end
   1.189  
   1.190 -lemma le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
   1.191 +lemma%important le_measure: "sets M = sets N \<Longrightarrow> M \<le> N \<longleftrightarrow> (\<forall>A\<in>sets M. emeasure M A \<le> emeasure N A)"
   1.192 +  apply%unimportant -
   1.193    apply (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq)
   1.194    subgoal for X
   1.195      by (cases "X \<in> sets M") (auto simp: emeasure_notin_sets)
   1.196    done
   1.197  
   1.198 -definition sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
   1.199 +definition%important sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
   1.200  where
   1.201    "sup_measure' A B = measure_of (space A) (sets A) (\<lambda>X. SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
   1.202  
   1.203 @@ -2900,7 +2901,7 @@
   1.204    qed
   1.205  qed simp_all
   1.206  
   1.207 -definition sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.208 +definition%important sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   1.209  where
   1.210    "sup_lexord A B k s c =
   1.211      (if k A = k B then c else if \<not> k A \<le> k B \<and> \<not> k B \<le> k A then s else if k B \<le> k A then A else B)"
   1.212 @@ -2926,10 +2927,10 @@
   1.213       (simp_all add: eq_commute[of _ "sets x"] le_measure_iff emeasure_sigma le_fun_def
   1.214                      sigma_sets_superset_generator sigma_sets_le_sets_iff)
   1.215  
   1.216 -instantiation measure :: (type) semilattice_sup
   1.217 +instantiation%important measure :: (type) semilattice_sup
   1.218  begin
   1.219  
   1.220 -definition sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
   1.221 +definition%important sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
   1.222  where
   1.223    "sup_measure A B =
   1.224      sup_lexord A B space (sigma (space A \<union> space B) {})
   1.225 @@ -3057,7 +3058,7 @@
   1.226      by (simp add: A(3))
   1.227  qed
   1.228  
   1.229 -instantiation measure :: (type) complete_lattice
   1.230 +instantiation%important measure :: (type) complete_lattice
   1.231  begin
   1.232  
   1.233  interpretation sup_measure: comm_monoid_set sup "bot :: 'a measure"
   1.234 @@ -3092,7 +3093,7 @@
   1.235    "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> sets i = sets M) \<Longrightarrow> sets (sup_measure.F id I) = sets M"
   1.236    by (induction I rule: finite_ne_induct) (simp_all add: sets_sup)
   1.237  
   1.238 -definition Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
   1.239 +definition%important Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
   1.240  where
   1.241    "Sup_measure' M = measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
   1.242      (\<lambda>X. (SUP P:{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
   1.243 @@ -3163,20 +3164,20 @@
   1.244      using assms * by auto
   1.245  qed (rule UN_space_closed)
   1.246  
   1.247 -definition Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
   1.248 +definition%important Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
   1.249  where
   1.250    "Sup_measure = Sup_lexord space (Sup_lexord sets Sup_measure'
   1.251      (\<lambda>U. sigma (\<Union>u\<in>U. space u) (\<Union>u\<in>U. sets u))) (\<lambda>U. sigma (\<Union>u\<in>U. space u) {})"
   1.252  
   1.253 -definition Inf_measure :: "'a measure set \<Rightarrow> 'a measure"
   1.254 +definition%important Inf_measure :: "'a measure set \<Rightarrow> 'a measure"
   1.255  where
   1.256    "Inf_measure A = Sup {x. \<forall>a\<in>A. x \<le> a}"
   1.257  
   1.258 -definition inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
   1.259 +definition%important inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
   1.260  where
   1.261    "inf_measure a b = Inf {a, b}"
   1.262  
   1.263 -definition top_measure :: "'a measure"
   1.264 +definition%important top_measure :: "'a measure"
   1.265  where
   1.266    "top_measure = Inf {}"
   1.267  
   1.268 @@ -3417,7 +3418,7 @@
   1.269    qed
   1.270  qed
   1.271  
   1.272 -subsubsection \<open>Supremum of a set of $\sigma$-algebras\<close>
   1.273 +subsubsection%unimportant \<open>Supremum of a set of $\sigma$-algebras\<close>
   1.274  
   1.275  lemma space_Sup_eq_UN: "space (Sup M) = (\<Union>x\<in>M. space x)"
   1.276    unfolding Sup_measure_def