src/HOL/Probability/Lebesgue_Integral_Substitution.thy
author hoelzl
Thu Jan 22 14:51:08 2015 +0100 (2015-01-22)
changeset 59425 c5e79df8cc21
parent 59092 d469103c0737
child 59452 2538b2c51769
permissions -rw-r--r--
import general thms from Density_Compiler
hoelzl@59092
     1
(*  Title:      HOL/Probability/Lebesgue_Integral_Substitution.thy
hoelzl@59092
     2
    Author:     Manuel Eberl
hoelzl@59092
     3
hoelzl@59092
     4
    Provides lemmas for integration by substitution for the basic integral types.
hoelzl@59092
     5
    Note that the substitution function must have a nonnegative derivative.
hoelzl@59092
     6
    This could probably be weakened somehow.
hoelzl@59092
     7
*)
hoelzl@59092
     8
hoelzl@59092
     9
section {* Integration by Substition *}
hoelzl@59092
    10
hoelzl@59092
    11
theory Lebesgue_Integral_Substitution
hoelzl@59092
    12
imports Interval_Integral
hoelzl@59092
    13
begin
hoelzl@59092
    14
hoelzl@59092
    15
lemma measurable_sets_borel:
hoelzl@59092
    16
    "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel"
hoelzl@59092
    17
  by (drule (1) measurable_sets) simp
hoelzl@59092
    18
hoelzl@59092
    19
lemma closure_Iii: 
hoelzl@59092
    20
  assumes "a < b"
hoelzl@59092
    21
  shows "closure {a<..<b::real} = {a..b}"
hoelzl@59092
    22
proof-
hoelzl@59092
    23
  have "{a<..<b} = ball ((a+b)/2) ((b-a)/2)" by (auto simp: dist_real_def field_simps not_less)
hoelzl@59092
    24
  also from assms have "closure ... = cball ((a+b)/2) ((b-a)/2)" by (intro closure_ball) simp
hoelzl@59092
    25
  also have "... = {a..b}" by (auto simp: dist_real_def field_simps not_less)
hoelzl@59092
    26
  finally show ?thesis .
hoelzl@59092
    27
qed
hoelzl@59092
    28
hoelzl@59092
    29
lemma continuous_ge_on_Iii:
hoelzl@59092
    30
  assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}"
hoelzl@59092
    31
  shows "g (x::real) \<ge> (a::real)"
hoelzl@59092
    32
proof-
hoelzl@59092
    33
  from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_Iii[symmetric])
hoelzl@59092
    34
  also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto
hoelzl@59092
    35
  hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono)
hoelzl@59092
    36
  also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
hoelzl@59092
    37
    by (auto simp: continuous_on_closed_vimage)
hoelzl@59092
    38
  hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
hoelzl@59092
    39
  finally show ?thesis using `x \<in> {c..d}` by auto 
hoelzl@59092
    40
qed 
hoelzl@59092
    41
hoelzl@59092
    42
lemma interior_real_semiline':
hoelzl@59092
    43
  fixes a :: real
hoelzl@59092
    44
  shows "interior {..a} = {..<a}"
hoelzl@59092
    45
proof -
hoelzl@59092
    46
  {
hoelzl@59092
    47
    fix y
hoelzl@59092
    48
    assume "a > y"
hoelzl@59092
    49
    then have "y \<in> interior {..a}"
hoelzl@59092
    50
      apply (simp add: mem_interior)
hoelzl@59092
    51
      apply (rule_tac x="(a-y)" in exI)
hoelzl@59092
    52
      apply (auto simp add: dist_norm)
hoelzl@59092
    53
      done
hoelzl@59092
    54
  }
hoelzl@59092
    55
  moreover
hoelzl@59092
    56
  {
hoelzl@59092
    57
    fix y
hoelzl@59092
    58
    assume "y \<in> interior {..a}"
hoelzl@59092
    59
    then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
hoelzl@59092
    60
      using mem_interior_cball[of y "{..a}"] by auto
hoelzl@59092
    61
    moreover from e have "y + e \<in> cball y e"
hoelzl@59092
    62
      by (auto simp add: cball_def dist_norm)
hoelzl@59092
    63
    ultimately have "a \<ge> y + e" by auto
hoelzl@59092
    64
    then have "a > y" using e by auto
hoelzl@59092
    65
  }
hoelzl@59092
    66
  ultimately show ?thesis by auto
hoelzl@59092
    67
qed
hoelzl@59092
    68
hoelzl@59092
    69
lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
hoelzl@59092
    70
proof-
hoelzl@59092
    71
  have "{a..b} = {a..} \<inter> {..b}" by auto
hoelzl@59092
    72
  also have "interior ... = {a<..} \<inter> {..<b}" 
hoelzl@59092
    73
    by (simp add: interior_real_semiline interior_real_semiline')
hoelzl@59092
    74
  also have "... = {a<..<b}" by auto
hoelzl@59092
    75
  finally show ?thesis .
hoelzl@59092
    76
qed
hoelzl@59092
    77
hoelzl@59092
    78
lemma nn_integral_indicator_singleton[simp]:
hoelzl@59092
    79
  assumes [measurable]: "{y} \<in> sets M"
hoelzl@59092
    80
  shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}"
hoelzl@59092
    81
proof-
hoelzl@59092
    82
  have "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = (\<integral>\<^sup>+x. max 0 (f y) * indicator {y} x \<partial>M)"
hoelzl@59092
    83
    by (subst nn_integral_max_0[symmetric]) (auto intro!: nn_integral_cong split: split_indicator)
hoelzl@59092
    84
  then show ?thesis
hoelzl@59092
    85
    by (simp add: nn_integral_cmult)
hoelzl@59092
    86
qed
hoelzl@59092
    87
hoelzl@59092
    88
lemma nn_integral_set_ereal:
hoelzl@59092
    89
  "(\<integral>\<^sup>+x. ereal (f x) * indicator A x \<partial>M) = (\<integral>\<^sup>+x. ereal (f x * indicator A x) \<partial>M)"
hoelzl@59092
    90
  by (rule nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
    91
hoelzl@59092
    92
lemma nn_integral_indicator_singleton'[simp]:
hoelzl@59092
    93
  assumes [measurable]: "{y} \<in> sets M"
hoelzl@59092
    94
  shows "(\<integral>\<^sup>+x. ereal (f x * indicator {y} x) \<partial>M) = max 0 (f y) * emeasure M {y}"
hoelzl@59092
    95
  by (subst nn_integral_set_ereal[symmetric]) simp
hoelzl@59092
    96
hoelzl@59092
    97
lemma set_borel_measurable_sets:
hoelzl@59092
    98
  fixes f :: "_ \<Rightarrow> _::real_normed_vector"
hoelzl@59092
    99
  assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
hoelzl@59092
   100
  shows "f -` B \<inter> X \<in> sets M"
hoelzl@59092
   101
proof -
hoelzl@59092
   102
  have "f \<in> borel_measurable (restrict_space M X)"
hoelzl@59092
   103
    using assms by (subst borel_measurable_restrict_space_iff) auto
hoelzl@59092
   104
  then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
hoelzl@59092
   105
    by (rule measurable_sets) fact
hoelzl@59092
   106
  with `X \<in> sets M` show ?thesis
hoelzl@59092
   107
    by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
hoelzl@59092
   108
qed
hoelzl@59092
   109
hoelzl@59092
   110
lemma borel_set_induct[consumes 1, case_names empty interval compl union]:
hoelzl@59092
   111
  assumes "A \<in> sets borel" 
hoelzl@59092
   112
  assumes empty: "P {}" and int: "\<And>a b. a \<le> b \<Longrightarrow> P {a..b}" and compl: "\<And>A. A \<in> sets borel \<Longrightarrow> P A \<Longrightarrow> P (-A)" and
hoelzl@59092
   113
          un: "\<And>f. disjoint_family f \<Longrightarrow> (\<And>i. f i \<in> sets borel) \<Longrightarrow>  (\<And>i. P (f i)) \<Longrightarrow> P (\<Union>i::nat. f i)"
hoelzl@59092
   114
  shows "P (A::real set)"
hoelzl@59092
   115
proof-
hoelzl@59092
   116
  let ?G = "range (\<lambda>(a,b). {a..b::real})"
hoelzl@59092
   117
  have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G" 
hoelzl@59092
   118
      using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def)
hoelzl@59092
   119
  thus ?thesis
hoelzl@59092
   120
  proof (induction rule: sigma_sets_induct_disjoint) 
hoelzl@59092
   121
    case (union f)
hoelzl@59092
   122
      from union.hyps(2) have "\<And>i. f i \<in> sets borel" by (auto simp: borel_eq_atLeastAtMost)
hoelzl@59092
   123
      with union show ?case by (auto intro: un)
hoelzl@59092
   124
  next
hoelzl@59092
   125
    case (basic A)
hoelzl@59092
   126
    then obtain a b where "A = {a .. b}" by auto
hoelzl@59092
   127
    then show ?case
hoelzl@59092
   128
      by (cases "a \<le> b") (auto intro: int empty)
hoelzl@59092
   129
  qed (auto intro: empty compl simp: Compl_eq_Diff_UNIV[symmetric] borel_eq_atLeastAtMost)
hoelzl@59092
   130
qed
hoelzl@59092
   131
hoelzl@59092
   132
definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
hoelzl@59092
   133
hoelzl@59092
   134
lemma mono_onI:
hoelzl@59092
   135
  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on f A"
hoelzl@59092
   136
  unfolding mono_on_def by simp
hoelzl@59092
   137
hoelzl@59092
   138
lemma mono_onD:
hoelzl@59092
   139
  "\<lbrakk>mono_on f A; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
hoelzl@59092
   140
  unfolding mono_on_def by simp
hoelzl@59092
   141
hoelzl@59092
   142
lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on f A"
hoelzl@59092
   143
  unfolding mono_def mono_on_def by auto
hoelzl@59092
   144
hoelzl@59092
   145
lemma mono_on_subset: "mono_on f A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on f B"
hoelzl@59092
   146
  unfolding mono_on_def by auto
hoelzl@59092
   147
hoelzl@59092
   148
definition "strict_mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s"
hoelzl@59092
   149
hoelzl@59092
   150
lemma strict_mono_onI:
hoelzl@59092
   151
  "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on f A"
hoelzl@59092
   152
  unfolding strict_mono_on_def by simp
hoelzl@59092
   153
hoelzl@59092
   154
lemma strict_mono_onD:
hoelzl@59092
   155
  "\<lbrakk>strict_mono_on f A; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
hoelzl@59092
   156
  unfolding strict_mono_on_def by simp
hoelzl@59092
   157
hoelzl@59092
   158
lemma mono_on_greaterD:
hoelzl@59092
   159
  assumes "mono_on g A" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
hoelzl@59092
   160
  shows "x > y"
hoelzl@59092
   161
proof (rule ccontr)
hoelzl@59092
   162
  assume "\<not>x > y"
hoelzl@59092
   163
  hence "x \<le> y" by (simp add: not_less)
hoelzl@59092
   164
  from assms(1-3) and this have "g x \<le> g y" by (rule mono_onD)
hoelzl@59092
   165
  with assms(4) show False by simp
hoelzl@59092
   166
qed
hoelzl@59092
   167
hoelzl@59092
   168
lemma strict_mono_inv:
hoelzl@59092
   169
  fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)"
hoelzl@59092
   170
  assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x"
hoelzl@59092
   171
  shows "strict_mono g"
hoelzl@59092
   172
proof
hoelzl@59092
   173
  fix x y :: 'b assume "x < y"
hoelzl@59092
   174
  from `surj f` obtain x' y' where [simp]: "x = f x'" "y = f y'" by blast
hoelzl@59092
   175
  with `x < y` and `strict_mono f` have "x' < y'" by (simp add: strict_mono_less)
hoelzl@59092
   176
  with inv show "g x < g y" by simp
hoelzl@59092
   177
qed
hoelzl@59092
   178
hoelzl@59092
   179
lemma strict_mono_on_imp_inj_on:
hoelzl@59092
   180
  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> (_ :: preorder)) A"
hoelzl@59092
   181
  shows "inj_on f A"
hoelzl@59092
   182
proof (rule inj_onI)
hoelzl@59092
   183
  fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
hoelzl@59092
   184
  thus "x = y"
hoelzl@59092
   185
    by (cases x y rule: linorder_cases)
hoelzl@59092
   186
       (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) 
hoelzl@59092
   187
qed
hoelzl@59092
   188
hoelzl@59092
   189
lemma strict_mono_on_leD:
hoelzl@59092
   190
  assumes "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A" "x \<in> A" "y \<in> A" "x \<le> y"
hoelzl@59092
   191
  shows "f x \<le> f y"
hoelzl@59092
   192
proof (insert le_less_linear[of y x], elim disjE)
hoelzl@59092
   193
  assume "x < y"
hoelzl@59092
   194
  with assms have "f x < f y" by (rule_tac strict_mono_onD[OF assms(1)]) simp_all
hoelzl@59092
   195
  thus ?thesis by (rule less_imp_le)
hoelzl@59092
   196
qed (insert assms, simp)
hoelzl@59092
   197
hoelzl@59092
   198
lemma strict_mono_on_eqD:
hoelzl@59092
   199
  fixes f :: "(_ :: linorder) \<Rightarrow> (_ :: preorder)"
hoelzl@59092
   200
  assumes "strict_mono_on f A" "f x = f y" "x \<in> A" "y \<in> A"
hoelzl@59092
   201
  shows "y = x"
hoelzl@59092
   202
  using assms by (rule_tac linorder_cases[of x y]) (auto dest: strict_mono_onD)
hoelzl@59092
   203
hoelzl@59092
   204
lemma mono_on_imp_deriv_nonneg:
hoelzl@59092
   205
  assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
hoelzl@59092
   206
  assumes "x \<in> interior A"
hoelzl@59092
   207
  shows "D \<ge> 0"
hoelzl@59092
   208
proof (rule tendsto_le_const)
hoelzl@59092
   209
  let ?A' = "(\<lambda>y. y - x) ` interior A"
hoelzl@59092
   210
  from deriv show "((\<lambda>h. (f (x + h) - f x) / h) ---> D) (at 0)"
hoelzl@59092
   211
      by (simp add: field_has_derivative_at has_field_derivative_def)
hoelzl@59092
   212
  from mono have mono': "mono_on f (interior A)" by (rule mono_on_subset) (rule interior_subset)
hoelzl@59092
   213
hoelzl@59092
   214
  show "eventually (\<lambda>h. (f (x + h) - f x) / h \<ge> 0) (at 0)"
hoelzl@59092
   215
  proof (subst eventually_at_topological, intro exI conjI ballI impI)
hoelzl@59092
   216
    have "open (interior A)" by simp
hoelzl@59092
   217
    hence "open (op + (-x) ` interior A)" by (rule open_translation)
hoelzl@59092
   218
    also have "(op + (-x) ` interior A) = ?A'" by auto
hoelzl@59092
   219
    finally show "open ?A'" .
hoelzl@59092
   220
  next
hoelzl@59092
   221
    from `x \<in> interior A` show "0 \<in> ?A'" by auto
hoelzl@59092
   222
  next
hoelzl@59092
   223
    fix h assume "h \<in> ?A'"
hoelzl@59092
   224
    hence "x + h \<in> interior A" by auto
hoelzl@59092
   225
    with mono' and `x \<in> interior A` show "(f (x + h) - f x) / h \<ge> 0"
hoelzl@59092
   226
      by (cases h rule: linorder_cases[of _ 0])
hoelzl@59092
   227
         (simp_all add: divide_nonpos_neg divide_nonneg_pos mono_onD field_simps)
hoelzl@59092
   228
  qed
hoelzl@59092
   229
qed simp
hoelzl@59092
   230
hoelzl@59092
   231
lemma strict_mono_on_imp_mono_on: 
hoelzl@59092
   232
  "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A"
hoelzl@59092
   233
  by (rule mono_onI, rule strict_mono_on_leD)
hoelzl@59092
   234
hoelzl@59092
   235
lemma has_real_derivative_imp_continuous_on:
hoelzl@59092
   236
  assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
hoelzl@59092
   237
  shows "continuous_on A f"
hoelzl@59092
   238
  apply (intro differentiable_imp_continuous_on, unfold differentiable_on_def)
hoelzl@59092
   239
  apply (intro ballI Deriv.differentiableI)
hoelzl@59092
   240
  apply (rule has_field_derivative_subset[OF assms])
hoelzl@59092
   241
  apply simp_all
hoelzl@59092
   242
  done
hoelzl@59092
   243
hoelzl@59092
   244
lemma closure_contains_Sup:
hoelzl@59092
   245
  fixes S :: "real set"
hoelzl@59092
   246
  assumes "S \<noteq> {}" "bdd_above S"
hoelzl@59092
   247
  shows "Sup S \<in> closure S"
hoelzl@59092
   248
proof-
hoelzl@59092
   249
  have "Inf (uminus ` S) \<in> closure (uminus ` S)" 
hoelzl@59092
   250
      using assms by (intro closure_contains_Inf) auto
hoelzl@59092
   251
  also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def)
hoelzl@59092
   252
  also have "closure (uminus ` S) = uminus ` closure S"
hoelzl@59092
   253
      by (rule sym, intro closure_injective_linear_image) (auto intro: linearI)
hoelzl@59092
   254
  finally show ?thesis by auto
hoelzl@59092
   255
qed
hoelzl@59092
   256
hoelzl@59092
   257
lemma closed_contains_Sup:
hoelzl@59092
   258
  fixes S :: "real set"
hoelzl@59092
   259
  shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
hoelzl@59092
   260
  by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
hoelzl@59092
   261
hoelzl@59092
   262
lemma deriv_nonneg_imp_mono:
hoelzl@59092
   263
  assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
hoelzl@59092
   264
  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
hoelzl@59092
   265
  assumes ab: "a \<le> b"
hoelzl@59092
   266
  shows "g a \<le> g b"
hoelzl@59092
   267
proof (cases "a < b")
hoelzl@59092
   268
  assume "a < b"
hoelzl@59092
   269
  from deriv have "\<forall>x. x \<ge> a \<and> x \<le> b \<longrightarrow> (g has_real_derivative g' x) (at x)" by simp
hoelzl@59092
   270
  from MVT2[OF `a < b` this] and deriv 
hoelzl@59092
   271
    obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
hoelzl@59092
   272
  from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
hoelzl@59092
   273
  with g_ab show ?thesis by simp
hoelzl@59092
   274
qed (insert ab, simp)
hoelzl@59092
   275
hoelzl@59092
   276
lemma continuous_interval_vimage_Int:
hoelzl@59092
   277
  assumes "continuous_on {a::real..b} g" and mono: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
hoelzl@59092
   278
  assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {g a..g b}"
hoelzl@59092
   279
  obtains c' d' where "{a..b} \<inter> g -` {c..d} = {c'..d'}" "c' \<le> d'" "g c' = c" "g d' = d"
hoelzl@59092
   280
proof-
hoelzl@59092
   281
    let ?A = "{a..b} \<inter> g -` {c..d}"
hoelzl@59092
   282
    from IVT'[of g a c b, OF _ _ `a \<le> b` assms(1)] assms(4,5) 
hoelzl@59092
   283
         obtain c'' where c'': "c'' \<in> ?A" "g c'' = c" by auto
hoelzl@59092
   284
    from IVT'[of g a d b, OF _ _ `a \<le> b` assms(1)] assms(4,5) 
hoelzl@59092
   285
         obtain d'' where d'': "d'' \<in> ?A" "g d'' = d" by auto
hoelzl@59092
   286
    hence [simp]: "?A \<noteq> {}" by blast
hoelzl@59092
   287
hoelzl@59092
   288
    def c' \<equiv> "Inf ?A" and d' \<equiv> "Sup ?A"
hoelzl@59092
   289
    have "?A \<subseteq> {c'..d'}" unfolding c'_def d'_def
hoelzl@59092
   290
        by (intro subsetI) (auto intro: cInf_lower cSup_upper)
hoelzl@59092
   291
    moreover from assms have "closed ?A" 
hoelzl@59092
   292
        using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp
hoelzl@59092
   293
    hence c'd'_in_set: "c' \<in> ?A" "d' \<in> ?A" unfolding c'_def d'_def
hoelzl@59092
   294
        by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+
hoelzl@59092
   295
    hence "{c'..d'} \<subseteq> ?A" using assms 
hoelzl@59092
   296
        by (intro subsetI)
hoelzl@59092
   297
           (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x] 
hoelzl@59092
   298
                 intro!: mono)
hoelzl@59092
   299
    moreover have "c' \<le> d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
hoelzl@59092
   300
    moreover have "g c' \<le> c" "g d' \<ge> d"
hoelzl@59092
   301
      apply (insert c'' d'' c'd'_in_set)
hoelzl@59092
   302
      apply (subst c''(2)[symmetric])
hoelzl@59092
   303
      apply (auto simp: c'_def intro!: mono cInf_lower c'') []
hoelzl@59092
   304
      apply (subst d''(2)[symmetric])
hoelzl@59092
   305
      apply (auto simp: d'_def intro!: mono cSup_upper d'') []
hoelzl@59092
   306
      done
hoelzl@59092
   307
    with c'd'_in_set have "g c' = c" "g d' = d" by auto
hoelzl@59092
   308
    ultimately show ?thesis using that by blast
hoelzl@59092
   309
qed
hoelzl@59092
   310
hoelzl@59092
   311
lemma nn_integral_substitution_aux:
hoelzl@59092
   312
  fixes f :: "real \<Rightarrow> ereal"
hoelzl@59092
   313
  assumes Mf: "f \<in> borel_measurable borel"
hoelzl@59092
   314
  assumes nonnegf: "\<And>x. f x \<ge> 0"
hoelzl@59092
   315
  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
hoelzl@59092
   316
  assumes contg': "continuous_on {a..b} g'" 
hoelzl@59092
   317
  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
hoelzl@59092
   318
  assumes "a < b"
hoelzl@59092
   319
  shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
hoelzl@59092
   320
             (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
hoelzl@59092
   321
proof-
hoelzl@59092
   322
  from `a < b` have [simp]: "a \<le> b" by simp
hoelzl@59092
   323
  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
hoelzl@59092
   324
  from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and 
hoelzl@59092
   325
                             Mg': "set_borel_measurable borel {a..b} g'" 
hoelzl@59092
   326
      by (simp_all only: set_measurable_continuous_on_ivl)
hoelzl@59092
   327
  from derivg have derivg': "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
hoelzl@59092
   328
    by (simp only: has_field_derivative_iff_has_vector_derivative)
hoelzl@59092
   329
hoelzl@59092
   330
  have real_ind[simp]: "\<And>A x. real (indicator A x :: ereal) = indicator A x" 
hoelzl@59092
   331
      by (auto split: split_indicator)
hoelzl@59092
   332
  have ereal_ind[simp]: "\<And>A x. ereal (indicator A x) = indicator A x" 
hoelzl@59092
   333
      by (auto split: split_indicator)
hoelzl@59092
   334
  have [simp]: "\<And>x A. indicator A (g x) = indicator (g -` A) x" 
hoelzl@59092
   335
      by (auto split: split_indicator)
hoelzl@59092
   336
hoelzl@59092
   337
  from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
hoelzl@59092
   338
    by (rule deriv_nonneg_imp_mono) simp_all
hoelzl@59092
   339
  with monog have [simp]: "g a \<le> g b" by (auto intro: mono_onD)
hoelzl@59092
   340
hoelzl@59092
   341
  show ?thesis
hoelzl@59092
   342
  proof (induction rule: borel_measurable_induct[OF Mf nonnegf, case_names cong set mult add sup])
hoelzl@59092
   343
    case (cong f1 f2)
hoelzl@59092
   344
    from cong.hyps(3) have "f1 = f2" by auto
hoelzl@59092
   345
    with cong show ?case by simp
hoelzl@59092
   346
  next
hoelzl@59092
   347
    case (set A)
hoelzl@59092
   348
    from set.hyps show ?case
hoelzl@59092
   349
    proof (induction rule: borel_set_induct)
hoelzl@59092
   350
      case empty
hoelzl@59092
   351
      thus ?case by simp
hoelzl@59092
   352
    next
hoelzl@59092
   353
      case (interval c d)
hoelzl@59092
   354
      {
hoelzl@59092
   355
        fix u v :: real assume asm: "{u..v} \<subseteq> {g a..g b}" "u \<le> v"
hoelzl@59092
   356
        
hoelzl@59092
   357
        obtain u' v' where u'v': "{a..b} \<inter> g-`{u..v} = {u'..v'}" "u' \<le> v'" "g u' = u" "g v' = v"
hoelzl@59092
   358
             using asm by (rule_tac continuous_interval_vimage_Int[OF contg monog, of u v]) simp_all
hoelzl@59092
   359
        hence "{u'..v'} \<subseteq> {a..b}" "{u'..v'} \<subseteq> g -` {u..v}" by blast+
hoelzl@59092
   360
        with u'v'(2) have "u' \<in> g -` {u..v}" "v' \<in> g -` {u..v}" by auto
hoelzl@59092
   361
        from u'v'(1) have [simp]: "{a..b} \<inter> g -` {u..v} \<in> sets borel" by simp
hoelzl@59092
   362
        
hoelzl@59092
   363
        have A: "continuous_on {min u' v'..max u' v'} g'"
hoelzl@59092
   364
            by (simp only: u'v' max_absorb2 min_absorb1) 
hoelzl@59092
   365
               (intro continuous_on_subset[OF contg'], insert u'v', auto)
hoelzl@59092
   366
        have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})"
hoelzl@59092
   367
           using asm by (intro has_field_derivative_subset[OF derivg] set_mp[OF `{u'..v'} \<subseteq> {a..b}`]) auto
hoelzl@59092
   368
        hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow> 
hoelzl@59092
   369
                      (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})" 
hoelzl@59092
   370
            by (simp only: u'v' max_absorb2 min_absorb1) 
hoelzl@59092
   371
               (auto simp: has_field_derivative_iff_has_vector_derivative)
hoelzl@59092
   372
        have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
hoelzl@59092
   373
          by (rule set_integrable_subset[OF borel_integrable_atLeastAtMost'[OF contg']]) simp_all
hoelzl@59092
   374
        hence "(\<integral>\<^sup>+x. ereal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) = 
hoelzl@59092
   375
                   LBINT x:{a..b} \<inter> g-`{u..v}. g' x" 
hoelzl@59092
   376
          by (subst ereal_ind[symmetric], subst times_ereal.simps, subst nn_integral_eq_integral)
hoelzl@59092
   377
             (auto intro: measurable_sets Mg simp: derivg_nonneg mult.commute split: split_indicator)
hoelzl@59092
   378
        also from interval_integral_FTC_finite[OF A B]
hoelzl@59092
   379
            have "LBINT x:{a..b} \<inter> g-`{u..v}. g' x = v - u"
hoelzl@59092
   380
                by (simp add: u'v' interval_integral_Icc `u \<le> v`)
hoelzl@59092
   381
        finally have "(\<integral>\<^sup>+ x. ereal (g' x) * indicator ({a..b} \<inter> g -` {u..v}) x \<partial>lborel) =
hoelzl@59092
   382
                           ereal (v - u)" .
hoelzl@59092
   383
      } note A = this
hoelzl@59092
   384
  
hoelzl@59092
   385
      have "(\<integral>\<^sup>+x. indicator {c..d} (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) =
hoelzl@59092
   386
               (\<integral>\<^sup>+ x. ereal (g' x) * indicator ({a..b} \<inter> g -` {c..d}) x \<partial>lborel)" 
hoelzl@59092
   387
        by (intro nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   388
      also have "{a..b} \<inter> g-`{c..d} = {a..b} \<inter> g-`{max (g a) c..min (g b) d}" 
hoelzl@59092
   389
        using `a \<le> b` `c \<le> d`
hoelzl@59092
   390
        by (auto intro!: monog intro: order.trans)
hoelzl@59092
   391
      also have "(\<integral>\<^sup>+ x. ereal (g' x) * indicator ... x \<partial>lborel) =
hoelzl@59092
   392
        (if max (g a) c \<le> min (g b) d then min (g b) d - max (g a) c else 0)"
hoelzl@59092
   393
         using `c \<le> d` by (simp add: A)
hoelzl@59092
   394
      also have "... = (\<integral>\<^sup>+ x. indicator ({g a..g b} \<inter> {c..d}) x \<partial>lborel)"
hoelzl@59092
   395
        by (subst nn_integral_indicator) (auto intro!: measurable_sets Mg simp:)
hoelzl@59092
   396
      also have "... = (\<integral>\<^sup>+ x. indicator {c..d} x * indicator {g a..g b} x \<partial>lborel)"
hoelzl@59092
   397
        by (intro nn_integral_cong) (auto split: split_indicator)
hoelzl@59092
   398
      finally show ?case ..
hoelzl@59092
   399
hoelzl@59092
   400
      next
hoelzl@59092
   401
hoelzl@59092
   402
      case (compl A)
hoelzl@59092
   403
      note `A \<in> sets borel`[measurable]
hoelzl@59092
   404
      from emeasure_mono[of "A \<inter> {g a..g b}" "{g a..g b}" lborel]
hoelzl@59092
   405
          have [simp]: "emeasure lborel (A \<inter> {g a..g b}) \<noteq> \<infinity>" by auto
hoelzl@59092
   406
      have [simp]: "g -` A \<inter> {a..b} \<in> sets borel"
hoelzl@59092
   407
        by (rule set_borel_measurable_sets[OF Mg]) auto
hoelzl@59092
   408
      have [simp]: "g -` (-A) \<inter> {a..b} \<in> sets borel"
hoelzl@59092
   409
        by (rule set_borel_measurable_sets[OF Mg]) auto
hoelzl@59092
   410
hoelzl@59092
   411
      have "(\<integral>\<^sup>+x. indicator (-A) x * indicator {g a..g b} x \<partial>lborel) = 
hoelzl@59092
   412
                (\<integral>\<^sup>+x. indicator (-A \<inter> {g a..g b}) x \<partial>lborel)" 
hoelzl@59092
   413
        by (rule nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   414
      also from compl have "... = emeasure lborel ({g a..g b} - A)" using derivg_nonneg
hoelzl@59092
   415
        by (simp add: vimage_Compl diff_eq Int_commute[of "-A"])
hoelzl@59092
   416
      also have "{g a..g b} - A = {g a..g b} - A \<inter> {g a..g b}" by blast
hoelzl@59092
   417
      also have "emeasure lborel ... = g b - g a - emeasure lborel (A \<inter> {g a..g b})"
hoelzl@59092
   418
             using `A \<in> sets borel` by (subst emeasure_Diff) (auto simp: real_of_ereal_minus)
hoelzl@59092
   419
     also have "emeasure lborel (A \<inter> {g a..g b}) = 
hoelzl@59092
   420
                    \<integral>\<^sup>+x. indicator A x * indicator {g a..g b} x \<partial>lborel" 
hoelzl@59092
   421
       using `A \<in> sets borel`
hoelzl@59092
   422
       by (subst nn_integral_indicator[symmetric], simp, intro nn_integral_cong)
hoelzl@59092
   423
          (simp split: split_indicator)
hoelzl@59092
   424
      also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I")
hoelzl@59092
   425
        by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   426
      also have "g b - g a = LBINT x:{a..b}. g' x" using derivg'
hoelzl@59092
   427
        by (intro integral_FTC_atLeastAtMost[symmetric])
hoelzl@59092
   428
           (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg]
hoelzl@59092
   429
                 has_vector_derivative_at_within)
hoelzl@59092
   430
      also have "ereal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel"
hoelzl@59092
   431
        using borel_integrable_atLeastAtMost'[OF contg']
hoelzl@59092
   432
        by (subst nn_integral_eq_integral)
hoelzl@59092
   433
           (simp_all add: mult.commute derivg_nonneg split: split_indicator)
hoelzl@59092
   434
      also have Mg'': "(\<lambda>x. indicator (g -` A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x))
hoelzl@59092
   435
                            \<in> borel_measurable borel" using Mg'
hoelzl@59092
   436
        by (intro borel_measurable_ereal_times borel_measurable_indicator)
hoelzl@59092
   437
           (simp_all add: mult.commute)
hoelzl@59092
   438
      have le: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel) \<le>
hoelzl@59092
   439
                        (\<integral>\<^sup>+x. ereal (g' x) * indicator {a..b} x \<partial>lborel)"
hoelzl@59092
   440
         by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg)
hoelzl@59092
   441
      note integrable = borel_integrable_atLeastAtMost'[OF contg']
hoelzl@59092
   442
      with le have notinf: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel) \<noteq> \<infinity>"
hoelzl@59092
   443
          by (auto simp: real_integrable_def nn_integral_set_ereal mult.commute)
hoelzl@59092
   444
      have "(\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel) - ?I = 
hoelzl@59092
   445
                  \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) - 
hoelzl@59092
   446
                        indicator (g -` A \<inter> {a..b}) x * ereal (g' x * indicator {a..b} x) \<partial>lborel"
hoelzl@59092
   447
        apply (intro nn_integral_diff[symmetric])
hoelzl@59092
   448
        apply (insert Mg', simp add: mult.commute) []
hoelzl@59092
   449
        apply (insert Mg'', simp) []
hoelzl@59092
   450
        apply (simp split: split_indicator add: derivg_nonneg)
hoelzl@59092
   451
        apply (rule notinf)
hoelzl@59092
   452
        apply (simp split: split_indicator add: derivg_nonneg)
hoelzl@59092
   453
        done
hoelzl@59092
   454
      also have "... = \<integral>\<^sup>+ x. indicator (-A) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
hoelzl@59092
   455
        by (intro nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   456
      finally show ?case .
hoelzl@59092
   457
hoelzl@59092
   458
    next
hoelzl@59092
   459
      case (union f)
hoelzl@59092
   460
      then have [simp]: "\<And>i. {a..b} \<inter> g -` f i \<in> sets borel"
hoelzl@59092
   461
        by (subst Int_commute, intro set_borel_measurable_sets[OF Mg]) auto
hoelzl@59092
   462
      have "g -` (\<Union>i. f i) \<inter> {a..b} = (\<Union>i. {a..b} \<inter> g -` f i)" by auto
hoelzl@59092
   463
      hence "g -` (\<Union>i. f i) \<inter> {a..b} \<in> sets borel" by (auto simp del: UN_simps)
hoelzl@59092
   464
hoelzl@59092
   465
      have "(\<integral>\<^sup>+x. indicator (\<Union>i. f i) x * indicator {g a..g b} x \<partial>lborel) = 
hoelzl@59092
   466
                \<integral>\<^sup>+x. indicator (\<Union>i. {g a..g b} \<inter> f i) x \<partial>lborel"
hoelzl@59092
   467
          by (intro nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   468
      also from union have "... = emeasure lborel (\<Union>i. {g a..g b} \<inter> f i)" by simp
hoelzl@59092
   469
      also from union have "... = (\<Sum>i. emeasure lborel ({g a..g b} \<inter> f i))"
hoelzl@59092
   470
        by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def)
hoelzl@59092
   471
      also from union have "... = (\<Sum>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel)" by simp
hoelzl@59092
   472
      also have "(\<lambda>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel) = 
hoelzl@59092
   473
                           (\<lambda>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel)"
hoelzl@59092
   474
        by (intro ext nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   475
      also from union.IH have "(\<Sum>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel) = 
hoelzl@59092
   476
          (\<Sum>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)" by simp
hoelzl@59092
   477
      also have "(\<lambda>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) =
hoelzl@59092
   478
                         (\<lambda>i. \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x \<partial>lborel)"
hoelzl@59092
   479
        by (intro ext nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   480
      also have "(\<Sum>i. ... i) = \<integral>\<^sup>+ x. (\<Sum>i. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) \<partial>lborel"
hoelzl@59092
   481
        using Mg'
hoelzl@59092
   482
        apply (intro nn_integral_suminf[symmetric])
hoelzl@59092
   483
        apply (rule borel_measurable_ereal_times, simp add: borel_measurable_ereal mult.commute)
hoelzl@59092
   484
        apply (rule borel_measurable_indicator, subst sets_lborel)
hoelzl@59092
   485
        apply (simp_all split: split_indicator add: derivg_nonneg)
hoelzl@59092
   486
        done
hoelzl@59092
   487
      also have "(\<lambda>x i. ereal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) =
hoelzl@59092
   488
                      (\<lambda>x i. ereal (g' x * indicator {a..b} x) * indicator (g -` f i) x)"
hoelzl@59092
   489
        by (intro ext) (simp split: split_indicator)
hoelzl@59092
   490
      also have "(\<integral>\<^sup>+ x. (\<Sum>i. ereal (g' x * indicator {a..b} x) * indicator (g -` f i) x) \<partial>lborel) =
hoelzl@59092
   491
                     \<integral>\<^sup>+ x. ereal (g' x * indicator {a..b} x) * (\<Sum>i. indicator (g -` f i) x) \<partial>lborel"
hoelzl@59092
   492
        by (intro nn_integral_cong suminf_cmult_ereal) (auto split: split_indicator simp: derivg_nonneg)
hoelzl@59092
   493
      also from union have "(\<lambda>x. \<Sum>i. indicator (g -` f i) x :: ereal) = (\<lambda>x. indicator (\<Union>i. g -` f i) x)"
hoelzl@59092
   494
        by (intro ext suminf_indicator) (auto simp: disjoint_family_on_def)
hoelzl@59092
   495
      also have "(\<integral>\<^sup>+x. ereal (g' x * indicator {a..b} x) * ... x \<partial>lborel) =
hoelzl@59092
   496
                    (\<integral>\<^sup>+x. indicator (\<Union>i. f i) (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
hoelzl@59092
   497
       by (intro nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   498
      finally show ?case .
hoelzl@59092
   499
  qed
hoelzl@59092
   500
hoelzl@59092
   501
next
hoelzl@59092
   502
  case (mult f c)
hoelzl@59092
   503
    note Mf[measurable] = `f \<in> borel_measurable borel`
hoelzl@59092
   504
    let ?I = "indicator {a..b}"
hoelzl@59092
   505
    have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
hoelzl@59092
   506
      by (intro borel_measurable_ereal_times measurable_compose[OF _ Mf])
hoelzl@59092
   507
         (simp_all add: borel_measurable_ereal mult.commute)
hoelzl@59092
   508
    also have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. f (g x) * ereal (g' x) * ?I x)"
hoelzl@59092
   509
      by (intro ext) (simp split: split_indicator)
hoelzl@59092
   510
    finally have Mf': "(\<lambda>x. f (g x) * ereal (g' x) * ?I x) \<in> borel_measurable borel" .
hoelzl@59092
   511
    with mult show ?case
hoelzl@59092
   512
      by (subst (1 2 3) mult_ac, subst (1 2) nn_integral_cmult) (simp_all add: mult_ac)
hoelzl@59092
   513
 
hoelzl@59092
   514
next
hoelzl@59092
   515
  case (add f2 f1)
hoelzl@59092
   516
    let ?I = "indicator {a..b}"
hoelzl@59092
   517
    {
hoelzl@59092
   518
      fix f :: "real \<Rightarrow> ereal" assume Mf: "f \<in> borel_measurable borel"
hoelzl@59092
   519
      have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
hoelzl@59092
   520
        by (intro borel_measurable_ereal_times measurable_compose[OF _ Mf])
hoelzl@59092
   521
           (simp_all add: borel_measurable_ereal mult.commute)
hoelzl@59092
   522
      also have "(\<lambda>x. f (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. f (g x) * ereal (g' x) * ?I x)"
hoelzl@59092
   523
        by (intro ext) (simp split: split_indicator)
hoelzl@59092
   524
      finally have "(\<lambda>x. f (g x) * ereal (g' x) * ?I x) \<in> borel_measurable borel" .
hoelzl@59092
   525
    } note Mf' = this[OF `f1 \<in> borel_measurable borel`] this[OF `f2 \<in> borel_measurable borel`]
hoelzl@59092
   526
    from add have not_neginf: "\<And>x. f1 x \<noteq> -\<infinity>" "\<And>x. f2 x \<noteq> -\<infinity>" 
hoelzl@59092
   527
      by (metis Infty_neq_0(1) ereal_0_le_uminus_iff ereal_infty_less_eq(1))+
hoelzl@59092
   528
hoelzl@59092
   529
    have "(\<integral>\<^sup>+ x. (f1 x + f2 x) * indicator {g a..g b} x \<partial>lborel) =
hoelzl@59092
   530
             (\<integral>\<^sup>+ x. f1 x * indicator {g a..g b} x + f2 x * indicator {g a..g b} x \<partial>lborel)"
hoelzl@59092
   531
      by (intro nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   532
    also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel) +
hoelzl@59092
   533
                                (\<integral>\<^sup>+ x. f2 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
hoelzl@59092
   534
      by (simp_all add: nn_integral_add)
hoelzl@59092
   535
    also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ereal (g' x) * indicator {a..b} x + 
hoelzl@59092
   536
                                      f2 (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
hoelzl@59092
   537
      by (intro nn_integral_add[symmetric])
hoelzl@59092
   538
         (auto simp add: Mf' derivg_nonneg split: split_indicator)
hoelzl@59092
   539
    also from not_neginf have "... = \<integral>\<^sup>+ x. (f1 (g x) + f2 (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
hoelzl@59092
   540
      by (intro nn_integral_cong) (simp split: split_indicator add: ereal_distrib)
hoelzl@59092
   541
    finally show ?case .
hoelzl@59092
   542
hoelzl@59092
   543
next
hoelzl@59092
   544
  case (sup F)
hoelzl@59092
   545
  {
hoelzl@59092
   546
    fix i
hoelzl@59092
   547
    let ?I = "indicator {a..b}"
hoelzl@59092
   548
    have "(\<lambda>x. F i (g x * ?I x) * ereal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg'
hoelzl@59092
   549
      by (rule_tac borel_measurable_ereal_times, rule_tac measurable_compose[OF _ sup.hyps(1)])
hoelzl@59092
   550
         (simp_all add: mult.commute)
hoelzl@59092
   551
    also have "(\<lambda>x. F i (g x * ?I x) * ereal (g' x * ?I x)) = (\<lambda>x. F i (g x) * ereal (g' x) * ?I x)"
hoelzl@59092
   552
      by (intro ext) (simp split: split_indicator)
hoelzl@59092
   553
     finally have "... \<in> borel_measurable borel" .
hoelzl@59092
   554
  } note Mf' = this
hoelzl@59092
   555
hoelzl@59092
   556
    have "(\<integral>\<^sup>+x. (SUP i. F i x) * indicator {g a..g b} x \<partial>lborel) = 
hoelzl@59092
   557
               \<integral>\<^sup>+x. (SUP i. F i x* indicator {g a..g b} x) \<partial>lborel"
hoelzl@59092
   558
      by (intro nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   559
    also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i x* indicator {g a..g b} x \<partial>lborel)"
hoelzl@59092
   560
      by (intro nn_integral_monotone_convergence_SUP)
hoelzl@59092
   561
         (auto simp: incseq_def le_fun_def split: split_indicator)
hoelzl@59092
   562
    also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel)"
hoelzl@59092
   563
      by simp
hoelzl@59092
   564
    also from sup have "... =  \<integral>\<^sup>+x. (SUP i. F i (g x) * ereal (g' x) * indicator {a..b} x) \<partial>lborel"
hoelzl@59092
   565
      by (intro nn_integral_monotone_convergence_SUP[symmetric])
hoelzl@59092
   566
         (auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator
hoelzl@59092
   567
               intro!: ereal_mult_right_mono)
hoelzl@59092
   568
    also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
hoelzl@59092
   569
      by (subst mult.assoc, subst mult.commute, subst SUP_ereal_cmult)
hoelzl@59092
   570
         (auto split: split_indicator simp: derivg_nonneg mult_ac)
hoelzl@59092
   571
    finally show ?case by simp
hoelzl@59092
   572
  qed
hoelzl@59092
   573
qed
hoelzl@59092
   574
hoelzl@59092
   575
lemma nn_integral_substitution:
hoelzl@59092
   576
  fixes f :: "real \<Rightarrow> real"
hoelzl@59092
   577
  assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f"
hoelzl@59092
   578
  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
hoelzl@59092
   579
  assumes contg': "continuous_on {a..b} g'" 
hoelzl@59092
   580
  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
hoelzl@59092
   581
  assumes "a \<le> b"
hoelzl@59092
   582
  shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
hoelzl@59092
   583
             (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
hoelzl@59092
   584
proof (cases "a = b")
hoelzl@59092
   585
  assume "a \<noteq> b"
hoelzl@59092
   586
  with `a \<le> b` have "a < b" by auto
hoelzl@59092
   587
  let ?f' = "\<lambda>x. max 0 (f x * indicator {g a..g b} x)"
hoelzl@59092
   588
hoelzl@59092
   589
  from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
hoelzl@59092
   590
    by (rule deriv_nonneg_imp_mono) simp_all
hoelzl@59092
   591
  have bounds: "\<And>x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g x \<ge> g a" "\<And>x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g x \<le> g b"
hoelzl@59092
   592
    by (auto intro: monog)
hoelzl@59092
   593
hoelzl@59092
   594
  from derivg_nonneg have nonneg: 
hoelzl@59092
   595
    "\<And>f x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g' x \<noteq> 0 \<Longrightarrow> f x * ereal (g' x) \<ge> 0 \<Longrightarrow> f x \<ge> 0"
hoelzl@59092
   596
    by (force simp: ereal_zero_le_0_iff field_simps)
hoelzl@59092
   597
  have nonneg': "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<not> 0 \<le> f (g x) \<Longrightarrow> 0 \<le> f (g x) * g' x \<Longrightarrow> g' x = 0"
hoelzl@59092
   598
    by (metis atLeastAtMost_iff derivg_nonneg eq_iff mult_eq_0_iff mult_le_0_iff)
hoelzl@59092
   599
hoelzl@59092
   600
  have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 
hoelzl@59092
   601
            (\<integral>\<^sup>+x. ereal (?f' x) * indicator {g a..g b} x \<partial>lborel)"
hoelzl@59092
   602
    by (subst nn_integral_max_0[symmetric], intro nn_integral_cong) 
hoelzl@59092
   603
       (auto split: split_indicator simp: zero_ereal_def)
hoelzl@59092
   604
  also have "... = \<integral>\<^sup>+ x. ?f' (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel" using Mf
hoelzl@59092
   605
    by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg `a < b`]) 
hoelzl@59092
   606
       (auto simp add: zero_ereal_def mult.commute)
hoelzl@59092
   607
  also have "... = \<integral>\<^sup>+ x. max 0 (f (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
hoelzl@59092
   608
    by (intro nn_integral_cong) 
hoelzl@59092
   609
       (auto split: split_indicator simp: max_def dest: bounds)
hoelzl@59092
   610
  also have "... = \<integral>\<^sup>+ x. max 0 (f (g x) * ereal (g' x) * indicator {a..b} x) \<partial>lborel"
hoelzl@59092
   611
    by (intro nn_integral_cong)
hoelzl@59092
   612
       (auto simp: max_def derivg_nonneg split: split_indicator intro!: nonneg')
hoelzl@59092
   613
  also have "... = \<integral>\<^sup>+ x. f (g x) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
hoelzl@59092
   614
    by (rule nn_integral_max_0)
hoelzl@59092
   615
  also have "... = \<integral>\<^sup>+x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel"
hoelzl@59092
   616
    by (intro nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   617
  finally show ?thesis .
hoelzl@59092
   618
qed auto
hoelzl@59092
   619
hoelzl@59092
   620
lemma integral_substitution:
hoelzl@59092
   621
  assumes integrable: "set_integrable lborel {g a..g b} f"
hoelzl@59092
   622
  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
hoelzl@59092
   623
  assumes contg': "continuous_on {a..b} g'" 
hoelzl@59092
   624
  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
hoelzl@59092
   625
  assumes "a \<le> b"
hoelzl@59092
   626
  shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
hoelzl@59092
   627
    and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)"
hoelzl@59092
   628
proof-
hoelzl@59092
   629
  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
hoelzl@59092
   630
  from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and 
hoelzl@59092
   631
                             Mg': "set_borel_measurable borel {a..b} g'" 
hoelzl@59092
   632
      by (simp_all only: set_measurable_continuous_on_ivl)
hoelzl@59092
   633
  from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
hoelzl@59092
   634
    by (rule deriv_nonneg_imp_mono) simp_all
hoelzl@59092
   635
hoelzl@59092
   636
  have "(\<lambda>x. ereal (f x) * indicator {g a..g b} x) = 
hoelzl@59092
   637
           (\<lambda>x. ereal (f x * indicator {g a..g b} x))" 
hoelzl@59092
   638
    by (intro ext) (simp split: split_indicator)
hoelzl@59092
   639
  with integrable have M1: "(\<lambda>x. f x * indicator {g a..g b} x) \<in> borel_measurable borel"
hoelzl@59092
   640
    unfolding real_integrable_def by (force simp: mult.commute)
hoelzl@59092
   641
  have "(\<lambda>x. ereal (-f x) * indicator {g a..g b} x) = 
hoelzl@59092
   642
           (\<lambda>x. -ereal (f x * indicator {g a..g b} x))" 
hoelzl@59092
   643
    by (intro ext) (simp split: split_indicator)
hoelzl@59092
   644
  with integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel"
hoelzl@59092
   645
    unfolding real_integrable_def by (force simp: mult.commute)
hoelzl@59092
   646
hoelzl@59092
   647
  have "LBINT x. (f x :: real) * indicator {g a..g b} x = 
hoelzl@59092
   648
          real (\<integral>\<^sup>+ x. ereal (f x) * indicator {g a..g b} x \<partial>lborel) -
hoelzl@59092
   649
          real (\<integral>\<^sup>+ x. ereal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
hoelzl@59092
   650
    by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ereal mult.commute)
hoelzl@59092
   651
  also have "(\<integral>\<^sup>+x. ereal (f x) * indicator {g a..g b} x \<partial>lborel) =
hoelzl@59092
   652
               (\<integral>\<^sup>+x. ereal (f x * indicator {g a..g b} x) \<partial>lborel)"
hoelzl@59092
   653
    by (intro nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   654
  also with M1 have A: "(\<integral>\<^sup>+ x. ereal (f x * indicator {g a..g b} x) \<partial>lborel) =
hoelzl@59092
   655
                            (\<integral>\<^sup>+ x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
hoelzl@59092
   656
    by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg `a \<le> b`]) 
hoelzl@59092
   657
       (auto simp: nn_integral_set_ereal mult.commute)
hoelzl@59092
   658
  also have "(\<integral>\<^sup>+ x. ereal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
hoelzl@59092
   659
               (\<integral>\<^sup>+ x. ereal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
hoelzl@59092
   660
    by (intro nn_integral_cong) (simp split: split_indicator)
hoelzl@59092
   661
  also with M2 have B: "(\<integral>\<^sup>+ x. ereal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
hoelzl@59092
   662
                            (\<integral>\<^sup>+ x. ereal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
hoelzl@59092
   663
    by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg `a \<le> b`])
hoelzl@59092
   664
       (auto simp: nn_integral_set_ereal mult.commute)
hoelzl@59092
   665
hoelzl@59092
   666
  also {
hoelzl@59092
   667
    from integrable have Mf: "set_borel_measurable borel {g a..g b} f" 
hoelzl@59092
   668
      unfolding real_integrable_def by simp
hoelzl@59092
   669
    from borel_measurable_times[OF measurable_compose[OF Mg Mf] Mg']
hoelzl@59092
   670
      have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) *
hoelzl@59092
   671
                     (g' x * indicator {a..b} x)) \<in> borel_measurable borel"  (is "?f \<in> _") 
hoelzl@59092
   672
      by (simp add: mult.commute)
hoelzl@59092
   673
    also have "?f = (\<lambda>x. f (g x) * g' x * indicator {a..b} x)"
hoelzl@59092
   674
      using monog by (intro ext) (auto split: split_indicator)
hoelzl@59092
   675
    finally show "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
hoelzl@59092
   676
      using A B integrable unfolding real_integrable_def 
hoelzl@59092
   677
      by (simp_all add: nn_integral_set_ereal mult.commute)
hoelzl@59092
   678
  } note integrable' = this
hoelzl@59092
   679
hoelzl@59092
   680
  have "real (\<integral>\<^sup>+ x. ereal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel) -
hoelzl@59092
   681
                  real (\<integral>\<^sup>+ x. ereal (-f (g x) * g' x * indicator {a..b} x) \<partial>lborel) =
hoelzl@59092
   682
                (LBINT x. f (g x) * g' x * indicator {a..b} x)" using integrable'
hoelzl@59092
   683
    by (subst real_lebesgue_integral_def) (simp_all add: field_simps)
hoelzl@59092
   684
  finally show "(LBINT x. f x * indicator {g a..g b} x) = 
hoelzl@59092
   685
                     (LBINT x. f (g x) * g' x * indicator {a..b} x)" .
hoelzl@59092
   686
qed
hoelzl@59092
   687
hoelzl@59092
   688
lemma interval_integral_substitution:
hoelzl@59092
   689
  assumes integrable: "set_integrable lborel {g a..g b} f"
hoelzl@59092
   690
  assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
hoelzl@59092
   691
  assumes contg': "continuous_on {a..b} g'" 
hoelzl@59092
   692
  assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
hoelzl@59092
   693
  assumes "a \<le> b"
hoelzl@59092
   694
  shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)"
hoelzl@59092
   695
    and "(LBINT x=g a..g b. f x) = (LBINT x=a..b. f (g x) * g' x)"
hoelzl@59092
   696
  apply (rule integral_substitution[OF assms], simp, simp)
hoelzl@59092
   697
  apply (subst (1 2) interval_integral_Icc, fact)
hoelzl@59092
   698
  apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact)
hoelzl@59092
   699
  using integral_substitution(2)[OF assms]
hoelzl@59092
   700
  apply (simp add: mult.commute)
hoelzl@59092
   701
  done
hoelzl@59092
   702
hoelzl@59092
   703
lemma set_borel_integrable_singleton[simp]:
hoelzl@59092
   704
  "set_integrable lborel {x} (f :: real \<Rightarrow> real)"
hoelzl@59092
   705
  by (subst integrable_discrete_difference[where X="{x}" and g="\<lambda>_. 0"]) auto
hoelzl@59092
   706
hoelzl@59092
   707
end