Theory HOL-Analysis.Regularity

(*  Title:      HOL/Analysis/Regularity.thy
    Author:     Fabian Immler, TU München
*)

section ‹Regularity of Measures›

theory Regularity (* FIX suggestion to rename  e.g. RegularityMeasures and/ or move as
this theory consists of 1 result only  *)
imports Measure_Space Borel_Space
begin

theorem
  fixes M::"'a::{second_countable_topology, complete_space} measure"
  assumes sb: "sets M = sets borel"
  assumes "emeasure M (space M)  "
  assumes "B  sets borel"
  shows inner_regular: "emeasure M B =
    (SUP K  {K. K  B  compact K}. emeasure M K)" (is "?inner B")
  and outer_regular: "emeasure M B =
    (INF U  {U. B  U  open U}. emeasure M U)" (is "?outer B")
proof -
  have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)
  hence sU: "space M = UNIV" by simp
  interpret finite_measure M by rule fact
  have approx_inner: "A. A  sets M 
    (e. e > 0  K. K  A  compact K  emeasure M A  emeasure M K + ennreal e)  ?inner A"
    by (rule ennreal_approx_SUP)
      (force intro!: emeasure_mono simp: compact_imp_closed emeasure_eq_measure)+
  have approx_outer: "A. A  sets M 
    (e. e > 0  B. A  B  open B  emeasure M B  emeasure M A + ennreal e)  ?outer A"
    by (rule ennreal_approx_INF)
       (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
  from countable_dense_setE obtain X :: "'a set"
    where X: "countable X" "Y :: 'a set. open Y  Y  {}  dX. d  Y"
    by auto
  {
    fix r::real assume "r > 0" hence "y. open (ball y r)" "y. ball y r  {}" by auto
    with X(2)[OF this]
    have x: "space M = (xX. cball x r)"
      by (auto simp add: sU) (metis dist_commute order_less_imp_le)
    let ?U = "k. (n{0..k}. cball (from_nat_into X n) r)"
    have "(λk. emeasure M (n{0..k}. cball (from_nat_into X n) r))  M ?U"
      by (rule Lim_emeasure_incseq) (auto intro!: borel_closed bexI simp: incseq_def Us sb)
    also have "?U = space M"
    proof safe
      fix x from X(2)[OF open_ball[of x r]] r > 0 obtain d where d: "dX" "d  ball x r" by auto
      show "x  ?U"
        using X(1) d
        by simp (auto intro!: exI [where x = "to_nat_on X d"] simp: dist_commute Bex_def)
    qed (simp add: sU)
    finally have "(λk. M (n{0..k}. cball (from_nat_into X n) r))  M (space M)" .
  } note M_space = this
  {
    fix e ::real and n :: nat assume "e > 0" "n > 0"
    hence "1/n > 0" "e * 2 powr - n > 0" by (auto)
    from M_space[OF 1/n>0]
    have "(λk. measure M (i{0..k}. cball (from_nat_into X i) (1/real n)))  measure M (space M)"
      unfolding emeasure_eq_measure by (auto)
    from metric_LIMSEQ_D[OF this 0 < e * 2 powr -n]
    obtain k where "dist (measure M (i{0..k}. cball (from_nat_into X i) (1/real n))) (measure M (space M)) <
      e * 2 powr -n"
      by auto
    hence "measure M (i{0..k}. cball (from_nat_into X i) (1/real n)) 
      measure M (space M) - e * 2 powr -real n"
      by (auto simp: dist_real_def)
    hence "k. measure M (i{0..k}. cball (from_nat_into X i) (1/real n)) 
      measure M (space M) - e * 2 powr - real n" ..
  } note k=this
  hence "e{0<..}. (n::nat){0<..}. k.
    measure M (i{0..k}. cball (from_nat_into X i) (1/real n))  measure M (space M) - e * 2 powr - real n"
    by blast
  then obtain k where k: "e{0<..}. n{0<..}. measure M (space M) - e * 2 powr - real (n::nat)
     measure M (i{0..k e n}. cball (from_nat_into X i) (1 / n))"
    by metis
  hence k: "e n. e > 0  n > 0  measure M (space M) - e * 2 powr - n
     measure M (i{0..k e n}. cball (from_nat_into X i) (1 / n))"
    unfolding Ball_def by blast
  have approx_space:
    "K  {K. K  space M  compact K}. emeasure M (space M)  emeasure M K + ennreal e"
    (is "?thesis e") if "0 < e" for e :: real
  proof -
    define B where [abs_def]:
      "B n = (i{0..k e (Suc n)}. cball (from_nat_into X i) (1 / Suc n))" for n
    have "n. closed (B n)" by (auto simp: B_def)
    hence [simp]: "n. B n  sets M" by (simp add: sb)
    from k[OF e > 0 zero_less_Suc]
    have "n. measure M (space M) - measure M (B n)  e * 2 powr - real (Suc n)"
      by (simp add: algebra_simps B_def finite_measure_compl)
    hence B_compl_le: "n::nat. measure M (space M - B n)  e * 2 powr - real (Suc n)"
      by (simp add: finite_measure_compl)
    define K where "K = (n. B n)"
    from closed (B _) have "closed K" by (auto simp: K_def)
    hence [simp]: "K  sets M" by (simp add: sb)
    have "measure M (space M) - measure M K = measure M (space M - K)"
      by (simp add: finite_measure_compl)
    also have " = emeasure M (n. space M - B n)" by (auto simp: K_def emeasure_eq_measure)
    also have "  (n. emeasure M (space M - B n))"
      by (rule emeasure_subadditive_countably) (auto simp: summable_def)
    also have "  (n. ennreal (e*2 powr - real (Suc n)))"
      using B_compl_le by (intro suminf_le) (simp_all add: emeasure_eq_measure ennreal_leI)
    also have "  (n. ennreal (e * (1 / 2) ^ Suc n))"
      by (simp add: powr_minus powr_realpow field_simps del: of_nat_Suc)
    also have " = ennreal e * (n. ennreal ((1 / 2) ^ Suc n))"
      unfolding ennreal_power[symmetric]
      using 0 < e
      by (simp add: ac_simps ennreal_mult' divide_ennreal[symmetric] divide_ennreal_def
                    ennreal_power[symmetric])
    also have " = e"
      by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto
    finally have "measure M (space M)  measure M K + e"
      using 0 < e by simp
    hence "emeasure M (space M)  emeasure M K + e"
      using 0 < e by (simp add: emeasure_eq_measure flip: ennreal_plus)
    moreover have "compact K"
      unfolding compact_eq_totally_bounded
    proof safe
      show "complete K" using closed K by (simp add: complete_eq_closed)
      fix e'::real assume "0 < e'"
      then obtain n where n: "1 / real (Suc n) < e'" by (rule nat_approx_posE)
      let ?k = "from_nat_into X ` {0..k e (Suc n)}"
      have "finite ?k" by simp
      moreover have "K  (x?k. ball x e')" unfolding K_def B_def using n by force
      ultimately show "k. finite k  K  (xk. ball x e')" by blast
    qed
    ultimately
    show ?thesis by (auto simp: sU)
  qed
  { fix A::"'a set" assume "closed A" hence "A  sets borel" by (simp add: compact_imp_closed)
    hence [simp]: "A  sets M" by (simp add: sb)
    have "?inner A"
    proof (rule approx_inner)
      fix e::real assume "e > 0"
      from approx_space[OF this] obtain K where
        K: "K  space M" "compact K" "emeasure M (space M)  emeasure M K + e"
        by (auto simp: emeasure_eq_measure)
      hence [simp]: "K  sets M" by (simp add: sb compact_imp_closed)
      have "measure M A - measure M (A  K) = measure M (A - A  K)"
        by (subst finite_measure_Diff) auto
      also have "A - A  K = A  K - K" by auto
      also have "measure M  = measure M (A  K) - measure M K"
        by (subst finite_measure_Diff) auto
      also have "  measure M (space M) - measure M K"
        by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
      also have "  e"
        using K 0 < e by (simp add: emeasure_eq_measure flip: ennreal_plus)
      finally have "emeasure M A  emeasure M (A  K) + ennreal e"
        using 0<e by (simp add: emeasure_eq_measure algebra_simps flip: ennreal_plus)
      moreover have "A  K  A" "compact (A  K)" using closed A compact K by auto
      ultimately show "K  A. compact K  emeasure M A  emeasure M K + ennreal e"
        by blast
    qed simp
    have "?outer A"
    proof cases
      assume "A  {}"
      let ?G = "λd. {x. infdist x A < d}"
      {
        fix d
        have "?G d = (λx. infdist x A) -` {..<d}" by auto
        also have "open "
          by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_ident)
        finally have "open (?G d)" .
      } note open_G = this
      from in_closed_iff_infdist_zero[OF closed A A  {}]
      have "A = {x. infdist x A = 0}" by auto
      also have " = (i. ?G (1/real (Suc i)))"
      proof (auto simp del: of_nat_Suc, rule ccontr)
        fix x
        assume "infdist x A  0"
        then have pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
        then obtain n where n: "1 / real (Suc n) < infdist x A" by (rule nat_approx_posE)
        assume "i. infdist x A < 1 / real (Suc i)"
        then have "infdist x A < 1 / real (Suc n)" by auto
        with n show False by simp
      qed
      also have "M  = (INF n. emeasure M (?G (1 / real (Suc n))))"
      proof (rule INF_emeasure_decseq[symmetric], safe)
        fix i::nat
        from open_G[of "1 / real (Suc i)"]
        show "?G (1 / real (Suc i))  sets M" by (simp add: sb borel_open)
      next
        show "decseq (λi. {x. infdist x A < 1 / real (Suc i)})"
          by (auto intro: less_trans intro!: divide_strict_left_mono
            simp: decseq_def le_eq_less_or_eq)
      qed simp
      finally
      have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" .
      moreover
      have "  (INF U{U. A  U  open U}. emeasure M U)"
      proof (intro INF_mono)
        fix m
        have "?G (1 / real (Suc m))  {U. A  U  open U}" using open_G by auto
        moreover have "M (?G (1 / real (Suc m)))  M (?G (1 / real (Suc m)))" by simp
        ultimately show "U{U. A  U  open U}.
          emeasure M U  emeasure M {x. infdist x A < 1 / real (Suc m)}"
          by blast
      qed
      moreover
      have "emeasure M A  (INF U{U. A  U  open U}. emeasure M U)"
        by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
      ultimately show ?thesis by simp
    qed (auto intro!: INF_eqI)
    note ?inner A ?outer A }
  note closed_in_D = this
  from B  sets borel
  have "Int_stable (Collect closed)" "Collect closed  Pow UNIV" "B  sigma_sets UNIV (Collect closed)"
    by (auto simp: Int_stable_def borel_eq_closed)
  then show "?inner B" "?outer B"
  proof (induct B rule: sigma_sets_induct_disjoint)
    case empty
    { case 1 show ?case by (intro SUP_eqI[symmetric]) auto }
    { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
  next
    case (basic B)
    { case 1 from basic closed_in_D show ?case by auto }
    { case 2 from basic closed_in_D show ?case by auto }
  next
    case (compl B)
    note inner = compl(2) and outer = compl(3)
    from compl have [simp]: "B  sets M" by (auto simp: sb borel_eq_closed)
    case 2
    have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
    also have " = (INF K{K. K  B  compact K}. M (space M) -  M K)"
      by (subst ennreal_SUP_const_minus) (auto simp: less_top[symmetric] inner)
    also have " = (INF U{U. U  B  compact U}. M (space M - U))"
      by (auto simp add: emeasure_compl sb compact_imp_closed)
    also have "  (INF U{U. U  B  closed U}. M (space M - U))"
      by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
    also have "(INF U{U. U  B  closed U}. M (space M - U)) =
        (INF U{U. space M - B  U  open U}. emeasure M U)"
      apply (rule arg_cong [of _ _ Inf])
      using sU
      apply (auto simp add: image_iff)
      apply (rule exI [of _ "UNIV - y" for y])
      apply safe
        apply (auto simp add: double_diff)
      done
    finally have
      "(INF U{U. space M - B  U  open U}. emeasure M U)  emeasure M (space M - B)" .
    moreover have
      "(INF U{U. space M - B  U  open U}. emeasure M U)  emeasure M (space M - B)"
      by (auto simp: sb sU intro!: INF_greatest emeasure_mono)
    ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])

    case 1
    have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
    also have " = (SUP U {U. B  U  open U}. M (space M) -  M U)"
      unfolding outer by (subst ennreal_INF_const_minus) auto
    also have " = (SUP U{U. B  U  open U}. M (space M - U))"
      by (auto simp add: emeasure_compl sb compact_imp_closed)
    also have " = (SUP K{K. K  space M - B  closed K}. emeasure M K)"
      unfolding SUP_image [of _ "λu. space M - u" _, symmetric, unfolded comp_def]
      apply (rule arg_cong [of _ _ Sup])
      using sU apply (auto intro!: imageI)
      done
    also have " = (SUP K{K. K  space M - B  compact K}. emeasure M K)"
    proof (safe intro!: antisym SUP_least)
      fix K assume "closed K" "K  space M - B"
      from closed_in_D[OF closed K]
      have K_inner: "emeasure M K = (SUP K{Ka. Ka  K  compact Ka}. emeasure M K)" by simp
      show "emeasure M K  (SUP K{K. K  space M - B  compact K}. emeasure M K)"
        unfolding K_inner using K  space M - B
        by (auto intro!: SUP_upper SUP_least)
    qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
    finally show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])
  next
    case (union D)
    then have "range D  sets M" by (auto simp: sb borel_eq_closed)
    with union have M[symmetric]: "(i. M (D i)) = M (i. D i)" by (intro suminf_emeasure)
    also have "(λn. i<n. M (D i))  (i. M (D i))"
      by (intro summable_LIMSEQ) auto
    finally have measure_LIMSEQ: "(λn. i<n. measure M (D i))  measure M (i. D i)"
      by (simp add: emeasure_eq_measure sum_nonneg)
    have "(i. D i)  sets M" using range D  sets M by auto

    case 1
    show ?case
    proof (rule approx_inner)
      fix e::real assume "e > 0"
      with measure_LIMSEQ
      have "no. nno. ¦(i<n. measure M (D i)) -measure M (x. D x)¦ < e/2"
        by (auto simp: lim_sequentially dist_real_def simp del: less_divide_eq_numeral1)
      hence "n0. ¦(i<n0. measure M (D i)) - measure M (x. D x)¦ < e/2" by auto
      then obtain n0 where n0: "¦(i<n0. measure M (D i)) - measure M (i. D i)¦ < e/2"
        unfolding choice_iff by blast
      have "ennreal (i<n0. measure M (D i)) = (i<n0. M (D i))"
        by (auto simp add: emeasure_eq_measure)
      also have "  (i. M (D i))" by (rule sum_le_suminf) auto
      also have " = M (i. D i)" by (simp add: M)
      also have " = measure M (i. D i)" by (simp add: emeasure_eq_measure)
      finally have n0: "measure M (i. D i) - (i<n0. measure M (D i)) < e/2"
        using n0 by (auto simp: sum_nonneg)
      have "i. K. K  D i  compact K  emeasure M (D i)  emeasure M K + e/(2*Suc n0)"
      proof
        fix i
        from 0 < e have "0 < e/(2*Suc n0)" by simp
        have "emeasure M (D i) = (SUP K{K. K  (D i)  compact K}. emeasure M K)"
          using union by blast
        from SUP_approx_ennreal[OF 0 < e/(2*Suc n0) _ this]
        show "K. K  D i  compact K  emeasure M (D i)  emeasure M K + e/(2*Suc n0)"
          by (auto simp: emeasure_eq_measure intro: less_imp_le compact_empty)
      qed
      then obtain K where K: "i. K i  D i" "i. compact (K i)"
        "i. emeasure M (D i)  emeasure M (K i) + e/(2*Suc n0)"
        unfolding choice_iff by blast
      let ?K = "i{..<n0}. K i"
      have "disjoint_family_on K {..<n0}" using K disjoint_family D
        unfolding disjoint_family_on_def by blast
      hence mK: "measure M ?K = (i<n0. measure M (K i))" using K
        by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed)
      have "measure M (i. D i) < (i<n0. measure M (D i)) + e/2" using n0 by simp
      also have "(i<n0. measure M (D i))  (i<n0. measure M (K i) + e/(2*Suc n0))"
        using K 0 < e
        by (auto intro: sum_mono simp: emeasure_eq_measure simp flip: ennreal_plus)
      also have " = (i<n0. measure M (K i)) + (i<n0. e/(2*Suc n0))"
        by (simp add: sum.distrib)
      also have "  (i<n0. measure M (K i)) +  e / 2" using 0 < e
        by (auto simp: field_simps intro!: mult_left_mono)
      finally
      have "measure M (i. D i) < (i<n0. measure M (K i)) + e / 2 + e / 2"
        by auto
      hence "M (i. D i) < M ?K + e"
        using 0<e by (auto simp: mK emeasure_eq_measure sum_nonneg ennreal_less_iff simp flip: ennreal_plus)
      moreover
      have "?K  (i. D i)" using K by auto
      moreover
      have "compact ?K" using K by auto
      ultimately
      have "?K(i. D i)  compact ?K  emeasure M (i. D i)  emeasure M ?K + ennreal e" by simp
      thus "Ki. D i. compact K  emeasure M (i. D i)  emeasure M K + ennreal e" ..
    qed fact
    case 2
    show ?case
    proof (rule approx_outer[OF (i. D i)  sets M])
      fix e::real assume "e > 0"
      have "i::nat. U. D i  U  open U  e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
      proof
        fix i::nat
        from 0 < e have "0 < e/(2 powr Suc i)" by simp
        have "emeasure M (D i) = (INF U{U. (D i)  U  open U}. emeasure M U)"
          using union by blast
        from INF_approx_ennreal[OF 0 < e/(2 powr Suc i) this]
        show "U. D i  U  open U  e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
          using 0<e
          by (auto simp: emeasure_eq_measure sum_nonneg ennreal_less_iff ennreal_minus
                         finite_measure_mono sb
                   simp flip: ennreal_plus)
      qed
      then obtain U where U: "i. D i  U i" "i. open (U i)"
        "i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)"
        unfolding choice_iff by blast
      let ?U = "i. U i"
      have "ennreal (measure M ?U - measure M (i. D i)) = M ?U - M (i. D i)"
        using U(1,2)
        by (subst ennreal_minus[symmetric])
           (auto intro!: finite_measure_mono simp: sb emeasure_eq_measure)
      also have " = M (?U - (i. D i))" using U  (i. D i)  sets M
        by (subst emeasure_Diff) (auto simp: sb)
      also have "  M (i. U i - D i)" using U  range D  sets M
        by (intro emeasure_mono) (auto simp: sb intro!: sets.countable_nat_UN sets.Diff)
      also have "  (i. M (U i - D i))" using U  range D  sets M
        by (intro emeasure_subadditive_countably) (auto intro!: sets.Diff simp: sb)
      also have "  (i. ennreal e/(2 powr Suc i))" using U range D  sets M
        using 0<e
        by (intro suminf_le, subst emeasure_Diff)
           (auto simp: emeasure_Diff emeasure_eq_measure sb ennreal_minus
                       finite_measure_mono divide_ennreal ennreal_less_iff
                 intro: less_imp_le)
      also have "  (n. ennreal (e * (1 / 2) ^ Suc n))"
        using 0<e
        by (simp add: powr_minus powr_realpow field_simps divide_ennreal del: of_nat_Suc)
      also have " = ennreal e * (n. ennreal ((1 / 2) ^  Suc n))"
        unfolding ennreal_power[symmetric]
        using 0 < e
        by (simp add: ac_simps ennreal_mult' divide_ennreal[symmetric] divide_ennreal_def
                      ennreal_power[symmetric])
      also have " = ennreal e"
        by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto
      finally have "emeasure M ?U  emeasure M (i. D i) + ennreal e"
        using 0<e by (simp add: emeasure_eq_measure flip: ennreal_plus)
      moreover
      have "(i. D i)  ?U" using U by auto
      moreover
      have "open ?U" using U by auto
      ultimately
      have "(i. D i)  ?U  open ?U  emeasure M ?U  emeasure M (i. D i) + ennreal e" by simp
      thus "B. (i. D i)  B  open B  emeasure M B  emeasure M (i. D i) + ennreal e" ..
    qed
  qed
qed

end