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 (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 "(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
from this obtain M1 M2 where "hahn_space_decomp M1 M2" by auto
note mprop = this
have "m1 A = μ (A ∩ M1)" using assms jordan_decomp_pos_meas mprop by simp
also have "... = n1 A" using assms jordan_decomp_pos_meas[of n1] mprop
by simp
finally show "m1 A = n1 A" .
have "m2 A = -μ (A ∩ M2)" using assms jordan_decomp_neg_meas mprop by simp
also have "... = n2 A" using assms jordan_decomp_neg_meas[of n1] mprop
by simp
finally show "m2 A = n2 A" .
qed
end
end