Quelle Lebesgue_Integral_Substitution.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Lebesgue_Integral_Substitution.thy
    Author:     Manuel Eberl

    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 for the Lebesgue Integral\<close>

theory Lebesgue_Integral_Substitution
imports Interval_Integral
begin

lemma nn_integral_substitution_aux:
  fixes f :: "real \ ennreal"
  assumes Mf: "f \ borel_measurable borel"
  assumes nonnegf: "\x. f x \ 0"
  assumes derivg: "\x. x \ {a..b} \ (g has_real_derivative g' x) (at x)"
  assumes contg': "continuous_on {a..b} g'"
  assumes derivg_nonneg: "\x. x \ {a..b} \ g' x \ 0"
  assumes "a < b"
  shows "(\\<^sup>+x. f x * indicator {g a..g b} x \lborel) =
             (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
proof-
  from \<open>a < b\<close> have [simp]: "a \<le> b" by simp
  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
  from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and
                             Mg': "set_borel_measurable borel {a..b} g'"
    using atLeastAtMost_borel set_measurable_continuous_on by blast+
  from derivg have derivg': "\x. x \ {a..b} \ (g has_vector_derivative g' x) (at x)"
    by (simp only: has_real_derivative_iff_has_vector_derivative)

  have real_ind[simp]: "\A x. enn2real (indicator A x) = indicator A x"
      by (auto split: split_indicator)
  have ennreal_ind[simp]: "\A x. ennreal (indicator A x) = indicator A x"
      by (auto split: split_indicator)
  have [simp]: "\x A. indicator A (g x) = indicator (g -` A) x"
      by (auto split: split_indicator)

  from derivg derivg_nonneg have monog: "\x y. a \ x \ x \ y \ y \ b \ g x \ g y"
    by (rule deriv_nonneg_imp_mono) simp_all
  with monog have [simp]: "g a \ g b" by (auto intro: mono_onD)

  show ?thesis
  proof (induction rule: borel_measurable_induct[OF Mf, case_names cong set mult add sup])
    case (cong f1 f2)
    from cong.hyps(3) have "f1 = f2" by auto
    with cong show ?case by simp
  next
    case (set A)
    from set.hyps show ?case
    proof (induction rule: borel_set_induct)
      case empty
      thus ?case by simp
    next
      case (interval c d)
      {
        fix u v :: real assume asm: "{u..v} \ {g a..g b}" "u \ v"

        obtain u' v' where u'v': "{a..b} \ g-`{u..v} = {u'..v'}" "u' \ v'" "g u' = u" "g v' = v"
             using asm by (rule_tac continuous_interval_vimage_Int[OF contg monog, of u v]) simp_all
        hence "{u'..v'} \ {a..b}" "{u'..v'} \ g -` {u..v}" by blast+
        with u'v'(2) have "u' \ g -` {u..v}" "v' \ g -` {u..v}" by auto
        from u'v'(1) have [simp]: "{a..b} \ g -` {u..v} \ sets borel" by simp

        have A: "continuous_on {min u' v'..max u' v'} g'"
            by (simp only: u'v' max_absorb2 min_absorb1)
               (intro continuous_on_subset[OF contg'], insert u'v', auto)
        have "\x. x \ {u'..v'} \ (g has_real_derivative g' x) (at x within {u'..v'})"
           using asm by (intro has_field_derivative_subset[OF derivg] subsetD[OF \<open>{u'..v'} \<subseteq> {a..b}\<close>]) auto
        hence B: "\x. min u' v' \ x \ x \ max u' v' \
                      (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
            by (simp only: u'v' max_absorb2 min_absorb1)
               (auto simp: has_real_derivative_iff_has_vector_derivative)
          have "integrable lborel (\x. indicator ({a..b} \ g -` {u..v}) x *\<^sub>R g' x)"
            using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
            by (metis \<open>{u'..v'} \<subseteq> {a..b}\<close> eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))
        hence "(\\<^sup>+x. ennreal (g' x) * indicator ({a..b} \ g-` {u..v}) x \lborel) =
                   (LBINT x:{a..b} \<inter> g-`{u..v}. g' x)"
          unfolding set_lebesgue_integral_def
          by (subst nn_integral_eq_integral[symmetric])
             (auto intro!: derivg_nonneg nn_integral_cong split: split_indicator)
        also from interval_integral_FTC_finite[OF A B]
            have "(LBINT x:{a..b} \ g-`{u..v}. g' x) = v - u"
                by (simp add: u'v' interval_integral_Icc \<open>u \<le> v\<close>)
        finally have "(\\<^sup>+ x. ennreal (g' x) * indicator ({a..b} \ g -` {u..v}) x \lborel) =
                           ennreal (v - u)" .
      } note A = this

      have "(\\<^sup>+x. indicator {c..d} (g x) * ennreal (g' x) * indicator {a..b} x \lborel) =
               (\<integral>\<^sup>+ x. ennreal (g' x) * indicator ({a..b} \<inter> g -` {c..d}) x \<partial>lborel)"
        by (intro nn_integral_cong) (simp split: split_indicator)
      also have "{a..b} \ g-`{c..d} = {a..b} \ g-`{max (g a) c..min (g b) d}"
        using \<open>a \<le> b\<close> \<open>c \<le> d\<close>
        by (auto intro!: monog intro: order.trans)
      also have "(\\<^sup>+ x. ennreal (g' x) * indicator ... x \lborel) =
        (if max (g a) c \<le> min (g b) d then min (g b) d - max (g a) c else 0)"
         using \<open>c \<le> d\<close> by (simp add: A)
      also have "... = (\\<^sup>+ x. indicator ({g a..g b} \ {c..d}) x \lborel)"
        by (subst nn_integral_indicator) (auto intro!: measurable_sets Mg simp:)
      also have "... = (\\<^sup>+ x. indicator {c..d} x * indicator {g a..g b} x \lborel)"
        by (intro nn_integral_cong) (auto split: split_indicator)
      finally show ?case ..

      next

      case (compl A)
      note \<open>A \<in> sets borel\<close>[measurable]
      from emeasure_mono[of "A \ {g a..g b}" "{g a..g b}" lborel]
      have [simp]: "emeasure lborel (A \ {g a..g b}) \ top" by (auto simp: top_unique)
      have [simp]: "g -` A \ {a..b} \ sets borel"
        by (rule set_borel_measurable_sets[OF Mg]) auto
      have [simp]: "g -` (-A) \ {a..b} \ sets borel"
        by (rule set_borel_measurable_sets[OF Mg]) auto

      have "(\\<^sup>+x. indicator (-A) x * indicator {g a..g b} x \lborel) =
                (\<integral>\<^sup>+x. indicator (-A \<inter> {g a..g b}) x \<partial>lborel)"
        by (rule nn_integral_cong) (simp split: split_indicator)
      also from compl have "... = emeasure lborel ({g a..g b} - A)" using derivg_nonneg
        by (simp add: vimage_Compl diff_eq Int_commute[of "-A"])
      also have "{g a..g b} - A = {g a..g b} - A \ {g a..g b}" by blast
      also have "emeasure lborel ... = g b - g a - emeasure lborel (A \ {g a..g b})"
             using \<open>A \<in> sets borel\<close> by (subst emeasure_Diff) auto
     also have "emeasure lborel (A \ {g a..g b}) =
                    \<integral>\<^sup>+x. indicator A x * indicator {g a..g b} x \<partial>lborel"
       using \<open>A \<in> sets borel\<close>
       by (subst nn_integral_indicator[symmetric], simp, intro nn_integral_cong)
          (simp split: split_indicator)
      also have "... = \\<^sup>+ x. indicator (g-`A \ {a..b}) x * ennreal (g' x * indicator {a..b} x) \lborel" (is "_ = ?I")
        by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
      also have "g b - g a = (LBINT x:{a..b}. g' x)" using derivg'
        unfolding set_lebesgue_integral_def
        by (intro integral_FTC_atLeastAtMost[symmetric])
           (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
                 has_vector_derivative_at_within)
      also have "ennreal ... = (\\<^sup>+ x. g' x * indicator {a..b} x \lborel)"
        using borel_integrable_atLeastAtMost'[OF contg'] unfolding set_lebesgue_integral_def
        by (subst nn_integral_eq_integral)
           (simp_all add: mult.commute derivg_nonneg set_integrable_def split: split_indicator)
      also have Mg'': "(\x. indicator (g -` A \ {a..b}) x * ennreal (g' x * indicator {a..b} x))
                            \<in> borel_measurable borel" using Mg'
        by (intro borel_measurable_times_ennreal borel_measurable_indicator)
           (simp_all add: mult.commute set_borel_measurable_def)
      have le: "(\\<^sup>+x. indicator (g-`A \ {a..b}) x * ennreal (g' x * indicator {a..b} x) \lborel) \
                        (\<integral>\<^sup>+x. ennreal (g' x) * indicator {a..b} x \<partial>lborel)"
         by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg)
      note integrable = borel_integrable_atLeastAtMost'[OF contg']
      with le have notinf: "(\\<^sup>+x. indicator (g-`A \ {a..b}) x * ennreal (g' x * indicator {a..b} x) \lborel) \ top"
          by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique set_integrable_def)
      have "(\\<^sup>+ x. g' x * indicator {a..b} x \lborel) - ?I =
                  \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) -
                        indicator (g -` A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel"
        apply (intro nn_integral_diff[symmetric])
        apply (insert Mg', simp add: mult.commute set_borel_measurable_def) []
        apply (insert Mg'', simp) []
        apply (simp split: split_indicator add: derivg_nonneg)
        apply (rule notinf)
        apply (simp split: split_indicator add: derivg_nonneg)
        done
      also have "... = \\<^sup>+ x. indicator (-A) (g x) * ennreal (g' x) * indicator {a..b} x \lborel"
        by (intro nn_integral_cong) (simp split: split_indicator)
      finally show ?case .

    next
      case (union f)
      then have [simp]: "\i. {a..b} \ g -` f i \ sets borel"
        by (subst Int_commute, intro set_borel_measurable_sets[OF Mg]) auto
      have "g -` (\i. f i) \ {a..b} = (\i. {a..b} \ g -` f i)" by auto
      hence "g -` (\i. f i) \ {a..b} \ sets borel" by (auto simp del: UN_simps)

      have "(\\<^sup>+x. indicator (\i. f i) x * indicator {g a..g b} x \lborel) =
                \<integral>\<^sup>+x. indicator (\<Union>i. {g a..g b} \<inter> f i) x \<partial>lborel"
          by (intro nn_integral_cong) (simp split: split_indicator)
      also from union have "... = emeasure lborel (\i. {g a..g b} \ f i)" by simp
      also from union have "... = (\i. emeasure lborel ({g a..g b} \ f i))"
        by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def)
      also from union have "... = (\i. \\<^sup>+x. indicator ({g a..g b} \ f i) x \lborel)" by simp
      also have "(\i. \\<^sup>+x. indicator ({g a..g b} \ f i) x \lborel) =
                           (\<lambda>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel)"
        by (intro ext nn_integral_cong) (simp split: split_indicator)
      also from union.IH have "(\i. \\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \lborel) =
          (\<Sum>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)" by simp
      also have "(\i. \\<^sup>+ x. indicator (f i) (g x) * ennreal (g' x) * indicator {a..b} x \lborel) =
                         (\<lambda>i. \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x \<partial>lborel)"
        by (intro ext nn_integral_cong) (simp split: split_indicator)
      also have "(\i. ... i) = \\<^sup>+ x. (\i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \ g -` f i) x) \lborel"
        using Mg'
        apply (intro nn_integral_suminf[symmetric])
        apply (rule borel_measurable_times_ennreal, simp add: mult.commute set_borel_measurable_def)
        apply (rule borel_measurable_indicator, subst sets_lborel)
        apply (simp_all split: split_indicator add: derivg_nonneg)
        done
      also have "(\x i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \ g -` f i) x) =
                      (\<lambda>x i. ennreal (g' x * indicator {a..b} x) * indicator (g -` f i) x)"
        by (intro ext) (simp split: split_indicator)
      also have "(\\<^sup>+ x. (\i. ennreal (g' x * indicator {a..b} x) * indicator (g -` f i) x) \lborel) =
                     \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) * (\<Sum>i. indicator (g -` f i) x) \<partial>lborel"
        by (intro nn_integral_cong) (auto split: split_indicator simp: derivg_nonneg)
      also from union have "(\x. \i. indicator (g -` f i) x :: ennreal) = (\x. indicator (\i. g -` f i) x)"
        by (intro ext suminf_indicator) (auto simp: disjoint_family_on_def)
      also have "(\\<^sup>+x. ennreal (g' x * indicator {a..b} x) * ... x \lborel) =
                    (\<integral>\<^sup>+x. indicator (\<Union>i. f i) (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)"
       by (intro nn_integral_cong) (simp split: split_indicator)
      finally show ?case .
  qed

next
  case (mult f c)
    note Mf[measurable] = \<open>f \<in> borel_measurable borel\<close>
    let ?I = "indicator {a..b}"
    have "(\x. f (g x * ?I x) * ennreal (g' x * ?I x)) \ borel_measurable borel" using Mg Mg'
      by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
         (simp_all add: mult.commute set_borel_measurable_def)
    also have "(\x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\x. f (g x) * ennreal (g' x) * ?I x)"
      by (intro ext) (simp split: split_indicator)
    finally have Mf': "(\x. f (g x) * ennreal (g' x) * ?I x) \ borel_measurable borel" .
    with mult show ?case
      by (subst (1 2 3) mult_ac, subst (1 2) nn_integral_cmult) (simp_all add: mult_ac)

next
  case (add f2 f1)
    let ?I = "indicator {a..b}"
    {
      fix f :: "real \ ennreal" assume Mf: "f \ borel_measurable borel"
      have "(\x. f (g x * ?I x) * ennreal (g' x * ?I x)) \ borel_measurable borel" using Mg Mg'
        by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf])
           (simp_all add:  mult.commute set_borel_measurable_def)
      also have "(\x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\x. f (g x) * ennreal (g' x) * ?I x)"
        by (intro ext) (simp split: split_indicator)
      finally have "(\x. f (g x) * ennreal (g' x) * ?I x) \ borel_measurable borel" .
    } note Mf' = this[OF \f1 \ borel_measurable borel\] this[OF \f2 \ borel_measurable borel\]

    have "(\\<^sup>+ x. (f1 x + f2 x) * indicator {g a..g b} x \lborel) =
             (\<integral>\<^sup>+ x. f1 x * indicator {g a..g b} x + f2 x * indicator {g a..g b} x \<partial>lborel)"
      by (intro nn_integral_cong) (simp split: split_indicator)
    also from add have "... = (\\<^sup>+ x. f1 (g x) * ennreal (g' x) * indicator {a..b} x \lborel) +
                                (\<integral>\<^sup>+ x. f2 (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)"
      by (simp_all add: nn_integral_add)
    also from add have "... = (\\<^sup>+ x. f1 (g x) * ennreal (g' x) * indicator {a..b} x +
                                      f2 (g x) * ennreal (g' x) * indicator {a..b} x \lborel)"
      by (intro nn_integral_add[symmetric])
         (auto simp add: Mf' derivg_nonneg split: split_indicator)
    also have "... = \\<^sup>+ x. (f1 (g x) + f2 (g x)) * ennreal (g' x) * indicator {a..b} x \lborel"
      by (intro nn_integral_cong) (simp split: split_indicator add: distrib_right)
    finally show ?case .

next
  case (sup F)
  {
    fix i
    let ?I = "indicator {a..b}"
    have "(\x. F i (g x * ?I x) * ennreal (g' x * ?I x)) \ borel_measurable borel" using Mg Mg'
      by (rule_tac borel_measurable_times_ennreal, rule_tac measurable_compose[OF _ sup.hyps(1)])
         (simp_all add: mult.commute set_borel_measurable_def)
    also have "(\x. F i (g x * ?I x) * ennreal (g' x * ?I x)) = (\x. F i (g x) * ennreal (g' x) * ?I x)"
      by (intro ext) (simp split: split_indicator)
     finally have "... \ borel_measurable borel" .
  } note Mf' = this

    have "(\\<^sup>+x. (SUP i. F i x) * indicator {g a..g b} x \lborel) =
               \<integral>\<^sup>+x. (SUP i. F i x* indicator {g a..g b} x) \<partial>lborel"
      by (intro nn_integral_cong) (simp split: split_indicator)
    also from sup have "... = (SUP i. \\<^sup>+x. F i x* indicator {g a..g b} x \lborel)"
      by (intro nn_integral_monotone_convergence_SUP)
         (auto simp: incseq_def le_fun_def split: split_indicator)
    also from sup have "... = (SUP i. \\<^sup>+x. F i (g x) * ennreal (g' x) * indicator {a..b} x \lborel)"
      by simp
    also from sup have "... = \\<^sup>+x. (SUP i. F i (g x) * ennreal (g' x) * indicator {a..b} x) \lborel"
      by (intro nn_integral_monotone_convergence_SUP[symmetric])
         (auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator
               intro!: mult_right_mono)
    also from sup have "... = \\<^sup>+x. (SUP i. F i (g x)) * ennreal (g' x) * indicator {a..b} x \lborel"
      by (subst mult.assoc, subst mult.commute, subst SUP_mult_left_ennreal)
         (auto split: split_indicator simp: derivg_nonneg mult_ac)
    finally show ?case by (simp add: image_comp)
  qed
qed

theorem nn_integral_substitution:
  fixes f :: "real \ real"
  assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f"
  assumes derivg: "\x. x \ {a..b} \ (g has_real_derivative g' x) (at x)"
  assumes contg': "continuous_on {a..b} g'"
  assumes derivg_nonneg: "\x. x \ {a..b} \ g' x \ 0"
  assumes "a \ b"
  shows "(\\<^sup>+x. f x * indicator {g a..g b} x \lborel) =
             (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
proof (cases "a = b")
  assume "a \ b"
  with \<open>a \<le> b\<close> have "a < b" by auto
  let ?f' = "\x. f x * indicator {g a..g b} x"

  from derivg derivg_nonneg have monog: "\x y. a \ x \ x \ y \ y \ b \ g x \ g y"
    by (rule deriv_nonneg_imp_mono) simp_all
  have bounds: "\x. x \ a \ x \ b \ g x \ g a" "\x. x \ a \ x \ b \ g x \ g b"
    by (auto intro: monog)

  from derivg_nonneg have nonneg:
    "\f x. x \ a \ x \ b \ g' x \ 0 \ f x * ennreal (g' x) \ 0 \ f x \ 0"
    by (force simp: field_simps)
  have nonneg': "\x. a \ x \ x \ b \ \ 0 \ f (g x) \ 0 \ f (g x) * g' x \ g' x = 0"
    by (metis atLeastAtMost_iff derivg_nonneg eq_iff mult_eq_0_iff mult_le_0_iff)

  have "(\\<^sup>+x. f x * indicator {g a..g b} x \lborel) =
            (\<integral>\<^sup>+x. ennreal (?f' x) * indicator {g a..g b} x \<partial>lborel)"
    by (intro nn_integral_cong)
       (auto split: split_indicator split_max simp: zero_ennreal.rep_eq ennreal_neg)
  also have "... = \\<^sup>+ x. ?f' (g x) * ennreal (g' x) * indicator {a..b} x \lborel" using Mf
    by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg \a < b\])
       (auto simp add: mult.commute set_borel_measurable_def)
  also have "... = \\<^sup>+ x. f (g x) * ennreal (g' x) * indicator {a..b} x \lborel"
    by (intro nn_integral_cong) (auto split: split_indicator simp: max_def dest: bounds)
  also have "... = \\<^sup>+x. ennreal (f (g x) * g' x * indicator {a..b} x) \lborel"
    by (intro nn_integral_cong) (auto simp: mult.commute derivg_nonneg ennreal_mult' split: split_indicator)
  finally show ?thesis .
qed auto

theorem integral_substitution:
  assumes integrable: "set_integrable lborel {g a..g b} f"
  assumes derivg: "\x. x \ {a..b} \ (g has_real_derivative g' x) (at x)"
  assumes contg': "continuous_on {a..b} g'"
  assumes derivg_nonneg: "\x. x \ {a..b} \ g' x \ 0"
  assumes "a \ b"
  shows "set_integrable lborel {a..b} (\x. f (g x) * g' x)"
    and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)"
proof-
  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
  with contg' have Mg: "set_borel_measurable borel {a..b} g"
    and Mg': "set_borel_measurable borel {a..b} g'"
    using atLeastAtMost_borel set_measurable_continuous_on by blast+
  from derivg derivg_nonneg have monog: "\x y. a \ x \ x \ y \ y \ b \ g x \ g y"
    by (rule deriv_nonneg_imp_mono) simp_all

  have "(\x. ennreal (f x) * indicator {g a..g b} x) =
           (\<lambda>x. ennreal (f x * indicator {g a..g b} x))"
    by (intro ext) (simp split: split_indicator)
  with integrable have M1: "(\x. f x * indicator {g a..g b} x) \ borel_measurable borel"
    by (force simp: mult.commute set_integrable_def)
  from integrable have M2: "(\x. -f x * indicator {g a..g b} x) \ borel_measurable borel"
    by (force simp: mult.commute set_integrable_def)

  have "(LBINT x. (f x :: real) * indicator {g a..g b} x) =
          enn2real (\<integral>\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) -
          enn2real (\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
    unfolding set_integrable_def
    by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute)
  also have *: "(\\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \lborel) =
      (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)"
    by (intro nn_integral_cong) (simp split: split_indicator)
  also from M1 * have A: "(\\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \lborel) =
                            (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
    by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \a \ b\])
       (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)
  also have **: "(\\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \lborel) =
      (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
    by (intro nn_integral_cong) (simp split: split_indicator)
  also from M2 ** have B: "(\\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \lborel) =
        (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
    by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \a \ b\])
       (auto simp: nn_integral_set_ennreal mult.commute set_borel_measurable_def)

  also {
    from integrable have Mf: "set_borel_measurable borel {g a..g b} f"
      unfolding set_borel_measurable_def set_integrable_def by simp
    from measurable_compose Mg Mf Mg' borel_measurable_times
    have "(\x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
                     (g' x * indicator {a..b} x)) \ borel_measurable borel" (is "?f \ _")
      by (simp add: mult.commute set_borel_measurable_def)
    also have "?f = (\x. f (g x) * g' x * indicator {a..b} x)"
      using monog by (intro ext) (auto split: split_indicator)
    finally show "set_integrable lborel {a..b} (\x. f (g x) * g' x)"
      using A B integrable unfolding real_integrable_def set_integrable_def
      by (simp_all add: nn_integral_set_ennreal mult.commute)
  } note integrable' = this

  have "enn2real (\\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \lborel) -
                  enn2real (\<integral>\<^sup>+ x. ennreal (-f (g x) * g' x * indicator {a..b} x) \<partial>lborel) =
                (LBINT x. f (g x) * g' x * indicator {a..b} x)"
    using integrable' unfolding set_integrable_def
    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

theorem interval_integral_substitution:
  assumes integrable: "set_integrable lborel {g a..g b} f"
  assumes derivg: "\x. x \ {a..b} \ (g has_real_derivative g' x) (at x)"
  assumes contg': "continuous_on {a..b} g'"
  assumes derivg_nonneg: "\x. x \ {a..b} \ g' x \ 0"
  assumes "a \ b"
  shows "set_integrable lborel {a..b} (\x. f (g x) * g' x)"
    and "(LBINT x=g a..g b. f x) = (LBINT x=a..b. f (g x) * g' x)"
  apply (rule integral_substitution[OF assms], simp, simp)
  apply (subst (1 2) interval_integral_Icc, fact)
  apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact)
  using integral_substitution(2)[OF assms]
  apply (simp add: mult.commute set_lebesgue_integral_def)
  done

lemma set_borel_integrable_singleton[simp]: "set_integrable lborel {x} (f :: real \ real)"
  unfolding set_integrable_def
  by (subst integrable_discrete_difference[where X="{x}" and g="\_. 0"]) auto

end

quality100%

¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.