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 "x∪y ∈ 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 "... = (∑i∈insert 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. ∑i≤n. μ (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 (∑i≤n. μ (A i))) ⤏ 
      e2ennreal (μ (⋃ (range A)))) sequentially"
    using tendsto_e2ennrealI[of "(λn. ∑i≤n. μ (A i))" "μ (⋃ (range A))"] 
    by simp
  moreover have "⋀n. e2ennreal (∑i≤n. μ (A i)) = (∑i≤n. e2ennreal (μ (A i)))"
    using e2ennreal_finite_sum by (metis enn2ereal_nonneg eq finite_atMost)
  ultimately have "((λn. (∑i≤n. 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_lower2‹DB ∈ 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_lower2‹DB ∈ 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 "∀E∈sets 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 "∀E∈sets 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 "∀m∈UNIV. ∀n∈UNIV. 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 ∧ 
    (∀Aa∈sets 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 " ¬(∀Aa∈sets 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 "∀E∈sets 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 "A∩P ∈ 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] ‹A∩P ∈ sets M› ‹A∩N ∈ 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 "A∩P ∈ 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
      ‹A∩P ∈ sets M› ‹A∩N ∈ 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 "(∀E∈sets M. m1 E < ∞) ∨ (∀E∈sets 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
  with jordan_decomp_neg_meas jordan_decomp_pos_meas 
  show "m1 A = n1 A" "m2 A = n2 A" by (metis assms)+
qed

end

end