# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1523809367 -3600
# Node ID adc1a992c4702d6bab270e8f76f4082c16f67a50
# Parent  7643b005b29abc26fac98dbfc741804fdf18e95f
a few more results

diff -r 7643b005b29a -r adc1a992c470 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Apr 15 13:57:00 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Apr 15 17:22:47 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"
diff -r 7643b005b29a -r adc1a992c470 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Apr 15 13:57:00 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Apr 15 17:22:47 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>
 
diff -r 7643b005b29a -r adc1a992c470 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Apr 15 13:57:00 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Apr 15 17:22:47 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"
diff -r 7643b005b29a -r adc1a992c470 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Apr 15 13:57:00 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Apr 15 17:22:47 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: