Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/sources/formale Sprachen/Isabelle/HOL/Analysis/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 92 kB image not shown  

Impressum Equivalence_Measurable_On_Borel.thy   Sprache: Isabelle

 
(*  Title:      HOL/Analysis/Equivalence_Measurable_On_Borel
    Author: LC Paulson (some material ported from HOL Light)
*)

section\<open>Equivalence Between Classical Borel Measurability and HOL Light's\<close>

theory Equivalence_Measurable_On_Borel
  imports Equivalence_Lebesgue_Henstock_Integration Improper_Integral Continuous_Extension
begin

subsection\<open>Austin's Lemma\<close>

lemma Austin_Lemma:
  fixes \<D> :: "'a::euclidean_space set set"
  assumes "finite \" and \: "\D. D \ \ \ \k a b. D = cbox a b \ (\i \ Basis. b\i - a\i = k)"
  obtains \<C> where "\<C> \<subseteq> \<D>" "pairwise disjnt \<C>"
                  "measure lebesgue (\\) \ measure lebesgue (\\) / 3 ^ (DIM('a))"
  using assms
proof (induction "card \" arbitrary: \ thesis rule: less_induct)
  case less
  show ?case
  proof (cases "\ = {}")
    case True
    then show thesis
      using less by auto
  next
    case False
    then have "Max (Sigma_Algebra.measure lebesgue ` \) \ Sigma_Algebra.measure lebesgue ` \"
      using Max_in finite_imageI \<open>finite \<D>\<close> by blast
    then obtain D where "D \ \" and "measure lebesgue D = Max (measure lebesgue ` \)"
      by auto
    then have D: "\C. C \ \ \ measure lebesgue C \ measure lebesgue D"
      by (simp add: \<open>finite \<D>\<close>)
    let ?\<E> = "{C. C \<in> \<D> - {D} \<and> disjnt C D}"
    obtain \<D>' where \<D>'sub: "\<D>' \<subseteq> ?\<E>" and \<D>'dis: "pairwise disjnt \<D>'"
      and \<D>'m: "measure lebesgue (\<Union>\<D>') \<ge> measure lebesgue (\<Union>?\<E>) / 3 ^ (DIM('a))"
    proof (rule less.hyps)
      have *: "?\ \ \"
        using \<open>D \<in> \<D>\<close> by auto
      then show "card ?\ < card \" "finite ?\"
        by (auto simp: \<open>finite \<D>\<close> psubset_card_mono)
      show "\k a b. D = cbox a b \ (\i\Basis. b \ i - a \ i = k)" if "D \ ?\" for D
        using less.prems(3) that by auto
    qed
    then have [simp]: "\\' - D = \\'"
      by (auto simp: disjnt_iff)
    show ?thesis
    proof (rule less.prems)
      show "insert D \' \ \"
        using \<D>'sub \<open>D \<in> \<D>\<close> by blast
      show "disjoint (insert D \')"
        using \<D>'dis \<D>'sub by (fastforce simp add: pairwise_def disjnt_sym)
      obtain a3 b3 where  m3: "content (cbox a3 b3) = 3 ^ DIM('a) * measure lebesgue D"
        and sub3: "\C. \C \ \; \ disjnt C D\ \ C \ cbox a3 b3"
      proof -
        obtain k a b where ab: "D = cbox a b" and k: "\i. i \ Basis \ b\i - a\i = k"
          using less.prems \<open>D \<in> \<D>\<close> by meson
        then have eqk: "\i. i \ Basis \ a \ i \ b \ i \ k \ 0"
          by force
        show thesis
        proof
          let ?a = "(a + b) /\<^sub>R 2 - (3/2) *\<^sub>R (b - a)"
          let ?b = "(a + b) /\<^sub>R 2 + (3/2) *\<^sub>R (b - a)"
          have eq: "(\i\Basis. b \ i * 3 - a \ i * 3) = (\i\Basis. b \ i - a \ i) * 3 ^ DIM('a)"
            by (simp add: comm_monoid_mult_class.prod.distrib flip: left_diff_distrib inner_diff_left)
          show "content (cbox ?a ?b) = 3 ^ DIM('a) * measure lebesgue D"
            by (simp add: content_cbox_if box_eq_empty algebra_simps eq ab k)
          show "C \ cbox ?a ?b" if "C \ \" and CD: "\ disjnt C D" for C
          proof -
            obtain k' a' b' where ab': "C = cbox a' b'" and k': "\i. i \ Basis \ b'\i - a'\i = k'"
              using less.prems \<open>C \<in> \<D>\<close> by meson
            then have eqk': "\i. i \ Basis \ a' \ i \ b' \ i \ k' \ 0"
              by force
            show ?thesis
            proof (clarsimp simp add: disjoint_interval disjnt_def ab ab' not_less subset_box algebra_simps)
              show "a \ i * 2 \ a' \ i + b \ i \ a \ i + b' \ i \ b \ i * 2"
                if * [rule_format]: "\j\Basis. a' \ j \ b' \ j" and "i \ Basis" for i
              proof -
                have "a' \ i \ b' \ i \ a \ i \ b \ i \ a \ i \ b' \ i \ a' \ i \ b \ i"
                  using \<open>i \<in> Basis\<close> CD by (simp_all add: disjoint_interval disjnt_def ab ab' not_less)
                then show ?thesis
                  using D [OF \<open>C \<in> \<D>\<close>] \<open>i \<in> Basis\<close>
                  apply (simp add: ab ab' k k' eqk eqk' content_cbox_cases)
                  using k k' by fastforce
              qed
            qed
          qed
        qed
      qed
      have \<D>lm: "\<And>D. D \<in> \<D> \<Longrightarrow> D \<in> lmeasurable"
        using less.prems(3) by blast
      have "measure lebesgue (\\) \ measure lebesgue (cbox a3 b3 \ (\\ - cbox a3 b3))"
      proof (rule measure_mono_fmeasurable)
        show "\\ \ sets lebesgue"
          using \<D>lm \<open>finite \<D>\<close> by blast
        show "cbox a3 b3 \ (\\ - cbox a3 b3) \ lmeasurable"
          by (simp add: \<D>lm fmeasurable.Un fmeasurable.finite_Union less.prems(2) subset_eq)
      qed auto
      also have "\ = content (cbox a3 b3) + measure lebesgue (\\ - cbox a3 b3)"
        by (simp add: \<D>lm fmeasurable.finite_Union less.prems(2) measure_Un2 subsetI)
      also have "\ \ (measure lebesgue D + measure lebesgue (\\')) * 3 ^ DIM('a)"
      proof -
        have "(\\ - cbox a3 b3) \ \?\"
          using sub3 by fastforce
        then have "measure lebesgue (\\ - cbox a3 b3) \ measure lebesgue (\?\)"
        proof (rule measure_mono_fmeasurable)
          show "\ \ - cbox a3 b3 \ sets lebesgue"
            by (simp add: \<D>lm fmeasurableD less.prems(2) sets.Diff sets.finite_Union subsetI)
          show "\ {C \ \ - {D}. disjnt C D} \ lmeasurable"
            using \<D>lm less.prems(2) by auto
        qed
        then have "measure lebesgue (\\ - cbox a3 b3) / 3 ^ DIM('a) \ measure lebesgue (\ \')"
          using \<D>'m by (simp add: field_split_simps)
        then show ?thesis
          by (simp add: m3 field_simps)
      qed
      also have "\ \ measure lebesgue (\(insert D \')) * 3 ^ DIM('a)"
      proof (simp add: \<D>lm \<open>D \<in> \<D>\<close>)
        show "measure lebesgue D + measure lebesgue (\\') \ measure lebesgue (D \ \ \')"
        proof (subst measure_Un2)
          show "\ \' \ lmeasurable"
            by (meson \<D>lm \<open>insert D \<D>' \<subseteq> \<D>\<close> fmeasurable.finite_Union less.prems(2) finite_subset subset_eq subset_insertI)
          show "measure lebesgue D + measure lebesgue (\ \') \ measure lebesgue D + measure lebesgue (\ \' - D)"
            using \<open>insert D \<D>' \<subseteq> \<D>\<close> infinite_super less.prems(2) by force
        qed (simp add: \<D>lm \<open>D \<in> \<D>\<close>)
      qed
      finally show "measure lebesgue (\\) / 3 ^ DIM('a) \ measure lebesgue (\(insert D \'))"
        by (simp add: field_split_simps)
    qed
  qed
qed


subsection\<open>A differentiability-like property of the indefinite integral.        \<close>

proposition integrable_ccontinuous_explicit:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes "\a b::'a. f integrable_on cbox a b"
  obtains N where
       "negligible N"
       "\x e. \x \ N; 0 < e\ \
               \<exists>d>0. \<forall>h. 0 < h \<and> h < d \<longrightarrow>
                         norm(integral (cbox x (x + h *\<^sub>R One)) f /\<^sub>R h ^ DIM('a) - f x) < e"
proof -
  define BOX where "BOX \ \h. \x::'a. cbox x (x + h *\<^sub>R One)"
  define BOX2 where "BOX2 \ \h. \x::'a. cbox (x - h *\<^sub>R One) (x + h *\<^sub>R One)"
  define i where "i \ \h x. integral (BOX h x) f /\<^sub>R h ^ DIM('a)"
  define \<Psi> where "\<Psi> \<equiv> \<lambda>x r. \<forall>d>0. \<exists>h. 0 < h \<and> h < d \<and> r \<le> norm(i h x - f x)"
  let ?N = "{x. \e>0. \ x e}"
  have "\N. negligible N \ (\x e. x \ N \ 0 < e \ \ \ x e)"
  proof (rule exI ; intro conjI allI impI)
    let ?M =  "\n. {x. \ x (inverse(real n + 1))}"
    have "negligible ({x. \ x \} \ cbox a b)"
      if "\ > 0" for a b \
    proof (cases "negligible(cbox a b)")
      case True
      then show ?thesis
        by (simp add: negligible_Int)
    next
      case False
      then have "box a b \ {}"
        by (simp add: negligible_interval)
      then have ab: "\i. i \ Basis \ a\i < b\i"
        by (simp add: box_ne_empty)
      show ?thesis
        unfolding negligible_outer_le
      proof (intro allI impI)
        fix e::real
        let ?ee = "(e * \) / 2 / 6 ^ (DIM('a))"
        assume "e > 0"
        then have gt0: "?ee > 0"
          using \<open>\<mu> > 0\<close> by auto
        have f': "f integrable_on cbox (a - One) (b + One)"
          using assms by blast
        obtain \<gamma> where "gauge \<gamma>"
          and \<gamma>: "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox (a - One) (b + One)); \<gamma> fine p\<rbrakk>
                    \<Longrightarrow> (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < ?ee"
          using Henstock_lemma [OF f' gt0] that by auto
        let ?E = "{x. x \ cbox a b \ \ x \}"
        have "\h>0. BOX h x \ \ x \
                    BOX h x \<subseteq> cbox (a - One) (b + One) \<and> \<mu> \<le> norm (i h x - f x)"
          if "x \ cbox a b" "\ x \" for x
        proof -
          obtain d where "d > 0" and d: "ball x d \ \ x"
            using gaugeD [OF \<open>gauge \<gamma>\<close>, of x] openE by blast
          then obtain h where "0 < h" "h < 1" and hless: "h < d / real DIM('a)"
                          and mule: "\ \ norm (i h x - f x)"
            using \<open>\<Psi> x \<mu>\<close> [unfolded \<Psi>_def, rule_format, of "min 1 (d / DIM('a))"]
            by auto
          show ?thesis
          proof (intro exI conjI)
            show "0 < h" "\ \ norm (i h x - f x)" by fact+
            have "BOX h x \ ball x d"
            proof (clarsimp simp: BOX_def mem_box dist_norm algebra_simps)
              fix y
              assume "\i\Basis. x \ i \ y \ i \ y \ i \ h + x \ i"
              then have lt: "\(x - y) \ i\ < d / real DIM('a)" if "i \ Basis" for i
                using hless that by (force simp: inner_diff_left)
              have "norm (x - y) \ (\i\Basis. \(x - y) \ i\)"
                using norm_le_l1 by blast
              also have "\ < d"
                using sum_bounded_above_strict [of Basis "\i. \(x - y) \ i\" "d / DIM('a)", OF lt]
                by auto
              finally show "norm (x - y) < d" .
            qed
            with d show "BOX h x \ \ x"
              by blast
            show "BOX h x \ cbox (a - One) (b + One)"
              using that \<open>h < 1\<close>
              by (force simp: BOX_def mem_box algebra_simps intro: subset_box_imp)
          qed
        qed
        then obtain \<eta> where h0: "\<And>x. x \<in> ?E \<Longrightarrow> \<eta> x > 0"
          and BOX_\<gamma>: "\<And>x. x \<in> ?E \<Longrightarrow> BOX (\<eta> x) x \<subseteq> \<gamma> x"
          and "\x. x \ ?E \ BOX (\ x) x \ cbox (a - One) (b + One) \ \ \ norm (i (\ x) x - f x)"
          by simp metis
        then have BOX_cbox: "\x. x \ ?E \ BOX (\ x) x \ cbox (a - One) (b + One)"
             and \<mu>_le: "\<And>x. x \<in> ?E \<Longrightarrow> \<mu> \<le> norm (i (\<eta> x) x - f x)"
          by blast+
        define \<gamma>' where "\<gamma>' \<equiv> \<lambda>x. if x \<in> cbox a b \<and> \<Psi> x \<mu> then ball x (\<eta> x) else \<gamma> x"
        have "gauge \'"
          using \<open>gauge \<gamma>\<close> by (auto simp: h0 gauge_def \<gamma>'_def)
        obtain \<D> where "countable \<D>"
          and \<D>: "\<Union>\<D> \<subseteq> cbox a b"
          "\K. K \ \ \ interior K \ {} \ (\c d. K = cbox c d)"
          and Dcovered: "\K. K \ \ \ \x. x \ cbox a b \ \ x \ \ x \ K \ K \ \' x"
          and subUD: "?E \ \\"
          by (rule covering_lemma [of ?E a b \<gamma>']) (simp_all add: Bex_def \<open>box a b \<noteq> {}\<close> \<open>gauge \<gamma>'\<close>)
        then have "\ \ sets lebesgue"
          by fastforce
        show "\T. {x. \ x \} \ cbox a b \ T \ T \ lmeasurable \ measure lebesgue T \ e"
        proof (intro exI conjI)
          show "{x. \ x \} \ cbox a b \ \\"
            apply auto
            using subUD by auto
          have mUE: "measure lebesgue (\ \) \ measure lebesgue (cbox a b)"
            if "\ \ \" "finite \" for \
          proof (rule measure_mono_fmeasurable)
            show "\ \ \ cbox a b"
              using \<D>(1) that(1) by blast
            show "\ \ \ sets lebesgue"
              by (metis \<D>(2) fmeasurable.finite_Union fmeasurableD lmeasurable_cbox subset_eq that)
          qed auto
          then show "\\ \ lmeasurable"
            by (metis \<D>(2) \<open>countable \<D>\<close> fmeasurable_Union_bound lmeasurable_cbox)
          then have leab: "measure lebesgue (\\) \ measure lebesgue (cbox a b)"
            by (meson \<D>(1) fmeasurableD lmeasurable_cbox measure_mono_fmeasurable)
          obtain \<F> where "\<F> \<subseteq> \<D>" "finite \<F>"
            and \<F>: "measure lebesgue (\<Union>\<D>) \<le> 2 * measure lebesgue (\<Union>\<F>)"
          proof (cases "measure lebesgue (\\) = 0")
            case True
            then show ?thesis
              by (force intro: that [where \<F> = "{}"])
          next
            case False
            obtain \<F> where "\<F> \<subseteq> \<D>" "finite \<F>"
              and \<F>: "measure lebesgue (\<Union>\<D>)/2 < measure lebesgue (\<Union>\<F>)"
            proof (rule measure_countable_Union_approachable [of \<D> "measure lebesgue (\<Union>\<D>) / 2" "content (cbox a b)"])
              show "countable \"
                by fact
              show "0 < measure lebesgue (\ \) / 2"
                using False by (simp add: zero_less_measure_iff)
              show Dlm: "D \ lmeasurable" if "D \ \" for D
                using \<D>(2) that by blast
              show "measure lebesgue (\ \) \ content (cbox a b)"
                if "\ \ \" "finite \" for \
              proof -
                have "measure lebesgue (\ \) \ measure lebesgue (\\)"
                proof (rule measure_mono_fmeasurable)
                  show "\ \ \ \ \"
                    by (simp add: Sup_subset_mono \<open>\<F> \<subseteq> \<D>\<close>)
                  show "\ \ \ sets lebesgue"
                    by (meson Dlm fmeasurableD sets.finite_Union subset_eq that)
                  show "\ \ \ lmeasurable"
                    by fact
                qed
                also have "\ \ measure lebesgue (cbox a b)"
                proof (rule measure_mono_fmeasurable)
                  show "\ \ \ sets lebesgue"
                    by (simp add: \<open>\<Union> \<D> \<in> lmeasurable\<close> fmeasurableD)
                qed (auto simp:\<D>(1))
                finally show ?thesis
                  by simp
              qed
            qed auto
            then show ?thesis
              using that by auto
          qed
          obtain tag where tag_in_E: "\D. D \ \ \ tag D \ ?E"
            and tag_in_self: "\D. D \ \ \ tag D \ D"
            and tag_sub: "\D. D \ \ \ D \ \' (tag D)"
            using Dcovered by simp metis
          then have sub_ball_tag: "\D. D \ \ \ D \ ball (tag D) (\ (tag D))"
            by (simp add: \<gamma>'_def)
          define \<Phi> where "\<Phi> \<equiv> \<lambda>D. BOX (\<eta>(tag D)) (tag D)"
          define \<Phi>2 where "\<Phi>2 \<equiv> \<lambda>D. BOX2 (\<eta>(tag D)) (tag D)"
          obtain \<C> where "\<C> \<subseteq> \<Phi>2 ` \<F>" "pairwise disjnt \<C>"
            "measure lebesgue (\\) \ measure lebesgue (\(\2`\)) / 3 ^ (DIM('a))"
          proof (rule Austin_Lemma)
            show "finite (\2`\)"
              using \<open>finite \<F>\<close> by blast
            have "\k a b. \2 D = cbox a b \ (\i\Basis. b \ i - a \ i = k)" if "D \ \" for D
              apply (rule_tac x="2 * \(tag D)" in exI)
              apply (rule_tac x="tag D - \(tag D) *\<^sub>R One" in exI)
              apply (rule_tac x="tag D + \(tag D) *\<^sub>R One" in exI)
              using that
              apply (auto simp: \<Phi>2_def BOX2_def algebra_simps)
              done
            then show "\D. D \ \2 ` \ \ \k a b. D = cbox a b \ (\i\Basis. b \ i - a \ i = k)"
              by blast
          qed auto
          then obtain \<G> where "\<G> \<subseteq> \<F>" and disj: "pairwise disjnt (\<Phi>2 ` \<G>)"
            and "measure lebesgue (\(\2 ` \)) \ measure lebesgue (\(\2`\)) / 3 ^ (DIM('a))"
            unfolding \<Phi>2_def subset_image_iff
            by (meson empty_subsetI equals0D pairwise_imageI)
          moreover
          have "measure lebesgue (\(\2 ` \)) * 3 ^ DIM('a) \ e/2"
          proof -
            have "finite \"
              using \<open>finite \<F>\<close> \<open>\<G> \<subseteq> \<F>\<close> infinite_super by blast
            have BOX2_m: "\x. x \ tag ` \ \ BOX2 (\ x) x \ lmeasurable"
              by (auto simp: BOX2_def)
            have BOX_m: "\x. x \ tag ` \ \ BOX (\ x) x \ lmeasurable"
              by (auto simp: BOX_def)
            have BOX_sub: "BOX (\ x) x \ BOX2 (\ x) x" for x
              by (auto simp: BOX_def BOX2_def subset_box algebra_simps)
            have DISJ2: "BOX2 (\ (tag X)) (tag X) \ BOX2 (\ (tag Y)) (tag Y) = {}"
              if "X \ \" "Y \ \" "tag X \ tag Y" for X Y
            proof -
              obtain i where i: "i \ Basis" "tag X \ i \ tag Y \ i"
                using \<open>tag X \<noteq> tag Y\<close> by (auto simp: euclidean_eq_iff [of "tag X"])
              have XY: "X \ \" "Y \ \"
                using \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> that by auto
              then have "0 \ \ (tag X)" "0 \ \ (tag Y)"
                by (meson h0 le_cases not_le tag_in_E)+
              with XY i have "BOX2 (\ (tag X)) (tag X) \ BOX2 (\ (tag Y)) (tag Y)"
                unfolding eq_iff
                by (fastforce simp add: BOX2_def subset_box algebra_simps)
              then show ?thesis
                using disj that by (auto simp: pairwise_def disjnt_def \<Phi>2_def)
            qed
            then have BOX2_disj: "pairwise (\x y. negligible (BOX2 (\ x) x \ BOX2 (\ y) y)) (tag ` \)"
              by (simp add: pairwise_imageI)
            then have BOX_disj: "pairwise (\x y. negligible (BOX (\ x) x \ BOX (\ y) y)) (tag ` \)"
            proof (rule pairwise_mono)
              show "negligible (BOX (\ x) x \ BOX (\ y) y)"
                if "negligible (BOX2 (\ x) x \ BOX2 (\ y) y)" for x y
                by (metis (no_types, opaque_lifting) that Int_mono negligible_subset BOX_sub)
            qed auto

            have eq: "\box. (\D. box (\ (tag D)) (tag D)) ` \ = (\t. box (\ t) t) ` tag ` \"
              by (simp add: image_comp)
            have "measure lebesgue (BOX2 (\ t) t) * 3 ^ DIM('a)
                = measure lebesgue (BOX (\<eta> t) t) * (2*3) ^ DIM('a)"
              if "t \ tag ` \" for t
            proof -
              have "content (cbox (t - \ t *\<^sub>R One) (t + \ t *\<^sub>R One))
                  = content (cbox t (t + \<eta> t *\<^sub>R One)) * 2 ^ DIM('a)"
                using that by (simp add: algebra_simps content_cbox_if box_eq_empty)
              then show ?thesis
                by (simp add: BOX2_def BOX_def flip: power_mult_distrib)
            qed
            then have "measure lebesgue (\(\2 ` \)) * 3 ^ DIM('a) = measure lebesgue (\(\ ` \)) * 6 ^ DIM('a)"
              unfolding \<Phi>_def \<Phi>2_def eq
              by (simp add: measure_negligible_finite_Union_image
                  \<open>finite \<G>\<close> BOX2_m BOX_m BOX2_disj BOX_disj sum_distrib_right
                  del: UN_simps)
            also have "\ \ e/2"
            proof -
              have "\ * measure lebesgue (\D\\. \ D) \ \ * (\D \ \`\. measure lebesgue D)"
                using \<open>\<mu> > 0\<close> \<open>finite \<G>\<close> by (force simp: BOX_m \<Phi>_def fmeasurableD intro: measure_Union_le)
              also have "\ = (\D \ \`\. measure lebesgue D * \)"
                by (metis mult.commute sum_distrib_right)
              also have "\ \ (\(x, K) \ (\D. (tag D, \ D)) ` \. norm (content K *\<^sub>R f x - integral K f))"
              proof (rule sum_le_included; clarify?)
                fix D
                assume "D \ \"
                then have "\ (tag D) > 0"
                  using \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> h0 tag_in_E by auto
                then have m_\<Phi>: "measure lebesgue (\<Phi> D) > 0"
                  by (simp add: \<Phi>_def BOX_def algebra_simps)
                have "\ \ norm (i (\(tag D)) (tag D) - f(tag D))"
                  using \<mu>_le \<open>D \<in> \<G>\<close> \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> tag_in_E by auto
                also have "\ = norm ((content (\ D) *\<^sub>R f(tag D) - integral (\ D) f) /\<^sub>R measure lebesgue (\ D))"
                  using m_\<Phi>
                  unfolding i_def \<Phi>_def BOX_def
                  by (simp add: algebra_simps content_cbox_plus norm_minus_commute)
                finally have "measure lebesgue (\ D) * \ \ norm (content (\ D) *\<^sub>R f(tag D) - integral (\ D) f)"
                  using m_\<Phi> by simp (simp add: field_simps)
                then show "\y\(\D. (tag D, \ D)) ` \.
                        snd y = \<Phi> D \<and> measure lebesgue (\<Phi> D) * \<mu> \<le> (case y of (x, k) \<Rightarrow> norm (content k *\<^sub>R f x - integral k f))"
                  using \<open>D \<in> \<G>\<close> by auto
              qed (use \<open>finite \<G>\<close> in auto)
              also have "\ < ?ee"
              proof (rule \<gamma>)
                show "(\D. (tag D, \ D)) ` \ tagged_partial_division_of cbox (a - One) (b + One)"
                  unfolding tagged_partial_division_of_def
                proof (intro conjI allI impI ; clarify ?)
                  show "tag D \ \ D"
                    if "D \ \" for D
                    using that \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> h0 tag_in_E
                    by (auto simp: \<Phi>_def BOX_def mem_box algebra_simps eucl_less_le_not_le in_mono)
                  show "y \ cbox (a - One) (b + One)" if "D \ \" "y \ \ D" for D y
                    using that BOX_cbox \<Phi>_def \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> tag_in_E by blast
                  show "tag D = tag E \ \ D = \ E"
                    if "D \ \" "E \ \" and ne: "interior (\ D) \ interior (\ E) \ {}" for D E
                  proof -
                    have "BOX2 (\ (tag D)) (tag D) \ BOX2 (\ (tag E)) (tag E) = {} \ tag E = tag D"
                      using DISJ2 \<open>D \<in> \<G>\<close> \<open>E \<in> \<G>\<close> by force
                    then have "BOX (\ (tag D)) (tag D) \ BOX (\ (tag E)) (tag E) = {} \ tag E = tag D"
                      using BOX_sub by blast
                    then show "tag D = tag E \ \ D = \ E"
                      by (metis \<Phi>_def interior_Int interior_empty ne)
                  qed
                qed (use \<open>finite \<G>\<close> \<Phi>_def BOX_def in auto)
                show "\ fine (\D. (tag D, \ D)) ` \"
                  unfolding fine_def \<Phi>_def using BOX_\<gamma> \<open>\<F> \<subseteq> \<D>\<close> \<open>\<G> \<subseteq> \<F>\<close> tag_in_E by blast
              qed
              finally show ?thesis
                using \<open>\<mu> > 0\<close> by (auto simp: field_split_simps)
          qed
            finally show ?thesis .
          qed
          moreover
          have "measure lebesgue (\\) \ measure lebesgue (\(\2`\))"
          proof (rule measure_mono_fmeasurable)
            have "D \ ball (tag D) (\(tag D))" if "D \ \" for D
              using \<open>\<F> \<subseteq> \<D>\<close> sub_ball_tag that by blast
            moreover have "ball (tag D) (\(tag D)) \ BOX2 (\ (tag D)) (tag D)" if "D \ \" for D
            proof (clarsimp simp: \<Phi>2_def BOX2_def mem_box algebra_simps dist_norm)
              fix x and i::'a
              assume "norm (tag D - x) < \ (tag D)" and "i \ Basis"
              then have "\tag D \ i - x \ i\ \ \ (tag D)"
                by (metis eucl_less_le_not_le inner_commute inner_diff_right norm_bound_Basis_le)
              then show "tag D \ i \ x \ i + \ (tag D) \ x \ i \ \ (tag D) + tag D \ i"
                by (simp add: abs_diff_le_iff)
            qed
            ultimately show "\\ \ \(\2`\)"
              by (force simp: \<Phi>2_def)
            show "\\ \ sets lebesgue"
              using \<open>finite \<F>\<close> \<open>\<D> \<subseteq> sets lebesgue\<close> \<open>\<F> \<subseteq> \<D>\<close> by blast
            show "\(\2`\) \ lmeasurable"
              unfolding \<Phi>2_def BOX2_def using \<open>finite \<F>\<close> by blast
          qed
          ultimately
          have "measure lebesgue (\\) \ e/2"
            by (auto simp: field_split_simps)
          then show "measure lebesgue (\\) \ e"
            using \<F> by linarith
        qed
      qed
    qed
    then have "\j. negligible {x. \ x (inverse(real j + 1))}"
      using negligible_on_intervals
      by (metis (full_types) inverse_positive_iff_positive le_add_same_cancel1 linorder_not_le nat_le_real_less not_add_less1 of_nat_0)
    then have "negligible ?M"
      by auto
    moreover have "?N \ ?M"
    proof (clarsimp simp: dist_norm)
      fix y e
      assume "0 < e"
        and ye [rule_format]: "\ y e"
      then obtain k where k: "0 < k" "inverse (real k + 1) < e"
        by (metis One_nat_def add.commute less_add_same_cancel2 less_imp_inverse_less less_trans neq0_conv of_nat_1 of_nat_Suc reals_Archimedean zero_less_one)
      with ye show "\n. \ y (inverse (real n + 1))"
        apply (rule_tac x=k in exI)
        unfolding \<Psi>_def
        by (force intro: less_le_trans)
    qed
    ultimately show "negligible ?N"
      by (blast intro: negligible_subset)
    show "\ \ x e" if "x \ ?N \ 0 < e" for x e
      using that by blast
  qed
  with that show ?thesis
    unfolding i_def BOX_def \<Psi>_def by (fastforce simp add: not_le)
qed


subsection\<open>HOL Light measurability\<close>

definition measurable_on :: "('a::euclidean_space \ 'b::real_normed_vector) \ 'a set \ bool"
  (infixr \<open>measurable'_on\<close> 46)
  where "f measurable_on S \
        \<exists>N g. negligible N \<and>
              (\<forall>n. continuous_on UNIV (g n)) \<and>
              (\<forall>x. x \<notin> N \<longrightarrow> (\<lambda>n. g n x) \<longlonglongrightarrow> (if x \<in> S then f x else 0))"

lemma measurable_on_UNIV:
  "(\x. if x \ S then f x else 0) measurable_on UNIV \ f measurable_on S"
  by (auto simp: measurable_on_def)

lemma measurable_on_spike_set:
  assumes f: "f measurable_on S" and neg: "negligible ((S - T) \ (T - S))"
  shows "f measurable_on T"
proof -
  obtain N and F
    where N: "negligible N"
      and conF: "\n. continuous_on UNIV (F n)"
      and tendsF: "\x. x \ N \ (\n. F n x) \ (if x \ S then f x else 0)"
    using f by (auto simp: measurable_on_def)
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "continuous_on UNIV (\x. F n x)" for n
      by (intro conF continuous_intros)
    show "negligible (N \ (S - T) \ (T - S))"
      by (metis (full_types) N neg negligible_Un_eq)
    show "(\n. F n x) \ (if x \ T then f x else 0)"
      if "x \ (N \ (S - T) \ (T - S))" for x
      using that tendsF [of x] by auto
  qed
qed

text\<open> Various common equivalent forms of function measurability.                \<close>

lemma measurable_on_0 [simp]: "(\x. 0) measurable_on S"
  unfolding measurable_on_def
proof (intro exI conjI allI impI)
  show "(\n. 0) \ (if x \ S then 0::'b else 0)" for x
    by force
qed auto

lemma measurable_on_scaleR_const:
  assumes f: "f measurable_on S"
  shows "(\x. c *\<^sub>R f x) measurable_on S"
proof -
  obtain NF and F
    where NF: "negligible NF"
      and conF: "\n. continuous_on UNIV (F n)"
      and tendsF: "\x. x \ NF \ (\n. F n x) \ (if x \ S then f x else 0)"
    using f by (auto simp: measurable_on_def)
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "continuous_on UNIV (\x. c *\<^sub>R F n x)" for n
      by (intro conF continuous_intros)
    show "(\n. c *\<^sub>R F n x) \ (if x \ S then c *\<^sub>R f x else 0)"
      if "x \ NF" for x
      using tendsto_scaleR [OF tendsto_const tendsF, of x] that by auto
  qed (auto simp: NF)
qed


lemma measurable_on_cmul:
  fixes c :: real
  assumes "f measurable_on S"
  shows "(\x. c * f x) measurable_on S"
  using measurable_on_scaleR_const [OF assms] by simp

lemma measurable_on_cdivide:
  fixes c :: real
  assumes "f measurable_on S"
  shows "(\x. f x / c) measurable_on S"
proof (cases "c=0")
  case False
  then show ?thesis
    using measurable_on_cmul [of f S "1/c"]
    by (simp add: assms)
qed auto


lemma measurable_on_minus:
   "f measurable_on S \ (\x. -(f x)) measurable_on S"
  using measurable_on_scaleR_const [of f S "-1"] by auto


lemma continuous_imp_measurable_on:
   "continuous_on UNIV f \ f measurable_on UNIV"
  unfolding measurable_on_def
  apply (rule_tac x="{}" in exI)
  apply (rule_tac x="\n. f" in exI, auto)
  done

proposition integrable_subintervals_imp_measurable:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes "\a b. f integrable_on cbox a b"
  shows "f measurable_on UNIV"
proof -
  define BOX where "BOX \ \h. \x::'a. cbox x (x + h *\<^sub>R One)"
  define i where "i \ \h x. integral (BOX h x) f /\<^sub>R h ^ DIM('a)"
  obtain N where "negligible N"
    and k: "\x e. \x \ N; 0 < e\
            \<Longrightarrow> \<exists>d>0. \<forall>h. 0 < h \<and> h < d \<longrightarrow>
                  norm (integral (cbox x (x + h *\<^sub>R One)) f /\<^sub>R h ^ DIM('a) - f x) < e"
    using integrable_ccontinuous_explicit assms by blast
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "continuous_on UNIV ((\n x. i (inverse(Suc n)) x) n)" for n
    proof (clarsimp simp: continuous_on_iff)
      show "\d>0. \x'. dist x' x < d \ dist (i (inverse (1 + real n)) x') (i (inverse (1 + real n)) x) < e"
        if "0 < e"
        for x e
      proof -
        let ?e = "e / (1 + real n) ^ DIM('a)"
        have "?e > 0"
          using \<open>e > 0\<close> by auto
        moreover have "x \ cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One)"
          by (simp add: mem_box inner_diff_left inner_left_distrib)
        moreover have "x + One /\<^sub>R real (Suc n) \ cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One)"
          by (auto simp: mem_box inner_diff_left inner_left_distrib field_simps)
        ultimately obtain \<delta> where "\<delta> > 0"
          and \<delta>: "\<And>c' d'. \<lbrakk>c' \<in> cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One);
                           d' \ cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One);
                           norm(c' - x) \ \; norm(d' - (x + One /\<^sub>R Suc n)) \ \\
                          \<Longrightarrow> norm(integral(cbox c' d') f - integral(cbox x (x + One /\<^sub>R Suc n)) f) < ?e"
          by (blast intro: indefinite_integral_continuous [of f _ _ x] assms)
        show ?thesis
        proof (intro exI impI conjI allI)
          show "min \ 1 > 0"
            using \<open>\<delta> > 0\<close> by auto
          show "dist (i (inverse (1 + real n)) y) (i (inverse (1 + real n)) x) < e"
            if "dist y x < min \ 1" for y
          proof -
            have no: "norm (y - x) < 1"
              using that by (auto simp: dist_norm)
            have le1: "inverse (1 + real n) \ 1"
              by (auto simp: field_split_simps)
            have "norm (integral (cbox y (y + One /\<^sub>R real (Suc n))) f
                - integral (cbox x (x + One /\<^sub>R real (Suc n))) f)
                < e / (1 + real n) ^ DIM('a)"
            proof (rule \<delta>)
              show "y \ cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One)"
                using no by (auto simp: mem_box algebra_simps dest: Basis_le_norm [of _ "y-x"])
              show "y + One /\<^sub>R real (Suc n) \ cbox (x - 2 *\<^sub>R One) (x + 2 *\<^sub>R One)"
              proof (simp add: dist_norm mem_box algebra_simps, intro ballI conjI)
                fix i::'a
                assume "i \ Basis"
                then have 1: "\y \ i - x \ i\ < 1"
                  by (metis inner_commute inner_diff_right no norm_bound_Basis_lt)
                moreover have "\ < (2 + inverse (1 + real n))" "1 \ 2 - inverse (1 + real n)"
                  by (auto simp: field_simps)
                ultimately show "x \ i \ y \ i + (2 + inverse (1 + real n))"
                                "y \ i + inverse (1 + real n) \ x \ i + 2"
                  by linarith+
              qed
              show "norm (y - x) \ \" "norm (y + One /\<^sub>R real (Suc n) - (x + One /\<^sub>R real (Suc n))) \ \"
                using that by (auto simp: dist_norm)
            qed
            then show ?thesis
              using that by (simp add: dist_norm i_def BOX_def flip: scaleR_diff_right) (simp add: field_simps)
          qed
        qed
      qed
    qed
    show "negligible N"
      by (simp add: \<open>negligible N\<close>)
    show "(\n. i (inverse (Suc n)) x) \ (if x \ UNIV then f x else 0)"
      if "x \ N" for x
      unfolding lim_sequentially
    proof clarsimp
      show "\no. \n\no. dist (i (inverse (1 + real n)) x) (f x) < e"
        if "0 < e" for e
      proof -
        obtain d where "d > 0"
          and d: "\h. \0 < h; h < d\ \
              norm (integral (cbox x (x + h *\<^sub>R One)) f /\<^sub>R h ^ DIM('a) - f x) < e"
          using k [of x e] \<open>x \<notin> N\<close> \<open>0 < e\<close> by blast
        then obtain M where M: "M \ 0" "0 < inverse (real M)" "inverse (real M) < d"
          using real_arch_invD by auto
        show ?thesis
        proof (intro exI allI impI)
          show "dist (i (inverse (1 + real n)) x) (f x) < e"
            if "M \ n" for n
          proof -
            have *: "0 < inverse (1 + real n)" "inverse (1 + real n) \ inverse M"
              using that \<open>M \<noteq> 0\<close> by auto
            show ?thesis
              using that M
              apply (simp add: i_def BOX_def dist_norm)
              apply (blast intro: le_less_trans * d)
              done
          qed
        qed
      qed
    qed
  qed
qed


subsection\<open>Composing continuous and measurable functions; a few variants\<close>

lemma measurable_on_compose_continuous:
   assumes f: "f measurable_on UNIV" and g: "continuous_on UNIV g"
   shows "(g \ f) measurable_on UNIV"
proof -
  obtain N and F
    where "negligible N"
      and conF: "\n. continuous_on UNIV (F n)"
      and tendsF: "\x. x \ N \ (\n. F n x) \ f x"
    using f by (auto simp: measurable_on_def)
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "negligible N"
      by fact
    show "continuous_on UNIV (g \ (F n))" for n
      using conF continuous_on_compose continuous_on_subset g by blast
    show "(\n. (g \ F n) x) \ (if x \ UNIV then (g \ f) x else 0)"
      if "x \ N" for x :: 'a
      using that g tendsF by (auto simp: continuous_on_def intro: tendsto_compose)
  qed
qed

lemma measurable_on_compose_continuous_0:
   assumes f: "f measurable_on S" and g: "continuous_on UNIV g" and "g 0 = 0"
   shows "(g \ f) measurable_on S"
proof -
  have f': "(\x. if x \ S then f x else 0) measurable_on UNIV"
    using f measurable_on_UNIV by blast
  show ?thesis
    using measurable_on_compose_continuous [OF f' g]
    by (simp add: measurable_on_UNIV o_def if_distrib \<open>g 0 = 0\<close> cong: if_cong)
qed


lemma measurable_on_compose_continuous_box:
  assumes fm: "f measurable_on UNIV" and fab: "\x. f x \ box a b"
    and contg: "continuous_on (box a b) g"
  shows "(g \ f) measurable_on UNIV"
proof -
  have "\\. (\n. continuous_on UNIV (\ n)) \ (\x. x \ N \ (\n. \ n x) \ g (f x))"
    if "negligible N"
      and conth [rule_format]: "\n. continuous_on UNIV (\x. h n x)"
      and tends [rule_format]: "\x. x \ N \ (\n. h n x) \ f x"
    for N and h :: "nat \ 'a \ 'b"
  proof -
    define \<theta> where "\<theta> \<equiv> \<lambda>n x. (\<Sum>i\<in>Basis. (max (a\<bullet>i + (b\<bullet>i - a\<bullet>i) / real (n+2))
                                            (min ((h n x)\<bullet>i)
                                                 (b\<bullet>i - (b\<bullet>i - a\<bullet>i) / real (n+2)))) *\<^sub>R i)"
    have aibi: "\i. i \ Basis \ a \ i < b \ i"
      using box_ne_empty(2) fab by auto
    then have *: "\i n. i \ Basis \ a \ i + real n * (a \ i) < b \ i + real n * (b \ i)"
      by (meson add_mono_thms_linordered_field(3) less_eq_real_def mult_left_mono of_nat_0_le_iff)
    show ?thesis
    proof (intro exI conjI allI impI)
      show "continuous_on UNIV (g \ (\ n))" for n :: nat
        unfolding \<theta>_def
        apply (intro continuous_on_compose2 [OF contg] continuous_intros conth)
        apply (auto simp: aibi * mem_box less_max_iff_disj min_less_iff_disj field_split_simps)
        done
      show "(\n. (g \ \ n) x) \ g (f x)"
        if "x \ N" for x
        unfolding o_def
      proof (rule isCont_tendsto_compose [where g=g])
        show "isCont g (f x)"
          using contg fab continuous_on_eq_continuous_at by blast
        have "(\n. \ n x) \ (\i\Basis. max (a \ i) (min (f x \ i) (b \ i)) *\<^sub>R i)"
          unfolding \<theta>_def
        proof (intro tendsto_intros \<open>x \<notin> N\<close> tends)
          fix i::'b
          assume "i \ Basis"
          have a: "(\n. a \ i + (b \ i - a \ i) / real n) \ a\i + 0"
            by (intro tendsto_add lim_const_over_n tendsto_const)
          show "(\n. a \ i + (b \ i - a \ i) / real (n + 2)) \ a \ i"
            using LIMSEQ_ignore_initial_segment [where k=2, OF a] by simp
          have b: "(\n. b\i - (b \ i - a \ i) / (real n)) \ b\i - 0"
            by (intro tendsto_diff lim_const_over_n tendsto_const)
          show "(\n. b \ i - (b \ i - a \ i) / real (n + 2)) \ b \ i"
            using LIMSEQ_ignore_initial_segment [where k=2, OF b] by simp
        qed
        also have "(\i\Basis. max (a \ i) (min (f x \ i) (b \ i)) *\<^sub>R i) = (\i\Basis. (f x \ i) *\<^sub>R i)"
          using fab by (auto simp add: mem_box intro: sum.cong)
        also have "\ = f x"
          using euclidean_representation by blast
        finally show "(\n. \ n x) \ f x" .
      qed
    qed
  qed
  then show ?thesis
    using fm by (auto simp: measurable_on_def)
qed

lemma measurable_on_Pair:
  assumes f: "f measurable_on S" and g: "g measurable_on S"
  shows "(\x. (f x, g x)) measurable_on S"
proof -
  obtain NF and F
    where NF: "negligible NF"
      and conF: "\n. continuous_on UNIV (F n)"
      and tendsF: "\x. x \ NF \ (\n. F n x) \ (if x \ S then f x else 0)"
    using f by (auto simp: measurable_on_def)
  obtain NG and G
    where NG: "negligible NG"
      and conG: "\n. continuous_on UNIV (G n)"
      and tendsG: "\x. x \ NG \ (\n. G n x) \ (if x \ S then g x else 0)"
    using g by (auto simp: measurable_on_def)
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "negligible (NF \ NG)"
      by (simp add: NF NG)
    show "continuous_on UNIV (\x. (F n x, G n x))" for n
      using conF conG continuous_on_Pair by blast
    show "(\n. (F n x, G n x)) \ (if x \ S then (f x, g x) else 0)"
      if "x \ NF \ NG" for x
      using tendsto_Pair [OF tendsF tendsG, of x x] that unfolding zero_prod_def
      by (simp add: split: if_split_asm)
  qed
qed

lemma measurable_on_combine:
  assumes f: "f measurable_on S" and g: "g measurable_on S"
    and h: "continuous_on UNIV (\x. h (fst x) (snd x))" and "h 0 0 = 0"
  shows "(\x. h (f x) (g x)) measurable_on S"
proof -
  have *: "(\x. h (f x) (g x)) = (\x. h (fst x) (snd x)) \ (\x. (f x, g x))"
    by auto
  show ?thesis
    unfolding * by (auto simp: measurable_on_compose_continuous_0 measurable_on_Pair assms)
qed

lemma measurable_on_add:
  assumes f: "f measurable_on S" and g: "g measurable_on S"
  shows "(\x. f x + g x) measurable_on S"
  by (intro continuous_intros measurable_on_combine [OF assms]) auto

lemma measurable_on_diff:
  assumes f: "f measurable_on S" and g: "g measurable_on S"
  shows "(\x. f x - g x) measurable_on S"
  by (intro continuous_intros measurable_on_combine [OF assms]) auto

lemma measurable_on_scaleR:
  assumes f: "f measurable_on S" and g: "g measurable_on S"
  shows "(\x. f x *\<^sub>R g x) measurable_on S"
  by (intro continuous_intros measurable_on_combine [OF assms]) auto

lemma measurable_on_sum:
  assumes "finite I" "\i. i \ I \ f i measurable_on S"
  shows "(\x. sum (\i. f i x) I) measurable_on S"
  using assms by (induction I) (auto simp: measurable_on_add)

lemma measurable_on_spike:
  assumes f: "f measurable_on T" and "negligible S" and gf: "\x. x \ T - S \ g x = f x"
  shows "g measurable_on T"
proof -
  obtain NF and F
    where NF: "negligible NF"
      and conF: "\n. continuous_on UNIV (F n)"
      and tendsF: "\x. x \ NF \ (\n. F n x) \ (if x \ T then f x else 0)"
    using f by (auto simp: measurable_on_def)
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "negligible (NF \ S)"
      by (simp add: NF \<open>negligible S\<close>)
    show "\x. x \ NF \ S \ (\n. F n x) \ (if x \ T then g x else 0)"
      by (metis (full_types) Diff_iff Un_iff gf tendsF)
  qed (auto simp: conF)
qed

proposition indicator_measurable_on:
  assumes "S \ sets lebesgue"
  shows "indicat_real S measurable_on UNIV"
proof -
  { fix n::nat
    let ?\<epsilon> = "(1::real) / (2 * 2^n)"
    have \<epsilon>: "?\<epsilon> > 0"
      by auto
    obtain T where "closed T" "T \ S" "S-T \ lmeasurable" and ST: "emeasure lebesgue (S - T) < ?\"
      by (meson \<epsilon> assms sets_lebesgue_inner_closed)
    obtain U where "open U" "S \ U" "(U - S) \ lmeasurable" and US: "emeasure lebesgue (U - S) < ?\"
      by (meson \<epsilon> assms sets_lebesgue_outer_open)
    have eq: "-T \ U = (S-T) \ (U - S)"
      using \<open>T \<subseteq> S\<close> \<open>S \<subseteq> U\<close> by auto
    have "emeasure lebesgue ((S-T) \ (U - S)) \ emeasure lebesgue (S - T) + emeasure lebesgue (U - S)"
      using \<open>S - T \<in> lmeasurable\<close> \<open>U - S \<in> lmeasurable\<close> emeasure_subadditive by blast
    also have "\ < ?\ + ?\"
      using ST US add_mono_ennreal by metis
    finally have le: "emeasure lebesgue (-T \ U) < ennreal (1 / 2^n)"
      by (simp add: eq)
    have 1: "continuous_on (T \ -U) (indicat_real S)"
      unfolding indicator_def of_bool_def
    proof (rule continuous_on_cases [OF \<open>closed T\<close>])
      show "closed (- U)"
        using \<open>open U\<close> by blast
      show "continuous_on T (\x. 1::real)" "continuous_on (- U) (\x. 0::real)"
        by (auto simp: continuous_on)
      show "\x. x \ T \ x \ S \ x \ - U \ x \ S \ (1::real) = 0"
        using \<open>T \<subseteq> S\<close> \<open>S \<subseteq> U\<close> by auto
    qed
    have 2: "closedin (top_of_set UNIV) (T \ -U)"
      using \<open>closed T\<close> \<open>open U\<close> by auto
    obtain g where "continuous_on UNIV g" "\x. x \ T \ -U \ g x = indicat_real S x" "\x. norm(g x) \ 1"
      by (rule Tietze [OF 1 2, of 1]) auto
    with le have "\g E. continuous_on UNIV g \ (\x \ -E. g x = indicat_real S x) \
                        (\<forall>x. norm(g x) \<le> 1) \<and> E \<in> sets lebesgue \<and> emeasure lebesgue E < ennreal (1 / 2^n)"
      apply (rule_tac x=g in exI)
      apply (rule_tac x="-T \ U" in exI)
      using \<open>S - T \<in> lmeasurable\<close> \<open>U - S \<in> lmeasurable\<close> eq by auto
  }
  then obtain g E where cont: "\n. continuous_on UNIV (g n)"
    and geq: "\n x. x \ - E n \ g n x = indicat_real S x"
    and ng1: "\n x. norm(g n x) \ 1"
    and Eset: "\n. E n \ sets lebesgue"
    and Em: "\n. emeasure lebesgue (E n) < ennreal (1 / 2^n)"
    by metis
  have null: "limsup E \ null_sets lebesgue"
  proof (rule borel_cantelli_limsup1 [OF Eset])
    show "emeasure lebesgue (E n) < \" for n
      by (metis Em infinity_ennreal_def order.asym top.not_eq_extremum)
    show "summable (\n. measure lebesgue (E n))"
    proof (rule summable_comparison_test' [OF summable_geometric, of "1/2" 0])
      show "norm (measure lebesgue (E n)) \ (1/2) ^ n" for n
        using Em [of n] by (simp add: measure_def enn2real_leI power_one_over)
    qed auto
  qed
  have tends: "(\n. g n x) \ indicat_real S x" if "x \ limsup E" for x
  proof -
    have "\\<^sub>F n in sequentially. x \ - E n"
      using that by (simp add: mem_limsup_iff not_frequently)
    then show ?thesis
      unfolding tendsto_iff dist_real_def
      by (simp add: eventually_mono geq)
  qed
  show ?thesis
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "negligible (limsup E)"
      using negligible_iff_null_sets null by blast
    show "continuous_on UNIV (g n)" for n
      using cont by blast
  qed (use tends in auto)
qed

lemma measurable_on_restrict:
  assumes f: "f measurable_on UNIV" and S: "S \ sets lebesgue"
  shows "(\x. if x \ S then f x else 0) measurable_on UNIV"
proof -
  have "indicat_real S measurable_on UNIV"
    by (simp add: S indicator_measurable_on)
  then show ?thesis
    using measurable_on_scaleR [OF _ f, of "indicat_real S"]
    by (simp add: indicator_scaleR_eq_if)
qed

lemma measurable_on_const_UNIV: "(\x. k) measurable_on UNIV"
  by (simp add: continuous_imp_measurable_on)

lemma measurable_on_const [simp]: "S \ sets lebesgue \ (\x. k) measurable_on S"
  using measurable_on_UNIV measurable_on_const_UNIV measurable_on_restrict by blast

lemma simple_function_indicator_representation_real:
  fixes f ::"'a \ real"
  assumes f: "simple_function M f" and x: "x \ space M" and nn: "\x. f x \ 0"
  shows "f x = (\y \ f ` space M. y * indicator (f -` {y} \ space M) x)"
proof -
  have f': "simple_function M (ennreal \ f)"
    by (simp add: f)
  have *: "f x =
     enn2real
      (\<Sum>y\<in> ennreal ` f ` space M.
         y * indicator ((ennreal \<circ> f) -` {y} \<inter> space M) x)"
    using arg_cong [OF simple_function_indicator_representation [OF f' x], of enn2real, simplified nn o_def] nn
    unfolding o_def image_comp
    by (metis enn2real_ennreal)
  have "enn2real (\y\ennreal ` f ` space M. if ennreal (f x) = y \ x \ space M then y else 0)
      = sum (enn2real \<circ> (\<lambda>y. if ennreal (f x) = y \<and> x \<in> space M then y else 0))
            (ennreal ` f ` space M)"
    by (rule enn2real_sum) auto
  also have "\ = sum (enn2real \ (\y. if ennreal (f x) = y \ x \ space M then y else 0) \ ennreal)
                   (f ` space M)"
    by (rule sum.reindex) (use nn in \<open>auto simp: inj_on_def intro: sum.cong\<close>)
  also have "\ = (\y\f ` space M. if f x = y \ x \ space M then y else 0)"
    using nn
    by (auto simp: inj_on_def intro: sum.cong)
  finally show ?thesis
    by (subst *) (simp add: enn2real_sum indicator_def of_bool_def if_distrib cong: if_cong)
qed

lemma\<^marker>\<open>tag important\<close> simple_function_induct_real
    [consumes 1, case_names cong set mult add, induct set: simple_function]:
  fixes u :: "'a \ real"
  assumes u: "simple_function M u"
  assumes cong: "\f g. simple_function M f \ simple_function M g \ (AE x in M. f x = g x) \ P f \ P g"
  assumes set: "\A. A \ sets M \ P (indicator A)"
  assumes mult: "\u c. P u \ P (\x. c * u x)"
  assumes add: "\u v. P u \ P v \ P (\x. u x + v x)"
  and nn: "\x. u x \ 0"
  shows "P u"
proof (rule cong)
  from AE_space show "AE x in M. (\y\u ` space M. y * indicator (u -` {y} \ space M) x) = u x"
  proof eventually_elim
    fix x assume x: "x \ space M"
    from simple_function_indicator_representation_real[OF u x] nn
    show "(\y\u ` space M. y * indicator (u -` {y} \ space M) x) = u x"
      by metis
  qed
next
  from u have "finite (u ` space M)"
    unfolding simple_function_def by auto
  then show "P (\x. \y\u ` space M. y * indicator (u -` {y} \ space M) x)"
  proof induct
    case empty
    then show ?case
      using set[of "{}"] by (simp add: indicator_def[abs_def])
  next
    case (insert a F)
    have eq: "\ {y. u x = y \ (y = a \ y \ F) \ x \ space M}
            = (if u x = a \<and> x \<in> space M then a else 0) + \<Sum> {y. u x = y \<and> y \<in> F \<and> x \<in> space M}" for x
    proof (cases "x \ space M")
      case True
      have *: "{y. u x = y \ (y = a \ y \ F)} = {y. u x = a \ y = a} \ {y. u x = y \ y \ F}"
        by auto
      show ?thesis
        using insert by (simp add: * True)
    qed auto
    have a: "P (\x. a * indicator (u -` {a} \ space M) x)"
    proof (intro mult set)
      show "u -` {a} \ space M \ sets M"
        using u by auto
    qed
    show ?case
      using nn insert a
      by (simp add: eq indicator_times_eq_if [where f = "\x. a"] add)
  qed
next
  show "simple_function M (\x. (\y\u ` space M. y * indicator (u -` {y} \ space M) x))"
    apply (subst simple_function_cong)
    apply (rule simple_function_indicator_representation_real[symmetric])
    apply (auto intro: u nn)
    done
qed fact

proposition simple_function_measurable_on_UNIV:
  fixes f :: "'a::euclidean_space \ real"
  assumes f: "simple_function lebesgue f" and nn: "\x. f x \ 0"
  shows "f measurable_on UNIV"
  using f
proof (induction f)
  case (cong f g)
  then obtain N where "negligible N" "{x. g x \ f x} \ N"
    by (auto simp: eventually_ae_filter_negligible eq_commute)
  then show ?case
    by (blast intro: measurable_on_spike cong)
next
  case (set S)
  then show ?case
    by (simp add: indicator_measurable_on)
next
  case (mult u c)
  then show ?case
    by (simp add: measurable_on_cmul)
  case (add u v)
  then show ?case
    by (simp add: measurable_on_add)
qed (auto simp: nn)

lemma simple_function_lebesgue_if:
  fixes f :: "'a::euclidean_space \ real"
  assumes f: "simple_function lebesgue f" and S: "S \ sets lebesgue"
  shows "simple_function lebesgue (\x. if x \ S then f x else 0)"
proof -
  have ffin: "finite (range f)" and fsets: "\x. f -` {f x} \ sets lebesgue"
    using f by (auto simp: simple_function_def)
  have "finite (f ` S)"
    by (meson finite_subset subset_image_iff ffin top_greatest)
  moreover have "finite ((\x. 0::real) ` T)" for T :: "'a set"
    by (auto simp: image_def)
  moreover have if_sets: "(\x. if x \ S then f x else 0) -` {f a} \ sets lebesgue" for a
  proof -
    have *: "(\x. if x \ S then f x else 0) -` {f a}
           = (if f a = 0 then -S \<union> f -` {f a} else (f -` {f a}) \<inter> S)"
      by (auto simp: split: if_split_asm)
    show ?thesis
      unfolding * by (metis Compl_in_sets_lebesgue S sets.Int sets.Un fsets)
  qed
  moreover have "(\x. if x \ S then f x else 0) -` {0} \ sets lebesgue"
  proof (cases "0 \ range f")
    case True
    then show ?thesis
      by (metis (no_types, lifting) if_sets rangeE)
  next
    case False
    then have "(\x. if x \ S then f x else 0) -` {0} = -S"
      by auto
    then show ?thesis
      by (simp add: Compl_in_sets_lebesgue S)
  qed
  ultimately show ?thesis
    by (auto simp: simple_function_def)
qed

corollary simple_function_measurable_on:
  fixes f :: "'a::euclidean_space \ real"
  assumes f: "simple_function lebesgue f" and nn: "\x. f x \ 0" and S: "S \ sets lebesgue"
  shows "f measurable_on S"
  by (simp add: measurable_on_UNIV [symmetric, of f] S f simple_function_lebesgue_if nn simple_function_measurable_on_UNIV)

lemma
  fixes f :: "'a::euclidean_space \ 'b::ordered_euclidean_space"
  assumes f: "f measurable_on S" and g: "g measurable_on S"
  shows measurable_on_sup: "(\x. sup (f x) (g x)) measurable_on S"
  and   measurable_on_inf: "(\x. inf (f x) (g x)) measurable_on S"
proof -
  obtain NF and F
    where NF: "negligible NF"
      and conF: "\n. continuous_on UNIV (F n)"
      and tendsF: "\x. x \ NF \ (\n. F n x) \ (if x \ S then f x else 0)"
    using f by (auto simp: measurable_on_def)
  obtain NG and G
    where NG: "negligible NG"
      and conG: "\n. continuous_on UNIV (G n)"
      and tendsG: "\x. x \ NG \ (\n. G n x) \ (if x \ S then g x else 0)"
    using g by (auto simp: measurable_on_def)
  show "(\x. sup (f x) (g x)) measurable_on S"
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "continuous_on UNIV (\x. sup (F n x) (G n x))" for n
      unfolding sup_max eucl_sup  by (intro conF conG continuous_intros)
    show "(\n. sup (F n x) (G n x)) \ (if x \ S then sup (f x) (g x) else 0)"
      if "x \ NF \ NG" for x
      using tendsto_sup [OF tendsF tendsG, of x x] that by auto
  qed (simp add: NF NG)
  show "(\x. inf (f x) (g x)) measurable_on S"
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "continuous_on UNIV (\x. inf (F n x) (G n x))" for n
      unfolding inf_min eucl_inf  by (intro conF conG continuous_intros)
    show "(\n. inf (F n x) (G n x)) \ (if x \ S then inf (f x) (g x) else 0)"
      if "x \ NF \ NG" for x
      using tendsto_inf [OF tendsF tendsG, of x x] that by auto
  qed (simp add: NF NG)
qed

proposition measurable_on_componentwise_UNIV:
  "f measurable_on UNIV \ (\i\Basis. (\x. (f x \ i) *\<^sub>R i) measurable_on UNIV)"
  (is "?lhs = ?rhs")
proof
  assume L: ?lhs
  show ?rhs
  proof
    fix i::'b
    assume "i \ Basis"
    have cont: "continuous_on UNIV (\x. (x \ i) *\<^sub>R i)"
      by (intro continuous_intros)
    show "(\x. (f x \ i) *\<^sub>R i) measurable_on UNIV"
      using measurable_on_compose_continuous [OF L cont]
      by (simp add: o_def)
  qed
next
  assume ?rhs
  then have "\N g. negligible N \
              (\<forall>n. continuous_on UNIV (g n)) \<and>
              (\<forall>x. x \<notin> N \<longrightarrow> (\<lambda>n. g n x) \<longlonglongrightarrow> (f x \<bullet> i) *\<^sub>R i)"
    if "i \ Basis" for i
    by (simp add: measurable_on_def that)
  then obtain N g where N: "\i. i \ Basis \ negligible (N i)"
        and cont: "\i n. i \ Basis \ continuous_on UNIV (g i n)"
        and tends: "\i x. \i \ Basis; x \ N i\ \ (\n. g i n x) \ (f x \ i) *\<^sub>R i"
    by metis
  show ?lhs
    unfolding measurable_on_def
  proof (intro exI conjI allI impI)
    show "negligible (\i \ Basis. N i)"
      using N eucl.finite_Basis by blast
    show "continuous_on UNIV (\x. (\i\Basis. g i n x))" for n
      by (intro continuous_intros cont)
  next
    fix x
    assume "x \ (\i \ Basis. N i)"
    then have "\i. i \ Basis \ x \ N i"
      by auto
    then have "(\n. (\i\Basis. g i n x)) \ (\i\Basis. (f x \ i) *\<^sub>R i)"
      by (intro tends tendsto_intros)
    then show "(\n. (\i\Basis. g i n x)) \ (if x \ UNIV then f x else 0)"
      by (simp add: euclidean_representation)
  qed
qed

corollary measurable_on_componentwise:
  "f measurable_on S \ (\i\Basis. (\x. (f x \ i) *\<^sub>R i) measurable_on S)"
  apply (subst measurable_on_UNIV [symmetric])
  apply (subst measurable_on_componentwise_UNIV)
  apply (simp add: measurable_on_UNIV if_distrib [of "\x. inner x _"] if_distrib [of "\x. scaleR x _"] cong: if_cong)
  done


(*FIXME: avoid duplication of proofs WRT borel_measurable_implies_simple_function_sequence*)
lemma\<^marker>\<open>tag important\<close> borel_measurable_implies_simple_function_sequence_real:
  fixes u :: "'a \ real"
  assumes u[measurable]: "u \ borel_measurable M" and nn: "\x. u x \ 0"
  shows "\f. incseq f \ (\i. simple_function M (f i)) \ (\x. bdd_above (range (\i. f i x))) \
             (\<forall>i x. 0 \<le> f i x) \<and> u = (SUP i. f i)"
proof -
  define f where [abs_def]:
    "f i x = real_of_int (floor ((min i (u x)) * 2^i)) / 2^i" for i x

  have [simp]: "0 \ f i x" for i x
    by (auto simp: f_def intro!: divide_nonneg_nonneg mult_nonneg_nonneg nn)

  have *: "2^n * real_of_int x = real_of_int (2^n * x)" for n x
    by simp

  have "real_of_int \real i * 2 ^ i\ = real_of_int \i * 2 ^ i\" for i
    by (intro arg_cong[where f=real_of_int]) simp
  then have [simp]: "real_of_int \real i * 2 ^ i\ = i * 2 ^ i" for i
    unfolding floor_of_nat by simp

  have bdd: "bdd_above (range (\i. f i x))" for x
    by (rule bdd_aboveI [where M = "u x"]) (auto simp: f_def field_simps min_def)

  have "incseq f"
  proof (intro monoI le_funI)
    fix m n :: nat and x assume "m \ n"
    moreover
    { fix d :: nat
      have "\2^d::real\ * \2^m * (min (of_nat m) (u x))\ \ \2^d * (2^m * (min (of_nat m) (u x)))\"
        by (rule le_mult_floor) (auto simp: nn)
      also have "\ \ \2^d * (2^m * (min (of_nat d + of_nat m) (u x)))\"
        by (intro floor_mono mult_mono min.mono)
           (auto simp: nn min_less_iff_disj of_nat_less_top)
      finally have "f m x \ f(m + d) x"
        unfolding f_def
        by (auto simp: field_simps power_add * simp del: of_int_mult) }
    ultimately show "f m x \ f n x"
      by (auto simp: le_iff_add)
  qed
  then have inc_f: "incseq (\i. f i x)" for x
    by (auto simp: incseq_def le_fun_def)
  moreover
  have "simple_function M (f i)" for i
  proof (rule simple_function_borel_measurable)
    have "\(min (of_nat i) (u x)) * 2 ^ i\ \ \int i * 2 ^ i\" for x
      by (auto split: split_min intro!: floor_mono)
    then have "f i ` space M \ (\n. real_of_int n / 2^i) ` {0 .. of_nat i * 2^i}"
--> --------------------

--> maximum size reached

--> --------------------

99%


¤ Dauer der Verarbeitung: 0.36 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.





                                                                                                                                                                                                                                                                                                                                                                                                     

Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder
Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge