# HG changeset patch # User hoelzl # Date 1354886948 -3600 # Node ID bd68cf816dd3fad94b89a955fd1f5ec5ef82c7c4 # Parent f18b92f91818acfdaa4dc5dfc60c984f587d443c fundamental theorem of calculus for the Lebesgue integral diff -r f18b92f91818 -r bd68cf816dd3 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Dec 07 14:28:57 2012 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Dec 07 14:29:08 2012 +0100 @@ -1698,6 +1698,13 @@ by auto qed +lemma has_vector_derivative_withinI_DERIV: + assumes f: "DERIV f x :> y" shows "(f has_vector_derivative y) (at x within s)" + unfolding has_vector_derivative_def real_scaleR_def + apply (rule has_derivative_at_within) + using DERIV_conv_has_derivative[THEN iffD1, OF f] + apply (subst mult_commute) . + lemma vector_derivative_unique_at: assumes "(f has_vector_derivative f') (at x)" assumes "(f has_vector_derivative f'') (at x)" diff -r f18b92f91818 -r bd68cf816dd3 src/HOL/Probability/Lebesgue_Measure.thy --- a/src/HOL/Probability/Lebesgue_Measure.thy Fri Dec 07 14:28:57 2012 +0100 +++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri Dec 07 14:29:08 2012 +0100 @@ -1020,4 +1020,159 @@ shows "integral\<^isup>L lborel f = \x. f (p2e x) \((\\<^isub>M i\{.. real" + assumes f_borel: "f \ borel_measurable borel" and nonneg: "\x. 0 \ f x" + assumes f: "f integrable_on UNIV" + shows "integrable lborel f" +proof - + have "(\\<^isup>+ x. ereal (f x) \lborel) \ \" + using has_integral_iff_positive_integral_lborel[OF f_borel nonneg] f + by (auto simp: integrable_on_def) + moreover have "(\\<^isup>+ x. ereal (- f x) \lborel) = 0" + using f_borel nonneg by (subst positive_integral_0_iff_AE) auto + ultimately show ?thesis + using f_borel by (auto simp: integrable_def) +qed + +subsection {* Fundamental Theorem of Calculus for the Lebesgue integral *} + +lemma borel_integrable_atLeastAtMost: + fixes a b :: real + assumes f: "\x. a \ x \ x \ b \ isCont f x" + shows "integrable lborel (\x. f x * indicator {a .. b} x)" (is "integrable _ ?f") +proof cases + assume "a \ b" + + from isCont_Lb_Ub[OF `a \ b`, of f] f + obtain M L where + bounds: "\x. a \ x \ x \ b \ f x \ M" "\x. a \ x \ x \ b \ L \ f x" + by metis + + show ?thesis + proof (rule integrable_bound) + show "integrable lborel (\x. max \M\ \L\ * indicator {a..b} x)" + by (rule integral_cmul_indicator) simp_all + show "AE x in lborel. \?f x\ \ max \M\ \L\ * indicator {a..b} x" + proof (rule AE_I2) + fix x show "\?f x\ \ max \M\ \L\ * indicator {a..b} x" + using bounds[of x] by (auto split: split_indicator) + qed + + let ?g = "\x. if x = a then f a else if x = b then f b else if x \ {a <..< b} then f x else 0" + from f have "continuous_on {a <..< b} f" + by (subst continuous_on_eq_continuous_at) (auto simp add: continuous_isCont) + then have "?g \ borel_measurable borel" + using borel_measurable_continuous_on_open[of "{a <..< b }" f "\x. x" borel 0] + by (auto intro!: measurable_If[where P="\x. x = a"] measurable_If[where P="\x. x = b"]) + also have "?g = ?f" + using `a \ b` by (auto intro!: ext split: split_indicator) + finally show "?f \ borel_measurable lborel" + by simp + qed +qed simp + +lemma integral_FTC_atLeastAtMost: + fixes a b :: real + assumes "a \ b" + and F: "\x. a \ x \ x \ b \ DERIV F x :> f x" + and f: "\x. a \ x \ x \ b \ isCont f x" + shows "integral\<^isup>L lborel (\x. f x * indicator {a .. b} x) = F b - F a" +proof - + let ?f = "\x. f x * indicator {a .. b} x" + have "(?f has_integral (\x. ?f x \lborel)) UNIV" + using borel_integrable_atLeastAtMost[OF f] + by (rule borel_integral_has_integral) + moreover + have "(f has_integral F b - F a) {a .. b}" + by (intro fundamental_theorem_of_calculus has_vector_derivative_withinI_DERIV ballI assms) auto + then have "(?f has_integral F b - F a) {a .. b}" + by (subst has_integral_eq_eq[where g=f]) auto + then have "(?f has_integral F b - F a) UNIV" + by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto + ultimately show "integral\<^isup>L lborel ?f = F b - F a" + by (rule has_integral_unique) +qed + +text {* + +For the positive integral we replace continuity with Borel-measurability. + +*} + +lemma positive_integral_FTC_atLeastAtMost: + assumes f_borel: "f \ borel_measurable borel" + assumes f: "\x. x \ {a..b} \ DERIV F x :> f x" "\x. x \ {a..b} \ 0 \ f x" and "a \ b" + shows "(\\<^isup>+x. f x * indicator {a .. b} x \lborel) = F b - F a" +proof - + have i: "(f has_integral F b - F a) {a..b}" + by (intro fundamental_theorem_of_calculus ballI has_vector_derivative_withinI_DERIV assms) + have i: "((\x. f x * indicator {a..b} x) has_integral F b - F a) {a..b}" + by (rule has_integral_eq[OF _ i]) auto + have i: "((\x. f x * indicator {a..b} x) has_integral F b - F a) UNIV" + by (rule has_integral_on_superset[OF _ _ i]) auto + then have "(\\<^isup>+x. ereal (f x * indicator {a .. b} x) \lborel) = F b - F a" + using f f_borel + by (subst has_integral_iff_positive_integral_lborel[symmetric]) (auto split: split_indicator) + also have "(\\<^isup>+x. ereal (f x * indicator {a .. b} x) \lborel) = (\\<^isup>+x. ereal (f x) * indicator {a .. b} x \lborel)" + by (auto intro!: positive_integral_cong simp: indicator_def) + finally show ?thesis by simp +qed + +lemma positive_integral_FTC_atLeast: + fixes f :: "real \ real" + assumes f_borel: "f \ borel_measurable borel" + assumes f: "\x. a \ x \ DERIV F x :> f x" + assumes nonneg: "\x. a \ x \ 0 \ f x" + assumes lim: "(F ---> T) at_top" + shows "(\\<^isup>+x. ereal (f x) * indicator {a ..} x \lborel) = T - F a" +proof - + let ?f = "\(i::nat) (x::real). ereal (f x) * indicator {a..a + real i} x" + let ?fR = "\x. ereal (f x) * indicator {a ..} x" + have "\x. (SUP i::nat. ?f i x) = ?fR x" + proof (rule SUP_Lim_ereal) + show "\x. incseq (\i. ?f i x)" + using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator) + + fix x + from reals_Archimedean2[of "x - a"] guess n .. + then have "eventually (\n. ?f n x = ?fR x) sequentially" + by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator) + then show "(\n. ?f n x) ----> ?fR x" + by (rule Lim_eventually) + qed + then have "integral\<^isup>P lborel ?fR = (\\<^isup>+ x. (SUP i::nat. ?f i x) \lborel)" + by simp + also have "\ = (SUP i::nat. (\\<^isup>+ x. ?f i x \lborel))" + proof (rule positive_integral_monotone_convergence_SUP) + show "incseq ?f" + using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator) + show "\i. (?f i) \ borel_measurable lborel" + using f_borel by auto + show "\i x. 0 \ ?f i x" + using nonneg by (auto split: split_indicator) + qed + also have "\ = (SUP i::nat. F (a + real i) - F a)" + by (subst positive_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto + also have "\ = T - F a" + proof (rule SUP_Lim_ereal) + show "incseq (\n. ereal (F (a + real n) - F a))" + proof (simp add: incseq_def, safe) + fix m n :: nat assume "m \ n" + with f nonneg show "F (a + real m) \ F (a + real n)" + by (intro DERIV_nonneg_imp_nondecreasing[where f=F]) + (simp, metis add_increasing2 order_refl order_trans real_of_nat_ge_zero) + qed + have "(\x. F (a + real x)) ----> T" + apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top]) + apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl]) + apply (rule filterlim_real_sequentially) + done + then show "(\n. ereal (F (a + real n) - F a)) ----> ereal (T - F a)" + unfolding lim_ereal + by (intro tendsto_diff) auto + qed + finally show ?thesis . +qed + end