Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: middle_value_select.prf Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Analysis/Lebesgue_Measure.thy
    Author:     Johannes Hölzl, TU München
    Author:     Robert Himmelmann, TU München
    Author:     Jeremy Avigad
    Author:     Luke Serafin
*)

section \<open>Lebesgue Measure\<close>

theory Lebesgue_Measure
imports
  Finite_Product_Measure
  Caratheodory
  Complete_Measure
  Summation_Tests
  Regularity
begin

lemma measure_eqI_lessThan:
  fixes M N :: "real measure"
  assumes sets: "sets M = sets borel" "sets N = sets borel"
  assumes fin: "\x. emeasure M {x <..} < \"
  assumes "\x. emeasure M {x <..} = emeasure N {x <..}"
  shows "M = N"
proof (rule measure_eqI_generator_eq_countable)
  let ?LT = "\a::real. {a <..}" let ?E = "range ?LT"
  show "Int_stable ?E"
    by (auto simp: Int_stable_def lessThan_Int_lessThan)

  show "?E \ Pow UNIV" "sets M = sigma_sets UNIV ?E" "sets N = sigma_sets UNIV ?E"
    unfolding sets borel_Ioi by auto

  show "?LT`Rats \ ?E" "(\i\Rats. ?LT i) = UNIV" "\a. a \ ?LT`Rats \ emeasure M a \ \"
    using fin by (auto intro: Rats_no_bot_less simp: less_top)
qed (auto intro: assms countable_rat)

subsection \<open>Measures defined by monotonous functions\<close>

text \<open>
  Every right-continuous and nondecreasing function gives rise to a measure on the reals:
\<close>

definition\<^marker>\<open>tag important\<close> interval_measure :: "(real \<Rightarrow> real) \<Rightarrow> real measure" where
  "interval_measure F =
     extend_measure UNIV {(a, b). a \<le> b} (\<lambda>(a, b). {a<..b}) (\<lambda>(a, b). ennreal (F b - F a))"

lemma\<^marker>\<open>tag important\<close> emeasure_interval_measure_Ioc:
  assumes "a \ b"
  assumes mono_F: "\x y. x \ y \ F x \ F y"
  assumes right_cont_F : "\a. continuous (at_right a) F"
  shows "emeasure (interval_measure F) {a<..b} = F b - F a"
proof (rule extend_measure_caratheodory_pair[OF interval_measure_def \<open>a \<le> b\<close>])
  show "semiring_of_sets UNIV {{a<..b} |a b :: real. a \ b}"
  proof (unfold_locales, safe)
    fix a b c d :: real assume *: "a \ b" "c \ d"
    then show "\C\{{a<..b} |a b. a \ b}. finite C \ disjoint C \ {a<..b} - {c<..d} = \C"
    proof cases
      let ?C = "{{a<..b}}"
      assume "b < c \ d \ a \ d \ c"
      with * have "?C \ {{a<..b} |a b. a \ b} \ finite ?C \ disjoint ?C \ {a<..b} - {c<..d} = \?C"
        by (auto simp add: disjoint_def)
      thus ?thesis ..
    next
      let ?C = "{{a<..c}, {d<..b}}"
      assume "\ (b < c \ d \ a \ d \ c)"
      with * have "?C \ {{a<..b} |a b. a \ b} \ finite ?C \ disjoint ?C \ {a<..b} - {c<..d} = \?C"
        by (auto simp add: disjoint_def Ioc_inj) (metis linear)+
      thus ?thesis ..
    qed
  qed (auto simp: Ioc_inj, metis linear)
next
  fix l r :: "nat \ real" and a b :: real
  assume l_r[simp]: "\n. l n \ r n" and "a \ b" and disj: "disjoint_family (\n. {l n<..r n})"
  assume lr_eq_ab: "(\i. {l i<..r i}) = {a<..b}"

  have [intro, simp]: "\a b. a \ b \ F a \ F b"
    by (auto intro!: l_r mono_F)

  { fix S :: "nat set" assume "finite S"
    moreover note \<open>a \<le> b\<close>
    moreover have "\i. i \ S \ {l i <.. r i} \ {a <.. b}"
      unfolding lr_eq_ab[symmetric] by auto
    ultimately have "(\i\S. F (r i) - F (l i)) \ F b - F a"
    proof (induction S arbitrary: a rule: finite_psubset_induct)
      case (psubset S)
      show ?case
      proof cases
        assume "\i\S. l i < r i"
        with \<open>finite S\<close> have "Min (l ` {i\<in>S. l i < r i}) \<in> l ` {i\<in>S. l i < r i}"
          by (intro Min_in) auto
        then obtain m where m: "m \ S" "l m < r m" "l m = Min (l ` {i\S. l i < r i})"
          by fastforce

        have "(\i\S. F (r i) - F (l i)) = (F (r m) - F (l m)) + (\i\S - {m}. F (r i) - F (l i))"
          using m psubset by (intro sum.remove) auto
        also have "(\i\S - {m}. F (r i) - F (l i)) \ F b - F (r m)"
        proof (intro psubset.IH)
          show "S - {m} \ S"
            using \<open>m\<in>S\<close> by auto
          show "r m \ b"
            using psubset.prems(2)[OF \<open>m\<in>S\<close>] \<open>l m < r m\<close> by auto
        next
          fix i assume "i \ S - {m}"
          then have i: "i \ S" "i \ m" by auto
          { assume i': "l i < r i" "l i < r m"
            with \<open>finite S\<close> i m have "l m \<le> l i"
              by auto
            with i' have "{l i <.. r i} \ {l m <.. r m} \ {}"
              by auto
            then have False
              using disjoint_family_onD[OF disj, of i m] i by auto }
          then have "l i \ r i \ r m \ l i"
            unfolding not_less[symmetric] using l_r[of i] by auto
          then show "{l i <.. r i} \ {r m <.. b}"
            using psubset.prems(2)[OF \<open>i\<in>S\<close>] by auto
        qed
        also have "F (r m) - F (l m) \ F (r m) - F a"
          using psubset.prems(2)[OF \<open>m \<in> S\<close>] \<open>l m < r m\<close>
          by (auto simp add: Ioc_subset_iff intro!: mono_F)
        finally show ?case
          by (auto intro: add_mono)
      qed (auto simp add: \<open>a \<le> b\<close> less_le)
    qed }
  note claim1 = this

  (* second key induction: a lower bound on the measures of any finite collection of Ai's
     that cover an interval {u..v} *)

  { fix S u v and l r :: "nat \ real"
    assume "finite S" "\i. i\S \ l i < r i" "{u..v} \ (\i\S. {l i<..< r i})"
    then have "F v - F u \ (\i\S. F (r i) - F (l i))"
    proof (induction arbitrary: v u rule: finite_psubset_induct)
      case (psubset S)
      show ?case
      proof cases
        assume "S = {}" then show ?case
          using psubset by (simp add: mono_F)
      next
        assume "S \ {}"
        then obtain j where "j \ S"
          by auto

        let ?R = "r j < u \ l j > v \ (\i\S-{j}. l i \ l j \ r j \ r i)"
        show ?case
        proof cases
          assume "?R"
          with \<open>j \<in> S\<close> psubset.prems have "{u..v} \<subseteq> (\<Union>i\<in>S-{j}. {l i<..< r i})"
            apply (auto simp: subset_eq Ball_def)
            apply (metis Diff_iff less_le_trans leD linear singletonD)
            apply (metis Diff_iff less_le_trans leD linear singletonD)
            apply (metis order_trans less_le_not_le linear)
            done
          with \<open>j \<in> S\<close> have "F v - F u \<le> (\<Sum>i\<in>S - {j}. F (r i) - F (l i))"
            by (intro psubset) auto
          also have "\ \ (\i\S. F (r i) - F (l i))"
            using psubset.prems
            by (intro sum_mono2 psubset) (auto intro: less_imp_le)
          finally show ?thesis .
        next
          assume "\ ?R"
          then have j: "u \ r j" "l j \ v" "\i. i \ S - {j} \ r i < r j \ l i > l j"
            by (auto simp: not_less)
          let ?S1 = "{i \ S. l i < l j}"
          let ?S2 = "{i \ S. r i > r j}"

          have "(\i\S. F (r i) - F (l i)) \ (\i\?S1 \ ?S2 \ {j}. F (r i) - F (l i))"
            using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j
            by (intro sum_mono2) (auto intro: less_imp_le)
          also have "(\i\?S1 \ ?S2 \ {j}. F (r i) - F (l i)) =
            (\<Sum>i\<in>?S1. F (r i) - F (l i)) + (\<Sum>i\<in>?S2 . F (r i) - F (l i)) + (F (r j) - F (l j))"
            using psubset(1) psubset.prems(1) j
            apply (subst sum.union_disjoint)
            apply simp_all
            apply (subst sum.union_disjoint)
            apply auto
            apply (metis less_le_not_le)
            done
          also (xtrans) have "(\i\?S1. F (r i) - F (l i)) \ F (l j) - F u"
            using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j
            apply (intro psubset.IH psubset)
            apply (auto simp: subset_eq Ball_def)
            apply (metis less_le_trans not_le)
            done
          also (xtrans) have "(\i\?S2. F (r i) - F (l i)) \ F v - F (r j)"
            using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j
            apply (intro psubset.IH psubset)
            apply (auto simp: subset_eq Ball_def)
            apply (metis le_less_trans not_le)
            done
          finally (xtrans) show ?case
            by (auto simp: add_mono)
        qed
      qed
    qed }
  note claim2 = this

  (* now prove the inequality going the other way *)
  have "ennreal (F b - F a) \ (\i. ennreal (F (r i) - F (l i)))"
  proof (rule ennreal_le_epsilon)
    fix epsilon :: real assume egt0: "epsilon > 0"
    have "\i. \d>0. F (r i + d) < F (r i) + epsilon / 2^(i+2)"
    proof
      fix i
      note right_cont_F [of "r i"]
      thus "\d>0. F (r i + d) < F (r i) + epsilon / 2^(i+2)"
        apply -
        apply (subst (asm) continuous_at_right_real_increasing)
        apply (rule mono_F, assumption)
        apply (drule_tac x = "epsilon / 2 ^ (i + 2)" in spec)
        apply (erule impE)
        using egt0 by (auto simp add: field_simps)
    qed
    then obtain delta where
        deltai_gt0: "\i. delta i > 0" and
        deltai_prop: "\i. F (r i + delta i) < F (r i) + epsilon / 2^(i+2)"
      by metis
    have "\a' > a. F a' - F a < epsilon / 2"
      apply (insert right_cont_F [of a])
      apply (subst (asm) continuous_at_right_real_increasing)
      using mono_F apply force
      apply (drule_tac x = "epsilon / 2" in spec)
      using egt0 unfolding mult.commute [of 2] by force
    then obtain a' where a'lea [arith]: "a' > a" and
      a_prop: "F a' - F a < epsilon / 2"
      by auto
    define S' where "S' = {i. l i < r i}"
    obtain S :: "nat set" where
      "S \ S'" and finS: "finite S" and
      Sprop: "{a'..b} \ (\i \ S. {l i<..
    proof (rule compactE_image)
      show "compact {a'..b}"
        by (rule compact_Icc)
      show "\i. i \ S' \ open ({l i<..
      have "{a'..b} \ {a <.. b}"
        by auto
      also have "{a <.. b} = (\i\S'. {l i<..r i})"
        unfolding lr_eq_ab[symmetric] by (fastforce simp add: S'_def intro: less_le_trans)
      also have "\ \ (\i \ S'. {l i<..
        apply (intro UN_mono)
        apply (auto simp: S'_def)
        apply (cut_tac i=i in deltai_gt0)
        apply simp
        done
      finally show "{a'..b} \ (\i \ S'. {l i<..
    qed
    with S'_def have Sprop2: "\i. i \ S \ l i < r i" by auto
    from finS have "\n. \i \ S. i \ n"
      by (subst finite_nat_set_iff_bounded_le [symmetric])
    then obtain n where Sbound [rule_format]: "\i \ S. i \ n" ..
    have "F b - F a' \ (\i\S. F (r i + delta i) - F (l i))"
      apply (rule claim2 [rule_format])
      using finS Sprop apply auto
      apply (frule Sprop2)
      apply (subgoal_tac "delta i > 0")
      apply arith
      by (rule deltai_gt0)
    also have "... \ (\i \ S. F(r i) - F(l i) + epsilon / 2^(i+2))"
      apply (rule sum_mono)
      apply simp
      apply (rule order_trans)
      apply (rule less_imp_le)
      apply (rule deltai_prop)
      by auto
    also have "... = (\i \ S. F(r i) - F(l i)) +
        (epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _")
      by (subst sum.distrib) (simp add: field_simps sum_distrib_left)
    also have "... \ ?t + (epsilon / 4) * (\ i < Suc n. (1 / 2)^i)"
      apply (rule add_left_mono)
      apply (rule mult_left_mono)
      apply (rule sum_mono2)
      using egt0 apply auto
      by (frule Sbound, auto)
    also have "... \ ?t + (epsilon / 2)"
      apply (rule add_left_mono)
      apply (subst geometric_sum)
      apply auto
      apply (rule mult_left_mono)
      using egt0 apply auto
      done
    finally have aux2: "F b - F a' \ (\i\S. F (r i) - F (l i)) + epsilon / 2"
      by simp

    have "F b - F a = (F b - F a') + (F a' - F a)"
      by auto
    also have "... \ (F b - F a') + epsilon / 2"
      using a_prop by (intro add_left_mono) simp
    also have "... \ (\i\S. F (r i) - F (l i)) + epsilon / 2 + epsilon / 2"
      apply (intro add_right_mono)
      apply (rule aux2)
      done
    also have "... = (\i\S. F (r i) - F (l i)) + epsilon"
      by auto
    also have "... \ (\i\n. F (r i) - F (l i)) + epsilon"
      using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono2)
    finally have "ennreal (F b - F a) \ (\i\n. ennreal (F (r i) - F (l i))) + epsilon"
      using egt0 by (simp add: sum_nonneg flip: ennreal_plus)
    then show "ennreal (F b - F a) \ (\i. ennreal (F (r i) - F (l i))) + (epsilon :: real)"
      by (rule order_trans) (auto intro!: add_mono sum_le_suminf simp del: sum_ennreal)
  qed
  moreover have "(\i. ennreal (F (r i) - F (l i))) \ ennreal (F b - F a)"
    using \<open>a \<le> b\<close> by (auto intro!: suminf_le_const ennreal_le_iff[THEN iffD2] claim1)
  ultimately show "(\n. ennreal (F (r n) - F (l n))) = ennreal (F b - F a)"
    by (rule antisym[rotated])
qed (auto simp: Ioc_inj mono_F)

lemma measure_interval_measure_Ioc:
  assumes "a \ b" and "\x y. x \ y \ F x \ F y" and "\a. continuous (at_right a) F"
  shows "measure (interval_measure F) {a <.. b} = F b - F a"
  unfolding measure_def
  by (simp add: assms emeasure_interval_measure_Ioc)

lemma emeasure_interval_measure_Ioc_eq:
  "(\x y. x \ y \ F x \ F y) \ (\a. continuous (at_right a) F) \
    emeasure (interval_measure F) {a <.. b} = (if a \<le> b then F b - F a else 0)"
  using emeasure_interval_measure_Ioc[of a b F] by auto

lemma\<^marker>\<open>tag important\<close> sets_interval_measure [simp, measurable_cong]:
    "sets (interval_measure F) = sets borel"
  apply (simp add: sets_extend_measure interval_measure_def borel_sigma_sets_Ioc)
  apply (rule sigma_sets_eqI)
  apply auto
  apply (case_tac "a \ ba")
  apply (auto intro: sigma_sets.Empty)
  done

lemma space_interval_measure [simp]: "space (interval_measure F) = UNIV"
  by (simp add: interval_measure_def space_extend_measure)

lemma emeasure_interval_measure_Icc:
  assumes "a \ b"
  assumes mono_F: "\x y. x \ y \ F x \ F y"
  assumes cont_F : "continuous_on UNIV F"
  shows "emeasure (interval_measure F) {a .. b} = F b - F a"
proof (rule tendsto_unique)
  { fix a b :: real assume "a \ b" then have "emeasure (interval_measure F) {a <.. b} = F b - F a"
      using cont_F
      by (subst emeasure_interval_measure_Ioc)
         (auto intro: mono_F continuous_within_subset simp: continuous_on_eq_continuous_within) }
  note * = this

  let ?F = "interval_measure F"
  show "((\a. F b - F a) \ emeasure ?F {a..b}) (at_left a)"
  proof (rule tendsto_at_left_sequentially)
    show "a - 1 < a" by simp
    fix X assume "\n. X n < a" "incseq X" "X \ a"
    with \<open>a \<le> b\<close> have "(\<lambda>n. emeasure ?F {X n<..b}) \<longlonglongrightarrow> emeasure ?F (\<Inter>n. {X n <..b})"
      apply (intro Lim_emeasure_decseq)
      apply (auto simp: decseq_def incseq_def emeasure_interval_measure_Ioc *)
      apply force
      apply (subst (asm ) *)
      apply (auto intro: less_le_trans less_imp_le)
      done
    also have "(\n. {X n <..b}) = {a..b}"
      using \<open>\<And>n. X n < a\<close>
      apply auto
      apply (rule LIMSEQ_le_const2[OF \<open>X \<longlonglongrightarrow> a\<close>])
      apply (auto intro: less_imp_le)
      apply (auto intro: less_le_trans)
      done
    also have "(\n. emeasure ?F {X n<..b}) = (\n. F b - F (X n))"
      using \<open>\<And>n. X n < a\<close> \<open>a \<le> b\<close> by (subst *) (auto intro: less_imp_le less_le_trans)
    finally show "(\n. F b - F (X n)) \ emeasure ?F {a..b}" .
  qed
  show "((\a. ennreal (F b - F a)) \ F b - F a) (at_left a)"
    by (rule continuous_on_tendsto_compose[where g="\x. x" and s=UNIV])
       (auto simp: continuous_on_ennreal continuous_on_diff cont_F)
qed (rule trivial_limit_at_left_real)

lemma\<^marker>\<open>tag important\<close> sigma_finite_interval_measure:
  assumes mono_F: "\x y. x \ y \ F x \ F y"
  assumes right_cont_F : "\a. continuous (at_right a) F"
  shows "sigma_finite_measure (interval_measure F)"
  apply unfold_locales
  apply (intro exI[of _ "(\(a, b). {a <.. b}) ` (\ \ \)"])
  apply (auto intro!: Rats_no_top_le Rats_no_bot_less countable_rat simp: emeasure_interval_measure_Ioc_eq[OF assms])
  done

subsection \<open>Lebesgue-Borel measure\<close>

definition\<^marker>\<open>tag important\<close> lborel :: "('a :: euclidean_space) measure" where
  "lborel = distr (\\<^sub>M b\Basis. interval_measure (\x. x)) borel (\f. \b\Basis. f b *\<^sub>R b)"

abbreviation\<^marker>\<open>tag important\<close> lebesgue :: "'a::euclidean_space measure"
  where "lebesgue \ completion lborel"

abbreviation\<^marker>\<open>tag important\<close> lebesgue_on :: "'a set \<Rightarrow> 'a::euclidean_space measure"
  where "lebesgue_on \ \ restrict_space (completion lborel) \"

lemma lebesgue_on_mono:
  assumes major: "AE x in lebesgue_on S. P x" and minor: "\x.\P x; x \ S\ \ Q x"
  shows "AE x in lebesgue_on S. Q x"
proof -
  have "AE a in lebesgue_on S. P a \ Q a"
    using minor space_restrict_space by fastforce
  then show ?thesis
    using major by auto
qed

lemma integral_eq_zero_null_sets:
  assumes "S \ null_sets lebesgue"
  shows "integral\<^sup>L (lebesgue_on S) f = 0"
proof (rule integral_eq_zero_AE)
  show "AE x in lebesgue_on S. f x = 0"
    by (metis (no_types, lifting) assms AE_not_in lebesgue_on_mono null_setsD2 null_sets_restrict_space order_refl)
qed

lemma
  shows sets_lborel[simp, measurable_cong]: "sets lborel = sets borel"
    and space_lborel[simp]: "space lborel = space borel"
    and measurable_lborel1[simp]: "measurable M lborel = measurable M borel"
    and measurable_lborel2[simp]: "measurable lborel M = measurable borel M"
  by (simp_all add: lborel_def)

lemma space_lebesgue_on [simp]: "space (lebesgue_on S) = S"
  by (simp add: space_restrict_space)

lemma sets_lebesgue_on_refl [iff]: "S \ sets (lebesgue_on S)"
    by (metis inf_top.right_neutral sets.top space_borel space_completion space_lborel space_restrict_space)

lemma Compl_in_sets_lebesgue: "-A \ sets lebesgue \ A \ sets lebesgue"
  by (metis Compl_eq_Diff_UNIV double_compl space_borel space_completion space_lborel Sigma_Algebra.sets.compl_sets)

lemma measurable_lebesgue_cong:
  assumes "\x. x \ S \ f x = g x"
  shows "f \ measurable (lebesgue_on S) M \ g \ measurable (lebesgue_on S) M"
  by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space)

lemma lebesgue_on_UNIV_eq: "lebesgue_on UNIV = lebesgue"
proof -
  have "measure_of UNIV (sets lebesgue) (emeasure lebesgue) = lebesgue"
    by (metis measure_of_of_measure space_borel space_completion space_lborel)
  then show ?thesis
    by (auto simp: restrict_space_def)
qed

lemma integral_restrict_Int:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes "S \ sets lebesgue" "T \ sets lebesgue"
  shows "integral\<^sup>L (lebesgue_on T) (\x. if x \ S then f x else 0) = integral\<^sup>L (lebesgue_on (S \ T)) f"
proof -
  have "(\x. indicat_real T x *\<^sub>R (if x \ S then f x else 0)) = (\x. indicat_real (S \ T) x *\<^sub>R f x)"
    by (force simp: indicator_def)
  then show ?thesis
    by (simp add: assms sets.Int Bochner_Integration.integral_restrict_space)
qed

lemma integral_restrict:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes "S \ T" "S \ sets lebesgue" "T \ sets lebesgue"
  shows "integral\<^sup>L (lebesgue_on T) (\x. if x \ S then f x else 0) = integral\<^sup>L (lebesgue_on S) f"
  using integral_restrict_Int [of S T f] assms
  by (simp add: Int_absorb2)

lemma integral_restrict_UNIV:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes "S \ sets lebesgue"
  shows "integral\<^sup>L lebesgue (\x. if x \ S then f x else 0) = integral\<^sup>L (lebesgue_on S) f"
  using integral_restrict_Int [of S UNIV f] assms
  by (simp add: lebesgue_on_UNIV_eq)

lemma integrable_lebesgue_on_empty [iff]:
  fixes f :: "'a::euclidean_space \ 'b::{second_countable_topology,banach}"
  shows "integrable (lebesgue_on {}) f"
  by (simp add: integrable_restrict_space)

lemma integral_lebesgue_on_empty [simp]:
  fixes f :: "'a::euclidean_space \ 'b::{second_countable_topology,banach}"
  shows "integral\<^sup>L (lebesgue_on {}) f = 0"
  by (simp add: Bochner_Integration.integral_empty)
lemma has_bochner_integral_restrict_space:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
  shows "has_bochner_integral (restrict_space M \) f i
     \<longleftrightarrow> has_bochner_integral M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) i"
  by (simp add: integrable_restrict_space [OF assms] integral_restrict_space [OF assms] has_bochner_integral_iff)

lemma integrable_restrict_UNIV:
  fixes f :: "'a::euclidean_space \ 'b::{banach, second_countable_topology}"
  assumes S: "S \ sets lebesgue"
  shows  "integrable lebesgue (\x. if x \ S then f x else 0) \ integrable (lebesgue_on S) f"
  using has_bochner_integral_restrict_space [of S lebesgue f] assms
  by (simp add: integrable.simps indicator_scaleR_eq_if)

lemma integral_mono_lebesgue_on_AE:
  fixes f::"_ \ real"
  assumes f: "integrable (lebesgue_on T) f"
    and gf: "AE x in (lebesgue_on S). g x \ f x"
    and f0: "AE x in (lebesgue_on T). 0 \ f x"
    and "S \ T" and S: "S \ sets lebesgue" and T: "T \ sets lebesgue"
  shows "(\x. g x \(lebesgue_on S)) \ (\x. f x \(lebesgue_on T))"
proof -
  have "(\x. g x \(lebesgue_on S)) = (\x. (if x \ S then g x else 0) \lebesgue)"
    by (simp add: Lebesgue_Measure.integral_restrict_UNIV S)
  also have "\ \ (\x. (if x \ T then f x else 0) \lebesgue)"
  proof (rule Bochner_Integration.integral_mono_AE')
    show "integrable lebesgue (\x. if x \ T then f x else 0)"
      by (simp add: integrable_restrict_UNIV T f)
    show "AE x in lebesgue. (if x \ S then g x else 0) \ (if x \ T then f x else 0)"
      using assms by (auto simp: AE_restrict_space_iff)
    show "AE x in lebesgue. 0 \ (if x \ T then f x else 0)"
      using f0 by (simp add: AE_restrict_space_iff T)
  qed
  also have "\ = (\x. f x \(lebesgue_on T))"
    using Lebesgue_Measure.integral_restrict_UNIV T by blast
  finally show ?thesis .
qed

subsection \<open>Borel measurability\<close>

lemma borel_measurable_if_I:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes f: "f \ borel_measurable (lebesgue_on S)" and S: "S \ sets lebesgue"
  shows "(\x. if x \ S then f x else 0) \ borel_measurable lebesgue"
proof -
  have eq: "{x. x \ S} \ {x. f x \ Y} = {x. x \ S} \ {x. f x \ Y} \ S" for Y
    by blast
  show ?thesis
  using f S
  apply (simp add: vimage_def in_borel_measurable_borel Ball_def)
  apply (elim all_forward imp_forward asm_rl)
  apply (simp only: Collect_conj_eq Collect_disj_eq imp_conv_disj eq)
  apply (auto simp: Compl_eq [symmetric] Compl_in_sets_lebesgue sets_restrict_space_iff)
  done
qed

lemma borel_measurable_if_D:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes "(\x. if x \ S then f x else 0) \ borel_measurable lebesgue"
  shows "f \ borel_measurable (lebesgue_on S)"
  using assms
  apply (simp add: in_borel_measurable_borel Ball_def)
  apply (elim all_forward imp_forward asm_rl)
  apply (force simp: space_restrict_space sets_restrict_space image_iff intro: rev_bexI)
  done

lemma borel_measurable_if:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes "S \ sets lebesgue"
  shows "(\x. if x \ S then f x else 0) \ borel_measurable lebesgue \ f \ borel_measurable (lebesgue_on S)"
  using assms borel_measurable_if_D borel_measurable_if_I by blast

lemma borel_measurable_if_lebesgue_on:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes "S \ sets lebesgue" "T \ sets lebesgue" "S \ T"
  shows "(\x. if x \ S then f x else 0) \ borel_measurable (lebesgue_on T) \ f \ borel_measurable (lebesgue_on S)"
    (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    using measurable_restrict_mono [OF _ \<open>S \<subseteq> T\<close>]
    by (subst measurable_lebesgue_cong [where g = "(\x. if x \ S then f x else 0)"]) auto
next
  assume ?rhs then show ?lhs
    by (simp add: \<open>S \<in> sets lebesgue\<close> borel_measurable_if_I measurable_restrict_space1)
qed

lemma borel_measurable_vimage_halfspace_component_lt:
     "f \ borel_measurable (lebesgue_on S) \
      (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i < a} \<in> sets (lebesgue_on S))"
  apply (rule trans [OF borel_measurable_iff_halfspace_less])
  apply (fastforce simp add: space_restrict_space)
  done

lemma borel_measurable_vimage_halfspace_component_ge:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  shows "f \ borel_measurable (lebesgue_on S) \
         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<ge> a} \<in> sets (lebesgue_on S))"
  apply (rule trans [OF borel_measurable_iff_halfspace_ge])
  apply (fastforce simp add: space_restrict_space)
  done

lemma borel_measurable_vimage_halfspace_component_gt:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  shows "f \ borel_measurable (lebesgue_on S) \
         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i > a} \<in> sets (lebesgue_on S))"
  apply (rule trans [OF borel_measurable_iff_halfspace_greater])
  apply (fastforce simp add: space_restrict_space)
  done

lemma borel_measurable_vimage_halfspace_component_le:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  shows "f \ borel_measurable (lebesgue_on S) \
         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<le> a} \<in> sets (lebesgue_on S))"
  apply (rule trans [OF borel_measurable_iff_halfspace_le])
  apply (fastforce simp add: space_restrict_space)
  done

lemma
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  shows borel_measurable_vimage_open_interval:
         "f \ borel_measurable (lebesgue_on S) \
         (\<forall>a b. {x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S))" (is ?thesis1)
   and borel_measurable_vimage_open:
         "f \ borel_measurable (lebesgue_on S) \
         (\<forall>T. open T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))" (is ?thesis2)
proof -
  have "{x \ S. f x \ box a b} \ sets (lebesgue_on S)" if "f \ borel_measurable (lebesgue_on S)" for a b
  proof -
    have "S = S \ space lebesgue"
      by simp
    then have "S \ (f -` box a b) \ sets (lebesgue_on S)"
      by (metis (no_types) box_borel in_borel_measurable_borel inf_sup_aci(1) space_restrict_space that)
    then show ?thesis
      by (simp add: Collect_conj_eq vimage_def)
  qed
  moreover
  have "{x \ S. f x \ T} \ sets (lebesgue_on S)"
       if T: "\a b. {x \ S. f x \ box a b} \ sets (lebesgue_on S)" "open T" for T
  proof -
    obtain \<D> where "countable \<D>" and \<D>: "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = box a b" "\<Union>\<D> = T"
      using open_countable_Union_open_box that \<open>open T\<close> by metis
    then have eq: "{x \ S. f x \ T} = (\U \ \. {x \ S. f x \ U})"
      by blast
    have "{x \ S. f x \ U} \ sets (lebesgue_on S)" if "U \ \" for U
      using that T \<D> by blast
    then show ?thesis
      by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \countable \\])
  qed
  moreover
  have eq: "{x \ S. f x \ i < a} = {x \ S. f x \ {y. y \ i < a}}" for i a
    by auto
  have "f \ borel_measurable (lebesgue_on S)"
    if "\T. open T \ {x \ S. f x \ T} \ sets (lebesgue_on S)"
    by (metis (no_types) eq borel_measurable_vimage_halfspace_component_lt open_halfspace_component_lt that)
  ultimately show "?thesis1" "?thesis2"
    by blast+
qed

lemma borel_measurable_vimage_closed:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  shows "f \ borel_measurable (lebesgue_on S) \
         (\<forall>T. closed T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
        (is "?lhs = ?rhs")
proof -
  have eq: "{x \ S. f x \ T} = S - {x \ S. f x \ (- T)}" for T
    by auto
  show ?thesis
    apply (simp add: borel_measurable_vimage_open, safe)
     apply (simp_all (no_asm) add: eq)
     apply (intro sets.Diff sets_lebesgue_on_refl, force simp: closed_open)
    apply (intro sets.Diff sets_lebesgue_on_refl, force simp: open_closed)
    done
qed

lemma borel_measurable_vimage_closed_interval:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  shows "f \ borel_measurable (lebesgue_on S) \
         (\<forall>a b. {x \<in> S. f x \<in> cbox a b} \<in> sets (lebesgue_on S))"
        (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    using borel_measurable_vimage_closed by blast
next
  assume RHS: ?rhs
  have "{x \ S. f x \ T} \ sets (lebesgue_on S)" if "open T" for T
  proof -
    obtain \<D> where "countable \<D>" and \<D>: "\<D> \<subseteq> Pow T" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = cbox a b" "\<Union>\<D> = T"
      using open_countable_Union_open_cbox that \<open>open T\<close> by metis
    then have eq: "{x \ S. f x \ T} = (\U \ \. {x \ S. f x \ U})"
      by blast
    have "{x \ S. f x \ U} \ sets (lebesgue_on S)" if "U \ \" for U
      using that \<D> by (metis RHS)
    then show ?thesis
      by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \countable \\])
  qed
  then show ?lhs
    by (simp add: borel_measurable_vimage_open)
qed

lemma borel_measurable_vimage_borel:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  shows "f \ borel_measurable (lebesgue_on S) \
         (\<forall>T. T \<in> sets borel \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
        (is "?lhs = ?rhs")
proof
  assume f: ?lhs
  then show ?rhs
    using measurable_sets [OF f]
      by (simp add: Collect_conj_eq inf_sup_aci(1) space_restrict_space vimage_def)
qed (simp add: borel_measurable_vimage_open_interval)

lemma lebesgue_measurable_vimage_borel:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  assumes "f \ borel_measurable lebesgue" "T \ sets borel"
  shows "{x. f x \ T} \ sets lebesgue"
  using assms borel_measurable_vimage_borel [of f UNIV] by auto

lemma borel_measurable_lebesgue_preimage_borel:
  fixes f :: "'a::euclidean_space \ 'b::euclidean_space"
  shows "f \ borel_measurable lebesgue \
         (\<forall>T. T \<in> sets borel \<longrightarrow> {x. f x \<in> T} \<in> sets lebesgue)"
  apply (intro iffI allI impI lebesgue_measurable_vimage_borel)
    apply (auto simp: in_borel_measurable_borel vimage_def)
  done

subsection \<^marker>\<open>tag unimportant\<close> \<open>Measurability of continuous functions\<close>

lemma continuous_imp_measurable_on_sets_lebesgue:
  assumes f: "continuous_on S f" and S: "S \ sets lebesgue"
  shows "f \ borel_measurable (lebesgue_on S)"
proof -
  have "sets (restrict_space borel S) \ sets (lebesgue_on S)"
    by (simp add: mono_restrict_space subsetI)
  then show ?thesis
    by (simp add: borel_measurable_continuous_on_restrict [OF f] borel_measurable_subalgebra
                  space_restrict_space)
qed

lemma id_borel_measurable_lebesgue [iff]: "id \ borel_measurable lebesgue"
  by (simp add: measurable_completion)

lemma id_borel_measurable_lebesgue_on [iff]: "id \ borel_measurable (lebesgue_on S)"
  by (simp add: measurable_completion measurable_restrict_space1)

context
begin

interpretation sigma_finite_measure "interval_measure (\x. x)"
  by (rule sigma_finite_interval_measure) auto
interpretation finite_product_sigma_finite "\_. interval_measure (\x. x)" Basis
  proof qed simp

lemma lborel_eq_real: "lborel = interval_measure (\x. x)"
  unfolding lborel_def Basis_real_def
  using distr_id[of "interval_measure (\x. x)"]
  by (subst distr_component[symmetric])
     (simp_all add: distr_distr comp_def del: distr_id cong: distr_cong)

lemma lborel_eq: "lborel = distr (\\<^sub>M b\Basis. lborel) borel (\f. \b\Basis. f b *\<^sub>R b)"
  by (subst lborel_def) (simp add: lborel_eq_real)

lemma nn_integral_lborel_prod:
  assumes [measurable]: "\b. b \ Basis \ f b \ borel_measurable borel"
  assumes nn[simp]: "\b x. b \ Basis \ 0 \ f b x"
  shows "(\\<^sup>+x. (\b\Basis. f b (x \ b)) \lborel) = (\b\Basis. (\\<^sup>+x. f b x \lborel))"
  by (simp add: lborel_def nn_integral_distr product_nn_integral_prod
                product_nn_integral_singleton)

lemma emeasure_lborel_Icc[simp]:
  fixes l u :: real
  assumes [simp]: "l \ u"
  shows "emeasure lborel {l .. u} = u - l"
proof -
  have "((\f. f 1) -` {l..u} \ space (Pi\<^sub>M {1} (\b. interval_measure (\x. x)))) = {1::real} \\<^sub>E {l..u}"
    by (auto simp: space_PiM)
  then show ?thesis
    by (simp add: lborel_def emeasure_distr emeasure_PiM emeasure_interval_measure_Icc)
qed

lemma emeasure_lborel_Icc_eq: "emeasure lborel {l .. u} = ennreal (if l \ u then u - l else 0)"
  by simp

lemma\<^marker>\<open>tag important\<close> emeasure_lborel_cbox[simp]:
  assumes [simp]: "\b. b \ Basis \ l \ b \ u \ b"
  shows "emeasure lborel (cbox l u) = (\b\Basis. (u - l) \ b)"
proof -
  have "(\x. \b\Basis. indicator {l\b .. u\b} (x \ b) :: ennreal) = indicator (cbox l u)"
    by (auto simp: fun_eq_iff cbox_def split: split_indicator)
  then have "emeasure lborel (cbox l u) = (\\<^sup>+x. (\b\Basis. indicator {l\b .. u\b} (x \ b)) \lborel)"
    by simp
  also have "\ = (\b\Basis. (u - l) \ b)"
    by (subst nn_integral_lborel_prod) (simp_all add: prod_ennreal inner_diff_left)
  finally show ?thesis .
qed

lemma AE_lborel_singleton: "AE x in lborel::'a::euclidean_space measure. x \ c"
  using SOME_Basis AE_discrete_difference [of "{c}" lborel] emeasure_lborel_cbox [of c c]
  by (auto simp add: power_0_left)

lemma emeasure_lborel_Ioo[simp]:
  assumes [simp]: "l \ u"
  shows "emeasure lborel {l <..< u} = ennreal (u - l)"
proof -
  have "emeasure lborel {l <..< u} = emeasure lborel {l .. u}"
    using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto
  then show ?thesis
    by simp
qed

lemma emeasure_lborel_Ioc[simp]:
  assumes [simp]: "l \ u"
  shows "emeasure lborel {l <.. u} = ennreal (u - l)"
proof -
  have "emeasure lborel {l <.. u} = emeasure lborel {l .. u}"
    using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto
  then show ?thesis
    by simp
qed

lemma emeasure_lborel_Ico[simp]:
  assumes [simp]: "l \ u"
  shows "emeasure lborel {l ..< u} = ennreal (u - l)"
proof -
  have "emeasure lborel {l ..< u} = emeasure lborel {l .. u}"
    using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto
  then show ?thesis
    by simp
qed

lemma emeasure_lborel_box[simp]:
  assumes [simp]: "\b. b \ Basis \ l \ b \ u \ b"
  shows "emeasure lborel (box l u) = (\b\Basis. (u - l) \ b)"
proof -
  have "(\x. \b\Basis. indicator {l\b <..< u\b} (x \ b) :: ennreal) = indicator (box l u)"
    by (auto simp: fun_eq_iff box_def split: split_indicator)
  then have "emeasure lborel (box l u) = (\\<^sup>+x. (\b\Basis. indicator {l\b <..< u\b} (x \ b)) \lborel)"
    by simp
  also have "\ = (\b\Basis. (u - l) \ b)"
    by (subst nn_integral_lborel_prod) (simp_all add: prod_ennreal inner_diff_left)
  finally show ?thesis .
qed

lemma emeasure_lborel_cbox_eq:
  "emeasure lborel (cbox l u) = (if \b\Basis. l \ b \ u \ b then \b\Basis. (u - l) \ b else 0)"
  using box_eq_empty(2)[THEN iffD2, of u l] by (auto simp: not_le)

lemma emeasure_lborel_box_eq:
  "emeasure lborel (box l u) = (if \b\Basis. l \ b \ u \ b then \b\Basis. (u - l) \ b else 0)"
  using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force

lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
  using emeasure_lborel_cbox[of x x] nonempty_Basis
  by (auto simp del: emeasure_lborel_cbox nonempty_Basis)

lemma emeasure_lborel_cbox_finite: "emeasure lborel (cbox a b) < \"
  by (auto simp: emeasure_lborel_cbox_eq)

lemma emeasure_lborel_box_finite: "emeasure lborel (box a b) < \"
  by (auto simp: emeasure_lborel_box_eq)

lemma emeasure_lborel_ball_finite: "emeasure lborel (ball c r) < \"
proof -
  have "bounded (ball c r)" by simp
  from bounded_subset_cbox_symmetric[OF this] obtain a where a: "ball c r \ cbox (-a) a"
    by auto
  hence "emeasure lborel (ball c r) \ emeasure lborel (cbox (-a) a)"
    by (intro emeasure_mono) auto
  also have "\ < \" by (simp add: emeasure_lborel_cbox_eq)
  finally show ?thesis .
qed

lemma emeasure_lborel_cball_finite: "emeasure lborel (cball c r) < \"
proof -
  have "bounded (cball c r)" by simp
  from bounded_subset_cbox_symmetric[OF this] obtain a where a: "cball c r \ cbox (-a) a"
    by auto
  hence "emeasure lborel (cball c r) \ emeasure lborel (cbox (-a) a)"
    by (intro emeasure_mono) auto
  also have "\ < \" by (simp add: emeasure_lborel_cbox_eq)
  finally show ?thesis .
qed

lemma fmeasurable_cbox [iff]: "cbox a b \ fmeasurable lborel"
  and fmeasurable_box [iff]: "box a b \ fmeasurable lborel"
  by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq)

lemma
  fixes l u :: real
  assumes [simp]: "l \ u"
  shows measure_lborel_Icc[simp]: "measure lborel {l .. u} = u - l"
    and measure_lborel_Ico[simp]: "measure lborel {l ..< u} = u - l"
    and measure_lborel_Ioc[simp]: "measure lborel {l <.. u} = u - l"
    and measure_lborel_Ioo[simp]: "measure lborel {l <..< u} = u - l"
  by (simp_all add: measure_def)

lemma
  assumes [simp]: "\b. b \ Basis \ l \ b \ u \ b"
  shows measure_lborel_box[simp]: "measure lborel (box l u) = (\b\Basis. (u - l) \ b)"
    and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\b\Basis. (u - l) \ b)"
  by (simp_all add: measure_def inner_diff_left prod_nonneg)

lemma measure_lborel_cbox_eq:
  "measure lborel (cbox l u) = (if \b\Basis. l \ b \ u \ b then \b\Basis. (u - l) \ b else 0)"
  using box_eq_empty(2)[THEN iffD2, of u l] by (auto simp: not_le)

lemma measure_lborel_box_eq:
  "measure lborel (box l u) = (if \b\Basis. l \ b \ u \ b then \b\Basis. (u - l) \ b else 0)"
  using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force

lemma measure_lborel_singleton[simp]: "measure lborel {x} = 0"
  by (simp add: measure_def)

lemma sigma_finite_lborel: "sigma_finite_measure lborel"
proof
  show "\A::'a set set. countable A \ A \ sets lborel \ \A = space lborel \ (\a\A. emeasure lborel a \ \)"
    by (intro exI[of _ "range (\n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One))"])
       (auto simp: emeasure_lborel_cbox_eq UN_box_eq_UNIV)
qed

end

lemma emeasure_lborel_UNIV [simp]: "emeasure lborel (UNIV::'a::euclidean_space set) = \"
proof -
  { fix n::nat
    let ?Ba = "Basis :: 'a set"
    have "real n \ (2::real) ^ card ?Ba * real n"
      by (simp add: mult_le_cancel_right1)
    also
    have "... \ (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba"
      apply (rule mult_left_mono)
      apply (metis DIM_positive One_nat_def less_eq_Suc_le less_imp_le of_nat_le_iff of_nat_power self_le_power zero_less_Suc)
      apply (simp)
      done
    finally have "real n \ (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" .
  } note [intro!] = this
  show ?thesis
    unfolding UN_box_eq_UNIV[symmetric]
    apply (subst SUP_emeasure_incseq[symmetric])
    apply (auto simp: incseq_def subset_box inner_add_left
      simp del: Sup_eq_top_iff SUP_eq_top_iff
      intro!: ennreal_SUP_eq_top)
    done
qed

lemma emeasure_lborel_countable:
  fixes A :: "'a::euclidean_space set"
  assumes "countable A"
  shows "emeasure lborel A = 0"
proof -
  have "A \ (\i. {from_nat_into A i})" using from_nat_into_surj assms by force
  then have "emeasure lborel A \ emeasure lborel (\i. {from_nat_into A i})"
    by (intro emeasure_mono) auto
  also have "emeasure lborel (\i. {from_nat_into A i}) = 0"
    by (rule emeasure_UN_eq_0) auto
  finally show ?thesis
    by (auto simp add: )
qed

lemma countable_imp_null_set_lborel: "countable A \ A \ null_sets lborel"
  by (simp add: null_sets_def emeasure_lborel_countable sets.countable)

lemma finite_imp_null_set_lborel: "finite A \ A \ null_sets lborel"
  by (intro countable_imp_null_set_lborel countable_finite)

lemma insert_null_sets_iff [simp]: "insert a N \ null_sets lebesgue \ N \ null_sets lebesgue"
    (is "?lhs = ?rhs")
proof
  assume ?lhs then show ?rhs
    by (meson completion.complete2 subset_insertI)
next
  assume ?rhs then show ?lhs
  by (simp add: null_sets.insert_in_sets null_setsI)
qed

lemma insert_null_sets_lebesgue_on_iff [simp]:
  assumes "a \ S" "S \ sets lebesgue"
  shows "insert a N \ null_sets (lebesgue_on S) \ N \ null_sets (lebesgue_on S)"
  by (simp add: assms null_sets_restrict_space)

lemma lborel_neq_count_space[simp]: "lborel \ count_space (A::('a::ordered_euclidean_space) set)"
proof
  assume asm: "lborel = count_space A"
  have "space lborel = UNIV" by simp
  hence [simp]: "A = UNIV" by (subst (asm) asm) (simp only: space_count_space)
  have "emeasure lborel {undefined::'a} = 1"
      by (subst asm, subst emeasure_count_space_finite) auto
  moreover have "emeasure lborel {undefined} \ 1" by simp
  ultimately show False by contradiction
qed

lemma mem_closed_if_AE_lebesgue_open:
  assumes "open S" "closed C"
  assumes "AE x \ S in lebesgue. x \ C"
  assumes "x \ S"
  shows "x \ C"
proof (rule ccontr)
  assume xC: "x \ C"
  with openE[of "S - C"] assms
  obtain e where e: "0 < e" "ball x e \ S - C"
    by blast
  then obtain a b where box: "x \ box a b" "box a b \ S - C"
    by (metis rational_boxes order_trans)
  then have "0 < emeasure lebesgue (box a b)"
    by (auto simp: emeasure_lborel_box_eq mem_box algebra_simps intro!: prod_pos)
  also have "\ \ emeasure lebesgue (S - C)"
    using assms box
    by (auto intro!: emeasure_mono)
  also have "\ = 0"
    using assms
    by (auto simp: eventually_ae_filter completion.complete2 set_diff_eq null_setsD1)
  finally show False by simp
qed

lemma mem_closed_if_AE_lebesgue: "closed C \ (AE x in lebesgue. x \ C) \ x \ C"
  using mem_closed_if_AE_lebesgue_open[OF open_UNIV] by simp

subsection \<open>Affine transformation on the Lebesgue-Borel\<close>

lemma\<^marker>\<open>tag important\<close> lborel_eqI:
  fixes M :: "'a::euclidean_space measure"
  assumes emeasure_eq: "\l u. (\b. b \ Basis \ l \ b \ u \ b) \ emeasure M (box l u) = (\b\Basis. (u - l) \ b)"
  assumes sets_eq: "sets M = sets borel"
  shows "lborel = M"
proof (rule measure_eqI_generator_eq)
  let ?E = "range (\(a, b). box a b::'a set)"
  show "Int_stable ?E"
    by (auto simp: Int_stable_def box_Int_box)

  show "?E \ Pow UNIV" "sets lborel = sigma_sets UNIV ?E" "sets M = sigma_sets UNIV ?E"
    by (simp_all add: borel_eq_box sets_eq)

  let ?A = "\n::nat. box (- (real n *\<^sub>R One)) (real n *\<^sub>R One) :: 'a set"
  show "range ?A \ ?E" "(\i. ?A i) = UNIV"
    unfolding UN_box_eq_UNIV by auto

  { fix i show "emeasure lborel (?A i) \ \" by auto }
  { fix X assume "X \ ?E" then show "emeasure lborel X = emeasure M X"
      apply (auto simp: emeasure_eq emeasure_lborel_box_eq)
      apply (subst box_eq_empty(1)[THEN iffD2])
      apply (auto intro: less_imp_le simp: not_le)
      done }
qed

lemma\<^marker>\<open>tag important\<close> lborel_affine_euclidean:
  fixes c :: "'a::euclidean_space \ real" and t
  defines "T x \ t + (\j\Basis. (c j * (x \ j)) *\<^sub>R j)"
  assumes c: "\j. j \ Basis \ c j \ 0"
  shows "lborel = density (distr lborel borel T) (\_. (\j\Basis. \c j\))" (is "_ = ?D")
proof (rule lborel_eqI)
  let ?B = "Basis :: 'a set"
  fix l u assume le: "\b. b \ ?B \ l \ b \ u \ b"
  have [measurable]: "T \ borel \\<^sub>M borel"
    by (simp add: T_def[abs_def])
  have eq: "T -` box l u = box
    (\<Sum>j\<in>Basis. (((if 0 < c j then l - t else u - t) \<bullet> j) / c j) *\<^sub>R j)
    (\<Sum>j\<in>Basis. (((if 0 < c j then u - t else l - t) \<bullet> j) / c j) *\<^sub>R j)"
    using c by (auto simp: box_def T_def field_simps inner_simps divide_less_eq)
  with le c show "emeasure ?D (box l u) = (\b\?B. (u - l) \ b)"
    by (auto simp: emeasure_density emeasure_distr nn_integral_multc emeasure_lborel_box_eq inner_simps
                   field_split_simps ennreal_mult'[symmetric] prod_nonneg prod.distrib[symmetric]
             intro!: prod.cong)
qed simp

lemma lborel_affine:
  fixes t :: "'a::euclidean_space"
  shows "c \ 0 \ lborel = density (distr lborel borel (\x. t + c *\<^sub>R x)) (\_. \c\^DIM('a))"
  using lborel_affine_euclidean[where c="\_::'a. c" and t=t]
  unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric] euclidean_representation prod_constant by simp

lemma lborel_real_affine:
  "c \ 0 \ lborel = density (distr lborel borel (\x. t + c * x)) (\_. ennreal (abs c))"
  using lborel_affine[of c t] by simp

lemma AE_borel_affine:
  fixes P :: "real \ bool"
  shows "c \ 0 \ Measurable.pred borel P \ AE x in lborel. P x \ AE x in lborel. P (t + c * x)"
  by (subst lborel_real_affine[where t="- t / c" and c="1 / c"])
     (simp_all add: AE_density AE_distr_iff field_simps)

lemma nn_integral_real_affine:
  fixes c :: real assumes [measurable]: "f \ borel_measurable borel" and c: "c \ 0"
  shows "(\\<^sup>+x. f x \lborel) = \c\ * (\\<^sup>+x. f (t + c * x) \lborel)"
  by (subst lborel_real_affine[OF c, of t])
     (simp add: nn_integral_density nn_integral_distr nn_integral_cmult)

lemma lborel_integrable_real_affine:
  fixes f :: "real \ 'a :: {banach, second_countable_topology}"
  assumes f: "integrable lborel f"
  shows "c \ 0 \ integrable lborel (\x. f (t + c * x))"
  using f f[THEN borel_measurable_integrable] unfolding integrable_iff_bounded
  by (subst (asm) nn_integral_real_affine[where c=c and t=t]) (auto simp: ennreal_mult_less_top)

lemma lborel_integrable_real_affine_iff:
  fixes f :: "real \ 'a :: {banach, second_countable_topology}"
  shows "c \ 0 \ integrable lborel (\x. f (t + c * x)) \ integrable lborel f"
  using
    lborel_integrable_real_affine[of f c t]
    lborel_integrable_real_affine[of "\x. f (t + c * x)" "1/c" "-t/c"]
  by (auto simp add: field_simps)

lemma\<^marker>\<open>tag important\<close> lborel_integral_real_affine:
  fixes f :: "real \ 'a :: {banach, second_countable_topology}" and c :: real
  assumes c: "c \ 0" shows "(\x. f x \ lborel) = \c\ *\<^sub>R (\x. f (t + c * x) \lborel)"
proof cases
  assume f[measurable]: "integrable lborel f" then show ?thesis
    using c f f[THEN borel_measurable_integrable] f[THEN lborel_integrable_real_affine, of c t]
    by (subst lborel_real_affine[OF c, of t])
       (simp add: integral_density integral_distr)
next
  assume "\ integrable lborel f" with c show ?thesis
    by (simp add: lborel_integrable_real_affine_iff not_integrable_integral_eq)
qed

lemma
  fixes c :: "'a::euclidean_space \ real" and t
  assumes c: "\j. j \ Basis \ c j \ 0"
  defines "T == (\x. t + (\j\Basis. (c j * (x \ j)) *\<^sub>R j))"
  shows lebesgue_affine_euclidean: "lebesgue = density (distr lebesgue lebesgue T) (\_. (\j\Basis. \c j\))" (is "_ = ?D")
    and lebesgue_affine_measurable: "T \ lebesgue \\<^sub>M lebesgue"
proof -
  have T_borel[measurable]: "T \ borel \\<^sub>M borel"
    by (auto simp: T_def[abs_def])
  { fix A :: "'a set" assume A: "A \ sets borel"
    then have "emeasure lborel A = 0 \ emeasure (density (distr lborel borel T) (\_. (\j\Basis. \c j\))) A = 0"
      unfolding T_def using c by (subst lborel_affine_euclidean[symmetric]) auto
    also have "\ \ emeasure (distr lebesgue lborel T) A = 0"
      using A c by (simp add: distr_completion emeasure_density nn_integral_cmult prod_nonneg cong: distr_cong)
    finally have "emeasure lborel A = 0 \ emeasure (distr lebesgue lborel T) A = 0" . }
  then have eq: "null_sets lborel = null_sets (distr lebesgue lborel T)"
    by (auto simp: null_sets_def)

  show "T \ lebesgue \\<^sub>M lebesgue"
    by (rule completion.measurable_completion2) (auto simp: eq measurable_completion)

  have "lebesgue = completion (density (distr lborel borel T) (\_. (\j\Basis. \c j\)))"
    using c by (subst lborel_affine_euclidean[of c t]) (simp_all add: T_def[abs_def])
  also have "\ = density (completion (distr lebesgue lborel T)) (\_. (\j\Basis. \c j\))"
    using c by (auto intro!: always_eventually prod_pos completion_density_eq simp: distr_completion cong: distr_cong)
  also have "\ = density (distr lebesgue lebesgue T) (\_. (\j\Basis. \c j\))"
    by (subst completion.completion_distr_eq) (auto simp: eq measurable_completion)
  finally show "lebesgue = density (distr lebesgue lebesgue T) (\_. (\j\Basis. \c j\))" .
qed

corollary lebesgue_real_affine:
  "c \ 0 \ lebesgue = density (distr lebesgue lebesgue (\x. t + c * x)) (\_. ennreal (abs c))"
    using lebesgue_affine_euclidean [where c= "\x::real. c"] by simp

lemma nn_integral_real_affine_lebesgue:
  fixes c :: real assumes f[measurable]: "f \ borel_measurable lebesgue" and c: "c \ 0"
  shows "(\\<^sup>+x. f x \lebesgue) = ennreal\c\ * (\\<^sup>+x. f(t + c * x) \lebesgue)"
proof -
  have "(\\<^sup>+x. f x \lebesgue) = (\\<^sup>+x. f x \density (distr lebesgue lebesgue (\x. t + c * x)) (\x. ennreal \c\))"
    using lebesgue_real_affine c by auto
  also have "\ = \\<^sup>+ x. ennreal \c\ * f x \distr lebesgue lebesgue (\x. t + c * x)"
    by (subst nn_integral_density) auto
  also have "\ = ennreal \c\ * integral\<^sup>N (distr lebesgue lebesgue (\x. t + c * x)) f"
    using f measurable_distr_eq1 nn_integral_cmult by blast
  also have "\ = \c\ * (\\<^sup>+x. f(t + c * x) \lebesgue)"
    using lebesgue_affine_measurable[where c= "\x::real. c"]
    by (subst nn_integral_distr) (force+)
  finally show ?thesis .
qed

lemma lebesgue_measurable_scaling[measurable]: "(*\<^sub>R) x \ lebesgue \\<^sub>M lebesgue"
proof cases
  assume "x = 0"
  then have "(*\<^sub>R) x = (\x. 0::'a)"
    by (auto simp: fun_eq_iff)
  then show ?thesis by auto
next
  assume "x \ 0" then show ?thesis
    using lebesgue_affine_measurable[of "\_. x" 0]
    unfolding scaleR_scaleR[symmetric] scaleR_sum_right[symmetric] euclidean_representation
    by (auto simp add: ac_simps)
qed

lemma
  fixes m :: real and \<delta> :: "'a::euclidean_space"
  defines "T r d x \ r *\<^sub>R x + d"
  shows emeasure_lebesgue_affine: "emeasure lebesgue (T m \ ` S) = \m\ ^ DIM('a) * emeasure lebesgue S" (is ?e)
    and measure_lebesgue_affine: "measure lebesgue (T m \ ` S) = \m\ ^ DIM('a) * measure lebesgue S" (is ?m)
proof -
  show ?e
  proof cases
    assume "m = 0" then show ?thesis
      by (simp add: image_constant_conv T_def[abs_def])
  next
    let ?T = "T m \" and ?T' = "T (1 / m) (- ((1/m) *\<^sub>R \))"
    assume "m \ 0"
    then have s_comp_s: "?T' \ ?T = id" "?T \ ?T' = id"
      by (auto simp: T_def[abs_def] fun_eq_iff scaleR_add_right scaleR_diff_right)
    then have "inv ?T' = ?T" "bij ?T'"
      by (auto intro: inv_unique_comp o_bij)
    then have eq: "T m \ ` S = T (1 / m) ((-1/m) *\<^sub>R \) -` S \ space lebesgue"
      using bij_vimage_eq_inv_image[OF \<open>bij ?T'\<close>, of S] by auto

    have trans_eq_T: "(\x. \ + (\j\Basis. (m * (x \ j)) *\<^sub>R j)) = T m \" for m \
      unfolding T_def[abs_def] scaleR_scaleR[symmetric] scaleR_sum_right[symmetric]
      by (auto simp add: euclidean_representation ac_simps)

    have T[measurable]: "T r d \ lebesgue \\<^sub>M lebesgue" for r d
      using lebesgue_affine_measurable[of "\_. r" d]
      by (cases "r = 0") (auto simp: trans_eq_T T_def[abs_def])

    show ?thesis
    proof cases
      assume "S \ sets lebesgue" with \m \ 0\ show ?thesis
        unfolding eq
        apply (subst lebesgue_affine_euclidean[of "\_. m" \])
        apply (simp_all add: emeasure_density trans_eq_T nn_integral_cmult emeasure_distr
                        del: space_completion emeasure_completion)
        apply (simp add: vimage_comp s_comp_s)
        done
    next
      assume "S \ sets lebesgue"
      moreover have "?T ` S \ sets lebesgue"
      proof
        assume "?T ` S \ sets lebesgue"
        then have "?T -` (?T ` S) \ space lebesgue \ sets lebesgue"
          by (rule measurable_sets[OF T])
        also have "?T -` (?T ` S) \ space lebesgue = S"
          by (simp add: vimage_comp s_comp_s eq)
        finally show False using \<open>S \<notin> sets lebesgue\<close> by auto
      qed
      ultimately show ?thesis
        by (simp add: emeasure_notin_sets)
    qed
  qed
  show ?m
    unfolding measure_def \<open>?e\<close> by (simp add: enn2real_mult prod_nonneg)
qed

lemma lebesgue_real_scale:
  assumes "c \ 0"
  shows   "lebesgue = density (distr lebesgue lebesgue (\x. c * x)) (\x. ennreal \c\)"
  using assms by (subst lebesgue_affine_euclidean[of "\_. c" 0]) simp_all

lemma divideR_right:
  fixes x y :: "'a::real_normed_vector"
  shows "r \ 0 \ y = x /\<^sub>R r \ r *\<^sub>R y = x"
  using scaleR_cancel_left[of r y "x /\<^sub>R r"] by simp

lemma lborel_has_bochner_integral_real_affine_iff:
  fixes x :: "'a :: {banach, second_countable_topology}"
  shows "c \ 0 \
    has_bochner_integral lborel f x \<longleftrightarrow>
    has_bochner_integral lborel (\<lambda>x. f (t + c * x)) (x /\<^sub>R \<bar>c\<bar>)"
  unfolding has_bochner_integral_iff lborel_integrable_real_affine_iff
  by (simp_all add: lborel_integral_real_affine[symmetric] divideR_right cong: conj_cong)

lemma lborel_distr_uminus: "distr lborel borel uminus = (lborel :: real measure)"
  by (subst lborel_real_affine[of "-1" 0])
     (auto simp: density_1 one_ennreal_def[symmetric])

lemma lborel_distr_mult:
  assumes "(c::real) \ 0"
  shows "distr lborel borel ((*) c) = density lborel (\_. inverse \c\)"
proof-
  have "distr lborel borel ((*) c) = distr lborel lborel ((*) c)" by (simp cong: distr_cong)
  also from assms have "... = density lborel (\_. inverse \c\)"
    by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr)
  finally show ?thesis .
qed

lemma lborel_distr_mult':
  assumes "(c::real) \ 0"
  shows "lborel = density (distr lborel borel ((*) c)) (\_. \c\)"
proof-
  have "lborel = density lborel (\_. 1)" by (rule density_1[symmetric])
  also from assms have "(\_. 1 :: ennreal) = (\_. inverse \c\ * \c\)" by (intro ext) simp
  also have "density lborel ... = density (density lborel (\_. inverse \c\)) (\_. \c\)"
    by (subst density_density_eq) (auto simp: ennreal_mult)
  also from assms have "density lborel (\_. inverse \c\) = distr lborel borel ((*) c)"
    by (rule lborel_distr_mult[symmetric])
  finally show ?thesis .
qed

lemma lborel_distr_plus:
  fixes c :: "'a::euclidean_space"
  shows "distr lborel borel ((+) c) = lborel"
by (subst lborel_affine[of 1 c], auto simp: density_1)

interpretation lborel: sigma_finite_measure lborel
  by (rule sigma_finite_lborel)

interpretation lborel_pair: pair_sigma_finite lborel lborel ..

lemma\<^marker>\<open>tag important\<close> lborel_prod:
  "lborel \\<^sub>M lborel = (lborel :: ('a::euclidean_space \ 'b::euclidean_space) measure)"
proof (rule lborel_eqI[symmetric], clarify)
  fix la ua :: 'a and lb ub :: 'b
  assume lu: "\a b. (a, b) \ Basis \ (la, lb) \ (a, b) \ (ua, ub) \ (a, b)"
  have [simp]:
    "\b. b \ Basis \ la \ b \ ua \ b"
    "\b. b \ Basis \ lb \ b \ ub \ b"
    "inj_on (\u. (u, 0)) Basis" "inj_on (\u. (0, u)) Basis"
    "(\u. (u, 0)) ` Basis \ (\u. (0, u)) ` Basis = {}"
    "box (la, lb) (ua, ub) = box la ua \ box lb ub"
    using lu[of _ 0] lu[of 0] by (auto intro!: inj_onI simp add: Basis_prod_def ball_Un box_def)
  show "emeasure (lborel \\<^sub>M lborel) (box (la, lb) (ua, ub)) =
      ennreal (prod ((\<bullet>) ((ua, ub) - (la, lb))) Basis)"
    by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def prod.union_disjoint
                  prod.reindex ennreal_mult inner_diff_left prod_nonneg)
qed (simp add: borel_prod[symmetric])

(* FIXME: conversion in measurable prover *)
lemma lborelD_Collect[measurable (raw)]: "{x\space borel. P x} \ sets borel \ {x\space lborel. P x} \ sets lborel"
  by simp

lemma lborelD[measurable (raw)]: "A \ sets borel \ A \ sets lborel"
  by simp

lemma emeasure_bounded_finite:
  assumes "bounded A" shows "emeasure lborel A < \"
proof -
  obtain a b where "A \ cbox a b"
    by (meson bounded_subset_cbox_symmetric \<open>bounded A\<close>)
  then have "emeasure lborel A \ emeasure lborel (cbox a b)"
    by (intro emeasure_mono) auto
  then show ?thesis
    by (auto simp: emeasure_lborel_cbox_eq prod_nonneg less_top[symmetric] top_unique split: if_split_asm)
qed

lemma emeasure_compact_finite: "compact A \ emeasure lborel A < \"
  using emeasure_bounded_finite[of A] by (auto intro: compact_imp_bounded)

lemma borel_integrable_compact:
  fixes f :: "'a::euclidean_space \ 'b::{banach, second_countable_topology}"
  assumes "compact S" "continuous_on S f"
  shows "integrable lborel (\x. indicator S x *\<^sub>R f x)"
proof cases
  assume "S \ {}"
  have "continuous_on S (\x. norm (f x))"
    using assms by (intro continuous_intros)
  from continuous_attains_sup[OF \<open>compact S\<close> \<open>S \<noteq> {}\<close> this]
  obtain M where M: "\x. x \ S \ norm (f x) \ M"
    by auto
  show ?thesis
  proof (rule integrable_bound)
    show "integrable lborel (\x. indicator S x * M)"
      using assms by (auto intro!: emeasure_compact_finite borel_compact integrable_mult_left)
    show "(\x. indicator S x *\<^sub>R f x) \ borel_measurable lborel"
      using assms by (auto intro!: borel_measurable_continuous_on_indicator borel_compact)
    show "AE x in lborel. norm (indicator S x *\<^sub>R f x) \ norm (indicator S x * M)"
      by (auto split: split_indicator simp: abs_real_def dest!: M)
  qed
qed simp

lemma borel_integrable_atLeastAtMost:
  fixes f :: "real \ real"
  assumes f: "\x. a \ x \ x \ b \ isCont f x"
  shows "integrable lborel (\x. f x * indicator {a .. b} x)" (is "integrable _ ?f")
proof -
  have "integrable lborel (\x. indicator {a .. b} x *\<^sub>R f x)"
  proof (rule borel_integrable_compact)
    from f show "continuous_on {a..b} f"
      by (auto intro: continuous_at_imp_continuous_on)
  qed simp
  then show ?thesis
    by (auto simp: mult.commute)
qed

subsection \<open>Lebesgue measurable sets\<close>

abbreviation\<^marker>\<open>tag important\<close> lmeasurable :: "'a::euclidean_space set set"
where
  "lmeasurable \ fmeasurable lebesgue"

lemma not_measurable_UNIV [simp]: "UNIV \ lmeasurable"
  by (simp add: fmeasurable_def)

lemma\<^marker>\<open>tag important\<close> lmeasurable_iff_integrable:
  "S \ lmeasurable \ integrable lebesgue (indicator S :: 'a::euclidean_space \ real)"
  by (auto simp: fmeasurable_def integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator)

lemma lmeasurable_cbox [iff]: "cbox a b \ lmeasurable"
  and lmeasurable_box [iff]: "box a b \ lmeasurable"
  by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq)

lemma
  fixes a::real
  shows lmeasurable_interval [iff]: "{a..b} \ lmeasurable" "{a<.. lmeasurable"
  apply (metis box_real(2) lmeasurable_cbox)
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.71 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.