Theory Complete_Measure

theory Complete_Measure
imports Probability_Measure
(*  Title:      HOL/Probability/Complete_Measure.thy
    Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
*)

theory Complete_Measure
  imports Bochner_Integration Probability_Measure
begin

definition
  "split_completion M A p = (if A ∈ sets M then p = (A, {}) else
   ∃N'. A = fst p ∪ snd p ∧ fst p ∩ snd p = {} ∧ fst p ∈ sets M ∧ snd p ⊆ N' ∧ N' ∈ null_sets M)"

definition
  "main_part M A = fst (Eps (split_completion M A))"

definition
  "null_part M A = snd (Eps (split_completion M A))"

definition completion :: "'a measure ⇒ 'a measure" where
  "completion M = measure_of (space M) { S ∪ N |S N N'. S ∈ sets M ∧ N' ∈ null_sets M ∧ N ⊆ N' }
    (emeasure M ∘ main_part M)"

lemma completion_into_space:
  "{ S ∪ N |S N N'. S ∈ sets M ∧ N' ∈ null_sets M ∧ N ⊆ N' } ⊆ Pow (space M)"
  using sets.sets_into_space by auto

lemma space_completion[simp]: "space (completion M) = space M"
  unfolding completion_def using space_measure_of[OF completion_into_space] by simp

lemma completionI:
  assumes "A = S ∪ N" "N ⊆ N'" "N' ∈ null_sets M" "S ∈ sets M"
  shows "A ∈ { S ∪ N |S N N'. S ∈ sets M ∧ N' ∈ null_sets M ∧ N ⊆ N' }"
  using assms by auto

lemma completionE:
  assumes "A ∈ { S ∪ N |S N N'. S ∈ sets M ∧ N' ∈ null_sets M ∧ N ⊆ N' }"
  obtains S N N' where "A = S ∪ N" "N ⊆ N'" "N' ∈ null_sets M" "S ∈ sets M"
  using assms by auto

lemma sigma_algebra_completion:
  "sigma_algebra (space M) { S ∪ N |S N N'. S ∈ sets M ∧ N' ∈ null_sets M ∧ N ⊆ N' }"
    (is "sigma_algebra _ ?A")
  unfolding sigma_algebra_iff2
proof (intro conjI ballI allI impI)
  show "?A ⊆ Pow (space M)"
    using sets.sets_into_space by auto
next
  show "{} ∈ ?A" by auto
next
  let ?C = "space M"
  fix A assume "A ∈ ?A" from completionE[OF this] guess S N N' .
  then show "space M - A ∈ ?A"
    by (intro completionI[of _ "(?C - S) ∩ (?C - N')" "(?C - S) ∩ N' ∩ (?C - N)"]) auto
next
  fix A :: "nat ⇒ 'a set" assume A: "range A ⊆ ?A"
  then have "∀n. ∃S N N'. A n = S ∪ N ∧ S ∈ sets M ∧ N' ∈ null_sets M ∧ N ⊆ N'"
    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 ∈ ?A"
    using null_sets_UN[of N']
    by (intro completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"]) auto
qed

lemma sets_completion:
  "sets (completion M) = { S ∪ N |S N N'. S ∈ sets M ∧ N' ∈ null_sets M ∧ N ⊆ N' }"
  using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_completion] by (simp add: completion_def)

lemma sets_completionE:
  assumes "A ∈ sets (completion M)"
  obtains S N N' where "A = S ∪ N" "N ⊆ N'" "N' ∈ null_sets M" "S ∈ sets M"
  using assms unfolding sets_completion by auto

lemma sets_completionI:
  assumes "A = S ∪ N" "N ⊆ N'" "N' ∈ null_sets M" "S ∈ sets M"
  shows "A ∈ sets (completion M)"
  using assms unfolding sets_completion by auto

lemma sets_completionI_sets[intro, simp]:
  "A ∈ sets M ⟹ A ∈ sets (completion M)"
  unfolding sets_completion by force

lemma null_sets_completion:
  assumes "N' ∈ null_sets M" "N ⊆ N'" shows "N ∈ sets (completion M)"
  using assms by (intro sets_completionI[of N "{}" N N']) auto

lemma split_completion:
  assumes "A ∈ sets (completion M)"
  shows "split_completion M A (main_part M A, null_part M A)"
proof cases
  assume "A ∈ sets M" then show ?thesis
    by (simp add: split_completion_def[abs_def] main_part_def null_part_def)
next
  assume nA: "A ∉ sets M"
  show ?thesis
    unfolding main_part_def null_part_def if_not_P[OF nA]
  proof (rule someI2_ex)
    from assms[THEN sets_completionE] guess S N N' . note A = this
    let ?P = "(S, N - S)"
    show "∃p. split_completion M A p"
      unfolding split_completion_def if_not_P[OF nA] using A
    proof (intro exI conjI)
      show "A = fst ?P ∪ snd ?P" using A by auto
      show "snd ?P ⊆ N'" using A by auto
   qed auto
  qed auto
qed

lemma
  assumes "S ∈ sets (completion M)"
  shows main_part_sets[intro, simp]: "main_part M S ∈ sets M"
    and main_part_null_part_Un[simp]: "main_part M S ∪ null_part M S = S"
    and main_part_null_part_Int[simp]: "main_part M S ∩ null_part M S = {}"
  using split_completion[OF assms]
  by (auto simp: split_completion_def split: if_split_asm)

lemma main_part[simp]: "S ∈ sets M ⟹ main_part M S = S"
  using split_completion[of S M]
  by (auto simp: split_completion_def split: if_split_asm)

lemma null_part:
  assumes "S ∈ sets (completion M)" shows "∃N. N∈null_sets M ∧ null_part M S ⊆ N"
  using split_completion[OF assms] by (auto simp: split_completion_def split: if_split_asm)

lemma null_part_sets[intro, simp]:
  assumes "S ∈ sets M" shows "null_part M S ∈ sets M" "emeasure M (null_part M S) = 0"
proof -
  have S: "S ∈ sets (completion M)" using assms by auto
  have "S - main_part M S ∈ 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 M S = null_part M S" by auto
  ultimately show sets: "null_part M S ∈ sets M" by auto
  from null_part[OF S] guess N ..
  with emeasure_eq_0[of N _ "null_part M S"] sets
  show "emeasure M (null_part M S) = 0" by auto
qed

lemma emeasure_main_part_UN:
  fixes S :: "nat ⇒ 'a set"
  assumes "range S ⊆ sets (completion M)"
  shows "emeasure M (main_part M (⋃i. (S i))) = emeasure M (⋃i. main_part M (S i))"
proof -
  have S: "⋀i. S i ∈ sets (completion M)" using assms by auto
  then have UN: "(⋃i. S i) ∈ sets (completion M)" by auto
  have "∀i. ∃N. N ∈ null_sets M ∧ null_part M (S i) ⊆ N"
    using null_part[OF S] by auto
  from choice[OF this] guess N .. note N = this
  then have UN_N: "(⋃i. N i) ∈ null_sets M" by (intro null_sets_UN) auto
  have "(⋃i. S i) ∈ sets (completion M)" using S by auto
  from null_part[OF this] guess N' .. note N' = this
  let ?N = "(⋃i. N i) ∪ N'"
  have null_set: "?N ∈ null_sets M" using N' UN_N by (intro null_sets.Un) auto
  have "main_part M (⋃i. S i) ∪ ?N = (main_part M (⋃i. S i) ∪ null_part M (⋃i. S i)) ∪ ?N"
    using N' by auto
  also have "… = (⋃i. main_part M (S i) ∪ null_part M (S i)) ∪ ?N"
    unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto
  also have "… = (⋃i. main_part M (S i)) ∪ ?N"
    using N by auto
  finally have *: "main_part M (⋃i. S i) ∪ ?N = (⋃i. main_part M (S i)) ∪ ?N" .
  have "emeasure M (main_part M (⋃i. S i)) = emeasure M (main_part M (⋃i. S i) ∪ ?N)"
    using null_set UN by (intro emeasure_Un_null_set[symmetric]) auto
  also have "… = emeasure M ((⋃i. main_part M (S i)) ∪ ?N)"
    unfolding * ..
  also have "… = emeasure M (⋃i. main_part M (S i))"
    using null_set S by (intro emeasure_Un_null_set) auto
  finally show ?thesis .
qed

lemma emeasure_completion[simp]:
  assumes S: "S ∈ sets (completion M)" shows "emeasure (completion M) S = emeasure M (main_part M S)"
proof (subst emeasure_measure_of[OF completion_def completion_into_space])
  let  = "emeasure M ∘ main_part M"
  show "S ∈ sets (completion M)" "?μ S = emeasure M (main_part M S) " using S by simp_all
  show "positive (sets (completion M)) ?μ"
    by (simp add: positive_def)
  show "countably_additive (sets (completion M)) ?μ"
  proof (intro countably_additiveI)
    fix A :: "nat ⇒ 'a set" assume A: "range A ⊆ sets (completion M)" "disjoint_family A"
    have "disjoint_family (λi. main_part M (A i))"
    proof (intro disjoint_family_on_bisimulation[OF A(2)])
      fix n m assume "A n ∩ A m = {}"
      then have "(main_part M (A n) ∪ null_part M (A n)) ∩ (main_part M (A m) ∪ null_part M (A m)) = {}"
        using A by (subst (1 2) main_part_null_part_Un) auto
      then show "main_part M (A n) ∩ main_part M (A m) = {}" by auto
    qed
    then have "(∑n. emeasure M (main_part M (A n))) = emeasure M (⋃i. main_part M (A i))"
      using A by (auto intro!: suminf_emeasure)
    then show "(∑n. ?μ (A n)) = ?μ (UNION UNIV A)"
      by (simp add: completion_def emeasure_main_part_UN[OF A(1)])
  qed
qed

lemma emeasure_completion_UN:
  "range S ⊆ sets (completion M) ⟹
    emeasure (completion M) (⋃i::nat. (S i)) = emeasure M (⋃i. main_part M (S i))"
  by (subst emeasure_completion) (auto simp add: emeasure_main_part_UN)

lemma emeasure_completion_Un:
  assumes S: "S ∈ sets (completion M)" and T: "T ∈ sets (completion M)"
  shows "emeasure (completion M) (S ∪ T) = emeasure M (main_part M S ∪ main_part M T)"
proof (subst emeasure_completion)
  have UN: "(⋃i. binary (main_part M S) (main_part M T) i) = (⋃i. main_part M (binary S T i))"
    unfolding binary_def by (auto split: if_split_asm)
  show "emeasure M (main_part M (S ∪ T)) = emeasure M (main_part M S ∪ main_part M T)"
    using emeasure_main_part_UN[of "binary S T" M] assms
    by (simp add: range_binary_eq, simp add: Un_range_binary UN)
qed (auto intro: S T)

lemma sets_completionI_sub:
  assumes N: "N' ∈ null_sets M" "N ⊆ N'"
  shows "N ∈ sets (completion M)"
  using assms by (intro sets_completionI[of _ "{}" N N']) auto

lemma completion_ex_simple_function:
  assumes f: "simple_function (completion M) f"
  shows "∃f'. simple_function M f' ∧ (AE x in M. f x = f' x)"
proof -
  let ?F = "λx. f -` {x} ∩ space M"
  have F: "⋀x. ?F x ∈ sets (completion M)" and fin: "finite (f`space M)"
    using simple_functionD[OF f] simple_functionD[OF f] by simp_all
  have "∀x. ∃N. N ∈ null_sets M ∧ null_part M (?F x) ⊆ N"
    using F null_part by auto
  from choice[OF this] obtain N where
    N: "⋀x. null_part M (?F x) ⊆ N x" "⋀x. N x ∈ null_sets M" by auto
  let ?N = "⋃x∈f`space M. N x"
  let ?f' = "λx. if x ∈ ?N then undefined else f x"
  have sets: "?N ∈ null_sets M" 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 ⊆ f`space M ∪ {undefined}" by auto
    from finite_subset[OF this] simple_functionD(1)[OF f]
    show "finite (?f' ` space M)" by auto
  next
    fix x assume "x ∈ space M"
    have "?f' -` {?f' x} ∩ space M =
      (if x ∈ ?N then ?F undefined ∪ ?N
       else if f x = undefined then ?F (f x) ∪ ?N
       else ?F (f x) - ?N)"
      using N(2) sets.sets_into_space by (auto split: if_split_asm simp: null_sets_def)
    moreover { fix y have "?F y ∪ ?N ∈ sets M"
      proof cases
        assume y: "y ∈ f`space M"
        have "?F y ∪ ?N = (main_part M (?F y) ∪ null_part M (?F y)) ∪ ?N"
          using main_part_null_part_Un[OF F] by auto
        also have "… = main_part M (?F y) ∪ ?N"
          using y N by auto
        finally show ?thesis
          using F sets by auto
      next
        assume "y ∉ 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 M (?F (f x)) ∪ null_part M (?F (f x)) - ?N"
        using main_part_null_part_Un[OF F] by auto
      also have "… = main_part M (?F (f x)) - ?N"
        using N ‹x ∈ space M› by auto
      finally have "?F (f x) - ?N ∈ sets M"
        using F sets by auto }
    ultimately show "?f' -` {?f' x} ∩ space M ∈ sets M" by auto
  next
    show "AE x in M. f x = ?f' x"
      by (rule AE_I', rule sets) auto
  qed
qed

lemma completion_ex_borel_measurable:
  fixes g :: "'a ⇒ ennreal"
  assumes g: "g ∈ borel_measurable (completion M)"
  shows "∃g'∈borel_measurable M. (AE x in M. g x = g' x)"
proof -
  from g[THEN borel_measurable_implies_simple_function_sequence'] guess f . note f = this
  from this(1)[THEN completion_ex_simple_function]
  have "∀i. ∃f'. simple_function M f' ∧ (AE x in M. f i x = f' x)" ..
  from this[THEN choice] obtain f' where
    sf: "⋀i. simple_function M (f' i)" and
    AE: "∀i. AE x in M. f i x = f' i x" by auto
  show ?thesis
  proof (intro bexI)
    from AE[unfolded AE_all_countable[symmetric]]
    show "AE x in M. g x = (SUP i. f' i x)" (is "AE x in M. g x = ?f x")
    proof (elim AE_mp, safe intro!: AE_I2)
      fix x assume eq: "∀i. f i x = f' i x"
      moreover have "g x = (SUP i. f i x)"
        unfolding f by (auto split: split_max)
      ultimately show "g x = ?f x" by auto
    qed
    show "?f ∈ borel_measurable M"
      using sf[THEN borel_measurable_simple_function] by auto
  qed
qed

lemma (in prob_space) prob_space_completion: "prob_space (completion M)"
  by (rule prob_spaceI) (simp add: emeasure_space_1)

lemma null_sets_completionI: "N ∈ null_sets M ⟹ N ∈ null_sets (completion M)"
  by (auto simp: null_sets_def)

lemma AE_completion: "(AE x in M. P x) ⟹ (AE x in completion M. P x)"
  unfolding eventually_ae_filter by (auto intro: null_sets_completionI)

lemma null_sets_completion_iff: "N ∈ sets M ⟹ N ∈ null_sets (completion M) ⟷ N ∈ null_sets M"
  by (auto simp: null_sets_def)

lemma AE_completion_iff: "{x∈space M. P x} ∈ sets M ⟹ (AE x in M. P x) ⟷ (AE x in completion M. P x)"
  by (simp add: AE_iff_null null_sets_completion_iff)

end