Theory Differential_Privacy.Differential_Privacy_Divergence
theory Differential_Privacy_Divergence
imports "Comparable_Probability_Measures"
begin
section ‹Divergence for Differential Privacy›
text‹ First, we introduce the divergence for differential privacy. ›
definition DP_divergence :: "'a measure ⇒ 'a measure ⇒ real ⇒ ereal " where
"DP_divergence M N ε = Sup {ereal(measure M A - (exp ε) * measure N A) | A::'a set. A ∈ (sets M)}"
lemma DP_divergence_SUP:
shows "DP_divergence M N ε = (⨆ (A::'a set) ∈ (sets M). ereal(measure M A - (exp ε) * measure N A))"
by (auto simp: setcompr_eq_image DP_divergence_def)
subsection ‹Basic Properties›
subsubsection ‹Non-negativity›
lemma DP_divergence_nonnegativity:
shows "0 ≤ DP_divergence M N ε"
proof(unfold DP_divergence_SUP, rule Sup_upper2[of 0])
have "{} ∈ sets M" "(λA :: 'a set. ereal (measure M A - exp ε * measure N A)) {} = 0"
by auto
thus "0 ∈ (λA. ereal (measure M A - exp ε * measure N A)) ` sets M"
by force
qed(auto)
subsubsection ‹Graded predicate›
lemma DP_divergence_forall:
shows "(∀ A ∈ (sets M). (measure M A - (exp ε) * measure N A ≤ (δ :: real)))
⟷ DP_divergence M N ε ≤ (δ :: real)"
unfolding DP_divergence_SUP by (auto simp: SUP_le_iff)
lemma DP_divergence_leE:
assumes "DP_divergence M N ε ≤ (δ :: real)"
shows "measure M A ≤ (exp ε) * measure N A + (δ :: real)"
proof(cases "A ∈ (sets M)")
case True
then show ?thesis using DP_divergence_forall assms(1) by force
next
case False
then have "measure M A = 0 " "0 ≤ measure N A " "0 ≤ (exp ε)"
using measure_notin_sets by auto
moreover have "0 ≤ ereal δ"
using assms DP_divergence_nonnegativity[of M N ε] dual_order.trans by blast
ultimately show ?thesis by auto
qed
lemma DP_divergence_leI:
assumes "⋀ A. A ∈ (sets M) ⟹ measure M A ≤ (exp ε) * measure N A + (δ :: real)"
shows "DP_divergence M N ε ≤ (δ :: real)"
using assms unfolding DP_divergence_def by(intro cSup_least, fastforce+)
subsubsection ‹ ‹(0,0)›-DP means the equality of distributions ›
lemma prob_measure_eqI_le:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
and le:"∀ A ∈ sets M. emeasure M A ≤ emeasure N A"
shows "M = N"
proof(rule measure_eqI)
interpret pM: prob_space M
using actual_prob_space M by auto
interpret pN: prob_space N
using actual_prob_space N by auto
show *: "sets M = sets N"
using M N space_prob_algebra_sets by blast
show " ⋀A. A ∈ sets M ⟹ emeasure M A = emeasure N A"
proof (rule ccontr)
fix A assume A: "A ∈ sets M" and neq:"emeasure M A ≠ emeasure N A"
then have A2: "A ∈ sets N" and A3: "A ∈ sets L"
using M N space_prob_algebra_sets by blast+
from neq consider
"emeasure M A < emeasure N A" | "emeasure M A > emeasure N A"
by fastforce
then show False
proof(cases)
case 1
have Ms: "emeasure M (space M - A) = emeasure M (space M) - emeasure M A"
using A sets.sets_into_space by(subst emeasure_Diff,auto)
have Ns: "emeasure N (space M - A) = emeasure N (space N) - emeasure N A"
using A2 sets.sets_into_space sets_eq_imp_space_eq[OF *] by(subst emeasure_Diff,auto)
have "emeasure M (space M - A) > emeasure N (space M - A)"
unfolding Ms Ns pM.emeasure_space_1 pN.emeasure_space_1
by (meson "1" ennreal_mono_minus_cancel ennreal_one_less_top leI less_le_not_le pM.measure_le_1 pN.measure_le_1)
moreover have "emeasure M (space M - A)≤ emeasure N (space M - A)"
using le A by auto
ultimately show ?thesis
by auto
next
case 2
from le A have "emeasure M A ≤ emeasure N A"
by auto
with 2 show ?thesis
by auto
qed
qed
qed
lemma DP_divergence_zero:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
and DP0:"DP_divergence M N (0::real) ≤ (0::real)"
shows "M = N"
proof(intro prob_measure_eqI_le[of M L N] M N ballI)
interpret comparable_probability_measures L M N
by(unfold_locales,auto simp: M N)
interpret pM: prob_space M
by auto
interpret pN: prob_space N
by auto
fix A assume " A ∈ sets M"
hence "measure M A - measure N A ≤ 0"
using DP0[simplified zero_ereal_def] unfolding DP_divergence_forall[symmetric] by auto
hence "measure M A ≤ measure N A"
by auto
thus "emeasure M A ≤ emeasure N A"
by (simp add: pM.emeasure_eq_measure pN.emeasure_eq_measure)
qed
subsubsection ‹Conversion from pointwise DP \cite{Prasad803anote} ›
lemma DP_divergence_pointwise:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
and C: "C ∈ sets M"
and "∀A∈sets M. A ⊆ C ⟶ measure M A ≤ exp ε * measure N A"
and "1 - δ ≤ measure M C"
shows "DP_divergence M N (ε::real) ≤ δ"
proof(rule DP_divergence_leI)
interpret comparable_probability_measures L M N
by(unfold_locales, auto simp: assms)
fix A assume A:"A ∈ sets M"
define A1 and A2 where "A1 = A ∩ C" and "A2 = A - C"
hence A1s[measurable]:"A1 ∈ sets M" and A2s[measurable]:"A2 ∈ sets M" and A1C:"A1 ⊆ C" and A12: "A1 ∪ A2 = A"
unfolding A1_def A2_def using C A by auto
hence "measure M A1 ≤ (exp ε) * measure N A1"
using assms(4) by blast
also have "... ≤ (exp ε) * measure N A"
using A1s A2s unfolding A12[symmetric]
by(subst measure_Union[of N A1 A2]) (auto simp add: finite_measure.emeasure_finite A1_def A2_def)
finally have 1: "measure M A1 ≤ exp ε * measure N A".
have A2Cc:"A2 ⊆ space M - C"
by (metis A A2_def Diff_mono sets.sets_into_space subset_refl)
have "measure M A2 ≤ measure M (space M - C)"
by(intro finite_measure.finite_measure_mono A2Cc Sigma_Algebra.sets.compl_sets C,auto)
also have "... = measure M (space M) - measure M C"
using assms(3) finM finite_measure.finite_measure_compl by blast
also have "...≤ 1 - (1 - δ)"
using M actual_prob_space prob_space.axioms assms(5) prob_space.prob_space by force
also have "... = δ"
by auto
finally have 2: "measure M A2 ≤ δ".
have "measure M A = measure M A1 + measure M A2"
using A1s A2s unfolding A12[symmetric]
by(subst measure_Union[of M A1 A2]) (auto simp add: finite_measure.emeasure_finite A1_def A2_def)
also have "... ≤ exp ε * measure N A + δ"
using 1 2 by auto
finally show "measure M A ≤ exp ε * measure N A + δ" .
qed
subsubsection ‹(Reverse-) Monotonicity for ‹ε› ›
lemma DP_divergence_monotonicity:
assumes "ε1 ≤ ε2"
shows "DP_divergence M N ε2 ≤ DP_divergence M N ε1"
proof(unfold DP_divergence_SUP, rule SUP_mono)
fix A assume *: "A ∈ sets M"
have "ereal (measure M A - exp ε2 * measure N A) ≤ ereal (measure M A - exp ε1 * measure N A)"
by (auto simp: assms mult_mono')
with * show "∃m∈sets M. ereal (measure M A - exp ε2 * measure N A) ≤ ereal (measure M m - exp ε1 * measure N m)"
by blast
qed
corollary DP_divergence_monotonicity':
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
and "ε1 ≤ ε2" and "δ1 ≤ δ2"
shows "DP_divergence M N ε1 ≤ δ1 ⟹ DP_divergence M N ε2 ≤ δ2"
by (meson DP_divergence_monotonicity M N assms gfp.leq_trans)
subsubsection ‹ Reflexivity ›
lemma DP_divergence_reflexivity:
shows "DP_divergence M M 0 = 0"
proof(unfold DP_divergence_SUP)
have "∀ A ∈sets M. ereal (measure M A - exp 0 * measure M A) = (0 :: ereal)"
by auto
thus "(⨆A ∈sets M. ereal (measure M A - exp 0 * measure M A)) = (0 :: ereal)"
by (metis (no_types, lifting) SUP_ereal_eq_0_iff_nonneg empty_iff order_refl sets.top)
qed
corollary DP_divergence_reflexivity':
assumes "0 ≤ ε "
shows "DP_divergence M M ε = 0"
proof-
have "DP_divergence M M ε ≤ DP_divergence M M 0"
by(rule DP_divergence_monotonicity, auto simp: assms)
also have "... = 0"
by(auto simp: DP_divergence_reflexivity)
finally have 1: "DP_divergence M M ε ≤ 0".
have 2: "0 ≤ DP_divergence M M ε"
by(auto simp: DP_divergence_nonnegativity[of M M ε])
from 1 2 show ?thesis by auto
qed
subsubsection ‹ Transitivity ›
lemma DP_divergence_transitivity:
assumes DP1: "DP_divergence M1 M2 ε1 ≤ 0"
and DP2: "DP_divergence M2 M3 ε2 ≤ 0"
shows "DP_divergence M1 M3 (ε1+ε2) ≤ 0"
unfolding zero_ereal_def
proof(subst DP_divergence_forall[symmetric],intro ballI)
fix A assume AM1: " A ∈ sets M1"
have "measure M1 A ≤ exp ε1 * measure M2 A"
using DP_divergence_leE[OF DP1[simplified zero_ereal_def]] by auto
also have " ... ≤ exp ε1 * exp ε2 * measure M3 A"
using DP_divergence_leE[OF DP2[simplified zero_ereal_def]] by auto
finally have "measure M1 A ≤ exp (ε1 + ε2) * measure M3 A"
unfolding exp_add[of ε1 ε2, symmetric] by auto
thus "measure M1 A - exp (ε1 + ε2) * measure M3 A ≤ 0" by auto
qed
subsubsection ‹ Composability ›
proposition DP_divergence_composability:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
and f: "f ∈ L →⇩M prob_algebra K"
and g: "g ∈ L →⇩M prob_algebra K"
and div1: "DP_divergence M N ε1 ≤ (δ1 :: real)"
and div2: "∀x ∈ (space L). DP_divergence (f x) (g x) ε2 ≤ (δ2 :: real)"
and "0 ≤ ε1" and "0 ≤ ε2"
shows "DP_divergence (M ⤜ f) (N ⤜ g) (ε1 + ε2) ≤ δ1 + δ2"
proof(subst DP_divergence_forall[THEN sym])
note [measurable] = f g
interpret comparable_probability_measures L M N
by(unfold_locales, auto simp: assms)
show "∀A∈sets (M ⤜ f). measure (M ⤜ f) A - exp (ε1 + ε2) * measure (N ⤜ g) A ≤ δ1 + δ2"
proof
fix "A" assume "A ∈ sets (M ⤜ f)"
hence AinSetsK: "A ∈ sets K"
using M f sets_bind' by blast
have f2[measurable]: "f ∈ sum_measure M N →⇩M prob_algebra K"
using setMN_L by measurable
have g2[measurable]: "g ∈ sum_measure M N →⇩M prob_algebra K"
using setMN_L by measurable
have ess_boundedf[simp]: "ess_bounded (sum_measure M N) (λx. measure (f x) A)"
by (intro probability_kernel_evaluation_ess_bounded[where M = K] AinSetsK f2)
have ess_boundedg[simp]: "ess_bounded (sum_measure M N) (λx. measure (g x) A)"
by (intro probability_kernel_evaluation_ess_bounded[where M = K] AinSetsK g2)
have integrablef[simp]: "integrable (sum_measure M N) (λx. measure (f x) A)"
by (auto simp:AinSetsK)
have integrableg[simp]: "integrable (sum_measure M N) (λx. measure (g x) A)"
by (auto simp: AinSetsK)
have meas1[measurable_cong]: "measurable L (prob_algebra K) = measurable (sum_measure M N) (prob_algebra K)"
by(rule measurable_cong_sets, simp_all)
have f2[measurable]: "f ∈ sum_measure M N →⇩M prob_algebra K"
by auto
have g2[measurable]: "g ∈ sum_measure M N →⇩M prob_algebra K"
by auto
have "∀x∈ space (sum_measure M N). measure (f x) A - (exp ε2) * measure (g x) A ≤ δ2"
proof
fix x assume A: "x ∈ space (sum_measure M N)"
hence A2: "A ∈ sets (f x)"
by (metis AinSetsK f2 measurable_prob_algebraD subprob_measurableD(2))
from A have xxx: "DP_divergence (f x) (g x) ε2 ≤ δ2"
using div2 spaceMN_L by auto
show "measure (f x) A - exp ε2* measure (g x) A ≤ δ2"
using xxx[simplified DP_divergence_forall[THEN sym,rule_format]] A2 by blast
qed
hence ineq7: "∀x∈ space (sum_measure M N). measure (f x) A - δ2 ≤ exp ε2 * measure (g x) A "
by auto
have "∀x∈ space (sum_measure M N). measure (f x) A- δ2 ≤ min 1 (exp ε2 * measure (g x) A) "
proof
fix x assume Ass0: "x ∈ space (sum_measure M N)"
hence "0 ≤ DP_divergence (f x) (g x) ε2"
using DP_divergence_nonnegativity by auto
also have "DP_divergence (f x) (g x) ε2 ≤ δ2"
using div2 Ass0 spaceMN_L by auto
finally have posdelta2: "0 ≤ δ2"by auto
hence minA: "measure (f x) A - δ2 ≤ 1"
using evaluations_probabilistic_process(3)[OF f AinSetsK] assms Ass0 spaceMN_L by auto
have minB: "measure (f x) A - δ2 ≤ exp ε2 * measure (g x) A"
using Ass0 ineq7 by auto
from minA minB show "measure (f x) A - δ2 ≤ min 1 (exp ε2 * measure (g x) A)"
by auto
qed
hence inequalityB: "∀x∈ space (sum_measure M N). max 0 (measure (f x) A - δ2) ≤ min 1 (exp ε2 * measure (g x) A)"
by auto
have inequalityC: "∀x∈ space (sum_measure M N). dM x * max 0 (measure (f x) A - δ2) ≤ dM x * min 1 (exp ε2 * measure (g x) A)"
proof
fix x assume A0: "x∈ space (sum_measure M N)"
with inequalityB have P1: "(max 0 (measure (f x) A - δ2)) ≤ min 1 ((exp ε2) * measure (g x) A) "
by auto
thus "dM x * max 0 (measure (f x) A - δ2) ≤ dM x * min 1 (exp ε2 * measure (g x) A)"
by(intro mult_left_mono, auto)
qed
have "(measure (M ⤜ f) A) - exp (ε1 + ε2) * (measure (N ⤜ g) A) = (∫ x. (dM x) * (measure (f x) A) ∂(sum_measure M N)) - (exp (ε1 + ε2)) * (∫ x. (dN x) * (measure (g x) A) ∂(sum_measure M N))"
using AinSetsK dM_bind_integral[OF f2] dN_bind_integral[OF g2] by auto
also have "... = (∫ x. (dM x) * (measure (f x) A) ∂(sum_measure M N)) - (∫ x. (exp (ε1 + ε2)) * (dN x) * (measure (g x) A) ∂(sum_measure M N)) "
by (metis (mono_tags, lifting) Bochner_Integration.integral_cong integral_mult_right_zero mult.assoc)
also have "... = (∫ x. (dM x) * (measure (f x) A) - (exp (ε1 + ε2)) * (dN x) * (measure (g x) A) ∂(sum_measure M N)) "
by(rule Bochner_Integration.integral_diff[THEN sym],auto)
also have "... = (∫ x. (dM x) * (measure (f x) A) - (exp ε1) * (exp ε2) * (dN x) * (measure (g x) A) ∂(sum_measure M N)) "
by (auto simp: exp_add)
also have "... ≤ (∫ x. (dM x) * (max 0 (measure (f x) A - δ2) + δ2) - (exp ε1) * (dN x) * min 1 ((exp ε2) * (measure (g x) A)) ∂(sum_measure M N)) "
proof(rule integral_mono)
fix x assume A0: "x ∈ space (sum_measure M N)"
have "dM x * measure (f x) A - exp ε1 * exp ε2 * dN x * measure (g x) A = dM x * ((measure (f x) A - δ2) + δ2)- exp ε1 * dN x *(exp ε2 * measure (g x) A)"
by auto
also have "... ≤ dM x * ((max 0 (measure (f x) A - δ2)) + δ2)- exp ε1 * dN x *(exp ε2 * measure (g x) A)"
by(auto simp: mult_left_mono)
also have "... ≤ dM x * ((max 0 (measure (f x) A - δ2)) + δ2)- exp ε1 * dN x * (min 1 (exp ε2 * measure (g x) A))"
by(auto simp: mult_left_mono)
finally show "dM x * measure (f x) A - exp ε1 * exp ε2 * dN x * measure (g x) A ≤ dM x * (max 0 (measure (f x) A - δ2) + δ2) - exp ε1 * dN x * min 1 (exp ε2 * measure (g x) A)".
qed(auto)
also have "... = (∫ x. (dM x) * (max 0 (measure (f x) A - δ2)) - (exp ε1) * (dN x) * min 1 ((exp ε2)* (measure (g x) A)) + (dM x) *δ2 ∂(sum_measure M N)) "
by (auto simp: diff_add_eq ring_class.ring_distribs(1))
also have "... ≤ (∫ x. (dM x) * (min 1 ((exp ε2)* (measure (g x) A))) - (exp ε1) * (dN x) * min 1 ((exp ε2)* (measure (g x) A)) + dM x *δ2 ∂(sum_measure M N)) "
proof(rule integral_mono)
show "integrable (sum_measure M N) (λx. dM x * (min 1 ((exp ε2) * measure (g x) A)) - exp ε1 * dN x * min 1 (exp ε2 * measure (g x) A) + dM x * δ2)" by auto
fix x assume "x ∈ space (sum_measure M N)"
with inequalityC have "dM x * max 0 (measure (f x) A - δ2) ≤ dM x * (min 1 ((exp ε2) * measure (g x) A))"
by blast
thus "dM x * max 0 (measure (f x) A - δ2) - exp ε1 * dN x * min 1 (exp ε2 * measure (g x) A) + dM x * δ2 ≤ dM x * min 1 (exp ε2 * measure (g x) A) - exp ε1 * dN x * min 1 (exp ε2 * measure (g x) A) + dM x * δ2"
by auto
qed(auto)
also have "... =(∫ x. ((dM x) - (exp ε1) * (dN x)) * min 1 ((exp ε2) * (measure (g x) A)) + dM x *δ2 ∂(sum_measure M N)) "
by (auto simp: vector_space_over_itself.scale_left_diff_distrib)
also have "... =(∫ x. ((dM x) - (exp ε1) * (dN x)) * min 1 ((exp ε2) * (measure (g x) A))∂(sum_measure M N)) +(∫ x. dM x *δ2 ∂(sum_measure M N)) "
by(rule Bochner_Integration.integral_add,auto)
finally have *: "(measure (M ⤜ f) A) - exp (ε1 + ε2) * (measure (N ⤜ g) A)≤(∫ x. ((dM x) - (exp ε1) * (dN x)) * min 1 ((exp ε2)* (measure (g x) A))∂(sum_measure M N)) +(∫ x. dM x *δ2 ∂(sum_measure M N))".
have "(∫ x. dM x *δ2 ∂(sum_measure M N))=(∫ x. δ2 ∂(density (sum_measure M N) dM))"
by(rule integral_real_density[THEN sym],auto)
also have "... =(∫ x. δ2 ∂(density (sum_measure M N)(ennreal o dM)))"
by (meson comp_def[THEN sym])
also have "... =(∫ x. δ2 ∂M)"
using dM_density by auto
also have "... = δ2 * measure M (space M)"
by auto
also have "... ≤ δ2"
using prob_space.prob_space prob_spaceM by fastforce
finally have **: "(∫ x. dM x *δ2 ∂(sum_measure M N)) ≤ δ2".
let ?B = "{x∈ space (sum_measure M N). 0 ≤ ((dM x) - (exp ε1) * (dN x))}"
have mble10: "?B ∈ sets (sum_measure M N)"
by measurable
have "(∫ x. ((dM x) - (exp ε1) * (dN x)) * min 1 ((exp ε2)* (measure (g x) A))∂(sum_measure M N)) ≤ (∫ x∈ ?B. (((dM x) - (exp ε1) * (dN x)) * min 1 ((exp ε2)* (measure (g x) A)))∂(sum_measure M N))"
proof(rule integral_drop_negative_part2)
show "(λx. (dM x - exp ε1 * dN x) * min 1 (exp ε2 * measure (g x) A)) ∈ borel_measurable (sum_measure M N)"
using integrablef integrableg by measurable
show "integrable (sum_measure M N) (λx. (dM x - exp ε1 * dN x) * min 1 (exp ε2 * measure (g x) A))"
by auto
show "{x ∈ space (sum_measure M N). 0 ≤ dM x - exp ε1 * dN x} ∈ sets (sum_measure M N)"
by measurable
show "{x ∈ space (sum_measure M N). 0 < (dM x - exp ε1 * dN x) * min 1 (exp ε2 * measure (g x) A)} ⊆ {x ∈ space (sum_measure M N). 0 ≤ dM x - exp ε1 * dN x}"
proof(rule subsetI, safe)
fix x assume "x ∈ space (sum_measure M N)" and "0 < (dM x - exp ε1 * dN x) * min 1 (exp ε2 * measure (g x) A)"
hence "0 < (dM x - exp ε1 * dN x) ∧ 0 < min 1 (exp ε2 * measure (g x) A)"
by (metis exp_gt_zero lambda_one min.absorb4 min.order_iff mult_pos_pos vector_space_over_itself.scale_zero_right alethe_comp_simplify1(3) zero_less_measure_iff zero_less_mult_pos2)
thus "0 ≤ dM x - exp ε1 * dN x"
by auto
qed
show "{x ∈ space (sum_measure M N). 0 ≤ dM x - exp ε1 * dN x} ⊆ {x ∈ space (sum_measure M N). 0 ≤ (dM x - exp ε1 * dN x) * min 1 (exp ε2 * measure (g x) A)}"
by auto
qed
also have "... ≤ (∫ x∈ ?B. ((dM x) - (exp ε1) * (dN x)) ∂(sum_measure M N))"
using mble10 by(intro set_integral_mono,unfold set_integrable_def,auto simp: mult_left_le)
also have "... = (∫ x∈ ?B. (dM x) ∂(sum_measure M N)) - (∫ x∈ ?B. ((exp ε1) * (dN x)) ∂(sum_measure M N))"
using mble10 by(intro set_integral_diff, auto simp:set_integrable_def)
also have "... = (∫ x∈ ?B. (dM x) ∂(sum_measure M N)) - (exp ε1) * (∫ x∈ ?B. (dN x) ∂(sum_measure M N))"
by auto
also have "... = measure M ?B - (exp ε1) * (measure N ?B)"
proof-
have "(∫ x∈ ?B. dM x ∂(sum_measure M N)) = (∫ x. (dM x * indicator ?B x) ∂ (sum_measure M N))"
by (auto simp: mult.commute set_lebesgue_integral_def)
also have "... = (∫ x. indicator ?B x ∂(density (sum_measure M N) dM))"
by(rule integral_real_density[THEN sym],measurable)
also have "... = (∫ x. indicator ?B x ∂(density (sum_measure M N) (ennreal o dM)))"
by (metis comp_apply)
also have "... = (∫ x. indicator ?B x *⇩R 1 ∂(density (sum_measure M N) (ennreal o dM)))"
by auto
also have "... = (∫ x∈ ?B. 1 ∂(density (sum_measure M N) (ennreal o dM)))"
by(auto simp:set_lebesgue_integral_def)
also have "... = 1 * measure (density (sum_measure M N) (ennreal o dM)) ?B"
proof(rule set_integral_indicator)
show "emeasure (density (sum_measure M N) (ennreal ∘ dM)) ?B < ⊤"
using finite_measure.emeasure_finite[of M ?B,OF finM] diff_gt_0_iff_gt_ennreal by force
qed(measurable)
also have "... = 1 * measure M ?B"
using dM_density by auto
finally have eq11: "(∫ x∈ ?B. dM x ∂(sum_measure M N)) = measure M ?B"
by auto
have "(∫ x∈ ?B. dN x ∂(sum_measure M N)) = (∫ x. (dN x * indicator ?B x) ∂ (sum_measure M N))"
by (auto simp: mult.commute set_lebesgue_integral_def)
also have "... = (∫ x. indicator ?B x ∂(density (sum_measure M N) dN))"
by(rule integral_real_density[THEN sym],measurable)
also have "... = (∫ x. indicator ?B x ∂(density (sum_measure M N) (ennreal o dN)))"
by (metis comp_apply)
also have "... = (∫ x∈ ?B. 1 ∂(density (sum_measure M N) (ennreal o dN)))"
by(auto simp:set_lebesgue_integral_def)
also have "... = 1 * measure (density (sum_measure M N) (ennreal o dN)) ?B"
proof(rule set_integral_indicator,measurable)
show "emeasure (density (sum_measure M N) (ennreal ∘ dN)) ?B < ⊤"
using finite_measure.emeasure_finite[of N ?B,OF finN] diff_gt_0_iff_gt_ennreal by force
qed
also have "... = 1 * measure N ?B"
using dN_density by auto
finally have eq21: "(∫ x∈ ?B. dN x ∂(sum_measure M N)) = measure N ?B"
by auto
show ?thesis
using eq11 eq21 by auto
qed
also have "... ≤ δ1"
using div1 DP_divergence_forall mble10 setMN_M by blast
finally have ***: "(∫ x. ((dM x) - (exp ε1) * (dN x)) * min 1 ((exp ε2)* (measure (g x) A))∂(sum_measure M N)) ≤ δ1".
show "measure (M ⤜ f) A - exp (ε1 + ε2) * measure (N ⤜ g) A ≤ δ1 + δ2"
using * ** *** by auto
qed
qed
subsubsection ‹ Post-processing inequality ›
corollary DP_divergence_postprocessing:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
and f: "f ∈ L →⇩M (prob_algebra K)"
and div1: "DP_divergence M N ε1 ≤ (δ1 :: real)"
and "0≤ ε1"
shows "DP_divergence (bind M f) (bind N f) ε1 ≤ δ1"
proof-
have div2: "∀x ∈ (space L). DP_divergence (f x) (f x) 0 ≤ ereal 0"
proof
fix x assume A0: "x ∈ space L"
have "DP_divergence (f x) (f x) 0 = 0"
by(rule DP_divergence_reflexivity)
thus "DP_divergence (f x) (f x) 0 ≤ ereal 0"
by auto
qed
have "DP_divergence (M ⤜ f) (N ⤜ f) (ε1 + 0) ≤ ereal (δ1 + 0) "
by(rule DP_divergence_composability[of M L N f K f ε1 δ1 0 0], auto simp: assms div2)
thus "DP_divergence (M ⤜ f) (N ⤜ f) ε1 ≤ ereal δ1"by auto
qed
subsubsection ‹ Law for the strength of the Giry monad ›
lemma DP_divergence_strength:
assumes "M ∈ space (prob_algebra L)"
and "N ∈ space (prob_algebra L)"
and "DP_divergence M N ε1 ≤ (δ1 :: real)"
and "0≤ ε1"
and x:"x ∈ space K"
shows "DP_divergence ((return K x) ⨂⇩M M) ((return K x) ⨂⇩M N) ε1 ≤ δ1"
proof-
interpret comparable_probability_measures L M N
by(unfold_locales, auto simp: assms)
define f where "f = (λ y. (return (K ⨂⇩M L) (x, y)))"
have f: "f ∈ L →⇩M (prob_algebra (K ⨂⇩M L))"
using assms f_def by force
have 1:"DP_divergence (bind M f) (bind N f) ε1 ≤ δ1"
using DP_divergence_postprocessing assms f by blast
moreover have 2:"(return K x) ⨂⇩M M = (M ⤜ f)"
by(subst Giry_strength_bind_return[OF M x])(metis f_def return_cong sets_pair_measure_cong sets_return spaceM)
moreover have 3:"(return K x) ⨂⇩M N = (N ⤜ f) "
by(subst Giry_strength_bind_return[OF N x])(metis f_def return_cong sets_pair_measure_cong sets_return spaceN)
ultimately show "DP_divergence ((return K x) ⨂⇩M M) ((return K x) ⨂⇩M N) ε1 ≤ δ1"
by auto
qed
subsubsection ‹ Additivity: law for the double-strength of the Giry monad›
lemma DP_divergence_additivity:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
and M2: "M2 ∈ space (prob_algebra K)"
and N2: "N2 ∈ space (prob_algebra K)"
and div1: "DP_divergence M N ε1 ≤ (δ1 :: real)"
and div2': "DP_divergence M2 N2 ε2 ≤ (δ2 :: real)"
and "0 ≤ ε1" and "0 ≤ ε2"
shows "DP_divergence (M ⨂⇩M M2) (N ⨂⇩M N2) (ε1 + ε2) ≤ δ1 + δ2"
proof-
interpret comparable_probability_measures L M N
by(unfold_locales, auto simp: assms)
interpret c2: comparable_probability_measures K M2 N2
by(unfold_locales, auto simp: assms)
have 1: "M ⨂⇩M M2 = M ⤜ (λx. M2 ⤜ (λy. return (L ⨂⇩M K) (x, y)))"
by(subst return_cong[of "M ⨂⇩M M2",symmetric])(auto simp: pair_prob_space_def pair_sigma_finite_def assms finite_measure_def prob_space_imp_sigma_finite sets_pair_measure intro!: pair_prob_space.pair_measure_eq_bind )
have 2: "N ⨂⇩M N2 = N ⤜ (λx. N2 ⤜ (λy. return (L ⨂⇩M K) (x, y)))"
by(subst return_cong[of "N ⨂⇩M N2",symmetric])(auto simp: pair_prob_space_def pair_sigma_finite_def assms finite_measure_def prob_space_imp_sigma_finite sets_pair_measure intro!: pair_prob_space.pair_measure_eq_bind )
have " DP_divergence (M ⨂⇩M M2) (N ⨂⇩M N2) (ε1 + ε2) = DP_divergence (M ⤜ (λx. M2 ⤜ (λy. return (L ⨂⇩M K) (x, y)))) (N ⤜ (λx. N2 ⤜ (λy. return (L ⨂⇩M K) (x, y)))) (ε1 + ε2)"
using 1 2 by auto
also have "... ≤ δ1 + δ2"
proof(rule DP_divergence_composability[where L = L and K = " (L ⨂⇩M K)"])
show "(λx. M2 ⤜ (λy. return (L ⨂⇩M K) (x, y))) ∈ L →⇩M prob_algebra (L ⨂⇩M K)"
and "(λx. N2 ⤜ (λy. return (L ⨂⇩M K) (x, y))) ∈ L →⇩M prob_algebra (L ⨂⇩M K)"
by(rule measurable_bind_prob_space2[where N = K],auto simp: assms)+
qed(auto intro!: DP_divergence_postprocessing[where K = "L ⨂⇩M K"] assms measurable_bind_prob_space2[where N = K])
finally show ?thesis.
qed
subsection ‹Hypotehsis testing interpretation›
subsubsection ‹Privacy region›
definition DP_region_one_side :: "real ⇒ real ⇒ (real × real) set" where
"DP_region_one_side ε δ = {(x::real,y::real). (x - exp(ε) * y ≤ δ) ∧ 0 ≤ x ∧ x ≤ 1 ∧ 0≤ y ∧ y ≤ 1} "
lemma DP_divergence_region:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
shows "(∀ A ∈ (sets M). ((measure M A, measure N A) ∈ DP_region_one_side ε δ)) ⟷ DP_divergence M N ε ≤ (δ :: real)"
proof-
interpret comparable_probability_measures L M N
by(unfold_locales,auto simp: assms)
show ?thesis
by(subst DP_divergence_forall[symmetric],unfold DP_region_one_side_def,auto intro!: prob_space.prob_le_1)
qed
subsubsection ‹2-generatedness of @{term DP_divergence} \cite{DBLP:journals/corr/abs-1905-09982} ›
lemma DP_divergence_2_generated_deterministic:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
and "0 ≤ ε"
shows "DP_divergence M N ε = (⨆ f ∈ L →⇩M (count_space (UNIV :: bool set)). DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε)"
proof-
interpret comparable_probability_measures L M N
by(unfold_locales,auto simp: assms)
show ?thesis
proof(intro SUP_eqI[THEN sym])
fix f :: "_⇒bool" assume A0: "Measurable.pred L f"
hence eq1: "distr M (count_space UNIV) f = M ⤜ return (count_space UNIV) ∘ f"
by (metis bind_return_distr measurable_cong_sets prob_space.not_empty prob_spaceM spaceM)
have eq2: "distr N (count_space UNIV) f = N ⤜ return (count_space UNIV) ∘ f"
by (metis A0 bind_return_distr measurable_cong_sets prob_space.not_empty prob_spaceN spaceN)
have "DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε = DP_divergence (M ⤜ return (count_space UNIV) ∘ f) (N ⤜ return (count_space UNIV) ∘ f) ε"
using eq1 eq2 by auto
also have "... ≤ DP_divergence M N ε"
by(rule ereal_le_real,auto intro!: DP_divergence_postprocessing measurable_comp[where N = "count_space UNIV"] A0 assms measurable_return_prob_space)
finally show "DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε ≤ DP_divergence M N ε".
next
fix y :: ereal assume A0: "(⋀f. Measurable.pred L f ⟹ DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε ≤ y)"
show "DP_divergence M N ε ≤ y"
unfolding DP_divergence_def
proof(subst Sup_le_iff,safe)
fix i assume A1: "i ∈ sets M"
hence [measurable]: "Measurable.pred L (λ x.(x ∈ i))"
by auto
have [simp]:"(λx. x ∈ i) -` {True} = i"
by auto
from A1 A0 have "DP_divergence (distr M (count_space UNIV) (λ x.(x ∈ i))) (distr N (count_space UNIV) (λ x.(x ∈ i))) ε ≤ y"
by auto
hence ineq1: "measure (distr M (count_space UNIV) (λ x.(x ∈ i))) {True} - exp ε * measure (distr N (count_space UNIV) (λ x.(x ∈ i))) {True} ≤ y"
using DP_divergence_def[of "(distr M (count_space UNIV) (λ x.(x ∈ i)))" "(distr N (count_space UNIV) (λ x.(x ∈ i)))"ε ] by (auto simp: Sup_le_iff)
have eq1: "measure (distr M (count_space UNIV) (λ x.(x ∈ i))) {True} = measure M i "
using measure_distr[of "(λ x.(x ∈ i))"M "(count_space UNIV)" "{True}"] spaceM(1) A1 by auto
have eq2: "measure (distr N (count_space UNIV) (λ x.(x ∈ i))) {True} = measure N i "
using measure_distr[of "(λ x.(x ∈ i))"N "(count_space UNIV)" "{True}"] spaceN(1) A1 by auto
from ineq1 show "ereal (measure M i - exp ε * measure N i) ≤ y"
unfolding eq1 eq2 by auto
qed
qed
qed
lemma DP_divergence_2_generated:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
assumes "0 ≤ ε"
shows "DP_divergence M N ε = (⨆ f ∈ L →⇩M (prob_algebra (count_space (UNIV :: bool set))). DP_divergence (M ⤜ f) (N ⤜ f) ε)"
proof-
interpret comparable_probability_measures L M N
by(unfold_locales,auto simp: assms)
show ?thesis
proof(subst DP_divergence_2_generated_deterministic[OF assms],intro order_antisym)
show "(⨆f∈L →⇩M prob_algebra (count_space (UNIV :: bool set)). DP_divergence (M ⤜ f) (N ⤜ f) ε) ≤ (⨆f∈L →⇩M count_space (UNIV :: bool set). DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε)"
proof(subst SUP_le_iff)
show "∀i∈L →⇩M prob_algebra (count_space (UNIV :: bool set)). DP_divergence (M ⤜ i) (N ⤜ i) ε ≤ (⨆f∈L →⇩M count_space (UNIV :: bool set). DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε)"
proof
fix i :: "_ ⇒ bool measure" assume A0: "i ∈ L →⇩M prob_algebra (count_space UNIV)"
have "DP_divergence (M ⤜ i) (N ⤜ i) ε ≤ DP_divergence M N ε"
using DP_divergence_postprocessing A0 assms ereal_le_real by blast
also have "... = (⨆f :: 'a ⇒ bool∈L →⇩M count_space UNIV. DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε)"
using DP_divergence_2_generated_deterministic assms by blast
finally show "DP_divergence (M ⤜ i) (N ⤜ i) ε ≤ (⨆f :: 'a ⇒ bool∈L →⇩M count_space UNIV. DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε)".
qed
qed
show "(⨆f :: 'a ⇒ bool∈L →⇩M count_space UNIV. DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε) ≤ (⨆f :: 'a ⇒ bool measure∈L →⇩M prob_algebra (count_space UNIV). DP_divergence (M ⤜ f) (N ⤜ f) ε)"
proof(rule SUP_mono)
fix f :: "_⇒bool" assume A0: "f ∈ L →⇩M count_space UNIV"
show "∃m :: 'a ⇒ bool measure∈L →⇩M prob_algebra (count_space UNIV). DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε ≤ DP_divergence (M ⤜ m) (N ⤜ m) ε"
proof(unfold Bex_def)
have "(((return (count_space UNIV)) o f) ∈ L →⇩M prob_algebra (count_space UNIV)) ∧ (DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε = DP_divergence (M ⤜((return (count_space (UNIV :: bool set))) o f)) (N ⤜((return (count_space (UNIV :: bool set))) o f)) ε)"
proof(safe)
show "return (count_space UNIV) ∘ f ∈ L →⇩M prob_algebra (count_space UNIV)"using A0 by auto
from A0 have eq1: "(distr M (count_space UNIV) f) = M ⤜((return (count_space (UNIV :: bool set))) o f)"
by (metis bind_return_distr measurable_return1 prob_space.not_empty return_sets_cong spaceM prob_spaceM)
from A0 have eq2: "(distr N (count_space UNIV) f) = N ⤜((return (count_space (UNIV :: bool set))) o f)"
by (metis bind_return_distr measurable_cong_sets prob_space.not_empty spaceMN_M spaceMN_N spaceN prob_spaceN )
from eq1 eq2 show "DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε = DP_divergence (M ⤜ return (count_space UNIV) ∘ f) (N ⤜ return (count_space UNIV) ∘ f) ε"
by auto
qed
thus "∃x :: 'a ⇒ bool measure. x ∈ L →⇩M prob_algebra (count_space UNIV) ∧ DP_divergence (distr M (count_space UNIV) f) (distr N (count_space UNIV) f) ε ≤ DP_divergence (M ⤜ x) (N ⤜ x) ε"
by auto
qed
qed
qed
qed
subsection ‹real version of @{term DP_divergence}›
subsubsection ‹finiteness›
definition DP_divergence_real :: "'a measure ⇒ 'a measure ⇒ real ⇒ real " where
"DP_divergence_real M N ε = Sup {(measure M A - (exp ε) * measure N A) | A::'a set. A ∈ (sets M)}"
lemma DP_divergence_real_SUP:
shows "DP_divergence_real M N ε = (⨆ (A::'a set) ∈ (sets M). (measure M A - (exp ε) * measure N A))"
by (auto simp: setcompr_eq_image DP_divergence_real_def)
lemma DP_divergence_real_leI:
assumes "⋀ A. A ∈ (sets M) ⟹ measure M A ≤ (exp ε) * measure N A + (δ :: real)"
shows "DP_divergence_real M N ε ≤ (δ :: real)"
using assms unfolding DP_divergence_real_def by(intro cSup_least, fastforce+)
subsubsection ‹real version of @{term DP_divergence}›
text ‹ If @{term M} and @{term N} are finite then @{term DP_divergence} and the following version @{term DP_divergence_real} are the same.
However, if @{term M} and @{term N} are not finite, @{term "DP_divergence_real M N ε"} is not well defined.
Hence, the latter needs extra assumptions for the finiteness of measures @{term M} and @{term N}.
For example the following lemmas need a kind of finiteness of@{term M} and @{term N}.›
lemma DP_divergence_is_real:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
shows "DP_divergence M N ε = DP_divergence_real M N ε"
unfolding DP_divergence_def DP_divergence_real_def
proof(subst ereal_Sup)
interpret pM: prob_space M
using M actual_prob_space by auto
interpret pN: prob_space N
using N actual_prob_space by auto
{
fix A assume "A ∈ (sets M)"
have "pM.prob A - exp ε * pN.prob A ≤ pM.prob A"
by auto
also have "... ≤ 1"
by auto
finally have 1: "pM.prob A - exp ε * pN.prob A ≤ 1".
have " - exp ε ≤ - exp ε * pN.prob A"
by auto
also have "... ≤ pM.prob A - exp ε * pN.prob A"
by auto
finally have 2: "- exp ε ≤ pM.prob A - exp ε * pN.prob A".
note 1 2
}note * = this
hence "⨆ (ereal ` {pM.prob A - exp ε * pN.prob A |A. A ∈ pM.events}) ≤ ereal 1"
unfolding SUP_le_iff by auto
moreover from * have "ereal (- exp ε) ≤ ⨆ (ereal ` {pM.prob A - exp ε * pN.prob A |A. A ∈ pM.events})"
by(intro SUP_upper2, auto)
ultimately show " ¦⨆ (ereal ` {pM.prob A - exp ε * pN.prob A |A. A ∈ pM.events})¦ ≠ ∞"
by auto
have " {ereal (pM.prob A - exp ε * pN.prob A) |A. A ∈ pM.events} = ereal ` {pM.prob A - exp ε * pN.prob A |A. A ∈ pM.events}"
by blast
thus " ⨆ {ereal (pM.prob A - exp ε * pN.prob A) |A. A ∈ pM.events} = ⨆ (ereal ` {pM.prob A - exp ε * pN.prob A |A. A ∈ pM.events})"
by auto
qed
corollary DP_divergence_real_forall:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
shows "(∀ A ∈ (sets M). (measure M A - (exp ε) * measure N A ≤ (δ :: real))) ⟷ DP_divergence_real M N ε ≤ (δ :: real)"
unfolding DP_divergence_forall DP_divergence_is_real[OF M N] by auto
corollary DP_divergence_real_inequality1:
assumes M: "M ∈ space (prob_algebra L)"
and N: "N ∈ space (prob_algebra L)"
and "A ∈ (sets M)" and "DP_divergence_real M N ε ≤ (δ :: real)"
shows "measure M A ≤ (exp ε) * measure N A + (δ :: real)"
using DP_divergence_real_forall[OF M N] assms(3) assms(4) by force
end