(* Title: HOL/Probability/Fin_Map.thy Author: Fabian Immler, TU München *) section ‹Finite Maps› theory Fin_Map imports "HOL-Analysis.Finite_Product_Measure" "HOL-Library.Finite_Map" begin text ‹The \<^type>‹fmap› type can be instantiated to \<^class>‹polish_space›, needed for the proof of projective limit. \<^const>‹extensional› functions are used for the representation in order to stay close to the developments of (finite) products \<^const>‹Pi⇩_{E}› and their sigma-algebra \<^const>‹Pi⇩_{M}›.› type_notation fmap ("(_ ⇒⇩_{F}/_)" [22, 21] 21) unbundle fmap.lifting subsection ‹Domain and Application› lift_definition domain::"('i ⇒⇩_{F}'a) ⇒ 'i set" is dom . lemma finite_domain[simp, intro]: "finite (domain P)" by transfer simp lift_definition proj :: "('i ⇒⇩_{F}'a) ⇒ 'i ⇒ 'a" ("'((_)')⇩_{F}" [0] 1000) is "λf x. if x ∈ dom f then the (f x) else undefined" . declare [[coercion proj]] lemma extensional_proj[simp, intro]: "(P)⇩_{F}∈ extensional (domain P)" by transfer (auto simp: extensional_def) lemma proj_undefined[simp, intro]: "i ∉ domain P ⟹ P i = undefined" using extensional_proj[of P] unfolding extensional_def by auto lemma finmap_eq_iff: "P = Q ⟷ (domain P = domain Q ∧ (∀i∈domain P. P i = Q i))" apply transfer apply (safe intro!: ext) subgoal for P Q x by (cases "x ∈ dom P"; cases "P x") (auto dest!: bspec[where x=x]) done subsection ‹Constructor of Finite Maps› lift_definition finmap_of::"'i set ⇒ ('i ⇒ 'a) ⇒ ('i ⇒⇩_{F}'a)" is "λI f x. if x ∈ I ∧ finite I then Some (f x) else None" by (simp add: dom_def) lemma proj_finmap_of[simp]: assumes "finite inds" shows "(finmap_of inds f)⇩_{F}= restrict f inds" using assms by transfer force lemma domain_finmap_of[simp]: assumes "finite inds" shows "domain (finmap_of inds f) = inds" using assms by transfer (auto split: if_splits) lemma finmap_of_eq_iff[simp]: assumes "finite i" "finite j" shows "finmap_of i m = finmap_of j n ⟷ i = j ∧ (∀k∈i. m k= n k)" using assms by (auto simp: finmap_eq_iff) lemma finmap_of_inj_on_extensional_finite: assumes "finite K" assumes "S ⊆ extensional K" shows "inj_on (finmap_of K) S" proof (rule inj_onI) fix x y::"'a ⇒ 'b" assume "finmap_of K x = finmap_of K y" hence "(finmap_of K x)⇩_{F}= (finmap_of K y)⇩_{F}" by simp moreover assume "x ∈ S" "y ∈ S" hence "x ∈ extensional K" "y ∈ extensional K" using assms by auto ultimately show "x = y" using assms by (simp add: extensional_restrict) qed subsection ‹Product set of Finite Maps› text ‹This is \<^term>‹Pi› for Finite Maps, most of this is copied› definition Pi' :: "'i set ⇒ ('i ⇒ 'a set) ⇒ ('i ⇒⇩_{F}'a) set" where "Pi' I A = { P. domain P = I ∧ (∀i. i ∈ I ⟶ (P)⇩_{F}i ∈ A i) } " syntax "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3Π'' _∈_./ _)" 10) translations "Π' x∈A. B" == "CONST Pi' A (λx. B)" subsubsection‹Basic Properties of \<^term>‹Pi'›› lemma Pi'_I[intro!]: "domain f = A ⟹ (⋀x. x ∈ A ⟹ f x ∈ B x) ⟹ f ∈ Pi' A B" by (simp add: Pi'_def) lemma Pi'_I'[simp]: "domain f = A ⟹ (⋀x. x ∈ A ⟶ f x ∈ B x) ⟹ f ∈ Pi' A B" by (simp add:Pi'_def) lemma Pi'_mem: "f∈ Pi' A B ⟹ x ∈ A ⟹ f x ∈ B x" by (simp add: Pi'_def) lemma Pi'_iff: "f ∈ Pi' I X ⟷ domain f = I ∧ (∀i∈I. f i ∈ X i)" unfolding Pi'_def by auto lemma Pi'E [elim]: "f ∈ Pi' A B ⟹ (f x ∈ B x ⟹ domain f = A ⟹ Q) ⟹ (x ∉ A ⟹ Q) ⟹ Q" by(auto simp: Pi'_def) lemma in_Pi'_cong: "domain f = domain g ⟹ (⋀ w. w ∈ A ⟹ f w = g w) ⟹ f ∈ Pi' A B ⟷ g ∈ Pi' A B" by (auto simp: Pi'_def) lemma Pi'_eq_empty[simp]: assumes "finite A" shows "(Pi' A B) = {} ⟷ (∃x∈A. B x = {})" using assms apply (simp add: Pi'_def, auto) apply (drule_tac x = "finmap_of A (λu. SOME y. y ∈ B u)" in spec, auto) apply (cut_tac P= "%y. y ∈ B i" in some_eq_ex, auto) done lemma Pi'_mono: "(⋀x. x ∈ A ⟹ B x ⊆ C x) ⟹ Pi' A B ⊆ Pi' A C" by (auto simp: Pi'_def) lemma Pi_Pi': "finite A ⟹ (Pi⇩_{E}A B) = proj ` Pi' A B" apply (auto simp: Pi'_def Pi_def extensional_def) apply (rule_tac x = "finmap_of A (restrict x A)" in image_eqI) apply auto done subsection ‹Topological Space of Finite Maps› instantiation fmap :: (type, topological_space) topological_space begin definition open_fmap :: "('a ⇒⇩_{F}'b) set ⇒ bool" where [code del]: "open_fmap = generate_topology {Pi' a b|a b. ∀i∈a. open (b i)}" lemma open_Pi'I: "(⋀i. i ∈ I ⟹ open (A i)) ⟹ open (Pi' I A)" by (auto intro: generate_topology.Basis simp: open_fmap_def) instance using topological_space_generate_topology by intro_classes (auto simp: open_fmap_def class.topological_space_def) end lemma open_restricted_space: shows "open {m. P (domain m)}" proof - have "{m. P (domain m)} = (⋃i ∈ Collect P. {m. domain m = i})" by auto also have "open …" proof (rule, safe, cases) fix i::"'a set" assume "finite i" hence "{m. domain m = i} = Pi' i (λ_. UNIV)" by (auto simp: Pi'_def) also have "open …" by (auto intro: open_Pi'I simp: ‹finite i›) finally show "open {m. domain m = i}" . next fix i::"'a set" assume "¬ finite i" hence "{m. domain m = i} = {}" by auto also have "open …" by simp finally show "open {m. domain m = i}" . qed finally show ?thesis . qed lemma closed_restricted_space: shows "closed {m. P (domain m)}" using open_restricted_space[of "λx. ¬ P x"] unfolding closed_def by (rule back_subst) auto lemma tendsto_proj: "((λx. x) ⤏ a) F ⟹ ((λx. (x)⇩_{F}i) ⤏ (a)⇩_{F}i) F" unfolding tendsto_def proof safe fix S::"'b set" let ?S = "Pi' (domain a) (λx. if x = i then S else UNIV)" assume "open S" hence "open ?S" by (auto intro!: open_Pi'I) moreover assume "∀S. open S ⟶ a ∈ S ⟶ eventually (λx. x ∈ S) F" "a i ∈ S" ultimately have "eventually (λx. x ∈ ?S) F" by auto thus "eventually (λx. (x)⇩_{F}i ∈ S) F" by eventually_elim (insert ‹a i ∈ S›, force simp: Pi'_iff split: if_split_asm) qed lemma continuous_proj: shows "continuous_on s (λx. (x)⇩_{F}i)" unfolding continuous_on_def by (safe intro!: tendsto_proj tendsto_ident_at) instance fmap :: (type, first_countable_topology) first_countable_topology proof fix x::"'a⇒⇩_{F}'b" have "∀i. ∃A. countable A ∧ (∀a∈A. x i ∈ a) ∧ (∀a∈A. open a) ∧ (∀S. open S ∧ x i ∈ S ⟶ (∃a∈A. a ⊆ S)) ∧ (∀a b. a ∈ A ⟶ b ∈ A ⟶ a ∩ b ∈ A)" (is "∀i. ?th i") proof fix i from first_countable_basis_Int_stableE[of "x i"] obtain A where "countable A" "⋀C. C ∈ A ⟹ (x)⇩_{F}i ∈ C" "⋀C. C ∈ A ⟹ open C" "⋀S. open S ⟹ (x)⇩_{F}i ∈ S ⟹ ∃A∈A. A ⊆ S" "⋀C D. C ∈ A ⟹ D ∈ A ⟹ C ∩ D ∈ A" by auto thus "?th i" by (intro exI[where x=A]) simp qed then obtain A where A: "∀i. countable (A i) ∧ Ball (A i) ((∈) ((x)⇩_{F}i)) ∧ Ball (A i) open ∧ (∀S. open S ∧ (x)⇩_{F}i ∈ S ⟶ (∃a∈A i. a ⊆ S)) ∧ (∀a b. a ∈ A i ⟶ b ∈ A i ⟶ a ∩ b ∈ A i)" by (auto simp: choice_iff) hence open_sub: "⋀i S. i∈domain x ⟹ open (S i) ⟹ x i∈(S i) ⟹ (∃a∈A i. a⊆(S i))" by auto have A_notempty: "⋀i. i ∈ domain x ⟹ A i ≠ {}" using open_sub[of _ "λ_. UNIV"] by auto let ?A = "(λf. Pi' (domain x) f) ` (Pi⇩_{E}(domain x) A)" show "∃A::nat ⇒ ('a⇒⇩_{F}'b) set. (∀i. x ∈ (A i) ∧ open (A i)) ∧ (∀S. open S ∧ x ∈ S ⟶ (∃i. A i ⊆ S))" proof (rule first_countableI[of "?A"], safe) show "countable ?A" using A by (simp add: countable_PiE) next fix S::"('a ⇒⇩_{F}'b) set" assume "open S" "x ∈ S" thus "∃a∈?A. a ⊆ S" unfolding open_fmap_def proof (induct rule: generate_topology.induct) case UNIV thus ?case by (auto simp add: ex_in_conv PiE_eq_empty_iff A_notempty) next case (Int a b) then obtain f g where "f ∈ Pi⇩_{E}(domain x) A" "Pi' (domain x) f ⊆ a" "g ∈ Pi⇩_{E}(domain x) A" "Pi' (domain x) g ⊆ b" by auto thus ?case using A by (auto simp: Pi'_iff PiE_iff extensional_def Int_stable_def intro!: bexI[where x="λi. f i ∩ g i"]) next case (UN B) then obtain b where "x ∈ b" "b ∈ B" by auto hence "∃a∈?A. a ⊆ b" using UN by simp thus ?case using ‹b ∈ B› by (metis Sup_upper2) next case (Basis s) then obtain a b where xs: "x∈ Pi' a b" "s = Pi' a b" "⋀i. i∈a ⟹ open (b i)" by auto have "∀i. ∃a. (i ∈ domain x ∧ open (b i) ∧ (x)⇩_{F}i ∈ b i) ⟶ (a∈A i ∧ a ⊆ b i)" using open_sub[of _ b] by auto then obtain b' where "⋀i. i ∈ domain x ⟹ open (b i) ⟹ (x)⇩_{F}i ∈ b i ⟹ (b' i ∈A i ∧ b' i ⊆ b i)" unfolding choice_iff by auto with xs have "⋀i. i ∈ a ⟹ (b' i ∈A i ∧ b' i ⊆ b i)" "Pi' a b' ⊆ Pi' a b" by (auto simp: Pi'_iff intro!: Pi'_mono) thus ?case using xs by (intro bexI[where x="Pi' a b'"]) (auto simp: Pi'_iff intro!: image_eqI[where x="restrict b' (domain x)"]) qed qed (insert A,auto simp: PiE_iff intro!: open_Pi'I) qed subsection ‹Metric Space of Finite Maps› (* TODO: Product of uniform spaces and compatibility with metric_spaces! *) instantiation fmap :: (type, metric_space) dist begin definition dist_fmap where "dist P Q = Max (range (λi. dist ((P)⇩_{F}i) ((Q)⇩_{F}i))) + (if domain P = domain Q then 0 else 1)" instance .. end instantiation fmap :: (type, metric_space) uniformity_dist begin definition [code del]: "(uniformity :: (('a, 'b) fmap × ('a ⇒⇩_{F}'b)) filter) = (INF e∈{0 <..}. principal {(x, y). dist x y < e})" instance by standard (rule uniformity_fmap_def) end declare uniformity_Abort[where 'a="('a ⇒⇩_{F}'b::metric_space)", code] instantiation fmap :: (type, metric_space) metric_space begin lemma finite_proj_image': "x ∉ domain P ⟹ finite ((P)⇩_{F}` S)" by (rule finite_subset[of _ "proj P ` (domain P ∩ S ∪ {x})"]) auto lemma finite_proj_image: "finite ((P)⇩_{F}` S)" by (cases "∃x. x ∉ domain P") (auto intro: finite_proj_image' finite_subset[where B="domain P"]) lemma finite_proj_diag: "finite ((λi. d ((P)⇩_{F}i) ((Q)⇩_{F}i)) ` S)" proof - have "(λi. d ((P)⇩_{F}i) ((Q)⇩_{F}i)) ` S = (λ(i, j). d i j) ` ((λi. ((P)⇩_{F}i, (Q)⇩_{F}i)) ` S)" by auto moreover have "((λi. ((P)⇩_{F}i, (Q)⇩_{F}i)) ` S) ⊆ (λi. (P)⇩_{F}i) ` S × (λi. (Q)⇩_{F}i) ` S" by auto moreover have "finite …" using finite_proj_image[of P S] finite_proj_image[of Q S] by (intro finite_cartesian_product) simp_all ultimately show ?thesis by (simp add: finite_subset) qed lemma dist_le_1_imp_domain_eq: shows "dist P Q < 1 ⟹ domain P = domain Q" by (simp add: dist_fmap_def finite_proj_diag split: if_split_asm) lemma dist_proj: shows "dist ((x)⇩_{F}i) ((y)⇩_{F}i) ≤ dist x y" proof - have "dist (x i) (y i) ≤ Max (range (λi. dist (x i) (y i)))" by (simp add: Max_ge_iff finite_proj_diag) also have "… ≤ dist x y" by (simp add: dist_fmap_def) finally show ?thesis . qed lemma dist_finmap_lessI: assumes "domain P = domain Q" assumes "0 < e" assumes "⋀i. i ∈ domain P ⟹ dist (P i) (Q i) < e" shows "dist P Q < e" proof - have "dist P Q = Max (range (λi. dist (P i) (Q i)))" using assms by (simp add: dist_fmap_def finite_proj_diag) also have "… < e" proof (subst Max_less_iff, safe) fix i show "dist ((P)⇩_{F}i) ((Q)⇩_{F}i) < e" using assms by (cases "i ∈ domain P") simp_all qed (simp add: finite_proj_diag) finally show ?thesis . qed instance proof fix S::"('a ⇒⇩_{F}'b) set" have *: "open S = (∀x∈S. ∃e>0. ∀y. dist y x < e ⟶ y ∈ S)" (is "_ = ?od") proof assume "open S" thus ?od unfolding open_fmap_def proof (induct rule: generate_topology.induct) case UNIV thus ?case by (auto intro: zero_less_one) next case (Int a b) show ?case proof safe fix x assume x: "x ∈ a" "x ∈ b" with Int x obtain e1 e2 where "e1>0" "∀y. dist y x < e1 ⟶ y ∈ a" "e2>0" "∀y. dist y x < e2 ⟶ y ∈ b" by force thus "∃e>0. ∀y. dist y x < e ⟶ y ∈ a ∩ b" by (auto intro!: exI[where x="min e1 e2"]) qed next case (UN K) show ?case proof safe fix x X assume "x ∈ X" and X: "X ∈ K" with UN obtain e where "e>0" "⋀y. dist y x < e ⟶ y ∈ X" by force with X show "∃e>0. ∀y. dist y x < e ⟶ y ∈ ⋃K" by auto qed next case (Basis s) then obtain a b where s: "s = Pi' a b" and b: "⋀i. i∈a ⟹ open (b i)" by auto show ?case proof safe fix x assume "x ∈ s" hence [simp]: "finite a" and a_dom: "a = domain x" using s by (auto simp: Pi'_iff) obtain es where es: "∀i ∈ a. es i > 0 ∧ (∀y. dist y (proj x i) < es i ⟶ y ∈ b i)" using b ‹x ∈ s› by atomize_elim (intro bchoice, auto simp: open_dist s) hence in_b: "⋀i y. i ∈ a ⟹ dist y (proj x i) < es i ⟹ y ∈ b i" by auto show "∃e>0. ∀y. dist y x < e ⟶ y ∈ s" proof (cases, rule, safe) assume "a ≠ {}" show "0 < min 1 (Min (es ` a))" using es by (auto simp: ‹a ≠ {}›) fix y assume d: "dist y x < min 1 (Min (es ` a))" show "y ∈ s" unfolding s proof show "domain y = a" using d s ‹a ≠ {}› by (auto simp: dist_le_1_imp_domain_eq a_dom) fix i assume i: "i ∈ a" hence "dist ((y)⇩_{F}i) ((x)⇩_{F}i) < es i" using d by (auto simp: dist_fmap_def ‹a ≠ {}› intro!: le_less_trans[OF dist_proj]) with i show "y i ∈ b i" by (rule in_b) qed next assume "¬a ≠ {}" thus "∃e>0. ∀y. dist y x < e ⟶ y ∈ s" using s ‹x ∈ s› by (auto simp: Pi'_def dist_le_1_imp_domain_eq intro!: exI[where x=1]) qed qed qed next assume "∀x∈S. ∃e>0. ∀y. dist y x < e ⟶ y ∈ S" then obtain e where e_pos: "⋀x. x ∈ S ⟹ e x > 0" and e_in: "⋀x y . x ∈ S ⟹ dist y x < e x ⟹ y ∈ S" unfolding bchoice_iff by auto have S_eq: "S = ⋃{Pi' a b| a b. ∃x∈S. domain x = a ∧ b = (λi. ball (x i) (e x))}" proof safe fix x assume "x ∈ S" thus "x ∈ ⋃{Pi' a b| a b. ∃x∈S. domain x = a ∧ b = (λi. ball (x i) (e x))}" using e_pos by (auto intro!: exI[where x="Pi' (domain x) (λi. ball (x i) (e x))"]) next fix x y assume "y ∈ S" moreover assume "x ∈ (Π' i∈domain y. ball (y i) (e y))" hence "dist x y < e y" using e_pos ‹y ∈ S› by (auto simp: dist_fmap_def Pi'_iff finite_proj_diag dist_commute) ultimately show "x ∈ S" by (rule e_in) qed also have "open …" unfolding open_fmap_def by (intro generate_topology.UN) (auto intro: generate_topology.Basis) finally show "open S" . qed show "open S = (∀x∈S. ∀⇩_{F}(x', y) in uniformity. x' = x ⟶ y ∈ S)" unfolding * eventually_uniformity_metric by (simp del: split_paired_All add: dist_fmap_def dist_commute eq_commute) next fix P Q::"'a ⇒⇩_{F}'b" have Max_eq_iff: "⋀A m. finite A ⟹ A ≠ {} ⟹ (Max A = m) = (m ∈ A ∧ (∀a∈A. a ≤ m))" by (auto intro: Max_in Max_eqI) show "dist P Q = 0 ⟷ P = Q" by (auto simp: finmap_eq_iff dist_fmap_def Max_ge_iff finite_proj_diag Max_eq_iff add_nonneg_eq_0_iff intro!: Max_eqI image_eqI[where x=undefined]) next fix P Q R::"'a ⇒⇩_{F}'b" let ?dists = "λP Q i. dist ((P)⇩_{F}i) ((Q)⇩_{F}i)" let ?dpq = "?dists P Q" and ?dpr = "?dists P R" and ?dqr = "?dists Q R" let ?dom = "λP Q. (if domain P = domain Q then 0 else 1::real)" have "dist P Q = Max (range ?dpq) + ?dom P Q" by (simp add: dist_fmap_def) also obtain t where "t ∈ range ?dpq" "t = Max (range ?dpq)" by (simp add: finite_proj_diag) then obtain i where "Max (range ?dpq) = ?dpq i" by auto also have "?dpq i ≤ ?dpr i + ?dqr i" by (rule dist_triangle2) also have "?dpr i ≤ Max (range ?dpr)" by (simp add: finite_proj_diag) also have "?dqr i ≤ Max (range ?dqr)" by (simp add: finite_proj_diag) also have "?dom P Q ≤ ?dom P R + ?dom Q R" by simp finally show "dist P Q ≤ dist P R + dist Q R" by (simp add: dist_fmap_def ac_simps) qed end subsection ‹Complete Space of Finite Maps› lemma tendsto_finmap: fixes f::"nat ⇒ ('i ⇒⇩_{F}('a::metric_space))" assumes ind_f: "⋀n. domain (f n) = domain g" assumes proj_g: "⋀i. i ∈ domain g ⟹ (λn. (f n) i) ⇢ g i" shows "f ⇢ g" unfolding tendsto_iff proof safe fix e::real assume "0 < e" let ?dists = "λx i. dist ((f x)⇩_{F}i) ((g)⇩_{F}i)" have "eventually (λx. ∀i∈domain g. ?dists x i < e) sequentially" using finite_domain[of g] proj_g proof induct case (insert i G) with ‹0 < e› have "eventually (λx. ?dists x i < e) sequentially" by (auto simp add: tendsto_iff) moreover from insert have "eventually (λx. ∀i∈G. dist ((f x)⇩_{F}i) ((g)⇩_{F}i) < e) sequentially" by simp ultimately show ?case by eventually_elim auto qed simp thus "eventually (λx. dist (f x) g < e) sequentially" by eventually_elim (auto simp add: dist_fmap_def finite_proj_diag ind_f ‹0 < e›) qed instance fmap :: (type, complete_space) complete_space proof fix P::"nat ⇒ 'a ⇒⇩_{F}'b" assume "Cauchy P" then obtain Nd where Nd: "⋀n. n ≥ Nd ⟹ dist (P n) (P Nd) < 1" by (force simp: Cauchy_altdef2) define d where "d = domain (P Nd)" with Nd have dim: "⋀n. n ≥ Nd ⟹ domain (P n) = d" using dist_le_1_imp_domain_eq by auto have [simp]: "finite d" unfolding d_def by simp define p where "p i n = P n i" for i n define q where "q i = lim (p i)" for i define Q where "Q = finmap_of d q" have q: "⋀i. i ∈ d ⟹ q i = Q i" by (auto simp add: Q_def Abs_fmap_inverse) { fix i assume "i ∈ d" have "Cauchy (p i)" unfolding Cauchy_altdef2 p_def proof safe fix e::real assume "0 < e" with ‹Cauchy P› obtain N where N: "⋀n. n≥N ⟹ dist (P n) (P N) < min e 1" by (force simp: Cauchy_altdef2 min_def) hence "⋀n. n ≥ N ⟹ domain (P n) = domain (P N)" using dist_le_1_imp_domain_eq by auto with dim have dim: "⋀n. n ≥ N ⟹ domain (P n) = d" by (metis nat_le_linear) show "∃N. ∀n≥N. dist ((P n) i) ((P N) i) < e" proof (safe intro!: exI[where x="N"]) fix n assume "N ≤ n" have "N ≤ N" by simp have "dist ((P n) i) ((P N) i) ≤ dist (P n) (P N)" using dim[OF ‹N ≤ n›] dim[OF ‹N ≤ N›] ‹i ∈ d› by (auto intro!: dist_proj) also have "… < e" using N[OF ‹N ≤ n›] by simp finally show "dist ((P n) i) ((P N) i) < e" . qed qed hence "convergent (p i)" by (metis Cauchy_convergent_iff) hence "p i ⇢ q i" unfolding q_def convergent_def by (metis limI) } note p = this have "P ⇢ Q" proof (rule metric_LIMSEQ_I) fix e::real assume "0 < e" have "∃ni. ∀i∈d. ∀n≥ni i. dist (p i n) (q i) < e" proof (safe intro!: bchoice) fix i assume "i ∈ d" from p[OF ‹i ∈ d›, THEN metric_LIMSEQ_D, OF ‹0 < e›] show "∃no. ∀n≥no. dist (p i n) (q i) < e" . qed then obtain ni where ni: "∀i∈d. ∀n≥ni i. dist (p i n) (q i) < e" .. define N where "N = max Nd (Max (ni ` d))" show "∃N. ∀n≥N. dist (P n) Q < e" proof (safe intro!: exI[where x="N"]) fix n assume "N ≤ n" hence dom: "domain (P n) = d" "domain Q = d" "domain (P n) = domain Q" using dim by (simp_all add: N_def Q_def dim_def Abs_fmap_inverse) show "dist (P n) Q < e" proof (rule dist_finmap_lessI[OF dom(3) ‹0 < e›]) fix i assume "i ∈ domain (P n)" hence "ni i ≤ Max (ni ` d)" using dom by simp also have "… ≤ N" by (simp add: N_def) finally show "dist ((P n)⇩_{F}i) ((Q)⇩_{F}i) < e" using ni ‹i ∈ domain (P n)› ‹N ≤ n› dom by (auto simp: p_def q N_def less_imp_le) qed qed qed thus "convergent P" by (auto simp: convergent_def) qed subsection ‹Second Countable Space of Finite Maps› instantiation fmap :: (countable, second_countable_topology) second_countable_topology begin definition basis_proj::"'b set set" where "basis_proj = (SOME B. countable B ∧ topological_basis B)" lemma countable_basis_proj: "countable basis_proj" and basis_proj: "topological_basis basis_proj" unfolding basis_proj_def by (intro is_basis countable_basis)+ definition basis_finmap::"('a ⇒⇩_{F}'b) set set" where "basis_finmap = {Pi' I S|I S. finite I ∧ (∀i ∈ I. S i ∈ basis_proj)}" lemma in_basis_finmapI: assumes "finite I" assumes "⋀i. i ∈ I ⟹ S i ∈ basis_proj" shows "Pi' I S ∈ basis_finmap" using assms unfolding basis_finmap_def by auto lemma basis_finmap_eq: assumes "basis_proj ≠ {}" shows "basis_finmap = (λf. Pi' (domain f) (λi. from_nat_into basis_proj ((f)⇩_{F}i))) ` (UNIV::('a ⇒⇩_{F}nat) set)" (is "_ = ?f ` _") unfolding basis_finmap_def proof safe fix I::"'a set" and S::"'a ⇒ 'b set" assume "finite I" "∀i∈I. S i ∈ basis_proj" hence "Pi' I S = ?f (finmap_of I (λx. to_nat_on basis_proj (S x)))" by (force simp: Pi'_def countable_basis_proj) thus "Pi' I S ∈ range ?f" by simp next fix x and f::"'a ⇒⇩_{F}nat" show "∃I S. (Π' i∈domain f. from_nat_into basis_proj ((f)⇩_{F}i)) = Pi' I S ∧ finite I ∧ (∀i∈I. S i ∈ basis_proj)" using assms by (auto intro: from_nat_into) qed lemma basis_finmap_eq_empty: "basis_proj = {} ⟹ basis_finmap = {Pi' {} undefined}" by (auto simp: Pi'_iff basis_finmap_def) lemma countable_basis_finmap: "countable basis_finmap" by (cases "basis_proj = {}") (auto simp: basis_finmap_eq basis_finmap_eq_empty) lemma finmap_topological_basis: "topological_basis basis_finmap" proof (subst topological_basis_iff, safe) fix B' assume "B' ∈ basis_finmap" thus "open B'" by (auto intro!: open_Pi'I topological_basis_open[OF basis_proj] simp: topological_basis_def basis_finmap_def Let_def) next fix O'::"('a ⇒⇩_{F}'b) set" and x assume O': "open O'" "x ∈ O'" then obtain a where a: "x ∈ Pi' (domain x) a" "Pi' (domain x) a ⊆ O'" "⋀i. i∈domain x ⟹ open (a i)" unfolding open_fmap_def proof (atomize_elim, induct rule: generate_topology.induct) case (Int a b) let ?p="λa f. x ∈ Pi' (domain x) f ∧ Pi' (domain x) f ⊆ a ∧ (∀i. i ∈ domain x ⟶ open (f i))" from Int obtain f g where "?p a f" "?p b g" by auto thus ?case by (force intro!: exI[where x="λi. f i ∩ g i"] simp: Pi'_def) next case (UN k) then obtain kk a where "x ∈ kk" "kk ∈ k" "x ∈ Pi' (domain x) a" "Pi' (domain x) a ⊆ kk" "⋀i. i∈domain x ⟹ open (a i)" by force thus ?case by blast qed (auto simp: Pi'_def) have "∃B. (∀i∈domain x. x i ∈ B i ∧ B i ⊆ a i ∧ B i ∈ basis_proj)" proof (rule bchoice, safe) fix i assume "i ∈ domain x" hence "open (a i)" "x i ∈ a i" using a by auto from topological_basisE[OF basis_proj this] obtain b' where "b' ∈ basis_proj" "(x)⇩_{F}i ∈ b'" "b' ⊆ a i" by blast thus "∃y. x i ∈ y ∧ y ⊆ a i ∧ y ∈ basis_proj" by auto qed then obtain B where B: "∀i∈domain x. (x)⇩_{F}i ∈ B i ∧ B i ⊆ a i ∧ B i ∈ basis_proj" by auto define B' where "B' = Pi' (domain x) (λi. (B i)::'b set)" have "B' ⊆ Pi' (domain x) a" using B by (auto intro!: Pi'_mono simp: B'_def) also note ‹… ⊆ O'› finally show "∃B'∈basis_finmap. x ∈ B' ∧ B' ⊆ O'" using B by (auto intro!: bexI[where x=B'] Pi'_mono in_basis_finmapI simp: B'_def) qed lemma range_enum_basis_finmap_imp_open: assumes "x ∈ basis_finmap" shows "open x" using finmap_topological_basis assms by (auto simp: topological_basis_def) instance proof qed (blast intro: finmap_topological_basis countable_basis_finmap topological_basis_imp_subbasis) end subsection ‹Polish Space of Finite Maps› instance fmap :: (countable, polish_space) polish_space proof qed subsection ‹Product Measurable Space of Finite Maps› definition "PiF I M ≡ sigma (⋃J ∈ I. (Π' j∈J. space (M j))) {(Π' j∈J. X j) |X J. J ∈ I ∧ X ∈ (Π j∈J. sets (M j))}" abbreviation "Pi⇩_{F}I M ≡ PiF I M" syntax "_PiF" :: "pttrn ⇒ 'i set ⇒ 'a measure ⇒ ('i => 'a) measure" ("(3Π⇩_{F}_∈_./ _)" 10) translations "Π⇩_{F}x∈I. M" == "CONST PiF I (%x. M)" lemma PiF_gen_subset: "{(Π' j∈J. X j) |X J. J ∈ I ∧ X ∈ (Π j∈J. sets (M j))} ⊆ Pow (⋃J ∈ I. (Π' j∈J. space (M j)))" by (auto simp: Pi'_def) (blast dest: sets.sets_into_space) lemma space_PiF: "space (PiF I M) = (⋃J ∈ I. (Π' j∈J. space (M j)))" unfolding PiF_def using PiF_gen_subset by (rule space_measure_of) lemma sets_PiF: "sets (PiF I M) = sigma_sets (⋃J ∈ I. (Π' j∈J. space (M j))) {(Π' j∈J. X j) |X J. J ∈ I ∧ X ∈ (Π j∈J. sets (M j))}" unfolding PiF_def using PiF_gen_subset by (rule sets_measure_of) lemma sets_PiF_singleton: "sets (PiF {I} M) = sigma_sets (Π' j∈I. space (M j)) {(Π' j∈I. X j) |X. X ∈ (Π j∈I. sets (M j))}" unfolding sets_PiF by simp lemma in_sets_PiFI: assumes "X = (Pi' J S)" "J ∈ I" "⋀i. i∈J ⟹ S i ∈ sets (M i)" shows "X ∈ sets (PiF I M)" unfolding sets_PiF using assms by blast lemma product_in_sets_PiFI: assumes "J ∈ I" "⋀i. i∈J ⟹ S i ∈ sets (M i)" shows "(Pi' J S) ∈ sets (PiF I M)" unfolding sets_PiF using assms by blast lemma singleton_space_subset_in_sets: fixes J assumes "J ∈ I" assumes "finite J" shows "space (PiF {J} M) ∈ sets (PiF I M)" using assms by (intro in_sets_PiFI[where J=J and S="λi. space (M i)"]) (auto simp: product_def space_PiF) lemma singleton_subspace_set_in_sets: assumes A: "A ∈ sets (PiF {J} M)" assumes "finite J" assumes "J ∈ I" shows "A ∈ sets (PiF I M)" using A[unfolded sets_PiF] apply (induct A) unfolding sets_PiF[symmetric] unfolding space_PiF[symmetric] using assms by (auto intro: in_sets_PiFI intro!: singleton_space_subset_in_sets) lemma finite_measurable_singletonI: assumes "finite I" assumes "⋀J. J ∈ I ⟹ finite J" assumes MN: "⋀J. J ∈ I ⟹ A ∈ measurable (PiF {J} M) N" shows "A ∈ measurable (PiF I M) N" unfolding measurable_def proof safe fix y assume "y ∈ sets N" have "A -` y ∩ space (PiF I M) = (⋃J∈I. A -` y ∩ space (PiF {J} M))" by (auto simp: space_PiF) also have "… ∈ sets (PiF I M)" proof (rule sets.finite_UN) show "finite I" by fact fix J assume "J ∈ I" with assms have "finite J" by simp show "A -` y ∩ space (PiF {J} M) ∈ sets (PiF I M)" by (rule singleton_subspace_set_in_sets[OF measurable_sets[OF assms(3)]]) fact+ qed finally show "A -` y ∩ space (PiF I M) ∈ sets (PiF I M)" . next fix x assume "x ∈ space (PiF I M)" thus "A x ∈ space N" using MN[of "domain x"] by (auto simp: space_PiF measurable_space Pi'_def) qed lemma countable_finite_comprehension: fixes f :: "'a::countable set ⇒ _" assumes "⋀s. P s ⟹ finite s" assumes "⋀s. P s ⟹ f s ∈ sets M" shows "⋃{f s|s. P s} ∈ sets M" proof - have "⋃{f s|s. P s} = (⋃n::nat. let s = set (from_nat n) in if P s then f s else {})" proof safe fix x X s assume *: "x ∈ f s" "P s" with assms obtain l where "s = set l" using finite_list by blast with * show "x ∈ (⋃n. let s = set (from_nat n) in if P s then f s else {})" using ‹P s› by (auto intro!: exI[where x="to_nat l"]) next fix x n assume "x ∈ (let s = set (from_nat n) in if P s then f s else {})" thus "x ∈ ⋃{f s|s. P s}" using assms by (auto simp: Let_def split: if_split_asm) qed hence "⋃{f s|s. P s} = (⋃n. let s = set (from_nat n) in if P s then f s else {})" by simp also have "… ∈ sets M" using assms by (auto simp: Let_def) finally show ?thesis . qed lemma space_subset_in_sets: fixes J::"'a::countable set set" assumes "J ⊆ I" assumes "⋀j. j ∈ J ⟹ finite j" shows "space (PiF J M) ∈ sets (PiF I M)" proof - have "space (PiF J M) = ⋃{space (PiF {j} M)|j. j ∈ J}" unfolding space_PiF by blast also have "… ∈ sets (PiF I M)" using assms by (intro countable_finite_comprehension) (auto simp: singleton_space_subset_in_sets) finally show ?thesis . qed lemma subspace_set_in_sets: fixes J::"'a::countable set set" assumes A: "A ∈ sets (PiF J M)" assumes "J ⊆ I" assumes "⋀j. j ∈ J ⟹ finite j" shows "A ∈ sets (PiF I M)" using A[unfolded sets_PiF] apply (induct A) unfolding sets_PiF[symmetric] unfolding space_PiF[symmetric] using assms by (auto intro: in_sets_PiFI intro!: space_subset_in_sets) lemma countable_measurable_PiFI: fixes I::"'a::countable set set" assumes MN: "⋀J. J ∈ I ⟹ finite J ⟹ A ∈ measurable (PiF {J} M) N" shows "A ∈ measurable (PiF I M) N" unfolding measurable_def proof safe fix y assume "y ∈ sets N" have "A -` y = (⋃{A -` y ∩ {x. domain x = J}|J. finite J})" by auto { fix x::"'a ⇒⇩_{F}'b" from finite_list[of "domain x"] obtain xs where "set xs = domain x" by auto hence "∃n. domain x = set (from_nat n)" by (intro exI[where x="to_nat xs"]) auto } hence "A -` y ∩ space (PiF I M) = (⋃n. A -` y ∩ space (PiF ({set (from_nat n)}∩I) M))" by (auto simp: space_PiF Pi'_def) also have "… ∈ sets (PiF I M)" apply (intro sets.Int sets.countable_nat_UN subsetI, safe) apply (case_tac "set (from_nat i) ∈ I") apply simp_all apply (rule singleton_subspace_set_in_sets[OF measurable_sets[OF MN]]) using assms ‹y ∈ sets N› apply (auto simp: space_PiF) done finally show "A -` y ∩ space (PiF I M) ∈ sets (PiF I M)" . next fix x assume "x ∈ space (PiF I M)" thus "A x ∈ space N" using MN[of "domain x"] by (auto simp: space_PiF measurable_space Pi'_def) qed lemma measurable_PiF: assumes f: "⋀x. x ∈ space N ⟹ domain (f x) ∈ I ∧ (∀i∈domain (f x). (f x) i ∈ space (M i))" assumes S: "⋀J S. J ∈ I ⟹ (⋀i. i ∈ J ⟹ S i ∈ sets (M i)) ⟹ f -` (Pi' J S) ∩ space N ∈ sets N" shows "f ∈ measurable N (PiF I M)" unfolding PiF_def using PiF_gen_subset apply (rule measurable_measure_of) using f apply force apply (insert S, auto) done lemma restrict_sets_measurable: assumes A: "A ∈ sets (PiF I M)" and "J ⊆ I" shows "A ∩ {m. domain m ∈ J} ∈ sets (PiF J M)" using A[unfolded sets_PiF] proof (induct A) case (Basic a) then obtain K S where S: "a = Pi' K S" "K ∈ I" "(∀i∈K. S i ∈ sets (M i))" by auto show ?case proof cases assume "K ∈ J" hence "a ∩ {m. domain m ∈ J} ∈ {Pi' K X |X K. K ∈ J ∧ X ∈ (Π j∈K. sets (M j))}" using S by (auto intro!: exI[where x=K] exI[where x=S] simp: Pi'_def) also have "… ⊆ sets (PiF J M)" unfolding sets_PiF by auto finally show ?thesis . next assume "K ∉ J" hence "a ∩ {m. domain m ∈ J} = {}" using S by (auto simp: Pi'_def) also have "… ∈ sets (PiF J M)" by simp finally show ?thesis . qed next case (Union a) have "⋃(a ` UNIV) ∩ {m. domain m ∈ J} = (⋃i. (a i ∩ {m. domain m ∈ J}))" by simp also have "… ∈ sets (PiF J M)" using Union by (intro sets.countable_nat_UN) auto finally show ?case . next case (Compl a) have "(space (PiF I M) - a) ∩ {m. domain m ∈ J} = (space (PiF J M) - (a ∩ {m. domain m ∈ J}))" using ‹J ⊆ I› by (auto simp: space_PiF Pi'_def) also have "… ∈ sets (PiF J M)" using Compl by auto finally show ?case by (simp add: space_PiF) qed simp lemma measurable_finmap_of: assumes f: "⋀i. (∃x ∈ space N. i ∈ J x) ⟹ (λx. f x i) ∈ measurable N (M i)" assumes J: "⋀x. x ∈ space N ⟹ J x ∈ I" "⋀x. x ∈ space N ⟹ finite (J x)" assumes JN: "⋀S. {x. J x = S} ∩ space N ∈ sets N" shows "(λx. finmap_of (J x) (f x)) ∈ measurable N (PiF I M)" proof (rule measurable_PiF) fix x assume "x ∈ space N" with J[of x] measurable_space[OF f] show "domain (finmap_of (J x) (f x)) ∈ I ∧ (∀i∈domain (finmap_of (J x) (f x)). (finmap_of (J x) (f x)) i ∈ space (M i))" by auto next fix K S assume "K ∈ I" and *: "⋀i. i ∈ K ⟹ S i ∈ sets (M i)" with J have eq: "(λx. finmap_of (J x) (f x)) -` Pi' K S ∩ space N = (if ∃x ∈ space N. K = J x ∧ finite K then if K = {} then {x ∈ space N. J x = K} else (⋂i∈K. (λx. f x i) -` S i ∩ {x ∈ space N. J x = K}) else {})" by (auto simp: Pi'_def) have r: "{x ∈ space N. J x = K} = space N ∩ ({x. J x = K} ∩ space N)" by auto show "(λx. finmap_of (J x) (f x)) -` Pi' K S ∩ space N ∈ sets N" unfolding eq r apply (simp del: INT_simps add: ) apply (intro conjI impI sets.finite_INT JN sets.Int[OF sets.top]) apply simp apply assumption apply (subst Int_assoc[symmetric]) apply (rule sets.Int) apply (intro measurable_sets[OF f] *) apply force apply assumption apply (intro JN) done qed lemma measurable_PiM_finmap_of: assumes "finite J" shows "finmap_of J ∈ measurable (Pi⇩_{M}J M) (PiF {J} M)" apply (rule measurable_finmap_of) apply (rule measurable_component_singleton) apply simp apply rule apply (rule ‹finite J›) apply simp done lemma proj_measurable_singleton: assumes "A ∈ sets (M i)" shows "(λx. (x)⇩_{F}i) -` A ∩ space (PiF {I} M) ∈ sets (PiF {I} M)" proof cases assume "i ∈ I" hence "(λx. (x)⇩_{F}i) -` A ∩ space (PiF {I} M) = Pi' I (λx. if x = i then A else space (M x))" using sets.sets_into_space[OF ] ‹A ∈ sets (M i)› assms by (auto simp: space_PiF Pi'_def) thus ?thesis using assms ‹A ∈ sets (M i)› by (intro in_sets_PiFI) auto next assume "i ∉ I" hence "(λx. (x)⇩_{F}i) -` A ∩ space (PiF {I} M) = (if undefined ∈ A then space (PiF {I} M) else {})" by (auto simp: space_PiF Pi'_def) thus ?thesis by simp qed lemma measurable_proj_singleton: assumes "i ∈ I" shows "(λx. (x)⇩_{F}i) ∈ measurable (PiF {I} M) (M i)" by (unfold measurable_def, intro CollectI conjI ballI proj_measurable_singleton assms) (insert ‹i ∈ I›, auto simp: space_PiF) lemma measurable_proj_countable: fixes I::"'a::countable set set" assumes "y ∈ space (M i)" shows "(λx. if i ∈ domain x then (x)⇩_{F}i else y) ∈ measurable (PiF I M) (M i)" proof (rule countable_measurable_PiFI) fix J assume "J ∈ I" "finite J" show "(λx. if i ∈ domain x then x i else y) ∈ measurable (PiF {J} M) (M i)" unfolding measurable_def proof safe fix z assume "z ∈ sets (M i)" have "(λx. if i ∈ domain x then x i else y) -` z ∩ space (PiF {J} M) = (λx. if i ∈ J then (x)⇩_{F}i else y) -` z ∩ space (PiF {J} M)" by (auto simp: space_PiF Pi'_def) also have "… ∈ sets (PiF {J} M)" using ‹z ∈ sets (M i)› ‹finite J› by (cases "i ∈ J") (auto intro!: measurable_sets[OF measurable_proj_singleton]) finally show "(λx. if i ∈ domain x then x i else y) -` z ∩ space (PiF {J} M) ∈ sets (PiF {J} M)" . qed (insert ‹y ∈ space (M i)›, auto simp: space_PiF Pi'_def) qed lemma measurable_restrict_proj: assumes "J ∈ II" "finite J" shows "finmap_of J ∈ measurable (PiM J M) (PiF II M)" using assms by (intro measurable_finmap_of measurable_component_singleton) auto lemma measurable_proj_PiM: fixes J K ::"'a::countable set" and I::"'a set set" assumes "finite J" "J ∈ I" assumes "x ∈ space (PiM J M)" shows "proj ∈ measurable (PiF {J} M) (PiM J M)" proof (rule measurable_PiM_single) show "proj ∈ space (PiF {J} M) → (Π⇩_{E}i ∈ J. space (M i))" using assms by (auto simp add: space_PiM space_PiF extensional_def sets_PiF Pi'_def) next fix A i assume A: "i ∈ J" "A ∈ sets (M i)" show "{ω ∈ space (PiF {J} M). (ω)⇩_{F}i ∈ A} ∈ sets (PiF {J} M)" proof have "{ω ∈ space (PiF {J} M). (ω)⇩_{F}i ∈ A} = (λω. (ω)⇩_{F}i) -` A ∩ space (PiF {J} M)" by auto also have "… ∈ sets (PiF {J} M)" using assms A by (auto intro: measurable_sets[OF measurable_proj_singleton] simp: space_PiM) finally show ?thesis . qed simp qed lemma space_PiF_singleton_eq_product: assumes "finite I" shows "space (PiF {I} M) = (Π' i∈I. space (M i))" by (auto simp: product_def space_PiF assms) text ‹adapted from @{thm sets_PiM_single}› lemma sets_PiF_single: assumes "finite I" "I ≠ {}" shows "sets (PiF {I} M) = sigma_sets (Π' i∈I. space (M i)) {{f∈Π' i∈I. space (M i). f i ∈ A} | i A. i ∈ I ∧ A ∈ sets (M i)}" (is "_ = sigma_sets ?Ω ?R") unfolding sets_PiF_singleton proof (rule sigma_sets_eqI) interpret R: sigma_algebra ?Ω "sigma_sets ?Ω ?R" by (rule sigma_algebra_sigma_sets) auto fix A assume "A ∈ {Pi' I X |X. X ∈ (Π j∈I. sets (M j))}" then obtain X where X: "A = Pi' I X" "X ∈ (Π j∈I. sets (M j))" by auto show "A ∈ sigma_sets ?Ω ?R" proof - from ‹I ≠ {}› X have "A = (⋂j∈I. {f∈space (PiF {I} M). f j ∈ X j})" using sets.sets_into_space by (auto simp: space_PiF product_def) blast also have "… ∈ sigma_sets ?Ω ?R" using X ‹I ≠ {}› assms by (intro R.finite_INT) (auto simp: space_PiF) finally show "A ∈ sigma_sets ?Ω ?R" . qed next fix A assume "A ∈ ?R" then obtain i B where A: "A = {f∈Π' i∈I. space (M i). f i ∈ B}" "i ∈ I" "B ∈ sets (M i)" by auto then have "A = (Π' j ∈ I. if j = i then B else space (M j))" using sets.sets_into_space[OF A(3)] apply (auto simp: Pi'_iff split: if_split_asm) apply blast done also have "… ∈ sigma_sets ?Ω {Pi' I X |X. X ∈ (Π j∈I. sets (M j))}" using A by (intro sigma_sets.Basic ) (auto intro: exI[where x="λj. if j = i then B else space (M j)"]) finally show "A ∈ sigma_sets ?Ω {Pi' I X |X. X ∈ (Π j∈I. sets (M j))}" . qed text ‹adapted from @{thm PiE_cong}› lemma Pi'_cong: assumes "finite I" assumes "⋀i. i ∈ I ⟹ f i = g i" shows "Pi' I f = Pi' I g" using assms by (auto simp: Pi'_def) text ‹adapted from @{thm Pi_UN}› lemma Pi'_UN: fixes A :: "nat ⇒ 'i ⇒ 'a set" assumes "finite I" assumes mono: "⋀i n m. i ∈ I ⟹ n ≤ m ⟹ A n i ⊆ A m i" shows "(⋃n. Pi' I (A n)) = Pi' I (λi. ⋃n. A n i)" proof (intro set_eqI iffI) fix f assume "f ∈ Pi' I (λi. ⋃n. A n i)" then have "∀i∈I. ∃n. f i ∈ A n i" "domain f = I" by (auto simp: ‹finite I› Pi'_def) from bchoice[OF this(1)] obtain n where n: "⋀i. i ∈ I ⟹ f i ∈ (A (n i) i)" by auto obtain k where k: "⋀i. i ∈ I ⟹ n i ≤ k" using ‹finite I› finite_nat_set_iff_bounded_le[of "n`I"] by auto have "f ∈ Pi' I (λi. A k i)" proof fix i assume "i ∈ I" from mono[OF this, of "n i" k] k[OF this] n[OF this] ‹domain f = I› ‹i ∈ I› show "f i ∈ A k i " by (auto simp: ‹finite I›) qed (simp add: ‹domain f = I› ‹finite I›) then show "f ∈ (⋃n. Pi' I (A n))" by auto qed (auto simp: Pi'_def ‹finite I›) text ‹adapted from @{thm sets_PiM_sigma}› lemma sigma_fprod_algebra_sigma_eq: fixes E :: "'i ⇒ 'a set set" and S :: "'i ⇒ nat ⇒ 'a set" assumes [simp]: "finite I" "I ≠ {}" and S_union: "⋀i. i ∈ I ⟹ (⋃j. S i j) = space (M i)" and S_in_E: "⋀i. i ∈ I ⟹ range (S i) ⊆ E i" assumes E_closed: "⋀i. i ∈ I ⟹ E i ⊆ Pow (space (M i))" and E_generates: "⋀i. i ∈ I ⟹ sets (M i) = sigma_sets (space (M i)) (E i)" defines "P == { Pi' I F | F. ∀i∈I. F i ∈ E i }" shows "sets (PiF {I} M) = sigma_sets (space (PiF {I} M)) P" proof let ?P = "sigma (space (Pi⇩_{F}{I} M)) P" from ‹finite I›[THEN ex_bij_betw_finite_nat] obtain T where "bij_betw T I {0..<card I}" .. then have T: "⋀i. i ∈ I ⟹ T i < card I" "⋀i. i∈I ⟹ the_inv_into I T (T i) = i" by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f simp del: ‹finite I›) have P_closed: "P ⊆ Pow (space (Pi⇩_{F}{I} M))" using E_closed by (auto simp: space_PiF P_def Pi'_iff subset_eq) then have space_P: "space ?P = (Π' i∈I. space (M i))" by (simp add: space_PiF) have "sets (PiF {I} M) = sigma_sets (space ?P) {{f ∈ Π' i∈I. space (M i). f i ∈ A} |i A. i ∈ I ∧ A ∈ sets (M i)}" using sets_PiF_single[of I M] by (simp add: space_P) also have "… ⊆ sets (sigma (space (PiF {I} M)) P)" proof (safe intro!: sets.sigma_sets_subset) fix i A assume "i ∈ I" and A: "A ∈ sets (M i)" have "(λx. (x)⇩_{F}i) ∈ measurable ?P (sigma (space (M i)) (E i))" proof (subst measurable_iff_measure_of) show "E i ⊆ Pow (space (M i))" using ‹i ∈ I› by fact from space_P ‹i ∈ I› show "(λx. (x)⇩_{F}i) ∈ space ?P → space (M i)" by auto show "∀A∈E i. (λx. (x)⇩_{F}i) -` A ∩ space ?P ∈ sets ?P" proof fix A assume A: "A ∈ E i" from T have *: "∃xs. length xs = card I ∧ (∀j∈I. (g)⇩_{F}j ∈ (if i = j then A else S j (xs ! T j)))" if "domain g = I" and "∀j∈I. (g)⇩_{F}j ∈ (if i = j then A else S j (f j))" for g f using that by (auto intro!: exI [of _ "map (λn. f (the_inv_into I T n)) [0..<card I]"]) from A have "(λx. (x)⇩_{F}i) -` A ∩ space ?P = (Π' j∈I. if i = j then A else space (M j))" using E_closed ‹i ∈ I› by (auto simp: space_P Pi_iff subset_eq split: if_split_asm) also have "… = (Π' j∈I. ⋃n. if i = j then A else S j n)" by (intro Pi'_cong) (simp_all add: S_union) also have "… = {g. domain g = I ∧ (∃f. ∀j∈I. (g)⇩_{F}j ∈ (if i = j then A else S j (f j)))}" by (rule set_eqI) (simp del: if_image_distrib add: Pi'_iff bchoice_iff) also have "… = (⋃xs∈{xs. length xs = card I}. Π' j∈I. if i = j then A else S j (xs ! T j))" using * by (auto simp add: Pi'_iff split del: if_split) also have "… ∈ sets ?P" proof (safe intro!: sets.countable_UN) fix xs show "(Π' j∈I. if i = j then A else S j (xs ! T j)) ∈ sets ?P" using A S_in_E by (simp add: P_closed) (auto simp: P_def subset_eq intro!: exI[of _ "λj. if i = j then A else S j (xs ! T j)"]) qed finally show "(λx. (x)⇩_{F}i) -` A ∩ space ?P ∈ sets ?P" using P_closed by simp qed qed from measurable_sets[OF this, of A] A ‹i ∈ I› E_closed have "(λx. (x)⇩_{F}i) -` A ∩ space ?P ∈ sets ?P" by (simp add: E_generates) also have "(λx. (x)⇩_{F}i) -` A ∩ space ?P = {f ∈ Π' i∈I. space (M i). f i ∈ A}" using P_closed by (auto simp: space_PiF) finally show "… ∈ sets ?P" . qed finally show "sets (PiF {I} M) ⊆ sigma_sets (space (PiF {I} M)) P" by (simp add: P_closed) show "sigma_sets (space (PiF {I} M)) P ⊆ sets (PiF {I} M)" using ‹finite I› ‹I ≠ {}› by (auto intro!: sets.sigma_sets_subset product_in_sets_PiFI simp: E_generates P_def) qed lemma product_open_generates_sets_PiF_single: assumes "I ≠ {}" assumes [simp]: "finite I" shows "sets (PiF {I} (λ_. borel::'b::second_countable_topology measure)) = sigma_sets (space (PiF {I} (λ_. borel))) {Pi' I F |F. (∀i∈I. F i ∈ Collect open)}" proof - from open_countable_basisE[OF open_UNIV] obtain S::"'b set set" where S: "S ⊆ (SOME B. countable B ∧ topological_basis B)" "UNIV = ⋃ S" by auto show ?thesis proof (rule sigma_fprod_algebra_sigma_eq) show "finite I" by simp show "I ≠ {}" by fact define S' where "S' = from_nat_into S" show "(⋃j. S' j) = space borel" using S apply (auto simp add: from_nat_into countable_basis_proj S'_def basis_proj_def) apply (metis (lifting, mono_tags) UNIV_I UnionE basis_proj_def countable_basis_proj countable_subset from_nat_into_surj) done show "range S' ⊆ Collect open" using S apply (auto simp add: from_nat_into countable_basis_proj S'_def) apply (metis UNIV_not_empty Union_empty from_nat_into subsetD topological_basis_open[OF basis_proj] basis_proj_def) done show "Collect open ⊆ Pow (space borel)" by simp show "sets borel = sigma_sets (space borel) (Collect open)" by (simp add: borel_def) qed qed lemma finmap_UNIV[simp]: "(⋃J∈Collect finite. Π' j∈J. UNIV) = UNIV" by auto lemma borel_eq_PiF_borel: shows "(borel :: ('i::countable ⇒⇩_{F}'a::polish_space) measure) = PiF (Collect finite) (λ_. borel :: 'a measure)" unfolding borel_def PiF_def proof (rule measure_eqI, clarsimp, rule sigma_sets_eqI) fix a::"('i ⇒⇩_{F}'a) set" assume "a ∈ Collect open" hence "open a" by simp then obtain B' where B': "B'⊆basis_finmap" "a = ⋃B'" using finmap_topological_basis by (force simp add: topological_basis_def) have "a ∈ sigma UNIV {Pi' J X |X J. finite J ∧ X ∈ J → sigma_sets UNIV (Collect open)}" unfolding ‹a = ⋃B'› proof (rule sets.countable_Union) from B' countable_basis_finmap show "countable B'" by (metis countable_subset) next show "B' ⊆ sets (sigma UNIV {Pi' J X |X J. finite J ∧ X ∈ J → sigma_sets UNIV (Collect open)})" (is "_ ⊆ sets ?s") proof fix x assume "x ∈ B'" with B' have "x ∈ basis_finmap" by auto then obtain J X where "x = Pi' J X" "finite J" "X ∈ J → sigma_sets UNIV (Collect open)" by (auto simp: basis_finmap_def topological_basis_open[OF basis_proj]) thus "x ∈ sets ?s" by auto qed qed thus "a ∈ sigma_sets UNIV {Pi' J X |X J. finite J ∧ X ∈ J → sigma_sets UNIV (Collect open)}" by simp next fix b::"('i ⇒⇩_{F}'a) set" assume "b ∈ {Pi' J X |X J. finite J ∧ X ∈ J → sigma_sets UNIV (Collect open)}" hence b': "b ∈ sets (Pi⇩_{F}(Collect finite) (λ_. borel))" by (auto simp: sets_PiF borel_def) let ?b = "λJ. b ∩ {x. domain x = J}" have "b = ⋃((λJ. ?b J) ` Collect finite)" by auto also have "… ∈ sets borel" proof (rule sets.countable_Union, safe) fix J::"'i set" assume "finite J" { assume ef: "J = {}" have "?b J ∈ sets borel" proof cases assume "?b J ≠ {}" then obtain f where "f ∈ b" "domain f = {}" using ef by auto hence "?b J = {f}" using ‹J = {}› by (auto simp: finmap_eq_iff) also have "{f} ∈ sets borel" by simp finally show ?thesis . qed simp } moreover { assume "J ≠ ({}::'i set)" have "(?b J) = b ∩ {m. domain m ∈ {J}}" by auto also have "… ∈ sets (PiF {J} (λ_. borel))" using b' by (rule restrict_sets_measurable) (auto simp: ‹finite J›) also have "… = sigma_sets (space (PiF {J} (λ_. borel))) {Pi' (J) F |F. (∀j∈J. F j ∈ Collect open)}" (is "_ = sigma_sets _ ?P") by (rule product_open_generates_sets_PiF_single[OF ‹J ≠ {}› ‹finite J›]) also have "… ⊆ sigma_sets UNIV (Collect open)" by (intro sigma_sets_mono'') (auto intro!: open_Pi'I simp: space_PiF) finally have "(?b J) ∈ sets borel" by (simp add: borel_def) } ultimately show "(?b J) ∈ sets borel" by blast qed (simp add: countable_Collect_finite) finally show "b ∈ sigma_sets UNIV (Collect open)" by (simp add: borel_def) qed (simp add: emeasure_sigma borel_def PiF_def) subsection ‹Isomorphism between Functions and Finite Maps› lemma measurable_finmap_compose: shows "(λm. compose J m f) ∈ measurable (PiM (f ` J) (λ_. M)) (PiM J (λ_. M))" unfolding compose_def by measurable lemma measurable_compose_inv: assumes inj: "⋀j. j ∈ J ⟹ f' (f j) = j" shows "(λm. compose (f ` J) m f') ∈ measurable (PiM J (λ_. M)) (PiM (f ` J) (λ_. M))" unfolding compose_def by (rule measurable_restrict) (auto simp: inj) locale function_to_finmap = fixes J::"'a set" and f :: "'a ⇒ 'b::countable" and f' assumes [simp]: "finite J" assumes inv: "i ∈ J ⟹ f' (f i) = i" begin text ‹to measure finmaps› definition "fm = (finmap_of (f ` J)) o (λg. compose (f ` J) g f')" lemma domain_fm[simp]: "domain (fm x) = f ` J" unfolding fm_def by simp lemma fm_restrict[simp]: "fm (restrict y J) = fm y" unfolding fm_def by (auto simp: compose_def inv intro: restrict_ext) lemma fm_product: assumes "⋀i. space (M i) = UNIV" shows "fm -` Pi' (f ` J) S ∩ space (Pi⇩_{M}J M) = (Π⇩_{E}j ∈ J. S (f j))" using assms by (auto simp: inv fm_def compose_def space_PiM Pi'_def) lemma fm_measurable: assumes "f ` J ∈ N" shows "fm ∈ measurable (Pi⇩_{M}J (λ_. M)) (Pi⇩_{F}N (λ_. M))" unfolding fm_def proof (rule measurable_comp, rule measurable_compose_inv) show "finmap_of (f ` J) ∈ measurable (Pi⇩_{M}(f ` J) (λ_. M)) (PiF N (λ_. M)) " using assms by (intro measurable_finmap_of measurable_component_singleton) auto qed (simp_all add: inv) lemma proj_fm: assumes "x ∈ J" shows "fm m (f x) = m x" using assms by (auto simp: fm_def compose_def o_def inv) lemma inj_on_compose_f': "inj_on (λg. compose (f ` J) g f') (extensional J)" proof (rule inj_on_inverseI) fix x::"'a ⇒ 'c" assume "x ∈ extensional J" thus "(λx. compose J x f) (compose (f ` J) x f') = x" by (auto simp: compose_def inv extensional_def) qed lemma inj_on_fm: assumes "⋀i. space (M i) = UNIV" shows "inj_on fm (space (Pi⇩_{M}J M))" using assms apply (auto simp: fm_def space_PiM PiE_def) apply (rule comp_inj_on) apply (rule inj_on_compose_f') apply (rule finmap_of_inj_on_extensional_finite) apply simp apply (auto) done text ‹to measure functions› definition "mf = (λg. compose J g f) o proj" lemma mf_fm: assumes "x ∈ space (Pi⇩_{M}J (λ_. M))" shows "mf (fm x) = x" proof - have "mf (fm x) ∈ extensional J" by (auto simp: mf_def extensional_def compose_def) moreover have "x ∈ extensional J" using assms sets.sets_into_space by (force simp: space_PiM PiE_def) moreover { fix i assume "i ∈ J" hence "mf (fm x) i = x i" by (auto simp: inv mf_def compose_def fm_def) } ultimately show ?thesis by (rule extensionalityI) qed lemma mf_measurable: assumes "space M = UNIV" shows "mf ∈ measurable (PiF {f ` J} (λ_. M)) (PiM J (λ_. M))" unfolding mf_def proof (rule measurable_comp, rule measurable_proj_PiM) show "(λg. compose J g f) ∈ measurable (Pi⇩_{M}(f ` J) (λx. M)) (Pi⇩_{M}J (λ_. M))" by (rule measurable_finmap_compose) qed (auto simp add: space_PiM extensional_def assms) lemma fm_image_measurable: assumes "space M = UNIV" assumes "