Theory Riesz_Representation

(*  Title:   Riesz_Representation.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology
*)

section  ‹The Riesz Representation Theorem›
theory Riesz_Representation
  imports "Regular_Measure"
          "Urysohn_Locally_Compact_Hausdorff"
begin

subsection ‹ Lemmas for Complex-Valued Continuous Maps ›
(* TODO: Move *)
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 {xtopspace 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. (iI. f i x)) has_compact_support_on X"
proof -
  have "support_on (topspace X) (λx. (iI. f i x))  (iI. 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]:
  "(λxtopspace 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
         (xtopspace X. f x  0)  φ (λxtopspace X. f x)  0) 
  (f a. continuous_map X euclidean f  f has_compact_support_on X
          φ (λxtopspace X. a * f x) = a * φ (λxtopspace 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
          φ (λxtopspace X. f x + g x) = φ (λxtopspace X. f x) + φ (λxtopspace 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. xtopspace X  f x  0)  φ (λxtopspace X. f x)  0"
    and pos_lin_functional_on_CX_lin:
    "f a. continuous_map X euclidean f  f has_compact_support_on X
             φ (λxtopspace X. a * f x) = a * φ (λxtopspace 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
            φ (λxtopspace X. f x + g x) = φ (λxtopspace X. f x) + φ (λxtopspace 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. xtopspace X  Re (f x)  0)  (x. x  topspace X  f x  )
         φ (λxtopspace 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  (xtopspace X. f x  0)  φ (λxtopspace X. f x)  0) 
  (f a. continuous_map X euclidean f  φ (λxtopspace X. a * f x) = a * φ (λxtopspace X. f x)) 
  (f g. continuous_map X euclidean f  continuous_map X euclidean g
          φ (λxtopspace X. f x + g x) = φ (λxtopspace X. f x) + φ (λxtopspace 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. xtopspace X  f x  0)  φ (λxtopspace X. f x)  0"
    and pos_lin_functional_on_CX_compact_lin:
    "f a. continuous_map X euclidean f
             φ (λxtopspace X. a * f x) = a * φ (λxtopspace X. f x)"
    "f g. continuous_map X euclidean f  continuous_map X euclidean g
            φ (λxtopspace X. f x + g x) = φ (λxtopspace X. f x) + φ (λxtopspace 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 "φ (λxtopspace X. f x - g x) = φ (λxtopspace X. f x) - φ (λxtopspace 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 "φ (λxtopspace X. f x - g x) = φ (λxtopspace X. f x) - φ (λxtopspace 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 "φ (λxtopspace X. f x)  φ (λxtopspace X. g x)"
proof -
  have "φ (λxtopspace X. f x)  φ (λxtopspace X. f x) + φ (λxtopspace X. g x - f x)"
    by(auto intro!: pos_lin_functional_on_CX_pos[OF assms(1)] assms continuous_map_diff)
  also have "... = φ (λxtopspace 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 "... = φ (λxtopspace 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 "φ (λxtopspace X. f x)  φ (λxtopspace 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 "φ (λxtopspace X. 0) = 0"
proof -
  have "φ (λxtopspace X. 0) = φ (λxtopspace X. 0 * 0)"
    by simp
  also have "... = 0 * φ (λxtopspace 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 "φ (λxtopspace X. - f x) = - φ (λxtopspace 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 "φ (λxtopspace X. - f x) = - φ (λxtopspace 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 "φ (λxtopspace X. (iI. f i x)) = (iI. φ (λxtopspace 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 = φ (λxtopspace X. f a x + (iF. f i x))"
      by(simp add: sum.insert_if[OF ih(1)] ih(2) restrict_def)
    also have "... = φ (λxtopspace X. f a x) + φ (λxtopspace X. (iF. 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 "φ (λxtopspace X. f x)  "
proof -
  have "φ (λxtopspace X. f x) = φ (λxtopspace X. complex_of_real (Re (f x)))"
    by (metis (no_types, lifting) assms(4) of_real_Re restrict_ext)
  also have "... = φ (λxtopspace 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 "... = φ (λxtopspace X. complex_of_real (max 0 (Re (f x)))) - φ (λxtopspace 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 (φ (λxtopspace 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
       φ (λxtopspace X. f x)
          = complex_of_real (φ' (λxtopspace X. Re (f x))) + 𝗂 * complex_of_real (φ' (λxtopspace 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 "φ (λxtopspace X. f x)
          = complex_of_real (φ' (λxtopspace X. Re (f x))) + 𝗂 * complex_of_real (φ' (λxtopspace X. Im (f x)))"
    (is "?lhs = ?rhs")
  proof -
    have "φ (λxtopspace X. f x) = φ (λxtopspace X. Re (f x) + 𝗂 * Im (f x))"
      using complex_eq by presburger
    also have "... = φ (λxtopspace X. complex_of_real (Re (f x))) + φ (λxtopspace 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 "... = φ (λxtopspace X. complex_of_real (Re (f x))) + 𝗂 * φ (λxtopspace 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 (φ' (λxtopspace X. (Re (f x)))) + 𝗂 * complex_of_real (φ' (λxtopspace X. Im (f x)))"
    proof -
      have [simp]: "complex_of_real (φ' (λxtopspace X. Re (f x))) = φ (λxtopspace X. complex_of_real (Re (f x)))"
        (is "?l = ?r")
      proof -
        have "?l = complex_of_real (Re (φ (λxtopspace 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 (φ' (λxtopspace X. Im (f x))) = φ (λxtopspace X. complex_of_real (Im (f x)))"
        (is "?l = ?r")
      proof -
        have "?l = complex_of_real (Re (φ (λxtopspace 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" "xtopspace X. 0  f x"
    show "φ' (λxtopspace X. f x)  0"
    proof -
      have "0  φ (λxtopspace 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 (φ (λxtopspace X. complex_of_real (f x)))"
        by (simp add: less_eq_complex_def)
      also have "... = φ' (λxtopspace 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 "φ' (λxtopspace X. a * f x) = a * φ' (λxtopspace X. f x)"
    proof -
      have *:"φ (λxtopspace X. complex_of_real a * complex_of_real (f x)) = complex_of_real a * φ (λxtopspace X. complex_of_real (f x))"
        using f by(auto intro!: pos_lin_functional_on_CX_lin[OF plf])
      have "φ' (λxtopspace X. a * f x) = Re (φ (λxtopspace 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 (φ (λxtopspace X. complex_of_real (f x))))"
        unfolding * by simp
      also have "... =  a * φ' (λxtopspace 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 "φ' (λxtopspace X. f x + g x) = φ' (λxtopspace X. f x) + φ' (λxtopspace X. g x)"
    proof -
      have *: "φ (λxtopspace X. complex_of_real (f x) + complex_of_real (g x)) = φ (λxtopspace X. complex_of_real (f x)) + φ (λxtopspace X. complex_of_real (g x))"
        using fg by(auto intro!: pos_lin_functional_on_CX_lin[OF plf])
      have "φ' (λxtopspace X. f x + g x) = Re (φ (λxtopspace X. complex_of_real (f x + g x)))"
        by (metis (mono_tags, lifting) φ'_def restrict_apply' restrict_ext)
      also have "... = Re (φ (λxtopspace X. complex_of_real (f x)) + φ (λxtopspace X. complex_of_real (g x)))"
        unfolding of_real_add * by simp
      also have "... = Re (φ (λxtopspace X. complex_of_real (f x))) + Re (φ (λxtopspace X. complex_of_real (g x)))"
        by simp
      also have "... = φ' (λxtopspace X. f x) + φ' (λxtopspace 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. Asets 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. Asets 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. Asets 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. Asets 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. Asets 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. Asets 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. Asets 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. Asets 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. ameasure 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. ameasure 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)
          (Asets 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))
          (Asets 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  φ (λxtopspace 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 {xtopspace 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. {xtopspace X. (if x  topspace X then P x else Q x)  0} = {xtopspace X. P x  0}"
    by fastforce
  have times_unfold[simp]: "P Q. {xtopspace X. P x  Q x} = {xtopspace X. P x}  {xtopspace 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. (in. (?fA (Vi i) (hi i))) 
                          (xK. (in. hi i x) = 1)  (xtopspace X. 0  (in. hi i x)) 
                          (xtopspace X. (in. hi i x)  1)"
    if K:"compactin X K" "i::nat. i  n  openin X (Vi i)" "K  (in. Vi i)" for K Vi n
  proof -
    {
      fix x
      assume x:"x  K"
      have "in. 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. xK. 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  (xK. Ux x)"
      by fastforce
    from compactinD[OF K(1) _ this] xinK(3) obtain K' where K': "finite K'" "K'  K" "K  (xK'. 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  (in. 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  (in. 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 {xtopspace 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 {xtopspace 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 {xtopspace X. hi i x  0}) (topspace X - Vi i)   ?csupp (hi i)"
      by(intro bchoice) auto
    hence "hi. in. ?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 {xtopspace 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 {xtopspace X. gi i x  0}) (topspace X - Vi i)"
      "i. i  n  ?csupp (gi i)"
      by fast
    define hi where "hi  (λn. λxtopspace 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} = {xtopspace X. gi i x  0}  (j<i. {xtopspace X. gi j x  1})"
          using gi by(auto simp: hi_def)
        also have "...  {xtopspace 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:"(in. hi i x) = 1 - (in. (1 - gi i x))" if x:"x  topspace X"
      proof -
        have "(in. hi i x) = (jn. (i<j. (1 - gi i x)) * gi j x)"
          using x by (simp add: hi_def)
        also have "... = 1 - (in. (1 - gi i x))"
        proof -
          have [simp]: "(i<m. 1 - gi i x) * (1 - gi m x) = (im. 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 "(in. hi i x) = 1 - (in. (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 "(in. hi i x) = 1" .
      }
      assume x: "x  topspace X"
      then show "0  (in. hi i x)" "(in. 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} = {xtopspace X. gi i x  0}  (j<i. {xtopspace X. gi j x  1})"
        using gi by(auto simp: hi_def)
      also have "...  {xtopspace X. gi i x  0}"
        by blast
      finally have "X closure_of {x  topspace X. hi i x  0}  X closure_of {xtopspace 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 ` φ ` {(λxtopspace 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:"{(λxtopspace X. f x) |f. ?fA {} f} = {λxtopspace X. 0}"
      by(fastforce intro!: exI[where x="λxtopspace 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 ` φ ` {(λxtopspace 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. (iSuc 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}) 
                    (xX closure_of {xtopspace X. g x  0}. (iSuc 0. hi i x) = 1) 
                    (xtopspace X. 0  (iSuc 0. hi i x))  (xtopspace X. (iSuc 0. hi i x)  1)"
        proof(safe intro!: fApartition[of _ "Suc 0" "λi. case i of 0  V | _  U"])
          have 1:"(iSuc 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  (iSuc 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
          "(iSuc 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}) 
            (xX closure_of {xtopspace X. g x  0}. (iSuc 0. hi i x) = 1) 
            (xtopspace X. 0  (iSuc 0. hi i x))  (xtopspace X. (iSuc 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 {xtopspace X. g x  0}  (iSuc 0. hi i x) = 1"
          unfolding le_Suc_eq le_0_eq by auto
        have "ennreal (φ (λxtopspace X. g x)) = ennreal (φ (λxtopspace X. g x * (hi 0 x + hi (Suc 0) x)))"
        proof -
          have [simp]: "(λxtopspace X. g x) = (λxtopspace 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 = (λxtopspace X. g x * (hi 0 x + hi (Suc 0) x)) x"
            proof cases
              case 1
              then have "x  X closure_of {xtopspace 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 (φ (λxtopspace X. g x * hi 0 x + g x * hi (Suc 0) x))"
          by (simp add: ring_class.ring_distribs(1))
        also have "... = ennreal (φ (λxtopspace X. g x * hi 0 x) + φ (λxtopspace 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 (φ (λxtopspace X. g x * hi 0 x)) + ennreal (φ (λxtopspace 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. (λxtopspace 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="λxtopspace 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. (λxtopspace 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="λxtopspace 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 ` φ ` {(λxtopspace 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 - (in. Vi i)  {0}  X closure_of {x  topspace X. f x  0}  (in. 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}  (in. 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 - (in. Vi i)  {0}" "X closure_of {x  topspace X. f x  0}  (in. Vi i)"
            by blast
          have "ennreal (φ (restrict f (topspace X)))  μ' (in. Vi i)"
            using f(4) f n by(auto intro!: imageI exI[where x=f] Sup_upper simp: μ'_def)
          also have "...  (in. μ' (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 "...  (iSuc n'. μ' (Vi i))"
              using ih by fastforce
            finally show ?case .
          qed simp
          also have "... = (in. μ (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 ` φ ` {(λxtopspace X. f x) | f. ?fK K f}))" if K: "compactin X K" for K
  proof -
    have le1: "μ K  ennreal (φ (λxtopspace 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)) * φ (λxtopspace X. f x))" for n
      proof -
        let ?a = "(real n + 1) / (real n + 2)"
        define V where "V  {xtopspace 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 ` φ ` {(λxtopspace X. f x) |f. ?fA V f}))"
          by(simp add: μ'_def)
        also have "...  (1 / ?a) * φ (λxtopspace X. f x)"
          unfolding Sup_le_iff
        proof (safe intro!: ennreal_leI)
          fix g
          assume g: "?iscont g" "?csupp g" "X closure_of {xtopspace 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  φ (λxtopspace 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 (φ (λxtopspace 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 ` φ ` {(λxtopspace 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 (φ (λxtopspace 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 {xtopspace X. f x  0}) (topspace X - V)"
        "compactin X (X closure_of {xtopspace 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="λxtopspace X. f x"] simp: disjnt_iff)
      qed fact
      thus "aennreal ` φ ` {(λxtopspace X. f x)|f. ?fK K f}. a < y"
        using f compactin_subset_topspace[OF K] by(auto intro!: exI[where x="λxtopspace X. f x"])
    qed
  qed
  have μ_K: "μ K  ennreal (φ (λxtopspace 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 (φ (λxtopspace 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 (φ (λxtopspace 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 (φ (λxtopspace X. g x)) < μ (K1  K2) + ennreal e"
          using e by fastforce
        have "μ K1 + μ K2  ennreal (φ (λxtopspace X. (1 - f x) * g x)) + ennreal (φ (λxtopspace X. f x * g x))"
        proof(rule add_mono)
          show "μ K1  ennreal (φ (λxtopspace 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 (φ (λxtopspace 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 (φ (λxtopspace X. (1 - f x)*g x) + φ (λxtopspace 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 (φ (λxtopspace 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 (φ (λxtopspace 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 "(nN. μ (En n))  μ ( (range En)) + ennreal e" for N
        proof -
          have "(nN. μ (En n))  (nN. μ (Hn n) + ennreal ((1 / 2) ^ Suc n) * ennreal e)"
            by(rule sum_mono) (use Hn(3) order_less_le in auto)
          also have "... = (nN. μ (Hn n)) + (nN. ennreal ((1 / 2) ^ Suc n) * ennreal e)"
            by(rule sum.distrib)
          also have "... = μ (nN. Hn n) + (nN. ennreal ((1 / 2) ^ Suc n) * ennreal e)"
          proof -
            have "(nN. μ (Hn n)) = μ (nN. 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)) + (nN. ennreal ((1 / 2) ^ Suc n) * ennreal e)"
            using Hn(2) by(auto intro!: μ_mono)
          also have "...  μ ( (range En)) + ennreal e"
          proof -
            have "(nN. ennreal ((1 / 2) ^ Suc n) * ennreal e) = ennreal (nN. ((1 / 2) ^ Suc n)) * ennreal e"
              unfolding sum_distrib_right[symmetric] by simp
            also have "... = ennreal e * ennreal (nN. ((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 < (nN. μ (En n))"
            by fastforce
          obtain e where e: "e > 0" "y < (nN. μ (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 < (nN. μ (En n)) - ennreal e"
            by fact
          also have "...  (nN. μ (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 "... = (nN. μ (Hn n)) + (nN. ennreal ((1 / 2) ^ Suc n) * ennreal e) - ennreal e"
            by (simp add: sum.distrib)
          also have "... = μ (nN. Hn n) + (nN. ennreal ((1 / 2) ^ Suc n) * ennreal e) - ennreal e"
          proof -
            have "(nN. μ (Hn n)) = μ (nN. 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 "...  μ (nN. 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 "... = μ (nN. Hn n) + (n. ennreal ((1 / 2) ^ Suc n)) * ennreal e - ennreal e"
            using ennreal_suminf_multc by presburger
          also have "... = μ (nN. 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 "... = μ (nN. Hn n)"
            by simp
          finally show "Bex (μ ` {K. K   (range En)  compactin X K}) ((<) y)"
            using Hn by(auto intro!: exI[where x="nN. 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': "(iI. Ai i)  Mf" if "finite I" "(i. i  I  Ai i  Mf)" for Ai and I :: "nat set"
  proof -
    have "(iI. Ai i  Mf)  (iI. 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  (in. 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  (in. 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 "mUNIV. 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:"(Asets 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:"(Asets 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 {xtopspace 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  φ (λxtopspace X. f x) = (x. f x N)"
  proof safe
    have 1: "φ (λxtopspace X. f x)  (x. f x N)" if f:"?iscont f" "?csupp f" for f
    proof -
      let ?K = "X closure_of {xtopspace 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:"φ (λxtopspace 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. {xtopspace X. yn m < f x  f x  yn (Suc m)}  ?K)"
        have En_sets[measurable]: "En m  sets N" for m
        proof -
          have "{xtopspace 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 = (iL. 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  (iL. 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 
                   (xVi. 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  {xtopspace X. yn i < f x  f x < 1 / real (Suc n) + yn i}"
          have "En i  Vi'"
          proof -
            have "En i = En i  {xtopspace 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  (iL. 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  (iL. hi i x) = 1" "x. x  topspace X  0  (iL. hi i x)"
         "x. x  topspace X  (iL. hi i x)  1"
          by blast
        have f_sum_hif: "(iL. 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:"(iL. measure N (En i)) = measure N ?K"
        proof -
          have "(iL. measure N (En i)) = measure N (iL. 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  (iL. φ (λxtopspace 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 (φ (λxtopspace X. iL. 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. iL. hi i x"] has_compact_support_on_sum hi continuous_map_sum)
          also have "... =  ennreal (iL. φ (λxtopspace 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)) = φ (λxtopspace X. iL. f x * hi i x)"
          using f_sum_hif restrict_ext by force
        also have "... = (iL. φ (λxtopspace 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 "...  (iL. φ (λxtopspace 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 "... = (iL. (1 / (Suc n) + yn i) * φ (λxtopspace X. hi i x))"
          by(intro Finite_Cartesian_Product.sum_cong_aux linear hi) auto
        also have "... = (iL. (1 / (Suc n) + yn i + (B + 1)) * φ (λxtopspace X. hi i x))
                          - (iL. (B + 1) * φ (λxtopspace X. hi i x))"
          by(simp add: sum_subtractf[symmetric] distrib_right)
        also have "... = (iL. (1 / (Suc n) + yn i + (B + 1)) * φ (λxtopspace X. hi i x))
                          - (B + 1) * (iL. φ (λxtopspace X. hi i x))"
          by (simp add: sum_distrib_left)
        also have "...  (iL. (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 "... = (iL. (yn i - 1 / (Suc n)) * measure N (En i)) + 2 * (iL. ((1 / Suc n)) * measure N (En i))
                          + (iL. (B + 1) * measure N (En i))
                          + (iL. (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 "... = (iL. (yn i - 1 / (Suc n)) * measure N (En i)) + 1 / Suc n * 2* measure N ?K
                          + (iL. (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 "...  (iL. (yn i - 1 / (Suc n)) * measure N (En i)) + 1 / Suc n * 2* measure N ?K
                          + (iL. (1 / (Suc n) + B + (B + 1)) * (1 / Suc n / Suc L))"
        proof -
          have "(iL. (1 / (Suc n) + yn i + (B + 1)) * (1 / Suc n / Suc L))
                  (iL. (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 "... = (iL. (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 "... = (iL. (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 "(iL. (yn i - 1 / (Suc n)) * measure N (En i))  (x. f x N)" (is "?l  ?r")
          proof -
            have "?l = (iL. (x. (yn i - 1 / (Suc n)) * indicator (En i) x N))"
              by simp
            also have "... = (x. (iL. (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" | "iL. x  En i"
                by blast
              then show " (iL. (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 "(iL. (yn i - 1 / real (Suc n)) * indicat_real (En i) x)
                        = (jL. 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. iL. (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 "φ (λxtopspace X. f x) = (x. f x N)"
    proof(rule antisym)
      have "- φ (λxtopspace X. f x) = φ (λxtopspace 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 "φ (λxtopspace 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)
          (Asets 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))
          (Asets 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  φ (λxtopspace 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 (φ (λxtopspace 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)" "(Asets 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}))"
     "(Asets 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  ?φ' (λxtopspace 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: "φ (λxtopspace X. f x) = (x. f x N)"
    if f:"continuous_map X euclidean f" "f has_compact_support_on X" for f
  proof -
    have "φ (λxtopspace X. f x)
          = complex_of_real (?φ' (λxtopspace X. Re (f x))) + 𝗂 * complex_of_real (?φ' (λxtopspace 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 *:"?φ' (λxtopspace X. Re (f x)) = (x. Re (f x) N)"
        using f by(intro MN(7)) auto
      have **:"?φ' (λxtopspace 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)
          (Asets 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))
          (Asets 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  φ (λxtopspace 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)" "(Asets 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}))"
    "(Asets 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  φ (λxtopspace 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: "Asets 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: "Asets 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  φ (λxtopspace 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 "φ (λxtopspace 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)
          (Asets 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))
          (Asets 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  φ (λxtopspace 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)" "(Asets 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}))"
    "(Asets 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  φ (λxtopspace 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: "Asets 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: "Asets 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  φ (λxtopspace 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 "φ (λxtopspace 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
          (Asets 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))
          (Asets 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  φ (λxtopspace 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)"
  "(Asets 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))"
  "(Asets 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  φ (λxtopspace 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
          (Asets 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))
          (Asets 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  φ (λxtopspace 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)"
  "(Asets 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))"
  "(Asets 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  φ (λxtopspace 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  φ (λxtopspace 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"
  "(Asets 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))"
  "(Asets 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  φ (λxtopspace 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)) = integralL 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}  φ (λxtopspace 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"
  "(Asets 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))"
  "(Asets 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  φ (λxtopspace 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)) = integralL 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  φ (λxtopspace 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"
  "(Asets 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))"
  "(Asets 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  φ (λxtopspace 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 (φ (λxtopspace 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: "φ (λxtopspace 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  φ (λxtopspace 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   φ (λxtopspace X. f x) = (x. f x N))"
    "M. sets M = sets (borel_of X)  finite_measure M  (f. continuous_map X euclideanreal f   φ (λxtopspace 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 "... = φ (λxtopspace 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: "φ (λxtopspace 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}  φ (λxtopspace 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}   φ (λxtopspace 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}  φ (λxtopspace 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 "... = φ (λxtopspace 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 "φ (λxtopspace X. 1) = 1"
    shows "∃!N. sets N = sets (borel_of X)  prob_space N
            (f. continuous_map X euclideanreal f  φ (λxtopspace 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   φ (λxtopspace X. f x) = (x. f x N))"
    "M. sets M = sets (borel_of X)  finite_measure M  (f. continuous_map X euclideanreal f   φ (λxtopspace 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 "... = φ (λxtopspace 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 (φ (λxtopspace 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  φ (λxtopspace 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   φ (λxtopspace X. f x) = (x. f x N))"
    "M. sets M = sets (borel_of X)  finite_measure M  (f. continuous_map X euclidean f   φ (λxtopspace 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 (φ (λxtopspace 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 (φ (λxtopspace X. 1)) = 1"
    shows "∃!N. sets N = sets (borel_of X)  prob_space N
            (f. continuous_map X euclidean f  φ (λxtopspace 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   φ (λxtopspace X. f x) = (x. f x N))"
    "M. sets M = sets (borel_of X)  finite_measure M  (f. continuous_map X euclidean f   φ (λxtopspace 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 (φ (λxtopspace 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