--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun Apr 15 17:48:07 2018 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun Apr 15 17:22:58 2018 +0100
@@ -1172,7 +1172,7 @@
qed
qed
-subsection\<open>Applications\<close>
+subsection\<open>Applications to Negligibility\<close>
lemma negligible_hyperplane:
assumes "a \<noteq> 0 \<or> b \<noteq> 0" shows "negligible {x. a \<bullet> x = b}"
@@ -1268,11 +1268,77 @@
not_le emeasure_lborel_cbox_eq emeasure_lborel_box_eq
intro: eq_refl antisym less_imp_le)
-subsection \<open>Negligibility of a Lipschitz image of a negligible set\<close>
-
lemma measure_eq_0_null_sets: "S \<in> null_sets M \<Longrightarrow> measure M S = 0"
by (auto simp: measure_def null_sets_def)
+lemma negligible_imp_measure0: "negligible S \<Longrightarrow> measure lebesgue S = 0"
+ by (simp add: measure_eq_0_null_sets negligible_iff_null_sets)
+
+lemma negligible_iff_emeasure0: "S \<in> sets lebesgue \<Longrightarrow> (negligible S \<longleftrightarrow> emeasure lebesgue S = 0)"
+ by (auto simp: measure_eq_0_null_sets negligible_iff_null_sets)
+
+lemma negligible_iff_measure0: "S \<in> lmeasurable \<Longrightarrow> (negligible S \<longleftrightarrow> measure lebesgue S = 0)"
+ apply (auto simp: measure_eq_0_null_sets negligible_iff_null_sets)
+ by (metis completion.null_sets_outer subsetI)
+
+lemma negligible_imp_sets: "negligible S \<Longrightarrow> S \<in> sets lebesgue"
+ by (simp add: negligible_iff_null_sets null_setsD2)
+
+lemma negligible_imp_measurable: "negligible S \<Longrightarrow> S \<in> lmeasurable"
+ by (simp add: fmeasurableI_null_sets negligible_iff_null_sets)
+
+lemma negligible_iff_measure: "negligible S \<longleftrightarrow> S \<in> lmeasurable \<and> measure lebesgue S = 0"
+ by (fastforce simp: negligible_iff_measure0 negligible_imp_measurable dest: negligible_imp_measure0)
+
+lemma negligible_outer:
+ "negligible S \<longleftrightarrow> (\<forall>e>0. \<exists>T. S \<subseteq> T \<and> T \<in> lmeasurable \<and> measure lebesgue T < e)" (is "_ = ?rhs")
+proof
+ assume "negligible S" then show ?rhs
+ by (metis negligible_iff_measure order_refl)
+next
+ assume ?rhs then show "negligible S"
+ by (meson completion.null_sets_outer negligible_iff_null_sets)
+qed
+
+lemma negligible_outer_le:
+ "negligible S \<longleftrightarrow> (\<forall>e>0. \<exists>T. S \<subseteq> T \<and> T \<in> lmeasurable \<and> measure lebesgue T \<le> e)" (is "_ = ?rhs")
+proof
+ assume "negligible S" then show ?rhs
+ by (metis dual_order.strict_implies_order negligible_imp_measurable negligible_imp_measure0 order_refl)
+next
+ assume ?rhs then show "negligible S"
+ by (metis le_less_trans negligible_outer real_lbound_gt_zero)
+qed
+
+lemma negligible_UNIV: "negligible S \<longleftrightarrow> (indicat_real S has_integral 0) UNIV" (is "_=?rhs")
+proof
+ assume ?rhs
+ then show "negligible S"
+ apply (auto simp: negligible_def has_integral_iff integrable_on_indicator)
+ by (metis negligible integral_unique lmeasure_integral_UNIV negligible_iff_measure0)
+qed (simp add: negligible)
+
+lemma sets_negligible_symdiff:
+ "\<lbrakk>S \<in> sets lebesgue; negligible((S - T) \<union> (T - S))\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
+ by (metis Diff_Diff_Int Int_Diff_Un inf_commute negligible_Un_eq negligible_imp_sets sets.Diff sets.Un)
+
+lemma lmeasurable_negligible_symdiff:
+ "\<lbrakk>S \<in> lmeasurable; negligible((S - T) \<union> (T - S))\<rbrakk> \<Longrightarrow> T \<in> lmeasurable"
+ using integrable_spike_set_eq lmeasurable_iff_integrable_on by blast
+
+lemma measure_negligible_symdiff:
+ assumes S: "S \<in> lmeasurable"
+ and neg: "negligible (S - T \<union> (T - S))"
+ shows "measure lebesgue T = measure lebesgue S"
+proof -
+ have "measure lebesgue (S - T) = 0"
+ using neg negligible_Un_eq negligible_imp_measure0 by blast
+ then show ?thesis
+ by (metis S Un_commute add.right_neutral lmeasurable_negligible_symdiff measure_Un2 neg negligible_Un_eq negligible_imp_measure0)
+qed
+
+subsection \<open>Negligibility of a Lipschitz image of a negligible set\<close>
+
text\<open>The bound will be eliminated by a sort of onion argument\<close>
lemma locally_Lipschitz_negl_bounded:
fixes f :: "'M::euclidean_space \<Rightarrow> 'N::euclidean_space"
@@ -1631,12 +1697,13 @@
done
qed
+subsection\<open>Integral bounds\<close>
+
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)"
using integral_norm_bound[of M "\<lambda>x. indicator k x *\<^sub>R f x"] by (simp add: set_lebesgue_integral_def)
-
lemma set_integral_finite_UN_AE:
fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
assumes "finite I"
@@ -1676,7 +1743,6 @@
have *: "k \<in> d \<Longrightarrow> f absolutely_integrable_on k" for k
using f[THEN set_integrable_subset, of k] division_ofD(2,4)[OF d, of k] by auto
note d' = division_ofD[OF d]
-
have "(\<Sum>k\<in>d. norm (integral k f)) = (\<Sum>k\<in>d. norm (LINT x:k|lebesgue. f x))"
by (intro sum.cong refl arg_cong[where f=norm] set_lebesgue_integral_eq_integral(2)[symmetric] *)
also have "\<dots> \<le> (\<Sum>k\<in>d. LINT x:k|lebesgue. norm (f x))"
@@ -2208,11 +2274,15 @@
by blast
qed
+subsection\<open>Lemmas about absolute integrability\<close>
+
+text\<open>Redundant!\<close>
lemma absolutely_integrable_add[intro]:
fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on s"
by (rule set_integral_add)
+text\<open>Redundant!\<close>
lemma absolutely_integrable_diff[intro]:
fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) absolutely_integrable_on s"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Apr 15 17:48:07 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Apr 15 17:22:58 2018 +0100
@@ -2090,6 +2090,11 @@
qed
qed
+corollary negligible_standard_hyperplane_cart:
+ fixes k :: "'a::finite"
+ shows "negligible {x. x$k = (0::real)}"
+ by (simp add: cart_eq_inner_axis negligible_standard_hyperplane)
+
subsubsection \<open>Hence the main theorem about negligible sets\<close>
@@ -2354,34 +2359,13 @@
shows "negligible(\<Union>\<T>)"
using assms by induct auto
-lemma negligible:
- "negligible s \<longleftrightarrow> (\<forall>t::('a::euclidean_space) set. ((indicator s::'a\<Rightarrow>real) has_integral 0) t)"
- apply safe
- defer
- apply (subst negligible_def)
-proof -
- fix t :: "'a set"
- assume as: "negligible s"
- have *: "(\<lambda>x. if x \<in> s \<inter> t then 1 else 0) = (\<lambda>x. if x\<in>t then if x\<in>s then 1 else 0 else 0)"
- by auto
- show "((indicator s::'a\<Rightarrow>real) has_integral 0) t"
- apply (subst has_integral_alt)
- apply cases
- apply (subst if_P,assumption)
- unfolding if_not_P
- apply safe
- apply (rule as[unfolded negligible_def,rule_format])
- apply (rule_tac x=1 in exI)
- apply safe
- apply (rule zero_less_one)
- apply (rule_tac x=0 in exI)
- using negligible_subset[OF as,of "s \<inter> t"]
- unfolding negligible_def indicator_def [abs_def]
- unfolding *
- apply auto
- done
-qed auto
-
+lemma negligible: "negligible S \<longleftrightarrow> (\<forall>T. (indicat_real S has_integral 0) T)"
+proof (intro iffI allI)
+ fix T
+ assume "negligible S"
+ then show "(indicator S has_integral 0) T"
+ by (meson Diff_iff has_integral_negligible indicator_simps(2))
+qed (simp add: negligible_def)
subsection \<open>Finite case of the spike theorem is quite commonly needed\<close>
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Sun Apr 15 17:48:07 2018 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Sun Apr 15 17:22:58 2018 +0100
@@ -936,7 +936,6 @@
from continuous_attains_sup[OF \<open>compact S\<close> \<open>S \<noteq> {}\<close> this]
obtain M where M: "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> M"
by auto
-
show ?thesis
proof (rule integrable_bound)
show "integrable lborel (\<lambda>x. indicator S x * M)"
@@ -962,6 +961,8 @@
by (auto simp: mult.commute)
qed
+subsection\<open>Lebesgue measurable sets\<close>
+
abbreviation lmeasurable :: "'a::euclidean_space set set"
where
"lmeasurable \<equiv> fmeasurable lebesgue"
@@ -999,6 +1000,10 @@
by (auto dest!: AE_not_in)
qed
+lemma bounded_set_imp_lmeasurable:
+ assumes "bounded S" "S \<in> sets lebesgue" shows "S \<in> lmeasurable"
+ by (metis assms bounded_Un emeasure_bounded_finite emeasure_completion fmeasurableI main_part_null_part_Un)
+
subsection \<open>A nice lemma for negligibility proofs\<close>
lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Apr 15 17:48:07 2018 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Sun Apr 15 17:22:58 2018 +0100
@@ -3580,25 +3580,16 @@
and "bounded_linear f"
shows "bounded (f ` S)"
proof -
- from assms(1) obtain b where b: "b > 0" "\<forall>x\<in>S. norm x \<le> b"
+ from assms(1) obtain b where "b > 0" and b: "\<forall>x\<in>S. norm x \<le> b"
unfolding bounded_pos by auto
from assms(2) obtain B where B: "B > 0" "\<forall>x. norm (f x) \<le> B * norm x"
using bounded_linear.pos_bounded by (auto simp: ac_simps)
- {
- fix x
- assume "x \<in> S"
- then have "norm x \<le> b"
- using b by auto
- then have "norm (f x) \<le> B * b"
- using B(2)
- apply (erule_tac x=x in allE)
- apply (metis B(1) B(2) order_trans mult_le_cancel_left_pos)
- done
- }
- then show ?thesis
+ show ?thesis
unfolding bounded_pos
- apply (rule_tac x="b*B" in exI)
- using b B by (auto simp: mult.commute)
+ proof (intro exI, safe)
+ show "norm (f x) \<le> B * b" if "x \<in> S" for x
+ by (meson B b less_imp_le mult_left_mono order_trans that)
+ qed (use \<open>b > 0\<close> \<open>B > 0\<close> in auto)
qed
lemma bounded_scaling: