--- a/src/HOL/Analysis/Borel_Space.thy Thu Sep 12 14:22:47 2019 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy Thu Sep 12 14:51:50 2019 +0100
@@ -2101,7 +2101,7 @@
fixes p::real
assumes [measurable]: "f \<in> borel_measurable M"
shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> borel_measurable M"
-unfolding powr_def by auto
+ by simp
text \<open>The next one is a variation around \<open>measurable_restrict_space\<close>.\<close>
@@ -2115,6 +2115,12 @@
measurable_restrict_space2[of f, of "restrict_space M A", of B, of N] assms(2) space_restrict_space)
qed
+lemma measurable_restrict_mono:
+ assumes f: "f \<in> restrict_space M A \<rightarrow>\<^sub>M N" and "B \<subseteq> A"
+ shows "f \<in> restrict_space M B \<rightarrow>\<^sub>M N"
+by (rule measurable_compose[OF measurable_restrict_space3 f])
+ (insert \<open>B \<subseteq> A\<close>, auto)
+
text \<open>The next one is a variation around \<open>measurable_piecewise_restrict\<close>.\<close>
lemma measurable_piecewise_restrict2:
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Sep 12 14:22:47 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Sep 12 14:51:50 2019 +0100
@@ -1100,34 +1100,6 @@
by (simp add: fun_Compl_def uniformly_continuous_on_minus)
-subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological properties of linear functions\<close>
-
-lemma linear_lim_0:
- assumes "bounded_linear f"
- shows "(f \<longlongrightarrow> 0) (at (0))"
-proof -
- interpret f: bounded_linear f by fact
- have "(f \<longlongrightarrow> f 0) (at 0)"
- using tendsto_ident_at by (rule f.tendsto)
- then show ?thesis unfolding f.zero .
-qed
-
-lemma linear_continuous_at:
- assumes "bounded_linear f"
- shows "continuous (at a) f"
- unfolding continuous_at using assms
- apply (rule bounded_linear.tendsto)
- apply (rule tendsto_ident_at)
- done
-
-lemma linear_continuous_within:
- "bounded_linear f \<Longrightarrow> continuous (at x within s) f"
- using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
-
-lemma linear_continuous_on:
- "bounded_linear f \<Longrightarrow> continuous_on s f"
- using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
-
subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic Preserves Topological Properties\<close>
lemma open_scaling[intro]:
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Sep 12 14:22:47 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Sep 12 14:51:50 2019 +0100
@@ -4226,13 +4226,6 @@
qed
-lemma borel_measurable_vimage_halfspace_component_lt:
- "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
- (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i < a} \<in> sets (lebesgue_on S))"
- apply (rule trans [OF borel_measurable_iff_halfspace_less])
- apply (fastforce simp add: space_restrict_space)
- done
-
lemma borel_measurable_simple_function_limit:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
@@ -4298,174 +4291,6 @@
using borel_measurable_vimage_halfspace_component_lt by blast
qed
-lemma borel_measurable_vimage_halfspace_component_ge:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
- (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<ge> a} \<in> sets (lebesgue_on S))"
- apply (rule trans [OF borel_measurable_iff_halfspace_ge])
- apply (fastforce simp add: space_restrict_space)
- done
-
-lemma borel_measurable_vimage_halfspace_component_gt:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
- (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i > a} \<in> sets (lebesgue_on S))"
- apply (rule trans [OF borel_measurable_iff_halfspace_greater])
- apply (fastforce simp add: space_restrict_space)
- done
-
-lemma borel_measurable_vimage_halfspace_component_le:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
- (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<le> a} \<in> sets (lebesgue_on S))"
- apply (rule trans [OF borel_measurable_iff_halfspace_le])
- apply (fastforce simp add: space_restrict_space)
- done
-
-lemma
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows borel_measurable_vimage_open_interval:
- "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
- (\<forall>a b. {x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S))" (is ?thesis1)
- and borel_measurable_vimage_open:
- "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
- (\<forall>T. open T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))" (is ?thesis2)
-proof -
- have "{x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S)" if "f \<in> borel_measurable (lebesgue_on S)" for a b
- proof -
- have "S = S \<inter> space lebesgue"
- by simp
- then have "S \<inter> (f -` box a b) \<in> sets (lebesgue_on S)"
- by (metis (no_types) box_borel in_borel_measurable_borel inf_sup_aci(1) space_restrict_space that)
- then show ?thesis
- by (simp add: Collect_conj_eq vimage_def)
- qed
- moreover
- have "{x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)"
- if T: "\<And>a b. {x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S)" "open T" for T
- proof -
- obtain \<D> where "countable \<D>" and \<D>: "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = box a b" "\<Union>\<D> = T"
- using open_countable_Union_open_box that \<open>open T\<close> by metis
- then have eq: "{x \<in> S. f x \<in> T} = (\<Union>U \<in> \<D>. {x \<in> S. f x \<in> U})"
- by blast
- have "{x \<in> S. f x \<in> U} \<in> sets (lebesgue_on S)" if "U \<in> \<D>" for U
- using that T \<D> by blast
- then show ?thesis
- by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \<open>countable \<D>\<close>])
- qed
- moreover
- have eq: "{x \<in> S. f x \<bullet> i < a} = {x \<in> S. f x \<in> {y. y \<bullet> i < a}}" for i a
- by auto
- have "f \<in> borel_measurable (lebesgue_on S)"
- if "\<And>T. open T \<Longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)"
- by (metis (no_types) eq borel_measurable_vimage_halfspace_component_lt open_halfspace_component_lt that)
- ultimately show "?thesis1" "?thesis2"
- by blast+
-qed
-
-
-lemma borel_measurable_vimage_closed:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
- (\<forall>T. closed T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
- (is "?lhs = ?rhs")
-proof -
- have eq: "{x \<in> S. f x \<in> T} = S - {x \<in> S. f x \<in> (- T)}" for T
- by auto
- show ?thesis
- apply (simp add: borel_measurable_vimage_open, safe)
- apply (simp_all (no_asm) add: eq)
- apply (intro sets.Diff sets_lebesgue_on_refl, force simp: closed_open)
- apply (intro sets.Diff sets_lebesgue_on_refl, force simp: open_closed)
- done
-qed
-
-lemma borel_measurable_vimage_closed_interval:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
- (\<forall>a b. {x \<in> S. f x \<in> cbox a b} \<in> sets (lebesgue_on S))"
- (is "?lhs = ?rhs")
-proof
- assume ?lhs then show ?rhs
- using borel_measurable_vimage_closed by blast
-next
- assume RHS: ?rhs
- have "{x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)" if "open T" for T
- proof -
- obtain \<D> where "countable \<D>" and \<D>: "\<D> \<subseteq> Pow T" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = cbox a b" "\<Union>\<D> = T"
- using open_countable_Union_open_cbox that \<open>open T\<close> by metis
- then have eq: "{x \<in> S. f x \<in> T} = (\<Union>U \<in> \<D>. {x \<in> S. f x \<in> U})"
- by blast
- have "{x \<in> S. f x \<in> U} \<in> sets (lebesgue_on S)" if "U \<in> \<D>" for U
- using that \<D> by (metis RHS)
- then show ?thesis
- by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \<open>countable \<D>\<close>])
- qed
- then show ?lhs
- by (simp add: borel_measurable_vimage_open)
-qed
-
-lemma borel_measurable_UNIV_eq: "borel_measurable (lebesgue_on UNIV) = borel_measurable lebesgue"
- by auto
-
-lemma borel_measurable_vimage_borel:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
- (\<forall>T. T \<in> sets borel \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
- (is "?lhs = ?rhs")
-proof
- assume f: ?lhs
- then show ?rhs
- using measurable_sets [OF f]
- by (simp add: Collect_conj_eq inf_sup_aci(1) space_restrict_space vimage_def)
-qed (simp add: borel_measurable_vimage_open_interval)
-
-lemma lebesgue_measurable_vimage_borel:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes "f \<in> borel_measurable lebesgue" "T \<in> sets borel"
- shows "{x. f x \<in> T} \<in> sets lebesgue"
- using assms borel_measurable_vimage_borel [of f UNIV] by auto
-
-lemma borel_measurable_if_I:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes f: "f \<in> borel_measurable (lebesgue_on S)" and S: "S \<in> sets lebesgue"
- shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
-proof -
- have eq: "{x. x \<notin> S} \<union> {x. f x \<in> Y} = {x. x \<notin> S} \<union> {x. f x \<in> Y} \<inter> S" for Y
- by blast
- show ?thesis
- using f S
- apply (simp add: vimage_def in_borel_measurable_borel Ball_def)
- apply (elim all_forward imp_forward asm_rl)
- apply (simp only: Collect_conj_eq Collect_disj_eq imp_conv_disj eq)
- apply (auto simp: Compl_eq [symmetric] Compl_in_sets_lebesgue sets_restrict_space_iff)
- done
-qed
-
-lemma borel_measurable_if_D:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
- shows "f \<in> borel_measurable (lebesgue_on S)"
- using assms
- apply (simp add: in_borel_measurable_borel Ball_def)
- apply (elim all_forward imp_forward asm_rl)
- apply (force simp: space_restrict_space sets_restrict_space image_iff intro: rev_bexI)
- done
-
-lemma borel_measurable_if:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- assumes "S \<in> sets lebesgue"
- shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S)"
- using assms borel_measurable_if_D borel_measurable_if_I by blast
-
-lemma borel_measurable_lebesgue_preimage_borel:
- fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
- shows "f \<in> borel_measurable lebesgue \<longleftrightarrow>
- (\<forall>T. T \<in> sets borel \<longrightarrow> {x. f x \<in> T} \<in> sets lebesgue)"
- apply (intro iffI allI impI lebesgue_measurable_vimage_borel)
- apply (auto simp: in_borel_measurable_borel vimage_def)
- done
-
subsection \<open>Lebesgue sets and continuous images\<close>
proposition lebesgue_regular_inner:
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Sep 12 14:22:47 2019 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Sep 12 14:51:50 2019 +0100
@@ -494,6 +494,11 @@
shows "(f has_integral y) S \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) S"
using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
+lemma has_integral_divide:
+ fixes c :: "_ :: real_normed_div_algebra"
+ shows "(f has_integral y) S \<Longrightarrow> ((\<lambda>x. f x / c) has_integral (y / c)) S"
+ unfolding divide_inverse by (simp add: has_integral_mult_left)
+
text\<open>The case analysis eliminates the condition \<^term>\<open>f integrable_on S\<close> at the cost
of the type class constraint \<open>division_ring\<close>\<close>
corollary integral_mult_left [simp]:
@@ -2735,6 +2740,34 @@
shows "(\<lambda>x. x) integrable_on {a..b}"
by (metis atLeastatMost_empty_iff integrable_on_def has_integral_empty ident_has_integral)
+lemma integral_sin [simp]:
+ fixes a::real
+ assumes "a \<le> b" shows "integral {a..b} sin = cos a - cos b"
+proof -
+ have "(sin has_integral (- cos b - - cos a)) {a..b}"
+ proof (rule fundamental_theorem_of_calculus)
+ show "((\<lambda>a. - cos a) has_vector_derivative sin x) (at x within {a..b})" for x
+ unfolding has_field_derivative_iff_has_vector_derivative [symmetric]
+ by (rule derivative_eq_intros | force)+
+ qed (use assms in auto)
+ then show ?thesis
+ by (simp add: integral_unique)
+qed
+
+lemma integral_cos [simp]:
+ fixes a::real
+ assumes "a \<le> b" shows "integral {a..b} cos = sin b - sin a"
+proof -
+ have "(cos has_integral (sin b - sin a)) {a..b}"
+ proof (rule fundamental_theorem_of_calculus)
+ show "(sin has_vector_derivative cos x) (at x within {a..b})" for x
+ unfolding has_field_derivative_iff_has_vector_derivative [symmetric]
+ by (rule derivative_eq_intros | force)+
+ qed (use assms in auto)
+ then show ?thesis
+ by (simp add: integral_unique)
+qed
+
subsection \<open>Taylor series expansion\<close>
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Thu Sep 12 14:22:47 2019 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Thu Sep 12 14:51:50 2019 +0100
@@ -462,8 +462,232 @@
using integral_restrict_Int [of S UNIV f] assms
by (simp add: lebesgue_on_UNIV_eq)
+lemma integrable_lebesgue_on_empty [iff]:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{second_countable_topology,banach}"
+ shows "integrable (lebesgue_on {}) f"
+ by (simp add: integrable_restrict_space)
-text\<^marker>\<open>tag unimportant\<close> \<open>Measurability of continuous functions\<close>
+lemma integral_lebesgue_on_empty [simp]:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{second_countable_topology,banach}"
+ shows "integral\<^sup>L (lebesgue_on {}) f = 0"
+ by (simp add: Bochner_Integration.integral_empty)
+lemma has_bochner_integral_restrict_space:
+ fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+ assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
+ shows "has_bochner_integral (restrict_space M \<Omega>) f i
+ \<longleftrightarrow> has_bochner_integral M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) i"
+ by (simp add: integrable_restrict_space [OF assms] integral_restrict_space [OF assms] has_bochner_integral_iff)
+
+lemma integrable_restrict_UNIV:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
+ assumes S: "S \<in> sets lebesgue"
+ shows "integrable lebesgue (\<lambda>x. if x \<in> S then f x else 0) \<longleftrightarrow> integrable (lebesgue_on S) f"
+ using has_bochner_integral_restrict_space [of S lebesgue f] assms
+ by (simp add: integrable.simps indicator_scaleR_eq_if)
+
+lemma integral_mono_lebesgue_on_AE:
+ fixes f::"_ \<Rightarrow> real"
+ assumes f: "integrable (lebesgue_on T) f"
+ and gf: "AE x in (lebesgue_on S). g x \<le> f x"
+ and f0: "AE x in (lebesgue_on T). 0 \<le> f x"
+ and "S \<subseteq> T" and S: "S \<in> sets lebesgue" and T: "T \<in> sets lebesgue"
+ shows "(\<integral>x. g x \<partial>(lebesgue_on S)) \<le> (\<integral>x. f x \<partial>(lebesgue_on T))"
+proof -
+ have "(\<integral>x. g x \<partial>(lebesgue_on S)) = (\<integral>x. (if x \<in> S then g x else 0) \<partial>lebesgue)"
+ by (simp add: Lebesgue_Measure.integral_restrict_UNIV S)
+ also have "\<dots> \<le> (\<integral>x. (if x \<in> T then f x else 0) \<partial>lebesgue)"
+ proof (rule Bochner_Integration.integral_mono_AE')
+ show "integrable lebesgue (\<lambda>x. if x \<in> T then f x else 0)"
+ by (simp add: integrable_restrict_UNIV T f)
+ show "AE x in lebesgue. (if x \<in> S then g x else 0) \<le> (if x \<in> T then f x else 0)"
+ using assms by (auto simp: AE_restrict_space_iff)
+ show "AE x in lebesgue. 0 \<le> (if x \<in> T then f x else 0)"
+ using f0 by (simp add: AE_restrict_space_iff T)
+ qed
+ also have "\<dots> = (\<integral>x. f x \<partial>(lebesgue_on T))"
+ using Lebesgue_Measure.integral_restrict_UNIV T by blast
+ finally show ?thesis .
+qed
+
+
+subsection \<open>Borel measurability\<close>
+
+lemma borel_measurable_if_I:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes f: "f \<in> borel_measurable (lebesgue_on S)" and S: "S \<in> sets lebesgue"
+ shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
+proof -
+ have eq: "{x. x \<notin> S} \<union> {x. f x \<in> Y} = {x. x \<notin> S} \<union> {x. f x \<in> Y} \<inter> S" for Y
+ by blast
+ show ?thesis
+ using f S
+ apply (simp add: vimage_def in_borel_measurable_borel Ball_def)
+ apply (elim all_forward imp_forward asm_rl)
+ apply (simp only: Collect_conj_eq Collect_disj_eq imp_conv_disj eq)
+ apply (auto simp: Compl_eq [symmetric] Compl_in_sets_lebesgue sets_restrict_space_iff)
+ done
+qed
+
+lemma borel_measurable_if_D:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
+ shows "f \<in> borel_measurable (lebesgue_on S)"
+ using assms
+ apply (simp add: in_borel_measurable_borel Ball_def)
+ apply (elim all_forward imp_forward asm_rl)
+ apply (force simp: space_restrict_space sets_restrict_space image_iff intro: rev_bexI)
+ done
+
+lemma borel_measurable_if:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "S \<in> sets lebesgue"
+ shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S)"
+ using assms borel_measurable_if_D borel_measurable_if_I by blast
+
+lemma borel_measurable_vimage_halfspace_component_lt:
+ "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+ (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i < a} \<in> sets (lebesgue_on S))"
+ apply (rule trans [OF borel_measurable_iff_halfspace_less])
+ apply (fastforce simp add: space_restrict_space)
+ done
+
+lemma borel_measurable_vimage_halfspace_component_ge:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+ (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<ge> a} \<in> sets (lebesgue_on S))"
+ apply (rule trans [OF borel_measurable_iff_halfspace_ge])
+ apply (fastforce simp add: space_restrict_space)
+ done
+
+lemma borel_measurable_vimage_halfspace_component_gt:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+ (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i > a} \<in> sets (lebesgue_on S))"
+ apply (rule trans [OF borel_measurable_iff_halfspace_greater])
+ apply (fastforce simp add: space_restrict_space)
+ done
+
+lemma borel_measurable_vimage_halfspace_component_le:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+ (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<le> a} \<in> sets (lebesgue_on S))"
+ apply (rule trans [OF borel_measurable_iff_halfspace_le])
+ apply (fastforce simp add: space_restrict_space)
+ done
+
+lemma
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows borel_measurable_vimage_open_interval:
+ "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+ (\<forall>a b. {x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S))" (is ?thesis1)
+ and borel_measurable_vimage_open:
+ "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+ (\<forall>T. open T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))" (is ?thesis2)
+proof -
+ have "{x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S)" if "f \<in> borel_measurable (lebesgue_on S)" for a b
+ proof -
+ have "S = S \<inter> space lebesgue"
+ by simp
+ then have "S \<inter> (f -` box a b) \<in> sets (lebesgue_on S)"
+ by (metis (no_types) box_borel in_borel_measurable_borel inf_sup_aci(1) space_restrict_space that)
+ then show ?thesis
+ by (simp add: Collect_conj_eq vimage_def)
+ qed
+ moreover
+ have "{x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)"
+ if T: "\<And>a b. {x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S)" "open T" for T
+ proof -
+ obtain \<D> where "countable \<D>" and \<D>: "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = box a b" "\<Union>\<D> = T"
+ using open_countable_Union_open_box that \<open>open T\<close> by metis
+ then have eq: "{x \<in> S. f x \<in> T} = (\<Union>U \<in> \<D>. {x \<in> S. f x \<in> U})"
+ by blast
+ have "{x \<in> S. f x \<in> U} \<in> sets (lebesgue_on S)" if "U \<in> \<D>" for U
+ using that T \<D> by blast
+ then show ?thesis
+ by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \<open>countable \<D>\<close>])
+ qed
+ moreover
+ have eq: "{x \<in> S. f x \<bullet> i < a} = {x \<in> S. f x \<in> {y. y \<bullet> i < a}}" for i a
+ by auto
+ have "f \<in> borel_measurable (lebesgue_on S)"
+ if "\<And>T. open T \<Longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)"
+ by (metis (no_types) eq borel_measurable_vimage_halfspace_component_lt open_halfspace_component_lt that)
+ ultimately show "?thesis1" "?thesis2"
+ by blast+
+qed
+
+lemma borel_measurable_vimage_closed:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+ (\<forall>T. closed T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
+ (is "?lhs = ?rhs")
+proof -
+ have eq: "{x \<in> S. f x \<in> T} = S - {x \<in> S. f x \<in> (- T)}" for T
+ by auto
+ show ?thesis
+ apply (simp add: borel_measurable_vimage_open, safe)
+ apply (simp_all (no_asm) add: eq)
+ apply (intro sets.Diff sets_lebesgue_on_refl, force simp: closed_open)
+ apply (intro sets.Diff sets_lebesgue_on_refl, force simp: open_closed)
+ done
+qed
+
+lemma borel_measurable_vimage_closed_interval:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+ (\<forall>a b. {x \<in> S. f x \<in> cbox a b} \<in> sets (lebesgue_on S))"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ using borel_measurable_vimage_closed by blast
+next
+ assume RHS: ?rhs
+ have "{x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)" if "open T" for T
+ proof -
+ obtain \<D> where "countable \<D>" and \<D>: "\<D> \<subseteq> Pow T" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = cbox a b" "\<Union>\<D> = T"
+ using open_countable_Union_open_cbox that \<open>open T\<close> by metis
+ then have eq: "{x \<in> S. f x \<in> T} = (\<Union>U \<in> \<D>. {x \<in> S. f x \<in> U})"
+ by blast
+ have "{x \<in> S. f x \<in> U} \<in> sets (lebesgue_on S)" if "U \<in> \<D>" for U
+ using that \<D> by (metis RHS)
+ then show ?thesis
+ by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \<open>countable \<D>\<close>])
+ qed
+ then show ?lhs
+ by (simp add: borel_measurable_vimage_open)
+qed
+
+lemma borel_measurable_UNIV_eq: "borel_measurable (lebesgue_on UNIV) = borel_measurable lebesgue"
+ by auto
+
+lemma borel_measurable_vimage_borel:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+ (\<forall>T. T \<in> sets borel \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
+ (is "?lhs = ?rhs")
+proof
+ assume f: ?lhs
+ then show ?rhs
+ using measurable_sets [OF f]
+ by (simp add: Collect_conj_eq inf_sup_aci(1) space_restrict_space vimage_def)
+qed (simp add: borel_measurable_vimage_open_interval)
+
+lemma lebesgue_measurable_vimage_borel:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "f \<in> borel_measurable lebesgue" "T \<in> sets borel"
+ shows "{x. f x \<in> T} \<in> sets lebesgue"
+ using assms borel_measurable_vimage_borel [of f UNIV] by auto
+
+lemma borel_measurable_lebesgue_preimage_borel:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ shows "f \<in> borel_measurable lebesgue \<longleftrightarrow>
+ (\<forall>T. T \<in> sets borel \<longrightarrow> {x. f x \<in> T} \<in> sets lebesgue)"
+ apply (intro iffI allI impI lebesgue_measurable_vimage_borel)
+ apply (auto simp: in_borel_measurable_borel vimage_def)
+ done
+
+
+subsection \<^marker>\<open>tag unimportant\<close> \<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"
--- a/src/HOL/Analysis/Linear_Algebra.thy Thu Sep 12 14:22:47 2019 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Thu Sep 12 14:51:50 2019 +0100
@@ -1879,4 +1879,88 @@
orthogonal_commute orthogonal_def)
qed
+subsection\<open>Linear functions are (uniformly) continuous on any set\<close>
+
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological properties of linear functions\<close>
+
+lemma linear_lim_0:
+ assumes "bounded_linear f"
+ shows "(f \<longlongrightarrow> 0) (at (0))"
+proof -
+ interpret f: bounded_linear f by fact
+ have "(f \<longlongrightarrow> f 0) (at 0)"
+ using tendsto_ident_at by (rule f.tendsto)
+ then show ?thesis unfolding f.zero .
+qed
+
+lemma linear_continuous_at:
+ assumes "bounded_linear f"
+ shows "continuous (at a) f"
+ unfolding continuous_at using assms
+ apply (rule bounded_linear.tendsto)
+ apply (rule tendsto_ident_at)
+ done
+
+lemma linear_continuous_within:
+ "bounded_linear f \<Longrightarrow> continuous (at x within s) f"
+ using continuous_at_imp_continuous_at_within linear_continuous_at by blast
+
+lemma linear_continuous_on:
+ "bounded_linear f \<Longrightarrow> continuous_on s f"
+ using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
+
+lemma Lim_linear:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" and h :: "'b \<Rightarrow> 'c::real_normed_vector"
+ assumes "(f \<longlongrightarrow> l) F" "linear h"
+ shows "((\<lambda>x. h(f x)) \<longlongrightarrow> h l) F"
+proof -
+ obtain B where B: "B > 0" "\<And>x. norm (h x) \<le> B * norm x"
+ using linear_bounded_pos [OF \<open>linear h\<close>] by blast
+ show ?thesis
+ unfolding tendsto_iff
+ proof (intro allI impI)
+ show "\<forall>\<^sub>F x in F. dist (h (f x)) (h l) < e" if "e > 0" for e
+ proof -
+ have "\<forall>\<^sub>F x in F. dist (f x) l < e/B"
+ by (simp add: \<open>0 < B\<close> assms(1) tendstoD that)
+ then show ?thesis
+ unfolding dist_norm
+ proof (rule eventually_mono)
+ show "norm (h (f x) - h l) < e" if "norm (f x - l) < e / B" for x
+ using that B
+ apply (simp add: divide_simps)
+ by (metis \<open>linear h\<close> le_less_trans linear_diff mult.commute)
+ qed
+ qed
+ qed
+qed
+
+lemma linear_continuous_compose:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" and g :: "'b \<Rightarrow> 'c::real_normed_vector"
+ assumes "continuous F f" "linear g"
+ shows "continuous F (\<lambda>x. g(f x))"
+ using assms unfolding continuous_def by (rule Lim_linear)
+
+lemma linear_continuous_on_compose:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" and g :: "'b \<Rightarrow> 'c::real_normed_vector"
+ assumes "continuous_on S f" "linear g"
+ shows "continuous_on S (\<lambda>x. g(f x))"
+ using assms by (simp add: continuous_on_eq_continuous_within linear_continuous_compose)
+
+text\<open>Also bilinear functions, in composition form\<close>
+
+lemma bilinear_continuous_compose:
+ fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
+ assumes "continuous F f" "continuous F g" "bilinear h"
+ shows "continuous F (\<lambda>x. h (f x) (g x))"
+ using assms bilinear_conv_bounded_bilinear bounded_bilinear.continuous by blast
+
+lemma bilinear_continuous_on_compose:
+ fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
+ and f :: "'d::t2_space \<Rightarrow> 'a"
+ assumes "continuous_on S f" "continuous_on S g" "bilinear h"
+ shows "continuous_on S (\<lambda>x. h (f x) (g x))"
+ using assms by (simp add: continuous_on_eq_continuous_within bilinear_continuous_compose)
+
+
end
--- a/src/HOL/Library/Landau_Symbols.thy Thu Sep 12 14:22:47 2019 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy Thu Sep 12 14:51:50 2019 +0100
@@ -1641,10 +1641,6 @@
subsection \<open>Asymptotic Equivalence\<close>
-(* TODO Move *)
-lemma tendsto_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
- by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
-
named_theorems asymp_equiv_intros
named_theorems asymp_equiv_simps
@@ -1676,7 +1672,7 @@
by (intro always_eventually) simp
moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
- by (simp add: Landau_Symbols.tendsto_eventually)
+ by (simp add: tendsto_eventually)
qed
lemma asymp_equiv_symI:
--- a/src/HOL/Limits.thy Thu Sep 12 14:22:47 2019 +0200
+++ b/src/HOL/Limits.thy Thu Sep 12 14:51:50 2019 +0100
@@ -779,6 +779,14 @@
for c :: "'a::topological_semigroup_mult"
by (rule tendsto_mult [OF _ tendsto_const])
+lemma real_tendsto_mult_left_iff:
+ "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. c * f x) (c * l) F \<longleftrightarrow> tendsto f l F" for c :: real
+ by (auto simp: tendsto_mult_left dest: tendsto_mult_left [where c = "1/c"])
+
+lemma real_tendsto_mult_right_iff:
+ "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. f x * c) (l * c) F \<longleftrightarrow> tendsto f l F" for c :: real
+ by (simp add: mult.commute real_tendsto_mult_left_iff)
+
lemma lim_const_over_n [tendsto_intros]:
fixes a :: "'a::real_normed_field"
shows "(\<lambda>n. a / of_nat n) \<longlonglongrightarrow> 0"
--- a/src/HOL/Power.thy Thu Sep 12 14:22:47 2019 +0200
+++ b/src/HOL/Power.thy Thu Sep 12 14:51:50 2019 +0100
@@ -895,6 +895,11 @@
apply simp
done
+lemma dvd_power_iff_le:
+ fixes k::nat
+ shows "2 \<le> k \<Longrightarrow> ((k ^ m) dvd (k ^ n) \<longleftrightarrow> m \<le> n)"
+ using le_imp_power_dvd power_dvd_imp_le by force
+
lemma power2_nat_le_eq_le: "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n"
for m n :: nat
by (auto intro: power2_le_imp_le power_mono)
--- a/src/HOL/Probability/Tree_Space.thy Thu Sep 12 14:22:47 2019 +0200
+++ b/src/HOL/Probability/Tree_Space.thy Thu Sep 12 14:51:50 2019 +0100
@@ -247,13 +247,6 @@
by (auto simp: sets_restrict_space_iff space_restrict_space)
qed
-lemma measurable_restrict_mono:
- assumes f: "f \<in> restrict_space M A \<rightarrow>\<^sub>M N" and "B \<subseteq> A"
- shows "f \<in> restrict_space M B \<rightarrow>\<^sub>M N"
-by (rule measurable_compose[OF measurable_restrict_space3 f])
- (insert \<open>B \<subseteq> A\<close>, auto)
-
-
lemma measurable_value[measurable (raw)]:
assumes "f \<in> X \<rightarrow>\<^sub>M tree_sigma M"
and "\<And>x. x \<in> space X \<Longrightarrow> f x \<noteq> Leaf"