Theory DP_QBS_Examples
section ‹ Examples ›
theory DP_QBS_Examples
imports "DP_QBS"
"Differential_Privacy.Differential_Privacy_Randomized_Response"
begin
lemma qbs_space_list_qbs_borel[qbs]: "⋀r. r ∈ qbs_space (list_qbs borel⇩Q)"
and qbs_space_list_qbs_count_space[qbs]: "⋀i. r ∈ qbs_space (list_qbs (count_space⇩Q (UNIV :: _ :: countable)))"
by(auto simp: list_qbs_space)
subsection ‹ Randomized Response ›
lemma qbs_morphism_RR_mechanism[qbs]: "qbs_pmf ∘ RR_mechanism e ∈ count_space⇩Q UNIV →⇩Q monadP_qbs (count_space⇩Q UNIV)"
by(auto intro!: qbs_morphism_count_space' qbs_pmf_qbsP)
lemma qbs_DP_RR_mechanism:
assumes [arith]:"ε ≥ 0"
shows "DP_divergence⇩Q (RR_mechanism ε x) (RR_mechanism ε y) ε = 0"
proof(intro antisym DP_qbs_divergence_nonneg)
have [arith]: "1 + exp ε > 0"
by(auto simp: add_pos_nonneg intro!:divide_le_eq_1_pos[THEN iffD2])
have [arith]: "1 / (1 + exp ε) ≤ exp ε * exp ε / (1 + exp ε)"
by(rule order.trans[where b="exp ε * (1 / (1 + exp ε))"])
(auto simp: divide_right_mono mult_le_cancel_right1)
show "DP_divergence⇩Q (RR_mechanism ε x) (RR_mechanism ε y) ε ≤ 0"
unfolding zero_ereal_def
proof(rule DP_qbs_divergence_le_erealI)
fix A :: "bool set"
have ineq1: "measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A
≤ exp ε * measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A"
and ineq2: "measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A
≤ exp ε * measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A"
by(auto simp: mult_le_cancel_right1)
have ineq3: "measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A
≤ exp ε * measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A"
proof -
consider "A = {}" | "A = {True}" | "A = {False}" | "A = UNIV"
by (metis (full_types) UNIV_eq_I is_singletonI' is_singleton_the_elem)
then show ?thesis
by cases (simp_all add: measure_pmf_single RR_probability_flip1 RR_probability_flip2)
qed
have ineq4: "measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A
≤ exp ε * measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A"
proof -
consider "A = {}" | "A = {True}" | "A = {False}" | "A = UNIV"
by (metis (full_types) UNIV_eq_I is_singletonI' is_singleton_the_elem)
then show ?thesis
by cases (simp_all add: measure_pmf_single RR_probability_flip1 RR_probability_flip2)
qed
show " measure (qbs_l (qbs_pmf (RR_mechanism ε x))) A ≤ exp ε * measure (qbs_l (qbs_pmf (RR_mechanism ε y))) A + 0"
using ineq1 ineq2 ineq3 ineq4 by(auto simp: RR_mechanism_def)
qed
qed
subsection ‹ Laplace Distribution in QBS›
lemma qbs_morphism_laplace_density[qbs]:"laplace_density ∈ borel⇩Q ⇒⇩Q borel⇩Q ⇒⇩Q borel⇩Q ⇒⇩Q borel⇩Q"
proof -
have [simp]:"laplace_density = (λl m x. if l > 0 then exp(-¦x - m¦ / l) / (2 * l) else 0)"
by standard+ (simp add: laplace_density_def)
show ?thesis
by simp
qed
definition qbs_Lap_mechanism ("Lap'_mechanism⇩Q") where
"Lap_mechanism⇩Q ≡ λe x. if e ≤ 0 then return_qbs borel⇩Q x else density_qbs lborel⇩Q (laplace_density e x)"
lemma qbs_morphism_Lap_mechanism[qbs]:"Lap_mechanism⇩Q ∈ borel⇩Q →⇩Q borel⇩Q ⇒⇩Q monadP_qbs borel⇩Q"
by(intro curry_preserves_morphisms qbs_morphism_monadPI)
(auto intro!: prob_space_return
simp: qbs_Lap_mechanism_def qbs_l_return_qbs space_L qbs_l_density_qbs[of _ borel] prob_space_laplacian_density)
lemma qbs_l_Lap_mechanism: "qbs_l (Lap_mechanism⇩Q e r) = Lap_dist e r"
by(auto simp: qbs_Lap_mechanism_def qbs_l_return_qbs space_L qbs_l_density_qbs[of _ borel] Lap_dist_def cong: return_cong)
lemma qbs_Lap_mechanism_qbs_l_inverse:"Lap_mechanism⇩Q e x= qbs_l_inverse (Lap_dist e x)"
by(auto intro!: inj_onD[OF qbs_l_inj_P[of borel]] standard_borel_ne.qbs_l_qbs_l_inverse[OF _ sets_Lap_dist,symmetric]
standard_borel_ne.qbs_l_inverse_in_space_monadP[OF _ sets_Lap_dist] simp: qbs_l_Lap_mechanism)
proposition qbs_DP_Lap_mechanism:
assumes "ε > 0" and "¦x - y¦ ≤ r"
shows "DP_divergence⇩Q (Lap_mechanism⇩Q (1 / ε) x) (Lap_mechanism⇩Q (1 / ε) y) (r * ε) = 0"
using DP_divergence_Lap_dist'[where b="1 / ε"]
by(intro antisym DP_qbs_divergence_nonneg)
(auto simp: DP_qbs_qbs_L DP_qbs_divergence_qbs_l qbs_l_Lap_mechanism zero_ereal_def intro!: assms)
subsection ‹ Naive Report Noisy Max Mechanism›
primrec qbs_NaiveRNM :: "real ⇒ real list ⇒ real qbs_measure" where
"qbs_NaiveRNM ε [] = return_qbs borel 0" |
"qbs_NaiveRNM ε (x # xs) =
(case xs of
Nil ⇒ Lap_mechanism⇩Q (1 / ε) x |
y#ys ⇒ do {x1 ← Lap_mechanism⇩Q (1 / ε) x; x2 ← qbs_NaiveRNM ε xs;
return_qbs borel (max x1 x2)})"
lemma qbs_morhpism_NaiveRNM[qbs]: "qbs_NaiveRNM ∈ borel⇩Q ⇒⇩Q list_qbs borel ⇒⇩Q monadP_qbs borel⇩Q"
proof -
note [qbs] = return_qbs_morphismP bind_qbs_morphismP
show ?thesis
by(simp add: qbs_NaiveRNM_def)
qed
theorem qbs_DP_NaiveRNM':
assumes pos[arith,simp]: "ε > 0"
and "length xs = n" and "length ys = n"
and adj: "(∑i<n. ¦nth xs i - nth ys i¦) ≤ r"
shows "DP_divergence⇩Q (qbs_NaiveRNM ε xs) (qbs_NaiveRNM ε ys) (r * ε) = 0"
using assms(2,3,4)
proof(induct ys arbitrary: xs n r)
case Nil
then show ?case
by simp
next
case ih:(Cons y ys')
show ?case (is "?lhs = _")
proof(cases ys')
case Nil
then have "∃a. xs = [a]"
using ih
by (metis length_Suc_conv length_greater_0_conv)
then show ?thesis
using ih by(auto intro!: qbs_DP_Lap_mechanism)
next
case h:(Cons y' ys'')
note [qbs] = bind_qbs_morphismP return_qbs_morphismP
obtain x x' xs'' where xs:"xs = x # x' # xs''"
by (metis h ih(2) ih(3) length_Suc_conv)
define xs' where "xs' = x' # xs''"
obtain n' where n:"n = Suc n'"
using ih(3) by force
have xs_xs':"xs = x # xs'"
by(auto simp: xs'_def h xs)
have [simp]:"length xs' = n'" "length ys' = n'"
using ih(2) ih(3) by(auto simp: xs_xs' n)
define r1 where "r1 = ¦x - y¦"
define r2 where "r2 = (∑j<n'. ¦xs' ! j - ys' ! j¦)"
have "(∑i<n. ¦xs ! i - (y # ys') ! i¦) = ¦x - y¦ + (∑i<n'. ¦xs' ! i - ys' ! i¦)"
proof -
have "(∑i<n. ¦xs ! i - (y # ys') ! i¦) = (∑i∈{0} ∪ {Suc 0..<n}. ¦xs ! i - (y # ys') ! i¦)"
using atLeast1_lessThan_eq_remove0 lessThan_Suc_eq_insert_0 n by fastforce
also have "... = (∑i∈{0}. ¦xs ! i - (y # ys') ! i¦) + (∑i∈{Suc 0..<n}. ¦xs ! i - (y # ys') ! i¦)"
by(subst sum_Un) auto
also have "... = ¦x - y¦ + (∑i<n'. ¦xs ! Suc i - (y # ys') ! Suc i¦)"
unfolding n by(subst sum.atLeast_Suc_lessThan_Suc_shift) (simp add: xs_xs' n lessThan_atLeast0)
finally show ?thesis by(simp add: xs_xs')
qed
hence r12[arith,simp]: "r1 + r2 ≤ r" "0 ≤ r1" "0 ≤ r2" "¦x - y¦ ≤ r1" "(∑j<n'. ¦xs' ! j - ys' ! j¦) ≤ r2"
using ih(4) by(auto simp: r1_def r2_def)
have "?lhs =
DP_divergence⇩Q
(Lap_mechanism⇩Q (1 / ε) x ⤜ (λx1. qbs_NaiveRNM ε xs' ⤜ (λx2. return_qbs borel⇩Q (max x1 x2))))
(Lap_mechanism⇩Q (1 / ε) y ⤜ (λx1. qbs_NaiveRNM ε ys' ⤜ (λx2. return_qbs borel⇩Q (max x1 x2))))
(r * ε)"
by(auto simp: h xs xs'_def)
also have "... ≤
DP_divergence⇩Q
(Lap_mechanism⇩Q (1 / ε) x ⤜ (λx1. qbs_NaiveRNM ε xs' ⤜ (λx2. return_qbs borel⇩Q (max x1 x2))))
(Lap_mechanism⇩Q (1 / ε) y ⤜ (λx1. qbs_NaiveRNM ε ys' ⤜ (λx2. return_qbs borel⇩Q (max x1 x2))))
(r1 * ε + r2 * ε)"
by(auto intro!: DP_qbs_divergence_antimono simp: distrib_right[symmetric])
also have "... ≤ ereal (0 + 0)"
by(intro DP_qbs_divergence_compose[of _ qbs_borel _ _ qbs_borel]
DP_qbs_divergence_dataprocessing[of _ qbs_borel _ _ qbs_borel])
(auto simp: qbs_DP_Lap_mechanism ih(1))
finally show ?thesis
using antisym zero_ereal_def by fastforce
qed
qed
definition adj_naive_RNM :: "real ⇒ (real list × real list) set" where
"adj_naive_RNM r ≡ {(xs,ys). length xs = length ys ∧ (∑i<length xs. ¦nth xs i - nth ys i¦) ≤ r}"
theorem qbs_DP_NaiveRNM:
assumes pos: "ε > 0"
shows "differential_privacy⇩Q (qbs_NaiveRNM ε) (adj_naive_RNM r) (r * ε) 0"
proof(safe intro!: DP_qbs_adj_sym[THEN iffD2])
fix xs ys
assume *:"(xs, ys) ∈ adj_naive_RNM r"
let ?n = "length xs"
have "length xs = ?n" and "length ys = ?n" and "(∑i<?n. ¦nth xs i - nth ys i¦) ≤ r"
using * by(auto simp: adj_naive_RNM_def)
from qbs_DP_NaiveRNM'[OF pos this]
show "DP_inequality⇩Q (qbs_NaiveRNM ε xs) (qbs_NaiveRNM ε ys) (r * ε) 0"
by simp
qed(auto intro!: symI simp: adj_naive_RNM_def abs_minus_commute)
end