src/HOL/Probability/Measure.thy

Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.

header {*Measures*}

theory Measure
  imports Caratheodory
begin

text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}

section {* Equations for the measure function @{text \<mu>} *}

lemma (in measure_space) measure_countably_additive:
  assumes "range A \<subseteq> sets M" "disjoint_family A"
  shows "psuminf (\<lambda>i. \<mu> (A i)) = \<mu> (\<Union>i. A i)"
proof -
  have "(\<Union> i. A i) \<in> sets M" using assms(1) by (rule countable_UN)
  with ca assms show ?thesis by (simp add: countably_additive_def)
qed

lemma (in measure_space) measure_space_cong:
  assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = \<mu> A"
  shows "measure_space M \<nu>"
proof
  show "\<nu> {} = 0" using assms by auto
  show "countably_additive M \<nu>" unfolding countably_additive_def
  proof safe
    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A"
    then have "\<And>i. A i \<in> sets M" "(UNION UNIV A) \<in> sets M" by auto
    from this[THEN assms] measure_countably_additive[OF A]
    show "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (UNION UNIV A)" by simp
  qed
qed

lemma (in measure_space) additive: "additive M \<mu>"
proof (rule algebra.countably_additive_additive [OF _ _ ca])
  show "algebra M" by default
  show "positive \<mu>" by (simp add: positive_def)
qed

lemma (in measure_space) measure_additive:
     "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {}
      \<Longrightarrow> \<mu> a + \<mu> b = \<mu> (a \<union> b)"
  by (metis additiveD additive)

lemma (in measure_space) measure_mono:
  assumes "a \<subseteq> b" "a \<in> sets M" "b \<in> sets M"
  shows "\<mu> a \<le> \<mu> b"
proof -
  have "b = a \<union> (b - a)" using assms by auto
  moreover have "{} = a \<inter> (b - a)" by auto
  ultimately have "\<mu> b = \<mu> a + \<mu> (b - a)"
    using measure_additive[of a "b - a"] local.Diff[of b a] assms by auto
  moreover have "\<mu> (b - a) \<ge> 0" using assms by auto
  ultimately show "\<mu> a \<le> \<mu> b" by auto
qed

lemma (in measure_space) measure_compl:
  assumes s: "s \<in> sets M" and fin: "\<mu> s \<noteq> \<omega>"
  shows "\<mu> (space M - s) = \<mu> (space M) - \<mu> s"
proof -
  have s_less_space: "\<mu> s \<le> \<mu> (space M)"
    using s by (auto intro!: measure_mono sets_into_space)

  have "\<mu> (space M) = \<mu> (s \<union> (space M - s))" using s
    by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
  also have "... = \<mu> s + \<mu> (space M - s)"
    by (rule additiveD [OF additive]) (auto simp add: s)
  finally have "\<mu> (space M) = \<mu> s + \<mu> (space M - s)" .
  thus ?thesis
    unfolding minus_pinfreal_eq2[OF s_less_space fin]
    by (simp add: ac_simps)
qed

lemma (in measure_space) measure_Diff:
  assumes finite: "\<mu> B \<noteq> \<omega>"
  and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A"
  shows "\<mu> (A - B) = \<mu> A - \<mu> B"
proof -
  have *: "(A - B) \<union> B = A" using `B \<subseteq> A` by auto

  have "\<mu> ((A - B) \<union> B) = \<mu> (A - B) + \<mu> B"
    using measurable by (rule_tac measure_additive[symmetric]) auto
  thus ?thesis unfolding * using `\<mu> B \<noteq> \<omega>`
    by (simp add: pinfreal_cancel_plus_minus)
qed

lemma (in measure_space) measure_countable_increasing:
  assumes A: "range A \<subseteq> sets M"
      and A0: "A 0 = {}"
      and ASuc: "\<And>n.  A n \<subseteq> A (Suc n)"
  shows "(SUP n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
proof -
  {
    fix n
    have "\<mu> (A n) =
          setsum (\<mu> \<circ> (\<lambda>i. A (Suc i) - A i)) {..<n}"
      proof (induct n)
        case 0 thus ?case by (auto simp add: A0)
      next
        case (Suc m)
        have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
          by (metis ASuc Un_Diff_cancel Un_absorb1)
        hence "\<mu> (A (Suc m)) =
               \<mu> (A m) + \<mu> (A (Suc m) - A m)"
          by (subst measure_additive)
             (auto simp add: measure_additive range_subsetD [OF A])
        with Suc show ?case
          by simp
      qed }
  note Meq = this
  have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)"
    proof (rule UN_finite2_eq [where k=1], simp)
      fix i
      show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
        proof (induct i)
          case 0 thus ?case by (simp add: A0)
        next
          case (Suc i)
          thus ?case
            by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
        qed
    qed
  have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
    by (metis A Diff range_subsetD)
  have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
    by (blast intro: range_subsetD [OF A])
  have "psuminf ( (\<lambda>i. \<mu> (A (Suc i) - A i))) = \<mu> (\<Union>i. A (Suc i) - A i)"
    by (rule measure_countably_additive)
       (auto simp add: disjoint_family_Suc ASuc A1 A2)
  also have "... =  \<mu> (\<Union>i. A i)"
    by (simp add: Aeq)
  finally have "psuminf (\<lambda>i. \<mu> (A (Suc i) - A i)) = \<mu> (\<Union>i. A i)" .
  thus ?thesis
    by (auto simp add: Meq psuminf_def)
qed

lemma (in measure_space) continuity_from_below:
  assumes A: "range A \<subseteq> sets M"
      and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
  shows "(SUP n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
proof -
  have *: "(SUP n. \<mu> (nat_case {} A (Suc n))) = (SUP n. \<mu> (nat_case {} A n))"
    apply (rule Sup_mono_offset_Suc)
    apply (rule measure_mono)
    using assms by (auto split: nat.split)

  have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)"
    by (auto simp add: split: nat.splits)
  have meq: "\<And>n. \<mu> (A n) = (\<mu> \<circ> nat_case {} A) (Suc n)"
    by simp
  have "(SUP n. \<mu> (nat_case {} A n)) = \<mu> (\<Union>i. nat_case {} A i)"
    by (rule measure_countable_increasing)
       (auto simp add: range_subsetD [OF A] subsetD [OF ASuc] split: nat.splits)
  also have "\<mu> (\<Union>i. nat_case {} A i) = \<mu> (\<Union>i. A i)"
    by (simp add: ueq)
  finally have "(SUP n. \<mu> (nat_case {} A n)) = \<mu> (\<Union>i. A i)" .
  thus ?thesis unfolding meq * comp_def .
qed

lemma (in measure_space) measure_up:
  assumes "P \<in> sets M" "\<And>i. B i \<in> sets M" "B \<up> P"
  shows "(\<lambda>i. \<mu> (B i)) \<up> \<mu> P"
  using assms unfolding isoton_def
  by (auto intro!: measure_mono continuity_from_below)


lemma (in measure_space) continuity_from_above:
  assumes A: "range A \<subseteq> sets M"
  and mono_Suc: "\<And>n.  A (Suc n) \<subseteq> A n"
  and finite: "\<And>i. \<mu> (A i) \<noteq> \<omega>"
  shows "(INF n. \<mu> (A n)) = \<mu> (\<Inter>i. A i)"
proof -
  { fix n have "A n \<subseteq> A 0" using mono_Suc by (induct n) auto }
  note mono = this

  have le_MI: "\<mu> (\<Inter>i. A i) \<le> \<mu> (A 0)"
    using A by (auto intro!: measure_mono)
  hence *: "\<mu> (\<Inter>i. A i) \<noteq> \<omega>" using finite[of 0] by auto

  have le_IM: "(INF n. \<mu> (A n)) \<le> \<mu> (A 0)"
    by (rule INF_leI) simp

  have "\<mu> (A 0) - (INF n. \<mu> (A n)) = (SUP n. \<mu> (A 0 - A n))"
    unfolding pinfreal_SUP_minus[symmetric]
    using mono A finite by (subst measure_Diff) auto
  also have "\<dots> = \<mu> (\<Union>i. A 0 - A i)"
  proof (rule continuity_from_below)
    show "range (\<lambda>n. A 0 - A n) \<subseteq> sets M"
      using A by auto
    show "\<And>n. A 0 - A n \<subseteq> A 0 - A (Suc n)"
      using mono_Suc by auto
  qed
  also have "\<dots> = \<mu> (A 0) - \<mu> (\<Inter>i. A i)"
    using mono A finite * by (simp, subst measure_Diff) auto
  finally show ?thesis
    by (rule pinfreal_diff_eq_diff_imp_eq[OF finite[of 0] le_IM le_MI])
qed

lemma (in measure_space) measure_down:
  assumes "P \<in> sets M" "\<And>i. B i \<in> sets M" "B \<down> P"
  and finite: "\<And>i. \<mu> (B i) \<noteq> \<omega>"
  shows "(\<lambda>i. \<mu> (B i)) \<down> \<mu> P"
  using assms unfolding antiton_def
  by (auto intro!: measure_mono continuity_from_above)
lemma (in measure_space) measure_insert:
  assumes sets: "{x} \<in> sets M" "A \<in> sets M" and "x \<notin> A"
  shows "\<mu> (insert x A) = \<mu> {x} + \<mu> A"
proof -
  have "{x} \<inter> A = {}" using `x \<notin> A` by auto
  from measure_additive[OF sets this] show ?thesis by simp
qed

lemma (in measure_space) measure_finite_singleton:
  assumes fin: "finite S"
  and ssets: "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
  shows "\<mu> S = (\<Sum>x\<in>S. \<mu> {x})"
using assms proof induct
  case (insert x S)
  have *: "\<mu> S = (\<Sum>x\<in>S. \<mu> {x})" "{x} \<in> sets M"
    using insert.prems by (blast intro!: insert.hyps(3))+

  have "(\<Union>x\<in>S. {x}) \<in> sets M"
    using  insert.prems `finite S` by (blast intro!: finite_UN)
  hence "S \<in> sets M" by auto
  from measure_insert[OF `{x} \<in> sets M` this `x \<notin> S`]
  show ?case using `x \<notin> S` `finite S` * by simp
qed simp

lemma (in measure_space) measure_finitely_additive':
  assumes "f \<in> ({..< n :: nat} \<rightarrow> sets M)"
  assumes "\<And> a b. \<lbrakk>a < n ; b < n ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}"
  assumes "s = \<Union> (f ` {..< n})"
  shows "(\<Sum>i<n. (\<mu> \<circ> f) i) = \<mu> s"
proof -
  def f' == "\<lambda> i. (if i < n then f i else {})"
  have rf: "range f' \<subseteq> sets M" unfolding f'_def
    using assms empty_sets by auto
  have df: "disjoint_family f'" unfolding f'_def disjoint_family_on_def
    using assms by simp
  have "\<Union> range f' = (\<Union> i \<in> {..< n}. f i)"
    unfolding f'_def by auto
  then have "\<mu> s = \<mu> (\<Union> range f')"
    using assms by simp
  then have part1: "(\<Sum>\<^isub>\<infinity> i. \<mu> (f' i)) = \<mu> s"
    using df rf ca[unfolded countably_additive_def, rule_format, of f']
    by auto

  have "(\<Sum>\<^isub>\<infinity> i. \<mu> (f' i)) = (\<Sum> i< n. \<mu> (f' i))"
    by (rule psuminf_finite) (simp add: f'_def)
  also have "\<dots> = (\<Sum>i<n. \<mu> (f i))"
    unfolding f'_def by auto
  finally have part2: "(\<Sum>\<^isub>\<infinity> i. \<mu> (f' i)) = (\<Sum>i<n. \<mu> (f i))" by simp
  show ?thesis using part1 part2 by auto
qed


lemma (in measure_space) measure_finitely_additive:
  assumes "finite r"
  assumes "r \<subseteq> sets M"
  assumes d: "\<And> a b. \<lbrakk>a \<in> r ; b \<in> r ; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
  shows "(\<Sum> i \<in> r. \<mu> i) = \<mu> (\<Union> r)"
using assms
proof -
  (* counting the elements in r is enough *)
  let ?R = "{..<card r}"
  obtain f where f: "f ` ?R = r" "inj_on f ?R"
    using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite r`]
    unfolding atLeast0LessThan by auto
  hence f_into_sets: "f \<in> ?R \<rightarrow> sets M" using assms by auto
  have disj: "\<And> a b. \<lbrakk>a \<in> ?R ; b \<in> ?R ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}"
  proof -
    fix a b assume asm: "a \<in> ?R" "b \<in> ?R" "a \<noteq> b"
    hence neq: "f a \<noteq> f b" using f[unfolded inj_on_def, rule_format] by blast
    from asm have "f a \<in> r" "f b \<in> r" using f by auto
    thus "f a \<inter> f b = {}" using d[of "f a" "f b"] f using neq by auto
  qed
  have "(\<Union> r) = (\<Union> i \<in> ?R. f i)"
    using f by auto
  hence "\<mu> (\<Union> r)= \<mu> (\<Union> i \<in> ?R. f i)" by simp
  also have "\<dots> = (\<Sum> i \<in> ?R. \<mu> (f i))"
    using measure_finitely_additive'[OF f_into_sets disj] by simp
  also have "\<dots> = (\<Sum> a \<in> r. \<mu> a)"
    using f[rule_format] setsum_reindex[of f ?R "\<lambda> a. \<mu> a"] by auto
  finally show ?thesis by simp
qed

lemma (in measure_space) measure_finitely_additive'':
  assumes "finite s"
  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<in> sets M"
  assumes d: "disjoint_family_on a s"
  shows "(\<Sum> i \<in> s. \<mu> (a i)) = \<mu> (\<Union> i \<in> s. a i)"
using assms
proof -
  (* counting the elements in s is enough *)
  let ?R = "{..< card s}"
  obtain f where f: "f ` ?R = s" "inj_on f ?R"
    using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite s`]
    unfolding atLeast0LessThan by auto
  hence f_into_sets: "a \<circ> f \<in> ?R \<rightarrow> sets M" using assms unfolding o_def by auto
  have disj: "\<And> i j. \<lbrakk>i \<in> ?R ; j \<in> ?R ; i \<noteq> j\<rbrakk> \<Longrightarrow> (a \<circ> f) i \<inter> (a \<circ> f) j = {}"
  proof -
    fix i j assume asm: "i \<in> ?R" "j \<in> ?R" "i \<noteq> j"
    hence neq: "f i \<noteq> f j" using f[unfolded inj_on_def, rule_format] by blast
    from asm have "f i \<in> s" "f j \<in> s" using f by auto
    thus "(a \<circ> f) i \<inter> (a \<circ> f) j = {}"
      using d f neq unfolding disjoint_family_on_def by auto
  qed
  have "(\<Union> i \<in> s. a i) = (\<Union> i \<in> f ` ?R. a i)" using f by auto
  hence "(\<Union> i \<in> s. a i) = (\<Union> i \<in> ?R. a (f i))" by auto
  hence "\<mu> (\<Union> i \<in> s. a i) = (\<Sum> i \<in> ?R. \<mu> (a (f i)))"
    using measure_finitely_additive'[OF f_into_sets disj] by simp
  also have "\<dots> = (\<Sum> i \<in> s. \<mu> (a i))"
    using f[rule_format] setsum_reindex[of f ?R "\<lambda> i. \<mu> (a i)"] by auto
  finally show ?thesis by simp
qed

lemma (in sigma_algebra) finite_additivity_sufficient:
  assumes fin: "finite (space M)" and pos: "positive \<mu>" and add: "additive M \<mu>"
  shows "measure_space M \<mu>"
proof
  show [simp]: "\<mu> {} = 0" using pos by (simp add: positive_def)
  show "countably_additive M \<mu>"
    proof (auto simp add: countably_additive_def)
      fix A :: "nat \<Rightarrow> 'a set"
      assume A: "range A \<subseteq> sets M"
         and disj: "disjoint_family A"
         and UnA: "(\<Union>i. A i) \<in> sets M"
      def I \<equiv> "{i. A i \<noteq> {}}"
      have "Union (A ` I) \<subseteq> space M" using A
        by auto (metis range_subsetD subsetD sets_into_space)
      hence "finite (A ` I)"
        by (metis finite_UnionD finite_subset fin)
      moreover have "inj_on A I" using disj
        by (auto simp add: I_def disjoint_family_on_def inj_on_def)
      ultimately have finI: "finite I"
        by (metis finite_imageD)
      hence "\<exists>N. \<forall>m\<ge>N. A m = {}"
        proof (cases "I = {}")
          case True thus ?thesis by (simp add: I_def)
        next
          case False
          hence "\<forall>i\<in>I. i < Suc(Max I)"
            by (simp add: Max_less_iff [symmetric] finI)
          hence "\<forall>m \<ge> Suc(Max I). A m = {}"
            by (simp add: I_def) (metis less_le_not_le)
          thus ?thesis
            by blast
        qed
      then obtain N where N: "\<forall>m\<ge>N. A m = {}" by blast
      then have "\<forall>m\<ge>N. \<mu> (A m) = 0" by simp
      then have "(\<Sum>\<^isub>\<infinity> n. \<mu> (A n)) = setsum (\<lambda>m. \<mu> (A m)) {..<N}"
        by (simp add: psuminf_finite)
      also have "... = \<mu> (\<Union>i<N. A i)"
        proof (induct N)
          case 0 thus ?case by simp
        next
          case (Suc n)
          have "\<mu> (A n \<union> (\<Union> x<n. A x)) = \<mu> (A n) + \<mu> (\<Union> i<n. A i)"
            proof (rule Caratheodory.additiveD [OF add])
              show "A n \<inter> (\<Union> x<n. A x) = {}" using disj
                by (auto simp add: disjoint_family_on_def nat_less_le) blast
              show "A n \<in> sets M" using A
                by force
              show "(\<Union>i<n. A i) \<in> sets M"
                proof (induct n)
                  case 0 thus ?case by simp
                next
                  case (Suc n) thus ?case using A
                    by (simp add: lessThan_Suc Un range_subsetD)
                qed
            qed
          thus ?case using Suc
            by (simp add: lessThan_Suc)
        qed
      also have "... = \<mu> (\<Union>i. A i)"
        proof -
          have "(\<Union> i<N. A i) = (\<Union>i. A i)" using N
            by auto (metis Int_absorb N disjoint_iff_not_equal lessThan_iff not_leE)
          thus ?thesis by simp
        qed
      finally show "(\<Sum>\<^isub>\<infinity> n. \<mu> (A n)) = \<mu> (\<Union>i. A i)" .
    qed
qed

lemma (in measure_space) measure_setsum_split:
  assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M"
  assumes "(\<Union>i \<in> r. b i) = space M"
  assumes "disjoint_family_on b r"
  shows "\<mu> a = (\<Sum> i \<in> r. \<mu> (a \<inter> (b i)))"
proof -
  have *: "\<mu> a = \<mu> (\<Union>i \<in> r. a \<inter> b i)"
    using assms by auto
  show ?thesis unfolding *
  proof (rule measure_finitely_additive''[symmetric])
    show "finite r" using `finite r` by auto
    { fix i assume "i \<in> r"
      hence "b i \<in> sets M" using br_in_M by auto
      thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto
    }
    show "disjoint_family_on (\<lambda>i. a \<inter> b i) r"
      using `disjoint_family_on b r`
      unfolding disjoint_family_on_def by auto
  qed
qed

lemma (in measure_space) measure_subadditive:
  assumes measurable: "A \<in> sets M" "B \<in> sets M"
  shows "\<mu> (A \<union> B) \<le> \<mu> A + \<mu> B"
proof -
  from measure_additive[of A "B - A"]
  have "\<mu> (A \<union> B) = \<mu> A + \<mu> (B - A)"
    using assms by (simp add: Diff)
  also have "\<dots> \<le> \<mu> A + \<mu> B"
    using assms by (auto intro!: add_left_mono measure_mono)
  finally show ?thesis .
qed

lemma (in measure_space) measurable_countably_subadditive:
  assumes "range f \<subseteq> sets M"
  shows "\<mu> (\<Union>i. f i) \<le> (\<Sum>\<^isub>\<infinity> i. \<mu> (f i))"
proof -
  have "\<mu> (\<Union>i. f i) = \<mu> (\<Union>i. disjointed f i)"
    unfolding UN_disjointed_eq ..
  also have "\<dots> = (\<Sum>\<^isub>\<infinity> i. \<mu> (disjointed f i))"
    using range_disjointed_sets[OF assms] measure_countably_additive
    by (simp add:  disjoint_family_disjointed comp_def)
  also have "\<dots> \<le> (\<Sum>\<^isub>\<infinity> i. \<mu> (f i))"
  proof (rule psuminf_le, rule measure_mono)
    fix i show "disjointed f i \<subseteq> f i" by (rule disjointed_subset)
    show "f i \<in> sets M" "disjointed f i \<in> sets M"
      using assms range_disjointed_sets[OF assms] by auto
  qed
  finally show ?thesis .
qed

lemma (in measure_space) restricted_measure_space:
  assumes "S \<in> sets M"
  shows "measure_space (M\<lparr> space := S, sets := (\<lambda>A. S \<inter> A) ` sets M \<rparr>) \<mu>"
    (is "measure_space ?r \<mu>")
  unfolding measure_space_def measure_space_axioms_def
proof safe
  show "sigma_algebra ?r" using restricted_sigma_algebra[OF assms] .
  show "\<mu> {} = 0" by simp
  show "countably_additive ?r \<mu>"
    unfolding countably_additive_def
  proof safe
    fix A :: "nat \<Rightarrow> 'a set"
    assume *: "range A \<subseteq> sets ?r" and **: "disjoint_family A"
    from restriction_in_sets[OF assms *[simplified]] **
    show "(\<Sum>\<^isub>\<infinity> n. \<mu> (A n)) = \<mu> (\<Union>i. A i)"
      using measure_countably_additive by simp
  qed
qed

section "@{text \<sigma>}-finite Measures"

locale sigma_finite_measure = measure_space +
  assumes sigma_finite: "\<exists>A::nat \<Rightarrow> 'a set. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<omega>)"

lemma (in sigma_finite_measure) restricted_sigma_finite_measure:
  assumes "S \<in> sets M"
  shows "sigma_finite_measure (M\<lparr> space := S, sets := (\<lambda>A. S \<inter> A) ` sets M \<rparr>) \<mu>"
    (is "sigma_finite_measure ?r _")
  unfolding sigma_finite_measure_def sigma_finite_measure_axioms_def
proof safe
  show "measure_space ?r \<mu>" using restricted_measure_space[OF assms] .
next
  obtain A :: "nat \<Rightarrow> 'a set" where
      "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. \<mu> (A i) \<noteq> \<omega>"
    using sigma_finite by auto
  show "\<exists>A::nat \<Rightarrow> 'a set. range A \<subseteq> sets ?r \<and> (\<Union>i. A i) = space ?r \<and> (\<forall>i. \<mu> (A i) \<noteq> \<omega>)"
  proof (safe intro!: exI[of _ "\<lambda>i. A i \<inter> S"] del: notI)
    fix i
    show "A i \<inter> S \<in> sets ?r"
      using `range A \<subseteq> sets M` `S \<in> sets M` by auto
  next
    fix x i assume "x \<in> S" thus "x \<in> space ?r" by simp
  next
    fix x assume "x \<in> space ?r" thus "x \<in> (\<Union>i. A i \<inter> S)"
      using `(\<Union>i. A i) = space M` `S \<in> sets M` by auto
  next
    fix i
    have "\<mu> (A i \<inter> S) \<le> \<mu> (A i)"
      using `range A \<subseteq> sets M` `S \<in> sets M` by (auto intro!: measure_mono)
    also have "\<dots> < \<omega>" using `\<mu> (A i) \<noteq> \<omega>` by (auto simp: pinfreal_less_\<omega>)
    finally show "\<mu> (A i \<inter> S) \<noteq> \<omega>" by (auto simp: pinfreal_less_\<omega>)
  qed
qed

section "Real measure values"

lemma (in measure_space) real_measure_Union:
  assumes finite: "\<mu> A \<noteq> \<omega>" "\<mu> B \<noteq> \<omega>"
  and measurable: "A \<in> sets M" "B \<in> sets M" "A \<inter> B = {}"
  shows "real (\<mu> (A \<union> B)) = real (\<mu> A) + real (\<mu> B)"
  unfolding measure_additive[symmetric, OF measurable]
  using finite by (auto simp: real_of_pinfreal_add)

lemma (in measure_space) real_measure_finite_Union:
  assumes measurable:
    "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> sets M" "disjoint_family_on A S"
  assumes finite: "\<And>i. i \<in> S \<Longrightarrow> \<mu> (A i) \<noteq> \<omega>"
  shows "real (\<mu> (\<Union>i\<in>S. A i)) = (\<Sum>i\<in>S. real (\<mu> (A i)))"
  using real_of_pinfreal_setsum[of S, OF finite]
        measure_finitely_additive''[symmetric, OF measurable]
  by simp

lemma (in measure_space) real_measure_Diff:
  assumes finite: "\<mu> A \<noteq> \<omega>"
  and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A"
  shows "real (\<mu> (A - B)) = real (\<mu> A) - real (\<mu> B)"
proof -
  have "\<mu> (A - B) \<le> \<mu> A"
    "\<mu> B \<le> \<mu> A"
    using measurable by (auto intro!: measure_mono)
  hence "real (\<mu> ((A - B) \<union> B)) = real (\<mu> (A - B)) + real (\<mu> B)"
    using measurable finite by (rule_tac real_measure_Union) auto
  thus ?thesis using `B \<subseteq> A` by (auto simp: Un_absorb2)
qed

lemma (in measure_space) real_measure_UNION:
  assumes measurable: "range A \<subseteq> sets M" "disjoint_family A"
  assumes finite: "\<mu> (\<Union>i. A i) \<noteq> \<omega>"
  shows "(\<lambda>i. real (\<mu> (A i))) sums (real (\<mu> (\<Union>i. A i)))"
proof -
  have *: "(\<Sum>\<^isub>\<infinity> i. \<mu> (A i)) = \<mu> (\<Union>i. A i)"
    using measure_countably_additive[OF measurable] by (simp add: comp_def)
  hence "(\<Sum>\<^isub>\<infinity> i. \<mu> (A i)) \<noteq> \<omega>" using finite by simp
  from psuminf_imp_suminf[OF this]
  show ?thesis using * by simp
qed

lemma (in measure_space) real_measure_subadditive:
  assumes measurable: "A \<in> sets M" "B \<in> sets M"
  and fin: "\<mu> A \<noteq> \<omega>" "\<mu> B \<noteq> \<omega>"
  shows "real (\<mu> (A \<union> B)) \<le> real (\<mu> A) + real (\<mu> B)"
proof -
  have "real (\<mu> (A \<union> B)) \<le> real (\<mu> A + \<mu> B)"
    using measure_subadditive[OF measurable] fin by (auto intro!: real_of_pinfreal_mono)
  also have "\<dots> = real (\<mu> A) + real (\<mu> B)"
    using fin by (simp add: real_of_pinfreal_add)
  finally show ?thesis .
qed

lemma (in measure_space) real_measurable_countably_subadditive:
  assumes "range f \<subseteq> sets M" and "(\<Sum>\<^isub>\<infinity> i. \<mu> (f i)) \<noteq> \<omega>"
  shows "real (\<mu> (\<Union>i. f i)) \<le> (\<Sum> i. real (\<mu> (f i)))"
proof -
  have "real (\<mu> (\<Union>i. f i)) \<le> real (\<Sum>\<^isub>\<infinity> i. \<mu> (f i))"
    using assms by (auto intro!: real_of_pinfreal_mono measurable_countably_subadditive)
  also have "\<dots> = (\<Sum> i. real (\<mu> (f i)))"
    using assms by (auto intro!: sums_unique psuminf_imp_suminf)
  finally show ?thesis .
qed

lemma (in measure_space) real_measure_setsum_singleton:
  assumes S: "finite S" "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
  and fin: "\<And>x. x \<in> S \<Longrightarrow> \<mu> {x} \<noteq> \<omega>"
  shows "real (\<mu> S) = (\<Sum>x\<in>S. real (\<mu> {x}))"
  using measure_finite_singleton[OF S] fin by (simp add: real_of_pinfreal_setsum)

lemma (in measure_space) real_continuity_from_below:
  assumes A: "range A \<subseteq> sets M" "\<And>i. A i \<subseteq> A (Suc i)" and "\<mu> (\<Union>i. A i) \<noteq> \<omega>"
  shows "(\<lambda>i. real (\<mu> (A i))) ----> real (\<mu> (\<Union>i. A i))"
proof (rule SUP_eq_LIMSEQ[THEN iffD1])
  { fix n have "\<mu> (A n) \<le> \<mu> (\<Union>i. A i)"
      using A by (auto intro!: measure_mono)
    hence "\<mu> (A n) \<noteq> \<omega>" using assms by auto }
  note this[simp]

  show "mono (\<lambda>i. real (\<mu> (A i)))" unfolding mono_iff_le_Suc using A
    by (auto intro!: real_of_pinfreal_mono measure_mono)

  show "(SUP n. Real (real (\<mu> (A n)))) = Real (real (\<mu> (\<Union>i. A i)))"
    using continuity_from_below[OF A(1), OF A(2)]
    using assms by (simp add: Real_real)
qed simp_all

lemma (in measure_space) real_continuity_from_above:
  assumes A: "range A \<subseteq> sets M"
  and mono_Suc: "\<And>n.  A (Suc n) \<subseteq> A n"
  and finite: "\<And>i. \<mu> (A i) \<noteq> \<omega>"
  shows "(\<lambda>n. real (\<mu> (A n))) ----> real (\<mu> (\<Inter>i. A i))"
proof (rule INF_eq_LIMSEQ[THEN iffD1])
  { fix n have "\<mu> (\<Inter>i. A i) \<le> \<mu> (A n)"
      using A by (auto intro!: measure_mono)
    hence "\<mu> (\<Inter>i. A i) \<noteq> \<omega>" using assms by auto }
  note this[simp]

  show "mono (\<lambda>i. - real (\<mu> (A i)))" unfolding mono_iff_le_Suc using assms
    by (auto intro!: real_of_pinfreal_mono measure_mono)

  show "(INF n. Real (real (\<mu> (A n)))) =
    Real (real (\<mu> (\<Inter>i. A i)))"
    using continuity_from_above[OF A, OF mono_Suc finite]
    using assms by (simp add: Real_real)
qed simp_all

locale finite_measure = measure_space +
  assumes finite_measure_of_space: "\<mu> (space M) \<noteq> \<omega>"

sublocale finite_measure < sigma_finite_measure
proof
  show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<omega>)"
    using finite_measure_of_space by (auto intro!: exI[of _ "\<lambda>x. space M"])
qed

lemma (in finite_measure) finite_measure:
  assumes "A \<in> sets M"
  shows "\<mu> A \<noteq> \<omega>"
proof -
  from `A \<in> sets M` have "A \<subseteq> space M"
    using sets_into_space by blast
  hence "\<mu> A \<le> \<mu> (space M)"
    using assms top by (rule measure_mono)
  also have "\<dots> < \<omega>"
    using finite_measure_of_space unfolding pinfreal_less_\<omega> .
  finally show ?thesis unfolding pinfreal_less_\<omega> .
qed

lemma (in finite_measure) restricted_finite_measure:
  assumes "S \<in> sets M"
  shows "finite_measure (M\<lparr> space := S, sets := (\<lambda>A. S \<inter> A) ` sets M \<rparr>) \<mu>"
    (is "finite_measure ?r _")
  unfolding finite_measure_def finite_measure_axioms_def
proof (safe del: notI)
  show "measure_space ?r \<mu>" using restricted_measure_space[OF assms] .
next
  show "\<mu> (space ?r) \<noteq> \<omega>" using finite_measure[OF `S \<in> sets M`] by auto
qed

lemma (in finite_measure) real_finite_measure_Diff:
  assumes "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A"
  shows "real (\<mu> (A - B)) = real (\<mu> A) - real (\<mu> B)"
  using finite_measure[OF `A \<in> sets M`] by (rule real_measure_Diff[OF _ assms])

lemma (in finite_measure) real_finite_measure_Union:
  assumes sets: "A \<in> sets M" "B \<in> sets M" and "A \<inter> B = {}"
  shows "real (\<mu> (A \<union> B)) = real (\<mu> A) + real (\<mu> B)"
  using sets by (auto intro!: real_measure_Union[OF _ _ assms] finite_measure)

lemma (in finite_measure) real_finite_measure_finite_Union:
  assumes "finite S" and dis: "disjoint_family_on A S"
  and *: "\<And>i. i \<in> S \<Longrightarrow> A i \<in> sets M"
  shows "real (\<mu> (\<Union>i\<in>S. A i)) = (\<Sum>i\<in>S. real (\<mu> (A i)))"
proof (rule real_measure_finite_Union[OF `finite S` _ dis])
  fix i assume "i \<in> S" from *[OF this] show "A i \<in> sets M" .
  from finite_measure[OF this] show "\<mu> (A i) \<noteq> \<omega>" .
qed

lemma (in finite_measure) real_finite_measure_UNION:
  assumes measurable: "range A \<subseteq> sets M" "disjoint_family A"
  shows "(\<lambda>i. real (\<mu> (A i))) sums (real (\<mu> (\<Union>i. A i)))"
proof (rule real_measure_UNION[OF assms])
  have "(\<Union>i. A i) \<in> sets M" using measurable(1) by (rule countable_UN)
  thus "\<mu> (\<Union>i. A i) \<noteq> \<omega>" by (rule finite_measure)
qed

lemma (in finite_measure) real_measure_mono:
  "A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A \<subseteq> B \<Longrightarrow> real (\<mu> A) \<le> real (\<mu> B)"
  by (auto intro!: measure_mono real_of_pinfreal_mono finite_measure)

lemma (in finite_measure) real_finite_measure_subadditive:
  assumes measurable: "A \<in> sets M" "B \<in> sets M"
  shows "real (\<mu> (A \<union> B)) \<le> real (\<mu> A) + real (\<mu> B)"
  using measurable measurable[THEN finite_measure] by (rule real_measure_subadditive)

lemma (in finite_measure) real_finite_measurable_countably_subadditive:
  assumes "range f \<subseteq> sets M" and "summable (\<lambda>i. real (\<mu> (f i)))"
  shows "real (\<mu> (\<Union>i. f i)) \<le> (\<Sum> i. real (\<mu> (f i)))"
proof (rule real_measurable_countably_subadditive[OF assms(1)])
  have *: "\<And>i. f i \<in> sets M" using assms by auto
  have "(\<lambda>i. real (\<mu> (f i))) sums (\<Sum>i. real (\<mu> (f i)))"
    using assms(2) by (rule summable_sums)
  from suminf_imp_psuminf[OF this]
  have "(\<Sum>\<^isub>\<infinity>i. \<mu> (f i)) = Real (\<Sum>i. real (\<mu> (f i)))"
    using * by (simp add: Real_real finite_measure)
  thus "(\<Sum>\<^isub>\<infinity>i. \<mu> (f i)) \<noteq> \<omega>" by simp
qed

lemma (in finite_measure) real_finite_measure_finite_singelton:
  assumes "finite S" and *: "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M"
  shows "real (\<mu> S) = (\<Sum>x\<in>S. real (\<mu> {x}))"
proof (rule real_measure_setsum_singleton[OF `finite S`])
  fix x assume "x \<in> S" thus "{x} \<in> sets M" by (rule *)
  with finite_measure show "\<mu> {x} \<noteq> \<omega>" .
qed

lemma (in finite_measure) real_finite_continuity_from_below:
  assumes "range A \<subseteq> sets M" "\<And>i. A i \<subseteq> A (Suc i)"
  shows "(\<lambda>i. real (\<mu> (A i))) ----> real (\<mu> (\<Union>i. A i))"
  using real_continuity_from_below[OF assms(1), OF assms(2) finite_measure] assms by auto

lemma (in finite_measure) real_finite_continuity_from_above:
  assumes A: "range A \<subseteq> sets M"
  and mono_Suc: "\<And>n.  A (Suc n) \<subseteq> A n"
  shows "(\<lambda>n. real (\<mu> (A n))) ----> real (\<mu> (\<Inter>i. A i))"
  using real_continuity_from_above[OF A, OF mono_Suc finite_measure] A
  by auto

lemma (in finite_measure) real_finite_measure_finite_Union':
  assumes "finite S" "A`S \<subseteq> sets M" "disjoint_family_on A S"
  shows "real (\<mu> (\<Union>i\<in>S. A i)) = (\<Sum>i\<in>S. real (\<mu> (A i)))"
  using assms real_finite_measure_finite_Union[of S A] by auto

lemma (in finite_measure) finite_measure_compl:
  assumes s: "s \<in> sets M"
  shows "\<mu> (space M - s) = \<mu> (space M) - \<mu> s"
  using measure_compl[OF s, OF finite_measure, OF s] .

section {* Measure preserving *}

definition "measure_preserving A \<mu> B \<nu> =
    {f \<in> measurable A B. (\<forall>y \<in> sets B. \<mu> (f -` y \<inter> space A) = \<nu> y)}"

lemma (in finite_measure) measure_preserving_lift:
  fixes f :: "'a \<Rightarrow> 'a2" and A :: "('a2, 'b2) algebra_scheme"
  assumes "algebra A"
  assumes "finite_measure (sigma (space A) (sets A)) \<nu>" (is "finite_measure ?sA _")
  assumes fmp: "f \<in> measure_preserving M \<mu> A \<nu>"
  shows "f \<in> measure_preserving M \<mu> (sigma (space A) (sets A)) \<nu>"
proof -
  interpret sA: finite_measure ?sA \<nu> by fact
  interpret A: algebra A by fact
  show ?thesis using fmp
    proof (clarsimp simp add: measure_preserving_def)
      assume fm: "f \<in> measurable M A"
         and meq: "\<forall>y\<in>sets A. \<mu> (f -` y \<inter> space M) = \<nu> y"
      have f12: "f \<in> measurable M ?sA"
        using measurable_subset[OF A.sets_into_space] fm by auto
      hence ffn: "f \<in> space M \<rightarrow> space A"
        by (simp add: measurable_def)
      have "space M \<subseteq> f -` (space A)"
        by auto (metis PiE ffn)
      hence fveq [simp]: "(f -` (space A)) \<inter> space M = space M"
        by blast
      {
        fix y
        assume y: "y \<in> sets ?sA"
        have "sets ?sA = sigma_sets (space A) (sets A)" (is "_ = ?A") by (auto simp: sigma_def)
        also have "\<dots> \<subseteq> {s . \<mu> ((f -` s) \<inter> space M) = \<nu> s}"
          proof (rule A.sigma_property_disjoint, auto)
            fix x assume "x \<in> sets A" then show "\<mu> (f -` x \<inter> space M) = \<nu> x" by (simp add: meq)
          next
            fix s
            assume eq: "\<mu> (f -` s \<inter> space M) = \<nu> s" and s: "s \<in> ?A"
            then have s': "s \<in> sets ?sA" by (simp add: sigma_def)
            show "\<mu> (f -` (space A - s) \<inter> space M) = \<nu> (space A - s)"
              using sA.finite_measure_compl[OF s']
              using measurable_sets[OF f12 s'] meq[THEN bspec, OF A.top]
              by (simp add: vimage_Diff Diff_Int_distrib2 finite_measure_compl eq)
          next
            fix S
            assume S0: "S 0 = {}"
               and SSuc: "\<And>n.  S n \<subseteq> S (Suc n)"
               and rS1: "range S \<subseteq> {s. \<mu> (f -` s \<inter> space M) = \<nu> s}"
               and "range S \<subseteq> ?A"
            hence rS2: "range S \<subseteq> sets ?sA" by (simp add: sigma_def)
            have eq1: "\<And>i. \<mu> (f -` S i \<inter> space M) = \<nu> (S i)"
              using rS1 by blast
            have *: "(\<lambda>n. \<nu> (S n)) = (\<lambda>n. \<mu> (f -` S n \<inter> space M))"
              by (simp add: eq1)
            have "(SUP n. ... n) = \<mu> (\<Union>i. f -` S i \<inter> space M)"
              proof (rule measure_countable_increasing)
                show "range (\<lambda>i. f -` S i \<inter> space M) \<subseteq> sets M"
                  using f12 rS2 by (auto simp add: measurable_def)
                show "f -` S 0 \<inter> space M = {}" using S0
                  by blast
                show "\<And>n. f -` S n \<inter> space M \<subseteq> f -` S (Suc n) \<inter> space M"
                  using SSuc by auto
              qed
            also have "\<mu> (\<Union>i. f -` S i \<inter> space M) = \<mu> (f -` (\<Union>i. S i) \<inter> space M)"
              by (simp add: vimage_UN)
            finally have "(SUP n. \<nu> (S n)) = \<mu> (f -` (\<Union>i. S i) \<inter> space M)" unfolding * .
            moreover
            have "(SUP n. \<nu> (S n)) = \<nu> (\<Union>i. S i)"
              by (rule sA.measure_countable_increasing[OF rS2, OF S0 SSuc])
            ultimately
            show "\<mu> (f -` (\<Union>i. S i) \<inter> space M) = \<nu> (\<Union>i. S i)" by simp
          next
            fix S :: "nat => 'a2 set"
              assume dS: "disjoint_family S"
                 and rS1: "range S \<subseteq> {s. \<mu> (f -` s \<inter> space M) = \<nu> s}"
                 and "range S \<subseteq> ?A"
              hence rS2: "range S \<subseteq> sets ?sA" by (simp add: sigma_def)
              have "\<And>i. \<mu> (f -` S i \<inter> space M) = \<nu> (S i)"
                using rS1 by blast
              hence *: "(\<lambda>i. \<nu> (S i)) = (\<lambda>n. \<mu> (f -` S n \<inter> space M))"
                by simp
              have "psuminf ... = \<mu> (\<Union>i. f -` S i \<inter> space M)"
                proof (rule measure_countably_additive)
                  show "range (\<lambda>i. f -` S i \<inter> space M) \<subseteq> sets M"
                    using f12 rS2 by (auto simp add: measurable_def)
                  show "disjoint_family (\<lambda>i. f -` S i \<inter> space M)" using dS
                    by (auto simp add: disjoint_family_on_def)
                qed
              hence "(\<Sum>\<^isub>\<infinity> i. \<nu> (S i)) = \<mu> (\<Union>i. f -` S i \<inter> space M)" unfolding * .
              with sA.measure_countably_additive [OF rS2 dS]
              have "\<mu> (\<Union>i. f -` S i \<inter> space M) = \<nu> (\<Union>i. S i)"
                by simp
              moreover have "\<mu> (f -` (\<Union>i. S i) \<inter> space M) = \<mu> (\<Union>i. f -` S i \<inter> space M)"
                by (simp add: vimage_UN)
              ultimately show "\<mu> (f -` (\<Union>i. S i) \<inter> space M) = \<nu> (\<Union>i. S i)"
                by metis
          qed
        finally have "sets ?sA \<subseteq> {s . \<mu> ((f -` s) \<inter> space M) = \<nu> s}" .
        hence "\<mu> (f -` y \<inter> space M) = \<nu> y" using y by force
      }
      thus "f \<in> measurable M ?sA \<and> (\<forall>y\<in>sets ?sA. \<mu> (f -` y \<inter> space M) = \<nu> y)"
        by (blast intro: f12)
    qed
qed

section "Finite spaces"

locale finite_measure_space = measure_space +
  assumes finite_space: "finite (space M)"
  and sets_eq_Pow: "sets M = Pow (space M)"
  and finite_single_measure: "\<And>x. x \<in> space M \<Longrightarrow> \<mu> {x} \<noteq> \<omega>"

lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. \<mu> {x}) = \<mu> (space M)"
  using measure_finitely_additive''[of "space M" "\<lambda>i. {i}"]
  by (simp add: sets_eq_Pow disjoint_family_on_def finite_space)

sublocale finite_measure_space < finite_measure
proof
  show "\<mu> (space M) \<noteq> \<omega>"
    unfolding sum_over_space[symmetric] setsum_\<omega>
    using finite_space finite_single_measure by auto
qed

lemma psuminf_cmult_indicator:
  assumes "disjoint_family A" "x \<in> A i"
  shows "(\<Sum>\<^isub>\<infinity> n. f n * indicator (A n) x) = f i"
proof -
  have **: "\<And>n. f n * indicator (A n) x = (if n = i then f n else 0 :: pinfreal)"
    using `x \<in> A i` assms unfolding disjoint_family_on_def indicator_def by auto
  then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: pinfreal)"
    by (auto simp: setsum_cases)
  moreover have "(SUP n. if i < n then f i else 0) = (f i :: pinfreal)"
  proof (rule pinfreal_SUPI)
    fix y :: pinfreal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
    from this[of "Suc i"] show "f i \<le> y" by auto
  qed simp
  ultimately show ?thesis using `x \<in> A i` unfolding psuminf_def by auto
qed

lemma psuminf_indicator:
  assumes "disjoint_family A"
  shows "(\<Sum>\<^isub>\<infinity> n. indicator (A n) x) = indicator (\<Union>i. A i) x"
proof cases
  assume *: "x \<in> (\<Union>i. A i)"
  then obtain i where "x \<in> A i" by auto
  from psuminf_cmult_indicator[OF assms, OF this, of "\<lambda>i. 1"]
  show ?thesis using * by simp
qed simp

end