Quelle Lebesgue_Measure.thy Sprache: 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 (simp add: subset_eq Ball_def Bex_def)
            by (metis order_le_less_trans order_less_le_trans order_less_not_sym)
          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 *: "?S1 \ ?S2 = {}"
            using j by (fastforce simp add: disjoint_iff)
          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) by (simp add: * sum.union_disjoint disjoint_iff_not_equal)
          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"]
      then have "\d>0. F (r i + d) - F (r i) < epsilon / 2 ^ (i + 2)"
        by (simp add: continuous_at_right_real_increasing egt0)
      thus "\d>0. F (r i + d) < F (r i) + epsilon / 2^(i+2)"
        by force
    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"
      using right_cont_F [of a]
      by (metis continuous_at_right_real_increasing egt0 half_gt_zero less_add_same_cancel1 mono_F)
    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<..
        by (intro UN_mono; simp add: add.commute add_strict_increasing deltai_gt0 subset_iff)
      finally show "{a'..b} \ (\i \ S'. {l i<..
    qed
    with S'_def have Sprop2: "\i. i \ S \ l i < r i" by auto
    obtain n where Sbound: "\i. i \ S \ i \ n"
      using Max_ge finS by blast
    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"
    proof -
      have "F b - F a' \ (\i\S. F (r i + delta i) - F (l i))"
        using claim2 l_r Sprop by (simp add: deltai_gt0 finS add.commute add_strict_increasing)
      also have "... \ (\i \ S. F(r i) - F(l i) + epsilon / 2^(i+2))"
        by (smt (verit) sum_mono deltai_prop)
      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)"
        using egt0 Sbound by (intro add_left_mono mult_left_mono sum_mono2) force+
      also have "... \ ?t + (epsilon / 2)"
        using egt0 by (simp add: geometric_sum add_left_mono mult_left_mono)
      finally have "F b - F a' \ (\i\S. F (r i) - F (l i)) + epsilon / 2"
        by simp
      then show ?thesis
        by linarith
    qed
    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 image_def split: prod.split)
  by (metis greaterThanAtMost_empty nle_le)

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 X: "\n. X n < a" "incseq X" "X \ a"
    then have "emeasure (interval_measure F) {X n<..b} \ \" for n
      by (smt (verit) "*" \<open>a \<le> b\<close> ennreal_neq_top infinity_ennreal_def)
    with X have "(\n. emeasure ?F {X n<..b}) \ emeasure ?F (\n. {X n <..b})"
      by (intro Lim_emeasure_decseq; force simp: decseq_def incseq_def emeasure_interval_measure_Ioc *)
    also have "(\n. {X n <..b}) = {a..b}"
      apply auto
      apply (rule LIMSEQ_le_const2[OF \<open>X \<longlonglongrightarrow> a\<close>])
      using less_eq_real_def apply presburger
      using X(1) order_less_le_trans by blast
    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"
  by (simp add: emeasure_restrict_space measure_eqI)

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 by (smt (verit) measurable_lebesgue_cong measurable_restrict_space1)

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))"
  by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_less])

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))"
  by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_ge])

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))"
  by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_greater])

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))"
  by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_le])

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))"
proof -
  have eq: "{x \ S. f x \ T} = S - (S \ f -` (- T))" for T
    by auto
  show ?thesis
    unfolding borel_measurable_vimage_open eq
    by (metis Diff_Diff_Int closed_Compl diff_eq open_Compl sets.Diff sets_lebesgue_on_refl vimage_Compl)
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)"
  by (smt (verit, best) Collect_cong UNIV_I borel_measurable_vimage_borel lebesgue_on_UNIV_eq)

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)"
  by (metis borel_measurable_continuous_on_restrict borel_measurable_subalgebra f
      lebesgue_on_UNIV_eq mono_restrict_space sets_completionI_sets sets_lborel space_borel
      space_lebesgue_on space_restrict_space subsetI)

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"
  by (simp add: emeasure_interval_measure_Icc lborel_eq_real)

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)"
  by (simp add: emeasure_interval_measure_Ioc lborel_eq_real)

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) < \"
  by (metis bounded_ball bounded_subset_cbox_symmetric cbox_borel emeasure_lborel_cbox_finite
      emeasure_mono order_le_less_trans sets_lborel)

lemma emeasure_lborel_cball_finite: "emeasure lborel (cball c r) < \"
  by (metis bounded_cball bounded_subset_cbox_symmetric cbox_borel emeasure_lborel_cbox_finite
            emeasure_mono order_le_less_trans sets_lborel)

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 simp
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"
  by (meson completion.complete2 finite.simps finite_imp_null_set_lborel null_sets.insert_in_sets
      null_sets_completionI subset_insertI)

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]:
  fixes A :: "('a::ordered_euclidean_space) set"
  shows "lborel \ count_space A"
  by (metis finite.simps finite_imp_null_set_lborel insert_not_empty null_sets_count_space singleton_iff)

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
  show "emeasure lborel (?A i) \ \" for i by auto
  show "emeasure lborel X = emeasure M X" if "X \ ?E" for X
    using that box_eq_empty(1) by (fastforce simp: emeasure_eq emeasure_lborel_box_eq)
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 (simp add: completion.measurable_completion2 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 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"
  by (metis box_real lmeasurable_box lmeasurable_cbox)+

lemma fmeasurable_compact: "compact S \ S \ fmeasurable lborel"
  using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact)

lemma lmeasurable_compact: "compact S \ S \ lmeasurable"
  using fmeasurable_compact by (force simp: fmeasurable_def)

lemma measure_frontier:
   "bounded S \ measure lebesgue (frontier S) = measure lebesgue (closure S) - measure lebesgue (interior S)"
  using closure_subset interior_subset
  by (auto simp: frontier_def fmeasurable_compact intro!: measurable_measure_Diff)

lemma lmeasurable_closure:
   "bounded S \ closure S \ lmeasurable"
  by (simp add: lmeasurable_compact)

lemma lmeasurable_frontier:
   "bounded S \ frontier S \ lmeasurable"
  by (simp add: compact_frontier_bounded lmeasurable_compact)

lemma lmeasurable_open: "bounded S \ open S \ S \ lmeasurable"
  using emeasure_bounded_finite[of S] by (intro fmeasurableI) (auto simp: borel_open)

lemma lmeasurable_ball [simp]: "ball a r \ lmeasurable"
  by (simp add: lmeasurable_open)

lemma lmeasurable_cball [simp]: "cball a r \ lmeasurable"
  by (simp add: lmeasurable_compact)

lemma lmeasurable_interior: "bounded S \ interior S \ lmeasurable"
  by (simp add: bounded_interior lmeasurable_open)

lemma null_sets_cbox_Diff_box: "cbox a b - box a b \ null_sets lborel"
  by (simp add: emeasure_Diff emeasure_lborel_box_eq emeasure_lborel_cbox_eq null_setsI subset_box)

lemma bounded_set_imp_lmeasurable:
  assumes "bounded S" "S \ sets lebesgue" shows "S \ lmeasurable"
  by (metis assms bounded_Un emeasure_bounded_finite emeasure_completion fmeasurableI main_part_null_part_Un)

lemma finite_measure_lebesgue_on: "S \ lmeasurable \ finite_measure (lebesgue_on S)"
  by (auto simp: finite_measureI fmeasurable_def emeasure_restrict_space)

lemma integrable_const_ivl [iff]:
  fixes a::"'a::ordered_euclidean_space"
  shows "integrable (lebesgue_on {a..b}) (\x. c)"
  by (metis cbox_interval finite_measure.integrable_const finite_measure_lebesgue_on lmeasurable_cbox)

subsection\<^marker>\<open>tag unimportant\<close>\<open>Translation preserves Lebesgue measure\<close>

lemma sigma_sets_image:
  assumes S: "S \ sigma_sets \ M" and "M \ Pow \" "f ` \ = \" "inj_on f \"
    and M: "\y. y \ M \ f ` y \ M"
  shows "(f ` S) \ sigma_sets \ M"
  using S
proof (induct S rule: sigma_sets.induct)
  case (Basic a) then show ?case
    by (simp add: M)
next
  case Empty then show ?case
    by (simp add: sigma_sets.Empty)
next
  case (Compl a)
  with assms show ?case
    by (metis inj_on_image_set_diff sigma_sets.Compl sigma_sets_into_sp)
next
  case (Union a) then show ?case
    by (metis image_UN sigma_sets.simps)
qed

lemma null_sets_translation:
  assumes "N \ null_sets lborel" shows "{x. x - a \ N} \ null_sets lborel"
proof -
--> --------------------

--> maximum size reached

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

quality94%

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

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.