Theory Riesz_Representation.Regular_Measure

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

section  ‹Regular Measures ›
theory Regular_Measure
  imports "HOL-Probability.Probability"
          "Standard_Borel_Spaces.StandardBorel"
          "Urysohn_Locally_Compact_Hausdorff"
begin

context Metric_space
begin

lemma nbh_add: "(⋃b∈(⋃a∈A. mball a e). mball b f) ⊆ (⋃a∈A. mball a (e + f))"
proof clarify
  fix a x b
  assume h:"a ∈ A" "b ∈ mball a e" "x ∈ mball b f"
  show "x ∈ (⋃a∈A. mball a (e + f))"
  proof(rule UN_I[OF h(1)])
    show "x ∈ mball a (e + f)"
      using h triangle by fastforce
  qed
qed

lemma nbh_subset:
  assumes A: "A ⊆ M" and e: "e > 0"
  shows "A ⊆ (⋃a∈A. mball a e)"
  using A e by auto

lemma nbh_decseq:
  assumes "decseq an"
  shows "decseq (λn. ⋃a∈A. mball a (an n))"
proof(safe intro!: decseq_SucI)
  fix n a b
  assume "a ∈ A" "b ∈ mball a (an (Suc n))"
  with decseq_SucD[OF assms] show "b ∈ (⋃c∈A. mball c (an n))"
    by(auto intro!: bexI[where x=a] simp: frac_le order_less_le_trans)
qed

lemma nbh_Inter_closure_of:
  assumes A: "A ≠ {}" "A ⊆ M"
      and an:"⋀n. an n > 0" "decseq an" "an ⇢ 0"
    shows "(⋂n. ⋃a∈A. mball a (an n)) = mtopology closure_of A"
proof safe
  fix x
  assume x:"x ∈ (⋂n. ⋃a∈A. mball a (an n))"
  show "x ∈ mtopology closure_of A"
    unfolding metric_closure_of
  proof safe
    fix r :: real
    assume "0 < r"
    from LIMSEQ_D[OF an(3) this] an(1) obtain N where N: "⋀n. n ≥ N ⟹ an n < r"
      by fastforce
    show "∃y∈A. y ∈ mball x r"
    proof(rule ccontr)
      assume "¬ (∃y∈A. y ∈ mball x r)"
      then have 1:"∀y∈A. y ∉ mball x r"
        by auto
      obtain a where a:"a ∈ A" "x ∈ mball a (an N)"
        using x by auto
      with N[of N] have "a ∈ mball x (an N)" "mball x (an N) ⊆ mball x r"
        by (auto simp: commute)
      with a(1) 1 show False by auto
    qed
  qed(use x in auto)
next
  fix x n
  assume "x ∈ mtopology closure_of A"
  then have "x ∈ M" "∀r>0. ∃y∈A. y ∈ mball x r"
    by(auto simp: metric_closure_of)
  with an(1)[of n] obtain y where y:"y ∈ A" "y ∈ mball x (an n)"
    by auto
  thus "x ∈ (⋃a∈A. mball a (an n))"
    by(auto intro!: bexI[where x=y] simp: commute)
qed

end

lemma(in finite_measure)
  assumes "range A ⊆ sets M" "disjoint_family A"
  shows suminf_measure:"(∑i. measure M (A i)) = measure M (⋃i. A i)"
    and summable_measure: "summable (λi. measure M (A i))"
  using finite_measure_UNION[OF assms] by(auto dest: sums_unique simp: summable_def)

text ‹We refer to the lecture note~\cite{probmetric}.›
text ‹Inner regular and outer regular with abstract topologies.›

definition inner_regular :: "'a topology ⇒ 'a measure ⇒ bool" where
"inner_regular X M ⟷ sets M = sets (borel_of X) ∧ (∀A∈sets M. M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. M C))"

definition outer_regular :: "'a topology ⇒ 'a measure ⇒ bool" where
"outer_regular X M ⟷ sets M = sets (borel_of X) ∧ (∀A∈sets M. M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. M C))"

definition regular_measure :: "'a topology ⇒ 'a measure ⇒ bool" where
"regular_measure X M ⟷ inner_regular X M ∧ outer_regular X M"

lemma
  shows inner_reguarI: "sets M = sets (borel_of X) ⟹ (⋀A. A ∈ sets M
      ⟹ M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. M C)) ⟹ inner_regular X M"
    and inner_reguarD: "inner_regular X M ⟹ sets M = sets (borel_of X)"
    "inner_regular X M ⟹ A ∈ sets M ⟹ M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. M C)"
  by(auto simp: inner_regular_def)

lemma
  shows outer_reguarI: "sets M = sets (borel_of X)
     ⟹ (⋀A. A ∈ sets M ⟹ M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. M C)) ⟹ outer_regular X M"
    and outer_reguarD: "outer_regular X M ⟹ sets M = sets (borel_of X)"
    "outer_regular X M ⟹ A ∈ sets M ⟹ M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. M C)"
  by(auto simp: outer_regular_def)

lemma
  shows regular_measureI: "inner_regular X M ⟹ outer_regular X M ⟹ regular_measure X M"
    and regular_measureD:
    "regular_measure X M ⟹ inner_regular X M" "regular_measure X M ⟹ outer_regular X M"
  by(auto simp: regular_measure_def)

lemma inner_regular_finite_measure:
  assumes "finite_measure M"
  shows "inner_regular X M ⟷
         sets M = sets (borel_of X) ∧ (∀A∈sets M. measure M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. measure M C))"
  unfolding inner_regular_def
proof safe
  interpret M: finite_measure M by fact
  fix A
  assume "A ∈ sets M" "∀A∈sets M. M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. M C)"
  then have 1:"M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. M C)"
    by blast
  have "ennreal (measure M A) = ennreal (⨆C∈{C. closedin X C ∧ C ⊆ A}. measure M C)"
  proof -
    have "ennreal (measure M A) = M A"
      by (simp add: M.emeasure_eq_measure)
    also have "... = (⨆C∈{C. closedin X C ∧ C ⊆ A}. M C)"
      by fact
    also have "... = (⨆C∈{C. closedin X C ∧ C ⊆ A}. ennreal (measure M C))"
      by (simp add: M.emeasure_eq_measure)
    also have "... = ennreal (⨆C∈{C. closedin X C ∧ C ⊆ A}. measure M C)"
      by(intro ennreal_SUP[symmetric]) (use calculation in fastforce)+
    finally show ?thesis .
  qed
  moreover have "(⨆C∈{C. closedin X C ∧ C ⊆ A}. measure M C) ≥ 0"
    by(subst le_cSUP_iff)
      (auto intro!: bdd_aboveI[where M="measure M (space M)"] M.bounded_measure exI[where x="{}"])
  ultimately show "measure M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. measure M C)"
    by simp
next
  interpret M: finite_measure M by fact
  fix A
  assume "A ∈ sets M" "∀A∈sets M. measure M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. measure M C)"
  then have 1:"measure M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. measure M C)"
    by blast
  show "M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. M C)"
  proof -
    have "M A = ennreal (measure M A)"
      by(rule M.emeasure_eq_measure)
    also have "... = ennreal (⨆C∈{C. closedin X C ∧ C ⊆ A}. measure M C)"
      by (simp add: 1)
    also have "... = (⨆C∈{C. closedin X C ∧ C ⊆ A}. ennreal (measure M C))"
      by(intro ennreal_SUP)
        (metis (mono_tags, lifting) M.emeasure_eq_measure M.emeasure_finite SUP_least emeasure_space top.extremum_unique,blast)
    finally show ?thesis
      by (simp add: M.emeasure_eq_measure)
  qed
qed

lemma(in finite_measure)
  shows inner_regularI: "sets M = sets (borel_of X) ⟹ (⋀A. A ∈ sets M
     ⟹ measure M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. measure M C)) ⟹ inner_regular X M"
    and inner_regularD:
 "inner_regular X M ⟹ A ∈ sets M ⟹ measure M A = (⨆C∈{C. closedin X C ∧ C ⊆ A}. measure M C)"
  by(auto simp: inner_regular_finite_measure finite_measure_axioms)

lemma outer_regular_finite_measure:
  assumes "finite_measure M"
  shows "outer_regular X M ⟷ sets M = sets (borel_of X) ∧ (∀A∈sets M. measure M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. measure M C))"
  unfolding outer_regular_def
proof safe
  interpret M: finite_measure M by fact
  fix A
  assume A:"A ∈ sets M" "∀A∈sets M. measure M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. measure M C)"
     and sets_M: "sets M = sets (borel_of X)"
  then have 1:"measure M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. measure M C)"
    by blast
  have [simp]:"openin X (space M)"
    by (simp add: sets_M sets_eq_imp_space_eq space_borel_of)
  show "M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. M C)"
  proof -
    have "enn2ereal (M A) = ereal (measure M A)"
      by (simp add: M.emeasure_eq_measure)
    also have "... = ereal (⨅C∈{C. openin X C ∧ A ⊆ C}. measure M C)"
      by (simp add: 1)
    also have "... = (⨅ (ereal ` measure M ` {C. openin X C ∧ A ⊆ C}))"
      by(intro ereal_Inf') (auto intro!: bdd_belowI[where m=0] exI[where x="space M"] sets.sets_into_space[OF A(1)])
    also have "... = (⨅C∈{C. openin X C ∧ A ⊆ C}. enn2ereal (M C))"
      by (metis (no_types, lifting) M.emeasure_eq_measure enn2ereal_ennreal image_cong image_image measure_nonneg)
    also have "... = enn2ereal (⨅C∈{C. openin X C ∧ A ⊆ C}. M C)"
      by (simp add: Inf_ennreal.rep_eq image_image)
    finally show ?thesis
      using enn2ereal_inject by blast
  qed
next
  interpret M: finite_measure M by fact
  fix A
  assume A:"A ∈ sets M" "∀A∈sets M. M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. M C)"
     and sets_M: "sets M = sets (borel_of X)"
  then have 1:"M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. M C)"
    by blast
  have [simp]:"openin X (space M)"
    by (simp add: sets_M sets_eq_imp_space_eq space_borel_of)
  show "measure M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. measure M C)"
  proof -
    have "ereal (measure M A) = enn2ereal (M A)"
      by (simp add: M.emeasure_eq_measure)
    also have "... = enn2ereal (⨅C∈{C. openin X C ∧ A ⊆ C}. M C)"
      by(simp add: 1)
    also have "... = (⨅ (ereal ` measure M ` {C. openin X C ∧ A ⊆ C}))"
      by(auto simp: Inf_ennreal.rep_eq image_image M.emeasure_eq_measure)
    also have "... = ereal (⨅C∈{C. openin X C ∧ A ⊆ C}. measure M C)"
      by(intro ereal_Inf'[symmetric]) (auto intro!: bdd_belowI[where m=0] exI[where x="space M"] sets.sets_into_space[OF A(1)])
    finally show ?thesis
      by blast
  qed
qed

lemma(in finite_measure)
  shows outer_regularI: "sets M = sets (borel_of X) ⟹ (⋀A. A ∈ sets M
      ⟹ measure M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. measure M C)) ⟹ outer_regular X M"
    and outer_regularD: "outer_regular X M ⟹ A ∈ sets M
      ⟹ measure M A = (⨅C∈{C. openin X C ∧ A ⊆ C}. measure M C)"
  by(auto simp: outer_regular_finite_measure finite_measure_axioms)

text ‹Abstract version of @{thm inner_regular} and @{thm outer_regular}.›
lemma(in finite_measure)
  assumes "metrizable_space X" "sets (borel_of X) = sets M"
    shows inner_regular':"inner_regular X M"
      and outer_regular':"outer_regular X M"
proof -
  let ?Sup = "λA. (⨆C∈{C. closedin X C ∧ C ⊆ A}. measure M C)"
  let ?Inf = "λA. (⨅C∈{C. openin X C ∧ A ⊆ C}. measure M C)"
  {
    fix A
    assume A[measurable]: "A ∈ sets M"
    obtain d where d: "Metric_space (topspace X) d" "Metric_space.mtopology (topspace X) d = X"
      by (metis Metric_space.topspace_mtopology assms(1) metrizable_space_def)
    then interpret d: Metric_space "topspace X" d by simp
    have sets[measurable (raw)]: "⋀A. openin X A ⟹ A ∈ sets M"  "⋀A. closedin X A ⟹ A ∈ sets M"
      "⋀A. openin d.mtopology A ⟹ A ∈ sets M" "⋀A. closedin d.mtopology A ⟹ A ∈ sets M"
      by(auto simp: d assms(2)[symmetric] dest: borel_of_open borel_of_closed)
    have bdd[simp]: "⋀A. bdd_above (measure M ` {C. closedin X C ∧ C ⊆ A})"
      "⋀A. bdd_below (measure M ` {C. closedin X C ∧ C ⊆ A})"
      "⋀A. bdd_above (measure M ` {C. openin X C ∧ A ⊆ C})"
      "⋀A. bdd_below (measure M ` {C. openin X C ∧ A ⊆ C})"
      by(auto intro!: bdd_aboveI[where M="measure M (space M)"] bdd_belowI[where m=0] bounded_measure)
    have ne[simp]: "{C. closedin X C ∧ C ⊆ A} ≠ {}" "A ∈ sets M ⟹ {C. openin X C ∧ A ⊆ C} ≠ {}" for A
      using sets.sets_into_space[of A M,simplified space_borel_of]
        sets_eq_imp_space_eq[OF assms(2),simplified space_borel_of] by blast+
    have 1:"measure M A ≤ ?Inf A" "measure M A ≥ ?Sup A"
      using sets.sets_into_space[OF A[simplified assms(2)[symmetric]],simplified space_borel_of]
            openin_topspace closedin_topspace sets.sets_into_space[OF A]
      by(fastforce intro!: le_cInf_iff[where a="measure M A"
                                         and S="measure M ` {C. openin X C ∧ A ⊆ C}",THEN iffD2]
                           cSup_le_iff[where a="measure M A"
                                         and S="measure M ` {C. closedin X C ∧ C ⊆ A}",THEN iffD2]
                bdd_aboveI[where M="measure M (space M)"] bdd_belowI[where m=0] finite_measure_mono)+
    have setsM: "sigma_sets (topspace X) {U. closedin X U} = sets M"
      using sets_eq_imp_space_eq[OF assms(2)] by(auto simp: assms(2)[symmetric] sets_borel_of_closed)
    have 2:"Int_stable {U. closedin X U}" "{U. closedin X U} ⊆ Pow (topspace X)"
      by(auto dest: closedin_subset intro!: Int_stableI)

    have "measure M A ≤ ?Sup A ∧ measure M A ≥ ?Inf A"
    proof(rule sigma_sets_induct_disjoint[OF 2 A[simplified setsM[symmetric]]])
      fix a
      assume "a ∈ {U. closedin X U}"
      then have a[measurable]: "closedin X a" "a ∈ sets M"
        by(auto simp: assms(2)[symmetric] borel_of_closed)
      show "measure M a ≤ ?Sup a ∧ measure M a ≥ ?Inf a"
      proof (cases "a = {}")
        case empty:True
        thus ?thesis
          by(auto intro!: cINF_lower[where f="measure M" and x="{}",simplified] bdd_belowI[where m=0]
                    simp: empty)
      next
        case ne:False
        show ?thesis
        proof
          have "measure M a = ?Sup a"
            by(rule cSup_eq_maximum[symmetric],insert a(1),auto intro!: finite_measure_mono)
          thus "measure M a ≤ ?Sup a" by simp
        next
          show "measure M a ≥ ?Inf a"
          proof -
            have "?Inf a ≤ (⨅n. measure M (⋃x∈a. d.mball x (1 / Suc n)))"
            proof(rule cInf_superset_mono)
              show "range (λn. measure M (⋃x∈a. d.mball x (1 / real (Suc n)))) ⊆ measure M ` {C. openin X C ∧ a ⊆ C}"
              proof clarify
                fix n
                have "(⋃x∈a. d.mball x (1 / (1 + real n))) ∈ {C. openin X C ∧ a ⊆ C}"
                  using d.openin_mball[simplified d(2)]  closedin_subset[OF a(1)] by auto
                thus "measure M (⋃x∈a. d.mball x (1 / (Suc n))) ∈ measure M ` {C. openin X C ∧ a ⊆ C}"
                  by auto
              qed
            qed auto
            also have "... = measure M a"
            proof -
              have [measurable]: "(⋃x∈a. d.mball x (1 / (1 + real n))) ∈ sets M" for n
                by(auto simp: assms(2)[symmetric] d.openin_mball[simplified d] intro!: borel_of_open openin_clauses(3))
              have 0:"decseq (λn. ⋃x∈a. d.mball x (1 / (1 + real n)))"
                by(rule d.nbh_decseq) (auto intro!: decseq_SucI simp: frac_le)
              have 1:"decseq (λn. measure M (⋃x∈a. d.mball x (1 / (1 + real n))))"
                by(rule decseq_SucI,rule finite_measure_mono) (use decseq_SucD[OF 0] in auto)
              have 2:"(λn. measure M (⋃x∈a. d.mball x (1 / (1 + real n)))) ⇢ (⨅n. measure M (⋃x∈a. d.mball x (1 / Suc n)))"
                by(auto intro!: LIMSEQ_decseq_INF[OF _ 1] bdd_belowI[where m=0])
              moreover have "(λn. measure M (⋃x∈a. d.mball x (1 / (1 + real n)))) ⇢ measure M a"
              proof -
                have "(⋂n. (⋃x∈a. d.mball x (1 / (1 + real n)))) = d.mtopology closure_of a"
                  by(rule d.nbh_Inter_closure_of[OF ne])
                    (auto simp: closedin_subset[OF a(1)] frac_le
                      intro!: decseq_SucI LIMSEQ_inverse_real_of_nat[simplified inverse_eq_divide,simplified])
                also have "... = a"
                  by(auto simp: closure_of_eq d a)
                finally have "(⋂n. (⋃x∈a. d.mball x (1 / (1 + real n)))) = a" .
                moreover have "(λn. measure M (⋃x∈a. d.mball x (1 / (1 + real n))))
                                ⇢ measure M (⋂n. (⋃x∈a. d.mball x (1 / (1 + real n))))"
                  by(auto intro!: finite_Lim_measure_decseq simp: 0)
                ultimately show ?thesis by simp
              qed
              ultimately show ?thesis
                by(auto dest: LIMSEQ_unique)
            qed
            finally show "?Inf a ≤ measure M a" .
          qed
        qed
      qed
    next
      show "measure M {} ≤ ?Sup {} ∧ measure M {} ≥ ?Inf {}"
        by(auto intro!: cINF_lower[where f="measure M" and x="{}",simplified] bdd_belowI[where m=0])
    next
      fix a
      assume "a ∈ sigma_sets (topspace X) {U. closedin X U}"
        and ih:"measure M a ≤ ?Sup a ∧ measure M a ≥ ?Inf a"
      then have [measurable]:"a ∈ sets M"
        by(simp add: setsM)
      show "measure M (topspace X - a) ≤ ?Sup (topspace X - a) ∧ measure M (topspace X - a) ≥ ?Inf (topspace X - a)"
      proof
        show "measure M (topspace X - a) ≤ ?Sup (topspace X - a)"
        proof(safe intro!: le_cSup_iff_less[THEN iffD2])
          fix y
          assume "y < measure M (topspace X - a)"
          then have "measure M a < measure M (space M) - y"
            by(auto simp: sets_eq_imp_space_eq[OF assms(2),simplified space_borel_of] finite_measure_compl)
          then obtain U where U: "openin X U" "a ⊆ U" "measure M U ≤ measure M (space M) - y"
            using ih by(auto simp:  cInf_le_iff_less[OF ne(2) bdd(4)])
          show "∃C∈{C. closedin X C ∧ C ⊆ topspace X - a}. y ≤ Sigma_Algebra.measure M C"
          proof(safe intro!: bexI[where x="topspace X - U"])
            have [arith]:"measure M a ≤ measure M U"
              using U by(auto intro!: finite_measure_mono)
            show "y ≤ measure M (topspace X - U)"
              using U by(auto simp: sets_eq_imp_space_eq[OF assms(2),simplified space_borel_of] finite_measure_compl)
          qed(use U in auto)
        qed auto
      next
        show "?Inf (topspace X - a) ≤ measure M (topspace X - a)"
        proof(rule cInf_le_iff_less[THEN iffD2])
          show "∀y>measure M (topspace X - a). ∃C∈{C. openin X C ∧ topspace X - a ⊆ C}. measure M C ≤ y"
          proof safe
            fix y
            assume "measure M (topspace X - a) < y"
            then have "measure M (space M) - y < measure M a"
              by(auto simp: sets_eq_imp_space_eq[OF assms(2),simplified space_borel_of] finite_measure_compl)
            then obtain C where C: "closedin X C" "C ⊆ a" "measure M (space M) - y ≤ measure M C"
              using ih by(auto simp: le_cSup_iff_less[OF ne(1) bdd(1)])
            show "∃C∈{C. openin X C ∧ topspace X - a ⊆ C}.  measure M C ≤ y"
            proof(safe intro!: bexI[where x="topspace X - C"])
              have [arith]:"measure M C ≤ measure M a"
                using C by(auto intro!: finite_measure_mono)
              show "measure M (topspace X - C) ≤ y"
                using C by(auto simp: sets_eq_imp_space_eq[OF assms(2),simplified space_borel_of] finite_measure_compl)
            qed(use C in auto)
          qed
        qed auto
      qed
    next
      fix a :: "nat ⇒ _"
      assume h: "disjoint_family a" "range a ⊆ sigma_sets (topspace X) {U. closedin X U}"
        and ih: "⋀i. measure M (a i) ≤ ?Sup (a i) ∧ ?Inf (a i) ≤ measure M (a i)"
      then have a[measurable]: "⋀i. a i ∈ sets M"
        by(simp add: setsM)
      show "measure M (⋃i. a i) ≤ ?Sup (⋃i. a i) ∧ ?Inf (⋃i. a i) ≤ measure M (⋃i. a i)"
      proof
        show "measure M (⋃i. a i) ≤ ?Sup (⋃i. a i)"
        proof(rule le_cSup_iff_less[THEN iffD2])
          show "∀y< measure M (⋃ (range a)). ∃C∈{C. closedin X C ∧ C ⊆ ⋃ (range a)}. y ≤ measure M C"
          proof safe
            fix y
            assume "y < measure M (⋃i. a i)"
            also have "... = (∑i. measure M (a i))"
              by(rule suminf_measure[OF _ h(1),symmetric]) auto
            finally obtain N where N: "y < (∑i<N. measure M (a i))"
              by (meson linorder_not_less measure_nonneg suminf_le_const summableI_nonneg_bounded)
            consider "N = 0" | "N > 0" by auto
            then show "∃C∈{C. closedin X C ∧ C ⊆ ⋃ (range a)}. y ≤ measure M C"
            proof cases
              case 1
              with N show ?thesis by(auto intro!: exI[where x="{}"])
            next
              case [arith]:2
              define e where "e ≡ ((∑i<N. measure M (a i)) - y) / N"
              have e[arith]: "e > 0"
                using N by(auto simp: e_def)
              hence "⋀i. measure M (a i) - e < measure M (a i)" by auto
              hence "∀i. ∃Ci. closedin X Ci ∧ Ci ⊆ a i ∧ measure M (a i) - e ≤ measure M Ci"
                using ih[simplified le_cSup_iff_less[OF ne(1) bdd(1)]] by auto
              then obtain Ci where Ci: "⋀i. closedin X (Ci i)"
                "⋀i. Ci i ⊆ a i" "⋀i. measure M (a i) - e ≤ measure M (Ci i)"
                by metis
              with h have Ci_d:"disjoint_family_on Ci {..<N}"
                by(auto simp: disjoint_family_on_def) blast
              show ?thesis
              proof(safe intro!: bexI[where x="⋃ (Ci ` {..<N})"])
                have "y ≤ (∑i<N. measure M (a i)) - ((∑i<N. measure M (a i)) - y)" by auto
                also have "... ≤ (∑i<N. measure M (a i) - e)"
                  by(auto simp: e_def sum_subtractf)
                also have "... ≤ (∑i<N. measure M (Ci i))"
                  using Ci by(auto intro!: sum_mono)
                also have "... = measure M (⋃ (Ci ` {..<N}))"
                  by(rule finite_measure_finite_Union[OF _ _ Ci_d,symmetric]) (use Ci in auto)
                finally show "y ≤ measure M (⋃ (Ci ` {..<N}))" .
              qed(insert Ci,auto intro!: closedin_Union)
            qed
          qed
        qed auto
      next
        show "?Inf (⋃i. a i) ≤ measure M (⋃i. a i)"
        proof(rule cInf_le_iff_less[THEN iffD2])
          show "∀y> measure M (⋃ (range a)). ∃C∈{C. openin X C ∧ ⋃ (range a) ⊆ C}. measure M C ≤ y"
          proof safe
            fix y
            assume 1:"measure M (⋃i. a i) < y"
            define en where "en ≡ (λn. (y - measure M (⋃i. a i)) * (1 / 2) ^ (Suc n))"
            with 1 have [arith]:"en n > 0" for n by auto
            hence "measure M (a i) < measure M (a i) + en i" for i by auto
            hence "∃Ui. openin X Ui ∧ a i ⊆ Ui ∧ measure M Ui ≤ measure M (a i) + en i" for i
              using ih[of i,simplified cInf_le_iff_less[OF ne(2)[OF ‹a i ∈ sets M›] bdd(4)]] by auto
            then obtain Ui where Ui: "⋀i. openin X (Ui i)" "⋀i. a i ⊆ Ui i"
              "⋀i. measure M (Ui i) ≤ measure M (a i) + en i"
              by metis
            have [simp]: "summable en" "summable (λn. measure M (a n))"
              by(auto simp: en_def intro!: summable_measure h)
            hence [simp]: "summable (λn. measure M (a n) + en n)"
              by(auto intro!: summable_add)
            have [simp]:"summable (λn. measure M (Ui n))"
              using Ui by(auto intro!: summable_comparison_test_ev[OF _ ‹summable (λn. measure M (a n) + en n)›])
            show "∃C∈{C. openin X C ∧ ⋃ (range a) ⊆ C}. measure M C ≤ y"
            proof(safe intro!: bexI[where x="⋃i. Ui i"])
              have "measure M (⋃i. Ui i) ≤ (∑i. measure M (Ui i))"
                using Ui by(auto intro!: finite_measure_subadditive_countably)
              also have "... ≤ (∑i. measure M (a i) + en i)"
                by(auto intro!: suminf_le Ui)
              also have "... = (∑i. measure M (a i)) + (∑i. en i)"
                by(simp add: suminf_add)
              also have "... = measure M (⋃i. a i) + (y - measure M (⋃i. a i))"
              proof -
                have [simp]:"(∑i. measure M (a i)) = measure M (⋃i. a i)"
                  by(auto intro!: suminf_measure h)
                have "(∑i. en i) = (y - Sigma_Algebra.measure M (⋃ (range a))) / 2 * (∑n. (1 / 2) ^ n)"
                  by(simp only: suminf_mult[of "λn. (1 / 2) ^ n :: real",simplified,symmetric]) (simp add: en_def)
                also have "... = (y - measure M (⋃i. a i))"
                  by(simp add: suminf_geometric)
                finally show ?thesis by simp
              qed
              finally show "measure M (⋃i. Ui i) ≤ y" by simp
            qed(use Ui in auto)
          qed
          show "{C. openin X C ∧ ⋃ (range a) ⊆ C} ≠ {}"
            using sets.sets_into_space[OF a]
            by(force intro!: exI[where x="topspace X"] simp: sets_eq_imp_space_eq[OF assms(2),simplified space_borel_of])
        qed auto
      qed
    qed
    note 1 this
  }
  with assms(2) show "inner_regular X M" "outer_regular X M"
    by (fastforce intro!: inner_regularI outer_regularI)+
qed

definition tight_on_set :: "'a topology ⇒ 'a measure set ⇒ bool" where
"tight_on_set X Γ ⟷ (∀M∈Γ. finite_measure M ∧ sets (borel_of X) = sets M) ∧
                      (∀e>0. ∃K. compactin X K ∧ (∀M∈Γ. measure M (space M - K) < e))"

abbreviation tight_on :: "'a topology ⇒ 'a measure ⇒ bool" where
"tight_on X M ≡ tight_on_set X {M}"

lemma tight_on_def:
"tight_on X M ⟷ finite_measure M ∧ sets (borel_of X) = sets M ∧
                  (∀e>0. ∃K. compactin X K ∧ measure M (space M - K) < e)"
  by(auto simp: tight_on_set_def)

lemma tight_on_set_subset: "A ⊆ B ⟹ tight_on_set X B ⟹ tight_on_set X A"
  unfolding tight_on_set_def by blast

lemma tight_on_tight: "tight_on_set euclidean (Mi ` UNIV) ∧ (∀i. real_distribution (Mi i)) ⟷ tight Mi"
proof safe
  assume h:"tight_on_set euclideanreal (range Mi)" "∀i. real_distribution (Mi i)"
  show "tight Mi"
    unfolding tight_def
  proof safe
    fix e :: real
    assume e: "e > 0"
    with h(1) obtain K where K:
     "compact K" "⋀i. measure (Mi i) (space (Mi i) - K) < e"
      by(auto simp: tight_on_set_def)
    obtain r where r:
      "r > 0" "K ⊆ ball 0 r"
      by(metis bounded_subset_ballD[OF compact_imp_bounded[OF K(1)]])
    show "∃a b. a < b ∧ (∀n. 1 - e < measure (Mi n) {a<..b})"
    proof(rule exI[where x="-r"])
      show "∃b>- r. ∀n. 1 - e < measure (Mi n) {- r<..b}"
      proof(safe intro!: exI[where x=r])
        fix n
        interpret real_distribution "Mi n"
          using h by simp
        have [measurable]: "K ∈ sets (Mi n)"
          by (simp add: K(1) borel_compact)
        hence "1 - e < prob K"
          using K(2)[of n] by(simp add: prob_compl del: borel_UNIV)
        also have "... ≤ prob {- r<..<r}"
          using r by(auto intro!: finite_measure_mono simp: ball_eq_greaterThanLessThan)
        also have "... ≤ prob {-r<..r}"
          by(auto intro!: finite_measure_mono)
        finally show "1 - e < prob {-r<..r}" .
      qed(use r in auto)
    qed
  qed(use h in simp)
next
  assume h:"tight Mi"
  show "tight_on_set euclideanreal (range Mi)"
    unfolding tight_on_set_def
  proof safe
    fix e :: real
    assume e: "e > 0"
    with h obtain a b where ab: "a < b" "⋀n. measure (Mi n) {a<..b} > 1 - e"
      by(auto simp: tight_def)
    show "∃K. compactin euclideanreal K ∧ (∀M∈range Mi. measure M (space M - K) < e)"
    proof(safe intro!: exI[where x="{a..b}"])
      fix n
      interpret real_distribution "Mi n"
        using h by(auto simp: tight_def)
      have "prob (space (Mi n) - {a..b}) = 1 - prob {a..b}"
        by(rule prob_compl) simp
      also have "... ≤ 1 - prob {a<..b}"
        by(auto intro!: finite_measure_mono)
      also have "... < e"
        using ab(2)[of n] by auto
      finally show "prob (space (Mi n) - {a..b}) < e" .
    qed simp
  qed(insert h,auto simp: borel_of_euclidean tight_def real_distribution_def real_distribution_axioms_def prob_space_def)
qed(auto simp: tight_def)

lemma inner_regular'':
  assumes "metrizable_space X" "tight_on X M"
      and [measurable]:"A ∈ sets M"
    shows "measure M A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. measure M K)" (is "_ = ?rhs")
proof -
  have sets: "sets (borel_of X) = sets M"
    using assms(2) by(simp add: tight_on_def)
  interpret M: finite_measure M
    using assms(2) by(simp add: tight_on_def)
  have "measure M A ≥ ?rhs"
    using sets.sets_into_space[OF assms(3)]
    by(auto intro!: cSup_le_iff[THEN iffD2] M.finite_measure_mono bdd_aboveI[where M="measure M (space M)"])
  moreover have "measure M A ≤ ?rhs"
  proof -
    have "measure M A - e < ?rhs" if e[arith]: "e > 0" for e
    proof -
      obtain K where K: "compactin X K" "measure M (space M - K) < e"
        using assms(2)[simplified tight_on_def] e by metis
      hence [measurable]: "K ∈ sets M"
        by(auto simp: sets[symmetric]
            intro!: borel_of_closed compactin_imp_closedin[OF metrizable_imp_Hausdorff_space[OF assms(1)]])
      have "measure M A - e < measure M A - measure M (space M - K)"
        using K by auto
      also have "... ≤ measure M (A ∩ K)"
        by (metis Diff_mono M.finite_measure_Diff' M.finite_measure_mono ‹K ∈ sets M› assms(3) cancel_ab_semigroup_add_class.diff_right_commute dual_order.refl le_iff_diff_le_0 sets.Diff sets.sets_into_space sets.top)
      also have "... = (⨆C∈{C. closedin X C ∧ C ⊆ A ∩ K}. measure M C)"
        by(rule M.inner_regularD[OF M.inner_regular'[OF assms(1) sets]]) measurable
      also have "... ≤ ?rhs"
      proof(rule cSup_mono)
        show "⋀b. b ∈ Sigma_Algebra.measure M ` {C. closedin X C ∧ C ⊆ A ∩ K}
               ⟹ ∃a∈Sigma_Algebra.measure M ` {K. compactin X K ∧ K ⊆ A}. b ≤ a"
        proof safe
          fix C
          assume "closedin X C" "C ⊆ A ∩ K"
          then show "∃a∈Sigma_Algebra.measure M ` {K. compactin X K ∧ K ⊆ A}. measure M C ≤ a"
            by(auto intro!: closed_compactin[OF K(1)])
        qed
      qed(auto intro!: bdd_aboveI[where M="measure M (space M)"] M.bounded_measure)
      finally show ?thesis .
    qed
    thus ?thesis
      by (metis (full_types) cancel_ab_semigroup_add_class.diff_right_commute dual_order.refl le_iff_diff_le_0 less_iff_diff_less_0 linorder_not_less)
  qed
  ultimately show ?thesis by simp
qed

lemma(in finite_measure) tight_on_compact_space:
  assumes "metrizable_space X" "compact_space X" "sets (borel_of X) = sets M"
  shows "tight_on X M"
  using assms(1,2)
  by(auto simp: tight_on_def assms finite_measure_axioms sets_eq_imp_space_eq[OF assms(3)[symmetric]]
                compact_space_def space_borel_of
      intro!: exI[where x="space M"])

lemma(in finite_measure) tight_on_finite_space:
  assumes "metrizable_space X" "sets (borel_of X) = sets M" "finite (space M)"
  shows "tight_on X M"
proof -
  from assms(3) have "compact_space X"
    by(auto simp: assms compact_space_def sets_eq_imp_space_eq[OF assms(2)[symmetric]] space_borel_of
          intro!: finite_imp_compactin_eq[THEN iffD2])
  from tight_on_compact_space[OF assms(1) this assms(2)] show ?thesis .
qed

lemma(in finite_measure) tight_on_Polish:
  assumes "Polish_space X" "sets (borel_of X) = sets M"
  shows "tight_on X M"
proof(cases "finite (space M)")
  case True
  then show ?thesis
    by(auto intro!: tight_on_finite_space assms Polish_space_imp_metrizable_space)
next
  case inf:False
  then have inf2: "infinite (topspace X)"
    by(auto simp: sets_eq_imp_space_eq[OF assms(2)[symmetric]] space_borel_of)
  obtain d where d:"Metric_space (topspace X) d" "Metric_space.mtopology (topspace X) d = X"
    "Metric_space.mcomplete (topspace X) d"
    by (metis Metric_space.topspace_mtopology assms(1) completely_metrizable_space_def Polish_space_imp_completely_metrizable_space)
  interpret d: Metric_space "topspace X" d by fact
  have [measurable]:"⋀a e. d.mball a e ∈ sets M" "⋀a e. d.mcball a e ∈ sets M"
    using d.openin_mball d.closedin_mcball by(auto simp: assms(2)[symmetric] borel_of_open borel_of_closed d)
  show ?thesis
    unfolding tight_on_def
  proof safe
    fix e :: real
    assume e: "e > 0"
    from assms obtain U where U: "countable U" "dense_in X U"
      by(auto simp: separable_space_def2 Polish_space_def)
    have U_ne: "U ≠ {}"
      by (metis U(2) dense_in_nonempty inf2 infinite_imp_nonempty)
    let ?an = "from_nat_into U"
    have an:"⋀n. ?an n ∈ U"
      by (simp add: U_ne from_nat_into)
    have anU: "(⋃n. d.mball (?an n) e') = topspace X" if "e' > 0" for e'
    proof -
      have "(⋃n. d.mball (?an n) e') = (⋃u∈U. d.mball u e')"
        by(auto simp: UN_from_nat_into[OF U(1) U_ne])
      also have "... = topspace X"
        by(rule d.mdense_balls_cover[simplified d,OF U(2) that])
      finally show ?thesis .
    qed
    have "∃n. measure M (⋃i∈{..<n}. d.mball (?an i) (1 / Suc m)) > measure M (space M) - e * (1 / 2)^Suc m" for m
    proof -
      have 1:"(λn. measure M (⋃i∈{..<n}. d.mball (?an i) (1 / Suc m)))
               ⇢ measure M (⋃n. ⋃i∈{..<n}. d.mball (?an i) (1 / Suc m))"
        by(rule finite_Lim_measure_incseq) (fastforce simp: incseq_def)+
      have "(⋃n. ⋃i∈{..<n}. d.mball (?an i) (1 / Suc m)) = (⋃n. d.mball (?an n) (1 / Suc m))" by blast
      also have "... = topspace X"
        by(rule anU) auto
      also have "... = space M"
        by(simp add: sets_eq_imp_space_eq[OF assms(2),simplified space_borel_of])
      finally have "(λn. measure M (⋃i∈{..<n}. d.mball (?an i) (1 / Suc m))) ⇢ measure M (space M)"
        using 1 by simp
      moreover have "e * (1 / 2)^Suc m > 0" using e by auto
      ultimately have "∃N. ∀n≥N. ¦measure M (⋃i∈{..<n}. d.mball (?an i) (1 / Suc m)) - measure M (space M)¦ < e * (1/2)^Suc m"
        unfolding LIMSEQ_def dist_real_def by metis
      then obtain N where "measure M (space M) - measure M (⋃i∈{..<N}. d.mball (?an i) (1 / Suc m)) < e * (1/2)^Suc m"
        using bounded_measure by auto
      thus ?thesis
        by(auto intro!: exI[where x=N])
    qed
    then obtain n where n: "⋀m. measure M (⋃i∈{..<n m}. d.mball (?an i) (1 / Suc m)) > measure M (space M) - e * (1 / 2)^Suc m"
      by metis
    have n': "⋀m. measure M (⋃i∈{..<n m}. d.mcball (?an i) (1 / Suc m)) > measure M (space M) - e * (1 / 2)^Suc m"
      by(rule order.strict_trans2[OF n]) (auto intro!: finite_measure_mono)
    define K where "K ≡ ⋂m. ⋃k∈{..<n m}. d.mcball (?an k) (1 / Suc m)"
    have K_closed: "closedin d.mtopology K"
      by(auto intro!: closedin_Union simp: K_def)
    have K_compact: "compactin d.mtopology K"
    proof -
      have "d.mtotally_bounded K"
        unfolding d.mtotally_bounded_def2
      proof safe
        fix e' :: real
        assume [arith]:"e' > 0"
        then obtain m where m[arith]: "1 / Suc m < e'"
          using nat_approx_posE by blast
        have "K ⊆ (⋃k∈{..<n m}. d.mcball (?an k) (1 / Suc m))"
          by(auto simp: K_def)
        also have "... ⊆ (⋃k∈{..<n m}. d.mball (?an k) e')"
          using m by auto
        finally show "∃Ka. finite Ka ∧ Ka ⊆ topspace X ∧ K ⊆ (⋃x∈Ka. d.mball x e')"
          using an dense_in_subset[OF U(2)] by(fastforce intro!: exI[where x="?an ` {..<n m}"])
      qed
      thus ?thesis
        by(simp add: d.mtotally_bounded_eq_compact_closedin[OF d(3) K_closed,simplified])
    qed
    show "∃K. compactin X K ∧ measure M (space M - K) < e"
    proof(safe intro!: exI[where x=K])
      have sum:"summable (λm. measure M (space M - (⋃k∈{..<n m}. d.mcball (?an k) (1 / Suc m))))"
        apply(intro summable_comparison_test_ev[OF _  summable_mult[OF complete_algebra_summable_geometric[where x="1 / 2"]],of _ e] exI[where x=1])
         apply(simp add: eventually_sequentially finite_measure_compl)
         apply(intro exI[where x=1] allI)
        subgoal for l
          using n'[of l] e bounded_measure
          apply(auto intro!: order.strict_implies_order[OF order.strict_trans[where b="e* (1 / 2)^Suc l"]])
          done
        by simp
      have "measure M (space M - K) = measure M (⋃m. (space M - (⋃k∈{..<n m}. d.mcball (?an k) (1 / Suc m))))"
        by(auto simp: K_def)
      also have "... ≤ (∑m. measure M (space M - (⋃k∈{..<n m}. d.mcball (?an k) (1 / Suc m))))"
        by(rule finite_measure_subadditive_countably) (use sum in auto)
      also have "... = measure M (space M - (⋃k∈{..<n 0}. d.mcball (?an k) (1 / Suc 0)))
              + (∑m. measure M (space M - (⋃k∈{..<n (Suc m)}. d.mcball (?an k) (1 / Suc (Suc m)))))"
        using suminf_split_initial_segment[OF sum,of 1] by simp
      also have "... < e * (1 / 2)
              + (∑m. measure M (space M - (⋃k∈{..<n (Suc m)}. d.mcball (?an k) (1 / Suc (Suc m)))))"
        using n'[of 0] by(simp add: finite_measure_compl)
      also have "... ≤  e * (1 / 2) + (∑m. e * (1 / 2) ^ (Suc (Suc m)))"
      proof -
        have "(∑m. measure M (space M - (⋃k∈{..<n (Suc m)}. d.mcball (?an k) (1 / Suc (Suc m))))) ≤ (∑m. e * (1 / 2) ^ (Suc (Suc m)))"
        proof(rule suminf_le)
          fix l
          show "measure M (space M - (⋃k<n (Suc l). d.mcball (?an k) (1 / real (Suc (Suc l))))) ≤ e * (1 / 2) ^ Suc (Suc l)"
            using n'[of "Suc l"] by (auto simp: finite_measure_compl)
        qed(use summable_Suc_iff[THEN iffD2,OF sum] in auto)
        thus ?thesis by simp
      qed
      also have "... = e"
        by(simp add: suminf_geometric[of "1 / 2 :: real"] suminf_mult suminf_divide)
      finally show "measure M (space M - K) < e" .
    qed(use K_compact d in auto)
  qed(use finite_measure_axioms assms in auto)
qed

corollary(in finite_measure) inner_regular_Polish:
  assumes "Polish_space X" "sets (borel_of X) = sets M" "A ∈ sets M"
  shows "measure M A = (⨆K∈{K. compactin X K ∧ K ⊆ A}. measure M K)"
  by(auto intro!: tight_on_Polish inner_regular'' simp: assms Polish_space_imp_metrizable_space)

end