Theory Martingale

(*  Author:     Ata Keskin, TU München 
*)

theory Martingale
  imports Stochastic_Process Conditional_Expectation_Banach
begin                

section ‹Martingales›

text ‹The following locales are necessary for defining martingales.›

subsection ‹Martingale›

text ‹A martingale is an adapted process where the expected value of the next observation, given all past observations, is equal to the current value.›

locale martingale = sigma_finite_filtered_measure + adapted_process +
  assumes integrable: "⋀i. t⇩0 ≤ i ⟹ integrable M (X i)"
      and martingale_property: "⋀i j. t⇩0 ≤ i ⟹ i ≤ j ⟹ AE ξ in M. X i ξ = cond_exp M (F i) (X j) ξ"

locale martingale_order = martingale M F t⇩0 X for M F t⇩0 and X :: "_ ⇒ _ ⇒ _ :: {order_topology, ordered_real_vector}"
locale martingale_linorder = martingale M F t⇩0 X for M F t⇩0 and X :: "_ ⇒ _ ⇒ _ :: {linorder_topology, ordered_real_vector}"
sublocale martingale_linorder ⊆ martingale_order ..

lemma (in sigma_finite_filtered_measure) martingale_const_fun[intro]:  
  assumes "integrable M f" "f ∈ borel_measurable (F t⇩0)"
  shows "martingale M F t⇩0 (λ_. f)"
  using assms sigma_finite_subalgebra.cond_exp_F_meas[OF _ assms(1), THEN AE_symmetric] borel_measurable_mono
  by (unfold_locales) blast+

lemma (in sigma_finite_filtered_measure) martingale_cond_exp[intro]:  
  assumes "integrable M f"
  shows "martingale M F t⇩0 (λi. cond_exp M (F i) f)"
  using sigma_finite_subalgebra.borel_measurable_cond_exp' borel_measurable_cond_exp 
  by (unfold_locales) (auto intro: sigma_finite_subalgebra.cond_exp_nested_subalg[OF _ assms] simp add: subalgebra_F subalgebras)

corollary (in sigma_finite_filtered_measure) martingale_zero[intro]: "martingale M F t⇩0 (λ_ _. 0)" by fastforce

corollary (in finite_filtered_measure) martingale_const[intro]: "martingale M F t⇩0 (λ_ _. c)" by fastforce

subsection ‹Submartingale›

text ‹A submartingale is an adapted process where the expected value of the next observation, given all past observations, is greater than or equal to the current value.›

locale submartingale = sigma_finite_filtered_measure M F t⇩0 + adapted_process M F t⇩0 X for M F t⇩0 and X :: "_ ⇒ _ ⇒ _ :: {order_topology, ordered_real_vector}" +
  assumes integrable: "⋀i. t⇩0 ≤ i ⟹ integrable M (X i)"
      and submartingale_property: "⋀i j. t⇩0 ≤ i ⟹ i ≤ j ⟹ AE ξ in M. X i ξ ≤ cond_exp M (F i) (X j) ξ"

locale submartingale_linorder = submartingale M F t⇩0 X for M F t⇩0 and X :: "_ ⇒ _ ⇒ _ :: {linorder_topology}"

lemma (in sigma_finite_filtered_measure) submartingale_const_fun[intro]:  
  assumes "integrable M f" "f ∈ borel_measurable (F t⇩0)"
  shows "submartingale M F t⇩0 (λ_. f)"
proof -
  interpret martingale M F t⇩0 "λ_. f" using assms by (rule martingale_const_fun)
  show "submartingale M F t⇩0 (λ_. f)" using martingale_property by (unfold_locales) (force simp add: integrable)+
qed

lemma (in sigma_finite_filtered_measure) submartingale_cond_exp[intro]:  
  assumes "integrable M f"
  shows "submartingale M F t⇩0 (λi. cond_exp M (F i) f)"
proof -
  interpret martingale M F t⇩0 "λi. cond_exp M (F i) f" using assms by (rule martingale_cond_exp)
  show "submartingale M F t⇩0 (λi. cond_exp M (F i) f)" using martingale_property by (unfold_locales) (force simp add: integrable)+
qed

corollary (in finite_filtered_measure) submartingale_const[intro]: "submartingale M F t⇩0 (λ_ _. c)" by fastforce

sublocale martingale_order ⊆ submartingale using martingale_property by (unfold_locales) (force simp add: integrable)+
sublocale martingale_linorder ⊆ submartingale_linorder ..

subsection ‹Supermartingale›

text ‹A supermartingale is an adapted process where the expected value of the next observation, given all past observations, is less than or equal to the current value.›

locale supermartingale = sigma_finite_filtered_measure M F t⇩0 + adapted_process M F t⇩0 X for M F t⇩0 and X :: "_ ⇒ _ ⇒ _ :: {order_topology, ordered_real_vector}" +
  assumes integrable: "⋀i. t⇩0 ≤ i ⟹ integrable M (X i)"
      and supermartingale_property: "⋀i j. t⇩0 ≤ i ⟹ i ≤ j ⟹ AE ξ in M. X i ξ ≥ cond_exp M (F i) (X j) ξ"

locale supermartingale_linorder = supermartingale M F t⇩0 X for M F t⇩0 and X :: "_ ⇒ _ ⇒ _ :: {linorder_topology}"

lemma (in sigma_finite_filtered_measure) supermartingale_const_fun[intro]:  
  assumes "integrable M f" "f ∈ borel_measurable (F t⇩0)"
  shows "supermartingale M F t⇩0 (λ_. f)"
proof -
  interpret martingale M F t⇩0 "λ_. f" using assms by (rule martingale_const_fun)
  show "supermartingale M F t⇩0 (λ_. f)" using martingale_property by (unfold_locales) (force simp add: integrable)+
qed

lemma (in sigma_finite_filtered_measure) supermartingale_cond_exp[intro]:  
  assumes "integrable M f"
  shows "supermartingale M F t⇩0 (λi. cond_exp M (F i) f)"
proof -
  interpret martingale M F t⇩0 "λi. cond_exp M (F i) f" using assms by (rule martingale_cond_exp)
  show "supermartingale M F t⇩0 (λi. cond_exp M (F i) f)" using martingale_property by (unfold_locales) (force simp add: integrable)+
qed

corollary (in finite_filtered_measure) supermartingale_const[intro]: "supermartingale M F t⇩0 (λ_ _. c)" by fastforce

sublocale martingale_order ⊆ supermartingale using martingale_property by (unfold_locales) (force simp add: integrable)+
sublocale martingale_linorder ⊆ supermartingale_linorder ..

text ‹A stochastic process is a martingale, if and only if it is both a submartingale and a supermartingale.›

lemma martingale_iff: 
  shows "martingale M F t⇩0 X ⟷ submartingale M F t⇩0 X ∧ supermartingale M F t⇩0 X"
proof (rule iffI)
  assume asm: "martingale M F t⇩0 X"
  interpret martingale_order M F t⇩0 X by (intro martingale_order.intro asm)
  show "submartingale M F t⇩0 X ∧ supermartingale M F t⇩0 X" using submartingale_axioms supermartingale_axioms by blast
next
  assume asm: "submartingale M F t⇩0 X ∧ supermartingale M F t⇩0 X"
  interpret submartingale M F t⇩0 X by (simp add: asm)
  interpret supermartingale M F t⇩0 X by (simp add: asm)
  show "martingale M F t⇩0 X" using submartingale_property supermartingale_property by (unfold_locales) (intro integrable, blast, force)
qed

subsection ‹Martingale Lemmas›

text ‹In the following segment, we cover basic properties of martingales.›

context martingale
begin

lemma cond_exp_diff_eq_zero:
  assumes "t⇩0 ≤ i" "i ≤ j"
  shows "AE ξ in M. cond_exp M (F i) (λξ. X j ξ - X i ξ) ξ = 0"
  using martingale_property[OF assms] assms
        sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i]
        sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of "F i" j i] by fastforce

lemma set_integral_eq:
  assumes "A ∈ F i" "t⇩0 ≤ i" "i ≤ j"
  shows "set_lebesgue_integral M A (X i) = set_lebesgue_integral M A (X j)"
proof -
  interpret sigma_finite_subalgebra M "F i" using assms(2) by blast
  have "(∫x ∈ A. X i x ∂M) = (∫x ∈ A. cond_exp M (F i) (X j) x ∂M)" using martingale_property[OF assms(2,3)] borel_measurable_cond_exp' assms subalgebras subalgebra_def by (intro set_lebesgue_integral_cong_AE[OF _ random_variable]) fastforce+
  also have "... = (∫x ∈ A. X j x ∂M)" using assms by (auto simp: integrable intro: cond_exp_set_integral[symmetric])
  finally show ?thesis .
qed

lemma scaleR_const[intro]:
  shows "martingale M F t⇩0 (λi x. c *⇩R X i x)"
proof -
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    interpret sigma_finite_subalgebra M "F i" using asm by blast
    have "AE x in M. c *⇩R X i x = cond_exp M (F i) (λx. c *⇩R X j x) x" using asm cond_exp_scaleR_right[OF integrable, of j, THEN AE_symmetric] martingale_property[OF asm] by force
  }
  thus ?thesis by (unfold_locales) (auto simp add: integrable martingale.integrable)
qed

lemma uminus[intro]:
  shows "martingale M F t⇩0 (- X)" 
  using scaleR_const[of "-1"] by (force intro: back_subst[of "martingale M F t⇩0"])

lemma add[intro]:
  assumes "martingale M F t⇩0 Y"
  shows "martingale M F t⇩0 (λi ξ. X i ξ + Y i ξ)"
proof -
  interpret Y: martingale M F t⇩0 Y by (rule assms)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    hence "AE ξ in M. X i ξ + Y i ξ = cond_exp M (F i) (λx. X j x + Y j x) ξ" 
      using sigma_finite_subalgebra.cond_exp_add[OF _ integrable martingale.integrable[OF assms], of "F i" j j, THEN AE_symmetric]
            martingale_property[OF asm] martingale.martingale_property[OF assms asm] by force
  }
  thus ?thesis using assms
  by (unfold_locales) (auto simp add: integrable martingale.integrable)
qed

lemma diff[intro]:
  assumes "martingale M F t⇩0 Y"
  shows "martingale M F t⇩0 (λi x. X i x - Y i x)"
proof -
  interpret Y: martingale M F t⇩0 Y by (rule assms)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    hence "AE ξ in M. X i ξ - Y i ξ = cond_exp M (F i) (λx. X j x - Y j x) ξ" 
      using sigma_finite_subalgebra.cond_exp_diff[OF _ integrable martingale.integrable[OF assms], of "F i" j j, THEN AE_symmetric] 
            martingale_property[OF asm] martingale.martingale_property[OF assms asm] by fastforce
  }
  thus ?thesis using assms by (unfold_locales) (auto simp add: integrable martingale.integrable)  
qed

end

text ‹Using properties of the conditional expectation, we present the following alternative characterizations of martingales.›

lemma (in sigma_finite_filtered_measure) martingale_of_cond_exp_diff_eq_zero: 
  assumes adapted: "adapted_process M F t⇩0 X"
      and integrable: "⋀i. t⇩0 ≤ i ⟹ integrable M (X i)" 
      and diff_zero: "⋀i j. t⇩0 ≤ i ⟹ i ≤ j ⟹ AE x in M. cond_exp M (F i) (λξ. X j ξ - X i ξ) x = 0"
    shows "martingale M F t⇩0 X"
proof
  interpret adapted_process M F t⇩0 X by (rule adapted)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    thus "AE ξ in M. X i ξ = cond_exp M (F i) (X j) ξ" 
      using diff_zero[OF asm] sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of "F i" j i] 
            sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i] by fastforce
  }
qed (auto intro: integrable adapted[THEN adapted_process.adapted])

lemma (in sigma_finite_filtered_measure) martingale_of_set_integral_eq:
  assumes adapted: "adapted_process M F t⇩0 X"
      and integrable: "⋀i. t⇩0 ≤ i ⟹ integrable M (X i)"
      and "⋀A i j. t⇩0 ≤ i ⟹ i ≤ j ⟹ A ∈ F i ⟹ set_lebesgue_integral M A (X i) = set_lebesgue_integral M A (X j)" 
    shows "martingale M F t⇩0 X"
proof (unfold_locales)
  fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
  interpret adapted_process M F t⇩0 X by (rule adapted)
  interpret sigma_finite_subalgebra M "F i" using asm by blast
  interpret r: sigma_finite_measure "restr_to_subalg M (F i)" by (simp add: sigma_fin_subalg)
  {
    fix A assume "A ∈ restr_to_subalg M (F i)"
    hence *: "A ∈ F i" using sets_restr_to_subalg subalgebras asm by blast 
    have "set_lebesgue_integral (restr_to_subalg M (F i)) A (X i) = set_lebesgue_integral M A (X i)" using * subalg asm by (auto simp: set_lebesgue_integral_def intro: integral_subalgebra2 borel_measurable_scaleR adapted borel_measurable_indicator) 
    also have "... = set_lebesgue_integral M A (cond_exp M (F i) (X j))" using * assms(3)[OF asm] cond_exp_set_integral[OF integrable] asm by auto
    finally have "set_lebesgue_integral (restr_to_subalg M (F i)) A (X i) = set_lebesgue_integral (restr_to_subalg M (F i)) A (cond_exp M (F i) (X j))" using * subalg by (auto simp: set_lebesgue_integral_def intro!: integral_subalgebra2[symmetric] borel_measurable_scaleR borel_measurable_cond_exp borel_measurable_indicator)
  }
  hence "AE ξ in restr_to_subalg M (F i). X i ξ = cond_exp M (F i) (X j) ξ" using asm by (intro r.density_unique_banach, auto intro: integrable_in_subalg subalg borel_measurable_cond_exp integrable)
  thus "AE ξ in M. X i ξ = cond_exp M (F i) (X j) ξ" using AE_restr_to_subalg[OF subalg] by blast
qed (auto intro: integrable adapted[THEN adapted_process.adapted])

subsection ‹Submartingale Lemmas›

context submartingale
begin

lemma cond_exp_diff_nonneg:
  assumes "t⇩0 ≤ i" "i ≤ j"
  shows "AE x in M. cond_exp M (F i) (λξ. X j ξ - X i ξ) x ≥ 0"
  using submartingale_property[OF assms] assms sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of _ j i] sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i] by fastforce

lemma add[intro]:
  assumes "submartingale M F t⇩0 Y"
  shows "submartingale M F t⇩0 (λi ξ. X i ξ + Y i ξ)"
proof -
  interpret Y: submartingale M F t⇩0 Y by (rule assms)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    hence "AE ξ in M. X i ξ + Y i ξ ≤ cond_exp M (F i) (λx. X j x + Y j x) ξ" 
      using sigma_finite_subalgebra.cond_exp_add[OF _ integrable submartingale.integrable[OF assms], of "F i" j j] 
            submartingale_property[OF asm] submartingale.submartingale_property[OF assms asm] add_mono[of "X i _" _ "Y i _"] by force
  }
  thus ?thesis using assms by (unfold_locales) (auto simp add: borel_measurable_add random_variable adapted integrable Y.random_variable Y.adapted submartingale.integrable)  
qed

lemma diff[intro]:
  assumes "supermartingale M F t⇩0 Y"
  shows "submartingale M F t⇩0 (λi ξ. X i ξ - Y i ξ)"
proof -
  interpret Y: supermartingale M F t⇩0 Y by (rule assms)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    hence "AE ξ in M. X i ξ - Y i ξ ≤ cond_exp M (F i) (λx. X j x - Y j x) ξ" 
      using sigma_finite_subalgebra.cond_exp_diff[OF _ integrable supermartingale.integrable[OF assms], of "F i" j j] 
            submartingale_property[OF asm] supermartingale.supermartingale_property[OF assms asm] diff_mono[of "X i _" _ _ "Y i _"] by force
  }
  thus ?thesis using assms by (unfold_locales) (auto simp add: borel_measurable_diff random_variable adapted integrable Y.random_variable Y.adapted supermartingale.integrable)  
qed

lemma scaleR_nonneg: 
  assumes "c ≥ 0"
  shows "submartingale M F t⇩0 (λi ξ. c *⇩R X i ξ)"
proof
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    thus "AE ξ in M. c *⇩R X i ξ ≤ cond_exp M (F i) (λξ. c *⇩R X j ξ) ξ"  
      using sigma_finite_subalgebra.cond_exp_scaleR_right[OF _ integrable, of "F i" j c] submartingale_property[OF asm] by (fastforce intro!: scaleR_left_mono[OF _ assms])
  }
qed (auto simp add: borel_measurable_integrable borel_measurable_scaleR integrable random_variable adapted borel_measurable_const_scaleR)

lemma scaleR_le_zero: 
  assumes "c ≤ 0"
  shows "supermartingale M F t⇩0 (λi ξ. c *⇩R X i ξ)"
proof
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    thus "AE ξ in M. c *⇩R X i ξ ≥ cond_exp M (F i) (λξ. c *⇩R X j ξ) ξ" 
      using sigma_finite_subalgebra.cond_exp_scaleR_right[OF _ integrable, of "F i" j c] submartingale_property[OF asm] 
            by (fastforce intro!: scaleR_left_mono_neg[OF _ assms])
  }
qed (auto simp add: borel_measurable_integrable borel_measurable_scaleR integrable random_variable adapted borel_measurable_const_scaleR)

lemma uminus[intro]:
  shows "supermartingale M F t⇩0 (- X)"
  unfolding fun_Compl_def using scaleR_le_zero[of "-1"] by simp

end

context submartingale_linorder
begin

lemma set_integral_le:
  assumes "A ∈ F i" "t⇩0 ≤ i" "i ≤ j"
  shows "set_lebesgue_integral M A (X i) ≤ set_lebesgue_integral M A (X j)"  
  using submartingale_property[OF assms(2), of j] assms subsetD[OF sets_F_subset]
  by (subst sigma_finite_subalgebra.cond_exp_set_integral[OF _ integrable assms(1), of j])
     (auto intro!: scaleR_left_mono integral_mono_AE_banach integrable_mult_indicator integrable simp add: set_lebesgue_integral_def)

lemma max:
  assumes "submartingale M F t⇩0 Y"
  shows "submartingale M F t⇩0 (λi ξ. max (X i ξ) (Y i ξ))"
proof (unfold_locales)
  interpret Y: submartingale_linorder M F t⇩0 Y by (intro submartingale_linorder.intro assms)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    have "AE ξ in M. max (X i ξ) (Y i ξ) ≤ max (cond_exp M (F i) (X j) ξ) (cond_exp M (F i) (Y j) ξ)" using submartingale_property Y.submartingale_property asm unfolding max_def by fastforce
    thus "AE ξ in M. max (X i ξ) (Y i ξ) ≤ cond_exp M (F i) (λξ. max (X j ξ) (Y j ξ)) ξ" using sigma_finite_subalgebra.cond_exp_max[OF _ integrable Y.integrable, of "F i" j j] asm by (fast intro: order.trans)
  }
  show "⋀i. t⇩0 ≤ i ⟹ (λξ. max (X i ξ) (Y i ξ)) ∈ borel_measurable (F i)" "⋀i. t⇩0 ≤ i ⟹ integrable M (λξ. max (X i ξ) (Y i ξ))" by (force intro: Y.integrable integrable assms)+
qed

lemma max_0:
  shows "submartingale M F t⇩0 (λi ξ. max 0 (X i ξ))"
proof -
  interpret zero: martingale_linorder M F t⇩0 "λ_ _. 0" by (force intro: martingale_linorder.intro martingale_order.intro)
  show ?thesis by (intro zero.max submartingale_linorder.intro submartingale_axioms)
qed

end

lemma (in sigma_finite_filtered_measure) submartingale_of_cond_exp_diff_nonneg:
  assumes adapted: "adapted_process M F t⇩0 X"
      and integrable: "⋀i. t⇩0 ≤ i ⟹  integrable M (X i)" 
      and diff_nonneg: "⋀i j. t⇩0 ≤ i ⟹ i ≤ j ⟹ AE x in M. cond_exp M (F i) (λξ. X j ξ - X i ξ) x ≥ 0"
    shows "submartingale M F t⇩0 X"
proof (unfold_locales)
  interpret adapted_process M F t⇩0 X by (rule adapted)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    thus "AE ξ in M. X i ξ ≤ cond_exp M (F i) (X j) ξ" 
      using diff_nonneg[OF asm] sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of "F i" j i]
            sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i] by fastforce
  }
qed (auto intro: integrable adapted[THEN adapted_process.adapted])

lemma (in sigma_finite_filtered_measure) submartingale_of_set_integral_le:
  fixes X :: "_ ⇒ _ ⇒ _ :: {linorder_topology}"
  assumes adapted: "adapted_process M F t⇩0 X"
      and integrable: "⋀i. t⇩0 ≤ i ⟹ integrable M (X i)"
      and "⋀A i j. t⇩0 ≤ i ⟹ i ≤ j ⟹ A ∈ F i ⟹ set_lebesgue_integral M A (X i) ≤ set_lebesgue_integral M A (X j)"
    shows "submartingale M F t⇩0 X"
proof (unfold_locales)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    interpret adapted_process M F t⇩0 X by (rule adapted)
    interpret r: sigma_finite_measure "restr_to_subalg M (F i)" using asm sigma_finite_subalgebra.sigma_fin_subalg by blast
    {
      fix A assume "A ∈ restr_to_subalg M (F i)"
      hence *: "A ∈ F i" using asm sets_restr_to_subalg subalgebras by blast
      have "set_lebesgue_integral (restr_to_subalg M (F i)) A (X i) = set_lebesgue_integral M A (X i)" using * asm subalgebras by (auto simp: set_lebesgue_integral_def intro: integral_subalgebra2 borel_measurable_scaleR adapted borel_measurable_indicator) 
      also have "... ≤ set_lebesgue_integral M A (cond_exp M (F i) (X j))" using * assms(3)[OF asm] asm sigma_finite_subalgebra.cond_exp_set_integral[OF _ integrable] by fastforce
      also have "... = set_lebesgue_integral (restr_to_subalg M (F i)) A (cond_exp M (F i) (X j))" using * asm subalgebras by (auto simp: set_lebesgue_integral_def intro!: integral_subalgebra2[symmetric] borel_measurable_scaleR borel_measurable_cond_exp borel_measurable_indicator)
      finally have "0 ≤ set_lebesgue_integral (restr_to_subalg M (F i)) A (λξ. cond_exp M (F i) (X j) ξ - X i ξ)" using * asm subalgebras by (subst set_integral_diff, auto simp add: set_integrable_def sets_restr_to_subalg intro!: integrable adapted integrable_in_subalg borel_measurable_scaleR borel_measurable_indicator borel_measurable_cond_exp integrable_mult_indicator)
    }
    hence "AE ξ in restr_to_subalg M (F i). 0 ≤ cond_exp M (F i) (X j) ξ - X i ξ"
      by (intro r.density_nonneg integrable_in_subalg asm subalgebras borel_measurable_diff borel_measurable_cond_exp adapted Bochner_Integration.integrable_diff integrable_cond_exp integrable)  
    thus "AE ξ in M. X i ξ ≤ cond_exp M (F i) (X j) ξ" using AE_restr_to_subalg[OF subalgebras] asm by simp
  }
qed (auto intro: integrable adapted[THEN adapted_process.adapted])

subsection ‹Supermartingale Lemmas›

text ‹The following lemmas are exact duals of the ones for submartingales.›

context supermartingale
begin

lemma cond_exp_diff_nonneg:
  assumes "t⇩0 ≤ i" "i ≤ j"
  shows "AE x in M. cond_exp M (F i) (λξ. X i ξ - X j ξ) x ≥ 0"
  using assms supermartingale_property[OF assms] sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of "F i" i j] 
        sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i] by fastforce

lemma add[intro]:
  assumes "supermartingale M F t⇩0 Y"
  shows "supermartingale M F t⇩0 (λi ξ. X i ξ + Y i ξ)"
proof -
  interpret Y: supermartingale M F t⇩0 Y by (rule assms)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    hence "AE ξ in M. X i ξ + Y i ξ ≥ cond_exp M (F i) (λx. X j x + Y j x) ξ" 
      using sigma_finite_subalgebra.cond_exp_add[OF _ integrable supermartingale.integrable[OF assms], of "F i" j j] 
            supermartingale_property[OF asm] supermartingale.supermartingale_property[OF assms asm] add_mono[of _ "X i _" _ "Y i _"] by force
  }
  thus ?thesis using assms by (unfold_locales) (auto simp add: borel_measurable_add random_variable adapted integrable Y.random_variable Y.adapted supermartingale.integrable)  
qed

lemma diff[intro]:
  assumes "submartingale M F t⇩0 Y"
  shows "supermartingale M F t⇩0 (λi ξ. X i ξ - Y i ξ)"
proof -
  interpret Y: submartingale M F t⇩0 Y by (rule assms)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    hence "AE ξ in M. X i ξ - Y i ξ ≥ cond_exp M (F i) (λx. X j x - Y j x) ξ" 
      using sigma_finite_subalgebra.cond_exp_diff[OF _ integrable submartingale.integrable[OF assms], of "F i" j j, unfolded fun_diff_def] 
            supermartingale_property[OF asm] submartingale.submartingale_property[OF assms asm] diff_mono[of _ "X i _" "Y i _"] by force
  }
  thus ?thesis using assms by (unfold_locales) (auto simp add: borel_measurable_diff random_variable adapted integrable Y.random_variable Y.adapted submartingale.integrable)  
qed

lemma scaleR_nonneg: 
  assumes "c ≥ 0"
  shows "supermartingale M F t⇩0 (λi ξ. c *⇩R X i ξ)"
proof
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    thus "AE ξ in M. c *⇩R X i ξ ≥ cond_exp M (F i) (λξ. c *⇩R X j ξ) ξ"
      using sigma_finite_subalgebra.cond_exp_scaleR_right[OF _ integrable, of "F i" j c] supermartingale_property[OF asm] by (fastforce intro!: scaleR_left_mono[OF _ assms])
  }
qed (auto simp add: borel_measurable_integrable borel_measurable_scaleR integrable random_variable adapted borel_measurable_const_scaleR)

lemma scaleR_le_zero: 
  assumes "c ≤ 0"
  shows "submartingale M F t⇩0 (λi ξ. c *⇩R X i ξ)"
proof
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    thus "AE ξ in M. c *⇩R X i ξ ≤ cond_exp M (F i) (λξ. c *⇩R X j ξ) ξ" 
      using sigma_finite_subalgebra.cond_exp_scaleR_right[OF _ integrable, of "F i" j c] supermartingale_property[OF asm] by (fastforce intro!: scaleR_left_mono_neg[OF _ assms])
  }
qed (auto simp add: borel_measurable_integrable borel_measurable_scaleR integrable random_variable adapted borel_measurable_const_scaleR)

lemma uminus[intro]:
  shows "submartingale M F t⇩0 (- X)"
  unfolding fun_Compl_def using scaleR_le_zero[of "-1"] by simp

end

context supermartingale_linorder
begin

lemma set_integral_ge:
  assumes "A ∈ F i" "t⇩0 ≤ i" "i ≤ j"
  shows "set_lebesgue_integral M A (X i) ≥ set_lebesgue_integral M A (X j)"
  using supermartingale_property[OF assms(2), of j] assms subsetD[OF sets_F_subset]
  by (subst sigma_finite_subalgebra.cond_exp_set_integral[OF _ integrable assms(1), of j])
     (auto intro!: scaleR_left_mono integral_mono_AE_banach integrable_mult_indicator integrable simp add: set_lebesgue_integral_def)

lemma min:
  assumes "supermartingale M F t⇩0 Y"
  shows "supermartingale M F t⇩0 (λi ξ. min (X i ξ) (Y i ξ))"
proof (unfold_locales)
  interpret Y: supermartingale_linorder M F t⇩0 Y by (intro supermartingale_linorder.intro assms)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    have "AE ξ in M. min (X i ξ) (Y i ξ) ≥ min (cond_exp M (F i) (X j) ξ) (cond_exp M (F i) (Y j) ξ)" using supermartingale_property Y.supermartingale_property asm unfolding min_def by fastforce
    thus "AE ξ in M. min (X i ξ) (Y i ξ) ≥ cond_exp M (F i) (λξ. min (X j ξ) (Y j ξ)) ξ" using sigma_finite_subalgebra.cond_exp_min[OF _ integrable Y.integrable, of "F i" j j] asm by (fast intro: order.trans)
  }
  show "⋀i. t⇩0 ≤ i ⟹ (λξ. min (X i ξ) (Y i ξ)) ∈ borel_measurable (F i)" "⋀i. t⇩0 ≤ i ⟹ integrable M (λξ. min (X i ξ) (Y i ξ))" by (force intro: Y.integrable integrable assms)+
qed

lemma min_0:
  shows "supermartingale M F t⇩0 (λi ξ. min 0 (X i ξ))"
proof -
  interpret zero: martingale_linorder M F t⇩0 "λ_ _. 0" by (force intro: martingale_linorder.intro)
  show ?thesis by (intro zero.min supermartingale_linorder.intro supermartingale_axioms)
qed

end

lemma (in sigma_finite_filtered_measure) supermartingale_of_cond_exp_diff_le_zero:
  assumes adapted: "adapted_process M F t⇩0 X"
      and integrable: "⋀i. t⇩0 ≤ i ⟹ integrable M (X i)" 
      and diff_le_zero: "⋀i j. t⇩0 ≤ i ⟹ i ≤ j ⟹ AE x in M. cond_exp M (F i) (λξ. X j ξ - X i ξ) x ≤ 0"
    shows "supermartingale M F t⇩0 X"
proof 
  interpret adapted_process M F t⇩0 X by (rule adapted)
  {
    fix i j :: 'b assume asm: "t⇩0 ≤ i" "i ≤ j"
    thus "AE ξ in M. X i ξ ≥ cond_exp M (F i) (X j) ξ" 
      using diff_le_zero[OF asm] sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of "F i" j i] 
            sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i] by fastforce
  }
qed (auto intro: integrable adapted[THEN adapted_process.adapted])

lemma (in sigma_finite_filtered_measure) supermartingale_of_set_integral_ge:
  fixes X :: "_ ⇒ _ ⇒ _ :: {linorder_topology}"
  assumes adapted: "adapted_process M F t⇩0 X"
      and integrable: "⋀i. t⇩0 ≤ i ⟹ integrable M (X i)" 
      and "⋀A i j. t⇩0 ≤ i ⟹ i ≤ j ⟹ A ∈ F i ⟹ set_lebesgue_integral M A (X j) ≤ set_lebesgue_integral M A (X i)" 
    shows "supermartingale M F t⇩0 X"
proof -
  interpret adapted_process M F t⇩0 X by (rule adapted)
  note * = set_integral_uminus[unfolded set_integrable_def, OF integrable_mult_indicator[OF _ integrable]]
  have "supermartingale M F t⇩0 (-(- X))"
    using ord_eq_le_trans[OF * ord_le_eq_trans[OF le_imp_neg_le[OF assms(3)] *[symmetric]]] sets_F_subset[THEN subsetD]
    by (intro submartingale.uminus submartingale_of_set_integral_le[OF uminus_adapted]) 
       (clarsimp simp add: fun_Compl_def integrable | fastforce)+
  thus ?thesis unfolding fun_Compl_def by simp
qed

text ‹Many of the statements we have made concerning martingales can be simplified when the indexing set is the natural numbers. 
      Given a point in time \<^term>‹i ∈ ℕ›, it suffices to consider the successor \<^term>‹i + 1›, instead of all future times \<^term>‹j ≥ i›.›

subsection ‹Discrete Time Martingales›

context nat_sigma_finite_filtered_measure
begin

text ‹A predictable martingale is necessarily constant.›
lemma predictable_const:
  assumes "martingale M F 0 X" 
    and "predictable_process M F 0 X"
  shows "AE ξ in M. X i ξ = X j ξ"
proof -
  interpret martingale M F 0 X by (rule assms)
  have *: "AE ξ in M. X i ξ = X 0 ξ" for i
  proof (induction i)
    case 0
    then show ?case by (simp add: bot_nat_def)
  next
    case (Suc i)
    interpret S: adapted_process M F 0 "λi. X (Suc i)" by (intro predictable_implies_adapted_Suc assms)
    show ?case using Suc S.adapted[of i] martingale_property[OF _ le_SucI, of i] sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable, of "F i" "Suc i"] by fastforce
  qed
  show ?thesis using *[of i] *[of j] by force
qed

lemma martingale_of_set_integral_eq_Suc:
  assumes adapted: "adapted_process M F 0 X"
      and integrable: "⋀i. integrable M (X i)"
      and "⋀A i. A ∈ F i ⟹ set_lebesgue_integral M A (X i) = set_lebesgue_integral M A (X (Suc i))" 
    shows "martingale M F 0 X"
proof (intro martingale_of_set_integral_eq adapted integrable)
  fix i j A assume asm: "i ≤ j" "A ∈ sets (F i)"
  show "set_lebesgue_integral M A (X i) = set_lebesgue_integral M A (X j)" using asm
  proof (induction "j - i" arbitrary: i j)
    case 0
    then show ?case using asm by simp
  next
    case (Suc n)
    hence *: "n = j - Suc i" by linarith
    have "Suc i ≤ j" using Suc(2,3) by linarith
    thus ?case using sets_F_mono[OF _ le_SucI] Suc(4) Suc(1)[OF *] by (auto intro: assms(3)[THEN trans])
  qed
qed

lemma martingale_nat:
  assumes adapted: "adapted_process M F 0 X"
      and integrable: "⋀i. integrable M (X i)" 
      and "⋀i. AE ξ in M. X i ξ = cond_exp M (F i) (X (Suc i)) ξ" 
    shows "martingale M F 0 X"
proof (unfold_locales)
  interpret adapted_process M F 0 X by (rule adapted)
  fix i j :: nat assume asm: "i ≤ j"
  show "AE ξ in M. X i ξ = cond_exp M (F i) (X j) ξ" using asm
  proof (induction "j - i" arbitrary: i j)
    case 0
    hence "j = i" by simp
    thus ?case using sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, THEN AE_symmetric] by blast
  next
    case (Suc n)
    have j: "j = Suc (n + i)" using Suc by linarith
    have n: "n = n + i - i" using Suc by linarith
    have *: "AE ξ in M. cond_exp M (F (n + i)) (X j) ξ = X (n + i) ξ" unfolding j using assms(3)[THEN AE_symmetric] by blast
    have "AE ξ in M. cond_exp M (F i) (X j) ξ = cond_exp M (F i) (cond_exp M (F (n + i)) (X j)) ξ" by (intro cond_exp_nested_subalg integrable subalg, simp add: subalgebra_def sets_F_mono)
    hence "AE ξ in M. cond_exp M (F i) (X j) ξ = cond_exp M (F i) (X (n + i)) ξ" using cond_exp_cong_AE[OF integrable_cond_exp integrable *] by force
    thus ?case using Suc(1)[OF n] by fastforce
  qed
qed (auto simp add: integrable adapted[THEN adapted_process.adapted])

lemma martingale_of_cond_exp_diff_Suc_eq_zero:
  assumes adapted: "adapted_process M F 0 X"
      and integrable: "⋀i. integrable M (X i)" 
      and "⋀i. AE ξ in M. cond_exp M (F i) (λξ. X (Suc i) ξ - X i ξ) ξ = 0" 
    shows "martingale M F 0 X"
proof (intro martingale_nat integrable adapted)
  interpret adapted_process M F 0 X by (rule adapted)
  fix i 
  show "AE ξ in M. X i ξ = cond_exp M (F i) (X (Suc i)) ξ" using cond_exp_diff[OF integrable(1,1), of i "Suc i" i] cond_exp_F_meas[OF integrable adapted, of i] assms(3)[of i] by fastforce
qed

end

subsection ‹Discrete Time Submartingales›

context nat_sigma_finite_filtered_measure
begin

lemma predictable_mono:
  assumes "submartingale M F 0 X"
    and "predictable_process M F 0 X" "i ≤ j"
  shows "AE ξ in M. X i ξ ≤ X j ξ"
  using assms(3)
proof (induction "j - i" arbitrary: i j)
  case 0
  then show ?case by simp 
next
  case (Suc n)
  hence *: "n = j - Suc i" by linarith
  interpret submartingale M F 0 X by (rule assms)
  interpret S: adapted_process M F 0 "λi. X (Suc i)" by (intro predictable_implies_adapted_Suc assms)
  have "Suc i ≤ j" using Suc(2,3) by linarith
  thus ?case using Suc(1)[OF *] S.adapted[of i] submartingale_property[OF _ le_SucI, of i] sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable, of "F i" "Suc i"] by fastforce
qed

lemma submartingale_of_set_integral_le_Suc:
  fixes X :: "_ ⇒ _ ⇒ _ :: {linorder_topology}"
  assumes adapted: "adapted_process M F 0 X"
      and integrable: "⋀i. integrable M (X i)" 
      and "⋀A i. A ∈ F i ⟹ set_lebesgue_integral M A (X i) ≤ set_lebesgue_integral M A (X (Suc i))" 
    shows "submartingale M F 0 X"
proof (intro submartingale_of_set_integral_le adapted integrable)
  fix i j A assume asm: "i ≤ j" "A ∈ sets (F i)"
  show "set_lebesgue_integral M A (X i) ≤ set_lebesgue_integral M A (X j)" using asm
  proof (induction "j - i" arbitrary: i j)
    case 0
    then show ?case using asm by simp
  next
    case (Suc n)
    hence *: "n = j - Suc i" by linarith
    have "Suc i ≤ j" using Suc(2,3) by linarith
    thus ?case using sets_F_mono[OF _ le_SucI] Suc(4) Suc(1)[OF *] by (auto intro: assms(3)[THEN order_trans])
  qed
qed

lemma submartingale_nat:
  fixes X :: "_ ⇒ _ ⇒ _ :: {linorder_topology}"
  assumes adapted: "adapted_process M F 0 X"
      and integrable: "⋀i. integrable M (X i)" 
      and "⋀i. AE ξ in M. X i ξ ≤ cond_exp M (F i) (X (Suc i)) ξ" 
    shows "submartingale M F 0 X"
proof -
  show ?thesis using subalg assms(3) integrable
    by (intro submartingale_of_set_integral_le_Suc adapted integrable ord_le_eq_trans[OF set_integral_mono_AE_banach cond_exp_set_integral[symmetric]])
       (meson in_mono integrable_mult_indicator set_integrable_def subalgebra_def, meson integrable_cond_exp in_mono integrable_mult_indicator set_integrable_def subalgebra_def, fast+)
qed

lemma submartingale_of_cond_exp_diff_Suc_nonneg:
  fixes X :: "_ ⇒ _ ⇒ _ :: {linorder_topology}"
  assumes adapted: "adapted_process M F 0 X"
      and integrable: "⋀i. integrable M (X i)" 
      and "⋀i. AE ξ in M. cond_exp M (F i) (λξ. X (Suc i) ξ - X i ξ) ξ ≥ 0" 
    shows "submartingale M F 0 X"
proof (intro submartingale_nat integrable adapted)
  interpret adapted_process M F 0 X by (rule assms)
  fix i 
  show "AE ξ in M. X i ξ ≤ cond_exp M (F i) (X (Suc i)) ξ" using cond_exp_diff[OF integrable(1,1), of i "Suc i" i] cond_exp_F_meas[OF integrable adapted, of i] assms(3)[of i] by fastforce
qed

lemma submartingale_partial_sum_scaleR:
  assumes "submartingale_linorder M F 0 X"
    and "adapted_process M F 0 C" "⋀i. AE ξ in M. 0 ≤ C i ξ" "⋀i. AE ξ in M. C i ξ ≤ R"
  shows "submartingale M F 0 (λn ξ. ∑i<n. C i ξ *⇩R (X (Suc i) ξ - X i ξ))"
proof -
  interpret submartingale_linorder M F 0 X by (rule assms)
  interpret C: adapted_process M F 0 C by (rule assms)
  interpret C': adapted_process M F 0 "λi ξ. C (i - 1) ξ *⇩R (X i ξ - X (i - 1) ξ)" by (intro adapted_process.scaleR_right_adapted adapted_process.diff_adapted, unfold_locales) (auto intro: adaptedD C.adaptedD)+
  interpret S: adapted_process M F 0 "λn ξ. ∑i<n. C i ξ *⇩R (X (Suc i) ξ - X i ξ)" using C'.adapted_process_axioms[THEN partial_sum_Suc_adapted] diff_Suc_1 by simp
  have "integrable M (λx. C i x *⇩R (X (Suc i) x - X i x))" for i using assms(3,4)[of i] by (intro Bochner_Integration.integrable_bound[OF integrable_scaleR_right, OF Bochner_Integration.integrable_diff, OF integrable(1,1), of R "Suc i" i]) (auto simp add: mult_mono)
  moreover have "AE ξ in M. 0 ≤ cond_exp M (F i) (λξ. (∑i<Suc i. C i ξ *⇩R (X (Suc i) ξ - X i ξ)) - (∑i<i. C i ξ *⇩R (X (Suc i) ξ - X i ξ))) ξ" for i 
    using sigma_finite_subalgebra.cond_exp_measurable_scaleR[OF _ calculation _ C.adapted, of i] 
          cond_exp_diff_nonneg[OF _ le_SucI, OF _ order.refl, of i] assms(3,4)[of i] by (fastforce simp add: scaleR_nonneg_nonneg integrable)
  ultimately show ?thesis by (intro submartingale_of_cond_exp_diff_Suc_nonneg S.adapted_process_axioms Bochner_Integration.integrable_sum, blast+)
qed

lemma submartingale_partial_sum_scaleR':
  assumes "submartingale_linorder M F 0 X"
    and "predictable_process M F 0 C" "⋀i. AE ξ in M. 0 ≤ C i ξ" "⋀i. AE ξ in M. C i ξ ≤ R"
  shows "submartingale M F 0 (λn ξ. ∑i<n. C (Suc i) ξ *⇩R (X (Suc i) ξ - X i ξ))"
proof -
  interpret Suc_C: adapted_process M F 0 "λi. C (Suc i)" using predictable_implies_adapted_Suc assms by blast
  show ?thesis by (intro submartingale_partial_sum_scaleR[OF assms(1), of _ R] assms) (intro_locales)
qed

end

subsection ‹Discrete Time Supermartingales›

context nat_sigma_finite_filtered_measure
begin

lemma predictable_mono':
  assumes "supermartingale M F 0 X"
    and "predictable_process M F 0 X" "i ≤ j"
  shows "AE ξ in M. X i ξ ≥ X j ξ"
  using assms(3)
proof (induction "j - i" arbitrary: i j)
  case 0
  then show ?case by simp 
next
  case (Suc n)
  hence *: "n = j - Suc i" by linarith
  interpret supermartingale M F 0 X by (rule assms)
  interpret S: adapted_process M F 0 "λi. X (Suc i)" by (intro predictable_implies_adapted_Suc assms)
  have "Suc i ≤ j" using Suc(2,3) by linarith
  thus ?case using Suc(1)[OF *] S.adapted[of i] supermartingale_property[OF _ le_SucI, of i] sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable, of "F i" "Suc i"] by fastforce
qed
  
lemma supermartingale_of_set_integral_ge_Suc:
  fixes X :: "_ ⇒ _ ⇒ _ :: {linorder_topology}"
  assumes adapted: "adapted_process M F 0 X"
      and integrable: "⋀i. integrable M (X i)" 
      and "⋀A i. A ∈ F i ⟹ set_lebesgue_integral M A (X i) ≥ set_lebesgue_integral M A (X (Suc i))" 
    shows "supermartingale M F 0 X"
proof -
  interpret adapted_process M F 0 X by (rule assms)
  interpret uminus_X: adapted_process M F 0 "-X" by (rule uminus_adapted)
  note * = set_integral_uminus[unfolded set_integrable_def, OF integrable_mult_indicator[OF _ integrable]]
  have "supermartingale M F 0 (-(- X))" 
    using ord_eq_le_trans[OF * ord_le_eq_trans[OF le_imp_neg_le[OF assms(3)] *[symmetric]]] sets_F_subset[THEN subsetD]
    by (intro submartingale.uminus submartingale_of_set_integral_le_Suc[OF uminus_adapted]) 
       (clarsimp simp add: fun_Compl_def integrable | fastforce)+
  thus ?thesis unfolding fun_Compl_def by simp
qed

lemma supermartingale_nat:
  fixes X :: "_ ⇒ _ ⇒ _ :: {linorder_topology}"
  assumes adapted: "adapted_process M F 0 X"
      and integrable: "⋀i. integrable M (X i)" 
      and "⋀i. AE ξ in M. X i ξ ≥ cond_exp M (F i) (X (Suc i)) ξ" 
    shows "supermartingale M F 0 X"
proof -
  interpret adapted_process M F 0 X by (rule assms)
  have "AE ξ in M. - X i ξ ≤ cond_exp M (F i) (λx. - X (Suc i) x) ξ" for i using assms(3) cond_exp_uminus[OF integrable, of i "Suc i"] by force
  hence "supermartingale M F 0 (-(- X))" by (intro submartingale.uminus submartingale_nat[OF uminus_adapted]) (auto simp add: fun_Compl_def integrable)
  thus ?thesis unfolding fun_Compl_def by simp
qed

lemma supermartingale_of_cond_exp_diff_Suc_le_zero:
  fixes X :: "_ ⇒ _ ⇒ _ :: {linorder_topology}"
  assumes adapted: "adapted_process M F 0 X"
      and integrable: "⋀i. integrable M (X i)" 
      and "⋀i. AE ξ in M. cond_exp M (F i) (λξ. X (Suc i) ξ - X i ξ) ξ ≤ 0" 
    shows "supermartingale M F 0 X"
proof (intro supermartingale_nat integrable adapted) 
  interpret adapted_process M F 0 X by (rule assms)
  fix i
  show "AE ξ in M. X i ξ ≥ cond_exp M (F i) (X (Suc i)) ξ" using cond_exp_diff[OF integrable(1,1), of i "Suc i" i] cond_exp_F_meas[OF integrable adapted, of i] assms(3)[of i] by fastforce
qed

end

end