src/HOL/Analysis/Change_Of_Vars.thy

     using eq1 eq2 eq3
     by (simp add: algebra_simps)
 qed
 
 
-
 proposition
   fixes S :: "(real^'n) set"
   assumes "S \<in> lmeasurable"
   shows measurable_stretch: "((\<lambda>x. \<chi> k. m k * x$k) ` S) \<in> lmeasurable" (is  "?f ` S \<in> _")
     and measure_stretch: "measure lebesgue ((\<lambda>x. \<chi> k. m k * x$k) ` S) = \<bar>prod m UNIV\<bar> * measure lebesgue S"

       by (simp add: prm negligible_iff_measure0)
   qed
   then show "(?f ` S) \<in> lmeasurable" ?MEQ
     by metis+
 qed
-
 
 
 proposition
  fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
   assumes "linear f" "S \<in> lmeasurable"

       proof (intro exI conjI)
         show "0 < min d r" "min d r \<le> r"
           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)"
               and d: "norm (y - x) < d" and r: "norm (y - x) < r"
             show "\<bar>v \<bullet> (y - x)\<bar> < norm v * e * min d r / (2 * real CARD('m) ^ CARD('m))"

   assumes S: "S \<in> sets lebesgue" and f: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
   shows "(\<lambda>x. det(matrix(f' x))) \<in> borel_measurable (lebesgue_on S)"
   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"
   shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
          (\<forall>T. T \<in> sets borel \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets lebesgue)"

   ultimately show "{x \<in> S. f x \<in> U} \<in> sets lebesgue"
     using C by auto
 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:
   fixes P :: "'b::euclidean_space set"
   assumes "a \<ge> 0" and a: "a *\<^sub>R i \<noteq> 0" and i: "i \<in> Basis"

       using \<open>i \<in> Basis\<close>
       by (simp add: content_cbox [OF *] prod.distrib prod.If_cases Diff_eq [symmetric] 2)
   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"
     and P: "P \<subseteq> {x. a \<bullet> x = 0}" and "0 \<le> m" "0 \<le> e"
   obtains S where "S \<in> lmeasurable"

     show "measure lebesgue (T ` S) \<le> 2 * e * (2 * m) ^ (CARD('n) - 1)"
       using mS T by (simp add: S measure_orthogonal_image)
   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"
  obtains S where "S \<in> lmeasurable"
             and "{z. norm(z - w) \<le> m \<and> (\<exists>t \<in> P. norm(z - w - t) \<le> e)} \<subseteq> S"

     finally show "integral (g ` S) f \<le> ?b" .
   qed
 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)"
     and intS: "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) absolutely_integrable_on S"
   shows "f absolutely_integrable_on (g ` S)"

   assumes"\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f(g x)"
     and "\<And>x. x \<in> S \<Longrightarrow> (g has_derivative g' x) (at x within S)"
     and "(\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x)) integrable_on S"
   shows "integral (g ` S) f \<le> integral S (\<lambda>x. \<bar>det (matrix (g' x))\<bar> * f(g x))"
   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,