Theory Measure_Space_Supplement

(*  Author:     Ata Keskin, TU München 
*)

theory Measure_Space_Supplement
  imports "HOL-Analysis.Measure_Space"
begin

section ‹Supplementary Lemmas for Measure Spaces›

subsection ‹‹σ›-Algebra Generated by a Family of Functions›

definition family_vimage_algebra :: "'a set ⇒ ('a ⇒ 'b) set ⇒ 'b measure ⇒ 'a measure" where
  "family_vimage_algebra Ω S M ≡ sigma Ω (⋃f ∈ S. {f -` A ∩ Ω | A. A ∈ M})"

text ‹For singleton \<^term>‹S›, i.e. \<^term>‹S = {f}› for some \<^term>‹f›, the definition simplifies to that of \<^term>‹vimage_algebra›.›

lemma family_vimage_algebra_singleton: "family_vimage_algebra Ω {f} M = vimage_algebra Ω f M" unfolding family_vimage_algebra_def vimage_algebra_def by simp

lemma
  shows sets_family_vimage_algebra: "sets (family_vimage_algebra Ω S M) = sigma_sets Ω (⋃f ∈ S. {f -` A ∩ Ω | A. A ∈ M})" 
    and space_family_vimage_algebra[simp]: "space (family_vimage_algebra Ω S M) = Ω"
  by (auto simp add: family_vimage_algebra_def sets_measure_of_conv space_measure_of_conv)

lemma measurable_family_vimage_algebra:
  assumes "f ∈ S" "f ∈ Ω → space M"
  shows "f ∈ family_vimage_algebra Ω S M →⇩M M"
  using assms by (intro measurableI, auto simp add: sets_family_vimage_algebra)

lemma measurable_family_vimage_algebra_singleton:
  assumes "f ∈ Ω → space M"
  shows "f ∈ family_vimage_algebra Ω {f} M →⇩M M"
  using assms measurable_family_vimage_algebra by blast

text ‹A collection of functions are measurable with respect to some ‹σ›-algebra \<^term>‹N›, if and only if the ‹σ›-algebra they generate is contained in \<^term>‹N›.›
lemma measurable_family_iff_sets:
  shows "(S ⊆ N →⇩M M) ⟷ S ⊆ space N → space M ∧ family_vimage_algebra (space N) S M ⊆ N"
proof (standard, goal_cases)
  case 1
  hence subset: "S ⊆ space N → space M" using measurable_space by fast
  have "{f -` A ∩ space N |A. A ∈ M} ⊆ N" if "f ∈ S" for f using measurable_iff_sets[unfolded family_vimage_algebra_singleton[symmetric], of f] 1 subset that by (fastforce simp add: sets_family_vimage_algebra)
  then show ?case unfolding sets_family_vimage_algebra using sets.sigma_algebra_axioms by (simp add: subset, intro sigma_algebra.sigma_sets_subset, blast+)
next
  case 2
  hence subset: "S ⊆ space N → space M" by simp
  show ?case
  proof (standard, goal_cases)
    case (1 x)
    have "family_vimage_algebra (space N) {x} M ⊆ N" by (metis (no_types, lifting) 1 2 sets_family_vimage_algebra SUP_le_iff sigma_sets_le_sets_iff singletonD)
    thus ?case using measurable_iff_sets[unfolded family_vimage_algebra_singleton[symmetric]] subset[THEN subsetD, OF 1] by fast 
  qed
qed

lemma family_vimage_algebra_diff:
  shows "family_vimage_algebra Ω S M = sigma Ω (sets (family_vimage_algebra Ω (S - I) M) ∪ family_vimage_algebra Ω (S ∩ I) M)"
  using sets.space_closed space_measure_of_conv 
  unfolding family_vimage_algebra_def sets_family_vimage_algebra
  by (intro sigma_eqI, blast, fastforce)
     (intro sigma_sets_eqI, blast, simp add: sets_measure_of_conv split: if_splits, 
      meson Diff_subset Sup_subset_mono in_mono inf_sup_ord(1) sigma_sets_subseteq subset_image_iff, fastforce+)

end