src/HOL/Analysis/Lebesgue_Integral_Substitution.thy

     Provides lemmas for integration by substitution for the basic integral types.
     Note that the substitution function must have a nonnegative derivative.
     This could probably be weakened somehow.
 *)
 
-section \<open>Integration by Substition\<close>
+section \<open>Integration by Substition for the Lebesgue integral\<close>
 
 theory Lebesgue_Integral_Substitution
 imports Interval_Integral
 begin
 

          (auto split: split_indicator simp: derivg_nonneg mult_ac)
     finally show ?case by simp
   qed
 qed
 
-lemma nn_integral_substitution:
+theorem nn_integral_substitution:
   fixes f :: "real \<Rightarrow> real"
   assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f"
   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   assumes contg': "continuous_on {a..b} g'"
   assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"

   also have "... = \<integral>\<^sup>+x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel"
     by (intro nn_integral_cong) (auto simp: mult.commute derivg_nonneg ennreal_mult' split: split_indicator)
   finally show ?thesis .
 qed auto
 
-lemma integral_substitution:
+theorem integral_substitution:
   assumes integrable: "set_integrable lborel {g a..g b} f"
   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   assumes contg': "continuous_on {a..b} g'"
   assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   assumes "a \<le> b"

     by (subst real_lebesgue_integral_def) (simp_all add: field_simps)
   finally show "(LBINT x. f x * indicator {g a..g b} x) =
                      (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
 qed
 
-lemma interval_integral_substitution:
+theorem interval_integral_substitution:
   assumes integrable: "set_integrable lborel {g a..g b} f"
   assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   assumes contg': "continuous_on {a..b} g'"
   assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   assumes "a \<le> b"