src/HOL/Probability/Infinite_Product_Measure.thy

 (*  Title:      HOL/Probability/Infinite_Product_Measure.thy
     Author:     Johannes Hölzl, TU München
 *)
 
-section {*Infinite Product Measure*}
+section \<open>Infinite Product Measure\<close>
 
 theory Infinite_Product_Measure
   imports Probability_Measure Caratheodory Projective_Family
 begin
 

 proof (rule measure_eqI[symmetric])
   fix A assume "A \<in> sets (M i)"
   moreover have "((\<lambda>\<omega>. \<omega> i) -` A \<inter> space (PiM I M)) = {x\<in>space (PiM I M). x i \<in> A}"
     by auto
   ultimately show "emeasure (M i) A = emeasure (distr (PiM I M) (M i) (\<lambda>\<omega>. \<omega> i)) A"
-    by (auto simp: `i\<in>I` emeasure_distr measurable_component_singleton emeasure_PiM_Collect_single)
+    by (auto simp: \<open>i\<in>I\<close> emeasure_distr measurable_component_singleton emeasure_PiM_Collect_single)
 qed simp
 
 lemma (in product_prob_space) PiM_eq:
   assumes M': "sets M' = sets (PiM I M)"
   assumes eq: "\<And>J F. finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> (\<And>j. j \<in> J \<Longrightarrow> F j \<in> sets (M j)) \<Longrightarrow>

   apply simp
   apply (subst PiM_component)
   apply simp_all
   done
 
-subsection {* Sequence space *}
+subsection \<open>Sequence space\<close>
 
 definition comb_seq :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)" where
   "comb_seq i \<omega> \<omega>' j = (if j < i then \<omega> j else \<omega>' (j - i))"
 
 lemma split_comb_seq: "P (comb_seq i \<omega> \<omega>' j) \<longleftrightarrow> (j < i \<longrightarrow> P (\<omega> j)) \<and> (\<forall>k. j = i + k \<longrightarrow> P (\<omega>' k))"