Theory ME_Library_Complement

(*
   File:     ME_Library_Complement.thy
   Author:   Manuel Eberl, TU München
*)
theory ME_Library_Complement
  imports "HOL-Analysis.Analysis"
begin

(* TODO: could be put in the distribution *)

subsection ‹The trivial measurable space›

text ‹
  The trivial measurable space is the smallest possible ‹σ›-algebra, i.e. only the empty set
  and everything.
›
definition trivial_measure :: "'a set ⇒ 'a measure" where
  "trivial_measure X = sigma X {{}, X}"

lemma space_trivial_measure [simp]: "space (trivial_measure X) = X"
  by (simp add: trivial_measure_def)

lemma sets_trivial_measure: "sets (trivial_measure X) = {{}, X}"
  by (simp add: trivial_measure_def sigma_algebra_trivial sigma_algebra.sigma_sets_eq)

lemma measurable_trivial_measure:
  assumes "f ∈ space M → X" and "f -` X ∩ space M ∈ sets M"
  shows   "f ∈ M →⇩M trivial_measure X"
  using assms unfolding measurable_def by (auto simp: sets_trivial_measure)

lemma measurable_trivial_measure_iff:
  "f ∈ M →⇩M trivial_measure X ⟷ f ∈ space M → X ∧ f -` X ∩ space M ∈ sets M"
  unfolding measurable_def by (auto simp: sets_trivial_measure)


subsection ‹Pullback algebras›

text ‹
  The pullback algebra $f^{-1}(\Sigma)$ of a ‹σ›-algebra $(\Omega, \Sigma)$ is the smallest
  ‹σ›-algebra such that $f$ is $f^{-1}(\Sigma)--\Sigma$-measurable.
›
definition (in sigma_algebra) pullback_algebra :: "('b ⇒ 'a) ⇒ 'b set ⇒ 'b set set" where
  "pullback_algebra f Ω' = sigma_sets Ω' {f -` A ∩ Ω' |A. A ∈ M}"

lemma pullback_algebra_minimal:
  assumes "f ∈ M →⇩M N"
  shows   "sets.pullback_algebra N f (space M) ⊆ sets M"
proof
  fix X assume "X ∈ sets.pullback_algebra N f (space M)"
  thus "X ∈ sets M"
    unfolding sets.pullback_algebra_def
    by induction (use assms in ‹auto simp: measurable_def›)
qed

lemma (in sigma_algebra) in_pullback_algebra: "A ∈ M ⟹ f -` A ∩ Ω' ∈ pullback_algebra f Ω'"
  unfolding pullback_algebra_def by (rule sigma_sets.Basic) auto

end