# 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 = \<integral>x. f (p2e x) \<partial>((\<Pi>\<^isub>M i\<in>{..<DIM('a)}. lborel))"
   using f by (simp add: borel_fubini_positiv_integral lebesgue_integral_def)
 
+lemma integrable_on_borel_integrable:
+  fixes f :: "'a::ordered_euclidean_space \<Rightarrow> real"
+  assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
+  assumes f: "f integrable_on UNIV" 
+  shows "integrable lborel f"
+proof -
+  have "(\<integral>\<^isup>+ x. ereal (f x) \<partial>lborel) \<noteq> \<infinity>" 
+    using has_integral_iff_positive_integral_lborel[OF f_borel nonneg] f
+    by (auto simp: integrable_on_def)
+  moreover have "(\<integral>\<^isup>+ x. ereal (- f x) \<partial>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: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
+  shows "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is "integrable _ ?f")
+proof cases
+  assume "a \<le> b"
+
+  from isCont_Lb_Ub[OF `a \<le> b`, of f] f
+  obtain M L where
+    bounds: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> f x \<le> M" "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> L \<le> f x"
+    by metis
+
+  show ?thesis
+  proof (rule integrable_bound)
+    show "integrable lborel (\<lambda>x. max \<bar>M\<bar> \<bar>L\<bar> * indicator {a..b} x)"
+      by (rule integral_cmul_indicator) simp_all
+    show "AE x in lborel. \<bar>?f x\<bar> \<le> max \<bar>M\<bar> \<bar>L\<bar> * indicator {a..b} x"
+    proof (rule AE_I2)
+      fix x show "\<bar>?f x\<bar> \<le> max \<bar>M\<bar> \<bar>L\<bar> * indicator {a..b} x"
+        using bounds[of x] by (auto split: split_indicator)
+    qed
+
+    let ?g = "\<lambda>x. if x = a then f a else if x = b then f b else if x \<in> {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 \<in> borel_measurable borel"
+      using borel_measurable_continuous_on_open[of "{a <..< b }" f "\<lambda>x. x" borel 0]
+      by (auto intro!: measurable_If[where P="\<lambda>x. x = a"] measurable_If[where P="\<lambda>x. x = b"])
+    also have "?g = ?f"
+      using `a \<le> b` by (auto intro!: ext split: split_indicator)
+    finally show "?f \<in> borel_measurable lborel"
+      by simp
+  qed
+qed simp
+
+lemma integral_FTC_atLeastAtMost:
+  fixes a b :: real
+  assumes "a \<le> b"
+    and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> DERIV F x :> f x"
+    and f: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
+  shows "integral\<^isup>L lborel (\<lambda>x. f x * indicator {a .. b} x) = F b - F a"
+proof -
+  let ?f = "\<lambda>x. f x * indicator {a .. b} x"
+  have "(?f has_integral (\<integral>x. ?f x \<partial>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 \<in> borel_measurable borel"
+  assumes f: "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" and "a \<le> b"
+  shows "(\<integral>\<^isup>+x. f x * indicator {a .. b} x \<partial>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: "((\<lambda>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: "((\<lambda>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 "(\<integral>\<^isup>+x. ereal (f x * indicator {a .. b} x) \<partial>lborel) = F b - F a"
+    using f f_borel
+    by (subst has_integral_iff_positive_integral_lborel[symmetric]) (auto split: split_indicator)
+  also have "(\<integral>\<^isup>+x. ereal (f x * indicator {a .. b} x) \<partial>lborel) = (\<integral>\<^isup>+x. ereal (f x) * indicator {a .. b} x \<partial>lborel)"
+    by (auto intro!: positive_integral_cong simp: indicator_def)
+  finally show ?thesis by simp
+qed
+
+lemma positive_integral_FTC_atLeast:
+  fixes f :: "real \<Rightarrow> real"
+  assumes f_borel: "f \<in> borel_measurable borel"
+  assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x" 
+  assumes nonneg: "\<And>x. a \<le> x \<Longrightarrow> 0 \<le> f x"
+  assumes lim: "(F ---> T) at_top"
+  shows "(\<integral>\<^isup>+x. ereal (f x) * indicator {a ..} x \<partial>lborel) = T - F a"
+proof -
+  let ?f = "\<lambda>(i::nat) (x::real). ereal (f x) * indicator {a..a + real i} x"
+  let ?fR = "\<lambda>x. ereal (f x) * indicator {a ..} x"
+  have "\<And>x. (SUP i::nat. ?f i x) = ?fR x"
+  proof (rule SUP_Lim_ereal)
+    show "\<And>x. incseq (\<lambda>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 (\<lambda>n. ?f n x = ?fR x) sequentially"
+      by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
+    then show "(\<lambda>n. ?f n x) ----> ?fR x"
+      by (rule Lim_eventually)
+  qed
+  then have "integral\<^isup>P lborel ?fR = (\<integral>\<^isup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
+    by simp
+  also have "\<dots> = (SUP i::nat. (\<integral>\<^isup>+ x. ?f i x \<partial>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 "\<And>i. (?f i) \<in> borel_measurable lborel"
+      using f_borel by auto
+    show "\<And>i x. 0 \<le> ?f i x"
+      using nonneg by (auto split: split_indicator)
+  qed
+  also have "\<dots> = (SUP i::nat. F (a + real i) - F a)"
+    by (subst positive_integral_FTC_atLeastAtMost[OF f_borel f nonneg]) auto
+  also have "\<dots> = T - F a"
+  proof (rule SUP_Lim_ereal)
+    show "incseq (\<lambda>n. ereal (F (a + real n) - F a))"
+    proof (simp add: incseq_def, safe)
+      fix m n :: nat assume "m \<le> n"
+      with f nonneg show "F (a + real m) \<le> 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 "(\<lambda>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 "(\<lambda>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