Theory Optional_Stopping

section ‹Fair Games Theorem›

theory Optional_Stopping
  imports
    Piecewise_Stopping_Time
    "Martingales.Martingale"
begin

text ‹The optional stopping theorem (fair games theorem): an adapted integrable process is a
  submartingale if and only if for all bounded stopping times @{term τ} and @{term π} with
  @{term "τ ≤ π"}, the expected stopped value at @{term τ} is at most that at @{term π}.
  We also prove that the stopped process of a submartingale is a submartingale.›

context nat_sigma_finite_filtered_measure
begin

subsection ‹Helper lemmas›

lemma indicator_set_in_F:
  assumes τ_st: "stopping_time τ" and π_st: "stopping_time π"
  shows "{ω ∈ space M. τ ω ≤ i ∧ i < π ω} ∈ sets (F i)"
proof -
  have *: "Measurable.pred (F i) (λω. τ ω ≤ i ∧ ¬ π ω ≤ i)"
    by (simp add: π_st τ_st pred_intros_logic stopping_timeD)
  have eq: "{ω ∈ space M. τ ω ≤ i ∧ i < π ω} = {ω ∈ space (F i). τ ω ≤ i ∧ ¬ π ω ≤ i}"
    by auto
  show ?thesis using Measurable.predE[OF *] sets_F_subset[of i]
    by (auto simp: eq)
qed

subsection ‹Forward direction›

text ‹If @{term X} is a submartingale and @{term "τ ≤ π"} are bounded stopping times,
  then @{term "(∫ω. stopped_value X τ ω ∂M) ≤ (∫ω. stopped_value X π ω ∂M)"}.
  This corresponds to ▩‹Submartingale.expected_stoppedValue_mono› in Mathlib.›

theorem expected_stopped_value_mono:
  fixes X :: "nat ⇒ 'a ⇒ real"
  assumes sub: "submartingale_linorder M F 0 X"
    and τ_st: "stopping_time τ" and π_st: "stopping_time π"
    and le: "⋀ω. ω ∈ space M ⟹ τ ω ≤ π ω"
    and bnd: "⋀ω. ω ∈ space M ⟹ π ω ≤ N"
  shows "(∫ω. stopped_value X τ ω ∂M) ≤ (∫ω. stopped_value X π ω ∂M)"
proof -
  from sub interpret S: submartingale_linorder M F 0 X .
  have τ_bnd: "⋀ω. ω ∈ space M ⟹ τ ω ≤ N"
    using le bnd by (meson order_trans)
  ― ‹Integrability of stopped values›
  obtain int_τ: "integrable M (stopped_value X τ)" and int_π: "integrable M (stopped_value X π)"
    by (meson S.integrable τ_bnd τ_st π_st bnd integrable_stopped_value zero_le)
  ― ‹Suffices to show the difference is non-negative›
  have "0 ≤ (∫ω. stopped_value X π ω ∂M) - (∫ω. stopped_value X τ ω ∂M)"
  proof -
    have "(∫ω. stopped_value X π ω ∂M) - (∫ω. stopped_value X τ ω ∂M) =
          (∫ω. stopped_value X π ω - stopped_value X τ ω ∂M)"
      by (rule Bochner_Integration.integral_diff[OF int_π int_τ, symmetric])
    ― ‹Apply the telescoping identity AE›
    also have "… = (∫ω. (∑i≤N. indicator {ω ∈ space M. τ ω ≤ i ∧ i < π ω} ω *
      (X (Suc i) ω - X i ω)) ∂M)"
    proof (rule Bochner_Integration.integral_cong_AE)
      show "(λω. stopped_value X π ω - stopped_value X τ ω) ∈ borel_measurable M"
        using int_π int_τ by (intro borel_measurable_diff) auto
      show "(λω. ∑i≤N. indicator {ω ∈ space M. τ ω ≤ i ∧ i < π ω} ω *
        (X (Suc i) ω - X i ω)) ∈ borel_measurable M"
      proof (intro borel_measurable_sum borel_measurable_times borel_measurable_indicator
                   borel_measurable_diff borel_measurable_integrable)
        fix i assume "i ∈ {..N}"
        show "{ω ∈ space M. τ ω ≤ i ∧ i < π ω} ∈ sets M"
          using indicator_set_in_F[OF τ_st π_st] sets_F_subset by blast
      qed (auto simp: S.integrable)
      show "AE ω in M. stopped_value X π ω - stopped_value X τ ω =
        (∑i≤N. indicator {ω ∈ space M. τ ω ≤ i ∧ i < π ω} ω * (X (Suc i) ω - X i ω))"
        by (rule AE_I2) (simp add: stopped_value_sub_eq_sum[OF τ_st π_st le bnd])
    qed
    ― ‹Exchange integral and sum›
    also have "… = (∑i≤N. ∫ω. indicator {ω ∈ space M. τ ω ≤ i ∧ i < π ω} ω *
      (X (Suc i) ω - X i ω) ∂M)"
    proof (rule Bochner_Integration.integral_sum)
      fix i assume "i ∈ {..N}"
      have "{ω ∈ space M. τ ω ≤ i ∧ i < π ω} ∈ sets M"
        using indicator_set_in_F[OF τ_st π_st] sets_F_subset by blast
      then show "integrable M (λω. indicator {ω ∈ space M. τ ω ≤ i ∧ i < π ω} ω * (X (Suc i) ω - X i ω))"
        by (simp add: S.integrable integrable_real_mult_indicator mult.commute)
    qed
    ― ‹Each summand is non-negative via @{text set_integral_le}›
    also have "… ≥ 0"
    proof (rule sum_nonneg)
      fix i assume "i ∈ {..N}"
      let ?A = "{ω ∈ space M. τ ω ≤ i ∧ i < π ω}"
      have A_Fi: "?A ∈ sets (F i)"
        by (rule indicator_set_in_F[OF τ_st π_st])
      ― ‹The summand equals @{text "∫⇩A X(Suc i) - ∫⇩A X i"}›
      have eq: "(∫ω. indicat_real ?A ω * (X (Suc i) ω - X i ω) ∂M) =
        set_lebesgue_integral M ?A (X (Suc i)) - set_lebesgue_integral M ?A (X i)"
      proof -
        have "?A ∈ sets M"
          using A_Fi sets_F_subset by blast
        then have int: "integrable M (λx. indicat_real ?A x * X j x)" for j
          by (simp add: S.integrable integrable_real_mult_indicator mult.commute)
        have "(∫ω. indicat_real ?A ω * (X (Suc i) ω - X i ω) ∂M) =
          (∫ω. indicat_real ?A ω * X (Suc i) ω - indicat_real ?A ω * X i ω ∂M)"
          by (simp add: right_diff_distrib)
        also have "… = (∫ω. indicat_real ?A ω * X (Suc i) ω ∂M) - (∫ω. indicat_real ?A ω * X i ω ∂M)"
          using Bochner_Integration.integral_diff int by blast
        also have "… = set_lebesgue_integral M ?A (X (Suc i)) - set_lebesgue_integral M ?A (X i)"
          unfolding set_lebesgue_integral_def by (simp add: scaleR_conv_of_real)
        finally show ?thesis .
      qed
      ― ‹Apply the submartingale @{text set_integral_le} property›
      have "set_lebesgue_integral M ?A (X i) ≤ set_lebesgue_integral M ?A (X (Suc i))"
        by (rule S.set_integral_le[OF A_Fi]) simp_all
      then show "0 ≤ (∫ω. indicat_real ?A ω * (X (Suc i) ω - X i ω) ∂M)"
        unfolding eq by simp
    qed
    finally show ?thesis by simp
  qed
  then show ?thesis by simp
qed

subsection ‹Converse direction›

text ‹If an adapted integrable process satisfies the monotonicity of expected stopped values
  for all bounded stopping times, then it is a submartingale.
  This corresponds to ▩‹submartingale_of_expected_stoppedValue_mono› in Mathlib.›

theorem submartingale_of_expected_stopped_value_mono:
  fixes X :: "nat ⇒ 'a ⇒ real"
  assumes adapted: "adapted_process M F 0 X"
    and integrable: "⋀i. integrable M (X i)"
    and mono: "⋀τ π N. stopping_time τ ⟹ stopping_time π ⟹
      (⋀ω. ω ∈ space M ⟹ τ ω ≤ π ω) ⟹ (⋀ω. ω ∈ space M ⟹ π ω ≤ N) ⟹
      (∫ω. stopped_value X τ ω ∂M) ≤ (∫ω. stopped_value X π ω ∂M)"
  shows "submartingale M F 0 X"
proof (rule submartingale_of_set_integral_le_Suc[OF adapted integrable])
  fix A :: "'a set" and i :: nat
  assume A_Fi: "A ∈ sets (F i)"
  ― ‹Construct piecewise stopping times›
  define τ :: "'a ⇒ nat" where "τ ω = (if ω ∈ A then i else Suc i)" for ω
  define π :: "'a ⇒ nat" where "π ω = Suc i" for ω
  have τ_st: "stopping_time τ"
    unfolding τ_def by (rule stopping_time_piecewise_const) (simp_all add: A_Fi)
  have π_st: "stopping_time π"
    unfolding π_def by (rule stopping_time_const) simp
  have τ_le_π: "⋀ω. ω ∈ space M ⟹ τ ω ≤ π ω"
    unfolding τ_def π_def by simp
  have π_bnd: "⋀ω. ω ∈ space M ⟹ π ω ≤ Suc i"
    unfolding π_def by simp
  ― ‹Apply the monotonicity hypothesis›
  have ineq: "(∫ω. stopped_value X τ ω ∂M) ≤ (∫ω. stopped_value X π ω ∂M)"
    by (rule mono[OF τ_st π_st τ_le_π π_bnd])
  ― ‹Decompose stopped values›
  have A_sub: "A ⊆ space M"
    using A_Fi sets_F_subset sets.sets_into_space by blast
  have sv_τ: "stopped_value X τ = (λω. if ω ∈ A then X i ω else X (Suc i) ω)"
    unfolding τ_def by (rule stopped_value_piecewise_const[OF A_sub])
  have sv_π: "stopped_value X π = X (Suc i)"
    unfolding π_def stopped_value_def by simp
  ― ‹Decompose the integral of the piecewise function›
  have A_meas: "A ∈ sets M"
    using A_Fi sets_F_subset by blast
  have lhs: "(∫ω. stopped_value X τ ω ∂M) =
    set_lebesgue_integral M A (X i) + set_lebesgue_integral M (space M - A) (X (Suc i))"
    unfolding sv_τ by (rule integral_piecewise[OF A_meas integrable integrable])
  have rhs: "(∫ω. stopped_value X π ω ∂M) =
             set_lebesgue_integral M A (X (Suc i)) + set_lebesgue_integral M (space M - A) (X (Suc i))"
  proof -
    have "(∫ω. stopped_value X π ω ∂M) = (∫ω. X (Suc i) ω ∂M)"
      unfolding sv_π ..
    also have "… = (∫ω. (if ω ∈ A then X (Suc i) ω else X (Suc i) ω) ∂M)"
      by simp
    also have "… = set_lebesgue_integral M A (X (Suc i)) +
      set_lebesgue_integral M (space M - A) (X (Suc i))"
      by (rule integral_piecewise[OF A_meas integrable integrable])
    finally show ?thesis .
  qed
  show "set_lebesgue_integral M A (X i) ≤ set_lebesgue_integral M A (X (Suc i))"
    using ineq lhs rhs by simp
qed

subsection ‹The optional stopping theorem (iff)›

text ‹The full characterization: an adapted integrable process is a submartingale iff
  expected stopped values are monotone for all bounded stopping times.
  This corresponds to ▩‹submartingale_iff_expected_stoppedValue_mono› in Mathlib.›

theorem submartingale_iff_expected_stopped_value_mono:
  fixes X :: "nat ⇒ 'a ⇒ real"
  assumes "adapted_process M F 0 X" "⋀i. integrable M (X i)"
  shows "submartingale M F 0 X ⟷
    (∀τ π. stopping_time τ ⟶ stopping_time π ⟶
      (∀ω∈space M. τ ω ≤ π ω) ⟶ (∃N. ∀ω∈space M. π ω ≤ N) ⟶
      (∫ω. stopped_value X τ ω ∂M) ≤ (∫ω. stopped_value X π ω ∂M))" (is "?L = ?R")
proof
  show "?L ⟹ ?R"
    by (metis expected_stopped_value_mono submartingale_linorder_def)
  show "?R ⟹ ?L"
    by (intro submartingale_of_expected_stopped_value_mono[OF assms]) blast
qed

subsection ‹Stopped process of a submartingale›

text ‹The stopped process of a submartingale with respect to a stopping time is a submartingale.
  This corresponds to ▩‹Submartingale.stoppedProcess› in Mathlib.›

text ‹We first show the stopped process is adapted. The proof proceeds by induction:
  @{text "X⇧τ 0 = X 0"} is trivially @{term "F 0"}-measurable, and
  @{text "X⇧τ (Suc n) = if τ ≤ n then X⇧τ n else X (Suc n)"} is @{term "F (Suc n)"}-measurable
  by the induction hypothesis, adaptedness of @{term X}, and the stopping time property.›

lemma adapted_stopped_process:
  fixes X :: "nat ⇒ 'a ⇒ real"
  assumes adapted: "adapted_process M F 0 X" and τ_st: "stopping_time τ"
  shows "adapted_process M F 0 (stopped_process X τ)"
proof (rule adapted_process.intro[OF filtered_measure_axioms])
  show "adapted_process_axioms F 0 (stopped_process X τ)"
  proof (rule adapted_process_axioms.intro)
    fix i :: nat assume "0 ≤ i"
    show "stopped_process X τ i ∈ borel_measurable (F i)"
    proof (induction i)
      case 0
      have "stopped_process X τ 0 = X 0"
        unfolding stopped_process_def by simp
      then show ?case
        using adapted_process.adapted[OF adapted, of 0] by simp
    next
      case (Suc n)
      ― ‹The stopped process at @{term "Suc n"} equals a piecewise function on @{term "space M"}›
      have eq: "⋀ω. stopped_process X τ (Suc n) ω =
        (if τ ω ≤ n then stopped_process X τ n ω else X (Suc n) ω)"
        unfolding stopped_process_def by (auto simp: min_def)
      ― ‹@{term "F n"} is a sub-sigma-algebra of @{term "F (Suc n)"}›
      have subalg: "subalgebra (F (Suc n)) (F n)"
        unfolding subalgebra_def using space_F sets_F_mono[of n "Suc n"] by auto
      ― ‹The induction hypothesis gives @{term "F n"}-measurability, lift to @{term "F (Suc n)"}›
      have meas_n: "stopped_process X τ n ∈ borel_measurable (F (Suc n))"
        by (rule measurable_from_subalg[OF subalg Suc.IH])
      ― ‹@{term "X (Suc n)"} is @{term "F (Suc n)"}-measurable by adaptedness›
      have meas_Sn: "X (Suc n) ∈ borel_measurable (F (Suc n))"
        using adapted_process.adapted[OF adapted] by simp
      ― ‹The set @{term "{ω. τ ω ≤ n}"} is in @{term "sets (F (Suc n))"}›
      have set_Sn: "{ω ∈ space (F (Suc n)). τ ω ≤ n} ∈ sets (F (Suc n))"
        using τ_st order_less_imp_le predE stopping_time_measurable_le by blast
      ― ‹The piecewise function is @{term "F (Suc n)"}-measurable›
      let ?A = "{ω ∈ space (F (Suc n)). τ ω ≤ n}"
      have A_sets: "?A ∈ sets (F (Suc n))" by (rule set_Sn)
      have A_sub: "?A ⊆ space (F (Suc n))" using sets.sets_into_space[OF A_sets] .
      have meas_pw: "(λω. if ω ∈ ?A then stopped_process X τ n ω else X (Suc n) ω)
        ∈ borel_measurable (F (Suc n))"
        using measurable_If_set meas_n meas_Sn set_Sn by blast
      ― ‹Transfer: the stopped process agrees with the piecewise function on @{term "space (F (Suc n))"}›
      show ?case
        using measurable_cong[of "F (Suc n)" "stopped_process X τ (Suc n)"
          "λω. if ω ∈ ?A then stopped_process X τ n ω else _ ω"]
          eq meas_pw by fastforce
    qed
  qed
qed

theorem stopped_process_submartingale:
  fixes X :: "nat ⇒ 'a ⇒ real"
  assumes sub: "submartingale_linorder M F 0 X"
    and τ_st: "stopping_time τ"
  shows "submartingale M F 0 (stopped_process X τ)"
proof -
  let ?sv = "stopped_value (stopped_process X τ)"
  from sub interpret S: submartingale_linorder M F 0 X .
  ― ‹Use the converse direction: suffices to show monotonicity of expected stopped values›
  show ?thesis
  proof (rule submartingale_of_expected_stopped_value_mono)
    show "adapted_process M F 0 (stopped_process X τ)"
      by (simp add: S.adapted_process_axioms τ_st adapted_stopped_process)
    show "⋀i. integrable M (stopped_process X τ i)"
      by (simp add: S.integrable τ_st integrable_stopped_process)
  next
    fix σ ρ :: "'a ⇒ nat" and N :: nat
    assume σ_st: "stopping_time σ" and ρ_st: "stopping_time ρ"
      and "⋀ω. ω ∈ space M ⟹ σ ω ≤ ρ ω"
      and bnd: "⋀ω. ω ∈ space M ⟹ ρ ω ≤ N"
    then have le': "⋀ω. ω ∈ space M ⟹ min (σ ω) (τ ω) ≤ min (ρ ω) (τ ω)"
      by (simp add: min_le_iff_disj)
    ― ‹stopped value of the stopped process equals that of @{term X} with @{const min}›
    have sv: "?sv σ = stopped_value X (λω. min (σ ω) (τ ω))" "?sv ρ = stopped_value X (λω. min (ρ ω) (τ ω))"
      unfolding stopped_value_def stopped_process_def by auto
    ― ‹@{term "λω. min (σ ω) (τ ω)"} and @{term "λω. min (ρ ω) (τ ω)"} are stopping times›
    have st_σ': "stopping_time (λω. min (σ ω) (τ ω))"
      by (intro stopping_time_min σ_st τ_st)
    have st_ρ': "stopping_time (λω. min (ρ ω) (τ ω))"
      by (intro stopping_time_min ρ_st τ_st)
    ― ‹Apply the forward direction›
    show "(∫ω. ?sv σ ω ∂M) ≤ (∫ω. ?sv ρ ω ∂M)"
      using expected_stopped_value_mono[OF sub st_σ' st_ρ' le'] sv bnd min_le_iff_disj
      by metis
  qed
qed

end

end