# HG changeset patch # User paulson # Date 1548154247 0 # Node ID 82a6047159194cc4e512bce2dfb4c4809b38ebd6 # Parent 7263b59219c1a993ac49dff00137dfefa65d5344# Parent 61372780515b02f375339034164363dfcfb6354f merged diff -r 7263b59219c1 -r 82a604715919 src/HOL/Analysis/Abstract_Topology.thy --- a/src/HOL/Analysis/Abstract_Topology.thy Mon Jan 21 07:08:55 2019 +0000 +++ b/src/HOL/Analysis/Abstract_Topology.thy Tue Jan 22 10:50:47 2019 +0000 @@ -24,6 +24,9 @@ lemma istopology_openin[intro]: "istopology(openin U)" using openin[of U] by blast +lemma istopology_open: "istopology open" + by (auto simp: istopology_def) + lemma topology_inverse': "istopology U \ openin (topology U) = U" using topology_inverse[unfolded mem_Collect_eq] . @@ -290,6 +293,10 @@ lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \ V" by (auto simp: topspace_def openin_subtopology) +lemma topspace_subtopology_subset: + "S \ topspace X \ topspace(subtopology X S) = S" + by (simp add: inf.absorb_iff2 topspace_subtopology) + lemma closedin_subtopology: "closedin (subtopology U V) S \ (\T. closedin U T \ S = T \ V)" unfolding closedin_def topspace_subtopology by (auto simp: openin_subtopology) @@ -351,6 +358,10 @@ lemma subtopology_UNIV[simp]: "subtopology U UNIV = U" by (simp add: subtopology_superset) +lemma subtopology_restrict: + "subtopology X (topspace X \ S) = subtopology X S" + by (metis subtopology_subtopology subtopology_topspace) + lemma openin_subtopology_empty: "openin (subtopology U {}) S \ S = {}" by (metis Int_empty_right openin_empty openin_subtopology) @@ -395,11 +406,13 @@ subsection \The standard Euclidean topology\ -definition%important euclidean :: "'a::topological_space topology" - where "euclidean = topology open" +abbreviation%important euclidean :: "'a::topological_space topology" + where "euclidean \ topology open" + +abbreviation top_of_set :: "'a::topological_space set \ 'a topology" + where "top_of_set \ subtopology (topology open)" lemma open_openin: "open S \ openin euclidean S" - unfolding euclidean_def apply (rule cong[where x=S and y=S]) apply (rule topology_inverse[symmetric]) apply (auto simp: istopology_def) @@ -426,19 +439,6 @@ abbreviation euclideanreal :: "real topology" where "euclideanreal \ topology open" -lemma real_openin [simp]: "openin euclideanreal S = open S" - by (simp add: euclidean_def open_openin) - -lemma topspace_euclideanreal [simp]: "topspace euclideanreal = UNIV" - using openin_subset open_UNIV real_openin by blast - -lemma topspace_euclideanreal_subtopology [simp]: - "topspace (subtopology euclideanreal S) = S" - by (simp add: topspace_subtopology) - -lemma real_closedin [simp]: "closedin euclideanreal S = closed S" - by (simp add: closed_closedin euclidean_def) - subsection \Basic "localization" results are handy for connectedness.\ lemma openin_open: "openin (subtopology euclidean U) S \ (\T. open T \ (S = U \ T))" @@ -569,7 +569,7 @@ lemma openin_trans[trans]: "openin (subtopology euclidean T) S \ openin (subtopology euclidean U) T \ openin (subtopology euclidean U) S" - unfolding open_openin openin_open by blast + by (metis openin_Int_open openin_open) lemma openin_open_trans: "openin (subtopology euclidean T) S \ open T \ open S" by (auto simp: openin_open intro: openin_trans) @@ -1435,9 +1435,6 @@ by (auto simp: frontier_of_closures) qed -lemma continuous_map_id [simp]: "continuous_map X X id" - unfolding continuous_map_def using openin_subopen topspace_def by fastforce - lemma topology_finer_continuous_id: "topspace X = topspace Y \ ((\S. openin X S \ openin Y S) \ continuous_map Y X id)" unfolding continuous_map_def @@ -1541,6 +1538,16 @@ lemma continuous_map_iff_continuous_real [simp]: "continuous_map (subtopology euclideanreal S) euclideanreal g = continuous_on S g" by (force simp: continuous_map openin_subtopology continuous_on_open_invariant) +lemma continuous_map_id [simp]: "continuous_map X X id" + unfolding continuous_map_def using openin_subopen topspace_def by fastforce + +declare continuous_map_id [unfolded id_def, simp] + +lemma continuous_map_id_subt [simp]: "continuous_map (subtopology X S) X id" + by (simp add: continuous_map_from_subtopology) + +declare continuous_map_id_subt [unfolded id_def, simp] + subsection\Open and closed maps (not a priori assumed continuous)\ diff -r 7263b59219c1 -r 82a604715919 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Jan 21 07:08:55 2019 +0000 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Jan 22 10:50:47 2019 +0000 @@ -521,7 +521,7 @@ using mem_rel_interior_ball[of "x - e *\<^sub>R (x - c)" S] \e > 0\ by auto qed -lemma interior_real_semiline: +lemma interior_real_atLeast [simp]: fixes a :: real shows "interior {a..} = {a<..}" proof - @@ -561,7 +561,7 @@ finally show ?thesis using \x \ {c..d}\ by auto qed -lemma interior_real_semiline': +lemma interior_real_atMost [simp]: fixes a :: real shows "interior {..a} = {.. {..b}" by auto also have "interior \ = {a<..} \ {.. = {a<.. {}" unfolding set_eq_iff by (auto intro!: exI[of _ "a + 1"]) - then show ?thesis using interior_real_semiline interior_rel_interior_gen[of "{a..}"] + then show ?thesis using interior_real_atLeast interior_rel_interior_gen[of "{a..}"] by (auto split: if_split_asm) qed diff -r 7263b59219c1 -r 82a604715919 src/HOL/Analysis/Function_Topology.thy --- a/src/HOL/Analysis/Function_Topology.thy Mon Jan 21 07:08:55 2019 +0000 +++ b/src/HOL/Analysis/Function_Topology.thy Tue Jan 22 10:50:47 2019 +0000 @@ -268,8 +268,7 @@ lemma continuous_on_continuous_on_topo: "continuous_on s f \ continuous_on_topo (subtopology euclidean s) euclidean f" - unfolding continuous_on_open_invariant openin_open vimage_def continuous_on_topo_def -topspace_euclidean_subtopology open_openin topspace_euclidean by fast + by (auto simp: continuous_on_topo_def Int_commute continuous_openin_preimage_eq) lemma continuous_on_topo_UNIV: "continuous_on UNIV f \ continuous_on_topo euclidean euclidean f" @@ -843,8 +842,8 @@ have **: "finite {i. X i \ UNIV}" unfolding X_def V_def J_def using assms(1) by auto have "open (Pi\<^sub>E UNIV X)" - unfolding open_fun_def apply (rule product_topology_basis) - using * ** unfolding open_openin topspace_euclidean by auto + unfolding open_fun_def + by (simp_all add: * ** product_topology_basis) moreover have "Pi\<^sub>E UNIV X = {f. \i\I. f (x i) \ U i}" apply (auto simp add: PiE_iff) unfolding X_def V_def J_def proof (auto) @@ -995,7 +994,7 @@ using \open U \ x \ U\ unfolding open_fun_def by auto with product_topology_open_contains_basis[OF this] have "\X. x \ (\\<^sub>E i\UNIV. X i) \ (\i. open (X i)) \ finite {i. X i \ UNIV} \ (\\<^sub>E i\UNIV. X i) \ U" - unfolding topspace_euclidean open_openin by simp + by simp then obtain X where H: "x \ (\\<^sub>E i\UNIV. X i)" "\i. open (X i)" "finite {i. X i \ UNIV}" @@ -1064,7 +1063,7 @@ unfolding open_fun_def by auto with product_topology_open_contains_basis[OF this \x \ U\] have "\X. x \ (\\<^sub>E i\UNIV. X i) \ (\i. open (X i)) \ finite {i. X i \ UNIV} \ (\\<^sub>E i\UNIV. X i) \ U" - unfolding topspace_euclidean open_openin by simp + by simp then obtain X where H: "x \ (\\<^sub>E i\UNIV. X i)" "\i. open (X i)" "finite {i. X i \ UNIV}" @@ -1104,8 +1103,7 @@ show "open U" using \U \ K\ unfolding open_fun_def K_def apply (auto) apply (rule product_topology_basis) - using \\V. V \ B2 \ open V\ open_UNIV unfolding topspace_euclidean open_openin[symmetric] - by auto + using \\V. V \ B2 \ open V\ open_UNIV by auto qed show ?thesis using i ii iii by auto @@ -1155,7 +1153,7 @@ = blinfun_apply-`{g::('a\'b). \i\I. g (x i) \ U i} \ UNIV" by auto ultimately show ?thesis - unfolding strong_operator_topology_def open_openin apply (subst openin_pullback_topology) by auto + unfolding strong_operator_topology_def by (subst openin_pullback_topology) auto qed lemma strong_operator_topology_continuous_evaluation: diff -r 7263b59219c1 -r 82a604715919 src/HOL/Analysis/Infinite_Set_Sum.thy --- a/src/HOL/Analysis/Infinite_Set_Sum.thy Mon Jan 21 07:08:55 2019 +0000 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Tue Jan 22 10:50:47 2019 +0000 @@ -1,4 +1,4 @@ -(* +(* Title: HOL/Analysis/Infinite_Set_Sum.thy Author: Manuel Eberl, TU München @@ -22,12 +22,12 @@ finally show "X \ sets M" . next fix X assume "X \ sets M" - from sets.sets_into_space[OF this] and assms + from sets.sets_into_space[OF this] and assms show "X \ Pow A" by simp qed lemma measure_eqI_countable': - assumes spaces: "space M = A" "space N = A" + assumes spaces: "space M = A" "space N = A" assumes sets: "\x. x \ A \ {x} \ sets M" "\x. x \ A \ {x} \ sets N" assumes A: "countable A" assumes eq: "\a. a \ A \ emeasure M {a} = emeasure N {a}" @@ -39,32 +39,19 @@ by (intro sets_eq_countable assms) qed fact+ -lemma PiE_singleton: - assumes "f \ extensional A" - shows "PiE A (\x. {f x}) = {f}" -proof - - { - fix g assume "g \ PiE A (\x. {f x})" - hence "g x = f x" for x - using assms by (cases "x \ A") (auto simp: extensional_def) - hence "g = f" by (simp add: fun_eq_iff) - } - thus ?thesis using assms by (auto simp: extensional_def) -qed - lemma count_space_PiM_finite: fixes B :: "'a \ 'b set" assumes "finite A" "\i. countable (B i)" shows "PiM A (\i. count_space (B i)) = count_space (PiE A B)" proof (rule measure_eqI_countable') - show "space (PiM A (\i. count_space (B i))) = PiE A B" + show "space (PiM A (\i. count_space (B i))) = PiE A B" by (simp add: space_PiM) show "space (count_space (PiE A B)) = PiE A B" by simp next fix f assume f: "f \ PiE A B" hence "PiE A (\x. {f x}) \ sets (Pi\<^sub>M A (\i. count_space (B i)))" by (intro sets_PiM_I_finite assms) auto - also from f have "PiE A (\x. {f x}) = {f}" + also from f have "PiE A (\x. {f x}) = {f}" by (intro PiE_singleton) (auto simp: PiE_def) finally show "{f} \ sets (Pi\<^sub>M A (\i. count_space (B i)))" . next @@ -74,7 +61,7 @@ fix f assume f: "f \ PiE A B" hence "{f} = PiE A (\x. {f x})" by (intro PiE_singleton [symmetric]) (auto simp: PiE_def) - also have "emeasure (Pi\<^sub>M A (\i. count_space (B i))) \ = + also have "emeasure (Pi\<^sub>M A (\i. count_space (B i))) \ = (\i\A. emeasure (count_space (B i)) {f i})" using f assms by (subst emeasure_PiM) auto also have "\ = (\i\A. 1)" @@ -88,7 +75,7 @@ definition%important abs_summable_on :: - "('a \ 'b :: {banach, second_countable_topology}) \ 'a set \ bool" + "('a \ 'b :: {banach, second_countable_topology}) \ 'a set \ bool" (infix "abs'_summable'_on" 50) where "f abs_summable_on A \ integrable (count_space A) f" @@ -100,28 +87,28 @@ "infsetsum f A = lebesgue_integral (count_space A) f" syntax (ASCII) - "_infsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" + "_infsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10) syntax - "_infsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" + "_infsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" ("(2\\<^sub>a_\_./ _)" [0, 51, 10] 10) translations \ \Beware of argument permutation!\ "\\<^sub>ai\A. b" \ "CONST infsetsum (\i. b) A" syntax (ASCII) - "_uinfsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" + "_uinfsetsum" :: "pttrn \ 'a set \ 'b \ 'b::{banach, second_countable_topology}" ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10) syntax - "_uinfsetsum" :: "pttrn \ 'b \ 'b::{banach, second_countable_topology}" + "_uinfsetsum" :: "pttrn \ 'b \ 'b::{banach, second_countable_topology}" ("(2\\<^sub>a_./ _)" [0, 10] 10) translations \ \Beware of argument permutation!\ "\\<^sub>ai. b" \ "CONST infsetsum (\i. b) (CONST UNIV)" syntax (ASCII) - "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" + "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10) syntax - "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" + "_qinfsetsum" :: "pttrn \ bool \ 'a \ 'a::{banach, second_countable_topology}" ("(2\\<^sub>a_ | (_)./ _)" [0, 0, 10] 10) translations "\\<^sub>ax|P. t" => "CONST infsetsum (\x. t) {x. P}" @@ -156,7 +143,7 @@ by (rule restrict_count_space_subset [symmetric]) fact+ also have "integrable \ f \ set_integrable (count_space B) A f" by (simp add: integrable_restrict_space set_integrable_def) - finally show ?thesis + finally show ?thesis unfolding abs_summable_on_def set_integrable_def . qed @@ -164,12 +151,12 @@ unfolding abs_summable_on_def set_integrable_def by (metis (no_types) inf_top.right_neutral integrable_restrict_space restrict_count_space sets_UNIV) -lemma abs_summable_on_altdef': +lemma abs_summable_on_altdef': "A \ B \ f abs_summable_on A \ set_integrable (count_space B) A f" unfolding abs_summable_on_def set_integrable_def by (metis (no_types) Pow_iff abs_summable_on_def inf.orderE integrable_restrict_space restrict_count_space_subset set_integrable_def sets_count_space space_count_space) -lemma abs_summable_on_norm_iff [simp]: +lemma abs_summable_on_norm_iff [simp]: "(\x. norm (f x)) abs_summable_on A \ f abs_summable_on A" by (simp add: abs_summable_on_def integrable_norm_iff) @@ -183,8 +170,8 @@ assumes "g abs_summable_on A" assumes "\x. x \ A \ norm (f x) \ norm (g x)" shows "f abs_summable_on A" - using assms Bochner_Integration.integrable_bound[of "count_space A" g f] - unfolding abs_summable_on_def by (auto simp: AE_count_space) + using assms Bochner_Integration.integrable_bound[of "count_space A" g f] + unfolding abs_summable_on_def by (auto simp: AE_count_space) lemma abs_summable_on_comparison_test': assumes "g abs_summable_on A" @@ -220,7 +207,7 @@ "f abs_summable_on (A :: nat set) \ summable (\n. if n \ A then norm (f n) else 0)" proof - have "f abs_summable_on A \ summable (\x. norm (if x \ A then f x else 0))" - by (subst abs_summable_on_restrict'[of _ UNIV]) + by (subst abs_summable_on_restrict'[of _ UNIV]) (simp_all add: abs_summable_on_def integrable_count_space_nat_iff) also have "(\x. norm (if x \ A then f x else 0)) = (\x. if x \ A then norm (f x) else 0)" by auto @@ -277,7 +264,7 @@ show "f abs_summable_on insert x A" by simp qed -lemma abs_summable_sum: +lemma abs_summable_sum: assumes "\x. x \ A \ f x abs_summable_on B" shows "(\y. \x\A. f x y) abs_summable_on B" using assms unfolding abs_summable_on_def by (intro Bochner_Integration.integrable_sum) @@ -305,7 +292,7 @@ have *: "count_space B = distr (count_space A) (count_space B) g" by (rule distr_bij_count_space [symmetric]) fact show ?thesis unfolding abs_summable_on_def - by (subst *, subst integrable_distr_eq[of _ _ "count_space B"]) + by (subst *, subst integrable_distr_eq[of _ _ "count_space B"]) (insert assms, auto simp: bij_betw_def) qed @@ -314,7 +301,7 @@ shows "f abs_summable_on (g ` A)" proof - define g' where "g' = inv_into A g" - from assms have "(\x. f (g x)) abs_summable_on (g' ` g ` A)" + from assms have "(\x. f (g x)) abs_summable_on (g' ` g ` A)" by (rule abs_summable_on_subset) (auto simp: g'_def inv_into_into) also have "?this \ (\x. f (g (g' x))) abs_summable_on (g ` A)" unfolding g'_def by (intro abs_summable_on_reindex_bij_betw [symmetric] inj_on_imp_bij_betw inj_on_inv_into) auto @@ -323,7 +310,7 @@ finally show ?thesis . qed -lemma abs_summable_on_reindex_iff: +lemma abs_summable_on_reindex_iff: "inj_on g A \ (\x. f (g x)) abs_summable_on A \ f abs_summable_on (g ` A)" by (intro abs_summable_on_reindex_bij_betw inj_on_imp_bij_betw) @@ -465,9 +452,9 @@ lemma Im_infsetsum: "f abs_summable_on A \ Im (infsetsum f A) = (\\<^sub>ax\A. Im (f x))" by (simp add: infsetsum_def abs_summable_on_def) -lemma infsetsum_of_real: - shows "infsetsum (\x. of_real (f x) - :: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A = +lemma infsetsum_of_real: + shows "infsetsum (\x. of_real (f x) + :: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A = of_real (infsetsum f A)" unfolding infsetsum_def by (rule integral_bounded_linear'[OF bounded_linear_of_real bounded_linear_inner_left[of 1]]) auto @@ -475,7 +462,7 @@ lemma infsetsum_finite [simp]: "finite A \ infsetsum f A = (\x\A. f x)" by (simp add: infsetsum_def lebesgue_integral_count_space_finite) -lemma infsetsum_nat: +lemma infsetsum_nat: assumes "f abs_summable_on A" shows "infsetsum f A = (\n. if n \ A then f n else 0)" proof - @@ -487,7 +474,7 @@ finally show ?thesis . qed -lemma infsetsum_nat': +lemma infsetsum_nat': assumes "f abs_summable_on UNIV" shows "infsetsum f UNIV = (\n. f n)" using assms by (subst infsetsum_nat) auto @@ -539,7 +526,7 @@ by (intro infsetsum_Un_disjoint abs_summable_on_subset[OF assms]) auto also have "infsetsum f (B - A \ B) = infsetsum f B - infsetsum f (A \ B)" by (intro infsetsum_Diff abs_summable_on_subset[OF assms]) auto - finally show ?thesis + finally show ?thesis by (simp add: algebra_simps) qed @@ -550,8 +537,8 @@ have *: "count_space B = distr (count_space A) (count_space B) g" by (rule distr_bij_count_space [symmetric]) fact show ?thesis unfolding infsetsum_def - by (subst *, subst integral_distr[of _ _ "count_space B"]) - (insert assms, auto simp: bij_betw_def) + by (subst *, subst integral_distr[of _ _ "count_space B"]) + (insert assms, auto simp: bij_betw_def) qed theorem infsetsum_reindex: @@ -615,7 +602,7 @@ shows "infsetsum f (Sigma A B) = infsetsum (\x. infsetsum (\y. f (x, y)) (B x)) A" proof - define B' where "B' = (\i\A. B i)" - have [simp]: "countable B'" + have [simp]: "countable B'" unfolding B'_def by (intro countable_UN assms) interpret pair_sigma_finite "count_space A" "count_space B'" by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+ @@ -627,7 +614,7 @@ by (intro Bochner_Integration.integrable_cong) (auto simp: pair_measure_countable indicator_def split: if_splits) finally have integrable: \ . - + have "infsetsum (\x. infsetsum (\y. f (x, y)) (B x)) A = (\x. infsetsum (\y. f (x, y)) (B x) \count_space A)" unfolding infsetsum_def by simp @@ -635,9 +622,9 @@ proof (rule Bochner_Integration.integral_cong [OF refl]) show "\x. x \ space (count_space A) \ (\\<^sub>ay\B x. f (x, y)) = LINT y|count_space B'. indicat_real (B x) y *\<^sub>R f (x, y)" - using infsetsum_altdef'[of _ B'] + using infsetsum_altdef'[of _ B'] unfolding set_lebesgue_integral_def B'_def - by auto + by auto qed also have "\ = (\(x,y). indicator (B x) y *\<^sub>R f (x, y) \(count_space A \\<^sub>M count_space B'))" by (subst integral_fst [OF integrable]) auto @@ -695,12 +682,12 @@ theorem abs_summable_on_Sigma_iff: assumes [simp]: "countable A" and "\x. x \ A \ countable (B x)" - shows "f abs_summable_on Sigma A B \ + shows "f abs_summable_on Sigma A B \ (\x\A. (\y. f (x, y)) abs_summable_on B x) \ ((\x. infsetsum (\y. norm (f (x, y))) (B x)) abs_summable_on A)" proof safe define B' where "B' = (\x\A. B x)" - have [simp]: "countable B'" + have [simp]: "countable B'" unfolding B'_def using assms by auto interpret pair_sigma_finite "count_space A" "count_space B'" by (intro pair_sigma_finite.intro sigma_finite_measure_count_space_countable) fact+ @@ -714,12 +701,12 @@ by (subst abs_summable_on_altdef' [symmetric]) (auto simp: B'_def) also have "count_space (A \ B') = count_space A \\<^sub>M count_space B'" by (simp add: pair_measure_countable) - finally have "integrable (count_space A) - (\x. lebesgue_integral (count_space B') + finally have "integrable (count_space A) + (\x. lebesgue_integral (count_space B') (\y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y))))" unfolding set_integrable_def by (rule integrable_fst') also have "?this \ integrable (count_space A) - (\x. lebesgue_integral (count_space B') + (\x. lebesgue_integral (count_space B') (\y. indicator (B x) y *\<^sub>R norm (f (x, y))))" by (intro integrable_cong refl) (simp_all add: indicator_def) also have "\ \ integrable (count_space A) (\x. infsetsum (\y. norm (f (x, y))) (B x))" @@ -749,11 +736,11 @@ fix x assume x: "x \ A" with * have "(\y. f (x, y)) abs_summable_on B x" by blast - also have "?this \ integrable (count_space B') + also have "?this \ integrable (count_space B') (\y. indicator (B x) y *\<^sub>R f (x, y))" unfolding set_integrable_def [symmetric] using x by (intro abs_summable_on_altdef') (auto simp: B'_def) - also have "(\y. indicator (B x) y *\<^sub>R f (x, y)) = + also have "(\y. indicator (B x) y *\<^sub>R f (x, y)) = (\y. indicator (Sigma A B) (x, y) *\<^sub>R f (x, y))" using x by (auto simp: indicator_def) finally have "integrable (count_space B') @@ -805,7 +792,7 @@ also have "\ = PiM A (count_space \ B')" unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all also have "(\g. (\x\A. f x (g x)) \\) = (\x\A. infsetsum (f x) (B' x))" - by (subst product_integral_prod) + by (subst product_integral_prod) (insert summable finite, simp_all add: infsetsum_def B'_def abs_summable_on_def) also have "\ = (\x\A. infsetsum (f x) (B x))" by (intro prod.cong refl) (simp_all add: B'_def) @@ -813,44 +800,44 @@ qed lemma infsetsum_uminus: "infsetsum (\x. -f x) A = -infsetsum f A" - unfolding infsetsum_def abs_summable_on_def + unfolding infsetsum_def abs_summable_on_def by (rule Bochner_Integration.integral_minus) lemma infsetsum_add: assumes "f abs_summable_on A" and "g abs_summable_on A" shows "infsetsum (\x. f x + g x) A = infsetsum f A + infsetsum g A" - using assms unfolding infsetsum_def abs_summable_on_def + using assms unfolding infsetsum_def abs_summable_on_def by (rule Bochner_Integration.integral_add) lemma infsetsum_diff: assumes "f abs_summable_on A" and "g abs_summable_on A" shows "infsetsum (\x. f x - g x) A = infsetsum f A - infsetsum g A" - using assms unfolding infsetsum_def abs_summable_on_def + using assms unfolding infsetsum_def abs_summable_on_def by (rule Bochner_Integration.integral_diff) lemma infsetsum_scaleR_left: assumes "c \ 0 \ f abs_summable_on A" shows "infsetsum (\x. f x *\<^sub>R c) A = infsetsum f A *\<^sub>R c" - using assms unfolding infsetsum_def abs_summable_on_def + using assms unfolding infsetsum_def abs_summable_on_def by (rule Bochner_Integration.integral_scaleR_left) lemma infsetsum_scaleR_right: "infsetsum (\x. c *\<^sub>R f x) A = c *\<^sub>R infsetsum f A" - unfolding infsetsum_def abs_summable_on_def + unfolding infsetsum_def abs_summable_on_def by (subst Bochner_Integration.integral_scaleR_right) auto lemma infsetsum_cmult_left: fixes f :: "'a \ 'b :: {banach, real_normed_algebra, second_countable_topology}" assumes "c \ 0 \ f abs_summable_on A" shows "infsetsum (\x. f x * c) A = infsetsum f A * c" - using assms unfolding infsetsum_def abs_summable_on_def + using assms unfolding infsetsum_def abs_summable_on_def by (rule Bochner_Integration.integral_mult_left) lemma infsetsum_cmult_right: fixes f :: "'a \ 'b :: {banach, real_normed_algebra, second_countable_topology}" assumes "c \ 0 \ f abs_summable_on A" shows "infsetsum (\x. c * f x) A = c * infsetsum f A" - using assms unfolding infsetsum_def abs_summable_on_def + using assms unfolding infsetsum_def abs_summable_on_def by (rule Bochner_Integration.integral_mult_right) lemma infsetsum_cdiv: diff -r 7263b59219c1 -r 82a604715919 src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Mon Jan 21 07:08:55 2019 +0000 +++ b/src/HOL/Library/FuncSet.thy Tue Jan 22 10:50:47 2019 +0000 @@ -534,6 +534,49 @@ by auto qed +lemma PiE_singleton: + assumes "f \ extensional A" + shows "PiE A (\x. {f x}) = {f}" +proof - + { + fix g assume "g \ PiE A (\x. {f x})" + hence "g x = f x" for x + using assms by (cases "x \ A") (auto simp: extensional_def) + hence "g = f" by (simp add: fun_eq_iff) + } + thus ?thesis using assms by (auto simp: extensional_def) +qed + +lemma PiE_eq_singleton: "(\\<^sub>E i\I. S i) = {\i\I. f i} \ (\i\I. S i = {f i})" + by (metis (mono_tags, lifting) PiE_eq PiE_singleton insert_not_empty restrict_apply' restrict_extensional) + +lemma all_PiE_elements: + "(\z \ PiE I S. \i \ I. P i (z i)) \ PiE I S = {} \ (\i \ I. \x \ S i. P i x)" (is "?lhs = ?rhs") +proof (cases "PiE I S = {}") + case False + then obtain f where f: "\i. i \ I \ f i \ S i" + by fastforce + show ?thesis + proof + assume L: ?lhs + have "P i x" + if "i \ I" "x \ S i" for i x + proof - + have "(\j \ I. if j=i then x else f j) \ PiE I S" + by (simp add: f that(2)) + then have "P i ((\j \ I. if j=i then x else f j) i)" + using L that(1) by blast + with that show ?thesis + by simp + qed + then show ?rhs + by (simp add: False) + qed fastforce +qed simp + +lemma PiE_ext: "\x \ PiE k s; y \ PiE k s; \i. i \ k \ x i = y i\ \ x = y" + by (metis ext PiE_E) + subsubsection \Injective Extensional Function Spaces\ diff -r 7263b59219c1 -r 82a604715919 src/HOL/Probability/Weak_Convergence.thy --- a/src/HOL/Probability/Weak_Convergence.thy Mon Jan 21 07:08:55 2019 +0000 +++ b/src/HOL/Probability/Weak_Convergence.thy Tue Jan 22 10:50:47 2019 +0000 @@ -359,7 +359,7 @@ proof - interpret real_distribution M by simp show ?thesis - by (auto intro!: * simp: frontier_real_Iic isCont_cdf emeasure_eq_measure weak_conv_m_def weak_conv_def cdf_def2) + by (auto intro!: * simp: frontier_real_atMost isCont_cdf emeasure_eq_measure weak_conv_m_def weak_conv_def cdf_def2) qed theorem integral_cts_step_conv_imp_weak_conv: