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 (z3) 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 "