Theory Filtration

(*  Title:      Filtration.thy
    Author:     Mnacho Echenim, Univ. Grenoble Alpes
*)

section ‹Filtrations›

text ‹This theory introduces basic notions about filtrations, which permit to define adaptable processes
and predictable processes in the case where the filtration is indexed by natural numbers.›

theory Filtration imports "HOL-Probability.Probability"
begin
subsection ‹Basic definitions›
class linorder_bot = linorder + bot
instantiation nat::linorder_bot
begin
instance proof qed
end


definition filtration :: "'a measure ⇒ ('i::linorder_bot ⇒ 'a measure) ⇒ bool" where
  "filtration M F ⟷
    (∀t. subalgebra M (F t))  ∧
    (∀ s t. s ≤ t ⟶ subalgebra (F t) (F s))"

lemma filtrationI:
  assumes "∀t. subalgebra M (F t)"
  and "∀s t. s ≤ t ⟶ subalgebra (F t) (F s)"
shows "filtration M F" unfolding filtration_def using assms by simp

lemma filtrationE1:
  assumes "filtration M F"
  shows "subalgebra M (F t)" using assms unfolding filtration_def by simp

lemma filtrationE2:
  assumes "filtration M F"
  shows "s≤ t ⟹ subalgebra (F t) (F s)" using assms unfolding filtration_def by simp

locale filtrated_prob_space = prob_space +
  fixes F
  assumes filtration: "filtration M F"

lemma (in filtrated_prob_space) filtration_space:
  assumes "s ≤ t"
  shows "space (F s) = space (F t)" by (metis filtration filtration_def subalgebra_def)

lemma (in filtrated_prob_space) filtration_measurable:
  assumes "f∈ measurable (F t) N"
shows "f∈ measurable M N" unfolding measurable_def
proof
  show "f ∈ space M → space N ∧ (∀y∈sets N. f -` y ∩ space M ∈ sets M)"
  proof (intro conjI ballI)
    have "space (F t) = space M" using assms filtration unfolding filtration_def subalgebra_def by auto
    thus "f∈ space M → space N" using assms unfolding measurable_def by simp
    fix y
    assume "y∈ sets N"
    hence "f -`y∩ space M ∈ sets (F t)" using assms unfolding measurable_def
      using ‹space (F t) = space M› by auto
    thus "f -`y∩ space M ∈ sets M"  using assms filtration unfolding filtration_def subalgebra_def by auto
  qed
qed


lemma (in filtrated_prob_space) increasing_measurable_info:
  assumes "f∈ measurable (F s) N"
  and "s ≤ t"
  shows "f∈ measurable (F t) N"
proof (rule measurableI)
  have inc: "sets (F s) ⊆ sets (F t)"
    using assms(2) filtration by (simp add: filtration_def subalgebra_def)
  have sp: "space (F s) = space (F t)" by (metis filtration filtration_def subalgebra_def)
  thus "⋀x. x ∈ space (F t) ⟹ f x ∈ space N" using assms by (simp add: measurable_space)
  show "⋀A. A ∈ sets N ⟹ f -` A ∩ space (F t) ∈ sets (F t)"
  proof -
    fix A
    assume "A∈ sets N"
    hence "f -` A ∩ space (F s) ∈ sets (F s)" using assms using measurable_sets by blast
    hence "f -` A ∩ space (F s) ∈ sets (F t)" using subsetD[of "F s" "F t"] inc by blast
    thus "f -` A ∩ space (F t) ∈ sets (F t)" using sp by simp
  qed
qed



definition disc_filtr :: "'a measure ⇒ (nat ⇒ 'a measure) ⇒ bool" where
  "disc_filtr M F ⟷
    (∀n. subalgebra M (F n))  ∧
    (∀ n m. n ≤ m ⟶ subalgebra (F m) (F n))"


locale disc_filtr_prob_space = prob_space +
  fixes F
  assumes discrete_filtration: "disc_filtr M F"

lemma (in disc_filtr_prob_space) subalgebra_filtration:
  assumes "subalgebra N M"
  and "filtration M F"
shows "filtration N F"
proof (rule filtrationI)
  show "∀s t. s ≤ t ⟶ subalgebra (F t) (F s)" using assms unfolding filtration_def by simp
  show "∀t. subalgebra N (F t)"
  proof
    fix t
    have "subalgebra M (F t)" using assms unfolding filtration_def by auto
    thus "subalgebra N (F t)" using assms by (metis subalgebra_def subsetCE subsetI)
  qed
qed



sublocale disc_filtr_prob_space ⊆  filtrated_prob_space
proof unfold_locales
  show "filtration M F"
    using  discrete_filtration by (simp add: filtration_def disc_filtr_def)
qed



subsection ‹Stochastic processes›

text  ‹Stochastic processes are collections of measurable functions. Those of a particular interest when
there is a filtration are the adapted stochastic processes.›

definition stoch_procs where
  "stoch_procs M N = {X. ∀t. (X t) ∈ measurable M N}"

subsubsection ‹Adapted stochastic processes›

definition adapt_stoch_proc where
  "(adapt_stoch_proc F X N) ⟷ (∀t. (X t) ∈ measurable (F t) N)"


abbreviation "borel_adapt_stoch_proc F X ≡ adapt_stoch_proc F X borel"

lemma (in filtrated_prob_space) adapted_is_dsp:
  assumes "adapt_stoch_proc F X N"
  shows "X ∈ stoch_procs M N"
  unfolding  stoch_procs_def
  by (intro CollectI, (meson adapt_stoch_proc_def assms filtration filtration_def measurable_from_subalg))


lemma (in filtrated_prob_space) adapt_stoch_proc_borel_measurable:
  assumes "adapt_stoch_proc F X N"
  shows "∀n. (X n) ∈ measurable M N"
proof
  fix n
  have "X n ∈ measurable (F n) N" using assms unfolding  adapt_stoch_proc_def by simp
  moreover have "subalgebra M (F n)" using filtration unfolding filtration_def by simp
  ultimately show "X n ∈ measurable M N" by (simp add:measurable_from_subalg)
qed

lemma (in filtrated_prob_space) borel_adapt_stoch_proc_borel_measurable:
  assumes "borel_adapt_stoch_proc F X"
  shows "∀n. (X n) ∈ borel_measurable M"
proof
  fix n
  have "X n ∈ borel_measurable (F n)" using assms unfolding  adapt_stoch_proc_def by simp
  moreover have "subalgebra M (F n)" using filtration unfolding filtration_def by simp
  ultimately show "X n ∈ borel_measurable M" by (simp add:measurable_from_subalg)
qed


lemma (in filtrated_prob_space) constant_process_borel_adapted:
  shows "borel_adapt_stoch_proc F (λ n w. c)"
unfolding  adapt_stoch_proc_def
proof
  fix t
  show "(λw. c) ∈ borel_measurable (F t)" using borel_measurable_const by blast
qed


lemma (in filtrated_prob_space) borel_adapt_stoch_proc_add:
  fixes X::"'b ⇒ 'a ⇒ ('c::{second_countable_topology, topological_monoid_add})"
  assumes "borel_adapt_stoch_proc F X"
  and "borel_adapt_stoch_proc F Y"
shows "borel_adapt_stoch_proc F (λt w. X t w + Y t w)" unfolding adapt_stoch_proc_def
proof
  fix t
  have "X t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  moreover have "Y t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  ultimately show "(λw. X t w + Y t w) ∈ borel_measurable (F t)" by simp
qed


lemma (in filtrated_prob_space) borel_adapt_stoch_proc_sum:
  fixes A::"'d ⇒ 'b ⇒ 'a ⇒ ('c::{second_countable_topology, topological_comm_monoid_add})"
  assumes "⋀i. i∈ S ⟹ borel_adapt_stoch_proc F (A i)"
shows "borel_adapt_stoch_proc F (λ t w. (∑ i∈ S. A i t w))" unfolding adapt_stoch_proc_def
proof
  fix t
  have "⋀i. i∈ S⟹ A i t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  thus "(λ w. (∑ i∈ S. A i t w)) ∈ borel_measurable (F t)" by (simp add:borel_measurable_sum)
qed

lemma (in filtrated_prob_space) borel_adapt_stoch_proc_times:
  fixes X::"'b ⇒ 'a ⇒ ('c::{second_countable_topology, real_normed_algebra})"
  assumes "borel_adapt_stoch_proc F X"
  and "borel_adapt_stoch_proc F Y"
shows "borel_adapt_stoch_proc F (λt w. X t w * Y t w)" unfolding adapt_stoch_proc_def
proof
  fix t
  have "X t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  moreover have "Y t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  ultimately show "(λw. X t w * Y t w) ∈ borel_measurable (F t)" by simp
qed

lemma (in filtrated_prob_space) borel_adapt_stoch_proc_prod:
  fixes A::"'d ⇒ 'b ⇒ 'a ⇒ ('c::{second_countable_topology, real_normed_field})"
  assumes "⋀i. i∈ S ⟹ borel_adapt_stoch_proc F (A i)"
shows "borel_adapt_stoch_proc F (λ t w. (∏ i∈ S. A i t w))" unfolding adapt_stoch_proc_def
proof
  fix t
  have "⋀i. i∈ S⟹ A i t ∈ borel_measurable (F t)" using assms unfolding adapt_stoch_proc_def by simp
  thus "(λ w. (∏ i∈ S. A i t w)) ∈ borel_measurable (F t)" by simp
qed


subsubsection ‹Predictable stochastic processes›

definition predict_stoch_proc where
  "(predict_stoch_proc F X N) ⟷ (X 0 ∈ measurable (F 0) N ∧ (∀n. (X (Suc n)) ∈ measurable (F n) N))"


abbreviation  "borel_predict_stoch_proc F X ≡ predict_stoch_proc F X borel"

lemma (in disc_filtr_prob_space) predict_imp_adapt:
  assumes "predict_stoch_proc F X N"
  shows "adapt_stoch_proc F X N" unfolding adapt_stoch_proc_def
proof
  fix n
  show "X n ∈ measurable (F n) N"
  proof (cases "n = 0")
    case True
    thus ?thesis using assms unfolding predict_stoch_proc_def by auto
  next
    case False
    thus ?thesis using assms unfolding predict_stoch_proc_def
      by (metis Suc_n_not_le_n increasing_measurable_info nat_le_linear not0_implies_Suc)
  qed
qed


lemma (in disc_filtr_prob_space) predictable_is_dsp:
  assumes "predict_stoch_proc F X N"
  shows "X ∈ stoch_procs M N"
unfolding  stoch_procs_def
proof
  show "∀n. random_variable N (X n)"
  proof
    fix n
    show "random_variable N (X n)"
    proof (cases "n=0")
      case True
      thus ?thesis using assms unfolding predict_stoch_proc_def
        using filtration filtration_def measurable_from_subalg by blast
    next
      case False
      thus ?thesis using assms unfolding predict_stoch_proc_def
        by (metis filtration filtration_def measurable_from_subalg not0_implies_Suc)
    qed
  qed
qed



lemma (in disc_filtr_prob_space) borel_predict_stoch_proc_borel_measurable:
  assumes "borel_predict_stoch_proc F X"
  shows "∀n. (X n) ∈ borel_measurable M" using assms predictable_is_dsp unfolding stoch_procs_def by auto



lemma (in disc_filtr_prob_space) constant_process_borel_predictable:
  shows "borel_predict_stoch_proc F (λ n w. c)"
unfolding  predict_stoch_proc_def
proof
  show "(λw. c) ∈ borel_measurable (F 0)" using borel_measurable_const by blast
next
  show "∀n. (λw. c) ∈ borel_measurable (F n)" using borel_measurable_const by blast
qed

lemma (in disc_filtr_prob_space) borel_predict_stoch_proc_add:
  fixes X::"nat ⇒ 'a ⇒ ('c::{second_countable_topology, topological_monoid_add})"
  assumes "borel_predict_stoch_proc F X"
  and "borel_predict_stoch_proc F Y"
shows "borel_predict_stoch_proc F (λt w. X t w + Y t w)" unfolding predict_stoch_proc_def
proof
  show "(λw. X 0 w + Y 0 w) ∈ borel_measurable (F 0)"
    using assms(1) assms(2) borel_measurable_add predict_stoch_proc_def by blast
next
  show "∀n. (λw. X (Suc n) w + Y (Suc n) w) ∈ borel_measurable (F n)"
  proof
    fix n
    have "X (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    moreover have "Y (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    ultimately show "(λw. X (Suc n) w + Y (Suc n) w) ∈ borel_measurable (F n)" by simp
  qed
qed



lemma (in disc_filtr_prob_space) borel_predict_stoch_proc_sum:
  fixes A::"'d ⇒ nat ⇒ 'a ⇒ ('c::{second_countable_topology, topological_comm_monoid_add})"
  assumes "⋀i. i∈ S ⟹ borel_predict_stoch_proc F (A i)"
shows "borel_predict_stoch_proc F (λ t w. (∑ i∈ S. A i t w))" unfolding predict_stoch_proc_def
proof
  show "(λw. ∑i∈S. A i 0 w) ∈ borel_measurable (F 0)"
  proof
    have "⋀i. i∈ S⟹ A i 0 ∈ borel_measurable (F 0)" using assms unfolding predict_stoch_proc_def by simp
    thus "(λ w. (∑ i∈ S. A i 0 w)) ∈ borel_measurable (F 0)" by (simp add:borel_measurable_sum)
  qed simp
next
  show "∀n. (λw. ∑i∈S. A i (Suc n) w) ∈ borel_measurable (F n)"
  proof
    fix n
    have "⋀i. i∈ S⟹ A i (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    thus "(λ w. (∑ i∈ S. A i (Suc n) w)) ∈ borel_measurable (F n)" by (simp add:borel_measurable_sum)
  qed
qed


lemma (in disc_filtr_prob_space) borel_predict_stoch_proc_times:
  fixes X::"nat ⇒ 'a ⇒ ('c::{second_countable_topology, real_normed_algebra})"
  assumes "borel_predict_stoch_proc F X"
  and "borel_predict_stoch_proc F Y"
shows "borel_predict_stoch_proc F (λt w. X t w * Y t w)" unfolding predict_stoch_proc_def
proof
  show "(λw. X 0 w * Y 0 w) ∈ borel_measurable (F 0)"
  proof -
    have "X 0 ∈ borel_measurable (F 0)" using assms unfolding predict_stoch_proc_def by simp
    moreover have "Y 0 ∈ borel_measurable (F 0)" using assms unfolding predict_stoch_proc_def by simp
    ultimately show "(λw. X 0 w * Y 0 w) ∈ borel_measurable (F 0)" by simp
  qed
next
  show "∀n. (λw. X (Suc n) w * Y (Suc n) w) ∈ borel_measurable (F n)"
  proof
    fix n
    have "X (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    moreover have "Y (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    ultimately show "(λw. X (Suc n) w * Y (Suc n) w) ∈ borel_measurable (F n)" by simp
  qed
qed

lemma (in disc_filtr_prob_space) borel_predict_stoch_proc_prod:
  fixes A::"'d ⇒ nat ⇒ 'a ⇒ ('c::{second_countable_topology, real_normed_field})"
  assumes "⋀i. i∈ S ⟹ borel_predict_stoch_proc F (A i)"
shows "borel_predict_stoch_proc F (λ t w. (∏ i∈ S. A i t w))" unfolding predict_stoch_proc_def
proof
  show "(λw. ∏i∈S. A i 0 w) ∈ borel_measurable (F 0)"
  proof -
    have "⋀i. i∈ S⟹ A i 0 ∈ borel_measurable (F 0)" using assms unfolding predict_stoch_proc_def by simp
    thus "(λ w. (∏ i∈ S. A i 0 w)) ∈ borel_measurable (F 0)" by simp
  qed
next
  show "∀n. (λw. ∏i∈S. A i (Suc n) w) ∈ borel_measurable (F n)"
  proof
    fix n
    have "⋀i. i∈ S⟹ A i (Suc n) ∈ borel_measurable (F n)" using assms unfolding predict_stoch_proc_def by simp
    thus "(λ w. (∏ i∈ S. A i (Suc n) w)) ∈ borel_measurable (F n)" by simp
  qed
qed


definition (in prob_space) constant_image where
  "constant_image f = (if ∃ c::'b::{t2_space}. ∀x∈ space M. f x = c then
    SOME c. ∀x ∈ space M. f x = c else undefined)"

lemma (in prob_space) constant_imageI:
  assumes "∃c::'b::{t2_space}. ∀x∈ space M. f x = c"
  shows "∀x∈ space M. f x = (constant_image f)"
proof
  fix x
  assume "x∈ space M"
  let ?c = "SOME c. ∀x∈ space M. f x = c"
  have "f x = ?c" using ‹x∈ space M› someI_ex[of "λc. ∀x∈ space M. f x = c"] assms by blast
  thus "f x = (constant_image f)" by (simp add: assms prob_space.constant_image_def prob_space_axioms)
qed

lemma (in prob_space) constant_image_pos:
  assumes "∀x∈ space M. (0::real) < f x"
  and "∃c::real. ∀x∈ space M. f x = c"
shows "0 < (constant_image f)"
proof -
  {
    fix x
    assume "x∈ space M"
    hence "0 < f x" using assms by simp
    also have "... = constant_image f" using assms constant_imageI ‹x∈ space M› by auto
    finally have ?thesis .
  }
  thus ?thesis using subprob_not_empty by auto
qed

definition open_except where
"open_except x y = (if x = y then {} else SOME A. open A ∧ x∈ A ∧ y∉ A)"


lemma open_exceptI:
  assumes "(x::'b::{t1_space}) ≠ y"
  shows "open (open_except x y)" and "x∈ open_except x y" and  "y∉ open_except x y"
proof-
  have ex:"∃U. open U ∧ x ∈ U ∧ y ∉ U" using ‹x≠ y› by (simp add:t1_space)
  let ?V = "SOME A. open A ∧ x∈ A ∧ y∉ A"
  have vprop: "open ?V ∧ x ∈ ?V ∧ y ∉ ?V" using someI_ex[of "λU. open U ∧ x ∈ U ∧ y ∉ U"] ex by blast
  show "open (open_except x y)" by (simp add: open_except_def vprop)
  show "x∈ open_except x y" by (metis (full_types) open_except_def vprop)
  show "y∉ open_except x y" by (metis (full_types) open_except_def vprop)
qed

lemma open_except_set:
  assumes "finite A"
  and "(x::'b::{t1_space}) ∉ A"
shows "∃U. open U ∧ x∈ U ∧ U∩ A = {}"
proof(intro exI conjI)
  have "∀y∈ A. x≠ y" using assms by auto
  let ?U = "⋂ y ∈ A. open_except x y"
  show "open ?U"
  proof (intro open_INT ballI, (simp add: assms))
    fix y
    assume "y∈ A"
    show "open (open_except x y)" using ‹∀y∈ A. x≠ y› by (simp add: ‹y ∈ A› open_exceptI)
  qed
  show "x ∈ (⋂y∈A. open_except x y)"
  proof
    fix y
    assume "y∈ A"
    show "x∈open_except x y" using ‹∀y∈ A. x≠ y› by (simp add: ‹y ∈ A› open_exceptI)
  qed
  have "∀y∈A. y∉ ?U" using ‹∀y∈ A. x≠ y› open_exceptI(3) by auto
  thus "(⋂y∈A. open_except x y) ∩ A = {}" by auto
qed

definition open_exclude_set where
"open_exclude_set x A = (if (∃U. open U ∧ U∩ A = {x}) then SOME U. open U ∧ U ∩ A = {x} else {})"

lemma open_exclude_setI:
  assumes "∃U. open U ∧ U∩ A = {x}"
shows "open (open_exclude_set x A)" and "(open_exclude_set x A) ∩ A = {x}"
proof -
  let ?V = "SOME U. open U ∧ U ∩ A = {x}"
  have vprop: "open ?V ∧ ?V ∩ A = {x}" using someI_ex[of "λU. open U ∧ U ∩ A = {x}"] assms by blast
  show "open (open_exclude_set x A)" by (simp add: open_exclude_set_def vprop)
  show "open_exclude_set x A ∩ A = {x}" by (metis (mono_tags, lifting) open_exclude_set_def vprop)
qed

lemma open_exclude_finite:
  assumes "finite A"
  and "(x::'b::{t1_space})∈ A"
shows open_set: "open (open_exclude_set x A)" and inter_x:"(open_exclude_set x A) ∩ A = {x}"
proof -
  have "∃U. open U ∧ U∩ A = {x}"
  proof -
    have "∃U. open U ∧ x∈ U ∧ U∩ (A-{x}) = {}"
    proof (rule open_except_set)
      show "finite (A -{x})" using assms by auto
      show "x∉ A -{x}" by simp
    qed
    thus ?thesis using assms by auto
  qed
  thus "open (open_exclude_set x A)" and "(open_exclude_set x A) ∩ A = {x}" by (auto simp add: open_exclude_setI)
qed

subsection ‹Initially trivial filtrations›
text ‹Intuitively, these are filtrations that can be used to denote the fact that there is no information at the start.›

definition init_triv_filt::"'a measure ⇒ ('i::linorder_bot ⇒ 'a measure) ⇒ bool" where
  "init_triv_filt M F ⟷ filtration M F ∧ sets (F bot) = {{}, space M}"

lemma triv_measurable_cst:
  fixes f::"'a⇒'b::{t2_space}"
  assumes "space N = space M"
  and "space M ≠ {}"
  and "sets N = {{}, space M}"
  and "f∈ measurable N borel"
shows "∃ c::'b. ∀x∈ space N. f x = c"
proof -
  have "f `(space N) ≠ {}" using assms by (simp add: assms)
  hence "∃ c. c∈ f`(space N)" by auto
  from this obtain c where "c∈ f`(space N)" by auto
  have "∀x ∈ space N. f x = c"
  proof
    fix x
    assume "x∈ space N"
    show "f x = c"
    proof (rule ccontr)
      assume "f x ≠ c"
      hence "(∃U V. open U ∧ open V ∧ (f x) ∈ U ∧ c ∈ V ∧ U ∩ V = {})" by (simp add: separation_t2)
      from this obtain U and V where "open U" and "open V" and "(f x) ∈ U" and "c ∈ V" and "U ∩ V = {}" by blast
      have "(f -`V) ∩ space N = space N"
      proof -
        have "V∈ sets borel" using ‹open V› unfolding borel_def by simp
        hence "(f -`V) ∩ space N ∈ sets N" using assms unfolding measurable_def by simp
        show "(f -`V) ∩ space N = space N"
        proof (rule ccontr)
          assume "(f -`V) ∩ space N ≠ space N"
          hence "(f -`V) ∩ space N = {}" using assms ‹(f -`V) ∩ space N ∈ sets N› by simp
          thus False using ‹c∈V› using ‹c ∈ f ` space N› by blast
        qed
      qed
      have "((f-`U)∩ space N) ∩ ((f-`V) ∩ space N) = {}" using ‹U∩V = {}› by auto
      moreover have "(f -`U) ∩ space N ∈ sets N" using assms ‹open U› unfolding measurable_def by simp
      ultimately have "(f -`U) ∩ space N = {}" using assms ‹(f -`V) ∩ space N = space N› by simp
      thus False using ‹f x ∈ U› ‹x ∈ space N› by blast
    qed
  qed
  thus "∃ c. ∀x∈ space N. f x = c" by auto
qed

locale trivial_init_filtrated_prob_space = prob_space +
  fixes F
  assumes info_filtration: "init_triv_filt M F"

sublocale trivial_init_filtrated_prob_space ⊆ filtrated_prob_space
  using info_filtration unfolding init_triv_filt_def by (unfold_locales, simp)


locale triv_init_disc_filtr_prob_space = prob_space +
  fixes F
  assumes info_disc_filtr: "disc_filtr M F ∧ sets (F bot) = {{}, space M}"

sublocale triv_init_disc_filtr_prob_space ⊆ trivial_init_filtrated_prob_space
proof unfold_locales
  show "init_triv_filt M F" using info_disc_filtr bot_nat_def unfolding init_triv_filt_def disc_filtr_def
    by (simp add: filtrationI)

qed


sublocale triv_init_disc_filtr_prob_space ⊆ disc_filtr_prob_space
proof unfold_locales
  show "disc_filtr M F" using info_disc_filtr by simp
qed

lemma (in triv_init_disc_filtr_prob_space) adapted_init:
  assumes "borel_adapt_stoch_proc F x"
  shows "∃c. ∀w ∈ space M. ((x 0 w)::real) = c"
proof -
  have "space M = space (F 0)" using filtration
    by (simp add: filtration_def subalgebra_def)
  moreover have "∃c. ∀w ∈ space (F 0). x 0 w = c"
  proof (rule triv_measurable_cst)
    show "space (F 0) = space M" using ‹space M = space (F 0)› ..
    show "sets (F 0) = {{}, space M}" using info_disc_filtr
      by (simp add: init_triv_filt_def bot_nat_def)
    show "x 0 ∈ borel_measurable (F 0)" using assms by (simp add: adapt_stoch_proc_def)
    show "space M ≠ {}" by (simp add:not_empty)
  qed
  ultimately show ?thesis by simp
qed

subsection ‹Filtration-equivalent measure spaces›
text ‹This is a relaxation of the notion of equivalent probability spaces, where equivalence is tested modulo a
filtration. Equivalent measure spaces agree on events that have a zero probability of occurring; here, filtration-equivalent
measure spaces agree on such events when they belong to the filtration under consideration.›

definition filt_equiv where
"filt_equiv F M N ⟷ sets M = sets N ∧ filtration M F  ∧ (∀ t A. A ∈ sets (F t) ⟶ (emeasure M A = 0) ⟷ (emeasure N A = 0))"


lemma filt_equiv_space:
  assumes "filt_equiv F M N"
  shows "space M = space N" using assms unfolding filt_equiv_def
 filtration_def subalgebra_def by (meson sets_eq_imp_space_eq)

lemma filt_equiv_sets:
  assumes "filt_equiv F M N"
  shows "sets M = sets N" using assms unfolding filt_equiv_def by simp



lemma filt_equiv_filtration:
  assumes "filt_equiv F M N"
  shows "filtration N F" using assms unfolding filt_equiv_def filtration_def subalgebra_def
  by (metis sets_eq_imp_space_eq)




lemma (in filtrated_prob_space) AE_borel_eq:
fixes f::"'a⇒real"
assumes "f∈ borel_measurable (F t)"
and "g∈ borel_measurable (F t)"
and "AE w in M. f w = g w"
shows "{w∈ space M. f w ≠ g w} ∈ sets (F t) ∧ emeasure M {w∈ space M. f w ≠ g w} = 0"
proof
  show "{w ∈ space M. f w ≠ g w} ∈ sets (F t)"
  proof -
    define minus where "minus = (λw. (f w) - (g w))"
    have "minus ∈ borel_measurable (F t)" unfolding minus_def using assms by simp
    hence "{w∈ space (F t). 0 < minus w} ∈ sets (F t)" using borel_measurable_iff_greater by auto
    moreover have "{w∈ space (F t). minus w < 0} ∈ sets (F t)" using borel_measurable_iff_less
      ‹minus ∈ borel_measurable (F t)› by auto
    ultimately have "{w∈ space (F t). 0 < minus w} ∪ {w∈ space (F t). minus w < 0} ∈ sets (F t)" by simp
    moreover have "{w∈ space (F t). f w ≠ g w} = {w∈ space (F t). 0 < minus w} ∪ {w∈ space (F t). minus w < 0}"
    proof
      show "{w ∈ space (F t). f w ≠ g w} ⊆ {w ∈ space (F t). 0 < minus w} ∪ {w ∈ space (F t). minus w < 0}"
      proof
        fix w
        assume "w ∈ {w ∈ space (F t). f w ≠ g w}"
        hence "w∈ space (F t)" and "f w ≠ g w" by auto
        thus "w∈ {w ∈ space (F t). 0 < minus w} ∪ {w ∈ space (F t). minus w < 0}" unfolding minus_def
          by (cases "f w < g w") auto
      qed
      have "{w ∈ space (F t). 0 < minus w} ⊆ {w ∈ space (F t). f w ≠ g w}" unfolding minus_def by auto
      moreover have "{w ∈ space (F t). minus w < 0} ⊆ {w ∈ space (F t). f w ≠ g w}" unfolding minus_def by auto
      ultimately show "{w ∈ space (F t). 0 < minus w} ∪ {w ∈ space (F t). minus w < 0} ⊆ {w ∈ space (F t). f w ≠ g w}"
        by simp
    qed
    moreover have "space (F t) = space M" using filtration unfolding filtration_def subalgebra_def by simp
    ultimately show ?thesis by simp
  qed
  show "emeasure M {w∈ space M. f w ≠ g w} = 0" by (metis (no_types) AE_iff_measurable assms(3) emeasure_notin_sets)
qed


lemma (in prob_space) filt_equiv_borel_AE_eq:
  fixes f::"'a⇒ real"
  assumes "filt_equiv F M N"
and "f∈ borel_measurable (F t)"
and "g∈ borel_measurable (F t)"
and "AE w in M. f w = g w"
shows "AE w in N. f w = g w"
proof -
  have set0: "{w∈ space M. f w ≠ g w} ∈ sets (F t) ∧ emeasure M {w∈ space M. f w ≠ g w} = 0"
  proof (rule filtrated_prob_space.AE_borel_eq, (auto simp add: assms))
    show "filtrated_prob_space M F" using assms unfolding filt_equiv_def
      by (simp add: filtrated_prob_space_axioms.intro filtrated_prob_space_def prob_space_axioms)
  qed
  hence "emeasure N {w∈ space M. f w ≠ g w} = 0" using assms unfolding filt_equiv_def by auto
  moreover have "{w∈ space M. f w ≠ g w} ∈ sets N" using set0 assms unfolding filt_equiv_def
    filtration_def subalgebra_def by auto
  ultimately show ?thesis
  proof -
  have "space M = space N"
    by (metis assms(1) filt_equiv_space)
    then have "∀p. almost_everywhere N p ∨ {a ∈ space N. ¬ p a} ≠ {a ∈ space N. f a ≠ g a}"
      using AE_iff_measurable ‹emeasure N {w ∈ space M. f w ≠ g w} = 0› ‹{w ∈ space M. f w ≠ g w} ∈ sets N›
      by auto
    then show ?thesis
      by metis
  qed
qed

lemma filt_equiv_prob_space_subalgebra:
  assumes "prob_space N"
  and "filt_equiv F M N"
  and "sigma_finite_subalgebra M G"
shows "sigma_finite_subalgebra N G" unfolding sigma_finite_subalgebra_def
proof
  show "subalgebra N G"
    by (metis assms(2) assms(3) filt_equiv_space filt_equiv_def sigma_finite_subalgebra_def subalgebra_def)
  show "sigma_finite_measure (restr_to_subalg N G)" unfolding restr_to_subalg_def
    by (metis ‹subalgebra N G› assms(1) finite_measure_def finite_measure_restr_to_subalg prob_space_def restr_to_subalg_def)
qed


lemma filt_equiv_measurable:
  assumes "filt_equiv F M N"
  and "f∈ measurable M P"
shows "f∈ measurable N P" using assms unfolding filt_equiv_def measurable_def
proof -
  assume a1: "sets M = sets N ∧ Filtration.filtration M F ∧ (∀t A. A ∈ sets (F t) ⟶ (emeasure M A = 0) = (emeasure N A = 0))"
  assume a2: "f ∈ {f ∈ space M → space P. ∀y∈sets P. f -` y ∩ space M ∈ sets M}"
  have "space N = space M"
    using a1 by (metis (lifting) sets_eq_imp_space_eq)
  then show "f ∈ {f ∈ space N → space P. ∀C∈sets P. f -` C ∩ space N ∈ sets N}"
    using a2 a1 by force
qed


lemma filt_equiv_imp_subalgebra:
  assumes "filt_equiv F M N"
shows "subalgebra N M" unfolding subalgebra_def
  using assms filt_equiv_space filt_equiv_def by blast




end