Theory DP_QBS

(* Title:  DP_QBS.thy
   Author: Michikazu Hirata, Institute of Science Tokyo *)

theory DP_QBS
  imports "Differential_Privacy.Differential_Privacy_Divergence"
          "Differential_Privacy.Differential_Privacy_Standard"
          "S_Finite_Measure_Monad.Monad_QuasiBorel"
begin

declare qbs_morphism_imp_measurable[measurable_dest]

section ‹ Definitions›
text ‹ Details of differential privacy using quasi-Borel spaces are found at~\cite{Sato_Katsumata_2023}›

subsection ‹ Divergence for Differential Privacy using QBS›
definition DP_qbs_divergence :: "'a qbs_measure ⇒ 'a qbs_measure ⇒ real ⇒ ereal" ("DP'_divergence⇩Q") where
DP_qbs_divergence_qbs_l: "DP_divergence⇩Q p q e ≡ DP_divergence (qbs_l p) (qbs_l q) e"

abbreviation DP_qbs_inequality ("DP'_inequality⇩Q") where
"DP_qbs_inequality p q ε δ ≡ DP_divergence⇩Q p q ε ≤ ereal δ"

lemmas DP_qbs_divergence_def = DP_qbs_divergence_qbs_l[simplified DP_divergence_SUP]

(* non-negativity *)
lemma DP_qbs_divergence_nonneg[simp]: "0 ≤ DP_divergence⇩Q p q e"
  by(auto simp: le_SUP_iff zero_ereal_def DP_qbs_divergence_def intro!: bexI[where x="{}"])

lemma DP_qbs_divergence_le_ereal_iff:
  "DP_divergence⇩Q p q ε ≤ ereal δ ⟷ (∀A ∈ sets (qbs_l p). measure (qbs_l p) A - exp ε * measure (qbs_l q) A ≤ δ)"
  by (auto simp: DP_divergence_forall DP_qbs_divergence_qbs_l)

corollary DP_qbs_divergence_le_ereal_dest:
  assumes "DP_divergence⇩Q p q ε ≤ ereal δ"
  shows "measure (qbs_l p) A ≤ exp ε * measure (qbs_l q) A + δ"
  using assms order.trans[OF DP_qbs_divergence_nonneg assms]
  by(cases "A ∈ sets (qbs_l p)") (auto simp: DP_qbs_divergence_le_ereal_iff measure_notin_sets)

corollary DP_qbs_divergence_le_erealI:
  assumes "⋀ A. A ∈ sets (qbs_l p) ⟹ measure (qbs_l p) A ≤ exp ε * measure (qbs_l q) A + δ"
  shows "DP_divergence⇩Q p q ε ≤ ereal δ"
  using assms by(fastforce simp: DP_qbs_divergence_le_ereal_iff)

lemma DP_qbs_divergence_zero:
  assumes "p ∈ monadP_qbs X"
    and "q ∈ monadP_qbs X"
    and "DP_inequality⇩Q p q 0 0"
  shows "p = q"
  by(auto intro!: inj_onD[OF qbs_l_inj_P] DP_divergence_zero[where L="qbs_to_measure X"]
                  assms[simplified DP_qbs_divergence_qbs_l] measurable_space[OF qbs_l_measurable_prob]
            simp: space_L)

(* antimonotonicity for ε *)
lemma DP_qbs_divergence_antimono: "a ≤ b ⟹ DP_divergence⇩Q p q b ≤ DP_divergence⇩Q p q a"
  by(auto simp: DP_qbs_divergence_def intro!: SUP_mono' mult_right_mono)

(* reflexivity *)
lemma DP_qbs_divergence_refl[simp]: "DP_divergence⇩Q p p 0 = 0"
  unfolding DP_qbs_divergence_qbs_l by(rule DP_divergence_reflexivity)

lemma DP_qbs_divergence_refl'[simp]: "0 ≤ e ⟹ DP_divergence⇩Q p p e = 0"
  by(intro antisym DP_qbs_divergence_nonneg) (auto simp: DP_qbs_divergence_def SUP_le_iff mult_le_cancel_right1)

(* transitivity *)
lemma DP_qbs_divergence_trans':
  assumes "DP_inequality⇩Q p q ε δ"
    and "DP_inequality⇩Q q l ε' 0"
  shows "DP_inequality⇩Q p l (ε + ε') δ"
  unfolding DP_qbs_divergence_le_ereal_iff diff_le_eq
proof safe
  fix A
  assume [measurable]:"A ∈ sets (qbs_l p)"
  show "measure (qbs_l p) A ≤ δ + exp (ε + ε') * measure (qbs_l l) A"
  proof -
    have "measure (qbs_l p) A ≤ δ + exp ε * measure (qbs_l q) A"
      using assms(1) by(auto simp: DP_qbs_divergence_le_ereal_iff diff_le_eq)
    also have "... ≤ δ + exp ε * (exp ε' * measure (qbs_l l) A)"
      using DP_qbs_divergence_le_ereal_dest assms(2) by fastforce
    finally show ?thesis
      by (simp add: exp_add)
  qed
qed

lemmas DP_qbs_divergence_trans = DP_qbs_divergence_trans'[where δ=0]

(* composability *)
proposition DP_qbs_divergence_compose:
  assumes [qbs,measurable]:"p ∈ monadP_qbs X" "q ∈ monadP_qbs X" "f ∈ X →⇩Q monadP_qbs Y" "g ∈ X →⇩Q monadP_qbs Y"
    and dp1:"DP_divergence⇩Q p q ε ≤ ereal δ"
    and dp2:"⋀x. x ∈ qbs_space X ⟹ DP_divergence⇩Q (f x) (g x) ε' ≤ ereal δ'"
    and [arith]: "0 ≤ ε" "0 ≤ ε'"
  shows "DP_divergence⇩Q (p ⤜ f) (q ⤜ g) (ε + ε') ≤ ereal (δ + δ')"
proof -
  interpret comparable_probability_measures "qbs_to_measure X" "qbs_l p" "qbs_l q"
    by(auto simp: comparable_probability_measures_def space_L intro!: qbs_l_measurable_prob[THEN measurable_space])
  note [measurable,simp] = qbs_l_measurable_prob
  show ?thesis
    by(auto simp: qbs_l_bind_qbsP[of _ X _ Y] space_L M N DP_qbs_divergence_qbs_l
        intro!: DP_divergence_composability[where K="qbs_to_measure Y" and L="qbs_to_measure X"]
                dp1[simplified DP_qbs_divergence_qbs_l] dp2[simplified DP_qbs_divergence_qbs_l])
qed

(* Dataprocessing inequality *)
corollary DP_qbs_divergence_dataprocessing:
  assumes [qbs]:"p ∈ monadP_qbs X" "q ∈ monadP_qbs X" "f ∈ X →⇩Q monadP_qbs Y"
    and dp: "DP_divergence⇩Q p q ε ≤ ereal δ"
    and [arith]:"0 ≤ ε"
  shows  "DP_divergence⇩Q (p ⤜ f) (q ⤜ f) ε ≤ ereal δ"
proof -
  interpret comparable_probability_measures "qbs_to_measure X" "qbs_l p" "qbs_l q"
    by(auto simp: comparable_probability_measures_def space_L intro!: qbs_l_measurable_prob[THEN measurable_space])
  note [measurable] = qbs_l_measurable_prob qbs_morphism_imp_measurable[OF assms(3)]
  show ?thesis
    by(auto simp: qbs_l_bind_qbsP[of _ X _ Y] space_L M N DP_qbs_divergence_qbs_l
        intro!: DP_divergence_postprocessing[where L= "qbs_to_measure X" and K="qbs_to_measure Y"]
                dp[simplified DP_qbs_divergence_qbs_l])
qed

(* additivity = law for double-strength *)
lemma DP_qbs_divergence_additive:
  assumes [qbs]:"p ∈ monadP_qbs X" "q ∈ monadP_qbs X" "p' ∈ monadP_qbs Y" "q' ∈ monadP_qbs Y"
    and div1: "DP_divergence⇩Q p q ε ≤ ereal δ"
    and div2: "DP_divergence⇩Q p' q' ε' ≤ ereal δ'"
    and [arith]:"0 ≤ ε" "0 ≤ ε'"
  shows "DP_divergence⇩Q (p ⨂⇩Q⇩m⇩e⇩s p') (q ⨂⇩Q⇩m⇩e⇩s q') (ε + ε') ≤ ereal (δ + δ')"
proof -
  note [qbs] = return_qbs_morphismP bind_qbs_morphismP qbs_space_monadPM
  have "DP_divergence⇩Q (p ⨂⇩Q⇩m⇩e⇩s p') (q ⨂⇩Q⇩m⇩e⇩s q') (ε + ε')
      = DP_divergence⇩Q (p ⤜ (λx. p' ⤜ (λy. return_qbs (X ⨂⇩Q Y) (x, y))))
                       (q ⤜ (λx. q' ⤜ (λy. return_qbs (X ⨂⇩Q Y) (x, y)))) (ε + ε')"
    by(simp add: qbs_pair_measure_def[of _ X _ Y])
  also have "... ≤ ereal (δ + δ')"
    by(auto intro!: DP_qbs_divergence_compose[of _ X _ _ "X ⨂⇩Q Y"] div1 div2
                    DP_qbs_divergence_dataprocessing[of _ Y _ _ "X ⨂⇩Q Y"])
  finally show ?thesis .
qed

(* strengh law *)
corollary DP_qbs_divergence_strength:
  assumes [qbs]:"p ∈ monadP_qbs X" "q ∈ monadP_qbs X" "x ∈ qbs_space Y"
    and dp: "DP_divergence⇩Q p q ε ≤ ereal δ"
    and [simp]:"0 ≤ ε"
  shows "DP_divergence⇩Q (return_qbs Y x ⨂⇩Q⇩m⇩e⇩s p) (return_qbs Y x ⨂⇩Q⇩m⇩e⇩s q) ε ≤ ereal δ"
proof -
  note [qbs] = return_qbs_morphismP
  show ?thesis
    by(auto intro!: DP_qbs_divergence_additive[of _ Y _ _ X _ 0 0,simplified] dp)
qed


subsection ‹Differential Privacy using QBS›
definition DP_qbs ("differential'_privacy⇩Q") where
DP_qbs_qbs_L:"differential_privacy⇩Q M ≡ differential_privacy (λx. qbs_l (M x))"

lemma DP_qbs_def:
  "differential_privacy⇩Q M adj ε δ ⟷
   (∀(d1, d2)∈adj. DP_inequality⇩Q (M d1) (M d2) ε δ ∧ DP_inequality⇩Q (M d2) (M d1) ε δ)"
  by(simp add: DP_inequality_cong_DP_divergence differential_privacy_def DP_qbs_qbs_L DP_qbs_divergence_qbs_l)

lemma DP_qbs_adj_sym:
  assumes "sym adj"
  shows "differential_privacy⇩Q M adj ε δ ⟷ (∀ (d1,d2) ∈ adj.  DP_inequality⇩Q (M d1) (M d2) ε δ)"
  by(auto simp: differential_privacy_adj_sym[OF assms] DP_inequality_cong_DP_divergence
                DP_qbs_qbs_L DP_qbs_divergence_qbs_l)

lemma pure_DP_qbs_comp:
  assumes "adj ⊆ qbs_space X × qbs_space X"
    and "adj' ⊆ qbs_space X × qbs_space X"
    and "differential_privacy⇩Q M adj ε 0"
    and "differential_privacy⇩Q M adj' ε' 0"
    and "M ∈ X →⇩Q monadP_qbs Y"
  shows "differential_privacy⇩Q M (adj O adj') (ε + ε') 0"
  using assms
  by(auto intro!: pure_differential_privacy_comp[where X="qbs_to_measure X" and R="qbs_to_measure Y"]
      simp: space_L DP_qbs_qbs_L)

lemma pure_DP_qbs_trans_k:
  assumes "adj ⊆ qbs_space X × qbs_space X"
    and "differential_privacy⇩Q M adj ε 0"
    and "M ∈ X →⇩Q monadP_qbs Y"
  shows "differential_privacy⇩Q M (adj ^^ k) (k * ε) 0"
  using assms
  by(auto intro!: pure_differential_privacy_trans_k[where X="qbs_to_measure X" and R="qbs_to_measure Y"]
      simp: space_L DP_qbs_qbs_L)

proposition DP_qbs_postprocessing:
  assumes "ε ≥ 0"
    and "differential_privacy⇩Q M adj ε δ"
    and [qbs,measurable]:"M ∈ X →⇩Q monadP_qbs Y"
    and [qbs,measurable]:"N ∈ Y →⇩Q monadP_qbs Z"
    and "adj ⊆ qbs_space X × qbs_space X"
  shows "differential_privacy⇩Q (λx. M x ⤜ N) adj ε δ"
  using assms by(auto simp: DP_qbs_def intro!: DP_qbs_divergence_dataprocessing[of _ Y _ _ Z])

corollary DP_qbs_postprocessing_return:
  assumes "ε ≥ 0"
    and "differential_privacy⇩Q M adj ε δ"
    and "M ∈ X →⇩Q monadP_qbs Y"
    and "N ∈ Y →⇩Q Z"
    and "adj ⊆ qbs_space X × qbs_space X"
  shows "differential_privacy⇩Q (λx. M x ⤜ (λy. return_qbs Z (N y))) adj ε δ"
  by(intro DP_qbs_postprocessing[where X=X and Y=Y and Z=Z])
    (use return_qbs_morphismP[of Z] assms in auto)

lemma DP_qbs_preprocessing:
  assumes "ε ≥ 0"
    and "differential_privacy⇩Q M adj ε δ"
    and [measurable]:"f ∈ X' →⇩Q X"
    and "∀(x,y) ∈ adj'. ((f x), (f y)) ∈ adj"
    and "adj ⊆ qbs_space X × qbs_space X"
    and "adj' ⊆ qbs_space X' × qbs_space X'"
  shows "differential_privacy⇩Q (M ∘ f) adj' ε δ"
  using assms by(auto simp: DP_qbs_def)

proposition DP_qbs_bind_adaptive:
  assumes "ε ≥ 0" and "ε' ≥ 0"
    and [qbs]:"M ∈ X →⇩Q monadP_qbs Y"
    and "differential_privacy⇩Q M adj ε δ"
    and [qbs]:"N ∈ X ⇒⇩Q Y ⇒⇩Q monadP_qbs Z"
    and "⋀y. y ∈ qbs_space Y ⟹ differential_privacy⇩Q (λx. N x y) adj ε' δ'"
    and "adj ⊆ qbs_space X × qbs_space X"
  shows "differential_privacy⇩Q (λx. M x ⤜ N x) adj (ε + ε') (δ + δ')"
 using assms by(fastforce simp add: DP_qbs_def intro!: DP_qbs_divergence_compose[of _ Y _ _ Z])

proposition DP_qbs_bind_pair:
  assumes "ε ≥ 0" "ε' ≥ 0"
    and [qbs]:"M ∈ X →⇩Q monadP_qbs Y"
    and "differential_privacy⇩Q M adj ε δ"
    and [qbs]:"N ∈ X →⇩Q monadP_qbs Z"
    and "differential_privacy⇩Q N adj ε' δ'"
    and "adj ⊆ qbs_space X × qbs_space X"
  shows "differential_privacy⇩Q (λx. M x ⤜ (λy. N x ⤜ (λz. return_qbs (Y ⨂⇩Q Z) (y,z)))) adj (ε + ε') (δ + δ')"
proof -
  note [qbs] = return_qbs_morphismP bind_qbs_morphismP
  show "?thesis"
    using assms by(auto intro!: DP_qbs_bind_adaptive[where X=X and Y=Y and Z="Y ⨂⇩Q Z"]
                                DP_qbs_postprocessing[where X=X and Y=Z and Z="Y ⨂⇩Q Z"])
qed

end