src/HOL/Analysis/Interval_Integral.thy

     Author:     Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
 
 Lebesgue integral over an interval (with endpoints possibly +-\<infinity>)
 *)
 
-theory Interval_Integral (*FIX ME rename? Lebesgue  *)
+theory Interval_Integral
   imports Equivalence_Lebesgue_Henstock_Integration
 begin
 
-lemma continuous_on_vector_derivative:
+lemma%important continuous_on_vector_derivative:
   "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
-  by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
-
-definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
+  by%unimportant (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
+
+definition%important "einterval a b = {x. a < ereal x \<and> ereal x < b}"
 
 lemma einterval_eq[simp]:
   shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}"
     and einterval_eq_Ici: "einterval (ereal a) \<infinity> = {a <..}"
     and einterval_eq_Iic: "einterval (- \<infinity>) (ereal b) = {..< b}"

      (auto simp: einterval_def intro!: open_Collect_conj open_Collect_less continuous_intros)
 
 lemma borel_einterval[measurable]: "einterval a b \<in> sets borel"
   unfolding einterval_def by measurable
 
-subsection%important \<open>Approximating a (possibly infinite) interval\<close>
+subsection\<open>Approximating a (possibly infinite) interval\<close>
 
 lemma filterlim_sup1: "(LIM x F. f x :> G1) \<Longrightarrow> (LIM x F. f x :> (sup G1 G2))"
  unfolding filterlim_def by (auto intro: le_supI1)
 
-lemma ereal_incseq_approx:
+lemma%important ereal_incseq_approx:
   fixes a b :: ereal
   assumes "a < b"
   obtains X :: "nat \<Rightarrow> real" where "incseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> b"
-proof (cases b)
+proof%unimportant (cases b)
   case PInf
   with \<open>a < b\<close> have "a = -\<infinity> \<or> (\<exists>r. a = ereal r)"
     by (cases a) auto
   moreover have "(\<lambda>x. ereal (real (Suc x))) \<longlonglongrightarrow> \<infinity>"
     by (simp add: Lim_PInfty LIMSEQ_Suc_iff) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple)

   ultimately show thesis
     by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"])
        (auto simp: real incseq_def intro!: divide_left_mono)
 qed (insert \<open>a < b\<close>, auto)
 
-lemma ereal_decseq_approx:
+lemma%important ereal_decseq_approx:
   fixes a b :: ereal
   assumes "a < b"
   obtains X :: "nat \<Rightarrow> real" where
     "decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> a"
-proof -
+proof%unimportant -
   have "-b < -a" using \<open>a < b\<close> by simp
   from ereal_incseq_approx[OF this] guess X .
   then show thesis
     apply (intro that[of "\<lambda>i. - X i"])
     apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps)
     apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
     done
 qed
 
-proposition einterval_Icc_approximation:
+lemma%important einterval_Icc_approximation:
   fixes a b :: ereal
   assumes "a < b"
   obtains u l :: "nat \<Rightarrow> real" where
     "einterval a b = (\<Union>i. {l i .. u i})"
     "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
     "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
-proof -
+proof%unimportant -
   from dense[OF \<open>a < b\<close>] obtain c where "a < c" "c < b" by safe
   from ereal_incseq_approx[OF \<open>c < b\<close>] guess u . note u = this
   from ereal_decseq_approx[OF \<open>a < c\<close>] guess l . note l = this
   { fix i from less_trans[OF \<open>l i < c\<close> \<open>c < u i\<close>] have "l i < u i" by simp }
   have "einterval a b = (\<Union>i. {l i .. u i})"

   fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
   shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
     interval_lebesgue_integrable M a b (\<lambda>x. c * f x)"
   by (simp add: interval_lebesgue_integrable_def)
 
-lemma interval_lebesgue_integrable_mult_left [intro, simp]:
+lemma%important interval_lebesgue_integrable_mult_left [intro, simp]:
   fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
   shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
     interval_lebesgue_integrable M a b (\<lambda>x. f x * c)"
-  by (simp add: interval_lebesgue_integrable_def)
-
-lemma interval_lebesgue_integrable_divide [intro, simp]:
+  by%unimportant (simp add: interval_lebesgue_integrable_def)
+
+lemma%important interval_lebesgue_integrable_divide [intro, simp]:
   fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
   shows "(c \<noteq> 0 \<Longrightarrow> interval_lebesgue_integrable M a b f) \<Longrightarrow>
     interval_lebesgue_integrable M a b (\<lambda>x. f x / c)"
-  by (simp add: interval_lebesgue_integrable_def)
+  by%unimportant (simp add: interval_lebesgue_integrable_def)
 
 lemma interval_lebesgue_integral_mult_right [simp]:
   fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
   shows "interval_lebesgue_integral M a b (\<lambda>x. c * f x) =
     c * interval_lebesgue_integral M a b f"
   by (simp add: interval_lebesgue_integral_def)
 
-lemma interval_lebesgue_integral_mult_left [simp]:
+lemma%important interval_lebesgue_integral_mult_left [simp]:
   fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, second_countable_topology}"
   shows "interval_lebesgue_integral M a b (\<lambda>x. f x * c) =
     interval_lebesgue_integral M a b f * c"
-  by (simp add: interval_lebesgue_integral_def)
+  by%unimportant (simp add: interval_lebesgue_integral_def)
 
 lemma interval_lebesgue_integral_divide [simp]:
   fixes M a b c and f :: "real \<Rightarrow> 'a::{banach, real_normed_field, field, second_countable_topology}"
   shows "interval_lebesgue_integral M a b (\<lambda>x. f x / c) =
     interval_lebesgue_integral M a b f / c"

   "interval_lebesgue_integral M a b (\<lambda>x. complex_of_real (f x)) =
     of_real (interval_lebesgue_integral M a b f)"
   unfolding interval_lebesgue_integral_def
   by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real)
 
-lemma interval_lebesgue_integral_le_eq:
+lemma%important interval_lebesgue_integral_le_eq:
   fixes a b f
   assumes "a \<le> b"
   shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)"
-  using assms by (auto simp: interval_lebesgue_integral_def)
+using%unimportant assms by (auto simp: interval_lebesgue_integral_def)
 
 lemma interval_lebesgue_integral_gt_eq:
   fixes a b f
   assumes "a > b"
   shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)"

 lemma interval_integrable_endpoints_reverse:
   "interval_lebesgue_integrable lborel a b f \<longleftrightarrow>
     interval_lebesgue_integrable lborel b a f"
   by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same)
 
-lemma interval_integral_reflect:
+lemma%important interval_integral_reflect:
   "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))"
-proof (induct a b rule: linorder_wlog)
+proof%unimportant (induct a b rule: linorder_wlog)
   case (sym a b) then show ?case
     by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse
              split: if_split_asm)
 next
   case (le a b) 

   by (auto simp: interval_lebesgue_integral_le_eq interval_lebesgue_integrable_def)
 
 lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\<infinity> | M. f x) = (LINT x : {a<..} | M. f x)"
   unfolding interval_lebesgue_integral_def by auto
 
-proposition interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) =
+lemma%important interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \<infinity> f) =
   (set_integrable M {a<..} f)"
   unfolding%unimportant interval_lebesgue_integrable_def by auto
 
 subsection%important\<open>Basic properties of integration over an interval wrt lebesgue measure\<close>
 

   fixes a b c :: real
   shows "interval_lebesgue_integrable lborel a b (\<lambda>x. c)" and "LBINT x=a..b. c = c * (b - a)"
   unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq
   by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def)
 
-lemma interval_integral_cong_AE:
+lemma%important interval_integral_cong_AE:
   assumes [measurable]: "f \<in> borel_measurable borel" "g \<in> borel_measurable borel"
   assumes "AE x \<in> einterval (min a b) (max a b) in lborel. f x = g x"
   shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
   using assms
-proof (induct a b rule: linorder_wlog)
+proof%unimportant (induct a b rule: linorder_wlog)
   case (sym a b) then show ?case
     by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
 next
   case (le a b) then show ?case
     by (auto simp: interval_lebesgue_integral_def max_def min_def
              intro!: set_lebesgue_integral_cong_AE)
 qed
 
-lemma interval_integral_cong:
+lemma%important interval_integral_cong:
   assumes "\<And>x. x \<in> einterval (min a b) (max a b) \<Longrightarrow> f x = g x"
   shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g"
   using assms
-proof (induct a b rule: linorder_wlog)
+proof%unimportant (induct a b rule: linorder_wlog)
   case (sym a b) then show ?case
     by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b])
 next
   case (le a b) then show ?case
     by (auto simp: interval_lebesgue_integral_def max_def min_def

   unfolding interval_lebesgue_integral_def set_lebesgue_integral_def
   apply (intro if_cong refl arg_cong[where f="\<lambda>x. - x"] integral_discrete_difference[of X] assms)
   apply (auto simp: eq anti_eq einterval_iff split: split_indicator)
   done
 
-lemma interval_integral_sum:
+lemma%important interval_integral_sum:
   fixes a b c :: ereal
   assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f"
   shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)"
-proof -
+proof%unimportant -
   let ?I = "\<lambda>a b. LBINT x=a..b. f x"
   { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \<le> b" "b \<le> c"
     then have ord: "a \<le> b" "b \<le> c" "a \<le> c" and f': "set_integrable lborel (einterval a c) f"
       by (auto simp: interval_lebesgue_integrable_def)
     then have f: "set_borel_measurable borel (einterval a c) f"

     using integrable
     by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
        (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
 qed
 
-lemma interval_integrable_isCont:
+lemma%important interval_integrable_isCont:
   fixes a b and f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   shows "(\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> isCont f x) \<Longrightarrow>
     interval_lebesgue_integrable lborel a b f"
-proof (induct a b rule: linorder_wlog)
+proof%unimportant (induct a b rule: linorder_wlog)
   case (le a b) then show ?case
     unfolding interval_lebesgue_integrable_def set_integrable_def
     by (auto simp: interval_lebesgue_integrable_def
         intro!: set_integrable_subset[unfolded set_integrable_def, OF borel_integrable_compact[of "{a .. b}"]]
         continuous_at_imp_continuous_on)

   by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral)
 
 
 subsection%important\<open>General limit approximation arguments\<close>
 
-proposition interval_integral_Icc_approx_nonneg:
+lemma%important interval_integral_Icc_approx_nonneg:
   fixes a b :: ereal
   assumes "a < b"
   fixes u l :: "nat \<Rightarrow> real"
   assumes  approx: "einterval a b = (\<Union>i. {l i .. u i})"
     "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"

   assumes f_measurable: "set_borel_measurable lborel (einterval a b) f"
   assumes lbint_lim: "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> C"
   shows
     "set_integrable lborel (einterval a b) f"
     "(LBINT x=a..b. f x) = C"
-proof -
+proof%unimportant -
   have 1 [unfolded set_integrable_def]: "\<And>i. set_integrable lborel {l i..u i} f" by (rule f_integrable)
   have 2: "AE x in lborel. mono (\<lambda>n. indicator {l n..u n} x *\<^sub>R f x)"
   proof -
      from f_nonneg have "AE x in lborel. \<forall>i. l i \<le> x \<longrightarrow> x \<le> u i \<longrightarrow> 0 \<le> f x"
       by eventually_elim

   show "set_integrable lborel (einterval a b) f"
     unfolding set_integrable_def
     by (rule integrable_monotone_convergence[OF 1 2 3 4 5])
 qed
 
-proposition interval_integral_Icc_approx_integrable:
+lemma%important interval_integral_Icc_approx_integrable:
   fixes u l :: "nat \<Rightarrow> real" and a b :: ereal
   fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   assumes "a < b"
   assumes  approx: "einterval a b = (\<Union>i. {l i .. u i})"
     "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
     "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
   assumes f_integrable: "set_integrable lborel (einterval a b) f"
   shows "(\<lambda>i. LBINT x=l i.. u i. f x) \<longlonglongrightarrow> (LBINT x=a..b. f x)"
-proof -
+proof%unimportant -
   have "(\<lambda>i. LBINT x:{l i.. u i}. f x) \<longlonglongrightarrow> (LBINT x:einterval a b. f x)"
     unfolding set_lebesgue_integral_def
   proof (rule integral_dominated_convergence)
     show "integrable lborel (\<lambda>x. norm (indicator (einterval a b) x *\<^sub>R f x))"
       using f_integrable integrable_norm set_integrable_def by blast

 
 (*
   TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.)
 *)
 
-lemma interval_integral_FTC_finite:
+lemma%important interval_integral_FTC_finite:
   fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: real
   assumes f: "continuous_on {min a b..max a b} f"
   assumes F: "\<And>x. min a b \<le> x \<Longrightarrow> x \<le> max a b \<Longrightarrow> (F has_vector_derivative (f x)) (at x within
     {min a b..max a b})"
   shows "(LBINT x=a..b. f x) = F b - F a"
-proof (cases "a \<le> b")
+proof%unimportant (cases "a \<le> b")
   case True
   have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)"
     by (simp add: True interval_integral_Icc set_lebesgue_integral_def)
   also have "\<dots> = F b - F a"
   proof (rule integral_FTC_atLeastAtMost [OF True])

   finally show ?thesis
     by (metis interval_integral_endpoints_reverse)
 qed
 
 
-lemma interval_integral_FTC_nonneg:
+lemma%important interval_integral_FTC_nonneg:
   fixes f F :: "real \<Rightarrow> real" and a b :: ereal
   assumes "a < b"
   assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV F x :> f x"
   assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x"
   assumes f_nonneg: "AE x in lborel. a < ereal x \<longrightarrow> ereal x < b \<longrightarrow> 0 \<le> f x"
   assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
   assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
   shows
     "set_integrable lborel (einterval a b) f"
     "(LBINT x=a..b. f x) = B - A"
-proof -
+proof%unimportant -
   obtain u l where approx:
     "einterval a b = (\<Union>i. {l i .. u i})"
     "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
     "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
     by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])

     by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3])
   show "set_integrable lborel (einterval a b) f"
     by (rule interval_integral_Icc_approx_nonneg [OF \<open>a < b\<close> approx 1 f_nonneg 2 3])
 qed
 
-theorem interval_integral_FTC_integrable:
+lemma%important interval_integral_FTC_integrable:
   fixes f F :: "real \<Rightarrow> 'a::euclidean_space" and a b :: ereal
   assumes "a < b"
   assumes F: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> (F has_vector_derivative f x) (at x)"
   assumes f: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f x"
   assumes f_integrable: "set_integrable lborel (einterval a b) f"
   assumes A: "((F \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
   assumes B: "((F \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
   shows "(LBINT x=a..b. f x) = B - A"
-proof -
+proof%unimportant -
   obtain u l where approx:
     "einterval a b = (\<Union>i. {l i .. u i})"
     "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
     "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
     by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])

 (*
   The second Fundamental Theorem of Calculus and existence of antiderivatives on an
   einterval.
 *)
 
-theorem interval_integral_FTC2:
+lemma%important interval_integral_FTC2:
   fixes a b c :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
   assumes "a \<le> c" "c \<le> b"
   and contf: "continuous_on {a..b} f"
   fixes x :: real
   assumes "a \<le> x" and "x \<le> b"
   shows "((\<lambda>u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})"
-proof -
+proof%unimportant -
   let ?F = "(\<lambda>u. LBINT y=a..u. f y)"
   have intf: "set_integrable lborel {a..b} f"
     by (rule borel_integrable_atLeastAtMost', rule contf)
   have "((\<lambda>u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})"
     using \<open>a \<le> x\<close> \<open>x \<le> b\<close> 

       apply (auto simp: interval_lebesgue_integrable_def simp del: real_scaleR_def)
       by (rule set_integrable_subset [OF intf], auto simp: min_def max_def)
   qed (insert assms, auto)
 qed
 
-proposition einterval_antiderivative:
+lemma%important einterval_antiderivative:
   fixes a b :: ereal and f :: "real \<Rightarrow> 'a::euclidean_space"
   assumes "a < b" and contf: "\<And>x :: real. a < x \<Longrightarrow> x < b \<Longrightarrow> isCont f x"
   shows "\<exists>F. \<forall>x :: real. a < x \<longrightarrow> x < b \<longrightarrow> (F has_vector_derivative f x) (at x)"
-proof -
+proof%unimportant -
   from einterval_nonempty [OF \<open>a < b\<close>] obtain c :: real where [simp]: "a < c" "c < b"
     by (auto simp: einterval_def)
   let ?F = "(\<lambda>u. LBINT y=c..u. f y)"
   show ?thesis
   proof (rule exI, clarsimp)

 subsection%important\<open>The substitution theorem\<close>
 
 text\<open>Once again, three versions: first, for finite intervals, and then two versions for
     arbitrary intervals.\<close>
 
-theorem interval_integral_substitution_finite:
+lemma%important interval_integral_substitution_finite:
   fixes a b :: real and f :: "real \<Rightarrow> 'a::euclidean_space"
   assumes "a \<le> b"
   and derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_real_derivative (g' x)) (at x within {a..b})"
   and contf : "continuous_on (g ` {a..b}) f"
   and contg': "continuous_on {a..b} g'"
   shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y"
-proof-
+proof%unimportant-
   have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})"
     using derivg unfolding has_field_derivative_iff_has_vector_derivative .
   then have contg [simp]: "continuous_on {a..b} g"
     by (rule continuous_on_vector_derivative) auto
   have 1: "\<exists>x\<in>{a..b}. u = g x" if "min (g a) (g b) \<le> u" "u \<le> max (g a) (g b)" for u

   ultimately show ?thesis by simp
 qed
 
 (* TODO: is it possible to lift the assumption here that g' is nonnegative? *)
 
-theorem interval_integral_substitution_integrable:
+lemma%important interval_integral_substitution_integrable:
   fixes f :: "real \<Rightarrow> 'a::euclidean_space" and a b u v :: ereal
   assumes "a < b"
   and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
   and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)"
   and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"

   and A: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> A) (at_right a)"
   and B: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
   and integrable: "set_integrable lborel (einterval a b) (\<lambda>x. g' x *\<^sub>R f (g x))"
   and integrable2: "set_integrable lborel (einterval A B) (\<lambda>x. f x)"
   shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))"
-proof -
+proof%unimportant -
   obtain u l where approx [simp]:
     "einterval a b = (\<Union>i. {l i .. u i})"
     "incseq u" "decseq l" "\<And>i. l i < u i" "\<And>i. a < l i" "\<And>i. u i < b"
     "l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b" 
     by (blast intro: einterval_Icc_approximation[OF \<open>a < b\<close>])

 
 (* TODO: the last two proofs are only slightly different. Factor out common part?
    An alternative: make the second one the main one, and then have another lemma
    that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *)
 
-theorem interval_integral_substitution_nonneg:
+lemma%important interval_integral_substitution_nonneg:
   fixes f g g':: "real \<Rightarrow> real" and a b u v :: ereal
   assumes "a < b"
   and deriv_g: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> DERIV g x :> g' x"
   and contf: "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont f (g x)"
   and contg': "\<And>x. a < ereal x \<Longrightarrow> ereal x < b \<Longrightarrow> isCont g' x"

   and B: "((ereal \<circ> g \<circ> real_of_ereal) \<longlongrightarrow> B) (at_left b)"
   and integrable_fg: "set_integrable lborel (einterval a b) (\<lambda>x. f (g x) * g' x)"
   shows
     "set_integrable lborel (einterval A B) f"
     "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
-proof -
+proof%unimportant -
   from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
   note less_imp_le [simp]
   have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
     by (rule order_less_le_trans, rule approx, force)
   have lessb[simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"

   ("(4CLBINT _=_.._. _)" [0,60,60,61] 60)
 
 translations
   "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
 
-proposition interval_integral_norm:
+lemma%important interval_integral_norm:
   fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   shows "interval_lebesgue_integrable lborel a b f \<Longrightarrow> a \<le> b \<Longrightarrow>
     norm (LBINT t=a..b. f t) \<le> LBINT t=a..b. norm (f t)"
   using%unimportant integral_norm_bound[of lborel "\<lambda>x. indicator (einterval a b) x *\<^sub>R f x"]
   by%unimportant (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def)
 
-proposition interval_integral_norm2:
+lemma%important interval_integral_norm2:
   "interval_lebesgue_integrable lborel a b f \<Longrightarrow>
     norm (LBINT t=a..b. f t) \<le> \<bar>LBINT t=a..b. norm (f t)\<bar>"
-proof (induct a b rule: linorder_wlog)
+proof%unimportant (induct a b rule: linorder_wlog)
   case (sym a b) then show ?case
     by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b])
 next
   case (le a b)
   then have "\<bar>LBINT t=a..b. norm (f t)\<bar> = LBINT t=a..b. norm (f t)"