HOL-Analysis: add measurable sets with finite measures, prove affine transformation rule for the Lebesgue measure
--- 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>
--- 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)"
--- 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
--- 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")
--- 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:
--- 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)