Theory Differential_Privacy_Standard
theory Differential_Privacy_Standard
imports
"Differential_Privacy_Laplace_Mechanism_Multi"
"L1_norm_list"
"HOL.Transitive_Closure"
begin
section ‹Formalization of Differential privacy›
text ‹AFDP in this section means the textbook "The Algorithmic Foundations of Differential Privacy"written by Cynthia Dwork and Aaron Roth.›
subsection ‹Predicate of Differential privacy›
paragraph ‹The inequality for DP (cf. [Def 2.4, AFDP])›
definition DP_inequality:: "'a measure ⇒ 'a measure ⇒ real ⇒ real ⇒ bool"where
"DP_inequality M N ε δ ≡ (∀ A ∈ sets M. measure M A ≤ (exp ε) * measure N A + δ)"
paragraph ‹The divergence for DP (cf. [Barthe \& Olmedo, ICALP 2013])›
proposition DP_inequality_cong_DP_divergence:
shows "DP_inequality M N ε δ ⟷ DP_divergence M N ε ≤ δ"
by(auto simp: DP_divergence_forall[THEN sym] DP_inequality_def)
corollary DP_inequality_zero:
assumes "M ∈ space (prob_algebra L)"
and "N ∈ space (prob_algebra L)"
and "DP_inequality M N 0 0"
shows "M = N"
using assms DP_divergence_zero unfolding DP_inequality_cong_DP_divergence by auto
paragraph ‹Definition of the standard differential privacy with adjacency, and its basic properties›
text ‹ We first we abstract the domain of database and the adjacency relations. later we instantiate them according to the textbook.›
definition differential_privacy :: "('a ⇒ 'b measure) ⇒ ('a rel) ⇒ real ⇒ real ⇒ bool "where
"differential_privacy M adj ε δ ≡ ∀(d1,d2)∈adj. DP_inequality (M d1) (M d2) ε δ ∧ DP_inequality (M d2) (M d1) ε δ"
lemma differential_privacy_adj_sym:
assumes "sym adj"
shows "differential_privacy M adj ε δ ⟷ (∀ (d1,d2) ∈ adj. DP_inequality (M d1) (M d2) ε δ)"
using assms by(auto simp: differential_privacy_def sym_def)
lemma differential_privacy_symmetrize:
assumes "differential_privacy M adj ε δ"
shows "differential_privacy M (adj ∪ adj¯) ε δ"
using assms unfolding differential_privacy_def by blast
lemma differential_privacy_restrict:
assumes "differential_privacy M adj ε δ"
and "adj' ⊆ adj"
shows "differential_privacy M adj' ε δ"
using assms unfolding differential_privacy_def by blast
paragraph ‹Lemmas for group privacy (cf. [Theorem 2.2, AFDP])›
lemma pure_differential_privacy_comp:
assumes "adj1 ⊆ (space X) × (space X)"
and "adj2 ⊆ (space X) × (space X)"
and "differential_privacy M adj1 ε1 0"
and "differential_privacy M adj2 ε2 0"
and M:"M ∈ X →⇩M (prob_algebra R)"
shows "differential_privacy M (adj1 O adj2) (ε1 + ε2) 0"
using assms unfolding differential_privacy_def
proof(intro ballI)
note [measurable] = M
fix x assume a1: "∀(d1, d2)∈ adj1. DP_inequality (M d1) (M d2) ε1 0 ∧ DP_inequality (M d2) (M d1) ε1 0"
and a2: "∀(d2, d3)∈ adj2. DP_inequality (M d2) (M d3) ε2 0 ∧ DP_inequality (M d3) (M d2) ε2 0"
and "x ∈ (adj1 O adj2)"
then obtain d1 d2 d3
where x: "x = (d1,d3)"and a: "(d1,d2) ∈Restr adj1 (space X) "and b: "(d2,d3) ∈Restr adj2 (space X) "
using assms by blast
then have "DP_inequality (M d1) (M d2) ε1 0" "DP_inequality (M d2) (M d1) ε1 0" "DP_inequality (M d2) (M d3) ε2 0" "DP_inequality (M d3) (M d2) ε2 0"
using a1 a2 by auto
moreover have "M d1 ∈ space (prob_algebra R)" "M d2 ∈ space (prob_algebra R)" "M d3 ∈ space (prob_algebra R)"
using a b by(auto intro!: measurable_space[OF M])
ultimately have 1: "DP_inequality (M d1) (M d3) (ε1 + ε2) 0" and "DP_inequality (M d3) (M d1) (ε2 + ε1) 0"
unfolding DP_inequality_cong_DP_divergence zero_ereal_def[symmetric] by(intro DP_divergence_transitivity[of _ "(M d2)"],auto)+
hence "DP_inequality (M d3) (M d1) (ε1 + ε2) 0"
by argo
with 1 show "case x of (d1, d2) ⇒ DP_inequality (M d1) (M d2) (ε1 + ε2) 0 ∧ DP_inequality (M d2) (M d1) (ε1 + ε2) 0"
unfolding x case_prod_beta by auto
qed
lemma adj_trans_k:
assumes "adj ⊆ A × A"
and "0 < k"
shows "(adj ^^ k) ⊆ A × A"
using assms(2) by (induction k)(use assms(1) in fastforce)+
lemma pure_differential_privacy_trans_k:
assumes "adj ⊆ (space X) × (space X)"
and "differential_privacy M adj ε 0"
and M[measurable]:"M ∈ X →⇩M (prob_algebra R)"
shows "differential_privacy M (adj ^^ k) (k * ε) 0"
proof(induction k)
case 0
then show ?case
by(auto simp: differential_privacy_adj_sym sym_on_def DP_divergence_reflexivity DP_inequality_cong_DP_divergence)
next
case (Suc k)
then show ?case
proof(cases k)
case 0
then show ?thesis
using assms(1) assms(2) inf.orderE mult_eq_1_iff by fastforce
next
case (Suc l)
then have 1: "0 < k"
by auto
have 2: "((Suc k) * ε) = (k * ε) + ε "
by (simp add: mult.commute nat_distrib(2))
show ?thesis
unfolding relpow.simps 2
proof(subst pure_differential_privacy_comp[where X = X and R = R])
show "adj ^^ k ⊆ space X × space X"
by(unfold Suc, rule adj_trans_k, auto simp: assms)
qed(auto simp: assms Suc.IH)
qed
qed
paragraph ‹The relaxation of parameters (obvious in the pencil and paper manner).›
lemma DP_inequality_relax:
assumes 1: "ε ≤ ε'" and 2: "δ ≤ δ'"
and DP: "DP_inequality M N ε δ"
shows "DP_inequality M N ε' δ'"
unfolding DP_inequality_def
proof
fix A assume A: "A ∈ sets M "
hence "measure M A ≤ exp ε * measure N A + δ"
using DP by(auto simp: DP_inequality_def)
also have "... ≤ exp ε' * measure N A + δ'"
by (auto simp: add_mono mult_right_mono 1 2)
finally show "measure M A ≤ exp ε' * measure N A + δ'".
qed
proposition differential_privacy_relax:
assumes DP:"differential_privacy M adj ε δ"
and 1: "ε ≤ ε'"and 2: "δ ≤ δ'"
shows "differential_privacy M adj ε' δ'"
using DP DP_inequality_relax [OF 1 2] unfolding differential_privacy_def by blast
paragraph ‹Stability for post-processing (cf. [Prop 2.1, AFDP])›
proposition differential_privacy_postprocessing:
assumes "ε ≥ 0"
and "differential_privacy M adj ε δ"
and M: "M ∈ X →⇩M (prob_algebra R)"
and f: "f ∈ R →⇩M (prob_algebra R')"
and "adj ⊆ (space X) × (space X)"
shows "differential_privacy (λx. do{y ← M x; f y}) adj ε δ"
proof(subst differential_privacy_def)
note [measurable] = M f
note [arith] = assms(1)
show "∀(d1, d2)∈ adj. DP_inequality (M d1 ⤜ f) (M d2 ⤜ f) ε δ ∧ DP_inequality (M d2 ⤜ f) (M d1 ⤜ f) ε δ "
proof
fix x ::"'a × 'a"assume x:"x ∈ adj"
then obtain d1 d2 ::'a
where x: "x = (d1,d2)"
and d1: "d1 ∈ space X"
and d2: "d2 ∈ space X"
and d: "(d1,d2) ∈ Restr adj (space X)"
and div1[simp]: "DP_divergence (M d1) (M d2) ε ≤ δ "
and div2[simp]: "DP_divergence (M d2) (M d1) ε ≤ δ"
using DP_inequality_cong_DP_divergence assms differential_privacy_def[of M adj ε δ] by fastforce+
hence Md1[simp]: "M d1 ∈ space (prob_algebra R)"and Md2[simp]: "M d2 ∈ space (prob_algebra R)"
by(metis M measurable_space)+
have "DP_divergence (M d1 ⤜ f) (M d2 ⤜ f) ε ≤ δ"
by(auto simp: DP_divergence_postprocessing[where L = R and K = R'])
moreover have "DP_divergence (M d2 ⤜ f) (M d1 ⤜ f) ε ≤ δ"
by(auto simp: DP_divergence_postprocessing[where L = R and K = R'])
ultimately show "case x of (d1,d2) ⇒ DP_inequality (M d1 ⤜ f) (M d2 ⤜ f) ε δ ∧ DP_inequality (M d2 ⤜ f) (M d1 ⤜ f) ε δ"
unfolding DP_inequality_cong_DP_divergence using x by auto
qed
qed
corollary differential_privacy_postprocessing_deterministic:
assumes "ε ≥ 0"
and "differential_privacy M adj ε δ"
and M[measurable]: "M ∈ X →⇩M (prob_algebra R)"
and f[measurable]: "f ∈ R →⇩M R'"
and "adj ⊆ (space X) × (space X)"
shows "differential_privacy (λx. do{y ← M x; return R' (f y) } ) adj ε δ"
by(rule differential_privacy_postprocessing[where f = "(λ y. return R' (f y))"and X = X and R = R and R'= R'],auto simp: assms)
text ‹ To handle the sensitivity, we prepare the conversions of adjacency relations by pre-processing. ›
lemma differential_privacy_preprocessing:
assumes "ε ≥ 0"
and "differential_privacy M adj ε δ"
and f: "f ∈ X' →⇩M X"
and ftr: "∀(x,y) ∈ adj'. (f x, f y) ∈ adj"
and "adj ⊆ (space X) × (space X)"
and "adj' ⊆ (space X') × (space X')"
shows "differential_privacy (M o f) adj' ε δ"
proof(subst differential_privacy_def)
note [measurable] = f
show "∀(d1, d2)∈ adj'. DP_inequality ((M ∘ f) d1) ((M ∘ f) d2) ε δ ∧ DP_inequality ((M ∘ f) d2) ((M ∘ f) d1) ε δ"
proof
fix x ::"'c × 'c"assume x:"x ∈ adj'"
then obtain d1 d2 ::'c where x: "x = (d1,d2)"and d1: "d1 ∈ space X'"and d2: "d2 ∈ space X'"and d: "(d1,d2) ∈ Restr adj' (space X')"
using assms by auto
hence fd: "(f d1, f d2) ∈ adj"
using ftr by auto
hence "DP_inequality (M (f d1)) (M (f d2)) ε δ ∧ DP_inequality (M (f d2)) (M (f d1)) ε δ"
using differential_privacy_def[of M adj ε δ] assms by blast
thus "case x of (d1,d2) ⇒ DP_inequality ((M o f) d1) ((M o f) d2) ε δ ∧ DP_inequality ((M o f) d2) ((M o f) d1) ε δ"
using x by auto
qed
qed
paragraph ‹ "Adaptive"composition (cf. [Theorem B.1, AFDP])›
proposition differential_privacy_composition_adaptive:
assumes "ε ≥ 0"
and "ε' ≥ 0"
and M: "M ∈ X →⇩M (prob_algebra Y)"
and DPM: "differential_privacy M adj ε δ"
and N: "N ∈ (X ⨂⇩M Y) →⇩M (prob_algebra Z)"
and DPN: "∀ y ∈ space Y. differential_privacy (λ x. N (x,y)) adj ε' δ'"
and "adj ⊆ (space X) × (space X)"
shows "differential_privacy (λx. do{y ← M x; N (x, y)}) adj (ε + ε') (δ + δ')"
proof(subst differential_privacy_def)
note [measurable] = M N
note [simp] = space_pair_measure
show "∀(d1, d2)∈adj.
DP_inequality (M d1 ⤜ (λy. N (d1, y))) (M d2 ⤜ (λy. N (d2, y))) (ε + ε') (δ + δ') ∧
DP_inequality (M d2 ⤜ (λy. N (d2, y))) (M d1 ⤜ (λy. N (d1, y))) (ε + ε') (δ + δ') "
proof
fix x ::"'a × 'a"
assume x:"x ∈ adj"
then obtain x1 x2 ::'a
where x: "x = (x1,x2)"
and x1: "x1 ∈ space X"
and x2: "x2 ∈ space X"
and x': "(x1,x2) ∈ Restr adj (space X)"
and div1: "DP_divergence (M x1) (M x2) ε ≤ δ "
and div2: "DP_divergence (M x2) (M x1) ε ≤ δ"
using DP_inequality_cong_DP_divergence assms differential_privacy_def[of M adj ε δ] by fastforce+
hence N1: "(λy. N (x1, y)) ∈ Y →⇩M prob_algebra Z"and N2: "(λy. N (x2, y)) ∈ Y →⇩M prob_algebra Z"
by auto
have Mx1: "(M x1)∈ space(prob_algebra Y)"and Mx2: "(M x2)∈ space(prob_algebra Y)"
by (meson measurable_space M x1 x2)+
{
fix y::'b assume y: "y ∈ space Y"
have "DP_divergence (N (x1, y)) (N (x2, y)) ε' ≤ δ' ∧ DP_divergence (N (x2, y)) (N (x1, y)) ε' ≤ δ'"
using DPN DP_inequality_cong_DP_divergence differential_privacy_def[of "(λ x. N (x,y))"adj ε' δ'] x1 x2 x' y by fastforce+
}
hence p1: "∀y ∈ space Y. DP_divergence (N (x1, y)) (N (x2, y)) ε' ≤ δ'"and p2: "∀y ∈ space Y. DP_divergence (N (x2, y)) (N (x1, y)) ε' ≤ δ'"
by auto
hence "DP_divergence ( M x1 ⤜ (λy. N (x1, y))) ( M x2 ⤜ (λy. N (x2, y))) (ε + ε') ≤ (δ + δ') ∧ DP_divergence ( M x2 ⤜ (λy. N (x2, y))) ( M x1 ⤜ (λy. N (x1, y))) (ε + ε') ≤ (δ + δ')"
using DP_divergence_composability[of "M x1 "Y "M x2 ""(λy. N (x1, y))"Z "(λy. N (x2, y))"ε δ ε' δ' ,OF Mx1 Mx2 N1 N2 div1 _ assms(1,2)]
DP_divergence_composability[of "M x2 "Y "M x1 ""(λy. N (x2, y))"Z "(λy. N (x1, y))"ε δ ε' δ' ,OF Mx2 Mx1 N2 N1 div2 _ assms(1,2)] by auto
thus "case x of (x1,x2) ⇒ DP_inequality ( M x1 ⤜ (λy. N (x1, y))) ( M x2 ⤜ (λy. N (x2, y))) (ε + ε') (δ + δ') ∧ DP_inequality ( M x2 ⤜ (λy. N (x2, y))) ( M x1 ⤜ (λy. N (x1, y))) (ε + ε') (δ + δ')"
by (auto simp: x DP_inequality_cong_DP_divergence)
qed
qed
paragraph ‹ "Sequential"composition [Theorem 3.14, AFDP, generalized] ›
proposition differential_privacy_composition_pair:
assumes "ε ≥ 0"
and "ε' ≥ 0"
and DPM: "differential_privacy M adj ε δ"
and M[measurable]: "M ∈ X →⇩M (prob_algebra Y)"
and DPN: "differential_privacy N adj ε' δ'"
and N[measurable]: "N ∈ X →⇩M (prob_algebra Z)"
and "adj ⊆ (space X) × (space X)"
shows "differential_privacy (λx. do{y ← M x; z ← N x; return (Y ⨂⇩M Z) (y,z)} ) adj (ε + ε') (δ + δ')"
proof-
have p: "(λx. do{y ← M x; z ← N x; return (Y ⨂⇩M Z) (y,z)} ) = (λx. M x ⤜ (λy. case (x, y) of (x, y) ⇒ N x ⤜ (λz. return (Y ⨂⇩M Z) (y, z))))"
by auto
have "⋀y. y ∈ space Y ⟹ differential_privacy (λx. N x ⤜ (λz. return (Y ⨂⇩M Z) (y, z))) adj ε' δ'"
proof-
fix y assume [measurable]: "y ∈ space Y"
hence m: "(λx. N x ⤜ (λz. return (Y ⨂⇩M Z) (y, z))) ∈ X →⇩M prob_algebra (Y ⨂⇩M Z)"
by auto
show "differential_privacy (λx. N x ⤜ (λz. return (Y ⨂⇩M Z) (y, z))) adj ε' δ'"
by(rule differential_privacy_postprocessing[where f = "(λz. return (Y ⨂⇩M Z) (y, z))" and R' = "(Y ⨂⇩M Z)" and R = "Z" and X = X], auto simp: assms)
qed
thus ?thesis unfolding p using assms
by(subst differential_privacy_composition_adaptive[where N ="(λ(x,y). N x ⤜ (λz. return (Y ⨂⇩M Z) (y, z)) )"and Z = "(Y ⨂⇩M Z)"], auto )
qed
paragraph ‹ Laplace mechanism (1-dimensional version) (cf. [Def. 3.3 and Thm 3.6, AFDP]) ›
locale Lap_Mechanism_1dim =
fixes X::"'a measure"
and f::"'a ⇒ real"
and adj::"('a rel)"
assumes [measurable]: "f ∈ X →⇩M borel"
and adj: "adj ⊆ (space X) × (space X)"
begin
definition sensitivity:: ereal where
"sensitivity = Sup{ ereal ¦(f x) - (f y)¦ | x y::'a. x ∈ space X ∧ y ∈ space X ∧ (x,y) ∈ adj }"
definition LapMech_1dim::"real ⇒ 'a ⇒ real measure"where
"LapMech_1dim ε x = Lap_dist ((real_of_ereal sensitivity) / ε) (f x)"
lemma measurable_LapMech_1dim[measurable]:
shows "LapMech_1dim ε ∈ X →⇩M prob_algebra borel"
unfolding LapMech_1dim_def by auto
lemma LapMech_1dim_def2:
shows "LapMech_1dim ε x = do{y ← Lap_dist0 ((real_of_ereal sensitivity) / ε); return borel (f x + y) }"
using Lap_dist_def2 LapMech_1dim_def by auto
proposition differential_privacy_LapMech_1dim:
assumes pose: "0 < ε "and "sensitivity > 0"and "sensitivity < ∞"
shows "differential_privacy (LapMech_1dim ε) adj ε 0"
proof(subst differential_privacy_def)
show "∀(d1::'a, d2::'a)∈adj.
DP_inequality (LapMech_1dim ε d1) (LapMech_1dim ε d2) ε (0::real) ∧
DP_inequality (LapMech_1dim ε d2) (LapMech_1dim ε d1) ε (0::real)"
proof
fix x::"'a × 'a"assume "x ∈ adj"
then obtain d1 d2 where x: "x = (d1,d2)"and "(d1,d2) ∈ adj "and "d1 ∈ (space X)"and "d2 ∈ (space X)"
using adj by blast
with assms have "¦(f d1) - (f d2)¦ ≤ sensitivity "
unfolding sensitivity_def using le_Sup_iff by blast
with assms have q: "¦(f d1) - (f d2)¦ ≤ real_of_ereal sensitivity"
by (auto simp: ereal_le_real_iff)
hence q2: "¦(f d2) - (f d1)¦ ≤ real_of_ereal sensitivity"
by auto
from assms have pos: "0 < (real_of_ereal sensitivity)/ε"
by (auto simp: zero_less_real_of_ereal)
have a1: "DP_inequality (LapMech_1dim (ε::real) d1) (LapMech_1dim ε d2) ε (0::real)"
by (auto simp: DP_divergence_Lap_dist'_eps pose q DP_inequality_cong_DP_divergence LapMech_1dim_def )
have a2: "DP_inequality (LapMech_1dim (ε::real) d2) (LapMech_1dim ε d1) ε (0::real)"
by (auto simp: DP_divergence_Lap_dist'_eps pose q2 DP_inequality_cong_DP_divergence LapMech_1dim_def )
from a1 a2 show "case x of
(d1::'a, d2::'a) ⇒
DP_inequality (LapMech_1dim ε d1) (LapMech_1dim ε d2) ε (0::real) ∧
DP_inequality (LapMech_1dim ε d2) (LapMech_1dim ε d1) ε (0::real)"
by(auto simp:x)
qed
qed
end
paragraph ‹ Laplace mechanism (generalized version) (cf. [Def. 3.3 and Thm 3.6, AFDP]) ›
locale Lap_Mechanism_list =
fixes X::"'a measure"
and f::"'a ⇒ real list"
and adj::"('a rel)"
and m::nat
assumes [measurable]: "f ∈ X →⇩M (listM borel)"
and len: "⋀ x. x ∈ space X ⟹ length (f x) = m"
and adj: "adj ⊆ (space X) × (space X)"
begin
definition sensitivity:: ereal where
"sensitivity = Sup{ ereal ( ∑ i∈{1..m}. ¦ nth (f x) (i-1) - nth (f y) (i-1) ¦) | x y::'a. x ∈ space X ∧ y ∈ space X ∧ (x,y) ∈ adj}"
definition LapMech_list::"real ⇒ 'a ⇒ (real list) measure"where
"LapMech_list ε x = Lap_dist_list ((real_of_ereal sensitivity) / ε) (f x)"
lemma LapMech_list_def2:
assumes "x ∈ space X"
shows "LapMech_list ε x = do{ xs ← Lap_dist0_list (real_of_ereal sensitivity / ε) m; return (listM borel) (map2 (+) (f x) xs)}"
using Lap_dist_list_def2 len[OF assms] LapMech_list_def by auto
proposition differential_privacy_LapMech_list:
assumes pose: "ε > 0"
and "sensitivity > 0"
and "sensitivity < ∞"
shows "differential_privacy (LapMech_list ε) adj ε 0"
proof(subst differential_privacy_def)
show "∀(d1, d2)∈ adj. DP_inequality (LapMech_list ε d1) (LapMech_list ε d2) ε 0
∧ DP_inequality (LapMech_list ε d2) (LapMech_list ε d1) ε 0"
proof(rule ballI)
fix x::"'a × 'a"assume "x ∈ adj"
then obtain d1 d2::'a
where x: "x = (d1,d2)"
and "(d1,d2) ∈ adj "
and d1: "d1 ∈ (space X)"
and d2: "d2 ∈ (space X)"
using adj by blast
with assms have "(∑ i∈{1..m}. ¦ nth (f d1) (i-1) - nth (f d2) (i-1) ¦) ≤ sensitivity "
unfolding sensitivity_def using le_Sup_iff by blast
with assms have q: "(∑ i∈{1..m}. ¦ nth (f d1) (i-1) - nth (f d2) (i-1) ¦) ≤ real_of_ereal sensitivity"
by (auto simp: ereal_le_real_iff)
hence q2: "(∑ i∈{1..m}. ¦ nth (f d2) (i-1) - nth (f d1) (i-1) ¦) ≤ real_of_ereal sensitivity"
by (simp add: abs_minus_commute)
from assms have pos: "0 ≤ (real_of_ereal sensitivity)"
by (simp add: real_of_ereal_pos)
have fd1: "length (f d1) = m"and fd2: "length (f d2) = m"
using len d1 d2 by auto
have a1: "DP_inequality (LapMech_list (ε::real) d1) (LapMech_list ε d2) ε 0"
using DP_Lap_dist_list_eps[OF pose fd1 fd2 q pos] by (simp add: LapMech_list_def DP_inequality_cong_DP_divergence zero_ereal_def)
have a2: "DP_inequality (LapMech_list (ε::real) d2) (LapMech_list ε d1) ε 0"
using DP_Lap_dist_list_eps[OF pose fd2 fd1 q2 pos] by (simp add: LapMech_list_def DP_inequality_cong_DP_divergence zero_ereal_def)
show "case x of (d1, d2) ⇒ DP_inequality (local.LapMech_list ε d1) (local.LapMech_list ε d2) ε 0 ∧ DP_inequality (local.LapMech_list ε d2) (local.LapMech_list ε d1) ε 0"
by(auto simp:x a1 a2 )
qed
qed
end
subsection ‹ Formalization of Results in [AFDP]›
text‹We finally instantiate @{term X} and @{term adj} according to the textbook [AFDP] ›
locale results_AFDP =
fixes n ::nat
begin
interpretation L1_norm_list "(UNIV::nat set)" "(λ x y. ¦int x - int y¦)" n
by(unfold_locales,auto)
definition sp_Dataset :: "nat list measure"where
"sp_Dataset ≡ restrict_space (listM (count_space UNIV)) space_L1_norm_list"
definition adj_L1_norm :: "(nat list × nat list) set"where
"adj_L1_norm ≡ {(xs,ys)| xs ys. xs ∈ space sp_Dataset ∧ ys ∈ space sp_Dataset ∧ dist_L1_norm_list xs ys ≤ 1}"
definition dist_L1_norm :: "nat ⇒ (nat list × nat list) set"where
"dist_L1_norm k ≡ {(xs,ys)| xs ys. xs ∈ space sp_Dataset ∧ ys ∈ space sp_Dataset ∧ dist_L1_norm_list xs ys ≤ k}"
abbreviation
"differential_privacy_AFDP M ε δ ≡ differential_privacy M adj_L1_norm ε δ"
lemma adj_sub: "adj_L1_norm ⊆ space sp_Dataset × space sp_Dataset"
unfolding sp_Dataset_def adj_L1_norm_def by blast
lemmas differential_privacy_relax_AFDP' =
differential_privacy_relax[of _ adj_L1_norm]
lemmas differential_privacy_postprocessing_AFDP =
differential_privacy_postprocessing[of _ _ adj_L1_norm, OF _ _ _ _ adj_sub]
lemmas differential_privacy_composition_adaptive_AFDP =
differential_privacy_composition_adaptive[of _ _ _ _ _ adj_L1_norm, OF _ _ _ _ _ _ adj_sub]
lemmas differential_privacy_composition_pair_AFDP =
differential_privacy_composition_pair[of _ _ _ adj_L1_norm, OF _ _ _ _ _ _ adj_sub]
text‹Group privacy [Theorem 2.2, AFDP].›
lemma group_privacy_AFDP:
assumes M: "M ∈ sp_Dataset →⇩M prob_algebra Y"
and DP: " differential_privacy_AFDP M ε 0"
shows "differential_privacy M (dist_L1_norm k) (real k * ε) 0"
proof(rule differential_privacy_restrict[where adj = "adj_L1_norm ^^ k"and adj' = "dist_L1_norm k"])
show "differential_privacy M (adj_L1_norm ^^ k) (real k * ε) 0"
by(rule pure_differential_privacy_trans_k[OF adj_sub DP M])
show "dist_L1_norm k ⊆ adj_L1_norm ^^ k"
using L1_adj_iterate[of _ n _ k] unfolding space_restrict_space space_listM space_count_space lists_UNIV adj_L1_norm_def dist_L1_norm_def sp_Dataset_def by auto
qed
context
fixes f::"nat list ⇒ real"
assumes [measurable]: "f ∈ sp_Dataset →⇩M borel"
begin
interpretation Lap_Mechanism_1dim "sp_Dataset"f "adj_L1_norm"
by(unfold_locales,auto simp: adj_sub)
thm LapMech_1dim_def
definition LapMech_1dim_AFDP :: "real ⇒ nat list ⇒ real measure"where
"LapMech_1dim_AFDP ε x = do{y ← Lap_dist0 ((real_of_ereal sensitivity) / ε); return borel (f x + y) }"
lemma LapMech_1dim_AFDP':
shows "LapMech_1dim_AFDP = LapMech_1dim"
unfolding LapMech_1dim_AFDP_def LapMech_1dim_def2 by auto
lemmas differential_privacy_Lap_Mechanism_1dim_AFDP =
differential_privacy_LapMech_1dim[of _ , simplified LapMech_1dim_AFDP'[symmetric]]
end
context
fixes f::"nat list ⇒ real list"
and m::nat
assumes [measurable]: "f ∈ sp_Dataset →⇩M (listM borel)"
and len: "⋀ x. x ∈ space X ⟹ length (f x) = m"
begin
interpretation Lap_Mechanism_list "sp_Dataset"f "adj_L1_norm" m
by(unfold_locales,auto simp: len adj_sub)
definition LapMech_list_AFDP :: "real ⇒ nat list ⇒ real list measure"where
"LapMech_list_AFDP ε x = do{ ys ← (Lap_dist0_list(real_of_ereal sensitivity / ε) m); return (listM borel) (map2 (+) (f x) ys) }"
thm LapMech_list_def
lemma LapMech_list_AFDP':
assumes "x ∈ space sp_Dataset"
shows "LapMech_list_AFDP ε x = LapMech_list ε x"
unfolding LapMech_list_AFDP_def LapMech_list_def2[OF assms] by auto
lemma differential_privacy_Lap_Mechanism_list_AFDP:
assumes "0 < ε"
and "0 < sensitivity"
and "sensitivity < ∞"
shows "differential_privacy_AFDP (LapMech_list_AFDP ε) ε 0"
proof(subst differential_privacy_def)
{
fix d1 d2 assume d: "(d1, d2)∈ adj_L1_norm"
then have 1: "d1 ∈ (space sp_Dataset)"and 2: "d2 ∈ (space sp_Dataset)"
using adj_sub by auto
have "DP_inequality (LapMech_list_AFDP ε d1) (LapMech_list_AFDP ε d2) ε 0 ∧ DP_inequality (LapMech_list_AFDP ε d2) (LapMech_list_AFDP ε d1) ε 0"
using differential_privacy_LapMech_list[OF assms(1)] assms(2,3) d
unfolding LapMech_list_AFDP'[OF 1] LapMech_list_AFDP'[OF 2] differential_privacy_def by blast
}
thus "∀(d1, d2)∈ adj_L1_norm. DP_inequality (LapMech_list_AFDP ε d1) (LapMech_list_AFDP ε d2) ε 0 ∧ DP_inequality (LapMech_list_AFDP ε d2) (LapMech_list_AFDP ε d1) ε 0"
by blast
qed
end
end
end