Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Notations3.out Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Probability/Fin_Map.thy
    Author:     Fabian Immler, TU München
*)

section \<open>Finite Maps\<close>

theory Fin_Map
  imports "HOL-Analysis.Finite_Product_Measure" "HOL-Library.Finite_Map"
begin

text \<open>The \<^type>\<open>fmap\<close> type can be instantiated to \<^class>\<open>polish_space\<close>, needed for the proof of
  projective limit. \<^const>\<open>extensional\<close> functions are used for the representation in order to
  stay close to the developments of (finite) products \<^const>\<open>Pi\<^sub>E\<close> and their sigma-algebra
  \<^const>\<open>Pi\<^sub>M\<close>.\<close>

type_notation fmap ("(_ \\<^sub>F /_)" [22, 21] 21)

unbundle fmap.lifting

subsection \<open>Domain and Application\<close>

lift_definition domain::"('i \\<^sub>F 'a) \ 'i set" is dom .

lemma finite_domain[simp, intro]: "finite (domain P)"
  by transfer simp

lift_definition proj :: "('i \\<^sub>F 'a) \ 'i \ 'a" ("'((_)')\<^sub>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)\<^sub>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 \<open>Constructor of Finite Maps\<close>

lift_definition finmap_of::"'i set \ ('i \ 'a) \ ('i \\<^sub>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)\<^sub>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)\<^sub>F = (finmap_of K y)\<^sub>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 \<open>Product set of Finite Maps\<close>

text \<open>This is \<^term>\<open>Pi\<close> for Finite Maps, most of this is copied\<close>

definition Pi' :: "'i set \<Rightarrow> ('i \<Rightarrow> 'a set) \<Rightarrow> ('i \<Rightarrow>\<^sub>F 'a) set" where
  "Pi' I A = { P. domain P = I \ (\i. i \ I \ (P)\<^sub>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\<open>Basic Properties of \<^term>\<open>Pi'\<close>\<close>

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\<^sub>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 \<open>Topological Space of Finite Maps\<close>

instantiation fmap :: (type, topological_space) topological_space
begin

definition open_fmap :: "('a \\<^sub>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)\<^sub>F i) \ (a)\<^sub>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)\<^sub>F i \ S) F"
    by eventually_elim (insert \<open>a i \<in> S\<close>, force simp: Pi'_iff split: if_split_asm)
qed

lemma continuous_proj:
  shows "continuous_on s (\x. (x)\<^sub>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\\<^sub>F'b"
  have "\i. \A. countable A \ (\a\A. x i \ a) \ (\a\A. open a) \
    (\<forall>S. open S \<and> x i \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" (is "\<forall>i. ?th i")
  proof
    fix i from first_countable_basis_Int_stableE[of "x i"] guess A .
    thus "?th i" by (intro exI[where x=A]) simp
  qed
  then guess A unfolding choice_iff .. note A = this
  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\<^sub>E (domain x) A)"
  show "\A::nat \ ('a\\<^sub>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 \\<^sub>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\<^sub>E (domain x) A" "Pi' (domain x) f \ a" "g \ Pi\<^sub>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 \<open>b \<in> B\<close> by blast
    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)\<^sub>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)\<^sub>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 \<open>Metric Space of Finite Maps\<close>

(* 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)\<^sub>F i) ((Q)\<^sub>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 \\<^sub>F 'b)) filter) =
    (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"

instance
  by standard (rule uniformity_fmap_def)
end

declare uniformity_Abort[where 'a="('a \<Rightarrow>\<^sub>F 'b::metric_space)", code]

instantiation fmap :: (type, metric_space) metric_space
begin

lemma finite_proj_image': "x \ domain P \ finite ((P)\<^sub>F ` S)"
  by (rule finite_subset[of _ "proj P ` (domain P \ S \ {x})"]) auto

lemma finite_proj_image: "finite ((P)\<^sub>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)\<^sub>F i) ((Q)\<^sub>F i)) ` S)"
proof -
  have "(\i. d ((P)\<^sub>F i) ((Q)\<^sub>F i)) ` S = (\(i, j). d i j) ` ((\i. ((P)\<^sub>F i, (Q)\<^sub>F i)) ` S)" by auto
  moreover have "((\i. ((P)\<^sub>F i, (Q)\<^sub>F i)) ` S) \ (\i. (P)\<^sub>F i) ` S \ (\i. (Q)\<^sub>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)\<^sub>F i) ((y)\<^sub>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)\<^sub>F i) ((Q)\<^sub>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 \\<^sub>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 \<open>x \<in> s\<close> 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: \<open>a \<noteq> {}\<close>)
          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 \<open>a \<noteq> {}\<close> by (auto simp: dist_le_1_imp_domain_eq a_dom)
            fix i assume i: "i \ a"
            hence "dist ((y)\<^sub>F i) ((x)\<^sub>F i) < es i" using d
              by (auto simp: dist_fmap_def \<open>a \<noteq> {}\<close> 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 \<open>x \<in> s\<close> 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 \<open>y \<in> S\<close>
        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. \\<^sub>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 \\<^sub>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 \\<^sub>F 'b"
  let ?dists = "\P Q i. dist ((P)\<^sub>F i) ((Q)\<^sub>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 \<open>Complete Space of Finite Maps\<close>

lemma tendsto_finmap:
  fixes f::"nat \ ('i \\<^sub>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)\<^sub>F i) ((g)\<^sub>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 \<open>0 < e\<close> have "eventually (\<lambda>x. ?dists x i < e) sequentially" by (auto simp add: tendsto_iff)
    moreover
    from insert have "eventually (\x. \i\G. dist ((f x)\<^sub>F i) ((g)\<^sub>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 \<open>0 < e\<close>)
qed

instance fmap :: (type, complete_space) complete_space
proof
  fix P::"nat \ 'a \\<^sub>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 \<open>Cauchy P\<close> obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> 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 \<open>N \<le> n\<close>]  dim[OF \<open>N \<le> N\<close>] \<open>i \<in> d\<close>
          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 \<open>i \<in> d\<close>, THEN metric_LIMSEQ_D, OF \<open>0 < e\<close>]
      show "\no. \n\no. dist (p i n) (q i) < e" .
    qed then guess ni .. note ni = this
    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) \<open>0 < e\<close>])
        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)\<^sub>F i) ((Q)\<^sub>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 \<open>Second Countable Space of Finite Maps\<close>

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 \\<^sub>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)\<^sub>F i))) `
    (UNIV::('a \\<^sub>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 \\<^sub>F nat"
  show "\I S. (\' i\domain f. from_nat_into basis_proj ((f)\<^sub>F i)) = Pi' I S \
    finite I \<and> (\<forall>i\<in>I. S i \<in> 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' \<in> 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 \<Rightarrow>\<^sub>F 'b) set" and x
  assume O': "open O'" "x \<in> 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.
    (\<forall>i\<in>domain x. x i \<in> B i \<and> B i \<subseteq> a i \<and> B i \<in> 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] guess b' .
    thus "\y. x i \ y \ y \ a i \ y \ basis_proj" by auto
  qed
  then guess B .. note B = this
  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 \<open>\<dots> \<subseteq> O'\<close>
  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 \<open>Polish Space of Finite Maps\<close>

instance fmap :: (countable, polish_space) polish_space proof qed

subsection \<open>Product Measurable Space of Finite Maps\<close>

definition "PiF I M \
  sigma (\<Union>J \<in> I. (\<Pi>' j\<in>J. space (M j))) {(\<Pi>' j\<in>J. X j) |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>J. sets (M j))}"

abbreviation
  "Pi\<^sub>F I M \ PiF I M"

syntax
  "_PiF" :: "pttrn \ 'i set \ 'a measure \ ('i => 'a) measure" ("(3\\<^sub>F _\_./ _)" 10)
translations
  "\\<^sub>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 (\<Union>J \<in> I. (\<Pi>' j\<in>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)))
    {(\<Pi>' j\<in>J. X j) |X J. J \<in> I \<and> X \<in> (\<Pi> j\<in>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))
    {(\<Pi>' j\<in>I. X j) |X. X \<in> (\<Pi> j\<in>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 \\<^sub>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 \<open>y \<in> sets N\<close>
    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 \<open>J \<subseteq> I\<close> 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 \
        (\<forall>i\<in>domain (finmap_of (J x) (f x)). (finmap_of (J x) (f x)) i \<in> 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 \<exists>x \<in> space N. K = J x \<and> finite K then if K = {} then {x \<in> space N. J x = K}
      else (\<Inter>i\<in>K. (\<lambda>x. f x i) -` S i \<inter> {x \<in> 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\<^sub>M J M) (PiF {J} M)"
  apply (rule measurable_finmap_of)
  apply (rule measurable_component_singleton)
  apply simp
  apply rule
  apply (rule \<open>finite J\<close>)
  apply simp
  done

lemma proj_measurable_singleton:
  assumes "A \ sets (M i)"
  shows "(\x. (x)\<^sub>F i) -` A \ space (PiF {I} M) \ sets (PiF {I} M)"
proof cases
  assume "i \ I"
  hence "(\x. (x)\<^sub>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 ] \<open>A \<in> sets (M i)\<close> assms
    by (auto simp: space_PiF Pi'_def)
  thus ?thesis  using assms \<open>A \<in> sets (M i)\<close>
    by (intro in_sets_PiFI) auto
next
  assume "i \ I"
  hence "(\x. (x)\<^sub>F i) -` A \ space (PiF {I} M) =
    (if undefined \<in> 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)\<^sub>F i) \ measurable (PiF {I} M) (M i)"
  by (unfold measurable_def, intro CollectI conjI ballI proj_measurable_singleton assms)
     (insert \<open>i \<in> I\<close>, 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)\<^sub>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) =
      (\<lambda>x. if i \<in> J then (x)\<^sub>F i else y) -` z \<inter> 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 \<open>y \<in> space (M i)\<close>, 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) \ (\\<^sub>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). (\)\<^sub>F i \ A} \ sets (PiF {J} M)"
  proof
    have "{\ \ space (PiF {J} M). (\)\<^sub>F i \ A} =
      (\<lambda>\<omega>. (\<omega>)\<^sub>F i) -` A \<inter> 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 \<open>adapted from @{thm sets_PiM_single}\<close>

lemma sets_PiF_single:
  assumes "finite I" "I \ {}"
  shows "sets (PiF {I} M) =
    sigma_sets (\<Pi>' i\<in>I. space (M i))
      {{f\<in>\<Pi>' i\<in>I. space (M i). f i \<in> A} | i A. i \<in> I \<and> A \<in> sets (M i)}"
    (is "_ = sigma_sets ?\ ?R")
  unfolding sets_PiF_singleton
proof (rule sigma_sets_eqI)
  interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?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 \<open>I \<noteq> {}\<close> X have "A = (\<Inter>j\<in>I. {f\<in>space (PiF {I} M). f j \<in> X j})"
      using sets.sets_into_space
      by (auto simp: space_PiF product_def) blast
    also have "\ \ sigma_sets ?\ ?R"
      using X \<open>I \<noteq> {}\<close> 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 \<open>adapted from @{thm PiE_cong}\<close>

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 \<open>adapted from @{thm Pi_UN}\<close>

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 \<open>finite I\<close> 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] \<open>domain f = I\<close> \<open>i \<in> I\<close>
    show "f i \ A k i " by (auto simp: \finite I\)
  qed (simp add: \<open>domain f = I\<close> \<open>finite I\<close>)
  then show "f \ (\n. Pi' I (A n))" by auto
qed (auto simp: Pi'_def \finite I\)

text \<open>adapted from @{thm sets_PiM_sigma}\<close>

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\<^sub>F {I} M)) P"
  from \<open>finite I\<close>[THEN ex_bij_betw_finite_nat] guess T ..
  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: \<open>finite I\<close>)
  have P_closed: "P \ Pow (space (Pi\<^sub>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 \<in> \<Pi>' i\<in>I. space (M i). f i \<in> A} |i A. i \<in> I \<and> A \<in> 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)\<^sub>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 \<open>i \<in> I\<close> show "(\<lambda>x. (x)\<^sub>F i) \<in> space ?P \<rightarrow> space (M i)"
        by auto
      show "\A\E i. (\x. (x)\<^sub>F i) -` A \ space ?P \ sets ?P"
      proof
        fix A assume A: "A \ E i"
        from T have *: "\xs. length xs = card I
          \<and> (\<forall>j\<in>I. (g)\<^sub>F j \<in> (if i = j then A else S j (xs ! T j)))"
          if "domain g = I" and "\j\I. (g)\<^sub>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..
        from A have "(\x. (x)\<^sub>F i) -` A \ space ?P = (\' j\I. if i = j then A else space (M j))"
          using E_closed \<open>i \<in> I\<close> 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)\<^sub>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)\<^sub>F i) -` A \ space ?P \ sets ?P"
          using P_closed by simp
      qed
    qed
    from measurable_sets[OF this, of A] A \<open>i \<in> I\<close> E_closed
    have "(\x. (x)\<^sub>F i) -` A \ space ?P \ sets ?P"
      by (simp add: E_generates)
    also have "(\x. (x)\<^sub>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 \<open>finite I\<close> \<open>I \<noteq> {}\<close>
    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} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
proof -
  from open_countable_basisE[OF open_UNIV] guess S::"'b set set" . note S = this
  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 \\<^sub>F 'a::polish_space) measure) =
    PiF (Collect finite) (\<lambda>_. borel :: 'a measure)"
  unfolding borel_def PiF_def
proof (rule measure_eqI, clarsimp, rule sigma_sets_eqI)
  fix a::"('i \\<^sub>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 \<open>a = \<Union>B'\<close>
  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 \\<^sub>F 'a) set"
  assume "b \ {Pi' J X |X J. finite J \ X \ J \ sigma_sets UNIV (Collect open)}"
  hence b': "b \ sets (Pi\<^sub>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 \<open>J = {}\<close>
          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 \<open>J \<noteq> {}\<close> \<open>finite J\<close>])
      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 \<open>Isomorphism between Functions and Finite Maps\<close>

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 \<open>to measure finmaps\<close>

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\<^sub>M J M) = (\\<^sub>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\<^sub>M J (\_. M)) (Pi\<^sub>F N (\_. M))"
  unfolding fm_def
proof (rule measurable_comp, rule measurable_compose_inv)
  show "finmap_of (f ` J) \ measurable (Pi\<^sub>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\<^sub>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 \<open>to measure functions\<close>

definition "mf = (\g. compose J g f) o proj"

lemma mf_fm:
  assumes "x \ space (Pi\<^sub>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\<^sub>M (f ` J) (\x. M)) (Pi\<^sub>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 "X \ sets (Pi\<^sub>M J (\_. M))"
  shows "fm ` X \ sets (PiF {f ` J} (\_. M))"
proof -
  have "fm ` X = (mf) -` X \ space (PiF {f ` J} (\_. M))"
  proof safe
    fix x assume "x \ X"
    with mf_fm[of x] sets.sets_into_space[OF assms(2)] show "fm x \ mf -` X" by auto
    show "fm x \ space (PiF {f ` J} (\_. M))" by (simp add: space_PiF assms)
  next
    fix y x
    assume x: "mf y \ X"
    assume y: "y \ space (PiF {f ` J} (\_. M))"
    thus "y \ fm ` X"
      by (intro image_eqI[OF _ x], unfold finmap_eq_iff)
         (auto simp: space_PiF fm_def mf_def compose_def inv Pi'_def)
  qed
  also have "\ \ sets (PiF {f ` J} (\_. M))"
    using assms
    by (intro measurable_sets[OF mf_measurable]) auto
  finally show ?thesis .
qed

lemma fm_image_measurable_finite:
  assumes "space M = UNIV"
  assumes "X \ sets (Pi\<^sub>M J (\_. M::'c measure))"
  shows "fm ` X \ sets (PiF (Collect finite) (\_. M::'c measure))"
  using fm_image_measurable[OF assms]
  by (rule subspace_set_in_sets) (auto simp: finite_subset)

text \<open>measure on finmaps\<close>

definition "mapmeasure M N = distr M (PiF (Collect finite) N) (fm)"

lemma sets_mapmeasure[simp]: "sets (mapmeasure M N) = sets (PiF (Collect finite) N)"
  unfolding mapmeasure_def by simp

lemma space_mapmeasure[simp]: "space (mapmeasure M N) = space (PiF (Collect finite) N)"
  unfolding mapmeasure_def by simp

lemma mapmeasure_PiF:
  assumes s1: "space M = space (Pi\<^sub>M J (\_. N))"
  assumes s2: "sets M = sets (Pi\<^sub>M J (\_. N))"
  assumes "space N = UNIV"
  assumes "X \ sets (PiF (Collect finite) (\_. N))"
  shows "emeasure (mapmeasure M (\_. N)) X = emeasure M ((fm -` X \ extensional J))"
  using assms
  by (auto simp: measurable_cong_sets[OF s2 refl] mapmeasure_def emeasure_distr
    fm_measurable space_PiM PiE_def)

lemma mapmeasure_PiM:
  fixes N::"'c measure"
  assumes s1: "space M = space (Pi\<^sub>M J (\_. N))"
  assumes s2: "sets M = (Pi\<^sub>M J (\_. N))"
  assumes N: "space N = UNIV"
  assumes X: "X \ sets M"
  shows "emeasure M X = emeasure (mapmeasure M (\_. N)) (fm ` X)"
  unfolding mapmeasure_def
proof (subst emeasure_distr, subst measurable_cong_sets[OF s2 refl], rule fm_measurable)
  have "X \ space (Pi\<^sub>M J (\_. N))" using assms by (simp add: sets.sets_into_space)
  from assms inj_on_fm[of "\_. N"] subsetD[OF this] have "fm -` fm ` X \ space (Pi\<^sub>M J (\_. N)) = X"
    by (auto simp: vimage_image_eq inj_on_def)
  thus "emeasure M X = emeasure M (fm -` fm ` X \ space M)" using s1
    by simp
  show "fm ` X \ sets (PiF (Collect finite) (\_. N))"
    by (rule fm_image_measurable_finite[OF N X[simplified s2]])
qed simp

end

end

¤ Dauer der Verarbeitung: 0.81 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.