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