author paulson Sun Apr 15 13:57:00 2018 +0100 (2018-04-15) changeset 67982 7643b005b29a parent 67981 349c639e593c child 67983 487685540a51 child 67984 adc1a992c470
various new results on measures, integrals, etc., and some simplified proofs
```     1.1 --- a/src/HOL/Analysis/Ball_Volume.thy	Sat Apr 14 20:19:52 2018 +0100
1.2 +++ b/src/HOL/Analysis/Ball_Volume.thy	Sun Apr 15 13:57:00 2018 +0100
1.3 @@ -1,10 +1,10 @@
1.4  (*
1.5     File:     HOL/Analysis/Gamma_Function.thy
1.6     Author:   Manuel Eberl, TU München
1.7 +*)
1.8
1.9 -   The volume (Lebesgue measure) of an n-dimensional ball.
1.10 -*)
1.11 -section \<open>The volume of an \$n\$-ball\<close>
1.12 +section \<open>The volume (Lebesgue measure) of an \$n\$-dimensional ball\<close>
1.13 +
1.14  theory Ball_Volume
1.15    imports Gamma_Function Lebesgue_Integral_Substitution
1.16  begin
1.17 @@ -301,4 +301,30 @@
1.18  corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
1.19    by (simp add: content_ball unit_ball_vol_3)
1.20
1.21 +text \<open>
1.22 +  Useful equivalent forms
1.23 +\<close>
1.24 +corollary content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.25 +proof -
1.26 +  have "r > 0 \<Longrightarrow> content (ball c r) > 0"
1.27 +    by (simp add: content_ball unit_ball_vol_def)
1.28 +  then show ?thesis
1.29 +    by (fastforce simp: ball_empty)
1.30 +qed
1.31 +
1.32 +corollary content_ball_gt_0_iff [simp]: "0 < content (ball z r) \<longleftrightarrow> 0 < r"
1.33 +  by (auto simp: zero_less_measure_iff)
1.34 +
1.35 +corollary content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \<longleftrightarrow> r \<le> 0"
1.36 +proof (cases "r = 0")
1.37 +  case False
1.38 +  moreover have "r > 0 \<Longrightarrow> content (cball c r) > 0"
1.39 +    by (simp add: content_cball unit_ball_vol_def)
1.40 +  ultimately show ?thesis
1.41 +    by fastforce
1.42 +qed auto
1.43 +
1.44 +corollary content_cball_gt_0_iff [simp]: "0 < content (cball z r) \<longleftrightarrow> 0 < r"
1.45 +  by (auto simp: zero_less_measure_iff)
1.46 +
1.47  end
```
```     2.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sat Apr 14 20:19:52 2018 +0100
2.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Apr 15 13:57:00 2018 +0100
2.3 @@ -4,6 +4,16 @@
2.4  imports Finite_Cartesian_Product Derivative
2.5  begin
2.6
2.7 +lemma norm_le_componentwise:
2.8 +   "(\<And>b. b \<in> Basis \<Longrightarrow> abs(x \<bullet> b) \<le> abs(y \<bullet> b)) \<Longrightarrow> norm x \<le> norm y"
2.9 +  by (auto simp: norm_le euclidean_inner [of x x] euclidean_inner [of y y] abs_le_square_iff power2_eq_square intro!: sum_mono)
2.10 +
2.11 +lemma norm_le_componentwise_cart:
2.12 +  fixes x :: "real^'n"
2.13 +  shows "(\<And>i. abs(x\$i) \<le> abs(y\$i)) \<Longrightarrow> norm x \<le> norm y"
2.14 +  unfolding cart_eq_inner_axis
2.15 +  by (rule norm_le_componentwise) (metis axis_index)
2.16 +
2.17  lemma subspace_special_hyperplane: "subspace {x. x \$ k = 0}"
2.19
2.20 @@ -759,7 +769,7 @@
2.21    have "norm (\<chi> j. A \$ j \$ i) \<le> norm (A *v axis i 1)"
2.22      by (simp add: matrix_mult_dot cart_eq_inner_axis)
2.23    also have "\<dots> \<le> onorm (( *v) A)"
2.24 -    using onorm [OF bl, of "axis i 1"] by (auto simp: axis_in_Basis)
2.25 +    using onorm [OF bl, of "axis i 1"] by auto
2.26    finally have "norm (\<chi> j. A \$ j \$ i) \<le> onorm (( *v) A)" .
2.27    then show ?thesis
2.28      unfolding column_def .
```
```     3.1 --- a/src/HOL/Analysis/Complete_Measure.thy	Sat Apr 14 20:19:52 2018 +0100
3.2 +++ b/src/HOL/Analysis/Complete_Measure.thy	Sun Apr 15 13:57:00 2018 +0100
3.3 @@ -114,6 +114,11 @@
3.4    qed auto
3.5  qed
3.6
3.7 +lemma sets_restrict_space_subset:
3.8 +  assumes S: "S \<in> sets (completion M)"
3.9 +  shows "sets (restrict_space (completion M) S) \<subseteq> sets (completion M)"
3.10 +  by (metis assms sets.Int_space_eq2 sets_restrict_space_iff subsetI)
3.11 +
3.12  lemma
3.13    assumes "S \<in> sets (completion M)"
3.14    shows main_part_sets[intro, simp]: "main_part M S \<in> sets M"
3.15 @@ -989,6 +994,23 @@
3.16    finally show ?thesis .
3.17  qed
3.18
3.19 +lemma (in complete_measure) fmeasurable_measure_inner_outer_le:
3.20 +     "(S \<in> fmeasurable M \<and> m = measure M S) \<longleftrightarrow>
3.21 +        (\<forall>e>0. \<exists>T\<in>fmeasurable M. T \<subseteq> S \<and> m - e \<le> measure M T) \<and>
3.22 +        (\<forall>e>0. \<exists>U\<in>fmeasurable M. S \<subseteq> U \<and> measure M U \<le> m + e)" (is ?T1)
3.23 +  and null_sets_outer_le:
3.24 +     "S \<in> null_sets M \<longleftrightarrow> (\<forall>e>0. \<exists>T\<in>fmeasurable M. S \<subseteq> T \<and> measure M T \<le> e)" (is ?T2)
3.25 +proof -
3.26 +  have "e > 0 \<and> m - e/2 \<le> t \<Longrightarrow> m - e < t"
3.27 +       "e > 0 \<and> t \<le> m + e/2 \<Longrightarrow> t < m + e"
3.28 +       "e > 0 \<longleftrightarrow> e/2 > 0"
3.29 +       for e t
3.30 +    by auto
3.31 +  then show ?T1 ?T2
3.32 +    unfolding fmeasurable_measure_inner_outer null_sets_outer
3.33 +    by (meson dense le_less_trans less_imp_le)+
3.34 +qed
3.35 +
3.36  lemma (in cld_measure) notin_sets_outer_measure_of_cover:
3.37    assumes E: "E \<subseteq> space M" "E \<notin> sets M"
3.38    shows "\<exists>B\<in>sets M. 0 < emeasure M B \<and> emeasure M B < \<infinity> \<and>
```
```     4.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sat Apr 14 20:19:52 2018 +0100
4.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Apr 15 13:57:00 2018 +0100
4.3 @@ -6992,7 +6992,7 @@
4.4      done
4.5  qed
4.6
4.7 -subsubsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
4.8 +subsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
4.9
4.10  lemma image_stretch_interval:
4.11    "(\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k)) *\<^sub>R k) ` cbox a (b::'a::euclidean_space) =
```
```     5.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Apr 14 20:19:52 2018 +0100
5.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Apr 15 13:57:00 2018 +0100
5.3 @@ -945,7 +945,18 @@
5.4        by (auto simp: integrable_on_def nn_integral_completion)
5.5    qed
5.6  qed
5.7 -
5.8 +
5.9 +lemma integrable_on_lebesgue_on:
5.10 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
5.11 +  assumes f: "integrable (lebesgue_on S) f" and S: "S \<in> sets lebesgue"
5.12 +  shows "f integrable_on S"
5.13 +proof -
5.14 +  have "integrable lebesgue (\<lambda>x. indicator S x *\<^sub>R f x)"
5.15 +    using S f inf_top.comm_neutral integrable_restrict_space by blast
5.16 +  then show ?thesis
5.17 +    using absolutely_integrable_on_def set_integrable_def by blast
5.18 +qed
5.19 +
5.20  lemma absolutely_integrable_on_null [intro]:
5.21    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
5.22    shows "content (cbox a b) = 0 \<Longrightarrow> f absolutely_integrable_on (cbox a b)"
5.23 @@ -1051,6 +1062,39 @@
5.24  lemma lmeasure_integral: "S \<in> lmeasurable \<Longrightarrow> measure lebesgue S = integral S (\<lambda>x. 1::real)"
5.25    by (fastforce simp add: lmeasure_integral_UNIV indicator_def[abs_def] lmeasurable_iff_integrable_on)
5.26
5.27 +lemma integrable_on_const: "S \<in> lmeasurable \<Longrightarrow> (\<lambda>x. c) integrable_on S"
5.28 +  unfolding lmeasurable_iff_integrable
5.29 +  by (metis (mono_tags, lifting) integrable_eq integrable_on_scaleR_left lmeasurable_iff_integrable lmeasurable_iff_integrable_on scaleR_one)
5.30 +
5.31 +lemma integral_indicator:
5.32 +  assumes "(S \<inter> T) \<in> lmeasurable"
5.33 +  shows "integral T (indicator S) = measure lebesgue (S \<inter> T)"
5.34 +proof -
5.35 +  have "integral UNIV (indicator (S \<inter> T)) = integral UNIV (\<lambda>a. if a \<in> S \<inter> T then 1::real else 0)"
5.36 +    by (meson indicator_def)
5.37 +  moreover
5.38 +  have "(indicator (S \<inter> T) has_integral measure lebesgue (S \<inter> T)) UNIV"
5.39 +    using assms by (simp add: lmeasurable_iff_has_integral)
5.40 +  ultimately have "integral UNIV (\<lambda>x. if x \<in> S \<inter> T then 1 else 0) = measure lebesgue (S \<inter> T)"
5.41 +    by (metis (no_types) integral_unique)
5.42 +  then show ?thesis
5.43 +    using integral_restrict_Int [of UNIV "S \<inter> T" "\<lambda>x. 1::real"]
5.44 +    apply (simp add: integral_restrict_Int [symmetric])
5.45 +    by (meson indicator_def)
5.46 +qed
5.47 +
5.48 +lemma measurable_integrable:
5.49 +  fixes S :: "'a::euclidean_space set"
5.50 +  shows "S \<in> lmeasurable \<longleftrightarrow> (indicat_real S) integrable_on UNIV"
5.51 +  by (auto simp: lmeasurable_iff_integrable absolutely_integrable_on_iff_nonneg [symmetric] set_integrable_def)
5.52 +
5.53 +lemma integrable_on_indicator:
5.54 +  fixes S :: "'a::euclidean_space set"
5.55 +  shows "indicat_real S integrable_on T \<longleftrightarrow> (S \<inter> T) \<in> lmeasurable"
5.56 +  unfolding measurable_integrable
5.57 +  unfolding integrable_restrict_UNIV [of T, symmetric]
5.58 +  by (fastforce simp add: indicator_def elim: integrable_eq)
5.59 +
5.60  lemma
5.61    assumes \<D>: "\<D> division_of S"
5.62    shows lmeasurable_division: "S \<in> lmeasurable" (is ?l)
5.63 @@ -1072,7 +1116,6 @@
5.64      by (auto intro!: measure_Union_AE[symmetric] simp: completion.AE_iff_null_sets Int_def[symmetric] pairwise_def null_sets_def)
5.65  qed
5.66
5.67 -text \<open>This should be an abbreviation for negligible.\<close>
5.68  lemma negligible_iff_null_sets: "negligible S \<longleftrightarrow> S \<in> null_sets lebesgue"
5.69  proof
5.70    assume "negligible S"
5.71 @@ -2208,6 +2251,12 @@
5.72      using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
5.73  qed (use le in \<open>force intro!: always_eventually split: split_indicator\<close>)
5.74
5.75 +lemma absolutely_integrable_continuous:
5.76 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
5.77 +  shows "continuous_on (cbox a b) f \<Longrightarrow> f absolutely_integrable_on cbox a b"
5.78 +  using absolutely_integrable_integrable_bound
5.79 +  by (simp add: absolutely_integrable_on_def continuous_on_norm integrable_continuous)
5.80 +
5.81  subsection \<open>Componentwise\<close>
5.82
5.83  proposition absolutely_integrable_componentwise_iff:
```
```     6.1 --- a/src/HOL/Analysis/Fashoda_Theorem.thy	Sat Apr 14 20:19:52 2018 +0100
6.2 +++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Sun Apr 15 13:57:00 2018 +0100
6.3 @@ -269,15 +269,10 @@
6.4        by auto
6.5      moreover
6.6      from x1 have "g (x \$ 2) \<in> cbox (-1) 1"
6.7 -      apply -
6.8 -      apply (rule assms(2)[unfolded subset_eq,rule_format])
6.9 -      apply auto
6.10 -      done
6.11 +      using assms(2) by blast
6.12      ultimately show False
6.13        unfolding lem3[OF nz] vector_component_simps * mem_box_cart
6.14 -      apply (erule_tac x=1 in allE)
6.15 -      apply auto
6.16 -      done
6.17 +      using not_le by auto
6.18    next
6.19      assume as: "x\$1 = -1"
6.20      then have *: "f (x \$ 1) \$ 1 = - 1"
6.21 @@ -288,15 +283,10 @@
6.22        by auto
6.23      moreover
6.24      from x1 have "g (x \$ 2) \<in> cbox (-1) 1"
6.25 -      apply -
6.26 -      apply (rule assms(2)[unfolded subset_eq,rule_format])
6.27 -      apply auto
6.28 -      done
6.29 +      using assms(2) by blast
6.30      ultimately show False
6.31        unfolding lem3[OF nz] vector_component_simps * mem_box_cart
6.32 -      apply (erule_tac x=1 in allE)
6.33 -      apply auto
6.34 -      done
6.35 +      using not_le by auto
6.36    next
6.37      assume as: "x\$2 = 1"
6.38      then have *: "g (x \$ 2) \$ 2 = 1"
6.39 @@ -527,7 +517,7 @@
6.40        and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 \$ 2 = -1"
6.41        and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 \$ 2 = 1"
6.42        using assms as
6.43 -      by (simp_all add: axis_in_Basis cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
6.44 +      by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
6.46    qed
6.47    from z(1) obtain zf where zf:
```
```     7.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sat Apr 14 20:19:52 2018 +0100
7.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Apr 15 13:57:00 2018 +0100
7.3 @@ -607,20 +607,8 @@
7.4    apply (rule sum.neutral, simp add: axis_def)
7.5    done
7.6
7.7 -lemma sum_single:
7.8 -  assumes "finite A" and "k \<in> A" and "f k = y"
7.9 -  assumes "\<And>i. i \<in> A \<Longrightarrow> i \<noteq> k \<Longrightarrow> f i = 0"
7.10 -  shows "(\<Sum>i\<in>A. f i) = y"
7.11 -  apply (subst sum.remove [OF assms(1,2)])
7.12 -  apply (simp add: sum.neutral assms(3,4))
7.13 -  done
7.14 -
7.15  lemma inner_axis: "inner x (axis i y) = inner (x \$ i) y"
7.16 -  unfolding inner_vec_def
7.17 -  apply (rule_tac k=i in sum_single)
7.18 -  apply simp_all
7.19 -  apply (simp add: axis_def)
7.20 -  done
7.21 +  by (simp add: inner_vec_def axis_def sum.remove [where x=i])
7.22
7.23  lemma inner_axis': "inner(axis i y) x = inner y (x \$ i)"
7.24    by (simp add: inner_axis inner_commute)
7.25 @@ -649,22 +637,51 @@
7.26      by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
7.27  qed
7.28
7.29 -lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
7.30 -  apply (simp add: Basis_vec_def)
7.31 -  apply (subst card_UN_disjoint)
7.32 -     apply simp
7.33 -    apply simp
7.34 -   apply (auto simp: axis_eq_axis) [1]
7.35 -  apply (subst card_UN_disjoint)
7.36 -     apply (auto simp: axis_eq_axis)
7.37 -  done
7.38 +lemma DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
7.39 +proof -
7.40 +  have "card (\<Union>i::'b. \<Union>u::'a\<in>Basis. {axis i u}) = (\<Sum>i::'b\<in>UNIV. card (\<Union>u::'a\<in>Basis. {axis i u}))"
7.41 +    by (rule card_UN_disjoint) (auto simp: axis_eq_axis)
7.42 +  also have "... = CARD('b) * DIM('a)"
7.43 +    by (subst card_UN_disjoint) (auto simp: axis_eq_axis)
7.44 +  finally show ?thesis
7.45 +    by (simp add: Basis_vec_def)
7.46 +qed
7.47
7.48  end
7.49
7.50  lemma cart_eq_inner_axis: "a \$ i = inner a (axis i 1)"
7.52
7.53 -lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
7.54 -  by (auto simp add: Basis_vec_def axis_eq_axis)
7.55 +lemma axis_eq_0_iff [simp]:
7.56 +  shows "axis m x = 0 \<longleftrightarrow> x = 0"
7.57 +  by (simp add: axis_def vec_eq_iff)
7.58 +
7.59 +lemma axis_in_Basis_iff [simp]: "axis i a \<in> Basis \<longleftrightarrow> a \<in> Basis"
7.60 +  by (auto simp: Basis_vec_def axis_eq_axis)
7.61 +
7.62 +text\<open>Mapping each basis element to the corresponding finite index\<close>
7.63 +definition axis_index :: "('a::comm_ring_1)^'n \<Rightarrow> 'n" where "axis_index v \<equiv> SOME i. v = axis i 1"
7.64 +
7.65 +lemma axis_inverse:
7.66 +  fixes v :: "real^'n"
7.67 +  assumes "v \<in> Basis"
7.68 +  shows "\<exists>i. v = axis i 1"
7.69 +proof -
7.70 +  have "v \<in> (\<Union>n. \<Union>r\<in>Basis. {axis n r})"
7.71 +    using assms Basis_vec_def by blast
7.72 +  then show ?thesis
7.73 +    by (force simp add: vec_eq_iff)
7.74 +qed
7.75 +
7.76 +lemma axis_index:
7.77 +  fixes v :: "real^'n"
7.78 +  assumes "v \<in> Basis"
7.79 +  shows "v = axis (axis_index v) 1"
7.80 +  by (metis (mono_tags) assms axis_inverse axis_index_def someI_ex)
7.81 +
7.82 +lemma axis_index_axis [simp]:
7.83 +  fixes UU :: "real^'n"
7.84 +  shows "(axis_index (axis u 1 :: real^'n)) = (u::'n)"
7.85 +  by (simp add: axis_eq_axis axis_index_def)
7.86
7.87  end
```
```     8.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Apr 14 20:19:52 2018 +0100
8.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Apr 15 13:57:00 2018 +0100
8.3 @@ -3501,6 +3501,44 @@
8.4    using assms unfolding integrable_on_def
8.5    by (force dest: has_integral_stretch)
8.6
8.7 +lemma vec_lambda_eq_sum:
8.8 +  shows "(\<chi> k. f k (x \$ k)) = (\<Sum>k\<in>Basis. (f (axis_index k) (x \<bullet> k)) *\<^sub>R k)"
8.9 +    apply (simp add: Basis_vec_def cart_eq_inner_axis UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def)
8.10 +    apply (simp add: vec_eq_iff axis_def if_distrib cong: if_cong)
8.11 +    done
8.12 +
8.13 +lemma has_integral_stretch_cart:
8.14 +  fixes m :: "'n::finite \<Rightarrow> real"
8.15 +  assumes f: "(f has_integral i) (cbox a b)" and m: "\<And>k. m k \<noteq> 0"
8.16 +  shows "((\<lambda>x. f(\<chi> k. m k * x\$k)) has_integral i /\<^sub>R \<bar>prod m UNIV\<bar>)
8.17 +            ((\<lambda>x. \<chi> k. x\$k / m k) ` (cbox a b))"
8.18 +proof -
8.19 +  have *: "\<forall>k:: real^'n \<in> Basis. m (axis_index k) \<noteq> 0"
8.20 +    using axis_index by (simp add: m)
8.21 +  have eqp: "(\<Prod>k:: real^'n \<in> Basis. m (axis_index k)) = prod m UNIV"
8.22 +    by (simp add: Basis_vec_def UNION_singleton_eq_range prod.reindex axis_eq_axis inj_on_def)
8.23 +  show ?thesis
8.24 +    using has_integral_stretch [OF f *] vec_lambda_eq_sum [where f="\<lambda>i x. m i * x"] vec_lambda_eq_sum [where f="\<lambda>i x. x / m i"]
8.25 +    by (simp add: field_simps eqp)
8.26 +qed
8.27 +
8.28 +lemma image_stretch_interval_cart:
8.29 +  fixes m :: "'n::finite \<Rightarrow> real"
8.30 +  shows "(\<lambda>x. \<chi> k. m k * x\$k) ` cbox a b =
8.31 +            (if cbox a b = {} then {}
8.32 +            else cbox (\<chi> k. min (m k * a\$k) (m k * b\$k)) (\<chi> k. max (m k * a\$k) (m k * b\$k)))"
8.33 +proof -
8.34 +  have *: "(\<Sum>k\<in>Basis. min (m (axis_index k) * (a \<bullet> k)) (m (axis_index k) * (b \<bullet> k)) *\<^sub>R k)
8.35 +           = (\<chi> k. min (m k * a \$ k) (m k * b \$ k))"
8.36 +          "(\<Sum>k\<in>Basis. max (m (axis_index k) * (a \<bullet> k)) (m (axis_index k) * (b \<bullet> k)) *\<^sub>R k)
8.37 +           = (\<chi> k. max (m k * a \$ k) (m k * b \$ k))"
8.38 +    apply (simp_all add: Basis_vec_def cart_eq_inner_axis UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def)
8.39 +    apply (simp_all add: vec_eq_iff axis_def if_distrib cong: if_cong)
8.40 +    done
8.41 +  show ?thesis
8.42 +    by (simp add: vec_lambda_eq_sum [where f="\<lambda>i x. m i * x"] image_stretch_interval eq_cbox *)
8.43 +qed
8.44 +
8.45
8.46  subsection \<open>even more special cases\<close>
8.47
```
```     9.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sat Apr 14 20:19:52 2018 +0100
9.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Apr 15 13:57:00 2018 +0100
9.3 @@ -393,6 +393,23 @@
9.4  lemma Compl_in_sets_lebesgue: "-A \<in> sets lebesgue \<longleftrightarrow> A  \<in> sets lebesgue"
9.5    by (metis Compl_eq_Diff_UNIV double_compl space_borel space_completion space_lborel Sigma_Algebra.sets.compl_sets)
9.6
9.7 +lemma measurable_lebesgue_cong:
9.8 +  assumes "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
9.9 +  shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
9.10 +  by (metis (mono_tags, lifting) IntD1 assms measurable_cong_strong space_restrict_space)
9.11 +
9.12 +text\<open>Measurability of continuous functions\<close>
9.13 +lemma continuous_imp_measurable_on_sets_lebesgue:
9.14 +  assumes f: "continuous_on S f" and S: "S \<in> sets lebesgue"
9.15 +  shows "f \<in> borel_measurable (lebesgue_on S)"
9.16 +proof -
9.17 +  have "sets (restrict_space borel S) \<subseteq> sets (lebesgue_on S)"
9.18 +    by (simp add: mono_restrict_space subsetI)
9.19 +  then show ?thesis
9.20 +    by (simp add: borel_measurable_continuous_on_restrict [OF f] borel_measurable_subalgebra
9.21 +                  space_restrict_space)
9.22 +qed
9.23 +
9.24  context
9.25  begin
9.26
9.27 @@ -446,7 +463,7 @@
9.28
9.29  lemma AE_lborel_singleton: "AE x in lborel::'a::euclidean_space measure. x \<noteq> c"
9.30    using SOME_Basis AE_discrete_difference [of "{c}" lborel] emeasure_lborel_cbox [of c c]
9.31 -  by (auto simp add: cbox_sing prod_constant power_0_left)
9.32 +  by (auto simp add: power_0_left)
9.33
9.34  lemma emeasure_lborel_Ioo[simp]:
9.35    assumes [simp]: "l \<le> u"
9.36 @@ -542,7 +559,7 @@
9.37
9.38  end
9.39
9.40 -lemma emeasure_lborel_UNIV: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>"
9.41 +lemma emeasure_lborel_UNIV [simp]: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>"
9.42  proof -
9.43    { fix n::nat
9.44      let ?Ba = "Basis :: 'a set"
9.45 @@ -949,6 +966,9 @@
9.46  where
9.47    "lmeasurable \<equiv> fmeasurable lebesgue"
9.48
9.49 +lemma not_measurable_UNIV [simp]: "UNIV \<notin> lmeasurable"
9.50 +  by (simp add: fmeasurable_def)
9.51 +
9.52  lemma lmeasurable_iff_integrable:
9.53    "S \<in> lmeasurable \<longleftrightarrow> integrable lebesgue (indicator S :: 'a::euclidean_space \<Rightarrow> real)"
9.54    by (auto simp: fmeasurable_def integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator)
```
```    10.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sat Apr 14 20:19:52 2018 +0100
10.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Sun Apr 15 13:57:00 2018 +0100
10.3 @@ -1962,15 +1962,43 @@
10.4  lemma linear_bounded_pos:
10.5    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
10.6    assumes lf: "linear f"
10.7 -  shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
10.8 + obtains B where "B > 0" "\<And>x. norm (f x) \<le> B * norm x"
10.9  proof -
10.10    have "\<exists>B > 0. \<forall>x. norm (f x) \<le> norm x * B"
10.11      using lf unfolding linear_conv_bounded_linear
10.12      by (rule bounded_linear.pos_bounded)
10.13 -  then show ?thesis
10.14 -    by (simp only: mult.commute)
10.15 +  with that show ?thesis
10.16 +    by (auto simp: mult.commute)
10.17  qed
10.18
10.19 +lemma linear_invertible_bounded_below_pos:
10.20 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
10.21 +  assumes "linear f" "linear g" "g \<circ> f = id"
10.22 +  obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
10.23 +proof -
10.24 +  obtain B where "B > 0" and B: "\<And>x. norm (g x) \<le> B * norm x"
10.25 +    using linear_bounded_pos [OF \<open>linear g\<close>] by blast
10.26 +  show thesis
10.27 +  proof
10.28 +    show "0 < 1/B"
10.29 +      by (simp add: \<open>B > 0\<close>)
10.30 +    show "1/B * norm x \<le> norm (f x)" for x
10.31 +    proof -
10.32 +      have "1/B * norm x = 1/B * norm (g (f x))"
10.33 +        using assms by (simp add: pointfree_idE)
10.34 +      also have "\<dots> \<le> norm (f x)"
10.35 +        using B [of "f x"] by (simp add: \<open>B > 0\<close> mult.commute pos_divide_le_eq)
10.36 +      finally show ?thesis .
10.37 +    qed
10.38 +  qed
10.39 +qed
10.40 +
10.41 +lemma linear_inj_bounded_below_pos:
10.42 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
10.43 +  assumes "linear f" "inj f"
10.44 +  obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
10.45 +  using linear_injective_left_inverse [OF assms] linear_invertible_bounded_below_pos assms by blast
10.46 +
10.47  lemma bounded_linearI':
10.48    fixes f ::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
10.49    assumes "\<And>x y. f (x + y) = f x + f y"
```
```    11.1 --- a/src/HOL/Analysis/Measure_Space.thy	Sat Apr 14 20:19:52 2018 +0100
11.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Sun Apr 15 13:57:00 2018 +0100
11.3 @@ -1534,6 +1534,9 @@
11.4  lemma measure_nonneg[simp]: "0 \<le> measure M A"
11.5    unfolding measure_def by auto
11.6
11.7 +lemma measure_nonneg' [simp]: "\<not> measure M A < 0"
11.8 +  using measure_nonneg not_le by blast
11.9 +
11.10  lemma zero_less_measure_iff: "0 < measure M A \<longleftrightarrow> measure M A \<noteq> 0"
11.11    using measure_nonneg[of M A] by (auto simp add: le_less)
11.12
11.13 @@ -1686,7 +1689,7 @@
11.14    moreover have "ennreal (measure M (A i)) = emeasure M (A i)" for i
11.15      using assms emeasure_mono[of "A _" "\<Union>i. A i" M]
11.16      by (intro emeasure_eq_ennreal_measure[symmetric]) (auto simp: less_top UN_upper intro: le_less_trans)
11.17 -  ultimately show "(\<lambda>x. ennreal (Sigma_Algebra.measure M (A x))) \<longlonglongrightarrow> ennreal (Sigma_Algebra.measure M (\<Union>i. A i))"
11.18 +  ultimately show "(\<lambda>x. ennreal (measure M (A x))) \<longlonglongrightarrow> ennreal (measure M (\<Union>i. A i))"
11.19      using A by (auto intro!: Lim_emeasure_incseq)
11.20  qed auto
11.21
11.22 @@ -1699,7 +1702,7 @@
11.23      by (auto intro!: emeasure_eq_ennreal_measure[symmetric] simp: INT_lower less_top intro: le_less_trans)
11.24    moreover have "ennreal (measure M (A i)) = emeasure M (A i)" for i
11.25      using A fin[of i] by (intro emeasure_eq_ennreal_measure[symmetric]) auto
11.26 -  ultimately show "(\<lambda>x. ennreal (Sigma_Algebra.measure M (A x))) \<longlonglongrightarrow> ennreal (Sigma_Algebra.measure M (\<Inter>i. A i))"
11.27 +  ultimately show "(\<lambda>x. ennreal (measure M (A x))) \<longlonglongrightarrow> ennreal (measure M (\<Inter>i. A i))"
11.28      using fin A by (auto intro!: Lim_emeasure_decseq)
11.29  qed auto
11.30
11.31 @@ -1772,6 +1775,32 @@
11.32      using assms by (intro sets.countable_INT') auto
11.33  qed
11.34
11.35 +lemma measurable_measure_Diff:
11.36 +  assumes "A \<in> fmeasurable M" "B \<in> sets M" "B \<subseteq> A"
11.37 +  shows "measure M (A - B) = measure M A - measure M B"
11.38 +  by (simp add: assms fmeasurableD fmeasurableD2 measure_Diff)
11.39 +
11.40 +lemma measurable_Un_null_set:
11.41 +  assumes "B \<in> null_sets M"
11.42 +  shows "(A \<union> B \<in> fmeasurable M \<and> A \<in> sets M) \<longleftrightarrow> A \<in> fmeasurable M"
11.43 +  using assms  by (fastforce simp add: fmeasurable.Un fmeasurableI_null_sets intro: fmeasurableI2)
11.44 +
11.45 +lemma measurable_Diff_null_set:
11.46 +  assumes "B \<in> null_sets M"
11.47 +  shows "(A - B) \<in> fmeasurable M \<and> A \<in> sets M \<longleftrightarrow> A \<in> fmeasurable M"
11.48 +  using assms
11.49 +  by (metis Un_Diff_cancel2 fmeasurable.Diff fmeasurableD fmeasurableI_null_sets measurable_Un_null_set)
11.50 +
11.51 +lemma fmeasurable_Diff_D:
11.52 +    assumes m: "T - S \<in> fmeasurable M" "S \<in> fmeasurable M" and sub: "S \<subseteq> T"
11.53 +    shows "T \<in> fmeasurable M"
11.54 +proof -
11.55 +  have "T = S \<union> (T - S)"
11.56 +    using assms by blast
11.57 +  then show ?thesis
11.58 +    by (metis m fmeasurable.Un)
11.59 +qed
11.60 +
11.61  lemma measure_Un2:
11.62    "A \<in> fmeasurable M \<Longrightarrow> B \<in> fmeasurable M \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M (B - A)"
11.63    using measure_Union[of M A "B - A"] by (auto simp: fmeasurableD2 fmeasurable.Diff)
11.64 @@ -1801,12 +1830,13 @@
11.65      measure M (\<Union>i\<in>I. F i) = (\<Sum>i\<in>I. measure M (F i))"
11.66    unfolding AE_pairwise[OF countable_finite, OF I]
11.67    using I
11.68 -  apply (induction I rule: finite_induct)
11.69 -   apply simp
11.70 -  apply (simp add: pairwise_insert)
11.71 -  apply (subst measure_Un_AE)
11.72 -  apply auto
11.73 -  done
11.74 +proof (induction I rule: finite_induct)
11.75 +  case (insert x I)
11.76 +  have "measure M (F x \<union> UNION I F) = measure M (F x) + measure M (UNION I F)"
11.77 +    by (rule measure_Un_AE) (use insert in \<open>auto simp: pairwise_insert\<close>)
11.78 +    with insert show ?case
11.79 +      by (simp add: pairwise_insert )
11.80 +qed simp
11.81
11.82  lemma measure_UNION':
11.83    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i \<in> fmeasurable M) \<Longrightarrow> pairwise (\<lambda>i j. disjnt (F i) (F j)) I \<Longrightarrow>
11.84 @@ -1888,6 +1918,18 @@
11.85    then show ?fm ?m by auto
11.86  qed
11.87
11.88 +lemma measure_diff_le_measure_setdiff:
11.89 +  assumes "S \<in> fmeasurable M" "T \<in> fmeasurable M"
11.90 +  shows "measure M S - measure M T \<le> measure M (S - T)"
11.91 +proof -
11.92 +  have "measure M S \<le> measure M ((S - T) \<union> T)"
11.93 +    by (simp add: assms fmeasurable.Un fmeasurableD measure_mono_fmeasurable)
11.94 +  also have "\<dots> \<le> measure M (S - T) + measure M T"
11.95 +    using assms by (blast intro: measure_Un_le)
11.96 +  finally show ?thesis
11.97 +    by (simp add: algebra_simps)
11.98 +qed
11.99 +
11.100  lemma suminf_exist_split2:
11.101    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
11.102    assumes "summable f"
```
```    12.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Sat Apr 14 20:19:52 2018 +0100
12.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Sun Apr 15 13:57:00 2018 +0100
12.3 @@ -2096,7 +2096,7 @@
12.4  lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M"
12.5    using sets.sets_into_space unfolding restrict_space_def by (subst space_measure_of) auto
12.6
12.7 -lemma space_restrict_space2: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
12.8 +lemma space_restrict_space2 [simp]: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
12.9    by (simp add: space_restrict_space sets.sets_into_space)
12.10
12.11  lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = ((\<inter>) \<Omega>) ` sets M"
```
```    13.1 --- a/src/HOL/Probability/Information.thy	Sat Apr 14 20:19:52 2018 +0100
13.2 +++ b/src/HOL/Probability/Information.thy	Sun Apr 15 13:57:00 2018 +0100
13.3 @@ -834,9 +834,14 @@
13.4      - log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX)"
13.5      using Px Px_nn fin by (auto simp: measure_def)
13.6    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)"
13.7 -    unfolding distributed_distr_eq_density[OF X] using Px Px_nn
13.8 -    apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
13.9 -    by (subst integral_density) (auto simp del: integral_indicator intro!: Bochner_Integration.integral_cong)
13.10 +  proof -
13.11 +    have "integral\<^sup>L MX (indicator {x \<in> space MX. Px x \<noteq> 0}) = LINT x|MX. Px x *\<^sub>R (1 / Px x)"
13.12 +      by (rule Bochner_Integration.integral_cong) auto
13.13 +    also have "... = LINT x|density MX (\<lambda>x. ennreal (Px x)). 1 / Px x"
13.14 +      by (rule integral_density [symmetric]) (use Px Px_nn in auto)
13.15 +    finally show ?thesis
13.16 +      unfolding distributed_distr_eq_density[OF X] by simp
13.17 +  qed
13.18    also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
13.19    proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
13.20      show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"
```