Theory Differential_Privacy_Example_Report_Noisy_Max
theory Differential_Privacy_Example_Report_Noisy_Max
imports "Differential_Privacy_Standard"
begin
section ‹ Report Noisy Max mechanism for counting query with Laplace noise›
lemma measurable_let[measurable]:
assumes [measurable]: "g ∈ M →⇩M L"
and [measurable]: "(λ(x,y). f x y) ∈ M ⨂⇩M L →⇩M N"
shows "(λx. (Let (g x) (f x))) ∈ M →⇩M N"
unfolding Let_def by auto
subsection ‹ Formalization of argmax procedure›
primrec max_argmax :: "real list ⇒ (ereal × nat)" where
"max_argmax [] = (-∞,0)"|
"max_argmax (x#xs) = (let (m, i) = max_argmax xs in if x > m then (x,0) else (m, Suc i))"
value "max_argmax []"
value "max_argmax [1]"
value "max_argmax [2,1]"
value "max_argmax [1,2,3,4,5]"
value "max_argmax [1,5,2,3,4]"
value "([1,2,3,4,5]::int list) ! 4"
primrec max_argmax' :: "real list ⇒ (ereal × nat)" where
"max_argmax' [] = (-∞,0)"|
"max_argmax' (x#xs) = (if x > fst (max_argmax' xs) then (x,0) else (fst (max_argmax' xs),Suc (snd (max_argmax' xs))))"
lemma max_argmax_is_max_argmax':
shows "max_argmax xs = max_argmax' xs"
by(induction xs,auto simp: case_prod_beta)
lemma measurable_max_argmax[measurable]:
shows "max_argmax ∈ (listM (borel :: real measure)) →⇩M (borel :: (ereal measure)) ⨂⇩M count_space UNIV"
proof-
have 1: "(- ∞, 0) ∈ space (borel ⨂⇩M count_space UNIV)"
by (metis iso_tuple_UNIV_I measurable_Pair1' measurable_space space_borel space_count_space)
thus"max_argmax ∈ listM borel →⇩M (borel :: (ereal measure)) ⨂⇩M count_space UNIV"
unfolding max_argmax_def using measurable_rec_list''' 1 by measurable
qed
definition argmax_list :: "real list ⇒ nat" where
"argmax_list = snd o max_argmax "
lemma measurable_argmax_list[measurable]:
shows "argmax_list ∈ (listM (borel :: real measure)) →⇩M count_space UNIV"
by(unfold argmax_list_def, rule measurable_comp[where N = "(borel :: (ereal measure)) ⨂⇩M count_space UNIV"],auto)
lemma argmax_list_le_length:
shows "length xs = Suc k ⟹ (argmax_list xs) ≤ k"
proof(induction k arbitrary:xs)
case 0
then obtain x where xs: "xs = [x]"
by (metis length_0_conv length_Suc_conv)
then show ?case unfolding xs argmax_list_def comp_def max_argmax.simps by auto
next
case (Suc k)
then obtain y ys where xs: "xs = y # ys" and len:"length ys = Suc k"
by (meson length_Suc_conv)
from Suc.IH[of ys, OF len] obtain k' z where 1: "max_argmax ys = (z,k')" and 2: "k' ≤ k"
unfolding argmax_list_def comp_def by (metis prod.collapse)
then show ?case unfolding xs argmax_list_def comp_def max_argmax.simps 1 using 2 by auto
qed
lemma fst_max_argmax_append:
shows "(fst (max_argmax (xs @ ys))) = max (fst (max_argmax xs)) (fst (max_argmax ys))"
unfolding max_argmax_is_max_argmax' by(induction xs arbitrary: ys,auto)
lemma fst_max_argmax_is_max:
shows "fst (max_argmax xs) = Max (set xs ∪ {-∞})"
unfolding max_argmax_is_max_argmax'
proof(induction xs)
case Nil
then show ?case by auto
next
case (Cons a xs)
have 1: " Max (set (map ereal (a # xs)) ∪ {- ∞}) = max a (Max (set (map ereal xs) ∪ {- ∞}))"
by (simp add: Un_ac(3))
have "fst (max_argmax' (a # xs)) = ( if Max (set (map ereal xs) ∪ {- ∞}) < ereal a then (ereal a) else (Max (set (map ereal xs) ∪ {- ∞})))"
unfolding max_argmax'.simps Cons.IH by auto
also have "... = max a (Max (set (map ereal xs) ∪ {- ∞}))"
unfolding max_def
by (meson Metric_Arith.nnf_simps(8))
finally show ?case using 1 by auto
qed
lemma argmax_list_max_argmax:
assumes "xs ≠ []"
shows "(argmax_list xs) = m ⟷ max_argmax xs = (ereal (xs ! m), m)"
using assms proof(induction xs arbitrary: m)
case Nil
then show ?case by auto
next
case (Cons a xs)
then show ?case
proof(cases "xs = []")
case True
hence 1: "a # xs = [a]"
by auto
then show ?thesis unfolding 1 argmax_list_def comp_def max_argmax.simps by auto
next
case False
then show ?thesis
unfolding argmax_list_def comp_def max_argmax_is_max_argmax' max_argmax'.simps using less_ereal.simps(5) max_argmax'.simps(1) nth_Cons_0 nth_Cons_Suc split_pairs local.Cons(1) max_argmax_is_max_argmax' by fastforce
qed
qed
lemma argmax_list_gives_max:
assumes "xs ≠ []"
shows "(argmax_list xs) = m ⟹ ∀i ∈ {0..<length xs}. xs ! i ≤ xs ! m"
proof
fix i assume 1: "(argmax_list xs) = m" and i: "i ∈ {0..<length xs}"
hence "max_argmax xs = (ereal (xs ! m), m)"
using argmax_list_max_argmax[OF assms] by blast
with fst_max_argmax_is_max 1 have 0: " xs ! m = Max (set xs ∪ {-∞})"
by (metis fst_eqD)
have "xs ! i ≤ Max (set xs ∪ {-∞})"
using i by auto
thus "xs ! i ≤ xs ! m"
using 0 by (metis ereal_less_eq(3))
qed
lemma argmax_list_gives_max2:
assumes "xs ≠ []"
shows "(x ≤ (xs ! m) ∧ argmax_list xs = m) = (max_argmax (x#xs) = ((xs ! m), (Suc m)))"
proof(induction m)
case 0
then show ?case
unfolding argmax_list_max_argmax[of xs 0, OF assms] max_argmax_is_max_argmax' max_argmax'.simps
by (metis (mono_tags, lifting) Suc_n_not_n diff_Suc_1' ereal_less_eq(3) not_le split_conv split_pairs)
next
case (Suc m)
then show ?case
unfolding argmax_list_max_argmax[of xs m, OF assms] max_argmax_is_max_argmax' max_argmax'.simps
by(split if_split) (metis Suc_inject Zero_neq_Suc argmax_list_max_argmax assms basic_trans_rules(20) ereal_less_eq(3) fst_conv le_cases less_eq_ereal_def max_argmax_is_max_argmax' old.prod.case snd_conv)
qed
lemma fst_max_argmax_adj:
fixes xs ys rs :: "real list" and n :: nat
assumes "length xs = n"
and "length ys = n"
and "length rs = n"
and adj: "list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) xs ys"
shows "(fst (max_argmax (map2 (+) xs rs))) ≥ (fst (max_argmax (map2 (+) ys rs))) ∧ (fst (max_argmax (map2 (+) xs rs))) ≤ (fst (max_argmax (map2 (+) ys rs))) + 1"
using assms
proof(induction n arbitrary: xs ys rs)
case 0
hence q : "xs = []" "ys = []" "rs = []"
by auto
thus ?case unfolding q by auto
next
case (Suc n)
then obtain x2 y2 r2 ys2 xs2 rs2 where q: "xs = x2 # xs2" "ys = y2 # ys2" "rs = r2 # rs2"
using length_Suc_conv by metis
hence q2: "length xs2 = n" "length ys2 = n" "length rs2 = n"
using Suc.prems(1,2,3) by auto
from Suc.prems(4) have q3: "list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) xs2 ys2" and q4: "y2 ≤ x2 ∧ x2 ≤ y2 + 1"
unfolding q by auto
hence q5: "fst (max_argmax (map2 (+) ys2 rs2)) ≤ fst (max_argmax (map2 (+) xs2 rs2)) ∧
fst (max_argmax (map2 (+) xs2 rs2)) ≤ fst (max_argmax (map2 (+) ys2 rs2)) + 1"
using Suc(1) q2 by auto
from q4 have q6: "ereal (y2 + r2) ≤ ereal (x2 + r2) ∧ ereal (x2 + r2) ≤ ereal (y2 + r2) + 1"
by auto
have indx: "fst (max_argmax (map2 (+) xs rs)) = max (x2 + r2) (fst (max_argmax (map2 (+) xs2 rs2)))"
unfolding q max_argmax_is_max_argmax' by auto
have indy: "fst (max_argmax (map2 (+) ys rs)) = max (y2 + r2) (fst (max_argmax (map2 (+) ys2 rs2)))"
unfolding q max_argmax_is_max_argmax' by auto
show ?case
unfolding indx indy proof(intro conjI)
show "max (ereal (y2 + r2)) (fst (max_argmax (map2 (+) ys2 rs2))) ≤ max (ereal (x2 + r2)) (fst (max_argmax (map2 (+) xs2 rs2))) "
using q5 q6 using ereal_less_eq(3) max.mono by blast
have "max (ereal (x2 + r2)) (fst (max_argmax (map2 (+) xs2 rs2))) ≤ max (ereal (y2 + r2) + 1) (fst (max_argmax (map2 (+) ys2 rs2)) + 1)"
using q5 q6 using ereal_less_eq(3) max.mono by auto
also have "... ≤ (max (ereal (y2 + r2)) (fst (max_argmax (map2 (+) ys2 rs2)))) + 1"
by (meson add_right_mono max.bounded_iff max.cobounded1 max.cobounded2)
finally show "max (ereal (x2 + r2)) (fst (max_argmax (map2 (+) xs2 rs2))) ≤ max (ereal (y2 + r2)) (fst (max_argmax (map2 (+) ys2 rs2))) + 1".
qed
qed
subsection ‹ An auxiliary function to calculate the argmax of a list where an element has been inserted. ›
definition argmax_insert :: "real ⇒ real list ⇒ nat ⇒ nat" where
"argmax_insert k ks i = argmax_list (list_insert k ks i)"
lemma argmax_insert_i_i_0:
shows "(argmax_insert k xs 0 = 0) ⟷ (k > (fst (max_argmax xs)))"
unfolding argmax_insert_def argmax_list_def by (auto simp: max_argmax_is_max_argmax' list_insert_def)
lemma argmax_insert_i_i_expand:
assumes "xs ≠ []"
and "m ≤ n"
and "length xs = n"
shows "(argmax_insert k xs m = m) ⟷ (max_argmax ((take m xs) @ [k] @ (drop m xs))) = (k,m)"
unfolding argmax_insert_def by(subst argmax_list_max_argmax) (auto simp:assms nth_append list_insert_def)
lemma argmax_insert_i_i_iterate:
assumes "m ≤ n"
and "length xs = n"
shows "(argmax_insert k (x # xs) (Suc m) = (Suc m)) ⟷ ((x ≤ k) ∧ (argmax_insert k xs m = m))"
unfolding argmax_insert_def list_insert_def
proof(subst argmax_list_max_argmax)
show 0: "take (Suc m) (x # xs) @ [k] @ drop (Suc m) (x # xs) ≠ []"
by auto
have "m ≤ length xs"
using assms by auto
hence 1: "(take m xs @ [k] @ drop m xs) ! m = k"
by(subst nth_append, auto)
have 2: "take m xs @ [k] @ drop m xs ≠ []"
by auto
show "(max_argmax (take (Suc m) (x # xs) @ [k] @ drop (Suc m) (x # xs)) = (ereal ((take (Suc m) (x # xs) @ [k] @ drop (Suc m) (x # xs)) ! Suc m), Suc m)) =
(x ≤ k ∧ argmax_list (take m xs @ [k] @ drop m xs) = m)"
using argmax_list_gives_max2[of "take m xs @ [k] @ drop m xs" x " m", OF 2] unfolding 1 case_prod_beta
by (metis "1" Cons_eq_appendI drop_Suc_Cons nth_Cons_Suc prod.sel(1) prod.sel(2) take_Suc_Cons)
qed
lemma argmax_insert_i_i:
assumes "m ≤ n"
and "length xs = n"
shows "(argmax_insert k xs m = m) ⟷ (ereal k > (fst (max_argmax (drop m xs))) ∧ (ereal k ≥ (fst (max_argmax (take m xs)))))"
using assms unfolding max_argmax_is_max_argmax'
proof(induction xs arbitrary: n k m)
case Nil
thus ?case
by (metis drop_Nil drop_eq_Nil2 argmax_insert_i_i_0 less_eq_ereal_def list.size(3) order_antisym_conv take_Nil max_argmax_is_max_argmax')
next
case (Cons a zs)
thus ?case
proof(induction m arbitrary: n zs)
case 0
hence p: "⋀ xs. (take 0 xs) = []"
by auto
show ?case
unfolding p max_argmax'.simps(1) by (metis drop0 ereal_less_eq(2) fst_conv argmax_insert_i_i_0 max_argmax_is_max_argmax')
next
case (Suc m)
have a1: "(argmax_insert k (a # zs) (Suc m) = Suc m) ⟷ ((a ≤ k) ∧ (argmax_insert k zs m = m))"
using argmax_insert_i_i_iterate Suc.prems(2) Suc.prems(3) by auto
have a2: "(argmax_insert k zs m = m) ⟷ (fst (max_argmax' (drop m zs)) < ereal k ∧ fst (max_argmax' (take m zs)) ≤ ereal k)"
using Suc.prems(1) Suc.prems(2) Suc.prems(3) by auto
consider"fst (max_argmax' (take m zs)) < ereal a"|"fst (max_argmax' (take m zs)) > ereal a"| "fst (max_argmax' (take m zs)) = ereal a"
using linorder_less_linear by auto
hence a4: "((a ≤ k) ∧ fst (max_argmax' (take m zs)) ≤ ereal k) ⟷ fst (max_argmax' (take (Suc m) (a # zs))) ≤ ereal k"
proof(cases)
case 1
thus ?thesis
unfolding max_argmax'.simps(2) using less_eq_ereal_def order_less_le_trans by fastforce
next
case 2
hence "(a ≤ k ∧ fst (max_argmax' (take m zs)) ≤ ereal k) ⟷ (a < k ∧ fst (max_argmax' (take m zs)) ≤ ereal k)"
using leD nless_le by auto
thus ?thesis
unfolding max_argmax'.simps(2) using "2" le_ereal_less by auto
next
case 3
thus ?thesis
unfolding max_argmax'.simps(2) by auto
qed
from a1 a2 a4 show "(argmax_insert k (a # zs) (Suc m) = Suc m) ⟷ ((fst (max_argmax' (drop (Suc m) (a # zs))) < ereal k ∧ fst (max_argmax' (take (Suc m) (a # zs))) ≤ ereal k))"
by auto
qed
qed
lemma argmax_insert_i_i':
assumes "m ≤ n"
and "length xs = n"
shows "(argmax_insert k xs m = m) ⟷ (ereal k ≥ (fst (max_argmax xs)) ∧ (ereal k ≠ (fst (max_argmax (drop m xs)))))"
proof-
have "(argmax_insert k xs m = m) ⟷ (ereal k > (fst (max_argmax (drop m xs))) ∧ (ereal k ≥ (fst (max_argmax (take m xs)))))"
by (rule argmax_insert_i_i[OF assms])
also have "... ⟷ (ereal k ≥ (fst (max_argmax xs)) ∧ (ereal k ≠ (fst (max_argmax (drop m xs)))))"
proof-
have "fst (max_argmax xs) = fst (max_argmax ((take m xs) @ (drop m xs)))"
by auto
also have "... = max (fst (max_argmax (take m xs))) (fst (max_argmax (drop m xs)))"
using fst_max_argmax_append[symmetric] by auto
finally show ?thesis by auto
qed
finally show ?thesis.
qed
lemma argmax_insert_i_i'_region:
assumes "length xs = n" and "length ys = n" and "i ≤ n"
shows "{r | r :: real. argmax_insert (r + d) ((map2 (+) xs ys)) i = i} = {r | (r :: real). (ereal (r + d) ≥ (fst (max_argmax (map2 (+) xs ys))) ∧ (ereal (r + d) ≠ (fst (max_argmax (drop i (map2 (+) xs ys))))))}"
using assms argmax_insert_i_i' by auto
section ‹Formal proof of DP of RNM›
subsection ‹ A formal proof of the main part of differential privacy of report noisy max [Claim 3.9, AFDP] ›
locale Lap_Mechanism_RNM_mainpart =
fixes M::"'a measure"
and adj::"'a rel"
and c::"'a ⇒ real list"
assumes c: "c ∈ M →⇩M (listM borel)"
and cond: "∀ (x,y) ∈ adj. list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) (c x) (c y) ∨ list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) (c y) (c x)"
and adj: "adj ⊆ (space M) × (space M)"
begin
text ‹ We define an abstracted version of report noisy max mechanism. We later instantiate @{term c} with the counting query. ›
definition LapMech_RNM :: "real ⇒ 'a ⇒ nat measure" where
"LapMech_RNM ε x = do {y ← Lap_dist_list (1 / ε) (c x); return (count_space UNIV) (argmax_list y)}"
lemma measurable_LapMech_RNM[measurable]:
shows "LapMech_RNM ε ∈ M →⇩M prob_algebra(count_space UNIV)"
unfolding LapMech_RNM_def argmax_list_def using c by auto
paragraph ‹ Calculating the density of the probability distributions sampled from the main part of @{term LapMech_RNM}›
context
fixes ε::real
assumes pose:"0 < ε"
begin
paragraph ‹ The main part of @{term LapMech_RNM} ›
definition RNM' :: "real list ⇒ nat measure" where
"RNM' zs = do {y ← Lap_dist_list (1 / ε) (zs); return (count_space UNIV) (argmax_list y)}"
lemma RNM'_def2:
shows "RNM' zs = do {rs ← Lap_dist0_list (1 / ε) (length zs); y ← return (listM borel) (map2 (+) zs rs); return (count_space UNIV) (argmax_list y)}"
by (unfold RNM'_def Lap_dist_list_def2,subst bind_assoc[where N = "listM borel" and R = "count_space UNIV"],auto)
lemma measurable_RNM'[measurable]:
shows "RNM' ∈ listM borel →⇩M prob_algebra(count_space UNIV)"
unfolding RNM'_def argmax_list_def by auto
lemma LapMech_RNM_RNM'_c:
shows "LapMech_RNM ε = RNM' o c"
unfolding RNM'_def LapMech_RNM_def by auto
lemma RNM'_Nil:
shows "RNM' [] = return (count_space (UNIV :: nat set)) 0"
by(unfold RNM'_def Lap_dist_list.simps(1), subst bind_return[where N = "(count_space UNIV)"],auto simp: argmax_list_def)
lemma RNM'_singleton:
shows "RNM' [x] = return (count_space (UNIV :: nat set)) 0"
proof-
have "RNM' [x] = (Lap_dist (1/ε) x) ⤜ (λx1. return (listM borel) [] ⤜ (λx2. return (listM borel) (x1 # x2))) ⤜ (λy. return (count_space UNIV) (argmax_list y))"
unfolding RNM'_def by auto
also have "... = (Lap_dist (1/ε) x) ⤜ (λx1. return (listM borel) (x1 # [])) ⤜ (λy. return (count_space UNIV) (argmax_list y))"
by(subst bind_return, measurable)
also have "... = (Lap_dist (1/ε) x) ⤜ (λx1. return (count_space UNIV) (argmax_list [x1]))"
proof(subst bind_assoc)
show "Lap_dist (1 / ε) x ⤜ (λx. return (listM borel) [x] ⤜ (λy. return (count_space UNIV) (argmax_list y))) = Lap_dist (1 / ε) x ⤜ (λx1. return (count_space UNIV) (argmax_list [x1]))"
by(subst bind_return, measurable)
qed measurable
also have "... = return (count_space (UNIV :: nat set)) 0"
by(auto simp: bind_const' subprob_space_return argmax_list_def)
finally show ?thesis.
qed
lemma RNM'_support:
assumes "i ≥ length xs"
and "xs ≠ []"
shows "emeasure (RNM' xs){i} = 0"
unfolding RNM'_def
proof-
define n :: nat where n: "n = length xs"
have 1: "emeasure (Lap_dist_list (1/ε) xs) {zs. length zs = n} = 1"
using emeasure_Lap_dist_list_length[of _ xs] n by auto
show "emeasure (Lap_dist_list (1 / ε) xs ⤜ (λy. return (count_space UNIV) (argmax_list y))) {i} = 0"
proof(subst Giry_Monad.emeasure_bind)
show " space (Lap_dist_list (1 / ε) xs) ≠ {}"
by(auto simp: space_Lap_dist_list)
show "{i} ∈ sets (count_space UNIV)"
by auto
show " (λy. return (count_space UNIV) (argmax_list y)) ∈ Lap_dist_list (1 / ε) xs →⇩M subprob_algebra (count_space UNIV)"
by auto
show "(∫⇧+ x. emeasure (return (count_space UNIV) (argmax_list x)) {i} ∂Lap_dist_list (1 / ε) xs) = 0"
proof(subst Giry_Monad.emeasure_return)
show "(∫⇧+ x. indicator {i} (argmax_list x) ∂Lap_dist_list (1 / ε) xs) = 0"
proof(rule Distributions.nn_integral_zero',rule AE_mp)
show "almost_everywhere (Lap_dist_list (1 / ε) xs) (λzs. zs ∈{zs. length zs = n})"
by(rule prob_space.AE_prob_1,auto simp: measure_def 1)
show " AE x∈{zs. length zs = n} in Lap_dist_list (1 / ε) xs. indicator {i} (argmax_list x) = 0"
proof(rule AE_I2,rule impI)
fix x :: "real list" assume "x ∈ {zs. length zs = n}"
with n assms show "indicator {i} (argmax_list x) = 0"
by (metis (mono_tags, lifting) One_nat_def Suc_diff_le argmax_list_le_length diff_Suc_1' diff_is_0_eq indicator_simps(2) length_0_conv mem_Collect_eq not_less_eq_eq singletonD)
qed
qed
qed fact
qed
qed
paragraph ‹ The conditional distribution of @{term RNM'} when @{term "n - 1"} values of noise are fixed. ›
definition RNM_M :: "real list ⇒ real list ⇒ real ⇒ nat ⇒ nat measure" where
"RNM_M cs rs d i = do{r ← (Lap_dist0 (1/ε)); return (count_space UNIV) (argmax_insert (r+d) ((λ (xs,ys). (map2 (+) xs ys))(cs, rs)) i)}"
lemma space_RNM_M:
shows "space (RNM_M cs rs d i) = (UNIV :: nat set)"
unfolding RNM_M_def Lap_dist0_def by (metis empty_not_UNIV sets_return space_count_space space_bind space_Lap_dist )
lemma sets_RNM_M[measurable_cong]:
shows "sets (RNM_M cs rs d i) = sets (count_space (UNIV :: nat set))"
unfolding RNM_M_def Lap_dist0_def by(metis sets_bind sets_return space_Lap_dist empty_not_UNIV)
lemma RNM_M_Nil:
shows "emeasure (RNM_M [] [] d 0) {j ∈ UNIV. j = 0} = 1"
and "k ≠ 0 ⟹ emeasure (RNM_M [] [] d 0) {j ∈ UNIV. j = k} = 0"
proof-
have b: "Lap_dist0 (1/ε) ⤜ (λr. return (count_space UNIV) (0 :: nat)) = return (count_space UNIV) (0 :: nat)"
proof(rule measure_eqI)
show "sets (Lap_dist0 (1/ε) ⤜ (λr. return (count_space UNIV) 0)) = sets (return (count_space UNIV) 0)"
unfolding Lap_dist0_def by (metis countable_empty sets_bind space_Lap_dist uncountable_UNIV_real)
show "⋀A. A ∈ sets (Lap_dist0 (1/ε) ⤜ (λr. return (count_space UNIV) 0)) ⟹
emeasure (Lap_dist0 (1/ε) ⤜ (λr. return (count_space UNIV) 0)) A = emeasure (return (count_space UNIV) 0) A"
unfolding Lap_dist0_def by(subst emeasure_bind_const_prob_space,auto simp: subprob_space_return_ne)
qed
{
fix k :: nat
have "measure (Lap_dist0 (1/ε) ⤜ (λr. return (count_space UNIV) 0)) {j :: nat. j = k ∧ j ∈ space (Lap_dist0 (1/ε) ⤜ (λr. return (count_space UNIV) 0))}
= measure (return (count_space UNIV) 0) {j :: nat. j = k ∧ j ∈ space (return (count_space UNIV) 0)}"
unfolding b by standard
also have "... = measure (return (count_space UNIV) 0){k :: nat}"
by auto
}note * = this
show "emeasure (RNM_M [] [] d 0) {j ∈ UNIV. j = 0} = 1"
by(auto simp: RNM_M_def argmax_insert_def argmax_list_def b list_insert_def)
show "k ≠ 0 ⟹ emeasure (RNM_M [] [] d 0) {j ∈ UNIV. j = k} = 0"
by(auto simp: RNM_M_def argmax_insert_def argmax_list_def b list_insert_def)
qed
lemma RNM_M_Nil_indicator:
shows "emeasure (RNM_M [] [] d 0) = indicator {A :: nat set. A ∈ UNIV ∧ 0 ∈ A}"
proof
fix B :: "nat set"
have 1: "⋀ k :: nat. (if (k ∈ B ∧ k ≠ 0) then {k} else {}) ∈ null_sets (RNM_M [] [] d 0)"
proof(split if_split, intro conjI impI)
show "⋀k. k ∈ B ∧ k ≠ 0 ⟹ {k} ∈ null_sets (RNM_M [] [] d 0)"
using RNM_M_Nil(2)[of _ d] by auto
show "⋀k. ¬ (k ∈ B ∧ k ≠ 0) ⟹ {} ∈ null_sets (RNM_M [] [] d 0)"
by auto
qed
have 2: "⋃ (range (λ k. if (k ∈ B ∧ k ≠ 0) then {k} else {})) = {k :: nat. k ∈ B ∧ k ≠ 0}"
by auto
have "{k :: nat. k ∈ B ∧ k ≠ 0} ∈ null_sets (RNM_M [] [] d 0)"
using null_sets_UN'[of"UNIV :: nat set" "(λ k. if (k ∈ B ∧ k ≠ 0) then {k} else {})" "(RNM_M [] [] d 0)",OF _ 1 ]
unfolding 2[THEN sym] by auto
hence b: "emeasure (RNM_M [] [] d 0) {k ∈ B. k ≠ 0} = 0"
by blast
have a: "emeasure (RNM_M [] [] d 0) {0} = 1"
using RNM_M_Nil(1)[of d] by auto
show "emeasure (RNM_M [] [] d 0) B = indicator {A ∈ UNIV. 0 ∈ A} B"
proof(cases"0 ∈ B")
case True
hence B: "B = {0} ∪ {k. k ∈ B ∧ k ≠ 0}"by auto
hence "emeasure (RNM_M [] [] d 0) B = emeasure (RNM_M [] [] d 0) ({0} ∪ {k. k ∈ B ∧ k ≠ 0})"
by auto
also have "... = emeasure (RNM_M [] [] d 0) {0} + emeasure (RNM_M [] [] d 0) {k. k ∈ B ∧ k ≠ 0}"
by(rule plus_emeasure[THEN sym],auto simp: sets_RNM_M)
also have "... = 1"
using a b by auto
finally show ?thesis using True by auto
next
case False
hence B: "B = {k. k ∈ B ∧ k ≠ 0}"
using Collect_mem_eq by fastforce
hence "emeasure (RNM_M [] [] d 0) B = emeasure (RNM_M [] [] d 0) ({k. k ∈ B ∧ k ≠ 0})"
by auto
also have "... = 0"
using b by auto
finally show ?thesis using False by auto
qed
qed
lemma RNM_M_Nil_is_return_0:
shows "(RNM_M [] [] d 0) = return (count_space UNIV) 0"
proof(rule measure_eqI)
show "sets (RNM_M [] [] d 0) = sets (return (count_space UNIV) 0)"
by (auto simp: sets_RNM_M)
show "⋀A. A ∈ sets (RNM_M [] [] d 0) ⟹ emeasure (RNM_M [] [] d 0) A = emeasure (return (count_space UNIV) 0) A"
unfolding RNM_M_Nil_indicator sets_RNM_M emeasure_return
by(split split_indicator,auto)
qed
lemma RNM_M_probability:
fixes cs rs :: "real list"
assumes "length cs = n" and "length rs = n"
and "i ≤ n"
and pose: "ε > 0"
shows "𝒫(j in (RNM_M cs rs d i). j = i) = 𝒫(r in (Lap_dist0 (1/ε)). ereal(r + d) ≥ (fst (max_argmax (map2 (+) cs rs))))"
using assms
proof-
have "𝒫(j in (RNM_M cs rs d i). j = i) = measure (RNM_M cs rs d i) {j :: nat | j. j∈ UNIV ∧ j = i}"
using space_RNM_M by auto
also have "... = measure (Lap_dist0 (1/ε) ⤜ (λr. return (count_space (UNIV :: nat set)) (argmax_insert (r + d) (map (λ(x, y). x + y) (zip cs rs)) i))) {j :: nat | j. j∈ UNIV ∧ j = i}"
unfolding RNM_M_def by auto
also have "... = LINT r|(Lap_dist0 (1/ε)). measure (return (count_space (UNIV :: nat set)) (argmax_insert (r + d) (map (λ(x, y). x + y) (zip cs rs)) i)) {j :: nat | j. j∈ UNIV ∧ j = i}"
proof(intro subprob_space.measure_bind subprob_space_Lap_dist0)
show "{j |j. j ∈ ⊤ ∧ j = i} ∈ sets (count_space (UNIV :: nat set))"
by auto
have 1: "take i (map (λ(x, y). x + y) (zip cs rs)) ∈ space (listM borel)"
unfolding space_listM by auto
have 2: "drop i (map (λ(x, y). x + y) (zip cs rs)) ∈ space (listM borel)"
unfolding space_listM by auto
hence 3: "(λx. drop i (map (λ(x, y). x + y) (zip cs rs))) ∈ Lap_dist0 (1/ε) →⇩M listM borel"
by measurable
have "(λx. [x + d] @ drop i (map (λ(x, y). x + y) (zip cs rs))) ∈ Lap_dist0 (1/ε) →⇩M listM borel"
using listM_Nil 2 by measurable
show "(λr. return (count_space ⊤) (argmax_insert (r + d) (map (λ(x, y). x + y) (zip cs rs)) i)) ∈ Lap_dist0 (1/ε) →⇩M subprob_algebra (count_space ⊤)"
unfolding argmax_insert_def using space_listM sets_Lap_dist measurable_cong_sets 1 listM_Nil 2 by measurable
qed
also have "... = LINT r|(Lap_dist0 (1/ε)). (λ r. indicator {j :: nat | j. j∈ UNIV ∧ j = i} (argmax_insert (r + d) (map (λ(x, y). x + y) (zip cs rs)) i)) r"
by(subst measure_return,auto)
also have "... = LINT r|(Lap_dist0 (1/ε)). indicator {r | r :: real. argmax_insert (r + d) ((map2 (+) cs rs)) i = i} r"
proof(rule Bochner_Integration.integral_cong)
show "Lap_dist0 (1/ε) = Lap_dist0 (1/ε)"
by auto
fix x :: real assume "x ∈ space (Lap_dist0 (1/ε))"
hence x: "x ∈ UNIV"
by(auto simp: space_Lap_dist)
thus "indicator {j |j. j ∈ ⊤ ∧ j = i} (argmax_insert (x + d) (map (λ(x, y). x + y) (zip cs rs)) i) = indicator {r |r. argmax_insert (r + d) (map (λ(x, y). x + y) (zip cs rs)) i = i} x"
by(split split_indicator,auto)
qed
also have "... = measure (Lap_dist0 (1/ε)) ({r | r :: real. argmax_insert (r + d) ((map2 (+) cs rs)) i = i} ∩ space (Lap_dist0 (1/ε)))"
by auto
also have "... = measure (Lap_dist0 (1/ε)) ({r | r :: real. argmax_insert (r + d) ((map2 (+) cs rs)) i = i})"
unfolding space_Lap_dist0 by auto
also have "... = measure (Lap_dist0 (1/ε)) {r | (r :: real). (ereal (r + d) ≥ (fst (max_argmax (map2 (+) cs rs)))) ∧ ((ereal (r + d) ≠ (fst (max_argmax (drop i (map2 (+) cs rs))))))}"
by(subst argmax_insert_i_i' assms ,auto simp: assms)
also have "... = measure (Lap_dist0 (1/ε)) ({r | (r :: real). (ereal (r + d) ≥ (fst (max_argmax (map2 (+) cs rs))))}
- {r | (r :: real). (ereal (r + d) ≥ (fst (max_argmax (map2 (+) cs rs)))) ∧ (ereal (r + d) = (fst (max_argmax (drop i (map2 (+) cs rs)))))})"
proof-
have "{r | (r :: real). (ereal (r + d) ≥ (fst (max_argmax (map2 (+) cs rs)))) ∧ ((ereal (r + d) ≠ (fst (max_argmax (drop i (map2 (+) cs rs))))))}
= ({r | (r :: real). (ereal (r + d) ≥ (fst (max_argmax (map2 (+) cs rs))))}
- {r | (r :: real). (ereal (r + d) ≥ (fst (max_argmax (map2 (+) cs rs)))) ∧ (ereal (r + d) = (fst (max_argmax (drop i (map2 (+) cs rs)))))})"
by auto
thus ?thesis
by auto
qed
also have "... = measure (Lap_dist0 (1/ε)) {r | (r :: real). (ereal (r + d) ≥ (fst (max_argmax (map2 (+) cs rs))))}
- measure (Lap_dist0 (1/ε)) {r | (r :: real). (ereal (r + d) ≥ (fst (max_argmax (map2 (+) cs rs)))) ∧ (ereal (r + d) = (fst (max_argmax (drop i (map2 (+) cs rs)))))}"
using subprob_space_Lap_dist by(intro finite_measure.finite_measure_Diff,auto simp: subprob_space.axioms(1))
also have "... = measure (Lap_dist0 (1/ε)) {r | (r :: real). (ereal (r + d) ≥ (fst (max_argmax (map2 (+) cs rs))))}"
(is"measure (Lap_dist0 (1/ε)) ?A - measure (Lap_dist0 (1/ε)) ?B = measure (Lap_dist0 (1/ε)) ?A")
proof-
have "measure (Lap_dist0 (1/ε)) ?B = 0"
proof-
from pose have "(Lap_dist0 (1/ε)) = (density lborel (λx. ennreal (laplace_density (1 div ε) 0 x)))"
unfolding Lap_dist_def Lap_dist0_def by auto
hence 2: "absolutely_continuous lborel (Lap_dist0 (1/ε))"
by(auto intro: absolutely_continuousI_density)
have 3: "?B = (UNIV :: real set) ∩ (λr. ereal (r + d)) -` {r . r ≥ (fst (max_argmax (map2 (+) cs rs))) ∧ r = (fst (max_argmax (drop i (map2 (+) cs rs))))}"
(is"?B = ?C")
by auto
have "?C ∈ null_sets lborel"
proof(intro countable_imp_null_set_lborel countable_image_inj_Int_vimage)
show "inj_on (λr :: real. ereal (r + d)) ⊤"
unfolding inj_on_def by (metis add.commute add_left_cancel ereal.inject)
show "countable {r. fst (max_argmax (map (λ(x, y). x + y) (zip cs rs))) ≤ r ∧ r = fst (max_argmax (drop i (map (λ(x, y). x + y) (zip cs rs))))}"
by(rule countable_subset,auto)
qed
hence 4: "?B ∈ null_sets (Lap_dist0 (1/ε)) "
using 3 2 unfolding absolutely_continuous_def by auto
thus "measure (Lap_dist0 (1/ε)) ?B = 0"
unfolding null_sets_def using measure_eq_emeasure_eq_ennreal [of"0 :: real" "(Lap_dist0 (1/ε))" "?B"] by auto
qed
thus ?thesis
by auto
qed
also have "... = 𝒫(r in (Lap_dist0 (1/ε)). ereal(r + d) ≥ (fst (max_argmax (map2 (+) cs rs))))"
by (metis UNIV_I space_Lap_dist0)
finally show ?thesis .
qed
paragraph ‹differential privacy inequality on @{term RNM_M}›
lemma DP_RNM_M_i:
fixes xs ys rs :: "real list" and x y :: real and i n :: nat
assumes "length xs = n" and "length ys = n" and "length rs = n"
and adj': "x ≥ y ∧ x ≤ y + 1"
and adj: "list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) xs ys"
and "i ≤ n"
shows "𝒫(j in (RNM_M xs rs x i). j = i) ≤ (exp ε) * 𝒫(j in (RNM_M ys rs y i). j = i) ∧ 𝒫(j in (RNM_M ys rs y i). j = i) ≤ (exp ε) * 𝒫(j in (RNM_M xs rs x i). j = i)"
proof(cases"n = 0")
case True
hence xs: "xs = []" and ys: "ys = []" and rs: "rs = []" and i: "i = 0"
using assms by blast+
from pose have e: "exp ε ≥ 1"
by auto
thus ?thesis unfolding xs ys rs i RNM_M_Nil_is_return_0
by (auto simp: measure_return)
next
case False
have eq1: "⋀i :: nat. i ≤ n ⟹ 𝒫(j in (RNM_M xs rs x i). j = i) = 𝒫(r in (Lap_dist0 (1/ε)). ereal(r + x) ≥ (fst (max_argmax (map2 (+) xs rs))))"
using RNM_M_probability assms pose by auto
have eq2: "⋀i :: nat. i ≤ n ⟹ 𝒫(j in (RNM_M ys rs y i). j = i) = 𝒫(r in (Lap_dist0 (1/ε)). ereal(r + y) ≥ (fst (max_argmax (map2 (+) ys rs))))"
using RNM_M_probability assms pose by auto
have fin: "finite_measure (Lap_dist0 (1/ε))"
using prob_space_Lap_dist0 by (metis prob_space.finite_measure)
show ?thesis
using False assms
proof(intro conjI)
show "𝒫(j in RNM_M xs rs x i. j = i) ≤ exp ε * 𝒫(j in RNM_M ys rs y i. j = i)"
unfolding eq1[OF assms(6)] eq2[OF assms(6)]
proof-
have "{r :: real. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (r + x)} ⊆ {r :: real. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (r + x)}"
using fst_max_argmax_adj[of"xs"_"ys" "rs"] assms by(intro subsetI, unfold mem_Collect_eq,auto)
also have "... ⊆ {r :: real. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (r + y + 1)}"
using adj' Collect_mono_iff le_ereal_le by force
also have "... = {r | v r :: real. v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)}"
by (auto simp: add.commute add.left_commute)
finally have ineq1: "{r. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (r + x)} ⊆ {r | v r :: real. v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)}".
have meas1: "{z :: real. ∃v r. z = r ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)} ∈ sets (Lap_dist0 (1/ε))"
by auto
have "measure (Lap_dist0 (1/ε)) {r. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (r + x)} ≤ measure (Lap_dist0 (1/ε)) {r | v r :: real. v = r + 1 ∧ fst (max_argmax(map2 (+) ys rs)) ≤ ereal (v + y)}"
proof(intro measure_mono_fmeasurable ineq1)
show "{z. ∃v r. z = r ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)} ∈ fmeasurable (Lap_dist0 (1/ε))"
using prob_space_Lap_dist finite_measure.fmeasurable_eq_sets fin meas1 by blast
show "{r. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (r + x)} ∈ sets (Lap_dist0 (1/ε))"
by auto
qed
also have "... ≤ (exp ε) * measure (Lap_dist (1/ε) (-1)) {r | v r :: real. v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)} + (0 :: real)"
using meas1 unfolding Lap_dist0_def by(intro DP_divergence_leE meas1 DP_divergence_Lap_dist'_eps pose, auto)
also have "... = (exp ε) * measure (Lap_dist (1/ε) (-1)) {r | v r :: real. v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)}"
by auto
also have "... = (exp ε) * measure ((Lap_dist0 (1/ε)) ⤜ (λ r. return borel (r + (-1)))) {r | v r :: real. v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)}"
unfolding Lap_dist_def2[of "(1 / ε)" "-1"] Lap_dist0_def by auto
also have "... = (exp ε) * measure (Lap_dist0 (1/ε)) {(r + 1)| v r :: real. v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)}"
proof(subst subprob_space.measure_bind)
show "subprob_space (Lap_dist0 (1/ε))"
by auto
show "(λr. return borel (r + (-1))) ∈ Lap_dist0 (1/ε) →⇩M subprob_algebra borel"
by auto
show "exp ε * (LINT x|Lap_dist0 (1/ε). measure (return borel (x + (-1))) {z. ∃v r. z = r ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)})
= exp ε * measure (Lap_dist0 (1/ε)) {z. ∃v r. z = r + 1 ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)}"
using meas1 proof(subst measure_return)
show "{z. ∃v r. z = r ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)} ∈ sets borel"
by auto
have "exp ε * (LINT x|Lap_dist0 (1/ε). indicat_real {z. ∃v r. z = r ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)} (x + (-1))) = exp ε * (LINT x|Lap_dist0 (1/ε). indicat_real {z + 1 | z. ∃v r. z = r ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)} x)"
proof(subst Bochner_Integration.integral_cong)
have 1: "⋀x. ∀z. x = z + 1 ⟶ ¬ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (z + 1 + y) ⟹ indicat_real {z. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (z + 1 + y)} (x - 1) = 0"
proof-
fix x :: real assume "∀z :: real. x = z + 1 ⟶ ¬ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (z + 1 + y)"
hence *: "⋀z. x = z + 1 ⟹ ¬ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (x + y)"by auto
hence "¬ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (x + y)"using *[of"x - 1"] by auto
thus "indicat_real {z. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (z + 1 + y)} (x - 1) = 0"by auto
qed
show "⋀x. indicat_real {z. ∃v r. z = r ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)} (x + - 1) = indicat_real {z + 1 | z. ∃v r. z = r ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)} x"
by(split split_indicator, intro conjI impI allI,auto simp: 1)
qed(auto)
also have "... = exp ε * measure (Lap_dist0 (1/ε)) {z + 1 | z. ∃v r. z = r ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)}"
using Bochner_Integration.integral_indicator space_Lap_dist0 by auto
also have "... = exp ε * measure (Lap_dist0 (1/ε)) {z. ∃v r. z = r + 1 ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)}"
by (metis (no_types, lifting) add_cancel_right_right is_num_normalize(1) real_add_minus_iff)
finally show "exp ε * (LINT x|Lap_dist0 (1/ε). indicat_real {z. ∃v r. z = r ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)} (x + - 1)) = exp ε * Sigma_Algebra.measure (Lap_dist0 (1/ε)) {z. ∃v r. z = r + 1 ∧ v = r + 1 ∧ fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)}".
qed
qed(auto)
also have "... = exp ε * Sigma_Algebra.measure (Lap_dist0 (1/ε)) {v. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (v + y)}"
by (metis (no_types, lifting) add_cancel_right_right is_num_normalize(1) real_add_minus_iff)
finally have "Sigma_Algebra.measure (Lap_dist0 (1/ε)) {r. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (r + x)} ≤ exp ε * Sigma_Algebra.measure (Lap_dist0 (1/ε)) {r. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (r + y)}"by auto
thus"𝒫(r in Lap_dist0 (1/ε). fst (max_argmax (map2 (+) xs rs)) ≤ ereal (r + x)) ≤ exp ε * 𝒫(r in Lap_dist0 (1/ε). fst (max_argmax (map2 (+) ys rs)) ≤ ereal (r + y))"
using space_Lap_dist0 by auto
qed
next
show "𝒫(j in RNM_M ys rs y i. j = i) ≤ exp ε * 𝒫(j in RNM_M xs rs x i. j = i)"
unfolding eq1[OF assms(6)] eq2[OF assms(6)]
proof-
have "{r :: real. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (r + y)} ⊆ {r :: real. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (r + x)}"
using assms adj' Collect_mono_iff le_ereal_le by force
also have "... ⊆ {r :: real. fst (max_argmax (map2 (+) xs rs)) - 1 ≤ ereal (r + x)}"
using ereal_diff_add_transpose fst_max_argmax_adj[of"xs"_"ys" "rs"] assms by fastforce
also have "... ⊆ {v - (1 :: real) |v :: real. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}"
proof(rule subsetI)
fix z :: real assume "z ∈ {r. fst (max_argmax (map2 (+) xs rs)) - 1 ≤ ereal (r + x)}"
hence "fst (max_argmax (map2 (+) xs rs)) - 1 ≤ ereal (z + x)"
by blast
hence "fst (max_argmax (map2 (+) xs rs)) - 1 + 1 ≤ ereal (z + x) + 1"
by (metis add.commute add_left_mono)
hence "fst (max_argmax (map2 (+) xs rs)) - 1 + 1 ≤ ereal ((z + 1) + x)"
by (auto simp: add.commute add.left_commute)
hence "fst (max_argmax (map2 (+) xs rs)) ≤ ereal ((z + 1) + x)"
by (metis add.commute add_0 add_diff_eq_ereal cancel_comm_monoid_add_class.diff_cancel ereal_minus(1) one_ereal_def zero_ereal_def)
hence "z + (1 :: real) ∈ {v :: real. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}"
by auto
thus"z ∈ {v - (1 :: real) |v :: real. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}"
by force
qed
finally have ineq2: "{r. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (r + y)} ⊆ {v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}".
have "{v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)} = (λr. r + 1)-` {v |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}"
by force
also have "... ∈ sets (Lap_dist0 (1/ε))"
by auto
finally have meas2[measurable]: "{v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)} ∈ sets (Lap_dist0 (1/ε))".
hence "measure (Lap_dist0 (1/ε)) {r. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (r + y)} ≤ measure (Lap_dist0 (1/ε)) {v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}"
proof(intro ineq2 measure_mono_fmeasurable)
show "{r. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (r + y)} ∈ sets (Lap_dist0 (1/ε))"
by auto
thus "{v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)} ∈ fmeasurable (Lap_dist0 (1/ε))"
using prob_space_Lap_dist finite_measure.fmeasurable_eq_sets fin meas2 by blast
qed
also have "... ≤ (exp ε) * measure (Lap_dist (1/ε) (-1)) {v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)} + 0"
using meas2 unfolding Lap_dist0_def by (intro DP_divergence_leE DP_divergence_Lap_dist'_eps pose, auto)
also have "... = (exp ε) * measure ((Lap_dist0 (1/ε)) ⤜ (λ r. return borel (r + (-1)))) {v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}"
unfolding Lap_dist_def2[of "(1 / ε)" "-1"] Lap_dist0_def by auto
also have "... = (exp ε) * measure (Lap_dist0 (1/ε)) {v |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}"
proof(subst subprob_space.measure_bind)
show "subprob_space (Lap_dist0 (1/ε))"
by auto
show "(λr. return borel (r + -1)) ∈ Lap_dist0 (1/ε) →⇩M subprob_algebra borel"
by auto
show meas22: "{v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)} ∈ sets borel"
using meas2 sets_Lap_dist0 by blast
show "exp ε * (LINT z|Lap_dist0 (1/ε). measure (return borel (z + - 1)) {v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}) =
exp ε * measure (Lap_dist0 (1/ε)) {v |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}"
proof(subst measure_return,intro meas22)
have "exp ε * (LINT z|Lap_dist0 (1/ε). indicat_real {v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)} (z + - 1)) = exp ε * (LINT z|Lap_dist0 (1/ε). indicat_real {v |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)} z)"
proof(subst Bochner_Integration.integral_cong)
fix z :: real
show "indicat_real {v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)} (z + - 1) = indicat_real {v |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)} z"
unfolding indicator_def by auto
show "exp ε * integral⇧L (Lap_dist0 (1/ε)) (indicat_real {v |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}) =
exp ε * integral⇧L (Lap_dist0 (1/ε)) (indicat_real {v |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)})"
by auto
qed(auto)
also have "... = exp ε * measure (Lap_dist0 (1/ε)) {v |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}"
using Bochner_Integration.integral_indicator space_Lap_dist by auto
finally show "exp ε * (LINT z|Lap_dist0 (1/ε). indicat_real {v - 1 |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)} (z + - 1)) =
exp ε * Sigma_Algebra.measure (Lap_dist0 (1/ε)) {v |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}".
qed
qed
finally have " Sigma_Algebra.measure (Lap_dist0 (1/ε)) {r. fst (max_argmax (map2 (+) ys rs)) ≤ ereal (r + y)}
≤ exp ε * Sigma_Algebra.measure (Lap_dist0 (1/ε)) {v |v. fst (max_argmax (map2 (+) xs rs)) ≤ ereal (v + x)}".
thus"𝒫(r in Lap_dist0 (1/ε). fst (max_argmax (map2 (+) ys rs)) ≤ ereal (r + y)) ≤ exp ε * 𝒫(r in Lap_dist0 (1/ε). fst (max_argmax (map2 (+) xs rs)) ≤ ereal (r + x))"
using space_Lap_dist0 by auto
qed
qed
qed
paragraph ‹ Aggregating the differential privacy inequalities on @{term RNM_M} to those of @{term RNM'} ›
lemma RNM'_expand:
fixes n :: nat
assumes "length xs = n" and "i ≤ n"
shows "(RNM' (list_insert x xs i)) = do{rs ← (Lap_dist0_list (1 / ε) (length xs)); (RNM_M xs rs x i)}"
using assms
proof(induction n arbitrary: xs i)
note [measurable del] = borel_measurable_count_space
case 0
hence xs: "xs = []" and i: "i = 0"
by auto
have "Lap_dist0_list (1 / ε) 0 ⤜ (λrs. RNM_M [] rs x i) = (return (listM borel) []) ⤜ (λrs. RNM_M [] rs x i)"
by auto
also have "... = RNM_M [] [] x i"
by(subst bind_return[where N = "(count_space UNIV)"],auto simp: space_listM RNM_M_def argmax_insert_def argmax_list_def comp_def case_prod_beta)
also have "... = return (count_space UNIV) 0"
using RNM_M_Nil_is_return_0 RNM_M_def argmax_insert_def unfolding list_insert_def by force
also have "... = RNM' (list_insert x [] i)"
unfolding list_insert_def take.simps drop.simps append.simps RNM'_singleton by auto
finally show ?case unfolding xs i by auto
next
note borel_measurable_count_space[measurable del]
case (Suc n)
then obtain a ys where xs: "xs = a # ys" and n: "length ys = n"
by (metis Suc_length_conv)
have xxsl: "⋀x. length (x # xs) = Suc (Suc n)"
using n xs by auto
have Lap_mechanism_multi_replicate_insert: "⋀n k :: nat. k ≤ n ⟹( Lap_dist0_list (1 / ε) (Suc n)) = Lap_dist0 (1/ε) ⤜ (λz. Lap_dist0_list (1 / ε) n ⤜ (λzs. return (listM borel) (list_insert z zs k)))"
proof-
fix n k :: nat assume "k ≤ n"
thus"Lap_dist0_list (1 / ε) (Suc n) = Lap_dist0 (1/ε) ⤜ (λz. Lap_dist0_list (1 / ε) n ⤜ (λzs. return (listM borel) (list_insert z zs k)))"
proof(induction n arbitrary: k)
case 0
hence k: "k = 0"
by auto
thus ?case unfolding k list_insert_def unfolding Lap_dist0_def Lap_dist0_list.simps(2) append_Cons append_Nil drop_0 take_0 by auto
next
case (Suc n)
thus ?case proof(induction k)
case 0
thus ?case unfolding list_insert_def unfolding Lap_dist0_def Lap_dist0_list.simps(2) append_Cons append_Nil drop_0 take_0 by auto
next
case (Suc k)
hence "k ≤ n" by auto
hence 1: " Lap_dist0_list (1 / ε) (Suc n) = Lap_dist0 (1/ε) ⤜ (λz. Lap_dist0_list (1 / ε) n ⤜ (λzs. return (listM borel) (list_insert z zs k)))"
using Suc.prems(1) by auto
have "Lap_dist0_list (1 / ε) (Suc (Suc n)) = Lap_dist0 (1/ε) ⤜ (λy. Lap_dist0_list (1 / ε) (Suc n) ⤜ (λys. return (listM borel) (y # ys)))"
unfolding Lap_dist0_list.simps(2) Lap_dist0_def by auto
also have "... = Lap_dist0 (1/ε) ⤜ (λy. (Lap_dist0 (1/ε) ⤜ (λz. Lap_dist0_list (1 / ε) n ⤜ (λzs. return (listM borel) (list_insert z zs k)))) ⤜ (λys. return (listM borel) (y # ys)))"
using 1 by auto
also have "... = Lap_dist0 (1/ε) ⤜ (λy. (Lap_dist0 (1/ε) ⤜ (λz. Lap_dist0_list (1 / ε) n ⤜ (λzs. (return (listM borel) (list_insert z zs k)) ⤜ (λys. return (listM borel) (y # ys))))))"
proof(subst bind_assoc)
show "⋀y. (λz. Lap_dist0_list (1 / ε) n ⤜ (λzs. return (listM borel) (list_insert z zs k))) ∈ Lap_dist0 (1/ε) →⇩M subprob_algebra (listM borel)"
unfolding list_insert_def by measurable
show "⋀y. (λys. return (listM borel) (y # ys)) ∈ listM borel →⇩M subprob_algebra (listM borel)"
by measurable
show "Lap_dist0 (1/ε) ⤜ (λy. Lap_dist0 (1/ε) ⤜ (λx. Lap_dist0_list (1 / ε) n ⤜ (λzs. return (listM borel) (list_insert x zs k)) ⤜ (λys. return (listM borel) (y # ys)))) = Lap_dist0 (1/ε) ⤜ (λy. Lap_dist0 (1/ε) ⤜ (λz. Lap_dist0_list (1 / ε) n ⤜ (λzs. return (listM borel) (list_insert z zs k) ⤜ (λys. return (listM borel) (y # ys)))))"
by(subst bind_assoc,auto simp:list_insert_def) measurable
qed
also have "... = Lap_dist0 (1/ε) ⤜ (λy. (Lap_dist0 (1/ε) ⤜ (λz. Lap_dist0_list (1 / ε) n ⤜ (λzs. return (listM borel) (y # (list_insert z zs k))))))"
by(subst bind_return,auto simp:list_insert_def space_listM) measurable
also have "... = Lap_dist0 (1/ε) ⤜ (λz. (Lap_dist0 (1/ε) ⤜ (λy. Lap_dist0_list (1 / ε) n ⤜ (λzs. return (listM borel) ((list_insert y (z # zs) (Suc k)))))))"
unfolding list_insert_def by auto
also have "... = Lap_dist0 (1/ε) ⤜ (λy. (Lap_dist0 (1/ε) ⤜ (λz. Lap_dist0_list (1 / ε) n ⤜ (λzs. return (listM borel) ((list_insert y (z # zs) (Suc k)))))))"
proof(subst Giry_Monad.pair_prob_space.bind_rotate)
show "pair_prob_space (Lap_dist0 (1/ε)) (Lap_dist0 (1/ε))"
unfolding pair_prob_space_def pair_sigma_finite_def prob_space_Lap_dist using prob_space_Lap_dist prob_space_imp_sigma_finite by auto
show "(λ(x, y). Lap_dist0_list (1 / ε) n ⤜ (λzs. return (listM borel) (list_insert y (x # zs) (Suc k)))) ∈ Lap_dist0 (1/ε) ⨂⇩M Lap_dist0 (1/ε) →⇩M subprob_algebra (listM borel)"
unfolding list_insert_def by auto
qed(auto)
also have "... = Lap_dist0 (1/ε) ⤜ (λy. (Lap_dist0 (1/ε) ⤜ (λz. Lap_dist0_list (1 / ε) n ⤜ (λzs. (return (listM borel) (z # zs)) ⤜ (λzs2. return (listM borel) ((list_insert y zs2 (Suc k))))))))"
by(subst bind_return,auto simp:space_listM list_insert_def) measurable
also have "... = Lap_dist0 (1/ε) ⤜ (λy. (Lap_dist0 (1/ε) ⤜ (λz. Lap_dist0_list (1 / ε) n ⤜ (λzs. (return (listM borel) (z # zs))) ⤜ (λzs2. return (listM borel) ((list_insert y zs2 (Suc k)))))))"
by(subst bind_assoc,auto simp:space_listM list_insert_def) measurable
also have "... = Lap_dist0 (1/ε) ⤜ (λy. Lap_dist0_list (1 / ε) (Suc n) ⤜ (λzs2. return (listM borel) ((list_insert y zs2 (Suc k)))))"
unfolding Lap_dist0_list.simps(2) by(subst bind_assoc[where N = "listM borel" and R = "listM borel",symmetric],auto simp:space_listM list_insert_def Lap_dist0_def)
finally show ?case.
qed
qed
qed
{
fix x :: real and xs :: "real list" assume lxs: "length xs = Suc n"
have xxsl: "⋀x. length (x # xs) = Suc (Suc n)"
using lxs by auto
have "RNM' (x # xs) = Lap_dist0_list (1 / ε) (Suc (Suc n)) ⤜ (λys. return (listM borel) (map2 (+) (x # xs) ys)) ⤜ (λys. return (count_space UNIV) (snd (max_argmax ys)))"
unfolding RNM'_def Lap_dist_list_def2 argmax_list_def lxs xxsl by auto
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. Lap_dist0_list (1 / ε) (Suc n) ⤜ (λx2. return (listM borel) (x1 # x2))) ⤜ (λys. return (listM borel) (map2 (+) (x # xs) ys)) ⤜ (λys. return (count_space UNIV) (snd (max_argmax ys)))"
unfolding Lap_dist0_list.simps(2) Lap_dist0_def by auto
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. Lap_dist0_list (1 / ε) (Suc n) ⤜ (λx2. (return (listM borel) (x1 # x2)) ⤜ (λys. return (listM borel) (map2 (+) (x # xs) ys)))) ⤜ (λys. return (count_space UNIV) (snd (max_argmax ys)))"
by(subst bind_assoc[where N ="(listM borel)" and R ="(listM borel)"],measurable)+
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. Lap_dist0_list (1 / ε) (Suc n) ⤜ (λx2. return (listM borel) (map2 (+) (x # xs) (x1 # x2)))) ⤜ (λys. return (count_space UNIV) (snd (max_argmax ys)))"
by(subst bind_return,measurable)
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. Lap_dist0_list (1 / ε) (Suc n) ⤜ (λx2. return (listM borel) ((x + x1) # (map2 (+) xs x2)))) ⤜ (λys. return (count_space UNIV) (snd (max_argmax ys)))"
unfolding list.map by auto
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. Lap_dist0_list (1 / ε) (Suc n) ⤜ (λx2. (return (listM borel) ((x + x1) # (map2 (+) xs x2))) ⤜ (λys. return (count_space UNIV) (snd (max_argmax ys)))))"
by(subst bind_assoc[where N ="(listM borel)" and R ="(count_space UNIV)"],measurable)+
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. Lap_dist0_list (1 / ε) (Suc n) ⤜ (λx2. return (count_space UNIV) (snd (max_argmax ((x + x1) # (map2 (+) xs x2))))))"
by(subst bind_return,measurable)
also have "... = Lap_dist0_list (1 / ε) (Suc n) ⤜ (λx2. Lap_dist0 (1/ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax ((x + x1) # (map2 (+) xs x2))))))"
proof(subst Giry_Monad.pair_prob_space.bind_rotate)
show "pair_prob_space (Lap_dist0 (1/ε)) ( Lap_dist0_list (1 / ε) (Suc n))"
unfolding pair_prob_space_def pair_sigma_finite_def
by (meson prob_space_Lap_dist0 prob_space_Lap_dist0_list prob_space_imp_sigma_finite)
have "(λ(xa, y). return (count_space UNIV) (snd (max_argmax ((x + xa) # map2 (+) xs y)))) = (return (count_space UNIV)) o (λ zs. snd (max_argmax zs)) o (λ(xa, y). ((x + xa) # map2 (+) xs y))"
by auto
also have "... ∈ Lap_dist0 (1/ε) ⨂⇩M Lap_dist0_list (1 / ε) (Suc n) →⇩M subprob_algebra (count_space UNIV)"
by(intro measurable_comp[where N = "listM borel"] measurable_comp[where N = "(count_space UNIV)"], measurable)
finally show "(λ(xa, y). return (count_space UNIV) (snd (max_argmax ((x + xa) # map2 (+) xs y)))) ∈ Lap_dist0 (1/ε) ⨂⇩M Lap_dist0_list (1 / ε) (Suc n) →⇩M subprob_algebra (count_space UNIV)".
qed(auto)
finally have "RNM' (x # xs) = Lap_dist0_list (1 / ε) (Suc n) ⤜ (λx2. Lap_dist0 (1/ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax ((x + x1) # map2 (+) xs x2)))))".
}note * = this
show ?case proof(cases"i = 0")
case True
hence xxs: "(list_insert x xs i) = x # xs"
unfolding list_insert_def by auto
have "RNM' (list_insert x xs i) = Lap_dist0_list (1 / ε) (Suc n) ⤜ (λx2. Lap_dist0 (1/ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax ((x + x1) # (map2 (+) xs x2))))))"
unfolding xxs using *[of xs x, OF Suc(2)] by auto
also have "... = Lap_dist0_list (1 / ε) (length xs) ⤜ (λrs. RNM_M xs rs x i)"
unfolding RNM_M_def argmax_insert_def True drop_0 take_0 Suc.prems argmax_list_def comp_def list_insert_def
by (metis (no_types, lifting) Cons_eq_appendI add.commute case_prod_conv ext self_append_conv2)
finally show ?thesis.
next
case False
then obtain k :: nat where i: "i = Suc k"
by (metis list_decode.cases)
hence insxxsi: "(list_insert x xs i) = a # (list_insert x ys k)"
unfolding list_insert_def using xs by auto
have klessn: "k ≤ n"
using n i using Suc.prems(2) by auto
have leninsxxsi: "length (list_insert x ys k) = Suc n"
unfolding list_insert_def length_append length_drop length_take n using klessn by auto
have "RNM' (list_insert x xs i) = Lap_dist0_list (1 / ε) (Suc n)⤜ (λx2. Lap_dist0 (1/ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax ((a + x1) # map2 (+) (list_insert x ys k) x2)))))"
unfolding insxxsi *[of"(list_insert x ys k)"a,OF leninsxxsi] by auto
also have "... = (Lap_dist0 (1/ε) ⤜ (λp. Lap_dist0_list (1 / ε) n ⤜ (λps. return (listM borel) (list_insert p ps k)))) ⤜ (λx2. Lap_dist0 (1/ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax ((a + x1) # map2 (+) (list_insert x ys k) x2)))))"
unfolding Lap_mechanism_multi_replicate_insert[of k n, OF klessn] by auto
also have "... = Lap_dist0 (1/ε) ⤜ (λp. Lap_dist0_list (1 / ε) n ⤜ (λps. (return (listM borel) (list_insert p ps k)) ⤜ (λx2. Lap_dist0 (1/ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax ((a + x1) # map2 (+) (list_insert x ys k) x2)))))))"
proof(subst bind_assoc[where N ="(listM borel)" and R ="count_space UNIV"])
show "(λp. Lap_dist0_list (1 / ε) n ⤜ (λps. return (listM borel) (list_insert p ps k))) ∈ Lap_dist0 (1/ε) →⇩M subprob_algebra (listM borel)"
unfolding list_insert_def by measurable
show 1: "(λx2. Lap_dist0 (1/ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax ((a + x1) # map2 (+) (list_insert x ys k) x2))))) ∈ listM borel →⇩M subprob_algebra (count_space UNIV)"
by(rule measurable_bind[where N = "borel"],auto)
thus "Lap_dist0 (1/ε) ⤜
(λxa. Lap_dist0_list (1 / ε) n ⤜ (λps. return (listM borel) (list_insert xa ps k)) ⤜
(λx2. Lap_dist0 (1/ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax ((a + x1) # map2 (+) (list_insert x ys k) x2)))))) =
Lap_dist0 (1/ε) ⤜
(λp. Lap_dist0_list (1 / ε) n ⤜
(λps. return (listM borel) (list_insert p ps k) ⤜ (λx2. Lap_dist0 (1/ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax ((a + x1) # map2 (+) (list_insert x ys k) x2)))))))"
unfolding list_insert_def
by(subst bind_assoc[where N ="listM borel" and R ="count_space UNIV"],auto)
qed
also have "... = Lap_dist0 (1/ε) ⤜ (λp. Lap_dist0_list (1 / ε) n ⤜ (λps. Lap_dist0 (1/ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax ((a + x1) # map2 (+) (list_insert x ys k) (list_insert p ps k)))))))"
by(subst bind_return[where N = "count_space UNIV"],auto)
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. Lap_dist0_list (1 / ε) n ⤜ (λps. Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (map2 (+) (list_insert x (a # ys) (Suc k)) (list_insert x1 (p # ps) (Suc k))))))))"
unfolding list_insert_def by auto
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. Lap_dist0_list (1 / ε) n ⤜ (λps. Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) (p # ps)) (Suc k)))))))"
proof-
have "AE ps in Lap_dist0_list (1 / ε) n. ∀ x1 p. (snd (max_argmax (map2 (+) (list_insert x (a # ys) (Suc k)) (list_insert x1 (p # ps) (Suc k))))) = (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) (p # ps)) (Suc k))))"
proof(rule AE_mp)
show "⋀x1 p. almost_everywhere (Lap_dist0_list (1 / ε) n) (λps. ps ∈ {ps. length ps = n})"
proof(rule prob_space.AE_prob_1)
show "prob_space (Lap_dist0_list (1 / ε) n)"
by auto
show "Sigma_Algebra.measure (Lap_dist0_list (1 / ε) n) {ps. length ps = n} = 1"
unfolding Lap_dist0_list_Lap_dist_list[symmetric] using emeasure_Lap_dist_list_length [of "(1 / ε)" "(replicate n 0)"] unfolding measure_def length_replicate by auto
qed
show x: "AE ps∈{ps. length ps = n} in Lap_dist0_list (1 / ε) n.
∀x1 p.
snd (max_argmax (map2 (+) (list_insert x (a # ys) (Suc k)) (list_insert x1 (p # ps) (Suc k)))) =
snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) (p # ps)) (Suc k)))"
proof(rule AE_I2,rule impI,intro allI)
fix x1 p ps assume "ps ∈ space (Lap_dist0_list (1 / ε) n)" and "ps ∈ {ps. length ps = n}"
hence "length ps = n"by auto
hence l: "length ps = length ys"using n by auto
hence "(map2 (+) (list_insert x (a # ys) (Suc k)) (list_insert x1 (p # ps) (Suc k))) = map (λ (x,y). x + y) (zip (take (Suc k) (a # ys) @ [x] @ drop (Suc k) (a # ys)) (take (Suc k) (p # ps) @ [x1] @ drop (Suc k) (p # ps)))"
unfolding list_insert_def by auto
also have "... = map (λ (x,y). x + y) ((zip (take (Suc k) (a # ys))(take (Suc k) (p # ps))) @ [(x,x1)] @ (zip (drop (Suc k) (a # ys)))(drop (Suc k) (p # ps)))"
using l zip_append by auto
also have "... = map (λ (x,y). x + y) ((take (Suc k) (zip (a # ys) (p # ps))) @ [(x,x1)] @ (drop (Suc k) (zip (a # ys)(p # ps))))"
using l take_zip drop_zip by metis
also have "... = list_insert (x + x1) (map2 (+) (a # ys) (p # ps)) (Suc k)"
unfolding list_insert_def map_append drop_map take_map by auto
finally have "map2 (+) (list_insert x (a # ys) (Suc k)) (list_insert x1 (p # ps) (Suc k)) = list_insert (x + x1) (map2 (+) (a # ys) (p # ps)) (Suc k)".
thus"snd (max_argmax (map2 (+) (list_insert x (a # ys) (Suc k)) (list_insert x1 (p # ps) (Suc k)))) = snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) (p # ps)) (Suc k)))"by auto
qed
qed
hence x1: "⋀ x1. AE ps in Lap_dist0_list (1 / ε) n. (Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (map2 (+) (list_insert x (a # ys) (Suc k)) (list_insert x1 (p # ps) (Suc k))))))) = (Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) (p # ps)) (Suc k))))))"
using AE_mp by auto
hence "∀ x1. Lap_dist0_list (1 / ε) n ⤜
(λps. Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (map2 (+) (list_insert x (a # ys) (Suc k)) (list_insert x1 (p # ps) (Suc k))))))) =
Lap_dist0_list (1 / ε) n ⤜
(λps. Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) (p # ps)) (Suc k))))))"(is"∀ x1. ?P x1")
proof(intro allI)
fix x1 show "?P x1"
proof(rule bind_cong_AE'[of"Lap_dist0_list (1 / ε) n" "listM borel" "(λps. Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (map2 (+) (list_insert x (a # ys) (Suc k)) (list_insert x1 (p # ps) (Suc k)))))))" "(count_space UNIV) :: nat measure" "(λps. Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) (p # ps)) (Suc k))))))",OF _ _ _ x1])
show "Lap_dist0_list (1 / ε) n ∈ space (prob_algebra (listM borel))"
by auto
have 1: "take (Suc k) (a # ys) @ [x] @ drop (Suc k) (a # ys) ∈ space (listM borel)"
using space_listM_borel_UNIV by auto
have 2: "[x1] ∈ space (listM borel)"
by auto
show "(λps. Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (map2 (+) (list_insert x (a # ys) (Suc k)) (list_insert x1 (p # ps) (Suc k))))))) ∈ listM borel →⇩M prob_algebra (count_space UNIV)" unfolding list_insert_def
using 1 2 by measurable
have 3: "[x + x1] ∈ space (listM borel)"
by auto
show "(λps. Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) (p # ps)) (Suc k)))))) ∈ listM borel →⇩M prob_algebra (count_space UNIV)"
unfolding list_insert_def using 1 3 by measurable
qed
qed
thus"Lap_dist0 (1/ε) ⤜
(λx1. Lap_dist0_list (1 / ε) n ⤜
(λps. Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (map2 (+) (list_insert x (a # ys) (Suc k)) (list_insert x1 (p # ps) (Suc k)))))))) =
Lap_dist0 (1/ε) ⤜
(λx1. Lap_dist0_list (1 / ε) n ⤜
(λps. Lap_dist0 (1/ε) ⤜ (λp. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) (p # ps)) (Suc k)))))))"
by(auto elim!: bind_cong_AE')
qed
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. Lap_dist0_list (1 / ε) n ⤜ (λps. Lap_dist0 (1/ε) ⤜ (λp. (return (listM borel)(p # ps)) ⤜ (λrs. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) rs) (Suc k))))))))"
unfolding list_insert_def by(subst bind_return,measurable)
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. ((Lap_dist0_list (1 / ε) n ⤜ (λps. Lap_dist0 (1/ε) ⤜ (λp. (return (listM borel)(p # ps))) ⤜ (λrs. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) rs) (Suc k)))))))))"
unfolding list_insert_def by(subst bind_assoc,measurable)
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. ((Lap_dist0_list (1 / ε) n ⤜ (λps. Lap_dist0 (1/ε) ⤜ (λp. (return (listM borel)(p # ps)))) ⤜ (λrs. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) rs) (Suc k))))))))"
unfolding list_insert_def
by(subst bind_assoc[where N = "listM borel" and R = "count_space UNIV", THEN sym],auto)
also have "... = Lap_dist0 (1/ε) ⤜ (λx1. (Lap_dist0_list (1 / ε) (Suc n) ⤜ (λrs. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) rs) (Suc k)))))))"
unfolding Lap_dist0_list.simps Lap_dist0_def proof(subst pair_prob_space.bind_rotate [where N = "listM borel"])
show "pair_prob_space (Lap_dist0_list (1 / ε) n) (Lap_dist (1 / ε) 0)"
unfolding pair_prob_space_def pair_sigma_finite_def Lap_dist_list_def2[symmetric] using prob_space_Lap_dist prob_space_Lap_dist
by (auto simp: prob_space_imp_sigma_finite)
qed auto
also have "... = Lap_dist0_list (1 / ε) (Suc n) ⤜ (λrs. Lap_dist0 (1/ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) rs) (Suc k))))))"
proof(subst pair_prob_space.bind_rotate[where N = "count_space UNIV"])
show "pair_prob_space (Lap_dist0 (1 / ε)) (Lap_dist0_list (1 / ε) (Suc n))"
unfolding pair_prob_space_def pair_sigma_finite_def using prob_space_Lap_dist0 prob_space_Lap_dist0_list prob_space_imp_sigma_finite by metis
show "(λ(xa, y). return (count_space UNIV) (snd (max_argmax (list_insert (x + xa) (map2 (+) (a # ys) y) (Suc k))))) ∈ Lap_dist0 (1/ε) ⨂⇩M Lap_dist0_list (1 / ε) (Suc n) →⇩M subprob_algebra (count_space UNIV)"
unfolding list_insert_def listM_Nil by measurable
qed(auto)
finally have *: " RNM' (list_insert x xs i) = Lap_dist0_list (1 / ε) (Suc n) ⤜ (λrs. Lap_dist0 (1 / ε) ⤜ (λx1. return (count_space UNIV) (snd (max_argmax (list_insert (x + x1) (map2 (+) (a # ys) rs) (Suc k))))))" .
show ?thesis unfolding RNM_M_def * argmax_insert_def case_prod_beta argmax_list_def comp_def
by (simp add: i n xs Suc.prems list_insert_def Groups.add_ac(2))
qed
qed
lemma DP_RNM'_M_i:
fixes xs ys :: "real list" and i n :: nat
assumes lxs: "length xs = n"
and lys: "length ys = n"
and adj: "list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) xs ys"
shows "𝒫(j in (RNM' xs). j = i) ≤ (exp ε) * 𝒫(j in (RNM' ys). j = i) ∧ 𝒫(j in (RNM' ys). j = i) ≤ (exp ε) * 𝒫(j in (RNM' xs). j = i)"
using assms proof(cases"n = 0")
case True
hence xs: "xs = []" and ys: "ys = []"
using lxs lys by blast+
have 0: "RNM' [] = return (count_space UNIV) 0"using RNM'_Nil by auto
thus ?thesis proof(cases"i = 0")
case True
hence 02: "𝒫(j in local.RNM' []. j = 0) = 1"unfolding 0 measure_def by auto
show ?thesis unfolding xs ys True 02 using pose by auto
next
case False
hence 02: "𝒫(j in local.RNM' []. j = i) = 0"unfolding 0 measure_def by auto
show ?thesis unfolding xs ys 02 by auto
qed
next
case False
have space_Lap_dist_multi [simp]: "⋀ xs b. space (Lap_dist_list b xs) = UNIV"
by (auto simp: sets_Lap_dist_list sets_eq_imp_space_eq)
have space_RNM'_UNIV[simp]: "⋀xs. space (local.RNM' xs) = UNIV"
unfolding RNM'_def by (metis empty_not_UNIV sets_return space_Lap_dist_multi space_bind space_count_space)
hence space_RNM'_UNIV2[simp]: "⋀xs i. {j. j∈ space (RNM' xs) ∧ j = i} = {i}"
by auto
thus ?thesis proof(cases"i < n")
case True
define x where x: "x = nth xs i"
define y where y: "y = nth ys i"
define xs2 where xs2: "xs2 = (list_exclude i xs)"
define ys2 where ys2: "ys2 = (list_exclude i ys)"
have xs: "xs = (list_insert x xs2 i)"
by (metis length_0_conv length_greater_0_conv list_insert'_is_list_insert lxs cong_nth_total_nth False True insert_exclude x xs2)
have ys: "ys = (list_insert y ys2 i)"
by (metis length_0_conv length_greater_0_conv list_insert'_is_list_insert lys cong_nth_total_nth False True insert_exclude y ys2)
obtain m :: nat where n: "n = Suc m"using True False not0_implies_Suc by blast
have lxs2: "length xs2 = m"
by (metis One_nat_def True add.assoc add.commute add_left_imp_eq id_take_nth_drop length_append list.size(4) list_exclude_def lxs n plus_1_eq_Suc xs2)
have lys2: "length ys2 = m"
by (metis One_nat_def True add.assoc add.commute add_left_imp_eq id_take_nth_drop length_append list.size(4) list_exclude_def lys n plus_1_eq_Suc ys2)
have ilessm: "i ≤ m"
using True n by auto
have 1: "take i xs2 = take i xs"
unfolding xs2 list_exclude_def by auto have 2: "take i ys2 = take i ys"
unfolding ys2 list_exclude_def by auto
have 3: "drop i xs2 = drop (Suc i) xs"
by (metis"1"append_eq_append_conv append_take_drop_id list_exclude_def xs2)
have 4: "drop i ys2 = drop (Suc i) ys"
by (metis"2"append_eq_append_conv append_take_drop_id list_exclude_def ys2)
from adj have 5: "list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) (take i xs2)(take i ys2)" and 6: "list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) (drop i xs2)(drop i ys2)"
unfolding 1 2 3 4 using list_all2_takeI list_all2_dropI by blast+
have adj': "x ≥ y ∧ x ≤ y + 1"
unfolding x y using list_all2_conv_all_nth True False lxs lys adj by (metis (mono_tags, lifting))
have adj2: "list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) xs2 ys2"
using 5 6 lxs2 lys2 append_take_drop_id[of i xs2,THEN sym] append_take_drop_id[of i ys2,THEN sym] list_all2_appendI by fastforce
note * = DP_RNM_M_i[of xs2 m ys2 _ y x, OF lxs2 lys2 _ adj' adj2 ilessm]
have 7: "local.RNM' xs = (Lap_dist0_list (1 /ε) m) ⤜ (λrs. RNM_M xs2 rs x i)"
using RNM'_expand[of xs2 m i x,OF lxs2 ilessm] unfolding xs lxs2 by auto
have 8: "local.RNM' ys = (Lap_dist0_list (1 /ε) m) ⤜ (λrs. local.RNM_M ys2 rs y i)"
using RNM'_expand[of ys2 m i y,OF lys2 ilessm] unfolding ys lys2 by auto
have "𝒫(j in local.RNM' xs. j = i) = measure (Lap_dist0_list (1 /ε) m ⤜ (λrs. local.RNM_M xs2 rs x i)) {i}"
by (metis"7"space_RNM'_UNIV2)
also have "... = (LINT rs|Lap_dist0_list (1 /ε) m. measure (local.RNM_M xs2 rs x i) {i})"
proof(rule subprob_space.measure_bind)
show "subprob_space (Lap_dist0_list (1 /ε) m)"
by (metis prob_space_Lap_dist0_list prob_space_imp_subprob_space)
thus "(λrs. local.RNM_M xs2 rs x i) ∈ (Lap_dist0_list (1 /ε) m) →⇩M subprob_algebra (count_space UNIV)"
unfolding RNM_M_def argmax_insert_def argmax_list_def using list_insert_def by auto
show "{i} ∈ sets (count_space UNIV)"
by auto
qed
also have "... = (∫ rs ∈ space (Lap_dist0_list (1 /ε) m). measure (local.RNM_M xs2 rs x i) {i} ∂(Lap_dist0_list (1 /ε) m))"
unfolding set_lebesgue_integral_def
by (metis (no_types, lifting) Bochner_Integration.integral_cong indicator_eq_1_iff scaleR_simps(12))
also have "... = (∫ rs ∈ {xs. length xs = m} . measure (local.RNM_M xs2 rs x i) {i} ∂(Lap_dist0_list (1 /ε) m))"
proof(subst set_integral_null_delta)
show "integrable (Lap_dist0_list (1 /ε) m) (λrs. Sigma_Algebra.measure (local.RNM_M xs2 rs x i) {i})"
by(rule probability_kernel_evaluation_integrable[where M ="count_space UNIV"],auto simp: RNM_M_def argmax_insert_def prob_space.finite_measure)
show 1: "{xs. length xs = m} ∈ sets (Lap_dist0_list (1 /ε) m)"
unfolding sets_Lap_dist0_list using sets_listM_length[of borel m] by auto
show "space (Lap_dist0_list (1 /ε) m) ∈ sets (Lap_dist0_list (1 /ε) m)"
by blast
have "emeasure (Lap_dist0_list (1 /ε) m) (space (Lap_dist0_list (1 /ε) m)) = 1"
by(rule prob_space.emeasure_space_1,auto)
hence "emeasure (Lap_dist0_list (1 /ε) m) (space (Lap_dist0_list (1 /ε) m) - {xs. length xs = m}) = 0"
using emeasure_Lap_dist_list_length[of " (1 /ε)" "replicate m 0"] unfolding length_replicate length_map Lap_dist0_list_Lap_dist_list[symmetric] space_Lap_dist_multi
proof(subst emeasure_Diff)
have "space (Lap_dist_list (1 / ε) (replicate m 0)) ∈ sets (Lap_dist_list (1 / ε) (replicate m 0))"
by blast
thus " UNIV ∈ sets (Lap_dist_list (1 / ε) (replicate m 0))"
unfolding sets_Lap_dist_list by auto
show "{xs. length xs = m} ∈ sets (Lap_dist_list (1 / ε) (replicate m 0))"
unfolding sets_Lap_dist_list using sets_listM_length[of borel m] space_borel lists_UNIV by auto
qed(auto)
thus "sym_diff (space (Lap_dist0_list (1 / ε) m)) {xs. length xs = m} ∈ null_sets (Lap_dist0_list (1 / ε) m)"
by (metis"1"Diff_mono null_setsI sets.compl_sets sets.sets_into_space sup.orderE)
qed(auto)
finally have 9: " 𝒫(j in RNM' xs. j = i) = (∫rs∈{xs. length xs = m}. Sigma_Algebra.measure (RNM_M xs2 rs x i) {i}∂Lap_dist0_list (1 / ε) m)".
have "𝒫(j in local.RNM' ys. j = i) = measure (Lap_dist0_list (1 /ε) m ⤜ (λrs. local.RNM_M ys2 rs y i)) {i}"
by (metis"8"space_RNM'_UNIV2)
also have "... = LINT rs| Lap_dist0_list (1 /ε) m. measure (local.RNM_M ys2 rs y i) {i}"
proof(rule subprob_space.measure_bind)
show "subprob_space (Lap_dist0_list (1 /ε) m)"
by (metis prob_space_Lap_dist0_list prob_space_imp_subprob_space)
show "(λrs. local.RNM_M ys2 rs y i) ∈ Lap_dist0_list (1 /ε) m →⇩M subprob_algebra (count_space UNIV)"
unfolding RNM_M_def argmax_insert_def by(auto simp: list_insert_def)
show "{i} ∈ sets (count_space UNIV)"by auto
qed
also have "... = (∫ rs ∈ space (Lap_dist0_list (1 /ε) m) . measure (local.RNM_M ys2 rs y i) {i} ∂(Lap_dist0_list (1 /ε) m))"
unfolding set_lebesgue_integral_def
by (metis (no_types, lifting) Bochner_Integration.integral_cong indicator_eq_1_iff scaleR_simps(12))
also have "... = (∫ rs ∈ {ys. length ys = m} . measure (local.RNM_M ys2 rs y i) {i} ∂(Lap_dist0_list (1 /ε) m))"
proof(subst set_integral_null_delta)
show "integrable (Lap_dist0_list (1 /ε) m) (λrs. Sigma_Algebra.measure (local.RNM_M ys2 rs y i) {i})"
by(rule probability_kernel_evaluation_integrable[where M ="count_space UNIV"],auto simp: RNM_M_def argmax_insert_def prob_space.finite_measure)
show 1: "{ys. length ys = m} ∈ sets (Lap_dist0_list (1 /ε) m)"
unfolding sets_Lap_dist0_list using sets_listM_length[of borel m] by auto
show "space (Lap_dist0_list (1 /ε) m) ∈ sets (Lap_dist0_list (1 /ε) m)"
by blast
have "emeasure (Lap_dist0_list (1 /ε) m) (space (Lap_dist0_list (1 /ε) m)) = 1"
by(rule prob_space.emeasure_space_1,auto)
hence "emeasure (Lap_dist0_list (1 /ε) m) (space (Lap_dist0_list (1 /ε) m) - {ys. length ys = m}) = 0"
using emeasure_Lap_dist_list_length[of " (1 /ε)" "replicate m 0"]
unfolding length_replicate length_map Lap_dist0_list_Lap_dist_list[symmetric] space_Lap_dist_multi
proof(subst emeasure_Diff)
have "space (Lap_dist_list (1 / ε) (replicate m 0)) ∈ sets (Lap_dist_list (1 / ε) (replicate m 0))"
by blast
thus " UNIV ∈ sets (Lap_dist_list (1 / ε) (replicate m 0))"
unfolding sets_Lap_dist_list[of "(1 / ε)" "(replicate m 0)"] space_Lap_dist_list[of "(1 / ε)" "(replicate m 0)"] space_listM space_borel lists_UNIV by auto
show "{xs. length xs = m} ∈ sets (Lap_dist_list (1 / ε) (replicate m 0))"
unfolding sets_Lap_dist_list[of "(1 / ε)" "(replicate m 0)"]
using sets_listM_length[of borel m] space_borel lists_UNIV by auto
qed(auto)
thus "sym_diff (space (Lap_dist0_list (1 / ε) m)) {xs. length xs = m} ∈ null_sets (Lap_dist0_list (1 / ε) m)"
by (metis"1"Diff_mono null_setsI sets.compl_sets sets.sets_into_space sup.orderE)
qed(auto)
finally have 10: "𝒫(j in local.RNM' ys. j = i) = (∫rs∈{ys. length ys = m}. Sigma_Algebra.measure (local.RNM_M ys2 rs y i) {i}∂Lap_dist0_list (1 / ε) m)".
have c: "finite_measure (Lap_dist0_list (1 / ε) m)"
by (auto simp: prob_space.finite_measure)
show ?thesis
proof(rule conjI)
show "𝒫(j in local.RNM' xs. j = i) ≤ exp ε * 𝒫(j in local.RNM' ys. j = i)"
unfolding 9 10
proof(subst set_integral_mult_right[THEN sym],intro set_integral_mono)
show "⋀rs. rs ∈ {xs. length xs = m} ⟹ Sigma_Algebra.measure (local.RNM_M xs2 rs x i) {i} ≤ exp ε * Sigma_Algebra.measure (local.RNM_M ys2 rs y i) {i}"
using conjunct1[OF *] space_RNM_M by auto
show "set_integrable (Lap_dist0_list (1 / ε) m) {xs. length xs = m} (λxa. Sigma_Algebra.measure (local.RNM_M xs2 xa x i) {i})"
unfolding set_integrable_def real_scaleR_def
proof(intro integrable_ess_bounded_finite_measure c ess_bounded_mult indicat_real_ess_bounded probability_kernel_evaluation_ess_bounded)
show "{xs. length xs = m} ∈ sets (Lap_dist0_list (1 / ε) m)"
unfolding Lap_dist0_list_Lap_dist_list[symmetric] sets_Lap_dist_list using sets_listM_length[of borel m] by auto
show "(λxa. local.RNM_M xs2 xa x i) ∈ Lap_dist0_list (1 / ε) m →⇩M prob_algebra (count_space UNIV)"
unfolding RNM_M_def argmax_insert_def by(auto simp: list_insert_def)
qed(auto)
show "set_integrable (Lap_dist0_list (1 / ε) m) {xs. length xs = m} (λx. exp ε * Sigma_Algebra.measure (local.RNM_M ys2 x y i) {i})"
unfolding set_integrable_def real_scaleR_def
proof(intro integrable_ess_bounded_finite_measure c ess_bounded_mult indicat_real_ess_bounded probability_kernel_evaluation_ess_bounded)
show "{xs. length xs = m} ∈ sets (Lap_dist0_list (1 / ε) m)"
unfolding Lap_dist0_list_Lap_dist_list[symmetric] sets_Lap_dist_list using sets_listM_length[of borel m] by auto
show "(λx. local.RNM_M ys2 x y i) ∈ Lap_dist0_list (1 / ε) m →⇩M prob_algebra (count_space UNIV)"
unfolding RNM_M_def argmax_insert_def by(auto simp: list_insert_def)
qed(auto)
qed
show "𝒫(j in local.RNM' ys. j = i) ≤ exp ε * 𝒫(j in local.RNM' xs. j = i)"
unfolding 9 10
proof(subst set_integral_mult_right[THEN sym],intro set_integral_mono)
show "⋀rs. rs ∈ {ys. length ys = m} ⟹ Sigma_Algebra.measure (local.RNM_M ys2 rs y i) {i} ≤ exp ε * Sigma_Algebra.measure (local.RNM_M xs2 rs x i) {i}"
using conjunct2[OF *] space_RNM_M by auto
show "set_integrable (Lap_dist0_list (1 / ε) m) {ys. length ys = m} (λx. Sigma_Algebra.measure (local.RNM_M ys2 x y i) {i})"
unfolding set_integrable_def real_scaleR_def
proof(intro integrable_ess_bounded_finite_measure c ess_bounded_mult indicat_real_ess_bounded probability_kernel_evaluation_ess_bounded)
show "{xs. length xs = m} ∈ sets (Lap_dist0_list (1 / ε) m)"
unfolding Lap_dist0_list_Lap_dist_list[symmetric] sets_Lap_dist_list using sets_listM_length[of borel m] by auto
show "(λx. local.RNM_M ys2 x y i) ∈ Lap_dist0_list (1 / ε) m →⇩M prob_algebra (count_space UNIV)"
unfolding RNM_M_def argmax_insert_def by(auto simp: list_insert_def)
qed(auto)
show "set_integrable (Lap_dist0_list (1 / ε) m) {ys. length ys = m} (λxa. exp ε * Sigma_Algebra.measure (local.RNM_M xs2 xa x i) {i})"
unfolding set_integrable_def real_scaleR_def
proof(intro integrable_ess_bounded_finite_measure c ess_bounded_mult indicat_real_ess_bounded probability_kernel_evaluation_ess_bounded)
show "{xs. length xs = m} ∈ sets (Lap_dist0_list (1 / ε) m)"
unfolding Lap_dist0_list_Lap_dist_list[symmetric] sets_Lap_dist_list using sets_listM_length[of borel m] by auto
show "(λxa. local.RNM_M xs2 xa x i) ∈ Lap_dist0_list (1 / ε) m →⇩M prob_algebra (count_space UNIV)"
unfolding RNM_M_def argmax_insert_def by(auto simp: list_insert_def)
qed(auto)
qed
qed
next
case False
hence xsl: "i ≥ length xs" and ysl: "i ≥ length ys"
using lxs lys by auto
have xs': "xs ≠ []" and ys': "ys ≠ []"using ‹n ≠ 0› assms by blast+
hence 1: "𝒫(j in local.RNM' xs. j = i) = 0"using RNM'_support[of xs i, OF xsl xs'] unfolding measure_def by auto
hence 2: "𝒫(j in local.RNM' ys. j = i) = 0"using RNM'_support[of ys i, OF ysl ys'] unfolding measure_def by auto
show ?thesis unfolding 1 2 by auto
qed
qed
lemma DP_divergence_RNM':
fixes xs ys :: "real list"
assumes adj: "list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) xs ys"
shows "DP_divergence (RNM' xs) (RNM' ys) ε ≤ 0 ∧ DP_divergence (RNM' ys) (RNM' xs) ε ≤ 0"
proof-
have sets_RNM': "⋀xs. sets (local.RNM' xs) = sets (count_space UNIV)"
unfolding RNM'_def
by (metis emeasure_empty indicator_eq_0_iff indicator_eq_1_iff prob_space.emeasure_space_1 prob_space_Lap_dist_list sets_bind sets_return)
hence space_RNM': "⋀xs. space (local.RNM' xs) = UNIV"
by (metis sets_eq_imp_space_eq space_count_space)
have 0: "⋀ xs A. emeasure (local.RNM' xs) A = ennreal (Sigma_Algebra.measure (local.RNM' xs) A)"
proof(intro finite_measure.emeasure_eq_measure)
fix xs :: "real list" and A :: "nat set"have "xs ∈ space(listM borel)"by auto
show "finite_measure (local.RNM' xs)"
by (meson ‹xs ∈ space (listM borel)› measurable_RNM' measurable_prob_algebraD subprob_space.axioms(1) subprob_space_kernel)
qed
have "length xs = length ys"
using adj by(auto simp: list_all2_lengthD)
then obtain n :: nat where lxs: "length xs = n" and lys: "length ys = n"
by auto
have 1: "⋀i :: nat. 𝒫(j in (RNM' xs). j = i) ≤ (exp ε) * 𝒫(j in (RNM' ys). j = i)
∧ 𝒫(j in (RNM' ys). j = i) ≤ (exp ε) * 𝒫(j in (RNM' xs). j = i)"
using DP_RNM'_M_i[OF lxs lys adj] by auto
hence "⋀i :: nat. 𝒫(j in (RNM' xs). j = i) ≤ (exp ε) * 𝒫(j in (RNM' ys). j = i)"
by auto
hence "⋀n :: nat. enn2real(measure (local.RNM' xs) {n}) ≤ enn2real((exp ε) * measure (local.RNM' ys){n})"
unfolding measure_def by (auto simp: space_RNM')
hence ineq1: "⋀n :: nat. emeasure (local.RNM' xs) {n} ≤ (exp ε) * emeasure (local.RNM' ys){n}"
unfolding 0
by (metis (no_types, opaque_lifting)"0"Sigma_Algebra.measure_def dual_order.trans enn2real_nonneg ennreal_enn2real ennreal_leI ennreal_mult'' linorder_not_le top_greatest)
from 1 have "⋀i :: nat. 𝒫(j in (RNM' ys). j = i) ≤ (exp ε) * 𝒫(j in (RNM' xs). j = i)"
by auto
hence "⋀n :: nat. enn2real(measure (local.RNM' ys) {n}) ≤ enn2real((exp ε) * measure (local.RNM' xs){n})"
unfolding measure_def by (auto simp: space_RNM')
hence ineq2: "⋀n :: nat. emeasure (local.RNM' ys) {n} ≤ (exp ε) * emeasure (local.RNM' xs){n}"
unfolding 0
by (metis (no_types, opaque_lifting)"0"Sigma_Algebra.measure_def dual_order.trans enn2real_nonneg ennreal_enn2real ennreal_leI ennreal_mult'' linorder_not_le top_greatest)
{
fix A :: "nat set" and xs :: "real list"
have "emeasure (local.RNM' xs) A = (∑i. emeasure (local.RNM' xs) ((λj :: nat. if j ∈ A then {j} else {}) i))"
proof(subst suminf_emeasure)
show "range (λi :: nat. if i ∈ A then {i} else {}) ⊆ sets (local.RNM' xs)"
using sets_RNM' by auto
show "disjoint_family (λi. if i ∈ A then {i} else {})"
unfolding disjoint_family_on_def by auto
show "emeasure (local.RNM' xs) A = emeasure (local.RNM' xs) (⋃i. if i ∈ A then {i} else {})"by auto
qed
also have "... = (∑i. emeasure (local.RNM' xs){i} * indicator A i)"
by(rule suminf_cong,auto)
finally have "emeasure (local.RNM' xs) A = (∑i. emeasure (local.RNM' xs) {i} * indicator A i)".
}note * = this
show ?thesis proof(rule conjI)
have "DP_divergence (local.RNM' xs) (local.RNM' ys) ε ≤ (0 :: real)"
proof(rule DP_divergence_leI)
fix A assume "A ∈ sets (local.RNM' xs)"
have "emeasure (local.RNM' xs) A = (∑i. emeasure (local.RNM' xs){i} * indicator A i)"
using *[of xs A] by auto
also have "... ≤ (∑i. (exp ε) * (emeasure (local.RNM' ys){i} * indicator A i))"
proof(rule suminf_le)
show "summable (λi. emeasure (local.RNM' xs) {i} * indicator A i)"by auto
show "summable (λi. ennreal (exp ε) * (emeasure (local.RNM' ys){i} * indicator A i))"by auto
show "⋀n. emeasure (local.RNM' xs) {n} * indicator A n ≤ ennreal (exp ε) * (emeasure (local.RNM' ys) {n} * indicator A n)"
using ineq1
by (metis ab_semigroup_mult_class.mult_ac(1) antisym_conv1 mult_right_mono nless_le zero_less_iff_neq_zero)
qed
also have "... = ennreal (exp ε) * (∑i. (emeasure (local.RNM' ys) {i} * indicator A i))"
by auto
also have "... = ennreal (exp ε) * emeasure (local.RNM' ys) A"
using *[of ys A] by auto
finally have "emeasure (local.RNM' xs) A ≤ ennreal (exp ε) * emeasure (local.RNM' ys) A".
thus"Sigma_Algebra.measure (local.RNM' xs) A ≤ exp ε * Sigma_Algebra.measure (local.RNM' ys) A + 0"
by (metis"0"add_cancel_right_right enn2real_eq_posreal_iff enn2real_leI ennreal_mult'' exp_ge_zero measure_nonneg split_mult_pos_le zero_less_measure_iff)
qed
thus"DP_divergence (local.RNM' xs) (local.RNM' ys) ε ≤ 0"using zero_ereal_def by auto
next
have "DP_divergence (local.RNM' ys) (local.RNM' xs) ε ≤ (0 :: real)"
proof(rule DP_divergence_leI)
fix A assume "A ∈ sets (local.RNM' ys)"
have "emeasure (local.RNM' ys) A = (∑i. emeasure (local.RNM' ys){i} * indicator A i)"
using *[of ys A] by auto
also have "... ≤ (∑i. (exp ε) * (emeasure (local.RNM' xs){i} * indicator A i))"
proof(rule suminf_le)
show "summable (λi. emeasure (local.RNM' ys) {i} * indicator A i)"by auto
show "summable (λi. ennreal (exp ε) * (emeasure (local.RNM' xs){i} * indicator A i))"by auto
show "⋀n. emeasure (local.RNM' ys) {n} * indicator A n ≤ ennreal (exp ε) * (emeasure (local.RNM' xs) {n} * indicator A n)"
using ineq2
by (metis ab_semigroup_mult_class.mult_ac(1) antisym_conv1 mult_right_mono nless_le zero_less_iff_neq_zero)
qed
also have "... = ennreal (exp ε) * (∑i. (emeasure (local.RNM' xs) {i} * indicator A i))"
by auto
also have "... = ennreal (exp ε) * emeasure (local.RNM' xs) A"
using *[of xs A] by auto
finally have "emeasure (local.RNM' ys) A ≤ ennreal (exp ε) * emeasure (local.RNM' xs) A".
thus"Sigma_Algebra.measure (local.RNM' ys) A ≤ exp ε * Sigma_Algebra.measure (local.RNM' xs) A + 0"
by (metis"0"add_cancel_right_right enn2real_eq_posreal_iff enn2real_leI ennreal_mult'' exp_ge_zero measure_nonneg split_mult_pos_le zero_less_measure_iff)
qed
thus"DP_divergence (local.RNM' ys) (local.RNM' xs) ε ≤ 0"using zero_ereal_def by auto
qed
qed
lemma differential_privacy_LapMech_RNM':
shows "differential_privacy RNM' {(xs, ys) | xs ys. list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) xs ys } ε 0"
unfolding differential_privacy_def DP_inequality_cong_DP_divergence
proof(rule ballI)
fix x::"real list × real list" assume " x ∈ {(xs, ys) |xs ys. list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) xs ys}"
then obtain xs ys where x: "x = (xs,ys)" and 1: "list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) xs ys"
by blast
thus "case x of (d1, d2) ⇒ DP_divergence (RNM' d1) (RNM' d2) ε ≤ ereal 0 ∧ DP_divergence (RNM' d2) (RNM' d1) ε ≤ ereal 0"
using DP_divergence_RNM'[of xs ys]
by (simp add: zero_ereal_def)
qed
corollary differential_privacy_LapMech_RNM'_sym:
shows "differential_privacy RNM' {(xs, ys) | xs ys. list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) xs ys ∨ list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) ys xs } ε 0"
proof-
have 1: " {(xs, ys) | xs ys. list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) xs ys ∨ list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) ys xs }
= {(xs, ys) | xs ys. list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) xs ys } ∪ converse {(xs, ys) | xs ys. list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) xs ys }"
by blast
show ?thesis unfolding 1 proof(rule differential_privacy_symmetrize)
show " differential_privacy RNM' {(xs, ys) |xs ys. list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) xs ys} ε 0"
by (rule differential_privacy_LapMech_RNM')
qed
qed
theorem differential_privacy_LapMech_RNM:
shows "differential_privacy (LapMech_RNM ε) adj ε 0"
unfolding LapMech_RNM_RNM'_c
proof(rule differential_privacy_preprocessing)
show "(0::real) ≤ ε"
using pose by auto
show "differential_privacy RNM' {(xs, ys) | xs ys. list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) xs ys ∨ list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) ys xs } ε 0"
by (rule differential_privacy_LapMech_RNM'_sym)
show "c ∈ M →⇩M listM borel"
using c by auto
show "∀(x, y)∈ adj. (c x, c y) ∈ {(xs, ys) |xs ys. list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) xs ys ∨ list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) ys xs}"
using cond adj by auto
show "adj ⊆ space M × space M"
using adj.
show " {(xs, ys) |xs ys. list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) xs ys ∨ list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) ys xs} ⊆ space (listM borel) × space (listM borel)"
unfolding space_listM space_borel lists_UNIV by auto
qed
end
end
subsection ‹ Formal Proof of Exact [Claim 3.9,AFDP]›
text ‹
In the above theorem @{thm Lap_Mechanism_RNM_mainpart.differential_privacy_LapMech_RNM}, the query @{term c} to add noise is abstracted.
We here instantiate it with the counting query. Thus we here formalize and show the monotonicity and Lipschitz property of it.
›
locale Lap_Mechanism_RNM_counting =
fixes n::nat
and m::nat
and Q :: "nat ⇒ nat ⇒ bool"
assumes "⋀i. i ∈ {0..<m} ⟹ (Q i) ∈ UNIV → UNIV"
begin
interpretation results_AFDP n
by(unfold_locales)
interpretation L1_norm_list "(UNIV::nat set)" "(λ x y. ¦int x - int y¦)" n
by(unfold_locales,auto)
lemma adjacency_1_int_list:
assumes "(xs,ys) ∈ adj_L1_norm"
shows "(xs = ys) ∨ (∃ as a b bs. xs = as @ (a # bs) ∧ ys = as @ (b # bs) ∧ ¦int a - int b¦ = 1)"
using assms unfolding adj_L1_norm_def sp_Dataset_def space_restrict_space dist_L1_norm_list_def space_L1_norm_list_def
proof(induction n arbitrary: xs ys)
case 0
hence "xs = []" and "ys = []" by auto
then show ?case by auto
next
case (Suc n)
hence "length xs = Suc n"
and "length ys = Suc n"
and sum:"(∑i = 1..Suc n. real_of_int ¦int (xs ! (i - 1)) - int (ys ! (i - 1))¦) ≤ 1"
by blast+
then obtain x y ::nat and xs2 ys2 ::"nat list"
where xs: "xs = x # xs2"
and ys: "ys = y # ys2"
and xs2: "length xs2 = n"
and ys2:"length ys2 = n"
by (meson length_Suc_conv)
hence 1: "¦int x - int y¦ + (∑i = 1..n. real_of_int ¦int (xs2 ! (i - 1)) - int (ys2 ! (i - 1))¦) = (∑i = 1..Suc n. real_of_int ¦int (xs ! (i - 1)) - int(ys ! (i - 1))¦)"
using L1_norm_list.list_sum_dist_Cons[symmetric, OF xs2 ys2] by auto
then show ?case
proof(cases "x = y")
case True
hence "¦x - y¦ = 0"
by auto
with 1 sum have 2: "(∑i = 1..n. real_of_int ¦int(xs2 ! (i - 1)) - int(ys2 ! (i - 1))¦) ≤ 1"
by auto
have *: "(xs2, ys2) ∈ {(xs, ys) |xs ys. xs ∈ {xs ∈ lists UNIV. length xs = n} ∧ ys ∈ {xs ∈ lists UNIV. length xs = n} ∧ (∑i = 1..n. real_of_int ¦int(xs ! (i - 1)) - int(ys ! (i - 1))¦) ≤ 1}"
using xs2 ys2 2 by auto
from Suc.IH[of xs2 ys2] * have "(xs2 = ys2) ∨ (∃ as a b bs. xs2 = as @ (a # bs) ∧ ys2 = as @ (b # bs) ∧ ¦int a - int b¦ = 1)"
unfolding space_listM space_count_space by auto
with True xs ys show ?thesis
by (meson Cons_eq_appendI)
next
case False
hence 0: "1 ≤ ¦int x - int y¦"
by auto
with 1 sum have 2: "(∑i = 1..n. real_of_int ¦int(xs2 ! (i - 1)) - int(ys2 ! (i - 1))¦) ≤ 0"
by auto
have "(∑i = 1..n. real_of_int ¦int(xs2 ! (i - 1)) - int(ys2 ! (i - 1))¦) ≥ 0"
by auto
with 2 have 3:"(∑i = 1..n. real_of_int ¦int(xs2 ! (i - 1)) - int(ys2 ! (i - 1))¦) = 0"
by argo
with sum 1 have " ¦int x - int y¦ ≤ 1"
by auto
with 0 have 4:" ¦int x - int y¦ = 1"
by auto
hence "xs2 = ys2" using xs2 ys2 3
proof(subst L1_norm_list.dist_L1_norm_list_zero[of "UNIV" "λ x y. real_of_int ¦int x - int y¦" xs2 n ys2 ,symmetric])
show 1: " L1_norm_list UNIV (λx y. real_of_int ¦int x - int y¦)"
by(unfold_locales)
show " (∑i = 1..n. real_of_int ¦int(xs2 ! (i - 1)) - int(ys2 ! (i - 1))¦) = 0 ⟹ L1_norm_list.dist_L1_norm_list (λx y. real_of_int ¦int x - int y¦) n xs2 ys2 = 0 "
unfolding L1_norm_list.dist_L1_norm_list_def[OF 1] by simp
qed(auto)
with False xs ys 4 show ?thesis by blast
qed
qed
paragraph ‹ formalization of a list of counting query ›
primrec counting'::"nat ⇒ nat ⇒ nat list ⇒ nat" where
"counting' i 0 _ = 0" |
"counting' i (Suc k) xs = (if Q i k then (nth_total 0 xs k) else 0) + counting' i k xs"
lemma measurable_counting'[measurable]:
shows "(λ xs. counting' i k xs) ∈ (listM (count_space (UNIV::nat set))) →⇩M (count_space (UNIV::nat set))"
by(induction k,auto)
lemma counting'_sum:
assumes "k ≤ length xs"
shows "counting' i k xs = (∑j∈{0..<k}. (if Q i j then (xs ! j) else 0))"
proof-
have "counting' i k xs = (∑j∈{0..<k}. (if Q i j then (nth_total 0 xs j) else 0))"
by(induction k,auto)
also have "... = (∑j∈{0..<k}. (if Q i j then (xs ! j) else 0))"
proof(subst sum.cong)
show "{0..<k} = {0..<k}" by auto
show " ⋀x. x ∈ {0..<k} ⟹ (if Q i x then (nth_total 0 xs x) else 0) = (if Q i x then xs ! x else 0)"
using assms unfolding nth_total_def2 by auto
qed(auto)
finally show ?thesis by auto
qed
lemma sensitvity_counting':
assumes "(xs,ys) ∈ adj_L1_norm"
and len: "k ≤ n"
shows "¦int (counting' i k xs) - int (counting' i k ys)¦ ≤ 1"
proof-
from assms have xsl: "length xs = n" and ysl: "length ys = n" and le: "dist_L1_norm_list xs ys ≤ 1" and i: "k ≤ length xs" and i2: "k ≤ length ys"
by (auto simp:space_L1_norm_list_def adj_L1_norm_def sp_Dataset_def space_restrict_space dist_L1_norm_list_def space_listM)
from adjacency_1_int_list[OF assms(1)]
consider "xs = ys" | "(∃as a b bs. xs = as @ a # bs ∧ ys = as @ b # bs ∧ ¦int a - int b¦ = 1)"
by auto
then show ?thesis
proof(cases)
case 1
then show ?thesis by auto
next
case 2
then obtain as a b bs
where xs: "xs = as @ a # bs"
and ys: "ys = as @ b # bs"
and a: "¦int a - int b¦ = 1"
by blast
then show ?thesis unfolding counting'_sum[OF i] counting'_sum[OF i2]
proof-
have "¦int (∑j = 0..<k. if Q i j then xs ! j else 0) - int (∑j = 0..<k. if Q i j then ys ! j else 0)¦
= ¦(∑j = 0..<k. (if Q i j then int (xs ! j) else int 0)) - (∑j = 0..<k. if Q i j then int (ys ! j) else int 0)¦"
unfolding of_nat_sum if_distrib by auto
also have "... = ¦(∑j = 0..<k. (if Q i j then int (xs ! j) else 0)) - (∑j = 0..<k. if Q i j then int (ys ! j) else 0)¦"
unfolding int_ops(1) by auto
also have "... = ¦(∑j = 0..<k. (if Q i j then int (xs ! j) else 0) - (if Q i j then int (ys ! j) else 0))¦"
by (auto simp: sum_subtractf)
also have "... = ¦(∑j = 0..<k. (if Q i j then int (xs ! j) - int (ys ! j) else 0))¦"
by (metis (full_types, opaque_lifting) cancel_comm_monoid_add_class.diff_cancel)
also have "... ≤ (∑j = 0..<k. ¦(if Q i j then int (xs ! j) - int (ys ! j) else 0)¦)"
by(rule sum_abs)
also have "... ≤ (∑j = 0..<k. (if Q i j then ¦ int (xs ! j) - int (ys ! j)¦ else 0))"
by(auto simp: if_distrib)
also have "... ≤ (∑j = 0..<k. ¦ int (xs ! j) - int (ys ! j)¦)"
by (auto simp: sum_mono)
also have "... ≤ (∑j = 0..<n. ¦ int (xs ! j) - int (ys ! j)¦)"
by(rule sum_mono2, auto simp:len)
also have "... = (∑j = 1..n. ¦ int (xs ! (j - 1)) - int (ys ! (j - 1))¦)"
proof(subst sum.reindex_cong[where l = "λ i. i - 1" and B = "{1..n}" and h = "λ x. ¦int (xs ! (x - 1)) - int (ys ! (x - 1))¦"])
show "inj_on (λi. i - 1) {1..n}"
unfolding inj_on_def by auto
show "{0..<n} = (λi. i - 1) ` {1..n}"
unfolding image_def by force
qed(auto)
also have "... ≤ 1"
using le of_int_le_1_iff unfolding dist_L1_norm_list_def by fastforce
finally show "¦int (∑j = 0..<k. if Q i j then xs ! j else 0) - int (∑j = 0..<k. if Q i j then ys ! j else 0)¦ ≤ 1".
qed
qed
qed
paragraph‹A component of a tuple of counting queries›
definition counting::"nat ⇒ nat list ⇒ nat" where
"counting i xs = counting' i (length xs) xs"
lemma measurable_counting[measurable]:
shows "(counting i ) ∈ (listM (count_space (UNIV::nat set))) →⇩M (count_space (UNIV::nat set))"
unfolding counting_def by auto
lemma counting_sum:
shows "counting i xs = (∑j∈{0..<length xs}. (if Q i j then (xs ! j) else 0))"
unfolding counting_def by(rule counting'_sum,auto)
lemma sensitvity_counting:
assumes "(xs,ys) ∈ adj_L1_norm"
shows "¦int (counting k xs) - int (counting k ys)¦ ≤ 1"
proof-
from assms have xsl: "length xs = n" and ysl: "length ys = n" and le: " dist_L1_norm_list xs ys ≤ 1"
by (auto simp:space_L1_norm_list_def adj_L1_norm_def sp_Dataset_def space_restrict_space dist_L1_norm_list_def space_listM)
thus ?thesis unfolding counting_def using sensitvity_counting' assms
by auto
qed
paragraph‹A list(tuple) of counting queries›
definition counting_query::"nat list ⇒ nat list" where
"counting_query xs = map (λ k. counting k xs) [0..<m]"
lemma measurable_counting_query[measurable]:
shows "counting_query ∈ listM (count_space UNIV) →⇩M listM (count_space UNIV)"
unfolding counting_query_def
proof(induction m)
case 0
then show ?case by auto
next
case (Suc m)
have " (λxs. map (λk. counting k xs) [0..<Suc m]) = (λxs. (λxs. map (λk. counting k xs) [0..<m]) xs @ [counting m xs])"
by auto
also have "... ∈ listM (count_space UNIV) →⇩M listM (count_space UNIV)"
using Suc by auto
finally show ?case .
qed
lemma length_counting_query:
shows "length(counting_query xs) = m"
unfolding counting_query_def by auto
lemma counting_query_nth:
fixes k::nat assumes "k < m"
shows "counting_query xs ! k = counting k xs"
unfolding counting_query_def by(subst nth_map_upt[of k m 0 "(λ k. counting k xs)"],auto simp: assms)
corollary counting_query_nth':
fixes k::nat assumes "k < m"
shows "map real (counting_query xs) ! k = real (counting k xs)"
unfolding counting_query_def List.map.compositionality comp_def
by(subst nth_map_upt[of k m 0 "(λ k. real (counting k xs))"],auto simp: assms)
end
paragraph ‹A formalization of the report noisy max of noisy counting›
context
Lap_Mechanism_RNM_counting
begin
interpretation L1_norm_list "(UNIV::nat set)" "(λ x y. ¦int x - int y¦)" n
by(unfold_locales,auto)
interpretation results_AFDP n
by(unfold_locales)
definition RNM_counting :: "real ⇒ nat list ⇒ nat measure" where
"RNM_counting ε x = do {
y ← Lap_dist_list (1 / ε) (counting_query x);
return (count_space UNIV) (argmax_list y)
}"
paragraph ‹ Naive evaluation of differential privacy of @{term RNM_counting} ›
text ‹ The naive proof is as follows:
We first show that the counting query has the sensitivity @{term m}.
@{term RNM_counting} adds the Laplace noise with scale @{term "1 / ε"} to each element given by @{term counting_query}.
Thanks to the postprocessing inequality, the final process @{term argmax_list} does not change the differential privacy.
Therefore the differential privacy of @{term RNM_counting} is @{term "m * ε"} ›
interpretation Lap_Mechanism_list "listM (count_space UNIV)" "counting_query" "adj_L1_norm" m
unfolding counting_query_def
by(unfold_locales,induction m, auto simp: space_listM)
lemma sensitvity_counting_query_part:
fixes k::nat assumes "k < m"
and "(xs,ys) ∈ adj_L1_norm"
shows "¦map real (counting_query xs) ! k - map real (counting_query ys) ! k ¦ ≤ 1"
unfolding counting_query_nth'[OF assms(1)] using sensitvity_counting[OF assms(2)]
by (metis (mono_tags, opaque_lifting) of_int_abs of_int_diff of_int_le_1_iff of_int_of_nat_eq)
lemma sensitvity_counting_query:
shows "sensitivity ≤ m"
proof(unfold sensitivity_def, rule Sup_least, elim CollectE exE)
fix r::ereal and xs ys ::"nat list" assume r: "r = ereal (∑i = 1..m. ¦map real (counting_query xs) ! (i - 1) - map real (counting_query ys) ! (i - 1)¦) ∧
xs ∈ space (listM (count_space UNIV)) ∧ ys ∈ space (listM (count_space UNIV)) ∧ (xs, ys) ∈ adj_L1_norm"
hence "r = ereal (∑i = 1..m. ¦map real (counting_query xs) ! (i - 1) - map real (counting_query ys) ! (i - 1)¦)"
by auto
also have "... = ereal (∑i = 0..<m. ¦map real (counting_query xs) ! i- map real (counting_query ys) ! i¦)"
by(subst sum.reindex_cong[where B = "{0..<m}" and l = Suc and h = "λi. ¦map real (counting_query xs) ! i - map real (counting_query ys) ! i¦" ],auto)
also have "... ≤ ereal (∑i = 0..<m. (1::real) )"
by(subst ereal_less_eq(3),subst sum_mono, auto intro !: sensitvity_counting_query_part simp: r)
also have "... ≤ ereal m"
by auto
finally show "r ≤ ereal (real m)".
qed
corollary sensitvity_counting_query_finite:
shows "sensitivity < ∞"
using sensitvity_counting_query by auto
theorem Naive_differential_privacy_LapMech_RNM_AFDP:
assumes pose: "(ε::real) > 0"
shows "differential_privacy_AFDP (RNM_counting ε) (real (m * ε)) 0"
unfolding RNM_counting_def
proof(rule differential_privacy_postprocessing[where R' = "count_space UNIV" and R = "listM borel" ])
interpret Output: L1_norm_list "UNIV::real set" "λ m n. ¦m - n¦" m
by(unfold_locales,auto)
show "0 ≤ real (m * ε)"
using pose by auto
show "(λx. Lap_dist_list (1 / real ε) (map real (counting_query x))) ∈ (listM (count_space UNIV)) →⇩M prob_algebra (listM borel)"
by auto
show " (λy. return (count_space UNIV) (argmax_list y)) ∈ listM borel →⇩M prob_algebra (count_space UNIV)"
by auto
show adj: " adj_L1_norm ⊆ space (listM (count_space UNIV)) × space (listM (count_space UNIV))"
unfolding space_listM space_count_space by auto
have "differential_privacy ( (Lap_dist_list (1 / real ε)) o (λx. (map real (counting_query x))))
adj_L1_norm (m * ε) 0"
proof(intro differential_privacy_preprocessing)
show "0 ≤ real (m * ε)"
by fact
show " (λx. map real (counting_query x)) ∈ listM (count_space UNIV) →⇩M listM borel"
by auto
show "∀(x, y)∈adj_L1_norm. (map real (counting_query x), map real (counting_query y))
∈ {(xs, ys) |xs ys. length xs = m ∧ length ys = m ∧ Output.dist_L1_norm_list xs ys ≤ real m}"
unfolding adj_L1_norm_def Output.dist_L1_norm_list_def Int_def prod.case case_prod_beta
proof(intro ballI, elim CollectE conjE exE )
fix p xs ys assume p:"p = (xs, ys)" and "xs ∈ space sp_Dataset" and "ys ∈ space sp_Dataset" and adj:"dist_L1_norm_list xs ys ≤ 1"
hence "length xs = n" and "length ys = n" and c: "(xs, ys) ∈ adj_L1_norm"
by (auto simp:space_L1_norm_list_def adj_L1_norm_def sp_Dataset_def space_restrict_space dist_L1_norm_list_def space_listM)
have "ereal (∑i = 1..m. ¦map real (counting_query xs) ! (i - 1) - map real (counting_query ys) ! (i - 1)¦) ≤ ⨆ {ereal (∑i = 1..m. ¦map real (counting_query x) ! (i - 1) - map real (counting_query y) ! (i - 1)¦) |x y. x ∈ UNIV ∧ y ∈ UNIV ∧ (x, y) ∈ adj_L1_norm}"
by(auto intro!: Sup_upper c)
also have "... ≤ ereal(real m)"
using sensitvity_counting_query unfolding sensitivity_def space_listM space_count_space by auto
finally show "(map real (counting_query (fst p)), map real (counting_query (snd p)))
∈ {(xs, ys) |xs ys. length xs = m ∧ length ys = m ∧ (∑i = 1..m. ¦xs ! (i - 1) - ys ! (i - 1)¦) ≤ real m}"
unfolding p using length_counting_query by auto
qed
show "differential_privacy (Lap_dist_list (1 / real ε)) {(xs, ys) |xs ys. length xs = m ∧ length ys = m ∧ Output.dist_L1_norm_list xs ys ≤ real m} (real (m * ε)) 0"
proof(subst differential_privacy_adj_sym)
show "sym {(xs, ys) |xs ys. length xs = m ∧ length ys = m ∧ Output.dist_L1_norm_list xs ys ≤ real m}"
by(rule symI,auto simp:Output.MetL1.commute)
show "∀(d1, d2)∈ {(xs, ys) |xs ys. length xs = m ∧ length ys = m ∧ Output.dist_L1_norm_list xs ys ≤ real m}.
DP_inequality (Lap_dist_list (1 / real ε) d1) (Lap_dist_list (1 / real ε) d2) (real (m * ε)) 0"
unfolding Int_def prod.case case_prod_beta
proof(intro ballI, elim CollectE exE conjE)
fix p xs ys assume p: "p = (xs, ys)" and xs: "length xs = m " and ys: "length ys = m " and adj: "Output.dist_L1_norm_list xs ys ≤ real m"
have 0: "(real m / (1 / real ε)) = (real (m * ε))"
by auto
from xs ys adj p DP_Lap_dist_list[of "(1 / real ε)" xs m ys "real m",simplified 0]
show " DP_inequality (Lap_dist_list (1 / real ε) (fst p)) (Lap_dist_list (1 / real ε) (snd p)) (real (m * ε)) 0"
unfolding DP_inequality_cong_DP_divergence Output.dist_L1_norm_list_def p fst_def snd_def
by (metis assms(1) case_prod_conv ereal_eq_0(2) of_nat_0_le_iff zero_less_divide_1_iff)
qed
qed
qed(auto simp: space_listM)
thus "differential_privacy (λx. Lap_dist_list (1 / real ε) (map real (counting_query x))) adj_L1_norm (real (m * ε)) 0"
unfolding comp_def by auto
qed
paragraph ‹ True evaluation of differential privacy of @{term RNM_counting} ›
text ‹ in contrast to the naive proof, @{term counting_query} and @{term argmax_list} are essential. ›
lemma finer_sensitivity_counting_query:
assumes "(xs,ys) ∈ adj_L1_norm"
shows "list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) (counting_query xs) (counting_query ys) ∨ list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) (counting_query ys) (counting_query xs)"
proof-
note adjacency_1_int_list[OF assms]
then consider "xs = ys" | "(∃as a b bs. xs = as @ a # bs ∧ ys = as @ b # bs ∧ ¦int a - int b¦ = 1) ∧ xs ≠ ys"
by auto
then show ?thesis
proof(cases)
case 1
define zs where zs: " zs = (counting_query ys)"
have *: " list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) zs zs"
by(induction zs,auto)
thus ?thesis
unfolding 1 zs by auto
next
case 2
then obtain as a b bs
where xs:"xs = as @ a # bs"
and ys: "ys = as @ b # bs"
and d:"a < b ∨ b < a"
and diff:" ¦int a - int b¦ = 1"
using linorder_less_linear by blast
define m1::nat where m1: "m1 = length as"
{
fix k assume k: "k∈{0..<m}"
have 1: "({0..<m1}∪{Suc m1..<length xs})∪{m1} = {0..<length xs}"
unfolding m1 xs by auto
have a: "xs ! m1 = a" and b: " ys ! m1 = b"
unfolding m1 xs ys by auto
have ***: "⋀j. j ∈ ({0..<m1}∪{Suc m1..<length xs}) ⟹ xs ! j = ys ! j"
proof-
fix j assume "j ∈ ({0..<m1}∪{Suc m1..<length xs})"
hence 2: " j ∈ {0..<length xs}" and 3: " j ≠ m1"
using 1 by auto
have "⋀j. j ∈ {0..<length xs} ∧ j ≠ m1 ⟹ xs ! j = ys ! j"
using m1 unfolding xs ys by (simp add: nth_Cons' nth_append)
thus " xs ! j = ys ! j" using 2 3 by auto
qed
have " (∑j = 0..<length xs. if Q k j then xs ! j else 0) = (∑j∈({0..<m1}∪{Suc m1..<length xs})∪{m1}. if Q k j then xs ! j else 0)"
using 1 by auto
also have "... = (∑j∈{0..<m1}∪{Suc m1..<length xs}. if Q k j then xs ! j else 0) + (if Q k m1 then a else 0)"
by(subst sum_Un_nat,auto simp: a)
finally have A: "(∑j = 0..<length xs. if Q k j then xs ! j else 0) = (∑j∈{0..<m1}∪{Suc m1..<length xs}. if Q k j then xs ! j else 0) + (if Q k m1 then a else 0)" .
have " (∑j = 0..<length ys. if Q k j then ys ! j else 0) = (∑j∈({0..<m1}∪{Suc m1..<length xs})∪{m1}. if Q k j then ys ! j else 0)"
using 1 assms by (auto simp:space_L1_norm_list_def adj_L1_norm_def sp_Dataset_def space_restrict_space dist_L1_norm_list_def space_listM)
also have "... = (∑j∈{0..<m1}∪{Suc m1..<length xs}. if Q k j then ys ! j else 0) + (if Q k m1 then b else 0)"
by(subst sum_Un_nat,auto simp: b)
also have "... = (∑j∈{0..<m1}∪{Suc m1..<length xs}. if Q k j then xs ! j else 0) + (if Q k m1 then b else 0)"
using *** by(subst sum.cong[where B = "{0..<m1} ∪ {Suc m1..<length xs}" and h = "λ x. (if Q k x then xs ! x else 0) " ],auto)
finally have B: "(∑j = 0..<length ys. if Q k j then ys ! j else 0) = (∑j∈{0..<m1} ∪ {Suc m1..<length xs}. if Q k j then xs ! j else 0) + (if Q k m1 then b else 0)" .
note A B
}note *** = this
from d diff consider
"b = a + 1" | "a = b + 1"
by auto
thus ?thesis proof(cases)
case 1
have " list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) (counting_query ys) (counting_query xs)"
proof(subst list_all2_conv_all_nth,rule conjI)
show "length (counting_query ys) = length (counting_query xs)"
using length_counting_query by auto
show "∀i<length (counting_query ys). counting_query xs ! i ≤ counting_query ys ! i ∧ counting_query ys ! i ≤ counting_query xs ! i + 1"
proof(intro allI impI)
fix i assume "i < length (counting_query ys)"
hence i: "i < length [0..<m]" and i2: "i ∈ {0..<m}" and i3: "[0..<m] ! i = i"
unfolding length_counting_query by auto
thus "counting_query xs ! i ≤ counting_query ys ! i ∧ counting_query ys ! i ≤ counting_query xs ! i + 1"
unfolding counting_query_def counting_sum list_all2_conv_all_nth length_map length_upt
nth_map[of i "[0..<m]" "λk. ∑j = 0..<length xs. if Q k j then xs ! j else 0",OF i]
nth_map[of i "[0..<m]" "λk. ∑j = 0..<length ys. if Q k j then ys ! j else 0",OF i]
1 i3 ***(1)[OF i2] ***(2)[OF i2]
by auto
qed
qed
then show ?thesis by auto
next
case 2
have " list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) (counting_query xs) (counting_query ys)"
proof(subst list_all2_conv_all_nth,rule conjI)
show "length (counting_query xs) = length (counting_query ys)"
using length_counting_query by auto
show "∀i<length (counting_query xs). counting_query ys ! i ≤ counting_query xs ! i ∧ counting_query xs ! i ≤ counting_query ys ! i + 1"
proof(intro allI impI)
fix i assume "i < length (counting_query xs)"
hence i: "i < length [0..<m]" and i2: "i ∈ {0..<m}" and i3: "[0..<m] ! i = i"
unfolding length_counting_query by auto
thus "counting_query ys ! i ≤ counting_query xs ! i ∧ counting_query xs ! i ≤ counting_query ys ! i + 1"
unfolding counting_query_def counting_sum list_all2_conv_all_nth length_map length_upt
nth_map[of i "[0..<m]" "λk. ∑j = 0..<length xs. if Q k j then xs ! j else 0",OF i]
nth_map[of i "[0..<m]" "λk. ∑j = 0..<length ys. if Q k j then ys ! j else 0",OF i]
2 i3 ***(1)[OF i2] ***(2)[OF i2]
by auto
qed
qed
then show ?thesis by auto
qed
qed
qed
lemma list_all2_map_real_adj:
assumes "list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) xs ys"
shows "list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) (map real xs) (map real ys)"
using assms nth_map[of _ xs real] nth_map[of _ ys real] unfolding list_all2_conv_all_nth length_map
by force
lemma finer_sensitivity_counting_query':
assumes "(xs,ys) ∈ adj_L1_norm"
shows "list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) (map real (counting_query xs))(map real (counting_query ys)) ∨ list_all2 (λ x y. x ≥ y ∧ x ≤ y + 1) (map real (counting_query ys))(map real (counting_query xs))"
using finer_sensitivity_counting_query[OF assms] list_all2_map_real_adj by auto
interpretation Lap_Mechanism_RNM_mainpart "(listM (count_space UNIV))" adj_L1_norm "counting_query"
proof(unfold_locales)
show "(λx. map real (counting_query x)) ∈ (listM (count_space UNIV)) →⇩M listM borel"
by auto
show " ∀(x, y)∈ adj_L1_norm.
list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) (map real (counting_query x)) (map real (counting_query y)) ∨
list_all2 (λx y. y ≤ x ∧ x ≤ y + 1) (map real (counting_query y)) (map real (counting_query x))"
using finer_sensitivity_counting_query' by auto
show " adj_L1_norm ⊆ space (listM (count_space UNIV)) × space (listM (count_space UNIV))"
unfolding space_listM space_count_space by auto
qed
theorem differential_privacy_LapMech_RNM_AFDP:
assumes pose: "(ε::real) > 0"
shows "differential_privacy_AFDP (RNM_counting ε) ε 0"
using differential_privacy_LapMech_RNM[OF assms]
unfolding RNM_counting_def LapMech_RNM_def by auto
end
end