diff --git a/thys/Doob_Convergence/Stopping_Time.thy b/thys/Doob_Convergence/Stopping_Time.thy
--- a/thys/Doob_Convergence/Stopping_Time.thy
+++ b/thys/Doob_Convergence/Stopping_Time.thy
@@ -1,524 +1,524 @@
 (*  Author:     Ata Keskin, TU München 
 *)
 
 section \<open>Stopping Times and Hitting Times\<close>
 
 text \<open>In this section we formalize stopping times and hitting times. A stopping time is a random variable that represents the time at which a certain event occurs within a stochastic process. 
       A hitting time, also known as first passage time or first hitting time, is a specific type of stopping time that represents the first time a stochastic process reaches a particular state or crosses a certain threshold.\<close>
 
 theory Stopping_Time
-imports Martingales_Updates
+imports Martingales.Stochastic_Process
 begin                      
 
 subsection \<open>Stopping Time\<close>
 
 text \<open>The formalization of stopping times here is simply a rewrite of the document \<open>HOL-Probability.Stopping_Time\<close> \<^cite>\<open>"hoelzl2011measuretheory"\<close>.
       We have adapted the document to use the locales defined in our formalization of filtered measure spaces \<^cite>\<open>keskin2023formalization\<close> \<^cite>\<open>"Martingales-AFP"\<close>.
-      This way we can omit the partial formalization of filtrations in the original document. Furthermore, we can include the initial time index \<^term>\<open>t\<^sub>0\<close> that we introduced as well.\<close>
+      This way, we can omit the partial formalization of filtrations in the original document. Furthermore, we can include the initial time index \<^term>\<open>t\<^sub>0\<close> that we introduced as well.\<close>
 
 context linearly_filtered_measure
 begin
 
 \<comment> \<open>A stopping time is a measurable function from the measure space (possible events) into the time axis.\<close>
 
 definition stopping_time :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where
   "stopping_time T = ((T \<in> space M \<rightarrow> {t\<^sub>0..}) \<and> (\<forall>t\<ge>t\<^sub>0. Measurable.pred (F t) (\<lambda>x. T x \<le> t)))"
 
 lemma stopping_time_cong: 
   assumes "\<And>t x. t \<ge> t\<^sub>0 \<Longrightarrow> x \<in> space (F t) \<Longrightarrow> T x = S x"
   shows "stopping_time T = stopping_time S"
 proof (cases "T \<in> space M \<rightarrow> {t\<^sub>0..}")
   case True
   hence "S \<in> space M \<rightarrow> {t\<^sub>0..}" using assms space_F by force
   then show ?thesis unfolding stopping_time_def 
     using assms arg_cong[where f="(\<lambda>P. \<forall>t\<ge>t\<^sub>0. P t)"] measurable_cong[where M="F _" and f="\<lambda>x. T x \<le> _" and g="\<lambda>x. S x \<le> _"] True by metis
 next
   case False
   hence "S \<notin> space M \<rightarrow> {t\<^sub>0..}" using assms space_F by force
   then show ?thesis unfolding stopping_time_def using False by blast
 qed
 
 lemma stopping_time_ge_zero:
   assumes "stopping_time T" "\<omega> \<in> space M"
   shows "T \<omega> \<ge> t\<^sub>0"
   using assms unfolding stopping_time_def by auto
 
 lemma stopping_timeD: 
   assumes "stopping_time T" "t \<ge> t\<^sub>0"
   shows "Measurable.pred (F t) (\<lambda>x. T x \<le> t)"
   using assms unfolding stopping_time_def by simp
 
 lemma stopping_timeI[intro?]: 
   assumes "\<And>x. x \<in> space M \<Longrightarrow> T x \<ge> t\<^sub>0"
           "(\<And>t. t \<ge> t\<^sub>0 \<Longrightarrow> Measurable.pred (F t) (\<lambda>x. T x \<le> t))"
   shows "stopping_time T"
   using assms by (auto simp: stopping_time_def)
 
 lemma stopping_time_measurable:
   assumes "stopping_time T"
   shows "T \<in> borel_measurable M"
 proof (rule borel_measurableI_le)
   {
     fix t assume "\<not> t \<ge> t\<^sub>0"
     hence "{x \<in> space M. T x \<le> t} = {}" using assms dual_order.trans[of _ t "t\<^sub>0"] unfolding stopping_time_def by fastforce
     hence "{x \<in> space M. T x \<le> t} \<in> sets M" by (metis sets.empty_sets)
   }
   moreover
   {
     fix t assume asm: "t \<ge> t\<^sub>0"
     hence "{x \<in> space M. T x \<le> t} \<in> sets M" using stopping_timeD[OF assms asm] sets_F_subset unfolding Measurable.pred_def space_F[OF asm] by blast
   }
   ultimately show "{x \<in> space M. T x \<le> t} \<in> sets M" for t by blast
 qed
 
 lemma stopping_time_const: 
   assumes "t \<ge> t\<^sub>0"
   shows "stopping_time (\<lambda>x. t)" using assms by (auto simp: stopping_time_def)
 
 lemma stopping_time_min:
   assumes "stopping_time T" "stopping_time S"
   shows "stopping_time (\<lambda>x. min (T x) (S x))"
   using assms by (auto simp: stopping_time_def min_le_iff_disj intro!: pred_intros_logic)
 
 lemma stopping_time_max:
   assumes "stopping_time T" "stopping_time S"
   shows "stopping_time (\<lambda>x. max (T x) (S x))"
   using assms by (auto simp: stopping_time_def intro!: pred_intros_logic max.coboundedI1) 
 
 subsection \<open>\<open>\<sigma>\<close>-algebra of a Stopping Time\<close>
 
 text \<open>Moving on, we define the \<open>\<sigma>\<close>-algebra associated with a stopping time \<^term>\<open>T\<close>.
       It contains all the information up to time \<^term>\<open>T\<close>, the same way \<^term>\<open>F t\<close> contains all the information up to time \<^term>\<open>t\<close>.\<close>
 
 definition pre_sigma :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a measure" where
   "pre_sigma T = sigma (space M) {A \<in> sets M. \<forall>t\<ge>t\<^sub>0. {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)}"
 
 lemma measure_pre_sigma[simp]: "emeasure (pre_sigma T) = (\<lambda>_. 0)" by (simp add: pre_sigma_def emeasure_sigma)
 
 lemma sigma_algebra_pre_sigma:
   assumes "stopping_time T"
   shows "sigma_algebra (space M) {A \<in> sets M. \<forall>t\<ge>t\<^sub>0. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
 proof -
   let ?\<Sigma> = "{A \<in> sets M. \<forall>t\<ge>t\<^sub>0. {\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)}"
   {
     fix A assume asm: "A \<in> ?\<Sigma>"
     {
       fix t assume asm': "t \<ge> t\<^sub>0"
       hence "{\<omega>\<in>A. T \<omega> \<le> t} \<in> sets (F t)" using asm by blast
       then have "{\<omega> \<in> space (F t). T \<omega> \<le> t} - {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)" using assms[THEN stopping_timeD, OF asm'] by auto
       also have "{\<omega> \<in> space (F t). T \<omega> \<le> t} - {\<omega> \<in> A. T \<omega> \<le> t} = {\<omega> \<in> space M - A. T \<omega> \<le> t}" using space_F[OF asm'] by blast
       finally have "{\<omega> \<in> (space M) - A. T \<omega> \<le> t} \<in> sets (F t)" .
     }
     hence "space M - A \<in> ?\<Sigma>" using asm by blast
   }
   moreover 
   {
     fix A :: "nat \<Rightarrow> 'a set" assume asm: "range A \<subseteq> ?\<Sigma>"
     {
       fix t assume "t \<ge> t\<^sub>0"
       then have "(\<Union>i. {\<omega> \<in> A i. T \<omega> \<le> t}) \<in> sets (F t)" using asm by auto
       also have "(\<Union>i. {\<omega> \<in> A i. T \<omega> \<le> t}) = {\<omega> \<in> \<Union>(A ` UNIV). T \<omega> \<le> t}" by auto
       finally have "{\<omega> \<in> \<Union>(range A). T \<omega> \<le> t} \<in> sets (F t)" .
     }
     hence "\<Union>(range A) \<in> ?\<Sigma>" using asm by blast
   }
   ultimately show ?thesis unfolding sigma_algebra_iff2 by (auto intro!: sets.sets_into_space[THEN PowI, THEN subsetI])
 qed
 
 lemma space_pre_sigma[simp]: "space (pre_sigma T) = space M" unfolding pre_sigma_def by (intro space_measure_of_conv)
 
 lemma sets_pre_sigma: 
   assumes "stopping_time T"
   shows "sets (pre_sigma T) = {A \<in> sets M. \<forall>t\<ge>t\<^sub>0. {\<omega>\<in>A. T \<omega> \<le> t} \<in> F t}"
   unfolding pre_sigma_def using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_pre_sigma, OF assms] by blast
 
 lemma sets_pre_sigmaI: 
   assumes "stopping_time T"
       and "\<And>t. t \<ge> t\<^sub>0 \<Longrightarrow> {\<omega> \<in> A. T \<omega> \<le> t} \<in> F t"
     shows "A \<in> pre_sigma T"
 proof (cases "\<exists>t\<ge>t\<^sub>0. \<forall>t'. t' \<le> t")
   case True
   then obtain t where "t \<ge> t\<^sub>0" "{\<omega> \<in> A. T \<omega> \<le> t} = A" by blast
   hence "A \<in> M" using assms(2)[of t] sets_F_subset[of t] by fastforce
   thus ?thesis using assms(2) unfolding sets_pre_sigma[OF assms(1)] by blast
 next
   case False
   hence *: "{t<..} \<noteq> {}" if "t \<ge> t\<^sub>0" for t by (metis not_le empty_iff greaterThan_iff)
   obtain D :: "'b set" where D: "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> D \<inter> X \<noteq> {}" by (metis countable_dense_setE disjoint_iff)
   have **: "D \<inter> {t<..} \<noteq> {}" if "t \<ge> t\<^sub>0" for t using * that by (intro D(2)) auto
   {
     fix \<omega>
     obtain t where t: "t \<ge> t\<^sub>0" "T \<omega> \<le> t" using linorder_linear by auto
     moreover obtain t' where "t' \<in> D \<inter> {t<..} \<inter> {t\<^sub>0..}" using ** t by fastforce
     moreover have "T \<omega> \<le> t'" using calculation by fastforce
     ultimately have "\<exists>t. \<exists>t' \<in> D \<inter> {t<..} \<inter> {t\<^sub>0..}. T \<omega> \<le> t'" by blast
   }
   hence "(\<Union>t'\<in>(\<Union>t. D \<inter> {t<..} \<inter> {t\<^sub>0..}). {\<omega> \<in> A. T \<omega> \<le> t'}) = A" by fast
   moreover have "(\<Union>t'\<in>(\<Union>t. D \<inter> {t<..} \<inter> {t\<^sub>0..}). {\<omega> \<in> A. T \<omega> \<le> t'}) \<in> M" using D assms(2) sets_F_subset by (intro sets.countable_UN'', fastforce, fast) 
   ultimately have "A \<in> M" by argo
   thus ?thesis using assms(2) unfolding sets_pre_sigma[OF assms(1)] by blast
 qed
 
 lemma pred_pre_sigmaI:
   assumes "stopping_time T"
   shows "(\<And>t. t \<ge> t\<^sub>0 \<Longrightarrow> Measurable.pred (F t) (\<lambda>\<omega>. P \<omega> \<and> T \<omega> \<le> t)) \<Longrightarrow> Measurable.pred (pre_sigma T) P"
   unfolding pred_def space_pre_sigma using assms by (auto intro: sets_pre_sigmaI[OF assms(1)])
 
 lemma sets_pre_sigmaD: 
   assumes "stopping_time T" "A \<in> pre_sigma T" "t \<ge> t\<^sub>0" 
   shows "{\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)"
   using assms sets_pre_sigma by auto
 
 lemma borel_measurable_stopping_time_pre_sigma:
   assumes "stopping_time T" 
   shows "T \<in> borel_measurable (pre_sigma T)"
 proof (intro borel_measurableI_le sets_pre_sigmaI[OF assms])
   fix t t' assume asm: "t \<ge> t\<^sub>0"
   {
     assume "\<not> t' \<ge> t\<^sub>0"
     hence "{\<omega> \<in> {x \<in> space (pre_sigma T). T x \<le> t'}. T \<omega> \<le> t} = {}" using assms dual_order.trans[of _ t' "t\<^sub>0"] unfolding stopping_time_def by fastforce
     hence "{\<omega> \<in> {x \<in> space (pre_sigma T). T x \<le> t'}. T \<omega> \<le> t} \<in> sets (F t)" by (metis sets.empty_sets)
   }
   moreover
   {
     assume asm': "t' \<ge> t\<^sub>0"
     have "{\<omega> \<in> space (F (min t' t)). T \<omega> \<le> min t' t} \<in> sets (F (min t' t))"
       using assms asm asm' unfolding pred_def[symmetric] by (intro stopping_timeD) auto
     also have "\<dots> \<subseteq> sets (F t)"
       using assms asm asm' by (intro sets_F_mono) auto
     finally have "{\<omega> \<in> {x \<in> space (pre_sigma T). T x \<le> t'}. T \<omega> \<le> t} \<in> sets (F t)"
       using asm asm' by simp
   }
   ultimately show "{\<omega> \<in> {x \<in> space (pre_sigma T). T x \<le> t'}. T \<omega> \<le> t} \<in> sets (F t)" by blast
 qed
 
 lemma mono_pre_sigma:
   assumes "stopping_time T" "stopping_time S"
       and "\<And>x. x \<in> space M \<Longrightarrow> T x \<le> S x"
     shows "pre_sigma T \<subseteq> pre_sigma S"
 proof
   fix A assume "A \<in> pre_sigma T"
   hence asm: "A \<in> sets M" "t \<ge> t\<^sub>0 \<Longrightarrow> {\<omega> \<in> A. T \<omega> \<le> t} \<in> sets (F t)" for t using assms sets_pre_sigma by blast+
   {
     fix t assume asm': "t \<ge> t\<^sub>0"
     then have "A \<subseteq> space M" using sets.sets_into_space asm by blast
     have "{\<omega>\<in>A. T \<omega> \<le> t} \<inter> {\<omega>\<in>space (F t). S \<omega> \<le> t} \<in> sets (F t)"
       using asm asm' stopping_timeD[OF assms(2)] by (auto simp: pred_def)
     also have "{\<omega>\<in>A. T \<omega> \<le> t} \<inter> {\<omega>\<in>space (F t). S \<omega> \<le> t} = {\<omega>\<in>A. S \<omega> \<le> t}"
       using sets.sets_into_space[OF asm(1)] assms(3) order_trans asm' by fastforce
     finally have "{\<omega>\<in>A. S \<omega> \<le> t} \<in> sets (F t)" by simp
   }
   thus "A \<in> pre_sigma S" by (intro sets_pre_sigmaI assms asm) blast
 qed
 
 lemma stopping_time_measurable_le: 
   assumes "stopping_time T" "s \<ge> t\<^sub>0" "t \<ge> s" 
   shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> \<le> s)"
   using assms stopping_timeD[of T] sets_F_mono[of _ t] by (auto simp: pred_def)
 
 lemma stopping_time_measurable_less:
   assumes "stopping_time T" "s \<ge> t\<^sub>0" "t \<ge> s"
   shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < s)"
 proof -
   have "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < t)" if asm: "stopping_time T" "t \<ge> t\<^sub>0" for T t
   proof - 
     obtain D :: "'b set" where D: "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> D \<inter> X \<noteq> {}" by (metis countable_dense_setE disjoint_iff)
     show ?thesis
     proof cases
       assume *: "\<forall>t'\<in>{t\<^sub>0..<t}. {t'<..<t} \<noteq> {}"
       hence **: "D \<inter> {t'<..< t} \<noteq> {}" if "t' \<in> {t\<^sub>0..<t}" for t' using that by (intro D(2)) fastforce+
   
       show ?thesis
       proof (rule measurable_cong[THEN iffD2])
         show "T \<omega> < t \<longleftrightarrow> (\<exists>r\<in>D \<inter> {t\<^sub>0..<t}. T \<omega> \<le> r)" if "\<omega> \<in> space (F t)" for \<omega> 
           using **[of "T \<omega>"] that less_imp_le stopping_time_ge_zero asm by fastforce
         show "Measurable.pred (F t) (\<lambda>w. \<exists>r\<in>D \<inter> {t\<^sub>0..<t}. T w \<le> r)"
           using stopping_time_measurable_le asm D by (intro measurable_pred_countable) auto
       qed
     next
       assume "\<not> (\<forall>t'\<in>{t\<^sub>0..<t}. {t'<..<t} \<noteq> {})"
       then obtain t' where t': "t' \<in> {t\<^sub>0..<t}" "{t'<..<t} = {}" by blast
       show ?thesis
       proof (rule measurable_cong[THEN iffD2])
         show "T \<omega> < t \<longleftrightarrow> T \<omega> \<le> t'" for \<omega> using t' by (metis atLeastLessThan_iff emptyE greaterThanLessThan_iff linorder_not_less order.strict_trans1)
         show "Measurable.pred (F t) (\<lambda>w. T w \<le> t')" using t' by (intro stopping_time_measurable_le[OF asm(1)]) auto
       qed
     qed
   qed
   thus ?thesis
   using assms sets_F_mono[of _ t] by (auto simp add: pred_def)
 qed
 
 lemma stopping_time_measurable_ge:
   assumes "stopping_time T" "s \<ge> t\<^sub>0" "t \<ge> s"
   shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> \<ge> s)"
   by (auto simp: not_less[symmetric] intro: stopping_time_measurable_less[OF assms] Measurable.pred_intros_logic)
 
 lemma stopping_time_measurable_gr: 
   assumes "stopping_time T" "s \<ge> t\<^sub>0" "t \<ge> s"
   shows "Measurable.pred (F t) (\<lambda>x. s < T x)"
   by (auto simp add: not_le[symmetric] intro: stopping_time_measurable_le[OF assms] Measurable.pred_intros_logic)
 
 lemma stopping_time_measurable_eq:
   assumes "stopping_time T" "s \<ge> t\<^sub>0" "t \<ge> s"
   shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> = s)"
   unfolding eq_iff using stopping_time_measurable_le[OF assms] stopping_time_measurable_ge[OF assms]
   by (intro pred_intros_logic)
 
 lemma stopping_time_less_stopping_time:
   assumes "stopping_time T" "stopping_time S"
   shows "Measurable.pred (pre_sigma T) (\<lambda>\<omega>. T \<omega> < S \<omega>)"
 proof (rule pred_pre_sigmaI)
   fix t assume asm: "t \<ge> t\<^sub>0"
   obtain D :: "'b set" where D: "countable D" and semidense_D: "\<And>x y. x < y \<Longrightarrow> (\<exists>b\<in>D. x \<le> b \<and> b < y)"
     using countable_separating_set_linorder2 by auto
   show "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < S \<omega> \<and> T \<omega> \<le> t)"
   proof (rule measurable_cong[THEN iffD2])
     let ?f = "\<lambda>\<omega>. if T \<omega> = t then \<not> S \<omega> \<le> t else \<exists>s\<in>D \<inter> {t\<^sub>0..t}. T \<omega> \<le> s \<and> \<not> (S \<omega> \<le> s)"
     { 
       fix \<omega> assume "\<omega> \<in> space (F t)" "T \<omega> \<le> t" "T \<omega> \<noteq> t" "T \<omega> < S \<omega>"
       hence "t\<^sub>0 \<le> T \<omega>" "T \<omega> < min t (S \<omega>)" using asm stopping_time_ge_zero[OF assms(1)] by auto
       then obtain r where "r \<in> D" "t\<^sub>0 \<le> r" "T \<omega> \<le> r" "r < min t (S \<omega>)" using semidense_D order_trans by blast
       hence "\<exists>s\<in>D \<inter> {t\<^sub>0..t}. T \<omega> \<le> s \<and> s < S \<omega>" by auto 
     }
     thus "(T \<omega> < S \<omega> \<and> T \<omega> \<le> t) = ?f \<omega>" if "\<omega> \<in> space (F t)" for \<omega> using that by force
     show "Measurable.pred (F t) ?f"
       using assms asm D
       by (intro pred_intros_logic measurable_If measurable_pred_countable countable_Collect
                 stopping_time_measurable_le predE stopping_time_measurable_eq) auto
   qed
 qed (intro assms)
 
 end  
 
 lemma (in enat_filtered_measure) stopping_time_SUP_enat:
   fixes T :: "nat \<Rightarrow> ('a \<Rightarrow> enat)"
   shows "(\<And>i. stopping_time (T i)) \<Longrightarrow> stopping_time (SUP i. T i)"
   unfolding stopping_time_def SUP_apply SUP_le_iff by (auto intro!: pred_intros_countable)
 
 lemma (in enat_filtered_measure) stopping_time_Inf_enat:
   assumes "\<And>i. Measurable.pred (F i) (P i)"
   shows "stopping_time (\<lambda>\<omega>. Inf {i. P i \<omega>})"
 proof -
   {
     fix t :: enat assume asm: "t \<noteq> \<infinity>"
     moreover
     { 
       fix i \<omega> assume "Inf {i. P i \<omega>} \<le> t"
       moreover have "a < eSuc b \<longleftrightarrow> (a \<le> b \<and> a \<noteq> \<infinity>)" for a b by (cases a) auto
       ultimately have "(\<exists>i\<le>t. P i \<omega>)" using asm unfolding Inf_le_iff by (cases t) (auto elim!: allE[of _ "eSuc t"])
     }
     ultimately have *: "\<And>\<omega>. Inf {i. P i \<omega>} \<le> t \<longleftrightarrow> (\<exists>i\<in>{..t}. P i \<omega>)" by (auto intro!: Inf_lower2)
     have "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)" unfolding * using sets_F_mono assms by (intro pred_intros_countable_bounded) (auto simp: pred_def)
   }
   moreover have "Measurable.pred (F t) (\<lambda>\<omega>. Inf {i. P i \<omega>} \<le> t)" if "t = \<infinity>" for t using that by simp
   ultimately show ?thesis by (blast intro: stopping_timeI[OF i0_lb])
 qed
 
 lemma (in nat_filtered_measure) stopping_time_Inf_nat:
   assumes "\<And>i. Measurable.pred (F i) (P i)" 
           "\<And>i \<omega>. \<omega> \<in> space M \<Longrightarrow> \<exists>n. P n \<omega>"
   shows "stopping_time (\<lambda>\<omega>. Inf {i. P i \<omega>})"
 proof (rule stopping_time_cong[THEN iffD2])
   show "stopping_time (\<lambda>x. LEAST n. P n x)"
   proof
     fix t
     have "((LEAST n. P n \<omega>) \<le> t) = (\<exists>i\<le>t. P i \<omega>)" if "\<omega> \<in> space M" for \<omega> by (rule LeastI2_wellorder_ex[OF assms(2)[OF that]]) auto
     moreover have "Measurable.pred (F t) (\<lambda>w. \<exists>i\<in>{..t}. P i w)" using sets_F_mono[of _ t] assms by (intro pred_intros_countable_bounded) (auto simp: pred_def)
     ultimately show "Measurable.pred (F t) (\<lambda>\<omega>. (LEAST n. P n \<omega>) \<le> t)" by (subst measurable_cong[of "F t"]) auto
   qed (simp)
 qed (simp add: Inf_nat_def)
 
 definition stopped_value :: "('b \<Rightarrow> 'a \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'c)" where
   "stopped_value X \<tau> \<omega> = X (\<tau> \<omega>) \<omega>"
 
 subsection \<open>Hitting Time\<close>
 
 text \<open>Given a stochastic process \<open>X\<close> and a borel set \<open>A\<close>, \<open>hitting_time X A s t\<close> is the first time \<open>X\<close> is in \<open>A\<close> after time \<open>s\<close> and before time \<open>t\<close>.
       If \<open>X\<close> does not hit \<open>A\<close> after time \<open>s\<close> and before \<open>t\<close> then the hitting time is simply \<open>t\<close>. The definition presented here coincides with the definition of hitting times in mathlib \<^cite>\<open>"ying2022formalization"\<close>.\<close>
 
 context linearly_filtered_measure
 begin
 
 definition hitting_time :: "('b \<Rightarrow> 'a \<Rightarrow> 'c) \<Rightarrow> 'c set \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" where
   "hitting_time X A s t = (\<lambda>\<omega>. if \<exists>i\<in>{s..t} \<inter> {t\<^sub>0..}. X i \<omega> \<in> A then Inf ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A}) else max t\<^sub>0 t)"
 
 lemma hitting_time_def':
   "hitting_time X A s t = (\<lambda>\<omega>. Inf (insert (max t\<^sub>0 t) ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A})))"
 proof cases
   assume asm: "t\<^sub>0 \<le> s \<and> s \<le> t"
   hence "{s..t} \<inter> {t\<^sub>0..} = {s..t}" by simp
   {
     fix \<omega>
     assume *: "{s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A} \<noteq> {}"
     then obtain i where "i \<in> {s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A}" by blast
     hence "Inf ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A}) \<le> t" by (intro cInf_lower[of i, THEN order_trans]) auto
     hence "Inf (insert (max t\<^sub>0 t) ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A})) = Inf ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A})" using asm * inf_absorb2 by (subst cInf_insert_If) force+ 
     also have "... = hitting_time X A s t \<omega>" using * unfolding hitting_time_def by auto
     finally have "hitting_time X A s t \<omega> = Inf (insert (max t\<^sub>0 t) ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A}))" by argo
   }
   moreover
   {
     fix \<omega>
     assume "{s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A} = {}"
     hence "hitting_time X A s t \<omega> = Inf (insert (max t\<^sub>0 t) ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A}))" unfolding hitting_time_def by auto
   }
   ultimately show ?thesis by fast
 next
   assume "\<not> (t\<^sub>0 \<le> s \<and> s \<le> t)"
   moreover
   {
     assume asm: "s < t\<^sub>0" "t \<ge> t\<^sub>0"
     hence "{s..t} \<inter> {t\<^sub>0..} = {t\<^sub>0..t}" by simp
     {
       fix \<omega>
       assume *: "{s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A} \<noteq> {}"
       then obtain i where "i \<in> {s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A}" by blast
       hence "Inf ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A}) \<le> t" by (intro cInf_lower[of i, THEN order_trans]) auto
       hence "Inf (insert (max t\<^sub>0 t) ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A})) = Inf ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A})" using asm * inf_absorb2 by (subst cInf_insert_If) force+ 
       also have "... = hitting_time X A s t \<omega>" using * unfolding hitting_time_def by auto
       finally have "hitting_time X A s t \<omega> = Inf (insert (max t\<^sub>0 t) ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A}))" by argo
     }
     moreover
     {
       fix \<omega>
       assume "{s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A} = {}"
       hence "hitting_time X A s t \<omega> = Inf (insert (max t\<^sub>0 t) ({s..t} \<inter> {t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A}))" unfolding hitting_time_def by auto
     }
     ultimately have ?thesis by fast  
   }
   moreover have ?thesis if "s < t\<^sub>0" "t < t\<^sub>0" using that unfolding hitting_time_def by auto
   moreover have ?thesis if "s > t" using that unfolding hitting_time_def by auto
   ultimately show ?thesis by fastforce
 qed
 
 \<comment> \<open>The following lemma provides a sufficient condition for an injective function to preserve a hitting time.\<close>
 
 lemma hitting_time_inj_on:
   assumes "inj_on f S" "\<And>\<omega> t. t \<ge> t\<^sub>0 \<Longrightarrow> X t \<omega> \<in> S" "A \<subseteq> S"
   shows "hitting_time X A = hitting_time (\<lambda>t \<omega>. f (X t \<omega>)) (f ` A)"
 proof -
   have "X t \<omega> \<in> A \<longleftrightarrow> f (X t \<omega>) \<in> f ` A" if "t \<ge> t\<^sub>0" for t \<omega> using assms that inj_on_image_mem_iff by meson
   hence "{t\<^sub>0..} \<inter> {i. X i \<omega> \<in> A} = {t\<^sub>0..} \<inter> {i. f (X i \<omega>) \<in> f ` A}" for \<omega> by blast
   thus ?thesis unfolding hitting_time_def' Int_assoc by presburger
 qed
 
 lemma hitting_time_translate: 
   fixes c :: "_ :: ab_group_add"
   shows "hitting_time X A = hitting_time (\<lambda>n \<omega>. X n \<omega> + c) (((+) c) ` A)"
   by (subst hitting_time_inj_on[OF inj_on_add, of _ UNIV]) (simp add: add.commute)+
 
 lemma hitting_time_le: 
   assumes "t \<ge> t\<^sub>0"
   shows "hitting_time X A s t \<omega> \<le> t"
   unfolding hitting_time_def' using assms 
   by (intro cInf_lower[of "max t\<^sub>0 t", THEN order_trans]) auto
 
 lemma hitting_time_ge: 
   assumes "t \<ge> t\<^sub>0" "s \<le> t"
   shows "s \<le> hitting_time X A s t \<omega>"
   unfolding hitting_time_def' using assms 
   by (intro le_cInf_iff[THEN iffD2]) auto
 
 lemma hitting_time_mono:
   assumes "t \<ge> t\<^sub>0" "s \<le> s'" "t \<le> t'"
   shows "hitting_time X A s t \<omega> \<le> hitting_time X A s' t' \<omega>"
   unfolding hitting_time_def' using assms by (fastforce intro!: cInf_mono)
   
 end
 
 context nat_filtered_measure
 begin               
 
 \<comment> \<open>Hitting times are stopping times for adapted processes.\<close>
 
 lemma stopping_time_hitting_time:
   assumes "adapted_process M F 0 X" "A \<in> borel"
   shows "stopping_time (hitting_time X A s t)"
 proof -
   interpret adapted_process M F 0 X by (rule assms)
   have "insert t ({s..t} \<inter> {i. X i \<omega> \<in> A}) = {i. i = t \<or> i \<in> ({s..t} \<inter> {i. X i \<omega> \<in> A})}" for \<omega> by blast
   hence "hitting_time X A s t = (\<lambda>\<omega>. Inf {i. i = t \<or> i \<in> ({s..t} \<inter> {i. X i \<omega> \<in> A})})" unfolding hitting_time_def' by simp
   thus ?thesis using assms by (auto intro: stopping_time_Inf_nat)
 qed
 
 lemma stopping_time_hitting_time':
   assumes "adapted_process M F 0 X" "A \<in> borel" "stopping_time s" "\<And>\<omega>. s \<omega> \<le> t"
   shows "stopping_time (\<lambda>\<omega>. hitting_time X A (s \<omega>) t \<omega>)"
 proof -
   interpret adapted_process M F 0 X by (rule assms)
   {
     fix n
     have "s \<omega> \<le> hitting_time X A (s \<omega>) t \<omega>" if "s \<omega> > n" for \<omega> using hitting_time_ge[OF _ assms(4)] by simp
     hence "(\<Union>i\<in>{n<..}. {\<omega>. s \<omega> = i} \<inter> {\<omega>. hitting_time X A i t \<omega> \<le> n}) = {}" by fastforce
     hence *: "(\<lambda>\<omega>. hitting_time X A (s \<omega>) t \<omega> \<le> n) = (\<lambda>\<omega>. \<exists>i\<le>n. s \<omega> = i \<and> hitting_time X A i t \<omega> \<le> n)" by force
     
     have "Measurable.pred (F n) (\<lambda>\<omega>. s \<omega> = i \<and> hitting_time X A i t \<omega> \<le> n)" if "i \<le> n" for i
     proof -
       have "Measurable.pred (F i) (\<lambda>\<omega>. s \<omega> = i)" using stopping_time_measurable_eq assms by blast
       hence "Measurable.pred (F n) (\<lambda>\<omega>. s \<omega> = i)" by (meson less_eq_nat.simps measurable_from_subalg subalgebra_F that)
       moreover have "Measurable.pred (F n) (\<lambda>\<omega>. hitting_time X A i t \<omega> \<le> n)" using stopping_timeD[OF stopping_time_hitting_time, OF assms(1,2)] by blast
       ultimately show ?thesis by auto
     qed
     hence "Measurable.pred (F n) (\<lambda>\<omega>. \<exists>i\<le>n. s \<omega> = i \<and> hitting_time X A i t \<omega> \<le> n)" by (intro pred_intros_countable) auto
     hence "Measurable.pred (F n) (\<lambda>\<omega>. hitting_time X A (s \<omega>) t \<omega> \<le> n)" using * by argo
   }
   thus ?thesis by (intro stopping_timeI) auto
 qed
 
 \<comment> \<open>If \<^term>\<open>X\<close> hits \<^term>\<open>A\<close> at time \<^term>\<open>j \<in> {s..t}\<close>, then the stopped value of \<^term>\<open>X\<close> at the hitting time of \<^term>\<open>A\<close> in the interval \<^term>\<open>{s..t}\<close> is an element of \<^term>\<open>A\<close>.\<close>
 
 lemma stopped_value_hitting_time_mem:
   assumes "j \<in> {s..t}" "X j \<omega> \<in> A"
   shows "stopped_value X (hitting_time X A s t) \<omega> \<in> A"
 proof -
   have "\<exists>i\<in>{s..t} \<inter> {0..}. X i \<omega> \<in> A" using assms by blast
   moreover have "Inf ({s..t} \<inter> {i. X i \<omega> \<in> A}) \<in> {s..t} \<inter> {i. X i \<omega> \<in> A}" using assms by (blast intro!: Inf_nat_def1)
   ultimately show ?thesis unfolding hitting_time_def stopped_value_def by simp
 qed
 
 lemma hitting_time_le_iff:
   assumes "i < t"
   shows "hitting_time X A s t \<omega> \<le> i \<longleftrightarrow> (\<exists>j \<in> {s..i}. X j \<omega> \<in> A)" (is "?lhs = ?rhs")
 proof 
   assume ?lhs
   moreover have "hitting_time X A s t \<omega> \<in> insert t ({s..t} \<inter> {i. X i \<omega> \<in> A})" by (metis hitting_time_def' Int_atLeastAtMostR2 inf_sup_aci(1) insertI1 max_0L wellorder_InfI)
   ultimately have "hitting_time X A s t \<omega> \<in> {s..i} \<inter> {i. X i \<omega> \<in> A}" using assms by force
   thus ?rhs by blast
 next
   assume ?rhs
   then obtain j where j: "j \<in> {s..i}" "X j \<omega> \<in> A" by blast
   hence "hitting_time X A s t \<omega> \<le> j" unfolding hitting_time_def' using assms by (auto intro: cInf_lower)
   thus ?lhs using j by simp
 qed
 
 lemma hitting_time_less_iff:
   assumes "i \<le> t"
   shows "hitting_time X A s t \<omega> < i \<longleftrightarrow> (\<exists>j \<in> {s..<i}. X j \<omega> \<in> A)" (is "?lhs = ?rhs")
 proof 
   assume ?lhs
   moreover have "hitting_time X A s t \<omega> \<in> insert t ({s..t} \<inter> {i. X i \<omega> \<in> A})" by (metis hitting_time_def' Int_atLeastAtMostR2 inf_sup_aci(1) insertI1 max_0L wellorder_InfI)
   ultimately have "hitting_time X A s t \<omega> \<in> {s..<i} \<inter> {i. X i \<omega> \<in> A}" using assms by force
   thus ?rhs by blast
 next
   assume ?rhs
   then obtain j where j: "j \<in> {s..<i}" "X j \<omega> \<in> A" by blast
   hence "hitting_time X A s t \<omega> \<le> j" unfolding hitting_time_def' using assms by (auto intro: cInf_lower)
   thus ?lhs using j by simp
 qed
 
 \<comment> \<open>If \<^term>\<open>X\<close> already hits \<^term>\<open>A\<close> in the interval \<^term>\<open>{s..t}\<close>, then \<^term>\<open>hitting_time X A s t = hitting_time X A s t'\<close> for \<^term>\<open>t' \<ge> t\<close>.\<close>
 
 lemma hitting_time_eq_hitting_time:
   assumes "t \<le> t'" "j \<in> {s..t}" "X j \<omega> \<in> A"
   shows "hitting_time X A s t \<omega> = hitting_time X A s t' \<omega>" (is "?lhs = ?rhs")
 proof -
   have "hitting_time X A s t \<omega> \<in> {s..t'}" using hitting_time_le[THEN order_trans, of t t' X A s] hitting_time_ge[of t s X A] assms by auto
   moreover have "stopped_value X (hitting_time X A s t) \<omega> \<in> A" by (blast intro: stopped_value_hitting_time_mem assms)
   ultimately have "hitting_time X A s t' \<omega> \<le> hitting_time X A s t \<omega>" by (fastforce simp add: hitting_time_def'[where t=t'] stopped_value_def intro!: cInf_lower)
   thus ?thesis by (blast intro: le_antisym hitting_time_mono[OF _ order_refl assms(1)])
 qed
 
 end
 
 end
\ No newline at end of file
diff --git a/thys/Doob_Convergence/Upcrossing.thy b/thys/Doob_Convergence/Upcrossing.thy
--- a/thys/Doob_Convergence/Upcrossing.thy
+++ b/thys/Doob_Convergence/Upcrossing.thy
@@ -1,639 +1,639 @@
 (*  Author:     Ata Keskin, TU München 
 *)
 
 section \<open>Doob's Upcrossing Inequality and Martingale Convergence Theorems\<close>
 
 text \<open>In this section we formalize upcrossings and downcrossings. Following this, we prove Doob's upcrossing inequality and first martingale convergence theorem.\<close>
 
 theory Upcrossing
-  imports Stopping_Time
+  imports Martingales.Martingale Stopping_Time
 begin
 
 (* TODO: This can be added to the library under HOL-Analysis.Borel_Space *)
 lemma real_embedding_borel_measurable: "real \<in> borel_measurable borel" by (auto intro: borel_measurable_continuous_onI)
 
 (* TODO: Add this to the library under HOL-Analysis.Extended_Real_Limits *)
 lemma limsup_lower_bound:
   fixes u:: "nat \<Rightarrow> ereal"
   assumes "limsup u > l"
   shows "\<exists>N>k. u N > l"
 proof -
   have "limsup u = - liminf (\<lambda>n. - u n)" using liminf_ereal_cminus[of 0 u] by simp
   hence "liminf (\<lambda>n. - u n) < - l" using assms ereal_less_uminus_reorder by presburger
   hence "\<exists>N>k. - u N < - l" using liminf_upper_bound by blast
   thus ?thesis using ereal_less_uminus_reorder by simp
 qed
 
 lemma ereal_abs_max_min: "\<bar>c\<bar> = max 0 c - min 0 c" for c :: ereal 
   by (cases "c \<ge> 0") auto
 
 subsection \<open>Upcrossings and Downcrossings\<close>
 
 text \<open>Given a stochastic process \<^term>\<open>X\<close>, real values \<^term>\<open>a\<close> and \<^term>\<open>b\<close>, and some point in time \<^term>\<open>N\<close>, we would like to define a notion of "upcrossings" of \<^term>\<open>X\<close> across the band \<^term>\<open>{a..b}\<close> which counts the 
     number of times any realization of \<^term>\<open>X\<close> crosses from below \<^term>\<open>a\<close> to above \<^term>\<open>b\<close> before time \<^term>\<open>N\<close>. To make this heuristic rigorous, we inductively define the following hitting times.\<close>
 
 context nat_filtered_measure
 begin
 
 context
   fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> real"
     and a b :: real
     and N :: nat
 begin
 
 primrec upcrossing :: "nat \<Rightarrow> 'a \<Rightarrow> nat" where
   "upcrossing 0 = (\<lambda>\<omega>. 0)" |
   "upcrossing (Suc n) = (\<lambda>\<omega>. hitting_time X {b..} (hitting_time X {..a} (upcrossing n \<omega>) N \<omega>) N \<omega>)"
 
 definition downcrossing :: "nat \<Rightarrow> 'a \<Rightarrow> nat" where
   "downcrossing n = (\<lambda>\<omega>. hitting_time X {..a} (upcrossing n \<omega>) N \<omega>)"
 
 lemma upcrossing_simps:
   "upcrossing 0 = (\<lambda>\<omega>. 0)"
   "upcrossing (Suc n) = (\<lambda>\<omega>. hitting_time X {b..} (downcrossing n \<omega>) N \<omega>)"
   by (auto simp add: downcrossing_def)
 
 lemma downcrossing_simps:
   "downcrossing 0 = hitting_time X {..a} 0 N"
   "downcrossing n = (\<lambda>\<omega>. hitting_time X {..a} (upcrossing n \<omega>) N \<omega>)"
   by (auto simp add: downcrossing_def)
 
 declare upcrossing.simps[simp del]
 
 lemma upcrossing_le: "upcrossing n \<omega> \<le> N"
   by (cases n) (auto simp add: upcrossing_simps hitting_time_le)
 
 lemma downcrossing_le: "downcrossing n \<omega> \<le> N"
   by (cases n) (auto simp add: downcrossing_simps hitting_time_le)
 
 lemma upcrossing_le_downcrossing: "upcrossing n \<omega> \<le> downcrossing n \<omega>"
   unfolding downcrossing_simps by (auto intro: hitting_time_ge upcrossing_le)
 
 lemma downcrossing_le_upcrossing_Suc: "downcrossing n \<omega> \<le> upcrossing (Suc n) \<omega>"
   unfolding upcrossing_simps by (auto intro: hitting_time_ge downcrossing_le)
 
 lemma upcrossing_mono:
   assumes "n \<le> m"
   shows "upcrossing n \<omega> \<le> upcrossing m \<omega>"
   using order_trans[OF upcrossing_le_downcrossing downcrossing_le_upcrossing_Suc] assms
   by (rule lift_Suc_mono_le)
 
 lemma downcrossing_mono:
   assumes "n \<le> m"
   shows "downcrossing n \<omega> \<le> downcrossing m \<omega>"
   using order_trans[OF downcrossing_le_upcrossing_Suc upcrossing_le_downcrossing] assms
   by (rule lift_Suc_mono_le)
 
 \<comment> \<open>The following lemmas help us make statements about when an upcrossing (resp. downcrossing) occurs, and the value that the process takes at that instant.\<close>
 
 lemma stopped_value_upcrossing:
   assumes "upcrossing (Suc n) \<omega> \<noteq> N"
   shows "stopped_value X (upcrossing (Suc n)) \<omega> \<ge> b"
 proof -
   have *: "upcrossing (Suc n) \<omega> < N" using le_neq_implies_less upcrossing_le assms by presburger
   have "\<exists>j \<in> {downcrossing n \<omega>..upcrossing (Suc n) \<omega>}. X j \<omega> \<in> {b..}"
     using hitting_time_le_iff[THEN iffD1, OF *] upcrossing_simps by fastforce
   then obtain j where j: "j \<in> {downcrossing n \<omega>..N}" "X j \<omega> \<in> {b..}" using * by (meson atLeastatMost_subset_iff le_refl subsetD upcrossing_le)
   thus ?thesis using stopped_value_hitting_time_mem[of j _ _ X] unfolding upcrossing_simps stopped_value_def by blast
 qed
 
 lemma stopped_value_downcrossing:
   assumes "downcrossing n \<omega> \<noteq> N"
   shows "stopped_value X (downcrossing n) \<omega> \<le> a"
 proof -
   have *: "downcrossing n \<omega> < N" using le_neq_implies_less downcrossing_le assms by presburger
   have "\<exists>j \<in> {upcrossing n \<omega>..downcrossing n \<omega>}. X j \<omega> \<in> {..a}"
     using hitting_time_le_iff[THEN iffD1, OF *] downcrossing_simps by fastforce
   then obtain j where j: "j \<in> {upcrossing n \<omega>..N}" "X j \<omega> \<in> {..a}" using * by (meson atLeastatMost_subset_iff le_refl subsetD downcrossing_le)
   thus ?thesis using stopped_value_hitting_time_mem[of j _ _ X] unfolding downcrossing_simps stopped_value_def by blast
 qed
 
 lemma upcrossing_less_downcrossing:
   assumes "a < b" "downcrossing (Suc n) \<omega> \<noteq> N"
   shows "upcrossing (Suc n) \<omega> < downcrossing (Suc n) \<omega>"
 proof -
   have "upcrossing (Suc n) \<omega> \<noteq> N" using assms by (metis le_antisym downcrossing_le upcrossing_le_downcrossing)
   hence "stopped_value X (downcrossing (Suc n)) \<omega> < stopped_value X (upcrossing (Suc n)) \<omega>"
     using assms stopped_value_downcrossing stopped_value_upcrossing by force
   hence "downcrossing (Suc n) \<omega> \<noteq> upcrossing (Suc n) \<omega>" unfolding stopped_value_def by force
   thus ?thesis using upcrossing_le_downcrossing by (simp add: le_neq_implies_less)
 qed
 
 lemma downcrossing_less_upcrossing:
   assumes "a < b" "upcrossing (Suc n) \<omega> \<noteq> N"
   shows "downcrossing n \<omega> < upcrossing (Suc n) \<omega>"
 proof -
   have "downcrossing n \<omega> \<noteq> N" using assms by (metis le_antisym upcrossing_le downcrossing_le_upcrossing_Suc)
   hence "stopped_value X (downcrossing n) \<omega> < stopped_value X (upcrossing (Suc n)) \<omega>"
     using assms stopped_value_downcrossing stopped_value_upcrossing by force
   hence "downcrossing n \<omega> \<noteq> upcrossing (Suc n) \<omega>" unfolding stopped_value_def by force
   thus ?thesis using downcrossing_le_upcrossing_Suc by (simp add: le_neq_implies_less)
 qed
 
 lemma upcrossing_less_Suc:
   assumes "a < b" "upcrossing n \<omega> \<noteq> N"
   shows "upcrossing n \<omega> < upcrossing (Suc n) \<omega>"
   by (metis assms upcrossing_le_downcrossing downcrossing_less_upcrossing order_le_less_trans le_neq_implies_less upcrossing_le)
 
 (* The following lemma is a more elegant version of the same lemma on mathlib. *)
 
 lemma upcrossing_eq_bound:
   assumes "a < b" "n \<ge> N"
   shows "upcrossing n \<omega> = N"
 proof -
   have *: "upcrossing N \<omega> = N"
   proof -
     {
       assume *: "upcrossing N \<omega> \<noteq> N"
       hence asm: "upcrossing n \<omega> < N" if "n \<le> N" for n using upcrossing_mono upcrossing_le that by (metis le_antisym le_neq_implies_less)
       {
         fix i j
         assume "i \<le> N" "i < j"
         hence "upcrossing i \<omega> \<noteq> upcrossing j \<omega>" by (metis Suc_leI asm assms(1) leD upcrossing_less_Suc upcrossing_mono)
       }
       moreover
       {
         fix j
         assume "j \<le> N"
         hence "upcrossing j \<omega> \<le> upcrossing N \<omega>" using upcrossing_mono by blast
         hence "upcrossing (Suc N) \<omega> \<noteq> upcrossing j \<omega>" using upcrossing_less_Suc[OF assms(1) *] by simp
       }
       ultimately have "inj_on (\<lambda>n. upcrossing n \<omega>) {..Suc N}" unfolding inj_on_def by (metis atMost_iff le_SucE linorder_less_linear)
       hence "card ((\<lambda>n. upcrossing n \<omega>) ` {..Suc N}) = Suc (Suc N)" by (simp add: inj_on_iff_eq_card[THEN iffD1])
       moreover have "(\<lambda>n. upcrossing n \<omega>) ` {..Suc N} \<subseteq> {..N}" using upcrossing_le by blast
       moreover have "card ((\<lambda>n. upcrossing n \<omega>) ` {..Suc N}) \<le> Suc N" using card_mono[OF _ calculation(2)] by simp
       ultimately have False by linarith
     }
     thus ?thesis by blast
   qed
   thus ?thesis using upcrossing_mono[OF assms(2), of \<omega>] upcrossing_le[of n \<omega>] by simp
 qed
 
 lemma downcrossing_eq_bound:
   assumes "a < b" "n \<ge> N"
   shows "downcrossing n \<omega> = N"
   using upcrossing_le_downcrossing[of n \<omega>] downcrossing_le[of n \<omega>] upcrossing_eq_bound[OF assms] by simp
 
 lemma stopping_time_crossings: 
   assumes "adapted_process M F 0 X"
   shows "stopping_time (upcrossing n)" "stopping_time (downcrossing n)"
 proof -
   have "stopping_time (upcrossing n) \<and> stopping_time (downcrossing n)"
   proof (induction n)
     case 0
     then show ?case unfolding upcrossing_simps downcrossing_simps
       using stopping_time_const stopping_time_hitting_time[OF assms] by simp
   next
     case (Suc n)
     have "stopping_time (upcrossing (Suc n))" unfolding upcrossing_simps
       using assms Suc downcrossing_le by (intro stopping_time_hitting_time') auto
     moreover have "stopping_time (downcrossing (Suc n))" unfolding downcrossing_simps
       using assms calculation upcrossing_le by (intro stopping_time_hitting_time') auto
     ultimately show ?case by blast
   qed
   thus "stopping_time (upcrossing n)" "stopping_time (downcrossing n)" by blast+
 qed
 
 lemmas stopping_time_upcrossing = stopping_time_crossings(1)
 lemmas stopping_time_downcrossing = stopping_time_crossings(2)
 
 \<comment> \<open>We define \<open>upcrossings_before\<close> as the number of upcrossings which take place strictly before time \<^term>\<open>N\<close>.\<close>
 
 definition upcrossings_before :: "'a \<Rightarrow> nat" where
   "upcrossings_before = (\<lambda>\<omega>. Sup {n. upcrossing n \<omega> < N})"
 
 lemma upcrossings_before_bdd_above: 
   assumes "a < b"
   shows "bdd_above {n. upcrossing n \<omega> < N}"
 proof -
   have "{n. upcrossing n \<omega> < N} \<subseteq> {..<N}" unfolding lessThan_def Collect_mono_iff
     using upcrossing_eq_bound[OF assms] linorder_not_less order_less_irrefl by metis
   thus ?thesis by (meson bdd_above_Iio bdd_above_mono)
 qed
 
 lemma upcrossings_before_less:
   assumes "a < b" "0 < N"
   shows "upcrossings_before \<omega> < N"
 proof -
   have *: "{n. upcrossing n \<omega> < N} \<subseteq> {..<N}" unfolding lessThan_def Collect_mono_iff
     using upcrossing_eq_bound[OF assms(1)] linorder_not_less order_less_irrefl by metis
   have "upcrossing 0 \<omega> < N" unfolding upcrossing_simps by (rule assms)
   moreover have "Sup {..<N} < N" unfolding Sup_nat_def using assms by simp
   ultimately show ?thesis unfolding upcrossings_before_def using cSup_subset_mono[OF _ _ *] by force
 qed
 
 lemma upcrossings_before_less_implies_crossing_eq_bound:
   assumes "a < b" "upcrossings_before \<omega> < n"
   shows "upcrossing n \<omega> = N"
         "downcrossing n \<omega> = N"
 proof -
   have "\<not> upcrossing n \<omega> < N" using assms upcrossings_before_bdd_above[of \<omega>] upcrossings_before_def bdd_above_nat finite_Sup_less_iff by fastforce
   thus "upcrossing n \<omega> = N" using upcrossing_le[of n \<omega>] by simp
   thus "downcrossing n \<omega> = N" using upcrossing_le_downcrossing[of n \<omega>] downcrossing_le[of n \<omega>] by simp
 qed
 
 lemma upcrossings_before_le:
   assumes "a < b"
   shows "upcrossings_before \<omega> \<le> N"
   using upcrossings_before_less assms less_le_not_le upcrossings_before_def
   by (cases N) auto
 
 lemma upcrossings_before_mem:
   assumes "a < b" "0 < N"
   shows "upcrossings_before \<omega> \<in> {n. upcrossing n \<omega> < N} \<inter> {..<N}"
 proof -
   have "upcrossing 0 \<omega> < N" using assms unfolding upcrossing_simps by simp
   hence "{n. upcrossing n \<omega> < N} \<noteq> {}" by blast
   moreover have "finite {n. upcrossing n \<omega> < N}" using upcrossings_before_bdd_above[OF assms(1)] by (simp add: bdd_above_nat)
   ultimately show ?thesis using Max_in upcrossings_before_less[OF assms(1,2)] Sup_nat_def upcrossings_before_def by auto
 qed
 
 lemma upcrossing_less_of_le_upcrossings_before:
   assumes "a < b" "0 < N" "n \<le> upcrossings_before \<omega>" 
   shows "upcrossing n \<omega> < N"
   using upcrossings_before_mem[OF assms(1,2), of \<omega>] upcrossing_mono[OF assms(3), of \<omega>] by simp
 
 lemma upcrossings_before_sum_def:
   assumes "a < b"
   shows "upcrossings_before \<omega> = (\<Sum>k\<in>{1..N}. indicator {n. upcrossing n \<omega> < N} k)"
 proof (cases N)
   case 0
   then show ?thesis unfolding upcrossings_before_def by simp
 next
   case (Suc N')
   have "upcrossing 0 \<omega> < N" using assms Suc unfolding upcrossing_simps by simp
   hence "{n. upcrossing n \<omega> < N} \<noteq> {}" by blast
   hence *: "\<not> upcrossing n \<omega> < N" if "n \<in> {upcrossings_before \<omega> <..N}" for n
     using finite_Sup_less_iff[THEN iffD1, OF bdd_above_nat[THEN iffD1, OF upcrossings_before_bdd_above], of \<omega> n]
     by (metis that assms greaterThanAtMost_iff less_not_refl mem_Collect_eq upcrossings_before_def)
   have **: "upcrossing n \<omega> < N" if "n \<in> {1..upcrossings_before \<omega>}" for n
     using assms that Suc by (intro upcrossing_less_of_le_upcrossings_before) auto
   have "upcrossings_before \<omega> < N" using upcrossings_before_less Suc assms by simp
   hence "{1..N} - {1..upcrossings_before \<omega>} = {upcrossings_before \<omega><..N}"
         "{1..N} \<inter> {1..upcrossings_before \<omega>} = {1..upcrossings_before \<omega>}" by force+
   hence "(\<Sum>k\<in>{1..N}. indicator {n. upcrossing n \<omega> < N} k) = 
         (\<Sum>k\<in>{1..upcrossings_before \<omega>}. indicator {n. upcrossing n \<omega> < N} k) + (\<Sum>k\<in>{upcrossings_before \<omega> <..N}. indicator {n. upcrossing n \<omega> < N} k)"
     using sum.Int_Diff[OF finite_atLeastAtMost, of _ 1 N "{1..upcrossings_before \<omega>}"] by metis
   also have "... = upcrossings_before \<omega>" using * ** by simp
   finally show ?thesis by argo
 qed
 
 lemma upcrossings_before_measurable:
   assumes "adapted_process M F 0 X" "a < b"
   shows "upcrossings_before \<in> borel_measurable M"
   unfolding upcrossings_before_sum_def[OF assms(2)]
   using stopping_time_measurable[OF stopping_time_crossings(1), OF assms(1)] by simp
 
 lemma upcrossings_before_measurable':
   assumes "adapted_process M F 0 X" "a < b"
   shows "(\<lambda>\<omega>. real (upcrossings_before \<omega>)) \<in> borel_measurable M"
   using real_embedding_borel_measurable upcrossings_before_measurable[OF assms] by simp 
 
 end
 
 lemma crossing_eq_crossing:
   assumes "N \<le> N'"
       and "downcrossing X a b N n \<omega> < N"
     shows "upcrossing X a b N n \<omega> = upcrossing X a b N' n \<omega>"
           "downcrossing X a b N n \<omega> = downcrossing X a b N' n \<omega>"
 proof -
   have "upcrossing X a b N n \<omega> = upcrossing X a b N' n \<omega> \<and> downcrossing X a b N n \<omega> = downcrossing X a b N' n \<omega>" using assms(2)
   proof (induction n)
     case 0
     show ?case by (metis (no_types, lifting) upcrossing_simps(1) assms atLeast_0 bot_nat_0.extremum hitting_time_def hitting_time_eq_hitting_time inf_top.right_neutral leD downcrossing_mono downcrossing_simps(1) max_nat.left_neutral)
   next
     case (Suc n)
     hence upper_less: "upcrossing X a b N (Suc n) \<omega> < N" using upcrossing_le_downcrossing Suc order.strict_trans1 by blast
     hence lower_less: "downcrossing X a b N n \<omega> < N" using downcrossing_le_upcrossing_Suc order.strict_trans1 by blast
 
     obtain j where "j \<in> {downcrossing X a b N n \<omega>..<N}" "X j \<omega> \<in> {b..}"
       using hitting_time_less_iff[THEN iffD1, OF order_refl] upper_less by (force simp add: upcrossing_simps)
     hence upper_eq: "upcrossing X a b N (Suc n) \<omega> = upcrossing X a b N' (Suc n) \<omega>"
       using Suc(1)[OF lower_less] assms(1) 
       by (auto simp add: upcrossing_simps intro!: hitting_time_eq_hitting_time)
     obtain j where j: "j \<in> {upcrossing X a b N (Suc n) \<omega>..<N}" "X j \<omega> \<in> {..a}" using Suc(2) hitting_time_less_iff[THEN iffD1, OF order_refl] by (force simp add: downcrossing_simps)
     thus ?case unfolding downcrossing_simps upper_eq by (force intro: hitting_time_eq_hitting_time assms)
   qed
   thus "upcrossing X a b N n \<omega> = upcrossing X a b N' n \<omega>" "downcrossing X a b N n \<omega> = downcrossing X a b N' n \<omega>" by auto
 qed
 
 lemma crossing_eq_crossing':
   assumes "N \<le> N'"
       and "upcrossing X a b N (Suc n) \<omega> < N"
     shows "upcrossing X a b N (Suc n) \<omega> = upcrossing X a b N' (Suc n) \<omega>"
           "downcrossing X a b N n \<omega> = downcrossing X a b N' n \<omega>"
 proof -
   show lower_eq: "downcrossing X a b N n \<omega> = downcrossing X a b N' n \<omega>"
     using downcrossing_le_upcrossing_Suc[THEN order.strict_trans1] crossing_eq_crossing assms by fast
   have "\<exists>j\<in>{downcrossing X a b N n \<omega>..<N}. X j \<omega> \<in> {b..}" using assms(2) by (intro hitting_time_less_iff[OF order_refl, THEN iffD1]) (simp add: upcrossing_simps lower_eq)
   then obtain j where "j\<in>{downcrossing X a b N n \<omega>..N}" "X j \<omega> \<in> {b..}" by fastforce
   thus "upcrossing X a b N (Suc n) \<omega> = upcrossing X a b N' (Suc n) \<omega>"
     unfolding upcrossing_simps stopped_value_def using hitting_time_eq_hitting_time[OF assms(1)] lower_eq by metis
 qed
 
 lemma upcrossing_eq_upcrossing:
   assumes "N \<le> N'"
       and "upcrossing X a b N n \<omega> < N"
     shows "upcrossing X a b N n \<omega> = upcrossing X a b N' n \<omega>"
   using crossing_eq_crossing'[OF assms(1)] assms(2) upcrossing_simps
   by (cases n) (presburger, fast)
 
 lemma upcrossings_before_zero: "upcrossings_before X a b 0 \<omega> = 0" 
   unfolding upcrossings_before_def by simp
 
 lemma upcrossings_before_less_exists_upcrossing:
   assumes "a < b"
       and upcrossing: "N \<le> L" "X L \<omega> < a" "L \<le> U" "b < X U \<omega>"
     shows "upcrossings_before X a b N \<omega> < upcrossings_before X a b (Suc U) \<omega>"
 proof -
   have "upcrossing X a b (Suc U) (upcrossings_before X a b N \<omega>) \<omega> \<le> L"
     using assms upcrossing_le[THEN order_trans, OF upcrossing(1)]
     by (cases "0 < N", subst upcrossing_eq_upcrossing[of N "Suc U", symmetric, OF _ upcrossing_less_of_le_upcrossings_before])
        (auto simp add: upcrossings_before_zero upcrossing_simps) 
   hence "downcrossing X a b (Suc U) (upcrossings_before X a b N \<omega>) \<omega> \<le> U" 
     unfolding downcrossing_simps using upcrossing by (force intro: hitting_time_le_iff[THEN iffD2])
   hence "upcrossing X a b (Suc U) (Suc (upcrossings_before X a b N \<omega>)) \<omega> < Suc U" 
     unfolding upcrossing_simps using upcrossing by (force intro: hitting_time_less_iff[THEN iffD2])
   thus ?thesis using cSup_upper[OF _ upcrossings_before_bdd_above[OF assms(1)]] upcrossings_before_def by fastforce
 qed
 
 lemma crossings_translate:
   "upcrossing X a b N = upcrossing (\<lambda>n \<omega>. (X n \<omega> + c)) (a + c) (b + c) N"
   "downcrossing X a b N = downcrossing (\<lambda>n \<omega>. (X n \<omega> + c)) (a + c) (b + c) N"
 proof -
   have upper: "upcrossing X a b N n = upcrossing (\<lambda>n \<omega>. (X n \<omega> + c)) (a + c) (b + c) N n" for n
   proof (induction n)
     case 0
     then show ?case by (simp only: upcrossing.simps)
   next
     case (Suc n)
     have "((+) c ` {..a}) = {..a + c}" by simp
     moreover have "((+) c ` {b..}) = {b + c..}" by simp
     ultimately show ?case unfolding upcrossing.simps using hitting_time_translate[of X "{b..}" c] hitting_time_translate[of X "{..a}" c] Suc by presburger 
   qed
   thus "upcrossing X a b N = upcrossing (\<lambda>n \<omega>. (X n \<omega> + c)) (a + c) (b + c) N" by blast
   have "((+) c ` {..a}) = {..a + c}" by simp
   thus "downcrossing X a b N = downcrossing (\<lambda>n \<omega>. (X n \<omega> + c)) (a + c) (b + c) N" using upper downcrossing_simps hitting_time_translate[of X "{..a}" c] by presburger
 qed
 
 lemma upcrossings_before_translate: 
   "upcrossings_before X a b N = upcrossings_before (\<lambda>n \<omega>. (X n \<omega> + c)) (a + c) (b + c) N"
   using upcrossings_before_def crossings_translate by simp
 
 lemma crossings_pos_eq:
   assumes "a < b"
   shows "upcrossing X a b N = upcrossing (\<lambda>n \<omega>. max 0 (X n \<omega> - a)) 0 (b - a) N"
         "downcrossing X a b N = downcrossing (\<lambda>n \<omega>. max 0 (X n \<omega> - a)) 0 (b - a) N"
 proof -
   have *: "max 0 (x - a) \<in> {..0} \<longleftrightarrow> x - a \<in> {..0}" "max 0 (x - a) \<in> {b - a..} \<longleftrightarrow> x - a \<in> {b - a..}" for x using assms by auto
   have "upcrossing X a b N = upcrossing (\<lambda>n \<omega>. X n \<omega> - a) 0 (b - a) N" using crossings_translate[of X a b N "- a"] by simp
   thus upper: "upcrossing X a b N = upcrossing (\<lambda>n \<omega>. max 0 (X n \<omega> - a)) 0 (b - a) N" unfolding upcrossing_def hitting_time_def' using * by presburger
 
   thus "downcrossing X a b N = downcrossing (\<lambda>n \<omega>. max 0 (X n \<omega> - a)) 0 (b - a) N" 
     unfolding downcrossing_simps hitting_time_def' using upper * by simp
 qed
 
 lemma upcrossings_before_mono:
   assumes "a < b" "N \<le> N'"
   shows "upcrossings_before X a b N \<omega> \<le> upcrossings_before X a b N' \<omega>"
 proof (cases N)
   case 0
   then show ?thesis unfolding upcrossings_before_def by simp
 next
   case (Suc N')
   hence "upcrossing X a b N 0 \<omega> < N" unfolding upcrossing_simps by simp
   thus ?thesis unfolding upcrossings_before_def using upcrossings_before_bdd_above upcrossing_eq_upcrossing assms by (intro cSup_subset_mono) auto
 qed
 
 lemma upcrossings_before_pos_eq:
   assumes "a < b"
   shows "upcrossings_before X a b N = upcrossings_before (\<lambda>n \<omega>. max 0 (X n \<omega> - a)) 0 (b - a) N"
   using upcrossings_before_def crossings_pos_eq[OF assms] by simp
 
 \<comment> \<open>We define \<open>upcrossings\<close> to be the total number of upcrossings a stochastic process completes as \<open>N \<longlonglongrightarrow> \<infinity>\<close>.\<close>
 
 definition upcrossings :: "(nat \<Rightarrow> 'a \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> real \<Rightarrow> 'a \<Rightarrow> ennreal" where
   "upcrossings X a b = (\<lambda>\<omega>. (SUP N. ennreal (upcrossings_before X a b N \<omega>)))"
 
 lemma upcrossings_measurable: 
   assumes "adapted_process M F 0 X" "a < b"
   shows "upcrossings X a b \<in> borel_measurable M"
   unfolding upcrossings_def
   using upcrossings_before_measurable'[OF assms] by (auto intro!: borel_measurable_SUP)
 
 end
 
 lemma (in nat_finite_filtered_measure) integrable_upcrossings_before:
   assumes "adapted_process M F 0 X" "a < b"
   shows "integrable M (\<lambda>\<omega>. real (upcrossings_before X a b N \<omega>))"
 proof -
   have "(\<integral>\<^sup>+ x. ennreal (norm (real (upcrossings_before X a b N x))) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal N \<partial>M)" using upcrossings_before_le[OF assms(2)] by (intro nn_integral_mono) simp
   also have "... = ennreal N * emeasure M (space M)" by simp
   also have "... < \<infinity>" by (metis emeasure_real ennreal_less_top ennreal_mult_less_top infinity_ennreal_def)
   finally show ?thesis by (intro integrableI_bounded upcrossings_before_measurable' assms)
 qed
 
 subsection \<open>Doob's Upcrossing Inequality\<close>
 
 text \<open>Doob's upcrossing inequality provides a bound on the expected number of upcrossings a submartingale completes before some point in time. 
    The proof follows the proof presented in the paper \<open>A Formalization of Doob's Martingale Convergence Theorems in mathlib\<close> \<^cite>\<open>ying2022formalization\<close> \<^cite>\<open>Degenne_Ying_2022\<close>.\<close>
 
 context nat_finite_filtered_measure
 begin
 
 theorem upcrossing_inequality:
   fixes a b :: real and N :: nat
   assumes "submartingale M F 0 X"
   shows "(b - a) * (\<integral>\<omega>. real (upcrossings_before X a b N \<omega>) \<partial>M) \<le> (\<integral>\<omega>. max 0 (X N \<omega> - a) \<partial>M)"
 proof -
   interpret submartingale_linorder M F 0 X unfolding submartingale_linorder_def by (intro assms)
   show ?thesis 
   proof (cases "a < b")
     case True
     \<comment> \<open>We show the statement first for \<^term>\<open>X 0\<close> non-negative and \<^term>\<open>X N\<close> greater than or equal to \<^term>\<open>a\<close>.\<close>
     have *: "(b - a) * (\<integral>\<omega>. real (upcrossings_before X a b N \<omega>) \<partial>M) \<le> (\<integral>\<omega>. X N \<omega> \<partial>M)"
       if asm: "submartingale M F 0 X" "a < b" "\<And>\<omega>. X 0 \<omega> \<ge> 0" "\<And>\<omega>. X N \<omega> \<ge> a"
       for a b X
     proof -
       interpret subm: submartingale M F 0 X by (intro asm)      
       define C :: "nat \<Rightarrow> 'a \<Rightarrow> real" where "C = (\<lambda>n \<omega>. \<Sum>k < N. indicator {downcrossing X a b N k \<omega>..<upcrossing X a b N (Suc k) \<omega>} n)"
       have C_values: "C n \<omega> \<in> {0, 1}" for n \<omega>
       proof (cases "\<exists>j < N. n \<in> {downcrossing X a b N j \<omega>..<upcrossing X a b N (Suc j) \<omega>}")
         case True
         then obtain j where j: "j \<in> {..<N}" "n \<in> {downcrossing X a b N j \<omega>..<upcrossing X a b N (Suc j) \<omega>}" by blast
         {
           fix k l :: nat assume k_less_l: "k < l"
           hence Suc_k_le_l: "Suc k \<le> l" by simp
           have "{downcrossing X a b N k \<omega>..<upcrossing X a b N (Suc k) \<omega>} \<inter> {downcrossing X a b N l \<omega>..<upcrossing X a b N (Suc l) \<omega>} = 
                 {downcrossing X a b N l \<omega>..<upcrossing X a b N (Suc k) \<omega>}" 
             using k_less_l upcrossing_mono downcrossing_mono by simp
           moreover have "upcrossing X a b N (Suc k) \<omega> \<le> downcrossing X a b N l \<omega>"
             using upcrossing_le_downcrossing downcrossing_mono[OF Suc_k_le_l] order_trans by blast
           ultimately have "{downcrossing X a b N k \<omega>..<upcrossing X a b N (Suc k) \<omega>} \<inter> {downcrossing X a b N l \<omega>..<upcrossing X a b N (Suc l) \<omega>} = {}" by simp
         }
         hence "disjoint_family_on (\<lambda>k. {downcrossing X a b N k \<omega>..<upcrossing X a b N (Suc k) \<omega>}) {..<N}" 
           unfolding disjoint_family_on_def
           by (metis Int_commute linorder_less_linear)
         hence "C n \<omega> = 1" unfolding C_def using sum_indicator_disjoint_family[where ?f="\<lambda>_. 1"] j by fastforce
         thus ?thesis by blast
       next
         case False
         hence "C n \<omega> = 0" unfolding C_def by simp
         thus ?thesis by simp
       qed
       hence C_interval: "C n \<omega> \<in> {0..1}" for n \<omega> by (metis atLeastAtMost_iff empty_iff insert_iff order.refl zero_less_one_class.zero_le_one)
 
       \<comment> \<open>We consider the discrete stochastic integral of \<^term>\<open>C\<close> and \<^term>\<open>\<lambda>n \<omega>. 1 - C n \<omega>\<close>.\<close>
       define C' where "C' = (\<lambda>n \<omega>. \<Sum>k < n. C k \<omega> *\<^sub>R (X (Suc k) \<omega> - X k \<omega>))"
       define one_minus_C' where "one_minus_C' = (\<lambda>n \<omega>. \<Sum>k < n. (1 - C k \<omega>) *\<^sub>R (X (Suc k) \<omega> - X k \<omega>))"
 
       \<comment> \<open>We use the fact that the crossing times are stopping times to show that C is predictable.\<close>
       have adapted_C: "adapted_process M F 0 C"
       proof
         fix i
         have "(\<lambda>\<omega>. indicat_real {downcrossing X a b N k \<omega>..<upcrossing X a b N (Suc k) \<omega>} i) \<in> borel_measurable (F i)" for k
           unfolding indicator_def
           using stopping_time_upcrossing[OF subm.adapted_process_axioms, THEN stopping_time_measurable_gr]
                 stopping_time_downcrossing[OF subm.adapted_process_axioms, THEN stopping_time_measurable_le] 
           by force
         thus "C i \<in> borel_measurable (F i)" unfolding C_def by simp
       qed
       hence "adapted_process M F 0 (\<lambda>n \<omega>. 1 - C n \<omega>)" by (intro adapted_process.diff_adapted adapted_process_const)
       hence submartingale_one_minus_C': "submartingale M F 0 one_minus_C'" unfolding one_minus_C'_def using C_interval
         by (intro submartingale_partial_sum_scaleR[of _ _ 1] submartingale_linorder.intro asm) auto
 
       have "C n \<in> borel_measurable M" for n
         using adapted_C adapted_process.adapted measurable_from_subalg subalg by blast
 
       have integrable_C': "integrable M (C' n)" for n unfolding C'_def using C_interval
         by (intro submartingale_partial_sum_scaleR[THEN submartingale.integrable] submartingale_linorder.intro adapted_C asm) auto
 
       \<comment> \<open>We show the following inequality, by using the fact that \<^term>\<open>one_minus_C'\<close> is a submartingale.\<close>
       have "integral\<^sup>L M (C' n) \<le> integral\<^sup>L M (X n)" for n
       proof -                       
         interpret subm': submartingale_linorder M F 0 one_minus_C' unfolding submartingale_linorder_def by (rule submartingale_one_minus_C')
         have "0 \<le> integral\<^sup>L M (one_minus_C' n)"
           using subm'.set_integral_le[OF sets.top, where i=0 and j=n] space_F subm'.integrable by (fastforce simp add: set_integral_space one_minus_C'_def)
         moreover have "one_minus_C' n \<omega> = (\<Sum>k < n. X (Suc k) \<omega> - X k \<omega>) - C' n \<omega>" for \<omega>
           unfolding one_minus_C'_def C'_def by (simp only: scaleR_diff_left sum_subtractf scale_one)
         ultimately have "0 \<le> (LINT \<omega>|M. (\<Sum>k < n. X (Suc k) \<omega> - X k \<omega>)) - integral\<^sup>L M (C' n)"
           using subm.integrable integrable_C'
           by (subst Bochner_Integration.integral_diff[symmetric]) (auto simp add: one_minus_C'_def)
         moreover have "(LINT \<omega>|M. (\<Sum>k<n. X (Suc k) \<omega> - X k \<omega>)) \<le> (LINT \<omega>|M. X n \<omega>)" using asm sum_lessThan_telescope[of "\<lambda>i. X i _" n] subm.integrable
           by (intro integral_mono) auto
         ultimately show ?thesis by linarith
       qed
       moreover have "(b - a) * (\<integral>\<omega>. real (upcrossings_before X a b N \<omega>) \<partial>M) \<le> integral\<^sup>L M (C' N)"
       proof (cases N)
         case 0
         then show ?thesis using C'_def upcrossings_before_zero by simp
       next
         case (Suc N')
         {
           fix \<omega>
           have dc_not_N: "downcrossing X a b N k \<omega> \<noteq> N" if "k < upcrossings_before X a b N \<omega>" for k
             by (metis Suc Suc_leI asm(2) downcrossing_le_upcrossing_Suc leD that upcrossing_less_of_le_upcrossings_before zero_less_Suc)
           have uc_not_N:"upcrossing X a b N (Suc k) \<omega> \<noteq> N" if "k < upcrossings_before X a b N \<omega>" for k 
             by (metis Suc Suc_leI asm(2) order_less_irrefl that upcrossing_less_of_le_upcrossings_before zero_less_Suc)
 
           have subset_lessThan_N: "{downcrossing X a b N i \<omega>..<upcrossing X a b N (Suc i) \<omega>} \<subseteq> {..<N}" if "i < N" for i using that
             by (simp add: lessThan_atLeast0 upcrossing_le)
 
           \<comment> \<open>First we rewrite the sum as follows: \<close>
 
           have "C' N \<omega> = (\<Sum>k<N. \<Sum>i<N. indicator {downcrossing X a b N i \<omega>..<upcrossing X a b N (Suc i) \<omega>} k * (X (Suc k) \<omega> - X k \<omega>))"
             unfolding C'_def C_def by (simp add: sum_distrib_right)
           also have "... = (\<Sum>i<N. \<Sum>k<N. indicator {downcrossing X a b N i \<omega>..<upcrossing X a b N (Suc i) \<omega>} k * (X (Suc k) \<omega> - X k \<omega>))"
             using sum.swap by fast
           also have "... = (\<Sum>i<N. \<Sum>k\<in>{..<N} \<inter> {downcrossing X a b N i \<omega>..<upcrossing X a b N (Suc i) \<omega>}. X (Suc k) \<omega> - X k \<omega>)"
             by (subst Indicator_Function.sum_indicator_mult) simp+
           also have "... = (\<Sum>i<N. \<Sum>k\<in>{downcrossing X a b N i \<omega>..<upcrossing X a b N (Suc i) \<omega>}. X (Suc k) \<omega> - X k \<omega>)"
             using subset_lessThan_N[THEN Int_absorb1] by simp
           also have "... = (\<Sum>i<N. X (upcrossing X a b N (Suc i) \<omega>) \<omega> - X (downcrossing X a b N i \<omega>) \<omega>)" 
             by (subst sum_Suc_diff'[OF downcrossing_le_upcrossing_Suc]) blast
           finally have *: "C' N \<omega> = (\<Sum>i<N. X (upcrossing X a b N (Suc i) \<omega>) \<omega> - X (downcrossing X a b N i \<omega>) \<omega>)" .
 
           \<comment> \<open>For \<^term>\<open>k \<le> N\<close>, we consider three cases: \<close>
           \<comment> \<open>1. If \<^term>\<open>k < upcrossings_before X a b N \<omega>\<close>, then \<open>X (upcrossing X a b N (Suc k) \<omega>) \<omega> - X (downcrossing X a b N k \<omega>) \<omega> \<ge> b - a\<close>\<close>
           \<comment> \<open>2. If \<^term>\<open>k > upcrossings_before X a b N \<omega>\<close>, then \<open>X (upcrossing X a b N (Suc k) \<omega>) \<omega> = X (downcrossing X a b N k \<omega>) \<omega>\<close>\<close>
           \<comment> \<open>3. If \<^term>\<open>k = upcrossings_before X a b N \<omega>\<close>, then \<open>X (upcrossing X a b N (Suc k) \<omega>) \<omega> - X (downcrossing X a b N k \<omega>) \<omega> \<ge> 0\<close>\<close>
 
           have summand_zero_if: "X (upcrossing X a b N (Suc k) \<omega>) \<omega> - X (downcrossing X a b N k \<omega>) \<omega> = 0" if "k > upcrossings_before X a b N \<omega>" for k
             using that upcrossings_before_less_implies_crossing_eq_bound[OF asm(2)] by simp
 
           have summand_nonneg_if: "X (upcrossing X a b N (Suc (upcrossings_before X a b N \<omega>)) \<omega>) \<omega> - X (downcrossing X a b N (upcrossings_before X a b N \<omega>) \<omega>) \<omega> \<ge> 0"
             using upcrossings_before_less_implies_crossing_eq_bound(1)[OF asm(2) lessI]
                   stopped_value_downcrossing[of X a b N _ \<omega>, THEN order_trans, OF _ asm(4)[of \<omega>]]
             by (cases "downcrossing X a b N (upcrossings_before X a b N \<omega>) \<omega> \<noteq> N") (simp add: stopped_value_def)+
 
           have interval: "{upcrossings_before X a b N \<omega>..<N} - {upcrossings_before X a b N \<omega>} = {upcrossings_before X a b N \<omega><..<N}"
             using Diff_insert atLeastSucLessThan_greaterThanLessThan lessThan_Suc lessThan_minus_lessThan by metis
 
           have "(b - a) * real (upcrossings_before X a b N \<omega>) = (\<Sum>_<upcrossings_before X a b N \<omega>. b - a)" by simp
           also have "... \<le> (\<Sum>k<upcrossings_before X a b N \<omega>. stopped_value X (upcrossing X a b N (Suc k)) \<omega> - stopped_value X (downcrossing X a b N k) \<omega>)"
             using stopped_value_downcrossing[OF dc_not_N] stopped_value_upcrossing[OF uc_not_N] by (force intro!: sum_mono)
           also have "... = (\<Sum>k<upcrossings_before X a b N \<omega>. X (upcrossing X a b N (Suc k) \<omega>) \<omega> - X (downcrossing X a b N k \<omega>) \<omega>)" unfolding stopped_value_def by blast
           also have "... \<le> (\<Sum>k<upcrossings_before X a b N \<omega>. X (upcrossing X a b N (Suc k) \<omega>) \<omega> - X (downcrossing X a b N k \<omega>) \<omega>)
                           + (\<Sum>k\<in>{upcrossings_before X a b N \<omega>}. X (upcrossing X a b N (Suc k) \<omega>) \<omega> - X (downcrossing X a b N k \<omega>) \<omega>)
                           + (\<Sum>k\<in>{upcrossings_before X a b N \<omega><..<N}. X (upcrossing X a b N (Suc k) \<omega>) \<omega> - X (downcrossing X a b N k \<omega>) \<omega>)" 
             using summand_zero_if summand_nonneg_if by auto
           also have "... = (\<Sum>k<N. X (upcrossing X a b N (Suc k) \<omega>) \<omega> - X (downcrossing X a b N k \<omega>) \<omega>)"
             using upcrossings_before_le[OF asm(2)]
             by (subst sum.subset_diff[where A="{..<N}" and B="{..<upcrossings_before X a b N \<omega>}"], simp, simp,
                 subst sum.subset_diff[where A="{..<N} - {..<upcrossings_before X a b N \<omega>}" and B="{upcrossings_before X a b N \<omega>}"])
                (simp add: Suc asm(2) upcrossings_before_less, simp, simp add: interval)
           finally have "(b - a) * real (upcrossings_before X a b N \<omega>) \<le> C' N \<omega>" using * by presburger
         }
         thus ?thesis using integrable_upcrossings_before subm.adapted_process_axioms asm integrable_C'
           by (subst integral_mult_right_zero[symmetric], intro integral_mono) auto
       qed
       ultimately show ?thesis using order_trans by blast
     qed
 
     have "(b - a) * (\<integral>\<omega>. real (upcrossings_before X a b N \<omega>) \<partial>M) = (b - a) * (\<integral>\<omega>. real (upcrossings_before (\<lambda>n \<omega>. max 0 (X n \<omega> - a)) 0 (b - a) N \<omega>) \<partial>M)"
       using upcrossings_before_pos_eq[OF True] by simp                                                                             
     also have "... \<le> (\<integral>\<omega>. max 0 (X N \<omega> - a) \<partial>M)" 
       using *[OF submartingale_linorder.max_0[OF submartingale_linorder.intro, OF submartingale.diff, OF assms supermartingale_const], of 0 "b - a" a] True by simp
     finally show ?thesis .
   next
     case False
     have "0 \<le> (\<integral>\<omega>. max 0 (X N \<omega> - a) \<partial>M)" by simp
     moreover have "0 \<le> (\<integral>\<omega>. real (upcrossings_before X a b N \<omega>) \<partial>M)" by simp
     moreover have "b - a \<le> 0" using False by simp
     ultimately show ?thesis using mult_nonpos_nonneg order_trans by meson
   qed
 qed
 
 theorem upcrossing_inequality_Sup:
   fixes a b :: real
   assumes "submartingale M F 0 X"
   shows "(b - a) * (\<integral>\<^sup>+\<omega>. upcrossings X a b \<omega> \<partial>M) \<le> (SUP N. (\<integral>\<^sup>+\<omega>. max 0 (X N \<omega> - a) \<partial>M))"
 proof -
   interpret submartingale M F 0 X by (intro assms)
   show ?thesis
   proof (cases "a < b")
     case True
     have "(\<integral>\<^sup>+\<omega>. upcrossings X a b \<omega> \<partial>M) = (SUP N. (\<integral>\<^sup>+\<omega>. real (upcrossings_before X a b N \<omega>) \<partial>M))"
       unfolding upcrossings_def
       using upcrossings_before_mono True upcrossings_before_measurable'[OF adapted_process_axioms]
       by (auto intro: nn_integral_monotone_convergence_SUP simp add: mono_def le_funI)
     hence "(b - a) * (\<integral>\<^sup>+\<omega>. upcrossings X a b \<omega> \<partial>M) = (SUP N. (b - a) * (\<integral>\<^sup>+\<omega>. real (upcrossings_before X a b N \<omega>) \<partial>M))"
       by (simp add: SUP_mult_left_ennreal)
     moreover
     {
       fix N
       have "(\<integral>\<^sup>+\<omega>. real (upcrossings_before X a b N \<omega>) \<partial>M) = (\<integral>\<omega>. real (upcrossings_before X a b N \<omega>) \<partial>M)" 
         by (force intro!: nn_integral_eq_integral integrable_upcrossings_before True adapted_process_axioms)
       moreover have "(\<integral>\<^sup>+\<omega>. max 0 (X N \<omega> - a) \<partial>M) = (\<integral>\<omega>. max 0 (X N \<omega> - a) \<partial>M)"
         using Bochner_Integration.integrable_diff[OF integrable integrable_const]
         by (force intro!: nn_integral_eq_integral)
       ultimately have "(b - a) * (\<integral>\<^sup>+\<omega>. real (upcrossings_before X a b N \<omega>) \<partial>M) \<le> (\<integral>\<^sup>+\<omega>. max 0 (X N \<omega> - a) \<partial>M)"
         using upcrossing_inequality[OF assms, of b a N] True ennreal_mult'[symmetric] by simp
     }
     ultimately show ?thesis by (force intro!: Sup_mono)
   qed (simp add: ennreal_neg)
 qed
 
 end
 
 end
\ No newline at end of file