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