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