Theory Piecewise_Stopping_Time

section ‹Piecewise Stopping Times›

theory Piecewise_Stopping_Time
  imports Stopped_Value_Integration

begin

text ‹Piecewise constant stopping times and their interaction with stopped values and integration.
  These are needed for the converse direction of the optional stopping theorem.›

context nat_sigma_finite_filtered_measure
begin

subsection ‹Piecewise constant stopping times›

text ‹Given @{term "i ≤ j"} and an @{term "F i"}-measurable set @{term S}, the function that
  returns @{term i} on @{term S} and @{term j} on its complement is a stopping time.
  This corresponds to ▩‹isStoppingTime_piecewise_const› in Mathlib.›

lemma stopping_time_piecewise_const:
  assumes "i ≤ j" and S: "S ∈ sets (F i)"
  shows "stopping_time (λω. if ω ∈ S then i else j)"
proof (rule stopping_timeI)
  fix ω assume "ω ∈ space M"
  show "0 ≤ (if ω ∈ S then i else j)" by simp
next
  fix t :: nat assume "0 ≤ t"
  have space_eq: "space (F t) = space M" by simp
  have top: "space M ∈ sets (F t)" using sets.top[of "F t"] by simp
  show "Measurable.pred (F t) (λω. (if ω ∈ S then i else j) ≤ t)"
    unfolding Measurable.pred_def
  proof -
    consider "j ≤ t" | "i ≤ t" "¬ j ≤ t" | "¬ i ≤ t"
      using ‹i ≤ j› by linarith
    then show "{ω ∈ space (F t). (if ω ∈ S then i else j) ≤ t} ∈ sets (F t)"
    proof cases
      case 1
      then have "{ω ∈ space (F t). (if ω ∈ S then i else j) ≤ t} = space (F t)"
        using ‹i ≤ j› by (auto simp: space_eq)
      then show ?thesis using top space_eq by simp
    next
      case 2
      then have "{ω ∈ space (F t). (if ω ∈ S then i else j) ≤ t} = S"
        using S sets.sets_into_space subset_antisym by fastforce
      then show ?thesis
        using S 2 sets_F_mono by force 
    next
      case 3
      then show ?thesis 
        using ‹i ≤ j› by (auto simp: Measurable.pred_def space_eq split: if_splits)
    qed
  qed
qed

text ‹The stopped value at a piecewise constant stopping time decomposes into a piecewise function.
  This corresponds to ▩‹stoppedValue_piecewise_const› in Mathlib.›

lemma stopped_value_piecewise_const:
  assumes "S ⊆ space M"
  shows "stopped_value X (λω. if ω ∈ S then i else j) = (λω. if ω ∈ S then X i ω else X j ω)"
  unfolding stopped_value_def by (simp add: if_distrib if_distribR)

subsection ‹Integration over piecewise functions›

text ‹The integral of a piecewise function splits into integrals over the two pieces.
  This corresponds to ▩‹integral_piecewise› in Mathlib.›

lemma piecewise_eq_indicator_sum:
  fixes f g :: "'a ⇒ real"
  assumes "S ∈ sets M" "ω ∈ space M"
  shows "(if ω ∈ S then f ω else g ω) = indicat_real S ω * f ω + indicat_real (space M - S) ω * g ω"
  using ‹ω ∈ space M› by (auto simp: indicator_def)

lemma integral_piecewise:
  fixes f g :: "'a ⇒ real"
  assumes S_meas: "S ∈ sets M" and int_f: "integrable M f" and int_g: "integrable M g"
  shows "(∫ω. (if ω ∈ S then f ω else g ω) ∂M) =
    set_lebesgue_integral M S f + set_lebesgue_integral M (space M - S) g"
proof -
  let ?h = "λω. indicat_real S ω * f ω + indicat_real (space M - S) ω * g ω"
  have eq_ae: "AE ω in M. (if ω ∈ S then f ω else g ω) = ?h ω"
    by (rule AE_I2) (auto simp: indicator_def)
  have int_Sf: "integrable M (λω. indicat_real S ω * f ω)"
    using integrable_mult_indicator[OF S_meas int_f]
    by (simp add: scaleR_conv_of_real)
  have int_Sg: "integrable M (λω. indicat_real (space M - S) ω * g ω)"
    using integrable_mult_indicator[OF _ int_g] by (simp add: S_meas sets.Diff)
  have meas_if: "(λω. if ω ∈ S then f ω else g ω) ∈ borel_measurable M"
    by (intro measurable_If_set) (use int_f int_g S_meas in auto)
  have meas_h: "?h ∈ borel_measurable M"
    using int_Sf int_Sg by (intro borel_measurable_add) auto
  have "(∫ω. (if ω ∈ S then f ω else g ω) ∂M) = (∫ω. ?h ω ∂M)"
    by (rule integral_cong_AE[OF meas_if meas_h eq_ae])
  also have "… = (∫ω. indicat_real S ω * f ω ∂M) + (∫ω. indicat_real (space M - S) ω * g ω ∂M)"
    by (rule Bochner_Integration.integral_add[OF int_Sf int_Sg])
  also have "… = set_lebesgue_integral M S f + set_lebesgue_integral M (space M - S) g"
    unfolding set_lebesgue_integral_def by (simp add: scaleR_conv_of_real)
  finally show ?thesis .
qed

end

end