Theory Stopped_Value_Integration

section ‹Integrability of Stopped Values and Processes›

theory Stopped_Value_Integration
  imports "Doob_Convergence.Stopping_Time"
begin

text ‹Integrability of stopped values and stopped processes, and the telescoping identity
  for differences of stopped values. These results bridge the gap between the existing
  AFP theories (Martingales, ▩‹Doob_Convergence›) and the optional stopping theorem.›

context nat_sigma_finite_filtered_measure
begin

subsection ‹Stopped value as a sum of indicators›

text ‹A stopped value with a bounded stopping time can be written as a finite sum of indicators.›

lemma stopped_value_eq_sum:
  fixes X :: "nat ⇒ 'a ⇒ 'b :: real_vector"
  assumes τ_st: "stopping_time τ" and τ_bnd: "⋀ω. ω ∈ space M ⟹ τ ω ≤ N"
  assumes ω_in: "ω ∈ space M"
  shows "stopped_value X τ ω = (∑i≤N. indicator {ω ∈ space M. τ ω = i} ω *⇩R X i ω)"
proof -
  have "stopped_value X τ ω = X (τ ω) ω"
    by (simp add: stopped_value_def)
  also have "… = 1 *⇩R X (τ ω) ω" by (metis (full_types) scale_one)
  also have "… = indicator {ω ∈ space M. τ ω = τ ω} ω *⇩R X (τ ω) ω +
    (∑i ∈ {..N} - {τ ω}. indicator {ω ∈ space M. τ ω = i} ω *⇩R X i ω)"
    using ω_in by (simp add: indicator_def)
  also have "… = (∑i≤N. indicator {ω ∈ space M. τ ω = i} ω *⇩R X i ω)"
    using ω_in τ_bnd[OF ω_in]
    by (subst sum.remove [where x = "τ ω"]) simp_all
  finally show ?thesis .
qed

subsection ‹Telescoping identity for stopped values›

text ‹The difference of stopped values can be expressed as a sum of indicator-weighted increments.
  This corresponds to ▩‹stoppedValue_sub_eq_sum'› in Mathlib.›

lemma stopped_value_sub_eq_sum:
  fixes X :: "nat ⇒ 'a ⇒ real"
  assumes τ_st: "stopping_time τ" and π_st: "stopping_time π"
    and le: "⋀ω. ω ∈ space M ⟹ τ ω ≤ π ω"
    and bnd: "⋀ω. ω ∈ space M ⟹ π ω ≤ N"
    and ω_in: "ω ∈ space M"
  shows "stopped_value X π ω - stopped_value X τ ω =
    (∑i≤N. indicator {ω ∈ space M. τ ω ≤ i ∧ i < π ω} ω * (X (Suc i) ω - X i ω))"
proof -
  have "(∑i≤N. indicator {ω ∈ space M. τ ω ≤ i ∧ i < π ω} ω * (X (Suc i) ω - X i ω)) =
    (∑i∈{τ ω..<π ω}. X (Suc i) ω - X i ω)"
    using ω_in bnd[OF ω_in] 
    by (intro sum.mono_neutral_cong_right) (auto simp: indicator_def)
  also have "… = X (π ω) ω - X (τ ω) ω"
    using ω_in le sum_Suc_diff' by fastforce
  finally show ?thesis by (simp add: stopped_value_def)
qed

text ‹If each @{term "X i"} is integrable and the stopping time is bounded, then the stopped value
  is integrable. This corresponds to ▩‹integrable_stoppedValue› in Mathlib.›

lemma integrable_stopped_value:
  fixes X :: "nat ⇒ 'a ⇒ real"
  assumes τ_st: "stopping_time τ" and int_X: "⋀i. integrable M (X i)"
    and τ_bnd: "⋀ω. ω ∈ space M ⟹ τ ω ≤ N"
  shows "integrable M (stopped_value X τ)"
proof -
  ― ‹Each indicator set is measurable›
  have meas_eq: "⋀i. {ω ∈ space M. τ ω = i} ∈ sets M"
  proof -
    fix i :: nat
    have "Measurable.pred (F i) (λω. τ ω = i)"
      by (rule stopping_time_measurable_eq[OF τ_st]) simp_all
    then have "{ω ∈ space M. τ ω = i} ∈ sets (F i)"
      by (metis predE subalg subalgebra_def)
    then show "{ω ∈ space M. τ ω = i} ∈ sets M"
      using sets_F_subset[of i] by blast
  qed
  ― ‹Each summand is integrable›
  have int_summand: "⋀i. integrable M (λω. indicat_real {ω ∈ space M. τ ω = i} ω * X i ω)"
    by (simp add: int_X integrable_real_mult_indicator meas_eq mult.commute)
  ― ‹The sum is integrable›
  have int_sum: "integrable M (λω. ∑i≤N. indicat_real {ω ∈ space M. τ ω = i} ω * X i ω)"
    by (intro Bochner_Integration.integrable_sum) (auto intro: int_summand)
  ― ‹The stopped value agrees with the sum AE›
  have eq: "AE ω in M. (∑i≤N. indicat_real {ω ∈ space M. τ ω = i} ω * X i ω) =
    stopped_value X τ ω"
    by (intro AE_I2) (simp add: stopped_value_eq_sum[OF τ_st τ_bnd])
  have eq_space: "⋀ω. ω ∈ space M ⟹
    stopped_value X τ ω = (∑i≤N. indicat_real {ω ∈ space M. τ ω = i} ω * X i ω)"
    by (simp add: stopped_value_eq_sum[OF τ_st τ_bnd])
  ― ‹Measurability via @{thm measurable_cong} with the sum›
  have meas_sum: "(λω. ∑i≤N. indicat_real {ω ∈ space M. τ ω = i} ω * X i ω) ∈ borel_measurable M"
    using int_sum by (rule borel_measurable_integrable)
  have meas_sv: "stopped_value X τ ∈ borel_measurable M"
    using measurable_cong[of M "stopped_value X τ"
      "λω. ∑i≤N. indicat_real {ω ∈ space M. τ ω = i} ω * X i ω" borel]
      eq_space meas_sum by auto
  ― ‹Transfer integrability via AE equality›
  show ?thesis
    by (rule Bochner_Integration.integrable_cong_AE_imp[OF int_sum meas_sv eq])
qed

subsection ‹Stopped process›

text ‹The stopped process @{text "X⇧τ"} is defined as @{text "X (min i τ)"}.›

definition stopped_process :: "(nat ⇒ 'a ⇒ 'b) ⇒ ('a ⇒ nat) ⇒ nat ⇒ 'a ⇒ 'b" where
  "stopped_process X τ i ω ≡ X (min i (τ ω)) ω"

lemma stopped_process_eq_stopped_value:
  "stopped_process X τ i = stopped_value X (λω. min i (τ ω))"
  unfolding stopped_process_def stopped_value_def by simp

lemma integrable_stopped_process:
  fixes X :: "nat ⇒ 'a ⇒ real"
  assumes "stopping_time τ" "⋀i. integrable M (X i)"
  shows "integrable M (stopped_process X τ n)"
proof -
  have "stopping_time (λω. min n (τ ω))"
    by (intro stopping_time_min stopping_time_const assms) simp
  with assms show ?thesis
    unfolding stopped_process_eq_stopped_value
    using integrable_stopped_value min.cobounded1 by blast
qed

end

end