# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1524082370 -3600
# Node ID 0a2a1b6507c17b76786908356c451c7f93ca80a0
# Parent  40b790c5a11d9b7a89d1bdb95f280b5bec5dbb30
correction of TeX errors and other oversights

diff -r 40b790c5a11d -r 0a2a1b6507c1 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Wed Apr 18 18:46:51 2018 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Wed Apr 18 21:12:50 2018 +0100
@@ -346,7 +346,6 @@
 qed
 
 
-
 proposition
   fixes S :: "(real^'n) set"
   assumes "S \<in> lmeasurable"
@@ -451,7 +450,6 @@
 qed
 
 
-
 proposition
  fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
   assumes "linear f" "S \<in> lmeasurable"
@@ -1813,7 +1811,7 @@
           using \<open>r > 0\<close> \<open>d > 0\<close> by auto
         show "{x' \<in> S. \<exists>v. v \<noteq> 0 \<and> (\<forall>\<xi>>0. \<exists>e>0. \<forall>z\<in>S - {x'}. norm (x' - z) < e \<longrightarrow> \<bar>v \<bullet> (z - x')\<bar> < \<xi> * norm (x' - z))} \<inter> ball x (min d r) \<subseteq> ?W"
           proof (clarsimp simp: dist_norm norm_minus_commute)
-            fix y w 
+            fix y w
             assume "y \<in> S" "w \<noteq> 0"
               and less [rule_format]:
                     "\<forall>\<xi>>0. \<exists>e>0. \<forall>z\<in>S - {y}. norm (y - z) < e \<longrightarrow> \<bar>w \<bullet> (z - y)\<bar> < \<xi> * norm (y - z)"
@@ -2288,8 +2286,8 @@
   unfolding det_def
   by (intro measurable) (auto intro: f borel_measurable_partial_derivatives [OF S])
 
-text\<open>The localisation wrt S uses the same argument for many similar results.
-See HOL Light's MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_BOREL, etc.\<close>
+text\<open>The localisation wrt S uses the same argument for many similar results.\<close>
+(*See HOL Light's MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_BOREL, etc.*)
 lemma borel_measurable_lebesgue_on_preimage_borel:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "S \<in> sets lebesgue"
@@ -2370,27 +2368,6 @@
 qed
 
 
-
-thm integrable_on_subcbox
-
-proposition measurable_bounded_by_integrable_imp_integrable:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes f: "f \<in> borel_measurable (lebesgue_on S)" and g: "g integrable_on S"
-    and normf: "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> g x" and S: "S \<in> sets lebesgue"
-  shows "f integrable_on S"
-proof (rule integrable_on_all_intervals_integrable_bound [OF _ normf g])
-  show "(\<lambda>x. if x \<in> S then f x else 0) integrable_on cbox a b" for a b
-  proof (rule measurable_bounded_lemma)
-    show "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
-      by (simp add: S borel_measurable_UNIV f)
-    show "(\<lambda>x. if x \<in> S then g x else 0) integrable_on cbox a b"
-      by (simp add: g integrable_altD(1))
-    show "norm (if x \<in> S then f x else 0) \<le> (if x \<in> S then g x else 0)" for x
-      using normf by simp
-  qed
-qed
-
-
 subsection\<open>Simplest case of Sard's theorem (we don't need continuity of derivative)\<close>
 
 lemma Sard_lemma00:
@@ -2428,7 +2405,7 @@
   qed blast
 qed
 
-text\<open>As above, but reorienting the vector (HOL Light's @text{GEOM_BASIS_MULTIPLE_TAC})\<close>
+text\<open>As above, but reorienting the vector (HOL Light's @text{GEOM\_BASIS\_MULTIPLE\_TAC})\<close>
 lemma Sard_lemma0:
   fixes P :: "(real^'n::{finite,wellorder}) set"
   assumes "a \<noteq> 0"
@@ -2487,7 +2464,7 @@
   qed
 qed
 
-(*As above, but translating the sets (HOL Light's GEN_GEOM_ORIGIN_TAC)*)
+text\<open>As above, but translating the sets (HOL Light's @text{GEN\_GEOM\_ORIGIN\_TAC})\<close>
 lemma Sard_lemma1:
   fixes P :: "(real^'n::{finite,wellorder}) set"
    assumes P: "dim P < CARD('n)" and "0 \<le> m" "0 \<le> e"
@@ -3073,7 +3050,6 @@
 qed
 
 
-
 lemma absolutely_integrable_on_image_real:
   fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real" and g :: "real^'n::_ \<Rightarrow> real^'n::_"
   assumes der_g: "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)"
@@ -3166,7 +3142,6 @@
   using integral_on_image_ubound_nonneg [OF assms] by simp
 
 
-
 subsection\<open>Change-of-variables theorem\<close>
 
 text\<open>The classic change-of-variables theorem. We have two versions with quite general hypotheses,