equal
deleted
inserted
replaced
813 qed |
813 qed |
814 |
814 |
815 lemma borel_measurable_log[measurable (raw)]: |
815 lemma borel_measurable_log[measurable (raw)]: |
816 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M" |
816 "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M" |
817 unfolding log_def by auto |
817 unfolding log_def by auto |
|
818 |
|
819 lemma borel_measurable_exp[measurable]: "exp \<in> borel_measurable borel" |
|
820 by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI |
|
821 continuous_isCont[THEN iffD1] isCont_exp) |
818 |
822 |
819 lemma measurable_count_space_eq2_countable: |
823 lemma measurable_count_space_eq2_countable: |
820 fixes f :: "'a => 'c::countable" |
824 fixes f :: "'a => 'c::countable" |
821 shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))" |
825 shows "f \<in> measurable M (count_space A) \<longleftrightarrow> (f \<in> space M \<rightarrow> A \<and> (\<forall>a\<in>A. f -` {a} \<inter> space M \<in> sets M))" |
822 proof - |
826 proof - |