Theory Hahn_Jordan_Decomposition

section ‹Signed measures›

text ‹In this section we define signed measures. These are generalizations of measures that can also 
take negative values but cannot contain both $\infty$ and $-\infty$ in their range.›

subsection ‹Basic definitions›
theory Hahn_Jordan_Decomposition imports 
  "HOL-Probability.Probability" 
  Hahn_Jordan_Prelims
begin

definition signed_measure::"'a measure  ('a set  ereal)  bool" where
  "signed_measure M μ  μ {} = 0  (-  range μ    range μ)  
  (A. range A  sets M  disjoint_family A   (range A)  sets M  
  (λi. μ (A i)) sums μ ( (range A))) 
  (A. range A  sets M  disjoint_family A   (range A)  sets M  
  ¦μ ( (range A))¦ <   summable (λi. real_of_ereal ¦μ (A i)¦))"

lemma signed_measure_empty:
  assumes "signed_measure M μ"
  shows "μ {} = 0" using assms unfolding signed_measure_def by simp

lemma signed_measure_sums:
  assumes "signed_measure M μ"
    and "range A  M"
    and "disjoint_family A"
    and " (range A)  sets M"
  shows "(λi. μ (A i)) sums μ ( (range A))"
  using assms unfolding signed_measure_def by simp

lemma signed_measure_summable:
  assumes "signed_measure M μ"
    and "range A  M"
    and "disjoint_family A"
    and " (range A)  sets M"
    and "¦μ ( (range A))¦ < "
  shows "summable (λi. real_of_ereal ¦μ (A i)¦)"
  using assms unfolding signed_measure_def by simp

lemma signed_measure_inf_sum:
  assumes "signed_measure M μ"
    and "range A  M"
    and "disjoint_family A"
    and " (range A)  sets M"
  shows "(i. μ (A i)) = μ ( (range A))" using sums_unique assms 
    signed_measure_sums by (metis)

lemma signed_measure_abs_convergent:
  assumes "signed_measure M μ"
    and "range A  sets M"
    and "disjoint_family A"
    and " (range A)  sets M"
    and "¦μ ( (range A))¦ < "
  shows "summable (λi. real_of_ereal ¦μ (A i)¦)" using assms 
  unfolding signed_measure_def by simp

lemma signed_measure_additive:
  assumes "signed_measure M μ"
  shows "additive M μ"
proof (auto simp add: additive_def)
  fix x y
  assume x: "x  M" and y: "y  M" and "x  y = {}"
  hence "disjoint_family (binaryset x y)"
    by (auto simp add: disjoint_family_on_def binaryset_def)
  have "(λi. μ ((binaryset x y) i)) sums (μ x + μ y)"  using binaryset_sums 
      signed_measure_empty[of M μ] assms  by simp
  have "range (binaryset x y) = {x, y, {}}" using range_binaryset_eq by simp
  moreover have "{x, y, {}}  M" using x y by auto
  moreover have "xy  sets M" using x y by simp
  moreover have "( (range (binaryset x y))) = x y"
    by (simp add: calculation(1))
  ultimately have "(λi. μ ((binaryset x y) i)) sums μ (x  y)" using assms x y
      signed_measure_empty[of M μ] signed_measure_sums[of M μ]
      disjoint_family (binaryset x y) by (metis) 
  then show "μ (x  y) = μ x + μ y" 
    using (λi. μ ((binaryset x y) i)) sums (μ x + μ y) sums_unique2 by force
qed

lemma signed_measure_add:
  assumes "signed_measure M μ"
    and "a sets M"
    and "b sets M"
    and "a b = {}"
  shows "μ (a b) = μ a + μ b" using additiveD[OF signed_measure_additive] 
    assms by auto

lemma signed_measure_disj_sum:
  shows "finite I  signed_measure M μ  disjoint_family_on A I  
    (i. i  I  A i  sets M)  μ ( i I. A i) = ( i I. μ (A i))"
proof (induct rule:finite_induct)
  case empty
  then show ?case  unfolding signed_measure_def by simp
next
  case (insert x F)
  have "μ ( (A ` insert x F)) = μ (( (A `F))  A x)" 
    by (simp add: Un_commute)
  also have "... = μ ( (A `F)) + μ (A x)"
  proof -
    have "( (A `F))  (A x) = {}" using insert
      by (metis disjoint_family_on_insert inf_commute) 
    moreover have " (A `F)  sets M" using insert by auto
    moreover have "A x  sets M" using insert by simp
    ultimately show ?thesis by (meson insert.prems(1) signed_measure_add)
  qed
  also have "... = ( i F. μ (A i)) + μ (A x)" using insert
    by (metis disjoint_family_on_insert insert_iff)
  also have "... = (iinsert x F. μ (A i))"
    by (simp add: add.commute insert.hyps(1) insert.hyps(2)) 
  finally show ?case .
qed

lemma pos_signed_measure_count_additive:
  assumes "signed_measure M μ"
    and " E  sets M. 0  μ E"
  shows "countably_additive (sets M) (λA. e2ennreal (μ A))" 
  unfolding countably_additive_def
proof (intro allI impI)
  fix A::"nat  'a set"
  assume "range A  sets M"
    and "disjoint_family A"
    and " (range A)  sets M" note Aprops = this
  have eq: "i. μ (A i) = enn2ereal (e2ennreal (μ (A i)))" 
    using assms enn2ereal_e2ennreal Aprops by simp
  have "(λn. in. μ (A i))  μ ( (range A))" using 
      sums_def_le[of "λi. μ (A i)" "μ ( (range A))"] assms 
      signed_measure_sums[of M] Aprops by simp
  hence "((λn. e2ennreal (in. μ (A i)))  
      e2ennreal (μ ( (range A)))) sequentially"
    using tendsto_e2ennrealI[of "(λn. in. μ (A i))" "μ ( (range A))"] 
    by simp
  moreover have "n. e2ennreal (in. μ (A i)) = (in. e2ennreal (μ (A i)))"
    using e2ennreal_finite_sum by (metis enn2ereal_nonneg eq finite_atMost)
  ultimately have "((λn. (in. e2ennreal (μ (A i))))  
    e2ennreal (μ ( (range A)))) sequentially" by simp
  hence "(λi. e2ennreal (μ (A i))) sums e2ennreal (μ ( (range A)))" 
    using sums_def_le[of "λi. e2ennreal (μ (A i))" "e2ennreal (μ ( (range A)))"] 
    by simp
  thus "(i. e2ennreal (μ (A i))) = e2ennreal (μ ( (range A)))" 
    using sums_unique assms by (metis)
qed

lemma signed_measure_minus:
  assumes "signed_measure M μ"
  shows "signed_measure M (λA. - μ A)" unfolding signed_measure_def
proof (intro conjI)
  show "- μ {} = 0" using assms unfolding signed_measure_def by simp
  show "-   range (λA. - μ A)    range (λA. - μ A)" 
  proof (cases "  range μ")
    case True
    hence "-  range μ" using assms unfolding signed_measure_def by simp
    hence "  range (λA. - μ A)"  using ereal_uminus_eq_reorder by blast
    thus "-   range (λA. - μ A)    range (λA. - μ A)" by simp
  next
    case False
    hence "-  range (λA. - μ A)"  using ereal_uminus_eq_reorder 
      by (simp add: image_iff)
    thus "-   range (λA. - μ A)    range (λA. - μ A)" by simp
  qed
  show "A. range A  sets M  disjoint_family A   (range A)  sets M  
    ¦- μ ( (range A))¦ <   summable (λi. real_of_ereal ¦- μ (A i)¦)" 
  proof (intro allI impI)
    fix A::"nat  'a set"
    assume  "range A  sets M" and "disjoint_family A" and " (range A)  sets M"
      and "¦- μ ( (range A))¦ < " 
    thus "summable (λi. real_of_ereal ¦- μ (A i)¦)" using assms 
      unfolding signed_measure_def by simp
  qed
  show "A. range A  sets M  disjoint_family A   (range A)  sets M  
    (λi. - μ (A i)) sums - μ ( (range A))"
  proof -
    {
      fix A::"nat  'a set"
      assume  "range A  sets M" and "disjoint_family A" and 
        " (range A)  sets M" note Aprops = this
      have "-   range (λi. μ (A i))    range (λi. μ (A i))" 
      proof -
        have "range (λi. μ (A i))  range μ" by auto
        thus ?thesis  using assms unfolding signed_measure_def by auto
      qed
      moreover have "(λi. μ (A i)) sums μ ( (range A))" 
        using signed_measure_sums[of M] Aprops assms by simp
      ultimately have "(λi. - μ (A i)) sums - μ ( (range A))" 
        using sums_minus'[of "λi. μ (A i)"] by simp
    }
    thus ?thesis by auto
  qed
qed

locale near_finite_function =
  fixes μ:: "'b set  ereal"
  assumes inf_range: "-   range μ    range μ"

lemma (in near_finite_function) finite_subset:
  assumes "¦μ E¦ < "
    and "A E"
    and "μ E = μ A + μ (E - A)"
  shows "¦μ A¦ < "
proof (cases "  range μ")
  case False
  show ?thesis
  proof (cases "0 < μ A")
    case True
    hence "¦μ A¦ = μ A" by simp
    also have "... < " using False by (metis ereal_less_PInfty rangeI)
    finally show ?thesis .
  next
    case False
    hence "¦μ A¦ = -μ A" using not_less_iff_gr_or_eq by fastforce 
    also have "... = μ (E - A) - μ E"
    proof -
      have "μ E = μ A + μ (E - A)" using assms by simp 
      hence "μ E - μ A = μ (E - A)"
        by (metis abs_ereal_uminus assms(1) calculation ereal_diff_add_inverse 
            ereal_infty_less(2)  ereal_minus(5) ereal_minus_less_iff 
            ereal_minus_less_minus ereal_uminus_uminus less_ereal.simps(2) 
            minus_ereal_def  plus_ereal.simps(3))
      thus ?thesis using assms(1) ereal_add_uminus_conv_diff ereal_eq_minus 
        by auto 
    qed
    also have "...  μ (E - A) + ¦μ E¦"
      by (metis - μ A = μ (E - A) - μ E abs_ereal_less0 abs_ereal_pos 
          ereal_diff_le_self ereal_le_add_mono1 less_eq_ereal_def 
          minus_ereal_def not_le_imp_less)
    also have "... < " using assms   range μ
      by (metis UNIV_I ereal_less_PInfty ereal_plus_eq_PInfty image_eqI) 
    finally show ?thesis .
  qed
next
  case True
  hence "-  range μ" using inf_range by simp
  hence "- < μ A" by (metis ereal_infty_less(2) rangeI) 
  show ?thesis
  proof (cases "μ A < 0")
    case True
    hence "¦μ A¦ = -μ A" using not_less_iff_gr_or_eq by fastforce 
    also have "... < " using - < μ A using ereal_uminus_less_reorder 
      by blast 
    finally show ?thesis .
  next
    case False
    hence "¦μ A¦ = μ A" by simp
    also have "... = μ E - μ (E - A)"
    proof -
      have "μ E = μ A + μ (E - A)" using assms by simp  
      thus "μ A = μ E - μ (E - A)" by (metis add.right_neutral  assms(1)
            add_diff_eq_ereal calculation ereal_diff_add_eq_diff_diff_swap 
            ereal_diff_add_inverse ereal_infty_less(1) ereal_plus_eq_PInfty 
            ereal_x_minus_x)
    qed
    also have "...  ¦μ E¦ - μ (E - A)" 
      by (metis ¦μ A¦ = μ A μ A = μ E - μ (E - A) abs_ereal_ge0 
          abs_ereal_pos abs_ereal_uminus antisym_conv ereal_0_le_uminus_iff 
          ereal_abs_diff ereal_diff_le_mono_left ereal_diff_le_self le_cases 
          less_eq_ereal_def minus_ereal_def) 
    also have "... < " 
    proof -
      have "- < μ (E - A)" using -  range μ 
        by (metis ereal_infty_less(2) rangeI) 
      hence "- μ (E - A) < " using ereal_uminus_less_reorder by blast
      thus ?thesis using assms by (simp add: ereal_minus_eq_PInfty_iff 
            ereal_uminus_eq_reorder)
    qed
    finally show ?thesis .
  qed
qed

locale signed_measure_space=
  fixes M::"'a measure" and μ
  assumes sgn_meas: "signed_measure M μ"

sublocale signed_measure_space  near_finite_function
proof (unfold_locales)
  show "-   range μ    range μ" using sgn_meas 
    unfolding signed_measure_def by simp
qed

context signed_measure_space
begin
lemma signed_measure_finite_subset:
  assumes "E  sets M"
    and "¦μ E¦ < "
    and "A sets M"
    and "A E"
  shows "¦μ A¦ < "
proof (rule finite_subset)
  show "¦μ E¦ < " "A E" using assms by auto
  show "μ E = μ A + μ (E - A)" using assms 
      sgn_meas signed_measure_add[of M μ A "E - A"]
    by (metis Diff_disjoint Diff_partition sets.Diff)
qed

lemma measure_space_e2ennreal :
  assumes "measure_space (space M) (sets M) m  (E  sets M. m E < )  
    (E  sets M. m E  0)"
  shows "E  sets M. e2ennreal (m E) < "
proof 
  fix E
  assume "E  sets M"
  show "e2ennreal (m E) < "
  proof -
    have "m E < " using assms E  sets M
      by blast
    then have "e2ennreal (m E) < " using e2ennreal_less_top
      using m E <  by auto 
    thus ?thesis by simp
  qed
qed

subsection ‹Positive and negative subsets›

text ‹The Hahn decomposition theorem is based on the notions of positive and negative measurable
sets. A measurable set is positive (resp. negative) if all its measurable subsets have a positive
(resp. negative) measure by $\mu$. The decomposition theorem states that any measure space for
a signed measure can be decomposed into a positive and a negative measurable set.›

definition pos_meas_set  where
  "pos_meas_set E  E  sets M  (A  sets M. A  E  0  μ A)"

definition neg_meas_set  where
  "neg_meas_set E  E  sets M  (A  sets M. A  E  μ A  0)"

lemma pos_meas_setI:
  assumes "E  sets M"
    and "A. A  sets M  A  E  0  μ A"
  shows "pos_meas_set E" unfolding pos_meas_set_def using assms by simp

lemma pos_meas_setD1 :
  assumes "pos_meas_set E"
  shows "E  sets M"
  using assms unfolding pos_meas_set_def
  by simp

lemma neg_meas_setD1 :
  assumes "neg_meas_set E"
  shows "E  sets M" using assms unfolding neg_meas_set_def by simp

lemma neg_meas_setI:
  assumes "E  sets M"
    and "A. A  sets M  A  E  μ A  0"
  shows "neg_meas_set E" unfolding neg_meas_set_def using assms by simp

lemma pos_meas_self:
  assumes "pos_meas_set E"
  shows "0  μ E" using assms unfolding pos_meas_set_def by simp

lemma empty_pos_meas_set:
  shows "pos_meas_set {}"
  by (metis bot.extremum_uniqueI eq_iff pos_meas_set_def sets.empty_sets 
      sgn_meas signed_measure_empty)

lemma empty_neg_meas_set:
  shows "neg_meas_set {}"
  by (metis neg_meas_set_def order_refl sets.empty_sets sgn_meas 
      signed_measure_empty subset_empty)

lemma pos_measure_meas:
  assumes "pos_meas_set E"
    and "A E"
    and "A sets M"
  shows "0  μ A" using assms unfolding pos_meas_set_def by simp

lemma pos_meas_subset:
  assumes "pos_meas_set A"
    and "B A"
    and "B sets M"
  shows "pos_meas_set B" using  assms pos_meas_set_def by auto 

lemma neg_meas_subset:
  assumes "neg_meas_set A"
    and "B A"
    and "B sets M"
  shows "neg_meas_set B" using  assms neg_meas_set_def by auto 

lemma pos_meas_set_Union:
  assumes "(i::nat). pos_meas_set (A i)"
    and "i. A i  sets M"
    and "¦μ ( i. A i)¦ < "
  shows "pos_meas_set ( i. A i)"
proof (rule pos_meas_setI)
  show " (range A)  sets M" using sigma_algebra.countable_UN assms by simp
  obtain B where "disjoint_family B" and "((i::nat). B i) = ((i::nat). A i)"
    and "i. B i  sets M" and "i. B i  A i" using disj_Union2 assms by auto 
  fix C
  assume "C  sets M" and "C ( i. A i)"
  hence "C = C  ( i. A i)" by auto
  also have "... = C  ( i. B i)" using (i. B i) = (i. A i) by simp
  also have "... = ( i. C  B i)" by auto
  finally have "C = ( i. C  B i)" .
  hence "μ C = μ ( i. C  B i)" by simp
  also have "... = (i. μ (C  (B i)))"
  proof (rule signed_measure_inf_sum[symmetric])
    show "signed_measure M μ" using sgn_meas by simp
    show "disjoint_family (λi. C  B i)" using disjoint_family B
      by (meson Int_iff disjoint_family_subset subset_iff)
    show "range (λi. C  B i)  sets M" using C sets M i. B i  sets M 
      by auto
    show "(i. C  B i)  sets M" using C = ( i. C  B i) C sets M 
      by simp
  qed
  also have "...  0" 
  proof (rule suminf_nonneg)
    show "n. 0  μ (C  B n)"
    proof -
      fix n
      have "C B n  A n" using i. B i  A i by auto
      moreover have "C  B n  sets M" using C sets M i. B i  sets M 
        by simp
      ultimately show "0  μ (C  B n)" using assms pos_measure_meas[of "A n"] 
        by simp
    qed
    have "summable (λi. real_of_ereal (μ (C  B i)))"
    proof (rule summable_norm_cancel)
      have "n. norm (real_of_ereal (μ (C  B n))) = 
        real_of_ereal ¦μ (C  B n)¦" by simp
      moreover have "summable (λi. real_of_ereal ¦μ (C  B i)¦)"
      proof (rule signed_measure_abs_convergent)
        show "signed_measure M μ" using sgn_meas by simp
        show "range (λi. C  B i)  sets M" using C sets M 
            i. B i  sets M by auto
        show "disjoint_family (λi. C  B i)" using disjoint_family B
          by (meson Int_iff disjoint_family_subset subset_iff)
        show "(i. C  B i)  sets M" using C = ( i. C  B i) C sets M 
          by simp
        have "¦μ C¦ < "
        proof (rule signed_measure_finite_subset)
          show "( i. A i)  sets M" using assms by simp
          show "¦μ ( (range A))¦ < " using assms by simp
          show "C  sets M" using C  sets M .
          show "C   (range A)" using C   (range A) .
        qed
        thus "¦μ (i. C  B i)¦ < " using C = ( i. C  B i) by simp
      qed
      ultimately show "summable (λn. norm (real_of_ereal (μ (C  B n))))" 
        by auto
    qed
    thus "summable (λi. μ (C  B i))" by (simp add: n. 0  μ (C  B n) 
          summable_ereal_pos)
  qed
  finally show "0  μ C" .
qed

lemma pos_meas_set_pos_lim:
  assumes "(i::nat). pos_meas_set (A i)"
    and "i. A i  sets M"
  shows "0  μ ( i. A i)" 
proof -
  obtain B where "disjoint_family B" and "((i::nat). B i) = ((i::nat). A i)"
    and "i. B i  sets M" and "i. B i  A i" using disj_Union2 assms by auto 
  note Bprops = this
  have sums: "(λn. μ (B n)) sums μ (i. B i)" 
  proof (rule signed_measure_sums)
    show "signed_measure M μ" using sgn_meas .
    show "range B  sets M" using Bprops by auto
    show "disjoint_family B" using Bprops by simp
    show " (range B)  sets M" using Bprops by blast
  qed
  hence "summable (λn. μ (B n))" using sums_summable[of "λn. μ (B n)"] by simp
  hence "suminf (λn. μ (B n)) = μ (i. B i)" using sums sums_iff by auto
  thus ?thesis using suminf_nonneg
    by (metis Bprops(2) Bprops(3) Bprops(4) summable (λn. μ (B n)) assms(1) 
        pos_measure_meas)
qed

lemma pos_meas_disj_union:
  assumes "pos_meas_set A"
    and "pos_meas_set B"
    and "A B = {}"
  shows "pos_meas_set (A  B)" unfolding pos_meas_set_def
proof (intro conjI ballI impI)
  show "A B  sets M"
    by (metis assms(1) assms(2) pos_meas_set_def sets.Un)
next
  fix C
  assume "C sets M" and "C A B"
  define DA where "DA = C A"
  define DB where "DB = C B"
  have "DA sets M" using DA_def C  sets M assms(1) pos_meas_set_def 
    by blast
  have "DB sets M" using DB_def C  sets M assms(2) pos_meas_set_def 
    by blast 
  have "DA  DB = {}" unfolding DA_def DB_def using assms by auto
  have "C = DA  DB" unfolding DA_def DB_def using C A B by auto
  have "0  μ DB" using assms unfolding DB_def pos_meas_set_def
    by (metis  DB_def Int_lower2DB  sets M)
  also have "...  μ DA + μ DB" using assms unfolding  pos_meas_set_def
    by (metis DA_def Diff_Diff_Int Diff_subset Int_commute DA  sets M 
        ereal_le_add_self2)
  also have "... = μ C" using signed_measure_add sgn_meas DA  sets M 
      DB  sets M DA  DB = {} C = DA  DB by metis
  finally show "0  μ C" .
qed

lemma pos_meas_set_union:
  assumes "pos_meas_set A"
    and "pos_meas_set B"
  shows "pos_meas_set (A  B)" 
proof -
  define C where "C = B - A"
  have "A C = A B" unfolding C_def by auto
  moreover have "pos_meas_set (A C)" 
  proof (rule pos_meas_disj_union)
    show "pos_meas_set C" unfolding C_def
      by (meson Diff_subset assms(1) assms(2) sets.Diff 
          signed_measure_space.pos_meas_set_def 
          signed_measure_space.pos_meas_subset signed_measure_space_axioms)
    show "pos_meas_set A" using assms by simp
    show "A  C = {}" unfolding C_def by auto
  qed
  ultimately show ?thesis by simp
qed

lemma neg_meas_disj_union:
  assumes "neg_meas_set A"
    and "neg_meas_set B"
    and "A B = {}"
  shows "neg_meas_set (A  B)" unfolding neg_meas_set_def
proof (intro conjI ballI impI)
  show "A B  sets M"
    by (metis assms(1) assms(2) neg_meas_set_def sets.Un)
next
  fix C
  assume "C sets M" and "C A B"
  define DA where "DA = C A"
  define DB where "DB = C B"
  have "DA sets M" using DA_def C  sets M assms(1) neg_meas_set_def 
    by blast
  have "DB sets M" using DB_def C  sets M assms(2) neg_meas_set_def 
    by blast 
  have "DA  DB = {}" unfolding DA_def DB_def using assms by auto
  have "C = DA  DB" unfolding DA_def DB_def using C A B by auto
  have "μ C = μ DA + μ DB" using signed_measure_add sgn_meas DA  sets M 
      DB  sets M DA  DB = {} C = DA  DB by metis
  also have "...  μ DB" using assms unfolding  neg_meas_set_def
    by (metis DA_def Int_lower2 DA  sets M add_decreasing dual_order.refl)
  also have "...  0" using assms unfolding DB_def neg_meas_set_def
    by (metis  DB_def Int_lower2DB  sets M) 
  finally show "μ C  0" .
qed

lemma neg_meas_set_union:
  assumes "neg_meas_set A"
    and "neg_meas_set B"
  shows "neg_meas_set (A  B)" 
proof -
  define C where "C = B - A"
  have "A C = A B" unfolding C_def by auto
  moreover have "neg_meas_set (A C)" 
  proof (rule neg_meas_disj_union)
    show "neg_meas_set C" unfolding C_def
      by (meson Diff_subset assms(1) assms(2) sets.Diff neg_meas_set_def 
          neg_meas_subset signed_measure_space_axioms)
    show "neg_meas_set A" using assms by simp
    show "A  C = {}" unfolding C_def by auto
  qed
  ultimately show ?thesis by simp
qed

lemma neg_meas_self :
  assumes "neg_meas_set E"
  shows "μ E  0" using assms unfolding neg_meas_set_def by simp

lemma pos_meas_set_opp:
  assumes "signed_measure_space.pos_meas_set  M (λ A. - μ A) A"
  shows "neg_meas_set A"
proof - 
  have m_meas_pos : "signed_measure M  (λ A. - μ A)"
    using assms signed_measure_space_def 
    by (simp add: sgn_meas signed_measure_minus)
  thus ?thesis
    by (metis assms ereal_0_le_uminus_iff neg_meas_setI 
        signed_measure_space.intro signed_measure_space.pos_meas_set_def) 
qed

lemma neg_meas_set_opp:
  assumes "signed_measure_space.neg_meas_set M (λ A. - μ A) A"
  shows "pos_meas_set A"
proof -
  have m_meas_neg : "signed_measure M  (λ A. - μ A)"
    using assms signed_measure_space_def 
    by (simp add: sgn_meas signed_measure_minus)
  thus ?thesis
    by (metis assms ereal_uminus_le_0_iff m_meas_neg pos_meas_setI 
        signed_measure_space.intro signed_measure_space.neg_meas_set_def)
qed
end

lemma signed_measure_inter:
  assumes "signed_measure M μ"
    and "A  sets M"
  shows "signed_measure M (λE. μ (E  A))" unfolding signed_measure_def
proof (intro conjI)
  show "μ ({}  A) = 0" using assms(1) signed_measure_empty by auto 
  show "-   range (λE. μ (E  A))    range (λE. μ (E  A))"
  proof (rule ccontr)
    assume "¬ (-   range (λE. μ (E  A))    range (λE. μ (E  A)))"
    hence "-   range (λE. μ (E  A))    range (λE. μ (E  A))" by simp
    hence "-   range μ    range μ" by auto
    thus False using assms unfolding signed_measure_def by simp
  qed
  show "E. range E  sets M  disjoint_family E   (range E)  sets M  
    (λi. μ (E i  A)) sums μ ( (range E)  A)"
  proof (intro allI impI)
    fix E::"nat  'a set"
    assume "range E  sets M" and "disjoint_family E" and " (range E)  sets M" 
    note Eprops = this
    define F where "F = (λi. E i  A)"
    have "(λi. μ (F i)) sums μ ( (range F))" 
    proof (rule signed_measure_sums)
      show "signed_measure M μ" using assms by simp
      show "range F  sets M" using Eprops F_def assms by blast
      show "disjoint_family F" using Eprops F_def assms
        by (metis disjoint_family_subset inf.absorb_iff2 inf_commute 
            inf_right_idem)
      show " (range F)  sets M" using Eprops assms unfolding F_def
        by (simp add: Eprops assms countable_Un_Int(1) sets.Int)
    qed
    moreover have " (range F) = A   (range E)" unfolding F_def by auto   
    ultimately show "(λi. μ (E i  A)) sums μ ( (range E)  A)" 
      unfolding F_def by simp
  qed
  show "E. range E  sets M 
         disjoint_family E 
          (range E)  sets M  ¦μ ( (range E)  A)¦ <   
         summable (λi. real_of_ereal ¦μ (E i  A)¦)"
  proof (intro allI impI)
    fix E::"nat  'a set"
    assume "range E  sets M" and "disjoint_family E" and 
      " (range E)  sets M" and "¦μ ( (range E)  A)¦ < " note Eprops = this
    show "summable (λi. real_of_ereal ¦μ (E i  A)¦)"
    proof (rule signed_measure_summable)
      show "signed_measure M μ" using assms by simp
      show "range (λi. E i  A)  sets M" using Eprops assms by blast
      show "disjoint_family (λi. E i  A)" using Eprops assms 
          disjoint_family_subset inf.absorb_iff2 inf_commute inf_right_idem 
        by fastforce
      show "(i. E i  A)  sets M" using Eprops assms 
        by (simp add: Eprops assms countable_Un_Int(1) sets.Int)
      show "¦μ (i. E i  A)¦ < " using Eprops by auto
    qed
  qed
qed

context signed_measure_space
begin
lemma pos_signed_to_meas_space :
  assumes "pos_meas_set M1"
    and "m1 = (λA. μ (A  M1))"
  shows "measure_space (space M) (sets M) m1" unfolding measure_space_def
proof (intro conjI)
  show "sigma_algebra (space M) (sets M)"
    by (simp add: sets.sigma_algebra_axioms)
  show "positive (sets M) m1" using assms unfolding pos_meas_set_def
    by (metis Sigma_Algebra.positive_def Un_Int_eq(4) 
        e2ennreal_neg neg_meas_self sup_bot_right empty_neg_meas_set)
  show "countably_additive (sets M) m1" 
  proof (rule pos_signed_measure_count_additive)
    show "Esets M. 0  m1 E" by (metis assms inf.cobounded2 
          pos_meas_set_def sets.Int) 
    show "signed_measure M m1" using assms pos_meas_set_def 
        signed_measure_inter[of M μ M1] sgn_meas by blast
  qed
qed

lemma neg_signed_to_meas_space :
  assumes "neg_meas_set M2" 
    and "m2 = (λA. -μ (A  M2))"
  shows "measure_space (space M) (sets M) m2" unfolding measure_space_def
proof (intro conjI)
  show "sigma_algebra (space M) (sets M)"
    by (simp add: sets.sigma_algebra_axioms)
  show "positive (sets M) m2" using assms unfolding neg_meas_set_def
    by (metis Sigma_Algebra.positive_def e2ennreal_neg ereal_uminus_zero 
        inf.absorb_iff2 inf.orderE inf_bot_right neg_meas_self pos_meas_self 
        empty_neg_meas_set empty_pos_meas_set)
  show "countably_additive (sets M) m2" 
  proof (rule pos_signed_measure_count_additive)
    show "Esets M. 0  m2 E"
      by (metis assms ereal_uminus_eq_reorder ereal_uminus_le_0_iff 
          inf.cobounded2 neg_meas_set_def sets.Int) 
    have "signed_measure M (λA. μ (A  M2))" using assms neg_meas_set_def
        signed_measure_inter[of M μ M2] sgn_meas by blast
    thus "signed_measure M m2" using signed_measure_minus assms by simp 
  qed
qed

lemma pos_part_meas_nul_neg_set :
  assumes "pos_meas_set M1" 
    and "neg_meas_set M2" 
    and "m1 = (λA. μ (A  M1))"
    and "E  sets M"
    and "E  M2"
  shows "m1 E = 0"
proof -
  have "m1 E  0" using assms unfolding pos_meas_set_def
    by (simp add: E  sets M sets.Int) 
  have "μ E  0" using E  M2 assms unfolding neg_meas_set_def
    using E  sets M by blast 
  then have "m1 E  0" using μ E  0 assms
    by (metis Int_Un_eq(1) Un_subset_iff E  sets M E  M2 pos_meas_setD1 
        sets.Int signed_measure_space.neg_meas_set_def 
        signed_measure_space_axioms)
  thus "m1 E = 0" using m1 E  0 m1 E  0 by auto
qed

lemma neg_part_meas_nul_pos_set :
  assumes "pos_meas_set M1" 
    and "neg_meas_set M2" 
    and "m2 = (λA. -μ (A  M2))"
    and "E  sets M"
    and "E  M1"
  shows "m2 E = 0"
proof -
  have "m2 E  0" using assms unfolding neg_meas_set_def
    by (simp add: E  sets M sets.Int) 
  have "μ E  0" using  assms unfolding pos_meas_set_def by blast 
  then have "m2 E  0" using μ E  0 assms
    by (metis E  sets M E  M1 ereal_0_le_uminus_iff ereal_uminus_uminus 
        inf_sup_ord(1) neg_meas_setD1 pos_meas_set_def pos_meas_subset 
        sets.Int)
  thus "m2 E = 0" using m2 E  0 m2 E  0 by auto
qed

definition pos_sets where 
  "pos_sets = {A. A  sets M    pos_meas_set A}"

definition pos_img where 
  "pos_img = {μ A|A. A pos_sets}"

subsection ‹Essential uniqueness›

text ‹In this part, under the assumption that a measure space for a signed measure admits a
decomposition into a positive and a negative set, we prove that this decomposition is
essentially unique; in other words, that if two such decompositions $(P,N)$ and $(X,Y)$ exist, 
then any measurable subset of $(P\triangle X) \cup (N \triangle Y)$ has a null measure.›

definition hahn_space_decomp where
  "hahn_space_decomp M1 M2  (pos_meas_set M1)  (neg_meas_set M2)  
(space M = M1  M2)  (M1  M2 = {})"

lemma pos_neg_null_set:
  assumes "pos_meas_set A"
    and "neg_meas_set A"
  shows "μ A = 0" using assms pos_meas_self[of A] neg_meas_self[of A] by simp

lemma pos_diff_neg_meas_set:
  assumes "(pos_meas_set M1)" 
    and "(neg_meas_set N2)" 
    and "(space M = N1  N2)" 
    and "N1  sets M"
  shows "neg_meas_set ((M1 - N1)  space M)" using assms neg_meas_subset
  by (metis Diff_subset_conv Int_lower2 pos_meas_setD1 sets.Diff 
      sets.Int_space_eq2)

lemma neg_diff_pos_meas_set:
  assumes "(neg_meas_set M2)" 
    and "(pos_meas_set N1)" 
    and "(space M = N1  N2)" 
    and "N2  sets M"
  shows "pos_meas_set ((M2 - N2)  space M)" 
proof -
  have "(M2 - N2)  space M  N1" using assms by auto
  thus ?thesis using assms pos_meas_subset neg_meas_setD1 by blast
qed

lemma pos_sym_diff_neg_meas_set:
  assumes "hahn_space_decomp M1 M2"
    and "hahn_space_decomp N1 N2"
  shows "neg_meas_set ((sym_diff M1 N1)  space M)" using assms 
  unfolding hahn_space_decomp_def
  by (metis Int_Un_distrib2 neg_meas_set_union pos_meas_setD1 
      pos_diff_neg_meas_set) 

lemma neg_sym_diff_pos_meas_set:
  assumes "hahn_space_decomp M1 M2"
    and "hahn_space_decomp N1 N2"
  shows "pos_meas_set ((sym_diff M2 N2)  space M)" using assms 
    neg_diff_pos_meas_set unfolding hahn_space_decomp_def
  by (metis (no_types, lifting) Int_Un_distrib2 neg_meas_setD1 
      pos_meas_set_union)

lemma pos_meas_set_diff:
  assumes "pos_meas_set A"
    and "B sets M"
  shows "pos_meas_set ((A - B)  (space M))" using pos_meas_subset
  by (metis Diff_subset assms(1) assms(2) pos_meas_setD1 sets.Diff 
      sets.Int_space_eq2)

lemma pos_meas_set_sym_diff:
  assumes "pos_meas_set A"
    and "pos_meas_set B"
  shows "pos_meas_set ((sym_diff A B)  space M)" using pos_meas_set_diff
  by (metis Int_Un_distrib2 assms(1) assms(2) pos_meas_setD1 
      pos_meas_set_union)

lemma neg_meas_set_diff:
  assumes "neg_meas_set A"
    and "B sets M"
  shows "neg_meas_set ((A - B)  (space M))" using neg_meas_subset
  by (metis Diff_subset assms(1) assms(2) neg_meas_setD1 sets.Diff 
      sets.Int_space_eq2)

lemma neg_meas_set_sym_diff:
  assumes "neg_meas_set A"
    and "neg_meas_set B"
  shows "neg_meas_set ((sym_diff A B)  space M)" using neg_meas_set_diff
  by (metis Int_Un_distrib2 assms(1) assms(2) neg_meas_setD1 
      neg_meas_set_union)

lemma hahn_decomp_space_diff:
  assumes "hahn_space_decomp M1 M2"
    and "hahn_space_decomp N1 N2"
  shows "pos_meas_set ((sym_diff M1 N1  sym_diff M2 N2)  space M)"
    "neg_meas_set ((sym_diff M1 N1  sym_diff M2 N2)  space M)"
proof -
  show "pos_meas_set ((sym_diff M1 N1  sym_diff M2 N2)  space M)"
    by (metis Int_Un_distrib2 assms(1) assms(2) hahn_space_decomp_def 
        neg_sym_diff_pos_meas_set pos_meas_set_sym_diff pos_meas_set_union)
  show "neg_meas_set ((sym_diff M1 N1  sym_diff M2 N2)  space M)"
    by (metis Int_Un_distrib2 assms(1) assms(2) hahn_space_decomp_def 
        neg_meas_set_sym_diff neg_meas_set_union pos_sym_diff_neg_meas_set)
qed

lemma hahn_decomp_ess_unique:
  assumes "hahn_space_decomp M1 M2"
    and "hahn_space_decomp N1 N2"
    and "C  sym_diff M1 N1  sym_diff M2 N2"
    and "C sets M"
  shows "μ C = 0"
proof -
  have "C (sym_diff M1 N1  sym_diff M2 N2)  space M" using assms
    by (simp add: sets.sets_into_space)     
  thus ?thesis using assms hahn_decomp_space_diff pos_neg_null_set
    by (meson neg_meas_subset pos_meas_subset)
qed

section ‹Existence of a positive subset›

text ‹The goal of this part is to prove that any measurable set of finite and positive measure must 
contain a positive subset with a strictly positive measure.›

subsection ‹A sequence of negative subsets›

definition inf_neg where
  "inf_neg A = (if (A  sets M  pos_meas_set A) then (0::nat) 
  else Inf {n|n. (1::nat)  n  (B  sets M. B   A  μ B < ereal(-1/n))})"

lemma inf_neg_ne:
  assumes "A  sets M"
    and "¬ pos_meas_set A"
  shows "{n::nat|n. (1::nat)  n  
  (B  sets M. B   A  μ B < ereal (-1/n))}  {}"  
proof -
  define N where "N = {n::nat|n. (1::nat)  n  
    (B  sets M. B   A  μ B < ereal (-1/n))}"
  have "B  sets M. B A  μ B < 0" using assms unfolding pos_meas_set_def 
    by auto
  from this obtain B where "B sets M" and "B A" and "μ B < 0" by auto
  hence "n::nat. (1::nat)  n  μ B < ereal (-1/n)" 
  proof (cases "μ B = -")
    case True
    hence "μ B < -1/(2::nat)" by simp
    thus ?thesis using numeral_le_real_of_nat_iff one_le_numeral by blast 
  next
    case False
    hence "real_of_ereal (μ B) < 0" using μ B < 0
      by (metis Infty_neq_0(3) ereal_mult_eq_MInfty ereal_zero_mult 
          less_eq_ereal_def less_eq_real_def less_ereal.simps(2) 
          real_of_ereal_eq_0 real_of_ereal_le_0)
    hence "n::nat. Suc 0  n  real_of_ereal (μ B) < -1/n"
    proof -
      define nw where "nw =  Suc (nat (floor (-1/ (real_of_ereal (μ B)))))"
      have "Suc 0  nw" unfolding nw_def by simp
      have "0 < -1/ (real_of_ereal (μ B))" using real_of_ereal (μ B) < 0 
        by simp
      have "-1/ (real_of_ereal (μ B)) < nw" unfolding nw_def by linarith
      hence "1/nw < 1/(-1/ (real_of_ereal (μ B)))" 
        using 0 < -1/ (real_of_ereal (μ B)) by (metis frac_less2 
            le_eq_less_or_eq of_nat_1 of_nat_le_iff zero_less_one)
      also have "... = - (real_of_ereal (μ B))" by simp
      finally have "1/nw < - (real_of_ereal (μ B))" .
      hence "real_of_ereal (μ B) < -1/nw" by simp
      thus ?thesis using Suc 0  nw by auto
    qed
    from this obtain n1::nat where "Suc 0  n1" 
      and "real_of_ereal (μ B) < -1/n1" by auto
    hence "ereal (real_of_ereal (μ B)) < -1/n1" using real_ereal_leq[of "μ B"] 
        μ B < 0 by simp
    moreover have "μ B = real_of_ereal (μ B)" using μ B < 0 False
      by (metis less_ereal.simps(2) real_of_ereal.elims zero_ereal_def)
    ultimately show ?thesis  using Suc 0  n1 by auto 
  qed
  from this obtain n0::nat where "(1::nat)  n0" and "μ B < -1/n0" by auto
  hence "n0  {n::nat|n. (1::nat)  n  
    (B  sets M. B   A  μ B <  ereal(-1/n))}" 
    using B sets M B A by auto
  thus ?thesis by auto
qed

lemma inf_neg_ge_1:
  assumes "A  sets M"
    and "¬ pos_meas_set A"
  shows "(1::nat)  inf_neg A"
proof -
  define N where "N = {n::nat|n. (1::nat)  n  
    (B  sets M. B   A  μ B < ereal (-1/n))}"  
  have "N  {}" unfolding N_def using assms inf_neg_ne by auto
  moreover have "n. n N  (1::nat)  n" unfolding N_def by simp
  ultimately show "1  inf_neg A" unfolding inf_neg_def N_def
    using Inf_nat_def1 assms(1) assms(2) by presburger
qed

lemma inf_neg_pos:
  assumes "A  sets M"
    and "¬ pos_meas_set A"
  shows " B  sets M. B A  μ B < -1/(inf_neg A)"  
proof -
  define N where "N = {n::nat|n. (1::nat)  n  
    (B  sets M. B   A  μ B < ereal (-1/n))}"  
  have "N  {}" unfolding N_def using assms inf_neg_ne by auto
  hence "Inf N  N" using Inf_nat_def1[of N] by simp
  hence "inf_neg A  N" unfolding N_def inf_neg_def using assms by auto
  thus ?thesis unfolding N_def by auto
qed

definition rep_neg where
  "rep_neg A  = (if (A  sets M  pos_meas_set A) then {} else 
  SOME B. B  sets M  B  A  μ B  ereal (-1 / (inf_neg A)))"

lemma g_rep_neg:
  assumes "A sets M"
    and "¬ pos_meas_set A"
  shows "rep_neg A  sets M" "rep_neg A  A"  
    "μ (rep_neg A)  ereal (-1 / (inf_neg A))" 
proof -
  have " B. B  sets M  B A  μ B  -1 / (inf_neg A)" using assms 
      inf_neg_pos[of A] by auto
  from someI_ex[OF this] show "rep_neg A  sets M" "rep_neg A  A"  
    "μ (rep_neg A)  -1 / (inf_neg A)" 
    unfolding rep_neg_def using assms by auto
qed

lemma rep_neg_sets:
  shows "rep_neg A  sets M"
proof (cases "A  sets M  pos_meas_set A")
  case True
  then show ?thesis unfolding rep_neg_def by simp
next
  case False
  then show ?thesis using g_rep_neg(1) by blast
qed

lemma rep_neg_subset:
  shows "rep_neg A  A"
proof (cases "A  sets M  pos_meas_set A")
  case True
  then show ?thesis unfolding rep_neg_def by simp
next
  case False
  then show ?thesis using g_rep_neg(2) by blast
qed

lemma rep_neg_less:
  assumes "A sets M"
    and "¬ pos_meas_set A"
  shows "μ (rep_neg A)  ereal (-1 / (inf_neg A))" using assms g_rep_neg(3) 
  by simp

lemma rep_neg_leq:
  shows "μ (rep_neg A)  0"
proof (cases "A  sets M  pos_meas_set A")
  case True
  hence "rep_neg A = {}" unfolding rep_neg_def by simp
  then show ?thesis using sgn_meas signed_measure_empty by force 
next
  case False
  then show ?thesis using rep_neg_less by (metis le_ereal_le minus_divide_left 
        neg_le_0_iff_le of_nat_0 of_nat_le_iff zero_ereal_def zero_le 
        zero_le_divide_1_iff) 
qed

subsection ‹Construction of the positive subset›

fun pos_wtn
  where
    pos_wtn_base: "pos_wtn E 0 = E"|
    pos_wtn_step: "pos_wtn E (Suc n) = pos_wtn E n - rep_neg (pos_wtn E n)"

lemma pos_wtn_subset:
  shows "pos_wtn E n  E"
proof (induct n)
  case 0
  then show ?case using pos_wtn_base by simp
next
  case (Suc n)
  hence "rep_neg (pos_wtn E n)  pos_wtn E n" using rep_neg_subset by simp
  then show ?case using Suc by auto
qed

lemma pos_wtn_sets:
  assumes "E sets M"
  shows "pos_wtn E n  sets M"
proof (induct n)
  case 0
  then show ?case using assms by simp
next
  case (Suc n)
  then show ?case using pos_wtn_step rep_neg_sets by auto
qed

definition neg_wtn where
  "neg_wtn E (n::nat) = rep_neg (pos_wtn E n)"

lemma neg_wtn_neg_meas:
  shows "μ (neg_wtn E n)  0" unfolding neg_wtn_def using rep_neg_leq by simp

lemma neg_wtn_sets:
  shows "neg_wtn E n  sets M" unfolding neg_wtn_def using rep_neg_sets by simp

lemma neg_wtn_subset:
  shows "neg_wtn E n  E" unfolding neg_wtn_def  
  using pos_wtn_subset[of E n] rep_neg_subset[of "pos_wtn E n"] by simp

lemma neg_wtn_union_subset:
  shows "( i  n. neg_wtn E i)  E" using neg_wtn_subset by auto

lemma pos_wtn_Suc:
  shows "pos_wtn E (Suc n) = E - ( i  n. neg_wtn E i)" unfolding neg_wtn_def
proof (induct n)
  case 0
  then show ?case using pos_wtn_base pos_wtn_step by simp
next
  case (Suc n)
  have "pos_wtn E (Suc (Suc n)) = pos_wtn E (Suc n) - 
    rep_neg (pos_wtn E (Suc n))" 
    using pos_wtn_step by simp
  also have "... = (E - ( i  n. rep_neg (pos_wtn E i))) - 
    rep_neg (pos_wtn E (Suc n))"
    using Suc by simp
  also have "... = E - ( i  (Suc n). rep_neg (pos_wtn E i))" 
    using diff_union[of E "λi. rep_neg (pos_wtn E i)" n] by auto
  finally show "pos_wtn E (Suc (Suc n)) = 
    E - ( i  (Suc n). rep_neg (pos_wtn E i))" .
qed

definition pos_sub where
  "pos_sub E = ( n. pos_wtn E n)"

lemma pos_sub_sets:
  assumes "E sets M"
  shows "pos_sub E  sets M" unfolding pos_sub_def using pos_wtn_sets assms 
  by auto

lemma pos_sub_subset:
  shows "pos_sub E  E" unfolding pos_sub_def using pos_wtn_subset by blast

lemma pos_sub_infty:
  assumes "E  sets M"
    and "¦μ E¦ < "
  shows "¦μ (pos_sub E)¦ < " using signed_measure_finite_subset assms 
    pos_sub_sets pos_sub_subset by simp

lemma neg_wtn_djn:
  shows "disjoint_family (λn. neg_wtn E n)" unfolding disjoint_family_on_def
proof -
  {
    fix n 
    fix m::nat
    assume "n < m"
    hence "p. m = Suc p" using old.nat.exhaust by auto
    from this obtain p where "m = Suc p" by auto
    have "neg_wtn E m  pos_wtn E m" unfolding neg_wtn_def 
      by (simp add: rep_neg_subset)
    also have "... = E - ( i  p. neg_wtn E i)" using pos_wtn_Suc m = Suc p
      by simp
    finally have "neg_wtn E m  E - ( i  p. neg_wtn E i)" .
    moreover have "neg_wtn E n  ( i  p. neg_wtn E i)" using n < m 
        m = Suc p by (simp add: UN_upper) 
    ultimately have "neg_wtn E n  neg_wtn E m = {}" by auto
  }
  thus "mUNIV. nUNIV. m  n  neg_wtn E m  neg_wtn E n = {}"  
    by (metis inf_commute linorder_neqE_nat) 
qed
end

lemma disjoint_family_imp_on:
  assumes "disjoint_family A"
  shows "disjoint_family_on A S" 
  using assms disjoint_family_on_mono subset_UNIV by blast 

context signed_measure_space
begin
lemma neg_wtn_union_neg_meas:
  shows "μ ( i  n. neg_wtn E i)  0" 
proof -
  have "μ ( i  n. neg_wtn E i) = (i{.. n}. μ (neg_wtn E i))" 
  proof (rule signed_measure_disj_sum, simp+)
    show "signed_measure M μ" using sgn_meas .
    show "disjoint_family_on (neg_wtn E) {..n}" using neg_wtn_djn 
        disjoint_family_imp_on[of "neg_wtn E"] by simp
    show "i. i  {..n}  neg_wtn E i  sets M" using neg_wtn_sets by simp
  qed
  also have "...  0" using neg_wtn_neg_meas by (simp add: sum_nonpos) 
  finally show ?thesis .
qed

lemma pos_wtn_meas_gt:
  assumes "0 < μ E"
    and "E sets M"
  shows "0 < μ (pos_wtn E n)"
proof (cases "n = 0")
  case True
  then show ?thesis using assms by simp
next
  case False
  hence "m. n = Suc m" by (simp add: not0_implies_Suc) 
  from this obtain m where "n = Suc m" by auto
  hence eq: "pos_wtn E n = E - ( i  m. neg_wtn E i)" using pos_wtn_Suc 
    by simp
  hence "pos_wtn E n  ( i  m. neg_wtn E i) = {}" by auto
  moreover have "E = pos_wtn E n  ( i  m. neg_wtn E i)" 
    using eq neg_wtn_union_subset[of E m] by auto 
  ultimately have "μ E = μ (pos_wtn E n) + μ ( i  m. neg_wtn E i)" 
    using signed_measure_add[of M μ "pos_wtn E n" " i  m. neg_wtn E i"] 
      pos_wtn_sets neg_wtn_sets assms sgn_meas by auto
  hence "0 < μ (pos_wtn E n) + μ ( i  m. neg_wtn E i)" using assms by simp
  thus ?thesis using neg_wtn_union_neg_meas 
    by (metis add.right_neutral add_mono not_le) 
qed

definition union_wit where
  "union_wit E = ( n. neg_wtn E n)"

lemma union_wit_sets:
  shows "union_wit E  sets M" unfolding union_wit_def
proof (intro sigma_algebra.countable_nat_UN)
  show "sigma_algebra (space M) (sets M)" 
    by (simp add: sets.sigma_algebra_axioms) 
  show "range (neg_wtn E)  sets M"
  proof -
    {
      fix n
      have "neg_wtn E n  sets M" unfolding neg_wtn_def 
        by (simp add: rep_neg_sets)
    }
    thus ?thesis by auto
  qed
qed

lemma union_wit_subset:
  shows "union_wit E  E"
proof -
  {
    fix n
    have "neg_wtn E n  E" unfolding neg_wtn_def using pos_wtn_subset
        rep_neg_subset[of "pos_wtn E n"] by auto
  }
  thus ?thesis unfolding union_wit_def by auto
qed

lemma pos_sub_diff:
  shows "pos_sub E = E - union_wit E"
proof
  show "pos_sub E  E - union_wit E"
  proof -
    have "pos_sub E  E" using pos_sub_subset by simp
    moreover have "pos_sub E  union_wit E = {}" 
    proof (rule ccontr)
      assume "pos_sub E  union_wit E  {}"
      hence " a. a pos_sub E  union_wit E" by auto
      from this obtain a where "a pos_sub E  union_wit E" by auto
      hence "a union_wit E" by simp
      hence "n. a  rep_neg (pos_wtn E n)" unfolding union_wit_def neg_wtn_def
        by auto
      from this obtain n where "a  rep_neg (pos_wtn E n)" by auto
      have "a  pos_wtn E (Suc n)" using a pos_sub E  union_wit E 
        unfolding pos_sub_def by blast
      hence "a rep_neg (pos_wtn E n)" using pos_wtn_step by simp
      thus False using a  rep_neg (pos_wtn E n) by simp
    qed
    ultimately show ?thesis by auto
  qed
next
  show "E - union_wit E  pos_sub E"
  proof
    fix a
    assume "a  E - union_wit E"
    show "a  pos_sub E" unfolding pos_sub_def
    proof
      fix n
      show "a  pos_wtn E n"
      proof (cases "n = 0")
        case True
        thus ?thesis using pos_wtn_base a E - union_wit E by simp
      next
        case False
        hence "m. n = Suc m" by (simp add: not0_implies_Suc) 
        from this obtain m where "n = Suc m" by auto
        have "( i  m. rep_neg (pos_wtn E i))  
          ( n. (rep_neg (pos_wtn E n)))" by auto
        hence "a  E - ( i  m. rep_neg (pos_wtn E i))" 
          using a  E - union_wit E unfolding union_wit_def neg_wtn_def 
          by auto
        thus "a pos_wtn E n" using pos_wtn_Suc n = Suc m 
          unfolding neg_wtn_def by simp
      qed
    qed
  qed
qed

definition num_wtn where
  "num_wtn E n = inf_neg (pos_wtn E n)"

lemma num_wtn_geq:
  shows "μ (neg_wtn E n)  ereal (-1/(num_wtn E n))" 
proof (cases "(pos_wtn E n)  sets M  pos_meas_set (pos_wtn E n)")
  case True
  hence "neg_wtn E n = {}" unfolding neg_wtn_def rep_neg_def by simp
  moreover have "num_wtn E n = 0" using True unfolding num_wtn_def inf_neg_def 
    by simp
  ultimately show ?thesis using sgn_meas signed_measure_empty by force 
next
  case False
  then show ?thesis using g_rep_neg(3)[of "pos_wtn E n"] unfolding neg_wtn_def 
      num_wtn_def by simp
qed

lemma neg_wtn_infty:
  assumes "E  sets M"
    and "¦μ E¦ < "
  shows "¦μ (neg_wtn E i)¦ < "
proof (rule signed_measure_finite_subset)
  show "E  sets M" "¦μ E¦ < " using assms by auto
  show "neg_wtn E i  sets M" 
  proof (cases "pos_wtn E i  sets M  pos_meas_set (pos_wtn E i)")
    case True
    then show ?thesis unfolding neg_wtn_def rep_neg_def by simp
  next
    case False
    then show ?thesis unfolding neg_wtn_def 
      using g_rep_neg(1)[of "pos_wtn E i"] by simp
  qed
  show "neg_wtn E i  E" unfolding neg_wtn_def using pos_wtn_subset[of E] 
      rep_neg_subset[of "pos_wtn E i"] by auto
qed

lemma union_wit_infty:
  assumes "E  sets M"
    and "¦μ E¦ < "
  shows "¦μ (union_wit E)¦ < " using union_wit_subset union_wit_sets 
    signed_measure_finite_subset assms unfolding union_wit_def by simp

lemma neg_wtn_summable:
  assumes "E  sets M"
    and "¦μ E¦ < "
  shows "summable (λi. - real_of_ereal (μ (neg_wtn E i)))"
proof -
  have "signed_measure M μ" using sgn_meas .
  moreover have "range (neg_wtn E)  sets M" unfolding neg_wtn_def 
    using rep_neg_sets by auto
  moreover have "disjoint_family (neg_wtn E)" using neg_wtn_djn by simp
  moreover have " (range (neg_wtn E))  sets M" using union_wit_sets 
    unfolding union_wit_def by simp
  moreover have "¦μ ( (range (neg_wtn E)))¦ < " 
    using union_wit_subset signed_measure_finite_subset union_wit_sets assms
    unfolding union_wit_def by simp
  ultimately have "summable (λi. real_of_ereal ¦μ (neg_wtn E i)¦)" 
    using signed_measure_abs_convergent[of M ] by simp
  moreover have "i. ¦μ (neg_wtn E i)¦ = -(μ (neg_wtn E i))"
  proof -
    fix i
    have "μ (neg_wtn E i)  0" using rep_neg_leq[of "pos_wtn E i"] 
      unfolding neg_wtn_def .
    thus "¦μ (neg_wtn E i)¦ = -μ (neg_wtn E i)" using less_eq_ereal_def by auto 
  qed
  ultimately show ?thesis by simp
qed

lemma inv_num_wtn_summable:
  assumes "E  sets M"
    and "¦μ E¦ < "
  shows "summable (λn. 1/(num_wtn E n))"
proof (rule summable_bounded)
  show "i. 0  1 / real (num_wtn E i)" by simp
  show "i. 1 / real (num_wtn E i)  (λn. -real_of_ereal (μ (neg_wtn E n))) i"
  proof -
    fix i
    have "¦μ (neg_wtn E i)¦ < " using assms neg_wtn_infty by simp
    have "ereal (1/(num_wtn E i))  -μ (neg_wtn E i)" using num_wtn_geq[of E i] 
        ereal_minus_le_minus by fastforce 
    also have "... = ereal(- real_of_ereal (μ (neg_wtn E i)))" 
      using ¦μ (neg_wtn E i)¦ <  ereal_real' by auto
    finally have "ereal (1/(num_wtn E i))  
      ereal(- real_of_ereal (μ (neg_wtn E i)))" .
    thus "1 / real (num_wtn E i)  -real_of_ereal (μ (neg_wtn E i))" by simp
  qed
  show "summable (λi. - real_of_ereal (μ (neg_wtn E i)))" 
    using assms neg_wtn_summable by simp
qed

lemma inv_num_wtn_shift_summable:
  assumes "E  sets M"
    and "¦μ E¦ < "
  shows "summable (λn. 1/(num_wtn E n - 1))"
proof (rule sum_shift_denum)
  show "summable (λn. 1 / real (num_wtn E n))" using assms inv_num_wtn_summable
    by simp
qed

lemma neg_wtn_meas_sums:
  assumes "E  sets M"
    and "¦μ E¦ < "
  shows "(λi. - (μ (neg_wtn E i))) sums 
  suminf (λi. - real_of_ereal (μ (neg_wtn E i)))"
proof -
  have "(λi. ereal (- real_of_ereal (μ (neg_wtn E i)))) sums 
    suminf (λi. - real_of_ereal (μ (neg_wtn E i)))"
  proof (rule sums_ereal[THEN iffD2])
    have "summable (λi. - real_of_ereal (μ (neg_wtn E i)))" 
      using neg_wtn_summable assms by simp
    thus "(λx. - real_of_ereal (μ (neg_wtn E x))) 
      sums (i. - real_of_ereal (μ (neg_wtn E i)))" 
      by auto
  qed
  moreover have "i. μ (neg_wtn E i) = ereal (real_of_ereal (μ (neg_wtn E i)))"
  proof -
    fix i
    show "μ (neg_wtn E i) = ereal (real_of_ereal (μ (neg_wtn E i)))"
      using assms(1) assms(2) ereal_real' neg_wtn_infty by auto
  qed
  ultimately show ?thesis 
    by (metis (no_types, lifting) sums_cong uminus_ereal.simps(1)) 
qed

lemma neg_wtn_meas_suminf_le:
  assumes "E  sets M"
    and "¦μ E¦ < "
  shows "suminf (λi. μ (neg_wtn E i))  - suminf (λn. 1/(num_wtn E n))"
proof -
  have "suminf (λn. 1/(num_wtn E n))  
    suminf (λi. -real_of_ereal (μ (neg_wtn E i)))"
  proof (rule suminf_le)
    show "summable (λn.  1 / real (num_wtn E n))" using assms 
        inv_num_wtn_summable[of E] 
        summable_minus[of "λn. 1 / real (num_wtn E n)"]  by simp 
    show "summable (λi. -real_of_ereal (μ (neg_wtn E i)))" 
      using neg_wtn_summable assms
        summable_minus[of "λi. real_of_ereal (μ (neg_wtn E i))"] 
      by (simp add: summable_minus_iff) 
    show "n. 1 / real (num_wtn E n)  -real_of_ereal (μ (neg_wtn E n))"
    proof -
      fix n
      have "μ (neg_wtn E n)  ereal (- 1 / real (num_wtn E n))" 
        using num_wtn_geq by simp
      hence "ereal (1/ real (num_wtn E n))  - μ (neg_wtn E n)"
        by (metis add.inverse_inverse eq_iff ereal_uminus_le_reorder linear 
            minus_divide_left uminus_ereal.simps(1))
      have "real_of_ereal (ereal (1 / real (num_wtn E n)))  
        real_of_ereal (- μ (neg_wtn E n))"
      proof (rule real_of_ereal_positive_mono)
        show "0  ereal (1 / real (num_wtn E n))" by simp
        show "ereal (1 / real (num_wtn E n))  - μ (neg_wtn E n)" 
          using ereal (1 / real (num_wtn E n))  - μ (neg_wtn E n) .
        show "- μ (neg_wtn E n)  " using neg_wtn_infty[of E n] assms by auto
      qed
      thus "(1 / real (num_wtn E n))  -real_of_ereal ( μ (neg_wtn E n))" 
        by simp
    qed
  qed
  also have "... = - suminf (λi. real_of_ereal (μ (neg_wtn E i)))" 
  proof (rule suminf_minus)
    show "summable (λn. real_of_ereal (μ (neg_wtn E n)))" 
      using neg_wtn_summable assms
        summable_minus[of "λi. real_of_ereal (μ (neg_wtn E i))"] 
      by (simp add: summable_minus_iff) 
  qed
  finally have "suminf (λn. 1/(num_wtn E n))  
    - suminf (λi. real_of_ereal (μ (neg_wtn E i)))" .
  hence a:  "suminf (λi. real_of_ereal (μ (neg_wtn E i)))  
    - suminf (λn. 1/(num_wtn E n))" by simp
  show "suminf (λi. (μ (neg_wtn E i)))  ereal (-suminf (λn. 1/(num_wtn E n)))" 
  proof -
    have sumeq: "suminf (λi. ereal (real_of_ereal (μ (neg_wtn E i)))) = 
      suminf (λi. (real_of_ereal (μ (neg_wtn E i))))"
    proof (rule sums_suminf_ereal)
      have "summable (λi. -real_of_ereal (μ (neg_wtn E i)))" 
        using neg_wtn_summable assms
          summable_minus[of "λi. real_of_ereal (μ (neg_wtn E i))"] 
        by (simp add: summable_minus_iff)
      thus "(λi. real_of_ereal (μ (neg_wtn E i))) sums 
        (i. real_of_ereal (μ (neg_wtn E i)))" 
        using neg_wtn_summable[of E] assms summable_minus_iff by blast
    qed
    hence "suminf (λi. μ (neg_wtn E i)) = 
      suminf (λi. (real_of_ereal (μ (neg_wtn E i))))" 
    proof -
      have "i. ereal (real_of_ereal (μ (neg_wtn E i))) = μ (neg_wtn E i)"
      proof -
        fix i
        show "ereal (real_of_ereal (μ (neg_wtn E i))) = μ (neg_wtn E i)"
          using neg_wtn_infty[of E] assms by (simp add: ereal_real')
      qed
      thus ?thesis using sumeq by auto 
    qed
    thus ?thesis using a by simp
  qed
qed

lemma union_wit_meas_le:
  assumes "E  sets M"
    and "¦μ E¦ < "
  shows "μ (union_wit E)  - suminf (λn. 1 / real (num_wtn E n))" 
proof -
  have "μ (union_wit E) = μ ( (range (neg_wtn E)))" unfolding union_wit_def 
    by simp
  also have "... = (i. μ (neg_wtn E i))" 
  proof (rule signed_measure_inf_sum[symmetric])
    show "signed_measure M μ" using sgn_meas .
    show "range (neg_wtn E)  sets M" 
      by (simp add: image_subset_iff neg_wtn_def rep_neg_sets)
    show "disjoint_family (neg_wtn E)" using neg_wtn_djn by simp
    show " (range (neg_wtn E))  sets M" using union_wit_sets 
      unfolding union_wit_def by simp
  qed
  also have "...  - suminf (λn. 1 / real (num_wtn E n))" 
    using assms neg_wtn_meas_suminf_le by simp
  finally show ?thesis .
qed

lemma pos_sub_pos_meas:
  assumes "E  sets M"
    and "¦μ E¦ < "
    and "0 < μ E"
    and "¬ pos_meas_set E"
  shows "0 < μ (pos_sub E)"
proof -
  have "0 < μ E" using assms by simp
  also have "... = μ (pos_sub E) + μ (union_wit E)"
  proof -
    have "E = pos_sub E  (union_wit E)" 
      using pos_sub_diff[of E] union_wit_subset by force 
    moreover have "pos_sub E  union_wit E = {}" 
      using pos_sub_diff by auto
    ultimately show ?thesis 
      using signed_measure_add[of M μ "pos_sub E" "union_wit E"] 
        pos_sub_sets union_wit_sets assms sgn_meas by simp
  qed
  also have "...  μ (pos_sub E) + (- suminf (λn. 1 / real (num_wtn E n)))"
  proof -
    have "μ (union_wit E)  - suminf (λn. 1 / real (num_wtn E n))" 
      using union_wit_meas_le[of E] assms by simp
    thus ?thesis using union_wit_infty assms using add_left_mono by blast
  qed
  also have "... = μ (pos_sub E) - suminf (λn. 1 / real (num_wtn E n))"
    by (simp add: minus_ereal_def) 
  finally have "0 < μ (pos_sub E) - suminf (λn. 1 / real (num_wtn E n))" .
  moreover have "0 < suminf (λn. 1 / real (num_wtn E n))" 
  proof (rule suminf_pos2)
    show "0 < 1 / real (num_wtn E 0)" 
      using inf_neg_ge_1[of E] assms pos_wtn_base unfolding num_wtn_def by simp
    show "n. 0  1 / real (num_wtn E n)" by simp
    show "summable (λn. 1 / real (num_wtn E n))" 
      using assms inv_num_wtn_summable by simp
  qed
  ultimately show ?thesis  using pos_sub_infty assms by fastforce
qed

lemma num_wtn_conv:
  assumes "E  sets M"
    and "¦μ E¦ < "
  shows "(λn. 1/(num_wtn E n))  0"
proof (rule summable_LIMSEQ_zero)
  show "summable (λn. 1 / real (num_wtn E n))" 
    using assms inv_num_wtn_summable by simp
qed

lemma num_wtn_shift_conv:
  assumes "E  sets M"
    and "¦μ E¦ < "
  shows "(λn. 1/(num_wtn E n - 1))  0"
proof (rule summable_LIMSEQ_zero)
  show "summable (λn. 1 / real (num_wtn E n - 1))" 
    using assms inv_num_wtn_shift_summable by simp
qed

lemma inf_neg_E_set:
  assumes "0 < inf_neg E"
  shows "E  sets M" using assms unfolding inf_neg_def by presburger

lemma inf_neg_pos_meas:
  assumes "0 < inf_neg E"
  shows "¬ pos_meas_set E" using assms unfolding inf_neg_def by presburger

lemma inf_neg_mem:
  assumes "0 < inf_neg E"
  shows "inf_neg E  {n::nat|n. (1::nat)  n  
    (B  sets M. B   E  μ B < ereal (-1/n))}"
proof -
  have "E  sets M" using assms unfolding inf_neg_def by presburger
  moreover have "¬ pos_meas_set E" using assms unfolding inf_neg_def 
    by presburger
  ultimately have "{n::nat|n. (1::nat)  n  
    (B  sets M. B   E  μ B < ereal (-1/n))}  {}" 
    using inf_neg_ne[of E] by simp
  thus ?thesis unfolding inf_neg_def 
    by (meson Inf_nat_def1 E  sets M ¬ pos_meas_set E)
qed

lemma prec_inf_neg_pos:
  assumes "0 < inf_neg E - 1"
    and "B  sets M"
    and "B E"
  shows "-1/(inf_neg E - 1)  μ B"
proof (rule ccontr)
  define S where "S = {p::nat|p. (1::nat)  p  
    (B  sets M. B   E  μ B < ereal (-1/p))}"
  assume "¬ ereal (- 1 / real (inf_neg E - 1))  μ B"
  hence "μ B < -1/(inf_neg E - 1)" by auto
  hence "inf_neg E - 1 S" unfolding S_def using assms by auto
  have "Suc 0 < inf_neg E" using assms by simp
  hence "inf_neg E  S" unfolding  S_def using inf_neg_mem[of E] by simp
  hence "S  {}" by auto
  have "inf_neg E = Inf S" unfolding S_def inf_neg_def 
    using assms inf_neg_E_set inf_neg_pos_meas by auto
  have  "inf_neg E - 1 < inf_neg E" using assms by simp
  hence "inf_neg E -1  S" 
    using cInf_less_iff[of S] S  {} inf_neg E = Inf S by auto
  thus False using inf_neg E - 1  S by simp
qed

lemma pos_wtn_meas_ge:
  assumes "E  sets M"
    and "¦μ E¦ < "
    and "C sets M"
    and "n. C pos_wtn E n"
    and "n. 0 < num_wtn E n"
  shows "N. n N. - 1/ (num_wtn E n - 1)  μ C" 
proof -
  have "N. n N. 1/(num_wtn E n) < 1/2" using num_wtn_conv[of E] 
      conv_0_half[of "λn. 1 / real (num_wtn E n)"] assms by simp
  from this obtain N where "n N. 1/(num_wtn E n) < 1/2" by auto
  {
    fix n
    assume "N  n"
    hence "1/(num_wtn E n) < 1/2" using n N. 1/(num_wtn E n) < 1/2 by simp
    have "1/(1/2) < 1/(1/(num_wtn E n))" 
    proof (rule frac_less2, auto)
      show "2 / real (num_wtn E n) < 1" using 1/(num_wtn E n) < 1/2 
        by linarith
      show "0 < num_wtn E n" unfolding num_wtn_def using inf_neg_ge_1 assms
        by (simp add: num_wtn_def)
    qed
    hence "2 < (num_wtn E n)" by simp
    hence "Suc 0 < num_wtn E n - 1" unfolding num_wtn_def by simp
    hence "- 1/ (num_wtn E n - 1)  μ C" using assms prec_inf_neg_pos 
      unfolding num_wtn_def by simp
  }
  thus ?thesis by auto
qed

lemma pos_sub_pos_meas_subset:
  assumes "E  sets M"
    and "¦μ E¦ < "
    and "C sets M"
    and "C (pos_sub E)"
    and "n. 0 < num_wtn E n"
  shows "0  μ C"
proof -
  have "n. C  pos_wtn E n" using assms unfolding pos_sub_def by auto
  hence "N. n N. - 1/ (num_wtn E n - 1)  μ C" using  assms  
      pos_wtn_meas_ge[of E C] by simp
  from this obtain N where Nprop: "n N. - 1/ (num_wtn E n - 1)  μ C" by auto
  show "0  μ C"
  proof (rule lim_mono)
    show "n. N  n  - 1/ (num_wtn E n - 1)  (λn. μ C) n" 
      using Nprop by simp
    have "(λn.  ( 1 / real (num_wtn E n - 1)))  0" 
      using assms num_wtn_shift_conv[of E] by simp
    hence "(λn.  (- 1 / real (num_wtn E n - 1)))  0" 
      using tendsto_minus[of "λn. 1 / real (num_wtn E n - 1)" 0] by simp
    thus "(λn. ereal (- 1 / real (num_wtn E n - 1)))  0" 
      by (simp add: zero_ereal_def) 
    show "(λn. μ C)  μ C" by simp
  qed
qed

lemma pos_sub_pos_meas':
  assumes "E  sets M"
    and "¦μ E¦ < "
    and "0 < μ E"
    and "n. 0 < num_wtn E n"
  shows "0 < μ (pos_sub E)"
proof -
  have "0 < μ E" using assms by simp
  also have "... = μ (pos_sub E) + μ (union_wit E)"
  proof -
    have "E = pos_sub E  (union_wit E)" 
      using pos_sub_diff[of E] union_wit_subset by force 
    moreover have "pos_sub E  union_wit E = {}" 
      using pos_sub_diff by auto
    ultimately show ?thesis 
      using signed_measure_add[of M μ "pos_sub E" "union_wit E"] 
        pos_sub_sets union_wit_sets assms sgn_meas by simp
  qed
  also have "...  μ (pos_sub E) + (- suminf (λn. 1 / real (num_wtn E n)))"
  proof -
    have "μ (union_wit E)  - suminf (λn. 1 / real (num_wtn E n))" 
      using union_wit_meas_le[of E] assms by simp
    thus ?thesis using union_wit_infty assms using add_left_mono by blast
  qed
  also have "... = μ (pos_sub E) - suminf (λn. 1 / real (num_wtn E n))"
    by (simp add: minus_ereal_def) 
  finally have "0 < μ (pos_sub E) - suminf (λn. 1 / real (num_wtn E n))" .
  moreover have "0 < suminf (λn. 1 / real (num_wtn E n))" 
  proof (rule suminf_pos2)
    show "0 < 1 / real (num_wtn E 0)" using assms by simp
    show "n. 0  1 / real (num_wtn E n)" by simp
    show "summable (λn. 1 / real (num_wtn E n))" 
      using assms inv_num_wtn_summable by simp
  qed
  ultimately show ?thesis  using pos_sub_infty assms by fastforce
qed

text ‹We obtain the main result of this part on the existence of a positive subset.›

lemma exists_pos_meas_subset:
  assumes "E  sets M"
    and "¦μ E¦ < "
    and "0 < μ E"
  shows "A. A  E  pos_meas_set A  0 < μ A"
proof (cases "n. 0 < num_wtn E n")
  case True
  have "pos_meas_set (pos_sub E)" 
  proof (rule pos_meas_setI)
    show "pos_sub E  sets M" by (simp add: assms(1) pos_sub_sets) 
    fix A
    assume "A  sets M" and "A pos_sub E"
    thus "0  μ A" using assms True pos_sub_pos_meas_subset[of E] by simp
  qed
  moreover have "0 < μ (pos_sub E)" 
    using pos_sub_pos_meas'[of E] True assms by simp
  ultimately show ?thesis using pos_meas_set_def by (metis pos_sub_subset)
next
  case False
  hence "n. num_wtn E n = 0" by simp
  from this obtain n where "num_wtn E n = 0" by auto
  hence "pos_wtn E n  sets M  pos_meas_set (pos_wtn E n)" 
    using inf_neg_ge_1 unfolding num_wtn_def by fastforce
  hence "pos_meas_set (pos_wtn E n)" using assms 
    by (simp add: E  sets M pos_wtn_sets) 
  moreover have "0 < μ (pos_wtn E n)" using pos_wtn_meas_gt assms by simp
  ultimately show ?thesis using pos_meas_set_def by (meson pos_wtn_subset)   
qed

section ‹The Hahn decomposition theorem›

definition seq_meas where
  "seq_meas = (SOME f. incseq f  range f  pos_img    pos_img =  range f)"

lemma seq_meas_props:
  shows "incseq seq_meas  range seq_meas  pos_img  
     pos_img =  range seq_meas"
proof -
  have ex: "f. incseq f  range f  pos_img    pos_img =  range f"
  proof (rule Extended_Real.Sup_countable_SUP)
    show "pos_img  {}"
    proof -
      have "{}  pos_sets" using empty_pos_meas_set unfolding pos_sets_def 
        by simp
      hence "μ {}  pos_img" unfolding pos_img_def by auto
      thus ?thesis by auto
    qed 
  qed
  let ?V = "SOME f. incseq f  range f  pos_img    pos_img =  range f"
  have vprop: "incseq ?V  range ?V  pos_img   pos_img =  range ?V" 
    using someI_ex[of "λf. incseq f  range f  pos_img   
       pos_img =  range f"] ex by blast
  show ?thesis using seq_meas_def vprop by presburger
qed

definition seq_meas_rep where
  "seq_meas_rep n = (SOME A. A pos_sets  seq_meas n = μ A)"

lemma seq_meas_rep_ex:
  shows "seq_meas_rep n  pos_sets  μ (seq_meas_rep n) = seq_meas n"
proof -
  have ex: "A. A  pos_sets  seq_meas n = μ A" using seq_meas_props
    by (smt (verit) UNIV_I image_subset_iff mem_Collect_eq pos_img_def) 
  let ?V = "SOME A. A pos_sets  seq_meas n = μ A"
  have vprop: "?V pos_sets  seq_meas n = μ ?V" using 
      someI_ex[of "λA. A pos_sets  seq_meas n = μ A"] using ex by blast
  show ?thesis using seq_meas_rep_def vprop by fastforce 
qed

lemma seq_meas_rep_pos:
  assumes "E  sets M. μ E < " 
  shows "pos_meas_set ( i. seq_meas_rep i)" 
proof (rule pos_meas_set_Union)
  show " i. pos_meas_set (seq_meas_rep i)" 
    using seq_meas_rep_ex signed_measure_space.pos_sets_def 
      signed_measure_space_axioms by auto
  then show "i. seq_meas_rep i  sets M"
    by (simp add: pos_meas_setD1)
  show "¦μ ( (range seq_meas_rep))¦ < "
  proof -
    have "( (range seq_meas_rep))  sets M"
    proof (rule sigma_algebra.countable_Union)
      show "sigma_algebra (space M) (sets M)" 
        by (simp add: sets.sigma_algebra_axioms) 
      show "countable (range seq_meas_rep)" by simp
      show "range seq_meas_rep  sets M" 
        by (simp add: i. seq_meas_rep i  sets M image_subset_iff)
    qed
    hence "μ ( (range seq_meas_rep))  0 " 
      using i. pos_meas_set (seq_meas_rep i) i. seq_meas_rep i  sets M 
        signed_measure_space.pos_meas_set_pos_lim signed_measure_space_axioms 
      by blast
    thus ?thesis using assms  (range seq_meas_rep)  sets M abs_ereal_ge0  
      by simp
  qed   
qed

lemma sup_seq_meas_rep:
  assumes "E  sets M. μ E < " 
    and "S = ( pos_img)"
    and "A = ( i. seq_meas_rep i)"
  shows "μ A = S"
proof -
  have pms: "pos_meas_set ( i. seq_meas_rep i)" 
    using assms seq_meas_rep_pos by simp
  hence "μ A  S" 
    by (metis (mono_tags, lifting) Sup_upper S =  pos_img mem_Collect_eq 
        pos_img_def pos_meas_setD1 pos_sets_def assms(2) assms(3))  
  have "n. (μ A = μ (A - seq_meas_rep n) + μ (seq_meas_rep n))"
  proof
    fix n
    have "A = (A - seq_meas_rep n)  seq_meas_rep n " 
      using A =  (range seq_meas_rep) by blast
    hence "μ A = μ ((A - seq_meas_rep n)  seq_meas_rep n)"  by simp
    also have "... = μ (A - seq_meas_rep n) + μ (seq_meas_rep n)" 
    proof (rule signed_measure_add)
      show "signed_measure M μ" using sgn_meas by simp
      show "seq_meas_rep n  sets M"
        using pos_sets_def seq_meas_rep_ex by auto
      then show "A - seq_meas_rep n  sets M"
        by (simp add: assms pms pos_meas_setD1 sets.Diff)
      show "(A - seq_meas_rep n)  seq_meas_rep n = {}" by auto
    qed
    finally show "μ A = μ (A - seq_meas_rep n) + μ (seq_meas_rep n)".
  qed
  have "n. μ A  μ (seq_meas_rep n)" 
  proof 
    fix n
    have "μ A  0" using pms assms unfolding pos_meas_set_def by auto
    have "(A - seq_meas_rep n)  A" by simp
    hence "pos_meas_set (A - seq_meas_rep n)" 
    proof -
      have "(A - seq_meas_rep n)  sets M"
        using pms assms pos_meas_setD1 pos_sets_def seq_meas_rep_ex by auto
      thus ?thesis using pms assms unfolding pos_meas_set_def by auto
    qed
    hence "μ (A - seq_meas_rep n)  0" unfolding pos_meas_set_def by auto
    thus "μ (seq_meas_rep n)  μ A" 
      using n. (μ A = μ (A - seq_meas_rep n) + μ (seq_meas_rep n))
      by (metis ereal_le_add_self2) 
  qed
  hence "μ A  ( range seq_meas)" by (simp add: Sup_le_iff seq_meas_rep_ex)
  moreover have "S = ( range seq_meas)" 
    using seq_meas_props S = ( pos_img) by simp
  ultimately have "μ A  S" by simp
  thus "μ A = S" using μ A  S by simp
qed

lemma seq_meas_rep_compl:
  assumes "E  sets M. μ E < "
    and "A = ( i. seq_meas_rep i)"
  shows "neg_meas_set ((space M) - A)" unfolding neg_meas_set_def
proof (rule ccontr)
  assume asm: "¬ (space M - A  sets M  
    (Aasets M. Aa  space M - A  μ Aa  0))" 
  define S where "S = ( pos_img)"
  have "pos_meas_set A"  using assms seq_meas_rep_pos by simp
  have "μ A = S" using sup_seq_meas_rep assms  S_def by simp
  hence "S < " using assms pos_meas_set A pos_meas_setD1 by blast 
  have "(space M - A  sets M)"
    by (simp add: pos_meas_set A pos_meas_setD1 sets.compl_sets)
  hence " ¬(Aasets M. Aa  space M - A  μ Aa  0)" using asm by blast
  hence " E  sets M. E  ((space M) - A)  μ E > 0" 
    by (metis less_eq_ereal_def linear)
  from this obtain E where "E  sets M" and "E  ((space M) - A)" and 
    "μ E > 0" by auto
  have " A0  E. pos_meas_set A0  μ A0 > 0" 
  proof (rule exists_pos_meas_subset) 
    show "E  sets M" using E  sets M by simp
    show "0 < μ E" using μ E > 0 by simp
    show "¦μ E¦ < " 
    proof -
      have "μ E < " using assms E  sets M by simp
      moreover have "-  < μ E" using 0 < μ E by simp 
      ultimately show ?thesis
        by (meson ereal_infty_less(1) not_inftyI)
    qed
  qed
  from this obtain A0 where "A0  E" and "pos_meas_set A0" and " μ A0 > 0" 
    by auto
  have "pos_meas_set (A  A0)" 
    using pos_meas_set_union pos_meas_set A0 pos_meas_set A by simp
  have "μ (A  A0) = μ A + μ A0" 
  proof (rule signed_measure_add)
    show "signed_measure M μ" using sgn_meas by simp
    show "A  sets M" using pos_meas_set A 
      unfolding pos_meas_set_def by simp
    show "A0  sets M" using pos_meas_set A0 
      unfolding pos_meas_set_def by simp
    show "(A  A0) = {}" using A0  E E  ((space M) - A) by auto
  qed
  then have "μ (A  A0) > S" 
    using μ A = S μ A0 > 0
    by (metis S <  pos_meas_set (A  A0) abs_ereal_ge0 ereal_between(2) 
        not_inftyI not_less_iff_gr_or_eq pos_meas_self)
  have "(A  A0)  pos_sets"
  proof -
    have " (A  A0)  sets M" using sigma_algebra.countable_Union
      by (simp add: pos_meas_set (A  A0) pos_meas_setD1) 
    moreover have "pos_meas_set (A  A0)" using pos_meas_set (A  A0) by simp
    ultimately show ?thesis unfolding pos_sets_def by simp
  qed
  then have "μ (A  A0)  pos_img" unfolding pos_img_def by auto
  show False using μ (A  A0) > S μ (A  A0)  pos_img S = ( pos_img)
    by (metis Sup_upper sup.absorb_iff2 sup.strict_order_iff)
qed

lemma hahn_decomp_finite:
  assumes "E  sets M. μ E < "
  shows " M1 M2. hahn_space_decomp M1 M2" unfolding hahn_space_decomp_def
proof -
  define S where "S = ( pos_img)"
  define A where "A = ( i. seq_meas_rep i)" 
  have "pos_meas_set A" unfolding A_def using assms seq_meas_rep_pos by simp
  have "neg_meas_set ((space M) - A)" 
    using seq_meas_rep_compl assms unfolding A_def by simp
  show "M1 M2. pos_meas_set M1  neg_meas_set M2  space M = M1  M2  
    M1  M2 = {}"
  proof (intro exI conjI)
    show "pos_meas_set A" using pos_meas_set A .
    show "neg_meas_set (space M - A)" using neg_meas_set (space M - A) .
    show "space M = A  (space M - A)"
      by (metis Diff_partition pos_meas_set A inf.absorb_iff2 pos_meas_setD1 
          sets.Int_space_eq1) 
    show "A  (space M - A) = {}" by auto
  qed
qed

theorem hahn_decomposition:
  shows " M1 M2. hahn_space_decomp M1 M2"
proof (cases "E  sets M. μ E < ")
  case True
  thus ?thesis using hahn_decomp_finite by simp
next
  case False
  define m where "m = (λA . - μ A)"
  have " M1 M2. signed_measure_space.hahn_space_decomp M m M1 M2"
  proof (rule signed_measure_space.hahn_decomp_finite)
    show "signed_measure_space M m" 
      using signed_measure_minus sgn_meas m = (λA . - μ A)  
      by (unfold_locales, simp)
    show "Esets M. m E < "
    proof
      fix E
      assume "E  sets M"
      show "m E < "
      proof
        show "m E  "
        proof (rule ccontr)
          assume "¬ m E  "
          have "m E = "
            using ¬ m E   by auto 
          have "signed_measure M m"
            using signed_measure_space M m signed_measure_space_def by auto
          moreover have "m E = - μ E" using m = (λA . - μ A) by auto
          then have "  range m" using signed_measure M m
            by (metis (no_types, lifting) False ereal_less_PInfty 
                ereal_uminus_eq_reorder image_iff inf_range m_def rangeI)
          show False using m E =    range m
            by (metis rangeI)
        qed
      qed
    qed
  qed
  hence " M1 M2. (neg_meas_set M1)  (pos_meas_set M2)  (space M = M1  M2) 
    (M1  M2 = {})" 
    using pos_meas_set_opp neg_meas_set_opp unfolding m_def 
    by (metis sgn_meas signed_measure_minus signed_measure_space_def 
        signed_measure_space.hahn_space_decomp_def)
  thus ?thesis using hahn_space_decomp_def by (metis inf_commute sup_commute)
qed

section ‹The Jordan decomposition theorem›

definition jordan_decomp where
  "jordan_decomp m1 m2  ((measure_space (space M) (sets M) m1)  
    (measure_space (space M) (sets M) m2)  
    (A sets M. 0  m1 A) 
    ( A sets M. 0  m2 A) 
    (A  sets M. μ A = (m1 A) - (m2 A)) 
    ( P N A. hahn_space_decomp P N  
      (A  sets M  A  P  (m2 A) = 0)  
      (A  sets M  A  N  (m1 A) = 0)) 
    ((A  sets M. m1 A < )  (A  sets M. m2 A < )))"

lemma jordan_decomp_pos_meas:
  assumes "jordan_decomp m1 m2"
    and "hahn_space_decomp P N"
    and "A  sets M"
  shows "m1 A = μ (A  P)" 
proof -
  have "AP  sets M" using assms unfolding hahn_space_decomp_def
    by (simp add: pos_meas_setD1 sets.Int)
  have "A N  sets M" using assms unfolding hahn_space_decomp_def
    by (simp add: neg_meas_setD1 sets.Int)
  have "(A  P)  (A N) = {}" using assms unfolding hahn_space_decomp_def 
    by auto
  have "A = (A  P)  (A N)" using assms unfolding hahn_space_decomp_def
    by (metis Int_Un_distrib sets.Int_space_eq2)
  hence "m1 A = m1 ((A  P)  (A N))" by simp
  also have "... = m1 (A  P) + m1 (A  N)" 
    using assms pos_e2ennreal_additive[of M m1] AP  sets M AN  sets M 
      A  P  (A  N) = {} 
    unfolding jordan_decomp_def additive_def by simp
  also have "... = m1 (A  P)" using assms unfolding jordan_decomp_def
    by (metis Int_lower2 A  N  sets M add.right_neutral)
  also have "... = m1 (A  P) - m2 (A  P)" 
    using assms unfolding jordan_decomp_def
    by (metis Int_subset_iff A  P  sets M ereal_minus(7) 
        local.pos_wtn_base pos_wtn_subset)
  also have "... = μ (A  P)" using assms A  P  sets M 
    unfolding jordan_decomp_def by simp
  finally show ?thesis .
qed

lemma jordan_decomp_neg_meas:
  assumes "jordan_decomp m1 m2"
    and "hahn_space_decomp P N"
    and "A  sets M"
  shows "m2 A = -μ (A  N)" 
proof -
  have "AP  sets M" using assms unfolding hahn_space_decomp_def
    by (simp add: pos_meas_setD1 sets.Int)
  have "A N  sets M" using assms unfolding hahn_space_decomp_def
    by (simp add: neg_meas_setD1 sets.Int)
  have "(A  P)  (A N) = {}" 
    using assms unfolding hahn_space_decomp_def by auto
  have "A = (A  P)  (A N)" 
    using assms unfolding hahn_space_decomp_def
    by (metis Int_Un_distrib sets.Int_space_eq2)
  hence "m2 A = m2 ((A  P)  (A N))" by simp
  also have "... = m2 (A  P) + m2 (A  N)" 
    using pos_e2ennreal_additive[of M m2] assms
      AP  sets M AN  sets M A  P  (A  N) = {} 
    unfolding jordan_decomp_def additive_def by simp
  also have "... = m2 (A  N)" using assms unfolding jordan_decomp_def
    by (metis Int_lower2 A  P  sets M add.commute add.right_neutral)
  also have "... = m2 (A  N) - m1 (A  N)" 
    using assms unfolding jordan_decomp_def
    by (metis Int_lower2 A  N  sets M ereal_minus(7))
  also have "... = -μ (A  N)" using assms A  P  sets M 
    unfolding jordan_decomp_def
    by (metis Diff_cancel Diff_eq_empty_iff Int_Un_eq(2) A  N  sets M 
        m2 (A  N) = m2 (A  N) - m1 (A  N) ereal_minus(8) 
        ereal_uminus_eq_reorder sup.bounded_iff)
  finally show ?thesis .
qed

lemma pos_inter_neg_0:
  assumes "hahn_space_decomp M1 M2"
    and "hahn_space_decomp P N"
    and "A  sets M"
    and "A  N"
  shows "μ (A  M1) = 0"
proof -
  have "μ (A  M1) = μ (A  ((M1  P)  (M1  (sym_diff M1 P))))"
    by (metis Diff_subset_conv Int_Un_distrib Un_upper1 inf.orderE)
  also have "... = μ ((A  (M1  P))  (A  (M1  (sym_diff M1 P))))" 
    by (simp add: Int_Un_distrib) 
  also have "... = μ (A  (M1  P)) + μ (A  (M1  (sym_diff M1 P)))" 
  proof (rule signed_measure_add)
    show "signed_measure M μ" using sgn_meas .
    show "A  (M1  P)  sets M"
      by (meson assms(1) assms(2) assms(3) hahn_space_decomp_def sets.Int 
          signed_measure_space.pos_meas_setD1 signed_measure_space_axioms) 
    show "A  (M1  sym_diff M1 P)  sets M"
      by (meson Diff_subset assms(1) assms(2) assms(3) hahn_space_decomp_def 
          pos_meas_setD1 pos_meas_set_union pos_meas_subset sets.Diff sets.Int)
    show "A  (M1  P)  (A  (M1  sym_diff M1 P)) = {}" by auto
  qed
  also have "... = μ (A  (M1  (sym_diff M1 P)))"
  proof -
    have "A  (M1  P) = {}" using assms hahn_space_decomp_def by auto
    thus ?thesis using signed_measure_empty[OF sgn_meas] by simp
  qed
  also have "... = 0" 
  proof (rule hahn_decomp_ess_unique[OF assms(1) assms(2)]) 
    show "A  (M1  sym_diff M1 P)  sym_diff M1 P  sym_diff M2 N" by auto
    show "A  (M1  sym_diff M1 P)  sets M" 
    proof -
      have "sym_diff M1 P  sets M" using assms
        by (meson hahn_space_decomp_def sets.Diff sets.Un 
            signed_measure_space.pos_meas_setD1 signed_measure_space_axioms)
      hence "M1  sym_diff M1 P  sets M"
        by (meson assms(1) hahn_space_decomp_def pos_meas_setD1 sets.Int)
      thus ?thesis by (simp add: assms sets.Int)
    qed
  qed
  finally show ?thesis .
qed

lemma neg_inter_pos_0:
  assumes "hahn_space_decomp M1 M2"
    and "hahn_space_decomp P N"
    and "A  sets M"
    and "A  P"
  shows "μ (A  M2) = 0"
proof -
  have "μ (A  M2) = μ (A  ((M2  N)  (M2  (sym_diff M2 N))))"
    by (metis Diff_subset_conv Int_Un_distrib Un_upper1 inf.orderE)
  also have "... = μ ((A  (M2  N))  (A  (M2  (sym_diff M2 N))))" 
    by (simp add: Int_Un_distrib) 
  also have "... = μ (A  (M2  N)) + μ (A  (M2  (sym_diff M2 N)))" 
  proof (rule signed_measure_add)
    show "signed_measure M μ" using sgn_meas .
    show "A  (M2  N)  sets M"
      by (meson assms(1) assms(2) assms(3) hahn_space_decomp_def sets.Int 
          signed_measure_space.neg_meas_setD1 signed_measure_space_axioms) 
    show "A  (M2  sym_diff M2 N)  sets M"
      by (meson Diff_subset assms(1) assms(2) assms(3) hahn_space_decomp_def 
          neg_meas_setD1 neg_meas_set_union neg_meas_subset sets.Diff sets.Int)
    show "A  (M2  N)  (A  (M2  sym_diff M2 N)) = {}" by auto
  qed
  also have "... = μ (A  (M2  (sym_diff M2 N)))"
  proof -
    have "A  (M2  N) = {}" using assms hahn_space_decomp_def by auto
    thus ?thesis using signed_measure_empty[OF sgn_meas] by simp
  qed
  also have "... = 0" 
  proof (rule hahn_decomp_ess_unique[OF assms(1) assms(2)]) 
    show "A  (M2  sym_diff M2 N)  sym_diff M1 P  sym_diff M2 N" by auto
    show "A  (M2  sym_diff M2 N)  sets M" 
    proof -
      have "sym_diff M2 N  sets M" using assms
        by (meson hahn_space_decomp_def sets.Diff sets.Un 
            signed_measure_space.neg_meas_setD1 signed_measure_space_axioms)
      hence "M2  sym_diff M2 N  sets M"
        by (meson assms(1) hahn_space_decomp_def neg_meas_setD1 sets.Int)
      thus ?thesis by (simp add: assms sets.Int)
    qed
  qed
  finally show ?thesis .
qed

lemma jordan_decomposition :
  shows " m1 m2. jordan_decomp m1 m2" 
proof -
  have " M1 M2. hahn_space_decomp M1 M2" using hahn_decomposition 
    unfolding hahn_space_decomp_def by simp
  from this obtain M1 M2 where "hahn_space_decomp M1 M2" by auto 
  note Mprops = this
  define m1 where "m1 = (λA. μ (A  M1))"
  define m2 where "m2 = (λA. -μ (A  M2))"  
  show ?thesis unfolding jordan_decomp_def
  proof (intro exI allI impI conjI ballI)
    show "measure_space (space M) (sets M) (λx. e2ennreal (m1 x))" 
      using pos_signed_to_meas_space Mprops m1_def 
      unfolding hahn_space_decomp_def by auto
  next
    show "measure_space (space M) (sets M) (λx. e2ennreal (m2 x))" 
      using neg_signed_to_meas_space Mprops m2_def 
      unfolding hahn_space_decomp_def by auto
  next
    fix A
    assume "A sets M"
    thus "0  m1 A" unfolding m1_def using Mprops 
      unfolding hahn_space_decomp_def 
      by (meson inf_sup_ord(2) pos_meas_setD1 sets.Int 
          signed_measure_space.pos_measure_meas signed_measure_space_axioms)
  next
    fix A 
    assume "A sets M"
    thus "0  m2 A" unfolding m2_def using Mprops 
      unfolding hahn_space_decomp_def
      by (metis ereal_0_le_uminus_iff inf_sup_ord(2) neg_meas_self 
          neg_meas_setD1 neg_meas_subset sets.Int)
  next
    fix A
    assume "A  sets M"
    have "μ A = μ ((A  M1)  (A  M2))" using Mprops 
      unfolding hahn_space_decomp_def
      by (metis Int_Un_distrib A  sets M sets.Int_space_eq2)
    also have "... = μ (A  M1) + μ (A  M2)" 
    proof (rule signed_measure_add)
      show "signed_measure M μ" using sgn_meas .
      show "A  M1  sets M" using Mprops  A  sets M 
        unfolding hahn_space_decomp_def 
        by (simp add: pos_meas_setD1 sets.Int) 
      show "A  M2  sets M" using Mprops A  sets M 
        unfolding hahn_space_decomp_def
        by (simp add: neg_meas_setD1 sets.Int) 
      show "A  M1  (A  M2) = {}" using Mprops 
        unfolding hahn_space_decomp_def by auto
    qed
    also have "... = m1 A - m2 A" using m1_def m2_def by simp
    finally show "μ A = m1 A - m2 A" .    
  next
    fix P N A
    assume "hahn_space_decomp P N" and "A  sets M" and "A  N" 
    note hn = this
    have "μ (A  M1) = 0"
    proof (rule pos_inter_neg_0[OF _ hn])
      show "hahn_space_decomp M1 M2" using Mprops 
        unfolding hahn_space_decomp_def by simp
    qed
    thus "m1 A = 0" unfolding m1_def by simp
  next
    fix P N A
    assume "hahn_space_decomp P N" and "A  sets M" and "A  P" 
    note hp = this
    have "μ (A  M2) = 0"
    proof (rule neg_inter_pos_0[OF _ hp])
      show "hahn_space_decomp M1 M2" using Mprops 
        unfolding hahn_space_decomp_def by simp
    qed
    thus "m2 A = 0" unfolding m2_def by simp
  next
    show "(Esets M. m1 E < )  (Esets M. m2 E < )"
    proof (cases " E  sets M. m1 E < ")
      case True
      thus ?thesis by simp
    next
      case False
      have " E  sets M. m2 E < "
      proof
        fix E
        assume "E  sets M"
        show "m2 E < "
        proof -
          have "(m2 E) = -μ (E  M2)" using m2_def by simp        
          also have "...  " using False sgn_meas inf_range
            by (metis ereal_less_PInfty ereal_uminus_uminus m1_def rangeI)
          finally have "m2 E  " .
          thus ?thesis by (simp add: top.not_eq_extremum)
        qed
      qed
      thus ?thesis by simp
    qed
  qed
qed

lemma jordan_decomposition_unique :
  assumes "jordan_decomp m1 m2" 
    and "jordan_decomp n1 n2"
    and "A  sets M"
  shows "m1 A = n1 A" "m2 A = n2 A"
proof -
  have " M1 M2. hahn_space_decomp M1 M2" using hahn_decomposition by simp
  from this obtain M1 M2 where "hahn_space_decomp M1 M2" by auto 
  note mprop = this
  have "m1 A = μ (A  M1)" using assms jordan_decomp_pos_meas mprop by simp
  also have "... = n1 A" using assms jordan_decomp_pos_meas[of n1] mprop 
    by simp
  finally show "m1 A = n1 A" .
  have "m2 A = -μ (A  M2)" using assms jordan_decomp_neg_meas mprop by simp
  also have "... = n2 A" using assms jordan_decomp_neg_meas[of n1] mprop 
    by simp
  finally show "m2 A = n2 A" .
qed
end
end