Theory Differential_Privacy_Laplace_Mechanism
theory Differential_Privacy_Laplace_Mechanism
imports"Differential_Privacy_Divergence"
"Laplace_Distribution"
begin
section ‹Laplace mechanism ›
subsection ‹Laplace mechanism as a noise-adding mechanism›
subsubsection ‹Laplace distribution with scale ‹b› and average ‹μ››
definition Lap_dist :: "real ⇒ real ⇒ real measure" where
"Lap_dist b μ = (if b ≤ 0 then return borel μ else density lborel (laplace_density b μ))"
lemma shows prob_space_Lap_dist[simp,intro]: "prob_space (Lap_dist b x)"
and subprob_space_Lap_dist[simp,intro]: "subprob_space (Lap_dist b x)"
and sets_Lap_dist[measurable_cong]: "sets (Lap_dist b x) = sets borel"
and space_Lap_dist: "space (Lap_dist ε x) = UNIV"
using prob_space_laplacian_density prob_space_return[of x borel] prob_space_imp_subprob_space sets_eq_imp_space_eq Lap_dist_def
by(cases "b ≤ 0",auto)
lemma measurable_Lap_dist[measurable]:
shows "Lap_dist b ∈ borel →⇩M prob_algebra borel"
proof(cases"b ≤ 0")
case True
then show ?thesis unfolding Lap_dist_def by auto
next
case False
thus ?thesis
proof(intro measurable_prob_algebraI)
show " ⋀x. x ∈ space borel ⟹ prob_space (Lap_dist b x)"
by auto
show "Lap_dist b ∈ borel →⇩M subprob_algebra borel"
proof(rule measurable_subprob_algebra_generated[where Ω=UNIV and G="(range (λ a :: real. {..a}))"])
show pow1: "(range (λ a :: real. {..a})) ⊆ Pow UNIV"
by auto
show "sets borel = sigma_sets UNIV (range (λ a :: real. {..a}))"
using borel_eq_atMost by (metis pow1 sets_measure_of)
show "Int_stable (range (λ a :: real. {..a}))"
by(subst Int_stable_def,auto)
show "⋀a. a ∈ space borel ⟹ subprob_space (Lap_dist b a)"
by (auto simp: prob_space_imp_subprob_space)
show "⋀a. a ∈ space borel ⟹ sets (Lap_dist b a) = sets borel"
by (auto simp: sets_Lap_dist)
show "⋀A. A ∈ range atMost ⟹ (λa. emeasure (Lap_dist b a) A) ∈ borel →⇩M borel"
proof(safe,unfold Lap_dist_def)
fix x :: real assume "x ∈ UNIV"
have "(λa :: real. emeasure (density lborel (λx :: real. ennreal (laplace_density b a x))) {..x}) = (λa. laplace_CDF b a x)"
using emeasure_laplace_density False by auto
also have "... ∈ borel →⇩M borel"
using borel_measurable_laplace_CDF2 by auto
finally show "(λa :: real. emeasure (if b ≤ (0 :: real) then return borel a else density lborel (λx :: real. ennreal (laplace_density b a x))) {..x}) ∈ borel →⇩M borel"
using False by auto
qed
have "(λa. emeasure (Lap_dist b a) UNIV) = (λa. 1)"
using Lap_dist_def emeasure_laplace_density_mass_1 by auto
thus "(λa. emeasure (Lap_dist b a) UNIV) ∈ borel →⇩M borel"
by auto
qed
qed
qed
lemma Lap_dist_space_prob_algebra[simp,measurable]:
shows "(Lap_dist b x) ∈ space (prob_algebra borel)"
by (metis iso_tuple_UNIV_I measurable_Lap_dist measurable_space space_borel)
lemma Lap_dist_space_subprob_algebra[simp,measurable]:
shows "(Lap_dist b x) ∈ space (subprob_algebra borel)"
by (metis UNIV_I measurable_Lap_dist measurable_prob_algebraD measurable_space space_borel)
subsubsection ‹ The Laplace distribution with scale ‹b› and average ‹0››
definition "Lap_dist0 b ≡ Lap_dist b 0 "
text ‹ Actually @{term "Lap_dist b" } is a noise-addition of Laplace distribution with scale ‹b› and average ‹0›.›
lemma shows prob_space_Lap_dist0[simp,intro,measurable]: "prob_space (Lap_dist0 b)"
and subprob_space_Lap_dist0[simp,intro,measurable]: "subprob_space (Lap_dist0 b)"
and sets_Lap_dist0[measurable_cong]: "sets (Lap_dist0 b) = sets borel"
and space_Lap_dist0: "space (Lap_dist0 b) = UNIV"
and Lap_dist0_space_prob_algebra[simp,measurable]: "(Lap_dist0 b) ∈ space (prob_algebra borel)"
and Lap_dist0_space_subprob_algebra[simp,measurable]: "(Lap_dist0 b) ∈ space (subprob_algebra borel)"
unfolding Lap_dist0_def by(auto simp:sets_Lap_dist space_Lap_dist)
lemma Lap_dist_def2:
shows "(Lap_dist b x) = do{r ← Lap_dist0 b; return borel (x + r)}"
proof-
show " Lap_dist b x = Lap_dist0 b ⤜ (λr. return borel (x + r))"
proof(cases"b ≤ 0")
case True
hence " Lap_dist b x = return borel x"
by(auto simp: Lap_dist_def)
also have "... = return borel 0 ⤜ (λr. return borel (x + r))"
by(subst bind_return, measurable)
also have "... = do{r ← Lap_dist0 b; return borel (x + r)}"
by(auto simp: Lap_dist0_def Lap_dist_def True)
finally show ?thesis.
next
case False
hence "(Lap_dist b x) = density lborel (laplace_density b x)"
by(auto simp: Lap_dist_def)
also have "... = density ( distr lborel borel ((+) x)) (laplace_density b x) "
by(auto simp: Lebesgue_Measure.lborel_distr_plus[of x])
also have "... = (density lborel (laplace_density b 0)) ⤜ (λr. return borel (x + r))"
proof(subst bind_return_distr')
show " density (distr lborel borel ((+) x)) (λxa. ennreal (laplace_density b x xa)) =
distr (density lborel (λx. ennreal (laplace_density b 0 x))) borel ((+) x)"
proof(subst density_distr)
show "distr (density lborel (λxa. ennreal (laplace_density b x (x + xa)))) borel ((+) x) =
distr (density lborel (λx. ennreal (laplace_density b 0 x))) borel ((+) x)"
using laplace_density_shift[of b "0::real" x ] by (auto simp: add.commute)
qed(auto)
qed(auto)
also have "... = do{r ← Lap_dist0 b; return borel (x + r)}"
by(auto simp: Lap_dist_def Lap_dist0_def False)
finally show ?thesis.
qed
qed
corollary Lap_dist_shift:
shows "(Lap_dist b (x + y)) = do{r ← Lap_dist b x; return borel (y + r)}"
unfolding Lap_dist_def2
by(subst bind_assoc[where N = borel and R = borel],auto simp: bind_return[where N = borel] Lap_dist0_def ac_simps)
subsubsection ‹Differential Privacy of Laplace noise addition ›
proposition DP_divergence_Lap_dist':
assumes "b > 0"
and "¦ x - y ¦ ≤ r"
shows "DP_divergence (Lap_dist b x) (Lap_dist b y) (r / b) ≤ (0 :: real)"
proof(cases"r = 0")
case True
hence 0:"x = y"
using assms(2) by auto
have "DP_divergence (Lap_dist b x) (Lap_dist b y) (r / b) ≤ (0 :: real)"
by (auto simp: DP_divergence_reflexivity True 0)
thus ?thesis by argo
next
case False
hence posr: "r > 0"using assms(2) by auto
show "DP_divergence (Lap_dist b x) (Lap_dist b y) (r / b) ≤ ereal 0"
proof(intro DP_divergence_leI,unfold Lap_dist_def)
fix A :: "real set" assume " A ∈ sets (if b ≤ 0 then return borel x else density lborel (λs. ennreal (laplace_density b x s))) "
hence A[measurable]: "A ∈ sets borel"
using assms by (metis (mono_tags, lifting) sets_density sets_lborel sets_return)
have pos[simp]: "b > 0"
using posr assms by auto
hence nonneg[simp]: "b ≥ 0"
by argo
have "Sigma_Algebra.measure (if b ≤ 0 then return borel x else density lborel (λxa. ennreal (laplace_density b x xa))) A =
(Sigma_Algebra.emeasure (density lborel (λxa. ennreal (laplace_density b x xa))) A)"
using pos by(split if_split, intro conjI impI, linarith) (metis emeasure_eq_ennreal_measure emeasure_laplace_density_mass_1 emeasure_mono ennreal_one_less_top leD pos sets_density sets_lborel space_in_borel top_greatest)
also have "... = (∫⇧+ z. ennreal (laplace_density b x z) * indicator A z ∂lborel)"
by(rule emeasure_density,auto intro: A)
also have "... ≤ (∫⇧+ z. (exp (r / b)) * ennreal (laplace_density b y z) * indicator A z ∂lborel)"
proof(rule nn_integral_mono)
fix z :: real assume z: "z ∈space lborel"
have 0: "-¦z - x¦ ≤ r - ¦z - y¦"
using assms(2) posr by auto
hence 1: " exp (- ¦z - x¦ / b ) ≤exp (( r - ¦z - y ¦)/ b) "
by(subst exp_le_cancel_iff, intro divide_right_mono, auto)
have "ennreal (laplace_density b x z) = exp (- ¦z - x¦ / b ) / (2 * b)"
by(auto simp: laplace_density_def z)
also have "... ≤ exp (( r - ¦z - y ¦) / b ) / (2 * b)"
proof(subst ennreal_le_iff)
show "0 ≤ exp ((r - ¦z - y¦) / b) / (2 * b)"
by auto
show " exp (- ¦z - x¦ / b) / (2 * b) ≤ exp ((r - ¦z - y¦) / b) / (2 * b)"
by(subst divide_right_mono, rule 1,auto)
qed
also have "... = exp (- ¦z - y ¦/ b + r / b ) / (2 * b)"
by argo
also have "... = (exp (- ¦z - y ¦/ b) * exp ( r / b )) / (2 * b)"
using exp_add[of "- ¦z - y ¦/ b" " r / b"] by auto
also have "... = exp ( r / b) * (exp (- ¦z - y ¦/ b)) / (2 * b)"
by argo
also have "... = exp (r / b) * (laplace_density b y z)"
by(auto simp: laplace_density_def)
finally have "ennreal (laplace_density b x z) ≤ ennreal (exp (r / b) * laplace_density b y z)" .
thus "ennreal (laplace_density b x z) * indicator A z ≤ ennreal (exp (r / b)) * ennreal (laplace_density b y z) * indicator A z"
by (simp add: ennreal_mult' mult_right_mono)
qed
also have "... = (∫⇧+ z. (exp (r / b)) * ( ennreal (laplace_density b y z) * indicator A z) ∂lborel)"
by (auto simp: mult.assoc)
also have "... = (exp (r / b)) * (∫⇧+ z. ennreal (laplace_density b y z) * indicator A z ∂lborel)"
by(rule nn_integral_cmult, auto)
also have "... = (exp (r / b)) * (Sigma_Algebra.emeasure (density lborel (λxa. ennreal (laplace_density b y xa))) A)"
by(subst emeasure_density,auto intro: A)
also have "... = ennreal (exp (r / b)) * ennreal (Sigma_Algebra.measure (if b ≤ 0 then return borel y else density lborel (λxa. ennreal (laplace_density b y xa))) A)"
using pos by(split if_split, intro conjI impI, linarith)(metis emeasure_eq_ennreal_measure emeasure_laplace_density_mass_1 emeasure_mono ennreal_one_less_top leD pos sets_density sets_lborel space_in_borel top_greatest)
also have "... = (exp (r / b)) * (Sigma_Algebra.measure (if b ≤ 0 then return borel y else density lborel (λxa. ennreal (laplace_density b y xa))) A)"
by (auto simp: ennreal_mult'')
finally show "measure (if b ≤ 0 then return borel x else density lborel (λxa. ennreal (laplace_density b x xa))) A
≤ exp (r / b) * measure (if b ≤ 0 then return borel y else density lborel (λx. ennreal (laplace_density b y x))) A + 0"
by auto
qed
qed
corollary DP_divergence_Lap_dist'_eps:
assumes "ε > 0"
and "¦ x - y ¦ ≤ r"
shows "DP_divergence (Lap_dist (r / ε) x) (Lap_dist (r / ε) y) ε ≤ (0 :: real)"
proof(cases "r = 0")
case True
with assms have 1: "x = y" and 2: " (r / ε) = 0"
by auto
thus ?thesis
unfolding 1 2 using DP_divergence_reflexivity'[of ε "Lap_dist 0 y" ] assms by auto
next
case False
with assms have 0: "0 < r" and 1: "0 < (r / ε)"
by auto
show ?thesis
using 0 DP_divergence_Lap_dist'[OF 1 assms(2)] by auto
qed
corollary DP_divergence_Lap_dist_eps:
assumes "ε > 0"
and "¦ x - y ¦ ≤ 1"
shows "DP_divergence (Lap_dist (1 / ε) x) (Lap_dist (1 / ε) y) ε ≤ (0 :: real)"
using DP_divergence_Lap_dist'_eps[of ε x y 1] assms by auto
end