src/HOL/Analysis/Interval_Integral.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 69173 38beaaebe736 child 69678 0f4d4a13dc16 permissions -rw-r--r--
capitalize proper names in lemma names
 hoelzl@63627 ` 1` ```(* Title: HOL/Analysis/Interval_Integral.thy ``` hoelzl@63329 ` 2` ``` Author: Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU) ``` hoelzl@59092 ` 3` hoelzl@59092 ` 4` ```Lebesgue integral over an interval (with endpoints possibly +-\) ``` hoelzl@59092 ` 5` ```*) ``` hoelzl@59092 ` 6` hoelzl@59092 ` 7` ```theory Interval_Integral ``` hoelzl@63941 ` 8` ``` imports Equivalence_Lebesgue_Henstock_Integration ``` hoelzl@59092 ` 9` ```begin ``` hoelzl@59092 ` 10` ak2110@69173 ` 11` ```lemma%important continuous_on_vector_derivative: ``` hoelzl@59092 ` 12` ``` "(\x. x \ S \ (f has_vector_derivative f' x) (at x within S)) \ continuous_on S f" ``` ak2110@69173 ` 13` ``` by%unimportant (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous) ``` hoelzl@59092 ` 14` ak2110@69173 ` 15` ```definition%important "einterval a b = {x. a < ereal x \ ereal x < b}" ``` hoelzl@59092 ` 16` hoelzl@59092 ` 17` ```lemma einterval_eq[simp]: ``` hoelzl@59092 ` 18` ``` shows einterval_eq_Icc: "einterval (ereal a) (ereal b) = {a <..< b}" ``` hoelzl@59092 ` 19` ``` and einterval_eq_Ici: "einterval (ereal a) \ = {a <..}" ``` hoelzl@59092 ` 20` ``` and einterval_eq_Iic: "einterval (- \) (ereal b) = {..< b}" ``` hoelzl@59092 ` 21` ``` and einterval_eq_UNIV: "einterval (- \) \ = UNIV" ``` hoelzl@59092 ` 22` ``` by (auto simp: einterval_def) ``` hoelzl@59092 ` 23` hoelzl@59092 ` 24` ```lemma einterval_same: "einterval a a = {}" ``` lp15@68096 ` 25` ``` by (auto simp: einterval_def) ``` hoelzl@59092 ` 26` hoelzl@59092 ` 27` ```lemma einterval_iff: "x \ einterval a b \ a < ereal x \ ereal x < b" ``` hoelzl@59092 ` 28` ``` by (simp add: einterval_def) ``` hoelzl@59092 ` 29` hoelzl@59092 ` 30` ```lemma einterval_nonempty: "a < b \ \c. c \ einterval a b" ``` hoelzl@59092 ` 31` ``` by (cases a b rule: ereal2_cases, auto simp: einterval_def intro!: dense gt_ex lt_ex) ``` hoelzl@59092 ` 32` hoelzl@59092 ` 33` ```lemma open_einterval[simp]: "open (einterval a b)" ``` hoelzl@59092 ` 34` ``` by (cases a b rule: ereal2_cases) ``` hoelzl@59092 ` 35` ``` (auto simp: einterval_def intro!: open_Collect_conj open_Collect_less continuous_intros) ``` hoelzl@59092 ` 36` hoelzl@59092 ` 37` ```lemma borel_einterval[measurable]: "einterval a b \ sets borel" ``` hoelzl@59092 ` 38` ``` unfolding einterval_def by measurable ``` hoelzl@59092 ` 39` lp15@67974 ` 40` ```subsection\Approximating a (possibly infinite) interval\ ``` hoelzl@59092 ` 41` hoelzl@59092 ` 42` ```lemma filterlim_sup1: "(LIM x F. f x :> G1) \ (LIM x F. f x :> (sup G1 G2))" ``` hoelzl@59092 ` 43` ``` unfolding filterlim_def by (auto intro: le_supI1) ``` hoelzl@59092 ` 44` ak2110@69173 ` 45` ```lemma%important ereal_incseq_approx: ``` hoelzl@59092 ` 46` ``` fixes a b :: ereal ``` hoelzl@59092 ` 47` ``` assumes "a < b" ``` lp15@68095 ` 48` ``` obtains X :: "nat \ real" where "incseq X" "\i. a < X i" "\i. X i < b" "X \ b" ``` ak2110@69173 ` 49` ```proof%unimportant (cases b) ``` hoelzl@59092 ` 50` ``` case PInf ``` wenzelm@61808 ` 51` ``` with \a < b\ have "a = -\ \ (\r. a = ereal r)" ``` hoelzl@59092 ` 52` ``` by (cases a) auto ``` wenzelm@61969 ` 53` ``` moreover have "(\x. ereal (real (Suc x))) \ \" ``` lp15@68096 ` 54` ``` by (simp add: Lim_PInfty LIMSEQ_Suc_iff) (metis le_SucI of_nat_Suc of_nat_mono order_trans real_arch_simple) ``` wenzelm@61969 ` 55` ``` moreover have "\r. (\x. ereal (r + real (Suc x))) \ \" ``` lp15@68096 ` 56` ``` by (simp add: LIMSEQ_Suc_iff Lim_PInfty) (metis add.commute diff_le_eq nat_ceiling_le_eq) ``` hoelzl@59092 ` 57` ``` ultimately show thesis ``` lp15@61609 ` 58` ``` by (intro that[of "\i. real_of_ereal a + Suc i"]) ``` hoelzl@59092 ` 59` ``` (auto simp: incseq_def PInf) ``` hoelzl@59092 ` 60` ```next ``` hoelzl@59092 ` 61` ``` case (real b') ``` wenzelm@63040 ` 62` ``` define d where "d = b' - (if a = -\ then b' - 1 else real_of_ereal a)" ``` wenzelm@61808 ` 63` ``` with \a < b\ have a': "0 < d" ``` hoelzl@59092 ` 64` ``` by (cases a) (auto simp: real) ``` hoelzl@59092 ` 65` ``` moreover ``` hoelzl@59092 ` 66` ``` have "\i r. r < b' \ (b' - r) * 1 < (b' - r) * real (Suc (Suc i))" ``` hoelzl@59092 ` 67` ``` by (intro mult_strict_left_mono) auto ``` wenzelm@61808 ` 68` ``` with \a < b\ a' have "\i. a < ereal (b' - d / real (Suc (Suc i)))" ``` hoelzl@59092 ` 69` ``` by (cases a) (auto simp: real d_def field_simps) ``` lp15@68095 ` 70` ``` moreover ``` lp15@68095 ` 71` ``` have "(\i. b' - d / real i) \ b'" ``` lp15@68095 ` 72` ``` by (force intro: tendsto_eq_intros tendsto_divide_0[OF tendsto_const] filterlim_sup1 ``` lp15@68095 ` 73` ``` simp: at_infinity_eq_at_top_bot filterlim_real_sequentially) ``` lp15@68095 ` 74` ``` then have "(\i. b' - d / Suc (Suc i)) \ b'" ``` lp15@68095 ` 75` ``` by (blast intro: dest: filterlim_sequentially_Suc [THEN iffD2]) ``` hoelzl@59092 ` 76` ``` ultimately show thesis ``` hoelzl@59092 ` 77` ``` by (intro that[of "\i. b' - d / Suc (Suc i)"]) ``` lp15@68096 ` 78` ``` (auto simp: real incseq_def intro!: divide_left_mono) ``` wenzelm@61808 ` 79` ```qed (insert \a < b\, auto) ``` hoelzl@59092 ` 80` ak2110@69173 ` 81` ```lemma%important ereal_decseq_approx: ``` hoelzl@59092 ` 82` ``` fixes a b :: ereal ``` hoelzl@59092 ` 83` ``` assumes "a < b" ``` hoelzl@63329 ` 84` ``` obtains X :: "nat \ real" where ``` wenzelm@61969 ` 85` ``` "decseq X" "\i. a < X i" "\i. X i < b" "X \ a" ``` ak2110@69173 ` 86` ```proof%unimportant - ``` wenzelm@61808 ` 87` ``` have "-b < -a" using \a < b\ by simp ``` hoelzl@59092 ` 88` ``` from ereal_incseq_approx[OF this] guess X . ``` hoelzl@59092 ` 89` ``` then show thesis ``` hoelzl@59092 ` 90` ``` apply (intro that[of "\i. - X i"]) ``` nipkow@68403 ` 91` ``` apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps) ``` hoelzl@59092 ` 92` ``` apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+ ``` hoelzl@59092 ` 93` ``` done ``` hoelzl@59092 ` 94` ```qed ``` hoelzl@59092 ` 95` ak2110@69173 ` 96` ```lemma%important einterval_Icc_approximation: ``` hoelzl@59092 ` 97` ``` fixes a b :: ereal ``` hoelzl@59092 ` 98` ``` assumes "a < b" ``` hoelzl@63329 ` 99` ``` obtains u l :: "nat \ real" where ``` hoelzl@59092 ` 100` ``` "einterval a b = (\i. {l i .. u i})" ``` hoelzl@59092 ` 101` ``` "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" ``` wenzelm@61969 ` 102` ``` "l \ a" "u \ b" ``` ak2110@69173 ` 103` ```proof%unimportant - ``` wenzelm@61808 ` 104` ``` from dense[OF \a < b\] obtain c where "a < c" "c < b" by safe ``` wenzelm@61808 ` 105` ``` from ereal_incseq_approx[OF \c < b\] guess u . note u = this ``` wenzelm@61808 ` 106` ``` from ereal_decseq_approx[OF \a < c\] guess l . note l = this ``` wenzelm@61808 ` 107` ``` { fix i from less_trans[OF \l i < c\ \c < u i\] have "l i < u i" by simp } ``` hoelzl@59092 ` 108` ``` have "einterval a b = (\i. {l i .. u i})" ``` hoelzl@59092 ` 109` ``` proof (auto simp: einterval_iff) ``` hoelzl@59092 ` 110` ``` fix x assume "a < ereal x" "ereal x < b" ``` hoelzl@59092 ` 111` ``` have "eventually (\i. ereal (l i) < ereal x) sequentially" ``` wenzelm@61808 ` 112` ``` using l(4) \a < ereal x\ by (rule order_tendstoD) ``` hoelzl@63329 ` 113` ``` moreover ``` hoelzl@59092 ` 114` ``` have "eventually (\i. ereal x < ereal (u i)) sequentially" ``` wenzelm@61808 ` 115` ``` using u(4) \ereal x< b\ by (rule order_tendstoD) ``` hoelzl@59092 ` 116` ``` ultimately have "eventually (\i. l i < x \ x < u i) sequentially" ``` hoelzl@59092 ` 117` ``` by eventually_elim auto ``` hoelzl@59092 ` 118` ``` then show "\i. l i \ x \ x \ u i" ``` hoelzl@59092 ` 119` ``` by (auto intro: less_imp_le simp: eventually_sequentially) ``` hoelzl@59092 ` 120` ``` next ``` hoelzl@63329 ` 121` ``` fix x i assume "l i \ x" "x \ u i" ``` wenzelm@61808 ` 122` ``` with \a < ereal (l i)\ \ereal (u i) < b\ ``` hoelzl@59092 ` 123` ``` show "a < ereal x" "ereal x < b" ``` nipkow@68403 ` 124` ``` by (auto simp flip: ereal_less_eq(3)) ``` hoelzl@59092 ` 125` ``` qed ``` hoelzl@59092 ` 126` ``` show thesis ``` hoelzl@59092 ` 127` ``` by (intro that) fact+ ``` hoelzl@59092 ` 128` ```qed ``` hoelzl@59092 ` 129` hoelzl@63329 ` 130` ```(* TODO: in this definition, it would be more natural if einterval a b included a and b when ``` hoelzl@59092 ` 131` ``` they are real. *) ``` ak2110@69173 ` 132` ```definition%important interval_lebesgue_integral :: "real measure \ ereal \ ereal \ (real \ 'a) \ 'a::{banach, second_countable_topology}" where ``` hoelzl@59092 ` 133` ``` "interval_lebesgue_integral M a b f = ``` hoelzl@59092 ` 134` ``` (if a \ b then (LINT x:einterval a b|M. f x) else - (LINT x:einterval b a|M. f x))" ``` hoelzl@59092 ` 135` hoelzl@59092 ` 136` ```syntax ``` hoelzl@59092 ` 137` ``` "_ascii_interval_lebesgue_integral" :: "pttrn \ real \ real \ real measure \ real \ real" ``` hoelzl@59092 ` 138` ``` ("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60) ``` hoelzl@59092 ` 139` hoelzl@59092 ` 140` ```translations ``` hoelzl@59092 ` 141` ``` "LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\x. f)" ``` hoelzl@59092 ` 142` ak2110@69173 ` 143` ```definition%important interval_lebesgue_integrable :: "real measure \ ereal \ ereal \ (real \ 'a::{banach, second_countable_topology}) \ bool" where ``` hoelzl@59092 ` 144` ``` "interval_lebesgue_integrable M a b f = ``` hoelzl@59092 ` 145` ``` (if a \ b then set_integrable M (einterval a b) f else set_integrable M (einterval b a) f)" ``` hoelzl@59092 ` 146` hoelzl@59092 ` 147` ```syntax ``` hoelzl@59092 ` 148` ``` "_ascii_interval_lebesgue_borel_integral" :: "pttrn \ real \ real \ real \ real" ``` hoelzl@59092 ` 149` ``` ("(4LBINT _=_.._. _)" [0,60,60,61] 60) ``` hoelzl@59092 ` 150` hoelzl@59092 ` 151` ```translations ``` hoelzl@59092 ` 152` ``` "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\x. f)" ``` hoelzl@59092 ` 153` ak2110@69173 ` 154` ```subsection%important\Basic properties of integration over an interval\ ``` hoelzl@59092 ` 155` hoelzl@59092 ` 156` ```lemma interval_lebesgue_integral_cong: ``` hoelzl@59092 ` 157` ``` "a \ b \ (\x. x \ einterval a b \ f x = g x) \ einterval a b \ sets M \ ``` hoelzl@59092 ` 158` ``` interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g" ``` hoelzl@59092 ` 159` ``` by (auto intro: set_lebesgue_integral_cong simp: interval_lebesgue_integral_def) ``` hoelzl@59092 ` 160` hoelzl@59092 ` 161` ```lemma interval_lebesgue_integral_cong_AE: ``` hoelzl@59092 ` 162` ``` "f \ borel_measurable M \ g \ borel_measurable M \ ``` hoelzl@59092 ` 163` ``` a \ b \ AE x \ einterval a b in M. f x = g x \ einterval a b \ sets M \ ``` hoelzl@59092 ` 164` ``` interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g" ``` hoelzl@59092 ` 165` ``` by (auto intro: set_lebesgue_integral_cong_AE simp: interval_lebesgue_integral_def) ``` hoelzl@59092 ` 166` hoelzl@62083 ` 167` ```lemma interval_integrable_mirror: ``` hoelzl@62083 ` 168` ``` shows "interval_lebesgue_integrable lborel a b (\x. f (-x)) \ ``` hoelzl@62083 ` 169` ``` interval_lebesgue_integrable lborel (-b) (-a) f" ``` hoelzl@62083 ` 170` ```proof - ``` hoelzl@62083 ` 171` ``` have *: "indicator (einterval a b) (- x) = (indicator (einterval (-b) (-a)) x :: real)" ``` hoelzl@62083 ` 172` ``` for a b :: ereal and x :: real ``` hoelzl@62083 ` 173` ``` by (cases a b rule: ereal2_cases) (auto simp: einterval_def split: split_indicator) ``` hoelzl@62083 ` 174` ``` show ?thesis ``` hoelzl@62083 ` 175` ``` unfolding interval_lebesgue_integrable_def ``` hoelzl@62083 ` 176` ``` using lborel_integrable_real_affine_iff[symmetric, of "-1" "\x. indicator (einterval _ _) x *\<^sub>R f x" 0] ``` lp15@67974 ` 177` ``` by (simp add: * set_integrable_def) ``` hoelzl@62083 ` 178` ```qed ``` hoelzl@62083 ` 179` hoelzl@63329 ` 180` ```lemma interval_lebesgue_integral_add [intro, simp]: ``` hoelzl@63329 ` 181` ``` fixes M a b f ``` hoelzl@59092 ` 182` ``` assumes "interval_lebesgue_integrable M a b f" "interval_lebesgue_integrable M a b g" ``` hoelzl@63329 ` 183` ``` shows "interval_lebesgue_integrable M a b (\x. f x + g x)" and ``` hoelzl@63329 ` 184` ``` "interval_lebesgue_integral M a b (\x. f x + g x) = ``` hoelzl@59092 ` 185` ``` interval_lebesgue_integral M a b f + interval_lebesgue_integral M a b g" ``` lp15@68096 ` 186` ```using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def ``` hoelzl@59092 ` 187` ``` field_simps) ``` hoelzl@59092 ` 188` hoelzl@63329 ` 189` ```lemma interval_lebesgue_integral_diff [intro, simp]: ``` hoelzl@63329 ` 190` ``` fixes M a b f ``` hoelzl@59092 ` 191` ``` assumes "interval_lebesgue_integrable M a b f" ``` hoelzl@59092 ` 192` ``` "interval_lebesgue_integrable M a b g" ``` hoelzl@63329 ` 193` ``` shows "interval_lebesgue_integrable M a b (\x. f x - g x)" and ``` hoelzl@63329 ` 194` ``` "interval_lebesgue_integral M a b (\x. f x - g x) = ``` hoelzl@59092 ` 195` ``` interval_lebesgue_integral M a b f - interval_lebesgue_integral M a b g" ``` lp15@68096 ` 196` ```using assms by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def ``` hoelzl@59092 ` 197` ``` field_simps) ``` hoelzl@59092 ` 198` hoelzl@59092 ` 199` ```lemma interval_lebesgue_integrable_mult_right [intro, simp]: ``` hoelzl@59092 ` 200` ``` fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, second_countable_topology}" ``` hoelzl@59092 ` 201` ``` shows "(c \ 0 \ interval_lebesgue_integrable M a b f) \ ``` hoelzl@59092 ` 202` ``` interval_lebesgue_integrable M a b (\x. c * f x)" ``` hoelzl@59092 ` 203` ``` by (simp add: interval_lebesgue_integrable_def) ``` hoelzl@59092 ` 204` ak2110@69173 ` 205` ```lemma%important interval_lebesgue_integrable_mult_left [intro, simp]: ``` hoelzl@59092 ` 206` ``` fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, second_countable_topology}" ``` hoelzl@59092 ` 207` ``` shows "(c \ 0 \ interval_lebesgue_integrable M a b f) \ ``` hoelzl@59092 ` 208` ``` interval_lebesgue_integrable M a b (\x. f x * c)" ``` ak2110@69173 ` 209` ``` by%unimportant (simp add: interval_lebesgue_integrable_def) ``` hoelzl@59092 ` 210` ak2110@69173 ` 211` ```lemma%important interval_lebesgue_integrable_divide [intro, simp]: ``` haftmann@59867 ` 212` ``` fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, field, second_countable_topology}" ``` hoelzl@59092 ` 213` ``` shows "(c \ 0 \ interval_lebesgue_integrable M a b f) \ ``` hoelzl@59092 ` 214` ``` interval_lebesgue_integrable M a b (\x. f x / c)" ``` ak2110@69173 ` 215` ``` by%unimportant (simp add: interval_lebesgue_integrable_def) ``` hoelzl@59092 ` 216` hoelzl@59092 ` 217` ```lemma interval_lebesgue_integral_mult_right [simp]: ``` hoelzl@59092 ` 218` ``` fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, second_countable_topology}" ``` hoelzl@59092 ` 219` ``` shows "interval_lebesgue_integral M a b (\x. c * f x) = ``` hoelzl@59092 ` 220` ``` c * interval_lebesgue_integral M a b f" ``` hoelzl@59092 ` 221` ``` by (simp add: interval_lebesgue_integral_def) ``` hoelzl@59092 ` 222` ak2110@69173 ` 223` ```lemma%important interval_lebesgue_integral_mult_left [simp]: ``` hoelzl@59092 ` 224` ``` fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, second_countable_topology}" ``` hoelzl@59092 ` 225` ``` shows "interval_lebesgue_integral M a b (\x. f x * c) = ``` hoelzl@59092 ` 226` ``` interval_lebesgue_integral M a b f * c" ``` ak2110@69173 ` 227` ``` by%unimportant (simp add: interval_lebesgue_integral_def) ``` hoelzl@59092 ` 228` hoelzl@59092 ` 229` ```lemma interval_lebesgue_integral_divide [simp]: ``` haftmann@59867 ` 230` ``` fixes M a b c and f :: "real \ 'a::{banach, real_normed_field, field, second_countable_topology}" ``` hoelzl@59092 ` 231` ``` shows "interval_lebesgue_integral M a b (\x. f x / c) = ``` hoelzl@59092 ` 232` ``` interval_lebesgue_integral M a b f / c" ``` hoelzl@59092 ` 233` ``` by (simp add: interval_lebesgue_integral_def) ``` hoelzl@59092 ` 234` hoelzl@59092 ` 235` ```lemma interval_lebesgue_integral_uminus: ``` hoelzl@59092 ` 236` ``` "interval_lebesgue_integral M a b (\x. - f x) = - interval_lebesgue_integral M a b f" ``` lp15@68096 ` 237` ``` by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def) ``` hoelzl@59092 ` 238` hoelzl@59092 ` 239` ```lemma interval_lebesgue_integral_of_real: ``` hoelzl@59092 ` 240` ``` "interval_lebesgue_integral M a b (\x. complex_of_real (f x)) = ``` hoelzl@59092 ` 241` ``` of_real (interval_lebesgue_integral M a b f)" ``` hoelzl@59092 ` 242` ``` unfolding interval_lebesgue_integral_def ``` lp15@68096 ` 243` ``` by (auto simp: interval_lebesgue_integral_def set_integral_complex_of_real) ``` hoelzl@59092 ` 244` ak2110@69173 ` 245` ```lemma%important interval_lebesgue_integral_le_eq: ``` hoelzl@59092 ` 246` ``` fixes a b f ``` hoelzl@59092 ` 247` ``` assumes "a \ b" ``` hoelzl@59092 ` 248` ``` shows "interval_lebesgue_integral M a b f = (LINT x : einterval a b | M. f x)" ``` ak2110@69173 ` 249` ```using%unimportant assms by (auto simp: interval_lebesgue_integral_def) ``` hoelzl@59092 ` 250` hoelzl@63329 ` 251` ```lemma interval_lebesgue_integral_gt_eq: ``` hoelzl@59092 ` 252` ``` fixes a b f ``` hoelzl@59092 ` 253` ``` assumes "a > b" ``` hoelzl@59092 ` 254` ``` shows "interval_lebesgue_integral M a b f = -(LINT x : einterval b a | M. f x)" ``` lp15@68096 ` 255` ```using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def) ``` hoelzl@59092 ` 256` hoelzl@59092 ` 257` ```lemma interval_lebesgue_integral_gt_eq': ``` hoelzl@59092 ` 258` ``` fixes a b f ``` hoelzl@59092 ` 259` ``` assumes "a > b" ``` hoelzl@59092 ` 260` ``` shows "interval_lebesgue_integral M a b f = - interval_lebesgue_integral M b a f" ``` lp15@68096 ` 261` ```using assms by (auto simp: interval_lebesgue_integral_def less_imp_le einterval_def) ``` hoelzl@59092 ` 262` hoelzl@59092 ` 263` ```lemma interval_integral_endpoints_same [simp]: "(LBINT x=a..a. f x) = 0" ``` lp15@67974 ` 264` ``` by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same) ``` hoelzl@59092 ` 265` hoelzl@59092 ` 266` ```lemma interval_integral_endpoints_reverse: "(LBINT x=a..b. f x) = -(LBINT x=b..a. f x)" ``` lp15@67974 ` 267` ``` by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def einterval_same) ``` hoelzl@59092 ` 268` hoelzl@59092 ` 269` ```lemma interval_integrable_endpoints_reverse: ``` hoelzl@59092 ` 270` ``` "interval_lebesgue_integrable lborel a b f \ ``` hoelzl@59092 ` 271` ``` interval_lebesgue_integrable lborel b a f" ``` hoelzl@59092 ` 272` ``` by (cases a b rule: linorder_cases) (auto simp: interval_lebesgue_integrable_def einterval_same) ``` hoelzl@59092 ` 273` ak2110@69173 ` 274` ```lemma%important interval_integral_reflect: ``` hoelzl@59092 ` 275` ``` "(LBINT x=a..b. f x) = (LBINT x=-b..-a. f (-x))" ``` ak2110@69173 ` 276` ```proof%unimportant (induct a b rule: linorder_wlog) ``` hoelzl@59092 ` 277` ``` case (sym a b) then show ?case ``` lp15@68096 ` 278` ``` by (auto simp: interval_lebesgue_integral_def interval_integrable_endpoints_reverse ``` nipkow@62390 ` 279` ``` split: if_split_asm) ``` hoelzl@59092 ` 280` ```next ``` lp15@67974 ` 281` ``` case (le a b) ``` lp15@67974 ` 282` ``` have "LBINT x:{x. - x \ einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)" ``` lp15@67974 ` 283` ``` unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def ``` lp15@67974 ` 284` ``` apply (rule Bochner_Integration.integral_cong [OF refl]) ``` nipkow@68046 ` 285` ``` by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less ``` nipkow@68403 ` 286` ``` simp flip: uminus_ereal.simps ``` hoelzl@59092 ` 287` ``` split: split_indicator) ``` lp15@67974 ` 288` ``` then show ?case ``` lp15@67974 ` 289` ``` unfolding interval_lebesgue_integral_def ``` lp15@67974 ` 290` ``` by (subst set_integral_reflect) (simp add: le) ``` hoelzl@59092 ` 291` ```qed ``` hoelzl@59092 ` 292` hoelzl@61897 ` 293` ```lemma interval_lebesgue_integral_0_infty: ``` hoelzl@61897 ` 294` ``` "interval_lebesgue_integrable M 0 \ f \ set_integrable M {0<..} f" ``` hoelzl@61897 ` 295` ``` "interval_lebesgue_integral M 0 \ f = (LINT x:{0<..}|M. f x)" ``` hoelzl@63329 ` 296` ``` unfolding zero_ereal_def ``` hoelzl@61897 ` 297` ``` by (auto simp: interval_lebesgue_integral_le_eq interval_lebesgue_integrable_def) ``` hoelzl@61897 ` 298` hoelzl@61897 ` 299` ```lemma interval_integral_to_infinity_eq: "(LINT x=ereal a..\ | M. f x) = (LINT x : {a<..} | M. f x)" ``` hoelzl@61897 ` 300` ``` unfolding interval_lebesgue_integral_def by auto ``` hoelzl@61897 ` 301` ak2110@69173 ` 302` ```lemma%important interval_integrable_to_infinity_eq: "(interval_lebesgue_integrable M a \ f) = ``` hoelzl@61897 ` 303` ``` (set_integrable M {a<..} f)" ``` ak2110@69173 ` 304` ``` unfolding%unimportant interval_lebesgue_integrable_def by auto ``` hoelzl@61897 ` 305` ak2110@69173 ` 306` ```subsection%important\Basic properties of integration over an interval wrt lebesgue measure\ ``` hoelzl@59092 ` 307` hoelzl@59092 ` 308` ```lemma interval_integral_zero [simp]: ``` hoelzl@59092 ` 309` ``` fixes a b :: ereal ``` lp15@68096 ` 310` ``` shows "LBINT x=a..b. 0 = 0" ``` lp15@67974 ` 311` ```unfolding interval_lebesgue_integral_def set_lebesgue_integral_def einterval_eq ``` hoelzl@59092 ` 312` ```by simp ``` hoelzl@59092 ` 313` hoelzl@59092 ` 314` ```lemma interval_integral_const [intro, simp]: ``` hoelzl@59092 ` 315` ``` fixes a b c :: real ``` hoelzl@63329 ` 316` ``` shows "interval_lebesgue_integrable lborel a b (\x. c)" and "LBINT x=a..b. c = c * (b - a)" ``` lp15@67974 ` 317` ``` unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def einterval_eq ``` lp15@68096 ` 318` ``` by (auto simp: less_imp_le field_simps measure_def set_integrable_def set_lebesgue_integral_def) ``` hoelzl@59092 ` 319` ak2110@69173 ` 320` ```lemma%important interval_integral_cong_AE: ``` hoelzl@59092 ` 321` ``` assumes [measurable]: "f \ borel_measurable borel" "g \ borel_measurable borel" ``` hoelzl@59092 ` 322` ``` assumes "AE x \ einterval (min a b) (max a b) in lborel. f x = g x" ``` hoelzl@59092 ` 323` ``` shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" ``` hoelzl@59092 ` 324` ``` using assms ``` ak2110@69173 ` 325` ```proof%unimportant (induct a b rule: linorder_wlog) ``` hoelzl@59092 ` 326` ``` case (sym a b) then show ?case ``` hoelzl@59092 ` 327` ``` by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b]) ``` hoelzl@59092 ` 328` ```next ``` hoelzl@59092 ` 329` ``` case (le a b) then show ?case ``` hoelzl@59092 ` 330` ``` by (auto simp: interval_lebesgue_integral_def max_def min_def ``` hoelzl@59092 ` 331` ``` intro!: set_lebesgue_integral_cong_AE) ``` hoelzl@59092 ` 332` ```qed ``` hoelzl@59092 ` 333` ak2110@69173 ` 334` ```lemma%important interval_integral_cong: ``` hoelzl@63329 ` 335` ``` assumes "\x. x \ einterval (min a b) (max a b) \ f x = g x" ``` hoelzl@59092 ` 336` ``` shows "interval_lebesgue_integral lborel a b f = interval_lebesgue_integral lborel a b g" ``` hoelzl@59092 ` 337` ``` using assms ``` ak2110@69173 ` 338` ```proof%unimportant (induct a b rule: linorder_wlog) ``` hoelzl@59092 ` 339` ``` case (sym a b) then show ?case ``` hoelzl@59092 ` 340` ``` by (simp add: min.commute max.commute interval_integral_endpoints_reverse[of a b]) ``` hoelzl@59092 ` 341` ```next ``` hoelzl@59092 ` 342` ``` case (le a b) then show ?case ``` hoelzl@59092 ` 343` ``` by (auto simp: interval_lebesgue_integral_def max_def min_def ``` hoelzl@59092 ` 344` ``` intro!: set_lebesgue_integral_cong) ``` hoelzl@59092 ` 345` ```qed ``` hoelzl@59092 ` 346` hoelzl@59092 ` 347` ```lemma interval_lebesgue_integrable_cong_AE: ``` hoelzl@59092 ` 348` ``` "f \ borel_measurable lborel \ g \ borel_measurable lborel \ ``` hoelzl@59092 ` 349` ``` AE x \ einterval (min a b) (max a b) in lborel. f x = g x \ ``` hoelzl@59092 ` 350` ``` interval_lebesgue_integrable lborel a b f = interval_lebesgue_integrable lborel a b g" ``` lp15@68096 ` 351` ``` apply (simp add: interval_lebesgue_integrable_def) ``` hoelzl@59092 ` 352` ``` apply (intro conjI impI set_integrable_cong_AE) ``` hoelzl@59092 ` 353` ``` apply (auto simp: min_def max_def) ``` hoelzl@59092 ` 354` ``` done ``` hoelzl@59092 ` 355` hoelzl@59092 ` 356` ```lemma interval_integrable_abs_iff: ``` hoelzl@59092 ` 357` ``` fixes f :: "real \ real" ``` hoelzl@59092 ` 358` ``` shows "f \ borel_measurable lborel \ ``` hoelzl@59092 ` 359` ``` interval_lebesgue_integrable lborel a b (\x. \f x\) = interval_lebesgue_integrable lborel a b f" ``` hoelzl@59092 ` 360` ``` unfolding interval_lebesgue_integrable_def ``` hoelzl@59092 ` 361` ``` by (subst (1 2) set_integrable_abs_iff') simp_all ``` hoelzl@59092 ` 362` hoelzl@59092 ` 363` ```lemma interval_integral_Icc: ``` hoelzl@59092 ` 364` ``` fixes a b :: real ``` hoelzl@59092 ` 365` ``` shows "a \ b \ (LBINT x=a..b. f x) = (LBINT x : {a..b}. f x)" ``` hoelzl@59092 ` 366` ``` by (auto intro!: set_integral_discrete_difference[where X="{a, b}"] ``` hoelzl@59092 ` 367` ``` simp add: interval_lebesgue_integral_def) ``` hoelzl@59092 ` 368` hoelzl@59092 ` 369` ```lemma interval_integral_Icc': ``` hoelzl@59092 ` 370` ``` "a \ b \ (LBINT x=a..b. f x) = (LBINT x : {x. a \ ereal x \ ereal x \ b}. f x)" ``` lp15@61609 ` 371` ``` by (auto intro!: set_integral_discrete_difference[where X="{real_of_ereal a, real_of_ereal b}"] ``` hoelzl@59092 ` 372` ``` simp add: interval_lebesgue_integral_def einterval_iff) ``` hoelzl@59092 ` 373` hoelzl@59092 ` 374` ```lemma interval_integral_Ioc: ``` hoelzl@59092 ` 375` ``` "a \ b \ (LBINT x=a..b. f x) = (LBINT x : {a<..b}. f x)" ``` hoelzl@59092 ` 376` ``` by (auto intro!: set_integral_discrete_difference[where X="{a, b}"] ``` hoelzl@59092 ` 377` ``` simp add: interval_lebesgue_integral_def einterval_iff) ``` hoelzl@59092 ` 378` hoelzl@59092 ` 379` ```(* TODO: other versions as well? *) (* Yes: I need the Icc' version. *) ``` hoelzl@59092 ` 380` ```lemma interval_integral_Ioc': ``` hoelzl@59092 ` 381` ``` "a \ b \ (LBINT x=a..b. f x) = (LBINT x : {x. a < ereal x \ ereal x \ b}. f x)" ``` lp15@61609 ` 382` ``` by (auto intro!: set_integral_discrete_difference[where X="{real_of_ereal a, real_of_ereal b}"] ``` hoelzl@59092 ` 383` ``` simp add: interval_lebesgue_integral_def einterval_iff) ``` hoelzl@59092 ` 384` hoelzl@59092 ` 385` ```lemma interval_integral_Ico: ``` hoelzl@59092 ` 386` ``` "a \ b \ (LBINT x=a..b. f x) = (LBINT x : {a..a\ < \ \ (LBINT x=a..\. f x) = (LBINT x : {real_of_ereal a <..}. f x)" ``` lp15@68096 ` 392` ``` by (auto simp: interval_lebesgue_integral_def einterval_iff) ``` hoelzl@59092 ` 393` hoelzl@59092 ` 394` ```lemma interval_integral_Ioo: ``` hoelzl@61882 ` 395` ``` "a \ b \ \a\ < \ ==> \b\ < \ \ (LBINT x=a..b. f x) = (LBINT x : {real_of_ereal a <..< real_of_ereal b}. f x)" ``` lp15@68096 ` 396` ``` by (auto simp: interval_lebesgue_integral_def einterval_iff) ``` hoelzl@59092 ` 397` hoelzl@59092 ` 398` ```lemma interval_integral_discrete_difference: ``` hoelzl@59092 ` 399` ``` fixes f :: "real \ 'b::{banach, second_countable_topology}" and a b :: ereal ``` hoelzl@59092 ` 400` ``` assumes "countable X" ``` hoelzl@59092 ` 401` ``` and eq: "\x. a \ b \ a < x \ x < b \ x \ X \ f x = g x" ``` hoelzl@59092 ` 402` ``` and anti_eq: "\x. b \ a \ b < x \ x < a \ x \ X \ f x = g x" ``` hoelzl@59092 ` 403` ``` assumes "\x. x \ X \ emeasure M {x} = 0" "\x. x \ X \ {x} \ sets M" ``` hoelzl@59092 ` 404` ``` shows "interval_lebesgue_integral M a b f = interval_lebesgue_integral M a b g" ``` lp15@67974 ` 405` ``` unfolding interval_lebesgue_integral_def set_lebesgue_integral_def ``` hoelzl@59092 ` 406` ``` apply (intro if_cong refl arg_cong[where f="\x. - x"] integral_discrete_difference[of X] assms) ``` hoelzl@59092 ` 407` ``` apply (auto simp: eq anti_eq einterval_iff split: split_indicator) ``` hoelzl@59092 ` 408` ``` done ``` hoelzl@59092 ` 409` ak2110@69173 ` 410` ```lemma%important interval_integral_sum: ``` hoelzl@59092 ` 411` ``` fixes a b c :: ereal ``` hoelzl@63329 ` 412` ``` assumes integrable: "interval_lebesgue_integrable lborel (min a (min b c)) (max a (max b c)) f" ``` hoelzl@59092 ` 413` ``` shows "(LBINT x=a..b. f x) + (LBINT x=b..c. f x) = (LBINT x=a..c. f x)" ``` ak2110@69173 ` 414` ```proof%unimportant - ``` hoelzl@59092 ` 415` ``` let ?I = "\a b. LBINT x=a..b. f x" ``` hoelzl@59092 ` 416` ``` { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \ b" "b \ c" ``` hoelzl@59092 ` 417` ``` then have ord: "a \ b" "b \ c" "a \ c" and f': "set_integrable lborel (einterval a c) f" ``` hoelzl@59092 ` 418` ``` by (auto simp: interval_lebesgue_integrable_def) ``` hoelzl@59092 ` 419` ``` then have f: "set_borel_measurable borel (einterval a c) f" ``` lp15@67974 ` 420` ``` unfolding set_integrable_def set_borel_measurable_def ``` hoelzl@59092 ` 421` ``` by (drule_tac borel_measurable_integrable) simp ``` hoelzl@59092 ` 422` ``` have "(LBINT x:einterval a c. f x) = (LBINT x:einterval a b \ einterval b c. f x)" ``` hoelzl@59092 ` 423` ``` proof (rule set_integral_cong_set) ``` hoelzl@59092 ` 424` ``` show "AE x in lborel. (x \ einterval a b \ einterval b c) = (x \ einterval a c)" ``` lp15@61609 ` 425` ``` using AE_lborel_singleton[of "real_of_ereal b"] ord ``` hoelzl@59092 ` 426` ``` by (cases a b c rule: ereal3_cases) (auto simp: einterval_iff) ``` lp15@67974 ` 427` ``` show "set_borel_measurable lborel (einterval a c) f" "set_borel_measurable lborel (einterval a b \ einterval b c) f" ``` lp15@67974 ` 428` ``` unfolding set_borel_measurable_def ``` lp15@67974 ` 429` ``` using ord by (auto simp: einterval_iff intro!: set_borel_measurable_subset[OF f, unfolded set_borel_measurable_def]) ``` lp15@67974 ` 430` ``` qed ``` hoelzl@59092 ` 431` ``` also have "\ = (LBINT x:einterval a b. f x) + (LBINT x:einterval b c. f x)" ``` hoelzl@59092 ` 432` ``` using ord ``` hoelzl@59092 ` 433` ``` by (intro set_integral_Un_AE) (auto intro!: set_integrable_subset[OF f'] simp: einterval_iff not_less) ``` hoelzl@59092 ` 434` ``` finally have "?I a b + ?I b c = ?I a c" ``` hoelzl@59092 ` 435` ``` using ord by (simp add: interval_lebesgue_integral_def) ``` hoelzl@59092 ` 436` ``` } note 1 = this ``` hoelzl@59092 ` 437` ``` { fix a b c :: ereal assume "interval_lebesgue_integrable lborel a c f" "a \ b" "b \ c" ``` hoelzl@59092 ` 438` ``` from 1[OF this] have "?I b c + ?I a b = ?I a c" ``` hoelzl@59092 ` 439` ``` by (metis add.commute) ``` hoelzl@59092 ` 440` ``` } note 2 = this ``` hoelzl@59092 ` 441` ``` have 3: "\a b. b \ a \ (LBINT x=a..b. f x) = - (LBINT x=b..a. f x)" ``` hoelzl@59092 ` 442` ``` by (rule interval_integral_endpoints_reverse) ``` hoelzl@59092 ` 443` ``` show ?thesis ``` hoelzl@59092 ` 444` ``` using integrable ``` hoelzl@59092 ` 445` ``` by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases]) ``` hoelzl@59092 ` 446` ``` (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3) ``` hoelzl@59092 ` 447` ```qed ``` hoelzl@59092 ` 448` ak2110@69173 ` 449` ```lemma%important interval_integrable_isCont: ``` hoelzl@59092 ` 450` ``` fixes a b and f :: "real \ 'a::{banach, second_countable_topology}" ``` hoelzl@59092 ` 451` ``` shows "(\x. min a b \ x \ x \ max a b \ isCont f x) \ ``` hoelzl@59092 ` 452` ``` interval_lebesgue_integrable lborel a b f" ``` ak2110@69173 ` 453` ```proof%unimportant (induct a b rule: linorder_wlog) ``` hoelzl@59092 ` 454` ``` case (le a b) then show ?case ``` lp15@67974 ` 455` ``` unfolding interval_lebesgue_integrable_def set_integrable_def ``` hoelzl@59092 ` 456` ``` by (auto simp: interval_lebesgue_integrable_def ``` lp15@67974 ` 457` ``` intro!: set_integrable_subset[unfolded set_integrable_def, OF borel_integrable_compact[of "{a .. b}"]] ``` lp15@67974 ` 458` ``` continuous_at_imp_continuous_on) ``` hoelzl@59092 ` 459` ```qed (auto intro: interval_integrable_endpoints_reverse[THEN iffD1]) ``` hoelzl@59092 ` 460` hoelzl@59092 ` 461` ```lemma interval_integrable_continuous_on: ``` hoelzl@59092 ` 462` ``` fixes a b :: real and f ``` hoelzl@59092 ` 463` ``` assumes "a \ b" and "continuous_on {a..b} f" ``` hoelzl@59092 ` 464` ``` shows "interval_lebesgue_integrable lborel a b f" ``` hoelzl@59092 ` 465` ```using assms unfolding interval_lebesgue_integrable_def apply simp ``` hoelzl@59092 ` 466` ``` by (rule set_integrable_subset, rule borel_integrable_atLeastAtMost' [of a b], auto) ``` hoelzl@59092 ` 467` hoelzl@63329 ` 468` ```lemma interval_integral_eq_integral: ``` hoelzl@59092 ` 469` ``` fixes f :: "real \ 'a::euclidean_space" ``` hoelzl@59092 ` 470` ``` shows "a \ b \ set_integrable lborel {a..b} f \ LBINT x=a..b. f x = integral {a..b} f" ``` hoelzl@59092 ` 471` ``` by (subst interval_integral_Icc, simp) (rule set_borel_integral_eq_integral) ``` hoelzl@59092 ` 472` hoelzl@63329 ` 473` ```lemma interval_integral_eq_integral': ``` hoelzl@59092 ` 474` ``` fixes f :: "real \ 'a::euclidean_space" ``` hoelzl@59092 ` 475` ``` shows "a \ b \ set_integrable lborel (einterval a b) f \ LBINT x=a..b. f x = integral (einterval a b) f" ``` hoelzl@59092 ` 476` ``` by (subst interval_lebesgue_integral_le_eq, simp) (rule set_borel_integral_eq_integral) ``` hoelzl@63329 ` 477` lp15@67974 ` 478` ak2110@69173 ` 479` ```subsection%important\General limit approximation arguments\ ``` hoelzl@59092 ` 480` ak2110@69173 ` 481` ```lemma%important interval_integral_Icc_approx_nonneg: ``` hoelzl@59092 ` 482` ``` fixes a b :: ereal ``` hoelzl@59092 ` 483` ``` assumes "a < b" ``` hoelzl@59092 ` 484` ``` fixes u l :: "nat \ real" ``` hoelzl@59092 ` 485` ``` assumes approx: "einterval a b = (\i. {l i .. u i})" ``` hoelzl@59092 ` 486` ``` "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" ``` wenzelm@61969 ` 487` ``` "l \ a" "u \ b" ``` hoelzl@59092 ` 488` ``` fixes f :: "real \ real" ``` hoelzl@59092 ` 489` ``` assumes f_integrable: "\i. set_integrable lborel {l i..u i} f" ``` hoelzl@59092 ` 490` ``` assumes f_nonneg: "AE x in lborel. a < ereal x \ ereal x < b \ 0 \ f x" ``` hoelzl@59092 ` 491` ``` assumes f_measurable: "set_borel_measurable lborel (einterval a b) f" ``` wenzelm@61969 ` 492` ``` assumes lbint_lim: "(\i. LBINT x=l i.. u i. f x) \ C" ``` hoelzl@63329 ` 493` ``` shows ``` hoelzl@59092 ` 494` ``` "set_integrable lborel (einterval a b) f" ``` hoelzl@59092 ` 495` ``` "(LBINT x=a..b. f x) = C" ``` ak2110@69173 ` 496` ```proof%unimportant - ``` lp15@67974 ` 497` ``` have 1 [unfolded set_integrable_def]: "\i. set_integrable lborel {l i..u i} f" by (rule f_integrable) ``` hoelzl@59092 ` 498` ``` have 2: "AE x in lborel. mono (\n. indicator {l n..u n} x *\<^sub>R f x)" ``` hoelzl@59092 ` 499` ``` proof - ``` hoelzl@59092 ` 500` ``` from f_nonneg have "AE x in lborel. \i. l i \ x \ x \ u i \ 0 \ f x" ``` hoelzl@59092 ` 501` ``` by eventually_elim ``` hoelzl@59092 ` 502` ``` (metis approx(5) approx(6) dual_order.strict_trans1 ereal_less_eq(3) le_less_trans) ``` hoelzl@59092 ` 503` ``` then show ?thesis ``` hoelzl@59092 ` 504` ``` apply eventually_elim ``` hoelzl@59092 ` 505` ``` apply (auto simp: mono_def split: split_indicator) ``` hoelzl@59092 ` 506` ``` apply (metis approx(3) decseqD order_trans) ``` hoelzl@59092 ` 507` ``` apply (metis approx(2) incseqD order_trans) ``` hoelzl@59092 ` 508` ``` done ``` hoelzl@59092 ` 509` ``` qed ``` wenzelm@61969 ` 510` ``` have 3: "AE x in lborel. (\i. indicator {l i..u i} x *\<^sub>R f x) \ indicator (einterval a b) x *\<^sub>R f x" ``` hoelzl@59092 ` 511` ``` proof - ``` hoelzl@59092 ` 512` ``` { fix x i assume "l i \ x" "x \ u i" ``` hoelzl@59092 ` 513` ``` then have "eventually (\i. l i \ x \ x \ u i) sequentially" ``` hoelzl@59092 ` 514` ``` apply (auto simp: eventually_sequentially intro!: exI[of _ i]) ``` hoelzl@59092 ` 515` ``` apply (metis approx(3) decseqD order_trans) ``` hoelzl@59092 ` 516` ``` apply (metis approx(2) incseqD order_trans) ``` hoelzl@59092 ` 517` ``` done ``` hoelzl@59092 ` 518` ``` then have "eventually (\i. f x * indicator {l i..u i} x = f x) sequentially" ``` hoelzl@59092 ` 519` ``` by eventually_elim auto } ``` hoelzl@59092 ` 520` ``` then show ?thesis ``` hoelzl@59092 ` 521` ``` unfolding approx(1) by (auto intro!: AE_I2 Lim_eventually split: split_indicator) ``` hoelzl@59092 ` 522` ``` qed ``` wenzelm@61969 ` 523` ``` have 4: "(\i. \ x. indicator {l i..u i} x *\<^sub>R f x \lborel) \ C" ``` lp15@67974 ` 524` ``` using lbint_lim by (simp add: interval_integral_Icc [unfolded set_lebesgue_integral_def] approx less_imp_le) ``` lp15@67974 ` 525` ``` have 5: "(\x. indicat_real (einterval a b) x *\<^sub>R f x) \ borel_measurable lborel" ``` lp15@67974 ` 526` ``` using f_measurable set_borel_measurable_def by blast ``` hoelzl@59092 ` 527` ``` have "(LBINT x=a..b. f x) = lebesgue_integral lborel (\x. indicator (einterval a b) x *\<^sub>R f x)" ``` lp15@67974 ` 528` ``` using assms by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def less_imp_le) ``` lp15@68096 ` 529` ``` also have "\ = C" ``` lp15@67974 ` 530` ``` by (rule integral_monotone_convergence [OF 1 2 3 4 5]) ``` hoelzl@59092 ` 531` ``` finally show "(LBINT x=a..b. f x) = C" . ``` hoelzl@63329 ` 532` ``` show "set_integrable lborel (einterval a b) f" ``` lp15@67974 ` 533` ``` unfolding set_integrable_def ``` hoelzl@59092 ` 534` ``` by (rule integrable_monotone_convergence[OF 1 2 3 4 5]) ``` hoelzl@59092 ` 535` ```qed ``` hoelzl@59092 ` 536` ak2110@69173 ` 537` ```lemma%important interval_integral_Icc_approx_integrable: ``` hoelzl@59092 ` 538` ``` fixes u l :: "nat \ real" and a b :: ereal ``` hoelzl@59092 ` 539` ``` fixes f :: "real \ 'a::{banach, second_countable_topology}" ``` hoelzl@59092 ` 540` ``` assumes "a < b" ``` hoelzl@59092 ` 541` ``` assumes approx: "einterval a b = (\i. {l i .. u i})" ``` hoelzl@59092 ` 542` ``` "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" ``` wenzelm@61969 ` 543` ``` "l \ a" "u \ b" ``` hoelzl@59092 ` 544` ``` assumes f_integrable: "set_integrable lborel (einterval a b) f" ``` wenzelm@61969 ` 545` ``` shows "(\i. LBINT x=l i.. u i. f x) \ (LBINT x=a..b. f x)" ``` ak2110@69173 ` 546` ```proof%unimportant - ``` wenzelm@61969 ` 547` ``` have "(\i. LBINT x:{l i.. u i}. f x) \ (LBINT x:einterval a b. f x)" ``` lp15@67974 ` 548` ``` unfolding set_lebesgue_integral_def ``` hoelzl@59092 ` 549` ``` proof (rule integral_dominated_convergence) ``` hoelzl@59092 ` 550` ``` show "integrable lborel (\x. norm (indicator (einterval a b) x *\<^sub>R f x))" ``` lp15@67974 ` 551` ``` using f_integrable integrable_norm set_integrable_def by blast ``` lp15@67974 ` 552` ``` show "(\x. indicat_real (einterval a b) x *\<^sub>R f x) \ borel_measurable lborel" ``` lp15@67974 ` 553` ``` using f_integrable by (simp add: set_integrable_def) ``` lp15@67974 ` 554` ``` then show "\i. (\x. indicat_real {l i..u i} x *\<^sub>R f x) \ borel_measurable lborel" ``` lp15@67974 ` 555` ``` by (rule set_borel_measurable_subset [unfolded set_borel_measurable_def]) (auto simp: approx) ``` hoelzl@59092 ` 556` ``` show "\i. AE x in lborel. norm (indicator {l i..u i} x *\<^sub>R f x) \ norm (indicator (einterval a b) x *\<^sub>R f x)" ``` hoelzl@59092 ` 557` ``` by (intro AE_I2) (auto simp: approx split: split_indicator) ``` wenzelm@61969 ` 558` ``` show "AE x in lborel. (\i. indicator {l i..u i} x *\<^sub>R f x) \ indicator (einterval a b) x *\<^sub>R f x" ``` hoelzl@59092 ` 559` ``` proof (intro AE_I2 tendsto_intros Lim_eventually) ``` hoelzl@59092 ` 560` ``` fix x ``` hoelzl@63329 ` 561` ``` { fix i assume "l i \ x" "x \ u i" ``` wenzelm@61808 ` 562` ``` with \incseq u\[THEN incseqD, of i] \decseq l\[THEN decseqD, of i] ``` hoelzl@59092 ` 563` ``` have "eventually (\i. l i \ x \ x \ u i) sequentially" ``` hoelzl@59092 ` 564` ``` by (auto simp: eventually_sequentially decseq_def incseq_def intro: order_trans) } ``` hoelzl@59092 ` 565` ``` then show "eventually (\xa. indicator {l xa..u xa} x = (indicator (einterval a b) x::real)) sequentially" ``` wenzelm@61969 ` 566` ``` using approx order_tendstoD(2)[OF \l \ a\, of x] order_tendstoD(1)[OF \u \ b\, of x] ``` hoelzl@59092 ` 567` ``` by (auto split: split_indicator) ``` hoelzl@59092 ` 568` ``` qed ``` hoelzl@59092 ` 569` ``` qed ``` wenzelm@61808 ` 570` ``` with \a < b\ \\i. l i < u i\ show ?thesis ``` hoelzl@59092 ` 571` ``` by (simp add: interval_lebesgue_integral_le_eq[symmetric] interval_integral_Icc less_imp_le) ``` hoelzl@59092 ` 572` ```qed ``` hoelzl@59092 ` 573` ak2110@69173 ` 574` ```subsection%important\A slightly stronger Fundamental Theorem of Calculus\ ``` lp15@67974 ` 575` lp15@67974 ` 576` ```text\Three versions: first, for finite intervals, and then two versions for ``` lp15@67974 ` 577` ``` arbitrary intervals.\ ``` lp15@67974 ` 578` hoelzl@59092 ` 579` ```(* ``` hoelzl@59092 ` 580` ``` TODO: make the older versions corollaries of these (using continuous_at_imp_continuous_on, etc.) ``` hoelzl@59092 ` 581` ```*) ``` hoelzl@59092 ` 582` ak2110@69173 ` 583` ```lemma%important interval_integral_FTC_finite: ``` hoelzl@59092 ` 584` ``` fixes f F :: "real \ 'a::euclidean_space" and a b :: real ``` hoelzl@59092 ` 585` ``` assumes f: "continuous_on {min a b..max a b} f" ``` hoelzl@63329 ` 586` ``` assumes F: "\x. min a b \ x \ x \ max a b \ (F has_vector_derivative (f x)) (at x within ``` hoelzl@63329 ` 587` ``` {min a b..max a b})" ``` hoelzl@59092 ` 588` ``` shows "(LBINT x=a..b. f x) = F b - F a" ``` ak2110@69173 ` 589` ```proof%unimportant (cases "a \ b") ``` lp15@67974 ` 590` ``` case True ``` lp15@67974 ` 591` ``` have "(LBINT x=a..b. f x) = (LBINT x. indicat_real {a..b} x *\<^sub>R f x)" ``` lp15@67974 ` 592` ``` by (simp add: True interval_integral_Icc set_lebesgue_integral_def) ``` lp15@68096 ` 593` ``` also have "\ = F b - F a" ``` lp15@67974 ` 594` ``` proof (rule integral_FTC_atLeastAtMost [OF True]) ``` lp15@67974 ` 595` ``` show "continuous_on {a..b} f" ``` lp15@67974 ` 596` ``` using True f by linarith ``` lp15@67974 ` 597` ``` show "\x. \a \ x; x \ b\ \ (F has_vector_derivative f x) (at x within {a..b})" ``` lp15@67974 ` 598` ``` by (metis F True max.commute max_absorb1 min_def) ``` lp15@67974 ` 599` ``` qed ``` lp15@67974 ` 600` ``` finally show ?thesis . ``` lp15@67974 ` 601` ```next ``` lp15@67974 ` 602` ``` case False ``` lp15@67974 ` 603` ``` then have "b \ a" ``` lp15@67974 ` 604` ``` by simp ``` lp15@67974 ` 605` ``` have "- interval_lebesgue_integral lborel (ereal b) (ereal a) f = - (LBINT x. indicat_real {b..a} x *\<^sub>R f x)" ``` lp15@67974 ` 606` ``` by (simp add: \b \ a\ interval_integral_Icc set_lebesgue_integral_def) ``` lp15@68096 ` 607` ``` also have "\ = F b - F a" ``` lp15@67974 ` 608` ``` proof (subst integral_FTC_atLeastAtMost [OF \b \ a\]) ``` lp15@67974 ` 609` ``` show "continuous_on {b..a} f" ``` lp15@67974 ` 610` ``` using False f by linarith ``` lp15@67974 ` 611` ``` show "\x. \b \ x; x \ a\ ``` lp15@67974 ` 612` ``` \ (F has_vector_derivative f x) (at x within {b..a})" ``` lp15@67974 ` 613` ``` by (metis F False max_def min_def) ``` lp15@67974 ` 614` ``` qed auto ``` lp15@67974 ` 615` ``` finally show ?thesis ``` lp15@67974 ` 616` ``` by (metis interval_integral_endpoints_reverse) ``` lp15@67974 ` 617` ```qed ``` lp15@67974 ` 618` lp15@67974 ` 619` ak2110@69173 ` 620` ```lemma%important interval_integral_FTC_nonneg: ``` hoelzl@59092 ` 621` ``` fixes f F :: "real \ real" and a b :: ereal ``` hoelzl@59092 ` 622` ``` assumes "a < b" ``` hoelzl@63329 ` 623` ``` assumes F: "\x. a < ereal x \ ereal x < b \ DERIV F x :> f x" ``` hoelzl@63329 ` 624` ``` assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" ``` hoelzl@59092 ` 625` ``` assumes f_nonneg: "AE x in lborel. a < ereal x \ ereal x < b \ 0 \ f x" ``` wenzelm@61973 ` 626` ``` assumes A: "((F \ real_of_ereal) \ A) (at_right a)" ``` wenzelm@61973 ` 627` ``` assumes B: "((F \ real_of_ereal) \ B) (at_left b)" ``` hoelzl@59092 ` 628` ``` shows ``` hoelzl@63329 ` 629` ``` "set_integrable lborel (einterval a b) f" ``` hoelzl@59092 ` 630` ``` "(LBINT x=a..b. f x) = B - A" ``` ak2110@69173 ` 631` ```proof%unimportant - ``` lp15@68095 ` 632` ``` obtain u l where approx: ``` lp15@68095 ` 633` ``` "einterval a b = (\i. {l i .. u i})" ``` lp15@68095 ` 634` ``` "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" ``` lp15@68095 ` 635` ``` "l \ a" "u \ b" ``` lp15@68095 ` 636` ``` by (blast intro: einterval_Icc_approximation[OF \a < b\]) ``` hoelzl@59092 ` 637` ``` have [simp]: "\x i. l i \ x \ a < ereal x" ``` hoelzl@59092 ` 638` ``` by (rule order_less_le_trans, rule approx, force) ``` hoelzl@59092 ` 639` ``` have [simp]: "\x i. x \ u i \ ereal x < b" ``` hoelzl@59092 ` 640` ``` by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) ``` hoelzl@59092 ` 641` ``` have FTCi: "\i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)" ``` hoelzl@59092 ` 642` ``` using assms approx apply (intro interval_integral_FTC_finite) ``` lp15@68096 ` 643` ``` apply (auto simp: less_imp_le min_def max_def ``` hoelzl@59092 ` 644` ``` has_field_derivative_iff_has_vector_derivative[symmetric]) ``` hoelzl@59092 ` 645` ``` apply (rule continuous_at_imp_continuous_on, auto intro!: f) ``` hoelzl@59092 ` 646` ``` by (rule DERIV_subset [OF F], auto) ``` hoelzl@59092 ` 647` ``` have 1: "\i. set_integrable lborel {l i..u i} f" ``` hoelzl@59092 ` 648` ``` proof - ``` hoelzl@59092 ` 649` ``` fix i show "set_integrable lborel {l i .. u i} f" ``` lp15@67974 ` 650` ``` using \a < l i\ \u i < b\ unfolding set_integrable_def ``` hoelzl@59092 ` 651` ``` by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI) ``` nipkow@68403 ` 652` ``` (auto simp flip: ereal_less_eq) ``` hoelzl@59092 ` 653` ``` qed ``` hoelzl@59092 ` 654` ``` have 2: "set_borel_measurable lborel (einterval a b) f" ``` lp15@67974 ` 655` ``` unfolding set_borel_measurable_def ``` lp15@66164 ` 656` ``` by (auto simp del: real_scaleR_def intro!: borel_measurable_continuous_on_indicator ``` hoelzl@59092 ` 657` ``` simp: continuous_on_eq_continuous_at einterval_iff f) ``` wenzelm@61969 ` 658` ``` have 3: "(\i. LBINT x=l i..u i. f x) \ B - A" ``` hoelzl@59092 ` 659` ``` apply (subst FTCi) ``` hoelzl@59092 ` 660` ``` apply (intro tendsto_intros) ``` hoelzl@59092 ` 661` ``` using B approx unfolding tendsto_at_iff_sequentially comp_def ``` hoelzl@59092 ` 662` ``` using tendsto_at_iff_sequentially[where 'a=real] ``` hoelzl@59092 ` 663` ``` apply (elim allE[of _ "\i. ereal (u i)"], auto) ``` hoelzl@59092 ` 664` ``` using A approx unfolding tendsto_at_iff_sequentially comp_def ``` hoelzl@59092 ` 665` ``` by (elim allE[of _ "\i. ereal (l i)"], auto) ``` hoelzl@59092 ` 666` ``` show "(LBINT x=a..b. f x) = B - A" ``` wenzelm@61808 ` 667` ``` by (rule interval_integral_Icc_approx_nonneg [OF \a < b\ approx 1 f_nonneg 2 3]) ``` hoelzl@63329 ` 668` ``` show "set_integrable lborel (einterval a b) f" ``` wenzelm@61808 ` 669` ``` by (rule interval_integral_Icc_approx_nonneg [OF \a < b\ approx 1 f_nonneg 2 3]) ``` hoelzl@59092 ` 670` ```qed ``` hoelzl@59092 ` 671` ak2110@69173 ` 672` ```lemma%important interval_integral_FTC_integrable: ``` hoelzl@59092 ` 673` ``` fixes f F :: "real \ 'a::euclidean_space" and a b :: ereal ``` hoelzl@59092 ` 674` ``` assumes "a < b" ``` hoelzl@63329 ` 675` ``` assumes F: "\x. a < ereal x \ ereal x < b \ (F has_vector_derivative f x) (at x)" ``` hoelzl@63329 ` 676` ``` assumes f: "\x. a < ereal x \ ereal x < b \ isCont f x" ``` hoelzl@59092 ` 677` ``` assumes f_integrable: "set_integrable lborel (einterval a b) f" ``` wenzelm@61973 ` 678` ``` assumes A: "((F \ real_of_ereal) \ A) (at_right a)" ``` wenzelm@61973 ` 679` ``` assumes B: "((F \ real_of_ereal) \ B) (at_left b)" ``` hoelzl@59092 ` 680` ``` shows "(LBINT x=a..b. f x) = B - A" ``` ak2110@69173 ` 681` ```proof%unimportant - ``` lp15@68095 ` 682` ``` obtain u l where approx: ``` lp15@68095 ` 683` ``` "einterval a b = (\i. {l i .. u i})" ``` lp15@68095 ` 684` ``` "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" ``` lp15@68095 ` 685` ``` "l \ a" "u \ b" ``` lp15@68095 ` 686` ``` by (blast intro: einterval_Icc_approximation[OF \a < b\]) ``` hoelzl@59092 ` 687` ``` have [simp]: "\x i. l i \ x \ a < ereal x" ``` hoelzl@59092 ` 688` ``` by (rule order_less_le_trans, rule approx, force) ``` hoelzl@59092 ` 689` ``` have [simp]: "\x i. x \ u i \ ereal x < b" ``` hoelzl@59092 ` 690` ``` by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) ``` hoelzl@59092 ` 691` ``` have FTCi: "\i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)" ``` hoelzl@59092 ` 692` ``` using assms approx ``` lp15@68096 ` 693` ``` by (auto simp: less_imp_le min_def max_def ``` hoelzl@59092 ` 694` ``` intro!: f continuous_at_imp_continuous_on interval_integral_FTC_finite ``` hoelzl@59092 ` 695` ``` intro: has_vector_derivative_at_within) ``` wenzelm@61969 ` 696` ``` have "(\i. LBINT x=l i..u i. f x) \ B - A" ``` lp15@68096 ` 697` ``` unfolding FTCi ``` lp15@68096 ` 698` ``` proof (intro tendsto_intros) ``` lp15@68096 ` 699` ``` show "(\x. F (l x)) \ A" ``` lp15@68096 ` 700` ``` using A approx unfolding tendsto_at_iff_sequentially comp_def ``` lp15@68096 ` 701` ``` by (elim allE[of _ "\i. ereal (l i)"], auto) ``` lp15@68096 ` 702` ``` show "(\x. F (u x)) \ B" ``` lp15@68096 ` 703` ``` using B approx unfolding tendsto_at_iff_sequentially comp_def ``` lp15@68096 ` 704` ``` by (elim allE[of _ "\i. ereal (u i)"], auto) ``` lp15@68096 ` 705` ``` qed ``` wenzelm@61969 ` 706` ``` moreover have "(\i. LBINT x=l i..u i. f x) \ (LBINT x=a..b. f x)" ``` wenzelm@61808 ` 707` ``` by (rule interval_integral_Icc_approx_integrable [OF \a < b\ approx f_integrable]) ``` hoelzl@59092 ` 708` ``` ultimately show ?thesis ``` hoelzl@59092 ` 709` ``` by (elim LIMSEQ_unique) ``` hoelzl@59092 ` 710` ```qed ``` hoelzl@59092 ` 711` hoelzl@63329 ` 712` ```(* ``` hoelzl@59092 ` 713` ``` The second Fundamental Theorem of Calculus and existence of antiderivatives on an ``` hoelzl@59092 ` 714` ``` einterval. ``` hoelzl@59092 ` 715` ```*) ``` hoelzl@59092 ` 716` ak2110@69173 ` 717` ```lemma%important interval_integral_FTC2: ``` hoelzl@59092 ` 718` ``` fixes a b c :: real and f :: "real \ 'a::euclidean_space" ``` hoelzl@59092 ` 719` ``` assumes "a \ c" "c \ b" ``` hoelzl@59092 ` 720` ``` and contf: "continuous_on {a..b} f" ``` hoelzl@59092 ` 721` ``` fixes x :: real ``` hoelzl@59092 ` 722` ``` assumes "a \ x" and "x \ b" ``` hoelzl@59092 ` 723` ``` shows "((\u. LBINT y=c..u. f y) has_vector_derivative (f x)) (at x within {a..b})" ``` ak2110@69173 ` 724` ```proof%unimportant - ``` hoelzl@59092 ` 725` ``` let ?F = "(\u. LBINT y=a..u. f y)" ``` hoelzl@59092 ` 726` ``` have intf: "set_integrable lborel {a..b} f" ``` hoelzl@59092 ` 727` ``` by (rule borel_integrable_atLeastAtMost', rule contf) ``` hoelzl@59092 ` 728` ``` have "((\u. integral {a..u} f) has_vector_derivative f x) (at x within {a..b})" ``` lp15@68096 ` 729` ``` using \a \ x\ \x \ b\ ``` lp15@68096 ` 730` ``` by (auto intro: integral_has_vector_derivative continuous_on_subset [OF contf]) ``` hoelzl@59092 ` 731` ``` then have "((\u. integral {a..u} f) has_vector_derivative (f x)) (at x within {a..b})" ``` hoelzl@59092 ` 732` ``` by simp ``` hoelzl@59092 ` 733` ``` then have "(?F has_vector_derivative (f x)) (at x within {a..b})" ``` hoelzl@59092 ` 734` ``` by (rule has_vector_derivative_weaken) ``` hoelzl@59092 ` 735` ``` (auto intro!: assms interval_integral_eq_integral[symmetric] set_integrable_subset [OF intf]) ``` hoelzl@59092 ` 736` ``` then have "((\x. (LBINT y=c..a. f y) + ?F x) has_vector_derivative (f x)) (at x within {a..b})" ``` hoelzl@59092 ` 737` ``` by (auto intro!: derivative_eq_intros) ``` hoelzl@59092 ` 738` ``` then show ?thesis ``` hoelzl@59092 ` 739` ``` proof (rule has_vector_derivative_weaken) ``` hoelzl@59092 ` 740` ``` fix u assume "u \ {a .. b}" ``` hoelzl@59092 ` 741` ``` then show "(LBINT y=c..a. f y) + (LBINT y=a..u. f y) = (LBINT y=c..u. f y)" ``` hoelzl@59092 ` 742` ``` using assms ``` hoelzl@59092 ` 743` ``` apply (intro interval_integral_sum) ``` lp15@68096 ` 744` ``` apply (auto simp: interval_lebesgue_integrable_def simp del: real_scaleR_def) ``` lp15@68096 ` 745` ``` by (rule set_integrable_subset [OF intf], auto simp: min_def max_def) ``` hoelzl@59092 ` 746` ``` qed (insert assms, auto) ``` hoelzl@59092 ` 747` ```qed ``` hoelzl@59092 ` 748` ak2110@69173 ` 749` ```lemma%important einterval_antiderivative: ``` hoelzl@59092 ` 750` ``` fixes a b :: ereal and f :: "real \ 'a::euclidean_space" ``` hoelzl@59092 ` 751` ``` assumes "a < b" and contf: "\x :: real. a < x \ x < b \ isCont f x" ``` hoelzl@59092 ` 752` ``` shows "\F. \x :: real. a < x \ x < b \ (F has_vector_derivative f x) (at x)" ``` ak2110@69173 ` 753` ```proof%unimportant - ``` hoelzl@63329 ` 754` ``` from einterval_nonempty [OF \a < b\] obtain c :: real where [simp]: "a < c" "c < b" ``` lp15@68096 ` 755` ``` by (auto simp: einterval_def) ``` hoelzl@59092 ` 756` ``` let ?F = "(\u. LBINT y=c..u. f y)" ``` hoelzl@59092 ` 757` ``` show ?thesis ``` hoelzl@59092 ` 758` ``` proof (rule exI, clarsimp) ``` hoelzl@59092 ` 759` ``` fix x :: real ``` hoelzl@59092 ` 760` ``` assume [simp]: "a < x" "x < b" ``` hoelzl@59092 ` 761` ``` have 1: "a < min c x" by simp ``` hoelzl@63329 ` 762` ``` from einterval_nonempty [OF 1] obtain d :: real where [simp]: "a < d" "d < c" "d < x" ``` lp15@68096 ` 763` ``` by (auto simp: einterval_def) ``` hoelzl@59092 ` 764` ``` have 2: "max c x < b" by simp ``` hoelzl@63329 ` 765` ``` from einterval_nonempty [OF 2] obtain e :: real where [simp]: "c < e" "x < e" "e < b" ``` lp15@68096 ` 766` ``` by (auto simp: einterval_def) ``` lp15@68095 ` 767` ``` have "(?F has_vector_derivative f x) (at x within {d<..x. \d \ x; x \ e\ \ a < ereal x" ``` lp15@68095 ` 772` ``` using \a < ereal d\ ereal_less_ereal_Ex by auto ``` lp15@68095 ` 773` ``` show "\x. \d \ x; x \ e\ \ ereal x < b" ``` lp15@68095 ` 774` ``` using \ereal e < b\ ereal_less_eq(3) le_less_trans by blast ``` lp15@68095 ` 775` ``` qed ``` lp15@68095 ` 776` ``` then show "(?F has_vector_derivative f x) (at x within {d..e})" ``` lp15@68095 ` 777` ``` by (intro interval_integral_FTC2) (use \d < c\ \c < e\ \d < x\ \x < e\ in \linarith+\) ``` lp15@68095 ` 778` ``` qed auto ``` lp15@68095 ` 779` ``` then show "(?F has_vector_derivative f x) (at x)" ``` lp15@68096 ` 780` ``` by (force simp: has_vector_derivative_within_open [of _ "{d<..The substitution theorem\ ``` hoelzl@59092 ` 785` lp15@67974 ` 786` ```text\Once again, three versions: first, for finite intervals, and then two versions for ``` lp15@67974 ` 787` ``` arbitrary intervals.\ ``` hoelzl@63329 ` 788` ak2110@69173 ` 789` ```lemma%important interval_integral_substitution_finite: ``` hoelzl@59092 ` 790` ``` fixes a b :: real and f :: "real \ 'a::euclidean_space" ``` hoelzl@59092 ` 791` ``` assumes "a \ b" ``` hoelzl@59092 ` 792` ``` and derivg: "\x. a \ x \ x \ b \ (g has_real_derivative (g' x)) (at x within {a..b})" ``` hoelzl@59092 ` 793` ``` and contf : "continuous_on (g ` {a..b}) f" ``` hoelzl@59092 ` 794` ``` and contg': "continuous_on {a..b} g'" ``` hoelzl@59092 ` 795` ``` shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y" ``` ak2110@69173 ` 796` ```proof%unimportant- ``` hoelzl@59092 ` 797` ``` have v_derivg: "\x. a \ x \ x \ b \ (g has_vector_derivative (g' x)) (at x within {a..b})" ``` hoelzl@59092 ` 798` ``` using derivg unfolding has_field_derivative_iff_has_vector_derivative . ``` hoelzl@59092 ` 799` ``` then have contg [simp]: "continuous_on {a..b} g" ``` hoelzl@59092 ` 800` ``` by (rule continuous_on_vector_derivative) auto ``` lp15@68096 ` 801` ``` have 1: "\x\{a..b}. u = g x" if "min (g a) (g b) \ u" "u \ max (g a) (g b)" for u ``` lp15@68096 ` 802` ``` by (cases "g a \ g b") (use that assms IVT' [of g a u b] IVT2' [of g b u a] in \auto simp: min_def max_def\) ``` lp15@68096 ` 803` ``` obtain c d where g_im: "g ` {a..b} = {c..d}" and "c \ d" ``` lp15@68096 ` 804` ``` by (metis continuous_image_closed_interval contg \a \ b\) ``` lp15@68096 ` 805` ``` obtain F where derivF: ``` lp15@68096 ` 806` ``` "\x. \a \ x; x \ b\ \ (F has_vector_derivative (f (g x))) (at (g x) within (g ` {a..b}))" ``` lp15@68096 ` 807` ``` using continuous_on_subset [OF contf] g_im ``` lp15@68096 ` 808` ``` by (metis antiderivative_continuous atLeastAtMost_iff image_subset_iff set_eq_subset) ``` hoelzl@59092 ` 809` ``` have contfg: "continuous_on {a..b} (\x. f (g x))" ``` hoelzl@59092 ` 810` ``` by (blast intro: continuous_on_compose2 contf contg) ``` lp15@68096 ` 811` ``` have "LBINT x. indicat_real {a..b} x *\<^sub>R g' x *\<^sub>R f (g x) = F (g b) - F (g a)" ``` lp15@68096 ` 812` ``` apply (rule integral_FTC_atLeastAtMost ``` lp15@68096 ` 813` ``` [OF \a \ b\ vector_diff_chain_within[OF v_derivg derivF, unfolded comp_def]]) ``` hoelzl@59092 ` 814` ``` apply (auto intro!: continuous_on_scaleR contg' contfg) ``` hoelzl@59092 ` 815` ``` done ``` lp15@68096 ` 816` ``` then have "LBINT x=a..b. g' x *\<^sub>R f (g x) = F (g b) - F (g a)" ``` lp15@68096 ` 817` ``` by (simp add: assms interval_integral_Icc set_lebesgue_integral_def) ``` hoelzl@59092 ` 818` ``` moreover have "LBINT y=(g a)..(g b). f y = F (g b) - F (g a)" ``` lp15@68096 ` 819` ``` proof (rule interval_integral_FTC_finite) ``` lp15@68096 ` 820` ``` show "continuous_on {min (g a) (g b)..max (g a) (g b)} f" ``` lp15@68096 ` 821` ``` by (rule continuous_on_subset [OF contf]) (auto simp: image_def 1) ``` lp15@68096 ` 822` ``` show "(F has_vector_derivative f y) (at y within {min (g a) (g b)..max (g a) (g b)})" ``` lp15@68096 ` 823` ``` if y: "min (g a) (g b) \ y" "y \ max (g a) (g b)" for y ``` lp15@68096 ` 824` ``` proof - ``` lp15@68096 ` 825` ``` obtain x where "a \ x" "x \ b" "y = g x" ``` lp15@68096 ` 826` ``` using 1 y by force ``` lp15@68096 ` 827` ``` then show ?thesis ``` lp15@68096 ` 828` ``` by (auto simp: image_def intro!: 1 has_vector_derivative_within_subset [OF derivF]) ``` lp15@68096 ` 829` ``` qed ``` lp15@68096 ` 830` ``` qed ``` hoelzl@59092 ` 831` ``` ultimately show ?thesis by simp ``` hoelzl@59092 ` 832` ```qed ``` hoelzl@59092 ` 833` hoelzl@59092 ` 834` ```(* TODO: is it possible to lift the assumption here that g' is nonnegative? *) ``` hoelzl@59092 ` 835` ak2110@69173 ` 836` ```lemma%important interval_integral_substitution_integrable: ``` hoelzl@59092 ` 837` ``` fixes f :: "real \ 'a::euclidean_space" and a b u v :: ereal ``` hoelzl@63329 ` 838` ``` assumes "a < b" ``` hoelzl@59092 ` 839` ``` and deriv_g: "\x. a < ereal x \ ereal x < b \ DERIV g x :> g' x" ``` hoelzl@59092 ` 840` ``` and contf: "\x. a < ereal x \ ereal x < b \ isCont f (g x)" ``` hoelzl@59092 ` 841` ``` and contg': "\x. a < ereal x \ ereal x < b \ isCont g' x" ``` hoelzl@59092 ` 842` ``` and g'_nonneg: "\x. a \ ereal x \ ereal x \ b \ 0 \ g' x" ``` wenzelm@61973 ` 843` ``` and A: "((ereal \ g \ real_of_ereal) \ A) (at_right a)" ``` wenzelm@61973 ` 844` ``` and B: "((ereal \ g \ real_of_ereal) \ B) (at_left b)" ``` hoelzl@59092 ` 845` ``` and integrable: "set_integrable lborel (einterval a b) (\x. g' x *\<^sub>R f (g x))" ``` hoelzl@59092 ` 846` ``` and integrable2: "set_integrable lborel (einterval A B) (\x. f x)" ``` hoelzl@59092 ` 847` ``` shows "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))" ``` ak2110@69173 ` 848` ```proof%unimportant - ``` lp15@68095 ` 849` ``` obtain u l where approx [simp]: ``` lp15@68095 ` 850` ``` "einterval a b = (\i. {l i .. u i})" ``` lp15@68095 ` 851` ``` "incseq u" "decseq l" "\i. l i < u i" "\i. a < l i" "\i. u i < b" ``` lp15@68095 ` 852` ``` "l \ a" "u \ b" ``` lp15@68095 ` 853` ``` by (blast intro: einterval_Icc_approximation[OF \a < b\]) ``` hoelzl@59092 ` 854` ``` note less_imp_le [simp] ``` hoelzl@59092 ` 855` ``` have [simp]: "\x i. l i \ x \ a < ereal x" ``` hoelzl@59092 ` 856` ``` by (rule order_less_le_trans, rule approx, force) ``` hoelzl@59092 ` 857` ``` have [simp]: "\x i. x \ u i \ ereal x < b" ``` hoelzl@59092 ` 858` ``` by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) ``` lp15@68095 ` 859` ``` then have lessb[simp]: "\i. l i < b" ``` lp15@68095 ` 860` ``` using approx(4) less_eq_real_def by blast ``` hoelzl@63329 ` 861` ``` have [simp]: "\i. a < u i" ``` hoelzl@59092 ` 862` ``` by (rule order_less_trans, rule approx, auto, rule approx) ``` lp15@68095 ` 863` ``` have lle[simp]: "\i j. i \ j \ l j \ l i" by (rule decseqD, rule approx) ``` hoelzl@59092 ` 864` ``` have [simp]: "\i j. i \ j \ u i \ u j" by (rule incseqD, rule approx) ``` lp15@68095 ` 865` ``` have g_nondec [simp]: "g x \ g y" if "a < x" "x \ y" "y < b" for x y ``` lp15@68638 ` 866` ``` proof (rule DERIV_nonneg_imp_nondecreasing [OF \x \ y\], intro exI conjI) ``` lp15@68638 ` 867` ``` show "\u. x \ u \ u \ y \ (g has_real_derivative g' u) (at u)" ``` lp15@68095 ` 868` ``` by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that) ``` lp15@68638 ` 869` ``` show "\u. x \ u \ u \ y \ 0 \ g' u" ``` lp15@68095 ` 870` ``` by (meson assms(5) dual_order.trans le_ereal_le less_imp_le order_refl that) ``` lp15@68095 ` 871` ``` qed ``` hoelzl@59092 ` 872` ``` have "A \ B" and un: "einterval A B = (\i. {g(l i)<..i. g (l i)) \ A" ``` lp15@68096 ` 875` ``` using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def) ``` hoelzl@59092 ` 876` ``` by (drule_tac x = "\i. ereal (l i)" in spec, auto) ``` hoelzl@59092 ` 877` ``` hence A3: "\i. g (l i) \ A" ``` lp15@68532 ` 878` ``` by (intro decseq_ge, auto simp: decseq_def) ``` wenzelm@61969 ` 879` ``` have B2: "(\i. g (u i)) \ B" ``` lp15@68096 ` 880` ``` using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def) ``` hoelzl@59092 ` 881` ``` by (drule_tac x = "\i. ereal (u i)" in spec, auto) ``` hoelzl@59092 ` 882` ``` hence B3: "\i. g (u i) \ B" ``` lp15@68096 ` 883` ``` by (intro incseq_le, auto simp: incseq_def) ``` lp15@68095 ` 884` ``` have "ereal (g (l 0)) \ ereal (g (u 0))" ``` hoelzl@59092 ` 885` ``` by auto ``` lp15@68095 ` 886` ``` then show "A \ B" ``` lp15@68095 ` 887` ``` by (meson A3 B3 order.trans) ``` hoelzl@59092 ` 888` ``` { fix x :: real ``` hoelzl@63329 ` 889` ``` assume "A < x" and "x < B" ``` hoelzl@59092 ` 890` ``` then have "eventually (\i. ereal (g (l i)) < x \ x < ereal (g (u i))) sequentially" ``` lp15@68095 ` 891` ``` by (fast intro: eventually_conj order_tendstoD A2 B2) ``` hoelzl@59092 ` 892` ``` hence "\i. g (l i) < x \ x < g (u i)" ``` hoelzl@59092 ` 893` ``` by (simp add: eventually_sequentially, auto) ``` hoelzl@59092 ` 894` ``` } note AB = this ``` hoelzl@59092 ` 895` ``` show "einterval A B = (\i. {g(l i)<.. (\i. {g(l i)<..i. {g(l i)<.. einterval A B" ``` lp15@68095 ` 900` ``` proof (clarsimp simp add: einterval_def, intro conjI) ``` lp15@68095 ` 901` ``` show "\x i. \g (l i) < x; x < g (u i)\ \ A < ereal x" ``` lp15@68095 ` 902` ``` using A3 le_ereal_less by blast ``` lp15@68095 ` 903` ``` show "\x i. \g (l i) < x; x < g (u i)\ \ ereal x < B" ``` lp15@68095 ` 904` ``` using B3 ereal_le_less by blast ``` lp15@68095 ` 905` ``` qed ``` lp15@68095 ` 906` ``` qed ``` hoelzl@59092 ` 907` ``` qed ``` hoelzl@59092 ` 908` ``` (* finally, the main argument *) ``` lp15@68095 ` 909` ``` have eq1: "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" for i ``` lp15@68095 ` 910` ``` apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]]) ``` lp15@68095 ` 911` ``` unfolding has_field_derivative_iff_has_vector_derivative[symmetric] ``` lp15@68095 ` 912` ``` apply (auto intro!: continuous_at_imp_continuous_on contf contg') ``` lp15@68095 ` 913` ``` done ``` wenzelm@61969 ` 914` ``` have "(\i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) \ (LBINT x=a..b. g' x *\<^sub>R f (g x))" ``` wenzelm@61808 ` 915` ``` apply (rule interval_integral_Icc_approx_integrable [OF \a < b\ approx]) ``` hoelzl@59092 ` 916` ``` by (rule assms) ``` wenzelm@61969 ` 917` ``` hence 2: "(\i. (LBINT y=g (l i)..g (u i). f y)) \ (LBINT x=a..b. g' x *\<^sub>R f (g x))" ``` hoelzl@59092 ` 918` ``` by (simp add: eq1) ``` hoelzl@59092 ` 919` ``` have incseq: "incseq (\i. {g (l i)<..i. set_lebesgue_integral lborel {g (l i)<.. set_lebesgue_integral lborel (einterval A B) f" ``` lp15@68096 ` 925` ``` unfolding un by (rule set_integral_cont_up) (use incseq integrable2 un in auto) ``` lp15@68096 ` 926` ``` then have "(\i. (LBINT y=g (l i)..g (u i). f y)) \ (LBINT x = A..B. f x)" ``` lp15@68096 ` 927` ``` by (simp add: interval_lebesgue_integral_le_eq \A \ B\) ``` hoelzl@59092 ` 928` ``` thus ?thesis by (intro LIMSEQ_unique [OF _ 2]) ``` hoelzl@59092 ` 929` ```qed ``` hoelzl@59092 ` 930` hoelzl@59092 ` 931` ```(* TODO: the last two proofs are only slightly different. Factor out common part? ``` hoelzl@59092 ` 932` ``` An alternative: make the second one the main one, and then have another lemma ``` hoelzl@59092 ` 933` ``` that says that if f is nonnegative and all the other hypotheses hold, then it is integrable. *) ``` hoelzl@59092 ` 934` ak2110@69173 ` 935` ```lemma%important interval_integral_substitution_nonneg: ``` hoelzl@59092 ` 936` ``` fixes f g g':: "real \ real" and a b u v :: ereal ``` hoelzl@63329 ` 937` ``` assumes "a < b" ``` hoelzl@59092 ` 938` ``` and deriv_g: "\x. a < ereal x \ ereal x < b \ DERIV g x :> g' x" ``` hoelzl@59092 ` 939` ``` and contf: "\x. a < ereal x \ ereal x < b \ isCont f (g x)" ``` hoelzl@59092 ` 940` ``` and contg': "\x. a < ereal x \ ereal x < b \ isCont g' x" ``` hoelzl@59092 ` 941` ``` and f_nonneg: "\x. a < ereal x \ ereal x < b \ 0 \ f (g x)" (* TODO: make this AE? *) ``` hoelzl@59092 ` 942` ``` and g'_nonneg: "\x. a \ ereal x \ ereal x \ b \ 0 \ g' x" ``` wenzelm@61973 ` 943` ``` and A: "((ereal \ g \ real_of_ereal) \ A) (at_right a)" ``` wenzelm@61973 ` 944` ``` and B: "((ereal \ g \ real_of_ereal) \ B) (at_left b)" ``` hoelzl@59092 ` 945` ``` and integrable_fg: "set_integrable lborel (einterval a b) (\x. f (g x) * g' x)" ``` hoelzl@63329 ` 946` ``` shows ``` hoelzl@59092 ` 947` ``` "set_integrable lborel (einterval A B) f" ``` hoelzl@59092 ` 948` ``` "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))" ``` ak2110@69173 ` 949` ```proof%unimportant - ``` wenzelm@61808 ` 950` ``` from einterval_Icc_approximation[OF \a < b\] guess u l . note approx [simp] = this ``` hoelzl@59092 ` 951` ``` note less_imp_le [simp] ``` lp15@68096 ` 952` ``` have aless[simp]: "\x i. l i \ x \ a < ereal x" ``` hoelzl@59092 ` 953` ``` by (rule order_less_le_trans, rule approx, force) ``` lp15@68095 ` 954` ``` have lessb[simp]: "\x i. x \ u i \ ereal x < b" ``` hoelzl@59092 ` 955` ``` by (rule order_le_less_trans, subst ereal_less_eq(3), assumption, rule approx) ``` lp15@68095 ` 956` ``` have llb[simp]: "\i. l i < b" ``` lp15@68095 ` 957` ``` using lessb approx(4) less_eq_real_def by blast ``` lp15@68095 ` 958` ``` have alu[simp]: "\i. a < u i" ``` hoelzl@59092 ` 959` ``` by (rule order_less_trans, rule approx, auto, rule approx) ``` hoelzl@59092 ` 960` ``` have [simp]: "\i j. i \ j \ l j \ l i" by (rule decseqD, rule approx) ``` lp15@68095 ` 961` ``` have uleu[simp]: "\i j. i \ j \ u i \ u j" by (rule incseqD, rule approx) ``` lp15@68095 ` 962` ``` have g_nondec [simp]: "g x \ g y" if "a < x" "x \ y" "y < b" for x y ``` lp15@68638 ` 963` ``` proof (rule DERIV_nonneg_imp_nondecreasing [OF \x \ y\], intro exI conjI) ``` lp15@68638 ` 964` ``` show "\u. x \ u \ u \ y \ (g has_real_derivative g' u) (at u)" ``` lp15@68095 ` 965` ``` by (meson deriv_g ereal_less_eq(3) le_less_trans less_le_trans that) ``` lp15@68638 ` 966` ``` show "\u. x \ u \ u \ y \ 0 \ g' u" ``` lp15@68095 ` 967` ``` by (meson g'_nonneg less_ereal.simps(1) less_trans not_less that) ``` lp15@68095 ` 968` ``` qed ``` hoelzl@59092 ` 969` ``` have "A \ B" and un: "einterval A B = (\i. {g(l i)<..i. g (l i)) \ A" ``` lp15@68096 ` 972` ``` using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def) ``` hoelzl@59092 ` 973` ``` by (drule_tac x = "\i. ereal (l i)" in spec, auto) ``` hoelzl@59092 ` 974` ``` hence A3: "\i. g (l i) \ A" ``` lp15@68532 ` 975` ``` by (intro decseq_ge, auto simp: decseq_def) ``` wenzelm@61969 ` 976` ``` have B2: "(\i. g (u i)) \ B" ``` lp15@68096 ` 977` ``` using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def) ``` hoelzl@59092 ` 978` ``` by (drule_tac x = "\i. ereal (u i)" in spec, auto) ``` hoelzl@59092 ` 979` ``` hence B3: "\i. g (u i) \ B" ``` lp15@68096 ` 980` ``` by (intro incseq_le, auto simp: incseq_def) ``` lp15@68095 ` 981` ``` have "ereal (g (l 0)) \ ereal (g (u 0))" ``` hoelzl@59092 ` 982` ``` by auto ``` lp15@68095 ` 983` ``` then show "A \ B" ``` lp15@68095 ` 984` ``` by (meson A3 B3 order.trans) ``` hoelzl@59092 ` 985` ``` { fix x :: real ``` hoelzl@63329 ` 986` ``` assume "A < x" and "x < B" ``` hoelzl@59092 ` 987` ``` then have "eventually (\i. ereal (g (l i)) < x \ x < ereal (g (u i))) sequentially" ``` lp15@68096 ` 988` ``` by (fast intro: eventually_conj order_tendstoD A2 B2) ``` hoelzl@59092 ` 989` ``` hence "\i. g (l i) < x \ x < g (u i)" ``` hoelzl@59092 ` 990` ``` by (simp add: eventually_sequentially, auto) ``` hoelzl@59092 ` 991` ``` } note AB = this ``` hoelzl@59092 ` 992` ``` show "einterval A B = (\i. {g(l i)<.. (\i. {g (l i)<..i. {g (l i)<.. einterval A B" ``` lp15@68095 ` 997` ``` apply (clarsimp simp: einterval_def, intro conjI) ``` lp15@68095 ` 998` ``` using A3 le_ereal_less apply blast ``` lp15@68095 ` 999` ``` using B3 ereal_le_less by blast ``` lp15@68095 ` 1000` ``` qed ``` hoelzl@59092 ` 1001` ``` qed ``` lp15@68095 ` 1002` ``` (* finally, the main argument *) ``` lp15@68095 ` 1003` ``` have eq1: "(LBINT x=l i.. u i. (f (g x) * g' x)) = (LBINT y=g (l i)..g (u i). f y)" for i ``` lp15@68095 ` 1004` ``` proof - ``` lp15@68095 ` 1005` ``` have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" ``` lp15@68095 ` 1006` ``` apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]]) ``` lp15@68095 ` 1007` ``` unfolding has_field_derivative_iff_has_vector_derivative[symmetric] ``` lp15@68095 ` 1008` ``` apply (auto intro!: continuous_at_imp_continuous_on contf contg') ``` lp15@68095 ` 1009` ``` done ``` lp15@68095 ` 1010` ``` then show ?thesis ``` lp15@68095 ` 1011` ``` by (simp add: ac_simps) ``` lp15@68095 ` 1012` ``` qed ``` hoelzl@59092 ` 1013` ``` have incseq: "incseq (\i. {g (l i)<..c \ l i. c \ u i \ x = g c" if "g (l i) \ x" "x \ g (u i)" for x i ``` lp15@68095 ` 1018` ``` proof - ``` lp15@68095 ` 1019` ``` have "continuous_on {l i..u i} g" ``` lp15@68095 ` 1020` ``` by (force intro!: DERIV_isCont deriv_g continuous_at_imp_continuous_on) ``` lp15@68095 ` 1021` ``` with that show ?thesis ``` lp15@68095 ` 1022` ``` using IVT' [of g] approx(4) dual_order.strict_implies_order by blast ``` lp15@68095 ` 1023` ``` qed ``` lp15@68096 ` 1024` ``` have "continuous_on {g (l i)..g (u i)} f" for i ``` lp15@68096 ` 1025` ``` apply (intro continuous_intros continuous_at_imp_continuous_on) ``` lp15@68096 ` 1026` ``` using contf img by force ``` lp15@68096 ` 1027` ``` then have int_f: "\i. set_integrable lborel {g (l i)<..i. {g (l i)<..i. LBINT x=l i..u i. f (g x) * g' x) \ ?l" ``` lp15@68096 ` 1033` ``` by (intro assms interval_integral_Icc_approx_integrable [OF \a < b\ approx]) ``` lp15@68096 ` 1034` ``` hence "(\i. (LBINT y=g (l i)..g (u i). f y)) \ ?l" ``` lp15@68096 ` 1035` ``` by (simp add: eq1) ``` lp15@68096 ` 1036` ``` then show "(\i. set_lebesgue_integral lborel {g (l i)<.. ?l" ``` lp15@68096 ` 1037` ``` unfolding interval_lebesgue_integral_def by auto ``` lp15@68096 ` 1038` ``` have "\x i. g (l i) \ x \ x \ g (u i) \ 0 \ f x" ``` lp15@68096 ` 1039` ``` using aless f_nonneg img lessb by blast ``` lp15@68096 ` 1040` ``` then show "\x i. x \ {g (l i)<.. 0 \ f x" ``` lp15@68096 ` 1041` ``` using less_eq_real_def by auto ``` lp15@68096 ` 1042` ``` qed (auto simp: greaterThanLessThan_borel) ``` hoelzl@59092 ` 1043` ``` thus "set_integrable lborel (einterval A B) f" ``` hoelzl@59092 ` 1044` ``` by (simp add: un) ``` hoelzl@59092 ` 1045` hoelzl@59092 ` 1046` ``` have "(LBINT x=A..B. f x) = (LBINT x=a..b. g' x *\<^sub>R f (g x))" ``` hoelzl@59092 ` 1047` ``` proof (rule interval_integral_substitution_integrable) ``` hoelzl@59092 ` 1048` ``` show "set_integrable lborel (einterval a b) (\x. g' x *\<^sub>R f (g x))" ``` hoelzl@59092 ` 1049` ``` using integrable_fg by (simp add: ac_simps) ``` hoelzl@59092 ` 1050` ``` qed fact+ ``` hoelzl@59092 ` 1051` ``` then show "(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))" ``` hoelzl@59092 ` 1052` ``` by (simp add: ac_simps) ``` hoelzl@59092 ` 1053` ```qed ``` hoelzl@59092 ` 1054` hoelzl@59092 ` 1055` hoelzl@63941 ` 1056` ```syntax "_complex_lebesgue_borel_integral" :: "pttrn \ real \ complex" ``` hoelzl@63941 ` 1057` ``` ("(2CLBINT _. _)" [0,60] 60) ``` hoelzl@63941 ` 1058` hoelzl@63941 ` 1059` ```translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\x. f)" ``` hoelzl@63941 ` 1060` hoelzl@63941 ` 1061` ```syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \ real set \ real \ complex" ``` hoelzl@63941 ` 1062` ``` ("(3CLBINT _:_. _)" [0,60,61] 60) ``` hoelzl@59092 ` 1063` hoelzl@59092 ` 1064` ```translations ``` hoelzl@63941 ` 1065` ``` "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\x. f)" ``` hoelzl@59092 ` 1066` hoelzl@63329 ` 1067` ```abbreviation complex_interval_lebesgue_integral :: ``` hoelzl@59092 ` 1068` ``` "real measure \ ereal \ ereal \ (real \ complex) \ complex" where ``` hoelzl@59092 ` 1069` ``` "complex_interval_lebesgue_integral M a b f \ interval_lebesgue_integral M a b f" ``` hoelzl@59092 ` 1070` hoelzl@63329 ` 1071` ```abbreviation complex_interval_lebesgue_integrable :: ``` hoelzl@59092 ` 1072` ``` "real measure \ ereal \ ereal \ (real \ complex) \ bool" where ``` hoelzl@59092 ` 1073` ``` "complex_interval_lebesgue_integrable M a b f \ interval_lebesgue_integrable M a b f" ``` hoelzl@59092 ` 1074` hoelzl@59092 ` 1075` ```syntax ``` hoelzl@59092 ` 1076` ``` "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \ ereal \ ereal \ real \ complex" ``` hoelzl@59092 ` 1077` ``` ("(4CLBINT _=_.._. _)" [0,60,60,61] 60) ``` hoelzl@59092 ` 1078` hoelzl@59092 ` 1079` ```translations ``` hoelzl@59092 ` 1080` ``` "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\x. f)" ``` hoelzl@59092 ` 1081` ak2110@69173 ` 1082` ```lemma%important interval_integral_norm: ``` hoelzl@59092 ` 1083` ``` fixes f :: "real \ 'a :: {banach, second_countable_topology}" ``` hoelzl@59092 ` 1084` ``` shows "interval_lebesgue_integrable lborel a b f \ a \ b \ ``` hoelzl@59092 ` 1085` ``` norm (LBINT t=a..b. f t) \ LBINT t=a..b. norm (f t)" ``` ak2110@69173 ` 1086` ``` using%unimportant integral_norm_bound[of lborel "\x. indicator (einterval a b) x *\<^sub>R f x"] ``` ak2110@69173 ` 1087` ``` by%unimportant (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def) ``` hoelzl@59092 ` 1088` ak2110@69173 ` 1089` ```lemma%important interval_integral_norm2: ``` hoelzl@63329 ` 1090` ``` "interval_lebesgue_integrable lborel a b f \ ``` wenzelm@61945 ` 1091` ``` norm (LBINT t=a..b. f t) \ \LBINT t=a..b. norm (f t)\" ``` ak2110@69173 ` 1092` ```proof%unimportant (induct a b rule: linorder_wlog) ``` hoelzl@59092 ` 1093` ``` case (sym a b) then show ?case ``` hoelzl@59092 ` 1094` ``` by (simp add: interval_integral_endpoints_reverse[of a b] interval_integrable_endpoints_reverse[of a b]) ``` hoelzl@59092 ` 1095` ```next ``` hoelzl@63329 ` 1096` ``` case (le a b) ``` hoelzl@63329 ` 1097` ``` then have "\LBINT t=a..b. norm (f t)\ = LBINT t=a..b. norm (f t)" ``` hoelzl@59092 ` 1098` ``` using integrable_norm[of lborel "\x. indicator (einterval a b) x *\<^sub>R f x"] ``` lp15@68096 ` 1099` ``` by (auto simp: interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def ``` hoelzl@59092 ` 1100` ``` intro!: integral_nonneg_AE abs_of_nonneg) ``` hoelzl@59092 ` 1101` ``` then show ?case ``` hoelzl@59092 ` 1102` ``` using le by (simp add: interval_integral_norm) ``` hoelzl@59092 ` 1103` ```qed ``` hoelzl@59092 ` 1104` hoelzl@59092 ` 1105` ```(* TODO: should we have a library of facts like these? *) ``` hoelzl@59092 ` 1106` ```lemma integral_cos: "t \ 0 \ LBINT x=a..b. cos (t * x) = sin (t * b) / t - sin (t * a) / t" ``` hoelzl@59092 ` 1107` ``` apply (intro interval_integral_FTC_finite continuous_intros) ``` hoelzl@59092 ` 1108` ``` by (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative[symmetric]) ``` hoelzl@59092 ` 1109` hoelzl@59092 ` 1110` ```end ```