Theory Stochastic_Processes

(* Title:      Kolmgorov_Chentsov/Stochastic_Processes.thy
   Author:     Christian Pardillo Laursen, University of York
*)

section "Stochastic processes"

theory Stochastic_Processes
  imports Kolmogorov_Chentsov_Extras Dyadic_Interval
begin

text ‹ A stochastic process is an indexed collection of random variables. For compatibility with 
  \texttt{product\_prob\_space} we don't enforce conditions on the index set $I$ in the assumptions. ›

locale stochastic_process = prob_space +
  fixes M' :: "'b measure"
    and I :: "'t set"
    and X :: "'t ⇒ 'a ⇒ 'b"
  assumes random_process[measurable]: "⋀i. random_variable M' (X i)"

sublocale stochastic_process ⊆ product: product_prob_space "(λt. distr M M' (X t))"
  using prob_space_distr random_process by (blast intro: product_prob_spaceI)

lemma (in prob_space) stochastic_processI:
  assumes "⋀i. random_variable M' (X i)"
  shows "stochastic_process M M' X"
  by (simp add: assms prob_space_axioms stochastic_process_axioms.intro stochastic_process_def)

typedef ('t, 'a, 'b) stochastic_process =
  "{(M :: 'a measure, M' :: 'b measure, I :: 't set, X :: 't ⇒ 'a ⇒ 'b).
   stochastic_process M M' X}"
proof
  show "(return (sigma UNIV {{}, UNIV}) x, sigma UNIV UNIV, UNIV, λ_ _. c) ∈
       {(M, M', I, X). stochastic_process M M' X}" for x :: 'a and c :: 'b
    by (simp add: prob_space_return prob_space.stochastic_processI)
qed

setup_lifting type_definition_stochastic_process

lift_definition proc_source :: "('t,'a,'b) stochastic_process ⇒ 'a measure"
  is "fst" .

interpretation proc_source: prob_space "proc_source X"
  by (induction, simp add: proc_source_def Abs_stochastic_process_inverse case_prod_beta' stochastic_process_def)

lift_definition proc_target :: "('t,'a,'b) stochastic_process ⇒ 'b measure"
  is "fst ∘ snd" .

lift_definition proc_index :: "('t,'a,'b) stochastic_process ⇒ 't set"
  is "fst ∘ snd ∘ snd" .

lift_definition process :: "('t,'a,'b) stochastic_process ⇒ 't ⇒ 'a ⇒ 'b"
  is "snd ∘ snd ∘ snd" .

declare [[coercion process]]

lemma stochastic_process_construct [simp]: "stochastic_process (proc_source X) (proc_target X) (process X)"
  by (transfer, force)

interpretation stochastic_process "proc_source X" "proc_target X" "proc_index X" "process X"
  by simp

lemma stochastic_process_measurable [measurable]: "process X t ∈ (proc_source X) →⇩_M (proc_target X)"
  by (meson random_process)
text ‹ Here we construct a process on a given index set. For this we need to produce measurable
  functions for indices outside the index set; we use the constant function, but it needs to point at
  an element of the target set to be measurable. ›

context prob_space
begin

lift_definition process_of :: "'b measure ⇒ 't set ⇒ ('t ⇒ 'a ⇒ 'b) ⇒ 'b ⇒ ('t,'a,'b) stochastic_process"
  is "λ M' I X ω. if (∀t ∈ I. X t ∈ M →⇩_M M') ∧ ω ∈ space M'
  then (M, M', I, (λt. if t ∈ I then X t else (λ_. ω)))
  else (return (sigma UNIV {{}, UNIV}) (SOME x. True), sigma UNIV UNIV, I, λ_ _. ω)"
  by (simp add: stochastic_processI prob_space_return prob_space.stochastic_processI)

lemma index_process_of[simp]: "proc_index (process_of M' I X ω) = I"
  by (transfer, auto)

lemma
  assumes "∀t ∈ I. X t ∈ M →⇩_M M'" "ω ∈ space M'"
  shows
    source_process_of[simp]: "proc_source (process_of M' I X ω) = M" and
    target_process_of[simp]: "proc_target (process_of M' I X ω) = M'" and
    process_process_of[simp]: "process (process_of M' I X ω) = (λt. if t ∈ I then X t else (λ_. ω))"
  using assms by (transfer, auto)+

lemma process_of_apply:
  assumes "∀t ∈ I. X t ∈ M →⇩_M M'" "ω ∈ space M'" "t ∈ I"
  shows "process (process_of M' I X ω) t = X t"
  using assms by (meson process_process_of)
end

text ‹ We define the finite-dimensional distributions of our process. ›

lift_definition distributions :: "('t, 'a, 'b) stochastic_process ⇒ 't set ⇒ ('t ⇒ 'b) measure"
  is "λ(M, M', _, X) T. (Π⇩_M t∈T. distr M M' (X t))" .

lemma distributions_altdef: "distributions X T = (Π⇩_M t∈T. distr (proc_source X) (proc_target X) (X t))"
  by (transfer, auto)

lemma prob_space_distributions: "prob_space (distributions X J)"
  unfolding distributions_altdef
  by (simp add: prob_space_PiM proc_source.prob_space_distr random_process)

lemma sets_distributions: "sets (distributions X J) = sets (PiM J (λ_. (proc_target X)))"
  by (transfer, auto cong: sets_PiM_cong)

lemma space_distributions: "space (distributions X J) = (Π⇩_E i∈J. space (proc_target X))"
  by (transfer, auto simp add: space_PiM)

lemma emeasure_distributions:
  assumes "finite J" "⋀j. j∈J ⟹ A j ∈ sets (proc_target X)"
  shows "emeasure (distributions X J) (Pi⇩_E J A) = (∏j∈J. emeasure (distr (proc_source X) (proc_target X) (X j)) (A j))"
  by (simp add: assms(1) assms(2) distributions_altdef product.emeasure_PiM)

interpretation projective_family "(proc_index X)" "distributions X" "(λ_. proc_target X)"
proof (intro projective_family.intro)
  fix J and H
  let ?I = "proc_index X"
    and ?M = "proc_source X"
    and ?M' = "proc_target X"
  assume *: "J ⊆ H" "finite H" "H ⊆ ?I"
  then have "J ⊆ ?I"
    by simp
  show "distributions X J = distr (distributions X H) (Pi⇩_M J (λ_. ?M')) (λf. restrict f J)"
  proof (rule measure_eqI)
    show "sets (distributions X J) = sets (distr (distributions X H) (Pi⇩_M J (λ_. ?M')) (λf. restrict f J))"
      by (simp add: sets_distributions)
    fix S assume "S ∈ sets (distributions X J)"
    then have in_sets: "S ∈ sets (PiM J (λ_. ?M'))"
      by (simp add: sets_distributions)
    have prod_emb_distr: "(prod_emb H (λ_. ?M') J S) = (prod_emb H (λt. distr ?M ?M' (X t)) J S)"
      by (simp add: prod_emb_def)
    have "emeasure (distr (distributions X H) (Pi⇩_M J (λ_. ?M')) (λf. restrict f J)) S =
          emeasure (distributions X H) (prod_emb H (λ_. ?M') J S)"
      apply (rule emeasure_distr_restrict)
      by (simp_all add: "*" sets_distributions in_sets)
    also have "... = emeasure (distributions X J) S"
      unfolding distributions_altdef
      using *(1,2) in_sets prod_emb_distr by force
    finally show "emeasure (distributions X J) S 
                = emeasure (distr (distributions X H) (Pi⇩_M J (λ_. ?M')) (λf. restrict f J)) S"
      by argo
  qed
qed (rule prob_space_distributions)

locale polish_stochastic = stochastic_process M "borel :: 'b::polish_space measure" I X
  for M and I and X

(*
sublocale polish_stochastic ⊆ polish_projective I distributions
  by (simp add: polish_projective.intro projective_family_axioms) *)

lemma distributed_cong_random_variable:
  assumes "M = K" "N = L" "AE x in M. X x = Y x" "X ∈ M →⇩_M N" "Y ∈ K →⇩_M L" "f ∈ borel_measurable N"
  shows "distributed M N X f ⟷ distributed K L Y f"
  using assms by (auto simp add: distributed_def distr_cong_AE)

text ‹ For all sorted lists of indices, the increments specified by this list are independent ›

lift_definition indep_increments :: "('t :: linorder, 'a, 'b :: minus) stochastic_process ⇒ bool" is
  "λ(M, M', I, X).
  (∀l. set l ⊆ I ∧ sorted l ∧ length l ≥ 2 ⟶
     prob_space.indep_vars M (λ_. M') (λk v. X (l!k) v - X (l!(k-1)) v) {1..<length l})" .

lemma indep_incrementsE:
  assumes "indep_increments X"
    and "set l ⊆ proc_index X ∧ sorted l ∧ length l ≥ 2"
  shows "prob_space.indep_vars (proc_source X) (λ_. proc_target X)
         (λk v. X (l!k) v - X (l!(k-1)) v) {1..<length l}"
  using assms by (transfer, auto)

lemma indep_incrementsI:
  assumes "⋀l. set l ⊆ proc_index X ⟹ sorted l ⟹ length l ≥ 2 ⟹
   prob_space.indep_vars (proc_source X) (λ_. proc_target X) (λk v. X (l!k) v - X (l!(k-1)) v) {1..<length l}"
  shows "indep_increments X"
  using assms by (transfer, auto)

lemma indep_increments_indep_var:
  assumes "indep_increments X" "h ∈ proc_index X" "j ∈ proc_index X" "k ∈ proc_index X" "h ≤ j" "j ≤ k"
  shows "prob_space.indep_var (proc_source X) (proc_target X) (λv. X j v - X h v) (proc_target X) (λv. X k v - X j v)"
proof -
  let ?l = "[h,j,k]"
  have "set ?l ⊆ proc_index X ∧ sorted ?l ∧ 2 ≤ length ?l"
    using assms by auto
  then have "prob_space.indep_vars (proc_source X) (λ_. proc_target X) (λk v. X (?l!k) v - X (?l!(k-1)) v) {1..<length ?l}"
    by (rule indep_incrementsE[OF assms(1)])
  then show ?thesis
    using proc_source.indep_vars_indep_var by fastforce
qed

definition "stationary_increments X ⟷ (∀t1 t2 k. t1 > 0 ∧ t2 > 0 ∧ k > 0 ⟶ 
     distr (proc_source X) (proc_target X) (λv. X (t1 + k) v - X t1 v) =
     distr (proc_source X) (proc_target X) (λv. X (t2 + k) v - X t2 v))"

text ‹ Processes on the same source measure space, with the same index space, but not necessarily the same
  target measure since we only care about the measurable target space, not the measure ›

lift_definition compatible :: "('t,'a,'b) stochastic_process ⇒ ('t,'a,'b) stochastic_process ⇒ bool"
  is "λ(Mx, M'x, Ix, X) (My, M'y, Iy, _). Mx = My ∧ sets M'x = sets M'y ∧ Ix = Iy" .

lemma compatibleI:
  assumes "proc_source X = proc_source Y" "sets (proc_target X) = sets (proc_target Y)"
    "proc_index X = proc_index Y"
  shows "compatible X Y"
  using assms by (transfer, auto)

lemma
  assumes "compatible X Y"
  shows
    compatible_source [dest]: "proc_source X = proc_source Y" and
    compatible_target [dest]: "sets (proc_target X) = sets (proc_target Y)" and
    compatible_index [dest]: "proc_index X = proc_index Y"
  using assms by (transfer, auto)+

lemma compatible_refl [simp]: "compatible X X"
  by (transfer, auto)

lemma compatible_sym: "compatible X Y ⟹ compatible Y X"
  by (transfer, auto)

lemma compatible_trans:
  assumes "compatible X Y" "compatible Y Z"
  shows "compatible X Z"
  using assms by (transfer, auto)

lemma (in prob_space) compatible_process_of:
  assumes measurable: "∀t ∈ I. X t ∈ M →⇩_M M'" "∀t ∈ I. Y t ∈ M →⇩_M M'" 
    and "a ∈ space M'" "b ∈ space M'"
  shows "compatible (process_of M' I X a) (process_of M' I Y b)"
  using assms by (transfer, auto)

definition modification :: "('t,'a,'b) stochastic_process ⇒ ('t,'a,'b) stochastic_process ⇒ bool" where
  "modification X Y ⟷ compatible X Y ∧ (∀t ∈ proc_index X. AE x in proc_source X. X t x = Y t x)"

lemma modificationI [intro]:
  assumes "compatible X Y" "⋀t. t ∈ proc_index X ⟹ AE x in proc_source X. X t x = Y t x"
  shows "modification X Y"
  unfolding modification_def using assms by blast

lemma modificationD [dest]:
  assumes "modification X Y"
  shows "compatible X Y"
    and "⋀t. t ∈ proc_index X ⟹ AE x in proc_source X. X t x = Y t x"
  using assms unfolding modification_def by blast+

lemma modification_null_set:
  assumes "modification X Y" "t ∈ proc_index X"
  obtains N where "{x ∈ space (proc_source X). X t x ≠ Y t x} ⊆ N" "N ∈ null_sets (proc_source X)"
proof -
  from assms have "AE x in proc_source X. X t x = Y t x"
    by (rule modificationD(2))
  then have "∃N∈null_sets (proc_source X). {x ∈ space (proc_source X). X t x ≠ Y t x} ⊆ N"
    by (simp add: eventually_ae_filter)
  then show ?thesis
    using that by blast
qed

lemma modification_refl [simp]: "modification X X"
  by (simp add: modificationI)

lemma modification_sym: "modification X Y ⟹ modification Y X"
proof (rule modificationI)
  assume *: "modification X Y"
  then show compat: "compatible Y X"
    using compatible_sym modificationD(1) by blast
  fix t assume "t ∈ proc_index Y"
  then have "t ∈ proc_index X"
    using compatible_index[OF compat] by blast
  have "AE x in proc_source Y. X t x = Y t x"
    using modificationD(2)[OF * ‹t ∈ proc_index X›]
      compatible_source[OF compat] by argo
  then show "AE x in proc_source Y. Y t x = X t x"
    by force
qed

lemma modification_trans:
  assumes "modification X Y" "modification Y Z"
  shows "modification X Z"
proof (intro modificationI)
  show "compatible X Z"
    using compatible_trans modificationD(1) assms by blast
  fix t assume t: "t ∈ proc_index X"
  have XY: "AE x in proc_source X. process X t x = process Y t x"
    by (fact modificationD(2)[OF assms(1) t])
  have "t ∈ proc_index Y" "proc_source X = proc_source Y"
    using compatible_index compatible_source assms(1) modificationD(1) t by blast+
  then have "AE x in proc_source X. process Y t x = process Z t x"
    using modificationD(2)[OF assms(2)] by presburger
  then show "AE x in proc_source X. process X t x = process Z t x"
    using XY by fastforce
qed

lemma modification_imp_identical_distributions:
  assumes modification: "modification X Y"
    and index: "T ⊆ proc_index X"
  shows "distributions X T = distributions Y T"
proof -
  have "proc_source X = proc_source Y"
    using modification by blast
  moreover have "sets (proc_target X) = sets (proc_target Y)"
    using modification by blast
  ultimately have "distr (proc_source X) (proc_target X) (X x) =
         distr (proc_source Y) (proc_target Y) (Y x)"
    if "x ∈ T" for x
    apply (rule distr_cong_AE)
      apply (metis assms modificationD(2) subset_eq that)
     apply simp_all
    done
  then show ?thesis
    by (auto simp: distributions_altdef cong: PiM_cong)
qed

definition indistinguishable :: "('t,'a,'b) stochastic_process ⇒ ('t,'a,'b) stochastic_process ⇒ bool" where
  "indistinguishable X Y ⟷ compatible X Y ∧
 (∃N ∈ null_sets (proc_source X). ∀t ∈ proc_index X. {x ∈ space (proc_source X). X t x ≠ Y t x} ⊆ N)"

lemma indistinguishableI:
  assumes "compatible X Y" 
    and "∃N ∈ null_sets (proc_source X). (∀t ∈ proc_index X. {x ∈ space (proc_source X). X t x ≠ Y t x} ⊆ N)"
  shows "indistinguishable X Y"
  unfolding indistinguishable_def using assms by blast

lemma indistinguishable_null_set:
  assumes "indistinguishable X Y"
  obtains N where 
    "N ∈ null_sets (proc_source X)"
    "⋀t. t ∈ proc_index X ⟹ {x ∈ space (proc_source X). X t x ≠ Y t x} ⊆ N"
  using assms unfolding indistinguishable_def by force

lemma indistinguishableD:
  assumes "indistinguishable X Y"
  shows "compatible X Y"
    and "∃N ∈ null_sets (proc_source X). (∀t ∈ proc_index X. {x ∈ space (proc_source X). X t x ≠ Y t x} ⊆ N)"
  using assms unfolding indistinguishable_def by blast+

lemma indistinguishable_eq_AE:
  assumes "indistinguishable X Y"
  shows "AE x in proc_source X. ∀t ∈ proc_index X. X t x = Y t x"
  using assms[THEN indistinguishableD(2)] by (auto simp add: eventually_ae_filter)

lemma indistinguishable_null_ex:
  assumes "indistinguishable X Y"
  shows "∃N ∈ null_sets (proc_source X). {x ∈ space (proc_source X).∃t ∈ proc_index X. X t x ≠ Y t x} ⊆ N"
  using indistinguishableD(2)[OF assms] by blast

lemma indistinguishable_refl [simp]: "indistinguishable X X"
  by (auto intro: indistinguishableI)

lemma indistinguishable_sym: "indistinguishable X Y ⟹ indistinguishable Y X"
  unfolding indistinguishable_def apply (simp add: compatible_sym)
  by (smt (verit, ccfv_SIG) Collect_cong compatible_index compatible_source indistinguishable_def)

lemma indistinguishable_trans:
  assumes "indistinguishable X Y" "indistinguishable Y Z" 
  shows "indistinguishable X Z"
proof (intro indistinguishableI)
  show "compatible X Z"
    using assms indistinguishableD(1) compatible_trans by blast
  have eq: "proc_index X = proc_index Y" "proc_source X = proc_source Y"
    using compatible_index compatible_source indistinguishableD(1)[OF assms(1)] by blast+
  have "AE x in proc_source X. ∀t ∈ proc_index X. X t x = Y t x"
    by (fact indistinguishable_eq_AE[OF assms(1)])
  moreover have "AE x in proc_source X. ∀t ∈ proc_index X. Y t x = Z t x"
    apply (subst eq)+
    by (fact indistinguishable_eq_AE[OF assms(2)])
  ultimately have "AE x in proc_source X. ∀t ∈ proc_index X. X t x = Z t x"
    using assms by fastforce
  then obtain N where "N ∈ null_sets (proc_source X)" 
    "{x ∈ space (proc_source X).∃t∈proc_index X. process X t x ≠ process Z t x} ⊆ N"
    using eventually_ae_filter by (smt (verit) Collect_cong eventually_ae_filter)
  then show "∃N∈null_sets (proc_source X). ∀t∈proc_index X. {x ∈ space (proc_source X). process X t x ≠ process Z t x} ⊆ N"
    by blast
qed

lemma indistinguishable_modification: "indistinguishable X Y ⟹ modification X Y"
  apply (intro modificationI)
   apply (erule indistinguishableD(1))
  apply (drule indistinguishableD(2))
  using eventually_ae_filter by blast

text ‹ Klenke 21.5(i) ›

lemma modification_countable:
  assumes "modification X Y" "countable (proc_index X)"
  shows "indistinguishable X Y"
proof (rule indistinguishableI)
  show "compatible X Y"
    using assms(1) modification_def by auto
  let ?N = "(λt. {x ∈ space (proc_source X). X t x ≠ Y t x})"
  from assms(1) have "∀t ∈ proc_index X. AE x in proc_source X. X t x = Y t x"
    unfolding modification_def by argo
  then have "⋀t. t ∈ proc_index X ⟹ ∃N ∈ null_sets (proc_source X). ?N t ⊆ N"
    by (subst eventually_ae_filter[symmetric], blast)
  then have "∃N. ∀t ∈ proc_index X. N t ∈ null_sets (proc_source X) ∧ ?N t ⊆ N t"
    by meson
  then obtain N where N: "∀t ∈ proc_index X. (N t) ∈ null_sets (proc_source X) ∧ ?N t ⊆ N t"
    by blast
  then have null: "(⋃t ∈ proc_index X. N t) ∈ null_sets (proc_source X)"
    by (simp add: null_sets_UN' assms(2))
  moreover have "∀t∈proc_index X. ?N t ⊆ (⋃t ∈ proc_index X. N t)"
    using N by blast 
  ultimately show "∃N∈ null_sets (proc_source X). (∀t∈proc_index X. ?N t ⊆ N)"
    by blast
qed

text ‹ Klenke 21.5(ii). The textbook statement is more general - we reduce right continuity to regular continuity ›

lemma modification_continuous_indistinguishable:
  fixes X :: "(real, 'a, 'b :: metric_space) stochastic_process"
  assumes modification: "modification X Y"
    and interval: "∃T > 0. proc_index X = {0..T}"
    and rc: "AE ω in proc_source X. continuous_on (proc_index X) (λt. X t ω)"
    (is "AE ω in proc_source X. ?cont_X ω")
    "AE ω in proc_source Y. continuous_on (proc_index Y) (λt. Y t ω)"
    (is "AE ω in proc_source Y. ?cont_Y ω")
  shows "indistinguishable X Y"
proof (rule indistinguishableI)
  show "compatible X Y"
    using modification modification_def by blast
  obtain T where T: "proc_index X = {0..T}" "T > 0"
    using interval by blast
  define N where "N ≡ λt. {x ∈ space (proc_source X). X t x ≠ Y t x}"
  have 1: "∀t ∈ proc_index X. ∃S. N t ⊆ S ∧ S ∈ null_sets (proc_source X)"
    using modificationD(2)[OF modification] by (auto simp add: N_def eventually_ae_filter)
  text ‹ $S$ is a null set such that $X_t(x) \neq Y_t(x) \Longrightarrow x \in S_t$ ›
  obtain S where S: "∀t ∈ proc_index X. N t ⊆ S t ∧ S t ∈ null_sets (proc_source X)"
    using bchoice[OF 1] by blast
  have eq: "proc_source X = proc_source Y" "proc_index X = proc_index Y"
    using ‹compatible X Y› compatible_source compatible_index by blast+
  have "AE p in proc_source X. ?cont_X p ∧ ?cont_Y p"
    apply (rule AE_conjI)
    using eq rc by argo+
  text ‹ $R$ is a set of measure 1 such that if $x \in R$ then the paths at $x$ are continuous for $X$ and $Y$ ›
  then obtain R where R: "R ⊆ {p ∈ space (proc_source X). ?cont_X p ∧ ?cont_Y p}"
    "R ∈ sets (proc_source X)" "measure (proc_source X) R = 1"
    using proc_source.AE_E_prob by blast
  text ‹ We use an interval of dyadic rationals because we need to produce a countable dense set
  for $\{0..T\}$, which we have by @{thm dyadic_interval_dense}. ›
  let ?I = "dyadic_interval 0 T"
  let ?N' = "⋃n ∈ ?I. N n"
  have N_subset: "⋀t. t ∈ proc_index X ⟹ N t ∩ R ⊆ ?N'"
  proof
    fix t assume "t ∈ proc_index X"
    fix p assume *: "p ∈ N t ∩ R"
    then obtain ε where ε: "0 < ε" "ε = dist (X t p) (Y t p)"
      by (simp add: N_def)
    have cont_p: "continuous_on {0..T} (λt. Y t p)" "continuous_on {0..T} (λt. X t p)"
      using R *(1) T(1)[symmetric] eq(2) by auto
    then have continuous_dist: "continuous_on {0..T} (λt. dist (X t p) (Y t p))"
      using continuous_on_dist by fast
    {
      assume "∀r∈ ?I. X r p = Y r p"
      then have dist_0: "⋀r. r ∈ ?I ⟹ dist (X r p) (Y r p) = 0"
        by auto
      have "dist (X t p) (Y t p) = 0"
      proof -
        have dist_tendsto_0: "((λt. dist (X t p) (Y t p)) ⤏ 0)(at t within ?I)"
          using dist_0 continuous_dist
          by (smt (verit, best) Lim_transform_within ε tendsto_const)
        have XY: "((λt. X t p) ⤏ X t p)(at t within ?I)" "((λt. Y t p) ⤏ Y t p)(at t within ?I)"
          by (metis cont_p T(1) ‹t ∈ proc_index X› continuous_on_def tendsto_within_subset dyadic_interval_subset_interval)+
        show ?thesis
          apply (rule tendsto_unique[of "at t within ?I"])
            apply (simp add: trivial_limit_within)
            apply (metis T(1) T(2) ‹t ∈ proc_index X› dyadic_interval_dense islimpt_Icc limpt_of_closure)
          using tendsto_dist[OF XY] dist_tendsto_0 
          by simp_all
      qed
      then have False
        using ε by force
    }
    then have "∃r∈dyadic_interval 0 T. p ∈ N r"
      unfolding N_def using * R(2) sets.sets_into_space by auto
    then show "p ∈ ⋃ (N ` ?I)"
      by simp
  qed
  have null: "(space (proc_source X) - R) ∪ (⋃r ∈ ?I. S r) ∈ null_sets (proc_source X)"
    apply (rule null_sets.Un)
     apply (smt (verit) R(2,3) AE_iff_null_sets proc_source.prob_compl proc_source.prob_eq_0 sets.Diff sets.top)
    by (metis (no_types, lifting) S T(1) dyadic_interval_countable dyadic_interval_subset_interval in_mono null_sets_UN')
  have "(⋃r ∈ proc_index X. N r) ⊆ (space (proc_source X) - R) ∪ (⋃r ∈ proc_index X. N r)"
    by blast
  also have "... ⊆ (space (proc_source X) - R) ∪ (⋃r ∈ ?I. N r)"
    using N_subset N_def by blast
  also have "... ⊆ (space (proc_source X) - R) ∪ (⋃r ∈ ?I. S r)"
    by (smt (verit, ccfv_threshold)S T(1) UN_iff Un_iff dyadic_interval_subset_interval in_mono subsetI)
  finally show "∃N∈null_sets (proc_source X). ∀t∈proc_index X. {x ∈ space (proc_source X). process X t x ≠ process Y t x} ⊆ N"
    by (smt (verit) N_def null S SUP_le_iff order_trans)
qed

lift_definition restrict_index :: "('t, 'a, 'b) stochastic_process ⇒ 't set ⇒ ('t, 'a, 'b) stochastic_process"
  is "λ(M, M', I, X) T. (M, M', T, X)" by fast

lemma
  shows
    restrict_index_source[simp]: "proc_source (restrict_index X T) = proc_source X" and
    restrict_index_target[simp]: "proc_target (restrict_index X T) = proc_target X" and
    restrict_index_index[simp]:  "proc_index (restrict_index X T) = T" and
    restrict_index_process[simp]: "process (restrict_index X T) = process X"
  by (transfer, force)+

lemma restrict_index_override[simp]: "restrict_index (restrict_index X T) S = restrict_index X S"
  by (transfer, auto)

lemma compatible_restrict_index:
  assumes "compatible X Y"
  shows "compatible (restrict_index X S) (restrict_index Y S)"
  using assms unfolding compatible_def by (transfer, auto)

lemma modification_restrict_index:
  assumes "modification X Y" "S ⊆ proc_index X"
  shows "modification (restrict_index X S) (restrict_index Y S)"
  using assms unfolding modification_def
  apply (simp add: compatible_restrict_index)
  apply (metis restrict_index_source subsetD)
  done

lemma indistinguishable_restrict_index:
  assumes "indistinguishable X Y" "S ⊆ proc_index X"
  shows "indistinguishable (restrict_index X S) (restrict_index Y S)"
  using assms unfolding indistinguishable_def by (auto simp: compatible_restrict_index)

lemma AE_eq_minus [intro]:
  fixes a :: "'a ⇒ ('b :: real_normed_vector)"
  assumes "AE x in M. a x = b x" "AE x in M. c x = d x"
  shows "AE x in M. a x - c x = b x - d x"
  using assms by fastforce

lemma modification_indep_increments:
  fixes X Y :: "('a :: linorder, 'b, 'c :: {second_countable_topology, real_normed_vector}) stochastic_process"
  assumes "modification X Y" "sets (proc_target Y) = sets borel"
  shows "indep_increments X ⟹ indep_increments Y"
proof (intro indep_incrementsI, subst proc_source.indep_vars_iff_distr_eq_PiM, goal_cases)
  case (1 l)
  then show ?case by simp
next
  case (2 l i)
  then show ?case
    using assms apply measurable
    using modificationD(1)[OF assms(1), THEN compatible_source] assms(2)
    by (metis measurable_cong_sets random_process)+
next
  case (3 l)
  have target_X [measurable]: "sets (proc_target X) = sets borel"
    using assms by auto
  then have measurable_target: "f ∈ M →⇩_M proc_target X = (f ∈ borel_measurable M)" for f and M :: "'b measure"
    using measurable_cong_sets by blast
  have "AE ω in proc_source X. X (l ! i) ω = Y (l ! i) ω"
    if "i ∈ {0..<length l}" for i
    apply (rule assms(1)[THEN modificationD(2)])
    by (metis 3(2) that assms(1) atLeastLessThan_iff basic_trans_rules(31) 
        compatible_index modificationD(1) nth_mem)
  then have AE_eq: "AE ω in proc_source X. X (l!i) ω - X (l!(i-1)) ω = Y (l!i) ω - Y (l!(i-1)) ω"
    if "i ∈ {1..<length l}" for i
    using AE_eq_minus that by auto
  have AE_eq': "AE x in proc_source X. (λi∈{1..<length l}. X (l ! i) x - X (l ! (i - 1)) x) = 
        (λi∈{1..<length l}. Y (l ! i) x - Y (l ! (i - 1)) x)"
  proof (rule AE_mp)
    show "AE ω in proc_source X. ∀i ∈{1..<length l}. X (l!i) ω - X (l!(i-1)) ω = Y (l!i) ω - Y (l!(i-1)) ω"
    proof -
      {
        fix i assume *: "i ∈ {1..<length l}"
        obtain N where 
          "{ω ∈ space (proc_source X). X (l!i) ω - X (l!(i-1)) ω ≠ Y (l!i) ω - Y (l!(i-1)) ω} ⊆ N"
          "N ∈ proc_source X" "emeasure (proc_source X) N = 0"
          using AE_eq[OF *, THEN AE_E] .
        then have "∃N ∈ null_sets (proc_source X).
         {ω ∈ space (proc_source X). X (l!i) ω - X (l!(i-1)) ω ≠ Y (l!i) ω - Y (l!(i-1)) ω} ⊆ N"
          by blast
      } then obtain N where N: "N i ∈ null_sets (proc_source X)"
        "{ω ∈ space (proc_source X). X (l!i) ω - X (l!(i-1)) ω ≠ Y (l!i) ω - Y (l!(i-1)) ω} ⊆ N i"
      if "i ∈ {1..< length l}" for i
        by (metis (lifting) ext)
      have "{ω ∈ space (proc_source X). ¬ (∀i∈{1..<length l}. X (l ! i) ω - X (l ! (i - 1)) ω = Y (l ! i) ω - Y (l ! (i - 1)) ω)} ⊆ (⋃ i ∈ {1..< length l}. N i)"
        using N by blast
      moreover have "(⋃i ∈ {1..< length l}. N i) ∈ null_sets (proc_source X)"
        apply (rule null_sets.finite_UN)
        using 3 N by simp_all
      ultimately show ?thesis
        by (blast intro: AE_I)
    qed
    show "AE x in proc_source
             X. (∀i∈{1..<length l}. process X (l ! i) x - process X (l ! (i - 1)) x = process Y (l ! i) x - process Y (l ! (i - 1)) x) ⟶
                (λi∈{1..<length l}. process X (l ! i) x - process X (l ! (i - 1)) x) = (λi∈{1..<length l}. process Y (l ! i) x - process Y (l ! (i - 1)) x)"
      by (rule AE_I2, auto)
  qed                                            
  have "distr (proc_source Y) (Pi⇩_M {1..<length l} (λi. proc_target Y))
                (λx. λi∈{1..<length l}. Y (l ! i) x - Y (l ! (i - 1)) x) =
            distr (proc_source X) (Pi⇩_M {1..<length l} (λi. proc_target X))
              (λx. λi∈{1..<length l}. X (l ! i) x - X (l ! (i - 1)) x)"
    apply (rule sym)
    apply (rule distr_cong_AE)
    using assms(1) apply blast
       apply (metis assms(2) sets_PiM_cong target_X)
      apply (fact AE_eq')
     apply simp
     apply (rule measurable_restrict)
     apply (simp add: measurable_target)
    subgoal by measurable (meson measurable_target random_process)+
    apply (rule measurable_restrict)
    by (metis (full_types) assms(2) borel_measurable_diff measurable_cong_sets stochastic_process_measurable)
  also have "... = Pi⇩_M {1..<length l} (λi. distr (proc_source X) (proc_target X) (λv. X (l ! i) v - X (l ! (i - 1)) v))"
    apply (subst proc_source.indep_vars_iff_distr_eq_PiM[symmetric])
    subgoal using 3 by simp
     apply simp
     apply (metis (full_types) borel_measurable_diff measurable_cong_sets stochastic_process_measurable target_X)
    apply (rule indep_incrementsE)
     apply (fact 3(1))
    using 3(2-) assms(1) by blast
  also have "... = Pi⇩_M {1..<length l} (λi. distr (proc_source Y) (proc_target Y) (λv. Y (l ! i) v - Y (l ! (i - 1)) v))"
    apply (safe intro!: PiM_cong)
    apply (rule distr_cong_AE)
    subgoal using assms(1) by blast
    subgoal using assms(1) by blast
    subgoal using AE_eq by presburger
    subgoal by (metis (mono_tags) borel_measurable_diff measurable_target random_process)
    by (metis (full_types) assms(2) borel_measurable_diff measurable_cong_sets random_process)
  finally show ?case .
qed

end