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