src/HOL/Probability/Complete_Measure.thy

Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.

(*  Title:      Complete_Measure.thy
    Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
*)
theory Complete_Measure
imports Product_Measure
begin

locale completeable_measure_space = measure_space

definition (in completeable_measure_space) completion :: "'a algebra" where
  "completion = \<lparr> space = space M,
    sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' } \<rparr>"

lemma (in completeable_measure_space) space_completion[simp]:
  "space completion = space M" unfolding completion_def by simp

lemma (in completeable_measure_space) sets_completionE:
  assumes "A \<in> sets completion"
  obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
  using assms unfolding completion_def by auto

lemma (in completeable_measure_space) sets_completionI:
  assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
  shows "A \<in> sets completion"
  using assms unfolding completion_def by auto

lemma (in completeable_measure_space) sets_completionI_sets[intro]:
  "A \<in> sets M \<Longrightarrow> A \<in> sets completion"
  unfolding completion_def by force

lemma (in completeable_measure_space) null_sets_completion:
  assumes "N' \<in> null_sets" "N \<subseteq> N'" shows "N \<in> sets completion"
  apply(rule sets_completionI[of N "{}" N N'])
  using assms by auto

sublocale completeable_measure_space \<subseteq> completion!: sigma_algebra completion
proof (unfold sigma_algebra_iff2, safe)
  fix A x assume "A \<in> sets completion" "x \<in> A"
  with sets_into_space show "x \<in> space completion"
    by (auto elim!: sets_completionE)
next
  fix A assume "A \<in> sets completion"
  from this[THEN sets_completionE] guess S N N' . note A = this
  let ?C = "space completion"
  show "?C - A \<in> sets completion" using A
    by (intro sets_completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"])
       auto
next
  fix A ::"nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion"
  then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N'"
    unfolding completion_def by (auto simp: image_subset_iff)
  from choice[OF this] guess S ..
  from choice[OF this] guess N ..
  from choice[OF this] guess N' ..
  then show "UNION UNIV A \<in> sets completion"
    using null_sets_UN[of N']
    by (intro sets_completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"])
       auto
qed auto

definition (in completeable_measure_space)
  "split_completion A p = (\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and>
    fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets)"

definition (in completeable_measure_space)
  "main_part A = fst (Eps (split_completion A))"

definition (in completeable_measure_space)
  "null_part A = snd (Eps (split_completion A))"

lemma (in completeable_measure_space) split_completion:
  assumes "A \<in> sets completion"
  shows "split_completion A (main_part A, null_part A)"
  unfolding main_part_def null_part_def
proof (rule someI2_ex)
  from assms[THEN sets_completionE] guess S N N' . note A = this
  let ?P = "(S, N - S)"
  show "\<exists>p. split_completion A p"
    unfolding split_completion_def using A
  proof (intro exI conjI)
    show "A = fst ?P \<union> snd ?P" using A by auto
    show "snd ?P \<subseteq> N'" using A by auto
  qed auto
qed auto

lemma (in completeable_measure_space)
  assumes "S \<in> sets completion"
  shows main_part_sets[intro, simp]: "main_part S \<in> sets M"
    and main_part_null_part_Un[simp]: "main_part S \<union> null_part S = S"
    and main_part_null_part_Int[simp]: "main_part S \<inter> null_part S = {}"
  using split_completion[OF assms] by (auto simp: split_completion_def)

lemma (in completeable_measure_space) null_part:
  assumes "S \<in> sets completion" shows "\<exists>N. N\<in>null_sets \<and> null_part S \<subseteq> N"
  using split_completion[OF assms] by (auto simp: split_completion_def)

lemma (in completeable_measure_space) null_part_sets[intro, simp]:
  assumes "S \<in> sets M" shows "null_part S \<in> sets M" "\<mu> (null_part S) = 0"
proof -
  have S: "S \<in> sets completion" using assms by auto
  have "S - main_part S \<in> sets M" using assms by auto
  moreover
  from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
  have "S - main_part S = null_part S" by auto
  ultimately show sets: "null_part S \<in> sets M" by auto
  from null_part[OF S] guess N ..
  with measure_eq_0[of N "null_part S"] sets
  show "\<mu> (null_part S) = 0" by auto
qed

definition (in completeable_measure_space) "\<mu>' A = \<mu> (main_part A)"

lemma (in completeable_measure_space) \<mu>'_set[simp]:
  assumes "S \<in> sets M" shows "\<mu>' S = \<mu> S"
proof -
  have S: "S \<in> sets completion" using assms by auto
  then have "\<mu> S = \<mu> (main_part S \<union> null_part S)" by simp
  also have "\<dots> = \<mu> (main_part S)"
    using S assms measure_additive[of "main_part S" "null_part S"]
    by (auto simp: measure_additive)
  finally show ?thesis unfolding \<mu>'_def by simp
qed

lemma (in completeable_measure_space) sets_completionI_sub:
  assumes N: "N' \<in> null_sets" "N \<subseteq> N'"
  shows "N \<in> sets completion"
  using assms by (intro sets_completionI[of _ "{}" N N']) auto

lemma (in completeable_measure_space) \<mu>_main_part_UN:
  fixes S :: "nat \<Rightarrow> 'a set"
  assumes "range S \<subseteq> sets completion"
  shows "\<mu>' (\<Union>i. (S i)) = \<mu> (\<Union>i. main_part (S i))"
proof -
  have S: "\<And>i. S i \<in> sets completion" using assms by auto
  then have UN: "(\<Union>i. S i) \<in> sets completion" by auto
  have "\<forall>i. \<exists>N. N \<in> null_sets \<and> null_part (S i) \<subseteq> N"
    using null_part[OF S] by auto
  from choice[OF this] guess N .. note N = this
  then have UN_N: "(\<Union>i. N i) \<in> null_sets" by (intro null_sets_UN) auto
  have "(\<Union>i. S i) \<in> sets completion" using S by auto
  from null_part[OF this] guess N' .. note N' = this
  let ?N = "(\<Union>i. N i) \<union> N'"
  have null_set: "?N \<in> null_sets" using N' UN_N by (intro null_sets_Un) auto
  have "main_part (\<Union>i. S i) \<union> ?N = (main_part (\<Union>i. S i) \<union> null_part (\<Union>i. S i)) \<union> ?N"
    using N' by auto
  also have "\<dots> = (\<Union>i. main_part (S i) \<union> null_part (S i)) \<union> ?N"
    unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto
  also have "\<dots> = (\<Union>i. main_part (S i)) \<union> ?N"
    using N by auto
  finally have *: "main_part (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part (S i)) \<union> ?N" .
  have "\<mu> (main_part (\<Union>i. S i)) = \<mu> (main_part (\<Union>i. S i) \<union> ?N)"
    using null_set UN by (intro measure_Un_null_set[symmetric]) auto
  also have "\<dots> = \<mu> ((\<Union>i. main_part (S i)) \<union> ?N)"
    unfolding * ..
  also have "\<dots> = \<mu> (\<Union>i. main_part (S i))"
    using null_set S by (intro measure_Un_null_set) auto
  finally show ?thesis unfolding \<mu>'_def .
qed

lemma (in completeable_measure_space) \<mu>_main_part_Un:
  assumes S: "S \<in> sets completion" and T: "T \<in> sets completion"
  shows "\<mu>' (S \<union> T) = \<mu> (main_part S \<union> main_part T)"
proof -
  have UN: "(\<Union>i. binary (main_part S) (main_part T) i) = (\<Union>i. main_part (binary S T i))"
    unfolding binary_def by (auto split: split_if_asm)
  show ?thesis
    using \<mu>_main_part_UN[of "binary S T"] assms
    unfolding range_binary_eq Un_range_binary UN by auto
qed

sublocale completeable_measure_space \<subseteq> completion!: measure_space completion \<mu>'
proof
  show "\<mu>' {} = 0" by auto
next
  show "countably_additive completion \<mu>'"
  proof (unfold countably_additive_def, intro allI conjI impI)
    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"
    have "disjoint_family (\<lambda>i. main_part (A i))"
    proof (intro disjoint_family_on_bisimulation[OF A(2)])
      fix n m assume "A n \<inter> A m = {}"
      then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"
        using A by (subst (1 2) main_part_null_part_Un) auto
      then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
    qed
    then have "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu> (\<Union>i. main_part (A i))"
      unfolding \<mu>'_def using A by (intro measure_countably_additive) auto
    then show "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu>' (UNION UNIV A)"
      unfolding \<mu>_main_part_UN[OF A(1)] .
  qed
qed

lemma (in sigma_algebra) simple_functionD':
  assumes "simple_function f"
  shows "f -` {x} \<inter> space M \<in> sets M"
proof cases
  assume "x \<in> f`space M" from simple_functionD(2)[OF assms this] show ?thesis .
next
  assume "x \<notin> f`space M" then have "f -` {x} \<inter> space M = {}" by auto
  then show ?thesis by auto
qed

lemma (in sigma_algebra) simple_function_If:
  assumes sf: "simple_function f" "simple_function g" and A: "A \<in> sets M"
  shows "simple_function (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function ?IF")
proof -
  def F \<equiv> "\<lambda>x. f -` {x} \<inter> space M" and G \<equiv> "\<lambda>x. g -` {x} \<inter> space M"
  show ?thesis unfolding simple_function_def
  proof safe
    have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto
    from finite_subset[OF this] assms
    show "finite (?IF ` space M)" unfolding simple_function_def by auto
  next
    fix x assume "x \<in> space M"
    then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A
      then ((F (f x) \<inter> A) \<union> (G (f x) - (G (f x) \<inter> A)))
      else ((F (g x) \<inter> A) \<union> (G (g x) - (G (g x) \<inter> A))))"
      using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
    have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"
      unfolding F_def G_def using sf[THEN simple_functionD'] by auto
    show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto
  qed
qed

lemma (in measure_space) null_sets_finite_UN:
  assumes "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> null_sets"
  shows "(\<Union>i\<in>S. A i) \<in> null_sets"
proof (intro CollectI conjI)
  show "(\<Union>i\<in>S. A i) \<in> sets M" using assms by (intro finite_UN) auto
  have "\<mu> (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. \<mu> (A i))"
    using assms by (intro measure_finitely_subadditive) auto
  then show "\<mu> (\<Union>i\<in>S. A i) = 0"
    using assms by auto
qed

lemma (in completeable_measure_space) completion_ex_simple_function:
  assumes f: "completion.simple_function f"
  shows "\<exists>f'. simple_function f' \<and> (AE x. f x = f' x)"
proof -
  let "?F x" = "f -` {x} \<inter> space M"
  have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
    using completion.simple_functionD'[OF f]
      completion.simple_functionD[OF f] by simp_all
  have "\<forall>x. \<exists>N. N \<in> null_sets \<and> null_part (?F x) \<subseteq> N"
    using F null_part by auto
  from choice[OF this] obtain N where
    N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
  let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
  have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto
  show ?thesis unfolding simple_function_def
  proof (safe intro!: exI[of _ ?f'])
    have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
    from finite_subset[OF this] completion.simple_functionD(1)[OF f]
    show "finite (?f' ` space M)" by auto
  next
    fix x assume "x \<in> space M"
    have "?f' -` {?f' x} \<inter> space M =
      (if x \<in> ?N then ?F undefined \<union> ?N
       else if f x = undefined then ?F (f x) \<union> ?N
       else ?F (f x) - ?N)"
      using N(2) sets_into_space by (auto split: split_if_asm)
    moreover { fix y have "?F y \<union> ?N \<in> sets M"
      proof cases
        assume y: "y \<in> f`space M"
        have "?F y \<union> ?N = (main_part (?F y) \<union> null_part (?F y)) \<union> ?N"
          using main_part_null_part_Un[OF F] by auto
        also have "\<dots> = main_part (?F y) \<union> ?N"
          using y N by auto
        finally show ?thesis
          using F sets by auto
      next
        assume "y \<notin> f`space M" then have "?F y = {}" by auto
        then show ?thesis using sets by auto
      qed }
    moreover {
      have "?F (f x) - ?N = main_part (?F (f x)) \<union> null_part (?F (f x)) - ?N"
        using main_part_null_part_Un[OF F] by auto
      also have "\<dots> = main_part (?F (f x)) - ?N"
        using N `x \<in> space M` by auto
      finally have "?F (f x) - ?N \<in> sets M"
        using F sets by auto }
    ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto
  next
    show "AE x. f x = ?f' x"
      by (rule AE_I', rule sets) auto
  qed
qed

lemma (in completeable_measure_space) completion_ex_borel_measurable:
  fixes g :: "'a \<Rightarrow> pinfreal"
  assumes g: "g \<in> borel_measurable completion"
  shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
proof -
  from g[THEN completion.borel_measurable_implies_simple_function_sequence]
  obtain f where "\<And>i. completion.simple_function (f i)" "f \<up> g" by auto
  then have "\<forall>i. \<exists>f'. simple_function f' \<and> (AE x. f i x = f' x)"
    using completion_ex_simple_function by auto
  from this[THEN choice] obtain f' where
    sf: "\<And>i. simple_function (f' i)" and
    AE: "\<forall>i. AE x. f i x = f' i x" by auto
  show ?thesis
  proof (intro bexI)
    from AE[unfolded all_AE_countable]
    show "AE x. g x = (SUP i. f' i) x" (is "AE x. g x = ?f x")
    proof (rule AE_mp, safe intro!: AE_cong)
      fix x assume eq: "\<forall>i. f i x = f' i x"
      have "g x = (SUP i. f i x)"
        using `f \<up> g` unfolding isoton_def SUPR_fun_expand by auto
      then show "g x = ?f x"
        using eq unfolding SUPR_fun_expand by auto
    qed
    show "?f \<in> borel_measurable M"
      using sf by (auto intro!: borel_measurable_SUP
        intro: borel_measurable_simple_function)
  qed
qed

end