Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: arrays_examples.prf Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>Caratheodory Extension Theorem\<close>

theory Caratheodory
imports Measure_Space
begin

text \<open>
  Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
\<close>

lemma suminf_ennreal_2dimen:
  fixes f:: "nat \ nat \ ennreal"
  assumes "\m. g m = (\n. f (m,n))"
  shows "(\i. f (prod_decode i)) = suminf g"
proof -
  have g_def: "g = (\m. (\n. f (m,n)))"
    using assms by (simp add: fun_eq_iff)
  have reindex: "\B. (\x\B. f (prod_decode x)) = sum f (prod_decode ` B)"
    by (simp add: sum.reindex[OF inj_prod_decode] comp_def)
  have "(SUP n. \i UNIV \ UNIV. \in
  proof (intro SUP_eq; clarsimp simp: sum.cartesian_product reindex)
    fix n
    let ?M = "\f. Suc (Max (f ` prod_decode ` {..
    { fix a b x assume "x < n" and [symmetric]: "(a, b) = prod_decode x"
      then have "a < ?M fst" "b < ?M snd"
        by (auto intro!: Max_ge le_imp_less_Suc image_eqI) }
    then have "sum f (prod_decode ` {.. sum f ({.. {..
      by (auto intro!: sum_mono2)
    then show "\a b. sum f (prod_decode ` {.. sum f ({.. {..
  next
    fix a b
    let ?M = "prod_decode ` {.. {..
    { fix a' b' assume "a' < a" "b' < b" then have "(a', b') \ ?M"
        by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) }
    then have "sum f ({.. {.. sum f ?M"
      by (auto intro!: sum_mono2)
    then show "\n. sum f ({.. {.. sum f (prod_decode ` {..
      by auto
  qed
  also have "\ = (SUP p. \in. f (i, n))"
    unfolding suminf_sum[OF summableI, symmetric]
    by (simp add: suminf_eq_SUP SUP_pair sum.swap[of _ "{..< fst _}"])
  finally show ?thesis unfolding g_def
    by (simp add: suminf_eq_SUP)
qed

subsection \<open>Characterizations of Measures\<close>

definition\<^marker>\<open>tag important\<close> outer_measure_space where
  "outer_measure_space M f \ positive M f \ increasing M f \ countably_subadditive M f"

subsubsection\<^marker>\<open>tag important\<close> \<open>Lambda Systems\<close>

definition\<^marker>\<open>tag important\<close> lambda_system :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set set"
where
  "lambda_system \ M f = {l \ M. \x \ M. f (l \ x) + f ((\ - l) \ x) = f x}"

lemma (in algebra) lambda_system_eq:
  "lambda_system \ M f = {l \ M. \x \ M. f (x \ l) + f (x - l) = f x}"
proof -
  have [simp]: "\l x. l \ M \ x \ M \ (\ - l) \ x = x - l"
    by (metis Int_Diff Int_absorb1 Int_commute sets_into_space)
  show ?thesis
    by (auto simp add: lambda_system_def) (metis Int_commute)+
qed

lemma (in algebra) lambda_system_empty: "positive M f \ {} \ lambda_system \ M f"
  by (auto simp add: positive_def lambda_system_eq)

lemma lambda_system_sets: "x \ lambda_system \ M f \ x \ M"
  by (simp add: lambda_system_def)

lemma (in algebra) lambda_system_Compl:
  fixes f:: "'a set \ ennreal"
  assumes x: "x \ lambda_system \ M f"
  shows "\ - x \ lambda_system \ M f"
proof -
  have "x \ \"
    by (metis sets_into_space lambda_system_sets x)
  hence "\ - (\ - x) = x"
    by (metis double_diff equalityE)
  with x show ?thesis
    by (force simp add: lambda_system_def ac_simps)
qed

lemma (in algebra) lambda_system_Int:
  fixes f:: "'a set \ ennreal"
  assumes xl: "x \ lambda_system \ M f" and yl: "y \ lambda_system \ M f"
  shows "x \ y \ lambda_system \ M f"
proof -
  from xl yl show ?thesis
  proof (auto simp add: positive_def lambda_system_eq Int)
    fix u
    assume x: "x \ M" and y: "y \ M" and u: "u \ M"
       and fx: "\z\M. f (z \ x) + f (z - x) = f z"
       and fy: "\z\M. f (z \ y) + f (z - y) = f z"
    have "u - x \ y \ M"
      by (metis Diff Diff_Int Un u x y)
    moreover
    have "(u - (x \ y)) \ y = u \ y - x" by blast
    moreover
    have "u - x \ y - y = u - y" by blast
    ultimately
    have ey: "f (u - x \ y) = f (u \ y - x) + f (u - y)" using fy
      by force
    have "f (u \ (x \ y)) + f (u - x \ y)
          = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
      by (simp add: ey ac_simps)
    also have "... = (f ((u \ y) \ x) + f (u \ y - x)) + f (u - y)"
      by (simp add: Int_ac)
    also have "... = f (u \ y) + f (u - y)"
      using fx [THEN bspec, of "u \ y"] Int y u
      by force
    also have "... = f u"
      by (metis fy u)
    finally show "f (u \ (x \ y)) + f (u - x \ y) = f u" .
  qed
qed

lemma (in algebra) lambda_system_Un:
  fixes f:: "'a set \ ennreal"
  assumes xl: "x \ lambda_system \ M f" and yl: "y \ lambda_system \ M f"
  shows "x \ y \ lambda_system \ M f"
proof -
  have "(\ - x) \ (\ - y) \ M"
    by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
  moreover
  have "x \ y = \ - ((\ - x) \ (\ - y))"
    by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+
  ultimately show ?thesis
    by (metis lambda_system_Compl lambda_system_Int xl yl)
qed

lemma (in algebra) lambda_system_algebra:
  "positive M f \ algebra \ (lambda_system \ M f)"
  apply (auto simp add: algebra_iff_Un)
  apply (metis lambda_system_sets subsetD sets_into_space)
  apply (metis lambda_system_empty)
  apply (metis lambda_system_Compl)
  apply (metis lambda_system_Un)
  done

lemma (in algebra) lambda_system_strong_additive:
  assumes z: "z \ M" and disj: "x \ y = {}"
      and xl: "x \ lambda_system \ M f" and yl: "y \ lambda_system \ M f"
  shows "f (z \ (x \ y)) = f (z \ x) + f (z \ y)"
proof -
  have "z \ x = (z \ (x \ y)) \ x" using disj by blast
  moreover
  have "z \ y = (z \ (x \ y)) - x" using disj by blast
  moreover
  have "(z \ (x \ y)) \ M"
    by (metis Int Un lambda_system_sets xl yl z)
  ultimately show ?thesis using xl yl
    by (simp add: lambda_system_eq)
qed

lemma (in algebra) lambda_system_additive: "additive (lambda_system \ M f) f"
proof (auto simp add: additive_def)
  fix x and y
  assume disj: "x \ y = {}"
     and xl: "x \ lambda_system \ M f" and yl: "y \ lambda_system \ M f"
  hence  "x \ M" "y \ M" by (blast intro: lambda_system_sets)+
  thus "f (x \ y) = f x + f y"
    using lambda_system_strong_additive [OF top disj xl yl]
    by (simp add: Un)
qed

lemma lambda_system_increasing: "increasing M f \ increasing (lambda_system \ M f) f"
  by (simp add: increasing_def lambda_system_def)

lemma lambda_system_positive: "positive M f \ positive (lambda_system \ M f) f"
  by (simp add: positive_def lambda_system_def)

lemma (in algebra) lambda_system_strong_sum:
  fixes A:: "nat \ 'a set" and f :: "'a set \ ennreal"
  assumes f: "positive M f" and a: "a \ M"
      and A: "range A \ lambda_system \ M f"
      and disj: "disjoint_family A"
  shows  "(\i = 0..A i)) = f (a \ (\i\{0..
proof (induct n)
  case 0 show ?case using f by (simp add: positive_def)
next
  case (Suc n)
  have 2: "A n \ \ (A ` {0..
    by (force simp add: disjoint_family_on_def neq_iff)
  have 3: "A n \ lambda_system \ M f" using A
    by blast
  interpret l: algebra \<Omega> "lambda_system \<Omega> M f"
    using f by (rule lambda_system_algebra)
  have 4: "\ (A ` {0.. lambda_system \ M f"
    using A l.UNION_in_sets by simp
  from Suc.hyps show ?case
    by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
qed

proposition (in sigma_algebra) lambda_system_caratheodory:
  assumes oms: "outer_measure_space M f"
      and A: "range A \ lambda_system \ M f"
      and disj: "disjoint_family A"
  shows  "(\i. A i) \ lambda_system \ M f \ (\i. f (A i)) = f (\i. A i)"
proof -
  have pos: "positive M f" and inc: "increasing M f"
   and csa: "countably_subadditive M f"
    by (metis oms outer_measure_space_def)+
  have sa: "subadditive M f"
    by (metis countably_subadditive_subadditive csa pos)
  have A': "\S. A`S \ (lambda_system \ M f)" using A
    by auto
  interpret ls: algebra \<Omega> "lambda_system \<Omega> M f"
    using pos by (rule lambda_system_algebra)
  have A'': "range A \ M"
     by (metis A image_subset_iff lambda_system_sets)

  have U_in: "(\i. A i) \ M"
    by (metis A'' countable_UN)
  have U_eq: "f (\i. A i) = (\i. f (A i))"
  proof (rule antisym)
    show "f (\i. A i) \ (\i. f (A i))"
      using csa[unfolded countably_subadditive_def] A'' disj U_in by auto
    have dis: "\N. disjoint_family_on A {..
    show "(\i. f (A i)) \ f (\i. A i)"
      using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis] A''
      by (intro suminf_le_const[OF summableI]) (auto intro!: increasingD[OF inc] countable_UN)
  qed
  have "f (a \ (\i. A i)) + f (a - (\i. A i)) = f a"
    if a [iff]: "a \ M" for a
  proof (rule antisym)
    have "range (\i. a \ A i) \ M" using A''
      by blast
    moreover
    have "disjoint_family (\i. a \ A i)" using disj
      by (auto simp add: disjoint_family_on_def)
    moreover
    have "a \ (\i. A i) \ M"
      by (metis Int U_in a)
    ultimately
    have "f (a \ (\i. A i)) \ (\i. f (a \ A i))"
      using csa[unfolded countably_subadditive_def, rule_format, of "(\i. a \ A i)"]
      by (simp add: o_def)
    hence "f (a \ (\i. A i)) + f (a - (\i. A i)) \ (\i. f (a \ A i)) + f (a - (\i. A i))"
      by (rule add_right_mono)
    also have "\ \ f a"
    proof (intro ennreal_suminf_bound_add)
      fix n
      have UNION_in: "(\i\{0.. M"
        by (metis A'' UNION_in_sets)
      have le_fa: "f (\ (A ` {0.. a) \ f a" using A''
        by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
      have ls: "(\i\{0.. lambda_system \ M f"
        using ls.UNION_in_sets by (simp add: A)
      hence eq_fa: "f a = f (a \ (\i\{0..i\{0..
        by (simp add: lambda_system_eq UNION_in)
      have "f (a - (\i. A i)) \ f (a - (\i\{0..
        by (blast intro: increasingD [OF inc] UNION_in U_in)
      thus "(\i A i)) + f (a - (\i. A i)) \ f a"
        by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
    qed
    finally show "f (a \ (\i. A i)) + f (a - (\i. A i)) \ f a"
      by simp
  next
    have "f a \ f (a \ (\i. A i) \ (a - (\i. A i)))"
      by (blast intro:  increasingD [OF inc] U_in)
    also have "... \ f (a \ (\i. A i)) + f (a - (\i. A i))"
      by (blast intro: subadditiveD [OF sa] U_in)
    finally show "f a \ f (a \ (\i. A i)) + f (a - (\i. A i))" .
  qed
  thus  ?thesis
    by (simp add: lambda_system_eq sums_iff U_eq U_in)
qed

proposition (in sigma_algebra) caratheodory_lemma:
  assumes oms: "outer_measure_space M f"
  defines "L \ lambda_system \ M f"
  shows "measure_space \ L f"
proof -
  have pos: "positive M f"
    by (metis oms outer_measure_space_def)
  have alg: "algebra \ L"
    using lambda_system_algebra [of f, OF pos]
    by (simp add: algebra_iff_Un L_def)
  then
  have "sigma_algebra \ L"
    using lambda_system_caratheodory [OF oms]
    by (simp add: sigma_algebra_disjoint_iff L_def)
  moreover
  have "countably_additive L f" "positive L f"
    using pos lambda_system_caratheodory [OF oms]
    by (auto simp add: lambda_system_sets L_def countably_additive_def positive_def)
  ultimately
  show ?thesis
    using pos by (simp add: measure_space_def)
qed

definition\<^marker>\<open>tag important\<close> outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set \<Rightarrow> ennreal" where
   "outer_measure M f X =
     (INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))"

lemma (in ring_of_sets) outer_measure_agrees:
  assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s \ M"
  shows "outer_measure M f s = f s"
  unfolding outer_measure_def
proof (safe intro!: antisym INF_greatest)
  fix A :: "nat \ 'a set" assume A: "range A \ M" and dA: "disjoint_family A" and sA: "s \ (\x. A x)"
  have inc: "increasing M f"
    by (metis additive_increasing ca countably_additive_additive posf)
  have "f s = f (\i. A i \ s)"
    using sA by (auto simp: Int_absorb1)
  also have "\ = (\i. f (A i \ s))"
    using sA dA A s
    by (intro ca[unfolded countably_additive_def, rule_format, symmetric])
       (auto simp: Int_absorb1 disjoint_family_on_def)
  also have "... \ (\i. f (A i))"
    using A s by (auto intro!: suminf_le increasingD[OF inc])
  finally show "f s \ (\i. f (A i))" .
next
  have "(\i. f (if i = 0 then s else {})) \ f s"
    using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto
  with s show "(INF A\{A. range A \ M \ disjoint_family A \ s \ \(A ` UNIV)}. \i. f (A i)) \ f s"
    by (intro INF_lower2[of "\i. if i = 0 then s else {}"])
       (auto simp: disjoint_family_on_def)
qed

lemma outer_measure_empty:
  "positive M f \ {} \ M \ outer_measure M f {} = 0"
  unfolding outer_measure_def
  by (intro antisym INF_lower2[of  "\_. {}"]) (auto simp: disjoint_family_on_def positive_def)

lemma (in ring_of_sets) positive_outer_measure:
  assumes "positive M f" shows "positive (Pow \) (outer_measure M f)"
  unfolding positive_def by (auto simp: assms outer_measure_empty)

lemma (in ring_of_sets) increasing_outer_measure: "increasing (Pow \) (outer_measure M f)"
  by (force simp: increasing_def outer_measure_def intro!: INF_greatest intro: INF_lower)

lemma (in ring_of_sets) outer_measure_le:
  assumes pos: "positive M f" and inc: "increasing M f" and A: "range A \ M" and X: "X \ (\i. A i)"
  shows "outer_measure M f X \ (\i. f (A i))"
  unfolding outer_measure_def
proof (safe intro!: INF_lower2[of "disjointed A"] del: subsetI)
  show dA: "range (disjointed A) \ M"
    by (auto intro!: A range_disjointed_sets)
  have "\n. f (disjointed A n) \ f (A n)"
    by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
  then show "(\i. f (disjointed A i)) \ (\i. f (A i))"
    by (blast intro!: suminf_le)
qed (auto simp: X UN_disjointed_eq disjoint_family_disjointed)

lemma (in ring_of_sets) outer_measure_close:
  "outer_measure M f X < e \ \A. range A \ M \ disjoint_family A \ X \ (\i. A i) \ (\i. f (A i)) < e"
  unfolding outer_measure_def INF_less_iff by auto

lemma (in ring_of_sets) countably_subadditive_outer_measure:
  assumes posf: "positive M f" and inc: "increasing M f"
  shows "countably_subadditive (Pow \) (outer_measure M f)"
proof (simp add: countably_subadditive_def, safe)
  fix A :: "nat \ _" assume A: "range A \ Pow (\)" and sb: "(\i. A i) \ \"
  let ?O = "outer_measure M f"
  show "?O (\i. A i) \ (\n. ?O (A n))"
  proof (rule ennreal_le_epsilon)
    fix b and e :: real assume "0 < e" "(\n. outer_measure M f (A n)) < top"
    then have *: "\n. outer_measure M f (A n) < outer_measure M f (A n) + e * (1/2)^Suc n"
      by (auto simp add: less_top dest!: ennreal_suminf_lessD)
    obtain B
      where B: "\n. range (B n) \ M"
      and sbB: "\n. A n \ (\i. B n i)"
      and Ble: "\n. (\i. f (B n i)) \ ?O (A n) + e * (1/2)^(Suc n)"
      by (metis less_imp_le outer_measure_close[OF *])

    define C where "C = case_prod B o prod_decode"
    from B have B_in_M: "\i j. B i j \ M"
      by (rule range_subsetD)
    then have C: "range C \ M"
      by (auto simp add: C_def split_def)
    have A_C: "(\i. A i) \ (\i. C i)"
      using sbB by (auto simp add: C_def subset_eq) (metis prod.case prod_encode_inverse)

    have "?O (\i. A i) \ ?O (\i. C i)"
      using A_C A C by (intro increasing_outer_measure[THEN increasingD]) (auto dest!: sets_into_space)
    also have "\ \ (\i. f (C i))"
      using C by (intro outer_measure_le[OF posf inc]) auto
    also have "\ = (\n. \i. f (B n i))"
      using B_in_M unfolding C_def comp_def by (intro suminf_ennreal_2dimen) auto
    also have "\ \ (\n. ?O (A n) + e * (1/2) ^ Suc n)"
      using B_in_M by (intro suminf_le suminf_nonneg allI Ble) auto
    also have "... = (\n. ?O (A n)) + (\n. ennreal e * ennreal ((1/2) ^ Suc n))"
      using \<open>0 < e\<close> by (subst suminf_add[symmetric])
                       (auto simp del: ennreal_suminf_cmult simp add: ennreal_mult[symmetric])
    also have "\ = (\n. ?O (A n)) + e"
      unfolding ennreal_suminf_cmult
      by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto
    finally show "?O (\i. A i) \ (\n. ?O (A n)) + e" .
  qed
qed

lemma (in ring_of_sets) outer_measure_space_outer_measure:
  "positive M f \ increasing M f \ outer_measure_space (Pow \) (outer_measure M f)"
  by (simp add: outer_measure_space_def
    positive_outer_measure increasing_outer_measure countably_subadditive_outer_measure)

lemma (in ring_of_sets) algebra_subset_lambda_system:
  assumes posf: "positive M f" and inc: "increasing M f"
      and add: "additive M f"
  shows "M \ lambda_system \ (Pow \) (outer_measure M f)"
proof (auto dest: sets_into_space
            simp add: algebra.lambda_system_eq [OF algebra_Pow])
  fix x s assume x: "x \ M" and s: "s \ \"
  have [simp]: "\x. x \ M \ s \ (\ - x) = s - x" using s
    by blast
  have "outer_measure M f (s \ x) + outer_measure M f (s - x) \ outer_measure M f s"
    unfolding outer_measure_def[of M f s]
  proof (safe intro!: INF_greatest)
    fix A :: "nat \ 'a set" assume A: "disjoint_family A" "range A \ M" "s \ (\i. A i)"
    have "outer_measure M f (s \ x) \ (\i. f (A i \ x))"
      unfolding outer_measure_def
    proof (safe intro!: INF_lower2[of "\i. A i \ x"])
      from A(1) show "disjoint_family (\i. A i \ x)"
        by (rule disjoint_family_on_bisimulation) auto
    qed (insert x A, auto)
    moreover
    have "outer_measure M f (s - x) \ (\i. f (A i - x))"
      unfolding outer_measure_def
    proof (safe intro!: INF_lower2[of "\i. A i - x"])
      from A(1) show "disjoint_family (\i. A i - x)"
        by (rule disjoint_family_on_bisimulation) auto
    qed (insert x A, auto)
    ultimately have "outer_measure M f (s \ x) + outer_measure M f (s - x) \
        (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono)
    also have "\ = (\i. f (A i \ x) + f (A i - x))"
      using A(2) x posf by (subst suminf_add) (auto simp: positive_def)
    also have "\ = (\i. f (A i))"
      using A x
      by (subst add[THEN additiveD, symmetric])
         (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f])
    finally show "outer_measure M f (s \ x) + outer_measure M f (s - x) \ (\i. f (A i))" .
  qed
  moreover
  have "outer_measure M f s \ outer_measure M f (s \ x) + outer_measure M f (s - x)"
  proof -
    have "outer_measure M f s = outer_measure M f ((s \ x) \ (s - x))"
      by (metis Un_Diff_Int Un_commute)
    also have "... \ outer_measure M f (s \ x) + outer_measure M f (s - x)"
      apply (rule subadditiveD)
      apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow])
      apply (simp add: positive_def outer_measure_empty[OF posf])
      apply (rule countably_subadditive_outer_measure)
      using s by (auto intro!: posf inc)
    finally show ?thesis .
  qed
  ultimately
  show "outer_measure M f (s \ x) + outer_measure M f (s - x) = outer_measure M f s"
    by (rule order_antisym)
qed

lemma measure_down: "measure_space \ N \ \ sigma_algebra \ M \ M \ N \ measure_space \ M \"
  by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq)

subsection \<open>Caratheodory's theorem\<close>

theorem (in ring_of_sets) caratheodory':
  assumes posf: "positive M f" and ca: "countably_additive M f"
  shows "\\ :: 'a set \ ennreal. (\s \ M. \ s = f s) \ measure_space \ (sigma_sets \ M) \"
proof -
  have inc: "increasing M f"
    by (metis additive_increasing ca countably_additive_additive posf)
  let ?O = "outer_measure M f"
  define ls where "ls = lambda_system \ (Pow \) ?O"
  have mls: "measure_space \ ls ?O"
    using sigma_algebra.caratheodory_lemma
            [OF sigma_algebra_Pow outer_measure_space_outer_measure [OF posf inc]]
    by (simp add: ls_def)
  hence sls: "sigma_algebra \ ls"
    by (simp add: measure_space_def)
  have "M \ ls"
    by (simp add: ls_def)
       (metis ca posf inc countably_additive_additive algebra_subset_lambda_system)
  hence sgs_sb: "sigma_sets (\) (M) \ ls"
    using sigma_algebra.sigma_sets_subset [OF sls, of "M"]
    by simp
  have "measure_space \ (sigma_sets \ M) ?O"
    by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets)
       (simp_all add: sgs_sb space_closed)
  thus ?thesis using outer_measure_agrees [OF posf ca]
    by (intro exI[of _ ?O]) auto
qed

lemma (in ring_of_sets) caratheodory_empty_continuous:
  assumes f: "positive M f" "additive M f" and fin: "\A. A \ M \ f A \ \"
  assumes cont: "\A. range A \ M \ decseq A \ (\i. A i) = {} \ (\i. f (A i)) \ 0"
  shows "\\ :: 'a set \ ennreal. (\s \ M. \ s = f s) \ measure_space \ (sigma_sets \ M) \"
proof (intro caratheodory' empty_continuous_imp_countably_additive f)
  show "\A\M. f A \ \" using fin by auto
qed (rule cont)

subsection \<open>Volumes\<close>

definition\<^marker>\<open>tag important\<close> volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
  "volume M f \
  (f {} = 0) \<and> (\<forall>a\<in>M. 0 \<le> f a) \<and>
  (\<forall>C\<subseteq>M. disjoint C \<longrightarrow> finite C \<longrightarrow> \<Union>C \<in> M \<longrightarrow> f (\<Union>C) = (\<Sum>c\<in>C. f c))"

lemma volumeI:
  assumes "f {} = 0"
  assumes "\a. a \ M \ 0 \ f a"
  assumes "\C. C \ M \ disjoint C \ finite C \ \C \ M \ f (\C) = (\c\C. f c)"
  shows "volume M f"
  using assms by (auto simp: volume_def)

lemma volume_positive:
  "volume M f \ a \ M \ 0 \ f a"
  by (auto simp: volume_def)

lemma volume_empty:
  "volume M f \ f {} = 0"
  by (auto simp: volume_def)

proposition volume_finite_additive:
  assumes "volume M f"
  assumes A: "\i. i \ I \ A i \ M" "disjoint_family_on A I" "finite I" "\(A ` I) \ M"
  shows "f (\(A ` I)) = (\i\I. f (A i))"
proof -
  have "A`I \ M" "disjoint (A`I)" "finite (A`I)" "\(A`I) \ M"
    using A by (auto simp: disjoint_family_on_disjoint_image)
  with \<open>volume M f\<close> have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)"
    unfolding volume_def by blast
  also have "\ = (\i\I. f (A i))"
  proof (subst sum.reindex_nontrivial)
    fix i j assume "i \ I" "j \ I" "i \ j" "A i = A j"
    with \<open>disjoint_family_on A I\<close> have "A i = {}"
      by (auto simp: disjoint_family_on_def)
    then show "f (A i) = 0"
      using volume_empty[OF \<open>volume M f\<close>] by simp
  qed (auto intro: \<open>finite I\<close>)
  finally show "f (\(A ` I)) = (\i\I. f (A i))"
    by simp
qed

lemma (in ring_of_sets) volume_additiveI:
  assumes pos: "\a. a \ M \ 0 \ \ a"
  assumes [simp]: "\ {} = 0"
  assumes add: "\a b. a \ M \ b \ M \ a \ b = {} \ \ (a \ b) = \ a + \ b"
  shows "volume M \"
proof (unfold volume_def, safe)
  fix C assume "finite C" "C \ M" "disjoint C"
  then show "\ (\C) = sum \ C"
  proof (induct C)
    case (insert c C)
    from insert(1,2,4,5) have "\ (\(insert c C)) = \ c + \ (\C)"
      by (auto intro!: add simp: disjoint_def)
    with insert show ?case
      by (simp add: disjoint_def)
  qed simp
qed fact+

proposition (in semiring_of_sets) extend_volume:
  assumes "volume M \"
  shows "\\'. volume generated_ring \' \ (\a\M. \' a = \ a)"
proof -
  let ?R = generated_ring
  have "\a\?R. \m. \C\M. a = \C \ finite C \ disjoint C \ m = (\c\C. \ c)"
    by (auto simp: generated_ring_def)
  from bchoice[OF this] guess \<mu>' .. note \<mu>'_spec = this

  { fix C assume C: "C \ M" "finite C" "disjoint C"
    fix D assume D: "D \ M" "finite D" "disjoint D"
    assume "\C = \D"
    have "(\d\D. \ d) = (\d\D. \c\C. \ (c \ d))"
    proof (intro sum.cong refl)
      fix d assume "d \ D"
      have Un_eq_d: "(\c\C. c \ d) = d"
        using \<open>d \<in> D\<close> \<open>\<Union>C = \<Union>D\<close> by auto
      moreover have "\ (\c\C. c \ d) = (\c\C. \ (c \ d))"
      proof (rule volume_finite_additive)
        { fix c assume "c \ C" then show "c \ d \ M"
            using C D \<open>d \<in> D\<close> by auto }
        show "(\a\C. a \ d) \ M"
          unfolding Un_eq_d using \<open>d \<in> D\<close> D by auto
        show "disjoint_family_on (\a. a \ d) C"
          using \<open>disjoint C\<close> by (auto simp: disjoint_family_on_def disjoint_def)
      qed fact+
      ultimately show "\ d = (\c\C. \ (c \ d))" by simp
    qed }
  note split_sum = this

  { fix C assume C: "C \ M" "finite C" "disjoint C"
    fix D assume D: "D \ M" "finite D" "disjoint D"
    assume "\C = \D"
    with split_sum[OF C D] split_sum[OF D C]
    have "(\d\D. \ d) = (\c\C. \ c)"
      by (simp, subst sum.swap, simp add: ac_simps) }
  note sum_eq = this

  { fix C assume C: "C \ M" "finite C" "disjoint C"
    then have "\C \ ?R" by (auto simp: generated_ring_def)
    with \<mu>'_spec[THEN bspec, of "\<Union>C"]
    obtain D where
      D: "D \ M" "finite D" "disjoint D" "\C = \D" and "\' (\C) = (\d\D. \ d)"
      by auto
    with sum_eq[OF C D] have "\' (\C) = (\c\C. \ c)" by simp }
  note \<mu>' = this

  show ?thesis
  proof (intro exI conjI ring_of_sets.volume_additiveI[OF generating_ring] ballI)
    fix a assume "a \ M" with \'[of "{a}"] show "\' a = \ a"
      by (simp add: disjoint_def)
  next
    fix a assume "a \ ?R" then guess Ca .. note Ca = this
    with \<mu>'[of Ca] \<open>volume M \<mu>\<close>[THEN volume_positive]
    show "0 \ \' a"
      by (auto intro!: sum_nonneg)
  next
    show "\' {} = 0" using \'[of "{}"] by auto
  next
    fix a assume "a \ ?R" then guess Ca .. note Ca = this
    fix b assume "b \ ?R" then guess Cb .. note Cb = this
    assume "a \ b = {}"
    with Ca Cb have "Ca \ Cb \ {{}}" by auto
    then have C_Int_cases: "Ca \ Cb = {{}} \ Ca \ Cb = {}" by auto

    from \<open>a \<inter> b = {}\<close> have "\<mu>' (\<Union>(Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)"
      using Ca Cb by (intro \<mu>') (auto intro!: disjoint_union)
    also have "\ = (\c\Ca \ Cb. \ c) + (\c\Ca \ Cb. \ c)"
      using C_Int_cases volume_empty[OF \<open>volume M \<mu>\<close>] by (elim disjE) simp_all
    also have "\ = (\c\Ca. \ c) + (\c\Cb. \ c)"
      using Ca Cb by (simp add: sum.union_inter)
    also have "\ = \' a + \' b"
      using Ca Cb by (simp add: \<mu>')
    finally show "\' (a \ b) = \' a + \' b"
      using Ca Cb by simp
  qed
qed

subsubsection\<^marker>\<open>tag important\<close> \<open>Caratheodory on semirings\<close>

theorem (in semiring_of_sets) caratheodory:
  assumes pos: "positive M \" and ca: "countably_additive M \"
  shows "\\' :: 'a set \ ennreal. (\s \ M. \' s = \ s) \ measure_space \ (sigma_sets \ M) \'"
proof -
  have "volume M \"
  proof (rule volumeI)
    { fix a assume "a \ M" then show "0 \ \ a"
        using pos unfolding positive_def by auto }
    note p = this

    fix C assume sets_C: "C \ M" "\C \ M" and "disjoint C" "finite C"
    have "\F'. bij_betw F' {..
      by (rule finite_same_card_bij[OF _ \<open>finite C\<close>]) auto
    then guess F' .. note F' = this
    then have F': "C = F' ` {..< card C}" "inj_on F' {..< card C}"
      by (auto simp: bij_betw_def)
    { fix i j assume *: "i < card C" "j < card C" "i \ j"
      with F' have "F' i \<in> C" "F' j \<in> C" "F' i \<noteq> F' j"
        unfolding inj_on_def by auto
      with \<open>disjoint C\<close>[THEN disjointD]
      have "F' i \ F' j = {}"
        by auto }
    note F'_disj = this
    define F where "F i = (if i < card C then F' i else {})" for i
    then have "disjoint_family F"
      using F'_disj by (auto simp: disjoint_family_on_def)
    moreover from F' have "(\i. F i) = \C"
      by (auto simp add: F_def split: if_split_asm cong del: SUP_cong)
    moreover have sets_F: "\i. F i \ M"
      using F' sets_C by (auto simp: F_def)
    moreover note sets_C
    ultimately have "\ (\C) = (\i. \ (F i))"
      using ca[unfolded countably_additive_def, THEN spec, of F] by auto
    also have "\ = (\i (F' i))"
    proof -
      have "(\i. if i \ {..< card C} then \ (F' i) else 0) sums (\i (F' i))"
        by (rule sums_If_finite_set) auto
      also have "(\i. if i \ {..< card C} then \ (F' i) else 0) = (\i. \ (F i))"
        using pos by (auto simp: positive_def F_def)
      finally show "(\i. \ (F i)) = (\i (F' i))"
        by (simp add: sums_iff)
    qed
    also have "\ = (\c\C. \ c)"
      using F'(2) by (subst (2) F') (simp add: sum.reindex)
    finally show "\ (\C) = (\c\C. \ c)" .
  next
    show "\ {} = 0"
      using \<open>positive M \<mu>\<close> by (rule positiveD1)
  qed
  from extend_volume[OF this] obtain \<mu>_r where
    V: "volume generated_ring \_r" "\a. a \ M \ \ a = \_r a"
    by auto

  interpret G: ring_of_sets \<Omega> generated_ring
    by (rule generating_ring)

  have pos: "positive generated_ring \_r"
    using V unfolding positive_def by (auto simp: positive_def intro!: volume_positive volume_empty)

  have "countably_additive generated_ring \_r"
  proof (rule countably_additiveI)
    fix A' :: "nat \ 'a set" assume A': "range A' \ generated_ring" "disjoint_family A'"
      and Un_A: "(\i. A' i) \ generated_ring"

    from generated_ringE[OF Un_A] guess C' . note C' = this

    { fix c assume "c \ C'"
      moreover define A where [abs_def]: "A i = A' i \ c" for i
      ultimately have A: "range A \ generated_ring" "disjoint_family A"
        and Un_A: "(\i. A i) \ generated_ring"
        using A' C'
        by (auto intro!: G.Int G.finite_Union intro: generated_ringI_Basic simp: disjoint_family_on_def)
      from A C' \c \ C'\ have UN_eq: "(\i. A i) = c"
        by (auto simp: A_def)

      have "\i::nat. \f::nat \ 'a set. \_r (A i) = (\j. \_r (f j)) \ disjoint_family f \ \(range f) = A i \ (\j. f j \ M)"
        (is "\i. ?P i")
      proof
        fix i
        from A have Ai: "A i \ generated_ring" by auto
        from generated_ringE[OF this] guess C . note C = this

        have "\F'. bij_betw F' {..
          by (rule finite_same_card_bij[OF _ \<open>finite C\<close>]) auto
        then guess F .. note F = this
        define f where [abs_def]: "f i = (if i < card C then F i else {})" for i
        then have f: "bij_betw f {..< card C} C"
          by (intro bij_betw_cong[THEN iffD1, OF _ F]) auto
        with C have "\j. f j \ M"
          by (auto simp: Pi_iff f_def dest!: bij_betw_imp_funcset)
        moreover
        from f C have d_f: "disjoint_family_on f {..
          by (intro disjoint_image_disjoint_family_on) (auto simp: bij_betw_def)
        then have "disjoint_family f"
          by (auto simp: disjoint_family_on_def f_def)
        moreover
        have Ai_eq: "A i = (\x
          using f C Ai unfolding bij_betw_def by auto
        then have "\(range f) = A i"
          using f by (auto simp add: f_def)
        moreover
        { have "(\j. \_r (f j)) = (\j. if j \ {..< card C} then \_r (f j) else 0)"
            using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
          also have "\ = (\j_r (f j))"
            by (rule sums_If_finite_set[THEN sums_unique, symmetric]) simp
          also have "\ = \_r (A i)"
            using C f[THEN bij_betw_imp_funcset] unfolding Ai_eq
            by (intro volume_finite_additive[OF V(1) _ d_f, symmetric])
               (auto simp: Pi_iff Ai_eq intro: generated_ringI_Basic)
          finally have "\_r (A i) = (\j. \_r (f j))" .. }
        ultimately show "?P i"
          by blast
      qed
      from choice[OF this] guess f .. note f = this
      then have UN_f_eq: "(\i. case_prod f (prod_decode i)) = (\i. A i)"
        unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff)

      have d: "disjoint_family (\i. case_prod f (prod_decode i))"
        unfolding disjoint_family_on_def
      proof (intro ballI impI)
        fix m n :: nat assume "m \ n"
        then have neq: "prod_decode m \ prod_decode n"
          using inj_prod_decode[of UNIV] by (auto simp: inj_on_def)
        show "case_prod f (prod_decode m) \ case_prod f (prod_decode n) = {}"
        proof cases
          assume "fst (prod_decode m) = fst (prod_decode n)"
          then show ?thesis
            using neq f by (fastforce simp: disjoint_family_on_def)
        next
          assume neq: "fst (prod_decode m) \ fst (prod_decode n)"
          have "case_prod f (prod_decode m) \ A (fst (prod_decode m))"
            "case_prod f (prod_decode n) \ A (fst (prod_decode n))"
            using f[THEN spec, of "fst (prod_decode m)"]
            using f[THEN spec, of "fst (prod_decode n)"]
            by (auto simp: set_eq_iff)
          with f A neq show ?thesis
            by (fastforce simp: disjoint_family_on_def subset_eq set_eq_iff)
        qed
      qed
      from f have "(\n. \_r (A n)) = (\n. \_r (case_prod f (prod_decode n)))"
        by (intro suminf_ennreal_2dimen[symmetric] generated_ringI_Basic)
         (auto split: prod.split)
      also have "\ = (\n. \ (case_prod f (prod_decode n)))"
        using f V(2) by (auto intro!: arg_cong[where f=suminf] split: prod.split)
      also have "\ = \ (\i. case_prod f (prod_decode i))"
        using f \<open>c \<in> C'\<close> C'
        by (intro ca[unfolded countably_additive_def, rule_format])
           (auto split: prod.split simp: UN_f_eq d UN_eq)
      finally have "(\n. \_r (A' n \ c)) = \ c"
        using UN_f_eq UN_eq by (simp add: A_def) }
    note eq = this

    have "(\n. \_r (A' n)) = (\n. \c\C'. \_r (A' n \ c))"
      using C' A'
      by (subst volume_finite_additive[symmetric, OF V(1)])
         (auto simp: disjoint_def disjoint_family_on_def
               intro!: G.Int G.finite_Union arg_cong[where f="\X. suminf (\i. \_r (X i))"] ext
               intro: generated_ringI_Basic)
    also have "\ = (\c\C'. \n. \_r (A' n \ c))"
      using C' A'
      by (intro suminf_sum G.Int G.finite_Union) (auto intro: generated_ringI_Basic)
    also have "\ = (\c\C'. \_r c)"
      using eq V C' by (auto intro!: sum.cong)
    also have "\ = \_r (\C')"
      using C' Un_A
      by (subst volume_finite_additive[symmetric, OF V(1)])
         (auto simp: disjoint_family_on_def disjoint_def
               intro: generated_ringI_Basic)
    finally show "(\n. \_r (A' n)) = \_r (\i. A' i)"
      using C' by simp
  qed
  from G.caratheodory'[OF \positive generated_ring \_r\ \countably_additive generated_ring \_r\]
  guess \<mu>' ..
  with V show ?thesis
    unfolding sigma_sets_generated_ring_eq
    by (intro exI[of _ \<mu>']) (auto intro: generated_ringI_Basic)
qed

lemma extend_measure_caratheodory:
  fixes G :: "'i \ 'a set"
  assumes M: "M = extend_measure \ I G \"
  assumes "i \ I"
  assumes "semiring_of_sets \ (G ` I)"
  assumes empty: "\i. i \ I \ G i = {} \ \ i = 0"
  assumes inj: "\i j. i \ I \ j \ I \ G i = G j \ \ i = \ j"
  assumes nonneg: "\i. i \ I \ 0 \ \ i"
  assumes add: "\A::nat \ 'i. \j. A \ UNIV \ I \ j \ I \ disjoint_family (G \ A) \
    (\<Union>i. G (A i)) = G j \<Longrightarrow> (\<Sum>n. \<mu> (A n)) = \<mu> j"
  shows "emeasure M (G i) = \ i"

proof -
  interpret semiring_of_sets \<Omega> "G ` I"
    by fact
  have "\g\G`I. \i\I. g = G i"
    by auto
  then obtain sel where sel: "\g. g \ G ` I \ sel g \ I" "\g. g \ G ` I \ G (sel g) = g"
    by metis

  have "\\'. (\s\G ` I. \' s = \ (sel s)) \ measure_space \ (sigma_sets \ (G ` I)) \'"
  proof (rule caratheodory)
    show "positive (G ` I) (\s. \ (sel s))"
      by (auto simp: positive_def intro!: empty sel nonneg)
    show "countably_additive (G ` I) (\s. \ (sel s))"
    proof (rule countably_additiveI)
      fix A :: "nat \ 'a set" assume "range A \ G ` I" "disjoint_family A" "(\i. A i) \ G ` I"
      then show "(\i. \ (sel (A i))) = \ (sel (\i. A i))"
        by (intro add) (auto simp: sel image_subset_iff_funcset comp_def Pi_iff intro!: sel)
    qed
  qed
  then obtain \<mu>' where \<mu>': "\<forall>s\<in>G ` I. \<mu>' s = \<mu> (sel s)" "measure_space \<Omega> (sigma_sets \<Omega> (G ` I)) \<mu>'"
    by metis

  show ?thesis
  proof (rule emeasure_extend_measure[OF M])
    { fix i assume "i \ I" then show "\' (G i) = \ i"
      using \<mu>' by (auto intro!: inj sel) }
    show "G ` I \ Pow \"
      by (rule space_closed)
    then show "positive (sets M) \'" "countably_additive (sets M) \'"
      using \<mu>' by (simp_all add: M sets_extend_measure measure_space_def)
  qed fact
qed

proposition extend_measure_caratheodory_pair:
  fixes G :: "'i \ 'j \ 'a set"
  assumes M: "M = extend_measure \ {(a, b). P a b} (\(a, b). G a b) (\(a, b). \ a b)"
  assumes "P i j"
  assumes semiring: "semiring_of_sets \ {G a b | a b. P a b}"
  assumes empty: "\i j. P i j \ G i j = {} \ \ i j = 0"
  assumes inj: "\i j k l. P i j \ P k l \ G i j = G k l \ \ i j = \ k l"
  assumes nonneg: "\i j. P i j \ 0 \ \ i j"
  assumes add: "\A::nat \ 'i. \B::nat \ 'j. \j k.
    (\<And>n. P (A n) (B n)) \<Longrightarrow> P j k \<Longrightarrow> disjoint_family (\<lambda>n. G (A n) (B n)) \<Longrightarrow>
    (\<Union>i. G (A i) (B i)) = G j k \<Longrightarrow> (\<Sum>n. \<mu> (A n) (B n)) = \<mu> j k"
  shows "emeasure M (G i j) = \ i j"
proof -
  have "emeasure M ((\(a, b). G a b) (i, j)) = (\(a, b). \ a b) (i, j)"
  proof (rule extend_measure_caratheodory[OF M])
    show "semiring_of_sets \ ((\(a, b). G a b) ` {(a, b). P a b})"
      using semiring by (simp add: image_def conj_commute)
  next
    fix A :: "nat \ ('i \ 'j)" and j assume "A \ UNIV \ {(a, b). P a b}" "j \ {(a, b). P a b}"
      "disjoint_family ((\(a, b). G a b) \ A)"
      "(\i. case A i of (a, b) \ G a b) = (case j of (a, b) \ G a b)"
    then show "(\n. case A n of (a, b) \ \ a b) = (case j of (a, b) \ \ a b)"
      using add[of "\i. fst (A i)" "\i. snd (A i)" "fst j" "snd j"]
      by (simp add: split_beta' comp_def Pi_iff)
  qed (auto split: prod.splits intro: assms)
  then show ?thesis by simp
qed

end

¤ Dauer der Verarbeitung: 0.49 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.