# HG changeset patch
# User hoelzl
# Date 1475150097 -7200
# Node ID 02de4a58e210ec0209b272749de9672dd668d32f
# Parent  c3da799b1b456d7b07983130082270726143e3e5
HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure

diff -r c3da799b1b45 -r 02de4a58e210 src/HOL/Analysis/Complete_Measure.thy
--- a/src/HOL/Analysis/Complete_Measure.thy	Thu Sep 29 13:02:43 2016 +0200
+++ b/src/HOL/Analysis/Complete_Measure.thy	Thu Sep 29 13:54:57 2016 +0200
@@ -85,6 +85,9 @@
   "A \<in> sets M \<Longrightarrow> A \<in> sets (completion M)"
   unfolding sets_completion by force
 
+lemma measurable_completion: "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> f \<in> completion M \<rightarrow>\<^sub>M N"
+  by (auto simp: measurable_def)
+
 lemma null_sets_completion:
   assumes "N' \<in> null_sets M" "N \<subseteq> N'" shows "N \<in> sets (completion M)"
   using assms by (intro sets_completionI[of N "{}" N N']) auto
@@ -305,9 +308,6 @@
 lemma null_sets_completion_iff: "N \<in> sets M \<Longrightarrow> N \<in> null_sets (completion M) \<longleftrightarrow> N \<in> null_sets M"
   by (auto simp: null_sets_def)
 
-lemma AE_completion_iff: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in completion M. P x)"
-  by (simp add: AE_iff_null null_sets_completion_iff)
-
 lemma sets_completion_AE: "(AE x in M. \<not> P x) \<Longrightarrow> Measurable.pred (completion M) P"
   unfolding pred_def sets_completion eventually_ae_filter
   by auto
@@ -339,6 +339,12 @@
   "B \<subseteq> A \<Longrightarrow> A \<in> null_sets (completion M) \<Longrightarrow> B \<in> null_sets (completion M)"
   unfolding null_sets_completion_iff2 by auto
 
+interpretation completion: complete_measure "completion M" for M
+proof
+  show "B \<subseteq> A \<Longrightarrow> A \<in> null_sets (completion M) \<Longrightarrow> B \<in> sets (completion M)" for B A
+    using null_sets_completion_subset[of B A M] by (simp add: null_sets_def)
+qed
+
 lemma null_sets_restrict_space:
   "\<Omega> \<in> sets M \<Longrightarrow> A \<in> null_sets (restrict_space M \<Omega>) \<longleftrightarrow> A \<subseteq> \<Omega> \<and> A \<in> null_sets M"
   by (auto simp: null_sets_def emeasure_restrict_space sets_restrict_space)
@@ -416,6 +422,16 @@
     by (intro bexI[of _ s]) (auto simp: simple_integral_completion simple_function_completion)
 qed
 
+lemma integrable_completion:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> integrable (completion M) f \<longleftrightarrow> integrable M f"
+  by (rule integrable_subalgebra[symmetric]) auto
+
+lemma integral_completion:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" shows "integral\<^sup>L (completion M) f = integral\<^sup>L M f"
+  by (rule integral_subalgebra[symmetric]) (auto intro: f)
+
 locale semifinite_measure =
   fixes M :: "'a measure"
   assumes semifinite:
@@ -685,6 +701,260 @@
   finally show ?thesis .
 qed
 
+lemma (in complete_measure) complete_sets_sandwich_fmeasurable:
+  assumes [measurable]: "A \<in> fmeasurable M" "C \<in> fmeasurable M" and subset: "A \<subseteq> B" "B \<subseteq> C"
+    and measure: "measure M A = measure M C"
+  shows "B \<in> fmeasurable M"
+proof (rule fmeasurableI2)
+  show "B \<subseteq> C" "C \<in> fmeasurable M" by fact+
+  show "B \<in> sets M"
+  proof (rule complete_sets_sandwich)
+    show "A \<in> sets M" "C \<in> sets M" "A \<subseteq> B" "B \<subseteq> C"
+      using assms by auto
+    show "emeasure M A < \<infinity>"
+      using \<open>A \<in> fmeasurable M\<close> by (auto simp: fmeasurable_def)
+    show "emeasure M A = emeasure M C"
+      using assms by (simp add: emeasure_eq_measure2)
+  qed
+qed
+
+lemma AE_completion_iff: "(AE x in completion M. P x) \<longleftrightarrow> (AE x in M. P x)"
+proof
+  assume "AE x in completion M. P x"
+  then obtain N where "N \<in> null_sets (completion M)" and P: "{x\<in>space M. \<not> P x} \<subseteq> N"
+    unfolding eventually_ae_filter by auto
+  then obtain N' where N': "N' \<in> null_sets M" and "N \<subseteq> N'"
+    unfolding null_sets_completion_iff2 by auto
+  from P \<open>N \<subseteq> N'\<close> have "{x\<in>space M. \<not> P x} \<subseteq> N'"
+    by auto
+  with N' show "AE x in M. P x"
+    unfolding eventually_ae_filter by auto
+qed (rule AE_completion)
+
+lemma null_part_null_sets: "S \<in> completion M \<Longrightarrow> null_part M S \<in> null_sets (completion M)"
+  by (auto dest!: null_part intro: null_sets_completionI null_sets_completion_subset)
+
+lemma AE_notin_null_part: "S \<in> completion M \<Longrightarrow> (AE x in M. x \<notin> null_part M S)"
+  by (auto dest!: null_part_null_sets AE_not_in simp: AE_completion_iff)
+
+lemma completion_upper:
+  assumes A: "A \<in> sets (completion M)"
+  shows "\<exists>A'\<in>sets M. A \<subseteq> A' \<and> emeasure (completion M) A = emeasure M A'"
+proof -
+  from AE_notin_null_part[OF A] obtain N where N: "N \<in> null_sets M" "null_part M A \<subseteq> N"
+    unfolding eventually_ae_filter using null_part_null_sets[OF A, THEN null_setsD2, THEN sets.sets_into_space] by auto
+  show ?thesis
+  proof (intro bexI conjI)
+    show "A \<subseteq> main_part M A \<union> N"
+      using \<open>null_part M A \<subseteq> N\<close> by (subst main_part_null_part_Un[symmetric, OF A]) auto
+    show "emeasure (completion M) A = emeasure M (main_part M A \<union> N)"
+      using A \<open>N \<in> null_sets M\<close> by (simp add: emeasure_Un_null_set)
+  qed (use A N in auto)
+qed
+
+lemma AE_in_main_part:
+  assumes A: "A \<in> completion M" shows "AE x in M. x \<in> main_part M A \<longleftrightarrow> x \<in> A"
+  using AE_notin_null_part[OF A]
+  by (subst (2) main_part_null_part_Un[symmetric, OF A]) auto
+
+lemma completion_density_eq:
+  assumes ae: "AE x in M. 0 < f x" and [measurable]: "f \<in> M \<rightarrow>\<^sub>M borel"
+  shows "completion (density M f) = density (completion M) f"
+proof (intro measure_eqI)
+  have "N' \<in> sets M \<and> (AE x\<in>N' in M. f x = 0) \<longleftrightarrow> N' \<in> null_sets M" for N'
+  proof safe
+    assume N': "N' \<in> sets M" and ae_N': "AE x\<in>N' in M. f x = 0"
+    from ae_N' ae have "AE x in M. x \<notin> N'"
+      by eventually_elim auto
+    then show "N' \<in> null_sets M"
+      using N' by (simp add: AE_iff_null_sets)
+  next
+    assume N': "N' \<in> null_sets M" then show "N' \<in> sets M" "AE x\<in>N' in M. f x = 0"
+      using ae AE_not_in[OF N'] by (auto simp: less_le)
+  qed
+  then show sets_eq: "sets (completion (density M f)) = sets (density (completion M) f)"
+    by (simp add: sets_completion null_sets_density_iff)
+
+  fix A assume A: \<open>A \<in> completion (density M f)\<close>
+  moreover
+  have "A \<in> completion M"
+    using A unfolding sets_eq by simp
+  moreover
+  have "main_part (density M f) A \<in> M"
+    using A main_part_sets[of A "density M f"] unfolding sets_density sets_eq by simp
+  moreover have "AE x in M. x \<in> main_part (density M f) A \<longleftrightarrow> x \<in> A"
+    using AE_in_main_part[OF \<open>A \<in> completion (density M f)\<close>] ae by (auto simp add: AE_density)
+  ultimately show "emeasure (completion (density M f)) A = emeasure (density (completion M) f) A"
+    by (auto simp add: emeasure_density measurable_completion nn_integral_completion intro!: nn_integral_cong_AE)
+qed
+
+lemma null_sets_subset: "A \<subseteq> B \<Longrightarrow> A \<in> sets M \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> A \<in> null_sets M"
+  using emeasure_mono[of A B M] by (simp add: null_sets_def)
+
+lemma (in complete_measure) complete2: "A \<subseteq> B \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> A \<in> null_sets M"
+  using complete[of A B] null_sets_subset[of A B M] by simp
+
+lemma (in complete_measure) vimage_null_part_null_sets:
+  assumes f: "f \<in> M \<rightarrow>\<^sub>M N" and eq: "null_sets N \<subseteq> null_sets (distr M N f)"
+    and A: "A \<in> completion N"
+  shows "f -` null_part N A \<inter> space M \<in> null_sets M"
+proof -
+  obtain N' where "N' \<in> null_sets N" "null_part N A \<subseteq> N'"
+    using null_part[OF A] by auto
+  then have N': "N' \<in> null_sets (distr M N f)"
+    using eq by auto
+  show ?thesis
+  proof (rule complete2)
+    show "f -` null_part N A \<inter> space M \<subseteq> f -` N' \<inter> space M"
+      using \<open>null_part N A \<subseteq> N'\<close> by auto
+    show "f -` N' \<inter> space M \<in> null_sets M"
+      using f N' by (auto simp: null_sets_def emeasure_distr)
+  qed
+qed
+
+lemma (in complete_measure) vimage_null_part_sets:
+  "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> null_sets N \<subseteq> null_sets (distr M N f) \<Longrightarrow> A \<in> completion N \<Longrightarrow>
+  f -` null_part N A \<inter> space M \<in> sets M"
+  using vimage_null_part_null_sets[of f N A] by auto
+
+lemma (in complete_measure) measurable_completion2:
+  assumes f: "f \<in> M \<rightarrow>\<^sub>M N" and null_sets: "null_sets N \<subseteq> null_sets (distr M N f)"
+  shows "f \<in> M \<rightarrow>\<^sub>M completion N"
+proof (rule measurableI)
+  show "x \<in> space M \<Longrightarrow> f x \<in> space (completion N)" for x
+    using f[THEN measurable_space] by auto
+  fix A assume A: "A \<in> sets (completion N)"
+  have "f -` A \<inter> space M = (f -` main_part N A \<inter> space M) \<union> (f -` null_part N A \<inter> space M)"
+    using main_part_null_part_Un[OF A] by auto
+  then show "f -` A \<inter> space M \<in> sets M"
+    using f A null_sets by (auto intro: vimage_null_part_sets measurable_sets)
+qed
+
+lemma (in complete_measure) completion_distr_eq:
+  assumes X: "X \<in> M \<rightarrow>\<^sub>M N" and null_sets: "null_sets (distr M N X) = null_sets N"
+  shows "completion (distr M N X) = distr M (completion N) X"
+proof (rule measure_eqI)
+  show eq: "sets (completion (distr M N X)) = sets (distr M (completion N) X)"
+    by (simp add: sets_completion null_sets)
+
+  fix A assume A: "A \<in> completion (distr M N X)"
+  moreover have A': "A \<in> completion N"
+    using A by (simp add: eq)
+  moreover have "main_part (distr M N X) A \<in> sets N"
+    using main_part_sets[OF A] by simp
+  moreover have "X -` A \<inter> space M = (X -` main_part (distr M N X) A \<inter> space M) \<union> (X -` null_part (distr M N X) A \<inter> space M)"
+    using main_part_null_part_Un[OF A] by auto
+  moreover have "X -` null_part (distr M N X) A \<inter> space M \<in> null_sets M"
+    using X A by (intro vimage_null_part_null_sets) (auto cong: distr_cong)
+  ultimately show "emeasure (completion (distr M N X)) A = emeasure (distr M (completion N) X) A"
+    using X by (auto simp: emeasure_distr measurable_completion null_sets measurable_completion2
+                     intro!: emeasure_Un_null_set[symmetric])
+qed
+
+lemma distr_completion: "X \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> distr (completion M) N X = distr M N X"
+  by (intro measure_eqI) (auto simp: emeasure_distr measurable_completion)
+
+proposition (in complete_measure) fmeasurable_inner_outer:
+  "S \<in> fmeasurable M \<longleftrightarrow>
+    (\<forall>e>0. \<exists>T\<in>fmeasurable M. \<exists>U\<in>fmeasurable M. T \<subseteq> S \<and> S \<subseteq> U \<and> \<bar>measure M T - measure M U\<bar> < e)"
+  (is "_ \<longleftrightarrow> ?approx")
+proof safe
+  let ?\<mu> = "measure M" let ?D = "\<lambda>T U . \<bar>?\<mu> T - ?\<mu> U\<bar>"
+  assume ?approx
+  have "\<exists>A. \<forall>n. (fst (A n) \<in> fmeasurable M \<and> snd (A n) \<in> fmeasurable M \<and> fst (A n) \<subseteq> S \<and> S \<subseteq> snd (A n) \<and>
+    ?D (fst (A n)) (snd (A n)) < 1/Suc n) \<and> (fst (A n) \<subseteq> fst (A (Suc n)) \<and> snd (A (Suc n)) \<subseteq> snd (A n))"
+    (is "\<exists>A. \<forall>n. ?P n (A n) \<and> ?Q (A n) (A (Suc n))")
+  proof (intro dependent_nat_choice)
+    show "\<exists>A. ?P 0 A"
+      using \<open>?approx\<close>[THEN spec, of 1] by auto
+  next
+    fix A n assume "?P n A"
+    moreover
+    from \<open>?approx\<close>[THEN spec, of "1/Suc (Suc n)"]
+    obtain T U where *: "T \<in> fmeasurable M" "U \<in> fmeasurable M" "T \<subseteq> S" "S \<subseteq> U" "?D T U < 1 / Suc (Suc n)"
+      by auto
+    ultimately have "?\<mu> T \<le> ?\<mu> (T \<union> fst A)" "?\<mu> (U \<inter> snd A) \<le> ?\<mu> U"
+      "?\<mu> T \<le> ?\<mu> U" "?\<mu> (T \<union> fst A) \<le> ?\<mu> (U \<inter> snd A)"
+      by (auto intro!: measure_mono_fmeasurable)
+    then have "?D (T \<union> fst A) (U \<inter> snd A) \<le> ?D T U"
+      by auto
+    also have "?D T U < 1/Suc (Suc n)" by fact
+    finally show "\<exists>B. ?P (Suc n) B \<and> ?Q A B"
+      using \<open>?P n A\<close> *
+      by (intro exI[of _ "(T \<union> fst A, U \<inter> snd A)"] conjI) auto
+  qed
+  then obtain A
+    where lm: "\<And>n. fst (A n) \<in> fmeasurable M" "\<And>n. snd (A n) \<in> fmeasurable M"
+      and set_bound: "\<And>n. fst (A n) \<subseteq> S" "\<And>n. S \<subseteq> snd (A n)"
+      and mono: "\<And>n. fst (A n) \<subseteq> fst (A (Suc n))" "\<And>n. snd (A (Suc n)) \<subseteq> snd (A n)"
+      and bound: "\<And>n. ?D (fst (A n)) (snd (A n)) < 1/Suc n"
+    by metis
+
+  have INT_sA: "(\<Inter>n. snd (A n)) \<in> fmeasurable M"
+    using lm by (intro fmeasurable_INT[of _ 0]) auto
+  have UN_fA: "(\<Union>n. fst (A n)) \<in> fmeasurable M"
+    using lm order_trans[OF set_bound(1) set_bound(2)[of 0]] by (intro fmeasurable_UN[of _ _ "snd (A 0)"]) auto
+
+  have "(\<lambda>n. ?\<mu> (fst (A n)) - ?\<mu> (snd (A n))) \<longlonglongrightarrow> 0"
+    using bound
+    by (subst tendsto_rabs_zero_iff[symmetric])
+       (intro tendsto_sandwich[OF _ _ tendsto_const LIMSEQ_inverse_real_of_nat];
+        auto intro!: always_eventually less_imp_le simp: divide_inverse)
+  moreover
+  have "(\<lambda>n. ?\<mu> (fst (A n)) - ?\<mu> (snd (A n))) \<longlonglongrightarrow> ?\<mu> (\<Union>n. fst (A n)) - ?\<mu> (\<Inter>n. snd (A n))"
+  proof (intro tendsto_diff Lim_measure_incseq Lim_measure_decseq)
+    show "range (\<lambda>i. fst (A i)) \<subseteq> sets M" "range (\<lambda>i. snd (A i)) \<subseteq> sets M"
+      "incseq (\<lambda>i. fst (A i))" "decseq (\<lambda>n. snd (A n))"
+      using mono lm by (auto simp: incseq_Suc_iff decseq_Suc_iff intro!: measure_mono_fmeasurable)
+    show "emeasure M (\<Union>x. fst (A x)) \<noteq> \<infinity>" "emeasure M (snd (A n)) \<noteq> \<infinity>" for n
+      using lm(2)[of n] UN_fA by (auto simp: fmeasurable_def)
+  qed
+  ultimately have eq: "0 = ?\<mu> (\<Union>n. fst (A n)) - ?\<mu> (\<Inter>n. snd (A n))"
+    by (rule LIMSEQ_unique)
+
+  show "S \<in> fmeasurable M"
+    using UN_fA INT_sA
+  proof (rule complete_sets_sandwich_fmeasurable)
+    show "(\<Union>n. fst (A n)) \<subseteq> S" "S \<subseteq> (\<Inter>n. snd (A n))"
+      using set_bound by auto
+    show "?\<mu> (\<Union>n. fst (A n)) = ?\<mu> (\<Inter>n. snd (A n))"
+      using eq by auto
+  qed
+qed (auto intro!: bexI[of _ S])
+
+lemma (in complete_measure) fmeasurable_measure_inner_outer:
+   "(S \<in> fmeasurable M \<and> m = measure M S) \<longleftrightarrow>
+      (\<forall>e>0. \<exists>T\<in>fmeasurable M. T \<subseteq> S \<and> m - e < measure M T) \<and>
+      (\<forall>e>0. \<exists>U\<in>fmeasurable M. S \<subseteq> U \<and> measure M U < m + e)"
+    (is "?lhs = ?rhs")
+proof
+  assume RHS: ?rhs
+  then have T: "\<And>e. 0 < e \<longrightarrow> (\<exists>T\<in>fmeasurable M. T \<subseteq> S \<and> m - e < measure M T)"
+        and U: "\<And>e. 0 < e \<longrightarrow> (\<exists>U\<in>fmeasurable M. S \<subseteq> U \<and> measure M U < m + e)"
+    by auto
+  have "S \<in> fmeasurable M"
+  proof (subst fmeasurable_inner_outer, safe)
+    fix e::real assume "0 < e"
+    with RHS obtain T U where T: "T \<in> fmeasurable M" "T \<subseteq> S" "m - e/2 < measure M T"
+                          and U: "U \<in> fmeasurable M" "S \<subseteq> U" "measure M U < m + e/2"
+      by (meson half_gt_zero)+
+    moreover have "measure M U - measure M T < (m + e/2) - (m - e/2)"
+      by (intro diff_strict_mono) fact+
+    moreover have "measure M T \<le> measure M U"
+      using T U by (intro measure_mono_fmeasurable) auto
+    ultimately show "\<exists>T\<in>fmeasurable M. \<exists>U\<in>fmeasurable M. T \<subseteq> S \<and> S \<subseteq> U \<and> \<bar>measure M T - measure M U\<bar> < e"
+      apply (rule_tac bexI[OF _ \<open>T \<in> fmeasurable M\<close>])
+      apply (rule_tac bexI[OF _ \<open>U \<in> fmeasurable M\<close>])
+      by auto
+  qed
+  moreover have "m = measure M S"
+    using \<open>S \<in> fmeasurable M\<close> U[of "measure M S - m"] T[of "m - measure M S"]
+    by (cases m "measure M S" rule: linorder_cases)
+       (auto simp: not_le[symmetric] measure_mono_fmeasurable)
+  ultimately show ?lhs
+    by simp
+qed (auto intro!: bexI[of _ S])
+
 lemma (in cld_measure) notin_sets_outer_measure_of_cover:
   assumes E: "E \<subseteq> space M" "E \<notin> sets M"
   shows "\<exists>B\<in>sets M. 0 < emeasure M B \<and> emeasure M B < \<infinity> \<and>
diff -r c3da799b1b45 -r 02de4a58e210 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Sep 29 13:02:43 2016 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Sep 29 13:54:57 2016 +0200
@@ -22,12 +22,6 @@
     by simp
 qed
 
-abbreviation lebesgue :: "'a::euclidean_space measure"
-  where "lebesgue \<equiv> completion lborel"
-
-abbreviation lebesgue_on :: "'a set \<Rightarrow> 'a::euclidean_space measure"
-  where "lebesgue_on \<Omega> \<equiv> restrict_space (completion lborel) \<Omega>"
-
 lemma has_integral_implies_lebesgue_measurable_cbox:
   fixes f :: "'a :: euclidean_space \<Rightarrow> real"
   assumes f: "(f has_integral I) (cbox x y)"
@@ -779,19 +773,6 @@
 
 end
 
-lemma measurable_completion: "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> f \<in> completion M \<rightarrow>\<^sub>M N"
-  by (auto simp: measurable_def)
-
-lemma integrable_completion:
-  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
-  shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> integrable (completion M) f \<longleftrightarrow> integrable M f"
-  by (rule integrable_subalgebra[symmetric]) auto
-
-lemma integral_completion:
-  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
-  assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" shows "integral\<^sup>L (completion M) f = integral\<^sup>L M f"
-  by (rule integral_subalgebra[symmetric]) (auto intro: f)
-
 context
 begin
 
@@ -917,6 +898,11 @@
   shows "f integrable_on S" "LINT x:S | lebesgue. f x = integral S f"
   using has_integral_set_lebesgue[OF f] by (auto simp: integral_unique integrable_on_def)
 
+lemma lmeasurable_iff_has_integral:
+  "S \<in> lmeasurable \<longleftrightarrow> ((indicator S) has_integral measure lebesgue S) UNIV"
+  by (subst has_integral_iff_nn_integral_lebesgue)
+     (auto simp: ennreal_indicator emeasure_eq_measure2 borel_measurable_indicator_iff intro!: fmeasurableI)
+
 abbreviation
   absolutely_integrable_on :: "('a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool"
   (infixr "absolutely'_integrable'_on" 46)
@@ -948,11 +934,63 @@
   qed
 qed
 
+lemma absolutely_integrable_on_iff_nonneg:
+  fixes f :: "'a :: euclidean_space \<Rightarrow> real"
+  assumes "\<And>x. 0 \<le> f x" shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s"
+proof -
+  from assms have "(\<lambda>x. \<bar>f x\<bar>) = f"
+    by (intro ext) auto
+  then show ?thesis
+    unfolding absolutely_integrable_on_def by simp
+qed
+
 lemma absolutely_integrable_onI:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "f integrable_on s \<Longrightarrow> (\<lambda>x. norm (f x)) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
   unfolding absolutely_integrable_on_def by auto
 
+lemma lmeasurable_iff_integrable_on: "S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. 1::real) integrable_on S"
+  by (subst absolutely_integrable_on_iff_nonneg[symmetric])
+     (simp_all add: lmeasurable_iff_integrable)
+
+lemma lmeasure_integral_UNIV: "S \<in> lmeasurable \<Longrightarrow> measure lebesgue S = integral UNIV (indicator S)"
+  by (simp add: lmeasurable_iff_has_integral integral_unique)
+
+lemma lmeasure_integral: "S \<in> lmeasurable \<Longrightarrow> measure lebesgue S = integral S (\<lambda>x. 1::real)"
+  by (auto simp add: lmeasure_integral_UNIV indicator_def[abs_def] lmeasurable_iff_integrable_on)
+
+text \<open>This should be an abbreviation for negligible.\<close>
+lemma negligible_iff_null_sets: "negligible S \<longleftrightarrow> S \<in> null_sets lebesgue"
+proof
+  assume "negligible S"
+  then have "(indicator S has_integral (0::real)) UNIV"
+    by (auto simp: negligible)
+  then show "S \<in> null_sets lebesgue"
+    by (subst (asm) has_integral_iff_nn_integral_lebesgue)
+        (auto simp: borel_measurable_indicator_iff nn_integral_0_iff_AE AE_iff_null_sets indicator_eq_0_iff)
+next
+  assume S: "S \<in> null_sets lebesgue"
+  show "negligible S"
+    unfolding negligible_def
+  proof (safe intro!: has_integral_iff_nn_integral_lebesgue[THEN iffD2]
+                      has_integral_restrict_univ[where s="cbox _ _", THEN iffD1])
+    fix a b
+    show "(\<lambda>x. if x \<in> cbox a b then indicator S x else 0) \<in> lebesgue \<rightarrow>\<^sub>M borel"
+      using S by (auto intro!: measurable_If)
+    then show "(\<integral>\<^sup>+ x. ennreal (if x \<in> cbox a b then indicator S x else 0) \<partial>lebesgue) = ennreal 0"
+      using S[THEN AE_not_in] by (auto intro!: nn_integral_0_iff_AE[THEN iffD2])
+  qed auto
+qed
+
+lemma non_negligible_UNIV [simp]: "\<not> negligible UNIV"
+  unfolding negligible_iff_null_sets by (auto simp: null_sets_def emeasure_lborel_UNIV)
+
+lemma negligible_interval:
+  "negligible (cbox a b) \<longleftrightarrow> box a b = {}" "negligible (box a b) \<longleftrightarrow> box a b = {}"
+   by (auto simp: negligible_iff_null_sets null_sets_def setprod_nonneg inner_diff_left box_eq_empty
+                  not_le emeasure_lborel_cbox_eq emeasure_lborel_box_eq
+            intro: eq_refl antisym less_imp_le)
+
 lemma set_integral_norm_bound:
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> LINT x:k|M. norm (f x)"
diff -r c3da799b1b45 -r 02de4a58e210 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 29 13:02:43 2016 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 29 13:54:57 2016 +0200
@@ -8,7 +8,7 @@
 section \<open>Lebesgue measure\<close>
 
 theory Lebesgue_Measure
-  imports Finite_Product_Measure Bochner_Integration Caratheodory
+  imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure
 begin
 
 subsection \<open>Every right continuous and nondecreasing function gives rise to a measure\<close>
@@ -356,6 +356,12 @@
 definition lborel :: "('a :: euclidean_space) measure" where
   "lborel = distr (\<Pi>\<^sub>M b\<in>Basis. interval_measure (\<lambda>x. x)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
 
+abbreviation lebesgue :: "'a::euclidean_space measure"
+  where "lebesgue \<equiv> completion lborel"
+
+abbreviation lebesgue_on :: "'a set \<Rightarrow> 'a::euclidean_space measure"
+  where "lebesgue_on \<Omega> \<equiv> restrict_space (completion lborel) \<Omega>"
+
 lemma
   shows sets_lborel[simp, measurable_cong]: "sets lborel = sets borel"
     and space_lborel[simp]: "space lborel = space borel"
@@ -659,6 +665,92 @@
     by (simp add: lborel_integrable_real_affine_iff not_integrable_integral_eq)
 qed
 
+lemma
+  fixes c :: "'a::euclidean_space \<Rightarrow> real" and t
+  assumes c: "\<And>j. j \<in> Basis \<Longrightarrow> c j \<noteq> 0"
+  defines "T == (\<lambda>x. t + (\<Sum>j\<in>Basis. (c j * (x \<bullet> j)) *\<^sub>R j))"
+  shows lebesgue_affine_euclidean: "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" (is "_ = ?D")
+    and lebesgue_affine_measurable: "T \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
+proof -
+  have T_borel[measurable]: "T \<in> borel \<rightarrow>\<^sub>M borel"
+    by (auto simp: T_def[abs_def])
+  { fix A :: "'a set" assume A: "A \<in> sets borel"
+    then have "emeasure lborel A = 0 \<longleftrightarrow> emeasure (density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))) A = 0"
+      unfolding T_def using c by (subst lborel_affine_euclidean[symmetric]) auto
+    also have "\<dots> \<longleftrightarrow> emeasure (distr lebesgue lborel T) A = 0"
+      using A c by (simp add: distr_completion emeasure_density nn_integral_cmult setprod_nonneg cong: distr_cong)
+    finally have "emeasure lborel A = 0 \<longleftrightarrow> 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 \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
+    by (rule completion.measurable_completion2) (auto simp: eq measurable_completion)
+
+  have "lebesgue = completion (density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>)))"
+    using c by (subst lborel_affine_euclidean[of c t]) (simp_all add: T_def[abs_def])
+  also have "\<dots> = density (completion (distr lebesgue lborel T)) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))"
+    using c by (auto intro!: always_eventually setprod_pos completion_density_eq simp: distr_completion cong: distr_cong)
+  also have "\<dots> = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))"
+    by (subst completion.completion_distr_eq) (auto simp: eq measurable_completion)
+  finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" .
+qed
+
+lemma
+  fixes m :: real and \<delta> :: "'a::euclidean_space"
+  defines "T r d x \<equiv> r *\<^sub>R x + d"
+  shows emeasure_lebesgue_affine: "emeasure lebesgue (T m \<delta> ` S) = \<bar>m\<bar> ^ DIM('a) * emeasure lebesgue S" (is ?e)
+    and measure_lebesgue_affine: "measure lebesgue (T m \<delta> ` S) = \<bar>m\<bar> ^ 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 \<delta>" and ?T' = "T (1 / m) (- ((1/m) *\<^sub>R \<delta>))"
+    assume "m \<noteq> 0"
+    then have s_comp_s: "?T' \<circ> ?T = id" "?T \<circ> ?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 \<delta> ` S = T (1 / m) ((-1/m) *\<^sub>R \<delta>) -` S \<inter> space lebesgue"
+      using bij_vimage_eq_inv_image[OF \<open>bij ?T'\<close>, of S] by auto
+
+    have trans_eq_T: "(\<lambda>x. \<delta> + (\<Sum>j\<in>Basis. (m * (x \<bullet> j)) *\<^sub>R j)) = T m \<delta>" for m \<delta>
+      unfolding T_def[abs_def] scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric]
+      by (auto simp add: euclidean_representation ac_simps)
+
+    have T[measurable]: "T r d \<in> lebesgue \<rightarrow>\<^sub>M lebesgue" for r d
+      using lebesgue_affine_measurable[of "\<lambda>_. r" d]
+      by (cases "r = 0") (auto simp: trans_eq_T T_def[abs_def])
+
+    show ?thesis
+    proof cases
+      assume "S \<in> sets lebesgue" with \<open>m \<noteq> 0\<close> show ?thesis
+        unfolding eq
+        apply (subst lebesgue_affine_euclidean[of "\<lambda>_. m" \<delta>])
+        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 setprod_constant)
+        done
+    next
+      assume "S \<notin> sets lebesgue"
+      moreover have "?T ` S \<notin> sets lebesgue"
+      proof
+        assume "?T ` S \<in> sets lebesgue"
+        then have "?T -` (?T ` S) \<inter> space lebesgue \<in> sets lebesgue"
+          by (rule measurable_sets[OF T])
+        also have "?T -` (?T ` S) \<inter> 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 setprod_nonneg)
+qed
+
 lemma divideR_right:
   fixes x y :: "'a::real_normed_vector"
   shows "r \<noteq> 0 \<Longrightarrow> y = x /\<^sub>R r \<longleftrightarrow> r *\<^sub>R y = x"
@@ -780,4 +872,16 @@
     by (auto simp: mult.commute)
 qed
 
+abbreviation lmeasurable :: "'a::euclidean_space set set"
+where
+  "lmeasurable \<equiv> fmeasurable lebesgue"
+
+lemma lmeasurable_iff_integrable:
+  "S \<in> lmeasurable \<longleftrightarrow> integrable lebesgue (indicator S :: 'a::euclidean_space \<Rightarrow> real)"
+  by (auto simp: fmeasurable_def integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator)
+
+lemma lmeasurable_cbox [iff]: "cbox a b \<in> lmeasurable"
+  and lmeasurable_box [iff]: "box a b \<in> lmeasurable"
+  by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq)
+
 end
diff -r c3da799b1b45 -r 02de4a58e210 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Thu Sep 29 13:02:43 2016 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Sep 29 13:54:57 2016 +0200
@@ -965,6 +965,16 @@
 translations
   "AE x in M. P" \<rightleftharpoons> "CONST almost_everywhere M (\<lambda>x. P)"
 
+abbreviation
+  "set_almost_everywhere A M P \<equiv> AE x in M. x \<in> A \<longrightarrow> P x"
+
+syntax
+  "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
+  ("AE _\<in>_ in _./ _" [0,0,0,10] 10)
+
+translations
+  "AE x\<in>A in M. P" \<rightleftharpoons> "CONST set_almost_everywhere A M (\<lambda>x. P)"
+
 lemma eventually_ae_filter: "eventually P (ae_filter M) \<longleftrightarrow> (\<exists>N\<in>null_sets M. {x \<in> space M. \<not> P x} \<subseteq> N)"
   unfolding ae_filter_def by (subst eventually_INF_base) (auto simp: eventually_principal subset_eq)
 
@@ -1576,6 +1586,68 @@
     using fin A by (auto intro!: Lim_emeasure_decseq)
 qed auto
 
+subsection \<open>Set of measurable sets with finite measure\<close>
+
+definition fmeasurable :: "'a measure \<Rightarrow> 'a set set"
+where
+  "fmeasurable M = {A\<in>sets M. emeasure M A < \<infinity>}"
+
+lemma fmeasurableD[dest, measurable_dest]: "A \<in> fmeasurable M \<Longrightarrow> A \<in> sets M"
+  by (auto simp: fmeasurable_def)
+
+lemma fmeasurableI: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> A \<in> fmeasurable M"
+  by (auto simp: fmeasurable_def)
+
+lemma fmeasurableI_null_sets: "A \<in> null_sets M \<Longrightarrow> A \<in> fmeasurable M"
+  by (auto simp: fmeasurable_def)
+
+lemma fmeasurableI2: "A \<in> fmeasurable M \<Longrightarrow> B \<subseteq> A \<Longrightarrow> B \<in> sets M \<Longrightarrow> B \<in> fmeasurable M"
+  using emeasure_mono[of B A M] by (auto simp: fmeasurable_def)
+
+lemma measure_mono_fmeasurable:
+  "A \<subseteq> B \<Longrightarrow> A \<in> sets M \<Longrightarrow> B \<in> fmeasurable M \<Longrightarrow> measure M A \<le> measure M B"
+  by (auto simp: measure_def fmeasurable_def intro!: emeasure_mono enn2real_mono)
+
+lemma emeasure_eq_measure2: "A \<in> fmeasurable M \<Longrightarrow> emeasure M A = measure M A"
+  by (simp add: emeasure_eq_ennreal_measure fmeasurable_def less_top)
+
+interpretation fmeasurable: ring_of_sets "space M" "fmeasurable M"
+proof (rule ring_of_setsI)
+  show "fmeasurable M \<subseteq> Pow (space M)" "{} \<in> fmeasurable M"
+    by (auto simp: fmeasurable_def dest: sets.sets_into_space)
+  fix a b assume *: "a \<in> fmeasurable M" "b \<in> fmeasurable M"
+  then have "emeasure M (a \<union> b) \<le> emeasure M a + emeasure M b"
+    by (intro emeasure_subadditive) auto
+  also have "\<dots> < top"
+    using * by (auto simp: fmeasurable_def)
+  finally show  "a \<union> b \<in> fmeasurable M"
+    using * by (auto intro: fmeasurableI)
+  show "a - b \<in> fmeasurable M"
+    using emeasure_mono[of "a - b" a M] * by (auto simp: fmeasurable_def Diff_subset)
+qed
+
+lemma fmeasurable_Diff: "A \<in> fmeasurable M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A - B \<in> fmeasurable M"
+  using fmeasurableI2[of A M "A - B"] by auto
+
+lemma fmeasurable_UN:
+  assumes "countable I" "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> A" "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets M" "A \<in> fmeasurable M"
+  shows "(\<Union>i\<in>I. F i) \<in> fmeasurable M"
+proof (rule fmeasurableI2)
+  show "A \<in> fmeasurable M" "(\<Union>i\<in>I. F i) \<subseteq> A" using assms by auto
+  show "(\<Union>i\<in>I. F i) \<in> sets M"
+    using assms by (intro sets.countable_UN') auto
+qed
+
+lemma fmeasurable_INT:
+  assumes "countable I" "i \<in> I" "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets M" "F i \<in> fmeasurable M"
+  shows "(\<Inter>i\<in>I. F i) \<in> fmeasurable M"
+proof (rule fmeasurableI2)
+  show "F i \<in> fmeasurable M" "(\<Inter>i\<in>I. F i) \<subseteq> F i"
+    using assms by auto
+  show "(\<Inter>i\<in>I. F i) \<in> sets M"
+    using assms by (intro sets.countable_INT') auto
+qed
+
 subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
 
 locale finite_measure = sigma_finite_measure M for M +
@@ -1588,6 +1660,9 @@
 lemma (in finite_measure) emeasure_finite[simp, intro]: "emeasure M A \<noteq> top"
   using finite_emeasure_space emeasure_space[of M A] by (auto simp: top_unique)
 
+lemma (in finite_measure) fmeasurable_eq_sets: "fmeasurable M = sets M"
+  by (auto simp: fmeasurable_def less_top[symmetric])
+
 lemma (in finite_measure) emeasure_eq_measure: "emeasure M A = ennreal (measure M A)"
   by (intro emeasure_eq_ennreal_measure) simp
 
@@ -3135,7 +3210,7 @@
 proof -
   { fix a m assume "a \<in> sigma_sets \<Omega> m" "m \<in> M"
     then have "a \<in> sigma_sets \<Omega> (\<Union>M)"
-     by induction (auto intro: sigma_sets.intros) }
+     by induction (auto intro: sigma_sets.intros(2-)) }
   then show "sets (SUP m:M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
     apply (subst sets_Sup_eq[where X="\<Omega>"])
     apply (auto simp add: M) []
@@ -3317,7 +3392,7 @@
   assume "?M \<noteq> 0"
   then have *: "{x. ?m x \<noteq> 0} = (\<Union>n. {x. ?M / Suc n < ?m x})"
     using reals_Archimedean[of "?m x / ?M" for x]
-    by (auto simp: field_simps not_le[symmetric] measure_nonneg divide_le_0_iff measure_le_0_iff)
+    by (auto simp: field_simps not_le[symmetric] divide_le_0_iff measure_le_0_iff)
   have **: "\<And>n. finite {x. ?M / Suc n < ?m x}"
   proof (rule ccontr)
     fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X")
diff -r c3da799b1b45 -r 02de4a58e210 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Thu Sep 29 13:02:43 2016 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Thu Sep 29 13:54:57 2016 +0200
@@ -27,16 +27,6 @@
 translations
 "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
 
-abbreviation
-  "set_almost_everywhere A M P \<equiv> AE x in M. x \<in> A \<longrightarrow> P x"
-
-syntax
-  "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
-("AE _\<in>_ in _./ _" [0,0,0,10] 10)
-
-translations
-  "AE x\<in>A in M. P" == "CONST set_almost_everywhere A M (\<lambda>x. P)"
-
 (*
     Notation for integration wrt lebesgue measure on the reals:
 
diff -r c3da799b1b45 -r 02de4a58e210 src/HOL/Library/Indicator_Function.thy
--- a/src/HOL/Library/Indicator_Function.thy	Thu Sep 29 13:02:43 2016 +0200
+++ b/src/HOL/Library/Indicator_Function.thy	Thu Sep 29 13:54:57 2016 +0200
@@ -28,6 +28,9 @@
 lemma indicator_eq_1_iff: "indicator A x = (1::'a::zero_neq_one) \<longleftrightarrow> x \<in> A"
   by (auto simp: indicator_def)
 
+lemma indicator_UNIV [simp]: "indicator UNIV = (\<lambda>x. 1)"
+  by auto
+
 lemma indicator_leI:
   "(x \<in> A \<Longrightarrow> y \<in> B) \<Longrightarrow> (indicator A x :: 'a::linordered_nonzero_semiring) \<le> indicator B y"
   by (auto simp: indicator_def)