|
1 (* Title: HOL/Analysis/Lebesgue_Integral_Substitution.thy |
|
2 Author: Manuel Eberl |
|
3 |
|
4 Provides lemmas for integration by substitution for the basic integral types. |
|
5 Note that the substitution function must have a nonnegative derivative. |
|
6 This could probably be weakened somehow. |
|
7 *) |
|
8 |
|
9 section \<open>Integration by Substition\<close> |
|
10 |
|
11 theory Lebesgue_Integral_Substitution |
|
12 imports Interval_Integral |
|
13 begin |
|
14 |
|
15 lemma nn_integral_substitution_aux: |
|
16 fixes f :: "real \<Rightarrow> ennreal" |
|
17 assumes Mf: "f \<in> borel_measurable borel" |
|
18 assumes nonnegf: "\<And>x. f x \<ge> 0" |
|
19 assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" |
|
20 assumes contg': "continuous_on {a..b} g'" |
|
21 assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" |
|
22 assumes "a < b" |
|
23 shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = |
|
24 (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)" |
|
25 proof- |
|
26 from \<open>a < b\<close> have [simp]: "a \<le> b" by simp |
|
27 from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on) |
|
28 from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and |
|
29 Mg': "set_borel_measurable borel {a..b} g'" |
|
30 by (simp_all only: set_measurable_continuous_on_ivl) |
|
31 from derivg have derivg': "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)" |
|
32 by (simp only: has_field_derivative_iff_has_vector_derivative) |
|
33 |
|
34 have real_ind[simp]: "\<And>A x. enn2real (indicator A x) = indicator A x" |
|
35 by (auto split: split_indicator) |
|
36 have ennreal_ind[simp]: "\<And>A x. ennreal (indicator A x) = indicator A x" |
|
37 by (auto split: split_indicator) |
|
38 have [simp]: "\<And>x A. indicator A (g x) = indicator (g -` A) x" |
|
39 by (auto split: split_indicator) |
|
40 |
|
41 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" |
|
42 by (rule deriv_nonneg_imp_mono) simp_all |
|
43 with monog have [simp]: "g a \<le> g b" by (auto intro: mono_onD) |
|
44 |
|
45 show ?thesis |
|
46 proof (induction rule: borel_measurable_induct[OF Mf, case_names cong set mult add sup]) |
|
47 case (cong f1 f2) |
|
48 from cong.hyps(3) have "f1 = f2" by auto |
|
49 with cong show ?case by simp |
|
50 next |
|
51 case (set A) |
|
52 from set.hyps show ?case |
|
53 proof (induction rule: borel_set_induct) |
|
54 case empty |
|
55 thus ?case by simp |
|
56 next |
|
57 case (interval c d) |
|
58 { |
|
59 fix u v :: real assume asm: "{u..v} \<subseteq> {g a..g b}" "u \<le> v" |
|
60 |
|
61 obtain u' v' where u'v': "{a..b} \<inter> g-`{u..v} = {u'..v'}" "u' \<le> v'" "g u' = u" "g v' = v" |
|
62 using asm by (rule_tac continuous_interval_vimage_Int[OF contg monog, of u v]) simp_all |
|
63 hence "{u'..v'} \<subseteq> {a..b}" "{u'..v'} \<subseteq> g -` {u..v}" by blast+ |
|
64 with u'v'(2) have "u' \<in> g -` {u..v}" "v' \<in> g -` {u..v}" by auto |
|
65 from u'v'(1) have [simp]: "{a..b} \<inter> g -` {u..v} \<in> sets borel" by simp |
|
66 |
|
67 have A: "continuous_on {min u' v'..max u' v'} g'" |
|
68 by (simp only: u'v' max_absorb2 min_absorb1) |
|
69 (intro continuous_on_subset[OF contg'], insert u'v', auto) |
|
70 have "\<And>x. x \<in> {u'..v'} \<Longrightarrow> (g has_real_derivative g' x) (at x within {u'..v'})" |
|
71 using asm by (intro has_field_derivative_subset[OF derivg] set_mp[OF \<open>{u'..v'} \<subseteq> {a..b}\<close>]) auto |
|
72 hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow> |
|
73 (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})" |
|
74 by (simp only: u'v' max_absorb2 min_absorb1) |
|
75 (auto simp: has_field_derivative_iff_has_vector_derivative) |
|
76 have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)" |
|
77 by (rule set_integrable_subset[OF borel_integrable_atLeastAtMost'[OF contg']]) simp_all |
|
78 hence "(\<integral>\<^sup>+x. ennreal (g' x) * indicator ({a..b} \<inter> g-` {u..v}) x \<partial>lborel) = |
|
79 LBINT x:{a..b} \<inter> g-`{u..v}. g' x" |
|
80 by (subst nn_integral_eq_integral[symmetric]) |
|
81 (auto intro!: derivg_nonneg nn_integral_cong split: split_indicator) |
|
82 also from interval_integral_FTC_finite[OF A B] |
|
83 have "LBINT x:{a..b} \<inter> g-`{u..v}. g' x = v - u" |
|
84 by (simp add: u'v' interval_integral_Icc \<open>u \<le> v\<close>) |
|
85 finally have "(\<integral>\<^sup>+ x. ennreal (g' x) * indicator ({a..b} \<inter> g -` {u..v}) x \<partial>lborel) = |
|
86 ennreal (v - u)" . |
|
87 } note A = this |
|
88 |
|
89 have "(\<integral>\<^sup>+x. indicator {c..d} (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel) = |
|
90 (\<integral>\<^sup>+ x. ennreal (g' x) * indicator ({a..b} \<inter> g -` {c..d}) x \<partial>lborel)" |
|
91 by (intro nn_integral_cong) (simp split: split_indicator) |
|
92 also have "{a..b} \<inter> g-`{c..d} = {a..b} \<inter> g-`{max (g a) c..min (g b) d}" |
|
93 using \<open>a \<le> b\<close> \<open>c \<le> d\<close> |
|
94 by (auto intro!: monog intro: order.trans) |
|
95 also have "(\<integral>\<^sup>+ x. ennreal (g' x) * indicator ... x \<partial>lborel) = |
|
96 (if max (g a) c \<le> min (g b) d then min (g b) d - max (g a) c else 0)" |
|
97 using \<open>c \<le> d\<close> by (simp add: A) |
|
98 also have "... = (\<integral>\<^sup>+ x. indicator ({g a..g b} \<inter> {c..d}) x \<partial>lborel)" |
|
99 by (subst nn_integral_indicator) (auto intro!: measurable_sets Mg simp:) |
|
100 also have "... = (\<integral>\<^sup>+ x. indicator {c..d} x * indicator {g a..g b} x \<partial>lborel)" |
|
101 by (intro nn_integral_cong) (auto split: split_indicator) |
|
102 finally show ?case .. |
|
103 |
|
104 next |
|
105 |
|
106 case (compl A) |
|
107 note \<open>A \<in> sets borel\<close>[measurable] |
|
108 from emeasure_mono[of "A \<inter> {g a..g b}" "{g a..g b}" lborel] |
|
109 have [simp]: "emeasure lborel (A \<inter> {g a..g b}) \<noteq> top" by (auto simp: top_unique) |
|
110 have [simp]: "g -` A \<inter> {a..b} \<in> sets borel" |
|
111 by (rule set_borel_measurable_sets[OF Mg]) auto |
|
112 have [simp]: "g -` (-A) \<inter> {a..b} \<in> sets borel" |
|
113 by (rule set_borel_measurable_sets[OF Mg]) auto |
|
114 |
|
115 have "(\<integral>\<^sup>+x. indicator (-A) x * indicator {g a..g b} x \<partial>lborel) = |
|
116 (\<integral>\<^sup>+x. indicator (-A \<inter> {g a..g b}) x \<partial>lborel)" |
|
117 by (rule nn_integral_cong) (simp split: split_indicator) |
|
118 also from compl have "... = emeasure lborel ({g a..g b} - A)" using derivg_nonneg |
|
119 by (simp add: vimage_Compl diff_eq Int_commute[of "-A"]) |
|
120 also have "{g a..g b} - A = {g a..g b} - A \<inter> {g a..g b}" by blast |
|
121 also have "emeasure lborel ... = g b - g a - emeasure lborel (A \<inter> {g a..g b})" |
|
122 using \<open>A \<in> sets borel\<close> by (subst emeasure_Diff) (auto simp: ) |
|
123 also have "emeasure lborel (A \<inter> {g a..g b}) = |
|
124 \<integral>\<^sup>+x. indicator A x * indicator {g a..g b} x \<partial>lborel" |
|
125 using \<open>A \<in> sets borel\<close> |
|
126 by (subst nn_integral_indicator[symmetric], simp, intro nn_integral_cong) |
|
127 (simp split: split_indicator) |
|
128 also have "... = \<integral>\<^sup>+ x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel" (is "_ = ?I") |
|
129 by (subst compl.IH, intro nn_integral_cong) (simp split: split_indicator) |
|
130 also have "g b - g a = LBINT x:{a..b}. g' x" using derivg' |
|
131 by (intro integral_FTC_atLeastAtMost[symmetric]) |
|
132 (auto intro: continuous_on_subset[OF contg'] has_field_derivative_subset[OF derivg] |
|
133 has_vector_derivative_at_within) |
|
134 also have "ennreal ... = \<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel" |
|
135 using borel_integrable_atLeastAtMost'[OF contg'] |
|
136 by (subst nn_integral_eq_integral) |
|
137 (simp_all add: mult.commute derivg_nonneg split: split_indicator) |
|
138 also have Mg'': "(\<lambda>x. indicator (g -` A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x)) |
|
139 \<in> borel_measurable borel" using Mg' |
|
140 by (intro borel_measurable_times_ennreal borel_measurable_indicator) |
|
141 (simp_all add: mult.commute) |
|
142 have le: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel) \<le> |
|
143 (\<integral>\<^sup>+x. ennreal (g' x) * indicator {a..b} x \<partial>lborel)" |
|
144 by (intro nn_integral_mono) (simp split: split_indicator add: derivg_nonneg) |
|
145 note integrable = borel_integrable_atLeastAtMost'[OF contg'] |
|
146 with le have notinf: "(\<integral>\<^sup>+x. indicator (g-`A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel) \<noteq> top" |
|
147 by (auto simp: real_integrable_def nn_integral_set_ennreal mult.commute top_unique) |
|
148 have "(\<integral>\<^sup>+ x. g' x * indicator {a..b} x \<partial>lborel) - ?I = |
|
149 \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) - |
|
150 indicator (g -` A \<inter> {a..b}) x * ennreal (g' x * indicator {a..b} x) \<partial>lborel" |
|
151 apply (intro nn_integral_diff[symmetric]) |
|
152 apply (insert Mg', simp add: mult.commute) [] |
|
153 apply (insert Mg'', simp) [] |
|
154 apply (simp split: split_indicator add: derivg_nonneg) |
|
155 apply (rule notinf) |
|
156 apply (simp split: split_indicator add: derivg_nonneg) |
|
157 done |
|
158 also have "... = \<integral>\<^sup>+ x. indicator (-A) (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel" |
|
159 by (intro nn_integral_cong) (simp split: split_indicator) |
|
160 finally show ?case . |
|
161 |
|
162 next |
|
163 case (union f) |
|
164 then have [simp]: "\<And>i. {a..b} \<inter> g -` f i \<in> sets borel" |
|
165 by (subst Int_commute, intro set_borel_measurable_sets[OF Mg]) auto |
|
166 have "g -` (\<Union>i. f i) \<inter> {a..b} = (\<Union>i. {a..b} \<inter> g -` f i)" by auto |
|
167 hence "g -` (\<Union>i. f i) \<inter> {a..b} \<in> sets borel" by (auto simp del: UN_simps) |
|
168 |
|
169 have "(\<integral>\<^sup>+x. indicator (\<Union>i. f i) x * indicator {g a..g b} x \<partial>lborel) = |
|
170 \<integral>\<^sup>+x. indicator (\<Union>i. {g a..g b} \<inter> f i) x \<partial>lborel" |
|
171 by (intro nn_integral_cong) (simp split: split_indicator) |
|
172 also from union have "... = emeasure lborel (\<Union>i. {g a..g b} \<inter> f i)" by simp |
|
173 also from union have "... = (\<Sum>i. emeasure lborel ({g a..g b} \<inter> f i))" |
|
174 by (intro suminf_emeasure[symmetric]) (auto simp: disjoint_family_on_def) |
|
175 also from union have "... = (\<Sum>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel)" by simp |
|
176 also have "(\<lambda>i. \<integral>\<^sup>+x. indicator ({g a..g b} \<inter> f i) x \<partial>lborel) = |
|
177 (\<lambda>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel)" |
|
178 by (intro ext nn_integral_cong) (simp split: split_indicator) |
|
179 also from union.IH have "(\<Sum>i. \<integral>\<^sup>+x. indicator (f i) x * indicator {g a..g b} x \<partial>lborel) = |
|
180 (\<Sum>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)" by simp |
|
181 also have "(\<lambda>i. \<integral>\<^sup>+ x. indicator (f i) (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel) = |
|
182 (\<lambda>i. \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x \<partial>lborel)" |
|
183 by (intro ext nn_integral_cong) (simp split: split_indicator) |
|
184 also have "(\<Sum>i. ... i) = \<integral>\<^sup>+ x. (\<Sum>i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) \<partial>lborel" |
|
185 using Mg' |
|
186 apply (intro nn_integral_suminf[symmetric]) |
|
187 apply (rule borel_measurable_times_ennreal, simp add: mult.commute) |
|
188 apply (rule borel_measurable_indicator, subst sets_lborel) |
|
189 apply (simp_all split: split_indicator add: derivg_nonneg) |
|
190 done |
|
191 also have "(\<lambda>x i. ennreal (g' x * indicator {a..b} x) * indicator ({a..b} \<inter> g -` f i) x) = |
|
192 (\<lambda>x i. ennreal (g' x * indicator {a..b} x) * indicator (g -` f i) x)" |
|
193 by (intro ext) (simp split: split_indicator) |
|
194 also have "(\<integral>\<^sup>+ x. (\<Sum>i. ennreal (g' x * indicator {a..b} x) * indicator (g -` f i) x) \<partial>lborel) = |
|
195 \<integral>\<^sup>+ x. ennreal (g' x * indicator {a..b} x) * (\<Sum>i. indicator (g -` f i) x) \<partial>lborel" |
|
196 by (intro nn_integral_cong) (auto split: split_indicator simp: derivg_nonneg) |
|
197 also from union have "(\<lambda>x. \<Sum>i. indicator (g -` f i) x :: ennreal) = (\<lambda>x. indicator (\<Union>i. g -` f i) x)" |
|
198 by (intro ext suminf_indicator) (auto simp: disjoint_family_on_def) |
|
199 also have "(\<integral>\<^sup>+x. ennreal (g' x * indicator {a..b} x) * ... x \<partial>lborel) = |
|
200 (\<integral>\<^sup>+x. indicator (\<Union>i. f i) (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)" |
|
201 by (intro nn_integral_cong) (simp split: split_indicator) |
|
202 finally show ?case . |
|
203 qed |
|
204 |
|
205 next |
|
206 case (mult f c) |
|
207 note Mf[measurable] = \<open>f \<in> borel_measurable borel\<close> |
|
208 let ?I = "indicator {a..b}" |
|
209 have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg' |
|
210 by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf]) |
|
211 (simp_all add: mult.commute) |
|
212 also have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. f (g x) * ennreal (g' x) * ?I x)" |
|
213 by (intro ext) (simp split: split_indicator) |
|
214 finally have Mf': "(\<lambda>x. f (g x) * ennreal (g' x) * ?I x) \<in> borel_measurable borel" . |
|
215 with mult show ?case |
|
216 by (subst (1 2 3) mult_ac, subst (1 2) nn_integral_cmult) (simp_all add: mult_ac) |
|
217 |
|
218 next |
|
219 case (add f2 f1) |
|
220 let ?I = "indicator {a..b}" |
|
221 { |
|
222 fix f :: "real \<Rightarrow> ennreal" assume Mf: "f \<in> borel_measurable borel" |
|
223 have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg' |
|
224 by (intro borel_measurable_times_ennreal measurable_compose[OF _ Mf]) |
|
225 (simp_all add: mult.commute) |
|
226 also have "(\<lambda>x. f (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. f (g x) * ennreal (g' x) * ?I x)" |
|
227 by (intro ext) (simp split: split_indicator) |
|
228 finally have "(\<lambda>x. f (g x) * ennreal (g' x) * ?I x) \<in> borel_measurable borel" . |
|
229 } note Mf' = this[OF \<open>f1 \<in> borel_measurable borel\<close>] this[OF \<open>f2 \<in> borel_measurable borel\<close>] |
|
230 |
|
231 have "(\<integral>\<^sup>+ x. (f1 x + f2 x) * indicator {g a..g b} x \<partial>lborel) = |
|
232 (\<integral>\<^sup>+ x. f1 x * indicator {g a..g b} x + f2 x * indicator {g a..g b} x \<partial>lborel)" |
|
233 by (intro nn_integral_cong) (simp split: split_indicator) |
|
234 also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel) + |
|
235 (\<integral>\<^sup>+ x. f2 (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)" |
|
236 by (simp_all add: nn_integral_add) |
|
237 also from add have "... = (\<integral>\<^sup>+ x. f1 (g x) * ennreal (g' x) * indicator {a..b} x + |
|
238 f2 (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)" |
|
239 by (intro nn_integral_add[symmetric]) |
|
240 (auto simp add: Mf' derivg_nonneg split: split_indicator) |
|
241 also have "... = \<integral>\<^sup>+ x. (f1 (g x) + f2 (g x)) * ennreal (g' x) * indicator {a..b} x \<partial>lborel" |
|
242 by (intro nn_integral_cong) (simp split: split_indicator add: distrib_right) |
|
243 finally show ?case . |
|
244 |
|
245 next |
|
246 case (sup F) |
|
247 { |
|
248 fix i |
|
249 let ?I = "indicator {a..b}" |
|
250 have "(\<lambda>x. F i (g x * ?I x) * ennreal (g' x * ?I x)) \<in> borel_measurable borel" using Mg Mg' |
|
251 by (rule_tac borel_measurable_times_ennreal, rule_tac measurable_compose[OF _ sup.hyps(1)]) |
|
252 (simp_all add: mult.commute) |
|
253 also have "(\<lambda>x. F i (g x * ?I x) * ennreal (g' x * ?I x)) = (\<lambda>x. F i (g x) * ennreal (g' x) * ?I x)" |
|
254 by (intro ext) (simp split: split_indicator) |
|
255 finally have "... \<in> borel_measurable borel" . |
|
256 } note Mf' = this |
|
257 |
|
258 have "(\<integral>\<^sup>+x. (SUP i. F i x) * indicator {g a..g b} x \<partial>lborel) = |
|
259 \<integral>\<^sup>+x. (SUP i. F i x* indicator {g a..g b} x) \<partial>lborel" |
|
260 by (intro nn_integral_cong) (simp split: split_indicator) |
|
261 also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i x* indicator {g a..g b} x \<partial>lborel)" |
|
262 by (intro nn_integral_monotone_convergence_SUP) |
|
263 (auto simp: incseq_def le_fun_def split: split_indicator) |
|
264 also from sup have "... = (SUP i. \<integral>\<^sup>+x. F i (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel)" |
|
265 by simp |
|
266 also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x) * ennreal (g' x) * indicator {a..b} x) \<partial>lborel" |
|
267 by (intro nn_integral_monotone_convergence_SUP[symmetric]) |
|
268 (auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator |
|
269 intro!: mult_right_mono) |
|
270 also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ennreal (g' x) * indicator {a..b} x \<partial>lborel" |
|
271 by (subst mult.assoc, subst mult.commute, subst SUP_mult_left_ennreal) |
|
272 (auto split: split_indicator simp: derivg_nonneg mult_ac) |
|
273 finally show ?case by simp |
|
274 qed |
|
275 qed |
|
276 |
|
277 lemma nn_integral_substitution: |
|
278 fixes f :: "real \<Rightarrow> real" |
|
279 assumes Mf[measurable]: "set_borel_measurable borel {g a..g b} f" |
|
280 assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" |
|
281 assumes contg': "continuous_on {a..b} g'" |
|
282 assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" |
|
283 assumes "a \<le> b" |
|
284 shows "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = |
|
285 (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)" |
|
286 proof (cases "a = b") |
|
287 assume "a \<noteq> b" |
|
288 with \<open>a \<le> b\<close> have "a < b" by auto |
|
289 let ?f' = "\<lambda>x. f x * indicator {g a..g b} x" |
|
290 |
|
291 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" |
|
292 by (rule deriv_nonneg_imp_mono) simp_all |
|
293 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" |
|
294 by (auto intro: monog) |
|
295 |
|
296 from derivg_nonneg have nonneg: |
|
297 "\<And>f x. x \<ge> a \<Longrightarrow> x \<le> b \<Longrightarrow> g' x \<noteq> 0 \<Longrightarrow> f x * ennreal (g' x) \<ge> 0 \<Longrightarrow> f x \<ge> 0" |
|
298 by (force simp: field_simps) |
|
299 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" |
|
300 by (metis atLeastAtMost_iff derivg_nonneg eq_iff mult_eq_0_iff mult_le_0_iff) |
|
301 |
|
302 have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = |
|
303 (\<integral>\<^sup>+x. ennreal (?f' x) * indicator {g a..g b} x \<partial>lborel)" |
|
304 by (intro nn_integral_cong) |
|
305 (auto split: split_indicator split_max simp: zero_ennreal.rep_eq ennreal_neg) |
|
306 also have "... = \<integral>\<^sup>+ x. ?f' (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel" using Mf |
|
307 by (subst nn_integral_substitution_aux[OF _ _ derivg contg' derivg_nonneg \<open>a < b\<close>]) |
|
308 (auto simp add: mult.commute) |
|
309 also have "... = \<integral>\<^sup>+ x. f (g x) * ennreal (g' x) * indicator {a..b} x \<partial>lborel" |
|
310 by (intro nn_integral_cong) (auto split: split_indicator simp: max_def dest: bounds) |
|
311 also have "... = \<integral>\<^sup>+x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel" |
|
312 by (intro nn_integral_cong) (auto simp: mult.commute derivg_nonneg ennreal_mult' split: split_indicator) |
|
313 finally show ?thesis . |
|
314 qed auto |
|
315 |
|
316 lemma integral_substitution: |
|
317 assumes integrable: "set_integrable lborel {g a..g b} f" |
|
318 assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" |
|
319 assumes contg': "continuous_on {a..b} g'" |
|
320 assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" |
|
321 assumes "a \<le> b" |
|
322 shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)" |
|
323 and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)" |
|
324 proof- |
|
325 from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on) |
|
326 with contg' have Mg: "set_borel_measurable borel {a..b} g" |
|
327 and Mg': "set_borel_measurable borel {a..b} g'" |
|
328 by (simp_all only: set_measurable_continuous_on_ivl) |
|
329 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" |
|
330 by (rule deriv_nonneg_imp_mono) simp_all |
|
331 |
|
332 have "(\<lambda>x. ennreal (f x) * indicator {g a..g b} x) = |
|
333 (\<lambda>x. ennreal (f x * indicator {g a..g b} x))" |
|
334 by (intro ext) (simp split: split_indicator) |
|
335 with integrable have M1: "(\<lambda>x. f x * indicator {g a..g b} x) \<in> borel_measurable borel" |
|
336 unfolding real_integrable_def by (force simp: mult.commute) |
|
337 from integrable have M2: "(\<lambda>x. -f x * indicator {g a..g b} x) \<in> borel_measurable borel" |
|
338 unfolding real_integrable_def by (force simp: mult.commute) |
|
339 |
|
340 have "LBINT x. (f x :: real) * indicator {g a..g b} x = |
|
341 enn2real (\<integral>\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) - |
|
342 enn2real (\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable |
|
343 by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute) |
|
344 also have *: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) = |
|
345 (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)" |
|
346 by (intro nn_integral_cong) (simp split: split_indicator) |
|
347 also from M1 * have A: "(\<integral>\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel) = |
|
348 (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)" |
|
349 by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>]) |
|
350 (auto simp: nn_integral_set_ennreal mult.commute) |
|
351 also have **: "(\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel) = |
|
352 (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)" |
|
353 by (intro nn_integral_cong) (simp split: split_indicator) |
|
354 also from M2 ** have B: "(\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel) = |
|
355 (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)" |
|
356 by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>]) |
|
357 (auto simp: nn_integral_set_ennreal mult.commute) |
|
358 |
|
359 also { |
|
360 from integrable have Mf: "set_borel_measurable borel {g a..g b} f" |
|
361 unfolding real_integrable_def by simp |
|
362 from borel_measurable_times[OF measurable_compose[OF Mg Mf] Mg'] |
|
363 have "(\<lambda>x. f (g x * indicator {a..b} x) * indicator {g a..g b} (g x * indicator {a..b} x) * |
|
364 (g' x * indicator {a..b} x)) \<in> borel_measurable borel" (is "?f \<in> _") |
|
365 by (simp add: mult.commute) |
|
366 also have "?f = (\<lambda>x. f (g x) * g' x * indicator {a..b} x)" |
|
367 using monog by (intro ext) (auto split: split_indicator) |
|
368 finally show "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)" |
|
369 using A B integrable unfolding real_integrable_def |
|
370 by (simp_all add: nn_integral_set_ennreal mult.commute) |
|
371 } note integrable' = this |
|
372 |
|
373 have "enn2real (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel) - |
|
374 enn2real (\<integral>\<^sup>+ x. ennreal (-f (g x) * g' x * indicator {a..b} x) \<partial>lborel) = |
|
375 (LBINT x. f (g x) * g' x * indicator {a..b} x)" using integrable' |
|
376 by (subst real_lebesgue_integral_def) (simp_all add: field_simps) |
|
377 finally show "(LBINT x. f x * indicator {g a..g b} x) = |
|
378 (LBINT x. f (g x) * g' x * indicator {a..b} x)" . |
|
379 qed |
|
380 |
|
381 lemma interval_integral_substitution: |
|
382 assumes integrable: "set_integrable lborel {g a..g b} f" |
|
383 assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" |
|
384 assumes contg': "continuous_on {a..b} g'" |
|
385 assumes derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" |
|
386 assumes "a \<le> b" |
|
387 shows "set_integrable lborel {a..b} (\<lambda>x. f (g x) * g' x)" |
|
388 and "(LBINT x=g a..g b. f x) = (LBINT x=a..b. f (g x) * g' x)" |
|
389 apply (rule integral_substitution[OF assms], simp, simp) |
|
390 apply (subst (1 2) interval_integral_Icc, fact) |
|
391 apply (rule deriv_nonneg_imp_mono[OF derivg derivg_nonneg], simp, simp, fact) |
|
392 using integral_substitution(2)[OF assms] |
|
393 apply (simp add: mult.commute) |
|
394 done |
|
395 |
|
396 lemma set_borel_integrable_singleton[simp]: |
|
397 "set_integrable lborel {x} (f :: real \<Rightarrow> real)" |
|
398 by (subst integrable_discrete_difference[where X="{x}" and g="\<lambda>_. 0"]) auto |
|
399 |
|
400 end |