# 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 \<Longrightarrow> openin (topology U) = U"
   using topology_inverse[unfolded mem_Collect_eq] .
 
@@ -290,6 +293,10 @@
 lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
   by (auto simp: topspace_def openin_subtopology)
 
+lemma topspace_subtopology_subset:
+   "S \<subseteq> topspace X \<Longrightarrow> topspace(subtopology X S) = S"
+  by (simp add: inf.absorb_iff2 topspace_subtopology)
+
 lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> 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 \<inter> S) = subtopology X S"
+  by (metis subtopology_subtopology subtopology_topspace)
+
 lemma openin_subtopology_empty:
    "openin (subtopology U {}) S \<longleftrightarrow> S = {}"
 by (metis Int_empty_right openin_empty openin_subtopology)
@@ -395,11 +406,13 @@
 
 subsection \<open>The standard Euclidean topology\<close>
 
-definition%important euclidean :: "'a::topological_space topology"
-  where "euclidean = topology open"
+abbreviation%important euclidean :: "'a::topological_space topology"
+  where "euclidean \<equiv> topology open"
+
+abbreviation top_of_set :: "'a::topological_space set \<Rightarrow> 'a topology"
+  where "top_of_set \<equiv> subtopology (topology open)"
 
 lemma open_openin: "open S \<longleftrightarrow> 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 \<equiv> 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 \<open>Basic "localization" results are handy for connectedness.\<close>
 
 lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
@@ -569,7 +569,7 @@
 lemma openin_trans[trans]:
   "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T \<Longrightarrow>
     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 \<Longrightarrow> open T \<Longrightarrow> 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 \<Longrightarrow> ((\<forall>S. openin X S \<longrightarrow> openin Y S) \<longleftrightarrow> 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>Open and closed maps (not a priori assumed continuous)\<close>
 
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] \<open>e > 0\<close> 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 \<open>x \<in> {c..d}\<close> by auto
 qed
 
-lemma interior_real_semiline':
+lemma interior_real_atMost [simp]:
   fixes a :: real
   shows "interior {..a} = {..<a}"
 proof -
@@ -592,27 +592,36 @@
 proof-
   have "{a..b} = {a..} \<inter> {..b}" by auto
   also have "interior \<dots> = {a<..} \<inter> {..<b}"
-    by (simp add: interior_real_semiline interior_real_semiline')
+    by (simp add: interior_real_atLeast interior_real_atMost)
   also have "\<dots> = {a<..<b}" by auto
   finally show ?thesis .
 qed
 
 lemma interior_atLeastLessThan [simp]:
   fixes a::real shows "interior {a..<b} = {a<..<b}"
-  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost_real interior_Int interior_interior interior_real_semiline)
+  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost_real interior_Int interior_interior interior_real_atLeast)
 
 lemma interior_lessThanAtMost [simp]:
   fixes a::real shows "interior {a<..b} = {a<..<b}"
   by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost_real interior_Int
-            interior_interior interior_real_semiline)
+            interior_interior interior_real_atLeast)
 
 lemma interior_greaterThanLessThan_real [simp]: "interior {a<..<b} = {a<..<b :: real}"
   by (metis interior_atLeastAtMost_real interior_interior)
 
-lemma frontier_real_Iic [simp]:
+lemma frontier_real_atMost [simp]:
   fixes a :: real
   shows "frontier {..a} = {a}"
-  unfolding frontier_def by (auto simp: interior_real_semiline')
+  unfolding frontier_def by (auto simp: interior_real_atMost)
+
+lemma frontier_real_atLeast [simp]: "frontier {a..} = {a::real}"
+  by (auto simp: frontier_def)
+
+lemma frontier_real_greaterThan [simp]: "frontier {a<..} = {a::real}"
+  by (auto simp: interior_open frontier_def)
+
+lemma frontier_real_lessThan [simp]: "frontier {..<a} = {a::real}"
+  by (auto simp: interior_open frontier_def)
 
 lemma rel_interior_real_box [simp]:
   fixes a b :: real
@@ -634,7 +643,7 @@
 proof -
   have *: "{a<..} \<noteq> {}"
     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 \<longleftrightarrow> 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 \<longleftrightarrow> continuous_on_topo euclidean euclidean f"
@@ -843,8 +842,8 @@
   have **: "finite {i. X i \<noteq> 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. \<forall>i\<in>I. f (x i) \<in> U i}"
     apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
     proof (auto)
@@ -995,7 +994,7 @@
       using \<open>open U \<and> x \<in> U\<close> unfolding open_fun_def by auto
     with product_topology_open_contains_basis[OF this]
     have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
-      unfolding topspace_euclidean open_openin by simp
+      by simp
     then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
                            "\<And>i. open (X i)"
                            "finite {i. X i \<noteq> UNIV}"
@@ -1064,7 +1063,7 @@
       unfolding open_fun_def by auto
     with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
     have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
-      unfolding topspace_euclidean open_openin by simp
+      by simp
     then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
                            "\<And>i. open (X i)"
                            "finite {i. X i \<noteq> UNIV}"
@@ -1104,8 +1103,7 @@
     show "open U"
       using \<open>U \<in> K\<close> unfolding open_fun_def K_def apply (auto)
       apply (rule product_topology_basis)
-      using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV unfolding topspace_euclidean open_openin[symmetric]
-      by auto
+      using \<open>\<And>V. V \<in> B2 \<Longrightarrow> open V\<close> open_UNIV by auto
   qed
 
   show ?thesis using i ii iii by auto
@@ -1155,7 +1153,7 @@
                 = blinfun_apply-`{g::('a\<Rightarrow>'b). \<forall>i\<in>I. g (x i) \<in> U i} \<inter> 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 \<in> sets M" .
 next
   fix X assume "X \<in> sets M"
-  from sets.sets_into_space[OF this] and assms 
+  from sets.sets_into_space[OF this] and assms
     show "X \<in> 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: "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets M" "\<And>x. x \<in> A \<Longrightarrow> {x} \<in> sets N"
   assumes A: "countable A"
   assumes eq: "\<And>a. a \<in> A \<Longrightarrow> emeasure M {a} = emeasure N {a}"
@@ -39,32 +39,19 @@
     by (intro sets_eq_countable assms)
 qed fact+
 
-lemma PiE_singleton: 
-  assumes "f \<in> extensional A"
-  shows   "PiE A (\<lambda>x. {f x}) = {f}"
-proof -
-  {
-    fix g assume "g \<in> PiE A (\<lambda>x. {f x})"
-    hence "g x = f x" for x
-      using assms by (cases "x \<in> 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 \<Rightarrow> 'b set"
   assumes "finite A" "\<And>i. countable (B i)"
   shows   "PiM A (\<lambda>i. count_space (B i)) = count_space (PiE A B)"
 proof (rule measure_eqI_countable')
-  show "space (PiM A (\<lambda>i. count_space (B i))) = PiE A B" 
+  show "space (PiM A (\<lambda>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 \<in> PiE A B"
   hence "PiE A (\<lambda>x. {f x}) \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))"
     by (intro sets_PiM_I_finite assms) auto
-  also from f have "PiE A (\<lambda>x. {f x}) = {f}" 
+  also from f have "PiE A (\<lambda>x. {f x}) = {f}"
     by (intro PiE_singleton) (auto simp: PiE_def)
   finally show "{f} \<in> sets (Pi\<^sub>M A (\<lambda>i. count_space (B i)))" .
 next
@@ -74,7 +61,7 @@
   fix f assume f: "f \<in> PiE A B"
   hence "{f} = PiE A (\<lambda>x. {f x})"
     by (intro PiE_singleton [symmetric]) (auto simp: PiE_def)
-  also have "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) \<dots> = 
+  also have "emeasure (Pi\<^sub>M A (\<lambda>i. count_space (B i))) \<dots> =
                (\<Prod>i\<in>A. emeasure (count_space (B i)) {f i})"
     using f assms by (subst emeasure_PiM) auto
   also have "\<dots> = (\<Prod>i\<in>A. 1)"
@@ -88,7 +75,7 @@
 
 
 definition%important abs_summable_on ::
-    "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool" 
+    "('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool"
     (infix "abs'_summable'_on" 50)
  where
    "f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f"
@@ -100,28 +87,28 @@
    "infsetsum f A = lebesgue_integral (count_space A) f"
 
 syntax (ASCII)
-  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
   ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
 syntax
-  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  "_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
   ("(2\<Sum>\<^sub>a_\<in>_./ _)" [0, 51, 10] 10)
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>\<^sub>ai\<in>A. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) A"
 
 syntax (ASCII)
-  "_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  "_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
   ("(3INFSETSUM _:_./ _)" [0, 51, 10] 10)
 syntax
-  "_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}" 
+  "_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
   ("(2\<Sum>\<^sub>a_./ _)" [0, 10] 10)
 translations \<comment> \<open>Beware of argument permutation!\<close>
   "\<Sum>\<^sub>ai. b" \<rightleftharpoons> "CONST infsetsum (\<lambda>i. b) (CONST UNIV)"
 
 syntax (ASCII)
-  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
+  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
   ("(3INFSETSUM _ |/ _./ _)" [0, 0, 10] 10)
 syntax
-  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}" 
+  "_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
   ("(2\<Sum>\<^sub>a_ | (_)./ _)" [0, 0, 10] 10)
 translations
   "\<Sum>\<^sub>ax|P. t" => "CONST infsetsum (\<lambda>x. t) {x. P}"
@@ -156,7 +143,7 @@
     by (rule restrict_count_space_subset [symmetric]) fact+
   also have "integrable \<dots> f \<longleftrightarrow> 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 \<subseteq> B \<Longrightarrow> f abs_summable_on A \<longleftrightarrow> 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]:
   "(\<lambda>x. norm (f x)) abs_summable_on A \<longleftrightarrow> 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 "\<And>x. x \<in> A \<Longrightarrow> norm (f x) \<le> 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) \<longleftrightarrow> summable (\<lambda>n. if n \<in> A then norm (f n) else 0)"
 proof -
   have "f abs_summable_on A \<longleftrightarrow> summable (\<lambda>x. norm (if x \<in> 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 "(\<lambda>x. norm (if x \<in> A then f x else 0)) = (\<lambda>x. if x \<in> 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 "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B"
   shows   "(\<lambda>y. \<Sum>x\<in>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 "(\<lambda>x. f (g x)) abs_summable_on (g' ` g ` A)" 
+  from assms have "(\<lambda>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 \<longleftrightarrow> (\<lambda>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 \<Longrightarrow> (\<lambda>x. f (g x)) abs_summable_on A \<longleftrightarrow> 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 \<Longrightarrow> Im (infsetsum f A) = (\<Sum>\<^sub>ax\<in>A. Im (f x))"
   by (simp add: infsetsum_def abs_summable_on_def)
 
-lemma infsetsum_of_real: 
-  shows "infsetsum (\<lambda>x. of_real (f x) 
-           :: 'a :: {real_normed_algebra_1,banach,second_countable_topology,real_inner}) A = 
+lemma infsetsum_of_real:
+  shows "infsetsum (\<lambda>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 \<Longrightarrow> infsetsum f A = (\<Sum>x\<in>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 = (\<Sum>n. if n \<in> 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 = (\<Sum>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 \<inter> B) = infsetsum f B - infsetsum f (A \<inter> 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 (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A"
 proof -
   define B' where "B' = (\<Union>i\<in>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: \<dots> .
-  
+
   have "infsetsum (\<lambda>x. infsetsum (\<lambda>y. f (x, y)) (B x)) A =
           (\<integral>x. infsetsum (\<lambda>y. f (x, y)) (B x) \<partial>count_space A)"
     unfolding infsetsum_def by simp
@@ -635,9 +622,9 @@
   proof (rule Bochner_Integration.integral_cong [OF refl])
     show "\<And>x. x \<in> space (count_space A) \<Longrightarrow>
          (\<Sum>\<^sub>ay\<in>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 "\<dots> = (\<integral>(x,y). indicator (B x) y *\<^sub>R f (x, y) \<partial>(count_space A \<Otimes>\<^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 "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
-  shows   "f abs_summable_on Sigma A B \<longleftrightarrow> 
+  shows   "f abs_summable_on Sigma A B \<longleftrightarrow>
              (\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
              ((\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x)) abs_summable_on A)"
 proof safe
   define B' where "B' = (\<Union>x\<in>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 \<times> B') = count_space A \<Otimes>\<^sub>M count_space B'"
       by (simp add: pair_measure_countable)
-    finally have "integrable (count_space A) 
-                    (\<lambda>x. lebesgue_integral (count_space B') 
+    finally have "integrable (count_space A)
+                    (\<lambda>x. lebesgue_integral (count_space B')
                       (\<lambda>y. indicator (Sigma A B) (x, y) *\<^sub>R norm (f (x, y))))"
       unfolding set_integrable_def by (rule integrable_fst')
     also have "?this \<longleftrightarrow> integrable (count_space A)
-                    (\<lambda>x. lebesgue_integral (count_space B') 
+                    (\<lambda>x. lebesgue_integral (count_space B')
                       (\<lambda>y. indicator (B x) y *\<^sub>R norm (f (x, y))))"
       by (intro integrable_cong refl) (simp_all add: indicator_def)
     also have "\<dots> \<longleftrightarrow> integrable (count_space A) (\<lambda>x. infsetsum (\<lambda>y. norm (f (x, y))) (B x))"
@@ -749,11 +736,11 @@
         fix x assume x: "x \<in> A"
         with * have "(\<lambda>y. f (x, y)) abs_summable_on B x"
           by blast
-        also have "?this \<longleftrightarrow> integrable (count_space B') 
+        also have "?this \<longleftrightarrow> integrable (count_space B')
                       (\<lambda>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 "(\<lambda>y. indicator (B x) y *\<^sub>R f (x, y)) = 
+        also have "(\<lambda>y. indicator (B x) y *\<^sub>R f (x, y)) =
                      (\<lambda>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 "\<dots> = PiM A (count_space \<circ> B')"
     unfolding o_def using finite by (intro count_space_PiM_finite [symmetric]) simp_all
   also have "(\<integral>g. (\<Prod>x\<in>A. f x (g x)) \<partial>\<dots>) = (\<Prod>x\<in>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 "\<dots> = (\<Prod>x\<in>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 (\<lambda>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 (\<lambda>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 (\<lambda>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 \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   shows   "infsetsum (\<lambda>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 (\<lambda>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 \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   shows   "infsetsum (\<lambda>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 \<Rightarrow> 'b :: {banach, real_normed_algebra, second_countable_topology}"
   assumes "c \<noteq> 0 \<Longrightarrow> f abs_summable_on A"
   shows   "infsetsum (\<lambda>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 \<in> extensional A"
+  shows   "PiE A (\<lambda>x. {f x}) = {f}"
+proof -
+  {
+    fix g assume "g \<in> PiE A (\<lambda>x. {f x})"
+    hence "g x = f x" for x
+      using assms by (cases "x \<in> 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: "(\<Pi>\<^sub>E i\<in>I. S i) = {\<lambda>i\<in>I. f i} \<longleftrightarrow> (\<forall>i\<in>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:
+   "(\<forall>z \<in> PiE I S. \<forall>i \<in> I. P i (z i)) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. \<forall>x \<in> S i. P i x)" (is "?lhs = ?rhs")
+proof (cases "PiE I S = {}")
+  case False
+  then obtain f where f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> S i"
+    by fastforce
+  show ?thesis
+  proof
+    assume L: ?lhs
+    have "P i x"
+      if "i \<in> I" "x \<in> S i" for i x
+    proof -
+      have "(\<lambda>j \<in> I. if j=i then x else f j) \<in> PiE I S"
+        by (simp add: f that(2))
+      then have "P i ((\<lambda>j \<in> 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: "\<lbrakk>x \<in> PiE k s; y \<in> PiE k s; \<And>i. i \<in> k \<Longrightarrow> x i = y i\<rbrakk> \<Longrightarrow> x = y"
+  by (metis ext PiE_E)
+
 
 subsubsection \<open>Injective Extensional Function Spaces\<close>
 
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: