move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
authorhoelzl
Fri Sep 16 13:56:51 2016 +0200 (2016-09-16)
changeset 63886685fb01256af
parent 63885 a6cd18af8bf9
child 63890 3dd6bde2502d
child 63891 8947157ca830
child 63895 9afa979137da
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Embed_Measure.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Interval_Integral.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
src/HOL/Analysis/Set_Integral.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Probability/Characteristic_Functions.thy
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Levy.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/SPMF.thy
src/HOL/Probability/Sinc_Integral.thy
     1.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Thu Sep 15 22:41:05 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Fri Sep 16 13:56:51 2016 +0200
     1.3 @@ -187,7 +187,7 @@
     1.4        using U by (auto
     1.5            intro: borel_measurable_simple_function
     1.6            intro!: borel_measurable_enn2real borel_measurable_times
     1.7 -          simp: U'_def zero_le_mult_iff enn2real_nonneg)
     1.8 +          simp: U'_def zero_le_mult_iff)
     1.9      show "incseq U'"
    1.10        using U(2,3)
    1.11        by (auto simp: incseq_def le_fun_def image_iff eq_commute U'_def indicator_def enn2real_mono)
    1.12 @@ -212,7 +212,7 @@
    1.13      ultimately have U': "(\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z) = U' i"
    1.14        by (simp add: U'_def fun_eq_iff)
    1.15      have "\<And>x. x \<in> U' i ` space M \<Longrightarrow> 0 \<le> x"
    1.16 -      by (auto simp: U'_def enn2real_nonneg)
    1.17 +      by (auto simp: U'_def)
    1.18      with fin have "P (\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z)"
    1.19      proof induct
    1.20        case empty from set[of "{}"] show ?case
    1.21 @@ -866,7 +866,7 @@
    1.22      simple_bochner_integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
    1.23    by (simp add: simple_bochner_integrable.simps space_restrict_space
    1.24      simple_function_restrict_space[OF \<Omega>] emeasure_restrict_space[OF \<Omega>] Collect_restrict
    1.25 -    indicator_eq_0_iff conj_ac)
    1.26 +    indicator_eq_0_iff conj_left_commute)
    1.27  
    1.28  lemma simple_bochner_integral_restrict_space:
    1.29    fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
    1.30 @@ -1624,7 +1624,7 @@
    1.31        with seq show "\<exists>N. \<forall>n\<ge>N. 0 \<le> integral\<^sup>L M (U n)"
    1.32          by auto
    1.33      qed
    1.34 -  qed (auto simp: measure_nonneg integrable_mult_left_iff)
    1.35 +  qed (auto simp: integrable_mult_left_iff)
    1.36    also have "\<dots> = integral\<^sup>L M f"
    1.37      using nonneg by (auto intro!: integral_cong_AE)
    1.38    finally show ?thesis .
    1.39 @@ -2466,10 +2466,10 @@
    1.40    shows "ennreal (\<integral>x. enn2real (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
    1.41  proof (subst nn_integral_eq_integral[symmetric])
    1.42    show "integrable M (\<lambda>x. enn2real (f x))"
    1.43 -    using ae by (intro integrable_const_bound[where B=B]) (auto simp: enn2real_leI enn2real_nonneg)
    1.44 +    using ae by (intro integrable_const_bound[where B=B]) (auto simp: enn2real_leI)
    1.45    show "(\<integral>\<^sup>+ x. ennreal (enn2real (f x)) \<partial>M) = integral\<^sup>N M f"
    1.46      using ae by (intro nn_integral_cong_AE) (auto simp: le_less_trans[OF _ ennreal_less_top])
    1.47 -qed (auto simp: enn2real_nonneg)
    1.48 +qed auto
    1.49  
    1.50  lemma (in finite_measure) integral_less_AE:
    1.51    fixes X Y :: "'a \<Rightarrow> real"
     2.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 15 22:41:05 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Sep 16 13:56:51 2016 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
     2.5  
     2.6  theory Cartesian_Euclidean_Space
     2.7 -imports Finite_Cartesian_Product Henstock_Kurzweil_Integration
     2.8 +imports Finite_Cartesian_Product Derivative (* Henstock_Kurzweil_Integration *)
     2.9  begin
    2.10  
    2.11  lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
    2.12 @@ -927,7 +927,6 @@
    2.13    unfolding dot_matrix_product transpose_columnvector[symmetric]
    2.14      dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
    2.15  
    2.16 -
    2.17  lemma infnorm_cart:"infnorm (x::real^'n) = Sup {\<bar>x$i\<bar> |i. i\<in>UNIV}"
    2.18    by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right)
    2.19  
    2.20 @@ -1409,12 +1408,6 @@
    2.21    apply (rule bounded_linearI[where K=1])
    2.22    using component_le_norm_cart[of _ k] unfolding real_norm_def by auto
    2.23  
    2.24 -lemma integral_component_eq_cart[simp]:
    2.25 -  fixes f :: "'n::euclidean_space \<Rightarrow> real^'m"
    2.26 -  assumes "f integrable_on s"
    2.27 -  shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
    2.28 -  using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] .
    2.29 -
    2.30  lemma interval_split_cart:
    2.31    "{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
    2.32    "cbox a b \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}"
     3.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Sep 15 22:41:05 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Sep 16 13:56:51 2016 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  section \<open>Complex Analysis Basics\<close>
     3.5  
     3.6  theory Complex_Analysis_Basics
     3.7 -imports Cartesian_Euclidean_Space "~~/src/HOL/Library/Nonpos_Ints"
     3.8 +imports Henstock_Kurzweil_Integration "~~/src/HOL/Library/Nonpos_Ints"
     3.9  begin
    3.10  
    3.11  
     4.1 --- a/src/HOL/Analysis/Derivative.thy	Thu Sep 15 22:41:05 2016 +0200
     4.2 +++ b/src/HOL/Analysis/Derivative.thy	Fri Sep 16 13:56:51 2016 +0200
     4.3 @@ -9,6 +9,9 @@
     4.4  imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
     4.5  begin
     4.6  
     4.7 +lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
     4.8 +  by (rule bounded_linear_inner_left)
     4.9 +
    4.10  lemma onorm_inner_left:
    4.11    assumes "bounded_linear r"
    4.12    shows "onorm (\<lambda>x. r x \<bullet> f) \<le> onorm r * norm f"
    4.13 @@ -2906,5 +2909,4 @@
    4.14      by eventually_elim (auto simp: dist_norm field_simps)
    4.15  qed (auto intro!: bounded_linear_intros simp: split_beta')
    4.16  
    4.17 -
    4.18  end
     5.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Thu Sep 15 22:41:05 2016 +0200
     5.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Fri Sep 16 13:56:51 2016 +0200
     5.3 @@ -47,7 +47,7 @@
     5.4  lemma sets_embed_eq_vimage_algebra:
     5.5    assumes "inj_on f (space M)"
     5.6    shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)"
     5.7 -  by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 simple_image
     5.8 +  by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 Setcompr_eq_image
     5.9             dest: sets.sets_into_space
    5.10             intro!: image_cong the_inv_into_vimage[symmetric])
    5.11  
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 16 13:56:51 2016 +0200
     6.3 @@ -0,0 +1,606 @@
     6.4 +theory Equivalence_Lebesgue_Henstock_Integration
     6.5 +  imports Lebesgue_Measure Henstock_Kurzweil_Integration
     6.6 +begin
     6.7 +
     6.8 +subsection \<open>Equivalence Lebesgue integral on @{const lborel} and HK-integral\<close>
     6.9 +
    6.10 +lemma has_integral_measure_lborel:
    6.11 +  fixes A :: "'a::euclidean_space set"
    6.12 +  assumes A[measurable]: "A \<in> sets borel" and finite: "emeasure lborel A < \<infinity>"
    6.13 +  shows "((\<lambda>x. 1) has_integral measure lborel A) A"
    6.14 +proof -
    6.15 +  { fix l u :: 'a
    6.16 +    have "((\<lambda>x. 1) has_integral measure lborel (box l u)) (box l u)"
    6.17 +    proof cases
    6.18 +      assume "\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b"
    6.19 +      then show ?thesis
    6.20 +        apply simp
    6.21 +        apply (subst has_integral_restrict[symmetric, OF box_subset_cbox])
    6.22 +        apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"])
    6.23 +        using has_integral_const[of "1::real" l u]
    6.24 +        apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases)
    6.25 +        done
    6.26 +    next
    6.27 +      assume "\<not> (\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b)"
    6.28 +      then have "box l u = {}"
    6.29 +        unfolding box_eq_empty by (auto simp: not_le intro: less_imp_le)
    6.30 +      then show ?thesis
    6.31 +        by simp
    6.32 +    qed }
    6.33 +  note has_integral_box = this
    6.34 +
    6.35 +  { fix a b :: 'a let ?M = "\<lambda>A. measure lborel (A \<inter> box a b)"
    6.36 +    have "Int_stable  (range (\<lambda>(a, b). box a b))"
    6.37 +      by (auto simp: Int_stable_def box_Int_box)
    6.38 +    moreover have "(range (\<lambda>(a, b). box a b)) \<subseteq> Pow UNIV"
    6.39 +      by auto
    6.40 +    moreover have "A \<in> sigma_sets UNIV (range (\<lambda>(a, b). box a b))"
    6.41 +       using A unfolding borel_eq_box by simp
    6.42 +    ultimately have "((\<lambda>x. 1) has_integral ?M A) (A \<inter> box a b)"
    6.43 +    proof (induction rule: sigma_sets_induct_disjoint)
    6.44 +      case (basic A) then show ?case
    6.45 +        by (auto simp: box_Int_box has_integral_box)
    6.46 +    next
    6.47 +      case empty then show ?case
    6.48 +        by simp
    6.49 +    next
    6.50 +      case (compl A)
    6.51 +      then have [measurable]: "A \<in> sets borel"
    6.52 +        by (simp add: borel_eq_box)
    6.53 +
    6.54 +      have "((\<lambda>x. 1) has_integral ?M (box a b)) (box a b)"
    6.55 +        by (simp add: has_integral_box)
    6.56 +      moreover have "((\<lambda>x. if x \<in> A \<inter> box a b then 1 else 0) has_integral ?M A) (box a b)"
    6.57 +        by (subst has_integral_restrict) (auto intro: compl)
    6.58 +      ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
    6.59 +        by (rule has_integral_sub)
    6.60 +      then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
    6.61 +        by (rule has_integral_cong[THEN iffD1, rotated 1]) auto
    6.62 +      then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box a b)"
    6.63 +        by (subst (asm) has_integral_restrict) auto
    6.64 +      also have "?M (box a b) - ?M A = ?M (UNIV - A)"
    6.65 +        by (subst measure_Diff[symmetric]) (auto simp: emeasure_lborel_box_eq Diff_Int_distrib2)
    6.66 +      finally show ?case .
    6.67 +    next
    6.68 +      case (union F)
    6.69 +      then have [measurable]: "\<And>i. F i \<in> sets borel"
    6.70 +        by (simp add: borel_eq_box subset_eq)
    6.71 +      have "((\<lambda>x. if x \<in> UNION UNIV F \<inter> box a b then 1 else 0) has_integral ?M (\<Union>i. F i)) (box a b)"
    6.72 +      proof (rule has_integral_monotone_convergence_increasing)
    6.73 +        let ?f = "\<lambda>k x. \<Sum>i<k. if x \<in> F i \<inter> box a b then 1 else 0 :: real"
    6.74 +        show "\<And>k. (?f k has_integral (\<Sum>i<k. ?M (F i))) (box a b)"
    6.75 +          using union.IH by (auto intro!: has_integral_setsum simp del: Int_iff)
    6.76 +        show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
    6.77 +          by (intro setsum_mono2) auto
    6.78 +        from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
    6.79 +          by (auto simp add: disjoint_family_on_def)
    6.80 +        show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)"
    6.81 +          apply (auto simp: * setsum.If_cases Iio_Int_singleton)
    6.82 +          apply (rule_tac k="Suc xa" in LIMSEQ_offset)
    6.83 +          apply simp
    6.84 +          done
    6.85 +        have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)"
    6.86 +          by (intro emeasure_mono) auto
    6.87 +
    6.88 +        with union(1) show "(\<lambda>k. \<Sum>i<k. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F i)"
    6.89 +          unfolding sums_def[symmetric] UN_extend_simps
    6.90 +          by (intro measure_UNION) (auto simp: disjoint_family_on_def emeasure_lborel_box_eq top_unique)
    6.91 +      qed
    6.92 +      then show ?case
    6.93 +        by (subst (asm) has_integral_restrict) auto
    6.94 +    qed }
    6.95 +  note * = this
    6.96 +
    6.97 +  show ?thesis
    6.98 +  proof (rule has_integral_monotone_convergence_increasing)
    6.99 +    let ?B = "\<lambda>n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One) :: 'a set"
   6.100 +    let ?f = "\<lambda>n::nat. \<lambda>x. if x \<in> A \<inter> ?B n then 1 else 0 :: real"
   6.101 +    let ?M = "\<lambda>n. measure lborel (A \<inter> ?B n)"
   6.102 +
   6.103 +    show "\<And>n::nat. (?f n has_integral ?M n) A"
   6.104 +      using * by (subst has_integral_restrict) simp_all
   6.105 +    show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
   6.106 +      by (auto simp: box_def)
   6.107 +    { fix x assume "x \<in> A"
   6.108 +      moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) \<longlonglongrightarrow> indicator (\<Union>k::nat. A \<inter> ?B k) x"
   6.109 +        by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def)
   6.110 +      ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) \<longlonglongrightarrow> 1"
   6.111 +        by (simp add: indicator_def UN_box_eq_UNIV) }
   6.112 +
   6.113 +    have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> emeasure lborel (\<Union>n::nat. A \<inter> ?B n)"
   6.114 +      by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def)
   6.115 +    also have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) = (\<lambda>n. measure lborel (A \<inter> ?B n))"
   6.116 +    proof (intro ext emeasure_eq_ennreal_measure)
   6.117 +      fix n have "emeasure lborel (A \<inter> ?B n) \<le> emeasure lborel (?B n)"
   6.118 +        by (intro emeasure_mono) auto
   6.119 +      then show "emeasure lborel (A \<inter> ?B n) \<noteq> top"
   6.120 +        by (auto simp: top_unique)
   6.121 +    qed
   6.122 +    finally show "(\<lambda>n. measure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> measure lborel A"
   6.123 +      using emeasure_eq_ennreal_measure[of lborel A] finite
   6.124 +      by (simp add: UN_box_eq_UNIV less_top)
   6.125 +  qed
   6.126 +qed
   6.127 +
   6.128 +lemma nn_integral_has_integral:
   6.129 +  fixes f::"'a::euclidean_space \<Rightarrow> real"
   6.130 +  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
   6.131 +  shows "(f has_integral r) UNIV"
   6.132 +using f proof (induct f arbitrary: r rule: borel_measurable_induct_real)
   6.133 +  case (set A)
   6.134 +  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
   6.135 +    by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator)
   6.136 +  with set show ?case
   6.137 +    by (simp add: ennreal_indicator measure_def) (simp add: indicator_def)
   6.138 +next
   6.139 +  case (mult g c)
   6.140 +  then have "ennreal c * (\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal r"
   6.141 +    by (subst nn_integral_cmult[symmetric]) (auto simp: ennreal_mult)
   6.142 +  with \<open>0 \<le> r\<close> \<open>0 \<le> c\<close>
   6.143 +  obtain r' where "(c = 0 \<and> r = 0) \<or> (0 \<le> r' \<and> (\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel) = ennreal r' \<and> r = c * r')"
   6.144 +    by (cases "\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel" rule: ennreal_cases)
   6.145 +       (auto split: if_split_asm simp: ennreal_mult_top ennreal_mult[symmetric])
   6.146 +  with mult show ?case
   6.147 +    by (auto intro!: has_integral_cmult_real)
   6.148 +next
   6.149 +  case (add g h)
   6.150 +  then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lborel) = (\<integral>\<^sup>+ x. h x \<partial>lborel) + (\<integral>\<^sup>+ x. g x \<partial>lborel)"
   6.151 +    by (simp add: nn_integral_add)
   6.152 +  with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b"
   6.153 +    by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
   6.154 +       (auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus)
   6.155 +  with add show ?case
   6.156 +    by (auto intro!: has_integral_add)
   6.157 +next
   6.158 +  case (seq U)
   6.159 +  note seq(1)[measurable] and f[measurable]
   6.160 +
   6.161 +  { fix i x
   6.162 +    have "U i x \<le> f x"
   6.163 +      using seq(5)
   6.164 +      apply (rule LIMSEQ_le_const)
   6.165 +      using seq(4)
   6.166 +      apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def)
   6.167 +      done }
   6.168 +  note U_le_f = this
   6.169 +
   6.170 +  { fix i
   6.171 +    have "(\<integral>\<^sup>+x. U i x \<partial>lborel) \<le> (\<integral>\<^sup>+x. f x \<partial>lborel)"
   6.172 +      using seq(2) f(2) U_le_f by (intro nn_integral_mono) simp
   6.173 +    then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p" "p \<le> r" "0 \<le> p"
   6.174 +      using seq(6) \<open>0\<le>r\<close> by (cases "\<integral>\<^sup>+x. U i x \<partial>lborel" rule: ennreal_cases) (auto simp: top_unique)
   6.175 +    moreover note seq
   6.176 +    ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV"
   6.177 +      by auto }
   6.178 +  then obtain p where p: "\<And>i. (\<integral>\<^sup>+x. ennreal (U i x) \<partial>lborel) = ennreal (p i)"
   6.179 +    and bnd: "\<And>i. p i \<le> r" "\<And>i. 0 \<le> p i"
   6.180 +    and U_int: "\<And>i.(U i has_integral (p i)) UNIV" by metis
   6.181 +
   6.182 +  have int_eq: "\<And>i. integral UNIV (U i) = p i" using U_int by (rule integral_unique)
   6.183 +
   6.184 +  have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) \<longlonglongrightarrow> integral UNIV f"
   6.185 +  proof (rule monotone_convergence_increasing)
   6.186 +    show "\<forall>k. U k integrable_on UNIV" using U_int by auto
   6.187 +    show "\<forall>k. \<forall>x\<in>UNIV. U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def)
   6.188 +    then show "bounded {integral UNIV (U k) |k. True}"
   6.189 +      using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r])
   6.190 +    show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) \<longlonglongrightarrow> f x"
   6.191 +      using seq by auto
   6.192 +  qed
   6.193 +  moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. f x \<partial>lborel)"
   6.194 +    using seq f(2) U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
   6.195 +  ultimately have "integral UNIV f = r"
   6.196 +    by (auto simp add: bnd int_eq p seq intro: LIMSEQ_unique)
   6.197 +  with * show ?case
   6.198 +    by (simp add: has_integral_integral)
   6.199 +qed
   6.200 +
   6.201 +lemma nn_integral_lborel_eq_integral:
   6.202 +  fixes f::"'a::euclidean_space \<Rightarrow> real"
   6.203 +  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
   6.204 +  shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = integral UNIV f"
   6.205 +proof -
   6.206 +  from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
   6.207 +    by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
   6.208 +  then show ?thesis
   6.209 +    using nn_integral_has_integral[OF f(1,2) r] by (simp add: integral_unique)
   6.210 +qed
   6.211 +
   6.212 +lemma nn_integral_integrable_on:
   6.213 +  fixes f::"'a::euclidean_space \<Rightarrow> real"
   6.214 +  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
   6.215 +  shows "f integrable_on UNIV"
   6.216 +proof -
   6.217 +  from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
   6.218 +    by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
   6.219 +  then show ?thesis
   6.220 +    by (intro has_integral_integrable[where i=r] nn_integral_has_integral[where r=r] f)
   6.221 +qed
   6.222 +
   6.223 +lemma nn_integral_has_integral_lborel:
   6.224 +  fixes f :: "'a::euclidean_space \<Rightarrow> real"
   6.225 +  assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
   6.226 +  assumes I: "(f has_integral I) UNIV"
   6.227 +  shows "integral\<^sup>N lborel f = I"
   6.228 +proof -
   6.229 +  from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" by auto
   6.230 +  from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
   6.231 +  let ?B = "\<lambda>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One) :: 'a set"
   6.232 +
   6.233 +  note F(1)[THEN borel_measurable_simple_function, measurable]
   6.234 +
   6.235 +  have "0 \<le> I"
   6.236 +    using I by (rule has_integral_nonneg) (simp add: nonneg)
   6.237 +
   6.238 +  have F_le_f: "enn2real (F i x) \<le> f x" for i x
   6.239 +    using F(3,4)[where x=x] nonneg SUP_upper[of i UNIV "\<lambda>i. F i x"]
   6.240 +    by (cases "F i x" rule: ennreal_cases) auto
   6.241 +  let ?F = "\<lambda>i x. F i x * indicator (?B i) x"
   6.242 +  have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (SUP i. integral\<^sup>N lborel (\<lambda>x. ?F i x))"
   6.243 +  proof (subst nn_integral_monotone_convergence_SUP[symmetric])
   6.244 +    { fix x
   6.245 +      obtain j where j: "x \<in> ?B j"
   6.246 +        using UN_box_eq_UNIV by auto
   6.247 +
   6.248 +      have "ennreal (f x) = (SUP i. F i x)"
   6.249 +        using F(4)[of x] nonneg[of x] by (simp add: max_def)
   6.250 +      also have "\<dots> = (SUP i. ?F i x)"
   6.251 +      proof (rule SUP_eq)
   6.252 +        fix i show "\<exists>j\<in>UNIV. F i x \<le> ?F j x"
   6.253 +          using j F(2)
   6.254 +          by (intro bexI[of _ "max i j"])
   6.255 +             (auto split: split_max split_indicator simp: incseq_def le_fun_def box_def)
   6.256 +      qed (auto intro!: F split: split_indicator)
   6.257 +      finally have "ennreal (f x) =  (SUP i. ?F i x)" . }
   6.258 +    then show "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (\<integral>\<^sup>+ x. (SUP i. ?F i x) \<partial>lborel)"
   6.259 +      by simp
   6.260 +  qed (insert F, auto simp: incseq_def le_fun_def box_def split: split_indicator)
   6.261 +  also have "\<dots> \<le> ennreal I"
   6.262 +  proof (rule SUP_least)
   6.263 +    fix i :: nat
   6.264 +    have finite_F: "(\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel) < \<infinity>"
   6.265 +    proof (rule nn_integral_bound_simple_function)
   6.266 +      have "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} \<le>
   6.267 +        emeasure lborel (?B i)"
   6.268 +        by (intro emeasure_mono)  (auto split: split_indicator)
   6.269 +      then show "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} < \<infinity>"
   6.270 +        by (auto simp: less_top[symmetric] top_unique)
   6.271 +    qed (auto split: split_indicator
   6.272 +              intro!: F simple_function_compose1[where g="enn2real"] simple_function_ennreal)
   6.273 +
   6.274 +    have int_F: "(\<lambda>x. enn2real (F i x) * indicator (?B i) x) integrable_on UNIV"
   6.275 +      using F(4) finite_F
   6.276 +      by (intro nn_integral_integrable_on) (auto split: split_indicator simp: enn2real_nonneg)
   6.277 +
   6.278 +    have "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) =
   6.279 +      (\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel)"
   6.280 +      using F(3,4)
   6.281 +      by (intro nn_integral_cong) (auto simp: image_iff eq_commute split: split_indicator)
   6.282 +    also have "\<dots> = ennreal (integral UNIV (\<lambda>x. enn2real (F i x) * indicator (?B i) x))"
   6.283 +      using F
   6.284 +      by (intro nn_integral_lborel_eq_integral[OF _ _ finite_F])
   6.285 +         (auto split: split_indicator intro: enn2real_nonneg)
   6.286 +    also have "\<dots> \<le> ennreal I"
   6.287 +      by (auto intro!: has_integral_le[OF integrable_integral[OF int_F] I] nonneg F_le_f
   6.288 +               simp: \<open>0 \<le> I\<close> split: split_indicator )
   6.289 +    finally show "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) \<le> ennreal I" .
   6.290 +  qed
   6.291 +  finally have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) < \<infinity>"
   6.292 +    by (auto simp: less_top[symmetric] top_unique)
   6.293 +  from nn_integral_lborel_eq_integral[OF assms(1,2) this] I show ?thesis
   6.294 +    by (simp add: integral_unique)
   6.295 +qed
   6.296 +
   6.297 +lemma has_integral_iff_emeasure_lborel:
   6.298 +  fixes A :: "'a::euclidean_space set"
   6.299 +  assumes A[measurable]: "A \<in> sets borel" and [simp]: "0 \<le> r"
   6.300 +  shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ennreal r"
   6.301 +proof (cases "emeasure lborel A = \<infinity>")
   6.302 +  case emeasure_A: True
   6.303 +  have "\<not> (\<lambda>x. 1::real) integrable_on A"
   6.304 +  proof
   6.305 +    assume int: "(\<lambda>x. 1::real) integrable_on A"
   6.306 +    then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV"
   6.307 +      unfolding indicator_def[abs_def] integrable_restrict_univ .
   6.308 +    then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV"
   6.309 +      by auto
   6.310 +    from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False
   6.311 +      by (simp add: ennreal_indicator)
   6.312 +  qed
   6.313 +  with emeasure_A show ?thesis
   6.314 +    by auto
   6.315 +next
   6.316 +  case False
   6.317 +  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
   6.318 +    by (simp add: has_integral_measure_lborel less_top)
   6.319 +  with False show ?thesis
   6.320 +    by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
   6.321 +qed
   6.322 +
   6.323 +lemma has_integral_integral_real:
   6.324 +  fixes f::"'a::euclidean_space \<Rightarrow> real"
   6.325 +  assumes f: "integrable lborel f"
   6.326 +  shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
   6.327 +using f proof induct
   6.328 +  case (base A c) then show ?case
   6.329 +    by (auto intro!: has_integral_mult_left simp: )
   6.330 +       (simp add: emeasure_eq_ennreal_measure indicator_def has_integral_measure_lborel)
   6.331 +next
   6.332 +  case (add f g) then show ?case
   6.333 +    by (auto intro!: has_integral_add)
   6.334 +next
   6.335 +  case (lim f s)
   6.336 +  show ?case
   6.337 +  proof (rule has_integral_dominated_convergence)
   6.338 +    show "\<And>i. (s i has_integral integral\<^sup>L lborel (s i)) UNIV" by fact
   6.339 +    show "(\<lambda>x. norm (2 * f x)) integrable_on UNIV"
   6.340 +      using \<open>integrable lborel f\<close>
   6.341 +      by (intro nn_integral_integrable_on)
   6.342 +         (auto simp: integrable_iff_bounded abs_mult  nn_integral_cmult ennreal_mult ennreal_mult_less_top)
   6.343 +    show "\<And>k. \<forall>x\<in>UNIV. norm (s k x) \<le> norm (2 * f x)"
   6.344 +      using lim by (auto simp add: abs_mult)
   6.345 +    show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) \<longlonglongrightarrow> f x"
   6.346 +      using lim by auto
   6.347 +    show "(\<lambda>k. integral\<^sup>L lborel (s k)) \<longlonglongrightarrow> integral\<^sup>L lborel f"
   6.348 +      using lim lim(1)[THEN borel_measurable_integrable]
   6.349 +      by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
   6.350 +  qed
   6.351 +qed
   6.352 +
   6.353 +context
   6.354 +  fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   6.355 +begin
   6.356 +
   6.357 +lemma has_integral_integral_lborel:
   6.358 +  assumes f: "integrable lborel f"
   6.359 +  shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
   6.360 +proof -
   6.361 +  have "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b)) UNIV"
   6.362 +    using f by (intro has_integral_setsum finite_Basis ballI has_integral_scaleR_left has_integral_integral_real) auto
   6.363 +  also have eq_f: "(\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) = f"
   6.364 +    by (simp add: fun_eq_iff euclidean_representation)
   6.365 +  also have "(\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lborel f"
   6.366 +    using f by (subst (2) eq_f[symmetric]) simp
   6.367 +  finally show ?thesis .
   6.368 +qed
   6.369 +
   6.370 +lemma integrable_on_lborel: "integrable lborel f \<Longrightarrow> f integrable_on UNIV"
   6.371 +  using has_integral_integral_lborel by auto
   6.372 +
   6.373 +lemma integral_lborel: "integrable lborel f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lborel)"
   6.374 +  using has_integral_integral_lborel by auto
   6.375 +
   6.376 +end
   6.377 +
   6.378 +subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
   6.379 +
   6.380 +text \<open>
   6.381 +
   6.382 +For the positive integral we replace continuity with Borel-measurability.
   6.383 +
   6.384 +\<close>
   6.385 +
   6.386 +lemma
   6.387 +  fixes f :: "real \<Rightarrow> real"
   6.388 +  assumes [measurable]: "f \<in> borel_measurable borel"
   6.389 +  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"
   6.390 +  shows nn_integral_FTC_Icc: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?nn)
   6.391 +    and has_bochner_integral_FTC_Icc_nonneg:
   6.392 +      "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
   6.393 +    and integral_FTC_Icc_nonneg: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
   6.394 +    and integrable_FTC_Icc_nonneg: "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is ?int)
   6.395 +proof -
   6.396 +  have *: "(\<lambda>x. f x * indicator {a..b} x) \<in> borel_measurable borel" "\<And>x. 0 \<le> f x * indicator {a..b} x"
   6.397 +    using f(2) by (auto split: split_indicator)
   6.398 +
   6.399 +  have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b\<Longrightarrow> F x \<le> F y" for x y
   6.400 +    using f by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
   6.401 +
   6.402 +  have "(f has_integral F b - F a) {a..b}"
   6.403 +    by (intro fundamental_theorem_of_calculus)
   6.404 +       (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
   6.405 +             intro: has_field_derivative_subset[OF f(1)] \<open>a \<le> b\<close>)
   6.406 +  then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
   6.407 +    unfolding indicator_def if_distrib[where f="\<lambda>x. a * x" for a]
   6.408 +    by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
   6.409 +  then have nn: "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
   6.410 +    by (rule nn_integral_has_integral_lborel[OF *])
   6.411 +  then show ?has
   6.412 +    by (rule has_bochner_integral_nn_integral[rotated 3]) (simp_all add: * F_mono \<open>a \<le> b\<close>)
   6.413 +  then show ?eq ?int
   6.414 +    unfolding has_bochner_integral_iff by auto
   6.415 +  show ?nn
   6.416 +    by (subst nn[symmetric])
   6.417 +       (auto intro!: nn_integral_cong simp add: ennreal_mult f split: split_indicator)
   6.418 +qed
   6.419 +
   6.420 +lemma
   6.421 +  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
   6.422 +  assumes "a \<le> b"
   6.423 +  assumes "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
   6.424 +  assumes cont: "continuous_on {a .. b} f"
   6.425 +  shows has_bochner_integral_FTC_Icc:
   6.426 +      "has_bochner_integral lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) (F b - F a)" (is ?has)
   6.427 +    and integral_FTC_Icc: "(\<integral>x. indicator {a .. b} x *\<^sub>R f x \<partial>lborel) = F b - F a" (is ?eq)
   6.428 +proof -
   6.429 +  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
   6.430 +  have int: "integrable lborel ?f"
   6.431 +    using borel_integrable_compact[OF _ cont] by auto
   6.432 +  have "(f has_integral F b - F a) {a..b}"
   6.433 +    using assms(1,2) by (intro fundamental_theorem_of_calculus) auto
   6.434 +  moreover
   6.435 +  have "(f has_integral integral\<^sup>L lborel ?f) {a..b}"
   6.436 +    using has_integral_integral_lborel[OF int]
   6.437 +    unfolding indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a]
   6.438 +    by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
   6.439 +  ultimately show ?eq
   6.440 +    by (auto dest: has_integral_unique)
   6.441 +  then show ?has
   6.442 +    using int by (auto simp: has_bochner_integral_iff)
   6.443 +qed
   6.444 +
   6.445 +lemma
   6.446 +  fixes f :: "real \<Rightarrow> real"
   6.447 +  assumes "a \<le> b"
   6.448 +  assumes deriv: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> DERIV F x :> f x"
   6.449 +  assumes cont: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
   6.450 +  shows has_bochner_integral_FTC_Icc_real:
   6.451 +      "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
   6.452 +    and integral_FTC_Icc_real: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
   6.453 +proof -
   6.454 +  have 1: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
   6.455 +    unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
   6.456 +    using deriv by (auto intro: DERIV_subset)
   6.457 +  have 2: "continuous_on {a .. b} f"
   6.458 +    using cont by (intro continuous_at_imp_continuous_on) auto
   6.459 +  show ?has ?eq
   6.460 +    using has_bochner_integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2] integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2]
   6.461 +    by (auto simp: mult.commute)
   6.462 +qed
   6.463 +
   6.464 +lemma nn_integral_FTC_atLeast:
   6.465 +  fixes f :: "real \<Rightarrow> real"
   6.466 +  assumes f_borel: "f \<in> borel_measurable borel"
   6.467 +  assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x"
   6.468 +  assumes nonneg: "\<And>x. a \<le> x \<Longrightarrow> 0 \<le> f x"
   6.469 +  assumes lim: "(F \<longlongrightarrow> T) at_top"
   6.470 +  shows "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a ..} x \<partial>lborel) = T - F a"
   6.471 +proof -
   6.472 +  let ?f = "\<lambda>(i::nat) (x::real). ennreal (f x) * indicator {a..a + real i} x"
   6.473 +  let ?fR = "\<lambda>x. ennreal (f x) * indicator {a ..} x"
   6.474 +
   6.475 +  have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> F x \<le> F y" for x y
   6.476 +    using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
   6.477 +  then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x
   6.478 +    by (intro tendsto_le_const[OF _ lim])
   6.479 +       (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder)
   6.480 +
   6.481 +  have "(SUP i::nat. ?f i x) = ?fR x" for x
   6.482 +  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
   6.483 +    from reals_Archimedean2[of "x - a"] guess n ..
   6.484 +    then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
   6.485 +      by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
   6.486 +    then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
   6.487 +      by (rule Lim_eventually)
   6.488 +  qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
   6.489 +  then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
   6.490 +    by simp
   6.491 +  also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
   6.492 +  proof (rule nn_integral_monotone_convergence_SUP)
   6.493 +    show "incseq ?f"
   6.494 +      using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
   6.495 +    show "\<And>i. (?f i) \<in> borel_measurable lborel"
   6.496 +      using f_borel by auto
   6.497 +  qed
   6.498 +  also have "\<dots> = (SUP i::nat. ennreal (F (a + real i) - F a))"
   6.499 +    by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
   6.500 +  also have "\<dots> = T - F a"
   6.501 +  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
   6.502 +    have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
   6.503 +      apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top])
   6.504 +      apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl])
   6.505 +      apply (rule filterlim_real_sequentially)
   6.506 +      done
   6.507 +    then show "(\<lambda>n. ennreal (F (a + real n) - F a)) \<longlonglongrightarrow> ennreal (T - F a)"
   6.508 +      by (simp add: F_mono F_le_T tendsto_diff)
   6.509 +  qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
   6.510 +  finally show ?thesis .
   6.511 +qed
   6.512 +
   6.513 +lemma integral_power:
   6.514 +  "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k"
   6.515 +proof (subst integral_FTC_Icc_real)
   6.516 +  fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
   6.517 +    by (intro derivative_eq_intros) auto
   6.518 +qed (auto simp: field_simps simp del: of_nat_Suc)
   6.519 +
   6.520 +subsection \<open>Integration by parts\<close>
   6.521 +
   6.522 +lemma integral_by_parts_integrable:
   6.523 +  fixes f g F G::"real \<Rightarrow> real"
   6.524 +  assumes "a \<le> b"
   6.525 +  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
   6.526 +  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
   6.527 +  assumes [intro]: "!!x. DERIV F x :> f x"
   6.528 +  assumes [intro]: "!!x. DERIV G x :> g x"
   6.529 +  shows  "integrable lborel (\<lambda>x.((F x) * (g x) + (f x) * (G x)) * indicator {a .. b} x)"
   6.530 +  by (auto intro!: borel_integrable_atLeastAtMost continuous_intros) (auto intro!: DERIV_isCont)
   6.531 +
   6.532 +lemma integral_by_parts:
   6.533 +  fixes f g F G::"real \<Rightarrow> real"
   6.534 +  assumes [arith]: "a \<le> b"
   6.535 +  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
   6.536 +  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
   6.537 +  assumes [intro]: "!!x. DERIV F x :> f x"
   6.538 +  assumes [intro]: "!!x. DERIV G x :> g x"
   6.539 +  shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
   6.540 +            =  F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
   6.541 +proof-
   6.542 +  have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
   6.543 +    by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros)
   6.544 +      (auto intro!: DERIV_isCont)
   6.545 +
   6.546 +  have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
   6.547 +    (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
   6.548 +    apply (subst Bochner_Integration.integral_add[symmetric])
   6.549 +    apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros)
   6.550 +    by (auto intro!: DERIV_isCont Bochner_Integration.integral_cong split: split_indicator)
   6.551 +
   6.552 +  thus ?thesis using 0 by auto
   6.553 +qed
   6.554 +
   6.555 +lemma integral_by_parts':
   6.556 +  fixes f g F G::"real \<Rightarrow> real"
   6.557 +  assumes "a \<le> b"
   6.558 +  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
   6.559 +  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
   6.560 +  assumes "!!x. DERIV F x :> f x"
   6.561 +  assumes "!!x. DERIV G x :> g x"
   6.562 +  shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
   6.563 +            =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel"
   6.564 +  using integral_by_parts[OF assms] by (simp add: ac_simps)
   6.565 +
   6.566 +lemma has_bochner_integral_even_function:
   6.567 +  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   6.568 +  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
   6.569 +  assumes even: "\<And>x. f (- x) = f x"
   6.570 +  shows "has_bochner_integral lborel f (2 *\<^sub>R x)"
   6.571 +proof -
   6.572 +  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
   6.573 +    by (auto split: split_indicator)
   6.574 +  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x"
   6.575 +    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
   6.576 +       (auto simp: indicator even f)
   6.577 +  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + x)"
   6.578 +    by (rule has_bochner_integral_add)
   6.579 +  then have "has_bochner_integral lborel f (x + x)"
   6.580 +    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
   6.581 +       (auto split: split_indicator)
   6.582 +  then show ?thesis
   6.583 +    by (simp add: scaleR_2)
   6.584 +qed
   6.585 +
   6.586 +lemma has_bochner_integral_odd_function:
   6.587 +  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   6.588 +  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
   6.589 +  assumes odd: "\<And>x. f (- x) = - f x"
   6.590 +  shows "has_bochner_integral lborel f 0"
   6.591 +proof -
   6.592 +  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
   6.593 +    by (auto split: split_indicator)
   6.594 +  have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x"
   6.595 +    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
   6.596 +       (auto simp: indicator odd f)
   6.597 +  from has_bochner_integral_minus[OF this]
   6.598 +  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)"
   6.599 +    by simp
   6.600 +  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + - x)"
   6.601 +    by (rule has_bochner_integral_add)
   6.602 +  then have "has_bochner_integral lborel f (x + - x)"
   6.603 +    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
   6.604 +       (auto split: split_indicator)
   6.605 +  then show ?thesis
   6.606 +    by simp
   6.607 +qed
   6.608 +
   6.609 +end
     7.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 15 22:41:05 2016 +0200
     7.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 16 13:56:51 2016 +0200
     7.3 @@ -6,9 +6,7 @@
     7.4  
     7.5  theory Henstock_Kurzweil_Integration
     7.6  imports
     7.7 -  Derivative
     7.8 -  Uniform_Limit
     7.9 -  "~~/src/HOL/Library/Indicator_Function"
    7.10 +  Lebesgue_Measure
    7.11  begin
    7.12  
    7.13  lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
    7.14 @@ -22,122 +20,19 @@
    7.15  lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
    7.16  lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
    7.17  
    7.18 +lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
    7.19 +  by auto
    7.20 +
    7.21  declare norm_triangle_ineq4[intro]
    7.22  
    7.23 -lemma simple_image: "{f x |x . x \<in> s} = f ` s"
    7.24 -  by blast
    7.25 -
    7.26 -lemma linear_simps:
    7.27 -  assumes "bounded_linear f"
    7.28 -  shows
    7.29 -    "f (a + b) = f a + f b"
    7.30 -    "f (a - b) = f a - f b"
    7.31 -    "f 0 = 0"
    7.32 -    "f (- a) = - f a"
    7.33 -    "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
    7.34 -proof -
    7.35 -  interpret f: bounded_linear f by fact
    7.36 -  show "f (a + b) = f a + f b" by (rule f.add)
    7.37 -  show "f (a - b) = f a - f b" by (rule f.diff)
    7.38 -  show "f 0 = 0" by (rule f.zero)
    7.39 -  show "f (- a) = - f a" by (rule f.minus)
    7.40 -  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
    7.41 -qed
    7.42 -
    7.43 -lemma bounded_linearI:
    7.44 -  assumes "\<And>x y. f (x + y) = f x + f y"
    7.45 -    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
    7.46 -    and "\<And>x. norm (f x) \<le> norm x * K"
    7.47 -  shows "bounded_linear f"
    7.48 -  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
    7.49 -
    7.50 -lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
    7.51 -  by (rule bounded_linear_inner_left)
    7.52 -
    7.53 -lemma transitive_stepwise_lt_eq:
    7.54 -  assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
    7.55 -  shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))"
    7.56 -  (is "?l = ?r")
    7.57 -proof safe
    7.58 -  assume ?r
    7.59 -  fix n m :: nat
    7.60 -  assume "m < n"
    7.61 -  then show "R m n"
    7.62 -  proof (induct n arbitrary: m)
    7.63 -    case 0
    7.64 -    then show ?case by auto
    7.65 -  next
    7.66 -    case (Suc n)
    7.67 -    show ?case
    7.68 -    proof (cases "m < n")
    7.69 -      case True
    7.70 -      show ?thesis
    7.71 -        apply (rule assms[OF Suc(1)[OF True]])
    7.72 -        using \<open>?r\<close>
    7.73 -        apply auto
    7.74 -        done
    7.75 -    next
    7.76 -      case False
    7.77 -      then have "m = n"
    7.78 -        using Suc(2) by auto
    7.79 -      then show ?thesis
    7.80 -        using \<open>?r\<close> by auto
    7.81 -    qed
    7.82 -  qed
    7.83 -qed auto
    7.84 -
    7.85 -lemma transitive_stepwise_gt:
    7.86 -  assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n)"
    7.87 -  shows "\<forall>n>m. R m n"
    7.88 -proof -
    7.89 -  have "\<forall>m. \<forall>n>m. R m n"
    7.90 -    apply (subst transitive_stepwise_lt_eq)
    7.91 -    apply (blast intro: assms)+
    7.92 -    done
    7.93 -  then show ?thesis by auto
    7.94 -qed
    7.95 -
    7.96 -lemma transitive_stepwise_le_eq:
    7.97 -  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
    7.98 -  shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))"
    7.99 -  (is "?l = ?r")
   7.100 -proof safe
   7.101 -  assume ?r
   7.102 -  fix m n :: nat
   7.103 -  assume "m \<le> n"
   7.104 -  then show "R m n"
   7.105 -  proof (induct n arbitrary: m)
   7.106 -    case 0
   7.107 -    with assms show ?case by auto
   7.108 -  next
   7.109 -    case (Suc n)
   7.110 -    show ?case
   7.111 -    proof (cases "m \<le> n")
   7.112 -      case True
   7.113 -      with Suc.hyps \<open>\<forall>n. R n (Suc n)\<close> assms show ?thesis
   7.114 -        by blast
   7.115 -    next
   7.116 -      case False
   7.117 -      then have "m = Suc n"
   7.118 -        using Suc(2) by auto
   7.119 -      then show ?thesis
   7.120 -        using assms(1) by auto
   7.121 -    qed
   7.122 -  qed
   7.123 -qed auto
   7.124 -
   7.125  lemma transitive_stepwise_le:
   7.126 -  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
   7.127 -    and "\<And>n. R n (Suc n)"
   7.128 +  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
   7.129    shows "\<forall>n\<ge>m. R m n"
   7.130 -proof -
   7.131 -  have "\<forall>m. \<forall>n\<ge>m. R m n"
   7.132 -    apply (subst transitive_stepwise_le_eq)
   7.133 -    apply (blast intro: assms)+
   7.134 -    done
   7.135 -  then show ?thesis by auto
   7.136 -qed
   7.137 -
   7.138 +proof (intro allI impI)
   7.139 +  show "m \<le> n \<Longrightarrow> R m n" for n
   7.140 +    by (induction rule: dec_induct)
   7.141 +       (use assms in blast)+
   7.142 +qed
   7.143  
   7.144  subsection \<open>Some useful lemmas about intervals.\<close>
   7.145  
   7.146 @@ -208,13 +103,28 @@
   7.147      "finite f \<Longrightarrow> open s \<Longrightarrow> \<forall>t\<in>f. \<exists>a b. t = cbox a b \<Longrightarrow> \<forall>t\<in>f. s \<inter> (interior t) = {} \<Longrightarrow> s \<inter> interior (\<Union>f) = {}"
   7.148    using interior_Union_subset_cbox[of f "UNIV - s"] by auto
   7.149  
   7.150 +lemma interval_split:
   7.151 +  fixes a :: "'a::euclidean_space"
   7.152 +  assumes "k \<in> Basis"
   7.153 +  shows
   7.154 +    "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
   7.155 +    "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
   7.156 +  apply (rule_tac[!] set_eqI)
   7.157 +  unfolding Int_iff mem_box mem_Collect_eq
   7.158 +  using assms
   7.159 +  apply auto
   7.160 +  done
   7.161 +
   7.162 +lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
   7.163 +  by (simp add: box_ne_empty)
   7.164 +
   7.165  subsection \<open>Bounds on intervals where they exist.\<close>
   7.166  
   7.167  definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   7.168    where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
   7.169  
   7.170  definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   7.171 -   where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
   7.172 +  where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
   7.173  
   7.174  lemma interval_upperbound[simp]:
   7.175    "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
   7.176 @@ -242,7 +152,6 @@
   7.177      and "interval_lowerbound (cbox a b) = a"
   7.178    using assms unfolding box_ne_empty by auto
   7.179  
   7.180 -
   7.181  lemma interval_upperbound_Times:
   7.182    assumes "A \<noteq> {}" and "B \<noteq> {}"
   7.183    shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
   7.184 @@ -273,219 +182,83 @@
   7.185  
   7.186  subsection \<open>Content (length, area, volume...) of an interval.\<close>
   7.187  
   7.188 -definition "content (s::('a::euclidean_space) set) =
   7.189 -  (if s = {} then 0 else (\<Prod>i\<in>Basis. (interval_upperbound s)\<bullet>i - (interval_lowerbound s)\<bullet>i))"
   7.190 -
   7.191 -lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
   7.192 -  unfolding box_eq_empty unfolding not_ex not_less by auto
   7.193 -
   7.194 -lemma content_cbox:
   7.195 -  fixes a :: "'a::euclidean_space"
   7.196 -  assumes "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
   7.197 -  shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
   7.198 -  using interval_not_empty[OF assms]
   7.199 -  unfolding content_def
   7.200 -  by auto
   7.201 -
   7.202 -lemma content_cbox':
   7.203 -  fixes a :: "'a::euclidean_space"
   7.204 -  assumes "cbox a b \<noteq> {}"
   7.205 -  shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
   7.206 -    using assms box_ne_empty(1) content_cbox by blast
   7.207 +abbreviation content :: "'a::euclidean_space set \<Rightarrow> real"
   7.208 +  where "content s \<equiv> measure lborel s"
   7.209 +
   7.210 +lemma content_cbox_cases:
   7.211 +  "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
   7.212 +  by (simp add: measure_lborel_cbox_eq inner_diff)
   7.213 +
   7.214 +lemma content_cbox: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
   7.215 +  unfolding content_cbox_cases by simp
   7.216 +
   7.217 +lemma content_cbox': "cbox a b \<noteq> {} \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
   7.218 +  by (simp add: box_ne_empty inner_diff)
   7.219  
   7.220  lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
   7.221 -  by (auto simp: interval_upperbound_def interval_lowerbound_def content_def)
   7.222 +  by simp
   7.223  
   7.224  lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
   7.225    by (auto simp: content_real)
   7.226  
   7.227 -lemma content_singleton[simp]: "content {a} = 0"
   7.228 -proof -
   7.229 -  have "content (cbox a a) = 0"
   7.230 -    by (subst content_cbox) (auto simp: ex_in_conv)
   7.231 -  then show ?thesis by (simp add: cbox_sing)
   7.232 -qed
   7.233 -
   7.234 -lemma content_unit[iff]: "content(cbox 0 (One::'a::euclidean_space)) = 1"
   7.235 - proof -
   7.236 -   have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i"
   7.237 -    by auto
   7.238 -  have "0 \<in> cbox 0 (One::'a)"
   7.239 -    unfolding mem_box by auto
   7.240 -  then show ?thesis
   7.241 -     unfolding content_def interval_bounds[OF *] using setprod.neutral_const by auto
   7.242 - qed
   7.243 -
   7.244 -lemma content_pos_le[intro]:
   7.245 -  fixes a::"'a::euclidean_space"
   7.246 -  shows "0 \<le> content (cbox a b)"
   7.247 -proof (cases "cbox a b = {}")
   7.248 -  case False
   7.249 -  then have *: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
   7.250 -    unfolding box_ne_empty .
   7.251 -  have "0 \<le> (\<Prod>i\<in>Basis. interval_upperbound (cbox a b) \<bullet> i - interval_lowerbound (cbox a b) \<bullet> i)"
   7.252 -    apply (rule setprod_nonneg)
   7.253 -    unfolding interval_bounds[OF *]
   7.254 -    using *
   7.255 -    apply auto
   7.256 -    done
   7.257 -  also have "\<dots> = content (cbox a b)" using False by (simp add: content_def)
   7.258 -  finally show ?thesis .
   7.259 -qed (simp add: content_def)
   7.260 -
   7.261 -corollary content_nonneg [simp]:
   7.262 -  fixes a::"'a::euclidean_space"
   7.263 -  shows "~ content (cbox a b) < 0"
   7.264 -using not_le by blast
   7.265 -
   7.266 -lemma content_pos_lt:
   7.267 -  fixes a :: "'a::euclidean_space"
   7.268 -  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
   7.269 -  shows "0 < content (cbox a b)"
   7.270 -  using assms
   7.271 -  by (auto simp: content_def box_eq_empty intro!: setprod_pos)
   7.272 -
   7.273 -lemma content_eq_0:
   7.274 -  "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
   7.275 -  by (auto simp: content_def box_eq_empty intro!: setprod_pos bexI)
   7.276 -
   7.277 -lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
   7.278 -  by auto
   7.279 -
   7.280 -lemma content_cbox_cases:
   7.281 -  "content (cbox a (b::'a::euclidean_space)) =
   7.282 -    (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
   7.283 -  by (auto simp: not_le content_eq_0 intro: less_imp_le content_cbox)
   7.284 +lemma content_singleton: "content {a} = 0"
   7.285 +  by simp
   7.286 +
   7.287 +lemma content_unit[iff]: "content (cbox 0 (One::'a::euclidean_space)) = 1"
   7.288 +  by simp
   7.289 +
   7.290 +lemma content_pos_le[intro]: "0 \<le> content (cbox a b)"
   7.291 +  by simp
   7.292 +
   7.293 +corollary content_nonneg [simp]: "~ content (cbox a b) < 0"
   7.294 +  using not_le by blast
   7.295 +
   7.296 +lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
   7.297 +  by (auto simp: less_imp_le inner_diff box_eq_empty intro!: setprod_pos)
   7.298 +
   7.299 +lemma content_eq_0: "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
   7.300 +  by (auto simp: content_cbox_cases not_le intro: less_imp_le antisym eq_refl)
   7.301  
   7.302  lemma content_eq_0_interior: "content (cbox a b) = 0 \<longleftrightarrow> interior(cbox a b) = {}"
   7.303 -  unfolding content_eq_0 interior_cbox box_eq_empty
   7.304 -  by auto
   7.305 -
   7.306 -lemma content_pos_lt_eq:
   7.307 -  "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
   7.308 -proof (rule iffI)
   7.309 -  assume "0 < content (cbox a b)"
   7.310 -  then have "content (cbox a b) \<noteq> 0" by auto
   7.311 -  then show "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
   7.312 -    unfolding content_eq_0 not_ex not_le by fastforce
   7.313 -next
   7.314 -  assume "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
   7.315 -  then show "0 < content (cbox a b)"
   7.316 -    by (metis content_pos_lt)
   7.317 -qed
   7.318 +  unfolding content_eq_0 interior_cbox box_eq_empty by auto
   7.319 +
   7.320 +lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
   7.321 +  by (auto simp add: content_cbox_cases less_le setprod_nonneg)
   7.322  
   7.323  lemma content_empty [simp]: "content {} = 0"
   7.324 -  unfolding content_def by auto
   7.325 +  by simp
   7.326  
   7.327  lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b - a else 0)"
   7.328    by (simp add: content_real)
   7.329  
   7.330 -lemma content_subset:
   7.331 -  assumes "cbox a b \<subseteq> cbox c d"
   7.332 -  shows "content (cbox a b) \<le> content (cbox c d)"
   7.333 -proof (cases "cbox a b = {}")
   7.334 -  case True
   7.335 -  then show ?thesis
   7.336 -    using content_pos_le[of c d] by auto
   7.337 -next
   7.338 -  case False
   7.339 -  then have ab_ne: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
   7.340 -    unfolding box_ne_empty by auto
   7.341 -  then have ab_ab: "a\<in>cbox a b" "b\<in>cbox a b"
   7.342 -    unfolding mem_box by auto
   7.343 -  have "cbox c d \<noteq> {}" using assms False by auto
   7.344 -  then have cd_ne: "\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i"
   7.345 -    using assms unfolding box_ne_empty by auto
   7.346 -  have "\<And>i. i \<in> Basis \<Longrightarrow> 0 \<le> b \<bullet> i - a \<bullet> i"
   7.347 -    using ab_ne by auto
   7.348 -  moreover
   7.349 -  have "\<And>i. i \<in> Basis \<Longrightarrow> b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
   7.350 -    using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2)]
   7.351 -          assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(1)]
   7.352 -      by (metis diff_mono)
   7.353 -  ultimately show ?thesis
   7.354 -    unfolding content_def interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
   7.355 -    by (simp add: setprod_mono if_not_P[OF False] if_not_P[OF \<open>cbox c d \<noteq> {}\<close>])
   7.356 -qed
   7.357 +lemma content_subset: "cbox a b \<subseteq> cbox c d \<Longrightarrow> content (cbox a b) \<le> content (cbox c d)"
   7.358 +  unfolding measure_def
   7.359 +  by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq)
   7.360  
   7.361  lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
   7.362    unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
   7.363  
   7.364 -lemma content_times[simp]: "content (A \<times> B) = content A * content B"
   7.365 -proof (cases "A \<times> B = {}")
   7.366 -  let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound"
   7.367 -  let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound"
   7.368 -  assume nonempty: "A \<times> B \<noteq> {}"
   7.369 -  hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)"
   7.370 -      unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times)
   7.371 -  also have "... = content A * content B" unfolding content_def using nonempty
   7.372 -    apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp)
   7.373 -    apply (subst (1 2) setprod.reindex, auto intro: inj_onI)
   7.374 -    done
   7.375 -  finally show ?thesis .
   7.376 -qed (auto simp: content_def)
   7.377 -
   7.378  lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
   7.379 -  by (simp add: cbox_Pair_eq)
   7.380 +  unfolding measure_lborel_cbox_eq Basis_prod_def
   7.381 +  apply (subst setprod.union_disjoint)
   7.382 +  apply (auto simp: bex_Un ball_Un)
   7.383 +  apply (subst (1 2) setprod.reindex_nontrivial)
   7.384 +  apply auto
   7.385 +  done
   7.386  
   7.387  lemma content_cbox_pair_eq0_D:
   7.388     "content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0"
   7.389    by (simp add: content_Pair)
   7.390  
   7.391 -lemma content_eq_0_gen:
   7.392 -  fixes s :: "'a::euclidean_space set"
   7.393 -  assumes "bounded s"
   7.394 -  shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)"  (is "_ = ?rhs")
   7.395 -proof safe
   7.396 -  assume "content s = 0" then show ?rhs
   7.397 -    apply (clarsimp simp: ex_in_conv content_def split: if_split_asm)
   7.398 -    apply (rule_tac x=a in bexI)
   7.399 -    apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI)
   7.400 -    apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def)
   7.401 -    apply (drule cSUP_eq_cINF_D)
   7.402 -    apply (auto simp: bounded_inner_imp_bdd_above [OF assms]  bounded_inner_imp_bdd_below [OF assms])
   7.403 -    done
   7.404 -next
   7.405 -  fix i a
   7.406 -  assume "i \<in> Basis" "\<forall>x\<in>s. x \<bullet> i = a"
   7.407 -  then show "content s = 0"
   7.408 -    apply (clarsimp simp: content_def)
   7.409 -    apply (rule_tac x=i in bexI)
   7.410 -    apply (auto simp: interval_upperbound_def interval_lowerbound_def)
   7.411 -    done
   7.412 -qed
   7.413 -
   7.414 -lemma content_0_subset_gen:
   7.415 -  fixes a :: "'a::euclidean_space"
   7.416 -  assumes "content t = 0" "s \<subseteq> t" "bounded t" shows "content s = 0"
   7.417 -proof -
   7.418 -  have "bounded s"
   7.419 -    using assms by (metis bounded_subset)
   7.420 -  then show ?thesis
   7.421 -    using assms
   7.422 -    by (auto simp: content_eq_0_gen)
   7.423 -qed
   7.424 -
   7.425 -lemma content_0_subset: "\<lbrakk>content(cbox a b) = 0; s \<subseteq> cbox a b\<rbrakk> \<Longrightarrow> content s = 0"
   7.426 -  by (simp add: content_0_subset_gen bounded_cbox)
   7.427 -
   7.428 -
   7.429 -lemma interval_split:
   7.430 -  fixes a :: "'a::euclidean_space"
   7.431 -  assumes "k \<in> Basis"
   7.432 -  shows
   7.433 -    "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
   7.434 -    "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
   7.435 -  apply (rule_tac[!] set_eqI)
   7.436 -  unfolding Int_iff mem_box mem_Collect_eq
   7.437 -  using assms
   7.438 -  apply auto
   7.439 -  done
   7.440 +lemma content_0_subset: "content(cbox a b) = 0 \<Longrightarrow> s \<subseteq> cbox a b \<Longrightarrow> content s = 0"
   7.441 +  using emeasure_mono[of s "cbox a b" lborel]
   7.442 +  by (auto simp: measure_def enn2real_eq_0_iff emeasure_lborel_cbox_eq)
   7.443  
   7.444  lemma content_split:
   7.445    fixes a :: "'a::euclidean_space"
   7.446    assumes "k \<in> Basis"
   7.447    shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
   7.448 +  -- \<open>Prove using measure theory\<close>
   7.449  proof cases
   7.450    note simps = interval_split[OF assms] content_cbox_cases
   7.451    have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
   7.452 @@ -2040,11 +1813,6 @@
   7.453    "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)"
   7.454    unfolding setsum.operative_tagged_division[OF operative_content, symmetric] by blast
   7.455  
   7.456 -lemma
   7.457 -  shows real_inner_1_left: "inner 1 x = x"
   7.458 -  and real_inner_1_right: "inner x 1 = x"
   7.459 -  by simp_all
   7.460 -
   7.461  lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b"
   7.462    by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)
   7.463  
   7.464 @@ -3988,8 +3756,7 @@
   7.465    have "norm (setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> (\<Sum>i\<in>p. norm (content i *\<^sub>R c))"
   7.466      using norm_setsum by blast
   7.467    also have "...  \<le> e * (\<Sum>i\<in>p. \<bar>content i\<bar>)"
   7.468 -    apply (simp add: setsum_right_distrib[symmetric] mult.commute)
   7.469 -    using assms(2) mult_right_mono by blast
   7.470 +    by (simp add: setsum_right_distrib[symmetric] mult.commute assms(2) mult_right_mono setsum_nonneg)
   7.471    also have "... \<le> e * content (cbox a b)"
   7.472      apply (rule mult_left_mono [OF _ e])
   7.473      apply (simp add: sumeq)
   7.474 @@ -4458,65 +4225,70 @@
   7.475    assumes "0 < e"
   7.476      and k: "k \<in> Basis"
   7.477    obtains d where "0 < d" and "content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) < e"
   7.478 -proof (cases "content (cbox a b) = 0")
   7.479 -  case True
   7.480 -  then have ce: "content (cbox a b) < e"
   7.481 -    by (metis \<open>0 < e\<close>)
   7.482 +proof cases
   7.483 +  assume *: "a \<bullet> k \<le> c \<and> c \<le> b \<bullet> k \<and> (\<forall>j\<in>Basis. a \<bullet> j \<le> b \<bullet> j)"
   7.484 +  define a' where "a' d = (\<Sum>j\<in>Basis. (if j = k then max (a\<bullet>j) (c - d) else a\<bullet>j) *\<^sub>R j)" for d
   7.485 +  define b' where "b' d = (\<Sum>j\<in>Basis. (if j = k then min (b\<bullet>j) (c + d) else b\<bullet>j) *\<^sub>R j)" for d
   7.486 +
   7.487 +  have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> (\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j)) (at_right 0)"
   7.488 +    by (auto simp: b'_def a'_def intro!: tendsto_min tendsto_max tendsto_eq_intros)
   7.489 +  also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0"
   7.490 +    using k *
   7.491 +    by (intro setprod_zero bexI[OF _ k])
   7.492 +       (auto simp: b'_def a'_def inner_diff inner_setsum_left inner_not_same_Basis intro!: setsum.cong)
   7.493 +  also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) =
   7.494 +    ((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)"
   7.495 +  proof (intro tendsto_cong eventually_at_rightI)
   7.496 +    fix d :: real assume d: "d \<in> {0<..<1}"
   7.497 +    have "cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d} = cbox (a' d) (b' d)" for d
   7.498 +      using * d k by (auto simp add: cbox_def set_eq_iff Int_def ball_conj_distrib abs_diff_le_iff a'_def b'_def)
   7.499 +    moreover have "j \<in> Basis \<Longrightarrow> a' d \<bullet> j \<le> b' d \<bullet> j" for j
   7.500 +      using * d k by (auto simp: a'_def b'_def)
   7.501 +    ultimately show "(\<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) = content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})"
   7.502 +      by simp
   7.503 +  qed simp
   7.504 +  finally have "((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)" .
   7.505 +  from order_tendstoD(2)[OF this \<open>0<e\<close>]
   7.506 +  obtain d' where "0 < d'" and d': "\<And>y. y > 0 \<Longrightarrow> y < d' \<Longrightarrow> content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> y}) < e"
   7.507 +    by (subst (asm) eventually_at_right[of _ 1]) auto
   7.508    show ?thesis
   7.509 -    apply (rule that[of 1])
   7.510 -    apply simp
   7.511 -    unfolding interval_doublesplit[OF k]
   7.512 -    apply (rule le_less_trans[OF content_subset ce])
   7.513 -    apply (auto simp: interval_doublesplit[symmetric] k)
   7.514 -    done
   7.515 +    by (rule that[of "d'/2"], insert \<open>0<d'\<close> d'[of "d'/2"], auto)
   7.516  next
   7.517 -  case False
   7.518 -  define d where "d = e / 3 / setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
   7.519 -  note False[unfolded content_eq_0 not_ex not_le, rule_format]
   7.520 -  then have "\<And>x. x \<in> Basis \<Longrightarrow> b\<bullet>x > a\<bullet>x"
   7.521 -    by (auto simp add:not_le)
   7.522 -  then have prod0: "0 < setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
   7.523 -    by (force simp add: setprod_pos field_simps)
   7.524 -  then have "d > 0"
   7.525 -    using assms
   7.526 -    by (auto simp add: d_def field_simps)
   7.527 -  then show ?thesis
   7.528 -  proof (rule that[of d])
   7.529 -    have *: "Basis = insert k (Basis - {k})"
   7.530 -      using k by auto
   7.531 -    have less_e: "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) * (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i) < e"
   7.532 -    proof -
   7.533 -      have "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) \<le> 2 * d"
   7.534 +  assume *: "\<not> (a \<bullet> k \<le> c \<and> c \<le> b \<bullet> k \<and> (\<forall>j\<in>Basis. a \<bullet> j \<le> b \<bullet> j))"
   7.535 +  then have "(\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j) \<or> (c < a \<bullet> k \<or> b \<bullet> k < c)"
   7.536 +    by (auto simp: not_le)
   7.537 +  show thesis
   7.538 +  proof cases
   7.539 +    assume "\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j"
   7.540 +    then have [simp]: "cbox a b = {}"
   7.541 +      using box_ne_empty(1)[of a b] by auto
   7.542 +    show ?thesis
   7.543 +      by (rule that[of 1]) (simp_all add: \<open>0<e\<close>)
   7.544 +  next
   7.545 +    assume "\<not> (\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j)"
   7.546 +    with * have "c < a \<bullet> k \<or> b \<bullet> k < c"
   7.547 +      by auto
   7.548 +    then show thesis
   7.549 +    proof
   7.550 +      assume c: "c < a \<bullet> k"
   7.551 +      moreover have "x \<in> cbox a b \<Longrightarrow> c \<le> x \<bullet> k" for x
   7.552 +        using k c by (auto simp: cbox_def)
   7.553 +      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (a \<bullet> k - c) / 2} = {}"
   7.554 +        using k by (auto simp: cbox_def)
   7.555 +      with \<open>0<e\<close> c that[of "(a \<bullet> k - c) / 2"] show ?thesis
   7.556          by auto
   7.557 -      also have "\<dots> < e / (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i)"
   7.558 -        unfolding d_def
   7.559 -        using assms prod0
   7.560 -        by (auto simp add: field_simps)
   7.561 -      finally show "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) * (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i) < e"
   7.562 -        unfolding pos_less_divide_eq[OF prod0] .
   7.563 -    qed
   7.564 -    show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
   7.565 -    proof (cases "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = {}")
   7.566 -      case True
   7.567 -      then show ?thesis
   7.568 -        using assms by simp
   7.569      next
   7.570 -      case False
   7.571 -      then have
   7.572 -          "(\<Prod>i\<in>Basis - {k}. interval_upperbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i -
   7.573 -                interval_lowerbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i)
   7.574 -           = (\<Prod>i\<in>Basis - {k}. b\<bullet>i - a\<bullet>i)"
   7.575 -        by (simp add: box_eq_empty interval_doublesplit[OF k])
   7.576 -      then show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
   7.577 -        unfolding content_def
   7.578 -        using assms False
   7.579 -        apply (subst *)
   7.580 -        apply (subst setprod.insert)
   7.581 -        apply (simp_all add: interval_doublesplit[OF k] box_eq_empty not_less less_e)
   7.582 -        done
   7.583 -    qed
   7.584 -  qed
   7.585 -qed
   7.586 +      assume c: "b \<bullet> k < c"
   7.587 +      moreover have "x \<in> cbox a b \<Longrightarrow> x \<bullet> k \<le> c" for x
   7.588 +        using k c by (auto simp: cbox_def)
   7.589 +      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (c - b \<bullet> k) / 2} = {}"
   7.590 +        using k by (auto simp: cbox_def)
   7.591 +      with \<open>0<e\<close> c that[of "(c - b \<bullet> k) / 2"] show ?thesis
   7.592 +        by auto
   7.593 +    qed
   7.594 +  qed
   7.595 +qed
   7.596 +
   7.597  
   7.598  lemma negligible_standard_hyperplane[intro]:
   7.599    fixes k :: "'a::euclidean_space"
   7.600 @@ -5695,6 +5467,7 @@
   7.601      by auto
   7.602    from fundamental_theorem_of_calculus[rule_format, OF \<open>a \<le> b\<close> deriv]
   7.603    have "(i has_integral ?sum b - ?sum a) {a .. b}"
   7.604 +    using atLeastatMost_empty'[simp del]
   7.605      by (simp add: i_def g_def Dg_def)
   7.606    also
   7.607    have one: "(- 1) ^ p' * (- 1) ^ p' = (1::real)"
   7.608 @@ -6036,7 +5809,7 @@
   7.609          done
   7.610        show ?thesis
   7.611          using False
   7.612 -        apply (simp add: abs_eq_content del: content_real_if)
   7.613 +        apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
   7.614          apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
   7.615          using yx False d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
   7.616          done
   7.617 @@ -6054,7 +5827,7 @@
   7.618          done
   7.619        have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
   7.620          using True
   7.621 -        apply (simp add: abs_eq_content del: content_real_if)
   7.622 +        apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
   7.623          apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
   7.624          using yx True d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
   7.625          done
   7.626 @@ -6274,6 +6047,62 @@
   7.627  
   7.628  subsection \<open>Special case of a basic affine transformation.\<close>
   7.629  
   7.630 +lemma AE_lborel_inner_neq:
   7.631 +  assumes k: "k \<in> Basis"
   7.632 +  shows "AE x in lborel. x \<bullet> k \<noteq> c"
   7.633 +proof -
   7.634 +  interpret finite_product_sigma_finite "\<lambda>_. lborel" Basis
   7.635 +    proof qed simp
   7.636 +
   7.637 +  have "emeasure lborel {x\<in>space lborel. x \<bullet> k = c} = emeasure (\<Pi>\<^sub>M j::'a\<in>Basis. lborel) (\<Pi>\<^sub>E j\<in>Basis. if j = k then {c} else UNIV)"
   7.638 +    using k
   7.639 +    by (auto simp add: lborel_eq[where 'a='a] emeasure_distr intro!: arg_cong2[where f=emeasure])
   7.640 +       (auto simp: space_PiM PiE_iff extensional_def split: if_split_asm)
   7.641 +  also have "\<dots> = (\<Prod>j\<in>Basis. emeasure lborel (if j = k then {c} else UNIV))"
   7.642 +    by (intro measure_times) auto
   7.643 +  also have "\<dots> = 0"
   7.644 +    by (intro setprod_zero bexI[OF _ k]) auto
   7.645 +  finally show ?thesis
   7.646 +    by (subst AE_iff_measurable[OF _ refl]) auto
   7.647 +qed
   7.648 +
   7.649 +lemma content_image_stretch_interval:
   7.650 +  fixes m :: "'a::euclidean_space \<Rightarrow> real"
   7.651 +  defines "s f x \<equiv> (\<Sum>k::'a\<in>Basis. (f k * (x\<bullet>k)) *\<^sub>R k)"
   7.652 +  shows "content (s m ` cbox a b) = \<bar>\<Prod>k\<in>Basis. m k\<bar> * content (cbox a b)"
   7.653 +proof cases
   7.654 +  have s[measurable]: "s f \<in> borel \<rightarrow>\<^sub>M borel" for f
   7.655 +    by (auto simp: s_def[abs_def])
   7.656 +  assume m: "\<forall>k\<in>Basis. m k \<noteq> 0"
   7.657 +  then have s_comp_s: "s (\<lambda>k. 1 / m k) \<circ> s m = id" "s m \<circ> s (\<lambda>k. 1 / m k) = id"
   7.658 +    by (auto simp: s_def[abs_def] fun_eq_iff euclidean_representation)
   7.659 +  then have "inv (s (\<lambda>k. 1 / m k)) = s m" "bij (s (\<lambda>k. 1 / m k))"
   7.660 +    by (auto intro: inv_unique_comp o_bij)
   7.661 +  then have eq: "s m ` cbox a b = s (\<lambda>k. 1 / m k) -` cbox a b"
   7.662 +    using bij_vimage_eq_inv_image[OF \<open>bij (s (\<lambda>k. 1 / m k))\<close>, of "cbox a b"] by auto
   7.663 +  show ?thesis
   7.664 +    using m unfolding eq measure_def
   7.665 +    by (subst lborel_affine_euclidean[where c=m and t=0])
   7.666 +       (simp_all add: emeasure_density measurable_sets_borel[OF s] abs_setprod nn_integral_cmult
   7.667 +                      s_def[symmetric] emeasure_distr vimage_comp s_comp_s enn2real_mult setprod_nonneg)
   7.668 +next
   7.669 +  assume "\<not> (\<forall>k\<in>Basis. m k \<noteq> 0)"
   7.670 +  then obtain k where k: "k \<in> Basis" "m k = 0" by auto
   7.671 +  then have [simp]: "(\<Prod>k\<in>Basis. m k) = 0"
   7.672 +    by (intro setprod_zero) auto
   7.673 +  have "emeasure lborel {x\<in>space lborel. x \<in> s m ` cbox a b} = 0"
   7.674 +  proof (rule emeasure_eq_0_AE)
   7.675 +    show "AE x in lborel. x \<notin> s m ` cbox a b"
   7.676 +      using AE_lborel_inner_neq[OF \<open>k\<in>Basis\<close>]
   7.677 +    proof eventually_elim
   7.678 +      show "x \<bullet> k \<noteq> 0 \<Longrightarrow> x \<notin> s m ` cbox a b " for x
   7.679 +        using k by (auto simp: s_def[abs_def] cbox_def)
   7.680 +    qed
   7.681 +  qed
   7.682 +  then show ?thesis
   7.683 +    by (simp add: measure_def)
   7.684 +qed
   7.685 +
   7.686  lemma interval_image_affinity_interval:
   7.687    "\<exists>u v. (\<lambda>x. m *\<^sub>R (x::'a::euclidean_space) + c) ` cbox a b = cbox u v"
   7.688    unfolding image_affinity_cbox
   7.689 @@ -6344,43 +6173,6 @@
   7.690  
   7.691  subsection \<open>Special case of stretching coordinate axes separately.\<close>
   7.692  
   7.693 -lemma content_image_stretch_interval:
   7.694 -  "content ((\<lambda>x::'a::euclidean_space. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)::'a) ` cbox a b) =
   7.695 -    \<bar>setprod m Basis\<bar> * content (cbox a b)"
   7.696 -proof (cases "cbox a b = {}")
   7.697 -  case True
   7.698 -  then show ?thesis
   7.699 -    unfolding content_def image_is_empty image_stretch_interval if_P[OF True] by auto
   7.700 -next
   7.701 -  case False
   7.702 -  then have "(\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b \<noteq> {}"
   7.703 -    by auto
   7.704 -  then show ?thesis
   7.705 -    using False
   7.706 -    unfolding content_def image_stretch_interval
   7.707 -    apply -
   7.708 -    unfolding interval_bounds' if_not_P
   7.709 -    unfolding abs_setprod setprod.distrib[symmetric]
   7.710 -    apply (rule setprod.cong)
   7.711 -    apply (rule refl)
   7.712 -    unfolding lessThan_iff
   7.713 -    apply (simp only: inner_setsum_left_Basis)
   7.714 -  proof -
   7.715 -    fix i :: 'a
   7.716 -    assume i: "i \<in> Basis"
   7.717 -    have "(m i < 0 \<or> m i > 0) \<or> m i = 0"
   7.718 -      by auto
   7.719 -    then show "max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) - min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) =
   7.720 -      \<bar>m i\<bar> * (b \<bullet> i - a \<bullet> i)"
   7.721 -      apply -
   7.722 -      apply (erule disjE)+
   7.723 -      unfolding min_def max_def
   7.724 -      using False[unfolded box_ne_empty,rule_format,of i] i
   7.725 -      apply (auto simp add:field_simps not_le mult_le_cancel_left_neg mult_le_cancel_left_pos)
   7.726 -      done
   7.727 -  qed
   7.728 -qed
   7.729 -
   7.730  lemma has_integral_stretch:
   7.731    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   7.732    assumes "(f has_integral i) (cbox a b)"
   7.733 @@ -9324,7 +9116,7 @@
   7.734      proof (rule, goal_cases)
   7.735        case prems: (1 x)
   7.736        have "e / (4 * content (cbox a b)) > 0"
   7.737 -        using \<open>e>0\<close> False content_pos_le[of a b] by auto
   7.738 +        using \<open>e>0\<close> False content_pos_le[of a b] by (simp add: less_le)
   7.739        from assms(3)[rule_format, OF prems, THEN LIMSEQ_D, OF this]
   7.740        guess n .. note n=this
   7.741        then show ?case
   7.742 @@ -10314,7 +10106,7 @@
   7.743              done
   7.744            also have "\<dots> = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
   7.745              apply (rule setsum.mono_neutral_left)
   7.746 -            apply (subst simple_image)
   7.747 +            apply (subst Setcompr_eq_image)
   7.748              apply (rule finite_imageI)+
   7.749              apply fact
   7.750              unfolding d'_def uv
   7.751 @@ -10330,7 +10122,7 @@
   7.752                using l by auto
   7.753            qed
   7.754            also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
   7.755 -            unfolding simple_image
   7.756 +            unfolding Setcompr_eq_image
   7.757              apply (rule setsum.reindex_nontrivial [unfolded o_def])
   7.758              apply (rule finite_imageI)
   7.759              apply (rule p')
   7.760 @@ -10518,7 +10310,7 @@
   7.761              apply auto
   7.762              done
   7.763            also have "\<dots> = setsum content {k \<inter> cbox u v| k. k \<in> d}"
   7.764 -            unfolding simple_image
   7.765 +            unfolding Setcompr_eq_image
   7.766              apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
   7.767              apply (rule d')
   7.768            proof goal_cases
   7.769 @@ -10539,7 +10331,7 @@
   7.770            qed
   7.771            also have "\<dots> = setsum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
   7.772              apply (rule setsum.mono_neutral_right)
   7.773 -            unfolding simple_image
   7.774 +            unfolding Setcompr_eq_image
   7.775              apply (rule finite_imageI)
   7.776              apply (rule d')
   7.777              apply blast
   7.778 @@ -11394,7 +11186,7 @@
   7.779        also have "\<dots> < e' * norm (x - x0)"
   7.780          using \<open>e' > 0\<close> content_pos_le[of a b]
   7.781          by (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
   7.782 -          (auto simp: divide_simps e_def)
   7.783 +           (auto simp: divide_simps e_def simp del: measure_nonneg)
   7.784        finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
   7.785        then show ?case
   7.786          by (auto simp: divide_simps)
   7.787 @@ -11509,7 +11301,7 @@
   7.788        with \<open>e > 0\<close> have "e' > 0" by simp
   7.789        then have "\<forall>\<^sub>F n in F. \<forall>x\<in>cbox a b. norm (f n x - g x) < e' / content (cbox a b)"
   7.790          using u content_nonzero content_pos_le[of a b]
   7.791 -        by (auto simp: uniform_limit_iff dist_norm)
   7.792 +        by (auto simp: uniform_limit_iff dist_norm simp del: measure_nonneg)
   7.793        then show "\<forall>\<^sub>F n in F. dist (I n) J < e"
   7.794        proof eventually_elim
   7.795          case (elim n)
   7.796 @@ -11568,7 +11360,7 @@
   7.797        fix k :: nat
   7.798        show "norm (integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
   7.799          apply (rule integral_norm_bound_integral)
   7.800 -        unfolding simple_image
   7.801 +        unfolding Setcompr_eq_image
   7.802          apply (rule absolutely_integrable_onD)
   7.803          apply (rule absolutely_integrable_inf_real)
   7.804          prefer 5
   7.805 @@ -11585,7 +11377,7 @@
   7.806      qed
   7.807      fix k :: nat
   7.808      show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
   7.809 -      unfolding simple_image
   7.810 +      unfolding Setcompr_eq_image
   7.811        apply (rule absolutely_integrable_onD)
   7.812        apply (rule absolutely_integrable_inf_real)
   7.813        prefer 3
   7.814 @@ -11638,7 +11430,7 @@
   7.815      proof safe
   7.816        fix k :: nat
   7.817        show "norm (integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
   7.818 -        apply (rule integral_norm_bound_integral) unfolding simple_image
   7.819 +        apply (rule integral_norm_bound_integral) unfolding Setcompr_eq_image
   7.820          apply (rule absolutely_integrable_onD)
   7.821          apply(rule absolutely_integrable_sup_real)
   7.822          prefer 5 unfolding real_norm_def
   7.823 @@ -11656,7 +11448,7 @@
   7.824      qed
   7.825      fix k :: nat
   7.826      show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
   7.827 -      unfolding simple_image
   7.828 +      unfolding Setcompr_eq_image
   7.829        apply (rule absolutely_integrable_onD)
   7.830        apply (rule absolutely_integrable_sup_real)
   7.831        prefer 3
   7.832 @@ -12541,11 +12333,11 @@
   7.833    define f :: "nat \<Rightarrow> real \<Rightarrow> real" where "f = (\<lambda>n x. if x \<in> {a..n} then x powr e else 0)"
   7.834    define F where "F = (\<lambda>x. x powr (e + 1) / (e + 1))"
   7.835  
   7.836 -  have has_integral_f: "(f n has_integral (F n - F a)) {a..}" 
   7.837 +  have has_integral_f: "(f n has_integral (F n - F a)) {a..}"
   7.838      if n: "n \<ge> a" for n :: nat
   7.839    proof -
   7.840      from n assms have "((\<lambda>x. x powr e) has_integral (F n - F a)) {a..n}"
   7.841 -      by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros 
   7.842 +      by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros
   7.843              simp: has_field_derivative_iff_has_vector_derivative [symmetric] F_def)
   7.844      hence "(f n has_integral (F n - F a)) {a..n}"
   7.845        by (rule has_integral_eq [rotated]) (simp add: f_def)
   7.846 @@ -12559,12 +12351,12 @@
   7.847    next
   7.848      case False
   7.849      have "(f n has_integral 0) {a}" by (rule has_integral_refl)
   7.850 -    hence "(f n has_integral 0) {a..}" 
   7.851 +    hence "(f n has_integral 0) {a..}"
   7.852        by (rule has_integral_on_superset [rotated 2]) (insert False, simp_all add: f_def)
   7.853      with False show ?thesis by (simp add: integral_unique)
   7.854    qed
   7.855 -  
   7.856 -  have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and> 
   7.857 +
   7.858 +  have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and>
   7.859             (\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> integral {a..} (\<lambda>x. x powr e)"
   7.860    proof (intro monotone_convergence_increasing allI ballI)
   7.861      fix n :: nat
   7.862 @@ -12582,7 +12374,7 @@
   7.863      from filterlim_real_sequentially
   7.864        have "eventually (\<lambda>n. real n \<ge> x) at_top"
   7.865        by (simp add: filterlim_at_top)
   7.866 -    with x have "eventually (\<lambda>n. f n x = x powr e) at_top" 
   7.867 +    with x have "eventually (\<lambda>n. f n x = x powr e) at_top"
   7.868        by (auto elim!: eventually_mono simp: f_def)
   7.869      thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: Lim_eventually)
   7.870    next
   7.871 @@ -12603,11 +12395,11 @@
   7.872    hence "eventually (\<lambda>n. F n - F a = integral {a..} (f n)) at_top"
   7.873      by eventually_elim (simp add: integral_f)
   7.874    moreover have "(\<lambda>n. F n - F a) \<longlonglongrightarrow> 0 / (e + 1) - F a" unfolding F_def
   7.875 -    by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr] 
   7.876 +    by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr]
   7.877            filterlim_ident filterlim_real_sequentially | simp)+)
   7.878    hence "(\<lambda>n. F n - F a) \<longlonglongrightarrow> -F a" by simp
   7.879    ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (rule Lim_transform_eventually)
   7.880 -  from conjunct2[OF *] and this 
   7.881 +  from conjunct2[OF *] and this
   7.882      have "integral {a..} (\<lambda>x. x powr e) = -F a" by (rule LIMSEQ_unique)
   7.883    with conjunct1[OF *] show ?thesis
   7.884      by (simp add: has_integral_integral F_def)
   7.885 @@ -12620,7 +12412,7 @@
   7.886  proof -
   7.887    from assms have "real_of_int (-int n) < -1" by simp
   7.888    note has_integral_powr_to_inf[OF this \<open>a > 0\<close>]
   7.889 -  also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) = 
   7.890 +  also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) =
   7.891                   1 / (real (n - 1) * a powr (real (n - 1)))" using assms
   7.892      by (simp add: divide_simps powr_add [symmetric] of_nat_diff)
   7.893    also from assms have "a powr (real (n - 1)) = a ^ (n - 1)"
   7.894 @@ -12630,4 +12422,33 @@
   7.895         (insert assms, simp_all add: powr_minus powr_realpow divide_simps)
   7.896  qed
   7.897  
   7.898 +subsubsection \<open>Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\<close>
   7.899 +
   7.900 +lemma integral_component_eq_cart[simp]:
   7.901 +  fixes f :: "'n::euclidean_space \<Rightarrow> real^'m"
   7.902 +  assumes "f integrable_on s"
   7.903 +  shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
   7.904 +  using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] .
   7.905 +
   7.906 +lemma content_closed_interval:
   7.907 +  fixes a :: "'a::ordered_euclidean_space"
   7.908 +  assumes "a \<le> b"
   7.909 +  shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
   7.910 +  using content_cbox[of a b] assms
   7.911 +  by (simp add: cbox_interval eucl_le[where 'a='a])
   7.912 +
   7.913 +lemma integrable_const_ivl[intro]:
   7.914 +  fixes a::"'a::ordered_euclidean_space"
   7.915 +  shows "(\<lambda>x. c) integrable_on {a .. b}"
   7.916 +  unfolding cbox_interval[symmetric]
   7.917 +  by (rule integrable_const)
   7.918 +
   7.919 +lemma integrable_on_subinterval:
   7.920 +  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
   7.921 +  assumes "f integrable_on s"
   7.922 +    and "{a .. b} \<subseteq> s"
   7.923 +  shows "f integrable_on {a .. b}"
   7.924 +  using integrable_on_subcbox[of f s a b] assms
   7.925 +  by (simp add: cbox_interval)
   7.926 +
   7.927  end
     8.1 --- a/src/HOL/Analysis/Interval_Integral.thy	Thu Sep 15 22:41:05 2016 +0200
     8.2 +++ b/src/HOL/Analysis/Interval_Integral.thy	Fri Sep 16 13:56:51 2016 +0200
     8.3 @@ -311,7 +311,7 @@
     8.4                     ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
     8.5                     uminus_ereal.simps[symmetric]
     8.6               simp del: uminus_ereal.simps
     8.7 -             intro!: integral_cong
     8.8 +             intro!: Bochner_Integration.integral_cong
     8.9               split: split_indicator)
    8.10  qed
    8.11  
     9.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 15 22:41:05 2016 +0200
     9.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Fri Sep 16 13:56:51 2016 +0200
     9.3 @@ -469,6 +469,10 @@
     9.4    "emeasure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
     9.5    using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force
     9.6  
     9.7 +lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
     9.8 +  using emeasure_lborel_cbox[of x x] nonempty_Basis
     9.9 +  by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing setprod_constant)
    9.10 +
    9.11  lemma
    9.12    fixes l u :: real
    9.13    assumes [simp]: "l \<le> u"
    9.14 @@ -484,6 +488,17 @@
    9.15      and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
    9.16    by (simp_all add: measure_def inner_diff_left setprod_nonneg)
    9.17  
    9.18 +lemma measure_lborel_cbox_eq:
    9.19 +  "measure lborel (cbox l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
    9.20 +  using box_eq_empty(2)[THEN iffD2, of u l] by (auto simp: not_le)
    9.21 +
    9.22 +lemma measure_lborel_box_eq:
    9.23 +  "measure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
    9.24 +  using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force
    9.25 +
    9.26 +lemma measure_lborel_singleton[simp]: "measure lborel {x} = 0"
    9.27 +  by (simp add: measure_def)
    9.28 +
    9.29  lemma sigma_finite_lborel: "sigma_finite_measure lborel"
    9.30  proof
    9.31    show "\<exists>A::'a set set. countable A \<and> A \<subseteq> sets lborel \<and> \<Union>A = space lborel \<and> (\<forall>a\<in>A. emeasure lborel a \<noteq> \<infinity>)"
    9.32 @@ -516,10 +531,6 @@
    9.33      done
    9.34  qed
    9.35  
    9.36 -lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
    9.37 -  using emeasure_lborel_cbox[of x x] nonempty_Basis
    9.38 -  by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing setprod_constant)
    9.39 -
    9.40  lemma emeasure_lborel_countable:
    9.41    fixes A :: "'a::euclidean_space set"
    9.42    assumes "countable A"
    9.43 @@ -572,46 +583,38 @@
    9.44  
    9.45    { fix i show "emeasure lborel (?A i) \<noteq> \<infinity>" by auto }
    9.46    { fix X assume "X \<in> ?E" then show "emeasure lborel X = emeasure M X"
    9.47 -      apply (auto simp: emeasure_eq emeasure_lborel_box_eq )
    9.48 +      apply (auto simp: emeasure_eq emeasure_lborel_box_eq)
    9.49        apply (subst box_eq_empty(1)[THEN iffD2])
    9.50        apply (auto intro: less_imp_le simp: not_le)
    9.51        done }
    9.52  qed
    9.53  
    9.54 -lemma lborel_affine:
    9.55 -  fixes t :: "'a::euclidean_space" assumes "c \<noteq> 0"
    9.56 -  shows "lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))" (is "_ = ?D")
    9.57 +lemma lborel_affine_euclidean:
    9.58 +  fixes c :: "'a::euclidean_space \<Rightarrow> real" and t
    9.59 +  defines "T x \<equiv> t + (\<Sum>j\<in>Basis. (c j * (x \<bullet> j)) *\<^sub>R j)"
    9.60 +  assumes c: "\<And>j. j \<in> Basis \<Longrightarrow> c j \<noteq> 0"
    9.61 +  shows "lborel = density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" (is "_ = ?D")
    9.62  proof (rule lborel_eqI)
    9.63    let ?B = "Basis :: 'a set"
    9.64    fix l u assume le: "\<And>b. b \<in> ?B \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
    9.65 -  show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)"
    9.66 -  proof cases
    9.67 -    assume "0 < c"
    9.68 -    then have "(\<lambda>x. t + c *\<^sub>R x) -` box l u = box ((l - t) /\<^sub>R c) ((u - t) /\<^sub>R c)"
    9.69 -      by (auto simp: field_simps box_def inner_simps)
    9.70 -    with \<open>0 < c\<close> show ?thesis
    9.71 -      using le
    9.72 -      by (auto simp: field_simps inner_simps setprod_dividef setprod_constant setprod_nonneg
    9.73 -                     ennreal_mult[symmetric] emeasure_density nn_integral_distr emeasure_distr
    9.74 -                     nn_integral_cmult emeasure_lborel_box_eq borel_measurable_indicator')
    9.75 -  next
    9.76 -    assume "\<not> 0 < c" with \<open>c \<noteq> 0\<close> have "c < 0" by auto
    9.77 -    then have "box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c) = (\<lambda>x. t + c *\<^sub>R x) -` box l u"
    9.78 -      by (auto simp: field_simps box_def inner_simps)
    9.79 -    then have *: "\<And>x. indicator (box l u) (t + c *\<^sub>R x) = (indicator (box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c)) x :: ennreal)"
    9.80 -      by (auto split: split_indicator)
    9.81 -    have **: "(\<Prod>x\<in>Basis. (l \<bullet> x - u \<bullet> x) / c) = (\<Prod>x\<in>Basis. u \<bullet> x - l \<bullet> x) / (-c) ^ card (Basis::'a set)"
    9.82 -      using \<open>c < 0\<close>
    9.83 -      by (auto simp add: field_simps setprod_dividef[symmetric] setprod_constant[symmetric]
    9.84 -               intro!: setprod.cong)
    9.85 -    show ?thesis
    9.86 -      using \<open>c < 0\<close> le
    9.87 -      by (auto simp: * ** field_simps emeasure_density nn_integral_distr nn_integral_cmult
    9.88 -                     emeasure_lborel_box_eq inner_simps setprod_nonneg ennreal_mult[symmetric]
    9.89 -                     borel_measurable_indicator')
    9.90 -  qed
    9.91 +  have [measurable]: "T \<in> borel \<rightarrow>\<^sub>M borel"
    9.92 +    by (simp add: T_def[abs_def])
    9.93 +  have eq: "T -` box l u = box
    9.94 +    (\<Sum>j\<in>Basis. (((if 0 < c j then l - t else u - t) \<bullet> j) / c j) *\<^sub>R j)
    9.95 +    (\<Sum>j\<in>Basis. (((if 0 < c j then u - t else l - t) \<bullet> j) / c j) *\<^sub>R j)"
    9.96 +    using c by (auto simp: box_def T_def field_simps inner_simps divide_less_eq)
    9.97 +  with le c show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)"
    9.98 +    by (auto simp: emeasure_density emeasure_distr nn_integral_multc emeasure_lborel_box_eq inner_simps
    9.99 +                   field_simps divide_simps ennreal_mult'[symmetric] setprod_nonneg setprod.distrib[symmetric]
   9.100 +             intro!: setprod.cong)
   9.101  qed simp
   9.102  
   9.103 +lemma lborel_affine:
   9.104 +  fixes t :: "'a::euclidean_space"
   9.105 +  shows "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))"
   9.106 +  using lborel_affine_euclidean[where c="\<lambda>_::'a. c" and t=t]
   9.107 +  unfolding scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric] euclidean_representation setprod_constant by simp
   9.108 +
   9.109  lemma lborel_real_affine:
   9.110    "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. ennreal (abs c))"
   9.111    using lborel_affine[of c t] by simp
   9.112 @@ -726,378 +729,6 @@
   9.113  lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
   9.114  lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
   9.115  
   9.116 -subsection \<open>Equivalence Lebesgue integral on @{const lborel} and HK-integral\<close>
   9.117 -
   9.118 -lemma has_integral_measure_lborel:
   9.119 -  fixes A :: "'a::euclidean_space set"
   9.120 -  assumes A[measurable]: "A \<in> sets borel" and finite: "emeasure lborel A < \<infinity>"
   9.121 -  shows "((\<lambda>x. 1) has_integral measure lborel A) A"
   9.122 -proof -
   9.123 -  { fix l u :: 'a
   9.124 -    have "((\<lambda>x. 1) has_integral measure lborel (box l u)) (box l u)"
   9.125 -    proof cases
   9.126 -      assume "\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b"
   9.127 -      then show ?thesis
   9.128 -        apply simp
   9.129 -        apply (subst has_integral_restrict[symmetric, OF box_subset_cbox])
   9.130 -        apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"])
   9.131 -        using has_integral_const[of "1::real" l u]
   9.132 -        apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases)
   9.133 -        done
   9.134 -    next
   9.135 -      assume "\<not> (\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b)"
   9.136 -      then have "box l u = {}"
   9.137 -        unfolding box_eq_empty by (auto simp: not_le intro: less_imp_le)
   9.138 -      then show ?thesis
   9.139 -        by simp
   9.140 -    qed }
   9.141 -  note has_integral_box = this
   9.142 -
   9.143 -  { fix a b :: 'a let ?M = "\<lambda>A. measure lborel (A \<inter> box a b)"
   9.144 -    have "Int_stable  (range (\<lambda>(a, b). box a b))"
   9.145 -      by (auto simp: Int_stable_def box_Int_box)
   9.146 -    moreover have "(range (\<lambda>(a, b). box a b)) \<subseteq> Pow UNIV"
   9.147 -      by auto
   9.148 -    moreover have "A \<in> sigma_sets UNIV (range (\<lambda>(a, b). box a b))"
   9.149 -       using A unfolding borel_eq_box by simp
   9.150 -    ultimately have "((\<lambda>x. 1) has_integral ?M A) (A \<inter> box a b)"
   9.151 -    proof (induction rule: sigma_sets_induct_disjoint)
   9.152 -      case (basic A) then show ?case
   9.153 -        by (auto simp: box_Int_box has_integral_box)
   9.154 -    next
   9.155 -      case empty then show ?case
   9.156 -        by simp
   9.157 -    next
   9.158 -      case (compl A)
   9.159 -      then have [measurable]: "A \<in> sets borel"
   9.160 -        by (simp add: borel_eq_box)
   9.161 -
   9.162 -      have "((\<lambda>x. 1) has_integral ?M (box a b)) (box a b)"
   9.163 -        by (simp add: has_integral_box)
   9.164 -      moreover have "((\<lambda>x. if x \<in> A \<inter> box a b then 1 else 0) has_integral ?M A) (box a b)"
   9.165 -        by (subst has_integral_restrict) (auto intro: compl)
   9.166 -      ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
   9.167 -        by (rule has_integral_sub)
   9.168 -      then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
   9.169 -        by (rule has_integral_cong[THEN iffD1, rotated 1]) auto
   9.170 -      then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box a b)"
   9.171 -        by (subst (asm) has_integral_restrict) auto
   9.172 -      also have "?M (box a b) - ?M A = ?M (UNIV - A)"
   9.173 -        by (subst measure_Diff[symmetric]) (auto simp: emeasure_lborel_box_eq Diff_Int_distrib2)
   9.174 -      finally show ?case .
   9.175 -    next
   9.176 -      case (union F)
   9.177 -      then have [measurable]: "\<And>i. F i \<in> sets borel"
   9.178 -        by (simp add: borel_eq_box subset_eq)
   9.179 -      have "((\<lambda>x. if x \<in> UNION UNIV F \<inter> box a b then 1 else 0) has_integral ?M (\<Union>i. F i)) (box a b)"
   9.180 -      proof (rule has_integral_monotone_convergence_increasing)
   9.181 -        let ?f = "\<lambda>k x. \<Sum>i<k. if x \<in> F i \<inter> box a b then 1 else 0 :: real"
   9.182 -        show "\<And>k. (?f k has_integral (\<Sum>i<k. ?M (F i))) (box a b)"
   9.183 -          using union.IH by (auto intro!: has_integral_setsum simp del: Int_iff)
   9.184 -        show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
   9.185 -          by (intro setsum_mono2) auto
   9.186 -        from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
   9.187 -          by (auto simp add: disjoint_family_on_def)
   9.188 -        show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)"
   9.189 -          apply (auto simp: * setsum.If_cases Iio_Int_singleton)
   9.190 -          apply (rule_tac k="Suc xa" in LIMSEQ_offset)
   9.191 -          apply simp
   9.192 -          done
   9.193 -        have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)"
   9.194 -          by (intro emeasure_mono) auto
   9.195 -
   9.196 -        with union(1) show "(\<lambda>k. \<Sum>i<k. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F i)"
   9.197 -          unfolding sums_def[symmetric] UN_extend_simps
   9.198 -          by (intro measure_UNION) (auto simp: disjoint_family_on_def emeasure_lborel_box_eq top_unique)
   9.199 -      qed
   9.200 -      then show ?case
   9.201 -        by (subst (asm) has_integral_restrict) auto
   9.202 -    qed }
   9.203 -  note * = this
   9.204 -
   9.205 -  show ?thesis
   9.206 -  proof (rule has_integral_monotone_convergence_increasing)
   9.207 -    let ?B = "\<lambda>n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One) :: 'a set"
   9.208 -    let ?f = "\<lambda>n::nat. \<lambda>x. if x \<in> A \<inter> ?B n then 1 else 0 :: real"
   9.209 -    let ?M = "\<lambda>n. measure lborel (A \<inter> ?B n)"
   9.210 -
   9.211 -    show "\<And>n::nat. (?f n has_integral ?M n) A"
   9.212 -      using * by (subst has_integral_restrict) simp_all
   9.213 -    show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
   9.214 -      by (auto simp: box_def)
   9.215 -    { fix x assume "x \<in> A"
   9.216 -      moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) \<longlonglongrightarrow> indicator (\<Union>k::nat. A \<inter> ?B k) x"
   9.217 -        by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def)
   9.218 -      ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) \<longlonglongrightarrow> 1"
   9.219 -        by (simp add: indicator_def UN_box_eq_UNIV) }
   9.220 -
   9.221 -    have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> emeasure lborel (\<Union>n::nat. A \<inter> ?B n)"
   9.222 -      by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def)
   9.223 -    also have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) = (\<lambda>n. measure lborel (A \<inter> ?B n))"
   9.224 -    proof (intro ext emeasure_eq_ennreal_measure)
   9.225 -      fix n have "emeasure lborel (A \<inter> ?B n) \<le> emeasure lborel (?B n)"
   9.226 -        by (intro emeasure_mono) auto
   9.227 -      then show "emeasure lborel (A \<inter> ?B n) \<noteq> top"
   9.228 -        by (auto simp: top_unique)
   9.229 -    qed
   9.230 -    finally show "(\<lambda>n. measure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> measure lborel A"
   9.231 -      using emeasure_eq_ennreal_measure[of lborel A] finite
   9.232 -      by (simp add: UN_box_eq_UNIV less_top)
   9.233 -  qed
   9.234 -qed
   9.235 -
   9.236 -lemma nn_integral_has_integral:
   9.237 -  fixes f::"'a::euclidean_space \<Rightarrow> real"
   9.238 -  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
   9.239 -  shows "(f has_integral r) UNIV"
   9.240 -using f proof (induct f arbitrary: r rule: borel_measurable_induct_real)
   9.241 -  case (set A)
   9.242 -  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
   9.243 -    by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator)
   9.244 -  with set show ?case
   9.245 -    by (simp add: ennreal_indicator measure_def) (simp add: indicator_def)
   9.246 -next
   9.247 -  case (mult g c)
   9.248 -  then have "ennreal c * (\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal r"
   9.249 -    by (subst nn_integral_cmult[symmetric]) (auto simp: ennreal_mult)
   9.250 -  with \<open>0 \<le> r\<close> \<open>0 \<le> c\<close>
   9.251 -  obtain r' where "(c = 0 \<and> r = 0) \<or> (0 \<le> r' \<and> (\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel) = ennreal r' \<and> r = c * r')"
   9.252 -    by (cases "\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel" rule: ennreal_cases)
   9.253 -       (auto split: if_split_asm simp: ennreal_mult_top ennreal_mult[symmetric])
   9.254 -  with mult show ?case
   9.255 -    by (auto intro!: has_integral_cmult_real)
   9.256 -next
   9.257 -  case (add g h)
   9.258 -  then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lborel) = (\<integral>\<^sup>+ x. h x \<partial>lborel) + (\<integral>\<^sup>+ x. g x \<partial>lborel)"
   9.259 -    by (simp add: nn_integral_add)
   9.260 -  with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b"
   9.261 -    by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
   9.262 -       (auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus)
   9.263 -  with add show ?case
   9.264 -    by (auto intro!: has_integral_add)
   9.265 -next
   9.266 -  case (seq U)
   9.267 -  note seq(1)[measurable] and f[measurable]
   9.268 -
   9.269 -  { fix i x
   9.270 -    have "U i x \<le> f x"
   9.271 -      using seq(5)
   9.272 -      apply (rule LIMSEQ_le_const)
   9.273 -      using seq(4)
   9.274 -      apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def)
   9.275 -      done }
   9.276 -  note U_le_f = this
   9.277 -
   9.278 -  { fix i
   9.279 -    have "(\<integral>\<^sup>+x. U i x \<partial>lborel) \<le> (\<integral>\<^sup>+x. f x \<partial>lborel)"
   9.280 -      using seq(2) f(2) U_le_f by (intro nn_integral_mono) simp
   9.281 -    then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p" "p \<le> r" "0 \<le> p"
   9.282 -      using seq(6) \<open>0\<le>r\<close> by (cases "\<integral>\<^sup>+x. U i x \<partial>lborel" rule: ennreal_cases) (auto simp: top_unique)
   9.283 -    moreover note seq
   9.284 -    ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV"
   9.285 -      by auto }
   9.286 -  then obtain p where p: "\<And>i. (\<integral>\<^sup>+x. ennreal (U i x) \<partial>lborel) = ennreal (p i)"
   9.287 -    and bnd: "\<And>i. p i \<le> r" "\<And>i. 0 \<le> p i"
   9.288 -    and U_int: "\<And>i.(U i has_integral (p i)) UNIV" by metis
   9.289 -
   9.290 -  have int_eq: "\<And>i. integral UNIV (U i) = p i" using U_int by (rule integral_unique)
   9.291 -
   9.292 -  have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) \<longlonglongrightarrow> integral UNIV f"
   9.293 -  proof (rule monotone_convergence_increasing)
   9.294 -    show "\<forall>k. U k integrable_on UNIV" using U_int by auto
   9.295 -    show "\<forall>k. \<forall>x\<in>UNIV. U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def)
   9.296 -    then show "bounded {integral UNIV (U k) |k. True}"
   9.297 -      using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r])
   9.298 -    show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) \<longlonglongrightarrow> f x"
   9.299 -      using seq by auto
   9.300 -  qed
   9.301 -  moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. f x \<partial>lborel)"
   9.302 -    using seq f(2) U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
   9.303 -  ultimately have "integral UNIV f = r"
   9.304 -    by (auto simp add: bnd int_eq p seq intro: LIMSEQ_unique)
   9.305 -  with * show ?case
   9.306 -    by (simp add: has_integral_integral)
   9.307 -qed
   9.308 -
   9.309 -lemma nn_integral_lborel_eq_integral:
   9.310 -  fixes f::"'a::euclidean_space \<Rightarrow> real"
   9.311 -  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
   9.312 -  shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = integral UNIV f"
   9.313 -proof -
   9.314 -  from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
   9.315 -    by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
   9.316 -  then show ?thesis
   9.317 -    using nn_integral_has_integral[OF f(1,2) r] by (simp add: integral_unique)
   9.318 -qed
   9.319 -
   9.320 -lemma nn_integral_integrable_on:
   9.321 -  fixes f::"'a::euclidean_space \<Rightarrow> real"
   9.322 -  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
   9.323 -  shows "f integrable_on UNIV"
   9.324 -proof -
   9.325 -  from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
   9.326 -    by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
   9.327 -  then show ?thesis
   9.328 -    by (intro has_integral_integrable[where i=r] nn_integral_has_integral[where r=r] f)
   9.329 -qed
   9.330 -
   9.331 -lemma nn_integral_has_integral_lborel:
   9.332 -  fixes f :: "'a::euclidean_space \<Rightarrow> real"
   9.333 -  assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
   9.334 -  assumes I: "(f has_integral I) UNIV"
   9.335 -  shows "integral\<^sup>N lborel f = I"
   9.336 -proof -
   9.337 -  from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" by auto
   9.338 -  from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
   9.339 -  let ?B = "\<lambda>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One) :: 'a set"
   9.340 -
   9.341 -  note F(1)[THEN borel_measurable_simple_function, measurable]
   9.342 -
   9.343 -  have "0 \<le> I"
   9.344 -    using I by (rule has_integral_nonneg) (simp add: nonneg)
   9.345 -
   9.346 -  have F_le_f: "enn2real (F i x) \<le> f x" for i x
   9.347 -    using F(3,4)[where x=x] nonneg SUP_upper[of i UNIV "\<lambda>i. F i x"]
   9.348 -    by (cases "F i x" rule: ennreal_cases) auto
   9.349 -  let ?F = "\<lambda>i x. F i x * indicator (?B i) x"
   9.350 -  have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (SUP i. integral\<^sup>N lborel (\<lambda>x. ?F i x))"
   9.351 -  proof (subst nn_integral_monotone_convergence_SUP[symmetric])
   9.352 -    { fix x
   9.353 -      obtain j where j: "x \<in> ?B j"
   9.354 -        using UN_box_eq_UNIV by auto
   9.355 -
   9.356 -      have "ennreal (f x) = (SUP i. F i x)"
   9.357 -        using F(4)[of x] nonneg[of x] by (simp add: max_def)
   9.358 -      also have "\<dots> = (SUP i. ?F i x)"
   9.359 -      proof (rule SUP_eq)
   9.360 -        fix i show "\<exists>j\<in>UNIV. F i x \<le> ?F j x"
   9.361 -          using j F(2)
   9.362 -          by (intro bexI[of _ "max i j"])
   9.363 -             (auto split: split_max split_indicator simp: incseq_def le_fun_def box_def)
   9.364 -      qed (auto intro!: F split: split_indicator)
   9.365 -      finally have "ennreal (f x) =  (SUP i. ?F i x)" . }
   9.366 -    then show "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (\<integral>\<^sup>+ x. (SUP i. ?F i x) \<partial>lborel)"
   9.367 -      by simp
   9.368 -  qed (insert F, auto simp: incseq_def le_fun_def box_def split: split_indicator)
   9.369 -  also have "\<dots> \<le> ennreal I"
   9.370 -  proof (rule SUP_least)
   9.371 -    fix i :: nat
   9.372 -    have finite_F: "(\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel) < \<infinity>"
   9.373 -    proof (rule nn_integral_bound_simple_function)
   9.374 -      have "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} \<le>
   9.375 -        emeasure lborel (?B i)"
   9.376 -        by (intro emeasure_mono)  (auto split: split_indicator)
   9.377 -      then show "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} < \<infinity>"
   9.378 -        by (auto simp: less_top[symmetric] top_unique)
   9.379 -    qed (auto split: split_indicator
   9.380 -              intro!: F simple_function_compose1[where g="enn2real"] simple_function_ennreal)
   9.381 -
   9.382 -    have int_F: "(\<lambda>x. enn2real (F i x) * indicator (?B i) x) integrable_on UNIV"
   9.383 -      using F(4) finite_F
   9.384 -      by (intro nn_integral_integrable_on) (auto split: split_indicator simp: enn2real_nonneg)
   9.385 -
   9.386 -    have "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) =
   9.387 -      (\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel)"
   9.388 -      using F(3,4)
   9.389 -      by (intro nn_integral_cong) (auto simp: image_iff eq_commute split: split_indicator)
   9.390 -    also have "\<dots> = ennreal (integral UNIV (\<lambda>x. enn2real (F i x) * indicator (?B i) x))"
   9.391 -      using F
   9.392 -      by (intro nn_integral_lborel_eq_integral[OF _ _ finite_F])
   9.393 -         (auto split: split_indicator intro: enn2real_nonneg)
   9.394 -    also have "\<dots> \<le> ennreal I"
   9.395 -      by (auto intro!: has_integral_le[OF integrable_integral[OF int_F] I] nonneg F_le_f
   9.396 -               simp: \<open>0 \<le> I\<close> split: split_indicator )
   9.397 -    finally show "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) \<le> ennreal I" .
   9.398 -  qed
   9.399 -  finally have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) < \<infinity>"
   9.400 -    by (auto simp: less_top[symmetric] top_unique)
   9.401 -  from nn_integral_lborel_eq_integral[OF assms(1,2) this] I show ?thesis
   9.402 -    by (simp add: integral_unique)
   9.403 -qed
   9.404 -
   9.405 -lemma has_integral_iff_emeasure_lborel:
   9.406 -  fixes A :: "'a::euclidean_space set"
   9.407 -  assumes A[measurable]: "A \<in> sets borel" and [simp]: "0 \<le> r"
   9.408 -  shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ennreal r"
   9.409 -proof (cases "emeasure lborel A = \<infinity>")
   9.410 -  case emeasure_A: True
   9.411 -  have "\<not> (\<lambda>x. 1::real) integrable_on A"
   9.412 -  proof
   9.413 -    assume int: "(\<lambda>x. 1::real) integrable_on A"
   9.414 -    then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV"
   9.415 -      unfolding indicator_def[abs_def] integrable_restrict_univ .
   9.416 -    then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV"
   9.417 -      by auto
   9.418 -    from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False
   9.419 -      by (simp add: ennreal_indicator)
   9.420 -  qed
   9.421 -  with emeasure_A show ?thesis
   9.422 -    by auto
   9.423 -next
   9.424 -  case False
   9.425 -  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
   9.426 -    by (simp add: has_integral_measure_lborel less_top)
   9.427 -  with False show ?thesis
   9.428 -    by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
   9.429 -qed
   9.430 -
   9.431 -lemma has_integral_integral_real:
   9.432 -  fixes f::"'a::euclidean_space \<Rightarrow> real"
   9.433 -  assumes f: "integrable lborel f"
   9.434 -  shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
   9.435 -using f proof induct
   9.436 -  case (base A c) then show ?case
   9.437 -    by (auto intro!: has_integral_mult_left simp: )
   9.438 -       (simp add: emeasure_eq_ennreal_measure indicator_def has_integral_measure_lborel)
   9.439 -next
   9.440 -  case (add f g) then show ?case
   9.441 -    by (auto intro!: has_integral_add)
   9.442 -next
   9.443 -  case (lim f s)
   9.444 -  show ?case
   9.445 -  proof (rule has_integral_dominated_convergence)
   9.446 -    show "\<And>i. (s i has_integral integral\<^sup>L lborel (s i)) UNIV" by fact
   9.447 -    show "(\<lambda>x. norm (2 * f x)) integrable_on UNIV"
   9.448 -      using \<open>integrable lborel f\<close>
   9.449 -      by (intro nn_integral_integrable_on)
   9.450 -         (auto simp: integrable_iff_bounded abs_mult  nn_integral_cmult ennreal_mult ennreal_mult_less_top)
   9.451 -    show "\<And>k. \<forall>x\<in>UNIV. norm (s k x) \<le> norm (2 * f x)"
   9.452 -      using lim by (auto simp add: abs_mult)
   9.453 -    show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) \<longlonglongrightarrow> f x"
   9.454 -      using lim by auto
   9.455 -    show "(\<lambda>k. integral\<^sup>L lborel (s k)) \<longlonglongrightarrow> integral\<^sup>L lborel f"
   9.456 -      using lim lim(1)[THEN borel_measurable_integrable]
   9.457 -      by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
   9.458 -  qed
   9.459 -qed
   9.460 -
   9.461 -context
   9.462 -  fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   9.463 -begin
   9.464 -
   9.465 -lemma has_integral_integral_lborel:
   9.466 -  assumes f: "integrable lborel f"
   9.467 -  shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
   9.468 -proof -
   9.469 -  have "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b)) UNIV"
   9.470 -    using f by (intro has_integral_setsum finite_Basis ballI has_integral_scaleR_left has_integral_integral_real) auto
   9.471 -  also have eq_f: "(\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) = f"
   9.472 -    by (simp add: fun_eq_iff euclidean_representation)
   9.473 -  also have "(\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lborel f"
   9.474 -    using f by (subst (2) eq_f[symmetric]) simp
   9.475 -  finally show ?thesis .
   9.476 -qed
   9.477 -
   9.478 -lemma integrable_on_lborel: "integrable lborel f \<Longrightarrow> f integrable_on UNIV"
   9.479 -  using has_integral_integral_lborel by auto
   9.480 -
   9.481 -lemma integral_lborel: "integrable lborel f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lborel)"
   9.482 -  using has_integral_integral_lborel by auto
   9.483 -
   9.484 -end
   9.485 -
   9.486 -subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
   9.487 -
   9.488  lemma emeasure_bounded_finite:
   9.489    assumes "bounded A" shows "emeasure lborel A < \<infinity>"
   9.490  proof -
   9.491 @@ -1149,233 +780,4 @@
   9.492      by (auto simp: mult.commute)
   9.493  qed
   9.494  
   9.495 -text \<open>
   9.496 -
   9.497 -For the positive integral we replace continuity with Borel-measurability.
   9.498 -
   9.499 -\<close>
   9.500 -
   9.501 -lemma
   9.502 -  fixes f :: "real \<Rightarrow> real"
   9.503 -  assumes [measurable]: "f \<in> borel_measurable borel"
   9.504 -  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"
   9.505 -  shows nn_integral_FTC_Icc: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?nn)
   9.506 -    and has_bochner_integral_FTC_Icc_nonneg:
   9.507 -      "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
   9.508 -    and integral_FTC_Icc_nonneg: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
   9.509 -    and integrable_FTC_Icc_nonneg: "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is ?int)
   9.510 -proof -
   9.511 -  have *: "(\<lambda>x. f x * indicator {a..b} x) \<in> borel_measurable borel" "\<And>x. 0 \<le> f x * indicator {a..b} x"
   9.512 -    using f(2) by (auto split: split_indicator)
   9.513 -
   9.514 -  have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b\<Longrightarrow> F x \<le> F y" for x y
   9.515 -    using f by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
   9.516 -
   9.517 -  have "(f has_integral F b - F a) {a..b}"
   9.518 -    by (intro fundamental_theorem_of_calculus)
   9.519 -       (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
   9.520 -             intro: has_field_derivative_subset[OF f(1)] \<open>a \<le> b\<close>)
   9.521 -  then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
   9.522 -    unfolding indicator_def if_distrib[where f="\<lambda>x. a * x" for a]
   9.523 -    by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
   9.524 -  then have nn: "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
   9.525 -    by (rule nn_integral_has_integral_lborel[OF *])
   9.526 -  then show ?has
   9.527 -    by (rule has_bochner_integral_nn_integral[rotated 3]) (simp_all add: * F_mono \<open>a \<le> b\<close>)
   9.528 -  then show ?eq ?int
   9.529 -    unfolding has_bochner_integral_iff by auto
   9.530 -  show ?nn
   9.531 -    by (subst nn[symmetric])
   9.532 -       (auto intro!: nn_integral_cong simp add: ennreal_mult f split: split_indicator)
   9.533 -qed
   9.534 -
   9.535 -lemma
   9.536 -  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
   9.537 -  assumes "a \<le> b"
   9.538 -  assumes "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
   9.539 -  assumes cont: "continuous_on {a .. b} f"
   9.540 -  shows has_bochner_integral_FTC_Icc:
   9.541 -      "has_bochner_integral lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) (F b - F a)" (is ?has)
   9.542 -    and integral_FTC_Icc: "(\<integral>x. indicator {a .. b} x *\<^sub>R f x \<partial>lborel) = F b - F a" (is ?eq)
   9.543 -proof -
   9.544 -  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
   9.545 -  have int: "integrable lborel ?f"
   9.546 -    using borel_integrable_compact[OF _ cont] by auto
   9.547 -  have "(f has_integral F b - F a) {a..b}"
   9.548 -    using assms(1,2) by (intro fundamental_theorem_of_calculus) auto
   9.549 -  moreover
   9.550 -  have "(f has_integral integral\<^sup>L lborel ?f) {a..b}"
   9.551 -    using has_integral_integral_lborel[OF int]
   9.552 -    unfolding indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a]
   9.553 -    by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
   9.554 -  ultimately show ?eq
   9.555 -    by (auto dest: has_integral_unique)
   9.556 -  then show ?has
   9.557 -    using int by (auto simp: has_bochner_integral_iff)
   9.558 -qed
   9.559 -
   9.560 -lemma
   9.561 -  fixes f :: "real \<Rightarrow> real"
   9.562 -  assumes "a \<le> b"
   9.563 -  assumes deriv: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> DERIV F x :> f x"
   9.564 -  assumes cont: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
   9.565 -  shows has_bochner_integral_FTC_Icc_real:
   9.566 -      "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
   9.567 -    and integral_FTC_Icc_real: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
   9.568 -proof -
   9.569 -  have 1: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
   9.570 -    unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
   9.571 -    using deriv by (auto intro: DERIV_subset)
   9.572 -  have 2: "continuous_on {a .. b} f"
   9.573 -    using cont by (intro continuous_at_imp_continuous_on) auto
   9.574 -  show ?has ?eq
   9.575 -    using has_bochner_integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2] integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2]
   9.576 -    by (auto simp: mult.commute)
   9.577 -qed
   9.578 -
   9.579 -lemma nn_integral_FTC_atLeast:
   9.580 -  fixes f :: "real \<Rightarrow> real"
   9.581 -  assumes f_borel: "f \<in> borel_measurable borel"
   9.582 -  assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x"
   9.583 -  assumes nonneg: "\<And>x. a \<le> x \<Longrightarrow> 0 \<le> f x"
   9.584 -  assumes lim: "(F \<longlongrightarrow> T) at_top"
   9.585 -  shows "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a ..} x \<partial>lborel) = T - F a"
   9.586 -proof -
   9.587 -  let ?f = "\<lambda>(i::nat) (x::real). ennreal (f x) * indicator {a..a + real i} x"
   9.588 -  let ?fR = "\<lambda>x. ennreal (f x) * indicator {a ..} x"
   9.589 -
   9.590 -  have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> F x \<le> F y" for x y
   9.591 -    using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
   9.592 -  then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x
   9.593 -    by (intro tendsto_le_const[OF _ lim])
   9.594 -       (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder)
   9.595 -
   9.596 -  have "(SUP i::nat. ?f i x) = ?fR x" for x
   9.597 -  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
   9.598 -    from reals_Archimedean2[of "x - a"] guess n ..
   9.599 -    then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
   9.600 -      by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
   9.601 -    then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
   9.602 -      by (rule Lim_eventually)
   9.603 -  qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
   9.604 -  then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
   9.605 -    by simp
   9.606 -  also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
   9.607 -  proof (rule nn_integral_monotone_convergence_SUP)
   9.608 -    show "incseq ?f"
   9.609 -      using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
   9.610 -    show "\<And>i. (?f i) \<in> borel_measurable lborel"
   9.611 -      using f_borel by auto
   9.612 -  qed
   9.613 -  also have "\<dots> = (SUP i::nat. ennreal (F (a + real i) - F a))"
   9.614 -    by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
   9.615 -  also have "\<dots> = T - F a"
   9.616 -  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
   9.617 -    have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
   9.618 -      apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top])
   9.619 -      apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl])
   9.620 -      apply (rule filterlim_real_sequentially)
   9.621 -      done
   9.622 -    then show "(\<lambda>n. ennreal (F (a + real n) - F a)) \<longlonglongrightarrow> ennreal (T - F a)"
   9.623 -      by (simp add: F_mono F_le_T tendsto_diff)
   9.624 -  qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
   9.625 -  finally show ?thesis .
   9.626 -qed
   9.627 -
   9.628 -lemma integral_power:
   9.629 -  "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k"
   9.630 -proof (subst integral_FTC_Icc_real)
   9.631 -  fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
   9.632 -    by (intro derivative_eq_intros) auto
   9.633 -qed (auto simp: field_simps simp del: of_nat_Suc)
   9.634 -
   9.635 -subsection \<open>Integration by parts\<close>
   9.636 -
   9.637 -lemma integral_by_parts_integrable:
   9.638 -  fixes f g F G::"real \<Rightarrow> real"
   9.639 -  assumes "a \<le> b"
   9.640 -  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
   9.641 -  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
   9.642 -  assumes [intro]: "!!x. DERIV F x :> f x"
   9.643 -  assumes [intro]: "!!x. DERIV G x :> g x"
   9.644 -  shows  "integrable lborel (\<lambda>x.((F x) * (g x) + (f x) * (G x)) * indicator {a .. b} x)"
   9.645 -  by (auto intro!: borel_integrable_atLeastAtMost continuous_intros) (auto intro!: DERIV_isCont)
   9.646 -
   9.647 -lemma integral_by_parts:
   9.648 -  fixes f g F G::"real \<Rightarrow> real"
   9.649 -  assumes [arith]: "a \<le> b"
   9.650 -  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
   9.651 -  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
   9.652 -  assumes [intro]: "!!x. DERIV F x :> f x"
   9.653 -  assumes [intro]: "!!x. DERIV G x :> g x"
   9.654 -  shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
   9.655 -            =  F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
   9.656 -proof-
   9.657 -  have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
   9.658 -    by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros)
   9.659 -      (auto intro!: DERIV_isCont)
   9.660 -
   9.661 -  have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
   9.662 -    (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
   9.663 -    apply (subst integral_add[symmetric])
   9.664 -    apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros)
   9.665 -    by (auto intro!: DERIV_isCont integral_cong split:split_indicator)
   9.666 -
   9.667 -  thus ?thesis using 0 by auto
   9.668 -qed
   9.669 -
   9.670 -lemma integral_by_parts':
   9.671 -  fixes f g F G::"real \<Rightarrow> real"
   9.672 -  assumes "a \<le> b"
   9.673 -  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
   9.674 -  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
   9.675 -  assumes "!!x. DERIV F x :> f x"
   9.676 -  assumes "!!x. DERIV G x :> g x"
   9.677 -  shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
   9.678 -            =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel"
   9.679 -  using integral_by_parts[OF assms] by (simp add: ac_simps)
   9.680 -
   9.681 -lemma has_bochner_integral_even_function:
   9.682 -  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   9.683 -  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
   9.684 -  assumes even: "\<And>x. f (- x) = f x"
   9.685 -  shows "has_bochner_integral lborel f (2 *\<^sub>R x)"
   9.686 -proof -
   9.687 -  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
   9.688 -    by (auto split: split_indicator)
   9.689 -  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x"
   9.690 -    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
   9.691 -       (auto simp: indicator even f)
   9.692 -  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + x)"
   9.693 -    by (rule has_bochner_integral_add)
   9.694 -  then have "has_bochner_integral lborel f (x + x)"
   9.695 -    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
   9.696 -       (auto split: split_indicator)
   9.697 -  then show ?thesis
   9.698 -    by (simp add: scaleR_2)
   9.699 -qed
   9.700 -
   9.701 -lemma has_bochner_integral_odd_function:
   9.702 -  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   9.703 -  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
   9.704 -  assumes odd: "\<And>x. f (- x) = - f x"
   9.705 -  shows "has_bochner_integral lborel f 0"
   9.706 -proof -
   9.707 -  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
   9.708 -    by (auto split: split_indicator)
   9.709 -  have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x"
   9.710 -    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
   9.711 -       (auto simp: indicator odd f)
   9.712 -  from has_bochner_integral_minus[OF this]
   9.713 -  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)"
   9.714 -    by simp
   9.715 -  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + - x)"
   9.716 -    by (rule has_bochner_integral_add)
   9.717 -  then have "has_bochner_integral lborel f (x + - x)"
   9.718 -    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
   9.719 -       (auto split: split_indicator)
   9.720 -  then show ?thesis
   9.721 -    by simp
   9.722 -qed
   9.723 -
   9.724  end
    10.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 15 22:41:05 2016 +0200
    10.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Sep 16 13:56:51 2016 +0200
    10.3 @@ -10,6 +10,30 @@
    10.4    "~~/src/HOL/Library/Infinite_Set"
    10.5  begin
    10.6  
    10.7 +lemma linear_simps:
    10.8 +  assumes "bounded_linear f"
    10.9 +  shows
   10.10 +    "f (a + b) = f a + f b"
   10.11 +    "f (a - b) = f a - f b"
   10.12 +    "f 0 = 0"
   10.13 +    "f (- a) = - f a"
   10.14 +    "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
   10.15 +proof -
   10.16 +  interpret f: bounded_linear f by fact
   10.17 +  show "f (a + b) = f a + f b" by (rule f.add)
   10.18 +  show "f (a - b) = f a - f b" by (rule f.diff)
   10.19 +  show "f 0 = 0" by (rule f.zero)
   10.20 +  show "f (- a) = - f a" by (rule f.minus)
   10.21 +  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
   10.22 +qed
   10.23 +
   10.24 +lemma bounded_linearI:
   10.25 +  assumes "\<And>x y. f (x + y) = f x + f y"
   10.26 +    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
   10.27 +    and "\<And>x. norm (f x) \<le> norm x * K"
   10.28 +  shows "bounded_linear f"
   10.29 +  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
   10.30 +
   10.31  subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
   10.32  
   10.33  definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
    11.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Sep 15 22:41:05 2016 +0200
    11.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Sep 16 13:56:51 2016 +0200
    11.3 @@ -243,27 +243,6 @@
    11.4  lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
    11.5    by (auto intro: setsum_nonneg)
    11.6  
    11.7 -lemma content_closed_interval:
    11.8 -  fixes a :: "'a::ordered_euclidean_space"
    11.9 -  assumes "a \<le> b"
   11.10 -  shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
   11.11 -  using content_cbox[of a b] assms
   11.12 -  by (simp add: cbox_interval eucl_le[where 'a='a])
   11.13 -
   11.14 -lemma integrable_const_ivl[intro]:
   11.15 -  fixes a::"'a::ordered_euclidean_space"
   11.16 -  shows "(\<lambda>x. c) integrable_on {a .. b}"
   11.17 -  unfolding cbox_interval[symmetric]
   11.18 -  by (rule integrable_const)
   11.19 -
   11.20 -lemma integrable_on_subinterval:
   11.21 -  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
   11.22 -  assumes "f integrable_on s"
   11.23 -    and "{a .. b} \<subseteq> s"
   11.24 -  shows "f integrable_on {a .. b}"
   11.25 -  using integrable_on_subcbox[of f s a b] assms
   11.26 -  by (simp add: cbox_interval)
   11.27 -
   11.28  lemma
   11.29    fixes a b::"'a::ordered_euclidean_space"
   11.30    shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"
    12.1 --- a/src/HOL/Analysis/Set_Integral.thy	Thu Sep 15 22:41:05 2016 +0200
    12.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Fri Sep 16 13:56:51 2016 +0200
    12.3 @@ -7,7 +7,7 @@
    12.4  *)
    12.5  
    12.6  theory Set_Integral
    12.7 -  imports Bochner_Integration Lebesgue_Measure
    12.8 +  imports Equivalence_Lebesgue_Henstock_Integration
    12.9  begin
   12.10  
   12.11  (*
   12.12 @@ -85,7 +85,7 @@
   12.13  lemma set_lebesgue_integral_cong:
   12.14    assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
   12.15    shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
   12.16 -  using assms by (auto intro!: integral_cong split: split_indicator simp add: sets.sets_into_space)
   12.17 +  using assms by (auto intro!: Bochner_Integration.integral_cong split: split_indicator simp add: sets.sets_into_space)
   12.18  
   12.19  lemma set_lebesgue_integral_cong_AE:
   12.20    assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   12.21 @@ -118,22 +118,22 @@
   12.22  (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
   12.23  
   12.24  lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
   12.25 -  by (subst integral_scaleR_right[symmetric]) (auto intro!: integral_cong)
   12.26 +  by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
   12.27  
   12.28  lemma set_integral_mult_right [simp]:
   12.29    fixes a :: "'a::{real_normed_field, second_countable_topology}"
   12.30    shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
   12.31 -  by (subst integral_mult_right_zero[symmetric]) (auto intro!: integral_cong)
   12.32 +  by (subst integral_mult_right_zero[symmetric]) auto
   12.33  
   12.34  lemma set_integral_mult_left [simp]:
   12.35    fixes a :: "'a::{real_normed_field, second_countable_topology}"
   12.36    shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
   12.37 -  by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong)
   12.38 +  by (subst integral_mult_left_zero[symmetric]) auto
   12.39  
   12.40  lemma set_integral_divide_zero [simp]:
   12.41    fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   12.42    shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
   12.43 -  by (subst integral_divide_zero[symmetric], intro integral_cong)
   12.44 +  by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
   12.45       (auto split: split_indicator)
   12.46  
   12.47  lemma set_integrable_scaleR_right [simp, intro]:
   12.48 @@ -184,7 +184,7 @@
   12.49    fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   12.50    shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
   12.51    by (subst lborel_integral_real_affine[where c="-1" and t=0])
   12.52 -     (auto intro!: integral_cong split: split_indicator)
   12.53 +     (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
   12.54  
   12.55  (* question: why do we have this for negation, but multiplication by a constant
   12.56     requires an integrability assumption? *)
   12.57 @@ -194,7 +194,7 @@
   12.58  lemma set_integral_complex_of_real:
   12.59    "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
   12.60    by (subst integral_complex_of_real[symmetric])
   12.61 -     (auto intro!: integral_cong split: split_indicator)
   12.62 +     (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
   12.63  
   12.64  lemma set_integral_mono:
   12.65    fixes f g :: "_ \<Rightarrow> real"
   12.66 @@ -254,7 +254,7 @@
   12.67  proof -
   12.68    have "set_integrable M (A - B) f"
   12.69      using f_A by (rule set_integrable_subset) auto
   12.70 -  from integrable_add[OF this f_B] show ?thesis
   12.71 +  from Bochner_Integration.integrable_add[OF this f_B] show ?thesis
   12.72      by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
   12.73  qed
   12.74  
   12.75 @@ -410,7 +410,7 @@
   12.76        by simp
   12.77    qed
   12.78    show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
   12.79 -    apply (rule integral_cong[OF refl])
   12.80 +    apply (rule Bochner_Integration.integral_cong[OF refl])
   12.81      apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
   12.82      using sums_unique[OF indicator_sums[OF disj]]
   12.83      apply auto
    13.1 --- a/src/HOL/Library/Inner_Product.thy	Thu Sep 15 22:41:05 2016 +0200
    13.2 +++ b/src/HOL/Library/Inner_Product.thy	Fri Sep 16 13:56:51 2016 +0200
    13.3 @@ -260,6 +260,11 @@
    13.4  
    13.5  end
    13.6  
    13.7 +lemma
    13.8 +  shows real_inner_1_left[simp]: "inner 1 x = x"
    13.9 +    and real_inner_1_right[simp]: "inner x 1 = x"
   13.10 +  by simp_all
   13.11 +
   13.12  instantiation complex :: real_inner
   13.13  begin
   13.14  
    14.1 --- a/src/HOL/Probability/Characteristic_Functions.thy	Thu Sep 15 22:41:05 2016 +0200
    14.2 +++ b/src/HOL/Probability/Characteristic_Functions.thy	Fri Sep 16 13:56:51 2016 +0200
    14.3 @@ -316,13 +316,13 @@
    14.4    then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
    14.5      by (simp add: integ_c)
    14.6    also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
    14.7 -    unfolding char_def by (subst integral_diff[OF integ_iexp]) (auto intro!: integ_c)
    14.8 +    unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c)
    14.9    also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
   14.10 -    by (intro integral_norm_bound integrable_diff integ_iexp integrable_setsum integ_c) simp
   14.11 +    by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
   14.12    also have "\<dots> \<le> expectation (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
   14.13    proof (rule integral_mono)
   14.14      show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
   14.15 -      by (intro integrable_norm integrable_diff integ_iexp integrable_setsum integ_c) simp
   14.16 +      by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
   14.17      show "integrable M (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
   14.18        unfolding power_abs[symmetric]
   14.19        by (intro integrable_mult_right integrable_abs integrable_moments) simp
   14.20 @@ -360,16 +360,16 @@
   14.21    then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
   14.22      by (simp add: integ_c)
   14.23    also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
   14.24 -    unfolding char_def by (subst integral_diff[OF integ_iexp]) (auto intro!: integ_c)
   14.25 +    unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c)
   14.26    also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
   14.27 -    by (intro integral_norm_bound integrable_diff integ_iexp integrable_setsum integ_c) simp
   14.28 +    by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
   14.29    also have "\<dots> \<le> expectation (\<lambda>x. min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^(Suc n) / fact (Suc n)))"
   14.30      (is "_ \<le> expectation ?f")
   14.31    proof (rule integral_mono)
   14.32      show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
   14.33 -      by (intro integrable_norm integrable_diff integ_iexp integrable_setsum integ_c) simp
   14.34 +      by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
   14.35      show "integrable M ?f"
   14.36 -      by (rule integrable_bound[where f="\<lambda>x. 2 * \<bar>t * x\<bar> ^ n / fact n"])
   14.37 +      by (rule Bochner_Integration.integrable_bound[where f="\<lambda>x. 2 * \<bar>t * x\<bar> ^ n / fact n"])
   14.38           (auto simp: integrable_moments power_abs[symmetric] power_mult_distrib)
   14.39      show "cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)) \<le> ?f x" for x
   14.40        using iexp_approx1[of "t * x" n] iexp_approx2[of "t * x" n]
   14.41 @@ -377,9 +377,9 @@
   14.42    qed
   14.43    also have "\<dots> = (\<bar>t\<bar>^n / fact (Suc n)) * expectation (\<lambda>x. min (2 * \<bar>x\<bar>^n * Suc n) (\<bar>t\<bar> * \<bar>x\<bar>^Suc n))"
   14.44      unfolding *
   14.45 -  proof (rule integral_mult_right)
   14.46 +  proof (rule Bochner_Integration.integral_mult_right)
   14.47      show "integrable M (\<lambda>x. min (2 * \<bar>x\<bar> ^ n * real (Suc n)) (\<bar>t\<bar> * \<bar>x\<bar> ^ Suc n))"
   14.48 -      by (rule integrable_bound[where f="\<lambda>x. 2 * \<bar>x\<bar> ^ n * real (Suc n)"])
   14.49 +      by (rule Bochner_Integration.integrable_bound[where f="\<lambda>x. 2 * \<bar>x\<bar> ^ n * real (Suc n)"])
   14.50           (auto simp: integrable_moments power_abs[symmetric] power_mult_distrib)
   14.51    qed
   14.52    finally show ?thesis
    15.1 --- a/src/HOL/Probability/Distributions.thy	Thu Sep 15 22:41:05 2016 +0200
    15.2 +++ b/src/HOL/Probability/Distributions.thy	Fri Sep 16 13:56:51 2016 +0200
    15.3 @@ -608,7 +608,7 @@
    15.4      using D by (rule entropy_distr) simp
    15.5    also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) =
    15.6      (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
    15.7 -    by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
    15.8 +    by (intro Bochner_Integration.integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
    15.9    also have "\<dots> = (ln l - 1) / ln b"
   15.10      by simp
   15.11    finally show ?thesis
   15.12 @@ -750,7 +750,7 @@
   15.13      uniform_distributed_bounds[of X a b]
   15.14      uniform_distributed_measure[of X a b]
   15.15      distributed_measurable[of M lborel X]
   15.16 -  by (auto intro!: uniform_distrI_borel_atLeastAtMost)
   15.17 +  by (auto intro!: uniform_distrI_borel_atLeastAtMost simp del: content_real_if)
   15.18  
   15.19  lemma (in prob_space) uniform_distributed_expectation:
   15.20    fixes a b :: real
   15.21 @@ -762,13 +762,13 @@
   15.22  
   15.23    have "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) =
   15.24      (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)"
   15.25 -    by (intro integral_cong) auto
   15.26 +    by (intro Bochner_Integration.integral_cong) auto
   15.27    also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2"
   15.28    proof (subst integral_FTC_Icc_real)
   15.29      fix x
   15.30      show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
   15.31        using uniform_distributed_params[OF D]
   15.32 -      by (auto intro!: derivative_eq_intros)
   15.33 +      by (auto intro!: derivative_eq_intros simp del: content_real_if)
   15.34      show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
   15.35        using uniform_distributed_params[OF D]
   15.36        by (auto intro!: isCont_divide)
   15.37 @@ -791,12 +791,12 @@
   15.38    have [arith]: "a < b" using uniform_distributed_bounds[OF D] .
   15.39    let ?\<mu> = "expectation X" let ?D = "\<lambda>x. indicator {a..b} (x + ?\<mu>) / measure lborel {a..b}"
   15.40    have "(\<integral>x. x\<^sup>2 * (?D x) \<partial>lborel) = (\<integral>x. x\<^sup>2 * (indicator {a - ?\<mu> .. b - ?\<mu>} x) / measure lborel {a .. b} \<partial>lborel)"
   15.41 -    by (intro integral_cong) (auto split: split_indicator)
   15.42 +    by (intro Bochner_Integration.integral_cong) (auto split: split_indicator)
   15.43    also have "\<dots> = (b - a)\<^sup>2 / 12"
   15.44      by (simp add: integral_power uniform_distributed_expectation[OF D])
   15.45         (simp add: eval_nat_numeral field_simps )
   15.46    finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" .
   15.47 -qed (auto intro: D simp: measure_nonneg)
   15.48 +qed (auto intro: D simp del: content_real_if)
   15.49  
   15.50  subsection \<open>Normal distribution\<close>
   15.51  
   15.52 @@ -949,7 +949,7 @@
   15.53      proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI)
   15.54        fix b :: real assume b: "0 \<le> b"
   15.55        have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) = (\<integral>x. indicator {0..b} x *\<^sub>R (exp (- x\<^sup>2) * ((Suc k) * x ^ k)) \<partial>lborel)"
   15.56 -        unfolding integral_mult_right_zero[symmetric] by (intro integral_cong) auto
   15.57 +        unfolding integral_mult_right_zero[symmetric] by (intro Bochner_Integration.integral_cong) auto
   15.58        also have "\<dots> = exp (- b\<^sup>2) * b ^ (Suc k) - exp (- 0\<^sup>2) * 0 ^ (Suc k) -
   15.59            (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel)"
   15.60          by (rule integral_by_parts')
   15.61 @@ -957,7 +957,7 @@
   15.62                   simp: diff_Suc of_nat_Suc field_simps split: nat.split)
   15.63        also have "(\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel) =
   15.64          (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)"
   15.65 -        by (intro integral_cong) auto
   15.66 +        by (intro Bochner_Integration.integral_cong) auto
   15.67        finally have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) =
   15.68          exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)"
   15.69          by (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric])
   15.70 @@ -1361,10 +1361,10 @@
   15.71    have "entropy b lborel X = - (\<integral> x. normal_density \<mu> \<sigma> x * log b (normal_density \<mu> \<sigma> x) \<partial>lborel)"
   15.72      using D by (rule entropy_distr) simp
   15.73    also have "\<dots> = - (\<integral> x. normal_density \<mu> \<sigma> x * (- ln (2 * pi * \<sigma>\<^sup>2) - (x - \<mu>)\<^sup>2 / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
   15.74 -    by (intro arg_cong[where f="uminus"] integral_cong)
   15.75 +    by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong)
   15.76         (auto simp: normal_density_def field_simps ln_mult log_def ln_div ln_sqrt)
   15.77    also have "\<dots> = - (\<integral>x. - (normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
   15.78 -    by (intro arg_cong[where f="uminus"] integral_cong) (auto simp: divide_simps field_simps)
   15.79 +    by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong) (auto simp: divide_simps field_simps)
   15.80    also have "\<dots> = (\<integral>x. normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2 \<partial>lborel) / (2 * ln b)"
   15.81      by (simp del: minus_add_distrib)
   15.82    also have "\<dots> = (ln (2 * pi * \<sigma>\<^sup>2) + 1) / (2 * ln b)"
    16.1 --- a/src/HOL/Probability/Giry_Monad.thy	Thu Sep 15 22:41:05 2016 +0200
    16.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Fri Sep 16 13:56:51 2016 +0200
    16.3 @@ -862,15 +862,15 @@
    16.4    show ?integrable
    16.5      using M * by(simp add: real_integrable_def measurable_def nn_integral_empty)
    16.6    have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)"
    16.7 -  proof(rule integral_cong)
    16.8 +  proof(rule Bochner_Integration.integral_cong)
    16.9      fix M'
   16.10      assume "M' \<in> space M"
   16.11      with sets_eq_imp_space_eq[OF M] have "space M' = space N"
   16.12        by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
   16.13 -    with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: integral_empty)
   16.14 +    with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: Bochner_Integration.integral_empty)
   16.15    qed simp
   16.16    then show ?integral
   16.17 -    using M * by(simp add: integral_empty)
   16.18 +    using M * by(simp add: Bochner_Integration.integral_empty)
   16.19  next
   16.20    assume *: "space N \<noteq> {}"
   16.21  
   16.22 @@ -1213,7 +1213,7 @@
   16.23    also have "\<dots> = \<integral> x. integral\<^sup>L (N x) f \<partial>M"
   16.24      by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _])
   16.25    finally show ?integral by(simp add: bind_nonempty''[where N=K])
   16.26 -qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite integral_empty)
   16.27 +qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite Bochner_Integration.integral_empty)
   16.28  
   16.29  lemma (in prob_space) prob_space_bind:
   16.30    assumes ae: "AE x in M. prob_space (N x)"
    17.1 --- a/src/HOL/Probability/Information.thy	Thu Sep 15 22:41:05 2016 +0200
    17.2 +++ b/src/HOL/Probability/Information.thy	Fri Sep 16 13:56:51 2016 +0200
    17.3 @@ -840,7 +840,7 @@
    17.4    also have "- log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX) = - log b (\<integral> x. 1 / Px x \<partial>distr M MX X)"
    17.5      unfolding distributed_distr_eq_density[OF X] using Px Px_nn
    17.6      apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
    17.7 -    by (subst integral_density) (auto simp del: integral_indicator intro!: integral_cong)
    17.8 +    by (subst integral_density) (auto simp del: integral_indicator intro!: Bochner_Integration.integral_cong)
    17.9    also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
   17.10    proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
   17.11      show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"
   17.12 @@ -901,11 +901,11 @@
   17.13    have eq: "(\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
   17.14      (\<integral> x. (- log b (measure MX A) / measure MX A) * indicator A x \<partial>MX)"
   17.15      using uniform_distributed_params[OF X]
   17.16 -    by (intro integral_cong) (auto split: split_indicator simp: log_divide_eq zero_less_measure_iff)
   17.17 +    by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: log_divide_eq zero_less_measure_iff)
   17.18    show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
   17.19      log b (measure MX A)"
   17.20      unfolding eq using uniform_distributed_params[OF X]
   17.21 -    by (subst integral_mult_right) (auto simp: measure_def less_top[symmetric] intro!: integrable_real_indicator)
   17.22 +    by (subst Bochner_Integration.integral_mult_right) (auto simp: measure_def less_top[symmetric] intro!: integrable_real_indicator)
   17.23  qed simp
   17.24  
   17.25  lemma (in information_space) entropy_simple_distributed:
   17.26 @@ -1038,8 +1038,8 @@
   17.27      apply (subst mi_eq)
   17.28      apply (subst mutual_information_distr[OF S TP Px Px_nn Pyz _ Pxyz])
   17.29      apply (auto simp: space_pair_measure)
   17.30 -    apply (subst integral_diff[symmetric])
   17.31 -    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
   17.32 +    apply (subst Bochner_Integration.integral_diff[symmetric])
   17.33 +    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: Bochner_Integration.integral_diff)
   17.34      done
   17.35  
   17.36    let ?P = "density (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) Pxyz"
   17.37 @@ -1112,7 +1112,7 @@
   17.38      done
   17.39  
   17.40    have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
   17.41 -    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integrable_diff[OF I1 I2]])
   17.42 +    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ Bochner_Integration.integrable_diff[OF I1 I2]])
   17.43      using ae
   17.44      apply (auto simp: split_beta')
   17.45      done
   17.46 @@ -1297,8 +1297,8 @@
   17.47      apply simp
   17.48      apply simp
   17.49      apply (simp add: space_pair_measure)
   17.50 -    apply (subst integral_diff[symmetric])
   17.51 -    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
   17.52 +    apply (subst Bochner_Integration.integral_diff[symmetric])
   17.53 +    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: Bochner_Integration.integral_diff)
   17.54      done
   17.55  
   17.56    let ?P = "density (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) Pxyz"
   17.57 @@ -1373,7 +1373,7 @@
   17.58         (auto simp: split_beta' AE_density space_pair_measure intro!: AE_I2 ennreal_neg)
   17.59  
   17.60    have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
   17.61 -    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integrable_diff[OF I1 I2]])
   17.62 +    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ Bochner_Integration.integrable_diff[OF I1 I2]])
   17.63      using ae
   17.64      apply (auto simp: split_beta')
   17.65      done
   17.66 @@ -1593,7 +1593,7 @@
   17.67    also have "\<dots> = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^sub>M T))"
   17.68      using b_gt_1
   17.69      by (subst distributed_transform_integral[OF Pxy _ Py, where T=snd])
   17.70 -       (auto intro!: integral_cong simp: space_pair_measure)
   17.71 +       (auto intro!: Bochner_Integration.integral_cong simp: space_pair_measure)
   17.72    finally have e_eq: "entropy b T Y = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^sub>M T))" .
   17.73  
   17.74    have **: "\<And>x. x \<in> space (S \<Otimes>\<^sub>M T) \<Longrightarrow> 0 \<le> Pxy x"
   17.75 @@ -1618,7 +1618,7 @@
   17.76      apply auto
   17.77      done
   17.78    also have "\<dots> = - (\<integral>x. Pxy x * log b (Pxy x) \<partial>(S \<Otimes>\<^sub>M T)) - - (\<integral>x.  Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^sub>M T))"
   17.79 -    by (simp add: integral_diff[OF I1 I2])
   17.80 +    by (simp add: Bochner_Integration.integral_diff[OF I1 I2])
   17.81    finally show ?thesis
   17.82      using conditional_entropy_generic_eq[OF S T Py Py_nn Pxy Pxy_nn, simplified]
   17.83        entropy_distr[OF Pxy **, simplified] e_eq
   17.84 @@ -1785,9 +1785,9 @@
   17.85  
   17.86    have "entropy b S X + entropy b T Y - entropy b (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) = integral\<^sup>L (S \<Otimes>\<^sub>M T) ?f"
   17.87      unfolding X Y XY
   17.88 -    apply (subst integral_diff)
   17.89 -    apply (intro integrable_diff Ixy Ix Iy)+
   17.90 -    apply (subst integral_diff)
   17.91 +    apply (subst Bochner_Integration.integral_diff)
   17.92 +    apply (intro Bochner_Integration.integrable_diff Ixy Ix Iy)+
   17.93 +    apply (subst Bochner_Integration.integral_diff)
   17.94      apply (intro Ixy Ix Iy)+
   17.95      apply (simp add: field_simps)
   17.96      done
    18.1 --- a/src/HOL/Probability/Levy.thy	Thu Sep 15 22:41:05 2016 +0200
    18.2 +++ b/src/HOL/Probability/Levy.thy	Fri Sep 16 13:56:51 2016 +0200
    18.3 @@ -136,9 +136,9 @@
    18.4      have "(CLBINT t=-T..T. ?F t * \<phi> t) =
    18.5        (CLBINT t. (CLINT x | M. ?F t * iexp (t * x) * indicator {-T<..<T} t))"
    18.6        using \<open>T \<ge> 0\<close> unfolding \<phi>_def char_def interval_lebesgue_integral_def
    18.7 -      by (auto split: split_indicator intro!: integral_cong)
    18.8 +      by (auto split: split_indicator intro!: Bochner_Integration.integral_cong)
    18.9      also have "\<dots> = (CLBINT t. (CLINT x | M. ?f' (t, x)))"
   18.10 -      by (auto intro!: integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
   18.11 +      by (auto intro!: Bochner_Integration.integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
   18.12      also have "\<dots> = (CLINT x | M. (CLBINT t. ?f' (t, x)))"
   18.13      proof (intro P.Fubini_integral [symmetric] integrableI_bounded_set [where B="b - a"])
   18.14        show "emeasure (lborel \<Otimes>\<^sub>M M) ({- T<..<T} \<times> space M) < \<infinity>"
   18.15 @@ -151,7 +151,7 @@
   18.16      qed (auto split: split_indicator split_indicator_asm)
   18.17      also have "\<dots> = (CLINT x | M. (complex_of_real (2 * (sgn (x - a) *
   18.18           Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))))"
   18.19 -       using main_eq by (intro integral_cong, auto)
   18.20 +       using main_eq by (intro Bochner_Integration.integral_cong, auto)
   18.21      also have "\<dots> = complex_of_real (LINT x | M. (2 * (sgn (x - a) *
   18.22           Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))"
   18.23         by (rule integral_complex_of_real)
   18.24 @@ -336,11 +336,11 @@
   18.25          (CLBINT t:{-u..u}. (CLINT x | M n. 1 - iexp (t * x)))"
   18.26        unfolding char_def by (rule set_lebesgue_integral_cong, auto simp del: of_real_mult)
   18.27      also have "\<dots> = (CLBINT t. (CLINT x | M n. indicator {-u..u} t *\<^sub>R (1 - iexp (t * x))))"
   18.28 -      by (rule integral_cong) (auto split: split_indicator)
   18.29 +      by (rule Bochner_Integration.integral_cong) (auto split: split_indicator)
   18.30      also have "\<dots> = (CLINT x | M n. (CLBINT t:{-u..u}. 1 - iexp (t * x)))"
   18.31        using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta')
   18.32      also have "\<dots> = (CLINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))"
   18.33 -      using \<open>u > 0\<close> by (intro integral_cong, auto simp add: * simp del: of_real_mult)
   18.34 +      using \<open>u > 0\<close> by (intro Bochner_Integration.integral_cong, auto simp add: * simp del: of_real_mult)
   18.35      also have "\<dots> = (LINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))"
   18.36        by (rule integral_complex_of_real)
   18.37      finally have "Re (CLBINT t:{-u..u}. 1 - char (M n) t) =
    19.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Sep 15 22:41:05 2016 +0200
    19.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Sep 16 13:56:51 2016 +0200
    19.3 @@ -167,7 +167,7 @@
    19.4  
    19.5  lemma pmf_nonneg[simp]: "0 \<le> pmf p x"
    19.6    by transfer simp
    19.7 -  
    19.8 +
    19.9  lemma pmf_not_neg [simp]: "\<not>pmf p x < 0"
   19.10    by (simp add: not_less pmf_nonneg)
   19.11  
   19.12 @@ -546,7 +546,7 @@
   19.13  
   19.14  lemma measure_return_pmf [simp]: "measure_pmf.prob (return_pmf x) A = indicator A x"
   19.15  proof -
   19.16 -  have "ennreal (measure_pmf.prob (return_pmf x) A) = 
   19.17 +  have "ennreal (measure_pmf.prob (return_pmf x) A) =
   19.18            emeasure (measure_pmf (return_pmf x)) A"
   19.19      by (simp add: measure_pmf.emeasure_eq_measure)
   19.20    also have "\<dots> = ennreal (indicator A x)" by (simp add: ennreal_indicator)
   19.21 @@ -778,10 +778,10 @@
   19.22    have "1 = measure (measure_pmf M) UNIV" by simp
   19.23    also have "\<dots> = measure (measure_pmf N) {x} + measure (measure_pmf N) (UNIV - {x})"
   19.24      by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
   19.25 -  also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}" 
   19.26 +  also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}"
   19.27      by (simp add: measure_pmf_single)
   19.28    also have "measure (measure_pmf N) (UNIV - {x}) \<le> measure (measure_pmf M) (UNIV - {x})"
   19.29 -    by (subst (1 2) integral_pmf [symmetric]) 
   19.30 +    by (subst (1 2) integral_pmf [symmetric])
   19.31         (intro integral_mono integrable_pmf, simp_all add: ge)
   19.32    also have "measure (measure_pmf M) {x} + \<dots> = 1"
   19.33      by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
   19.34 @@ -803,7 +803,7 @@
   19.35      by unfold_locales
   19.36  
   19.37    have "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>A)"
   19.38 -    by (rule integral_cong) (auto intro!: integral_pmf_restrict)
   19.39 +    by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict)
   19.40    also have "\<dots> = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>restrict_space A A)"
   19.41      by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
   19.42                countable_set_pmf borel_measurable_count_space)
   19.43 @@ -815,7 +815,7 @@
   19.44      by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
   19.45                countable_set_pmf borel_measurable_count_space)
   19.46    also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)"
   19.47 -    by (rule integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
   19.48 +    by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
   19.49    finally show "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)" .
   19.50  qed
   19.51  
   19.52 @@ -1629,7 +1629,7 @@
   19.53  
   19.54  lemma map_pmf_of_set:
   19.55    assumes "finite A" "A \<noteq> {}"
   19.56 -  shows   "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))" 
   19.57 +  shows   "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))"
   19.58      (is "?lhs = ?rhs")
   19.59  proof (intro pmf_eqI)
   19.60    fix x
   19.61 @@ -1641,13 +1641,13 @@
   19.62  
   19.63  lemma pmf_bind_pmf_of_set:
   19.64    assumes "A \<noteq> {}" "finite A"
   19.65 -  shows   "pmf (bind_pmf (pmf_of_set A) f) x = 
   19.66 +  shows   "pmf (bind_pmf (pmf_of_set A) f) x =
   19.67               (\<Sum>xa\<in>A. pmf (f xa) x) / real_of_nat (card A)" (is "?lhs = ?rhs")
   19.68  proof -
   19.69    from assms have "card A > 0" by auto
   19.70    with assms have "ennreal ?lhs = ennreal ?rhs"
   19.71 -    by (subst ennreal_pmf_bind) 
   19.72 -       (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric] 
   19.73 +    by (subst ennreal_pmf_bind)
   19.74 +       (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric]
   19.75          setsum_nonneg ennreal_of_nat_eq_real_of_nat)
   19.76    thus ?thesis by (subst (asm) ennreal_inj) (auto intro!: setsum_nonneg divide_nonneg_nonneg)
   19.77  qed
   19.78 @@ -1675,10 +1675,10 @@
   19.79  qed
   19.80  
   19.81  text \<open>
   19.82 -  Choosing an element uniformly at random from the union of a disjoint family 
   19.83 -  of finite non-empty sets with the same size is the same as first choosing a set 
   19.84 -  from the family uniformly at random and then choosing an element from the chosen set 
   19.85 -  uniformly at random.  
   19.86 +  Choosing an element uniformly at random from the union of a disjoint family
   19.87 +  of finite non-empty sets with the same size is the same as first choosing a set
   19.88 +  from the family uniformly at random and then choosing an element from the chosen set
   19.89 +  uniformly at random.
   19.90  \<close>
   19.91  lemma pmf_of_set_UN:
   19.92    assumes "finite (UNION A f)" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
   19.93 @@ -1694,8 +1694,8 @@
   19.94      by (subst pmf_of_set) auto
   19.95    also from assms have "card (\<Union>x\<in>A. f x) = card A * n"
   19.96      by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def)
   19.97 -  also from assms 
   19.98 -    have "indicator (\<Union>x\<in>A. f x) x / real \<dots> = 
   19.99 +  also from assms
  19.100 +    have "indicator (\<Union>x\<in>A. f x) x / real \<dots> =
  19.101                indicator (\<Union>x\<in>A. f x) x / (n * real (card A))"
  19.102        by (simp add: setsum_divide_distrib [symmetric] mult_ac)
  19.103    also from assms have "indicator (\<Union>x\<in>A. f x) x = (\<Sum>y\<in>A. indicator (f y) x)"
  19.104 @@ -1794,17 +1794,17 @@
  19.105  
  19.106  lemma replicate_pmf_1: "replicate_pmf 1 p = map_pmf (\<lambda>x. [x]) p"
  19.107    by (simp add: map_pmf_def bind_return_pmf)
  19.108 -  
  19.109 -lemma set_replicate_pmf: 
  19.110 +
  19.111 +lemma set_replicate_pmf:
  19.112    "set_pmf (replicate_pmf n p) = {xs\<in>lists (set_pmf p). length xs = n}"
  19.113    by (induction n) (auto simp: length_Suc_conv)
  19.114  
  19.115  lemma replicate_pmf_distrib:
  19.116 -  "replicate_pmf (m + n) p = 
  19.117 +  "replicate_pmf (m + n) p =
  19.118       do {xs \<leftarrow> replicate_pmf m p; ys \<leftarrow> replicate_pmf n p; return_pmf (xs @ ys)}"
  19.119    by (induction m) (simp_all add: bind_return_pmf bind_return_pmf' bind_assoc_pmf)
  19.120  
  19.121 -lemma power_diff': 
  19.122 +lemma power_diff':
  19.123    assumes "b \<le> a"
  19.124    shows   "x ^ (a - b) = (if x = 0 \<and> a = b then 1 else x ^ a / (x::'a::field) ^ b)"
  19.125  proof (cases "x = 0")
  19.126 @@ -1812,12 +1812,12 @@
  19.127    with assms show ?thesis by (cases "a - b") simp_all
  19.128  qed (insert assms, simp_all add: power_diff)
  19.129  
  19.130 -  
  19.131 +
  19.132  lemma binomial_pmf_Suc:
  19.133    assumes "p \<in> {0..1}"
  19.134 -  shows   "binomial_pmf (Suc n) p = 
  19.135 -             do {b \<leftarrow> bernoulli_pmf p; 
  19.136 -                 k \<leftarrow> binomial_pmf n p; 
  19.137 +  shows   "binomial_pmf (Suc n) p =
  19.138 +             do {b \<leftarrow> bernoulli_pmf p;
  19.139 +                 k \<leftarrow> binomial_pmf n p;
  19.140                   return_pmf ((if b then 1 else 0) + k)}" (is "_ = ?rhs")
  19.141  proof (intro pmf_eqI)
  19.142    fix k
  19.143 @@ -1835,14 +1835,14 @@
  19.144  lemma binomial_pmf_altdef:
  19.145    assumes "p \<in> {0..1}"
  19.146    shows   "binomial_pmf n p = map_pmf (length \<circ> filter id) (replicate_pmf n (bernoulli_pmf p))"
  19.147 -  by (induction n) 
  19.148 -     (insert assms, auto simp: binomial_pmf_Suc map_pmf_def bind_return_pmf bind_assoc_pmf 
  19.149 +  by (induction n)
  19.150 +     (insert assms, auto simp: binomial_pmf_Suc map_pmf_def bind_return_pmf bind_assoc_pmf
  19.151          bind_return_pmf' binomial_pmf_0 intro!: bind_pmf_cong)
  19.152  
  19.153  
  19.154  subsection \<open>PMFs from assiciation lists\<close>
  19.155  
  19.156 -definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where 
  19.157 +definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where
  19.158    "pmf_of_list xs = embed_pmf (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
  19.159  
  19.160  definition pmf_of_list_wf where
  19.161 @@ -1870,12 +1870,12 @@
  19.162      from Cons.prems have "snd x \<ge> 0" by simp
  19.163      moreover have "b \<ge> 0" if "(a,b) \<in> set xs" for a b
  19.164        using Cons.prems[of b] that by force
  19.165 -    ultimately have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>x # xs. indicator {x'} y * p) \<partial>count_space UNIV) = 
  19.166 -            (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) + 
  19.167 +    ultimately have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>x # xs. indicator {x'} y * p) \<partial>count_space UNIV) =
  19.168 +            (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) +
  19.169              ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
  19.170 -      by (intro nn_integral_cong, subst ennreal_plus [symmetric]) 
  19.171 +      by (intro nn_integral_cong, subst ennreal_plus [symmetric])
  19.172           (auto simp: case_prod_unfold indicator_def intro!: sum_list_nonneg)
  19.173 -    also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) + 
  19.174 +    also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) +
  19.175                        (\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
  19.176        by (intro nn_integral_add)
  19.177           (force intro!: sum_list_nonneg AE_I2 intro: Cons simp: indicator_def)+
  19.178 @@ -1934,20 +1934,20 @@
  19.179  proof -
  19.180    have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
  19.181      by simp
  19.182 -  also from assms 
  19.183 +  also from assms
  19.184      have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
  19.185      by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list)
  19.186 -  also from assms 
  19.187 +  also from assms
  19.188      have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
  19.189      by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
  19.190 -  also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. 
  19.191 +  also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
  19.192        indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
  19.193      using assms by (intro ennreal_cong setsum.cong) (auto simp: pmf_pmf_of_list)
  19.194    also have "?S = (\<Sum>x\<in>set_pmf (pmf_of_list xs). indicator A x * pmf (pmf_of_list xs) x)"
  19.195      using assms by (intro setsum.mono_neutral_left set_pmf_of_list finite_set_pmf_of_list) auto
  19.196    also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)"
  19.197      using assms by (intro setsum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq)
  19.198 -  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * 
  19.199 +  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x *
  19.200                        sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
  19.201      using assms by (simp add: pmf_pmf_of_list)
  19.202    also have "\<dots> = (\<Sum>x\<in>set (map fst xs). sum_list (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
  19.203 @@ -1955,17 +1955,17 @@
  19.204    also have "\<dots> = (\<Sum>x\<in>set (map fst xs). (\<Sum>xa = 0..<length xs.
  19.205                       if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
  19.206      by (intro setsum.cong refl, subst sum_list_map_filter', subst sum_list_setsum_nth) simp
  19.207 -  also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs). 
  19.208 +  also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
  19.209                       if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
  19.210      by (rule setsum.commute)
  19.211 -  also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then 
  19.212 +  also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
  19.213                       (\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
  19.214      by (auto intro!: setsum.cong setsum.neutral)
  19.215    also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
  19.216      by (intro setsum.cong refl) (simp_all add: setsum.delta)
  19.217    also have "\<dots> = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
  19.218      by (subst sum_list_map_filter', subst sum_list_setsum_nth) simp_all
  19.219 -  finally show ?thesis . 
  19.220 +  finally show ?thesis .
  19.221  qed
  19.222  
  19.223  lemma measure_pmf_of_list:
  19.224 @@ -1989,7 +1989,7 @@
  19.225    "sum_list (filter (\<lambda>x. x \<noteq> 0) xs) = sum_list xs"
  19.226    by (induction xs) simp_all
  19.227  (* END MOVE *)
  19.228 -  
  19.229 +
  19.230  lemma set_pmf_of_list_eq:
  19.231    assumes "pmf_of_list_wf xs" "\<And>x. x \<in> snd ` set xs \<Longrightarrow> x > 0"
  19.232    shows   "set_pmf (pmf_of_list xs) = fst ` set xs"
  19.233 @@ -2000,13 +2000,13 @@
  19.234      from B have "sum_list (map snd [z\<leftarrow>xs. fst z = x]) = 0"
  19.235        by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
  19.236      moreover from y have "y \<in> snd ` {xa \<in> set xs. fst xa = x}" by force
  19.237 -    ultimately have "y = 0" using assms(1) 
  19.238 +    ultimately have "y = 0" using assms(1)
  19.239        by (subst (asm) sum_list_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def)
  19.240      with assms(2) y have False by force
  19.241    }
  19.242    thus "fst ` set xs \<subseteq> set_pmf (pmf_of_list xs)" by blast
  19.243  qed (insert set_pmf_of_list[OF assms(1)], simp_all)
  19.244 -  
  19.245 +
  19.246  lemma pmf_of_list_remove_zeros:
  19.247    assumes "pmf_of_list_wf xs"
  19.248    defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"
    20.1 --- a/src/HOL/Probability/Probability_Measure.thy	Thu Sep 15 22:41:05 2016 +0200
    20.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Fri Sep 16 13:56:51 2016 +0200
    20.3 @@ -225,7 +225,7 @@
    20.4        using prob_space by (simp add: X)
    20.5      also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
    20.6        using \<open>x \<in> I\<close> \<open>open I\<close> X(2)
    20.7 -      apply (intro integral_mono_AE integrable_add integrable_mult_right integrable_diff
    20.8 +      apply (intro integral_mono_AE Bochner_Integration.integrable_add Bochner_Integration.integrable_mult_right Bochner_Integration.integrable_diff
    20.9                  integrable_const X q)
   20.10        apply (elim eventually_mono)
   20.11        apply (intro convex_le_Inf_differential)
    21.1 --- a/src/HOL/Probability/SPMF.thy	Thu Sep 15 22:41:05 2016 +0200
    21.2 +++ b/src/HOL/Probability/SPMF.thy	Fri Sep 16 13:56:51 2016 +0200
    21.3 @@ -554,11 +554,11 @@
    21.4    have "?lhs = \<integral> x. ?f x \<partial>measure_pmf p"
    21.5      by(simp add: bind_spmf_def pmf_bind)
    21.6    also have "\<dots> = \<integral> x. ?f None * indicator {None} x + ?f x * indicator (range Some) x \<partial>measure_pmf p"
    21.7 -    by(rule integral_cong)(auto simp add: indicator_def)
    21.8 +    by(rule Bochner_Integration.integral_cong)(auto simp add: indicator_def)
    21.9    also have "\<dots> = (\<integral> x. ?f None * indicator {None} x \<partial>measure_pmf p) + (\<integral> x. ?f x * indicator (range Some) x \<partial>measure_pmf p)"
   21.10 -    by(rule integral_add)(auto 4 3 intro: integrable_real_mult_indicator measure_pmf.integrable_const_bound[where B=1] simp add: AE_measure_pmf_iff pmf_le_1)
   21.11 +    by(rule Bochner_Integration.integral_add)(auto 4 3 intro: integrable_real_mult_indicator measure_pmf.integrable_const_bound[where B=1] simp add: AE_measure_pmf_iff pmf_le_1)
   21.12    also have "\<dots> = pmf p None + \<integral> x. indicator (range Some) x * pmf (f (the x)) None \<partial>measure_pmf p"
   21.13 -    by(auto simp add: measure_measure_pmf_finite indicator_eq_0_iff intro!: integral_cong)
   21.14 +    by(auto simp add: measure_measure_pmf_finite indicator_eq_0_iff intro!: Bochner_Integration.integral_cong)
   21.15    also have "\<dots> = ?rhs" unfolding measure_spmf_def
   21.16      by(subst integral_distr)(auto simp add: integral_restrict_space)
   21.17    finally show ?thesis .
   21.18 @@ -566,7 +566,7 @@
   21.19  
   21.20  lemma spmf_bind: "spmf (p \<bind> f) y = \<integral> x. spmf (f x) y \<partial>measure_spmf p"
   21.21  unfolding measure_spmf_def
   21.22 -by(subst integral_distr)(auto simp add: bind_spmf_def pmf_bind integral_restrict_space indicator_eq_0_iff intro!: integral_cong split: option.split)
   21.23 +by(subst integral_distr)(auto simp add: bind_spmf_def pmf_bind integral_restrict_space indicator_eq_0_iff intro!: Bochner_Integration.integral_cong split: option.split)
   21.24  
   21.25  lemma ennreal_spmf_bind: "ennreal (spmf (p \<bind> f) x) = \<integral>\<^sup>+ y. spmf (f y) x \<partial>measure_spmf p"
   21.26  by(auto simp add: bind_spmf_def ennreal_pmf_bind nn_integral_measure_spmf_conv_measure_pmf nn_integral_restrict_space intro: nn_integral_cong split: split_indicator option.split)
   21.27 @@ -2688,7 +2688,7 @@
   21.28  lemma pmf_try_spmf_None [simp]: "pmf (TRY p ELSE q) None = pmf p None * pmf q None" (is "?lhs = ?rhs")
   21.29  proof -
   21.30    have "?lhs = \<integral> x. pmf q None * indicator {None} x \<partial>measure_pmf p"
   21.31 -    unfolding try_spmf_def pmf_bind by(rule integral_cong)(simp_all split: option.split)
   21.32 +    unfolding try_spmf_def pmf_bind by(rule Bochner_Integration.integral_cong)(simp_all split: option.split)
   21.33    also have "\<dots> = ?rhs" by(simp add: measure_pmf_single)
   21.34    finally show ?thesis .
   21.35  qed
    22.1 --- a/src/HOL/Probability/Sinc_Integral.thy	Thu Sep 15 22:41:05 2016 +0200
    22.2 +++ b/src/HOL/Probability/Sinc_Integral.thy	Fri Sep 16 13:56:51 2016 +0200
    22.3 @@ -263,7 +263,7 @@
    22.4    from lborel_integrable_real_affine[OF this, of t 0]
    22.5    show ?thesis
    22.6      unfolding interval_lebesgue_integral_0_infty
    22.7 -    by (rule integrable_bound) (auto simp: field_simps * split: split_indicator)
    22.8 +    by (rule Bochner_Integration.integrable_bound) (auto simp: field_simps * split: split_indicator)
    22.9  qed
   22.10  
   22.11  lemma Si_at_top: "(Si \<longlongrightarrow> pi / 2) at_top"
   22.12 @@ -291,7 +291,7 @@
   22.13          fix x :: real assume x: "x \<noteq> 0" "x \<noteq> t"
   22.14          have "LBINT y. \<bar>indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))\<bar> =
   22.15              LBINT y. \<bar>sin x\<bar> * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x"
   22.16 -          by (intro integral_cong) (auto split: split_indicator simp: abs_mult)
   22.17 +          by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult)
   22.18          also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>.  exp (- (y * x)))"
   22.19            by (cases "x > 0")
   22.20               (auto simp: field_simps interval_lebesgue_integral_0_infty split: split_indicator)
   22.21 @@ -315,7 +315,7 @@
   22.22      also have "... = LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x)"
   22.23        using \<open>0\<le>t\<close>
   22.24        by (auto simp: interval_lebesgue_integral_def zero_ereal_def ac_simps
   22.25 -               split: split_indicator intro!: integral_cong)
   22.26 +               split: split_indicator intro!: Bochner_Integration.integral_cong)
   22.27      also have "\<dots> = LBINT u=0..\<infinity>. 1 / (1 + u\<^sup>2) - 1 / (1 + u\<^sup>2) * (exp (- (u * t)) * (u * sin t + cos t))"
   22.28        by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong)
   22.29      also have "... = pi / 2 - (LBINT u=0..\<infinity>. exp (- (u * t)) * (u * sin t + cos t) / (1 + u^2))"