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 (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