Theory Differential_Privacy.Measurable_Isomorphism

(*
 Title:Measurable_Isomorphism.thy
 Author: Tetsuya Sato
*)

theory Measurable_Isomorphism
  imports
    "HOL-Analysis.Sigma_Algebra"
begin

lemma measurable_isomorphism_iff:
  assumes "f ∈ M →M N"
    and "g ∈ N →M M"
    and "∀ x ∈ space M. g(f(x)) = x"
    and "∀ y ∈ space N. f(g(y)) = y"
  shows "⋀ h. (h ∈ N →M K) ⟷ (h o f ∈ M →M K)"
    "⋀ h. (h ∈ M →M K) ⟷ (h o g ∈ N →M K)"
    "⋀ h. (h ∈ K →M M) ⟷ (f o h ∈ K →M N)∧(h ∈ space K → space M)"
    "⋀ h. (h ∈ K →M N) ⟷ (g o h ∈ K →M M)∧(h ∈ space K → space N)"
proof-
  show "⋀ h. (h ∈ N →M K) ⟷ (h o f ∈ M →M K)"
  proof(intro iffI measurable_comp[OF assms(1)],clarify)
    fix h assume "h ∘ f ∈ M →M K"
    hence "h o f o g ∈ N →M K"
      using assms(2) measurable_comp by blast
    thus"h ∈ N →M K"
      by(subst measurable_cong, auto simp add: assms)
  qed
  show "⋀h. (h ∈ M →M K) = (h ∘ g ∈ N →M K)"
  proof(intro iffI measurable_comp[OF assms(2)],clarify)
    fix h assume "h ∘ g ∈ N →M K"
    hence "h o g o f ∈ M →M K"
      using assms(1) measurable_comp by blast
    thus"h ∈ M →M K"
      by(subst measurable_cong, auto simp add: assms)
  qed
  show "⋀h. (h ∈ K →M M) ⟷ (f o h ∈ K →M N)∧(h ∈ space K → space M)"
  proof(intro iffI conjI measurable_comp[OF _ assms(1)],clarify)
    fix h assume "f ∘ h ∈ K →M N ∧ h ∈ space K → space M"
    hence "g o f o h ∈ K →M M ∧ h ∈ space K → space M"
      using assms(2) measurable_comp by(subst comp_assoc, auto)
    hence "g o f o h ∈ K →M M ∧ (∀w ∈ space K. (g o f o h) w = (h w))"
      using assms (3,4) by auto
    thus"h ∈ K →M M"
      using assms (3,4) by(subst measurable_cong, auto)
  qed(auto simp:measurable_def)
  show "⋀h. (h ∈ K →M N) = (g ∘ h ∈ K →M M ∧ h ∈ space K → space N)"
  proof(intro iffI conjI measurable_comp[OF _ assms(2)],clarify)
    fix h assume "g ∘ h ∈ K →M M ∧ h ∈ space K → space N"
    hence "f o g ∘ h ∈ K →M N ∧ h ∈ space K → space N"
      using assms(1) measurable_comp by(subst comp_assoc, auto)
    hence "f o g o h ∈ K →M N ∧ (∀w ∈ space K. (f o g o h) w = (h w))"
      using assms (3,4) by auto
    thus"h ∈ K →M N"
      using assms (3,4) by(subst measurable_cong, auto)
  qed(auto simp:measurable_def)
qed

end