various new results on measures, integrals, etc., and some simplified proofs
authorpaulson <lp15@cam.ac.uk>
Sun Apr 15 13:57:00 2018 +0100 (13 months ago)
changeset 679827643b005b29a
parent 67981 349c639e593c
child 67983 487685540a51
child 67984 adc1a992c470
various new results on measures, integrals, etc., and some simplified proofs
src/HOL/Analysis/Ball_Volume.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Complete_Measure.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Fashoda_Theorem.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Sigma_Algebra.thy
src/HOL/Probability/Information.thy
     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.18    by (simp add: subspace_def)
    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.45           (simp_all add: inner_axis)
    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.51    by (simp add: inner_axis)
    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<..}"