Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: testtracker.vdmsl Sprache: Isabelle

Original von: 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 (insert assms, simp)
  ultimately show ?thesis using assms
    by (subst suminf_eq_SUP) (auto simp: indicator_def)
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
  thus ?thesis
    unfolding indicator_def
    by (simp add: if_distrib sum.If_cases[OF \<open>finite P\<close>])
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 add: binaryset_def f)
    qed
  moreover
  have "... \ f A + f B" by (rule tendsto_const)
  ultimately
  have "(\n. \i< Suc (Suc n). f (binaryset A B i)) \ f A + f B"
    by metis
  hence "(\n. \i< n+2. f (binaryset A B i)) \ f A + f B"
    by simp
  thus ?thesis by (rule LIMSEQ_offset [where k=2])
qed

lemma binaryset_sums:
  assumes f: "f {} = 0"
  shows  "(\n. f (binaryset A B n)) sums (f A + f B)"
    by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f] atLeast0LessThan)

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 add: 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 add: 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 add: 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 add: 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 add: 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 add: positive_def)

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

lemma increasingD:
  "increasing M f \ x \ y \ x\M \ y\M \ f x \ f y"
  by (auto simp add: 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 add: 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 add: additive_def)
  with insert show ?case using ad disjoint_family_on_mono[of S "insert s S" A]
    by (auto simp add: 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 add: 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))" using addf
    by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2))
  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 (auto simp: increasing_def intro: add_left_mono)
  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))" using insert by simp
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 add: 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 add: 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 \<union> y) = (\<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 posf x y
    by (auto simp add: 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 (insert f A, auto simp: positive_def)

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\{i. F i \ {}}. \x. x \ F i" by auto
  from bchoice[OF this] obtain f where f: "\i. F i \ {} \ f i \ F i" by auto

  have inj_f: "inj_on f {i. F i \ {}}"
  proof (rule inj_onI, simp)
    fix i j a b assume *: "f i = f j" "F i \ {}" "F j \ {}"
    then have "f i \ F i" "f j \ F j" using f by force+
    with disj * show "i = j" by (auto simp: disjoint_family_on_def)
  qed
  have "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 (rule finite_subset) fact
  qed fact
  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))"
    using f(1)[unfolded positive_def] dA
    by (auto intro!: 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: "\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 "(\n. f (\i f (\i. A i)"
  proof (unfold *[symmetric], intro cont[rule_format])
    show "range (\i. \i M" "(\i. \i M"
      using A * by auto
  qed (force intro!: incseq_SucI)
  moreover have "\n. f (\ii
    using A
    by (intro additive_sum[OF f, of _ A, symmetric])
       (auto intro: disjoint_family_on_mono[where B=UNIV])
  ultimately
  have "(\i. f (A i)) sums f (\i. A i)"
    unfolding sums_def by simp
  from sums_unique[OF this]
  show "(\i. f (A i)) = f (\i. A i)" by simp
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: "(\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[THEN spec, of A] show "(\i. f (A i)) \ 0"
    using \<open>positive M f\<close>[unfolded positive_def] by auto
next
  assume cont: "\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)
  { fix i
    have "f (A i - (\i. A i)) \ f (A i)" using A by (auto intro!: f_mono)
    then have "f (A i - (\i. A i)) \ \"
      using A by (auto simp: top_unique) }
  note f_fin = this
  have "(\i. f (A i - (\i. A i))) \ 0"
  proof (intro cont[rule_format, OF _ decseq _ f_fin])
    show "range (\i. A i - (\i. A i)) \ M" "(\i. A i - (\i. A i)) = {}"
      using A by auto
  qed
  from INF_Lim[OF decseq_f this]
  have "(INF n. f (A n - (\i. A i))) = 0" .
  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
    by (subst INF_ennreal_add_const) (auto simp: decseq_f)
  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 by (subst f(2)[THEN additiveD]) auto
    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 f(3)[rule_format, of "A i"] A by (auto simp: ennreal_add_diff_cancel subset_eq) }
  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 finite: "emeasure M B \ \"
  and [measurable]: "A \ sets M" "B \ sets M" and "B \ A"
  shows "emeasure M (A - B) = emeasure M A - emeasure M B"
proof -
  have "(A - B) \ B = A" using \B \ A\ by auto
  then have "emeasure M A = emeasure M ((A - B) \ B)" by simp
  also have "\ = emeasure M (A - B) + emeasure M B"
    by (subst plus_emeasure[symmetric]) auto
  finally show "emeasure M (A - B) = emeasure M A - emeasure M B"
    using finite by simp
qed

lemma emeasure_compl:
  "s \ sets M \ emeasure M s \ \ \ emeasure M (space M - s) = emeasure M (space M) - emeasure M s"
  by (rule emeasure_Diff) (auto dest: 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 (auto simp add: sets.countably_additive_iff_continuous_from_below emeasure_positive
    emeasure_additive)

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 add: 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 show ?thesis
    by (rule ennreal_minus_cancel[rotated 3])
       (insert finite A, auto intro: INF_lower emeasure_mono)
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 (intro bexI[of _ i'] emeasure_mono decseqD[OF \decseq A\] A) auto
  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 (insert L fin, 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 (insert L, auto intro: INF_lower)
  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 (intro INF_lower2[of i]) auto
  qed (insert L, 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 add: 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 add: 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 g=f and f=F and P="Measurable.pred N", 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[abs_def]
    by (subst SUP_emeasure_incseq) (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure])
qed (auto simp add: iter le_fun_def SUP_apply[abs_def] 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 (insert assms, 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

  { fix F D assume "F \ E" and "?\ F \ \"
    then have [intro]: "F \ sigma_sets \ E" by auto
    have "?\ F \ \" using \?\ F \ \\ \F \ E\ eq by simp
    assume "D \ sets M"
    with \<open>Int_stable E\<close> \<open>E \<subseteq> Pow \<Omega>\<close> have "emeasure M (F \<inter> D) = emeasure N (F \<inter> D)"
      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 }
  note * = this
  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 [simp, intro]: "\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)
      then show "emeasure M (?D i) = emeasure N (?D i)"
        using *[of "A i" "?D i", OF _ A(3)] A(1) by auto
    qed
    ultimately show "emeasure M F = emeasure N F"
      by (simp add: image_subset_iff \<open>sets M = sets N\<close>[symmetric] F_eq[symmetric] 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
  have "space M = \" "space N = \"
    using sets E(2) unfolding * by (auto dest: sets_eq_imp_space_eq simp del: sets_measure_of)
  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))"
proof -
  have "(\i\I. N i) = \(N ` range (from_nat_into I))"
    using I by simp
  also have "\ = (\i. (N \ from_nat_into I) i)"
    by simp
  finally show ?thesis by simp
qed

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 (insert assms, 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 (insert assms, 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(2,1) by (rule null_set_Diff)
  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" ("AE _ in _. _" [0,0,10] 10)

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"
  ("AE _\_ in _./ _" [0,0,0,10] 10)

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
  have "emeasure M ?P \ emeasure M N"
    using assms N(1,2) by (auto intro: emeasure_mono)
  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_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" "{x\space M. P x} \ sets M"
  shows "emeasure M {x\space M. \ P x} = 0" (is "emeasure M ?P = 0")
proof -
  have "{x\space M. \ P x} = space M - {x\space M. P x}" by auto
  with AE_iff_null[of M P] assms show ?thesis by auto
qed

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"
proof -
  from AE_P obtain A where P: "{x\space M. \ P x} \ A"
    and A: "A \ sets M" "emeasure M A = 0"
    by (auto elim!: AE_E)

  from AE_imp obtain B where imp: "{x\space M. P x \ \ Q x} \ B"
    and B: "B \ sets M" "emeasure M B = 0"
    by (auto elim!: AE_E)

  show ?thesis
  proof (intro AE_I)
    have "emeasure M (A \ B) \ 0"
      using emeasure_subadditive[of A M B] A B by auto
    then show "A \ B \ sets M" "emeasure M (A \ B) = 0"
      using A B by auto
    show "{x\space M. \ Q x} \ A \ B"
      using P imp by auto
  qed
qed

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...]\<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] guess N . note N = this
  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 (rule AE_I[where N="{}"]) auto

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"
  from this[unfolded eventually_ae_filter Bex_def, THEN choice]
  obtain N where N: "\i. N i \ null_sets M" "\i. {x\space M. \ P i x} \ N i" by auto
  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"
  from this[unfolded eventually_ae_filter Bex_def, THEN bchoice]
  obtain N where N: "\y. y \ X \ N y \ null_sets M" "\y. y \ X \ {x\space M. \ P x y} \ N y"
    by auto
  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

lemma AE_finite_all:
  assumes f: "finite S" shows "(AE x in M. \i\S. P i x) \ (\i\S. AE x in M. P i x)"
  using f by induct auto

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"
  using AE_finite_all[OF \<open>finite S\<close>] by auto

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 iff: "AE x in M. x \ A \ x \ B"
  assumes A: "A \ sets M" and B: "B \ sets M"
  shows "emeasure M A = emeasure M B"
  using assms by (safe intro!: antisym emeasure_mono_AE) auto

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) (insert 1, 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) (insert 2, 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
    proof -
      have "emeasure M (disjointed A i) \ emeasure M (A i)"
        using range disjointed_subset[of A i] by (auto intro!: emeasure_mono)
      then show ?thesis using measure[of i] by (auto simp: top_unique)
    qed
  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"])
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.117 Sekunden (vorverarbeitet) ¤

Bilder Diashow
Bilder sprechenden Kalenders
Eigene Datei ansehen

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.