Theory Riesz_Representation
section ‹The Riesz Representation Theorem›
theory Riesz_Representation
imports "Regular_Measure"
"Urysohn_Locally_Compact_Hausdorff"
begin
subsection ‹ Lemmas for Complex-Valued Continuous Maps ›
lemma continuous_map_Re'[simp,continuous_intros]: "continuous_map euclidean euclideanreal Re"
and continuous_map_Im'[simp,continuous_intros]: "continuous_map euclidean euclideanreal Im"
and continuous_map_complex_of_real'[simp,continuous_intros]: "continuous_map euclideanreal euclidean complex_of_real"
by(auto simp: continuous_on tendsto_Re tendsto_Im)
corollary
assumes "continuous_map X euclidean f"
shows continuous_map_Re[simp,continuous_intros]: "continuous_map X euclideanreal (λx. Re (f x))"
and continuous_map_Im[simp,continuous_intros]: "continuous_map X euclideanreal (λx. Im (f x))"
by(auto intro!: continuous_map_compose[OF assms,simplified comp_def] continuous_map_Re' continuous_map_Im')
lemma continuous_map_of_real_iff[simp]:
"continuous_map X euclidean (λx. of_real (f x) :: _ :: real_normed_div_algebra) ⟷ continuous_map X euclideanreal f"
by(auto simp: continuous_map_atin tendsto_of_real_iff)
lemma continuous_map_complex_mult [continuous_intros]:
fixes f :: "'a ⇒ complex"
shows "⟦continuous_map X euclidean f; continuous_map X euclidean g⟧ ⟹ continuous_map X euclidean (λx. f x * g x)"
by (simp add: continuous_map_atin tendsto_mult)
lemma continuous_map_complex_mult_left:
fixes f :: "'a ⇒ complex"
shows "continuous_map X euclidean f ⟹ continuous_map X euclidean (λx. c * f x)"
by(simp add: continuous_map_atin tendsto_mult)
lemma complex_continuous_map_iff:
"continuous_map X euclidean f ⟷ continuous_map X euclideanreal (λx. Re (f x)) ∧ continuous_map X euclideanreal (λx. Im (f x))"
proof safe
assume "continuous_map X euclideanreal (λx. Re (f x))" "continuous_map X euclideanreal (λx. Im (f x))"
then have "continuous_map X euclidean (λx. Re (f x) + 𝗂 * Im (f x))"
by(auto intro!: continuous_map_add continuous_map_complex_mult_left continuous_map_compose[of X euclideanreal,simplified comp_def])
thus "continuous_map X euclidean f"
using complex_eq by auto
qed(use continuous_map_compose[OF _ continuous_map_Re',simplified comp_def] continuous_map_compose[OF _ continuous_map_Im',simplified comp_def] in auto)
lemma complex_integrable_iff: "complex_integrable M f ⟷ integrable M (λx. Re (f x)) ∧ integrable M (λx. Im (f x))"
proof safe
assume h[measurable]:"integrable M (λx. Re (f x))" "integrable M (λx. Im (f x))"
show "complex_integrable M f"
unfolding integrable_iff_bounded
proof safe
show f[measurable]:"f ∈ borel_measurable M"
using borel_measurable_complex_iff h by blast
have "(∫⇧+ x. ennreal (cmod (f x)) ∂M) ≤ (∫⇧+ x. ennreal (¦Re (f x)¦ + ¦Im (f x)¦) ∂M)"
by(intro nn_integral_mono ennreal_leI) (use cmod_le in auto)
also have "... = (∫⇧+ x. ennreal ¦Re (f x)¦ ∂M) + (∫⇧+ x. ennreal ¦Im (f x)¦ ∂M)"
by(auto intro!: nn_integral_add)
also have "... < ∞"
using h by(auto simp: integrable_iff_bounded)
finally show "(∫⇧+ x. ennreal (cmod (f x)) ∂M) < ∞" .
qed
qed(auto dest: integrable_Re integrable_Im)
subsection ‹ Compact Supports ›
definition has_compact_support_on :: "('a ⇒ 'b :: monoid_add) ⇒ 'a topology ⇒ bool"
(infix ‹has'_compact'_support'_on› 60) where
"f has_compact_support_on X ⟷ compactin X (X closure_of support_on (topspace X) f)"
lemma has_compact_support_on_iff:
"f has_compact_support_on X ⟷ compactin X (X closure_of {x∈topspace X. f x ≠ 0})"
by(simp add: has_compact_support_on_def support_on_def)
lemma has_compact_support_on_zero[simp]: "(λx. 0) has_compact_support_on X"
by(simp add: has_compact_support_on_iff)
lemma has_compact_support_on_compact_space[simp]: "compact_space X ⟹ f has_compact_support_on X"
by(auto simp: has_compact_support_on_def closedin_compact_space)
lemma has_compact_support_on_add[simp,intro!]:
assumes "f has_compact_support_on X" "g has_compact_support_on X"
shows "(λx. f x + g x) has_compact_support_on X"
proof -
have "support_on (topspace X) (λx. f x + g x)
⊆ support_on (topspace X) f ∪ support_on (topspace X) g"
by(auto simp: in_support_on)
moreover have "compactin X (X closure_of ...)"
using assms by(simp add: has_compact_support_on_def compactin_Un)
ultimately show ?thesis
unfolding has_compact_support_on_def by (meson closed_compactin closedin_closure_of closure_of_mono)
qed
lemma has_compact_support_on_sum:
assumes "finite I" "⋀i. i ∈ I ⟹ f i has_compact_support_on X"
shows "(λx. (∑i∈I. f i x)) has_compact_support_on X"
proof -
have "support_on (topspace X) (λx. (∑i∈I. f i x)) ⊆ (⋃i∈I. support_on (topspace X) (f i))"
by(simp add: subset_eq) (meson in_support_on sum.neutral)
moreover have "compactin X (X closure_of ...)"
using assms by(auto simp: has_compact_support_on_def closure_of_Union intro!: compactin_Union)
ultimately show ?thesis
unfolding has_compact_support_on_def by (meson closed_compactin closedin_closure_of closure_of_mono)
qed
lemma has_compact_support_on_mult_left:
fixes g :: "_ ⇒ _ :: mult_zero"
assumes "g has_compact_support_on X"
shows "(λx. f x * g x) has_compact_support_on X"
proof -
have "support_on (topspace X) (λx. f x * g x) ⊆ support_on (topspace X) g"
by(auto simp add: in_support_on)
thus ?thesis
using assms unfolding has_compact_support_on_def
by (meson closed_compactin closedin_closure_of closure_of_mono)
qed
lemma has_compact_support_on_mult_right:
fixes f :: "_ ⇒ _ :: mult_zero"
assumes "f has_compact_support_on X"
shows "(λx. f x * g x) has_compact_support_on X"
proof -
have "support_on (topspace X) (λx. f x * g x) ⊆ support_on (topspace X) f"
by(auto simp add: in_support_on)
thus ?thesis
using assms unfolding has_compact_support_on_def
by (meson closed_compactin closedin_closure_of closure_of_mono)
qed
lemma has_compact_support_on_uminus_iff[simp]:
fixes f :: "_ ⇒ _ :: group_add"
shows "(λx. - f x) has_compact_support_on X ⟷ f has_compact_support_on X"
by(auto simp: has_compact_support_on_def support_on_def)
lemma has_compact_support_on_diff[simp,intro!]:
fixes f :: "_ ⇒ _ :: group_add"
shows "f has_compact_support_on X ⟹ g has_compact_support_on X
⟹ (λx. f x - g x) has_compact_support_on X"
unfolding diff_conv_add_uminus by(intro has_compact_support_on_add) auto
lemma has_compact_support_on_max[simp,intro!]:
assumes "f has_compact_support_on X" "g has_compact_support_on X"
shows "(λx. max (f x) (g x)) has_compact_support_on X"
proof -
have "support_on (topspace X) (λx. max (f x) (g x))
⊆ support_on (topspace X) f ∪ support_on (topspace X) g"
by (simp add: in_support_on max_def_raw unfold_simps(2))
moreover have "compactin X (X closure_of ...)"
using assms by(simp add: has_compact_support_on_def compactin_Un)
ultimately show ?thesis
unfolding has_compact_support_on_def by (meson closed_compactin closedin_closure_of closure_of_mono)
qed
lemma has_compact_support_on_ext_iff[iff]:
"(λx∈topspace X. f x) has_compact_support_on X ⟷ f has_compact_support_on X"
by(auto intro!: arg_cong2[where f=compactin] arg_cong2[where f="(closure_of)"]
simp: has_compact_support_on_def in_support_on)
lemma has_compact_support_on_of_real_iff[iff]:
"(λx. of_real (f x)) has_compact_support_on X = f has_compact_support_on X"
by(auto simp: has_compact_support_on_iff)
lemma has_compact_support_on_complex_iff:
"f has_compact_support_on X ⟷
(λx. Re (f x)) has_compact_support_on X ∧ (λx. Im (f x)) has_compact_support_on X"
proof safe
assume h:"(λx. Re (f x)) has_compact_support_on X" "(λx. Im (f x)) has_compact_support_on X"
have "support_on (topspace X) f ⊆ support_on (topspace X) (λx. Re (f x)) ∪ support_on (topspace X) (λx. Im (f x))"
using complex.expand by(auto simp: in_support_on)
hence "X closure_of support_on (topspace X) f
⊆ X closure_of support_on (topspace X) (λx. Re (f x)) ∪ X closure_of support_on (topspace X) (λx. Im (f x))"
by (metis (no_types, lifting) closure_of_Un sup.absorb_iff2)
thus "f has_compact_support_on X"
using h unfolding has_compact_support_on_def
by (meson closed_compactin closedin_closure_of compactin_Un)
next
assume h:"f has_compact_support_on X"
have "support_on (topspace X) (λx. Re (f x)) ⊆ support_on (topspace X) f"
"support_on (topspace X) (λx. Im (f x)) ⊆ support_on (topspace X) f"
by(auto simp: in_support_on)
thus "(λx. Re (f x)) has_compact_support_on X" "(λx. Im (f x)) has_compact_support_on X"
using h by(auto simp: closed_compactin closure_of_mono has_compact_support_on_def)
qed
lemma [simp]:
assumes "f has_compact_support_on X"
shows has_compact_support_on_Re:"(λx. Re (f x)) has_compact_support_on X"
and has_compact_support_on_Im:"(λx. Im (f x)) has_compact_support_on X"
using assms by(auto simp: has_compact_support_on_complex_iff)
subsection ‹ Positive Linear Functionsls ›
definition positive_linear_functional_on_CX :: "'a topology ⇒ (('a ⇒ 'b :: {ring, order, topological_space}) ⇒ 'b) ⇒ bool"
where "positive_linear_functional_on_CX X φ ≡
(∀f. continuous_map X euclidean f ⟶ f has_compact_support_on X
⟶ (∀x∈topspace X. f x ≥ 0) ⟶ φ (λx∈topspace X. f x) ≥ 0) ∧
(∀f a. continuous_map X euclidean f ⟶ f has_compact_support_on X
⟶ φ (λx∈topspace X. a * f x) = a * φ (λx∈topspace X. f x)) ∧
(∀f g. continuous_map X euclidean f ⟶ f has_compact_support_on X
⟶ continuous_map X euclidean g ⟶ g has_compact_support_on X
⟶ φ (λx∈topspace X. f x + g x) = φ (λx∈topspace X. f x) + φ (λx∈topspace X. g x))"
lemma
assumes "positive_linear_functional_on_CX X φ"
shows pos_lin_functional_on_CX_pos:
"⋀f. continuous_map X euclidean f ⟹ f has_compact_support_on X
⟹ (⋀x. x∈topspace X ⟹ f x ≥ 0) ⟹ φ (λx∈topspace X. f x) ≥ 0"
and pos_lin_functional_on_CX_lin:
"⋀f a. continuous_map X euclidean f ⟹ f has_compact_support_on X
⟹ φ (λx∈topspace X. a * f x) = a * φ (λx∈topspace X. f x)"
"⋀f g. continuous_map X euclidean f ⟹ f has_compact_support_on X
⟹ continuous_map X euclidean g ⟹ g has_compact_support_on X
⟹ φ (λx∈topspace X. f x + g x) = φ (λx∈topspace X. f x) + φ (λx∈topspace X. g x)"
using assms by(auto simp: positive_linear_functional_on_CX_def)
lemma pos_lin_functional_on_CX_pos_complex:
assumes "positive_linear_functional_on_CX X φ"
shows "continuous_map X euclidean f ⟹ f has_compact_support_on X
⟹ (⋀x. x∈topspace X ⟹ Re (f x) ≥ 0) ⟹ (⋀x. x ∈ topspace X ⟹ f x ∈ ℝ)
⟹ φ (λx∈topspace X. f x) ≥ 0"
by(intro pos_lin_functional_on_CX_pos[OF assms]) (simp_all add: complex_is_Real_iff less_eq_complex_def)
lemma positive_linear_functional_on_CX_compact:
assumes "compact_space X"
shows "positive_linear_functional_on_CX X φ ⟷
(∀f. continuous_map X euclidean f ⟶ (∀x∈topspace X. f x ≥ 0) ⟶ φ (λx∈topspace X. f x) ≥ 0) ∧
(∀f a. continuous_map X euclidean f ⟶ φ (λx∈topspace X. a * f x) = a * φ (λx∈topspace X. f x)) ∧
(∀f g. continuous_map X euclidean f ⟶ continuous_map X euclidean g
⟶ φ (λx∈topspace X. f x + g x) = φ (λx∈topspace X. f x) + φ (λx∈topspace X. g x))"
by(auto simp: positive_linear_functional_on_CX_def assms)
lemma
assumes "positive_linear_functional_on_CX X φ" "compact_space X"
shows pos_lin_functional_on_CX_compact_pos:
"⋀f. continuous_map X euclidean f
⟹ (⋀x. x∈topspace X ⟹ f x ≥ 0) ⟹ φ (λx∈topspace X. f x) ≥ 0"
and pos_lin_functional_on_CX_compact_lin:
"⋀f a. continuous_map X euclidean f
⟹ φ (λx∈topspace X. a * f x) = a * φ (λx∈topspace X. f x)"
"⋀f g. continuous_map X euclidean f ⟹ continuous_map X euclidean g
⟹ φ (λx∈topspace X. f x + g x) = φ (λx∈topspace X. f x) + φ (λx∈topspace X. g x)"
using assms(1) by(auto simp: positive_linear_functional_on_CX_compact assms(2))
lemma pos_lin_functional_on_CX_diff:
fixes f :: "_ ⇒ _ :: {real_normed_vector, ring_1}"
assumes "positive_linear_functional_on_CX X φ"
and cont:"continuous_map X euclidean f" "continuous_map X euclidean g"
and csupp: "f has_compact_support_on X" "g has_compact_support_on X"
shows "φ (λx∈topspace X. f x - g x) = φ (λx∈topspace X. f x) - φ (λx∈topspace X. g x)"
using pos_lin_functional_on_CX_lin(2)[OF assms(1),of f "λx. - g x"] cont csupp
pos_lin_functional_on_CX_lin(1)[OF assms(1) cont(2) csupp(2),of "- 1"] by simp
lemma pos_lin_functional_on_CX_compact_diff:
fixes f :: "_ ⇒ _ :: {real_normed_vector, ring_1}"
assumes "positive_linear_functional_on_CX X φ" "compact_space X"
and "continuous_map X euclidean f" "continuous_map X euclidean g"
shows "φ (λx∈topspace X. f x - g x) = φ (λx∈topspace X. f x) - φ (λx∈topspace X. g x)"
using assms(2) by(auto intro!: pos_lin_functional_on_CX_diff assms)
lemma pos_lin_functional_on_CX_mono:
fixes f :: "_ ⇒ _ :: {real_normed_vector, ring_1, ordered_ab_group_add}"
assumes "positive_linear_functional_on_CX X φ"
and mono:"⋀x. x ∈ topspace X ⟹ f x ≤ g x"
and cont:"continuous_map X euclidean f" "continuous_map X euclidean g"
and csupp: "f has_compact_support_on X" "g has_compact_support_on X"
shows "φ (λx∈topspace X. f x) ≤ φ (λx∈topspace X. g x)"
proof -
have "φ (λx∈topspace X. f x) ≤ φ (λx∈topspace X. f x) + φ (λx∈topspace X. g x - f x)"
by(auto intro!: pos_lin_functional_on_CX_pos[OF assms(1)] assms continuous_map_diff)
also have "... = φ (λx∈topspace X. f x + (g x - f x))"
by(intro pos_lin_functional_on_CX_lin(2)[symmetric]) (auto intro!: assms continuous_map_diff)
also have "... = φ (λx∈topspace X. g x)"
by simp
finally show ?thesis .
qed
lemma pos_lin_functional_on_CX_compact_mono:
fixes f :: "_ ⇒ _ :: {real_normed_vector, ring_1, ordered_ab_group_add}"
assumes "positive_linear_functional_on_CX X φ" "compact_space X"
and "⋀x. x ∈ topspace X ⟹ f x ≤ g x"
and "continuous_map X euclidean f" "continuous_map X euclidean g"
shows "φ (λx∈topspace X. f x) ≤ φ (λx∈topspace X. g x)"
using assms(2) by(auto intro!: assms pos_lin_functional_on_CX_mono)
lemma pos_lin_functional_on_CX_zero:
assumes "positive_linear_functional_on_CX X φ"
shows "φ (λx∈topspace X. 0) = 0"
proof -
have "φ (λx∈topspace X. 0) = φ (λx∈topspace X. 0 * 0)"
by simp
also have "... = 0 * φ (λx∈topspace X. 0)"
by(intro pos_lin_functional_on_CX_lin) (auto simp: assms)
finally show ?thesis
by simp
qed
lemma pos_lin_functional_on_CX_uminus:
fixes f :: "_ ⇒ _ :: {real_normed_vector, ring_1}"
assumes "positive_linear_functional_on_CX X φ"
and "continuous_map X euclidean f"
and csupp: "f has_compact_support_on X"
shows "φ (λx∈topspace X. - f x) = - φ (λx∈topspace X. f x)"
using pos_lin_functional_on_CX_diff[of X φ "λx. 0" f]
by(auto simp: assms pos_lin_functional_on_CX_zero)
lemma pos_lin_functional_on_CX_compact_uminus:
fixes f :: "_ ⇒ _ :: {real_normed_vector, ring_1}"
assumes "positive_linear_functional_on_CX X φ" "compact_space X"
and "continuous_map X euclidean f"
shows "φ (λx∈topspace X. - f x) = - φ (λx∈topspace X. f x)"
using pos_lin_functional_on_CX_diff[of X φ "λx. 0" f]
by(auto simp: assms pos_lin_functional_on_CX_zero)
lemma pos_lin_functional_on_CX_sum:
fixes f :: "_ ⇒ _ ⇒ _ :: {real_normed_vector}"
assumes "positive_linear_functional_on_CX X φ"
and "finite I" "⋀i. i ∈ I ⟹ continuous_map X euclidean (f i)"
and "⋀i. i ∈ I ⟹ f i has_compact_support_on X"
shows "φ (λx∈topspace X. (∑i∈I. f i x)) = (∑i∈I. φ (λx∈topspace X. f i x))"
using assms(2,3,4)
proof induction
case empty
show ?case
using pos_lin_functional_on_CX_zero[OF assms(1)] by(simp add: restrict_def)
next
case ih:(insert a F)
show ?case (is "?lhs = ?rhs")
proof -
have "?lhs = φ (λx∈topspace X. f a x + (∑i∈F. f i x))"
by(simp add: sum.insert_if[OF ih(1)] ih(2) restrict_def)
also have "... = φ (λx∈topspace X. f a x) + φ (λx∈topspace X. (∑i∈F. f i x))"
by (auto intro!: pos_lin_functional_on_CX_lin[OF assms(1)]
has_compact_support_on_sum ih continuous_map_sum)
also have "... = ?rhs"
by(simp add: ih) (simp add: restrict_def)
finally show ?thesis .
qed
qed
lemma pos_lin_functional_on_CX_pos_is_real:
fixes f :: "_ ⇒ complex"
assumes "positive_linear_functional_on_CX X φ"
and "continuous_map X euclidean f" "f has_compact_support_on X"
and "⋀x. x ∈ topspace X ⟹ f x ∈ ℝ"
shows "φ (λx∈topspace X. f x) ∈ ℝ"
proof -
have "φ (λx∈topspace X. f x) = φ (λx∈topspace X. complex_of_real (Re (f x)))"
by (metis (no_types, lifting) assms(4) of_real_Re restrict_ext)
also have "... = φ (λx∈topspace X. complex_of_real (max 0 (Re (f x))) - complex_of_real (max 0 (- Re (f x))))"
by (metis (no_types, opaque_lifting) diff_0 diff_0_right equation_minus_iff max.absorb_iff2 max.order_iff neg_0_le_iff_le nle_le of_real_diff)
also have "... = φ (λx∈topspace X. complex_of_real (max 0 (Re (f x)))) - φ (λx∈topspace X. complex_of_real (max 0 (- Re (f x))))"
using assms by(auto intro!: pos_lin_functional_on_CX_diff continuous_map_real_max)
also have "... ∈ ℝ"
using assms by(intro Reals_diff)
(auto intro!: nonnegative_complex_is_real pos_lin_functional_on_CX_pos[OF assms(1)] continuous_map_real_max
simp: less_eq_complex_def)
finally show ?thesis .
qed
lemma
fixes φ X
defines "φ' ≡ (λf. Re (φ (λx∈topspace X. complex_of_real (f x))))"
assumes plf:"positive_linear_functional_on_CX X φ"
shows pos_lin_functional_on_CX_complex_decompose:
"⋀f. continuous_map X euclidean f ⟹ f has_compact_support_on X
⟹ φ (λx∈topspace X. f x)
= complex_of_real (φ' (λx∈topspace X. Re (f x))) + 𝗂 * complex_of_real (φ' (λx∈topspace X. Im (f x)))"
and pos_lin_functional_on_CX_complex_decompose_plf:
"positive_linear_functional_on_CX X φ'"
proof -
fix f :: "_ ⇒ complex"
assume f:"continuous_map X euclidean f" "f has_compact_support_on X"
show "φ (λx∈topspace X. f x)
= complex_of_real (φ' (λx∈topspace X. Re (f x))) + 𝗂 * complex_of_real (φ' (λx∈topspace X. Im (f x)))"
(is "?lhs = ?rhs")
proof -
have "φ (λx∈topspace X. f x) = φ (λx∈topspace X. Re (f x) + 𝗂 * Im (f x))"
using complex_eq by presburger
also have "... = φ (λx∈topspace X. complex_of_real (Re (f x))) + φ (λx∈topspace X. 𝗂 * complex_of_real (Im (f x)))"
using f by(auto intro!: pos_lin_functional_on_CX_lin[OF plf] has_compact_support_on_mult_left continuous_map_complex_mult_left)
also have "... = φ (λx∈topspace X. complex_of_real (Re (f x))) + 𝗂 * φ (λx∈topspace X. complex_of_real (Im (f x)))"
using f by(auto intro!: pos_lin_functional_on_CX_lin[OF plf])
also have "... = complex_of_real (φ' (λx∈topspace X. (Re (f x)))) + 𝗂 * complex_of_real (φ' (λx∈topspace X. Im (f x)))"
proof -
have [simp]: "complex_of_real (φ' (λx∈topspace X. Re (f x))) = φ (λx∈topspace X. complex_of_real (Re (f x)))"
(is "?l = ?r")
proof -
have "?l = complex_of_real (Re (φ (λx∈topspace X. complex_of_real (Re (f x)))))"
by (metis (mono_tags, lifting) φ'_def restrict_apply' restrict_ext)
also have "... = ?r"
by(intro of_real_Re pos_lin_functional_on_CX_pos_is_real[OF plf]) (use f in auto)
finally show ?thesis .
qed
have [simp]: "complex_of_real (φ' (λx∈topspace X. Im (f x))) = φ (λx∈topspace X. complex_of_real (Im (f x)))"
(is "?l = ?r")
proof -
have "?l = complex_of_real (Re (φ (λx∈topspace X. complex_of_real (Im (f x)))))"
by (metis (mono_tags, lifting) φ'_def restrict_apply' restrict_ext)
also have "... = ?r"
by(intro of_real_Re pos_lin_functional_on_CX_pos_is_real[OF plf]) (use f in auto)
finally show ?thesis .
qed
show ?thesis by simp
qed
finally show ?thesis .
qed
next
show "positive_linear_functional_on_CX X φ'"
unfolding positive_linear_functional_on_CX_def
proof safe
fix f
assume f:"continuous_map X euclideanreal f" "f has_compact_support_on X" "∀x∈topspace X. 0 ≤ f x"
show "φ' (λx∈topspace X. f x) ≥ 0"
proof -
have "0 ≤ φ (λx∈topspace X. complex_of_real (f x))"
using f by(intro pos_lin_functional_on_CX_pos[OF plf]) (simp_all add: less_eq_complex_def)
hence "0 ≤ Re (φ (λx∈topspace X. complex_of_real (f x)))"
by (simp add: less_eq_complex_def)
also have "... = φ' (λx∈topspace X. f x)"
by (metis (mono_tags, lifting) φ'_def restrict_apply' restrict_ext)
finally show ?thesis .
qed
next
fix a f
assume f:"continuous_map X euclideanreal f" "f has_compact_support_on X"
show "φ' (λx∈topspace X. a * f x) = a * φ' (λx∈topspace X. f x)"
proof -
have *:"φ (λx∈topspace X. complex_of_real a * complex_of_real (f x)) = complex_of_real a * φ (λx∈topspace X. complex_of_real (f x))"
using f by(auto intro!: pos_lin_functional_on_CX_lin[OF plf])
have "φ' (λx∈topspace X. a * f x) = Re (φ (λx∈topspace X. complex_of_real a * complex_of_real (f x)))"
by (metis (mono_tags, lifting) φ'_def of_real_mult restrict_apply' restrict_ext)
also have "... = a * (Re (φ (λx∈topspace X. complex_of_real (f x))))"
unfolding * by simp
also have "... = a * φ' (λx∈topspace X. f x)"
by (metis (mono_tags, lifting) φ'_def restrict_apply' restrict_ext)
finally show ?thesis .
qed
next
fix f g
assume fg:"continuous_map X euclideanreal f" "f has_compact_support_on X"
"continuous_map X euclideanreal g" "g has_compact_support_on X"
show "φ' (λx∈topspace X. f x + g x) = φ' (λx∈topspace X. f x) + φ' (λx∈topspace X. g x)"
proof -
have *: "φ (λx∈topspace X. complex_of_real (f x) + complex_of_real (g x)) = φ (λx∈topspace X. complex_of_real (f x)) + φ (λx∈topspace X. complex_of_real (g x))"
using fg by(auto intro!: pos_lin_functional_on_CX_lin[OF plf])
have "φ' (λx∈topspace X. f x + g x) = Re (φ (λx∈topspace X. complex_of_real (f x + g x)))"
by (metis (mono_tags, lifting) φ'_def restrict_apply' restrict_ext)
also have "... = Re (φ (λx∈topspace X. complex_of_real (f x)) + φ (λx∈topspace X. complex_of_real (g x)))"
unfolding of_real_add * by simp
also have "... = Re (φ (λx∈topspace X. complex_of_real (f x))) + Re (φ (λx∈topspace X. complex_of_real (g x)))"
by simp
also have "... = φ' (λx∈topspace X. f x) + φ' (λx∈topspace X. g x)"
by (metis (mono_tags, lifting) φ'_def restrict_apply' restrict_ext)
finally show ?thesis .
qed
qed
qed
subsection ‹ Lemmas for Uniqueness ›
lemma rep_measures_real_unique:
assumes "locally_compact_space X" "Hausdorff_space X"
assumes N: "subalgebra N (borel_of X)"
"⋀f. continuous_map X euclideanreal f ⟹ f has_compact_support_on X ⟹ integrable N f"
"⋀A. A∈sets N ⟹ emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C)"
"⋀A. openin X A ⟹ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K)"
"⋀A. A∈sets N ⟹ emeasure N A < ∞ ⟹ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K)"
"⋀K. compactin X K ⟹ N K < ∞"
assumes M: "subalgebra M (borel_of X)"
"⋀f. continuous_map X euclideanreal f ⟹ f has_compact_support_on X ⟹ integrable M f"
"⋀A. A∈sets M ⟹ emeasure M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure M C)"
"⋀A. openin X A ⟹ emeasure M A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure M K)"
"⋀A. A∈sets M ⟹ emeasure M A < ∞ ⟹ emeasure M A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure M K)"
"⋀K. compactin X K ⟹ M K < ∞"
and sets_eq: "sets N = sets M"
and integ_eq: "⋀f. continuous_map X euclideanreal f ⟹ f has_compact_support_on X ⟹ (∫x. f x ∂N) = (∫x. f x ∂M)"
shows "N = M"
proof(intro measure_eqI sets_eq)
have space_N: "space N = topspace X" and space_M: "space M = topspace X"
using N(1) M(1) by(auto simp: subalgebra_def space_borel_of)
have "N K = M K" if K:"compactin X K" for K
proof -
have kc: "kc_space X"
using Hausdorff_imp_kc_space assms(2) by blast
have K_sets[measurable]: "K ∈ sets N" "K ∈ sets M"
using N(1) M(1) compactin_imp_closedin_gen[OF kc K]
by(auto simp: borel_of_closed subalgebra_def)
show ?thesis
proof(rule antisym[OF ennreal_le_epsilon ennreal_le_epsilon])
fix e :: real
assume e: "e > 0"
show "emeasure N K ≤ emeasure M K + ennreal e"
proof -
have "emeasure M K ≥ ⨅ (emeasure M ` {C. openin X C ∧ K ⊆ C})"
by(simp add: M(3)[OF K_sets(2)])
from Inf_le_iff[THEN iffD1,OF this,rule_format,of "emeasure M K + e"]
obtain U where U:"openin X U" "K ⊆ U" "emeasure M U < emeasure M K + ennreal e"
using K M(6) e by fastforce
then have [measurable]: "U ∈ sets M"
using M(1) by(auto simp: subalgebra_def borel_of_open)
then obtain f where f:"continuous_map X (top_of_set {0..1::real}) f"
"f ` (topspace X - U) ⊆ {0}" "f ` K ⊆ {1}"
"disjnt (X closure_of {x ∈ topspace X. f x ≠ 0}) (topspace X - U)"
"compactin X (X closure_of {x ∈ topspace X. f x ≠ 0})"
using Urysohn_locally_compact_Hausdorff_closed_compact_support[OF assms(1) disjI1[OF assms(2)],of 0 1 "topspace X - U" K] U K
by(simp add: closedin_def disjnt_iff) blast
have f_int: "integrable N f" "integrable M f"
using f by(auto intro!: N M simp: continuous_map_in_subtopology has_compact_support_on_iff)
have f_01: "x ∈ topspace X ⟹ 0 ≤ f x" "x ∈ topspace X ⟹ f x ≤ 1" for x
using continuous_map_image_subset_topspace[OF f(1)] by auto
have "emeasure N K = (∫⇧+x. indicator K x ∂N)"
by simp
also have "... ≤ (∫⇧+x. f x ∂N)"
using f(3) by(intro nn_integral_mono) (auto simp: indicator_def)
also have "... = ennreal (∫x. f x ∂N)"
by(rule nn_integral_eq_integral) (use f_int continuous_map_image_subset_topspace[OF f(1)] f_01 space_N in auto)
also have "... = ennreal (∫x. f x ∂M)"
using f by(auto intro!: ennreal_cong integ_eq simp: continuous_map_in_subtopology has_compact_support_on_iff)
also have "... = (∫⇧+x. f x ∂M)"
by(rule nn_integral_eq_integral[symmetric])
(use f_int continuous_map_image_subset_topspace[OF f(1)] f_01 space_M in auto)
also have "... ≤ (∫⇧+x. indicator U x ∂M)"
using f(2) f_01 by(intro nn_integral_mono) (auto simp: indicator_def space_M)
also have "... = emeasure M U"
by simp
also have "... < emeasure M K + ennreal e"
by fact
finally show ?thesis
by simp
qed
next
fix e :: real
assume e: "e > 0"
show "emeasure M K ≤ emeasure N K + ennreal e"
proof -
have "emeasure N K ≥ ⨅ (emeasure N ` {C. openin X C ∧ K ⊆ C})"
by(simp add: N(3)[OF K_sets(1)])
from Inf_le_iff[THEN iffD1,OF this,rule_format,of "emeasure N K + e"]
obtain U where U:"openin X U" "K ⊆ U" "emeasure N U < emeasure N K + ennreal e"
using K N(6) e by fastforce
then have [measurable]: "U ∈ sets N"
using N(1) by(auto simp: subalgebra_def borel_of_open)
then obtain f where f:"continuous_map X (top_of_set {0..1::real}) f"
"f ` (topspace X - U) ⊆ {0}" "f ` K ⊆ {1}"
"disjnt (X closure_of {x ∈ topspace X. f x ≠ 0}) (topspace X - U)"
"compactin X (X closure_of {x ∈ topspace X. f x ≠ 0})"
using Urysohn_locally_compact_Hausdorff_closed_compact_support[OF assms(1) disjI1[OF assms(2)],of 0 1 "topspace X - U" K] U K
by(simp add: closedin_def disjnt_iff) blast
have f_int: "integrable N f" "integrable M f"
using f by(auto intro!: N M simp: continuous_map_in_subtopology has_compact_support_on_iff)
have f_01: "x ∈ topspace X ⟹ 0 ≤ f x" "x ∈ topspace X ⟹ f x ≤ 1" for x
using continuous_map_image_subset_topspace[OF f(1)] by auto
have "emeasure M K = (∫⇧+x. indicator K x ∂M)"
by simp
also have "... ≤ (∫⇧+x. f x ∂M)"
using f(3) by(intro nn_integral_mono) (auto simp: indicator_def)
also have "... = ennreal (∫x. f x ∂M)"
by(rule nn_integral_eq_integral) (use f_int continuous_map_image_subset_topspace[OF f(1)] f_01 space_M in auto)
also have "... = ennreal (∫x. f x ∂N)"
using f by(auto intro!: ennreal_cong integ_eq[symmetric] simp: continuous_map_in_subtopology has_compact_support_on_iff)
also have "... = (∫⇧+x. f x ∂N)"
by(rule nn_integral_eq_integral[symmetric])
(use f_int continuous_map_image_subset_topspace[OF f(1)] f_01 space_N in auto)
also have "... ≤ (∫⇧+x. indicator U x ∂N)"
using f(2) f_01 by(intro nn_integral_mono) (auto simp: indicator_def space_N)
also have "... = emeasure N U"
by simp
also have "... < emeasure N K + ennreal e"
by fact
finally show ?thesis
by simp
qed
qed
qed
hence "⋀A. openin X A ⟹ emeasure N A = emeasure M A"
by(auto simp: N(4) M(4))
thus "⋀A. A ∈ sets N ⟹ emeasure N A = emeasure M A"
using N(3) M(3) by(auto simp: sets_eq)
qed
lemma rep_measures_complex_unique:
fixes X :: "'a topology"
assumes "locally_compact_space X" "Hausdorff_space X"
assumes N: "subalgebra N (borel_of X)"
"⋀f. continuous_map X euclidean f ⟹ f has_compact_support_on X ⟹ complex_integrable N f"
"⋀A. A∈sets N ⟹ emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C)"
"⋀A. openin X A ⟹ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K)"
"⋀A. A∈sets N ⟹ emeasure N A < ∞ ⟹ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K)"
"⋀K. compactin X K ⟹ N K < ∞"
assumes M: "subalgebra M (borel_of X)"
"⋀f. continuous_map X euclidean f ⟹ f has_compact_support_on X ⟹ complex_integrable M f"
"⋀A. A∈sets M ⟹ emeasure M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure M C)"
"⋀A. openin X A ⟹ emeasure M A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure M K)"
"⋀A. A∈sets M ⟹ emeasure M A < ∞ ⟹ emeasure M A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure M K)"
"⋀K. compactin X K ⟹ M K < ∞"
and sets_eq: "sets N = sets M"
and integ_eq: "⋀f::'a ⇒ complex. continuous_map X euclidean f ⟹ f has_compact_support_on X
⟹ (∫x. f x ∂N) = (∫x. f x ∂M)"
shows "N = M"
proof(rule rep_measures_real_unique[OF assms(1,2)])
fix f
assume f:"continuous_map X euclideanreal f" "f has_compact_support_on X"
show "(∫x. f x ∂N) = (∫x. f x ∂M)"
proof -
have "(∫x. f x ∂N) = Re (∫x. (complex_of_real (f x)) ∂N)"
by simp
also have "... = Re (∫x. (complex_of_real (f x)) ∂M)"
proof -
have 1:"(∫x. (complex_of_real (f x)) ∂N) = (∫x. (complex_of_real (f x)) ∂M)"
by(rule integ_eq) (auto intro!: f)
show ?thesis
unfolding 1 by simp
qed
finally show ?thesis
by simp
qed
next
fix f
assume "continuous_map X euclideanreal f" "f has_compact_support_on X"
hence "complex_integrable N (λx. complex_of_real (f x))" "complex_integrable M (λx. complex_of_real (f x))"
by (auto intro!: M N)
thus "integrable N f" "integrable M f"
using complex_of_real_integrable_eq by auto
qed fact+
lemma finite_tight_measure_eq:
assumes "locally_compact_space X" "metrizable_space X" "tight_on X N" "tight_on X M"
and integ_eq: "⋀f. continuous_map X euclideanreal f ⟹ f ∈ topspace X → {0..1} ⟹ (∫x. f x ∂N) = (∫x. f x ∂M)"
shows "N = M"
proof(rule measure_eqI)
interpret N: finite_measure N
using assms(3) tight_on_def by blast
interpret M: finite_measure M
using assms(4) tight_on_def by blast
have integ_N: "⋀A. A ∈ sets N ⟹ integrable N (indicat_real A)"
and integ_M: "⋀A. A ∈ sets M ⟹ integrable M (indicat_real A)"
by (auto simp add: N.emeasure_eq_measure M.emeasure_eq_measure)
have sets_N: "sets N = borel_of X" and space_N: "space N = topspace X"
and sets_M: "sets M = borel_of X" and space_M: "space M = topspace X"
using assms(3,4) sets_eq_imp_space_eq[of _ "borel_of X"]
by(auto simp: tight_on_def space_borel_of)
fix A
assume [measurable]:"A ∈ sets N"
then have [measurable]: "A ∈ sets M"
using sets_M sets_N by blast
have "measure M A = ⨆ (Sigma_Algebra.measure M ` {K. compactin X K ∧ K ⊆ A})"
by(auto intro!: inner_regular''[OF assms(2,4)])
also have "... = ⨆ (Sigma_Algebra.measure N ` {K. compactin X K ∧ K ⊆ A})"
proof -
have "measure M K = measure N K" if K:"compactin X K" "K ⊆ A" for K
proof -
have [measurable]: "K ∈ sets M" "K ∈ sets N"
by(auto simp: sets_M sets_N intro!: borel_of_closed compactin_imp_closedin K metrizable_imp_Hausdorff_space assms)
show ?thesis
proof(rule antisym[OF field_le_epsilon field_le_epsilon])
fix e :: real
assume e:"e > 0"
have "∀y>measure N K. ∃a∈measure N ` {C. openin X C ∧ K ⊆ C}. a < y"
by(intro cInf_le_iff[THEN iffD1] eq_refl[OF N.outer_regularD[OF N.outer_regular'[OF assms(2) sets_N[symmetric]],symmetric]])
(auto intro!: bdd_belowI[where m=0] compactin_subset_topspace[OF K(1)])
from this[rule_format,of "measure N K + e"] obtain U where U: "openin X U" "K ⊆ U" "measure N U < measure N K + e"
using e by auto
then have [measurable]: "U ∈ sets M" "U ∈ sets N"
by(auto simp: sets_N sets_M intro!: borel_of_open)
obtain f where f:"continuous_map X (top_of_set {0..1::real}) f"
"f ` (topspace X - U) ⊆ {0}" "f ` K ⊆ {1}"
"disjnt (X closure_of {x ∈ topspace X. f x ≠ 0}) (topspace X - U)"
"compactin X (X closure_of {x ∈ topspace X. f x ≠ 0})"
using Urysohn_locally_compact_Hausdorff_closed_compact_support[OF assms(1) disjI1[OF metrizable_imp_Hausdorff_space[OF assms(2)]],of 0 1 "topspace X - U" K] U K
by(simp add: closedin_def disjnt_iff) blast
hence f': "continuous_map X euclideanreal f"
"⋀x. x ∈ topspace X ⟹ f x ≥ 0" "⋀x. x ∈ topspace X ⟹ f x ≤ 1"
by (auto simp add: continuous_map_in_subtopology)
have [measurable]: "f ∈ borel_measurable M" "f ∈ borel_measurable N"
using continuous_map_measurable[OF f'(1)]
by(auto simp: borel_of_euclidean sets_N sets_M cong: measurable_cong_sets)
from f'(2,3) have f_int[simp]: "integrable M f" "integrable N f"
by(auto intro!: M.integrable_const_bound[where B=1] N.integrable_const_bound[where B=1] simp: space_N space_M)
have "measure M K = (∫x. indicator K x ∂M)"
by simp
also have "... ≤ (∫x. f x ∂M)"
using f(3) f'(2) by(intro integral_mono integ_M) (auto simp: space_M indicator_def)
also have "... = (∫x. f x ∂N)"
by(auto intro!: integ_eq[symmetric] f')
also have "... ≤ (∫x. indicator U x ∂N)"
using f(2) f'(3) by(intro integral_mono integ_N) (auto simp: space_N indicator_def)
also have "... ≤ measure N K + e"
using U(3) by fastforce
finally show "measure M K ≤ measure N K + e" .
next
fix e :: real
assume e:"e > 0"
have "∀y>measure M K. ∃a∈measure M ` {C. openin X C ∧ K ⊆ C}. a < y"
by(intro cInf_le_iff[THEN iffD1] eq_refl[OF M.outer_regularD[OF M.outer_regular'[OF assms(2) sets_M[symmetric]],symmetric]])
(auto intro!: bdd_belowI[where m=0] compactin_subset_topspace[OF K(1)])
from this[rule_format,of "measure M K + e"] obtain U where U: "openin X U" "K ⊆ U" "measure M U < measure M K + e"
using e by auto
then have [measurable]: "U ∈ sets M" "U ∈ sets N"
by(auto simp: sets_N sets_M intro!: borel_of_open)
obtain f where f:"continuous_map X (top_of_set {0..1::real}) f"
"f ` (topspace X - U) ⊆ {0}" "f ` K ⊆ {1}"
"disjnt (X closure_of {x ∈ topspace X. f x ≠ 0}) (topspace X - U)"
"compactin X (X closure_of {x ∈ topspace X. f x ≠ 0})"
using Urysohn_locally_compact_Hausdorff_closed_compact_support[OF assms(1) disjI1[OF metrizable_imp_Hausdorff_space[OF assms(2)]],of 0 1 "topspace X - U" K] U K
by(simp add: closedin_def disjnt_iff) blast
hence f': "continuous_map X euclideanreal f"
"⋀x. x ∈ topspace X ⟹ f x ≥ 0" "⋀x. x ∈ topspace X ⟹ f x ≤ 1"
by (auto simp add: continuous_map_in_subtopology)
have [measurable]: "f ∈ borel_measurable M" "f ∈ borel_measurable N"
using continuous_map_measurable[OF f'(1)]
by(auto simp: borel_of_euclidean sets_N sets_M cong: measurable_cong_sets)
from f'(2,3) have f_int[simp]: "integrable M f" "integrable N f"
by(auto intro!: M.integrable_const_bound[where B=1] N.integrable_const_bound[where B=1] simp: space_N space_M)
have "measure N K = (∫x. indicator K x ∂N)"
by simp
also have "... ≤ (∫x. f x ∂N)"
using f(3) f'(2) by(intro integral_mono integ_N) (auto simp: space_N indicator_def)
also have "... = (∫x. f x ∂M)"
by(auto intro!: integ_eq f')
also have "... ≤ (∫x. indicator U x ∂M)"
using f(2) f'(3) by(intro integral_mono integ_M) (auto simp: space_M indicator_def)
also have "... ≤ measure M K + e"
using U(3) by fastforce
finally show "measure N K ≤ measure M K + e" .
qed
qed
thus ?thesis
by simp
qed
also have "... = measure N A"
by(auto intro!: inner_regular''[symmetric,OF assms(2,3)])
finally show "emeasure N A = emeasure M A"
using M.emeasure_eq_measure N.emeasure_eq_measure by presburger
qed(insert assms(3,4), auto simp: tight_on_def)
subsection ‹ Riesez Representation Theorem for Real Numbers ›
theorem Riesz_representation_real_complete:
fixes X :: "'a topology" and φ :: "('a ⇒ real) ⇒ real"
assumes lh:"locally_compact_space X" "Hausdorff_space X"
and plf:"positive_linear_functional_on_CX X φ"
shows "∃M. ∃!N. sets N = M ∧ subalgebra N (borel_of X)
∧ (∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))
∧ (∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀A∈sets N. emeasure N A < ∞
⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀K. compactin X K ⟶ emeasure N K < ∞)
∧ (∀f. continuous_map X euclideanreal f ⟶ f has_compact_support_on X ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))
∧ (∀f. continuous_map X euclideanreal f ⟶ f has_compact_support_on X ⟶ integrable N f)
∧ complete_measure N"
proof -
let ?iscont = "λf. continuous_map X euclideanreal f"
let ?csupp = "λf. f has_compact_support_on X"
let ?fA = "λA f. ?iscont f ∧ ?csupp f ∧ X closure_of {x∈topspace X. f x ≠ 0} ⊆ A
∧ f ∈ topspace X → {0..1} ∧ f ∈ topspace X - A → {0}"
let ?fK = "λK f. ?iscont f ∧ ?csupp f ∧ f ∈ topspace X → {0..1} ∧ f ∈ K → {1}"
have ext_sup[simp]:
"⋀P Q. {x∈topspace X. (if x ∈ topspace X then P x else Q x) ≠ 0} = {x∈topspace X. P x ≠ 0}"
by fastforce
have times_unfold[simp]: "⋀P Q. {x∈topspace X. P x ∧ Q x} = {x∈topspace X. P x} ∩ {x∈topspace X. Q x}"
by fastforce
note pos = pos_lin_functional_on_CX_pos[OF plf]
note linear = pos_lin_functional_on_CX_lin[OF plf]
note φdiff = pos_lin_functional_on_CX_diff[OF plf]
note φmono = pos_lin_functional_on_CX_mono[OF plf]
note φ_0 = pos_lin_functional_on_CX_zero[OF plf]
text ‹ Lemma 2.13~\cite{Rudin}.›
have fApartition: "∃hi. (∀i≤n. (?fA (Vi i) (hi i))) ∧
(∀x∈K. (∑i≤n. hi i x) = 1) ∧ (∀x∈topspace X. 0 ≤ (∑i≤n. hi i x)) ∧
(∀x∈topspace X. (∑i≤n. hi i x) ≤ 1)"
if K:"compactin X K" "⋀i::nat. i ≤ n ⟹ openin X (Vi i)" "K ⊆ (⋃i≤n. Vi i)" for K Vi n
proof -
{
fix x
assume x:"x ∈ K"
have "∃i≤n. x ∈ Vi i ∧ (∃U V. openin X U ∧ (compactin X V) ∧ x ∈ U ∧ U ⊆ V ∧ V ⊆ Vi i)"
proof -
obtain i where i: "i ≤ n" "x ∈ Vi i"
using K x by blast
thus ?thesis
using locally_compact_space_neighbourhood_base[of X] neighbourhood_base_of[of "λU. compactin X U" X] lh K
by(fastforce intro!: exI[where x=i])
qed
}
hence "∃ix Ux Vx. ∀x∈K. ix x ≤ n ∧ x ∈ Vi (ix x) ∧ openin X (Ux x) ∧
compactin X (Vx x) ∧ x ∈ Ux x ∧ Ux x ⊆ Vx x ∧ Vx x ⊆ Vi (ix x)"
by metis
then obtain ix Ux Vx where xinK: "⋀x. x ∈ K ⟹ ix x ≤ n" "⋀x. x ∈ K ⟹ x ∈ Vi (ix x)"
"⋀x. x ∈ K ⟹ openin X (Ux x)" "⋀x. x ∈ K ⟹ compactin X (Vx x)" "⋀x. x ∈ K ⟹ x ∈ Ux x"
"⋀x. x ∈ K ⟹ Ux x ⊆ Vx x" "⋀x. x ∈ K ⟹ Vx x ⊆ Vi (ix x)"
by blast
hence "K ⊆ (⋃x∈K. Ux x)"
by fastforce
from compactinD[OF K(1) _ this] xinK(3) obtain K' where K': "finite K'" "K' ⊆ K" "K ⊆ (⋃x∈K'. Ux x)"
by (metis (no_types, lifting) finite_subset_image imageE)
define Hi where "Hi ≡ (λi. ⋃ (Vx ` {x. x ∈ K' ∧ ix x = i}))"
have Hi_Vi: "⋀i. i ≤ n ⟹ Hi i ⊆ Vi i"
using xinK K' by(fastforce simp: Hi_def)
have K_unHi: "K ⊆ (⋃i≤n. Hi i)"
proof
fix x
assume "x ∈ K"
then obtain y where y:"y ∈ K'" "x ∈ Ux y"
using K' by auto
then have "x ∈ Vx y" "ix y ≤ n"
using K' xinK[of y] by auto
with y show "x ∈ (⋃i≤n. Hi i)"
by(fastforce simp: Hi_def)
qed
have compactin_Hi: "⋀i. i ≤ n ⟹ compactin X (Hi i)"
using xinK K' by(auto intro!: compactin_Union simp: Hi_def)
{
fix i
assume "i ∈ {..n}"
then have i: "i ≤ n" by auto
have "closedin X (topspace X - Vi i)" "disjnt (topspace X - Vi i) (Hi i)"
using Hi_Vi[OF i] K(2)[OF i] by (auto simp: disjnt_def)
from Urysohn_locally_compact_Hausdorff_closed_compact_support[of _ 0 1,OF lh(1) disjI1[OF lh(2)] _ this(1) compactin_Hi[OF i] this(2)]
have "∃hi. continuous_map X (top_of_set {0..1::real}) hi ∧ hi ` (topspace X - Vi i) ⊆ {0} ∧
hi ` Hi i ⊆ {1} ∧ disjnt (X closure_of {x∈topspace X. hi x ≠ 0}) (topspace X - Vi i) ∧
?csupp hi"
unfolding has_compact_support_on_iff by fastforce
hence "∃hi. ?iscont hi ∧ hi ` topspace X ⊆ {0..1} ∧ hi ` (topspace X - Vi i) ⊆ {0} ∧
hi ` Hi i ⊆ {1} ∧ disjnt (X closure_of {x∈topspace X. hi x ≠ 0}) (topspace X - Vi i) ∧
?csupp hi"
by (auto simp add: continuous_map_in_subtopology disjnt_def has_compact_support_on_def)
}
hence "∃hi. ∀i∈{..n}. ?iscont (hi i) ∧ hi i ` topspace X ⊆ {0..1} ∧
hi i ` (topspace X - Vi i) ⊆ {0} ∧ hi i ` Hi i ⊆ {1} ∧
disjnt (X closure_of {x∈topspace X. hi i x ≠ 0}) (topspace X - Vi i) ∧ ?csupp (hi i)"
by(intro bchoice) auto
hence "∃hi. ∀i≤n. ?iscont (hi i) ∧ hi i ` topspace X ⊆ {0..1} ∧ hi i ` (topspace X - Vi i) ⊆ {0} ∧
hi i ` Hi i ⊆ {1} ∧ disjnt (X closure_of {x∈topspace X. hi i x ≠ 0}) (topspace X - Vi i) ∧ ?csupp (hi i)"
by (meson atMost_iff)
then obtain gi where gi: "⋀i. i ≤ n ⟹ ?iscont (gi i)"
"⋀i. i ≤ n ⟹ gi i ` topspace X ⊆ {0..1}" "⋀i. i ≤ n ⟹ gi i ` (topspace X - Vi i) ⊆ {0}"
"⋀i. i ≤ n ⟹ gi i ` Hi i ⊆ {1}"
"⋀i. i ≤ n ⟹ disjnt (X closure_of {x∈topspace X. gi i x ≠ 0}) (topspace X - Vi i)"
"⋀i. i ≤ n ⟹ ?csupp (gi i)"
by fast
define hi where "hi ≡ (λn. λx∈topspace X. (∏i<n. (1 - gi i x)) * gi n x)"
show ?thesis
proof(safe intro!: exI[where x=hi])
fix i
assume i: "i ≤ n"
then show "?iscont (hi i)"
using gi(1) by(auto simp: hi_def intro!: continuous_map_real_mult continuous_map_prod continuous_map_diff)
show "?csupp (hi i)"
proof -
have "{x ∈ topspace X. hi i x ≠ 0} = {x∈topspace X. gi i x ≠ 0} ∩ (⋂j<i. {x∈topspace X. gi j x ≠ 1})"
using gi by(auto simp: hi_def)
also have "... ⊆ {x∈topspace X. gi i x ≠ 0}"
by blast
finally show ?thesis
using gi(6)[OF i] closure_of_mono closed_compactin
by(fastforce simp: has_compact_support_on_iff)
qed
next
fix i x
assume i: "i ≤ n" and x: "x ∈ topspace X"
{
assume "x ∉ Vi i"
with i x gi(3)[of i] show "hi i x = 0"
by(auto simp: hi_def)
}
show "hi i x ∈ {0..1}"
using i x gi(2) by(auto simp: hi_def image_subset_iff intro!: mult_nonneg_nonneg mult_le_one prod_le_1 prod_nonneg)
next
fix x
have 1:"(∑i≤n. hi i x) = 1 - (∏i≤n. (1 - gi i x))" if x:"x ∈ topspace X"
proof -
have "(∑i≤n. hi i x) = (∑j≤n. (∏i<j. (1 - gi i x)) * gi j x)"
using x by (simp add: hi_def)
also have "... = 1 - (∏i≤n. (1 - gi i x))"
proof -
have [simp]: "(∏i<m. 1 - gi i x) * (1 - gi m x) = (∏i≤m. 1 - gi i x)" for m
by (metis lessThan_Suc_atMost prod.lessThan_Suc)
show ?thesis
by(induction n, simp_all) (simp add: right_diff_distrib)
qed
finally show ?thesis .
qed
{
assume x:"x ∈ K"
then obtain i where i: "i ≤ n" "x ∈ Hi i"
using K_unHi by auto
have "x ∈ topspace X"
using K(1) x compactin_subset_topspace by auto
hence "(∑i≤n. hi i x) = 1 - (∏i≤n. (1 - gi i x))"
by(simp add: 1)
also have "... = 1"
using i gi(4)[OF i(1)] by(auto intro!: prod_zero bexI[where x=i])
finally show "(∑i≤n. hi i x) = 1" .
}
assume x: "x ∈ topspace X"
then show "0 ≤ (∑i≤n. hi i x)" "(∑i≤n. hi i x) ≤ 1"
using gi(2) by(auto simp: 1 image_subset_iff intro!: prod_nonneg prod_le_1)
next
fix i x
assume h:"i ≤ n" "x ∈ X closure_of {x ∈ topspace X. hi i x ≠ 0}"
have "{x ∈ topspace X. hi i x ≠ 0} = {x∈topspace X. gi i x ≠ 0} ∩ (⋂j<i. {x∈topspace X. gi j x ≠ 1})"
using gi by(auto simp: hi_def)
also have "... ⊆ {x∈topspace X. gi i x ≠ 0}"
by blast
finally have "X closure_of {x ∈ topspace X. hi i x ≠ 0} ⊆ X closure_of {x∈topspace X. gi i x ≠ 0}"
by(rule closure_of_mono)
thus "x ∈ Vi i"
using gi(5)[OF h(1)] h(2) closure_of_subset_topspace by(fastforce simp: disjnt_def)
qed
qed
note [simp, intro!] = continuous_map_add continuous_map_diff continuous_map_real_mult
define μ' where "μ' ≡ (λA. ⨆ (ennreal ` φ ` {(λx∈topspace X. f x) |f. ?fA A f}))"
define μ where "μ ≡ (λA. ⨅ (μ' ` {V. A ⊆ V ∧ openin X V}))"
define Mf where "Mf ≡ {E. E ⊆ topspace X ∧ μ E < ⊤ ∧ μ E = (⨆ (μ ` {K. K ⊆ E ∧ compactin X K}))}"
define M where "M ≡ {E. E ⊆ topspace X ∧ (∀K. compactin X K ⟶ E ∩ K ∈ Mf)}"
have μ'_mono: "⋀A B. A ⊆ B ⟹ μ' A ≤ μ' B"
unfolding μ'_def by(fastforce intro!: SUP_subset_mono imageI)
have μ_open: "μ A = μ' A" if "openin X A" for A
unfolding μ_def by (metis (mono_tags, lifting) INF_eqI μ'_mono dual_order.refl mem_Collect_eq that)
have μ_mono: "⋀A B. A ⊆ B ⟹ μ A ≤ μ B"
unfolding μ_def by(auto intro!: INF_superset_mono)
have μ_fin_subset: "μ A < ∞ ⟹ A ⊆ topspace X" for A
by (metis (mono_tags, lifting) INF_less_iff μ_def mem_Collect_eq openin_subset order.trans)
have μ'_empty: "μ' {} = 0" and μ_empty: "μ {} = 0"
proof -
have 1:"{(λx∈topspace X. f x) |f. ?fA {} f} = {λx∈topspace X. 0}"
by(fastforce intro!: exI[where x="λx∈topspace X. 0"])
thus "μ' {} = 0" "μ {} = 0"
by(auto simp: μ'_def φ_0 μ_open)
qed
have empty_in_Mf: "{} ∈ Mf"
by(auto simp: Mf_def μ_empty)
have step1: "μ (⋃ (range Ei)) ≤ (∑i. μ (Ei i))" for Ei
proof -
have 1: "μ' (V ∪ U) ≤ μ' V + μ' U" if VU: "openin X V" "openin X U" for V U
proof -
have "μ' (V ∪ U) = ⨆ (ennreal ` φ ` {(λx∈topspace X. f x) |f. ?fA (V ∪ U) f})"
by(simp add: μ'_def)
also have "... ≤ μ' V + μ' U"
unfolding Sup_le_iff
proof safe
fix g
assume g: "?iscont g" "?csupp g" "g ∈ topspace X → {0..1}" "g ∈ topspace X - (V ∪ U) → {0}"
"X closure_of {x ∈ topspace X. g x ≠ 0} ⊆ V ∪ U"
have "∃hi. (∀i≤Suc 0. ?iscont (hi i) ∧ ?csupp (hi i) ∧
X closure_of {x ∈ topspace X. hi i x ≠ 0} ⊆ (case i of 0 ⇒ V | Suc _ ⇒ U) ∧
hi i ∈ topspace X → {0..1} ∧
hi i ∈ topspace X - (case i of 0 ⇒ V | Suc _ ⇒ U) → {0}) ∧
(∀x∈X closure_of {x∈topspace X. g x ≠ 0}. (∑i≤Suc 0. hi i x) = 1) ∧
(∀x∈topspace X. 0 ≤ (∑i≤Suc 0. hi i x)) ∧ (∀x∈topspace X. (∑i≤Suc 0. hi i x) ≤ 1)"
proof(safe intro!: fApartition[of _ "Suc 0" "λi. case i of 0 ⇒ V | _ ⇒ U"])
have 1:"(⋃i≤Suc 0. case i of 0 ⇒ V | Suc _ ⇒ U) = U ∪ V"
by(fastforce simp: le_Suc_eq)
show "⋀x. x ∈ X closure_of {x ∈ topspace X. g x ≠ 0} ⟹ x ∈ (⋃i≤Suc 0. case i of 0 ⇒ V | Suc _ ⇒ U)"
unfolding 1 using g by blast
next
show "compactin X (X closure_of {x ∈ topspace X. g x ≠ 0})"
using g by(simp add: has_compact_support_on_iff)
qed(use g VU le_Suc_eq in auto)
then obtain hi where
"(∀i≤Suc 0. ?iscont (hi i) ∧ ?csupp (hi i) ∧
X closure_of {x ∈ topspace X. hi i x ≠ 0} ⊆ (case i of 0 ⇒ V | Suc _ ⇒ U) ∧
hi i ∈ topspace X → {0..1} ∧ hi i ∈ topspace X - (case i of 0 ⇒ V | Suc _ ⇒ U) → {0}) ∧
(∀x∈X closure_of {x∈topspace X. g x ≠ 0}. (∑i≤Suc 0. hi i x) = 1) ∧
(∀x∈topspace X. 0 ≤ (∑i≤Suc 0. hi i x)) ∧ (∀x∈topspace X. (∑i≤Suc 0. hi i x) ≤ 1)"
by blast
hence h0: "?iscont (hi 0)" "?csupp (hi 0)" "X closure_of {x ∈ topspace X. hi 0 x ≠ 0} ⊆ V"
"hi 0 ∈ topspace X → {0..1}" "hi 0 ∈ topspace X - V → {0}"
and h1: "?iscont (hi (Suc 0))" "?csupp (hi (Suc 0))" "X closure_of {x ∈ topspace X. hi (Suc 0) x ≠ 0} ⊆ U"
"hi (Suc 0) ∈ topspace X → {0..1}" "hi (Suc 0) ∈ topspace X - U → {0}"
and h01_sum: "⋀x. x ∈ X closure_of {x∈topspace X. g x ≠ 0} ⟹ (∑i≤Suc 0. hi i x) = 1"
unfolding le_Suc_eq le_0_eq by auto
have "ennreal (φ (λx∈topspace X. g x)) = ennreal (φ (λx∈topspace X. g x * (hi 0 x + hi (Suc 0) x)))"
proof -
have [simp]: "(λx∈topspace X. g x) = (λx∈topspace X. g x * (hi 0 x + hi (Suc 0) x))"
proof
fix x
consider "g x ≠ 0" "x ∈ topspace X" | "g x = 0" | "x ∉ topspace X"
by fastforce
then show "restrict g (topspace X) x = (λx∈topspace X. g x * (hi 0 x + hi (Suc 0) x)) x"
proof cases
case 1
then have "x ∈ X closure_of {x∈topspace X. g x ≠ 0}"
using in_closure_of by fastforce
from h01_sum[OF this] show ?thesis
by simp
qed simp_all
qed
show ?thesis
by simp
qed
also have "... = ennreal (φ (λx∈topspace X. g x * hi 0 x + g x * hi (Suc 0) x))"
by (simp add: ring_class.ring_distribs(1))
also have "... = ennreal (φ (λx∈topspace X. g x * hi 0 x) + φ (λx∈topspace X. g x * hi (Suc 0) x))"
by(intro ennreal_cong linear(2) has_compact_support_on_mult_left continuous_map_real_mult g h0 h1)
also have "... = ennreal (φ (λx∈topspace X. g x * hi 0 x)) + ennreal (φ (λx∈topspace X. g x * hi (Suc 0) x))"
using g(3) h0(4) h1(4)
by(auto intro!: ennreal_plus pos g h0 h1 has_compact_support_on_mult_left mult_nonneg_nonneg)
also have "... ≤ μ' V + μ' U"
unfolding μ'_def
proof(safe intro!: add_mono Sup_upper imageI)
show "∃f. (λx∈topspace X. g x * hi 0 x) = restrict f (topspace X) ∧ ?iscont f ∧ ?csupp f ∧
X closure_of {x ∈ topspace X. f x ≠ 0} ⊆ V ∧ f ∈ topspace X → {0..1} ∧ f ∈ topspace X - V → {0}"
using Pi_mem[OF g(3)] Pi_mem[OF h0(4)] in_mono[OF closure_of_mono[OF inf_sup_ord(2)[of "{x ∈ topspace X. g x ≠ 0}"]]] h0(3,5)
by(auto intro!: exI[where x="λx∈topspace X. g x * hi 0 x"] g(1,2) h0(1,2) has_compact_support_on_mult_left mult_le_one mult_nonneg_nonneg)
show "∃f. (λx∈topspace X. g x * hi (Suc 0) x) = restrict f (topspace X) ∧ ?iscont f ∧
?csupp f ∧ X closure_of {x ∈ topspace X. f x ≠ 0} ⊆ U ∧ f ∈ topspace X → {0..1} ∧ f ∈ topspace X - U → {0}"
using Pi_mem[OF g(3)] Pi_mem[OF h1(4)] in_mono[OF closure_of_mono[OF inf_sup_ord(2)[of "{x ∈ topspace X. g x ≠ 0}"]]] h1(3,5)
by(auto intro!: exI[where x="λx∈topspace X. g x * hi 1 x"] g(1,2) h1(1,2) has_compact_support_on_mult_left mult_le_one mult_nonneg_nonneg)
qed
finally show "ennreal (φ (restrict g (topspace X))) ≤ μ' V + μ' U" .
qed
finally show "μ' (V ∪ U) ≤ μ' V + μ' U" .
qed
consider "∃i. μ (Ei i) = ∞" | "⋀i. μ (Ei i) < ∞"
using top.not_eq_extremum by auto
then show ?thesis
proof cases
case 1
then show ?thesis
by (metis μ_mono ennreal_suminf_lessD infinity_ennreal_def linorder_not_le subset_UNIV top.not_eq_extremum)
next
case fin:2
show ?thesis
proof(rule ennreal_le_epsilon)
fix e :: real
assume e: "0 < e"
have "∃Vi. Ei i ⊆ Vi ∧ openin X Vi ∧ μ' Vi ≤ μ (Ei i) + ennreal ((1 / 2)^Suc i) * ennreal e" for i
proof -
have 1:"μ (Ei i) < μ (Ei i) + ennreal ((1 / 2) ^ Suc i) * ennreal e"
using e fin less_le by fastforce
have "0 < ennreal ((1 / 2)^Suc i) * ennreal e"
using e by (simp add: ennreal_zero_less_mult_iff)
have "(⨅ (μ' ` {V. Ei i ⊆ V ∧ openin X V})) ≤ μ (Ei i)"
by(auto simp: μ_def)
from Inf_le_iff[THEN iffD1,OF this,rule_format,OF 1]
show ?thesis
by auto
qed
then obtain Vi where Vi: "⋀i. Vi i ⊇ Ei i" "⋀i. openin X (Vi i)"
"⋀i. μ (Vi i) ≤ μ (Ei i) + ennreal ((1 / 2)^Suc i) * ennreal e"
by (metis μ_open)
hence "μ (⋃ (range Ei)) ≤ μ (⋃ (range Vi))"
by(auto intro!: μ_mono)
also have "... = μ' (⋃ (range Vi))"
using Vi by(auto intro!: μ_open)
also have "... = (⨆ (ennreal ` φ ` {(λx∈topspace X. f x) |f. ?fA (⋃ (range Vi)) f}))"
by(simp add: μ'_def)
also have "... ≤ (∑i. μ (Ei i)) + ennreal e"
unfolding Sup_le_iff
proof safe
fix f
assume f: "?iscont f" "?csupp f" "X closure_of {x ∈ topspace X. f x ≠ 0} ⊆ ⋃ (range Vi)" "f ∈ topspace X → {0..1}" "f ∈ topspace X - ⋃ (range Vi) → {0}"
have "∃n. f ∈ topspace X - (⋃i≤n. Vi i) → {0} ∧ X closure_of {x ∈ topspace X. f x ≠ 0} ⊆ (⋃i≤n. Vi i)"
proof -
obtain K where K:"finite K" "K ⊆ range Vi" "X closure_of {x ∈ topspace X. f x ≠ 0} ⊆ ⋃ K"
using compactinD[OF f(2)[simplified has_compact_support_on_iff]] Vi(2) f(3)
by (metis (mono_tags, lifting) imageE)
hence "∃n. K ⊆ Vi ` {..n}"
by (metis (no_types, lifting) finite_nat_iff_bounded_le finite_subset_image image_mono)
then obtain n where n: "X closure_of {x ∈ topspace X. f x ≠ 0} ⊆ (⋃i≤n. Vi i)"
using K(3) by fastforce
show ?thesis
using in_closure_of n subsetD by(fastforce intro!: exI[where x=n])
qed
then obtain n where n:"f ∈ topspace X - (⋃i≤n. Vi i) → {0}" "X closure_of {x ∈ topspace X. f x ≠ 0} ⊆ (⋃i≤n. Vi i)"
by blast
have "ennreal (φ (restrict f (topspace X))) ≤ μ' (⋃i≤n. Vi i)"
using f(4) f n by(auto intro!: imageI exI[where x=f] Sup_upper simp: μ'_def)
also have "... ≤ (∑i≤n. μ' (Vi i))"
proof(induction n)
case ih:(Suc n')
have [simp]:"μ' (⋃ (Vi ` {..Suc n'})) = μ' (⋃ (Vi ` {..n'}) ∪ Vi (Suc n'))"
by(rule arg_cong[of _ _ μ']) (fastforce simp: le_Suc_eq)
also have "... ≤ μ' (⋃ (Vi ` {..n'})) + μ' (Vi (Suc n'))"
using Vi(2) by(auto intro!: 1)
also have "... ≤ (∑i≤Suc n'. μ' (Vi i))"
using ih by fastforce
finally show ?case .
qed simp
also have "... = (∑i≤n. μ (Vi i))"
using Vi(2) by(simp add: μ_open)
also have "... ≤ (∑i. μ (Vi i))"
by (auto intro!: incseq_SucI incseq_le[OF _ summable_LIMSEQ'])
also have "... ≤ (∑i. μ (Ei i) + ennreal ((1 / 2)^Suc i) * ennreal e)"
by(intro suminf_le Vi(3)) auto
also have "... = (∑i. μ (Ei i)) + (∑i. ennreal ((1 / 2)^Suc i) * ennreal e)"
by(rule suminf_add[symmetric]) auto
also have "... = (∑i. μ (Ei i)) + (∑i. ennreal ((1 / 2)^Suc i)) * ennreal e"
by simp
also have "... = (∑i. μ (Ei i)) + ennreal 1 * ennreal e"
proof -
have "(∑i. ennreal ((1 / 2)^Suc i)) = ennreal 1"
by(rule suminf_ennreal_eq) (use power_half_series in auto)
thus ?thesis
by presburger
qed
also have "... = (∑i. μ (Ei i)) + ennreal e"
by simp
finally show "ennreal (φ (restrict f (topspace X))) ≤ (∑i. μ (Ei i)) + ennreal e" .
qed
finally show "μ (⋃ (range Ei)) ≤ (∑i. μ (Ei i)) + ennreal e" .
qed
qed
qed
have step1': "μ (E1 ∪ E2) ≤ μ E1 + μ E2" for E1 E2
proof -
define En where "En ≡ (λn::nat. if n = 0 then E1 else if n = 1 then E2 else {})"
have 1: "(⋃ (range En)) = (E1 ∪ E2)"
by(auto simp: En_def)
have 2: "(∑i. μ (En i)) = μ E1 + μ E2"
using suminf_offset[of "λi. μ (En i)",of "Suc (Suc 0)"]
by(auto simp: En_def μ_empty)
show ?thesis
using step1[of En] by(simp add: 1 2)
qed
have step2: "K ∈ Mf" "μ K = (⨅ (ennreal ` φ ` {(λx∈topspace X. f x) | f. ?fK K f}))" if K: "compactin X K" for K
proof -
have le1: "μ K ≤ ennreal (φ (λx∈topspace X. f x))" if f:"?iscont f" "?csupp f" "f ∈ topspace X → {0..1}" "f ∈ K → {1}" for f
proof -
have f: "continuous_map X (top_of_set {0..1::real}) f" "f ` K ⊆ {1}" "?csupp f"
using f by (auto simp: continuous_map_in_subtopology)
hence f_cont: "?iscont f" "f ∈ topspace X → {0..1}"
by (auto simp add: continuous_map_in_subtopology)
have 1:"μ K ≤ ennreal (1 / ((real n + 1) / (real n + 2)) * φ (λx∈topspace X. f x))" for n
proof -
let ?a = "(real n + 1) / (real n + 2)"
define V where "V ≡ {x∈topspace X. ?a < f x}"
have openinV:"openin X V"
using f(1)by (auto simp: V_def continuous_map_upper_lower_semicontinuous_lt_gen)
have KV: "K ⊆ V"
using f(2) compactin_subset_topspace[OF K] by(auto simp: V_def)
hence "μ K ≤ μ V"
by(rule μ_mono)
also have "... = μ' V"
by(simp add: μ_open openinV)
also have "... = (⨆ (ennreal ` φ ` {(λx∈topspace X. f x) |f. ?fA V f}))"
by(simp add: μ'_def)
also have "... ≤ (1 / ?a) * φ (λx∈topspace X. f x)"
unfolding Sup_le_iff
proof (safe intro!: ennreal_leI)
fix g
assume g: "?iscont g" "?csupp g" "X closure_of {x∈topspace X. g x ≠ 0} ⊆ V"
"g ∈ topspace X → {0..1}" "g ∈ topspace X - V → {0}"
show "φ (restrict g (topspace X)) ≤ 1 / ?a * φ (restrict f (topspace X))" (is "?l ≤ ?r")
proof -
have "?l ≤ φ (λx∈topspace X. 1 / ?a * f x)"
proof(rule φmono)
fix x
assume x: "x ∈ topspace X"
consider "g x ≠ 0" | "g x = 0"
by fastforce
then show "g x ≤ 1 / ((real n + 1) / (real n + 2)) * f x"
proof cases
case 1
then have "x ∈ V"
using g(5) x by auto
hence "?a < f x"
by(auto simp: V_def x)
hence "1 < 1 / ?a * f x"
by (simp add: divide_less_eq mult.commute)
thus ?thesis
by(intro order.strict_implies_order[OF order.strict_trans1[of "g x" 1 "1 / ?a * f x"]]) (use g(4) x in auto)
qed(use Pi_mem[OF f_cont(2)] x in auto)
qed(intro g f_cont f has_compact_support_on_mult_left continuous_map_real_mult continuous_map_canonical_const)+
also have "... = ?r"
by(intro linear f f_cont)
finally show ?thesis .
qed
qed
finally show ?thesis .
qed
have 2:"(λn. ennreal (1 / ((real n + 1) / (real n + 2)) * φ (restrict f (topspace X))))
⇢ ennreal (φ (restrict f (topspace X)))"
proof(intro tendsto_ennrealI tendsto_mult_right[where l="1::real",simplified])
have 1: "(λn. 1 / ((real n + 1) / (real n + 2))) = (λn. real (Suc (Suc n)) / real (Suc n))"
by (simp add: add.commute)
show "(λn. 1 / ((real n + 1) / (real n + 2))) ⇢ 1"
unfolding 1 by(rule LIMSEQ_Suc[OF LIMSEQ_Suc_n_over_n])
qed
show "μ K ≤ ennreal (φ (λx∈topspace X. f x))"
by(rule Lim_bounded2[where N=0,OF 2]) (use 1 in auto)
qed
have muK_fin:"μ K < ⊤"
proof -
obtain f where f: "continuous_map X (top_of_set {0..1::real}) f" "f ` K ⊆ {1}" "?csupp f"
using Urysohn_locally_compact_Hausdorff_closed_compact_support[OF lh(1) disjI1[OF lh(2)]
zero_le_one closedin_empty K] by(auto simp: has_compact_support_on_iff)
hence "?iscont f" "?csupp f" "f ∈ topspace X → {0..1}" "f ∈ K → {1}"
by(auto simp: continuous_map_in_subtopology)
from le1[OF this]
show ?thesis
using dual_order.strict_trans2 ennreal_less_top by blast
qed
moreover have " μ K = (⨆ (μ ` {K'. K' ⊆ K ∧ compactin X K'}))"
by (metis (no_types, lifting) SUP_eqI μ_mono mem_Collect_eq subset_refl K)
ultimately show "K ∈ Mf"
using compactin_subset_topspace[OF K] by(simp add: Mf_def)
show "μ K = (⨅ (ennreal ` φ ` {(λx∈topspace X. f x) |f. ?fK K f}))"
proof(safe intro!: antisym le_Inf_iff[THEN iffD2] Inf_le_iff[THEN iffD2])
fix g
assume "?iscont g" "?csupp g" "g ∈ topspace X → {0..1}" "g ∈ K → {1}"
from le1[OF this(1-4)]
show "μ K ≤ ennreal (φ (λx∈topspace X. g x))"
by force
next
fix y
assume "μ K < y"
then obtain V where V: "openin X V" "K ⊆ V" "μ' V < y"
by (metis (mono_tags, lifting) INF_less_iff μ_def mem_Collect_eq)
hence "closedin X (topspace X - V)" "disjnt (topspace X - V) K"
by (auto simp: disjnt_def)
from Urysohn_locally_compact_Hausdorff_closed_compact_support[OF lh(1) disjI1[OF lh(2)] zero_le_one this(1) K this(2)]
obtain f where f':"continuous_map X (subtopology euclidean {0..1}) f" "f ` (topspace X - V) ⊆ {0::real}"
"f ` K ⊆ {1}" "disjnt (X closure_of {x∈topspace X. f x ≠ 0}) (topspace X - V)"
"compactin X (X closure_of {x∈topspace X. f x ≠ 0})"
by blast
hence f:"?iscont f" "?csupp f" "⋀x. x ∈ topspace X ⟹ f x ≥ 0"
"⋀x. x ∈ topspace X ⟹ f x ≤ 1" "⋀x. x ∈ K ⟹ f x = 1"
by(auto simp: has_compact_support_on_iff continuous_map_in_subtopology)
have "ennreal (φ (restrict f (topspace X))) < y"
proof(rule order.strict_trans1)
show "ennreal (φ (restrict f (topspace X))) ≤ μ' V"
unfolding μ'_def using f' f in_closure_of
by (fastforce intro!: Sup_upper imageI exI[where x="λx∈topspace X. f x"] simp: disjnt_iff)
qed fact
thus "∃a∈ennreal ` φ ` {(λx∈topspace X. f x)|f. ?fK K f}. a < y"
using f compactin_subset_topspace[OF K] by(auto intro!: exI[where x="λx∈topspace X. f x"])
qed
qed
have μ_K: "μ K ≤ ennreal (φ (λx∈topspace X. f x))" if K: "compactin X K" and f:"?fK K f" for K f
using le_Inf_iff[THEN iffD1,OF eq_refl[OF step2(2)[OF K]]] f by blast
have step3: "μ A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. μ K)" "μ A < ∞ ⟹ A ∈ Mf" if A:"openin X A" for A
proof -
show "μ A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. μ K)"
proof(safe intro!: antisym le_Sup_iff[THEN iffD2] Sup_le_iff[THEN iffD2])
fix y
assume y: "y < μ A"
from less_SUP_iff[THEN iffD1,OF less_INF_D[OF y[simplified μ_def],simplified μ'_def],of A]
obtain f where f: "?iscont f" "?csupp f" "X closure_of {x ∈ topspace X. f x ≠ 0} ⊆ A"
"f ∈ topspace X → {0..1}" "f ∈ topspace X - A → {0}" "y < ennreal (φ (λx∈topspace X. f x))"
using A by blast
show "∃a∈μ ` {K. compactin X K ∧ K ⊆ A}. y < a"
proof(rule bexI[where x="μ (X closure_of {x ∈ topspace X. f x ≠ 0})"])
show "y < μ (X closure_of {a ∈ topspace X. f a ≠ 0})"
proof(rule order.strict_trans2)
show "ennreal (φ (λx∈topspace X. f x)) ≤ μ (X closure_of {a ∈ topspace X. f a ≠ 0})"
using f in_closure_of in_mono
by(fastforce intro!: Sup_upper imageI exI[where x=f] simp: μ_def le_Inf_iff μ'_def)
qed fact
qed(use f(2,3) has_compact_support_on_iff in auto)
qed(auto intro!: μ_mono)
thus "μ A < ∞ ⟹ A ∈ Mf"
unfolding Mf_def using openin_subset[OF A] by simp metis
qed
have step4: "μ (⋃n. En n) = (∑n. μ (En n))" "μ (⋃n. En n) < ∞ ⟹ (⋃n. En n) ∈ Mf"
if En: "⋀n. En n ∈ Mf" "disjoint_family En" for En
proof -
have compacts: "μ (K1 ∪ K2) = μ K1 + μ K2" if K: "compactin X K1" "compactin X K2" "disjnt K1 K2" for K1 K2
proof(rule antisym)
show "μ (K1 ∪ K2) ≤ μ K1 + μ K2"
by(rule step1')
next
show "μ K1 + μ K2 ≤ μ (K1 ∪ K2)"
proof(rule ennreal_le_epsilon)
fix e :: real
assume e: "0 < e" "μ (K1 ∪ K2) < ⊤"
from Urysohn_locally_compact_Hausdorff_closed_compact_support[OF lh(1) disjI1[OF lh(2)]
zero_le_one compactin_imp_closedin[OF lh(2) K(1)] K(2,3)]
obtain f where f: "continuous_map X (top_of_set {0..1::real}) f" "f ` K1 ⊆ {0}" "f ` K2 ⊆ {1}"
"disjnt (X closure_of {x ∈ topspace X. f x ≠ 0}) K1" "compactin X (X closure_of {x ∈ topspace X. f x ≠ 0})"
by blast
hence f': "?iscont f" "?csupp f" "⋀x. x ∈ topspace X ⟹ f x ≥ 0" "⋀x. x ∈ topspace X ⟹ f x ≤ 1"
by(auto simp: has_compact_support_on_iff continuous_map_in_subtopology)
from Inf_le_iff[THEN iffD1,OF eq_refl[OF step2(2)[symmetric,OF compactin_Un[OF K(1,2)]]],rule_format,of "μ (K1 ∪ K2) + ennreal e"]
obtain g where g: "?iscont g" "?csupp g" "g ∈ topspace X → {0..1}" "g ∈ K1 ∪ K2 → {1}"
"ennreal (φ (λx∈topspace X. g x)) < μ (K1 ∪ K2) + ennreal e"
using e by fastforce
have "μ K1 + μ K2 ≤ ennreal (φ (λx∈topspace X. (1 - f x) * g x)) + ennreal (φ (λx∈topspace X. f x * g x))"
proof(rule add_mono)
show "μ K1 ≤ ennreal (φ (λx∈topspace X. (1 - f x) * g x))"
using f' Pi_mem[OF g(3)] g(1,2,4,5) f(2) compactin_subset_topspace[OF K(1)]
by(auto intro!: μ_K has_compact_support_on_mult_left mult_nonneg_nonneg mult_le_one K(1) mult_eq_1[THEN iffD2])
show "μ K2 ≤ ennreal (φ (λx∈topspace X. f x * g x))"
using g f Pi_mem[OF g(3)] f' compactin_subset_topspace[OF K(2)]
by(auto intro!: μ_K[OF K(2)] has_compact_support_on_mult_left mult_nonneg_nonneg mult_le_one mult_eq_1[THEN iffD2])
qed
also have "... = ennreal (φ (λx∈topspace X. (1 - f x)*g x) + φ (λx∈topspace X. f x * g x))"
using f' g by(auto intro!: ennreal_plus[symmetric] pos has_compact_support_on_mult_left mult_nonneg_nonneg)
also have "... = ennreal (φ (λx∈topspace X. (1 - f x) * g x + f x * g x))"
by(auto intro!: ennreal_cong linear[symmetric] has_compact_support_on_mult_left f' g)
also have "... = ennreal (φ (λx∈topspace X. g x))"
by (simp add: Groups.mult_ac(2) right_diff_distrib)
also have "... < μ (K1 ∪ K2) + ennreal e"
by fact
finally show "μ K1 + μ K2 ≤ μ (K1 ∪ K2) + ennreal e"
by order
qed
qed
have Hn:"∃Hn. ∀n. compactin X (Hn n) ∧ (Hn n) ⊆ En n ∧ μ (En n) < μ (Hn n) + ennreal ((1 / 2)^Suc n) * ennreal e'"
if e': "e' > 0" for e'
proof(safe intro!: choice)
show "∃Hn. compactin X Hn ∧ Hn ⊆ En n ∧ μ (En n) < μ Hn + ennreal ((1 / 2)^Suc n) * ennreal e'" for n
proof(cases "μ (En n) < ennreal ((1 / 2)^Suc n) * ennreal e'")
case True
then show ?thesis
using e' by(auto intro!: exI[where x="{}"] simp: μ_empty ennreal_zero_less_mult_iff)
next
case False
then have le: "μ (En n) ≥ ennreal ((1 / 2) ^ Suc n) * ennreal e'"
by order
hence pos:"0 < μ (En n)"
using e' zero_less_power by fastforce
have fin: "μ (En n) < ⊤"
using En Mf_def by blast
hence 1:"μ (En n) - ennreal ((1 / 2)^Suc n) * ennreal e' < μ (En n)"
using pos by(auto intro!: ennreal_between simp: ennreal_zero_less_mult_iff e')
have "μ (En n) = ⨆ (μ ` {K. K ⊆ (En n) ∧ compactin X K})"
using En by(auto simp: Mf_def)
from le_Sup_iff[THEN iffD1,OF eq_refl[OF this],rule_format,OF 1]
obtain Hn where Hn: "Hn ⊆ En n" "compactin X Hn" "μ (En n) - ennreal ((1 / 2)^Suc n) * ennreal e' < μ Hn"
by blast
hence "μ (En n) < μ Hn + ennreal ((1 / 2)^Suc n) * ennreal e'"
by (metis diff_diff_ennreal' diff_gt_0_iff_gt_ennreal fin le order_less_le)
with Hn(1,2) show ?thesis
by blast
qed
qed
show 1:"μ (⋃n. En n) = (∑n. μ (En n))"
proof(rule antisym)
show "(∑n. μ (En n)) ≤ μ (⋃ (range En))"
proof(rule ennreal_le_epsilon)
fix e :: real
assume fin: "μ (⋃ (range En)) < ⊤" and e:"0 < e"
from Hn[OF e] obtain Hn where Hn: "⋀n. compactin X (Hn n)" "⋀n. Hn n ⊆ En n"
"⋀n. μ (En n) < μ (Hn n) + ennreal ((1 / 2) ^ Suc n) * ennreal e"
by blast
have "(∑n≤N. μ (En n)) ≤ μ (⋃ (range En)) + ennreal e" for N
proof -
have "(∑n≤N. μ (En n)) ≤ (∑n≤N. μ (Hn n) + ennreal ((1 / 2) ^ Suc n) * ennreal e)"
by(rule sum_mono) (use Hn(3) order_less_le in auto)
also have "... = (∑n≤N. μ (Hn n)) + (∑n≤N. ennreal ((1 / 2) ^ Suc n) * ennreal e)"
by(rule sum.distrib)
also have "... = μ (⋃n≤N. Hn n) + (∑n≤N. ennreal ((1 / 2) ^ Suc n) * ennreal e)"
proof -
have "(∑n≤N. μ (Hn n)) = μ (⋃n≤N. Hn n)"
proof(induction N)
case ih:(Suc N')
show ?case (is "?l = ?r")
proof -
have "?l = μ (⋃ (Hn ` {..N'})) + μ (Hn (Suc N'))"
by(simp add: ih)
also have "... = μ ((⋃ (Hn ` {..N'})) ∪ Hn (Suc N'))"
proof(rule compacts[symmetric])
show "disjnt (⋃ (Hn ` {..N'})) (Hn (Suc N'))"
using En(2) Hn(2) unfolding disjoint_family_on_def disjnt_iff
by (metis Int_iff Suc_n_not_le_n UNIV_I UN_iff atMost_iff empty_iff in_mono)
qed(auto intro!: compactin_Union Hn)
also have "... = ?r"
by (simp add: Un_commute atMost_Suc)
finally show ?thesis .
qed
qed simp
thus ?thesis
by simp
qed
also have "... ≤ μ (⋃ (range En)) + (∑n≤N. ennreal ((1 / 2) ^ Suc n) * ennreal e)"
using Hn(2) by(auto intro!: μ_mono)
also have "... ≤ μ (⋃ (range En)) + ennreal e"
proof -
have "(∑n≤N. ennreal ((1 / 2) ^ Suc n) * ennreal e) = ennreal (∑n≤N. ((1 / 2) ^ Suc n)) * ennreal e"
unfolding sum_distrib_right[symmetric] by simp
also have "... = ennreal e * ennreal (∑n≤N. ((1 / 2) ^ Suc n))"
using mult.commute by blast
also have "... ≤ ennreal e * ennreal (∑n. ((1 / 2) ^ Suc n))"
using e by(auto intro!: ennreal_mult_le_mult_iff[THEN iffD2] ennreal_leI sum_le_suminf)
also have "... = ennreal e"
using power_half_series sums_unique by fastforce
finally show ?thesis
by fastforce
qed
finally show ?thesis .
qed
thus "(∑n. μ (En n)) ≤ μ (⋃ (range En)) + ennreal e"
by(auto intro!: LIMSEQ_le_const2[OF summable_LIMSEQ'] exI[where x=0])
qed
qed fact
show "⋃ (range En) ∈ Mf" if "μ (⋃ (range En)) < ∞"
proof -
have "μ (⋃ (range En)) = (⨆ (μ ` {K. K ⊆ (⋃ (range En)) ∧ compactin X K}))"
proof(rule antisym)
show "μ (⋃ (range En)) ≤ ⨆ (μ ` {K. K ⊆ ⋃ (range En) ∧ compactin X K})"
unfolding le_Sup_iff
proof safe
fix y
assume "y < μ (⋃ (range En))"
from order_tendstoD(1)[OF summable_LIMSEQ' this[simplified 1]]
obtain N where N: "y < (∑n≤N. μ (En n))"
by fastforce
obtain e where e: "e > 0" "y < (∑n≤N. μ (En n)) - ennreal e"
by (metis N ennreal_le_epsilon ennreal_less_top less_diff_eq_ennreal linorder_not_le)
from Hn[OF e(1)] obtain Hn where Hn: "⋀n. compactin X (Hn n)" "⋀n. Hn n ⊆ En n"
"⋀n. μ (En n) < μ (Hn n) + ennreal ((1 / 2) ^ Suc n) * ennreal e"
by blast
have "y < (∑n≤N. μ (En n)) - ennreal e"
by fact
also have "... ≤ (∑n≤N. μ (Hn n) + ennreal ((1 / 2) ^ Suc n) * ennreal e) - ennreal e"
by(intro ennreal_minus_mono sum_mono) (use Hn(3) order_less_le in auto)
also have "... = (∑n≤N. μ (Hn n)) + (∑n≤N. ennreal ((1 / 2) ^ Suc n) * ennreal e) - ennreal e"
by (simp add: sum.distrib)
also have "... = μ (⋃n≤N. Hn n) + (∑n≤N. ennreal ((1 / 2) ^ Suc n) * ennreal e) - ennreal e"
proof -
have "(∑n≤N. μ (Hn n)) = μ (⋃n≤N. Hn n)"
proof(induction N)
case ih:(Suc N')
show ?case (is "?l = ?r")
proof -
have "?l = μ (⋃ (Hn ` {..N'})) + μ (Hn (Suc N'))"
by(simp add: ih)
also have "... = μ ((⋃ (Hn ` {..N'})) ∪ Hn (Suc N'))"
proof(rule compacts[symmetric])
show "disjnt (⋃ (Hn ` {..N'})) (Hn (Suc N'))"
using En(2) Hn(2) unfolding disjoint_family_on_def disjnt_iff
by (metis Int_iff Suc_n_not_le_n UNIV_I UN_iff atMost_iff empty_iff in_mono)
qed(auto intro!: compactin_Union Hn)
also have "... = ?r"
by (simp add: Un_commute atMost_Suc)
finally show ?thesis .
qed
qed simp
thus ?thesis
by simp
qed
also have "... ≤ μ (⋃n≤N. Hn n) + (∑n. ennreal ((1 / 2) ^ Suc n) * ennreal e) - ennreal e"
by(intro ennreal_minus_mono add_mono sum_le_suminf) (use e in auto)
also have "... = μ (⋃n≤N. Hn n) + (∑n. ennreal ((1 / 2) ^ Suc n)) * ennreal e - ennreal e"
using ennreal_suminf_multc by presburger
also have "... = μ (⋃n≤N. Hn n) + ennreal e - ennreal e"
proof -
have "(∑n. ennreal ((1 / 2) ^ Suc n)) = ennreal 1"
by(rule suminf_ennreal_eq) (use power_half_series in auto)
thus ?thesis
by fastforce
qed
also have "... = μ (⋃n≤N. Hn n)"
by simp
finally show "Bex (μ ` {K. K ⊆ ⋃ (range En) ∧ compactin X K}) ((<) y)"
using Hn by(auto intro!: exI[where x="⋃n≤N. Hn n"] compactin_Union)
qed
qed(auto intro!: Sup_le_iff[THEN iffD2] μ_mono)
moreover have "(⋃ (range En)) ⊆ topspace X"
using En by(auto simp: Mf_def)
ultimately show ?thesis
using that by(auto simp: Mf_def)
qed
qed
have step4': "μ (E1 ∪ E2) = μ E1 + μ E2" "μ(E1 ∪ E2) < ∞ ⟹ E1 ∪ E2 ∈ Mf"
if E: "E1 ∈ Mf" "E2 ∈ Mf" "disjnt E1 E2" for E1 E2
proof -
define En where "En ≡ (λn::nat. if n = 0 then E1 else if n = 1 then E2 else {})"
have 1: "(⋃ (range En)) = (E1 ∪ E2)"
by(auto simp: En_def)
have 2: "(∑i. μ (En i)) = μ E1 + μ E2"
using suminf_offset[of "λi. μ (En i)",of "Suc (Suc 0)"]
by(auto simp: En_def μ_empty)
have 3:"disjoint_family En"
using E(3) by(auto simp: disjoint_family_on_def disjnt_def En_def)
have 4: "⋀n. En n ∈ Mf"
using E(1,2) by(auto simp: En_def empty_in_Mf)
show "μ (E1 ∪ E2) = μ E1 + μ E2" "μ(E1 ∪ E2) < ∞ ⟹ E1 ∪ E2 ∈ Mf"
using step4[of En] E(1) by(simp_all add: 1 2 3 4)
qed
have step5: "∃V K. openin X V ∧ compactin X K ∧ K ⊆ E ∧ E ⊆ V ∧ μ (V - K) < ennreal e"
if E: "E ∈ Mf" and e: "e > 0" for E e
proof-
have 1:"μ E < μ E + ennreal (e / 2)"
using E e by(simp add: Mf_def) (metis μ_mono linorder_not_le)
hence 2: "μ E + ennreal (e / 2) < μ E + ennreal (e / 2) + ennreal (e / 2)"
by simp
from Inf_le_iff[THEN iffD1,OF eq_refl,rule_format,OF _ 1]
obtain V where V: "openin X V" "E ⊆ V" "μ V < μ E + ennreal (e / 2)"
using μ_def μ_open by force
have "μ E + ennreal (e / 2) + ennreal (e / 2) ≤ (⨆K∈{K. K ⊆ E ∧ compactin X K}. μ K + ennreal e)"
by(subst ennreal_SUP_add_left,insert E e) (auto simp: ennreal_plus_if Mf_def)
from le_Sup_iff[THEN iffD1,OF this,rule_format,OF 2]
obtain K where K: "compactin X K" "K ⊆ E" "μ E + ennreal (e / 2) < μ K + ennreal e"
by blast
have "μ (V - K) < ∞"
by (metis Diff_subset V(3) μ_mono dual_order.strict_trans1 infinity_ennreal_def order_le_less_trans top_greatest)
hence "μ K + μ (V - K) = μ (K ∪ (V - K))"
by(intro step4'(1)[symmetric,OF step2(1)[OF K(1)] step3(2)] openin_diff V(1) compactin_imp_closedin K(1) lh(2))
(auto simp: disjnt_iff)
also have "... = μ V"
by (metis Diff_partition K(2) V(2) order_trans)
also have "... < μ K + ennreal e"
by(auto intro!: order.strict_trans[OF V(3)] K)
finally have "μ (V - K) < ennreal e"
by(simp add: ennreal_add_left_cancel_less)
thus ?thesis
using V K by blast
qed
have step6: "⋀A B. A ∈ Mf ⟹ B ∈ Mf ⟹ A - B ∈ Mf" "⋀A B. A ∈ Mf ⟹ B ∈ Mf ⟹ A ∪ B ∈ Mf"
"⋀A B. A ∈ Mf ⟹ B ∈ Mf ⟹ A ∩ B ∈ Mf"
proof -
{
fix A B
assume AB: "A ∈ Mf" "B ∈ Mf"
have dif1: "μ (A - B) < ∞"
by (metis (no_types, lifting) AB(1) Diff_subset Mf_def μ_mono infinity_ennreal_def mem_Collect_eq order_le_less_trans)
have "μ (A - B) = (⨆ (μ ` {K. K ⊆ (A - B) ∧ compactin X K}))"
proof(rule antisym)
show "μ (A - B) ≤ ⨆ (μ ` {K. K ⊆ A - B ∧ compactin X K})"
unfolding le_Sup_iff
proof safe
fix y
assume y:"y < μ (A - B)"
then obtain e where e: "e > 0" "ennreal e = μ (A - B) - y"
by (metis dif1 diff_gt_0_iff_gt_ennreal diff_le_self_ennreal ennreal_cases ennreal_less_zero_iff neq_top_trans order_less_le)
from step5[OF AB(1) half_gt_zero[OF e(1)]] step5[OF AB(2) half_gt_zero[OF e(1)]]
obtain V1 V2 K1 K2 where VK:
"openin X V1" "compactin X K1" "K1 ⊆ A" "A ⊆ V1" "μ (V1 - K1) < ennreal (e / 2)"
"openin X V2" "compactin X K2" "K2 ⊆ B" "B ⊆ V2" "μ (V2 - K2) < ennreal (e / 2)"
by auto
have K1V2:"compactin X (K1 - V2)"
by(auto intro!: closed_compactin[OF VK(2)] compactin_imp_closedin[OF lh(2) VK(2)] VK(6))
have "μ (A - B) ≤ μ ((K1 - V2) ∪ (V1 - K1) ∪ (V2 - K2))"
using VK by(auto intro!: μ_mono)
also have "... ≤ μ ((K1 - V2) ∪ (V1 - K1)) + μ (V2 - K2)"
by fact
also have "... ≤ μ (K1 - V2) + μ (V1 - K1) + μ (V2 - K2)"
by(auto intro!: step1')
also have "... < μ (K1 - V2) + μ (V1 - K1) + ennreal (e / 2)"
unfolding add.assoc ennreal_add_left_cancel_less ennreal_add_left_cancel_less
using step2(1)[OF K1V2] VK(5,10) Mf_def by fastforce
also have "... ≤ μ (K1 - V2) + ennreal (e / 2) + ennreal (e / 2)"
using order.strict_implies_order[OF VK(5)] by(auto simp: add_mono)
also have "... = μ (K1 - V2) + ennreal e"
using e(1) ennreal_plus_if by auto
finally have 1:"μ (A - B) < μ (K1 - V2) + ennreal e" .
show "∃a∈(μ ` {K. K ⊆ A - B ∧ compactin X K}). (y < a)"
proof(safe intro!: bexI[where x="μ (K1 - V2)"] imageI)
have "y < μ (K1 - V2) + ennreal e - ennreal e"
by (metis 1 add_diff_self_ennreal e(2) ennreal_less_top less_diff_eq_ennreal order_less_imp_le y)
also have "... = μ (K1 - V2)"
by simp
finally show "y < μ (K1 - V2)" .
qed(use K1V2 VK in auto)
qed
qed(auto intro!: μ_mono simp: Sup_le_iff)
with dif1 show "A - B ∈ Mf"
using Mf_def μ_fin_subset by auto
}
note diff=this
fix A B
assume AB: "A ∈ Mf" "B ∈ Mf"
show un: "A ∪ B ∈ Mf"
proof -
have "A ∪ B = (A - B) ∪ B"
by fastforce
also have "... ∈ Mf"
proof(rule step4'(2))
have "μ (A - B ∪ B) = μ (A - B) + μ B"
by(rule step4'(1)) (auto simp: diff AB disjnt_iff)
also have "... < ∞"
using Mf_def diff[OF AB] AB(2) by fastforce
finally show "μ (A - B ∪ B) < ∞" .
qed(auto simp: diff AB disjnt_iff)
finally show ?thesis .
qed
show int: "A ∩ B ∈ Mf"
proof -
have "A ∩ B = A - (A - B)"
by blast
also have "... ∈ Mf"
by(auto intro!: diff AB)
finally show ?thesis .
qed
qed
have step6': "(⋃i∈I. Ai i) ∈ Mf" if "finite I" "(⋀i. i ∈ I ⟹ Ai i ∈ Mf)" for Ai and I :: "nat set"
proof -
have "(∀i∈I. Ai i ∈ Mf) ⟶ (⋃i∈I. Ai i) ∈ Mf"
by(rule finite_induct[OF that(1)]) (auto intro!: step6(2) empty_in_Mf)
with that show ?thesis
by blast
qed
have step7: "sigma_algebra (topspace X) M" "sets (borel_of X) ⊆ M"
proof -
show sa:"sigma_algebra (topspace X) M"
unfolding sigma_algebra_iff2
proof(intro conjI ballI allI impI)
show "{} ∈ M"
using empty_in_Mf by(auto simp: M_def)
next
show M_subspace:"M ⊆ Pow (topspace X)"
by(auto simp: M_def)
{
fix s
assume s:"s ∈ M"
show "topspace X - s ∈ M"
unfolding M_def
proof(intro conjI CollectI allI impI)
fix K
assume K: "compactin X K"
have "(topspace X - s) ∩ K = K - (s ∩ K)"
using M_subspace s compactin_subset_topspace[OF K] by fast
also have "... ∈ Mf"
by(intro step6(1) step2(1)[OF K]) (use s K M_def in blast)
finally show "(topspace X - s) ∩ K ∈ Mf" .
qed blast
}
{
fix An :: "nat ⇒ _"
assume An: "range An ⊆ M"
show "(⋃ (range An)) ∈ M"
unfolding M_def
proof(intro CollectI conjI allI impI)
fix K
assume K: "compactin X K"
have "∃Bn. ∀n. Bn n = (An n ∩ K) - (⋃i<n. Bn i)"
by(rule dependent_wellorder_choice) auto
then obtain Bn where Bn: "⋀n. Bn n = (An n ∩ K) - (⋃i<n. Bn i)"
by blast
have Bn_disj:"disjoint_family Bn"
unfolding disjoint_family_on_def
proof safe
fix m n x
assume h:"m ≠ n" "x ∈ Bn m" "x ∈ Bn n"
then consider "m < n" | "n < m"
by linarith
then show "x ∈ {}"
proof cases
case 1
with h(3) have "x ∉ Bn m"
by(auto simp: Bn[of n])
with h(2) show ?thesis by blast
next
case 2
with h(2) have "x ∉ Bn n"
by(auto simp: Bn[of m])
with h(3) show ?thesis by blast
qed
qed
have un:"(⋃ (range An) ∩ K) = (⋃n. Bn n)"
proof -
have 1:"An n ∩ K ⊆ (⋃i≤n. Bn i)" for n
proof safe
fix x
assume x:"x ∈ An n" "x ∈ K"
define m where "m = (LEAST m. x ∈ An m)"
have m1:"⋀l. l < m ⟹ x ∈ An m ⟹ x ∉ An l"
using m_def not_less_Least by blast
hence x_nBn:"l < m ⟹ x ∉ Bn l" for l
by (metis Bn Diff_Diff_Int Diff_iff m_def not_less_Least)
have m2: "x ∈ An m"
by (metis LeastI_ex x(1) m_def)
have m3: "m ≤ n"
using m1 m2 not_le_imp_less x(1) by blast
have "x ∈ Bn m"
unfolding Bn[of m]
using x_nBn m2 x(2) by fast
thus "x ∈ ⋃ (Bn ` {..n})"
using m3 by blast
qed
have 2:"(⋃n. An n ∩ K) = (⋃n. Bn n)"
proof(rule antisym)
show "(⋃n. An n ∩ K) ⊆ ⋃ (range Bn)"
proof safe
fix n x
assume "x ∈ An n" "x ∈ K"
then have "x ∈ (⋃i≤n. Bn i)"
using 1 by fast
thus "x ∈ ⋃ (range Bn)"
by fast
qed
next
show " ⋃ (range Bn) ⊆ (⋃n. An n ∩ K)"
proof(rule SUP_mono)
show "∃m∈UNIV. Bn i ⊆ An m ∩ K" for i
by(auto intro!: bexI[where x=i] simp: Bn[of i])
qed
qed
thus ?thesis
by simp
qed
also have "... ∈ Mf"
proof(safe intro!: step4(2) Bn_disj)
fix n
show "Bn n ∈ Mf"
proof(rule less_induct)
fix n
show " (⋀m. m < n ⟹ Bn m ∈ Mf) ⟹ Bn n ∈ Mf"
using An K by(auto intro!: step6' step6(1) simp :Bn[of n] M_def)
qed
next
have "μ (⋃ (range Bn)) ≤ μ K"
unfolding un[symmetric] by(auto intro!: μ_mono)
also have "... < ∞"
using step2(1)[OF K] by(auto simp: Mf_def)
finally show "μ (⋃ (range Bn)) < ∞" .
qed
finally show "⋃ (range An) ∩ K ∈ Mf " .
qed(use An M_def in auto)
}
qed
show "sets (borel_of X) ⊆ M"
unfolding sets_borel_of_closed
proof(safe intro!: sigma_algebra.sigma_sets_subset[OF sa])
fix T
assume "closedin X T"
then show "T ∈ M"
by (simp add: Int_commute M_def closedin_subset compact_Int_closedin step2(1))
qed
qed
have step8: "A ∈ Mf ⟷ A ∈ M ∧ μ A < ∞" for A
proof safe
assume A: "A ∈ Mf"
then have "A ⊆ topspace X"
by(auto simp: Mf_def)
thus "A ∈ M"
by(auto simp: M_def intro!:step6(3)[OF A step2(1)])
show "μ A < ∞"
using A by(auto simp: Mf_def)
next
assume A: "A ∈ M" "μ A < ∞"
hence "A ⊆ topspace X"
using M_def by blast
moreover have "μ A = (⨆ (μ ` {K. K ⊆ A ∧ compactin X K}))"
proof(rule antisym)
show "μ A ≤ ⨆ (μ ` {K. K ⊆ A ∧ compactin X K})"
unfolding le_Sup_iff
proof safe
fix y
assume y:"y < μ A"
then obtain e where e: "e > 0" "ennreal e = μ A - y"
by (metis A(2) diff_gt_0_iff_gt_ennreal diff_le_self_ennreal ennreal_cases ennreal_less_zero_iff neq_top_trans order_less_le)
obtain U where U: "openin X U" "A ⊆ U" "μ U < ∞"
using Inf_less_iff[THEN iffD1,OF A(2)[simplified μ_def]] μ_open by force
from step5[OF step3(2)[OF U(1,3)] half_gt_zero[OF e(1)]]
obtain V K where VK:
"openin X V" "compactin X K" "K ⊆ U" "U ⊆ V" "μ (V - K) < ennreal (e / 2)"
by blast
have AK: "A ∩ K ∈ Mf"
using step2(1) VK(2) A by(auto simp: M_def)
hence e': "μ (A ∩ K) < μ (A ∩ K) + ennreal (e / 2)"
by (metis Diff_Diff_Int Diff_subset Int_commute U(3) VK(3) VK(5) μ_mono add.commute diff_gt_0_iff_gt_ennreal ennreal_add_diff_cancel infinity_ennreal_def order_le_less_trans top.not_eq_extremum zero_le)
have "μ (A ∩ K) + ennreal (e / 2) = (⨆K∈{L. L ⊆ (A ∩ K) ∧ compactin X L}. μ K + ennreal (e / 2))"
by(subst ennreal_SUP_add_left) (use AK Mf_def in auto)
from le_Sup_iff[THEN iffD1,OF this[THEN eq_refl],rule_format,OF e']
obtain H where H: "compactin X H" "H ⊆ A ∩ K" "μ (A ∩ K) < μ H + ennreal (e / 2)"
by blast
show "∃a∈μ ` {K. K ⊆ A ∧ compactin X K}. y < a"
proof(safe intro!: bexI[where x="μ H"] imageI H(1))
have "μ A ≤ μ ((A ∩ K) ∪ (V - K))"
using VK U by(auto intro!: μ_mono)
also have "... ≤ μ (A ∩ K) + μ (V - K)"
by(auto intro!: step1'(1))
also have "... < μ H + ennreal (e / 2) + ennreal (e / 2)"
using H(3) VK(5) add_strict_mono by blast
also have "... = μ H + ennreal e"
using e(1) ennreal_plus_if by fastforce
finally have 1: "μ A < μ H + ennreal e" .
have "y = μ A - ennreal e"
using A(2) diff_diff_ennreal e(2) y by fastforce
also have "... < μ H + ennreal e - ennreal e"
using 1
by (metis diff_le_self_ennreal e(2) ennreal_add_diff_cancel_right ennreal_less_top minus_less_iff_ennreal top_neq_ennreal)
also have "... = μ H"
by simp
finally show "y < μ H" .
qed(use H in auto)
qed
qed(auto simp: Sup_le_iff intro!: μ_mono)
ultimately show "A ∈ Mf"
using A(2) Mf_def by auto
qed
define N where "N ≡ measure_of (topspace X) M μ"
have step9: "measure_space (topspace X) M μ"
unfolding measure_space_def
proof safe
show "countably_additive M μ"
unfolding countably_additive_def
by (metis Sup_upper UNIV_I μ_mono image_eqI image_subset_iff infinity_ennreal_def linorder_not_less neq_top_trans step1 step4(1) step8)
qed(auto simp: step7 positive_def μ_empty)
have space_N: "space N = topspace X" and sets_N: "sets N = M" and emeasure_N: "A ∈ sets N ⟹ emeasure N A = μ A" for A
proof -
show "space N = topspace X"
by (simp add: N_def space_measure_of_conv)
show 1:"sets N = M"
by (simp add: N_def sigma_algebra.sets_measure_of_eq step7(1))
have "⋀x. x ∈ M ⟹ x ⊆ topspace X"
by(auto simp: M_def)
thus "A ∈ sets N ⟹ emeasure N A = μ A"
unfolding N_def using step9 by(auto intro!: emeasure_measure_of simp: measure_space_def 1[simplified N_def])
qed
have g1:"subalgebra N (borel_of X)" (is ?g1)
and g2:"(∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))" (is ?g2)
and g3:"(∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))" (is ?g3)
and g4:"(∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))" (is ?g4)
and g5:"(∀K. compactin X K ⟶ emeasure N K < ∞)" (is ?g5)
and g6:"complete_measure N" (is ?g6)
proof -
have 1: "⋀P. (⋀C. P C ⟹ C ∈ sets N) ⟹ emeasure N ` {C. P C} = μ ` {C. P C}"
using emeasure_N by auto
show ?g1
by(auto simp: subalgebra_def sets_N space_N space_borel_of step7)
show ?g2
proof -
have "emeasure N ` {C. openin X C ∧ A ⊆ C} = μ ` {C. openin X C ∧ A ⊆ C}" for A
using step7(2) by(auto intro!: 1 simp: sets_N dest: borel_of_open)
hence "emeasure N ` {C. openin X C ∧ A ⊆ C} = μ' ` {C. openin X C ∧ A ⊆ C}" for A
using μ_open by auto
thus ?thesis
by(simp add: emeasure_N sets_N μ_def) (metis (no_types, lifting) Collect_cong)
qed
show ?g3
by (metis (no_types, lifting) 1 borel_of_open emeasure_N sets_N step2(1) step3(1) step7(2) step8 subsetD)
show ?g4
proof safe
fix A
assume A[measurable]: "A ∈ sets N" "emeasure N A < ∞"
then have Mf:"A ∈ Mf"
by (simp add: emeasure_N sets_N step8)
have "emeasure N A = μ A"
by (simp add: emeasure_N)
also have "... = ⨆ (μ ` {K. compactin X K ∧ K ⊆ A})"
using Mf unfolding Mf_def by simp metis
also have "... = ⨆ (emeasure N ` {K. compactin X K ∧ K ⊆ A})"
using emeasure_N sets_N step2(1) step8 by auto
finally show "emeasure N A = ⨆ (emeasure N ` {K. compactin X K ∧ K ⊆ A})" .
qed
show ?g5
using emeasure_N sets_N step2(1) step8 by auto
show ?g6
proof
fix A B
assume AB:"B ⊆ A" "A ∈ null_sets N"
then have "μ A = 0"
by (metis emeasure_N null_setsD1 null_setsD2)
hence 1:"μ B = 0"
using μ_mono[OF AB(1)] by fastforce
have "B ∈ Mf"
proof -
have "B ⊆ topspace X"
by (metis AB gfp.leq_trans null_setsD2 sets.sets_into_space space_N)
moreover have "μ B = ⨆ (μ ` {K. K ⊆ B ∧ compactin X K})"
proof(rule antisym)
show "⨆ (μ ` {K. K ⊆ B ∧ compactin X K}) ≤ μ B"
by(auto simp: Sup_le_iff μ_mono)
qed(simp add: 1)
moreover have "μ B < ⊤"
by(simp add: 1)
ultimately show ?thesis
unfolding Mf_def by blast
qed
thus "B ∈ sets N"
by(simp add: step8 sets_N)
qed
qed
have g7: "(∀f. ?iscont f ⟶ ?csupp f ⟶ integrable N f)"
unfolding integrable_iff_bounded
proof safe
fix f
assume f:"?iscont f" "?csupp f"
then show [measurable]:"f ∈ borel_measurable N"
by(auto intro!: measurable_from_subalg[OF g1]
simp: lower_semicontinuous_map_measurable upper_lower_semicontinuous_map_iff_continuous_map)
let ?K = "X closure_of {x∈topspace X. f x ≠ 0}"
have K[measurable]: "compactin X ?K" "?K ∈ sets N"
using f(2) g1 sets_N step2(1) step8 by(auto simp: has_compact_support_on_iff subalgebra_def)
have "bounded (f ` ?K)"
using image_compactin[of X ?K euclideanreal f] f
by(auto simp: has_compact_support_on_iff intro!: compact_imp_bounded)
then obtain B where B:"⋀x. x ∈ ?K ⟹ ¦f x¦ ≤ B"
by (meson bounded_real imageI)
show "(∫⇧+ x. ennreal (norm (f x)) ∂N) < ∞"
proof -
have "(∫⇧+ x. ennreal (norm (f x)) ∂N) ≤ (∫⇧+ x. ennreal (indicator ?K x *¦f x¦) ∂N)"
using in_closure_of by(fastforce intro!: nn_integral_mono simp: indicator_def space_N)
also have "... ≤ (∫⇧+ x. ennreal (B * indicator ?K x) ∂N)"
using B by(auto intro!: nn_integral_mono ennreal_leI simp: indicator_def)
also have "... = (∫⇧+ x. ennreal B * indicator ?K x ∂N)"
by(auto intro!: nn_integral_cong simp: indicator_def)
also have "... = ennreal B * (∫⇧+ x. indicator ?K x ∂N)"
by(simp add: nn_integral_cmult)
also have "... = ennreal B * emeasure N ?K"
by simp
finally show ?thesis
using g5 K(1) ennreal_mult_less_top linorder_not_le top.not_eq_extremum by fastforce
qed
qed
have g8: "∀f. ?iscont f ⟶ ?csupp f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N)"
proof safe
have 1: "φ (λx∈topspace X. f x) ≤ (∫x. f x ∂N)" if f:"?iscont f" "?csupp f" for f
proof -
let ?K = "X closure_of {x∈topspace X. f x ≠ 0}"
have K[measurable]: "compactin X ?K" "?K ∈ sets N"
using f(2) g1 sets_N step2(1) step8 by(auto simp: has_compact_support_on_iff subalgebra_def)
have f_meas[measurable]: "f ∈ borel_measurable N"
using f by(auto intro!: measurable_from_subalg[OF g1]
simp: lower_semicontinuous_map_measurable upper_lower_semicontinuous_map_iff_continuous_map)
have "bounded (f ` ?K)"
using image_compactin[of X ?K euclideanreal f] f
by(auto simp: has_compact_support_on_iff intro!: compact_imp_bounded)
then obtain B' where B':"⋀x. x ∈ ?K ⟹ ¦f x¦ ≤ B'"
by (meson bounded_real imageI)
define B where "B ≡ max 1 B'"
have B_pos: "B > 0" and B: "⋀x. x ∈ ?K ⟹ ¦f x¦ ≤ B"
using B' by(auto simp add: B_def intro!: max.coboundedI2)
have 1:"φ (λx∈topspace X. f x) ≤ (∫x. f x ∂N) + 1 / (Suc n) * (2 * measure N ?K + (1 / Suc n) + 2 * B + 1)" for n
proof -
have "∃yn. ∀m::nat. yn m = (if m = 0 then - B - 1 else 1 / 2 * 1 / Suc n + yn (m - 1))"
by(rule dependent_wellorder_choice) auto
then obtain yn' where yn':"⋀m::nat. yn' m = (if m = 0 then - B - 1 else 1 / 2 * 1 / Suc n + yn' (m - 1))"
by blast
hence yn'_0: "yn' 0 = - B - 1" and yn'_Suc: "⋀m. yn' (Suc m) = 1 / 2 * 1 / Suc n + yn' m"
by simp_all
have yn'_accum: "yn' m = m * (1 / 2 * 1 / Suc n) + yn' 0" for m
by(induction m) (auto simp: yn'_Suc add_divide_distrib)
define L :: nat where "L = (LEAST k. B ≤ yn' k)"
define yn where "yn ≡ (λn. if n = L then B else yn' n)"
have L_least: "⋀i. i < L ⟹ yn' i < B"
by (metis L_def linorder_not_less not_less_Least)
have yn_L: "yn L = B"
by(auto simp: yn_def)
have yn'_L: "yn' L ≥ B"
unfolding L_def
proof(rule LeastI_ex)
show "∃x. B ≤ yn' x"
proof(safe intro!: exI[where x="nat (ceiling ((2 * B + 2) / ((1/2) * 1 / real (Suc n))))"])
have "B ≤ 2 * B + 2 + (- B - 1)"
using B_pos by fastforce
also have "... = (2 * B + 2) / ((1/2) * 1 / real (Suc n)) * (1 / 2 * 1 / Suc n) + yn' 0"
by(auto simp: yn'_0)
also have "... ≤ real (nat (ceiling ((2 * B + 2) / ((1/2) * 1 / real (Suc n))))) * (1 / 2 * 1 / Suc n) + yn' 0"
by(intro add_mono real_nat_ceiling_ge mult_right_mono) auto
also have "... = yn' (nat (ceiling ((2 * B + 2) / ((1/2) * 1 / real (Suc n)))))"
by (metis yn'_accum)
finally show " B ≤ yn' (nat ⌈(2 * B + 2) / (1 / 2 * 1 / real (Suc n))⌉)" .
qed
qed
have L_pos: "0 < L"
proof(rule ccontr)
assume "¬ 0 < L"
then have [simp]:"L = 0"
by blast
show False
using yn'_L yn'_0 B_pos by auto
qed
have yn_0: "yn 0 = - B - 1"
using L_pos by(auto simp: yn_def yn'_0)
have strict_mono_yn:"strict_mono yn"
proof(rule strict_monoI_Suc)
fix m
consider "m = L" | "Suc m = L" | "m < L" "Suc m < L" | "L < m" "L < Suc m"
by linarith
then show "yn m < yn (Suc m)"
proof cases
case 1
then have "yn m = B"
by(simp add: yn_L)
also have "... ≤ yn' m"
using yn'_L by(simp add: 1)
also have "... < yn' (Suc m)"
by (simp add: yn'_Suc)
also have "... = yn (Suc m)"
using 1 by(auto simp: yn_def)
finally show ?thesis .
next
case 2
then have "yn m = yn' m"
using yn_def by force
also have "... < B"
using L_least[of m] 2 by blast
also have "... = yn (Suc m)"
by(simp add: 2 yn_L)
finally show ?thesis .
qed(auto simp: yn_def yn'_Suc)
qed
have yn_le_L: "⋀i. i ≤ L ⟹ yn i ≤ B"
using L_least less_eq_real_def yn_def by auto
have yn_ge_L: "⋀i. L < i ⟹ B < yn i"
using strict_mono_yn[THEN strict_monoD] yn_L by blast
have yn_ge: "⋀i. - B - 1 ≤ yn i"
using monoD[OF strict_mono_mono[OF strict_mono_yn],of 0] yn_0 by auto
have yn_Suc_le: "yn (Suc i) < 1 / real (Suc n) + yn i" for i
proof -
consider "i = L" | "Suc i = L" | "i < L" "Suc i < L" | "L < i" "L < Suc i"
by linarith
then show ?thesis
proof cases
case 1
then have "yn (Suc i) = yn' (Suc L)"
by(simp add: yn_def)
also have "... = 1 / 2 * 1 / Suc n + yn' L"
by(simp add: yn'_Suc)
also have "... = (1 / 2) * (1 / Suc n) + (1 / 2) * (1 / Suc n) + yn' (L - 1)"
using L_pos yn' by fastforce
also have "... = 1 / Suc n + yn' (L - 1)"
unfolding semiring_normalization_rules(1) by simp
also have "... < 1 / Suc n + B"
by (simp add: L_least L_pos less_eq_real_def)
finally show ?thesis
by(simp add: 1 yn_L)
next
case 2
then have "yn (Suc i) = B"
by(simp add: yn_L)
also have "... ≤ yn' L"
using yn'_L .
also have "... = 1 / 2 * 1 / Suc n + yn' (L - 1)"
using yn' L_pos by simp
also have "... = 1 / 2 * 1 / Suc n + yn i"
using 2 yn_def by force
also have "... < 1 / Suc n + yn i"
by (simp add: pos_less_divide_eq)
finally show ?thesis .
qed(auto simp: yn_def yn'_Suc pos_less_divide_eq)
qed
have f_bound: "f x ∈ {yn 0<..yn L}" if x:"x ∈ ?K" for x
using B[OF x] yn_L yn_0 by auto
define En where "En ≡ (λm. {x∈topspace X. yn m < f x ∧ f x ≤ yn (Suc m)} ∩ ?K)"
have En_sets[measurable]: "En m ∈ sets N" for m
proof -
have "{x∈topspace X. yn m < f x ∧ f x ≤ yn (Suc m)} = f -` {yn m<..yn (Suc m)} ∩ space N"
by(auto simp: space_N)
also have "... ∈ sets N"
by simp
finally show ?thesis
by(simp add: En_def)
qed
have En_disjnt: "disjoint_family En"
unfolding disjoint_family_on_def
proof safe
fix m n x
assume "m ≠ n" and x: "x ∈ En n" "x ∈ En m"
then consider "m < n" | "n < m"
by linarith
thus "x ∈ {}"
proof cases
case 1
hence 1:"Suc m ≤ n"
by simp
from x have "f x ≤ yn (Suc m)" "yn n < f x"
by(auto simp: En_def)
with 1 show ?thesis
using monoD[OF strict_mono_mono[OF strict_mono_yn] 1] by linarith
next
case 2
hence 1:"Suc n ≤ m"
by simp
from x have "f x ≤ yn (Suc n)" "yn m < f x"
by(auto simp: En_def)
with 1 show ?thesis
using monoD[OF strict_mono_mono[OF strict_mono_yn] 1] by linarith
qed
qed
have K_eq_un_En: "?K = (⋃i≤L. En i)"
proof safe
fix x
assume x:"x ∈ ?K"
have "∃m∈{..L}. yn m < f x ∧ x ∈ topspace X ∧ f x ≤ yn (Suc m)"
proof(rule ccontr)
assume "¬ (∃m∈{..L}. yn m < f x ∧ x ∈ topspace X ∧ f x ≤ yn (Suc m))"
then have 1:"⋀m. m ≤ L ⟹ yn (Suc m) < f x ∨ f x ≤ yn m"
using compactin_subset_topspace[OF K(1)] x by force
then have "m ≤ L ⟹ yn (Suc m) < f x" for m
by(induction m) (use B x yn_0 in fastforce)+
hence "yn (Suc L) < f x"
by force
with yn_ge_L[of "Suc L"] f_bound x B show False
by fastforce
qed
thus "x ∈ (⋃i≤L. En i)"
using x by(auto simp: En_def)
qed(auto simp: En_def)
have emeasure_En_fin: "emeasure N (En i) < ∞" for i
proof -
have "emeasure N (En i) ≤ μ ?K"
unfolding emeasure_N[OF En_sets[of i]] by(auto intro!: μ_mono simp: En_def)
also have "... < ∞"
using step2(1)[OF K(1)] step8 by blast
finally show ?thesis .
qed
have "∃Vi. openin X Vi ∧ En i ⊆ Vi ∧ measure N Vi < measure N (En i) + (1 / Suc n) / Suc L ∧
(∀x∈Vi. f x < (1 / real (Suc n) + yn i)) ∧ emeasure N Vi < ∞" for i
proof -
have 1:"emeasure N (En i) < emeasure N (En i) + ennreal (1 / real (Suc n) / real (Suc L))"
unfolding ennreal_add_left_cancel_less[where b=0,simplified add_0_right]
using emeasure_En_fin by (simp add: order_less_le)
from Inf_le_iff[THEN iffD1,OF eq_refl[OF g2[rule_format,OF En_sets[of i],symmetric]],rule_format,OF this]
obtain Vi where Vi:"openin X Vi" "Vi ⊇ En i"
"emeasure N Vi < emeasure N (En i) + ennreal (1 / real (Suc n) / real (Suc L))"
by blast
hence "ennreal (measure N Vi) = emeasure N Vi"
unfolding measure_def using ennreal_enn2real_if by fastforce
also have "... < ennreal (measure N (En i)) + ennreal (1 / real (Suc n) / real (Suc L))"
using ennreal_enn2real_if emeasure_En_fin Vi by (metis emeasure_eq_ennreal_measure top.extremum_strict)
also have "... = ennreal (measure N (En i) + 1 / real (Suc n) / real (Suc L))"
by simp
finally have 1:"measure N Vi < measure N (En i) + 1 / real (Suc n) / real (Suc L)"
by(auto intro!: ennreal_less_iff[THEN iffD1])
define Vi' where "Vi' = Vi ∩ {x∈topspace X. yn i < f x ∧ f x < 1 / real (Suc n) + yn i}"
have "En i ⊆ Vi'"
proof -
have "En i = En i ∩ {x∈topspace X. yn i < f x ∧ f x < 1 / real (Suc n) + yn i}"
unfolding En_def using order.strict_trans1[OF _ yn_Suc_le] by fast
also have "... ⊆ Vi'"
using Vi(2) by(auto simp: Vi'_def)
finally show ?thesis .
qed
moreover have "openin X Vi'"
proof -
have "{x ∈ topspace X. yn i<f x ∧ f x< 1/real (Suc n) + yn i} = (f -` {yn i<..<1/real (Suc n) + yn i} ∩ topspace X)"
by fastforce
also have "openin X ..."
using continuous_map_open[OF f(1)] by simp
finally show ?thesis
using Vi(1) by(auto simp: Vi'_def)
qed
moreover have "measure N Vi' < measure N (En i) + (1 / real (Suc n) / real (Suc L))" (is "?l < ?r")
proof -
have "?l ≤ measure N Vi"
unfolding measure_def
proof(safe intro!: enn2real_mono emeasure_mono)
show "Vi ∈ sets N"
using Vi(1) borel_of_open sets_N step7(2) by blast
show "emeasure N Vi < ⊤"
by (metis ‹ennreal (Sigma_Algebra.measure N Vi) = emeasure N Vi› ennreal_less_top)
qed(auto simp: Vi'_def)
with 1 show ?thesis
by fastforce
qed
moreover have "⋀x. x ∈ Vi' ⟹ f x < (1 / real (Suc n) + yn i)"
by(auto simp: Vi'_def)
moreover have "emeasure N Vi' < ∞"
by (metis (no_types, lifting) Diff_Diff_Int Diff_subset Vi'_def Vi(1) ‹ennreal (measure N Vi) = emeasure N Vi› borel_of_open
emeasure_mono ennreal_less_top infinity_ennreal_def linorder_not_less sets_N step7(2) subsetD top.not_eq_extremum)
ultimately show ?thesis
by blast
qed
then obtain Vi where
Vi: "⋀i. openin X (Vi i)" "⋀i. En i ⊆ Vi i"
"⋀i. measure N (Vi i) < measure N (En i) + (1 / Suc n) / Suc L"
"⋀i x. x ∈ Vi i ⟹ f x < (1 / real (Suc n) + yn i)"
"⋀i. emeasure N (Vi i) < ∞"
by metis
have "?K ⊆ (⋃i≤L. Vi i)"
using K_eq_un_En Vi(2) by blast
from fApartition[OF K(1) Vi(1) this]
obtain hi where hi: "⋀i. i ≤ L ⟹ ?iscont (hi i)" "⋀i. i ≤ L ⟹ ?csupp (hi i)"
"⋀i. i ≤ L ⟹ X closure_of {x ∈ topspace X. hi i x ≠ 0} ⊆ Vi i"
"⋀i. i ≤ L ⟹ hi i ∈ topspace X → {0..1}" "⋀i. i ≤ L ⟹ hi i ∈ topspace X - Vi i → {0}"
"⋀x. x ∈ ?K ⟹ (∑i≤L. hi i x) = 1" "⋀x. x ∈ topspace X ⟹ 0 ≤ (∑i≤L. hi i x)"
"⋀x. x ∈ topspace X ⟹ (∑i≤L. hi i x) ≤ 1"
by blast
have f_sum_hif: "(∑i≤L. f x * hi i x) = f x" if x:"x ∈ topspace X" for x
proof(cases "f x = 0")
case False
then have "x ∈ ?K"
using in_closure_of x by fast
with hi(6)[OF this] show ?thesis
by(simp add: sum_distrib_left[symmetric])
qed simp
have sum_muEi:"(∑i≤L. measure N (En i)) = measure N ?K"
proof -
have "(∑i≤L. measure N (En i)) = measure N (⋃i≤L. En i)"
using emeasure_En_fin En_disjnt
by(fastforce intro!: measure_UNION'[symmetric] fmeasurableI pairwiseI simp: disjnt_iff disjoint_family_on_def)
also have "... = measure N ?K"
by(simp add: K_eq_un_En)
finally show ?thesis .
qed
have measure_K_le: "measure N ?K ≤ (∑i≤L. φ (λx∈topspace X. hi i x))"
proof -
have "ennreal (measure N ?K) = μ ?K"
by (metis (mono_tags, lifting) K(1) K(2) Sigma_Algebra.measure_def emeasure_N ennreal_enn2real g5 infinity_ennreal_def)
also have "μ ?K ≤ ennreal (φ (λx∈topspace X. ∑i≤L. hi i x))"
by(auto intro!: le_Inf_iff[THEN iffD1,OF eq_refl[OF step2(2)[OF K(1)]],rule_format]
imageI exI[where x="λx. ∑i≤L. hi i x"] has_compact_support_on_sum hi continuous_map_sum)
also have "... = ennreal (∑i≤L. φ (λx∈topspace X. hi i x))"
by(auto intro!: pos_lin_functional_on_CX_sum assms ennreal_cong hi)
finally show ?thesis
using Pi_mem[OF hi(4)] by(auto intro!: ennreal_le_iff[of _ "measure N ?K",THEN iffD1] sum_nonneg pos hi)
qed
have "φ (restrict f (topspace X)) = φ (λx∈topspace X. ∑i≤L. f x * hi i x)"
using f_sum_hif restrict_ext by force
also have "... = (∑i≤L. φ (λx∈topspace X. f x * hi i x))"
using f hi by(auto intro!: pos_lin_functional_on_CX_sum assms has_compact_support_on_mult_right)
also have "... ≤ (∑i≤L. φ (λx∈topspace X. (1 / (Suc n) + yn i) * hi i x))"
proof(safe intro!: sum_mono φmono)
fix i x
assume i:"i ≤ L" "x ∈ topspace X"
show "f x * hi i x ≤ (1 / (Suc n) + yn i) * hi i x"
proof(cases "x ∈ Vi i")
case True
hence "f x < 1 / (Suc n) + yn i"
by fact
thus ?thesis
using Pi_mem[OF hi(4)[OF i(1)] i(2)] by(intro mult_right_mono) auto
next
case False
then show ?thesis
using Pi_mem[OF hi(5)[OF i(1)]] i(2) by force
qed
qed(auto intro!: f hi has_compact_support_on_mult_left)
also have "... = (∑i≤L. (1 / (Suc n) + yn i) * φ (λx∈topspace X. hi i x))"
by(intro Finite_Cartesian_Product.sum_cong_aux linear hi) auto
also have "... = (∑i≤L. (1 / (Suc n) + yn i + (B + 1)) * φ (λx∈topspace X. hi i x))
- (∑i≤L. (B + 1) * φ (λx∈topspace X. hi i x))"
by(simp add: sum_subtractf[symmetric] distrib_right)
also have "... = (∑i≤L. (1 / (Suc n) + yn i + (B + 1)) * φ (λx∈topspace X. hi i x))
- (B + 1) * (∑i≤L. φ (λx∈topspace X. hi i x))"
by (simp add: sum_distrib_left)
also have "... ≤ (∑i≤L. (1 / (Suc n) + yn i + (B + 1)) * (measure N (En i) + (1 / Suc n / Suc L)))
- (B + 1) * measure N ?K"
proof(safe intro!: diff_mono[OF sum_mono[OF mult_left_mono]])
fix i
assume i: "i ≤ L"
show "φ (restrict (hi i) (topspace X)) ≤ measure N (En i) + 1 / (Suc n) / (Suc L)" (is "?l ≤ ?r")
proof -
have "?l ≤ measure N (Vi i)"
proof -
have "ennreal (φ (restrict (hi i) (topspace X))) ≤ μ' (Vi i)"
using hi(1,2,3,4,5)[OF i] by(auto intro!: SUP_upper imageI exI[where x="hi i"] simp: μ'_def)
also have "... = emeasure N (Vi i)"
by (metis Vi(1) μ_open borel_of_open emeasure_N sets_N step7(2) subsetD)
also have "... = ennreal (measure N (Vi i))"
using Vi(5)[of i] by(auto simp: measure_def intro!: ennreal_enn2real[symmetric])
finally show "φ (restrict (hi i) (topspace X)) ≤ measure N (Vi i)"
using ennreal_le_iff measure_nonneg by blast
qed
with Vi(3)[of i] show ?thesis
by linarith
qed
show "0 ≤ 1 / real (Suc n) + yn i + (B + 1)"
using yn_ge[of i] by(simp add: add.assoc)
qed(use B_pos measure_K_le in fastforce)
also have "... = (∑i≤L. (yn i - 1 / (Suc n)) * measure N (En i)) + 2 * (∑i≤L. ((1 / Suc n)) * measure N (En i))
+ (∑i≤L. (B + 1) * measure N (En i))
+ (∑i≤L. (1 / (Suc n) + yn i + (B + 1)) * (1 / Suc n / Suc L)) - (B + 1) * measure N ?K"
by(simp add: distrib_left distrib_right sum.distrib sum_subtractf left_diff_distrib)
also have "... = (∑i≤L. (yn i - 1 / (Suc n)) * measure N (En i)) + 1 / Suc n * 2* measure N ?K
+ (∑i≤L. (1 / (Suc n) + yn i + (B + 1)) * (1 / Suc n / Suc L))"
by(simp add: sum_distrib_left[symmetric] sum_muEi del: times_divide_eq_left)
also have "... ≤ (∑i≤L. (yn i - 1 / (Suc n)) * measure N (En i)) + 1 / Suc n * 2* measure N ?K
+ (∑i≤L. (1 / (Suc n) + B + (B + 1)) * (1 / Suc n / Suc L))"
proof -
have "(∑i≤L. (1 / (Suc n) + yn i + (B + 1)) * (1 / Suc n / Suc L))
≤ (∑i≤L. (1 / (Suc n) + B + (B + 1)) * (1 / Suc n / Suc L))"
proof(safe intro!: sum_mono mult_right_mono)
fix i
assume i: "i ≤ L"
show "1 / (Suc n) + yn i + (B + 1) ≤ 1 / (Suc n) + B + (B + 1)"
using yn_le_L[OF i] by fastforce
qed auto
thus ?thesis
by argo
qed
also have "... = (∑i≤L. (yn i - 1 / (Suc n)) * measure N (En i)) + 1 / Suc n * 2* measure N ?K
+ (1 / (Suc n) + B + (B + 1)) * (1 / Suc n)"
by simp
also have "... = (∑i≤L. (yn i - 1 / (Suc n)) * measure N (En i))
+ 1 / Suc n * (2 * measure N ?K + (1 / Suc n) + 2 * B + 1)"
by argo
also have "... ≤ (∫x. f x ∂N) + 1 / (Suc n) * (2 * measure N ?K + (1 / Suc n) + 2 * B + 1)"
proof -
have "(∑i≤L. (yn i - 1 / (Suc n)) * measure N (En i)) ≤ (∫x. f x ∂N)" (is "?l ≤ ?r")
proof -
have "?l = (∑i≤L. (∫x. (yn i - 1 / (Suc n)) * indicator (En i) x ∂N))"
by simp
also have "... = (∫x. (∑i≤L. (yn i - 1 / (Suc n)) * indicator (En i) x) ∂N)"
by(rule Bochner_Integration.integral_sum[symmetric]) (use emeasure_En_fin in simp)
also have "... ≤ ?r"
proof(rule integral_mono)
fix x
assume x: "x ∈ space N"
consider "⋀i. i ≤ L ⟹ x ∉ En i" | "∃i≤L. x ∈ En i"
by blast
then show " (∑i≤L. (yn i - 1 / real (Suc n)) * indicat_real (En i) x) ≤ f x"
proof cases
case 1
then have "x ∉ ?K"
by(simp add: K_eq_un_En)
hence "f x = 0"
using x in_closure_of by(fastforce simp: space_N)
with 1 show ?thesis
by force
next
case 2
then obtain i where i: "i ≤ L" "x ∈ En i"
by blast
with En_disjnt have "⋀j. j ≠ i ⟹ x ∉ En j"
by(auto simp: disjoint_family_on_def)
hence "(∑i≤L. (yn i - 1 / real (Suc n)) * indicat_real (En i) x)
= (∑j≤L. if j = i then (yn i - 1 / real (Suc n)) else 0)"
by(intro Finite_Cartesian_Product.sum_cong_aux) (use i in auto)
also have "... = yn i - 1 / real (Suc n)"
using i by auto
also have "... ≤ f x"
using i(2) by(auto simp: En_def diff_less_eq order_less_le_trans intro!: order.strict_implies_order)
finally show ?thesis .
qed
next
show "integrable N (λx. ∑i≤L. (yn i - 1 / real (Suc n)) * indicat_real (En i) x)"
using emeasure_En_fin by fastforce
qed(use g7 f in auto)
finally show ?thesis .
qed
thus ?thesis
by fastforce
qed
finally show ?thesis .
qed
show ?thesis
proof(rule Lim_bounded2)
show "(λn. (∫x. f x ∂N) + 1 / real (Suc n) * (2 * measure N ?K + 1 / real (Suc n) + 2 * B + 1)) ⇢ (∫x. f x ∂N)"
apply(rule tendsto_add[where b=0,simplified])
apply simp
apply(rule tendsto_mult[where a = "0::real", simplified,where b="2 * measure N ?K + 2 * B + 1"])
apply(intro LIMSEQ_Suc[OF lim_inverse_n'] tendsto_add[OF tendsto_const,of _ 0,simplified] tendsto_add[OF _ tendsto_const])+
done
qed(use 1 in auto)
qed
fix f
assume f: "?iscont f" "?csupp f"
show "φ (λx∈topspace X. f x) = (∫x. f x ∂N)"
proof(rule antisym)
have "- φ (λx∈topspace X. f x) = φ (λx∈topspace X. - f x)"
using f by(auto intro!: φdiff[of "λx. 0" f,simplified φ_0,simplified,symmetric])
also have "... ≤ (∫x. - f x ∂N)"
by(intro 1) (auto simp: f)
also have "... = - (∫x. f x ∂N)"
by simp
finally show "φ (λx∈topspace X. f x) ≥ (∫x. f x ∂N)"
by linarith
qed(intro f 1)
qed
show ?thesis
apply(intro exI[where x=M] ex1I[where a=N] rep_measures_real_unique[OF lh(1,2),of _ N])
using sets_N g1 g2 g3 g4 g5 g6 g7 g8 by auto
qed
subsection ‹ Riesz Representation Theorem for Complex Numbers›
theorem Riesz_representation_complex_complete:
fixes X :: "'a topology" and φ :: "('a ⇒ complex) ⇒ complex"
assumes lh:"locally_compact_space X" "Hausdorff_space X"
and plf:"positive_linear_functional_on_CX X φ"
shows "∃M. ∃!N. sets N = M ∧ subalgebra N (borel_of X)
∧ (∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))
∧ (∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀K. compactin X K ⟶ emeasure N K < ∞)
∧ (∀f. continuous_map X euclidean f ⟶ f has_compact_support_on X ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))
∧ (∀f. continuous_map X euclidean f ⟶ f has_compact_support_on X ⟶ complex_integrable N f)
∧ complete_measure N"
proof -
let ?φ' = "λf. Re (φ (λx∈topspace X. complex_of_real (f x)))"
from Riesz_representation_real_complete[OF lh pos_lin_functional_on_CX_complex_decompose_plf[OF plf]]
obtain M N where MN:
"sets N = M" "subalgebra N (borel_of X)" "(∀A∈sets N. emeasure N A = ⨅ (emeasure N ` {C. openin X C ∧ A ⊆ C}))"
"(∀A. openin X A ⟶ emeasure N A = ⨆ (emeasure N ` {K. compactin X K ∧ K ⊆ A}))"
"(∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = ⨆ (emeasure N ` {K. compactin X K ∧ K ⊆ A}))"
"(∀K. compactin X K ⟶ emeasure N K < ∞)"
"⋀f. continuous_map X euclideanreal f ⟹ f has_compact_support_on X ⟹ ?φ' (λx∈topspace X. f x) = (∫x. f x ∂N)"
"⋀f. continuous_map X euclideanreal f ⟹ f has_compact_support_on X ⟹ integrable N f" "complete_measure N"
by fastforce
have MN1: "complex_integrable N f" if f:"continuous_map X euclidean f" "f has_compact_support_on X" for f
using f unfolding complex_integrable_iff
by(auto intro!: MN(8))
have MN2: "φ (λx∈topspace X. f x) = (∫x. f x ∂N)"
if f:"continuous_map X euclidean f" "f has_compact_support_on X" for f
proof -
have "φ (λx∈topspace X. f x)
= complex_of_real (?φ' (λx∈topspace X. Re (f x))) + 𝗂 * complex_of_real (?φ' (λx∈topspace X. Im (f x)))"
using f by(intro pos_lin_functional_on_CX_complex_decompose[OF plf])
also have "... = complex_of_real (∫x. Re (f x) ∂N) + 𝗂 * complex_of_real (∫x. Im (f x) ∂N)"
proof -
have *:"?φ' (λx∈topspace X. Re (f x)) = (∫x. Re (f x) ∂N)"
using f by(intro MN(7)) auto
have **:"?φ' (λx∈topspace X. Im (f x)) = (∫x. Im (f x) ∂N)"
using f by(intro MN(7)) auto
show ?thesis
unfolding * ** ..
qed
also have "... = complex_of_real (Re (∫x. f x ∂N)) + 𝗂 * complex_of_real (Im (∫x. f x ∂N))"
by(simp add: integral_Im[OF MN1[OF that]] integral_Re[OF MN1[OF that]])
also have "... = (∫x. f x ∂N)"
using complex_eq by auto
finally show ?thesis .
qed
show ?thesis
apply(intro exI[where x=M] ex1I[where a=N] rep_measures_complex_unique[OF lh])
using MN(1-6,9) MN1 MN2
by auto
qed
subsection ‹ Other Forms of the Theorem ›
text ‹ In the case when the representation measure is on $X$.›
theorem Riesz_representation_real:
assumes lh:"locally_compact_space X" "Hausdorff_space X"
and "positive_linear_functional_on_CX X φ"
shows "∃!N. sets N = sets (borel_of X)
∧ (∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))
∧ (∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀K. compactin X K ⟶ emeasure N K < ∞)
∧ (∀f. continuous_map X euclideanreal f ⟶ f has_compact_support_on X ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))
∧ (∀f. continuous_map X euclideanreal f ⟶ f has_compact_support_on X ⟶ integrable N f)"
proof -
from Riesz_representation_real_complete[OF assms] obtain M N where MN:
"sets N = M" "subalgebra N (borel_of X)" "(∀A∈sets N. emeasure N A = ⨅ (emeasure N ` {C. openin X C ∧ A ⊆ C}))"
"(∀A. openin X A ⟶ emeasure N A = ⨆ (emeasure N ` {K. compactin X K ∧ K ⊆ A}))"
"(∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = ⨆ (emeasure N ` {K. compactin X K ∧ K ⊆ A}))"
"(∀K. compactin X K ⟶ emeasure N K < ∞)"
"⋀f. continuous_map X euclideanreal f ⟹ f has_compact_support_on X ⟹ φ (λx∈topspace X. f x) = (∫x. f x ∂N)"
"⋀f. continuous_map X euclideanreal f ⟹ f has_compact_support_on X ⟹ integrable N f" "complete_measure N"
by fastforce
define N' where "N' ≡ restr_to_subalg N (borel_of X)"
have g1: "sets N' = sets (borel_of X)" (is ?g1)
and g2: "∀A∈sets N'. emeasure N' A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N' C)" (is ?g2)
and g3: "∀A. openin X A ⟶ emeasure N' A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N' K)" (is ?g3)
and g4: "∀A∈sets N'. emeasure N' A < ∞ ⟶ emeasure N' A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N' K)" (is ?g4)
and g5: "∀K. compactin X K ⟶ emeasure N' K < ∞" (is ?g5)
and g6: "∀f. continuous_map X euclideanreal f ⟶ f has_compact_support_on X ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N')" (is ?g6)
and g7: "∀f. continuous_map X euclideanreal f ⟶ f has_compact_support_on X ⟶ integrable N' f" (is ?g7)
proof -
have sets_N': "sets N' = borel_of X"
using sets_restr_to_subalg[OF MN(2)] by(auto simp: N'_def)
have emeasure_N': "⋀A. A ∈ sets N' ⟹ emeasure N' A = emeasure N A"
by (simp add: MN(2) N'_def emeasure_restr_to_subalg sets_restr_to_subalg)
have setsN'[measurable]: "⋀A. openin X A ⟹ A ∈ sets N'" "⋀A. compactin X A ⟹ A ∈ sets N'"
by(auto simp: sets_N' dest: borel_of_open borel_of_closed[OF compactin_imp_closedin[OF lh(2)]])
have sets_N'_sets_N[simp]: "⋀A. A ∈ sets N' ⟹ A ∈ sets N"
using MN(2) sets_N' subalgebra_def by blast
show ?g1
by (simp add: MN(2) N'_def sets_restr_to_subalg)
show ?g2
using MN(3) by(auto simp: emeasure_N')
show ?g3
using MN(4) by(auto simp: emeasure_N')
show ?g4
using MN(5) by(auto simp: emeasure_N')
show ?g5
using MN(6) by(auto simp: emeasure_N')
show ?g6 ?g7
proof safe
fix f
assume f:"continuous_map X euclideanreal f" "f has_compact_support_on X"
then have [measurable]: "f ∈ borel_measurable (borel_of X)"
by (simp add: continuous_lower_semicontinuous lower_semicontinuous_map_measurable)
from MN(7,8) f show "φ (λx∈topspace X. f x) = (∫x. f x ∂N')" "integrable N' f"
by(auto simp: N'_def integral_subalgebra2[OF MN(2)] intro!: integrable_in_subalg[OF MN(2)])
qed
qed
have g8: "⋀L. sets L = sets (borel_of X) ⟹ subalgebra L (borel_of X)"
by (metis sets_eq_imp_space_eq subalgebra_def subset_refl)
show ?thesis
apply(intro ex1I[where a=N'] rep_measures_real_unique[OF lh])
using g1 g2 g3 g4 g5 g6 g7 g8 by auto
qed
theorem Riesz_representation_complex:
fixes X :: "'a topology" and φ :: "('a ⇒ complex) ⇒ complex"
assumes lh:"locally_compact_space X" "Hausdorff_space X"
and "positive_linear_functional_on_CX X φ"
shows "∃!N. sets N = sets (borel_of X)
∧ (∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))
∧ (∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀K. compactin X K ⟶ emeasure N K < ∞)
∧ (∀f. continuous_map X euclidean f ⟶ f has_compact_support_on X ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))
∧ (∀f. continuous_map X euclidean f ⟶ f has_compact_support_on X ⟶ complex_integrable N f)"
proof -
from Riesz_representation_complex_complete[OF assms] obtain M N where MN:
"sets N = M" "subalgebra N (borel_of X)" "(∀A∈sets N. emeasure N A = ⨅ (emeasure N ` {C. openin X C ∧ A ⊆ C}))"
"(∀A. openin X A ⟶ emeasure N A = ⨆ (emeasure N ` {K. compactin X K ∧ K ⊆ A}))"
"(∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = ⨆ (emeasure N ` {K. compactin X K ∧ K ⊆ A}))"
"(∀K. compactin X K ⟶ emeasure N K < ∞)"
"⋀f. continuous_map X euclidean f ⟹ f has_compact_support_on X ⟹ φ (λx∈topspace X. f x) = (∫x. f x ∂N)"
"⋀f. continuous_map X euclidean f ⟹ f has_compact_support_on X ⟹ complex_integrable N f" "complete_measure N"
by fastforce
define N' where "N' ≡ restr_to_subalg N (borel_of X)"
have g1: "sets N' = sets (borel_of X)" (is ?g1)
and g2: "∀A∈sets N'. emeasure N' A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N' C)" (is ?g2)
and g3: "∀A. openin X A ⟶ emeasure N' A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N' K)" (is ?g3)
and g4: "∀A∈sets N'. emeasure N' A < ∞ ⟶ emeasure N' A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N' K)" (is ?g4)
and g5: "∀K. compactin X K ⟶ emeasure N' K < ∞" (is ?g5)
and g6: "∀f. continuous_map X euclidean f ⟶ f has_compact_support_on X ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N')" (is ?g6)
and g7: "∀f. continuous_map X euclidean f ⟶ f has_compact_support_on X ⟶ complex_integrable N' f" (is ?g7)
proof -
have sets_N': "sets N' = borel_of X"
using sets_restr_to_subalg[OF MN(2)] by(auto simp: N'_def)
have emeasure_N': "⋀A. A ∈ sets N' ⟹ emeasure N' A = emeasure N A"
by (simp add: MN(2) N'_def emeasure_restr_to_subalg sets_restr_to_subalg)
have setsN'[measurable]: "⋀A. openin X A ⟹ A ∈ sets N'" "⋀A. compactin X A ⟹ A ∈ sets N'"
by(auto simp: sets_N' dest: borel_of_open borel_of_closed[OF compactin_imp_closedin[OF lh(2)]])
have sets_N'_sets_N[simp]: "⋀A. A ∈ sets N' ⟹ A ∈ sets N"
using MN(2) sets_N' subalgebra_def by blast
show ?g1
by (simp add: MN(2) N'_def sets_restr_to_subalg)
show ?g2
using MN(3) by(auto simp: emeasure_N')
show ?g3
using MN(4) by(auto simp: emeasure_N')
show ?g4
using MN(5) by(auto simp: emeasure_N')
show ?g5
using MN(6) by(auto simp: emeasure_N')
show ?g6 ?g7
proof safe
fix f :: "_ ⇒ complex"
assume f:"continuous_map X euclidean f" "f has_compact_support_on X"
then have [measurable]: "f ∈ borel_measurable (borel_of X)"
by (metis borel_of_euclidean continuous_map_measurable)
show "φ (λx∈topspace X. f x) = (∫x. f x ∂N')" "integrable N' f"
using MN(7,8) f by(auto simp: N'_def integral_subalgebra2[OF MN(2)] intro!: integrable_in_subalg[OF MN(2)])
qed
qed
have g8: "⋀L. sets L = sets (borel_of X) ⟹ subalgebra L (borel_of X)"
by (metis sets_eq_imp_space_eq subalgebra_def subset_refl)
show ?thesis
apply(intro ex1I[where a=N'] rep_measures_complex_unique[OF lh])
using g1 g2 g3 g4 g5 g6 g7 g8 by auto
qed
subsubsection ‹ Theorem for Compact Hausdorff Spaces ›
theorem Riesz_representation_real_compact_Hausdorff:
fixes X :: "'a topology" and φ :: "('a ⇒ real) ⇒ real"
assumes lh:"compact_space X" "Hausdorff_space X"
and "positive_linear_functional_on_CX X φ"
shows "∃!N. sets N = sets (borel_of X) ∧ finite_measure N
∧ (∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))
∧ (∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀K. compactin X K ⟶ emeasure N K < ∞)
∧ (∀f. continuous_map X euclideanreal f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))
∧ (∀f. continuous_map X euclideanreal f ⟶ integrable N f)"
proof -
have [simp]: "compactin X (X closure_of A)" for A
by (simp add: closedin_compact_space lh(1))
from Riesz_representation_real[OF compact_imp_locally_compact_space[OF lh(1)] assms(2,3)] obtain N where N:
"sets N = sets (borel_of X)"
"(∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))"
"(∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))"
"(∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))"
"(∀K. compactin X K ⟶ emeasure N K < ∞)"
"(∀f. continuous_map X euclideanreal f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
"(∀f. continuous_map X euclideanreal f ⟶ integrable N f)"
by(fastforce simp: assms(1))
have space_N:"space N = topspace X"
by (simp add: N(1) sets_eq_imp_space_eq space_borel_of)
have fin:"finite_measure N"
using N(5)[rule_format,of "topspace X"] lh(1)
by(auto intro!: finite_measureI simp: space_N compact_space_def)
have 1:"⋀L. sets L = sets (borel_of X) ⟹ subalgebra L (borel_of X)"
by (metis sets_eq_imp_space_eq subalgebra_def subset_refl)
show ?thesis
by(intro ex1I[where a=N] rep_measures_real_unique[OF compact_imp_locally_compact_space[OF lh(1)] lh(2)])
(use N fin 1 in auto)
qed
theorem Riesz_representation_complex_compact_Hausdorff:
fixes X :: "'a topology" and φ :: "('a ⇒ complex) ⇒ complex"
assumes lh:"compact_space X" "Hausdorff_space X"
and "positive_linear_functional_on_CX X φ"
shows "∃!N. sets N = sets (borel_of X) ∧ finite_measure N
∧ (∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))
∧ (∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))
∧ (∀K. compactin X K ⟶ emeasure N K < ∞)
∧ (∀f. continuous_map X euclidean f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))
∧ (∀f. continuous_map X euclidean f ⟶ complex_integrable N f)"
proof -
have [simp]: "compactin X (X closure_of A)" for A
by (simp add: closedin_compact_space lh(1))
from Riesz_representation_complex[OF compact_imp_locally_compact_space[OF lh(1)] assms(2,3)] obtain N where N:
"sets N = sets (borel_of X)"
"(∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))"
"(∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))"
"(∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))"
"(∀K. compactin X K ⟶ emeasure N K < ∞)"
"(∀f. continuous_map X euclidean f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
"(∀f. continuous_map X euclidean f ⟶ complex_integrable N f)"
by (fastforce simp: lh(1))
have space_N:"space N = topspace X"
by (simp add: N(1) sets_eq_imp_space_eq space_borel_of)
have fin:"finite_measure N"
using N(5)[rule_format,of "topspace X"] lh(1)
by(auto intro!: finite_measureI simp: space_N compact_space_def)
have 1:"⋀L. sets L = sets (borel_of X) ⟹ subalgebra L (borel_of X)"
by (metis sets_eq_imp_space_eq subalgebra_def subset_refl)
show ?thesis
by(intro ex1I[where a=N] rep_measures_complex_unique[OF compact_imp_locally_compact_space[OF lh(1)] lh(2)])
(use N fin 1 in auto)
qed
subsubsection ‹ Theorem for Compact Metrizable Spaces›
theorem Riesz_representation_real_compact_metrizable:
fixes X :: "'a topology" and φ :: "('a ⇒ real) ⇒ real"
assumes lh:"compact_space X" "metrizable_space X"
and plf:"positive_linear_functional_on_CX X φ"
shows "∃!N. sets N = sets (borel_of X) ∧ finite_measure N
∧ (∀f. continuous_map X euclideanreal f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
proof -
have hd: "Hausdorff_space X"
by (simp add: lh(2) metrizable_imp_Hausdorff_space)
from Riesz_representation_real_compact_Hausdorff[OF lh(1) hd plf] obtain N where N:
"sets N = sets (borel_of X)" "finite_measure N"
"(∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))"
"(∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))"
"(∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))"
"(∀K. compactin X K ⟶ emeasure N K < ∞)"
"(∀f. continuous_map X euclideanreal f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
"(∀f. continuous_map X euclideanreal f ⟶ integrable N f)"
by fastforce
then have tight_on_N:"tight_on X N"
using finite_measure.tight_on_compact_space lh(1) lh(2) by metis
show ?thesis
proof(safe intro!: ex1I[where a=N])
fix M
assume M:"sets M = sets (borel_of X)" "finite_measure M" "(∀f. continuous_map X euclideanreal f ⟶ φ (restrict f (topspace X)) = integral⇧L M f)"
then have "tight_on X M"
using finite_measure.tight_on_compact_space lh(1) lh(2) by blast
thus "M = N"
using N(7) M(3) by(auto intro!: finite_tight_measure_eq[OF compact_imp_locally_compact_space[OF lh(1)] lh(2)] tight_on_N)
qed(use N in auto)
qed
theorem Riesz_representation_real_compact_metrizable_le1:
fixes X :: "'a topology" and φ :: "('a ⇒ real) ⇒ real"
assumes lh:"compact_space X" "metrizable_space X"
and plf:"positive_linear_functional_on_CX X φ"
shows "∃!N. sets N = sets (borel_of X) ∧ finite_measure N
∧ (∀f. continuous_map X euclideanreal f ⟶ f ∈ topspace X → {0..1} ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
proof -
have hd: "Hausdorff_space X"
by (simp add: lh(2) metrizable_imp_Hausdorff_space)
from Riesz_representation_real_compact_Hausdorff[OF lh(1) hd plf] obtain N where N:
"sets N = sets (borel_of X)" "finite_measure N"
"(∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))"
"(∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))"
"(∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))"
"(∀K. compactin X K ⟶ emeasure N K < ∞)"
"(∀f. continuous_map X euclideanreal f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
"(∀f. continuous_map X euclideanreal f ⟶ integrable N f)"
by fastforce
then have tight_on_N:"tight_on X N"
using finite_measure.tight_on_compact_space lh(1) lh(2) by metis
show ?thesis
proof(safe intro!: ex1I[where a=N])
fix M
assume M:"sets M = sets (borel_of X)" "finite_measure M" "(∀f. continuous_map X euclideanreal f ⟶ f ∈ topspace X → {0..1} ⟶ φ (restrict f (topspace X)) = integral⇧L M f)"
then have "tight_on X M"
using finite_measure.tight_on_compact_space lh(1) lh(2) by blast
thus "M = N"
using N(7) M(3) by(auto intro!: finite_tight_measure_eq[OF compact_imp_locally_compact_space[OF lh(1)] lh(2)] tight_on_N)
qed(use N in auto)
qed
theorem Riesz_representation_complex_compact_metrizable:
fixes X :: "'a topology" and φ :: "('a ⇒ complex) ⇒ complex"
assumes lh:"compact_space X" "metrizable_space X"
and plf:"positive_linear_functional_on_CX X φ"
shows "∃!N. sets N = sets (borel_of X) ∧ finite_measure N
∧ (∀f. continuous_map X euclidean f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
proof-
have hd: "Hausdorff_space X"
by (simp add: lh(2) metrizable_imp_Hausdorff_space)
from Riesz_representation_complex_compact_Hausdorff[OF lh(1) hd plf] obtain N where N:
"sets N = sets (borel_of X)" "finite_measure N"
"(∀A∈sets N. emeasure N A = (⨅C∈{C. openin X C ∧ A ⊆ C}. emeasure N C))"
"(∀A. openin X A ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))"
"(∀A∈sets N. emeasure N A < ∞ ⟶ emeasure N A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. emeasure N K))"
"(∀K. compactin X K ⟶ emeasure N K < ∞)"
"(∀f. continuous_map X euclidean f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
"(∀f. continuous_map X euclidean f ⟶ complex_integrable N f)"
by fastforce
then have tight_on_N:"tight_on X N"
using finite_measure.tight_on_compact_space lh(1) lh(2) by metis
show ?thesis
proof(safe intro!: ex1I[where a=N])
fix M
assume M:"sets M = sets (borel_of X)" "finite_measure M" "(∀f. continuous_map X euclidean f ⟶ φ (restrict f (topspace X)) = (∫x. f x ∂M))"
then have tight_on_M:"tight_on X M"
using finite_measure.tight_on_compact_space lh(1) lh(2) by blast
have "(∫x. f x ∂N) = (∫x. f x ∂M)" if f:"continuous_map X euclideanreal f" for f
proof -
have "(∫x. f x ∂N) = Re (∫x. complex_of_real (f x) ∂N)"
by simp
also have "... = Re (φ (λx∈topspace X. complex_of_real (f x)))"
by(intro arg_cong[where f=Re] N(7)[rule_format,symmetric]) (simp add: f)
also have "... = Re (∫x. complex_of_real (f x) ∂M)"
by(intro arg_cong[where f=Re] M(3)[rule_format]) (simp add: f)
also have "... = (∫x. f x ∂M)"
by simp
finally show ?thesis .
qed
thus "M = N"
by(auto intro!: finite_tight_measure_eq[OF compact_imp_locally_compact_space[OF lh(1)] lh(2)] tight_on_N tight_on_M)
qed(use N in auto)
qed
theorem Riesz_representation_real_compact_metrizable_subprob:
fixes X :: "'a topology" and φ :: "('a ⇒ real) ⇒ real"
assumes lh:"compact_space X" "metrizable_space X"
and plf:"positive_linear_functional_on_CX X φ"
and le1: "φ (λx∈topspace X. 1) ≤ 1" and ne: "X ≠ trivial_topology"
shows "∃!N. sets N = sets (borel_of X) ∧ subprob_space N
∧ (∀f. continuous_map X euclideanreal f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
proof -
from Riesz_representation_real_compact_metrizable[OF assms(1-3)]
obtain N where N: "sets N = sets (borel_of X)" "finite_measure N" "(∀f. continuous_map X euclideanreal f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
"⋀M. sets M = sets (borel_of X) ⟹ finite_measure M ⟹ (∀f. continuous_map X euclideanreal f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂M)) ⟹ M = N"
by fastforce
then interpret finite_measure N
by blast
have subN:"subprob_space N"
proof
have "measure N (space N) = (∫x. 1 ∂N)"
by simp
also have "... = φ (λx∈topspace X. 1)"
by(intro N(3)[rule_format,symmetric]) simp
also have "... ≤ 1"
by fact
finally show "emeasure N (space N) ≤ 1"
by (simp add: emeasure_eq_measure)
next
show "space N ≠ {}"
using sets_eq_imp_space_eq[OF N(1)] ne by(auto simp: space_borel_of)
qed
show ?thesis
using N(4)[OF _ subprob_space.axioms(1)] subN N(1,3) by(auto intro!: ex1I[where a=N])
qed
theorem Riesz_representation_real_compact_metrizable_subprob_le1:
fixes X :: "'a topology" and φ :: "('a ⇒ real) ⇒ real"
assumes lh:"compact_space X" "metrizable_space X"
and plf:"positive_linear_functional_on_CX X φ"
and le1: "φ (λx∈topspace X. 1) ≤ 1" and ne: "X ≠ trivial_topology"
shows "∃!N. sets N = sets (borel_of X) ∧ subprob_space N
∧ (∀f. continuous_map X euclideanreal f ⟶ f ∈ topspace X → {0..1} ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
proof -
from Riesz_representation_real_compact_metrizable_le1[OF lh plf]
obtain N where N: "sets N = sets (borel_of X)" "finite_measure N" "(∀f. continuous_map X euclideanreal f ⟶ f ∈ topspace X → {0..1} ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
"⋀M. sets M = sets (borel_of X) ⟹ finite_measure M ⟹ (∀f. continuous_map X euclideanreal f ⟶ f ∈ topspace X → {0..1} ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂M)) ⟹ M = N"
by fastforce
then interpret finite_measure N
by blast
have subN:"subprob_space N"
proof
have "measure N (space N) = (∫x. 1 ∂N)"
by simp
also have "... = φ (λx∈topspace X. 1)"
by(intro N(3)[rule_format,symmetric]) simp_all
also have "... ≤ 1"
by fact
finally show "emeasure N (space N) ≤ 1"
by (simp add: emeasure_eq_measure)
next
show "space N ≠ {}"
using sets_eq_imp_space_eq[OF N(1)] ne by(auto simp: space_borel_of)
qed
show ?thesis
using N(4)[OF _ subprob_space.axioms(1)] subN N(1,3) by(auto intro!: ex1I[where a=N])
qed
theorem Riesz_representation_real_compact_metrizable_prob:
fixes X :: "'a topology" and φ :: "('a ⇒ real) ⇒ real"
assumes lh:"compact_space X" "metrizable_space X"
and plf:"positive_linear_functional_on_CX X φ"
and "φ (λx∈topspace X. 1) = 1"
shows "∃!N. sets N = sets (borel_of X) ∧ prob_space N
∧ (∀f. continuous_map X euclideanreal f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
proof -
from Riesz_representation_real_compact_metrizable[OF lh plf]
obtain N where N: "sets N = sets (borel_of X)" "finite_measure N" "(∀f. continuous_map X euclideanreal f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
"⋀M. sets M = sets (borel_of X) ⟹ finite_measure M ⟹ (∀f. continuous_map X euclideanreal f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂M)) ⟹ M = N"
by fastforce
then interpret finite_measure N
by blast
have probN:"prob_space N"
proof
have "measure N (space N) = (∫x. 1 ∂N)"
by simp
also have "... = φ (λx∈topspace X. 1)"
by(intro N(3)[rule_format,symmetric]) simp
also have "... = 1"
by fact
finally show "emeasure N (space N) = 1"
by (simp add: emeasure_eq_measure)
qed
show ?thesis
using N(4)[OF _ prob_space.finite_measure] probN N(1,3) by(auto intro!: ex1I[where a=N])
qed
theorem Riesz_representation_complex_compact_metrizable_subprob:
fixes X :: "'a topology" and φ :: "('a ⇒ complex) ⇒ complex"
assumes lh:"compact_space X" "metrizable_space X"
and plf:"positive_linear_functional_on_CX X φ"
and le1: "Re (φ (λx∈topspace X. 1)) ≤ 1" and ne: "X ≠ trivial_topology"
shows "∃!N. sets N = sets (borel_of X) ∧ subprob_space N
∧ (∀f. continuous_map X euclidean f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
proof -
from Riesz_representation_complex_compact_metrizable[OF lh plf]
obtain N where N: "sets N = sets (borel_of X)" "finite_measure N" "(∀f. continuous_map X euclidean f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
"⋀M. sets M = sets (borel_of X) ⟹ finite_measure M ⟹ (∀f. continuous_map X euclidean f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂M)) ⟹ M = N"
by fastforce
then interpret finite_measure N
by blast
have subN:"subprob_space N"
proof
have "measure N (space N) = (∫x. 1 ∂N)"
by simp
also have "... = Re (∫x. 1 ∂N)"
by simp
also have "... = Re (φ (λx∈topspace X. 1))"
by(intro arg_cong[where f=Re] N(3)[rule_format,symmetric]) simp
also have "... ≤ 1"
by fact
finally show "emeasure N (space N) ≤ 1"
by (simp add: emeasure_eq_measure)
next
show "space N ≠ {}"
using sets_eq_imp_space_eq[OF N(1)] ne by(auto simp: space_borel_of)
qed
show ?thesis
using N(4)[OF _ subprob_space.axioms(1)] subN N(1,3) by(auto intro!: ex1I[where a=N])
qed
theorem Riesz_representation_complex_compact_metrizable_prob:
fixes X :: "'a topology" and φ :: "('a ⇒ complex) ⇒ complex"
assumes lh:"compact_space X" "metrizable_space X"
and plf:"positive_linear_functional_on_CX X φ"
and "Re (φ (λx∈topspace X. 1)) = 1"
shows "∃!N. sets N = sets (borel_of X) ∧ prob_space N
∧ (∀f. continuous_map X euclidean f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
proof -
from Riesz_representation_complex_compact_metrizable[OF lh plf]
obtain N where N: "sets N = sets (borel_of X)" "finite_measure N" "(∀f. continuous_map X euclidean f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂N))"
"⋀M. sets M = sets (borel_of X) ⟹ finite_measure M ⟹ (∀f. continuous_map X euclidean f ⟶ φ (λx∈topspace X. f x) = (∫x. f x ∂M)) ⟹ M = N"
by fastforce
then interpret finite_measure N
by blast
have probN:"prob_space N"
proof
have "measure N (space N) = (∫x. 1 ∂N)"
by simp
also have "... = Re (∫x. 1 ∂N)"
by simp
also have "... = Re (φ (λx∈topspace X. 1))"
by(intro arg_cong[where f=Re] N(3)[rule_format,symmetric]) simp
also have "... = 1"
by fact
finally show "emeasure N (space N) = 1"
by (simp add: emeasure_eq_measure)
qed
show ?thesis
using N(4)[OF _ prob_space.finite_measure] probN N(1,3) by(auto intro!: ex1I[where a=N])
qed
end