Quelle Measure_Space.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Measure_Space.thy
    Author:     Lawrence C Paulson
    Author:     Johannes Hölzl, TU München
    Author:     Armin Heller, TU München
*)

section \<open>Measure Spaces\<close>

theory Measure_Space
imports
  Measurable "HOL-Library.Extended_Nonnegative_Real"
begin

subsection\<^marker>\<open>tag unimportant\<close> "Relate extended reals and the indicator function"

lemma suminf_cmult_indicator:
  fixes f :: "nat \ ennreal"
  assumes "disjoint_family A" "x \ A i"
  shows "(\n. f n * indicator (A n) x) = f i"
proof -
  have **: "\n. f n * indicator (A n) x = (if n = i then f n else 0 :: ennreal)"
    using \<open>x \<in> A i\<close> assms unfolding disjoint_family_on_def indicator_def by auto
  then have "\n. (\j
    by (auto simp: sum.If_cases)
  moreover have "(SUP n. if i < n then f i else 0) = (f i :: ennreal)"
  proof (rule SUP_eqI)
    fix y :: ennreal assume "\n. n \ UNIV \ (if i < n then f i else 0) \ y"
    from this[of "Suc i"] show "f i \ y" by auto
  qed (use assms in simp)
  ultimately show ?thesis using assms
    by (simp add: suminf_eq_SUP)
qed

lemma suminf_indicator:
  assumes "disjoint_family A"
  shows "(\n. indicator (A n) x :: ennreal) = indicator (\i. A i) x"
proof cases
  assume *: "x \ (\i. A i)"
  then obtain i where "x \ A i" by auto
  from suminf_cmult_indicator[OF assms(1), OF \<open>x \<in> A i\<close>, of "\<lambda>k. 1"]
  show ?thesis using * by simp
qed simp

lemma sum_indicator_disjoint_family:
  fixes f :: "'d \ 'e::semiring_1"
  assumes d: "disjoint_family_on A P" and "x \ A j" and "finite P" and "j \ P"
  shows "(\i\P. f i * indicator (A i) x) = f j"
proof -
  have "P \ {i. x \ A i} = {j}"
    using d \<open>x \<in> A j\<close> \<open>j \<in> P\<close> unfolding disjoint_family_on_def
    by auto
  with \<open>finite P\<close> show ?thesis
    by (simp add: indicator_def)
qed

text \<open>
  The type for emeasure spaces is already defined in \<^theory>\<open>HOL-Analysis.Sigma_Algebra\<close>, as it
  is also used to represent sigma algebras (with an arbitrary emeasure).
\<close>

subsection\<^marker>\<open>tag unimportant\<close> "Extend binary sets"

lemma LIMSEQ_binaryset:
  assumes f: "f {} = 0"
  shows  "(\n. \i f A + f B"
proof -
  have "(\n. \i < Suc (Suc n). f (binaryset A B i)) = (\n. f A + f B)"
    proof
      fix n
      show "(\i < Suc (Suc n). f (binaryset A B i)) = f A + f B"
        by (induct n)  (auto simp: binaryset_def f)
    qed
  thus ?thesis
    by (simp add: LIMSEQ_imp_Suc)
qed

lemma binaryset_sums:
  assumes f: "f {} = 0"
  shows  "(\n. f (binaryset A B n)) sums (f A + f B)"
  using LIMSEQ_binaryset f sums_def by blast

lemma suminf_binaryset_eq:
  fixes f :: "'a set \ 'b::{comm_monoid_add, t2_space}"
  shows "f {} = 0 \ (\n. f (binaryset A B n)) = f A + f B"
  by (metis binaryset_sums sums_unique)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Properties of a premeasure \<^term>\<open>\<mu>\<close>\<close>

text \<open>
  The definitions for \<^const>\<open>positive\<close> and \<^const>\<open>countably_additive\<close> should be here, by they are
  necessary to define \<^typ>\<open>'a measure\<close> in \<^theory>\<open>HOL-Analysis.Sigma_Algebra\<close>.
\<close>

definition subadditive where
  "subadditive M f \ (\x\M. \y\M. x \ y = {} \ f (x \ y) \ f x + f y)"

lemma subadditiveD: "subadditive M f \ x \ y = {} \ x \ M \ y \ M \ f (x \ y) \ f x + f y"
  by (auto simp: subadditive_def)

definition countably_subadditive where
  "countably_subadditive M f \
    (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))))"

lemma (in ring_of_sets) countably_subadditive_subadditive:
  fixes f :: "'a set \ ennreal"
  assumes f: "positive M f" and cs: "countably_subadditive M f"
  shows  "subadditive M f"
proof (auto simp: subadditive_def)
  fix x y
  assume x: "x \ M" and y: "y \ M" and "x \ y = {}"
  hence "disjoint_family (binaryset x y)"
    by (auto simp: disjoint_family_on_def binaryset_def)
  hence "range (binaryset x y) \ M \
         (\<Union>i. binaryset x y i) \<in> M \<longrightarrow>
         f (\<Union>i. binaryset x y i) \<le> (\<Sum> n. f (binaryset x y n))"
    using cs by (auto simp: countably_subadditive_def)
  hence "{x,y,{}} \ M \ x \ y \ M \
         f (x \<union> y) \<le> (\<Sum> n. f (binaryset x y n))"
    by (simp add: range_binaryset_eq UN_binaryset_eq)
  thus "f (x \ y) \ f x + f y" using f x y
    by (auto simp: Un o_def suminf_binaryset_eq positive_def)
qed

definition additive where
  "additive M \ \ (\x\M. \y\M. x \ y = {} \ \ (x \ y) = \ x + \ y)"

definition increasing where
  "increasing M \ \ (\x\M. \y\M. x \ y \ \ x \ \ y)"

lemma positiveD1: "positive M f \ f {} = 0" by (auto simp: positive_def)

lemma positiveD_empty:
  "positive M f \ f {} = 0"
  by (auto simp: positive_def)

lemma additiveD:
  "additive M f \ x \ y = {} \ x \ M \ y \ M \ f (x \ y) = f x + f y"
  by (auto simp: additive_def)

lemma increasingD:
  "increasing M f \ x \ y \ x\M \ y\M \ f x \ f y"
  by (auto simp: increasing_def)

lemma countably_additiveI[case_names countably]:
  "(\A. \range A \ M; disjoint_family A; (\i. A i) \ M\ \ (\i. f(A i)) = f(\i. A i))
  \<Longrightarrow> countably_additive M f"
  by (simp add: countably_additive_def)

lemma (in ring_of_sets) disjointed_additive:
  assumes f: "positive M f" "additive M f" and A: "range A \ M" "incseq A"
  shows "(\i\n. f (disjointed A i)) = f (A n)"
proof (induct n)
  case (Suc n)
  then have "(\i\Suc n. f (disjointed A i)) = f (A n) + f (disjointed A (Suc n))"
    by simp
  also have "\ = f (A n \ disjointed A (Suc n))"
    using A by (subst f(2)[THEN additiveD]) (auto simp: disjointed_mono)
  also have "A n \ disjointed A (Suc n) = A (Suc n)"
    using \<open>incseq A\<close> by (auto dest: incseq_SucD simp: disjointed_mono)
  finally show ?case .
qed simp

lemma (in ring_of_sets) additive_sum:
  fixes A:: "'i \ 'a set"
  assumes f: "positive M f" and ad: "additive M f" and "finite S"
      and A: "A`S \ M"
      and disj: "disjoint_family_on A S"
  shows  "(\i\S. f (A i)) = f (\i\S. A i)"
  using \<open>finite S\<close> disj A
proof induct
  case empty show ?case using f by (simp add: positive_def)
next
  case (insert s S)
  then have "A s \ (\i\S. A i) = {}"
    by (auto simp: disjoint_family_on_def neq_iff)
  moreover
  have "A s \ M" using insert by blast
  moreover have "(\i\S. A i) \ M"
    using insert \<open>finite S\<close> by auto
  ultimately have "f (A s \ (\i\S. A i)) = f (A s) + f(\i\S. A i)"
    using ad UNION_in_sets A by (auto simp: additive_def)
  with insert show ?case using ad disjoint_family_on_mono[of S "insert s S" A]
    by (auto simp: additive_def subset_insertI)
qed

lemma (in ring_of_sets) additive_increasing:
  fixes f :: "'a set \ ennreal"
  assumes posf: "positive M f" and addf: "additive M f"
  shows "increasing M f"
proof (auto simp: increasing_def)
  fix x y
  assume xy: "x \ M" "y \ M" "x \ y"
  then have "y - x \ M" by auto
  then have "f x + 0 \ f x + f (y-x)" by (intro add_left_mono zero_le)
  also have "\ = f (x \ (y-x))"
    by (metis addf Diff_disjoint \<open>y - x \<in> M\<close> additiveD xy(1))
  also have "\ = f y"
    by (metis Un_Diff_cancel Un_absorb1 xy(3))
  finally show "f x \ f y" by simp
qed

lemma (in ring_of_sets) subadditive:
  fixes f :: "'a set \ ennreal"
  assumes f: "positive M f" "additive M f" and A: "A`S \ M" and S: "finite S"
  shows "f (\i\S. A i) \ (\i\S. f (A i))"
using S A
proof (induct S)
  case empty thus ?case using f by (auto simp: positive_def)
next
  case (insert x F)
  hence in_M: "A x \ M" "(\i\F. A i) \ M" "(\i\F. A i) - A x \ M" using A by force+
  have subs: "(\i\F. A i) - A x \ (\i\F. A i)" by auto
  have "(\i\(insert x F). A i) = A x \ ((\i\F. A i) - A x)" by auto
  hence "f (\i\(insert x F). A i) = f (A x \ ((\i\F. A i) - A x))"
    by simp
  also have "\ = f (A x) + f ((\i\F. A i) - A x)"
    using f(2) by (rule additiveD) (insert in_M, auto)
  also have "\ \ f (A x) + f (\i\F. A i)"
    using additive_increasing[OF f] in_M subs
    by (simp add: increasingD)
  also have "\ \ f (A x) + (\i\F. f (A i))"
    using insert by (auto intro: add_left_mono)
  finally show "f (\i\(insert x F). A i) \ (\i\(insert x F). f (A i))"
    by (simp add: insert)
qed

lemma (in ring_of_sets) countably_additive_additive:
  fixes f :: "'a set \ ennreal"
  assumes posf: "positive M f" and ca: "countably_additive M f"
  shows "additive M f"
proof (auto simp: additive_def)
  fix x y
  assume x: "x \ M" and y: "y \ M" and "x \ y = {}"
  hence "disjoint_family (binaryset x y)"
    by (auto simp: disjoint_family_on_def binaryset_def)
  hence "range (binaryset x y) \ M \
         (\<Union>i. binaryset x y i) \<in> M \<longrightarrow>
         f (\<Union>i. binaryset x y i) = (\<Sum> n. f (binaryset x y n))"
    using ca by (simp add: countably_additive_def)
  hence "{x,y,{}} \ M \ x \ y \ M \ f (x \ y) = (\n. f (binaryset x y n))"
    by (simp add: range_binaryset_eq UN_binaryset_eq)
  thus "f (x \ y) = f x + f y" using posf x y
    by (auto simp: Un suminf_binaryset_eq positive_def)
qed

lemma (in algebra) increasing_additive_bound:
  fixes A:: "nat \ 'a set" and f :: "'a set \ ennreal"
  assumes f: "positive M f" and ad: "additive M f"
      and inc: "increasing M f"
      and A: "range A \ M"
      and disj: "disjoint_family A"
  shows  "(\i. f (A i)) \ f \"
proof (safe intro!: suminf_le_const)
  fix N
  note disj_N = disjoint_family_on_mono[OF _ disj, of "{..]
  have "(\ii\{..
    using A by (intro additive_sum [OF f ad]) (auto simp: disj_N)
  also have "\ \ f \" using space_closed A
    by (intro increasingD[OF inc] finite_UN) auto
  finally show "(\i f \" by simp
qed (use f A in \<open>auto simp: positive_def\<close>)

lemma (in ring_of_sets) countably_additiveI_finite:
  fixes \<mu> :: "'a set \<Rightarrow> ennreal"
  assumes "finite \" "positive M \" "additive M \"
  shows "countably_additive M \"
proof (rule countably_additiveI)
  fix F :: "nat \ 'a set" assume F: "range F \ M" "(\i. F i) \ M" and disj: "disjoint_family F"

  have "\i. F i \ {} \ (\x. x \ F i)" by auto
  then obtain f where f: "\i. F i \ {} \ f i \ F i" by metis

  have finU: "finite (\i. F i)"
    by (metis F(2) assms(1) infinite_super sets_into_space)

  have F_subset: "{i. \ (F i) \ 0} \ {i. F i \ {}}"
    by (auto simp: positiveD_empty[OF \<open>positive M \<mu>\<close>])
  moreover have fin_not_empty: "finite {i. F i \ {}}"
  proof (rule finite_imageD)
    from f have "f`{i. F i \ {}} \ (\i. F i)" by auto
    then show "finite (f`{i. F i \ {}})"
      by (simp add: finU finite_subset)
    show inj_f: "inj_on f {i. F i \ {}}"
      using f disj
      by (simp add: inj_on_def disjoint_family_on_def disjoint_iff) metis
  qed
  ultimately have fin_not_0: "finite {i. \ (F i) \ 0}"
    by (rule finite_subset)

  have disj_not_empty: "disjoint_family_on F {i. F i \ {}}"
    using disj by (auto simp: disjoint_family_on_def)

  from fin_not_0 have "(\i. \ (F i)) = (\i | \ (F i) \ 0. \ (F i))"
    by (rule suminf_finite) auto
  also have "\ = (\i | F i \ {}. \ (F i))"
    using fin_not_empty F_subset by (rule sum.mono_neutral_left) auto
  also have "\ = \ (\i\{i. F i \ {}}. F i)"
    using \<open>positive M \<mu>\<close> \<open>additive M \<mu>\<close> fin_not_empty disj_not_empty F by (intro additive_sum) auto
  also have "\ = \ (\i. F i)"
    by (rule arg_cong[where f=\<mu>]) auto
  finally show "(\i. \ (F i)) = \ (\i. F i)" .
qed

lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
  fixes f :: "'a set \ ennreal"
  assumes f: "positive M f" "additive M f"
  shows "countably_additive M f \
    (\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i))"
  unfolding countably_additive_def
proof safe
  assume count_sum: "\A. range A \ M \ disjoint_family A \ \(A ` UNIV) \ M \ (\i. f (A i)) = f (\(A ` UNIV))"
  fix A :: "nat \ 'a set" assume A: "range A \ M" "incseq A" "(\i. A i) \ M"
  then have dA: "range (disjointed A) \ M" by (auto simp: range_disjointed_sets)
  with count_sum[THEN spec, of "disjointed A"] A(3)
  have f_UN: "(\i. f (disjointed A i)) = f (\i. A i)"
    by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
  moreover have "(\n. (\i (\i. f (disjointed A i))"
    by (simp add: summable_LIMSEQ)
  from LIMSEQ_Suc[OF this]
  have "(\n. (\i\n. f (disjointed A i))) \ (\i. f (disjointed A i))"
    unfolding lessThan_Suc_atMost .
  moreover have "\n. (\i\n. f (disjointed A i)) = f (A n)"
    using disjointed_additive[OF f A(1,2)] .
  ultimately show "(\i. f (A i)) \ f (\i. A i)" by simp
next
  assume cont[rule_format]: "\A. range A \ M \ incseq A \ (\i. A i) \ M \ (\i. f (A i)) \ f (\i. A i)"
  fix A :: "nat \ 'a set" assume A: "range A \ M" "disjoint_family A" "(\i. A i) \ M"
  have *: "(\n. (\ii. A i)" by auto
  have "range (\i. \i M" "(\i. \i M"
    using A * by auto
  then have "(\n. f (\i f (\i. A i)"
    unfolding *[symmetric] by (force intro!: cont incseq_SucI)+
  moreover have "\n. f (\ii
    using A
    by (intro additive_sum[OF f, symmetric]) (auto intro: disjoint_family_on_mono)
  ultimately
  have "(\i. f (A i)) sums f (\i. A i)"
    unfolding sums_def by simp
  then show "(\i. f (A i)) = f (\i. A i)"
    by (metis sums_unique)
qed

lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
  fixes f :: "'a set \ ennreal"
  assumes f: "positive M f" "additive M f"
  shows "(\A. range A \ M \ decseq A \ (\i. A i) \ M \ (\i. f (A i) \ \) \ (\i. f (A i)) \ f (\i. A i))
     \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0)"
proof safe
  assume cont[rule_format]: "(\A. range A \ M \ decseq A \ (\i. A i) \ M \ (\i. f (A i) \ \) \ (\i. f (A i)) \ f (\i. A i))"
  fix A :: "nat \ 'a set"
  assume A: "range A \ M" "decseq A" "(\i. A i) = {}" "\i. f (A i) \ \"
  with cont[of A] show "(\i. f (A i)) \ 0"
    using \<open>positive M f\<close>[unfolded positive_def] by auto
next
  assume cont[rule_format]: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i) \ \) \ (\i. f (A i)) \ 0"
  fix A :: "nat \ 'a set"
  assume A: "range A \ M" "decseq A" "(\i. A i) \ M" "\i. f (A i) \ \"

  have f_mono: "\a b. a \ M \ b \ M \ a \ b \ f a \ f b"
    using additive_increasing[OF f] unfolding increasing_def by simp

  have decseq_fA: "decseq (\i. f (A i))"
    using A by (auto simp: decseq_def intro!: f_mono)
  have decseq: "decseq (\i. A i - (\i. A i))"
    using A by (auto simp: decseq_def)
  then have decseq_f: "decseq (\i. f (A i - (\i. A i)))"
    using A unfolding decseq_def by (auto intro!: f_mono Diff)
  have "f (\x. A x) \ f (A 0)"
    using A by (auto intro!: f_mono)
  then have f_Int_fin: "f (\x. A x) \ \"
    using A by (auto simp: top_unique)
  have f_fin: "f (A i - (\i. A i)) \ \" for i
    using A by (metis Diff Diff_subset f_mono infinity_ennreal_def range_subsetD top_unique)
  have "(\i. f (A i - (\i. A i))) \ 0"
  proof (intro cont[ OF _ decseq _ f_fin])
    show "range (\i. A i - (\i. A i)) \ M" "(\i. A i - (\i. A i)) = {}"
      using A by auto
  qed
  with INF_Lim decseq_f have "(INF n. f (A n - (\i. A i))) = 0" by metis
  moreover have "(INF n. f (\i. A i)) = f (\i. A i)"
    by auto
  ultimately have "(INF n. f (A n - (\i. A i)) + f (\i. A i)) = 0 + f (\i. A i)"
    using A(4) f_fin f_Int_fin
    using INF_ennreal_add_const by presburger
  moreover {
    fix n
    have "f (A n - (\i. A i)) + f (\i. A i) = f ((A n - (\i. A i)) \ (\i. A i))"
      using A f(2)
      by (metis (no_types) Diff Diff_disjoint add.commute additiveD range_subsetD sup_commute)
    also have "(A n - (\i. A i)) \ (\i. A i) = A n"
      by auto
    finally have "f (A n - (\i. A i)) + f (\i. A i) = f (A n)" . }
  ultimately have "(INF n. f (A n)) = f (\i. A i)"
    by simp
  with LIMSEQ_INF[OF decseq_fA]
  show "(\i. f (A i)) \ f (\i. A i)" by simp
qed

lemma (in ring_of_sets) empty_continuous_imp_continuous_from_below:
  fixes f :: "'a set \ ennreal"
  assumes f: "positive M f" "additive M f" "\A\M. f A \ \"
  assumes cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) \ 0"
  assumes A: "range A \ M" "incseq A" "(\i. A i) \ M"
  shows "(\i. f (A i)) \ f (\i. A i)"
proof -
  from A have "(\i. f ((\i. A i) - A i)) \ 0"
    by (intro cont[rule_format]) (auto simp: decseq_def incseq_def)
  moreover
  { fix i
    have "f ((\i. A i) - A i \ A i) = f ((\i. A i) - A i) + f (A i)"
      using A by (intro f(2)[THEN additiveD]) auto
    also have "((\i. A i) - A i) \ A i = (\i. A i)"
      by auto
    finally have "f ((\i. A i) - A i) = f (\i. A i) - f (A i)"
      using assms f by fastforce
  }
  moreover have "\\<^sub>F i in sequentially. f (A i) \ f (\i. A i)"
    using increasingD[OF additive_increasing[OF f(1, 2)], of "A _" "\i. A i"] A
    by (auto intro!: always_eventually simp: subset_eq)
  ultimately show "(\i. f (A i)) \ f (\i. A i)"
    by (auto intro: ennreal_tendsto_const_minus)
qed

lemma (in ring_of_sets) empty_continuous_imp_countably_additive:
  fixes f :: "'a set \ ennreal"
  assumes f: "positive M f" "additive M f" and fin: "\A\M. f A \ \"
  assumes cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) \ 0"
  shows "countably_additive M f"
  using countably_additive_iff_continuous_from_below[OF f]
  using empty_continuous_imp_continuous_from_below[OF f fin] cont
  by blast

subsection\<^marker>\<open>tag unimportant\<close> \<open>Properties of \<^const>\<open>emeasure\<close>\<close>

lemma emeasure_positive: "positive (sets M) (emeasure M)"
  by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)

lemma emeasure_empty[simp, intro]: "emeasure M {} = 0"
  using emeasure_positive[of M] by (simp add: positive_def)

lemma emeasure_single_in_space: "emeasure M {x} \ 0 \ x \ space M"
  using emeasure_notin_sets[of "{x}" M] by (auto dest: sets.sets_into_space zero_less_iff_neq_zero[THEN iffD2])

lemma emeasure_countably_additive: "countably_additive (sets M) (emeasure M)"
  by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)

lemma suminf_emeasure:
  "range A \ sets M \ disjoint_family A \ (\i. emeasure M (A i)) = emeasure M (\i. A i)"
  using sets.countable_UN[of A UNIV M] emeasure_countably_additive[of M]
  by (simp add: countably_additive_def)

lemma sums_emeasure:
  "disjoint_family F \ (\i. F i \ sets M) \ (\i. emeasure M (F i)) sums emeasure M (\i. F i)"
  unfolding sums_iff by (intro conjI suminf_emeasure) auto

lemma emeasure_additive: "additive (sets M) (emeasure M)"
  by (metis sets.countably_additive_additive emeasure_positive emeasure_countably_additive)

lemma plus_emeasure:
  "a \ sets M \ b \ sets M \ a \ b = {} \ emeasure M a + emeasure M b = emeasure M (a \ b)"
  using additiveD[OF emeasure_additive] ..

lemma emeasure_Un:
  "A \ sets M \ B \ sets M \ emeasure M (A \ B) = emeasure M A + emeasure M (B - A)"
  using plus_emeasure[of A M "B - A"] by auto

lemma emeasure_Un_Int:
  assumes "A \ sets M" "B \ sets M"
  shows "emeasure M A + emeasure M B = emeasure M (A \ B) + emeasure M (A \ B)"
proof -
  have "A = (A-B) \ (A \ B)" by auto
  then have "emeasure M A = emeasure M (A-B) + emeasure M (A \ B)"
    by (metis Diff_Diff_Int Diff_disjoint assms plus_emeasure sets.Diff)
  moreover have "A \ B = (A-B) \ B" by auto
  then have "emeasure M (A \ B) = emeasure M (A-B) + emeasure M B"
    by (metis Diff_disjoint Int_commute assms plus_emeasure sets.Diff)
  ultimately show ?thesis by (metis add.assoc add.commute)
qed

lemma sum_emeasure:
  "F`I \ sets M \ disjoint_family_on F I \ finite I \
    (\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)"
  by (metis sets.additive_sum emeasure_positive emeasure_additive)

lemma emeasure_mono:
  "a \ b \ b \ sets M \ emeasure M a \ emeasure M b"
  by (metis zero_le sets.additive_increasing emeasure_additive emeasure_notin_sets emeasure_positive increasingD)

lemma emeasure_space:
  "emeasure M A \ emeasure M (space M)"
  by (metis emeasure_mono emeasure_notin_sets sets.sets_into_space sets.top zero_le)

lemma emeasure_Diff:
  assumes \<infinity>: "emeasure M B \<noteq> \<infinity>"
  and "A \ sets M" "B \ sets M" and "B \ A"
shows "emeasure M (A - B) = emeasure M A - emeasure M B"
proof -
  have "emeasure M B + emeasure M (A - B) = emeasure M (B \ (A-B))"
    by (simp add: assms emeasure_Un)
  also have "... = emeasure M A"
    using Diff_partition \<open>B \<subseteq> A\<close> by fastforce
  finally show ?thesis
    by (metis \<infinity> ennreal_add_diff_cancel_left infinity_ennreal_def)
qed

lemma emeasure_compl:
  "s \ sets M \ emeasure M s \ \ \ emeasure M (space M - s) = emeasure M (space M) - emeasure M s"
  by (simp add: emeasure_Diff sets.sets_into_space)

lemma Lim_emeasure_incseq:
  "range A \ sets M \ incseq A \ (\i. (emeasure M (A i))) \ emeasure M (\i. A i)"
  using emeasure_countably_additive
  by (metis emeasure_additive emeasure_positive sets.countable_UN
      sets.countably_additive_iff_continuous_from_below)

lemma incseq_emeasure:
  assumes "range B \ sets M" "incseq B"
  shows "incseq (\i. emeasure M (B i))"
  using assms by (auto simp: incseq_def intro!: emeasure_mono)

lemma SUP_emeasure_incseq:
  assumes A: "range A \ sets M" "incseq A"
  shows "(SUP n. emeasure M (A n)) = emeasure M (\i. A i)"
  using LIMSEQ_SUP[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
  by (simp add: LIMSEQ_unique)

lemma decseq_emeasure:
  assumes "range B \ sets M" "decseq B"
  shows "decseq (\i. emeasure M (B i))"
  using assms by (auto simp: decseq_def intro!: emeasure_mono)

lemma INF_emeasure_decseq:
  assumes A: "range A \ sets M" and "decseq A"
  and finite: "\i. emeasure M (A i) \ \"
  shows "(INF n. emeasure M (A n)) = emeasure M (\i. A i)"
proof -
  have le_MI: "emeasure M (\i. A i) \ emeasure M (A 0)"
    using A by (auto intro!: emeasure_mono)
  hence *: "emeasure M (\i. A i) \ \" using finite[of 0] by (auto simp: top_unique)

  have "emeasure M (A 0) - (INF n. emeasure M (A n)) = (SUP n. emeasure M (A 0) - emeasure M (A n))"
    by (simp add: ennreal_INF_const_minus)
  also have "\ = (SUP n. emeasure M (A 0 - A n))"
    using A finite \<open>decseq A\<close>[unfolded decseq_def] by (subst emeasure_Diff) auto
  also have "\ = emeasure M (\i. A 0 - A i)"
  proof (rule SUP_emeasure_incseq)
    show "range (\n. A 0 - A n) \ sets M"
      using A by auto
    show "incseq (\n. A 0 - A n)"
      using \<open>decseq A\<close> by (auto simp: incseq_def decseq_def)
  qed
  also have "\ = emeasure M (A 0) - emeasure M (\i. A i)"
    using A finite * by (simp, subst emeasure_Diff) auto
  finally have "emeasure M (A 0) - (INF n. emeasure M (A n)) =
                emeasure M (A 0) - emeasure M (\<Inter> (range A))" .
  then show ?thesis
    by (metis Inf_lower ennreal_minus_cancel infinity_ennreal_def le_MI local.finite
        range_eqI)
qed

lemma INF_emeasure_decseq':
  assumes A: "\i. A i \ sets M" and "decseq A"
  and finite: "\i. emeasure M (A i) \ \"
  shows "(INF n. emeasure M (A n)) = emeasure M (\i. A i)"
proof -
  from finite obtain i where i: "emeasure M (A i) < \"
    by (auto simp: less_top)
  have fin: "i \ j \ emeasure M (A j) < \" for j
    by (rule le_less_trans[OF emeasure_mono i]) (auto intro!: decseqD[OF \<open>decseq A\<close>] A)

  have "(INF n. emeasure M (A n)) = (INF n. emeasure M (A (n + i)))"
  proof (rule INF_eq)
    show "\j\UNIV. emeasure M (A (j + i)) \ emeasure M (A i')" for i'
      by (meson A \<open>decseq A\<close> decseq_def emeasure_mono iso_tuple_UNIV_I nat_le_iff_add)
  qed auto
  also have "\ = emeasure M (INF n. (A (n + i)))"
    using A \<open>decseq A\<close> fin by (intro INF_emeasure_decseq) (auto simp: decseq_def less_top)
  also have "(INF n. (A (n + i))) = (INF n. A n)"
    by (meson INF_eq UNIV_I assms(2) decseqD le_add1)
  finally show ?thesis .
qed

lemma emeasure_INT_decseq_subset:
  fixes F :: "nat \ 'a set"
  assumes I: "I \ {}" and F: "\i j. i \ I \ j \ I \ i \ j \ F j \ F i"
  assumes F_sets[measurable]: "\i. i \ I \ F i \ sets M"
    and fin: "\i. i \ I \ emeasure M (F i) \ \"
  shows "emeasure M (\i\I. F i) = (INF i\I. emeasure M (F i))"
proof cases
  assume "finite I"
  have "(\i\I. F i) = F (Max I)"
    using I \<open>finite I\<close> by (intro antisym INF_lower INF_greatest F) auto
  moreover have "(INF i\I. emeasure M (F i)) = emeasure M (F (Max I))"
    using I \<open>finite I\<close> by (intro antisym INF_lower INF_greatest F emeasure_mono) auto
  ultimately show ?thesis
    by simp
next
  assume "infinite I"
  define L where "L n = (LEAST i. i \ I \ i \ n)" for n
  have L: "L n \ I \ n \ L n" for n
    unfolding L_def
  proof (rule LeastI_ex)
    show "\x. x \ I \ n \ x"
      using \<open>infinite I\<close> finite_subset[of I "{..< n}"]
      by (rule_tac ccontr) (auto simp: not_le)
  qed
  have L_eq[simp]: "i \ I \ L i = i" for i
    unfolding L_def by (intro Least_equality) auto
  have L_mono: "i \ j \ L i \ L j" for i j
    using L[of j] unfolding L_def by (intro Least_le) (auto simp: L_def)

  have "emeasure M (\i. F (L i)) = (INF i. emeasure M (F (L i)))"
  proof (intro INF_emeasure_decseq[symmetric])
    show "decseq (\i. F (L i))"
      using L by (intro antimonoI F L_mono) auto
  qed (use L fin in auto)
  also have "\ = (INF i\I. emeasure M (F i))"
  proof (intro antisym INF_greatest)
    show "i \ I \ (INF i. emeasure M (F (L i))) \ emeasure M (F i)" for i
      by (intro INF_lower2[of i]) auto
  qed (use L in \<open>auto intro: INF_lower\<close>)
  also have "(\i. F (L i)) = (\i\I. F i)"
  proof (intro antisym INF_greatest)
    show "i \ I \ (\i. F (L i)) \ F i" for i
      by (metis Inf_lower L_eq rangeI)
  qed (use L in auto)
  finally show ?thesis .
qed

lemma Lim_emeasure_decseq:
  assumes A: "range A \ sets M" "decseq A" and fin: "\i. emeasure M (A i) \ \"
  shows "(\i. emeasure M (A i)) \ emeasure M (\i. A i)"
  using LIMSEQ_INF[OF decseq_emeasure, OF A]
  using INF_emeasure_decseq[OF A fin] by simp

lemma emeasure_lfp'[consumes 1, case_names cont measurable]:
  assumes "P M"
  assumes cont: "sup_continuous F"
  assumes *: "\M A. P M \ (\N. P N \ Measurable.pred N A) \ Measurable.pred M (F A)"
  shows "emeasure M {x\space M. lfp F x} = (SUP i. emeasure M {x\space M. (F ^^ i) (\x. False) x})"
proof -
  have "emeasure M {x\space M. lfp F x} = emeasure M (\i. {x\space M. (F ^^ i) (\x. False) x})"
    using sup_continuous_lfp[OF cont] by (auto simp: bot_fun_def intro!: arg_cong2[where f=emeasure])
  moreover { fix i from \<open>P M\<close> have "{x\<in>space M. (F ^^ i) (\<lambda>x. False) x} \<in> sets M"
    by (induct i arbitrary: M) (auto simp: pred_def[symmetric] intro: *) }
  moreover have "incseq (\i. {x\space M. (F ^^ i) (\x. False) x})"
  proof (rule incseq_SucI)
    fix i
    have "(F ^^ i) (\x. False) \ (F ^^ (Suc i)) (\x. False)"
    proof (induct i)
      case 0 show ?case by (simp add: le_fun_def)
    next
      case Suc thus ?case using monoD[OF sup_continuous_mono[OF cont] Suc] by auto
    qed
    then show "{x \ space M. (F ^^ i) (\x. False) x} \ {x \ space M. (F ^^ Suc i) (\x. False) x}"
      by auto
  qed
  ultimately show ?thesis
    by (subst SUP_emeasure_incseq) auto
qed

lemma emeasure_lfp:
  assumes [simp]: "\s. sets (M s) = sets N"
  assumes cont: "sup_continuous F" "sup_continuous f"
  assumes meas: "\P. Measurable.pred N P \ Measurable.pred N (F P)"
  assumes iter: "\P s. Measurable.pred N P \ P \ lfp F \ emeasure (M s) {x\space N. F P x} = f (\s. emeasure (M s) {x\space N. P x}) s"
  shows "emeasure (M s) {x\space N. lfp F x} = lfp f s"
proof (subst lfp_transfer_bounded[where \<alpha>="\<lambda>F s. emeasure (M s) {x\<in>space N. F x}" and f=F , symmetric])
  fix C assume "incseq C" "\i. Measurable.pred N (C i)"
  then show "(\s. emeasure (M s) {x \ space N. (SUP i. C i) x}) = (SUP i. (\s. emeasure (M s) {x \ space N. C i x}))"
    unfolding SUP_apply
    by (subst SUP_emeasure_incseq) (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure])
qed (auto simp: iter le_fun_def SUP_apply intro!: meas cont)

lemma emeasure_subadditive_finite:
  "finite I \ A ` I \ sets M \ emeasure M (\i\I. A i) \ (\i\I. emeasure M (A i))"
  by (rule sets.subadditive[OF emeasure_positive emeasure_additive]) auto

lemma emeasure_subadditive:
  "A \ sets M \ B \ sets M \ emeasure M (A \ B) \ emeasure M A + emeasure M B"
  using emeasure_subadditive_finite[of "{True, False}" "\True \ A | False \ B" M] by simp

lemma emeasure_subadditive_countably:
  assumes "range f \ sets M"
  shows "emeasure M (\i. f i) \ (\i. emeasure M (f i))"
proof -
  have "emeasure M (\i. f i) = emeasure M (\i. disjointed f i)"
    unfolding UN_disjointed_eq ..
  also have "\ = (\i. emeasure M (disjointed f i))"
    using sets.range_disjointed_sets[OF assms] suminf_emeasure[of "disjointed f"]
    by (simp add:  disjoint_family_disjointed comp_def)
  also have "\ \ (\i. emeasure M (f i))"
    using sets.range_disjointed_sets[OF assms] assms
    by (auto intro!: suminf_le emeasure_mono disjointed_subset)
  finally show ?thesis .
qed

lemma emeasure_insert:
  assumes sets: "{x} \ sets M" "A \ sets M" and "x \ A"
  shows "emeasure M (insert x A) = emeasure M {x} + emeasure M A"
proof -
  have "{x} \ A = {}" using \x \ A\ by auto
  from plus_emeasure[OF sets this] show ?thesis by simp
qed

lemma emeasure_insert_ne:
  "A \ {} \ {x} \ sets M \ A \ sets M \ x \ A \ emeasure M (insert x A) = emeasure M {x} + emeasure M A"
  by (rule emeasure_insert)

lemma emeasure_eq_sum_singleton:
  assumes "finite S" "\x. x \ S \ {x} \ sets M"
  shows "emeasure M S = (\x\S. emeasure M {x})"
  using sum_emeasure[of "\x. {x}" S M] assms
  by (auto simp: disjoint_family_on_def subset_eq)

lemma sum_emeasure_cover:
  assumes "finite S" and "A \ sets M" and br_in_M: "B ` S \ sets M"
  assumes A: "A \ (\i\S. B i)"
  assumes disj: "disjoint_family_on B S"
  shows "emeasure M A = (\i\S. emeasure M (A \ (B i)))"
proof -
  have "(\i\S. emeasure M (A \ (B i))) = emeasure M (\i\S. A \ (B i))"
  proof (rule sum_emeasure)
    show "disjoint_family_on (\i. A \ B i) S"
      using \<open>disjoint_family_on B S\<close>
      unfolding disjoint_family_on_def by auto
  qed (use assms in auto)
  also have "(\i\S. A \ (B i)) = A"
    using A by auto
  finally show ?thesis by simp
qed

lemma emeasure_eq_0:
  "N \ sets M \ emeasure M N = 0 \ K \ N \ emeasure M K = 0"
  by (metis emeasure_mono order_eq_iff zero_le)

lemma emeasure_UN_eq_0:
  assumes "\i::nat. emeasure M (N i) = 0" and "range N \ sets M"
  shows "emeasure M (\i. N i) = 0"
proof -
  have "emeasure M (\i. N i) \ 0"
    using emeasure_subadditive_countably[OF assms(2)] assms(1) by simp
  then show ?thesis
    by (auto intro: antisym zero_le)
qed

lemma measure_eqI_finite:
  assumes [simp]: "sets M = Pow A" "sets N = Pow A" and "finite A"
  assumes eq: "\a. a \ A \ emeasure M {a} = emeasure N {a}"
  shows "M = N"
proof (rule measure_eqI)
  fix X assume "X \ sets M"
  then have X: "X \ A" by auto
  then have "emeasure M X = (\a\X. emeasure M {a})"
    using \<open>finite A\<close> by (subst emeasure_eq_sum_singleton) (auto dest: finite_subset)
  also have "\ = (\a\X. emeasure N {a})"
    using X eq by (auto intro!: sum.cong)
  also have "\ = emeasure N X"
    using X \<open>finite A\<close> by (subst emeasure_eq_sum_singleton) (auto dest: finite_subset)
  finally show "emeasure M X = emeasure N X" .
qed simp

lemma measure_eqI_generator_eq:
  fixes M N :: "'a measure" and E :: "'a set set" and A :: "nat \ 'a set"
  assumes "Int_stable E" "E \ Pow \"
  and eq: "\X. X \ E \ emeasure M X = emeasure N X"
  and M: "sets M = sigma_sets \ E"
  and N: "sets N = sigma_sets \ E"
  and A: "range A \ E" "(\i. A i) = \" "\i. emeasure M (A i) \ \"
  shows "M = N"
proof -
  let ?\<mu>  = "emeasure M" and ?\<nu> = "emeasure N"
  interpret S: sigma_algebra \<Omega> "sigma_sets \<Omega> E" by (rule sigma_algebra_sigma_sets) fact
  have "space M = \"
    using sets.top[of M] sets.space_closed[of M] S.top S.space_closed \<open>sets M = sigma_sets \<Omega> E\<close>
    by blast

  have *: "emeasure M (F \ D) = emeasure N (F \ D)"
    if "F \ E" and "?\ F \ \" and D: "D \ sets M" for F D
  proof -
    have [intro]: "F \ sigma_sets \ E"
      using that by auto
    have "?\ F \ \" using \?\ F \ \\ \F \ E\ eq by simp
    from \<open>Int_stable E\<close> \<open>E \<subseteq> Pow \<Omega>\<close> D show ?thesis
      unfolding M
    proof (induct rule: sigma_sets_induct_disjoint)
      case (basic A)
      then have "F \ A \ E" using \Int_stable E\ \F \ E\ by (auto simp: Int_stable_def)
      then show ?case using eq by auto
    next
      case empty then show ?case by simp
    next
      case (compl A)
      then have **: "F \ (\ - A) = F - (F \ A)"
        and [intro]: "F \ A \ sigma_sets \ E"
        using \<open>F \<in> E\<close> S.sets_into_space by (auto simp: M)
      have "?\ (F \ A) \ ?\ F" by (auto intro!: emeasure_mono simp: M N)
      then have "?\ (F \ A) \ \" using \?\ F \ \\ by (auto simp: top_unique)
      have "?\ (F \ A) \ ?\ F" by (auto intro!: emeasure_mono simp: M N)
      then have "?\ (F \ A) \ \" using \?\ F \ \\ by (auto simp: top_unique)
      then have "?\ (F \ (\ - A)) = ?\ F - ?\ (F \ A)" unfolding **
        using \<open>F \<inter> A \<in> sigma_sets \<Omega> E\<close> by (auto intro!: emeasure_Diff simp: M N)
      also have "\ = ?\ F - ?\ (F \ A)" using eq \F \ E\ compl by simp
      also have "\ = ?\ (F \ (\ - A))" unfolding **
        using \<open>F \<inter> A \<in> sigma_sets \<Omega> E\<close> \<open>?\<nu> (F \<inter> A) \<noteq> \<infinity>\<close>
        by (auto intro!: emeasure_Diff[symmetric] simp: M N)
      finally show ?case
        using \<open>space M = \<Omega>\<close> by auto
    next
      case (union A)
      then have "?\ (\x. F \ A x) = ?\ (\x. F \ A x)"
        by (subst (1 2) suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def subset_eq M N)
      with A show ?case
        by auto
    qed
  qed
  show "M = N"
  proof (rule measure_eqI)
    show "sets M = sets N"
      using M N by simp
    have [simp, intro]: "\i. A i \ sets M"
      using A(1) by (auto simp: subset_eq M)
    fix F assume "F \ sets M"
    let ?D = "disjointed (\i. F \ A i)"
    from \<open>space M = \<Omega>\<close> have F_eq: "F = (\<Union>i. ?D i)"
      using \<open>F \<in> sets M\<close>[THEN sets.sets_into_space] A(2)[symmetric] by (auto simp: UN_disjointed_eq)
    have DinM[simp]: "\i. ?D i \ sets M"
      using sets.range_disjointed_sets[of "\i. F \ A i" M] \F \ sets M\
      by (auto simp: subset_eq)
    have "disjoint_family ?D"
      by (auto simp: disjoint_family_disjointed)
    moreover
    have "(\i. emeasure M (?D i)) = (\i. emeasure N (?D i))"
    proof (intro arg_cong[where f=suminf] ext)
      fix i
      have "A i \ ?D i = ?D i"
        by (auto simp: disjointed_def)
      with A show "emeasure M (?D i) = emeasure N (?D i)"
        by (metis "*" DinM range_subsetD)
    qed
    ultimately show "emeasure M F = emeasure N F"
      by (metis DinM F_eq \<open>sets M = sets N\<close> image_subset_iff suminf_emeasure)
  qed
qed

lemma space_empty: "space M = {} \ M = count_space {}"
  by (rule measure_eqI) (simp_all add: space_empty_iff)

lemma measure_eqI_generator_eq_countable:
  fixes M N :: "'a measure" and E :: "'a set set" and A :: "'a set set"
  assumes E: "Int_stable E" "E \ Pow \" "\X. X \ E \ emeasure M X = emeasure N X"
    and sets: "sets M = sigma_sets \ E" "sets N = sigma_sets \ E"
  and A: "A \ E" "(\A) = \" "countable A" "\a. a \ A \ emeasure M a \ \"
  shows "M = N"
proof cases
  assume "\ = {}"
  have *: "sigma_sets \ E = sets (sigma \ E)"
    using E(2) by simp
  obtain "space M = \" "space N = \"
    by (simp add: "*" sets sets_eq_imp_space_eq space_measure_of_conv)
  then show "M = N"
    unfolding \<open>\<Omega> = {}\<close> by (auto dest: space_empty)
next
  assume "\ \ {}" with \\A = \\ have "A \ {}" by auto
  from this \<open>countable A\<close> have rng: "range (from_nat_into A) = A"
    by (rule range_from_nat_into)
  show "M = N"
  proof (rule measure_eqI_generator_eq[OF E sets])
    show "range (from_nat_into A) \ E"
      unfolding rng using \<open>A \<subseteq> E\<close> .
    show "(\i. from_nat_into A i) = \"
      unfolding rng using \<open>\<Union>A = \<Omega>\<close> .
    show "emeasure M (from_nat_into A i) \ \" for i
      using rng by (intro A) auto
  qed
qed

lemma measure_of_of_measure: "measure_of (space M) (sets M) (emeasure M) = M"
proof (intro measure_eqI emeasure_measure_of_sigma)
  show "sigma_algebra (space M) (sets M)" ..
  show "positive (sets M) (emeasure M)"
    by (simp add: positive_def)
  show "countably_additive (sets M) (emeasure M)"
    by (simp add: emeasure_countably_additive)
qed simp_all

subsection \<open>\<open>\<mu>\<close>-null sets\<close>

definition\<^marker>\<open>tag important\<close> null_sets :: "'a measure \<Rightarrow> 'a set set" where
  "null_sets M = {N\sets M. emeasure M N = 0}"

lemma null_setsD1[dest]: "A \ null_sets M \ emeasure M A = 0"
  by (simp add: null_sets_def)

lemma null_setsD2[dest]: "A \ null_sets M \ A \ sets M"
  unfolding null_sets_def by simp

lemma null_setsI[intro]: "emeasure M A = 0 \ A \ sets M \ A \ null_sets M"
  unfolding null_sets_def by simp

interpretation null_sets: ring_of_sets "space M" "null_sets M" for M
proof (rule ring_of_setsI)
  show "null_sets M \ Pow (space M)"
    using sets.sets_into_space by auto
  show "{} \ null_sets M"
    by auto
  fix A B assume null_sets: "A \ null_sets M" "B \ null_sets M"
  then have sets: "A \ sets M" "B \ sets M"
    by auto
  then have *: "emeasure M (A \ B) \ emeasure M A + emeasure M B"
    "emeasure M (A - B) \ emeasure M A"
    by (auto intro!: emeasure_subadditive emeasure_mono)
  then have "emeasure M B = 0" "emeasure M A = 0"
    using null_sets by auto
  with sets * show "A - B \ null_sets M" "A \ B \ null_sets M"
    by (auto intro!: antisym zero_le)
qed

lemma UN_from_nat_into:
  assumes I: "countable I" "I \ {}"
  shows "(\i\I. N i) = (\i. N (from_nat_into I i))"
  using assms  by (simp add: UN_extend_simps)

lemma null_sets_UN':
  assumes "countable I"
  assumes "\i. i \ I \ N i \ null_sets M"
  shows "(\i\I. N i) \ null_sets M"
proof cases
  assume "I = {}" then show ?thesis by simp
next
  assume "I \ {}"
  show ?thesis
  proof (intro conjI CollectI null_setsI)
    show "(\i\I. N i) \ sets M"
      using assms by (intro sets.countable_UN') auto
    have "emeasure M (\i\I. N i) \ (\n. emeasure M (N (from_nat_into I n)))"
      unfolding UN_from_nat_into[OF \<open>countable I\<close> \<open>I \<noteq> {}\<close>]
      using assms \<open>I \<noteq> {}\<close> by (intro emeasure_subadditive_countably) (auto intro: from_nat_into)
    also have "(\n. emeasure M (N (from_nat_into I n))) = (\_. 0)"
      using assms \<open>I \<noteq> {}\<close> by (auto intro: from_nat_into)
    finally show "emeasure M (\i\I. N i) = 0"
      by (intro antisym zero_le) simp
  qed
qed

lemma null_sets_UN[intro]:
  "(\i::'i::countable. N i \ null_sets M) \ (\i. N i) \ null_sets M"
  by (rule null_sets_UN') auto

lemma null_set_Int1:
  assumes "B \ null_sets M" "A \ sets M" shows "A \ B \ null_sets M"
proof (intro CollectI conjI null_setsI)
  show "emeasure M (A \ B) = 0" using assms
    by (intro emeasure_eq_0[of B _ "A \ B"]) auto
qed (use assms in auto)

lemma null_set_Int2:
  assumes "B \ null_sets M" "A \ sets M" shows "B \ A \ null_sets M"
  using assms by (subst Int_commute) (rule null_set_Int1)

lemma emeasure_Diff_null_set:
  assumes "B \ null_sets M" "A \ sets M"
  shows "emeasure M (A - B) = emeasure M A"
proof -
  have *: "A - B = (A - (A \ B))" by auto
  have "A \ B \ null_sets M" using assms by (rule null_set_Int1)
  then show ?thesis
    unfolding * using assms
    by (subst emeasure_Diff) auto
qed

lemma null_set_Diff:
  assumes "B \ null_sets M" "A \ sets M" shows "B - A \ null_sets M"
proof (intro CollectI conjI null_setsI)
  show "emeasure M (B - A) = 0"
    using assms by (intro emeasure_eq_0[of B _ "B - A"]) auto
qed (use assms in auto)

lemma emeasure_Un_null_set:
  assumes "A \ sets M" "B \ null_sets M"
  shows "emeasure M (A \ B) = emeasure M A"
proof -
  have *: "A \ B = A \ (B - A)" by auto
  have "B - A \ null_sets M" using assms
    using null_set_Diff by blast
  then show ?thesis
    unfolding * using assms
    by (subst plus_emeasure[symmetric]) auto
qed

lemma emeasure_Un':
  assumes "A \ sets M" "B \ sets M" "A \ B \ null_sets M"
  shows   "emeasure M (A \ B) = emeasure M A + emeasure M B"
proof -
  have "A \ B = A \ (B - A \ B)" by blast
  also have "emeasure M \ = emeasure M A + emeasure M (B - A \ B)"
    using assms by (subst plus_emeasure) auto
  also have "emeasure M (B - A \ B) = emeasure M B"
    using assms by (intro emeasure_Diff_null_set) auto
  finally show ?thesis .
qed

subsection \<open>The almost everywhere filter (i.e.\ quantifier)\<close>

definition\<^marker>\<open>tag important\<close> ae_filter :: "'a measure \<Rightarrow> 'a filter" where
  "ae_filter M = (INF N\null_sets M. principal (space M - N))"

abbreviation almost_everywhere :: "'a measure \ ('a \ bool) \ bool" where
  "almost_everywhere M P \ eventually P (ae_filter M)"

syntax
  "_almost_everywhere" :: "pttrn \ 'a \ bool \ bool"
    (\<open>(\<open>open_block notation=\<open>binder AE\<close>\<close>AE _ in _. _)\<close> [0,0,10] 10)
syntax_consts
  "_almost_everywhere" \<rightleftharpoons> almost_everywhere
translations
  "AE x in M. P" \<rightleftharpoons> "CONST almost_everywhere M (\<lambda>x. P)"

abbreviation
  "set_almost_everywhere A M P \ AE x in M. x \ A \ P x"

syntax
  "_set_almost_everywhere" :: "pttrn \ 'a set \ 'a \ bool \ bool"
    (\<open>(\<open>open_block notation=\<open>binder AE\<close>\<close>AE _\<in>_ in _./ _)\<close> [0,0,0,10] 10)
syntax_consts
  "_set_almost_everywhere" \<rightleftharpoons> set_almost_everywhere
translations
  "AE x\A in M. P" \ "CONST set_almost_everywhere A M (\x. P)"

lemma eventually_ae_filter: "eventually P (ae_filter M) \ (\N\null_sets M. {x \ space M. \ P x} \ N)"
  unfolding ae_filter_def by (subst eventually_INF_base) (auto simp: eventually_principal subset_eq)

lemma AE_I':
  "N \ null_sets M \ {x\space M. \ P x} \ N \ (AE x in M. P x)"
  unfolding eventually_ae_filter by auto

lemma AE_iff_null:
  assumes "{x\space M. \ P x} \ sets M" (is "?P \ sets M")
  shows "(AE x in M. P x) \ {x\space M. \ P x} \ null_sets M"
proof
  assume "AE x in M. P x" then obtain N where N: "N \ sets M" "?P \ N" "emeasure M N = 0"
    unfolding eventually_ae_filter by auto
  then have "emeasure M ?P \ emeasure M N"
    using emeasure_mono by blast
  then have "emeasure M ?P = 0"
    unfolding \<open>emeasure M N = 0\<close> by auto
  then show "?P \ null_sets M" using assms by auto
next
  assume "?P \ null_sets M" with assms show "AE x in M. P x" by (auto intro: AE_I')
qed

lemma AE_iff_null_sets:
  "N \ sets M \ N \ null_sets M \ (AE x in M. x \ N)"
  using Int_absorb1[OF sets.sets_into_space, of N M]
  by (subst AE_iff_null) (auto simp: Int_def[symmetric])

lemma ae_filter_eq_bot_iff: "ae_filter M = bot \ emeasure M (space M) = 0"
proof -
  have "ae_filter M = bot \ (AE x in M. False)"
    using trivial_limit_def by blast
  also have "\ \ space M \ null_sets M"
    by (simp add: AE_iff_null_sets eventually_ae_filter)
  also have "\ \ emeasure M (space M) = 0"
    by auto
  finally show ?thesis .
qed

lemma AE_not_in:
  "N \ null_sets M \ AE x in M. x \ N"
  by (metis AE_iff_null_sets null_setsD2)

lemma AE_iff_measurable:
  "N \ sets M \ {x\space M. \ P x} = N \ (AE x in M. P x) \ emeasure M N = 0"
  using AE_iff_null[of _ P] by auto

lemma AE_E[consumes 1]:
  assumes "AE x in M. P x"
  obtains N where "{x \ space M. \ P x} \ N" "emeasure M N = 0" "N \ sets M"
  using assms unfolding eventually_ae_filter by auto

lemma AE_E2:
  assumes "AE x in M. P x"
  shows "emeasure M {x\space M. \ P x} = 0"
  by (metis (mono_tags, lifting) AE_iff_null assms emeasure_notin_sets null_setsD1)

lemma AE_E3:
  assumes "AE x in M. P x"
  obtains N where "\x. x \ space M - N \ P x" "N \ null_sets M"
using assms unfolding eventually_ae_filter by auto

lemma AE_I:
  assumes "{x \ space M. \ P x} \ N" "emeasure M N = 0" "N \ sets M"
  shows "AE x in M. P x"
  using assms unfolding eventually_ae_filter by auto

lemma AE_mp[elim!]:
  assumes AE_P: "AE x in M. P x" and AE_imp: "AE x in M. P x \ Q x"
  shows "AE x in M. Q x"
  using assms by (fact eventually_rev_mp)

text \<open>The next lemma is convenient to combine with a lemma whose conclusion is of the
form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \<open>[symmetric]\<close> variant,
but using \<open>AE_symmetric[OF\<dots>]\<close> will replace it.\<close>

(* depricated replace by laws about eventually *)
lemma
  shows AE_iffI: "AE x in M. P x \ AE x in M. P x \ Q x \ AE x in M. Q x"
    and AE_disjI1: "AE x in M. P x \ AE x in M. P x \ Q x"
    and AE_disjI2: "AE x in M. Q x \ AE x in M. P x \ Q x"
    and AE_conjI: "AE x in M. P x \ AE x in M. Q x \ AE x in M. P x \ Q x"
    and AE_conj_iff[simp]: "(AE x in M. P x \ Q x) \ (AE x in M. P x) \ (AE x in M. Q x)"
  by auto

lemma AE_symmetric:
  assumes "AE x in M. P x = Q x"
  shows "AE x in M. Q x = P x"
  using assms by auto

lemma AE_impI:
  "(P \ AE x in M. Q x) \ AE x in M. P \ Q x"
  by fastforce

lemma AE_measure:
  assumes AE: "AE x in M. P x" and sets: "{x\space M. P x} \ sets M" (is "?P \ sets M")
  shows "emeasure M {x\space M. P x} = emeasure M (space M)"
proof -
  from AE_E[OF AE] obtain N
    where N: "{x \ space M. \ P x} \ N" "emeasure M N = 0" "N \ sets M"
    by auto
  with sets have "emeasure M (space M) \ emeasure M (?P \ N)"
    by (intro emeasure_mono) auto
  also have "\ \ emeasure M ?P + emeasure M N"
    using sets N by (intro emeasure_subadditive) auto
  also have "\ = emeasure M ?P" using N by simp
  finally show "emeasure M ?P = emeasure M (space M)"
    using emeasure_space[of M "?P"] by auto
qed

lemma AE_space: "AE x in M. x \ space M"
  by (auto intro: AE_I[where N="{}"])

lemma AE_I2[simp, intro]:
  "(\x. x \ space M \ P x) \ AE x in M. P x"
  using AE_space by force

lemma AE_Ball_mp:
  "\x\space M. P x \ AE x in M. P x \ Q x \ AE x in M. Q x"
  by auto

lemma AE_cong[cong]:
  "(\x. x \ space M \ P x \ Q x) \ (AE x in M. P x) \ (AE x in M. Q x)"
  by auto

lemma AE_cong_simp: "M = N \ (\x. x \ space N =simp=> P x = Q x) \ (AE x in M. P x) \ (AE x in N. Q x)"
  by (auto simp: simp_implies_def)

lemma AE_all_countable:
  "(AE x in M. \i. P i x) \ (\i::'i::countable. AE x in M. P i x)"
proof
  assume "\i. AE x in M. P i x"
  then obtain N where N: "\i. N i \ null_sets M" "\i. {x\space M. \ P i x} \ N i"
    unfolding eventually_ae_filter by metis
  have "{x\space M. \ (\i. P i x)} \ (\i. {x\space M. \ P i x})" by auto
  also have "\ \ (\i. N i)" using N by auto
  finally have "{x\space M. \ (\i. P i x)} \ (\i. N i)" .
  moreover from N have "(\i. N i) \ null_sets M"
    by (intro null_sets_UN) auto
  ultimately show "AE x in M. \i. P i x"
    unfolding eventually_ae_filter by auto
qed auto

lemma AE_ball_countable:
  assumes [intro]: "countable X"
  shows "(AE x in M. \y\X. P x y) \ (\y\X. AE x in M. P x y)"
proof
  assume "\y\X. AE x in M. P x y"
  then obtain N where N: "\y. y \ X \ N y \ null_sets M" "\y. y \ X \ {x\space M. \ P x y} \ N y"
    unfolding eventually_ae_filter by metis
  have "{x\space M. \ (\y\X. P x y)} \ (\y\X. {x\space M. \ P x y})"
    by auto
  also have "\ \ (\y\X. N y)"
    using N by auto
  finally have "{x\space M. \ (\y\X. P x y)} \ (\y\X. N y)" .
  moreover from N have "(\y\X. N y) \ null_sets M"
    by (intro null_sets_UN') auto
  ultimately show "AE x in M. \y\X. P x y"
    unfolding eventually_ae_filter by auto
qed auto

lemma AE_ball_countable':
  "(\N. N \ I \ AE x in M. P N x) \ countable I \ AE x in M. \N \ I. P N x"
  unfolding AE_ball_countable by simp

lemma AE_pairwise: "countable F \ pairwise (\A B. AE x in M. R x A B) F \ (AE x in M. pairwise (R x) F)"
  unfolding pairwise_alt by (simp add: AE_ball_countable)

lemma AE_discrete_difference:
  assumes X: "countable X"
  assumes null: "\x. x \ X \ emeasure M {x} = 0"
  assumes sets: "\x. x \ X \ {x} \ sets M"
  shows "AE x in M. x \ X"
proof -
  have "(\x\X. {x}) \ null_sets M"
    using assms by (intro null_sets_UN') auto
  from AE_not_in[OF this] show "AE x in M. x \ X"
    by auto
qed

lemmas AE_finite_all = eventually_ball_finite_distrib

lemma AE_finite_allI:
  assumes "finite S"
  shows "(\s. s \ S \ AE x in M. Q s x) \ AE x in M. \s\S. Q s x"
  by (simp add: AE_ball_countable' assms countable_finite)

lemma emeasure_mono_AE:
  assumes imp: "AE x in M. x \ A \ x \ B"
    and B: "B \ sets M"
  shows "emeasure M A \ emeasure M B"
proof cases
  assume A: "A \ sets M"
  from imp obtain N where N: "{x\space M. \ (x \ A \ x \ B)} \ N" "N \ null_sets M"
    by (auto simp: eventually_ae_filter)
  have "emeasure M A = emeasure M (A - N)"
    using N A by (subst emeasure_Diff_null_set) auto
  also have "emeasure M (A - N) \ emeasure M (B - N)"
    using N A B sets.sets_into_space by (auto intro!: emeasure_mono)
  also have "emeasure M (B - N) = emeasure M B"
    using N B by (subst emeasure_Diff_null_set) auto
  finally show ?thesis .
qed (simp add: emeasure_notin_sets)

lemma emeasure_eq_AE:
  assumes "AE x in M. x \ A \ x \ B" "A \ sets M" "B \ sets M"
  shows "emeasure M A = emeasure M B"
  using assms by (force intro!: antisym emeasure_mono_AE)

lemma emeasure_Collect_eq_AE:
  "AE x in M. P x \ Q x \ Measurable.pred M Q \ Measurable.pred M P \
   emeasure M {x\<in>space M. P x} = emeasure M {x\<in>space M. Q x}"
   by (intro emeasure_eq_AE) auto

lemma emeasure_eq_0_AE: "AE x in M. \ P x \ emeasure M {x\space M. P x} = 0"
  using AE_iff_measurable[OF _ refl, of M "\x. \ P x"]
  by (cases "{x\space M. P x} \ sets M") (simp_all add: emeasure_notin_sets)

lemma emeasure_0_AE:
  assumes "emeasure M (space M) = 0"
  shows "AE x in M. P x"
using eventually_ae_filter assms by blast

lemma emeasure_add_AE:
  assumes [measurable]: "A \ sets M" "B \ sets M" "C \ sets M"
  assumes 1: "AE x in M. x \ C \ x \ A \ x \ B"
  assumes 2: "AE x in M. \ (x \ A \ x \ B)"
  shows "emeasure M C = emeasure M A + emeasure M B"
proof -
  have "emeasure M C = emeasure M (A \ B)"
    by (rule emeasure_eq_AE) (use 1 in auto)
  also have "\ = emeasure M A + emeasure M (B - A)"
    by (subst plus_emeasure) auto
  also have "emeasure M (B - A) = emeasure M B"
    by (rule emeasure_eq_AE) (use 2 in auto)
  finally show ?thesis .
qed

subsection \<open>\<open>\<sigma>\<close>-finite Measures\<close>

locale\<^marker>\<open>tag important\<close> sigma_finite_measure =
  fixes M :: "'a measure"
  assumes sigma_finite_countable:
    "\A::'a set set. countable A \ A \ sets M \ (\A) = space M \ (\a\A. emeasure M a \ \)"

lemma (in sigma_finite_measure) sigma_finite:
  obtains A :: "nat \ 'a set"
  where "range A \ sets M" "(\i. A i) = space M" "\i. emeasure M (A i) \ \"
proof -
  obtain A :: "'a set set" where
    [simp]: "countable A" and
    A: "A \ sets M" "(\A) = space M" "\a. a \ A \ emeasure M a \ \"
    using sigma_finite_countable by metis
  show thesis
  proof cases
    assume "A = {}" with \<open>(\<Union>A) = space M\<close> show thesis
      by (intro that[of "\_. {}"]) auto
  next
    assume "A \ {}"
    show thesis
    proof
      show "range (from_nat_into A) \ sets M"
        using \<open>A \<noteq> {}\<close> A by auto
      have "(\i. from_nat_into A i) = \A"
        using range_from_nat_into[OF \<open>A \<noteq> {}\<close> \<open>countable A\<close>] by auto
      with A show "(\i. from_nat_into A i) = space M"
        by auto
    qed (intro A from_nat_into \<open>A \<noteq> {}\<close>)
  qed
qed

lemma (in sigma_finite_measure) sigma_finite_disjoint:
  obtains A :: "nat \ 'a set"
  where "range A \ sets M" "(\i. A i) = space M" "\i. emeasure M (A i) \ \" "disjoint_family A"
proof -
  obtain A :: "nat \ 'a set" where
    range: "range A \ sets M" and
    space: "(\i. A i) = space M" and
    measure: "\i. emeasure M (A i) \ \"
    using sigma_finite by blast
  show thesis
  proof (rule that[of "disjointed A"])
    show "range (disjointed A) \ sets M"
      by (rule sets.range_disjointed_sets[OF range])
    show "(\i. disjointed A i) = space M" and "disjoint_family (disjointed A)"
      using disjoint_family_disjointed UN_disjointed_eq[of A] space range
      by auto
    show "emeasure M (disjointed A i) \ \" for i
      using range disjointed_subset[of A i] measure[of i]
      by (simp add: emeasure_mono neq_top_trans)
  qed
qed

lemma (in sigma_finite_measure) sigma_finite_incseq:
  obtains A :: "nat \ 'a set"
  where "range A \ sets M" "(\i. A i) = space M" "\i. emeasure M (A i) \ \" "incseq A"
proof -
  obtain F :: "nat \ 'a set" where
    F: "range F \ sets M" "(\i. F i) = space M" "\i. emeasure M (F i) \ \"
    using sigma_finite by blast
  show thesis
  proof (rule that[of "\n. \i\n. F i"])
    show "range (\n. \i\n. F i) \ sets M"
      using F by (force simp: incseq_def)
    show "(\n. \i\n. F i) = space M"
      using F(2) by fastforce
    show "emeasure M (\i\n. F i) \ \" for n
    proof -
      have "emeasure M (\i\n. F i) \ (\i\n. emeasure M (F i))"
        using F by (auto intro!: emeasure_subadditive_finite)
      also have "\ < \"
        using F by (auto simp: sum_Pinfty less_top)
      finally show ?thesis by simp
    qed
    show "incseq (\n. \i\n. F i)"
      by (force simp: incseq_def)
  qed
qed

lemma (in sigma_finite_measure) approx_PInf_emeasure_with_finite:
  fixes C::real
  assumes W_meas: "W \ sets M"
      and W_inf: "emeasure M W = \"
  obtains Z where "Z \ sets M" "Z \ W" "emeasure M Z < \" "emeasure M Z > C"
proof -
  obtain A :: "nat \ 'a set"
    where A: "range A \ sets M" "(\i. A i) = space M" "\i. emeasure M (A i) \ \" "incseq A"
    using sigma_finite_incseq by blast
  define B where "B = (\i. W \ A i)"
--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.