--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Dec 26 21:28:20 2022 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Dec 27 10:38:34 2022 +0000
@@ -83,11 +83,8 @@
lemma retraction_openin_vimage_iff:
"openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
- if retraction: "retraction S T r" and "U \<subseteq> T"
- using retraction apply (rule retractionE)
- apply (rule continuous_right_inverse_imp_quotient_map [where g=r])
- using \<open>U \<subseteq> T\<close> apply (auto elim: continuous_on_subset)
- done
+ if "retraction S T r" and "U \<subseteq> T"
+ by (simp add: retraction_openin_vimage_iff that)
lemma retract_of_locally_compact:
fixes S :: "'a :: {heine_borel,real_normed_vector} set"
@@ -251,7 +248,7 @@
then obtain u l where "l \<in> s" "\<forall>b\<in>s. l \<le> b" "u \<in> s" "\<forall>b\<in>s. b \<le> u"
using insert by auto
with * show "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. a \<le> x" "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. x \<le> a"
- using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
+ by (metis insert_iff order.trans)+
qed auto
lemma kuhn_labelling_lemma:
@@ -1081,7 +1078,7 @@
qed }
with ks_f' eq \<open>a \<noteq> b.enum 0\<close> \<open>n \<noteq> 0\<close> show ?thesis
apply (intro ex1I[of _ "b.enum ` {.. n}"])
- apply auto []
+ apply fastforce
apply metis
done
next
@@ -1111,16 +1108,11 @@
have "{i} \<subseteq> {..n}"
using i by auto
{ fix j assume "j \<le> n"
- moreover have "j < i \<or> i = j \<or> i < j" by arith
- moreover note i
- ultimately have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
- apply (simp only: fun_eq_iff enum_def b.enum_def flip: image_comp)
+ with i Suc_i' have "enum j = b.enum j \<longleftrightarrow> j \<noteq> i"
+ unfolding fun_eq_iff enum_def b.enum_def image_comp [symmetric]
apply (cases \<open>i = j\<close>)
- apply simp
- apply (metis Suc_i' \<open>i \<le> n\<close> imageI in_upd_image lessI lessThan_iff lessThan_subset_iff less_irrefl_nat transpose_apply_second transpose_commute)
- apply (subst transpose_image_eq)
- apply (auto simp add: i'_def)
- done
+ apply (metis imageI in_upd_image lessI lessThan_iff lessThan_subset_iff order_less_le transpose_apply_first)
+ by (metis lessThan_iff linorder_not_less not_less_eq_eq order_less_le transpose_image_eq)
}
note enum_eq_benum = this
then have "enum ` ({.. n} - {i}) = b.enum ` ({.. n} - {i})"
@@ -1295,7 +1287,7 @@
lemma reduced_labelling_unique:
"r \<le> n \<Longrightarrow> \<forall>i<r. x i = 0 \<Longrightarrow> r = n \<or> x r \<noteq> 0 \<Longrightarrow> reduced n x = r"
- unfolding reduced_def by (rule LeastI2_wellorder[where a=n]) (metis le_less not_le)+
+ by (metis linorder_less_linear linorder_not_le reduced_labelling)
lemma reduced_labelling_zero: "j < n \<Longrightarrow> x j = 0 \<Longrightarrow> reduced n x \<noteq> j"
using reduced_labelling[of n x] by auto
@@ -1369,7 +1361,7 @@
by (auto simp: out_eq_p)
moreover
{ fix x assume "x \<in> s"
- with lab_1[rule_format, of n x] all_eq_p s_le_p[of x]
+ with lab_1[rule_format, of n x] all_eq_p s_le_p[of x]
have "?rl x \<le> n"
by (auto intro!: reduced_labelling_nonzero)
then have "?rl x = reduced n (lab x)"
@@ -1532,34 +1524,9 @@
(\<forall>x i. P x \<and> Q i \<and> x i = 1 \<longrightarrow> l x i = 1) \<and>
(\<forall>x i. P x \<and> Q i \<and> l x i = 0 \<longrightarrow> x i \<le> f x i) \<and>
(\<forall>x i. P x \<and> Q i \<and> l x i = 1 \<longrightarrow> f x i \<le> x i)"
-proof -
- have and_forall_thm: "\<And>P Q. (\<forall>x. P x) \<and> (\<forall>x. Q x) \<longleftrightarrow> (\<forall>x. P x \<and> Q x)"
- by auto
- have *: "\<forall>x y::real. 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow> x \<noteq> 1 \<and> x \<le> y \<or> x \<noteq> 0 \<and> y \<le> x"
- by auto
- show ?thesis
- unfolding and_forall_thm
- apply (subst choice_iff[symmetric])+
- apply rule
- apply rule
- proof -
- fix x x'
- let ?R = "\<lambda>y::nat.
- (P x \<and> Q x' \<and> x x' = 0 \<longrightarrow> y = 0) \<and>
- (P x \<and> Q x' \<and> x x' = 1 \<longrightarrow> y = 1) \<and>
- (P x \<and> Q x' \<and> y = 0 \<longrightarrow> x x' \<le> (f x) x') \<and>
- (P x \<and> Q x' \<and> y = 1 \<longrightarrow> (f x) x' \<le> x x')"
- have "0 \<le> f x x' \<and> f x x' \<le> 1" if "P x" "Q x'"
- using assms(2)[rule_format,of "f x" x'] that
- apply (drule_tac assms(1)[rule_format])
- apply auto
- done
- then have "?R 0 \<or> ?R 1"
- by auto
- then show "\<exists>y\<le>1. ?R y"
- by auto
- qed
-qed
+ unfolding all_conj_distrib [symmetric]
+ apply (subst choice_iff[symmetric])+
+ by (metis assms bot_nat_0.extremum nle_le zero_neq_one)
subsection \<open>Brouwer's fixed point theorem\<close>
@@ -1785,11 +1752,7 @@
using b' unfolding bij_betw_def by auto
define r' ::'a where "r' = (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i)"
have "\<And>i. i \<in> Basis \<Longrightarrow> r (b' i) \<le> p"
- apply (rule order_trans)
- apply (rule rs(1)[OF b'_im,THEN conjunct2])
- using q(1)[rule_format,OF b'_im]
- apply (auto simp: Suc_le_eq)
- done
+ using b'_im q(1) rs(1) by fastforce
then have "r' \<in> cbox 0 One"
unfolding r'_def cbox_def
using b'_Basis
@@ -1899,9 +1862,8 @@
have "\<exists>x\<in> cball 0 e. (f \<circ> closest_point S) x = x"
proof (rule_tac brouwer_ball[OF e(1)])
show "continuous_on (cball 0 e) (f \<circ> closest_point S)"
- apply (rule continuous_on_compose)
- using S compact_eq_bounded_closed continuous_on_closest_point apply blast
- by (meson S contf closest_point_in_set compact_imp_closed continuous_on_subset image_subsetI)
+ by (meson assms closest_point_in_set compact_eq_bounded_closed contf continuous_on_closest_point
+ continuous_on_compose continuous_on_subset image_subsetI)
show "(f \<circ> closest_point S) ` cball 0 e \<subseteq> cball 0 e"
by clarsimp (metis S fim closest_point_exists(1) compact_eq_bounded_closed e(2) image_subset_iff mem_cball_0 subsetCE)
qed (use assms in auto)
@@ -2033,9 +1995,7 @@
using \<open>bounded S\<close> bounded_subset_ballD by blast
have notga: "g x \<noteq> a" for x
unfolding g_def using fros fim \<open>a \<notin> T\<close>
- apply (auto simp: frontier_def)
- using fid interior_subset apply fastforce
- by (simp add: \<open>a \<in> S\<close> closure_def)
+ by (metis Un_iff \<open>a \<in> S\<close> closure_Un_frontier fid imageI subset_eq)
define h where "h \<equiv> (\<lambda>y. a + (B / norm(y - a)) *\<^sub>R (y - a)) \<circ> g"
have "\<not> (frontier (cball a B) retract_of (cball a B))"
by (metis no_retraction_cball \<open>0 < B\<close>)
@@ -2119,8 +2079,7 @@
using k \<open>x \<noteq> 0\<close> \<open>0 < dd x\<close>
apply (simp add: in_segment)
apply (rule_tac x = "dd x / k" in exI)
- apply (simp add: field_simps that)
- apply (simp add: vector_add_divide_simps algebra_simps)
+ apply (simp add: that vector_add_divide_simps algebra_simps)
done
ultimately show ?thesis
using segsub by (auto simp: rel_frontier_def)
@@ -2163,8 +2122,7 @@
then have "\<not> dd (x - a) \<le> 0 \<and> a + dd (x - a) *\<^sub>R (x - a) \<in> rel_frontier S"
using \<open>x \<noteq> a\<close> dd1 by fastforce
with \<open>x \<noteq> a\<close> show "(1 - u) *\<^sub>R x + u *\<^sub>R (a + dd (x - a) *\<^sub>R (x - a)) \<noteq> a"
- apply (auto simp: iff)
- using less_eq_real_def mult_le_0_iff not_less u by fastforce
+ using less_eq_real_def mult_le_0_iff not_less u by (fastforce simp: iff)
qed
qed
show "retraction (T - {a}) (rel_frontier S) (\<lambda>x. a + dd (x - a) *\<^sub>R (x - a))"
@@ -2216,9 +2174,8 @@
fixes S :: "'a::euclidean_space set"
assumes "bounded S" "convex S" "a \<in> rel_interior S"
shows "rel_frontier S retract_of (affine hull S - {a})"
-apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S "affine hull S" a])
-apply (auto simp: affine_imp_convex rel_frontier_affine_hull retract_of_def assms)
-done
+ by (meson assms convex_affine_hull dual_order.refl rel_frontier_affine_hull
+ rel_frontier_deformation_retract_of_punctured_convex retract_of_def)
corollary rel_boundary_retract_of_punctured_affine_hull:
fixes S :: "'a::euclidean_space set"
@@ -2231,29 +2188,24 @@
fixes S :: "'a::euclidean_space set"
assumes "convex S" "bounded S" "a \<in> rel_interior S" "convex T" "rel_frontier S \<subseteq> T" "T \<subseteq> affine hull S"
shows "(rel_frontier S) homotopy_eqv (T - {a})"
- apply (rule rel_frontier_deformation_retract_of_punctured_convex [of S T])
- using assms
- apply auto
- using deformation_retract_imp_homotopy_eqv homotopy_equivalent_space_sym by blast
+ by (meson assms deformation_retract_imp_homotopy_eqv homotopy_equivalent_space_sym
+ rel_frontier_deformation_retract_of_punctured_convex[of S T])
lemma homotopy_eqv_rel_frontier_punctured_affine_hull:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "bounded S" "a \<in> rel_interior S"
shows "(rel_frontier S) homotopy_eqv (affine hull S - {a})"
-apply (rule homotopy_eqv_rel_frontier_punctured_convex)
- using assms rel_frontier_affine_hull by force+
+ by (simp add: assms homotopy_eqv_rel_frontier_punctured_convex rel_frontier_affine_hull)
lemma path_connected_sphere_gen:
assumes "convex S" "bounded S" "aff_dim S \<noteq> 1"
shows "path_connected(rel_frontier S)"
-proof (cases "rel_interior S = {}")
- case True
+proof -
+ have "convex (closure S)"
+ using assms by auto
then show ?thesis
- by (simp add: \<open>convex S\<close> convex_imp_path_connected rel_frontier_def)
-next
- case False
- then show ?thesis
- by (metis aff_dim_affine_hull affine_affine_hull affine_imp_convex all_not_in_conv assms path_connected_punctured_convex rel_frontier_retract_of_punctured_affine_hull retract_of_path_connected)
+ by (metis Diff_empty aff_dim_affine_hull assms convex_affine_hull convex_imp_path_connected equals0I
+ path_connected_punctured_convex rel_frontier_def rel_frontier_retract_of_punctured_affine_hull retract_of_path_connected)
qed
lemma connected_sphere_gen:
@@ -2282,8 +2234,7 @@
then show ?thesis
apply (simp add: path_def path_image_def pathstart_def pathfinish_def homotopic_with_def)
apply (rule_tac x = "\<lambda>z. inverse(norm(snd z - (g \<circ> fst)z)) *\<^sub>R (snd z - (g \<circ> fst)z)" in exI)
- apply (intro conjI continuous_intros)
- apply (rule continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+
+ apply (rule conjI continuous_intros | erule continuous_on_subset | fastforce simp: divide_simps sphere_def)+
done
qed
@@ -2315,8 +2266,8 @@
using ball_subset_cball [of a r] r by auto
have cont1: "continuous_on (s \<union> connected_component_set (- s) a)
(\<lambda>x. a + r *\<^sub>R g x)"
- apply (rule continuous_intros)+
- using \<open>continuous_on (s \<union> c) g\<close> ceq by blast
+ using \<open>continuous_on (s \<union> c) g\<close> ceq
+ by (intro continuous_intros) blast
have cont2: "continuous_on (cball a r - connected_component_set (- s) a)
(\<lambda>x. a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
by (rule continuous_intros | force simp: \<open>a \<notin> s\<close>)+
@@ -2326,10 +2277,8 @@
else a + r *\<^sub>R ((x - a) /\<^sub>R norm (x - a)))"
apply (subst cb_eq)
apply (rule continuous_on_cases [OF _ _ cont1 cont2])
- using ceq cin
- apply (auto intro: closed_Un_complement_component
- simp: \<open>closed s\<close> open_Compl open_connected_component)
- done
+ using \<open>closed s\<close> ceq cin
+ by (force simp: closed_Diff open_Compl closed_Un_complement_component open_connected_component)+
have 2: "(\<lambda>x. a + r *\<^sub>R g x) ` (cball a r \<inter> connected_component_set (- s) a)
\<subseteq> sphere a r "
using \<open>0 < r\<close> by (force simp: dist_norm ceq)
@@ -2384,12 +2333,7 @@
and "x \<in> S"
and "\<And>x y. \<lbrakk>x\<in>S; y\<in>cball a e\<rbrakk> \<Longrightarrow> x + (y - f y) \<in> cball a e"
shows "\<exists>y\<in>cball a e. f y = x"
- apply (rule brouwer_surjective)
- apply (rule compact_cball convex_cball)+
- unfolding cball_eq_empty
- using assms
- apply auto
- done
+ by (smt (verit, best) assms brouwer_surjective cball_eq_empty compact_cball convex_cball)
subsubsection \<open>Inverse function theorem\<close>
@@ -2510,8 +2454,7 @@
lemma has_derivative_inverse_strong:
fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
- assumes "open S"
- and "x \<in> S"
+ assumes S: "open S" "x \<in> S"
and contf: "continuous_on S f"
and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
and derf: "(f has_derivative f') (at x)"
@@ -2524,23 +2467,16 @@
unfolding linear_conv_bounded_linear[symmetric]
using id right_inverse_linear by blast
moreover have "g' \<circ> f' = id"
- using id linf ling
- unfolding linear_conv_bounded_linear[symmetric]
- using linear_inverse_left
- by auto
+ using id linear_inverse_left linear_linear linf ling by blast
moreover have *: "\<And>T. \<lbrakk>T \<subseteq> S; x \<in> interior T\<rbrakk> \<Longrightarrow> f x \<in> interior (f ` T)"
- apply (rule sussmann_open_mapping)
- apply (rule assms ling)+
- apply auto
- done
+ using S derf contf id ling sussmann_open_mapping by blast
have "continuous (at (f x)) g"
unfolding continuous_at Lim_at
- proof (rule, rule)
+ proof (intro strip)
fix e :: real
assume "e > 0"
then have "f x \<in> interior (f ` (ball x e \<inter> S))"
- using *[rule_format,of "ball x e \<inter> S"] \<open>x \<in> S\<close>
- by (auto simp add: interior_open[OF open_ball] interior_open[OF assms(1)])
+ by (simp add: "*" S interior_open)
then obtain d where d: "0 < d" "ball (f x) d \<subseteq> f ` (ball x e \<inter> S)"
unfolding mem_interior by blast
show "\<exists>d>0. \<forall>y. 0 < dist y (f x) \<and> dist y (f x) < d \<longrightarrow> dist (g y) (g (f x)) < e"
@@ -2550,16 +2486,11 @@
then have "g y \<in> g ` f ` (ball x e \<inter> S)"
by (metis d(2) dist_commute mem_ball rev_image_eqI subset_iff)
then show "dist (g y) (g (f x)) < e"
- using gf[OF \<open>x \<in> S\<close>]
- by (simp add: assms(4) dist_commute image_iff)
+ using \<open>x \<in> S\<close> by (simp add: gf dist_commute image_iff)
qed (use d in auto)
qed
moreover have "f x \<in> interior (f ` S)"
- apply (rule sussmann_open_mapping)
- apply (rule assms ling)+
- using interior_open[OF assms(1)] and \<open>x \<in> S\<close>
- apply auto
- done
+ using "*" S interior_eq by blast
moreover have "f (g y) = y" if "y \<in> interior (f ` S)" for y
by (metis gf imageE interiorE subsetD that)
ultimately show ?thesis using assms
@@ -2576,26 +2507,20 @@
and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
and "(f has_derivative f') (at (g y))"
and "f' \<circ> g' = id"
- and "f (g y) = y"
+ and f: "f (g y) = y"
shows "(g has_derivative g') (at y)"
- using has_derivative_inverse_strong[OF assms(1-6)]
- unfolding assms(7)
- by simp
+ using has_derivative_inverse_strong[OF assms(1-6)] by (simp add: f)
text \<open>On a region.\<close>
theorem has_derivative_inverse_on:
fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
assumes "open S"
- and derf: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
+ and "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f'(x)) (at x)"
and "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
and "f' x \<circ> g' x = id"
and "x \<in> S"
shows "(g has_derivative g'(x)) (at (f x))"
-proof (rule has_derivative_inverse_strong[where g'="g' x" and f=f])
- show "continuous_on S f"
- unfolding continuous_on_eq_continuous_at[OF \<open>open S\<close>]
- using derf has_derivative_continuous by blast
-qed (use assms in auto)
+ by (meson assms continuous_on_eq_continuous_at has_derivative_continuous has_derivative_inverse_strong)
end
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Mon Dec 26 21:28:20 2022 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Tue Dec 27 10:38:34 2022 +0000
@@ -145,11 +145,8 @@
proof cases
assume "?R"
with \<open>j \<in> S\<close> psubset.prems have "{u..v} \<subseteq> (\<Union>i\<in>S-{j}. {l i<..< r i})"
- apply (auto simp: subset_eq Ball_def)
- apply (metis Diff_iff less_le_trans leD linear singletonD)
- apply (metis Diff_iff less_le_trans leD linear singletonD)
- apply (metis order_trans less_le_not_le linear)
- done
+ apply (simp add: subset_eq Ball_def Bex_def)
+ by (metis order_le_less_trans order_less_le_trans order_less_not_sym)
with \<open>j \<in> S\<close> have "F v - F u \<le> (\<Sum>i\<in>S - {j}. F (r i) - F (l i))"
by (intro psubset) auto
also have "\<dots> \<le> (\<Sum>i\<in>S. F (r i) - F (l i))"
@@ -162,19 +159,14 @@
by (auto simp: not_less)
let ?S1 = "{i \<in> S. l i < l j}"
let ?S2 = "{i \<in> S. r i > r j}"
-
+ have *: "?S1 \<inter> ?S2 = {}"
+ using j by (fastforce simp add: disjoint_iff)
have "(\<Sum>i\<in>S. F (r i) - F (l i)) \<ge> (\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i))"
using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j
by (intro sum_mono2) (auto intro: less_imp_le)
also have "(\<Sum>i\<in>?S1 \<union> ?S2 \<union> {j}. F (r i) - F (l i)) =
(\<Sum>i\<in>?S1. F (r i) - F (l i)) + (\<Sum>i\<in>?S2 . F (r i) - F (l i)) + (F (r j) - F (l j))"
- using psubset(1) psubset.prems(1) j
- apply (subst sum.union_disjoint)
- apply simp_all
- apply (subst sum.union_disjoint)
- apply auto
- apply (metis less_le_not_le)
- done
+ using psubset(1) by (simp add: * sum.union_disjoint disjoint_iff_not_equal)
also (xtrans) have "(\<Sum>i\<in>?S1. F (r i) - F (l i)) \<ge> F (l j) - F u"
using \<open>j \<in> S\<close> \<open>finite S\<close> psubset.prems j
apply (intro psubset.IH psubset)
@@ -202,31 +194,24 @@
proof
fix i
note right_cont_F [of "r i"]
+ then have "\<exists>d>0. F (r i + d) - F (r i) < epsilon / 2 ^ (i + 2)"
+ by (simp add: continuous_at_right_real_increasing egt0)
thus "\<exists>d>0. F (r i + d) < F (r i) + epsilon / 2^(i+2)"
- apply -
- apply (subst (asm) continuous_at_right_real_increasing)
- apply (rule mono_F, assumption)
- apply (drule_tac x = "epsilon / 2 ^ (i + 2)" in spec)
- apply (erule impE)
- using egt0 by (auto simp add: field_simps)
+ by force
qed
then obtain delta where
deltai_gt0: "\<And>i. delta i > 0" and
deltai_prop: "\<And>i. F (r i + delta i) < F (r i) + epsilon / 2^(i+2)"
by metis
have "\<exists>a' > a. F a' - F a < epsilon / 2"
- apply (insert right_cont_F [of a])
- apply (subst (asm) continuous_at_right_real_increasing)
- using mono_F apply force
- apply (drule_tac x = "epsilon / 2" in spec)
- using egt0 unfolding mult.commute [of 2] by force
+ using right_cont_F [of a]
+ by (metis continuous_at_right_real_increasing egt0 half_gt_zero less_add_same_cancel1 mono_F)
then obtain a' where a'lea [arith]: "a' > a" and
a_prop: "F a' - F a < epsilon / 2"
by auto
define S' where "S' = {i. l i < r i}"
- obtain S :: "nat set" where
- "S \<subseteq> S'" and finS: "finite S" and
- Sprop: "{a'..b} \<subseteq> (\<Union>i \<in> S. {l i<..<r i + delta i})"
+ obtain S :: "nat set" where "S \<subseteq> S'" and finS: "finite S"
+ and Sprop: "{a'..b} \<subseteq> (\<Union>i \<in> S. {l i<..<r i + delta i})"
proof (rule compactE_image)
show "compact {a'..b}"
by (rule compact_Icc)
@@ -236,58 +221,34 @@
also have "{a <.. b} = (\<Union>i\<in>S'. {l i<..r i})"
unfolding lr_eq_ab[symmetric] by (fastforce simp add: S'_def intro: less_le_trans)
also have "\<dots> \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})"
- apply (intro UN_mono)
- apply (auto simp: S'_def)
- apply (cut_tac i=i in deltai_gt0)
- apply simp
- done
+ by (intro UN_mono; simp add: add.commute add_strict_increasing deltai_gt0 subset_iff)
finally show "{a'..b} \<subseteq> (\<Union>i \<in> S'. {l i<..<r i + delta i})" .
qed
with S'_def have Sprop2: "\<And>i. i \<in> S \<Longrightarrow> l i < r i" by auto
- from finS have "\<exists>n. \<forall>i \<in> S. i \<le> n"
- by (subst finite_nat_set_iff_bounded_le [symmetric])
- then obtain n where Sbound [rule_format]: "\<forall>i \<in> S. i \<le> n" ..
- have "F b - F a' \<le> (\<Sum>i\<in>S. F (r i + delta i) - F (l i))"
- apply (rule claim2 [rule_format])
- using finS Sprop apply auto
- apply (frule Sprop2)
- apply (subgoal_tac "delta i > 0")
- apply arith
- by (rule deltai_gt0)
- also have "... \<le> (\<Sum>i \<in> S. F(r i) - F(l i) + epsilon / 2^(i+2))"
- apply (rule sum_mono)
- apply simp
- apply (rule order_trans)
- apply (rule less_imp_le)
- apply (rule deltai_prop)
- by auto
- also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) +
- (epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _")
- by (subst sum.distrib) (simp add: field_simps sum_distrib_left)
- also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)"
- apply (rule add_left_mono)
- apply (rule mult_left_mono)
- apply (rule sum_mono2)
- using egt0 apply auto
- by (frule Sbound, auto)
- also have "... \<le> ?t + (epsilon / 2)"
- apply (rule add_left_mono)
- apply (subst geometric_sum)
- apply auto
- apply (rule mult_left_mono)
- using egt0 apply auto
- done
- finally have aux2: "F b - F a' \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2"
- by simp
-
+ obtain n where Sbound: "\<And>i. i \<in> S \<Longrightarrow> i \<le> n"
+ using Max_ge finS by blast
have "F b - F a = (F b - F a') + (F a' - F a)"
by auto
also have "... \<le> (F b - F a') + epsilon / 2"
using a_prop by (intro add_left_mono) simp
also have "... \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2 + epsilon / 2"
- apply (intro add_right_mono)
- apply (rule aux2)
- done
+ proof -
+ have "F b - F a' \<le> (\<Sum>i\<in>S. F (r i + delta i) - F (l i))"
+ using claim2 l_r Sprop by (simp add: deltai_gt0 finS add.commute add_strict_increasing)
+ also have "... \<le> (\<Sum>i \<in> S. F(r i) - F(l i) + epsilon / 2^(i+2))"
+ by (smt (verit) sum_mono deltai_prop)
+ also have "... = (\<Sum>i \<in> S. F(r i) - F(l i)) +
+ (epsilon / 4) * (\<Sum>i \<in> S. (1 / 2)^i)" (is "_ = ?t + _")
+ by (subst sum.distrib) (simp add: field_simps sum_distrib_left)
+ also have "... \<le> ?t + (epsilon / 4) * (\<Sum> i < Suc n. (1 / 2)^i)"
+ using egt0 Sbound by (intro add_left_mono mult_left_mono sum_mono2) force+
+ also have "... \<le> ?t + (epsilon / 2)"
+ using egt0 by (simp add: geometric_sum add_left_mono mult_left_mono)
+ finally have "F b - F a' \<le> (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon / 2"
+ by simp
+ then show ?thesis
+ by linarith
+ qed
also have "... = (\<Sum>i\<in>S. F (r i) - F (l i)) + epsilon"
by auto
also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon"
@@ -316,12 +277,8 @@
lemma\<^marker>\<open>tag important\<close> sets_interval_measure [simp, measurable_cong]:
"sets (interval_measure F) = sets borel"
- apply (simp add: sets_extend_measure interval_measure_def borel_sigma_sets_Ioc)
- apply (rule sigma_sets_eqI)
- apply auto
- apply (case_tac "a \<le> ba")
- apply (auto intro: sigma_sets.Empty)
- done
+ apply (simp add: sets_extend_measure interval_measure_def borel_sigma_sets_Ioc image_def split: prod.split)
+ by (metis greaterThanAtMost_empty nle_le)
lemma space_interval_measure [simp]: "space (interval_measure F) = UNIV"
by (simp add: interval_measure_def space_extend_measure)
@@ -342,21 +299,16 @@
show "((\<lambda>a. F b - F a) \<longlongrightarrow> emeasure ?F {a..b}) (at_left a)"
proof (rule tendsto_at_left_sequentially)
show "a - 1 < a" by simp
- fix X assume "\<And>n. X n < a" "incseq X" "X \<longlonglongrightarrow> a"
- with \<open>a \<le> b\<close> have "(\<lambda>n. emeasure ?F {X n<..b}) \<longlonglongrightarrow> emeasure ?F (\<Inter>n. {X n <..b})"
- apply (intro Lim_emeasure_decseq)
- apply (auto simp: decseq_def incseq_def emeasure_interval_measure_Ioc *)
- apply force
- apply (subst (asm ) *)
- apply (auto intro: less_le_trans less_imp_le)
- done
+ fix X assume X: "\<And>n. X n < a" "incseq X" "X \<longlonglongrightarrow> a"
+ then have "emeasure (interval_measure F) {X n<..b} \<noteq> \<infinity>" for n
+ by (smt (verit) "*" \<open>a \<le> b\<close> ennreal_neq_top infinity_ennreal_def)
+ with X have "(\<lambda>n. emeasure ?F {X n<..b}) \<longlonglongrightarrow> emeasure ?F (\<Inter>n. {X n <..b})"
+ by (intro Lim_emeasure_decseq; force simp: decseq_def incseq_def emeasure_interval_measure_Ioc *)
also have "(\<Inter>n. {X n <..b}) = {a..b}"
- using \<open>\<And>n. X n < a\<close>
apply auto
apply (rule LIMSEQ_le_const2[OF \<open>X \<longlonglongrightarrow> a\<close>])
- apply (auto intro: less_imp_le)
- apply (auto intro: less_le_trans)
- done
+ using less_eq_real_def apply presburger
+ using X(1) order_less_le_trans by blast
also have "(\<lambda>n. emeasure ?F {X n<..b}) = (\<lambda>n. F b - F (X n))"
using \<open>\<And>n. X n < a\<close> \<open>a \<le> b\<close> by (subst *) (auto intro: less_imp_le less_le_trans)
finally show "(\<lambda>n. F b - F (X n)) \<longlonglongrightarrow> emeasure ?F {a..b}" .
@@ -426,12 +378,7 @@
by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space)
lemma lebesgue_on_UNIV_eq: "lebesgue_on UNIV = lebesgue"
-proof -
- have "measure_of UNIV (sets lebesgue) (emeasure lebesgue) = lebesgue"
- by (metis measure_of_of_measure space_borel space_completion space_lborel)
- then show ?thesis
- by (auto simp: restrict_space_def)
-qed
+ by (simp add: emeasure_restrict_space measure_eqI)
lemma integral_restrict_Int:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -528,11 +475,7 @@
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
+ using assms by (smt (verit) measurable_lebesgue_cong measurable_restrict_space1)
lemma borel_measurable_if:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -557,33 +500,25 @@
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
+ by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_less])
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
+ by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_ge])
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
+ by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_greater])
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
+ by (force simp add: space_restrict_space trans [OF borel_measurable_iff_halfspace_le])
lemma
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -630,16 +565,12 @@
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
+ have eq: "{x \<in> S. f x \<in> T} = S - (S \<inter> f -` (- 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
+ unfolding borel_measurable_vimage_open eq
+ by (metis Diff_Diff_Int closed_Compl diff_eq open_Compl sets.Diff sets_lebesgue_on_refl vimage_Compl)
qed
lemma borel_measurable_vimage_closed_interval:
@@ -689,9 +620,7 @@
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
+ by (smt (verit, best) Collect_cong UNIV_I borel_measurable_vimage_borel lebesgue_on_UNIV_eq)
subsection \<^marker>\<open>tag unimportant\<close> \<open>Measurability of continuous functions\<close>
@@ -699,13 +628,9 @@
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
+ by (metis borel_measurable_continuous_on_restrict borel_measurable_subalgebra f
+ lebesgue_on_UNIV_eq mono_restrict_space sets_completionI_sets sets_lborel space_borel
+ space_lebesgue_on space_restrict_space subsetI)
lemma id_borel_measurable_lebesgue [iff]: "id \<in> borel_measurable lebesgue"
by (simp add: measurable_completion)
@@ -741,12 +666,7 @@
fixes l u :: real
assumes [simp]: "l \<le> u"
shows "emeasure lborel {l .. u} = u - l"
-proof -
- have "((\<lambda>f. f 1) -` {l..u} \<inter> space (Pi\<^sub>M {1} (\<lambda>b. interval_measure (\<lambda>x. x)))) = {1::real} \<rightarrow>\<^sub>E {l..u}"
- by (auto simp: space_PiM)
- then show ?thesis
- by (simp add: lborel_def emeasure_distr emeasure_PiM emeasure_interval_measure_Icc)
-qed
+ by (simp add: emeasure_interval_measure_Icc lborel_eq_real)
lemma emeasure_lborel_Icc_eq: "emeasure lborel {l .. u} = ennreal (if l \<le> u then u - l else 0)"
by simp
@@ -781,12 +701,7 @@
lemma emeasure_lborel_Ioc[simp]:
assumes [simp]: "l \<le> u"
shows "emeasure lborel {l <.. u} = ennreal (u - l)"
-proof -
- have "emeasure lborel {l <.. u} = emeasure lborel {l .. u}"
- using AE_lborel_singleton[of u] AE_lborel_singleton[of l] by (intro emeasure_eq_AE) auto
- then show ?thesis
- by simp
-qed
+ by (simp add: emeasure_interval_measure_Ioc lborel_eq_real)
lemma emeasure_lborel_Ico[simp]:
assumes [simp]: "l \<le> u"
@@ -830,26 +745,12 @@
by (auto simp: emeasure_lborel_box_eq)
lemma emeasure_lborel_ball_finite: "emeasure lborel (ball c r) < \<infinity>"
-proof -
- have "bounded (ball c r)" by simp
- from bounded_subset_cbox_symmetric[OF this] obtain a where a: "ball c r \<subseteq> cbox (-a) a"
- by auto
- hence "emeasure lborel (ball c r) \<le> emeasure lborel (cbox (-a) a)"
- by (intro emeasure_mono) auto
- also have "\<dots> < \<infinity>" by (simp add: emeasure_lborel_cbox_eq)
- finally show ?thesis .
-qed
+ by (metis bounded_ball bounded_subset_cbox_symmetric cbox_borel emeasure_lborel_cbox_finite
+ emeasure_mono order_le_less_trans sets_lborel)
lemma emeasure_lborel_cball_finite: "emeasure lborel (cball c r) < \<infinity>"
-proof -
- have "bounded (cball c r)" by simp
- from bounded_subset_cbox_symmetric[OF this] obtain a where a: "cball c r \<subseteq> cbox (-a) a"
- by auto
- hence "emeasure lborel (cball c r) \<le> emeasure lborel (cbox (-a) a)"
- by (intro emeasure_mono) auto
- also have "\<dots> < \<infinity>" by (simp add: emeasure_lborel_cbox_eq)
- finally show ?thesis .
-qed
+ by (metis bounded_cball bounded_subset_cbox_symmetric cbox_borel emeasure_lborel_cbox_finite
+ emeasure_mono order_le_less_trans sets_lborel)
lemma fmeasurable_cbox [iff]: "cbox a b \<in> fmeasurable lborel"
and fmeasurable_box [iff]: "box a b \<in> fmeasurable lborel"
@@ -924,7 +825,7 @@
also have "emeasure lborel (\<Union>i. {from_nat_into A i}) = 0"
by (rule emeasure_UN_eq_0) auto
finally show ?thesis
- by (auto simp add: )
+ by simp
qed
lemma countable_imp_null_set_lborel: "countable A \<Longrightarrow> A \<in> null_sets lborel"
@@ -934,30 +835,18 @@
by (intro countable_imp_null_set_lborel countable_finite)
lemma insert_null_sets_iff [simp]: "insert a N \<in> null_sets lebesgue \<longleftrightarrow> N \<in> null_sets lebesgue"
- (is "?lhs = ?rhs")
-proof
- assume ?lhs then show ?rhs
- by (meson completion.complete2 subset_insertI)
-next
- assume ?rhs then show ?lhs
- by (simp add: null_sets.insert_in_sets null_setsI)
-qed
+ by (meson completion.complete2 finite.simps finite_imp_null_set_lborel null_sets.insert_in_sets
+ null_sets_completionI subset_insertI)
lemma insert_null_sets_lebesgue_on_iff [simp]:
assumes "a \<in> S" "S \<in> sets lebesgue"
shows "insert a N \<in> null_sets (lebesgue_on S) \<longleftrightarrow> N \<in> null_sets (lebesgue_on S)"
by (simp add: assms null_sets_restrict_space)
-lemma lborel_neq_count_space[simp]: "lborel \<noteq> count_space (A::('a::ordered_euclidean_space) set)"
-proof
- assume asm: "lborel = count_space A"
- have "space lborel = UNIV" by simp
- hence [simp]: "A = UNIV" by (subst (asm) asm) (simp only: space_count_space)
- have "emeasure lborel {undefined::'a} = 1"
- by (subst asm, subst emeasure_count_space_finite) auto
- moreover have "emeasure lborel {undefined} \<noteq> 1" by simp
- ultimately show False by contradiction
-qed
+lemma lborel_neq_count_space[simp]:
+ fixes A :: "('a::ordered_euclidean_space) set"
+ shows "lborel \<noteq> count_space A"
+ by (metis finite.simps finite_imp_null_set_lborel insert_not_empty null_sets_count_space singleton_iff)
lemma mem_closed_if_AE_lebesgue_open:
assumes "open S" "closed C"
@@ -1004,13 +893,9 @@
let ?A = "\<lambda>n::nat. box (- (real n *\<^sub>R One)) (real n *\<^sub>R One) :: 'a set"
show "range ?A \<subseteq> ?E" "(\<Union>i. ?A i) = UNIV"
unfolding UN_box_eq_UNIV by auto
-
- { fix i show "emeasure lborel (?A i) \<noteq> \<infinity>" by auto }
- { fix X assume "X \<in> ?E" then show "emeasure lborel X = emeasure M X"
- apply (auto simp: emeasure_eq emeasure_lborel_box_eq)
- apply (subst box_eq_empty(1)[THEN iffD2])
- apply (auto intro: less_imp_le simp: not_le)
- done }
+ show "emeasure lborel (?A i) \<noteq> \<infinity>" for i by auto
+ show "emeasure lborel X = emeasure M X" if "X \<in> ?E" for X
+ using that box_eq_empty(1) by (fastforce simp: emeasure_eq emeasure_lborel_box_eq)
qed
lemma\<^marker>\<open>tag important\<close> lborel_affine_euclidean:
@@ -1102,7 +987,7 @@
by (auto simp: null_sets_def)
show "T \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
- by (rule completion.measurable_completion2) (auto simp: eq measurable_completion)
+ by (simp add: completion.measurable_completion2 eq measurable_completion)
have "lebesgue = completion (density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>)))"
using c by (subst lborel_affine_euclidean[of c t]) (simp_all add: T_def[abs_def])
@@ -1135,7 +1020,7 @@
lemma lebesgue_measurable_scaling[measurable]: "(*\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
proof cases
- assume "x = 0"
+ assume "x = 0"
then have "(*\<^sub>R) x = (\<lambda>x. 0::'a)"
by (auto simp: fun_eq_iff)
then show ?thesis by auto
@@ -1352,8 +1237,7 @@
lemma
fixes a::real
shows lmeasurable_interval [iff]: "{a..b} \<in> lmeasurable" "{a<..<b} \<in> lmeasurable"
- apply (metis box_real(2) lmeasurable_cbox)
- by (metis box_real(1) lmeasurable_box)
+ by (metis box_real lmeasurable_box lmeasurable_cbox)+
lemma fmeasurable_compact: "compact S \<Longrightarrow> S \<in> fmeasurable lborel"
using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact)
@@ -1387,14 +1271,7 @@
by (simp add: bounded_interior lmeasurable_open)
lemma null_sets_cbox_Diff_box: "cbox a b - box a b \<in> null_sets lborel"
-proof -
- have "emeasure lborel (cbox a b - box a b) = 0"
- by (subst emeasure_Diff) (auto simp: emeasure_lborel_cbox_eq emeasure_lborel_box_eq box_subset_cbox)
- then have "cbox a b - box a b \<in> null_sets lborel"
- by (auto simp: null_sets_def)
- then show ?thesis
- by (auto dest!: AE_not_in)
-qed
+ by (simp add: emeasure_Diff emeasure_lborel_box_eq emeasure_lborel_cbox_eq null_setsI subset_box)
lemma bounded_set_imp_lmeasurable:
assumes "bounded S" "S \<in> sets lebesgue" shows "S \<in> lmeasurable"
@@ -1423,10 +1300,8 @@
by (simp add: sigma_sets.Empty)
next
case (Compl a)
- then have "\<Omega> - a \<subseteq> \<Omega>" "a \<subseteq> \<Omega>"
- by (auto simp: sigma_sets_into_sp [OF \<open>M \<subseteq> Pow \<Omega>\<close>])
- then show ?case
- by (auto simp: inj_on_image_set_diff [OF \<open>inj_on f \<Omega>\<close>] assms intro: Compl sigma_sets.Compl)
+ with assms show ?case
+ by (metis inj_on_image_set_diff sigma_sets.Compl sigma_sets_into_sp)
next
case (Union a) then show ?case
by (metis image_UN sigma_sets.simps)
@@ -1475,9 +1350,8 @@
lemma measurable_translation:
"S \<in> lmeasurable \<Longrightarrow> ((+) a ` S) \<in> lmeasurable"
using emeasure_lebesgue_affine [of 1 a S]
- apply (auto intro: lebesgue_sets_translation simp add: fmeasurable_def cong: image_cong_simp)
- apply (simp add: ac_simps)
- done
+ by (smt (verit, best) add.commute ennreal_1 fmeasurable_def image_cong lambda_one
+ lebesgue_sets_translation mem_Collect_eq power_one scaleR_one)
lemma measurable_translation_subtract:
"S \<in> lmeasurable \<Longrightarrow> ((\<lambda>x. x - a) ` S) \<in> lmeasurable"
@@ -1508,11 +1382,10 @@
let ?f = "\<lambda>n. root DIM('a) (Suc n)"
- have vimage_eq_image: "(*\<^sub>R) (?f n) -` S = (*\<^sub>R) (1 / ?f n) ` S" for n
- apply safe
- subgoal for x by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto
- subgoal by auto
- done
+ have "?f n *\<^sub>R x \<in> S \<Longrightarrow> x \<in> (*\<^sub>R) (1 / ?f n) ` S" for x n
+ by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto
+ then have vimage_eq_image: "(*\<^sub>R) (?f n) -` S = (*\<^sub>R) (1 / ?f n) ` S" for n
+ by auto
have eq: "(1 / ?f n) ^ DIM('a) = 1 / Suc n" for n
by (simp add: field_simps)
@@ -1642,12 +1515,12 @@
"emeasure (completion M) A = emeasure M A'"
proof -
from AE_notin_null_part[OF A] obtain N where N: "N \<in> null_sets M" "null_part M A \<subseteq> N"
- unfolding eventually_ae_filter using null_part_null_sets[OF A, THEN null_setsD2, THEN sets.sets_into_space] by auto
+ by (meson assms null_part)
let ?A' = "main_part M A \<union> N"
show ?thesis
proof
show "A \<subseteq> ?A'"
- using \<open>null_part M A \<subseteq> N\<close> by (subst main_part_null_part_Un[symmetric, OF A]) auto
+ using \<open>null_part M A \<subseteq> N\<close> assms main_part_null_part_Un by blast
have "main_part M A \<subseteq> A"
using assms main_part_null_part_Un by auto
then have "?A' - A \<subseteq> N"
--- a/src/HOL/Library/BigO.thy Mon Dec 26 21:28:20 2022 +0100
+++ b/src/HOL/Library/BigO.thy Tue Dec 27 10:38:34 2022 +0000
@@ -42,49 +42,22 @@
lemma bigo_pos_const:
"(\<exists>c::'a::linordered_idom. \<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>) \<longleftrightarrow>
(\<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>))"
- apply auto
- apply (case_tac "c = 0")
- apply simp
- apply (rule_tac x = "1" in exI)
- apply simp
- apply (rule_tac x = "\<bar>c\<bar>" in exI)
- apply auto
- apply (subgoal_tac "c * \<bar>f x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>")
- apply (erule_tac x = x in allE)
- apply force
- apply (rule mult_right_mono)
- apply (rule abs_ge_self)
- apply (rule abs_ge_zero)
- done
+ by (metis (no_types, opaque_lifting) abs_ge_zero abs_not_less_zero abs_of_nonneg dual_order.trans
+ mult_1 zero_less_abs_iff zero_less_mult_iff zero_less_one)
lemma bigo_alt_def: "O(f) = {h. \<exists>c. 0 < c \<and> (\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>)}"
by (auto simp add: bigo_def bigo_pos_const)
lemma bigo_elt_subset [intro]: "f \<in> O(g) \<Longrightarrow> O(f) \<le> O(g)"
apply (auto simp add: bigo_alt_def)
- apply (rule_tac x = "ca * c" in exI)
- apply (rule conjI)
- apply simp
- apply (rule allI)
- apply (drule_tac x = "xa" in spec)+
- apply (subgoal_tac "ca * \<bar>f xa\<bar> \<le> ca * (c * \<bar>g xa\<bar>)")
- apply (erule order_trans)
- apply (simp add: ac_simps)
- apply (rule mult_left_mono, assumption)
- apply (rule order_less_imp_le, assumption)
- done
+ by (metis (no_types, opaque_lifting) mult.assoc mult_le_cancel_iff2 order.trans
+ zero_less_mult_iff)
lemma bigo_refl [intro]: "f \<in> O(f)"
- apply (auto simp add: bigo_def)
- apply (rule_tac x = 1 in exI)
- apply simp
- done
+ using bigo_def comm_monoid_mult_class.mult_1 dual_order.eq_iff by blast
lemma bigo_zero: "0 \<in> O(g)"
- apply (auto simp add: bigo_def func_zero)
- apply (rule_tac x = 0 in exI)
- apply auto
- done
+ using bigo_def mult_le_cancel_left1 by fastforce
lemma bigo_zero2: "O(\<lambda>x. 0) = {\<lambda>x. 0}"
by (auto simp add: bigo_def)
@@ -92,21 +65,10 @@
lemma bigo_plus_self_subset [intro]: "O(f) + O(f) \<subseteq> O(f)"
apply (auto simp add: bigo_alt_def set_plus_def)
apply (rule_tac x = "c + ca" in exI)
- apply auto
- apply (simp add: ring_distribs func_plus)
- apply (rule order_trans)
- apply (rule abs_triangle_ineq)
- apply (rule add_mono)
- apply force
- apply force
- done
+ by (smt (verit, best) abs_triangle_ineq add_mono add_pos_pos comm_semiring_class.distrib dual_order.trans)
lemma bigo_plus_idemp [simp]: "O(f) + O(f) = O(f)"
- apply (rule equalityI)
- apply (rule bigo_plus_self_subset)
- apply (rule set_zero_plus2)
- apply (rule bigo_zero)
- done
+ by (simp add: antisym bigo_plus_self_subset bigo_zero set_zero_plus2)
lemma bigo_plus_subset [intro]: "O(f + g) \<subseteq> O(f) + O(g)"
apply (rule subsetI)
@@ -117,37 +79,22 @@
apply (rule_tac x = "c + c" in exI)
apply (clarsimp)
apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>f xa\<bar>")
- apply (erule_tac x = xa in allE)
- apply (erule order_trans)
- apply (simp)
+ apply (metis mult_2 order_trans)
apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
- apply (erule order_trans)
- apply (simp add: ring_distribs)
- apply (rule mult_left_mono)
- apply (simp add: abs_triangle_ineq)
- apply (simp add: order_less_le)
+ apply auto[1]
+ using abs_triangle_ineq mult_le_cancel_iff2 apply blast
+ apply (simp add: order_less_le)
apply (rule_tac x = "\<lambda>n. if \<bar>f n\<bar> < \<bar>g n\<bar> then x n else 0" in exI)
apply (rule conjI)
apply (rule_tac x = "c + c" in exI)
apply auto
apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> (c + c) * \<bar>g xa\<bar>")
- apply (erule_tac x = xa in allE)
- apply (erule order_trans)
- apply simp
- apply (subgoal_tac "c * \<bar>f xa + g xa\<bar> \<le> c * (\<bar>f xa\<bar> + \<bar>g xa\<bar>)")
- apply (erule order_trans)
- apply (simp add: ring_distribs)
- apply (rule mult_left_mono)
- apply (rule abs_triangle_ineq)
- apply (simp add: order_less_le)
+ apply (metis mult_2 order.trans)
+ apply simp
done
lemma bigo_plus_subset2 [intro]: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
- apply (subgoal_tac "A + B \<subseteq> O(f) + O(f)")
- apply (erule order_trans)
- apply simp
- apply (auto del: subsetI simp del: bigo_plus_idemp)
- done
+ using bigo_plus_idemp set_plus_mono2 by blast
lemma bigo_plus_eq: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. 0 \<le> g x \<Longrightarrow> O(f + g) = O(f) + O(g)"
apply (rule equalityI)
@@ -157,8 +104,7 @@
apply (rule_tac x = "max c ca" in exI)
apply (rule conjI)
apply (subgoal_tac "c \<le> max c ca")
- apply (erule order_less_le_trans)
- apply assumption
+ apply linarith
apply (rule max.cobounded1)
apply clarify
apply (drule_tac x = "xa" in spec)+
@@ -167,21 +113,9 @@
apply (subgoal_tac "\<bar>a xa + b xa\<bar> \<le> \<bar>a xa\<bar> + \<bar>b xa\<bar>")
apply (subgoal_tac "\<bar>a xa\<bar> + \<bar>b xa\<bar> \<le> max c ca * f xa + max c ca * g xa")
apply force
- apply (rule add_mono)
- apply (subgoal_tac "c * f xa \<le> max c ca * f xa")
- apply force
- apply (rule mult_right_mono)
- apply (rule max.cobounded1)
- apply assumption
- apply (subgoal_tac "ca * g xa \<le> max c ca * g xa")
- apply force
- apply (rule mult_right_mono)
- apply (rule max.cobounded2)
- apply assumption
- apply (rule abs_triangle_ineq)
- apply (rule add_nonneg_nonneg)
- apply assumption+
- done
+ apply (metis add_mono le_max_iff_disj max_mult_distrib_right)
+ using abs_triangle_ineq apply blast
+ using add_nonneg_nonneg by blast
lemma bigo_bounded_alt: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> c * g x \<Longrightarrow> f \<in> O(g)"
apply (auto simp add: bigo_def)