author hoelzl Fri Sep 16 13:56:51 2016 +0200 (2016-09-16) changeset 63886 685fb01256af 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
```     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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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))"
```