--- a/src/HOL/Analysis/Ball_Volume.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Ball_Volume.thy Sun Apr 15 13:57:00 2018 +0100
@@ -1,10 +1,10 @@
(*
File: HOL/Analysis/Gamma_Function.thy
Author: Manuel Eberl, TU München
+*)
- The volume (Lebesgue measure) of an n-dimensional ball.
-*)
-section \<open>The volume of an $n$-ball\<close>
+section \<open>The volume (Lebesgue measure) of an $n$-dimensional ball\<close>
+
theory Ball_Volume
imports Gamma_Function Lebesgue_Integral_Substitution
begin
@@ -301,4 +301,30 @@
corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
by (simp add: content_ball unit_ball_vol_3)
+text \<open>
+ Useful equivalent forms
+\<close>
+corollary content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \<longleftrightarrow> r \<le> 0"
+proof -
+ have "r > 0 \<Longrightarrow> content (ball c r) > 0"
+ by (simp add: content_ball unit_ball_vol_def)
+ then show ?thesis
+ by (fastforce simp: ball_empty)
+qed
+
+corollary content_ball_gt_0_iff [simp]: "0 < content (ball z r) \<longleftrightarrow> 0 < r"
+ by (auto simp: zero_less_measure_iff)
+
+corollary content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \<longleftrightarrow> r \<le> 0"
+proof (cases "r = 0")
+ case False
+ moreover have "r > 0 \<Longrightarrow> content (cball c r) > 0"
+ by (simp add: content_cball unit_ball_vol_def)
+ ultimately show ?thesis
+ by fastforce
+qed auto
+
+corollary content_cball_gt_0_iff [simp]: "0 < content (cball z r) \<longleftrightarrow> 0 < r"
+ by (auto simp: zero_less_measure_iff)
+
end
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Sun Apr 15 13:57:00 2018 +0100
@@ -4,6 +4,16 @@
imports Finite_Cartesian_Product Derivative
begin
+lemma norm_le_componentwise:
+ "(\<And>b. b \<in> Basis \<Longrightarrow> abs(x \<bullet> b) \<le> abs(y \<bullet> b)) \<Longrightarrow> norm x \<le> norm y"
+ 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)
+
+lemma norm_le_componentwise_cart:
+ fixes x :: "real^'n"
+ shows "(\<And>i. abs(x$i) \<le> abs(y$i)) \<Longrightarrow> norm x \<le> norm y"
+ unfolding cart_eq_inner_axis
+ by (rule norm_le_componentwise) (metis axis_index)
+
lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
by (simp add: subspace_def)
@@ -759,7 +769,7 @@
have "norm (\<chi> j. A $ j $ i) \<le> norm (A *v axis i 1)"
by (simp add: matrix_mult_dot cart_eq_inner_axis)
also have "\<dots> \<le> onorm (( *v) A)"
- using onorm [OF bl, of "axis i 1"] by (auto simp: axis_in_Basis)
+ using onorm [OF bl, of "axis i 1"] by auto
finally have "norm (\<chi> j. A $ j $ i) \<le> onorm (( *v) A)" .
then show ?thesis
unfolding column_def .
--- a/src/HOL/Analysis/Complete_Measure.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Complete_Measure.thy Sun Apr 15 13:57:00 2018 +0100
@@ -114,6 +114,11 @@
qed auto
qed
+lemma sets_restrict_space_subset:
+ assumes S: "S \<in> sets (completion M)"
+ shows "sets (restrict_space (completion M) S) \<subseteq> sets (completion M)"
+ by (metis assms sets.Int_space_eq2 sets_restrict_space_iff subsetI)
+
lemma
assumes "S \<in> sets (completion M)"
shows main_part_sets[intro, simp]: "main_part M S \<in> sets M"
@@ -989,6 +994,23 @@
finally show ?thesis .
qed
+lemma (in complete_measure) fmeasurable_measure_inner_outer_le:
+ "(S \<in> fmeasurable M \<and> m = measure M S) \<longleftrightarrow>
+ (\<forall>e>0. \<exists>T\<in>fmeasurable M. T \<subseteq> S \<and> m - e \<le> measure M T) \<and>
+ (\<forall>e>0. \<exists>U\<in>fmeasurable M. S \<subseteq> U \<and> measure M U \<le> m + e)" (is ?T1)
+ and null_sets_outer_le:
+ "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)
+proof -
+ have "e > 0 \<and> m - e/2 \<le> t \<Longrightarrow> m - e < t"
+ "e > 0 \<and> t \<le> m + e/2 \<Longrightarrow> t < m + e"
+ "e > 0 \<longleftrightarrow> e/2 > 0"
+ for e t
+ by auto
+ then show ?T1 ?T2
+ unfolding fmeasurable_measure_inner_outer null_sets_outer
+ by (meson dense le_less_trans less_imp_le)+
+qed
+
lemma (in cld_measure) notin_sets_outer_measure_of_cover:
assumes E: "E \<subseteq> space M" "E \<notin> sets M"
shows "\<exists>B\<in>sets M. 0 < emeasure M B \<and> emeasure M B < \<infinity> \<and>
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Sun Apr 15 13:57:00 2018 +0100
@@ -6992,7 +6992,7 @@
done
qed
-subsubsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
+subsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
lemma image_stretch_interval:
"(\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k)) *\<^sub>R k) ` cbox a (b::'a::euclidean_space) =
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sun Apr 15 13:57:00 2018 +0100
@@ -945,7 +945,18 @@
by (auto simp: integrable_on_def nn_integral_completion)
qed
qed
-
+
+lemma integrable_on_lebesgue_on:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes f: "integrable (lebesgue_on S) f" and S: "S \<in> sets lebesgue"
+ shows "f integrable_on S"
+proof -
+ have "integrable lebesgue (\<lambda>x. indicator S x *\<^sub>R f x)"
+ using S f inf_top.comm_neutral integrable_restrict_space by blast
+ then show ?thesis
+ using absolutely_integrable_on_def set_integrable_def by blast
+qed
+
lemma absolutely_integrable_on_null [intro]:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "content (cbox a b) = 0 \<Longrightarrow> f absolutely_integrable_on (cbox a b)"
@@ -1051,6 +1062,39 @@
lemma lmeasure_integral: "S \<in> lmeasurable \<Longrightarrow> measure lebesgue S = integral S (\<lambda>x. 1::real)"
by (fastforce simp add: lmeasure_integral_UNIV indicator_def[abs_def] lmeasurable_iff_integrable_on)
+lemma integrable_on_const: "S \<in> lmeasurable \<Longrightarrow> (\<lambda>x. c) integrable_on S"
+ unfolding lmeasurable_iff_integrable
+ by (metis (mono_tags, lifting) integrable_eq integrable_on_scaleR_left lmeasurable_iff_integrable lmeasurable_iff_integrable_on scaleR_one)
+
+lemma integral_indicator:
+ assumes "(S \<inter> T) \<in> lmeasurable"
+ shows "integral T (indicator S) = measure lebesgue (S \<inter> T)"
+proof -
+ have "integral UNIV (indicator (S \<inter> T)) = integral UNIV (\<lambda>a. if a \<in> S \<inter> T then 1::real else 0)"
+ by (meson indicator_def)
+ moreover
+ have "(indicator (S \<inter> T) has_integral measure lebesgue (S \<inter> T)) UNIV"
+ using assms by (simp add: lmeasurable_iff_has_integral)
+ ultimately have "integral UNIV (\<lambda>x. if x \<in> S \<inter> T then 1 else 0) = measure lebesgue (S \<inter> T)"
+ by (metis (no_types) integral_unique)
+ then show ?thesis
+ using integral_restrict_Int [of UNIV "S \<inter> T" "\<lambda>x. 1::real"]
+ apply (simp add: integral_restrict_Int [symmetric])
+ by (meson indicator_def)
+qed
+
+lemma measurable_integrable:
+ fixes S :: "'a::euclidean_space set"
+ shows "S \<in> lmeasurable \<longleftrightarrow> (indicat_real S) integrable_on UNIV"
+ by (auto simp: lmeasurable_iff_integrable absolutely_integrable_on_iff_nonneg [symmetric] set_integrable_def)
+
+lemma integrable_on_indicator:
+ fixes S :: "'a::euclidean_space set"
+ shows "indicat_real S integrable_on T \<longleftrightarrow> (S \<inter> T) \<in> lmeasurable"
+ unfolding measurable_integrable
+ unfolding integrable_restrict_UNIV [of T, symmetric]
+ by (fastforce simp add: indicator_def elim: integrable_eq)
+
lemma
assumes \<D>: "\<D> division_of S"
shows lmeasurable_division: "S \<in> lmeasurable" (is ?l)
@@ -1072,7 +1116,6 @@
by (auto intro!: measure_Union_AE[symmetric] simp: completion.AE_iff_null_sets Int_def[symmetric] pairwise_def null_sets_def)
qed
-text \<open>This should be an abbreviation for negligible.\<close>
lemma negligible_iff_null_sets: "negligible S \<longleftrightarrow> S \<in> null_sets lebesgue"
proof
assume "negligible S"
@@ -2208,6 +2251,12 @@
using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
qed (use le in \<open>force intro!: always_eventually split: split_indicator\<close>)
+lemma absolutely_integrable_continuous:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "continuous_on (cbox a b) f \<Longrightarrow> f absolutely_integrable_on cbox a b"
+ using absolutely_integrable_integrable_bound
+ by (simp add: absolutely_integrable_on_def continuous_on_norm integrable_continuous)
+
subsection \<open>Componentwise\<close>
proposition absolutely_integrable_componentwise_iff:
--- a/src/HOL/Analysis/Fashoda_Theorem.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy Sun Apr 15 13:57:00 2018 +0100
@@ -269,15 +269,10 @@
by auto
moreover
from x1 have "g (x $ 2) \<in> cbox (-1) 1"
- apply -
- apply (rule assms(2)[unfolded subset_eq,rule_format])
- apply auto
- done
+ using assms(2) by blast
ultimately show False
unfolding lem3[OF nz] vector_component_simps * mem_box_cart
- apply (erule_tac x=1 in allE)
- apply auto
- done
+ using not_le by auto
next
assume as: "x$1 = -1"
then have *: "f (x $ 1) $ 1 = - 1"
@@ -288,15 +283,10 @@
by auto
moreover
from x1 have "g (x $ 2) \<in> cbox (-1) 1"
- apply -
- apply (rule assms(2)[unfolded subset_eq,rule_format])
- apply auto
- done
+ using assms(2) by blast
ultimately show False
unfolding lem3[OF nz] vector_component_simps * mem_box_cart
- apply (erule_tac x=1 in allE)
- apply auto
- done
+ using not_le by auto
next
assume as: "x$2 = 1"
then have *: "g (x $ 2) $ 2 = 1"
@@ -527,7 +517,7 @@
and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
using assms as
- by (simp_all add: axis_in_Basis cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
+ by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
(simp_all add: inner_axis)
qed
from z(1) obtain zf where zf:
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Sun Apr 15 13:57:00 2018 +0100
@@ -607,20 +607,8 @@
apply (rule sum.neutral, simp add: axis_def)
done
-lemma sum_single:
- assumes "finite A" and "k \<in> A" and "f k = y"
- assumes "\<And>i. i \<in> A \<Longrightarrow> i \<noteq> k \<Longrightarrow> f i = 0"
- shows "(\<Sum>i\<in>A. f i) = y"
- apply (subst sum.remove [OF assms(1,2)])
- apply (simp add: sum.neutral assms(3,4))
- done
-
lemma inner_axis: "inner x (axis i y) = inner (x $ i) y"
- unfolding inner_vec_def
- apply (rule_tac k=i in sum_single)
- apply simp_all
- apply (simp add: axis_def)
- done
+ by (simp add: inner_vec_def axis_def sum.remove [where x=i])
lemma inner_axis': "inner(axis i y) x = inner y (x $ i)"
by (simp add: inner_axis inner_commute)
@@ -649,22 +637,51 @@
by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
qed
-lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
- apply (simp add: Basis_vec_def)
- apply (subst card_UN_disjoint)
- apply simp
- apply simp
- apply (auto simp: axis_eq_axis) [1]
- apply (subst card_UN_disjoint)
- apply (auto simp: axis_eq_axis)
- done
+lemma DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
+proof -
+ 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}))"
+ by (rule card_UN_disjoint) (auto simp: axis_eq_axis)
+ also have "... = CARD('b) * DIM('a)"
+ by (subst card_UN_disjoint) (auto simp: axis_eq_axis)
+ finally show ?thesis
+ by (simp add: Basis_vec_def)
+qed
end
lemma cart_eq_inner_axis: "a $ i = inner a (axis i 1)"
by (simp add: inner_axis)
-lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
- by (auto simp add: Basis_vec_def axis_eq_axis)
+lemma axis_eq_0_iff [simp]:
+ shows "axis m x = 0 \<longleftrightarrow> x = 0"
+ by (simp add: axis_def vec_eq_iff)
+
+lemma axis_in_Basis_iff [simp]: "axis i a \<in> Basis \<longleftrightarrow> a \<in> Basis"
+ by (auto simp: Basis_vec_def axis_eq_axis)
+
+text\<open>Mapping each basis element to the corresponding finite index\<close>
+definition axis_index :: "('a::comm_ring_1)^'n \<Rightarrow> 'n" where "axis_index v \<equiv> SOME i. v = axis i 1"
+
+lemma axis_inverse:
+ fixes v :: "real^'n"
+ assumes "v \<in> Basis"
+ shows "\<exists>i. v = axis i 1"
+proof -
+ have "v \<in> (\<Union>n. \<Union>r\<in>Basis. {axis n r})"
+ using assms Basis_vec_def by blast
+ then show ?thesis
+ by (force simp add: vec_eq_iff)
+qed
+
+lemma axis_index:
+ fixes v :: "real^'n"
+ assumes "v \<in> Basis"
+ shows "v = axis (axis_index v) 1"
+ by (metis (mono_tags) assms axis_inverse axis_index_def someI_ex)
+
+lemma axis_index_axis [simp]:
+ fixes UU :: "real^'n"
+ shows "(axis_index (axis u 1 :: real^'n)) = (u::'n)"
+ by (simp add: axis_eq_axis axis_index_def)
end
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sun Apr 15 13:57:00 2018 +0100
@@ -3501,6 +3501,44 @@
using assms unfolding integrable_on_def
by (force dest: has_integral_stretch)
+lemma vec_lambda_eq_sum:
+ shows "(\<chi> k. f k (x $ k)) = (\<Sum>k\<in>Basis. (f (axis_index k) (x \<bullet> k)) *\<^sub>R k)"
+ apply (simp add: Basis_vec_def cart_eq_inner_axis UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def)
+ apply (simp add: vec_eq_iff axis_def if_distrib cong: if_cong)
+ done
+
+lemma has_integral_stretch_cart:
+ fixes m :: "'n::finite \<Rightarrow> real"
+ assumes f: "(f has_integral i) (cbox a b)" and m: "\<And>k. m k \<noteq> 0"
+ shows "((\<lambda>x. f(\<chi> k. m k * x$k)) has_integral i /\<^sub>R \<bar>prod m UNIV\<bar>)
+ ((\<lambda>x. \<chi> k. x$k / m k) ` (cbox a b))"
+proof -
+ have *: "\<forall>k:: real^'n \<in> Basis. m (axis_index k) \<noteq> 0"
+ using axis_index by (simp add: m)
+ have eqp: "(\<Prod>k:: real^'n \<in> Basis. m (axis_index k)) = prod m UNIV"
+ by (simp add: Basis_vec_def UNION_singleton_eq_range prod.reindex axis_eq_axis inj_on_def)
+ show ?thesis
+ 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"]
+ by (simp add: field_simps eqp)
+qed
+
+lemma image_stretch_interval_cart:
+ fixes m :: "'n::finite \<Rightarrow> real"
+ shows "(\<lambda>x. \<chi> k. m k * x$k) ` cbox a b =
+ (if cbox a b = {} then {}
+ else cbox (\<chi> k. min (m k * a$k) (m k * b$k)) (\<chi> k. max (m k * a$k) (m k * b$k)))"
+proof -
+ have *: "(\<Sum>k\<in>Basis. min (m (axis_index k) * (a \<bullet> k)) (m (axis_index k) * (b \<bullet> k)) *\<^sub>R k)
+ = (\<chi> k. min (m k * a $ k) (m k * b $ k))"
+ "(\<Sum>k\<in>Basis. max (m (axis_index k) * (a \<bullet> k)) (m (axis_index k) * (b \<bullet> k)) *\<^sub>R k)
+ = (\<chi> k. max (m k * a $ k) (m k * b $ k))"
+ apply (simp_all add: Basis_vec_def cart_eq_inner_axis UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def)
+ apply (simp_all add: vec_eq_iff axis_def if_distrib cong: if_cong)
+ done
+ show ?thesis
+ by (simp add: vec_lambda_eq_sum [where f="\<lambda>i x. m i * x"] image_stretch_interval eq_cbox *)
+qed
+
subsection \<open>even more special cases\<close>
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Sun Apr 15 13:57:00 2018 +0100
@@ -393,6 +393,23 @@
lemma Compl_in_sets_lebesgue: "-A \<in> sets lebesgue \<longleftrightarrow> A \<in> sets lebesgue"
by (metis Compl_eq_Diff_UNIV double_compl space_borel space_completion space_lborel Sigma_Algebra.sets.compl_sets)
+lemma measurable_lebesgue_cong:
+ assumes "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
+ shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
+ by (metis (mono_tags, lifting) IntD1 assms measurable_cong_strong space_restrict_space)
+
+text\<open>Measurability of continuous functions\<close>
+lemma continuous_imp_measurable_on_sets_lebesgue:
+ assumes f: "continuous_on S f" and S: "S \<in> sets lebesgue"
+ shows "f \<in> borel_measurable (lebesgue_on S)"
+proof -
+ have "sets (restrict_space borel S) \<subseteq> sets (lebesgue_on S)"
+ by (simp add: mono_restrict_space subsetI)
+ then show ?thesis
+ by (simp add: borel_measurable_continuous_on_restrict [OF f] borel_measurable_subalgebra
+ space_restrict_space)
+qed
+
context
begin
@@ -446,7 +463,7 @@
lemma AE_lborel_singleton: "AE x in lborel::'a::euclidean_space measure. x \<noteq> c"
using SOME_Basis AE_discrete_difference [of "{c}" lborel] emeasure_lborel_cbox [of c c]
- by (auto simp add: cbox_sing prod_constant power_0_left)
+ by (auto simp add: power_0_left)
lemma emeasure_lborel_Ioo[simp]:
assumes [simp]: "l \<le> u"
@@ -542,7 +559,7 @@
end
-lemma emeasure_lborel_UNIV: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>"
+lemma emeasure_lborel_UNIV [simp]: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>"
proof -
{ fix n::nat
let ?Ba = "Basis :: 'a set"
@@ -949,6 +966,9 @@
where
"lmeasurable \<equiv> fmeasurable lebesgue"
+lemma not_measurable_UNIV [simp]: "UNIV \<notin> lmeasurable"
+ by (simp add: fmeasurable_def)
+
lemma lmeasurable_iff_integrable:
"S \<in> lmeasurable \<longleftrightarrow> integrable lebesgue (indicator S :: 'a::euclidean_space \<Rightarrow> real)"
by (auto simp: fmeasurable_def integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator)
--- a/src/HOL/Analysis/Linear_Algebra.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Sun Apr 15 13:57:00 2018 +0100
@@ -1962,15 +1962,43 @@
lemma linear_bounded_pos:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes lf: "linear f"
- shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
+ obtains B where "B > 0" "\<And>x. norm (f x) \<le> B * norm x"
proof -
have "\<exists>B > 0. \<forall>x. norm (f x) \<le> norm x * B"
using lf unfolding linear_conv_bounded_linear
by (rule bounded_linear.pos_bounded)
- then show ?thesis
- by (simp only: mult.commute)
+ with that show ?thesis
+ by (auto simp: mult.commute)
qed
+lemma linear_invertible_bounded_below_pos:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
+ assumes "linear f" "linear g" "g \<circ> f = id"
+ obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
+proof -
+ obtain B where "B > 0" and B: "\<And>x. norm (g x) \<le> B * norm x"
+ using linear_bounded_pos [OF \<open>linear g\<close>] by blast
+ show thesis
+ proof
+ show "0 < 1/B"
+ by (simp add: \<open>B > 0\<close>)
+ show "1/B * norm x \<le> norm (f x)" for x
+ proof -
+ have "1/B * norm x = 1/B * norm (g (f x))"
+ using assms by (simp add: pointfree_idE)
+ also have "\<dots> \<le> norm (f x)"
+ using B [of "f x"] by (simp add: \<open>B > 0\<close> mult.commute pos_divide_le_eq)
+ finally show ?thesis .
+ qed
+ qed
+qed
+
+lemma linear_inj_bounded_below_pos:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
+ assumes "linear f" "inj f"
+ obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
+ using linear_injective_left_inverse [OF assms] linear_invertible_bounded_below_pos assms by blast
+
lemma bounded_linearI':
fixes f ::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
assumes "\<And>x y. f (x + y) = f x + f y"
--- a/src/HOL/Analysis/Measure_Space.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Sun Apr 15 13:57:00 2018 +0100
@@ -1534,6 +1534,9 @@
lemma measure_nonneg[simp]: "0 \<le> measure M A"
unfolding measure_def by auto
+lemma measure_nonneg' [simp]: "\<not> measure M A < 0"
+ using measure_nonneg not_le by blast
+
lemma zero_less_measure_iff: "0 < measure M A \<longleftrightarrow> measure M A \<noteq> 0"
using measure_nonneg[of M A] by (auto simp add: le_less)
@@ -1686,7 +1689,7 @@
moreover have "ennreal (measure M (A i)) = emeasure M (A i)" for i
using assms emeasure_mono[of "A _" "\<Union>i. A i" M]
by (intro emeasure_eq_ennreal_measure[symmetric]) (auto simp: less_top UN_upper intro: le_less_trans)
- ultimately show "(\<lambda>x. ennreal (Sigma_Algebra.measure M (A x))) \<longlonglongrightarrow> ennreal (Sigma_Algebra.measure M (\<Union>i. A i))"
+ ultimately show "(\<lambda>x. ennreal (measure M (A x))) \<longlonglongrightarrow> ennreal (measure M (\<Union>i. A i))"
using A by (auto intro!: Lim_emeasure_incseq)
qed auto
@@ -1699,7 +1702,7 @@
by (auto intro!: emeasure_eq_ennreal_measure[symmetric] simp: INT_lower less_top intro: le_less_trans)
moreover have "ennreal (measure M (A i)) = emeasure M (A i)" for i
using A fin[of i] by (intro emeasure_eq_ennreal_measure[symmetric]) auto
- ultimately show "(\<lambda>x. ennreal (Sigma_Algebra.measure M (A x))) \<longlonglongrightarrow> ennreal (Sigma_Algebra.measure M (\<Inter>i. A i))"
+ ultimately show "(\<lambda>x. ennreal (measure M (A x))) \<longlonglongrightarrow> ennreal (measure M (\<Inter>i. A i))"
using fin A by (auto intro!: Lim_emeasure_decseq)
qed auto
@@ -1772,6 +1775,32 @@
using assms by (intro sets.countable_INT') auto
qed
+lemma measurable_measure_Diff:
+ assumes "A \<in> fmeasurable M" "B \<in> sets M" "B \<subseteq> A"
+ shows "measure M (A - B) = measure M A - measure M B"
+ by (simp add: assms fmeasurableD fmeasurableD2 measure_Diff)
+
+lemma measurable_Un_null_set:
+ assumes "B \<in> null_sets M"
+ shows "(A \<union> B \<in> fmeasurable M \<and> A \<in> sets M) \<longleftrightarrow> A \<in> fmeasurable M"
+ using assms by (fastforce simp add: fmeasurable.Un fmeasurableI_null_sets intro: fmeasurableI2)
+
+lemma measurable_Diff_null_set:
+ assumes "B \<in> null_sets M"
+ shows "(A - B) \<in> fmeasurable M \<and> A \<in> sets M \<longleftrightarrow> A \<in> fmeasurable M"
+ using assms
+ by (metis Un_Diff_cancel2 fmeasurable.Diff fmeasurableD fmeasurableI_null_sets measurable_Un_null_set)
+
+lemma fmeasurable_Diff_D:
+ assumes m: "T - S \<in> fmeasurable M" "S \<in> fmeasurable M" and sub: "S \<subseteq> T"
+ shows "T \<in> fmeasurable M"
+proof -
+ have "T = S \<union> (T - S)"
+ using assms by blast
+ then show ?thesis
+ by (metis m fmeasurable.Un)
+qed
+
lemma measure_Un2:
"A \<in> fmeasurable M \<Longrightarrow> B \<in> fmeasurable M \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M (B - A)"
using measure_Union[of M A "B - A"] by (auto simp: fmeasurableD2 fmeasurable.Diff)
@@ -1801,12 +1830,13 @@
measure M (\<Union>i\<in>I. F i) = (\<Sum>i\<in>I. measure M (F i))"
unfolding AE_pairwise[OF countable_finite, OF I]
using I
- apply (induction I rule: finite_induct)
- apply simp
- apply (simp add: pairwise_insert)
- apply (subst measure_Un_AE)
- apply auto
- done
+proof (induction I rule: finite_induct)
+ case (insert x I)
+ have "measure M (F x \<union> UNION I F) = measure M (F x) + measure M (UNION I F)"
+ by (rule measure_Un_AE) (use insert in \<open>auto simp: pairwise_insert\<close>)
+ with insert show ?case
+ by (simp add: pairwise_insert )
+qed simp
lemma measure_UNION':
"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>
@@ -1888,6 +1918,18 @@
then show ?fm ?m by auto
qed
+lemma measure_diff_le_measure_setdiff:
+ assumes "S \<in> fmeasurable M" "T \<in> fmeasurable M"
+ shows "measure M S - measure M T \<le> measure M (S - T)"
+proof -
+ have "measure M S \<le> measure M ((S - T) \<union> T)"
+ by (simp add: assms fmeasurable.Un fmeasurableD measure_mono_fmeasurable)
+ also have "\<dots> \<le> measure M (S - T) + measure M T"
+ using assms by (blast intro: measure_Un_le)
+ finally show ?thesis
+ by (simp add: algebra_simps)
+qed
+
lemma suminf_exist_split2:
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
assumes "summable f"
--- a/src/HOL/Analysis/Sigma_Algebra.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Sun Apr 15 13:57:00 2018 +0100
@@ -2096,7 +2096,7 @@
lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M"
using sets.sets_into_space unfolding restrict_space_def by (subst space_measure_of) auto
-lemma space_restrict_space2: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
+lemma space_restrict_space2 [simp]: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
by (simp add: space_restrict_space sets.sets_into_space)
lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = ((\<inter>) \<Omega>) ` sets M"
--- a/src/HOL/Probability/Information.thy Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Probability/Information.thy Sun Apr 15 13:57:00 2018 +0100
@@ -834,9 +834,14 @@
- log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX)"
using Px Px_nn fin by (auto simp: measure_def)
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)"
- unfolding distributed_distr_eq_density[OF X] using Px Px_nn
- apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
- by (subst integral_density) (auto simp del: integral_indicator intro!: Bochner_Integration.integral_cong)
+ proof -
+ have "integral\<^sup>L MX (indicator {x \<in> space MX. Px x \<noteq> 0}) = LINT x|MX. Px x *\<^sub>R (1 / Px x)"
+ by (rule Bochner_Integration.integral_cong) auto
+ also have "... = LINT x|density MX (\<lambda>x. ennreal (Px x)). 1 / Px x"
+ by (rule integral_density [symmetric]) (use Px Px_nn in auto)
+ finally show ?thesis
+ unfolding distributed_distr_eq_density[OF X] by simp
+ qed
also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"