Theory Differential_Privacy_Randomized_Response
theory Differential_Privacy_Randomized_Response
imports"Differential_Privacy_Divergence"
begin
section ‹Randomized Response Mechanism›
definition RR_mechanism :: "real ⇒ bool ⇒ bool pmf"
where "RR_mechanism ε x =
(if x then (bernoulli_pmf ((exp ε) / (1 + exp ε)))
else (bernoulli_pmf (1 / (1 + exp ε))))"
lemma meausrable_RR_mechanism[measurable]:
shows "measure_pmf o (RR_mechanism ε) ∈ measurable (count_space UNIV) (prob_algebra (count_space UNIV))"
proof(rule measurable_prob_algebraI)
fix x :: bool
show "prob_space ((measure_pmf ∘ RR_mechanism ε) x)"
unfolding RR_mechanism_def using prob_space_measure_pmf if_split_mem1 by auto
thus "measure_pmf ∘ RR_mechanism ε ∈ count_space UNIV →⇩M subprob_algebra (count_space UNIV)"
unfolding RR_mechanism_def space_measure_pmf
by (auto simp: measure_pmf_in_subprob_space)
qed
lemma RR_probability_flip1:
fixes ε :: real
assumes "ε ≥ 0"
shows "1 - 1 / (1 + exp ε) = exp ε / (1 + exp ε)"
using add_diff_cancel_left' add_divide_distrib div_self not_exp_less_zero square_bound_lemma vector_space_over_itself.scale_zero_left
by metis
lemma RR_probability_flip2:
fixes ε :: real
assumes "ε ≥ 0"
shows "1- exp ε / (1 + exp ε) = 1 / (1 + exp ε)"
using RR_probability_flip1 assms
by fastforce
lemma RR_mechanism_flip:
assumes "ε ≥ 0"
shows "bind_pmf (RR_mechanism ε x) (λ b :: bool. return_pmf (¬ b)) = (RR_mechanism ε (¬ x))"
unfolding RR_mechanism_def
proof-
have eq1: "bernoulli_pmf (exp ε / (1 + exp ε)) ⤜ (λb. return_pmf (¬ b)) = bernoulli_pmf (1 / (1 + exp ε))"
proof(rule pmf_eqI)
fix i :: bool
have "pmf (bernoulli_pmf (exp ε / ((1 :: real) + exp ε)) ⤜ (λb :: bool. return_pmf (¬ b))) i = (∫⇧+x. (pmf ((λb :: bool. return_pmf (¬ b)) x) i) ∂(measure_pmf (bernoulli_pmf (exp ε / ((1 :: real) + exp ε)))))"
using ennreal_pmf_bind by metis
also have "... = ennreal (pmf (return_pmf (¬ True)) i) * ennreal (exp ε / (1 + exp ε)) + ennreal (pmf (return_pmf (¬ False)) i) * ennreal (1 - exp ε / (1 + exp ε))"
by(rule nn_integral_bernoulli_pmf ; simp_all add: add_pos_nonneg)
also have "... = ennreal (pmf (return_pmf True) i) * ennreal (1 - exp ε / (1 + exp ε)) + ennreal (pmf (return_pmf False) i) * ennreal (1- (1 - exp ε / (1 + exp ε)))"
by auto
also have "... = (∫⇧+x. (pmf (return_pmf x) i) ∂bernoulli_pmf (1 - exp ε / (1 + exp ε)))"
by(rule nn_integral_bernoulli_pmf[where p ="(1 - exp ε / (1 + exp ε))",THEN sym] ; simp_all add: add_pos_nonneg)
also have "... = pmf (bind_pmf (bernoulli_pmf (1 - exp ε / (1 + exp ε))) return_pmf) i"
using ennreal_pmf_bind by metis
also have "... = (pmf (bernoulli_pmf (1 - exp ε / (1 + exp ε))) i)"
by (auto simp: bind_return_pmf')
also have "... = (pmf (bernoulli_pmf (1 / (1 + exp ε))) i)"
by (metis add.commute add_diff_cancel_left' add_divide_distrib div_self not_exp_less_zero square_bound_lemma vector_space_over_itself.scale_zero_left)
finally show "pmf (bernoulli_pmf (exp ε / (1 + exp ε)) ⤜ (λb. return_pmf (¬ b))) i = pmf (bernoulli_pmf (1 / (1 + exp ε))) i"by auto
qed
have eq2: "bernoulli_pmf (1 / (1 + exp ε)) ⤜ (λb. return_pmf (¬ b)) = bernoulli_pmf (exp ε / (1 + exp ε))"
proof(rule pmf_eqI)
fix i :: bool
have "pmf (bernoulli_pmf (1/ ((1 :: real) + exp ε)) ⤜ (λb :: bool. return_pmf (¬ b))) i = (∫⇧+x. (pmf ((λb :: bool. return_pmf (¬ b)) x) i) ∂(measure_pmf (bernoulli_pmf (1 / ((1 :: real) + exp ε)))))"
using ennreal_pmf_bind by metis
also have "... = ennreal (pmf (return_pmf (¬ True)) i) * ennreal (1 / (1 + exp ε)) + ennreal (pmf (return_pmf (¬ False)) i) * ennreal (1 - 1/ (1 + exp ε))"
by(rule nn_integral_bernoulli_pmf ; simp_all add: add_pos_nonneg)
also have "... = ennreal (pmf (return_pmf True) i) * ennreal (exp ε / (1 + exp ε)) + ennreal (pmf (return_pmf False) i) * ennreal (1 - exp ε / (1 + exp ε))"
by(auto simp:RR_probability_flip1 RR_probability_flip2 assms)
also have "... = (∫⇧+x. (pmf (return_pmf x) i) ∂bernoulli_pmf (exp ε / (1 + exp ε)))"
by(rule nn_integral_bernoulli_pmf[where p ="(exp ε / (1 + exp ε))",THEN sym] ; simp_all add: add_pos_nonneg)
also have "... = pmf (bind_pmf (bernoulli_pmf (exp ε / (1 + exp ε))) return_pmf) i"
using ennreal_pmf_bind by metis
also have "... = (pmf (bernoulli_pmf (exp ε / (1 + exp ε))) i)"
by (auto simp: bind_return_pmf')
finally show "pmf (bernoulli_pmf (1/ ((1 :: real) + exp ε)) ⤜ (λb :: bool. return_pmf (¬ b))) i = pmf (bernoulli_pmf (exp ε / (1 + exp ε))) i"by auto
qed
show "(if x then bernoulli_pmf (exp ε / ((1 :: real) + exp ε)) else bernoulli_pmf ((1 :: real) / ((1 :: real) + exp ε))) ⤜ (λb :: bool. return_pmf (¬ b)) =
(if ¬ x then bernoulli_pmf (exp ε / ((1 :: real) + exp ε)) else bernoulli_pmf ((1 :: real) / ((1 :: real) + exp ε)))"
using eq1 eq2 by auto
qed
proposition DP_RR_mechanism:
fixes ε :: real and x y :: bool
assumes "ε > 0"
shows "DP_divergence (RR_mechanism ε x) (RR_mechanism ε y) ε ≤ (0 :: real)"
proof(subst DP_divergence_forall[THEN sym],unfold RR_mechanism_def)
{
fix A :: "bool set" assume "A ∈ measure_pmf.events (if x then bernoulli_pmf (exp ε / ((1 :: real) + exp ε)) else bernoulli_pmf ((1 :: real) / ((1 :: real) + exp ε)))"
have ineq1: "measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A ≤ exp ε * measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A"
by (auto simp: assms leI mult_le_cancel_right1 order_less_imp_not_less)
have ineq2: "measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A ≤ exp ε * measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A"
by (meson assms linorder_not_less measure_nonneg' mult_le_cancel_right1 nle_le one_le_exp_iff)
consider"A = {}"|"A = {True}"|"A = {False}"|"A = {True,False}"
by (metis (full_types) Set.set_insert all_not_in_conv insertI2)
note split_A = this
hence ineq3: "measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A ≤ exp ε * measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A"
proof(cases)
case 1
thus ?thesis by auto
next
case 2
hence "measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A = (exp ε / (1 + exp ε))"
using pmf_bernoulli_True
by (auto simp: pmf.rep_eq pos_add_strict)
also have "... = exp ε * (1 / (1 + exp ε))"
by auto
also have "... = exp ε * measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A"
using pmf_bernoulli_True 2
by (auto simp: pmf.rep_eq pos_add_strict)
finally show ?thesis by auto
next
case 3
hence "measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A = 1 - (exp ε / (1 + exp ε))"
using pmf_bernoulli_False
by (auto simp: pmf.rep_eq pos_add_strict)
also have "... = (1 / (1 + exp ε))"
using RR_probability_flip2 assms by auto
also have "... ≤ exp ε * (exp ε / (1 + exp ε))"
by (metis (no_types, opaque_lifting) add_le_same_cancel1 assms divide_right_mono dual_order.trans less_add_one linorder_not_less mult_exp_exp nle_le one_le_exp_iff times_divide_eq_right)
also have "... = exp ε * (measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A)"
proof-
have "(measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A) = 1 - (1 / (1 + exp ε))"
using pmf_bernoulli_False 3
by (auto simp: pmf.rep_eq pos_add_strict)
also have "... = exp ε / (1 + exp ε)"
using RR_probability_flip1 assms by auto
finally show ?thesis by auto
qed
thus ?thesis
using calculation by auto
next
case 4
hence "A = UNIV"
by auto
thus ?thesis
using assms by fastforce
qed
from split_A
have ineq4: "measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A ≤ exp ε * measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A"
proof(cases)
case 1
thus ?thesis
by auto
next
case 2
hence "measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A = (1 / (1 + exp ε))"
using pmf_bernoulli_True
by (auto simp: pmf.rep_eq pos_add_strict)
also have "... ≤ exp ε * (exp ε / (1 + exp ε))"
by (metis (no_types, opaque_lifting) add_le_same_cancel1 assms divide_right_mono dual_order.trans less_add_one linorder_not_less mult_exp_exp nle_le one_le_exp_iff times_divide_eq_right)
also have "... = exp ε * measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A"
using pmf_bernoulli_True 2
by (auto simp: pmf.rep_eq pos_add_strict)
finally show ?thesis
by auto
next
case 3
hence "measure_pmf.prob (bernoulli_pmf (1 / (1 + exp ε))) A = 1 - (1 / (1 + exp ε))"
using pmf_bernoulli_False
by (auto simp: pmf.rep_eq pos_add_strict)
also have "... = (exp ε / (1 + exp ε))"
using RR_probability_flip1 assms by auto
also have "... = exp ε * (1 / (1 + exp ε))"
by auto
also have "... = exp ε * (measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A)"
proof-
have "(measure_pmf.prob (bernoulli_pmf (exp ε / (1 + exp ε))) A) = 1 - (exp ε / (1 + exp ε))"
using pmf_bernoulli_False 3
by (auto simp: pmf.rep_eq pos_add_strict)
also have "... = 1 / (1 + exp ε)"
using RR_probability_flip2 assms by auto
finally show ?thesis by auto
qed
thus ?thesis
using calculation by auto
next
case 4
hence "A = UNIV"
by auto
thus ?thesis
using assms by fastforce
qed
note ineq1 ineq2 ineq3 ineq4
}
thus"∀A :: bool set∈measure_pmf.events (if x then bernoulli_pmf (exp ε / ((1 :: real) + exp ε)) else bernoulli_pmf ((1 :: real) / ((1 :: real) + exp ε))). measure_pmf.prob (if x then bernoulli_pmf (exp ε / ((1 :: real) + exp ε)) else bernoulli_pmf ((1 :: real) / ((1 :: real) + exp ε))) A - exp ε * measure_pmf.prob (if y then bernoulli_pmf (exp ε / ((1 :: real) + exp ε)) else bernoulli_pmf ((1 :: real) / ((1 :: real) + exp ε))) A ≤ (0 :: real)"
by auto
qed
end