Quelle Measurable.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Measurable.thy
    Author:     Johannes Hölzl <hoelzl@in.tum.de>
*)
section \<open>Measurability Prover\<close>
theory Measurable
  imports
    Sigma_Algebra
    "HOL-Library.Order_Continuity"
begin

lemma (in algebra) sets_Collect_finite_All:
  assumes "\i. i \ S \ {x\\. P i x} \ M" "finite S"
  shows "{x\\. \i\S. P i x} \ M"
proof -
  have "{x\\. \i\S. P i x} = (if S = {} then \ else \i\S. {x\\. P i x})"
    by auto
  with assms show ?thesis by (auto intro!: sets_Collect_finite_All')
qed

abbreviation "pred M P \ P \ measurable M (count_space (UNIV::bool set))"

lemma pred_def: "pred M P \ {x\space M. P x} \ sets M"
proof
  assume "pred M P"
  then have "P -` {True} \ space M \ sets M"
    by (auto simp: measurable_count_space_eq2)
  also have "P -` {True} \ space M = {x\space M. P x}" by auto
  finally show "{x\space M. P x} \ sets M" .
next
  assume P: "{x\space M. P x} \ sets M"
  moreover
  { fix X
    have "X \ Pow (UNIV :: bool set)" by simp
    then have "P -` X \ space M = {x\space M. ((X = {True} \ P x) \ (X = {False} \ \ P x) \ X \ {})}"
      unfolding UNIV_bool Pow_insert Pow_empty by auto
    then have "P -` X \ space M \ sets M"
      by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) }
  then show "pred M P"
    by (auto simp: measurable_def)
qed

lemma pred_sets1: "{x\space M. P x} \ sets M \ f \ measurable N M \ pred N (\x. P (f x))"
  by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def)

lemma pred_sets2: "A \ sets N \ f \ measurable M N \ pred M (\x. f x \ A)"
  by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric])

ML_file \<open>measurable.ML\<close>

attribute_setup measurable = \<open>
  Scan.lift (
    (Args.add >> K true || Args.del >> K false || Scan.succeed true) --
    Scan.optional (Args.parens (
      Scan.optional (Args.$$$ "raw" >> K true) false --
      Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
    (false, Measurable.Concrete) >>
    Measurable.measurable_thm_attr)
\<close> "declaration of measurability theorems"

attribute_setup measurable_dest = Measurable.dest_thm_attr
  "add dest rule to measurability prover"

attribute_setup measurable_cong = Measurable.cong_thm_attr
  "add congurence rules to measurability prover"

method_setup\<^marker>\<open>tag important\<close> measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
  "measurability prover"

simproc_setup\<^marker>\<open>tag important\<close> measurable ("A \<in> sets M" | "f \<in> measurable M N") =
  \<open>K Measurable.proc\<close>

setup \<open>
  Global_Theory.add_thms_dynamic (\<^binding>\<open>measurable\<close>, Measurable.get_all)
\<close>

declare
  pred_sets1[measurable_dest]
  pred_sets2[measurable_dest]
  sets.sets_into_space[measurable_dest]

declare
  sets.top[measurable]
  sets.empty_sets[measurable (raw)]
  sets.Un[measurable (raw)]
  sets.Diff[measurable (raw)]

declare
  measurable_count_space[measurable (raw)]
  measurable_ident[measurable (raw)]
  measurable_id[measurable (raw)]
  measurable_const[measurable (raw)]
  measurable_If[measurable (raw)]
  measurable_comp[measurable (raw)]
  measurable_sets[measurable (raw)]

declare measurable_cong_sets[measurable_cong]
declare sets_restrict_space_cong[measurable_cong]
declare sets_restrict_UNIV[measurable_cong]

lemma predE[measurable (raw)]:
  "pred M P \ {x\space M. P x} \ sets M"
  unfolding pred_def .

lemma pred_intros_imp'[measurable (raw)]:
  "(K \ pred M (\x. P x)) \ pred M (\x. K \ P x)"
  by (cases K) auto

lemma pred_intros_conj1'[measurable (raw)]:
  "(K \ pred M (\x. P x)) \ pred M (\x. K \ P x)"
  by (cases K) auto

lemma pred_intros_conj2'[measurable (raw)]:
  "(K \ pred M (\x. P x)) \ pred M (\x. P x \ K)"
  by (cases K) auto

lemma pred_intros_disj1'[measurable (raw)]:
  "(\ K \ pred M (\x. P x)) \ pred M (\x. K \ P x)"
  by (cases K) auto

lemma pred_intros_disj2'[measurable (raw)]:
  "(\ K \ pred M (\x. P x)) \ pred M (\x. P x \ K)"
  by (cases K) auto

lemma pred_intros_logic[measurable (raw)]:
  "pred M (\x. x \ space M)"
  "pred M (\x. P x) \ pred M (\x. \ P x)"
  "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)"
  "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)"
  "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)"
  "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x = P x)"
  "pred M (\x. f x \ UNIV)"
  "pred M (\x. f x \ {})"
  "pred M (\x. P' (f x) x) \ pred M (\x. f x \ {y. P' y x})"
  "pred M (\x. f x \ (B x)) \ pred M (\x. f x \ - (B x))"
  "pred M (\x. f x \ (A x)) \ pred M (\x. f x \ (B x)) \ pred M (\x. f x \ (A x) - (B x))"
  "pred M (\x. f x \ (A x)) \ pred M (\x. f x \ (B x)) \ pred M (\x. f x \ (A x) \ (B x))"
  "pred M (\x. f x \ (A x)) \ pred M (\x. f x \ (B x)) \ pred M (\x. f x \ (A x) \ (B x))"
  "pred M (\x. g x (f x) \ (X x)) \ pred M (\x. f x \ (g x) -` (X x))"
  by (auto simp: iff_conv_conj_imp pred_def)

lemma pred_intros_countable[measurable (raw)]:
  fixes P :: "'a \ 'i :: countable \ bool"
  shows
    "(\i. pred M (\x. P x i)) \ pred M (\x. \i. P x i)"
    "(\i. pred M (\x. P x i)) \ pred M (\x. \i. P x i)"
  by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def)

lemma pred_intros_countable_bounded[measurable (raw)]:
  fixes X :: "'i :: countable set"
  shows
    "(\i. i \ X \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\X. N x i))"
    "(\i. i \ X \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\X. N x i))"
    "(\i. i \ X \ pred M (\x. P x i)) \ pred M (\x. \i\X. P x i)"
    "(\i. i \ X \ pred M (\x. P x i)) \ pred M (\x. \i\X. P x i)"
  by simp_all (auto simp: Bex_def Ball_def)

lemma pred_intros_finite[measurable (raw)]:
  "finite I \ (\i. i \ I \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\I. N x i))"
  "finite I \ (\i. i \ I \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\I. N x i))"
  "finite I \ (\i. i \ I \ pred M (\x. P x i)) \ pred M (\x. \i\I. P x i)"
  "finite I \ (\i. i \ I \ pred M (\x. P x i)) \ pred M (\x. \i\I. P x i)"
  by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def)

lemma countable_Un_Int[measurable (raw)]:
  "(\i :: 'i :: countable. i \ I \ N i \ sets M) \ (\i\I. N i) \ sets M"
  "I \ {} \ (\i :: 'i :: countable. i \ I \ N i \ sets M) \ (\i\I. N i) \ sets M"
  by auto

declare
  finite_UN[measurable (raw)]
  finite_INT[measurable (raw)]

lemma sets_Int_pred[measurable (raw)]:
  assumes space: "A \ B \ space M" and [measurable]: "pred M (\x. x \ A)" "pred M (\x. x \ B)"
  shows "A \ B \ sets M"
proof -
  have "{x\space M. x \ A \ B} \ sets M" by auto
  also have "{x\space M. x \ A \ B} = A \ B"
    using space by auto
  finally show ?thesis .
qed

lemma [measurable (raw generic)]:
  assumes f: "f \ measurable M N" and c: "c \ space N \ {c} \ sets N"
  shows pred_eq_const1: "pred M (\x. f x = c)"
    and pred_eq_const2: "pred M (\x. c = f x)"
proof -
  show "pred M (\x. f x = c)"
  proof cases
    assume "c \ space N"
    with measurable_sets[OF f c] show ?thesis
      by (auto simp: Int_def conj_commute pred_def)
  next
    assume "c \ space N"
    with f[THEN measurable_space] have "{x \ space M. f x = c} = {}" by auto
    then show ?thesis by (auto simp: pred_def cong: conj_cong)
  qed
  then show "pred M (\x. c = f x)"
    by (simp add: eq_commute)
qed

lemma pred_count_space_const1[measurable (raw)]:
  "f \ measurable M (count_space UNIV) \ Measurable.pred M (\x. f x = c)"
  by (intro pred_eq_const1[where N="count_space UNIV"]) (auto )

lemma pred_count_space_const2[measurable (raw)]:
  "f \ measurable M (count_space UNIV) \ Measurable.pred M (\x. c = f x)"
  by (intro pred_eq_const2[where N="count_space UNIV"]) (auto )

lemma pred_le_const[measurable (raw generic)]:
  assumes f: "f \ measurable M N" and c: "{.. c} \ sets N" shows "pred M (\x. f x \ c)"
  using measurable_sets[OF f c]
  by (auto simp: Int_def conj_commute eq_commute pred_def)

lemma pred_const_le[measurable (raw generic)]:
  assumes f: "f \ measurable M N" and c: "{c ..} \ sets N" shows "pred M (\x. c \ f x)"
  using measurable_sets[OF f c]
  by (auto simp: Int_def conj_commute eq_commute pred_def)

lemma pred_less_const[measurable (raw generic)]:
  assumes f: "f \ measurable M N" and c: "{..< c} \ sets N" shows "pred M (\x. f x < c)"
  using measurable_sets[OF f c]
  by (auto simp: Int_def conj_commute eq_commute pred_def)

lemma pred_const_less[measurable (raw generic)]:
  assumes f: "f \ measurable M N" and c: "{c <..} \ sets N" shows "pred M (\x. c < f x)"
  using measurable_sets[OF f c]
  by (auto simp: Int_def conj_commute eq_commute pred_def)

declare
  sets.Int[measurable (raw)]

lemma pred_in_If[measurable (raw)]:
  "(P \ pred M (\x. x \ A x)) \ (\ P \ pred M (\x. x \ B x)) \
    pred M (\<lambda>x. x \<in> (if P then A x else B x))"
  by auto

lemma sets_range[measurable_dest]:
  "A ` I \ sets M \ i \ I \ A i \ sets M"
  by auto

lemma pred_sets_range[measurable_dest]:
  "A ` I \ sets N \ i \ I \ f \ measurable M N \ pred M (\x. f x \ A i)"
  using pred_sets2[OF sets_range] by auto

lemma sets_All[measurable_dest]:
  "\i. A i \ sets (M i) \ A i \ sets (M i)"
  by auto

lemma pred_sets_All[measurable_dest]:
  "\i. A i \ sets (N i) \ f \ measurable M (N i) \ pred M (\x. f x \ A i)"
  using pred_sets2[OF sets_All, of A N f] by auto

lemma sets_Ball[measurable_dest]:
  "\i\I. A i \ sets (M i) \ i\I \ A i \ sets (M i)"
  by auto

lemma pred_sets_Ball[measurable_dest]:
  "\i\I. A i \ sets (N i) \ i\I \ f \ measurable M (N i) \ pred M (\x. f x \ A i)"
  using pred_sets2[OF sets_Ball, of _ _ _ f] by auto

lemma measurable_finite[measurable (raw)]:
  fixes S :: "'a \ nat set"
  assumes [measurable]: "\i. {x\space M. i \ S x} \ sets M"
  shows "pred M (\x. finite (S x))"
  unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)

lemma measurable_Least[measurable]:
  assumes [measurable]: "(\i::nat. (\x. P i x) \ measurable M (count_space UNIV))"
  shows "(\x. LEAST i. P i x) \ measurable M (count_space UNIV)"
  unfolding measurable_def by (safe intro!: sets_Least) simp_all

lemma measurable_Max_nat[measurable (raw)]:
  fixes P :: "nat \ 'a \ bool"
  assumes [measurable]: "\i. Measurable.pred M (P i)"
  shows "(\x. Max {i. P i x}) \ measurable M (count_space UNIV)"
  unfolding measurable_count_space_eq2_countable
proof safe
  fix n
  have 1: "Max {i. P i x} = the None" if "\i. \n\i. P n x" for x
    by (simp add: Max.infinite infinite_nat_iff_unbounded_le that)
  have 2: "finite {i. P i x}" if "\n\j. \ P n x" for j x
    by (metis bounded_nat_set_is_finite leI mem_Collect_eq that)
  have 3: "P (Max {i. P i x}) x" "i \ Max {i. P i x}" if "P i x" "\n\j. \ P n x" for x i j
      using that 2 Max_in[of "{i. P i x}"] by auto
  have "(\x. Max {i. P i x}) -` {n} \ space M = {x\space M. Max {i. P i x} = n}"
    by auto
  also have "\ =
    {x\<in>space M. if (\<forall>i. \<exists>n\<ge>i. P n x) then the None = n else
      if (\<exists>i. P i x) then P n x \<and> (\<forall>i>n. \<not> P i x)
      else Max {} = n}"
    by (intro arg_cong[where f=Collect] ext)
       (auto simp add: 1 2 3 not_le[symmetric] intro!: Max_eqI)
  also have "\ \ sets M"
    by measurable
  finally show "(\x. Max {i. P i x}) -` {n} \ space M \ sets M" .
qed simp

lemma measurable_Min_nat[measurable (raw)]:
  fixes P :: "nat \ 'a \ bool"
  assumes [measurable]: "\i. Measurable.pred M (P i)"
  shows "(\x. Min {i. P i x}) \ measurable M (count_space UNIV)"
  unfolding measurable_count_space_eq2_countable
proof safe
  fix n
  have 1: "Min {i. P i x} = the None" if "\i. \n\i. P n x" for x
    by (simp add: Min.infinite infinite_nat_iff_unbounded_le that)
  have 2: "finite {i. P i x}" if "\n\j. \ P n x" for j x
    by (metis bounded_nat_set_is_finite leI mem_Collect_eq that)
  have 3: "P (Min {i. P i x}) x" "i \ Min {i. P i x}" if "P i x" "\n\j. \ P n x" for x i j
      using that 2 Min_in[of "{i. P i x}"] by auto

  have "(\x. Min {i. P i x}) -` {n} \ space M = {x\space M. Min {i. P i x} = n}"
    by auto
  also have "\ =
    {x\<in>space M. if (\<forall>i. \<exists>n\<ge>i. P n x) then the None = n else
      if (\<exists>i. P i x) then P n x \<and> (\<forall>i<n. \<not> P i x)
      else Min {} = n}"
    by (intro arg_cong[where f=Collect] ext)
       (auto simp add: 1 2 3 not_le[symmetric] intro!: Min_eqI)
  also have "\ \ sets M"
    by measurable
  finally show "(\x. Min {i. P i x}) -` {n} \ space M \ sets M" .
qed simp

lemma measurable_count_space_insert[measurable (raw)]:
  "s \ S \ A \ sets (count_space S) \ insert s A \ sets (count_space S)"
  by simp

lemma sets_UNIV [measurable (raw)]: "A \ sets (count_space UNIV)"
  by simp

lemma measurable_card[measurable]:
  fixes S :: "'a \ nat set"
  assumes [measurable]: "\i. {x\space M. i \ S x} \ sets M"
  shows "(\x. card (S x)) \ measurable M (count_space UNIV)"
  unfolding measurable_count_space_eq2_countable
proof safe
  fix n show "(\x. card (S x)) -` {n} \ space M \ sets M"
  proof (cases n)
    case 0
    then have "(\x. card (S x)) -` {n} \ space M = {x\space M. infinite (S x) \ (\i. i \ S x)}"
      by auto
    also have "\ \ sets M"
      by measurable
    finally show ?thesis .
  next
    case (Suc i)
    then have "(\x. card (S x)) -` {n} \ space M =
               (\<Union>F\<in>{A\<in>{A. finite A}. card A = n}. {x\<in>space M. (\<forall>i. i \<in> S x \<longleftrightarrow> i \<in> F)})"
      unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite)
    also have "\ \ sets M"
      by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto
    finally show ?thesis .
  qed
qed rule

lemma measurable_pred_countable[measurable (raw)]:
  assumes "countable X"
  shows
    "(\i. i \ X \ Measurable.pred M (\x. P x i)) \ Measurable.pred M (\x. \i\X. P x i)"
    "(\i. i \ X \ Measurable.pred M (\x. P x i)) \ Measurable.pred M (\x. \i\X. P x i)"
  unfolding pred_def
  by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms)

subsection\<^marker>\<open>tag unimportant\<close> \<open>Measurability for (co)inductive predicates\<close>

lemma measurable_bot[measurable]: "bot \ measurable M (count_space UNIV)"
  by (simp add: bot_fun_def)

lemma measurable_top[measurable]: "top \ measurable M (count_space UNIV)"
  by (simp add: top_fun_def)

lemma measurable_SUP[measurable]:
  fixes F :: "'i \ 'a \ 'b::{complete_lattice, countable}"
  assumes [simp]: "countable I"
  assumes [measurable]: "\i. i \ I \ F i \ measurable M (count_space UNIV)"
  shows "(\x. SUP i\I. F i x) \ measurable M (count_space UNIV)"
  unfolding measurable_count_space_eq2_countable
proof (intro conjI strip)
  fix a
  have "(\x. SUP i\I. F i x) -` {a} \ space M =
        {x\<in>space M. (\<forall>i\<in>I. F i x \<le> a) \<and> (\<forall>b. (\<forall>i\<in>I. F i x \<le> b) \<longrightarrow> a \<le> b)}"
    unfolding SUP_le_iff[symmetric] by auto
  also have "\ \ sets M"
    by measurable
  finally show "(\x. SUP i\I. F i x) -` {a} \ space M \ sets M" .
qed auto

lemma measurable_INF[measurable]:
  fixes F :: "'i \ 'a \ 'b::{complete_lattice, countable}"
  assumes [simp]: "countable I"
  assumes [measurable]: "\i. i \ I \ F i \ measurable M (count_space UNIV)"
  shows "(\x. INF i\I. F i x) \ measurable M (count_space UNIV)"
  unfolding measurable_count_space_eq2_countable
proof (intro conjI strip)
  fix a
  have "(\x. INF i\I. F i x) -` {a} \ space M =
        {x\<in>space M. (\<forall>i\<in>I. a \<le> F i x) \<and> (\<forall>b. (\<forall>i\<in>I. b \<le> F i x) \<longrightarrow> b \<le> a)}"
    unfolding le_INF_iff[symmetric] by auto
  also have "\ \ sets M"
    by measurable
  finally show "(\x. INF i\I. F i x) -` {a} \ space M \ sets M" .
qed auto

lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
  fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})"
  assumes "P M"
  assumes F: "sup_continuous F"
  assumes *: "\M A. P M \ (\N. P N \ A \ measurable N (count_space UNIV)) \ F A \ measurable M (count_space UNIV)"
  shows "lfp F \ measurable M (count_space UNIV)"
proof -
  have "((F ^^ i) bot) \ measurable M (count_space UNIV)" for i
    using \<open>P M\<close> by (induct i arbitrary: M) (auto intro!: *)
  then have "(\x. SUP i. (F ^^ i) bot x) \ measurable M (count_space UNIV)"
    by measurable
  also have "(\x. SUP i. (F ^^ i) bot x) = lfp F"
    by (subst sup_continuous_lfp) (auto intro: F simp: image_comp)
  finally show ?thesis .
qed

lemma measurable_lfp:
  fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})"
  assumes F: "sup_continuous F"
  assumes *: "\A. A \ measurable M (count_space UNIV) \ F A \ measurable M (count_space UNIV)"
  shows "lfp F \ measurable M (count_space UNIV)"
  by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *)

lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]:
  fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})"
  assumes "P M"
  assumes F: "inf_continuous F"
  assumes *: "\M A. P M \ (\N. P N \ A \ measurable N (count_space UNIV)) \ F A \ measurable M (count_space UNIV)"
  shows "gfp F \ measurable M (count_space UNIV)"
proof -
  have "((F ^^ i) top) \ measurable M (count_space UNIV)" for i
    using \<open>P M\<close> by (induct i arbitrary: M) (auto intro!: *)
  then have "(\x. INF i. (F ^^ i) top x) \ measurable M (count_space UNIV)"
    by measurable
  also have "(\x. INF i. (F ^^ i) top x) = gfp F"
    by (subst inf_continuous_gfp) (auto intro: F simp: image_comp)
  finally show ?thesis .
qed

lemma measurable_gfp:
  fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})"
  assumes F: "inf_continuous F"
  assumes *: "\A. A \ measurable M (count_space UNIV) \ F A \ measurable M (count_space UNIV)"
  shows "gfp F \ measurable M (count_space UNIV)"
  by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *)

lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]:
  fixes F :: "('a \ 'c \ 'b) \ ('a \ 'c \ 'b::{complete_lattice, countable})"
  assumes "P M s"
  assumes F: "sup_continuous F"
  assumes *: "\M A s. P M s \ (\N t. P N t \ A t \ measurable N (count_space UNIV)) \ F A s \ measurable M (count_space UNIV)"
  shows "lfp F s \ measurable M (count_space UNIV)"
proof -
  have "(\x. (F ^^ i) bot s x) \ measurable M (count_space UNIV)" for i
    using \<open>P M s\<close> by (induct i arbitrary: M s) (auto intro!: *)
  then have "(\x. SUP i. (F ^^ i) bot s x) \ measurable M (count_space UNIV)"
    by measurable
  also have "(\x. SUP i. (F ^^ i) bot s x) = lfp F s"
    by (subst sup_continuous_lfp) (auto simp: F simp: image_comp)
  finally show ?thesis .
qed

lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]:
  fixes F :: "('a \ 'c \ 'b) \ ('a \ 'c \ 'b::{complete_lattice, countable})"
  assumes "P M s"
  assumes F: "inf_continuous F"
  assumes *: "\M A s. P M s \ (\N t. P N t \ A t \ measurable N (count_space UNIV)) \ F A s \ measurable M (count_space UNIV)"
  shows "gfp F s \ measurable M (count_space UNIV)"
proof -
  have "(\x. (F ^^ i) top s x) \ measurable M (count_space UNIV)" for i
    using \<open>P M s\<close> by (induct i arbitrary: M s) (auto intro!: *)
  then have "(\x. INF i. (F ^^ i) top s x) \ measurable M (count_space UNIV)"
    by measurable
  also have "(\x. INF i. (F ^^ i) top s x) = gfp F s"
    by (subst inf_continuous_gfp) (auto simp: F simp: image_comp)
  finally show ?thesis .
qed

lemma measurable_enat_coinduct:
  fixes f :: "'a \ enat"
  assumes "R f"
  assumes *: "\f. R f \ \g h i P. R g \ f = (\x. if P x then h x else eSuc (g (i x))) \
    Measurable.pred M P \<and>
    i \<in> measurable M M \<and>
    h \<in> measurable M (count_space UNIV)"
  shows "f \ measurable M (count_space UNIV)"
proof (simp add: measurable_count_space_eq2_countable, rule )
  fix a :: enat
  have "f -` {a} \ space M = {x\space M. f x = a}"
    by auto
  have "Measurable.pred M (\x. f x = enat i)" for i
    using \<open>R f\<close>
  proof (induction i arbitrary: f)
    case 0
    from *[OF this] obtain g h i P
      where f: "f = (\x. if P x then h x else eSuc (g (i x)))" and
        [measurable]: "Measurable.pred M P" "i \ measurable M M" "h \ measurable M (count_space UNIV)"
      by auto
    have "Measurable.pred M (\x. P x \ h x = 0)"
      by measurable
    also have "(\x. P x \ h x = 0) = (\x. f x = enat 0)"
      by (auto simp: f zero_enat_def[symmetric])
    finally show ?case .
  next
    case (Suc n)
    from *[OF Suc.prems] obtain g h i P
      where f: "f = (\x. if P x then h x else eSuc (g (i x)))" and "R g" and
        M[measurable]: "Measurable.pred M P" "i \ measurable M M" "h \ measurable M (count_space UNIV)"
      by auto
    have "(\x. f x = enat (Suc n)) =
        (\<lambda>x. (P x \<longrightarrow> h x = enat (Suc n)) \<and> (\<not> P x \<longrightarrow> g (i x) = enat n))"
      by (auto simp: f zero_enat_def[symmetric] eSuc_enat[symmetric])
    also have "Measurable.pred M \"
      by (intro pred_intros_logic measurable_compose[OF M(2)] Suc \<open>R g\<close>) measurable
    finally show ?case .
  qed
  then have fin: "f -` {enat i} \ space M \ sets M" for i
    by (simp add: pred_def Int_def conj_commute)
  show "f -` {a} \ space M \ sets M"
  proof (cases a)
    case infinity
    then have "f -` {a} \ space M = space M - (\n. f -` {enat n} \ space M)"
      by auto
    also have "\ \ sets M"
      by (intro sets.Diff sets.top sets.Un sets.countable_UN) (auto intro!: fin)
    finally show ?thesis .
  qed (simp add: fin)
qed

lemma measurable_THE:
  fixes P :: "'a \ 'b \ bool"
  assumes [measurable]: "\i. Measurable.pred M (P i)"
  assumes I[simp]: "countable I" "\i x. x \ space M \ P i x \ i \ I"
  assumes unique: "\x i j. x \ space M \ P i x \ P j x \ i = j"
  shows "(\x. THE i. P i x) \ measurable M (count_space UNIV)"
  unfolding measurable_def
proof safe
  fix X
  define f where "f x = (THE i. P i x)" for x
  define undef where "undef = (THE i::'a. False)"
  have f_eq: "f x = i" if "x \ space M" "P i x" for i x
    unfolding f_def using unique that by auto
  have "f x = undef" if "x \ space M" "\i\I. \ P i x" for x
    using that I f_def undef_def by moura
  then have "f -` X \ space M =
             (\<Union>i\<in>I \<inter> X. {x\<in>space M. P i x}) \<union> (if undef \<in> X then space M - (\<Union>i\<in>I. {x\<in>space M. P i x}) else {})"
    by (auto dest: f_eq)
  also have "\ \ sets M"
    by (auto intro!: sets.Diff sets.countable_UN')
  finally show "f -` X \ space M \ sets M" .
qed simp

lemma measurable_Ex1[measurable (raw)]:
  assumes [simp]: "countable I" and [measurable]: "\i. i \ I \ Measurable.pred M (P i)"
  shows "Measurable.pred M (\x. \!i\I. P i x)"
  unfolding bex1_def by measurable

lemma measurable_Sup_nat[measurable (raw)]:
  fixes F :: "'a \ nat set"
  assumes [measurable]: "\i. Measurable.pred M (\x. i \ F x)"
  shows "(\x. Sup (F x)) \ M \\<^sub>M count_space UNIV"
proof (clarsimp simp add: measurable_count_space_eq2_countable)
  fix a
  have F_empty_iff: "F x = {} \ (\i. i \ F x)" for x
    by auto
  have "Measurable.pred M (\x. if finite (F x) then if F x = {} then a = 0
    else a \<in> F x \<and> (\<forall>j. j \<in> F x \<longrightarrow> j \<le> a) else a = the None)"
    unfolding finite_nat_set_iff_bounded Ball_def F_empty_iff by measurable
  moreover have "(\x. Sup (F x)) -` {a} \ space M =
    {x\<in>space M. if finite (F x) then if F x = {} then a = 0
      else a \<in> F x \<and> (\<forall>j. j \<in> F x \<longrightarrow> j \<le> a) else a = the None}"
    by (intro set_eqI)
       (auto simp: Sup_nat_def Max.infinite intro!: Max_in Max_eqI)
  ultimately show "(\x. Sup (F x)) -` {a} \ space M \ sets M"
    by auto
qed

lemma measurable_if_split[measurable (raw)]:
  "(c \ Measurable.pred M f) \ (\ c \ Measurable.pred M g) \
   Measurable.pred M (if c then f else g)"
  by simp

lemma pred_restrict_space:
  assumes "S \ sets M"
  shows "Measurable.pred (restrict_space M S) P \ Measurable.pred M (\x. x \ S \ P x)"
  unfolding pred_def sets_Collect_restrict_space_iff[OF assms] ..

lemma measurable_predpow[measurable]:
  assumes "Measurable.pred M T"
  assumes "\Q. Measurable.pred M Q \ Measurable.pred M (R Q)"
  shows "Measurable.pred M ((R ^^ n) T)"
  by (induct n) (auto intro: assms)

lemma measurable_compose_countable_restrict:
  assumes P: "countable {i. P i}"
    and f: "f \ M \\<^sub>M count_space UNIV"
    and Q: "\i. P i \ pred M (Q i)"
  shows "pred M (\x. P (f x) \ Q (f x) x)"
proof -
  have P_f: "{x \ space M. P (f x)} \ sets M"
    unfolding pred_def[symmetric] by (rule measurable_compose[OF f]) simp
  have "pred (restrict_space M {x\space M. P (f x)}) (\x. Q (f x) x)"
  proof (rule measurable_compose_countable'[OF _ _ P])
    show "f \ restrict_space M {x\space M. P (f x)} \\<^sub>M count_space {i. P i}"
      by (rule measurable_count_space_extend[OF subset_UNIV])
         (auto simp: space_restrict_space intro!: measurable_restrict_space1 f)
  qed (auto intro!: measurable_restrict_space1 Q)
  then show ?thesis
    unfolding pred_restrict_space[OF P_f] by (simp cong: measurable_cong)
qed

lemma measurable_limsup [measurable (raw)]:
  assumes [measurable]: "\n. A n \ sets M"
  shows "limsup A \ sets M"
by (subst limsup_INF_SUP, auto)

lemma measurable_liminf [measurable (raw)]:
  assumes [measurable]: "\n. A n \ sets M"
  shows "liminf A \ sets M"
by (subst liminf_SUP_INF, auto)

lemma measurable_case_enat[measurable (raw)]:
  assumes f: "f \ M \\<^sub>M count_space UNIV" and g: "\i. g i \ M \\<^sub>M N" and h: "h \ M \\<^sub>M N"
  shows "(\x. case f x of enat i \ g i x | \ \ h x) \ M \\<^sub>M N"
proof (rule measurable_compose_countable[OF _ f])
  show "(\x. case i of enat i \ g i x | \ \ h x) \ M \\<^sub>M N" for i
    by (cases i) (auto intro: g h)
qed

hide_const (open) pred

end

quality100%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.