From 9082a8ba56d17655949521d6b70c0fbc0d6add39 Mon Sep 17 00:00:00 2001 From: Kousha Kalantari <25445970+KoushaKalantari@users.noreply.github.com> Date: Wed, 11 Nov 2026 17:43:46 -0800 Subject: [PATCH 1/2] feat: maximal leakage (Issa-Wagner-Kamath) Operational definition and Theorem 1 (supremum attained), data processing in both directions, support bounds, zero leakage iff independence, composition, additivity, and I(X;Y) <= L(X->Y) via mutualInfo. Co-Authored-By: Claude Opus 5.5 --- Statlib.lean | 4 + Statlib/Divergence/MaximalLeakage/Basic.lean | 156 ++++++++ .../Divergence/MaximalLeakage/MutualInfo.lean | 133 +++++++ .../MaximalLeakage/Operational.lean | 374 ++++++++++++++++++ .../Divergence/MaximalLeakage/Properties.lean | 285 +++++++++++++ 5 files changed, 952 insertions(+) create mode 100644 Statlib/Divergence/MaximalLeakage/Basic.lean create mode 100644 Statlib/Divergence/MaximalLeakage/MutualInfo.lean create mode 100644 Statlib/Divergence/MaximalLeakage/Operational.lean create mode 100644 Statlib/Divergence/MaximalLeakage/Properties.lean diff --git a/Statlib.lean b/Statlib.lean index a5f1af4..fd45fc9 100644 --- a/Statlib.lean +++ b/Statlib.lean @@ -38,6 +38,10 @@ import Statlib.Divergence.KullbackLeibler.CondKL import Statlib.Divergence.KullbackLeibler.Estimation import Statlib.Divergence.KullbackLeibler.Event import Statlib.Divergence.KullbackLeibler.KLDivFun +import Statlib.Divergence.MaximalLeakage.Basic +import Statlib.Divergence.MaximalLeakage.MutualInfo +import Statlib.Divergence.MaximalLeakage.Operational +import Statlib.Divergence.MaximalLeakage.Properties import Statlib.Divergence.MutualInformation.Basic import Statlib.Divergence.MutualInformation.Bool import Statlib.Divergence.MutualInformation.Estimation diff --git a/Statlib/Divergence/MaximalLeakage/Basic.lean b/Statlib/Divergence/MaximalLeakage/Basic.lean new file mode 100644 index 0000000..109d6e3 --- /dev/null +++ b/Statlib/Divergence/MaximalLeakage/Basic.lean @@ -0,0 +1,156 @@ +/- +Copyright (c) 2026 Kousha Kalantari. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kousha Kalantari +-/ +module + +public import Mathlib.Analysis.SpecialFunctions.Log.Basic +public import Mathlib.MeasureTheory.Integral.Lebesgue.Countable +public import Mathlib.Probability.Kernel.Composition.Comp + +/-! +# Maximal leakage on finite output alphabets + +Issa, Wagner and Kamath define the maximal leakage from `X` to `Y` operationally, as the largest +multiplicative gain an adversary observing `Y` gets in guessing any (randomized) function of `X`. +For finite alphabets they show (Theorem 1 of *An operational approach to information leakage*, +IEEE Trans. Inf. Theory 66(3), 2020) that it equals +`L(X → Y) = log ∑_y max_{x ∈ supp P_X} P_{Y|X}(y | x)`. + +This file takes that closed form as the definition, for an input law `μ` and a channel given by a +kernel `κ : Kernel α β` with finite output alphabet `β`. Logarithms are natural (nats), as in +Mathlib's `klDiv`. + +**Scope.** The supremum ranges over the atoms of `μ`, so the definition is only meaningful when +`μ` is purely atomic, e.g. when `α` is countable with measurable singletons. For an atomless `μ` +it is `0` and does *not* equal the operational maximal leakage. The lemmas below that need an +atom take it as an explicit hypothesis. + +## Main definitions + +* `maxLeakageSum μ κ`: the sum `∑_y ⨆_{x : μ {x} ≠ 0} κ x {y}`, in `ℝ≥0∞`. +* `maxLeakage μ κ`: its logarithm, the maximal leakage, in `ℝ`. + +## Main statements + +* `one_le_maxLeakageSum`, `maxLeakage_nonneg`: maximal leakage is nonnegative. +* `maxLeakageSum_le_card`, `maxLeakage_le_log_card`: `L(X → Y) ≤ log |Y|`. +* `maxLeakageSum_le_card_support`: `L(X → Y) ≤ log |supp X|`, multiplicative form. +* `maxLeakageSum_comp_le`, `maxLeakage_comp_le`: **data processing** — post-processing the output + through another channel `η` cannot increase maximal leakage. + +## See also + +* `Statlib.Divergence.MaximalLeakage.Operational`: the operational definition and Theorem 1 of + Issa–Wagner–Kamath, which shows that this closed form equals it. +* `Statlib.Divergence.MaximalLeakage.Properties`: data processing for pre-processing, + `L(X → Y) ≤ log |supp Y|`, zero leakage iff independence, composition and additivity. +* `Statlib.Divergence.MaximalLeakage.MutualInfo`: `I(X; Y) ≤ L(X → Y)`. + +## TODO + +* Maximal leakage as Sibson mutual information of order `∞`, and beyond finite alphabets. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +namespace InformationTheory + +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ : Measure α} {κ : Kernel α β} + +/-- The sum `∑_y ⨆_{x ∈ supp μ} κ x {y}` whose logarithm is the maximal leakage `maxLeakage μ κ`. +The supremum ranges over the atoms of `μ`, so this is only meaningful when `μ` is purely atomic, +e.g. for a countable input alphabet with measurable singletons. -/ +noncomputable def maxLeakageSum [Fintype β] (μ : Measure α) (κ : Kernel α β) : ℝ≥0∞ := + ∑ y, ⨆ (x) (_ : μ {x} ≠ 0), κ x {y} + +/-- The maximal leakage `L(X → Y)` from an input `X ∼ μ` to the output `Y` of the channel `κ`, +in nats, for a finite output alphabet and a purely atomic `μ` (see `maxLeakageSum`). -/ +noncomputable def maxLeakage [Fintype β] (μ : Measure α) (κ : Kernel α β) : ℝ := + Real.log (maxLeakageSum μ κ).toReal + +section Bounds + +variable [Fintype β] [MeasurableSingletonClass β] [IsMarkovKernel κ] + +omit [MeasurableSingletonClass β] in +lemma maxLeakageSum_le_card : maxLeakageSum μ κ ≤ Fintype.card β := by + calc maxLeakageSum μ κ ≤ ∑ _y : β, (1 : ℝ≥0∞) := + Finset.sum_le_sum fun y _ ↦ iSup₂_le fun x _ ↦ prob_le_one + _ = Fintype.card β := by simp + +omit [MeasurableSingletonClass β] in +lemma maxLeakageSum_ne_top : maxLeakageSum μ κ ≠ ∞ := + ne_top_of_le_ne_top (ENNReal.natCast_ne_top _) maxLeakageSum_le_card + +/-- Any atom `x` of `μ` already contributes the full mass `∑_y κ x {y} = 1`. -/ +lemma one_le_maxLeakageSum {x : α} (hx : μ {x} ≠ 0) : 1 ≤ maxLeakageSum μ κ := by + calc (1 : ℝ≥0∞) = ∑ y, κ x {y} := by simp [sum_measure_singleton (μ := κ x)] + _ ≤ maxLeakageSum μ κ := + Finset.sum_le_sum fun y _ ↦ le_iSup₂ (f := fun x (_ : μ {x} ≠ 0) ↦ κ x {y}) x hx + +lemma one_le_toReal_maxLeakageSum {x : α} (hx : μ {x} ≠ 0) : + 1 ≤ (maxLeakageSum μ κ).toReal := by + simpa using (ENNReal.toReal_le_toReal ENNReal.one_ne_top maxLeakageSum_ne_top).2 + (one_le_maxLeakageSum hx) + +lemma maxLeakage_nonneg {x : α} (hx : μ {x} ≠ 0) : 0 ≤ maxLeakage μ κ := + Real.log_nonneg (one_le_toReal_maxLeakageSum hx) + +/-- Maximal leakage is at most the logarithm of the output alphabet size. -/ +lemma maxLeakage_le_log_card {x : α} (hx : μ {x} ≠ 0) : + maxLeakage μ κ ≤ Real.log (Fintype.card β) := by + refine Real.log_le_log (by linarith [one_le_toReal_maxLeakageSum (κ := κ) hx]) ?_ + simpa using (ENNReal.toReal_le_toReal maxLeakageSum_ne_top (ENNReal.natCast_ne_top _)).2 + maxLeakageSum_le_card + +/-- Multiplicative form of `L(X → Y) ≤ log |supp X|`. -/ +lemma maxLeakageSum_le_card_support [Fintype α] [DecidablePred fun x : α ↦ μ {x} ≠ 0] : + maxLeakageSum μ κ ≤ (Finset.univ.filter fun x : α ↦ μ {x} ≠ 0).card := by + set S := Finset.univ.filter fun x : α ↦ μ {x} ≠ 0 + calc maxLeakageSum μ κ ≤ ∑ y, ∑ x ∈ S, κ x {y} := + Finset.sum_le_sum fun y _ ↦ iSup₂_le fun x hx ↦ + Finset.single_le_sum (f := fun x ↦ κ x {y}) (fun _ _ ↦ zero_le) (by simpa [S] using hx) + _ = ∑ x ∈ S, ∑ y, κ x {y} := Finset.sum_comm + _ = S.card := by simp [sum_measure_singleton] + +end Bounds + +section DataProcessing + +variable [Fintype β] [MeasurableSingletonClass β] [Fintype γ] [MeasurableSingletonClass γ] + +/-- **Data processing** for maximal leakage, multiplicative form: post-processing the channel +output by a Markov kernel `η` cannot increase `∑_y max_x κ x {y}`. -/ +lemma maxLeakageSum_comp_le (η : Kernel β γ) [IsMarkovKernel η] : + maxLeakageSum μ (η ∘ₖ κ) ≤ maxLeakageSum μ κ := by + have h_comp (x : α) (z : γ) : (η ∘ₖ κ) x {z} = ∑ y, η y {z} * κ x {y} := by + rw [Kernel.comp_apply' _ _ _ (measurableSet_singleton z), lintegral_fintype] + calc maxLeakageSum μ (η ∘ₖ κ) + ≤ ∑ z, ∑ y, η y {z} * ⨆ (x) (_ : μ {x} ≠ 0), κ x {y} := by + refine Finset.sum_le_sum fun z _ ↦ iSup₂_le fun x hx ↦ ?_ + rw [h_comp] + exact Finset.sum_le_sum fun y _ ↦ + mul_le_mul_right (le_iSup₂ (f := fun x (_ : μ {x} ≠ 0) ↦ κ x {y}) x hx) _ + _ = ∑ y, (∑ z, η y {z}) * ⨆ (x) (_ : μ {x} ≠ 0), κ x {y} := by + rw [Finset.sum_comm] + simp_rw [Finset.sum_mul] + _ = maxLeakageSum μ κ := by simp [maxLeakageSum, sum_measure_singleton] + +/-- **Data processing** for maximal leakage: for a Markov chain `X - Y - Z` obtained by +post-processing `Y` through `η`, `L(X → Z) ≤ L(X → Y)`. -/ +lemma maxLeakage_comp_le [IsMarkovKernel κ] (η : Kernel β γ) [IsMarkovKernel η] {x : α} + (hx : μ {x} ≠ 0) : + maxLeakage μ (η ∘ₖ κ) ≤ maxLeakage μ κ := by + refine Real.log_le_log (by linarith [one_le_toReal_maxLeakageSum (κ := η ∘ₖ κ) hx]) ?_ + exact (ENNReal.toReal_le_toReal maxLeakageSum_ne_top maxLeakageSum_ne_top).2 + (maxLeakageSum_comp_le η) + +end DataProcessing + +end InformationTheory diff --git a/Statlib/Divergence/MaximalLeakage/MutualInfo.lean b/Statlib/Divergence/MaximalLeakage/MutualInfo.lean new file mode 100644 index 0000000..09d4c42 --- /dev/null +++ b/Statlib/Divergence/MaximalLeakage/MutualInfo.lean @@ -0,0 +1,133 @@ +/- +Copyright (c) 2026 Kousha Kalantari. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kousha Kalantari +-/ +module + +public import Statlib.Divergence.MaximalLeakage.Basic +public import Statlib.Divergence.MutualInformation.Basic + +/-! +# Mutual information is at most maximal leakage + +Let `X ∼ μ` be an input on a countable alphabet and `Y` the output of a channel `κ` with a finite +output alphabet. Lemma 2 of Issa, Wagner and Kamath states that the mutual information is at most +the maximal leakage: `I(X; Y) ≤ L(X → Y) = log ∑_y max_{x ∈ supp P_X} P_{Y|X}(y | x)`. + +## Main statements + +* `mutualInfo_compProd_le_ofReal_maxLeakage`: `I(X; Y) ≤ L(X → Y)`, in `ℝ≥0∞`. +* `mutualInfo_compProd_ne_top`: in particular `I(X; Y)` is finite. +* `toReal_mutualInfo_compProd_le_maxLeakage`: `I(X; Y) ≤ L(X → Y)`, in `ℝ`. + +## Implementation notes + +Instead of applying Jensen's inequality to a finite-sum formula for `I(X; Y)`, we compare the +joint law with `μ × ν`, where `ν {y} ∝ max_{x ∈ supp μ} κ x {y}`. The compensation identity gives +`I(X; Y) ≤ KL(μ ⊗ κ, μ × ν) = ∫ KL(κ x, ν) dμ(x)`. Writing `S = ∑_y max_{x ∈ supp μ} κ x {y}`, every +atom `x` of `μ` satisfies `κ x {y} ≤ S * ν {y}`, so the log-likelihood ratio of `κ x` with respect +to `ν` is bounded by `log S` and `KL(κ x, ν) ≤ log S = L(X → Y)`. + +## References + +* I. Issa, A. B. Wagner, S. Kamath, *An operational approach to information leakage*, + IEEE Trans. Inf. Theory 66(3), 2020, Lemma 2. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +namespace InformationTheory + +variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {μ : Measure α} {κ : Kernel α β} + +section Auxiliary + +/- General-purpose lemmas, independent of maximal leakage; candidates for Mathlib. -/ + +/-- A nonzero measure on a countable space has an atom. -/ +lemma _root_.MeasureTheory.Measure.exists_measure_singleton_ne_zero [Countable α] + (μ : Measure α) [NeZero μ] : + ∃ x, μ {x} ≠ 0 := by + by_contra! h + exact NeZero.ne μ <| Measure.measure_univ_eq_zero.1 <| + (measure_null_iff_singleton Set.countable_univ).2 fun x _ ↦ h x + +/-- On a finite space, if `μ {y} ≤ c * ν {y}` for every `y`, then the Kullback-Leibler divergence +between the probability measures `μ` and `ν` is at most `log c`. -/ +lemma klDiv_le_ofReal_log_of_forall_le [Finite β] [MeasurableSingletonClass β] + {μ ν : Measure β} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] {c : ℝ≥0∞} (hc : c ≠ ∞) + (h : ∀ y, μ {y} ≤ c * ν {y}) : + klDiv μ ν ≤ ENNReal.ofReal (Real.log c.toReal) := by + have hac : μ ≪ ν := fun s hs ↦ by + rw [measure_eq_zero_iff_ae_notMem, ae_iff_of_countable] at hs ⊢ + exact fun y hy ↦ hs y fun hνy ↦ hy (by simpa [hνy] using h y) + have h_int : Integrable (llr μ ν) μ := .of_finite + -- At every atom `y` of `μ`, the density `dμ/dν` is positive and at most `c`. + have h_llr : ∀ᵐ y ∂μ, llr μ ν y ≤ Real.log c.toReal := by + refine ae_iff_of_countable.2 fun y hy ↦ ?_ + have hy_eq : μ {y} = μ.rnDeriv ν y * ν {y} := by + rw [← Measure.setLIntegral_rnDeriv hac, lintegral_singleton] + have h_pos : μ.rnDeriv ν y ≠ 0 := fun h0 ↦ hy (by simp [hy_eq, h0]) + have hνy : ν {y} ≠ 0 := fun h0 ↦ hy (by simp [hy_eq, h0]) + have h_le : μ.rnDeriv ν y ≤ c := + (ENNReal.mul_le_mul_iff_left hνy (measure_ne_top ν _)).1 (hy_eq ▸ h y) + exact Real.log_le_log (ENNReal.toReal_pos h_pos (ne_top_of_le_ne_top hc h_le)) + (ENNReal.toReal_mono hc h_le) + calc klDiv μ ν = ENNReal.ofReal (∫ y, llr μ ν y ∂μ) := by + simp [klDiv_of_ac_of_integrable hac h_int] + _ ≤ ENNReal.ofReal (∫ _, Real.log c.toReal ∂μ) := + ENNReal.ofReal_le_ofReal (integral_mono_ae h_int (integrable_const _) h_llr) + _ = ENNReal.ofReal (Real.log c.toReal) := by simp + +end Auxiliary + +variable [Countable α] [Fintype β] [MeasurableSingletonClass β] [IsProbabilityMeasure μ] + [IsMarkovKernel κ] + +/-- **Mutual information is at most maximal leakage** (Issa–Wagner–Kamath, Lemma 2): +`I(X; Y) ≤ L(X → Y)` for `X ∼ μ` on a countable alphabet and `Y` the output of the channel `κ`. -/ +theorem mutualInfo_compProd_le_ofReal_maxLeakage : + mutualInfo (μ ⊗ₘ κ) ≤ ENNReal.ofReal (maxLeakage μ κ) := by + obtain ⟨x₀, hx₀⟩ := MeasureTheory.Measure.exists_measure_singleton_ne_zero μ + set S := maxLeakageSum μ κ + have hS₀ : S ≠ 0 := (zero_lt_one.trans_le (one_le_maxLeakageSum hx₀)).ne' + have hS : S ≠ ∞ := maxLeakageSum_ne_top + -- The output law `ν {y} = S⁻¹ * max_{x ∈ supp μ} κ x {y}`. + let ν : Measure β := S⁻¹ • Measure.sum fun y ↦ (⨆ (x) (_ : μ {x} ≠ 0), κ x {y}) • .dirac y + have hν (y : β) : ν {y} = S⁻¹ * ⨆ (x) (_ : μ {x} ≠ 0), κ x {y} := by + simp only [ν, smul_apply, Measure.sum_smul_dirac_singleton, smul_eq_mul] + have : IsProbabilityMeasure ν := + ⟨by simpa [ν, S, maxLeakageSum] using ENNReal.inv_mul_cancel hS₀ hS⟩ + calc mutualInfo (μ ⊗ₘ κ) ≤ klDiv (μ ⊗ₘ κ) (μ.prod ν) := + le_self_add.trans_eq (klDiv_compProd_prod_eq_mutualInfo_add μ κ ν).symm + _ = ∫⁻ x, klDiv (κ x) ν ∂μ := by + rw [← Measure.compProd_const, ← condKL, condKL_eq_lintegral] + simp + _ ≤ ∫⁻ _, ENNReal.ofReal (maxLeakage μ κ) ∂μ := by + refine lintegral_mono_ae <| ae_iff_of_countable.2 fun x hx ↦ ?_ + refine klDiv_le_ofReal_log_of_forall_le hS fun y ↦ ?_ + rw [hν, ENNReal.mul_inv_cancel_left hS₀ hS] + exact le_iSup₂ (f := fun x (_ : μ {x} ≠ 0) ↦ κ x {y}) x hx + _ = ENNReal.ofReal (maxLeakage μ κ) := by simp + +omit [Fintype β] in +/-- The mutual information between an input on a countable alphabet and the output of a channel +with a finite output alphabet is finite. -/ +theorem mutualInfo_compProd_ne_top [Finite β] : mutualInfo (μ ⊗ₘ κ) ≠ ∞ := by + have := Fintype.ofFinite β + exact ne_top_of_le_ne_top ENNReal.ofReal_ne_top mutualInfo_compProd_le_ofReal_maxLeakage + +/-- **Mutual information is at most maximal leakage** (Issa–Wagner–Kamath, Lemma 2), real-valued +version: `I(X; Y) ≤ L(X → Y)`. -/ +theorem toReal_mutualInfo_compProd_le_maxLeakage : + (mutualInfo (μ ⊗ₘ κ)).toReal ≤ maxLeakage μ κ := by + obtain ⟨x, hx⟩ := MeasureTheory.Measure.exists_measure_singleton_ne_zero μ + exact ENNReal.toReal_le_of_le_ofReal (maxLeakage_nonneg hx) + mutualInfo_compProd_le_ofReal_maxLeakage + +end InformationTheory diff --git a/Statlib/Divergence/MaximalLeakage/Operational.lean b/Statlib/Divergence/MaximalLeakage/Operational.lean new file mode 100644 index 0000000..4c6415f --- /dev/null +++ b/Statlib/Divergence/MaximalLeakage/Operational.lean @@ -0,0 +1,374 @@ +/- +Copyright (c) 2026 Kousha Kalantari. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kousha Kalantari +-/ +module + +public import Statlib.Divergence.MaximalLeakage.Basic +public import Mathlib.Probability.Kernel.Composition.Prod +public import Mathlib.Probability.Kernel.Composition.MeasureComp + +/-! +# Operational meaning of maximal leakage + +Issa, Wagner and Kamath (*An operational approach to information leakage*, IEEE Trans. Inf. +Theory 66(3), 2020, Definition 1) define the maximal leakage from `X` to `Y` as +`L(X → Y) = sup_{U - X - Y - Û} log (P[U = Û] / max_u P_U(u))`, +the supremum ranging over all random variables `U`, `Û` on a common finite alphabet forming the +Markov chain `U - X - Y - Û`. It measures how much observing `Y` multiplies an adversary's chance +of guessing *some* randomized function `U` of `X`. Their Theorem 1 evaluates it in closed form: +`L(X → Y) = log ∑_y max_{x ∈ supp P_X} P_{Y|X}(y | x)`. + +We formalize the definition and prove Theorem 1 for finite alphabets. + +## Main definitions + +* `guessProb μ ρ κ g`: `P[U = Û]` when `X ∼ μ`, `U` is drawn from `X` through `ρ`, `Y` from `X` + through `κ` and the guess `Û` from `Y` through `g`. +* `blindGuessProb μ ρ`: `max_u P_U(u)`, the best success probability without observing `Y`. +* `opMaxLeakageSum μ κ`: the supremum of `P[U = Û] / max_u P_U(u)` over all finite alphabets + `Fin n` and all kernels `ρ`, `g`. Its logarithm is the operational maximal leakage. + +## Main statements + +* `guessProb_le`: the converse, `P[U = Û] ≤ (∑_y max_x κ x {y}) · max_u P_U(u)`. +* `opMaxLeakageSum_eq_maxLeakageSum`: **Theorem 1 of Issa–Wagner–Kamath**, the operational + definition equals the closed form `maxLeakageSum`. +* `exists_guessProb_div_eq`: the supremum is attained by an explicit guessing problem. +* `isGreatest_log_guessRatio`: Theorem 1 in the exact form of Definition 1, as the largest + value of `log (P[U = Û] / max_u P_U(u))`. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +namespace InformationTheory + +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ : Measure α} {κ : Kernel α β} {ρ : Kernel α γ} {g : Kernel β γ} + +/-- `P[U = Û]` in the Markov chain `U - X - Y - Û`: `X ∼ μ`, `U` is drawn from `X` through `ρ`, +`Y` is drawn from `X` through `κ` (independently of `U` given `X`), and the guess `Û` is drawn +from `Y` through `g`. -/ +noncomputable def guessProb (μ : Measure α) (ρ : Kernel α γ) (κ : Kernel α β) (g : Kernel β γ) : + ℝ≥0∞ := + ((ρ ×ₖ (g ∘ₖ κ)) ∘ₘ μ) {p | p.1 = p.2} + +/-- `max_u P_U(u)`: the best probability of guessing `U` without any observation. -/ +noncomputable def blindGuessProb (μ : Measure α) (ρ : Kernel α γ) : ℝ≥0∞ := + ⨆ u, (ρ ∘ₘ μ) {u} + +/-- The operational maximal leakage of Issa–Wagner–Kamath, multiplicative form: the supremum of +`P[U = Û] / max_u P_U(u)` over all finite alphabets `Fin n` for `U` and `Û`, all randomized +functions `ρ` of `X`, and all guessing rules `g` from `Y`. -/ +noncomputable def opMaxLeakageSum (μ : Measure α) (κ : Kernel α β) : ℝ≥0∞ := + ⨆ (n : ℕ) (ρ : Kernel α (Fin n)) (_ : IsMarkovKernel ρ) (g : Kernel β (Fin n)) + (_ : IsMarkovKernel g), guessProb μ ρ κ g / blindGuessProb μ ρ + +section Formulas + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + [Fintype γ] [MeasurableSingletonClass γ] + +omit [Fintype β] [MeasurableSingletonClass β] [Fintype γ] in +lemma comp_apply_singleton (μ : Measure α) (ρ : Kernel α γ) (u : γ) : + (ρ ∘ₘ μ) {u} = ∑ x, ρ x {u} * μ {x} := by + rw [Measure.bind_apply (measurableSet_singleton u) ρ.measurable.aemeasurable, + lintegral_fintype] + +omit [Fintype α] [MeasurableSingletonClass α] [Fintype γ] in +lemma kernel_comp_apply_singleton (κ : Kernel α β) (g : Kernel β γ) (x : α) (u : γ) : + (g ∘ₖ κ) x {u} = ∑ y, g y {u} * κ x {y} := by + rw [Kernel.comp_apply' _ _ _ (measurableSet_singleton u), lintegral_fintype] + +/-- `P[U = Û]` as a finite sum. -/ +lemma guessProb_eq_sum [IsMarkovKernel ρ] [IsMarkovKernel κ] [IsMarkovKernel g] : + guessProb μ ρ κ g = ∑ x, ∑ u, ∑ y, g y {u} * κ x {y} * ρ x {u} * μ {x} := by + have h_diag (x : α) : (ρ ×ₖ (g ∘ₖ κ)) x {p | p.1 = p.2} = ∑ u, (g ∘ₖ κ) x {u} * ρ x {u} := by + rw [Kernel.prod_apply, Measure.prod_apply (Set.toFinite _).measurableSet, lintegral_fintype] + congr 1 with u + congr 2 + ext v + simp [eq_comm] + rw [guessProb, Measure.bind_apply (Set.toFinite _).measurableSet + (ρ ×ₖ (g ∘ₖ κ)).measurable.aemeasurable, lintegral_fintype] + simp only [h_diag, kernel_comp_apply_singleton, Finset.sum_mul] + +end Formulas + +section Converse + +variable [Finite α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + [Finite γ] [MeasurableSingletonClass γ] + +omit [Finite α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] in +/-- On the support of `μ`, each channel entry is at most its column maximum; off the support +the term vanishes. -/ +lemma mul_le_iSup_mul (x : α) (y : β) : + κ x {y} * μ {x} ≤ (⨆ (x') (_ : μ {x'} ≠ 0), κ x' {y}) * μ {x} := by + by_cases hx : μ {x} = 0 + · simp [hx] + · gcongr + exact le_iSup₂ (f := fun x' (_ : μ {x'} ≠ 0) ↦ κ x' {y}) x hx + +/-- **Converse half of Theorem 1**: observing `Y` multiplies the chance of guessing any `U` by at +most `∑_y max_x κ x {y}`. -/ +lemma guessProb_le [IsMarkovKernel ρ] [IsMarkovKernel κ] [IsMarkovKernel g] : + guessProb μ ρ κ g ≤ maxLeakageSum μ κ * blindGuessProb μ ρ := by + have := Fintype.ofFinite α + have := Fintype.ofFinite γ + set M : β → ℝ≥0∞ := fun y ↦ ⨆ (x) (_ : μ {x} ≠ 0), κ x {y} + calc guessProb μ ρ κ g + = ∑ x, ∑ u, ∑ y, g y {u} * ρ x {u} * (κ x {y} * μ {x}) := by + rw [guessProb_eq_sum] + refine Finset.sum_congr rfl fun x _ ↦ Finset.sum_congr rfl fun u _ ↦ + Finset.sum_congr rfl fun y _ ↦ by ring + _ ≤ ∑ x, ∑ u, ∑ y, g y {u} * ρ x {u} * (M y * μ {x}) := by + exact Finset.sum_le_sum fun x _ ↦ Finset.sum_le_sum fun u _ ↦ Finset.sum_le_sum + fun y _ ↦ mul_le_mul' le_rfl (mul_le_iSup_mul x y) + _ = ∑ x, ∑ y, ∑ u, g y {u} * ρ x {u} * (M y * μ {x}) := + Finset.sum_congr rfl fun x _ ↦ Finset.sum_comm + _ = ∑ y, ∑ x, ∑ u, g y {u} * ρ x {u} * (M y * μ {x}) := Finset.sum_comm + _ = ∑ y, ∑ u, ∑ x, g y {u} * ρ x {u} * (M y * μ {x}) := + Finset.sum_congr rfl fun y _ ↦ Finset.sum_comm + _ = ∑ y, M y * ∑ u, g y {u} * (ρ ∘ₘ μ) {u} := by + simp_rw [comp_apply_singleton, Finset.mul_sum] + exact Finset.sum_congr rfl fun y _ ↦ Finset.sum_congr rfl fun u _ ↦ + Finset.sum_congr rfl fun x _ ↦ by ring + _ ≤ ∑ y, M y * ∑ u, g y {u} * blindGuessProb μ ρ := by + gcongr with y _ u _ + exact le_iSup (fun u ↦ (ρ ∘ₘ μ) {u}) u + _ = maxLeakageSum μ κ * blindGuessProb μ ρ := by + simp_rw [← Finset.sum_mul, sum_measure_singleton, Finset.coe_univ, measure_univ, one_mul] + rw [maxLeakageSum, Finset.sum_mul] + +end Converse + +section Relabel + +variable [Finite α] [MeasurableSingletonClass α] [Finite β] [MeasurableSingletonClass β] + [Fintype γ] [MeasurableSingletonClass γ] + +/-- Relabelling the common alphabet `γ` of `U` and `Û` as `Fin (card γ)` preserves the +guessing ratio. -/ +lemma exists_fin_guessProb_div_eq [IsMarkovKernel ρ] [IsMarkovKernel κ] [IsMarkovKernel g] : + ∃ (ρ' : Kernel α (Fin (Fintype.card γ))) (_ : IsMarkovKernel ρ') + (g' : Kernel β (Fin (Fintype.card γ))) (_ : IsMarkovKernel g'), + guessProb μ ρ' κ g' / blindGuessProb μ ρ' = guessProb μ ρ κ g / blindGuessProb μ ρ := by + have := Fintype.ofFinite α + have := Fintype.ofFinite β + set e := Fintype.equivFin γ + have he : Measurable e := measurable_of_finite _ + have h_preimage (u : γ) : e ⁻¹' {e u} = {u} := by + ext v + simp + have h_mapρ (a : α) (u : γ) : ρ.map e a {e u} = ρ a {u} := by + rw [Kernel.map_apply' _ he _ (measurableSet_singleton _), h_preimage] + have h_mapg (b : β) (u : γ) : g.map e b {e u} = g b {u} := by + rw [Kernel.map_apply' _ he _ (measurableSet_singleton _), h_preimage] + have := Kernel.IsMarkovKernel.map ρ he + have := Kernel.IsMarkovKernel.map g he + have h_guess : guessProb μ (ρ.map e) κ (g.map e) = guessProb μ ρ κ g := by + simp_rw [guessProb_eq_sum] + refine Finset.sum_congr rfl fun x _ ↦ ?_ + rw [← e.sum_comp] + simp [h_mapρ, h_mapg] + have h_blind : blindGuessProb μ (ρ.map e) = blindGuessProb μ ρ := by + rw [blindGuessProb, blindGuessProb, ← e.iSup_comp] + simp_rw [comp_apply_singleton, h_mapρ] + exact ⟨ρ.map e, inferInstance, g.map e, inferInstance, by rw [h_guess, h_blind]⟩ + +omit [Fintype γ] in +/-- The guessing ratio of any finite alphabet `γ` is bounded by the operational maximal leakage, +whose definition only ranges over the alphabets `Fin n`. -/ +lemma guessProb_div_le_opMaxLeakageSum [Finite γ] [IsMarkovKernel ρ] [IsMarkovKernel κ] + [IsMarkovKernel g] : guessProb μ ρ κ g / blindGuessProb μ ρ ≤ opMaxLeakageSum μ κ := by + have := Fintype.ofFinite γ + obtain ⟨ρ', hρ', g', hg', h⟩ := exists_fin_guessProb_div_eq (μ := μ) (ρ := ρ) (κ := κ) (g := g) + rw [← h] + exact le_iSup_of_le _ <| le_iSup₂_of_le ρ' hρ' <| le_iSup₂_of_le g' hg' le_rfl + +end Relabel + +section Achievability + +variable [Finite α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + +/-- **Achievability half of Theorem 1.** Let `c` be the smallest positive mass of `μ` and `k` +an integer with `1 / k < c`. Take `U = (X, J)` with `J ∈ {0, …, k}`, where given `X = x` we +put mass `c / μ {x}` on the *signal* symbol `(x, 0)` and spread the rest evenly over the +*junk* symbols `(x, 1), …, (x, k)`. Every signal symbol has probability exactly `c` and every +junk symbol at most `1 / k < c`, so `max_u P_U(u) ≤ c`. Guessing the signal symbol of the input +most likely to have produced `y` succeeds with probability `c · ∑_y max_x κ x {y}`. +Together with the converse `guessProb_le`, this guessing problem is optimal: the supremum in +the operational definition is attained. -/ +lemma exists_guessProb_div_eq [IsProbabilityMeasure μ] [IsMarkovKernel κ] : + ∃ (n : ℕ) (ρ : Kernel α (Fin n)) (_ : IsMarkovKernel ρ) (g : Kernel β (Fin n)) + (_ : IsMarkovKernel g), guessProb μ ρ κ g / blindGuessProb μ ρ = maxLeakageSum μ κ := by + classical + have := Fintype.ofFinite α + -- The support of `μ`, its smallest mass `c`, and an integer `k` with `1 / k < c`. + set S := Finset.univ.filter fun x : α ↦ μ {x} ≠ 0 + have hS : S.Nonempty := by + by_contra h + have h0 : ∀ x, μ {x} = 0 := fun x ↦ by + by_contra hx + exact h ⟨x, by simpa [S] using hx⟩ + have := sum_measure_singleton (μ := μ) (s := Finset.univ) + simp [h0] at this + set c := S.inf' hS fun x ↦ μ {x} + have hc_le (x : α) (hx : μ {x} ≠ 0) : c ≤ μ {x} := Finset.inf'_le _ (by simpa [S] using hx) + have hc0 : c ≠ 0 := by + obtain ⟨x, hxS, hx⟩ := Finset.exists_mem_eq_inf' hS fun x ↦ μ {x} + have hcx : c = μ {x} := hx + rw [hcx] + simpa [S] using hxS + obtain ⟨x₀, hx₀⟩ := hS + have hctop : c ≠ ∞ := + ne_top_of_le_ne_top (measure_ne_top μ {x₀}) (hc_le x₀ (by simpa [S] using hx₀)) + obtain ⟨k, hk⟩ := ENNReal.exists_inv_nat_lt hc0 + have hk0 : (k : ℝ≥0∞) ≠ 0 := by + rintro h + simp [h] at hk + -- The randomization `ρ` producing `U = (X, J)`. + set t : α → ℝ≥0∞ := fun x ↦ if μ {x} = 0 then 1 else c / μ {x} + have ht_le (x : α) : t x ≤ 1 := by + by_cases hx : μ {x} = 0 + · simp [t, hx] + · simp only [t, hx, ite_false] + exact ENNReal.div_le_of_le_mul (by simpa using hc_le x hx) + have ht_mul (x : α) (hx : μ {x} ≠ 0) : t x * μ {x} = c := by + simp only [t, hx, ite_false] + exact ENNReal.div_mul_cancel hx (measure_ne_top μ _) + set w : α → α × Fin (k + 1) → ℝ≥0∞ := fun x p ↦ + if p.1 = x then (if p.2 = 0 then t x else (1 - t x) / k) else 0 + set ρ : Kernel α (α × Fin (k + 1)) := + Kernel.ofFunOfCountable fun x ↦ ∑ p, w x p • Measure.dirac p + have hρ (x : α) (p : α × Fin (k + 1)) : ρ x {p} = w x p := by + simp [ρ, Kernel.ofFunOfCountable, Measure.dirac_apply' _ (measurableSet_singleton p), + Set.indicator] + have hw_sum (x : α) : ∑ p, w x p = 1 := by + rw [Fintype.sum_prod_type_right] + simp only [w, Finset.sum_ite_eq', Finset.mem_univ, ite_true] + rw [Fin.sum_univ_succ] + simp only [ite_true, Fin.succ_ne_zero, ite_false, Finset.sum_const, Finset.card_univ, + Fintype.card_fin, nsmul_eq_mul] + rw [mul_comm, ENNReal.div_mul_cancel hk0 (ENNReal.natCast_ne_top k), + add_tsub_cancel_of_le (ht_le x)] + have : IsMarkovKernel ρ := ⟨fun x ↦ ⟨by + rw [← Finset.coe_univ, ← sum_measure_singleton] + simp_rw [hρ, hw_sum]⟩⟩ + -- The guessing rule: the signal symbol of a most likely input. + choose xs hxsS hxs_max using fun y : β ↦ S.exists_max_image (fun x ↦ κ x {y}) ⟨x₀, hx₀⟩ + have hxs (y : β) : μ {xs y} ≠ 0 := by simpa [S] using hxsS y + have hM (y : β) : (⨆ (x) (_ : μ {x} ≠ 0), κ x {y}) = κ (xs y) {y} := + le_antisymm (iSup₂_le fun x hx ↦ hxs_max y x (by simpa [S] using hx)) + (le_iSup₂ (f := fun x (_ : μ {x} ≠ 0) ↦ κ x {y}) (xs y) (hxs y)) + set g : Kernel β (α × Fin (k + 1)) := + Kernel.deterministic (fun y ↦ (xs y, 0)) (measurable_of_finite _) + have hg (y : β) : g y {(xs y, 0)} = 1 := by simp [g, Kernel.deterministic_apply] + -- `P_U(u) ≤ c` for every `u`. + have h_blind : blindGuessProb μ ρ ≤ c := by + refine iSup_le fun p ↦ ?_ + rw [comp_apply_singleton, Finset.sum_eq_single p.1 (fun x _ hx ↦ by simp [hρ, w, Ne.symm hx]) + (by simp)] + rw [hρ] + by_cases hp : p.2 = 0 + · by_cases hx : μ {p.1} = 0 + · simp [hx] + · simp [w, hp, ht_mul p.1 hx] + · simp only [w, ite_true, hp, ite_false] + calc (1 - t p.1) / k * μ {p.1} ≤ 1 / k * 1 := by + gcongr + · exact tsub_le_self + · exact prob_le_one + _ ≤ c := by simpa using hk.le + -- `P[U = Û] ≥ c · ∑_y max_x κ x {y}`. + have h_guess : maxLeakageSum μ κ * c ≤ guessProb μ ρ κ g := by + calc maxLeakageSum μ κ * c + = ∑ y, g y {(xs y, 0)} * κ (xs y) {y} * ρ (xs y) {(xs y, 0)} * μ {xs y} := by + rw [maxLeakageSum, Finset.sum_mul] + refine Finset.sum_congr rfl fun y _ ↦ ?_ + rw [hM, hg, hρ, mul_assoc _ (w _ _), mul_comm (w _ _), ← mul_assoc] + simp only [w, ite_true, ← ht_mul _ (hxs y)] + ring + _ ≤ ∑ y, ∑ x, ∑ u, g y {u} * κ x {y} * ρ x {u} * μ {x} := + Finset.sum_le_sum fun y _ ↦ (Finset.single_le_sum (fun _ _ ↦ zero_le) + (Finset.mem_univ (xs y))).trans' <| + Finset.single_le_sum (f := fun u ↦ g y {u} * κ (xs y) {y} * ρ (xs y) {u} * + μ {xs y}) (fun _ _ ↦ zero_le) (Finset.mem_univ _) + _ = ∑ x, ∑ y, ∑ u, g y {u} * κ x {y} * ρ x {u} * μ {x} := Finset.sum_comm + _ = guessProb μ ρ κ g := by + rw [guessProb_eq_sum] + exact Finset.sum_congr rfl fun x _ ↦ Finset.sum_comm + have h_ge : maxLeakageSum μ κ ≤ guessProb μ ρ κ g / blindGuessProb μ ρ := + calc maxLeakageSum μ κ = maxLeakageSum μ κ * c / c := + (ENNReal.mul_div_cancel_right hc0 hctop).symm + _ ≤ guessProb μ ρ κ g / c := ENNReal.div_le_div_right h_guess _ + _ ≤ guessProb μ ρ κ g / blindGuessProb μ ρ := ENNReal.div_le_div_left h_blind _ + -- The converse gives the reverse inequality, so the construction is optimal. + have h_eq : guessProb μ ρ κ g / blindGuessProb μ ρ = maxLeakageSum μ κ := + le_antisymm (ENNReal.div_le_of_le_mul guessProb_le) h_ge + obtain ⟨ρ', hρ', g', hg', h⟩ := exists_fin_guessProb_div_eq (μ := μ) (ρ := ρ) (κ := κ) (g := g) + exact ⟨_, ρ', hρ', g', hg', h.trans h_eq⟩ + +lemma maxLeakageSum_le_opMaxLeakageSum [IsProbabilityMeasure μ] [IsMarkovKernel κ] : + maxLeakageSum μ κ ≤ opMaxLeakageSum μ κ := by + obtain ⟨n, ρ, hρ, g, hg, h⟩ := exists_guessProb_div_eq (μ := μ) (κ := κ) + rw [← h] + exact le_iSup_of_le n <| le_iSup₂_of_le ρ hρ <| le_iSup₂_of_le g hg le_rfl + +end Achievability + +section MainTheorem + +variable [Finite α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + +/-- **Theorem 1 of Issa–Wagner–Kamath**, multiplicative form: for finite alphabets, the +operational maximal leakage equals `∑_y max_{x ∈ supp μ} κ x {y}`. -/ +theorem opMaxLeakageSum_eq_maxLeakageSum [IsProbabilityMeasure μ] [IsMarkovKernel κ] : + opMaxLeakageSum μ κ = maxLeakageSum μ κ := by + refine le_antisymm ?_ maxLeakageSum_le_opMaxLeakageSum + refine iSup_le fun n ↦ iSup₂_le fun ρ _ ↦ iSup₂_le fun g _ ↦ ?_ + exact ENNReal.div_le_of_le_mul guessProb_le + +/-- Theorem 1 of Issa–Wagner–Kamath, stated as the logarithm of the supremum of the guessing +ratios. See `isGreatest_log_guessRatio` for the supremum of the logarithms. -/ +theorem log_opMaxLeakageSum_eq_maxLeakage [IsProbabilityMeasure μ] [IsMarkovKernel κ] : + Real.log (opMaxLeakageSum μ κ).toReal = maxLeakage μ κ := by + rw [opMaxLeakageSum_eq_maxLeakageSum, maxLeakage] + +/-- **Theorem 1 of Issa–Wagner–Kamath**, in the form of their Definition 1: over all guessing +problems `U - X - Y - Û` on a common finite alphabet, the largest value of +`log (P[U = Û] / max_u P_U(u))` is `maxLeakage μ κ = log ∑_y max_{x ∈ supp μ} κ x {y}`, and it +is attained. Problems with `P[U = Û] = 0` contribute `-∞` in the paper and are excluded here. -/ +theorem isGreatest_log_guessRatio [IsProbabilityMeasure μ] [IsMarkovKernel κ] : + IsGreatest {r : ℝ | ∃ (n : ℕ) (ρ : Kernel α (Fin n)) (_ : IsMarkovKernel ρ) + (g : Kernel β (Fin n)) (_ : IsMarkovKernel g), guessProb μ ρ κ g ≠ 0 ∧ + r = Real.log (guessProb μ ρ κ g / blindGuessProb μ ρ).toReal} (maxLeakage μ κ) := by + have := Fintype.ofFinite α + obtain ⟨x₀, hx₀⟩ : ∃ x, μ {x} ≠ 0 := by + by_contra! h + have := sum_measure_singleton (μ := μ) (s := Finset.univ) + simp [h] at this + refine ⟨?_, ?_⟩ + · obtain ⟨n, ρ, hρ, g, hg, h⟩ := exists_guessProb_div_eq (μ := μ) (κ := κ) + refine ⟨n, ρ, hρ, g, hg, fun h0 ↦ ?_, by rw [h, maxLeakage]⟩ + rw [h0, ENNReal.zero_div] at h + exact absurd ((one_le_maxLeakageSum (κ := κ) hx₀).trans_eq h.symm) (by simp) + · rintro r ⟨n, ρ, hρ, g, hg, h0, rfl⟩ + have hle : guessProb μ ρ κ g / blindGuessProb μ ρ ≤ maxLeakageSum μ κ := + ENNReal.div_le_of_le_mul guessProb_le + have h_blind : blindGuessProb μ ρ ≠ ∞ := + ne_top_of_le_ne_top ENNReal.one_ne_top (iSup_le fun _ ↦ prob_le_one) + have hpos : 0 < (guessProb μ ρ κ g / blindGuessProb μ ρ).toReal := + ENNReal.toReal_pos (by simp [ENNReal.div_eq_zero_iff, h0, h_blind]) + (ne_top_of_le_ne_top maxLeakageSum_ne_top hle) + exact Real.log_le_log hpos (ENNReal.toReal_mono maxLeakageSum_ne_top hle) + +end MainTheorem + +end InformationTheory diff --git a/Statlib/Divergence/MaximalLeakage/Properties.lean b/Statlib/Divergence/MaximalLeakage/Properties.lean new file mode 100644 index 0000000..77b1d76 --- /dev/null +++ b/Statlib/Divergence/MaximalLeakage/Properties.lean @@ -0,0 +1,285 @@ +/- +Copyright (c) 2026 Kousha Kalantari. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kousha Kalantari +-/ +module + +public import Statlib.Divergence.MaximalLeakage.Basic +public import Mathlib.Probability.Kernel.CompProdEqIff +public import Mathlib.Probability.Kernel.Composition.MeasureComp +public import Mathlib.Probability.Kernel.Composition.Prod + +/-! +# Properties of maximal leakage + +This file proves the structural properties of maximal leakage `maxLeakage μ κ` on finite +alphabets listed in Lemma 1, Corollary 1 and Lemma 6 of Issa, Wagner and Kamath, +*An operational approach to information leakage*, IEEE Trans. Inf. Theory 66(3), 2020 +(arXiv:1807.07878). Each statement comes in a multiplicative form about `maxLeakageSum` and, +where natural, in logarithmic form about `maxLeakage`. + +Throughout, `X ∼ μ` is the channel input and `Y` is the output of `κ : Kernel α β`, so that +`Y ∼ κ ∘ₘ μ`. + +## Main statements + +* `maxLeakageSum_comp_le_comp`, `maxLeakage_comp_le_comp`: **data processing** for + pre-processing: for a Markov chain `X - Y - Z`, `L(X → Z) ≤ L(Y → Z)`. +* `maxLeakageSum_le_card_support_comp`, `maxLeakage_le_log_card_support_comp`: + `L(X → Y) ≤ log |supp Y|`. +* `maxLeakageSum_eq_one_iff`, `maxLeakage_eq_zero_iff`: `L(X → Y) = 0` iff all rows of the + channel on the support of `X` coincide. +* `maxLeakage_eq_zero_iff_compProd_eq_prod`: `L(X → Y) = 0` iff `X` and `Y` are independent, + i.e. iff the joint law `μ ⊗ₘ κ` is the product of its marginals. +* `maxLeakageSum_prod_le`, `maxLeakage_prod_le`: for the channel `κ ×ₖ η` producing two + conditionally independent outputs `Y` and `Z` of `X`, `L(X → (Y, Z)) ≤ L(X → Y) + L(X → Z)`. +* `maxLeakageSum_parallelComp`, `maxLeakage_parallelComp`: for independent pairs + `(X₁, Y₁)` and `(X₂, Y₂)`, `L((X₁, X₂) → (Y₁, Y₂)) = L(X₁ → Y₁) + L(X₂ → Y₂)`. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +/-! ### Auxiliary lemmas + +The lemmas in this section are not specific to maximal leakage and are candidates for a +`ForMathlib` file. -/ + +section ForMathlib + +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ : Measure α} {κ : Kernel α β} + +/-- Over a finite intermediate alphabet, a composite kernel is a finite mixture. -/ +lemma ProbabilityTheory.Kernel.comp_apply_eq_sum [Fintype β] [MeasurableSingletonClass β] + (η : Kernel β γ) (κ : Kernel α β) (a : α) {s : Set γ} (hs : MeasurableSet s) : + (η ∘ₖ κ) a s = ∑ b, η b s * κ a {b} := by + rw [Kernel.comp_apply' _ _ _ hs, lintegral_fintype] + +/-- If `a` is an atom of `μ` and `κ a` charges `s`, then so does `κ ∘ₘ μ`. -/ +lemma MeasureTheory.Measure.comp_apply_ne_zero {s : Set β} (hs : MeasurableSet s) {a : α} + (ha : μ {a} ≠ 0) (hκ : κ a s ≠ 0) : + (κ ∘ₘ μ) s ≠ 0 := by + have h_le : κ a s * μ {a} ≤ (κ ∘ₘ μ) s := + calc κ a s * μ {a} = ∫⁻ x in {a}, κ x s ∂μ := + (lintegral_singleton' (κ.measurable_coe hs) a).symm + _ ≤ ∫⁻ x, κ x s ∂μ := setLIntegral_le_lintegral _ _ + _ = (κ ∘ₘ μ) s := (Measure.bind_apply hs κ.aemeasurable).symm + exact (pos_iff_ne_zero.2 (mul_ne_zero hκ ha)).trans_le h_le |>.ne' + +end ForMathlib + +namespace InformationTheory + +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ : Measure α} {κ : Kernel α β} + +section PreProcessing + +variable [MeasurableSingletonClass β] + +/-- **Data processing** for maximal leakage under pre-processing, multiplicative form: for a +Markov chain `X - Y - Z` with `Y` the output of `κ` and `Z` the output of `η`, +`L(X → Z) ≤ L(Y → Z)`. -/ +lemma maxLeakageSum_comp_le_comp [Finite β] [Fintype γ] [MeasurableSingletonClass γ] + [IsMarkovKernel κ] (η : Kernel β γ) : + maxLeakageSum μ (η ∘ₖ κ) ≤ maxLeakageSum (κ ∘ₘ μ) η := by + have := Fintype.ofFinite β + refine Finset.sum_le_sum fun z _ ↦ iSup₂_le fun x hx ↦ ?_ + set M := ⨆ (y) (_ : (κ ∘ₘ μ) {y} ≠ 0), η y {z} + -- Every `y` reachable from an atom `x` of `μ` is an atom of `κ ∘ₘ μ`, so `η y {z} ≤ M`. + have h_le (y : β) : η y {z} * κ x {y} ≤ M * κ x {y} := by + obtain hy | hy := eq_or_ne (κ x {y}) 0 + · simp [hy] + exact mul_le_mul_left + (le_iSup₂ (f := fun y (_ : (κ ∘ₘ μ) {y} ≠ 0) ↦ η y {z}) y + (Measure.comp_apply_ne_zero (measurableSet_singleton y) hx hy)) _ + calc (η ∘ₖ κ) x {z} = ∑ y, η y {z} * κ x {y} := + Kernel.comp_apply_eq_sum _ _ _ (measurableSet_singleton z) + _ ≤ ∑ y, M * κ x {y} := Finset.sum_le_sum fun y _ ↦ h_le y + _ = M := by + rw [← Finset.mul_sum, sum_measure_singleton, Finset.coe_univ, measure_univ, mul_one] + +/-- **Data processing** for maximal leakage under pre-processing: for a Markov chain +`X - Y - Z` with `Y` the output of `κ` and `Z` the output of `η`, `L(X → Z) ≤ L(Y → Z)`. -/ +lemma maxLeakage_comp_le_comp [Finite β] [Fintype γ] [MeasurableSingletonClass γ] + [IsMarkovKernel κ] (η : Kernel β γ) [IsMarkovKernel η] {x : α} (hx : μ {x} ≠ 0) : + maxLeakage μ (η ∘ₖ κ) ≤ maxLeakage (κ ∘ₘ μ) η := by + refine Real.log_le_log (by linarith [one_le_toReal_maxLeakageSum (κ := η ∘ₖ κ) hx]) ?_ + exact (ENNReal.toReal_le_toReal maxLeakageSum_ne_top maxLeakageSum_ne_top).2 + (maxLeakageSum_comp_le_comp η) + +/-- Multiplicative form of `L(X → Y) ≤ log |supp Y|`: maximal leakage is at most the logarithm of +the number of output symbols that occur with positive probability. -/ +lemma maxLeakageSum_le_card_support_comp [Fintype β] [IsMarkovKernel κ] + [DecidablePred fun y : β ↦ (κ ∘ₘ μ) {y} ≠ 0] : + maxLeakageSum μ κ ≤ (Finset.univ.filter fun y : β ↦ (κ ∘ₘ μ) {y} ≠ 0).card := + calc maxLeakageSum μ κ = maxLeakageSum μ (Kernel.id ∘ₖ κ) := by rw [Kernel.id_comp] + _ ≤ maxLeakageSum (κ ∘ₘ μ) Kernel.id := maxLeakageSum_comp_le_comp _ + _ ≤ _ := maxLeakageSum_le_card_support + +/-- Maximal leakage is at most the logarithm of the size of the support of the output: +`L(X → Y) ≤ log |supp Y|`. -/ +lemma maxLeakage_le_log_card_support_comp [Fintype β] [IsMarkovKernel κ] + [DecidablePred fun y : β ↦ (κ ∘ₘ μ) {y} ≠ 0] {x : α} (hx : μ {x} ≠ 0) : + maxLeakage μ κ ≤ Real.log (Finset.univ.filter fun y : β ↦ (κ ∘ₘ μ) {y} ≠ 0).card := by + refine Real.log_le_log (by linarith [one_le_toReal_maxLeakageSum (κ := κ) hx]) ?_ + simpa using (ENNReal.toReal_le_toReal maxLeakageSum_ne_top (ENNReal.natCast_ne_top _)).2 + maxLeakageSum_le_card_support_comp + +end PreProcessing + +section ZeroLeakage + +variable [Fintype β] [MeasurableSingletonClass β] [IsMarkovKernel κ] + +/-- Multiplicative form of `maxLeakage_eq_zero_iff`: given an atom of `μ`, `∑_y max_x κ x {y} = 1` +iff all rows of the channel on the support of `μ` coincide. -/ +lemma maxLeakageSum_eq_one_iff {x₀ : α} (hx₀ : μ {x₀} ≠ 0) : + maxLeakageSum μ κ = 1 ↔ ∀ x x', μ {x} ≠ 0 → μ {x'} ≠ 0 → κ x = κ x' := by + set M : β → ℝ≥0∞ := fun y ↦ ⨆ (x) (_ : μ {x} ≠ 0), κ x {y} + have hM_ne_top (y : β) : M y ≠ ∞ := + ne_top_of_le_ne_top ENNReal.one_ne_top (iSup₂_le fun _ _ ↦ prob_le_one) + have h_le {x : α} (hx : μ {x} ≠ 0) (y : β) : κ x {y} ≤ M y := + le_iSup₂ (f := fun x (_ : μ {x} ≠ 0) ↦ κ x {y}) x hx + constructor + · intro h + -- A row on the support is dominated by `M` and has the same total mass `1 = ∑ y, M y`, + -- so it equals `M`. + have h_row {x : α} (hx : μ {x} ≠ 0) (y : β) : κ x {y} = M y := by + have h_sum : ∑ y, (κ x {y}).toReal = ∑ y, (M y).toReal := by + rw [← ENNReal.toReal_sum fun y _ ↦ measure_ne_top _ _, + ← ENNReal.toReal_sum fun y _ ↦ hM_ne_top y, sum_measure_singleton, Finset.coe_univ, + measure_univ] + exact congrArg ENNReal.toReal h.symm + refine (ENNReal.toReal_eq_toReal_iff' (measure_ne_top _ _) (hM_ne_top y)).1 ?_ + exact (Finset.sum_eq_sum_iff_of_le fun y _ ↦ ENNReal.toReal_mono (hM_ne_top y) (h_le hx y)).1 + h_sum y (Finset.mem_univ y) + intro x x' hx hx' + exact Measure.ext_of_singleton fun y ↦ (h_row hx y).trans (h_row hx' y).symm + · intro h + have hM (y : β) : M y = κ x₀ {y} := + le_antisymm (iSup₂_le fun x hx ↦ by rw [h x x₀ hx hx₀]) (h_le hx₀ y) + calc maxLeakageSum μ κ = ∑ y, κ x₀ {y} := Finset.sum_congr rfl fun y _ ↦ hM y + _ = 1 := by rw [sum_measure_singleton, Finset.coe_univ, measure_univ] + +/-- **Zero leakage**, characterization on atoms: `L(X → Y) = 0` iff the channel rows `κ x` +coincide for all atoms `x` of `μ`. This is independence of `X` and `Y` only when `μ` is purely +atomic; see `maxLeakage_eq_zero_iff_compProd_eq_prod` for the independence statement. If `μ` +has no atoms, both sides hold trivially. -/ +lemma maxLeakage_eq_zero_iff : + maxLeakage μ κ = 0 ↔ ∀ x x', μ {x} ≠ 0 → μ {x'} ≠ 0 → κ x = κ x' := by + by_cases h_atom : ∃ x, μ {x} ≠ 0 + · obtain ⟨x₀, hx₀⟩ := h_atom + rw [← maxLeakageSum_eq_one_iff hx₀, ← ENNReal.toReal_eq_one_iff] + have h_pos : 0 < (maxLeakageSum μ κ).toReal := by + linarith [one_le_toReal_maxLeakageSum (κ := κ) hx₀] + exact ⟨Real.eq_one_of_pos_of_log_eq_zero h_pos, fun h ↦ by rw [maxLeakage, h, Real.log_one]⟩ + · -- Without atoms both sides hold trivially. + push Not at h_atom + simp [maxLeakage, maxLeakageSum, h_atom] + +/-- **Zero leakage iff independence**: for a probability measure `μ` on a countable input +alphabet, `L(X → Y) = 0` iff `X` and `Y` are independent, i.e. iff the joint law `μ ⊗ₘ κ` is the +product of the marginals `μ` and `κ ∘ₘ μ`. -/ +lemma maxLeakage_eq_zero_iff_compProd_eq_prod [Countable α] [IsProbabilityMeasure μ] : + maxLeakage μ κ = 0 ↔ μ ⊗ₘ κ = μ.prod (κ ∘ₘ μ) := by + rw [maxLeakage_eq_zero_iff, ← Measure.compProd_const, Kernel.compProd_eq_iff, + Filter.EventuallyEq, ae_iff_of_countable] + simp only [Kernel.const_apply] + constructor + · intro h x hx + have h_ae : ∀ᵐ x' ∂μ, κ x' = Kernel.const α (κ x) x' := + ae_iff_of_countable.2 fun x' hx' ↦ h x' x hx' hx + rw [Measure.comp_congr h_ae, Measure.const_comp, measure_univ, one_smul] + · intro h x x' hx hx' + rw [h x hx, h x' hx'] + +end ZeroLeakage + +section Composition + +variable [Fintype β] [Fintype γ] + +/-- **Composition** for maximal leakage, multiplicative form: if `Y` and `Z` are conditionally +independent outputs of `X`, through the channel `κ ×ₖ η`, then +`L(X → (Y, Z)) ≤ L(X → Y) + L(X → Z)`. -/ +lemma maxLeakageSum_prod_le (η : Kernel α γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] : + maxLeakageSum μ (κ ×ₖ η) ≤ maxLeakageSum μ κ * maxLeakageSum μ η := by + calc maxLeakageSum μ (κ ×ₖ η) + = ∑ y, ∑ z, ⨆ (x) (_ : μ {x} ≠ 0), κ x {y} * η x {z} := by + simp_rw [maxLeakageSum, Fintype.sum_prod_type, ← Set.singleton_prod_singleton, + Kernel.prod_apply_prod] + _ ≤ ∑ y, ∑ z, (⨆ (x) (_ : μ {x} ≠ 0), κ x {y}) * ⨆ (x) (_ : μ {x} ≠ 0), η x {z} := by + refine Finset.sum_le_sum fun y _ ↦ Finset.sum_le_sum fun z _ ↦ ?_ + exact iSup₂_le fun x hx ↦ mul_le_mul' + (le_iSup₂ (f := fun x (_ : μ {x} ≠ 0) ↦ κ x {y}) x hx) + (le_iSup₂ (f := fun x (_ : μ {x} ≠ 0) ↦ η x {z}) x hx) + _ = maxLeakageSum μ κ * maxLeakageSum μ η := (Finset.sum_mul_sum _ _ _ _).symm + +/-- **Composition** for maximal leakage: if `Y` and `Z` are conditionally independent outputs of +`X`, through the channel `κ ×ₖ η`, then `L(X → (Y, Z)) ≤ L(X → Y) + L(X → Z)`. -/ +lemma maxLeakage_prod_le [MeasurableSingletonClass β] [MeasurableSingletonClass γ] + [IsMarkovKernel κ] (η : Kernel α γ) [IsMarkovKernel η] {x : α} (hx : μ {x} ≠ 0) : + maxLeakage μ (κ ×ₖ η) ≤ maxLeakage μ κ + maxLeakage μ η := by + have hκ := one_le_toReal_maxLeakageSum (κ := κ) hx + have hη := one_le_toReal_maxLeakageSum (κ := η) hx + rw [maxLeakage, maxLeakage, maxLeakage, ← Real.log_mul (by positivity) (by positivity), + ← ENNReal.toReal_mul] + refine Real.log_le_log (by linarith [one_le_toReal_maxLeakageSum (κ := κ ×ₖ η) hx]) ?_ + exact (ENNReal.toReal_le_toReal maxLeakageSum_ne_top + (ENNReal.mul_ne_top maxLeakageSum_ne_top maxLeakageSum_ne_top)).2 (maxLeakageSum_prod_le η) + +end Composition + +section Independent + +variable {α₁ α₂ β₁ β₂ : Type*} {mα₁ : MeasurableSpace α₁} {mα₂ : MeasurableSpace α₂} + {mβ₁ : MeasurableSpace β₁} {mβ₂ : MeasurableSpace β₂} [Fintype β₁] [Fintype β₂] + {μ₁ : Measure α₁} {μ₂ : Measure α₂} {κ₁ : Kernel α₁ β₁} {κ₂ : Kernel α₂ β₂} + +/-- **Additivity** of maximal leakage for independent pairs, multiplicative form: if `X₁ ∼ μ₁` and +`X₂ ∼ μ₂` are independent and fed through the independent channels `κ₁` and `κ₂`, then +`L((X₁, X₂) → (Y₁, Y₂)) = L(X₁ → Y₁) + L(X₂ → Y₂)`. -/ +lemma maxLeakageSum_parallelComp [SFinite μ₂] [IsSFiniteKernel κ₁] [IsSFiniteKernel κ₂] : + maxLeakageSum (μ₁.prod μ₂) (κ₁ ∥ₖ κ₂) = maxLeakageSum μ₁ κ₁ * maxLeakageSum μ₂ κ₂ := by + -- The maximum over the product support of a product of rows is the product of the maxima. + have h_sup (y₁ : β₁) (y₂ : β₂) : + ⨆ (x) (_ : (μ₁.prod μ₂) {x} ≠ 0), (κ₁ ∥ₖ κ₂) x {(y₁, y₂)} = + (⨆ (x₁) (_ : μ₁ {x₁} ≠ 0), κ₁ x₁ {y₁}) * ⨆ (x₂) (_ : μ₂ {x₂} ≠ 0), κ₂ x₂ {y₂} := by + simp_rw [ENNReal.iSup_mul, ENNReal.mul_iSup] + refine le_antisymm (iSup₂_le fun ⟨x₁, x₂⟩ hx ↦ ?_) + (iSup₂_le fun x₁ hx₁ ↦ iSup₂_le fun x₂ hx₂ ↦ ?_) + · rw [← Set.singleton_prod_singleton, Measure.prod_prod, mul_ne_zero_iff] at hx + rw [← Set.singleton_prod_singleton, Kernel.parallelComp_apply_prod] + exact le_iSup₂_of_le x₁ hx.1 (le_iSup₂_of_le x₂ hx.2 le_rfl) + · have hx : (μ₁.prod μ₂) {(x₁, x₂)} ≠ 0 := by + rw [← Set.singleton_prod_singleton, Measure.prod_prod] + exact mul_ne_zero hx₁ hx₂ + refine le_iSup₂_of_le (f := fun x (_ : (μ₁.prod μ₂) {x} ≠ 0) ↦ (κ₁ ∥ₖ κ₂) x {(y₁, y₂)}) + (x₁, x₂) hx ?_ + rw [← Set.singleton_prod_singleton, Kernel.parallelComp_apply_prod] + calc maxLeakageSum (μ₁.prod μ₂) (κ₁ ∥ₖ κ₂) + = ∑ y₁, ∑ y₂, (⨆ (x₁) (_ : μ₁ {x₁} ≠ 0), κ₁ x₁ {y₁}) * + ⨆ (x₂) (_ : μ₂ {x₂} ≠ 0), κ₂ x₂ {y₂} := by + simp_rw [maxLeakageSum, Fintype.sum_prod_type, h_sup] + _ = maxLeakageSum μ₁ κ₁ * maxLeakageSum μ₂ κ₂ := (Finset.sum_mul_sum _ _ _ _).symm + +/-- **Additivity** of maximal leakage for independent pairs: if `X₁ ∼ μ₁` and `X₂ ∼ μ₂` are +independent and fed through the independent channels `κ₁` and `κ₂`, then +`L((X₁, X₂) → (Y₁, Y₂)) = L(X₁ → Y₁) + L(X₂ → Y₂)`. -/ +lemma maxLeakage_parallelComp [MeasurableSingletonClass β₁] [MeasurableSingletonClass β₂] + [SFinite μ₂] [IsMarkovKernel κ₁] [IsMarkovKernel κ₂] {x₁ : α₁} (hx₁ : μ₁ {x₁} ≠ 0) + {x₂ : α₂} (hx₂ : μ₂ {x₂} ≠ 0) : + maxLeakage (μ₁.prod μ₂) (κ₁ ∥ₖ κ₂) = maxLeakage μ₁ κ₁ + maxLeakage μ₂ κ₂ := by + have h₁ := one_le_toReal_maxLeakageSum (κ := κ₁) hx₁ + have h₂ := one_le_toReal_maxLeakageSum (κ := κ₂) hx₂ + rw [maxLeakage, maxLeakageSum_parallelComp, ENNReal.toReal_mul, + Real.log_mul (by positivity) (by positivity), maxLeakage, maxLeakage] + +end Independent + +end InformationTheory From b5e1b8f35d7fdc2d5d2b900dd6bc669429661351 Mon Sep 17 00:00:00 2001 From: Kousha Kalantari <25445970+KoushaKalantari@users.noreply.github.com> Date: Fri, 13 Nov 2026 10:08:38 -0800 Subject: [PATCH 2/2] =?UTF-8?q?feat(Privacy):=20differential=20privacy=20u?= =?UTF-8?q?nder=20Hamming=20distortion=20(Kalantari=E2=80=93Sankar?= =?UTF-8?q?=E2=80=93Sarwate)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- Statlib.lean | 1 + Statlib/Privacy/DPHamming/Basic.lean | 754 +++++++++++++++++++++++++++ 2 files changed, 755 insertions(+) create mode 100644 Statlib/Privacy/DPHamming/Basic.lean diff --git a/Statlib.lean b/Statlib.lean index 253c245..d325e02 100644 --- a/Statlib.lean +++ b/Statlib.lean @@ -142,6 +142,7 @@ import Statlib.ForMathlib.Probability.StrongLaw import Statlib.ForMathlib.Topology.Order.MonotoneConvergence import Statlib.Inference.Inference import Statlib.Inference.QMD +import Statlib.Privacy.DPHamming.Basic import Statlib.Testing.Binary import Statlib.Testing.BinaryRenyi import Statlib.Testing.ChangeMeasure diff --git a/Statlib/Privacy/DPHamming/Basic.lean b/Statlib/Privacy/DPHamming/Basic.lean new file mode 100644 index 0000000..db31c75 --- /dev/null +++ b/Statlib/Privacy/DPHamming/Basic.lean @@ -0,0 +1,754 @@ +/- +Copyright (c) 2026 Kousha Kalantari. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kousha Kalantari +-/ +module + +public import Statlib.Divergence.MaximalLeakage.MutualInfo +public import Mathlib.Algebra.Order.Rearrangement +public import Mathlib.Analysis.Convex.Basic +public import Mathlib.Analysis.Convex.Hull +public import Mathlib.Analysis.SpecialFunctions.Log.Basic +public import Mathlib.Data.Fin.Tuple.Sort +public import Mathlib.LinearAlgebra.Matrix.Stochastic + +/-! +# Privacy-utility tradeoffs under differential privacy and Hamming distortion + +This file formalizes the main results of K. Kalantari, L. Sankar and A. D. Sarwate, *Robust +privacy-utility tradeoffs under differential privacy and Hamming distortion*, IEEE Trans. Inf. +Forensics Security 13(11), 2018 ([arXiv:1601.06426](https://arxiv.org/abs/1601.06426)). + +A data value `X` from a finite alphabet `α` of size `M` is released through a mechanism `Q`, a +row-stochastic matrix with `Q x y` the probability of releasing `y` when the data is `x`. Privacy +is measured by (local) differential privacy: `Q` is `ε`-DP if `Q(y | x₁) ≤ e^ε Q(y | x₂)` for all +`x₁, x₂, y`. Utility is measured by the expected Hamming distortion +`E[1{X ≠ X̂}] = ∑_x P(x) (1 - Q(x | x))`, required to be at most `D` for *every* law `P` in a source +set `S` known to the publisher. The optimal leakage `ε*_DP(S, D)` is the least `ε` achieved by such +a mechanism. + +Source laws are vectors `P : α → ℝ` (in the probability simplex where needed) and mechanisms are +matrices in `Matrix.rowStochastic ℝ α`; the reduction step of Lemma 3 +(`mem_achievableDP_of_injective`) shows that this square output alphabet loses nothing. +Logarithms are natural. + +## Main definitions + +* `IsLocalDP Q ε`: `Q` is `ε`-differentially private (Definition 3). +* `hammingDistortion P Q`: the expected Hamming distortion. +* `validMechanisms S D`: the `(S, D)`-valid mechanisms (Definition 2). +* `achievableDP S D`, `optimalDP S D`: the privacy levels achieved by `(S, D)`-valid mechanisms, + and their infimum `ε*_DP(S, D)` in `EReal`, which is `⊤` when the set is empty (Definition 4). +* `IsClassI S`: the convex hull of `S` contains the uniform law (Definition 1, Class I). +* `symmMechanism D`: the symmetric mechanism `Q_D` of (7) (randomized response). +* `distortionThreshold S k`: the thresholds `D^(k)` of (9), for source sets on `Fin M`. + +## Main statements + +* `optimalDP_of_isClassI`: **Theorem 1**, for a Class I source set and `0 < D`, + `ε*_DP(S, D) = log ((M - 1)(1 - D) / D)` if `D < (M - 1) / M` and `0` otherwise. +* `isLeast_achievableDP_of_lt`: the symmetric mechanism is optimal whenever the convex hull of `S` + contains a law with every mass `> D / (M - 1)`; this contains the first cases of Theorems 1 and 2. +* `isLeast_achievableDP_of_lt_distortionThreshold_one`: **Theorem 2(b)**, case `0 < D < D^(1)`. +* `notMem_validMechanisms_of_lt_distortionThreshold`: **Theorem 2(a)**. +* `isLeast_achievableDP_zero_iff_distortionThreshold_le`: **Lemma 7**, and the case + `D ≥ D^(M-1)` of Theorem 2(b). +* `toReal_mutualInfo_compProd_le_of_isLocalDP`: DP leakage bounds MI leakage, through + `maxLeakage_le_of_isLocalDP` (maximal leakage is at most `ε`). + +## Correspondence with the paper + +* Definitions 1–4: `IsClassI`, `validMechanisms`, `IsLocalDP`, `achievableDP` / `optimalDP`. +* Lemma 1: `convex_setOf_isLocalDP` (convexity of the sublevel sets `{Q | ε_DP(Q) ≤ ε}`). +* Lemma 2: `validMechanisms_convexHull`, `achievableDP_convexHull`. +* Lemma 3, reduction step (any achievable `ε` is achieved by a square mechanism, rather than the + existence of an optimal one): `exists_square_mechanism`, `mem_achievableDP_of_injective`. +* Lemma 4, reduction step (any achievable `ε` is achieved by a mechanism with sorted distortions, + rather than the existence of such an optimal one): `exists_monotone_distortion`. +* Theorem 1: `isLeast_achievableDP_of_isClassI`, `isLeast_achievableDP_zero`, + `optimalDP_of_isClassI`. +* Theorem 2(a) and Lemma 8: `notMem_validMechanisms_of_lt_distortionThreshold`. +* Theorem 2(b), first case: `isLeast_achievableDP_of_lt_distortionThreshold_one`, with converse + `card_sub_one_mul_le_exp_mul` (eq. (46)) and achievability `isLocalDP_symmMechanism` (eq. (47)). +* Theorem 2(b), last case, and Lemma 7: `isLeast_achievableDP_zero_iff_distortionThreshold_le`, + and the general form `isLeast_achievableDP_zero_iff` for laws with a common mode. +* Lemma 10: `sum_mul_le_sum_mul_of_forall_ne_le`. +* Section III-A, "DP leakage is an upper bound on MI leakage": + `toReal_mutualInfo_compProd_le_of_isLocalDP`. + +## Implementation notes + +* A statement `ε*_DP(S, D) = v` of the paper is formalized as `IsLeast (achievableDP S D) v`: some + `(S, D)`-valid mechanism is `v`-DP and none is `ε`-DP for `ε < v`. This implies + `optimalDP S D = v` (`optimalDP_eq_of_isLeast`). The infimum `optimalDP` is taken in `EReal` so + that an infeasible regime (no valid mechanism with finite leakage, e.g. `D = 0` on an alphabet + with at least two symbols when `S` contains a full-support law) gives `⊤` rather than a junk + value. +* Class II source sets are taken in the normalized form of Remark 1: laws on `Fin M` that are + nonincreasing (`Antitone`). The Class II results do not need the hypothesis "not Class I" of + Definition 1, so they are stated without it. The thresholds `D^(k)` are suprema over `S` + (maxima in the paper), which is why `S` is assumed nonempty. +* The converse `card_sub_one_mul_le_exp_mul` is proved directly, without the coloring arguments + of Lemma 9. + +## Not formalized + +* Theorem 2(b) for `D^(1) ≤ D < D^(M-1)` (the linear programs (10)–(11) and Lemma 9) and + Theorem 3 with Corollary 1 (Class III bounds built on them). +* Lemmas 5 and 6 on the optimal mutual-information leakage. +-/ + +@[expose] public section + +open Finset Real + +namespace InformationTheory + +variable {α β : Type*} + +/-! ### Definitions -/ + +/-- **Local differential privacy** (Definition 3 of Kalantari–Sankar–Sarwate): a mechanism `Q`, +where `Q x y` is the probability of releasing `y` when the data is `x`, is `ε`-differentially +private if `Q(y | x₁) ≤ e^ε Q(y | x₂)` for all inputs `x₁, x₂` and outputs `y`. -/ +def IsLocalDP (Q : α → β → ℝ) (ε : ℝ) : Prop := + ∀ x₁ x₂ y, Q x₁ y ≤ exp ε * Q x₂ y + +section LocalDP + +variable {Q : α → β → ℝ} {ε : ℝ} + +/-- An `ε`-differentially private mechanism is `ε'`-differentially private for every `ε' ≥ ε`. -/ +lemma IsLocalDP.mono (hQ : ∀ x y, 0 ≤ Q x y) {ε' : ℝ} (h : IsLocalDP Q ε) + (hεε' : ε ≤ ε') : IsLocalDP Q ε' := fun x₁ x₂ y ↦ + (h x₁ x₂ y).trans (mul_le_mul_of_nonneg_right (exp_le_exp.2 hεε') (hQ x₂ y)) + +/-- **Lemma 1** (quasi-convexity of the leakage): for every `ε`, the set of `ε`-differentially +private mechanisms is convex. This is the sublevel-set characterization of the quasi-convexity of +`Q ↦ ε_DP(Q)` used in the paper. -/ +theorem convex_setOf_isLocalDP (ε : ℝ) : Convex ℝ {Q : α → β → ℝ | IsLocalDP Q ε} := by + intro Q₁ h₁ Q₂ h₂ a b ha hb _ x₁ x₂ y + simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul] + calc a * Q₁ x₁ y + b * Q₂ x₁ y ≤ a * (exp ε * Q₁ x₂ y) + b * (exp ε * Q₂ x₂ y) := by + gcongr + · exact h₁ x₁ x₂ y + · exact h₂ x₁ x₂ y + _ = exp ε * (a * Q₁ x₂ y + b * Q₂ x₂ y) := by ring + +end LocalDP + +section Definitions + +variable [Fintype α] [DecidableEq α] + +/-- The expected Hamming distortion `E[d(X, X̂)] = ∑_{x, x̂} P(x) Q(x̂ | x) 1{x ≠ x̂}` of a +mechanism `Q` whose output alphabet is the input alphabet, for a source with law `P`. -/ +def hammingDistortion (P : α → ℝ) (Q : Matrix α α ℝ) : ℝ := + ∑ x, ∑ y, P x * Q x y * if x = y then 0 else 1 + +/-- The `(S, D)`-valid mechanisms (Definition 2): the row-stochastic matrices whose expected +Hamming distortion is at most `D` for every source law `P ∈ S`. -/ +def validMechanisms (S : Set (α → ℝ)) (D : ℝ) : Set (Matrix α α ℝ) := + {Q | Q ∈ Matrix.rowStochastic ℝ α ∧ ∀ P ∈ S, hammingDistortion P Q ≤ D} + +/-- The privacy levels `ε` for which some `(S, D)`-valid mechanism is `ε`-differentially +private. This set is empty when no `(S, D)`-valid mechanism has finite DP leakage (for instance +for `D = 0`, an alphabet with at least two symbols and `S` containing a full-support law, where +only the identity is valid and it is not `ε`-DP for any finite `ε`); otherwise the +optimal leakage `ε*_DP(S, D)` of Definition 4 is its least element when it has one. -/ +def achievableDP (S : Set (α → ℝ)) (D : ℝ) : Set ℝ := + {ε | ∃ Q ∈ validMechanisms S D, IsLocalDP Q ε} + +/-- The optimal differential privacy leakage `ε*_DP(S, D) ∈ [-∞, ∞]` (Definition 4): the infimum +of the privacy levels achieved by `(S, D)`-valid mechanisms, in `EReal`. It is `⊤` (infinite +leakage) when no `(S, D)`-valid mechanism has finite DP leakage (`optimalDP_eq_top`). The main +results below show that the infimum is attained (`IsLeast (achievableDP S D) _`), which pins down +its value (`optimalDP_eq_of_isLeast`). -/ +noncomputable def optimalDP (S : Set (α → ℝ)) (D : ℝ) : EReal := + ⨅ ε ∈ achievableDP S D, (ε : EReal) + +omit [DecidableEq α] in +/-- A source set `S` is of **Class I** (Definition 1) if its convex hull contains the uniform +distribution. -/ +def IsClassI (S : Set (α → ℝ)) : Prop := + (fun _ ↦ (Fintype.card α : ℝ)⁻¹) ∈ convexHull ℝ S + +/-- The symmetric mechanism `Q_D` of (7) (randomized response): keep the input with probability +`1 - D`, otherwise release one of the other `M - 1` symbols uniformly at random. -/ +noncomputable def symmMechanism (D : ℝ) : Matrix α α ℝ := + fun x y ↦ if x = y then 1 - D else D / (Fintype.card α - 1) + +end Definitions + +/-! ### Basic properties -/ + +section Basic + +variable [Fintype α] [DecidableEq α] {S T : Set (α → ℝ)} {D ε : ℝ} {Q : Matrix α α ℝ} + +/-- For a row-stochastic `Q`, the expected Hamming distortion is `∑_x P(x) (1 - Q(x | x))`. -/ +lemma hammingDistortion_eq (hQ : Q ∈ Matrix.rowStochastic ℝ α) (P : α → ℝ) : + hammingDistortion P Q = ∑ x, P x * (1 - Q x x) := by + refine sum_congr rfl fun x _ ↦ ?_ + have h (y : α) : P x * Q x y * (if x = y then 0 else 1) = + P x * (Q x y - if x = y then Q x y else 0) := by + split_ifs <;> ring + simp_rw [h, ← mul_sum, sum_sub_distrib, sum_ite_eq, Matrix.sum_row_of_mem_rowStochastic hQ] + simp + +/-- The privacy level of a differentially private mechanism is nonnegative. -/ +lemma IsLocalDP.nonneg [Nonempty α] (hQ : Q ∈ Matrix.rowStochastic ℝ α) (h : IsLocalDP Q ε) : + 0 ≤ ε := by + by_contra! hε + obtain ⟨x⟩ := ‹Nonempty α› + have h0 (y : α) : Q x y ≤ 0 := by + nlinarith [h x x y, exp_lt_one_iff.2 hε, + Matrix.nonneg_of_mem_rowStochastic hQ (i := x) (j := y)] + linarith [Matrix.sum_row_of_mem_rowStochastic hQ x, sum_nonpos fun y (_ : y ∈ univ) ↦ h0 y] + +/-- The expected Hamming distortion is linear in the source law. -/ +lemma isLinearMap_hammingDistortion (Q : Matrix α α ℝ) : + IsLinearMap ℝ fun P : α → ℝ ↦ hammingDistortion P Q where + map_add P₁ P₂ := by simp only [hammingDistortion, Pi.add_apply, add_mul, sum_add_distrib] + map_smul c P := by simp only [hammingDistortion, Pi.smul_apply, smul_eq_mul, mul_sum, mul_assoc] + +/-- **Lemma 2**: a mechanism is valid for a source set iff it is valid for its convex hull. -/ +theorem validMechanisms_convexHull : validMechanisms (convexHull ℝ S) D = validMechanisms S D := by + ext Q + refine ⟨fun h ↦ ⟨h.1, fun P hP ↦ h.2 P (subset_convexHull ℝ S hP)⟩, fun h ↦ ⟨h.1, ?_⟩⟩ + exact (convex_halfSpace_le (isLinearMap_hammingDistortion Q) D).convexHull_subset_iff.2 h.2 + +/-- **Lemma 2**: the minimal leakage of a source set is that of its convex hull. -/ +theorem achievableDP_convexHull : achievableDP (convexHull ℝ S) D = achievableDP S D := by + simp [achievableDP, validMechanisms_convexHull] + +/-- If the minimum of the achievable privacy levels is `v`, then `ε*_DP(S, D) = v`. -/ +lemma optimalDP_eq_of_isLeast {v : ℝ} (h : IsLeast (achievableDP S D) v) : optimalDP S D = v := + le_antisymm (iInf₂_le v h.1) (le_iInf₂ fun _ hε ↦ EReal.coe_le_coe_iff.2 (h.2 hε)) + +/-- If no `(S, D)`-valid mechanism is `ε`-differentially private for any real `ε`, then +`ε*_DP(S, D) = ∞`. -/ +lemma optimalDP_eq_top (h : achievableDP S D = ∅) : optimalDP S D = ⊤ := by + simp [optimalDP, h] + +/-- More knowledge about the source (a smaller source set) can only decrease the leakage. -/ +lemma achievableDP_anti (h : S ⊆ T) : achievableDP T D ⊆ achievableDP S D := + fun _ ⟨Q, hQ, hε⟩ ↦ ⟨Q, ⟨hQ.1, fun P hP ↦ hQ.2 P (h hP)⟩, hε⟩ + +end Basic + +/-! ### The symmetric mechanism -/ + +section Symmetric + +variable [Fintype α] [DecidableEq α] [Nontrivial α] {D : ℝ} + +lemma sum_symmMechanism (D : ℝ) (x : α) : ∑ y, symmMechanism D x y = 1 := by + have hM : (1 : ℝ) < Fintype.card α := by exact_mod_cast Fintype.one_lt_card + have h (y : α) : symmMechanism D x y = D / (Fintype.card α - 1) + + if x = y then 1 - D - D / (Fintype.card α - 1) else 0 := by + unfold symmMechanism; split_ifs <;> ring + simp_rw [h, sum_add_distrib, sum_ite_eq, sum_const, card_univ, nsmul_eq_mul] + simp only [mem_univ, ↓reduceIte] + field_simp + ring + +lemma symmMechanism_mem_rowStochastic (hD₀ : 0 ≤ D) (hD₁ : D ≤ 1) : + (symmMechanism D : Matrix α α ℝ) ∈ Matrix.rowStochastic ℝ α := by + have hM : (1 : ℝ) < Fintype.card α := by exact_mod_cast Fintype.one_lt_card + refine Matrix.mem_rowStochastic_iff_sum.2 ⟨fun x y ↦ ?_, sum_symmMechanism D⟩ + unfold symmMechanism + split_ifs + · linarith + · exact div_nonneg hD₀ (by linarith) + +/-- The symmetric mechanism has expected Hamming distortion exactly `D` for every source law. -/ +lemma hammingDistortion_symmMechanism (hD₀ : 0 ≤ D) (hD₁ : D ≤ 1) {P : α → ℝ} + (hP : ∑ x, P x = 1) : hammingDistortion P (symmMechanism D) = D := by + rw [hammingDistortion_eq (symmMechanism_mem_rowStochastic hD₀ hD₁)] + simp [symmMechanism, ← sum_mul, hP] + +/-- The symmetric mechanism `Q_D` is `log ((M - 1)(1 - D) / D)`-differentially private for +`0 < D ≤ (M - 1) / M`. -/ +lemma isLocalDP_symmMechanism (hD₀ : 0 < D) (hD : D ≤ (Fintype.card α - 1) / Fintype.card α) : + IsLocalDP (symmMechanism D : Matrix α α ℝ) (log ((Fintype.card α - 1) * (1 - D) / D)) := by + set M : ℝ := (Fintype.card α : ℝ) + have hM : 1 < M := by simp only [M]; exact_mod_cast Fintype.one_lt_card (α := α) + have hMD : M * D ≤ M - 1 := by rwa [le_div_iff₀ (by linarith), mul_comm] at hD + set w := D / (M - 1) + set c := (M - 1) * (1 - D) / D + have hw : 0 ≤ w := div_nonneg hD₀.le (by linarith) + have hcw : c * w = 1 - D := by simp only [c, w]; field_simp + have hwD : w ≤ 1 - D := by rw [div_le_iff₀ (by linarith)]; nlinarith + have hc : 1 ≤ c := by rw [le_div_iff₀ hD₀]; nlinarith + intro x₁ x₂ y + rw [exp_log (by linarith)] + unfold symmMechanism + split_ifs <;> nlinarith + +end Symmetric + +/-! ### The converse -/ + +section Converse + +/-- **Lemma 10** (a rearrangement bound). Let `∑ a = ∑ a'`, let `b` be smallest at `i₀`, and let +`a' i ≤ a i` for every `i ≠ i₀`. Then `∑ a' b ≤ ∑ a b`. The paper states this for `b` sorted +nondecreasingly and `i₀` the first index, and also assumes `a'_{i₀} ≥ a_{i₀}`, which follows from +the other hypotheses; the bounds `0 ≤ a, a', b ≤ 1` of the paper are not needed. -/ +lemma sum_mul_le_sum_mul_of_forall_ne_le {ι : Type*} [Fintype ι] {a a' b : ι → ℝ} {i₀ : ι} + (hsum : ∑ i, a i = ∑ i, a' i) (hb : ∀ i, b i₀ ≤ b i) (h : ∀ i ≠ i₀, a' i ≤ a i) : + ∑ i, a' i * b i ≤ ∑ i, a i * b i := by + have key : ∑ i, (a i - a' i) * b i₀ ≤ ∑ i, (a i - a' i) * b i := sum_le_sum fun i _ ↦ by + rcases eq_or_ne i i₀ with rfl | hi + · exact le_rfl + · exact mul_le_mul_of_nonneg_left (hb i) (sub_nonneg.2 (h i hi)) + rw [← sum_mul, sum_sub_distrib, hsum, sub_self, zero_mul] at key + simpa [sub_mul, sum_sub_distrib] using key + +variable [Fintype α] [DecidableEq α] [Nontrivial α] {D ε : ℝ} {Q : Matrix α α ℝ} + +/-- **Converse bound** behind Theorems 1 and 2(b). Let `Q` be an `ε`-differentially private +mechanism with expected Hamming distortion at most `D > 0` under a source law `P` that puts mass +more than `D / (M - 1)` on every symbol. Then `(M - 1)(1 - D) ≤ e^ε D`, i.e. +`ε ≥ log ((M - 1)(1 - D) / D)`. + +The proof follows Section V-F of the paper but needs neither Lemma 4 nor the structural Lemma 9: +the row `i` of smallest distortion `D_i` already satisfies `e^ε D_i ≥ ∑_{y ≠ i} (1 - D_y)`, and +comparing `P` with the law `(1 - D, D / (M - 1), …, D / (M - 1))` as in Lemma 10 and (45) gives +`(1 - D) D_i + D / (M - 1) ∑_{y ≠ i} D_y ≤ D`. -/ +theorem card_sub_one_mul_le_exp_mul (hQ : Q ∈ Matrix.rowStochastic ℝ α) (hε : IsLocalDP Q ε) + {P : α → ℝ} (hP : ∑ x, P x = 1) (hD : 0 < D) (hPD : ∀ x, D / (Fintype.card α - 1) < P x) + (hdist : hammingDistortion P Q ≤ D) : + (Fintype.card α - 1) * (1 - D) ≤ exp ε * D := by + set M : ℝ := (Fintype.card α : ℝ) + have hM : 1 < M := by simp only [M]; exact_mod_cast Fintype.one_lt_card (α := α) + set w := D / (M - 1) with hw_def + have hw : 0 ≤ w := div_nonneg hD.le (by linarith) + have hMw : (M - 1) * w = D := by rw [hw_def]; field_simp + have hQ₀ (x y : α) : 0 ≤ Q x y := Matrix.nonneg_of_mem_rowStochastic hQ + have hrow := Matrix.sum_row_of_mem_rowStochastic hQ + -- The row `i` with the largest diagonal entry, i.e. the smallest distortion `D_i`. + obtain ⟨i, hi⟩ := Finite.exists_max fun x ↦ Q x x + set q := Q i i + set s := ∑ y ∈ univ.erase i, Q y y + -- Each `Q(y | y)` with `y ≠ i` is at most `e^ε Q(y | i)`, and these sum to `e^ε (1 - q)`. + have hrow_i : ∑ y ∈ univ.erase i, Q i y = 1 - q := by + rw [← hrow i, ← add_sum_erase _ _ (mem_univ i)]; ring + have hs : s ≤ exp ε * (1 - q) := by + rw [← hrow_i, mul_sum]; exact sum_le_sum fun y _ ↦ hε y i y + -- The distortion constraint `∑ P(x) Q(x | x) ≥ 1 - D`, split along the weights `P - w ≥ 0`. + rw [hammingDistortion_eq hQ] at hdist + have hdist' : 1 - D ≤ ∑ x, P x * Q x x := by + simp only [mul_sub, mul_one, sum_sub_distrib, hP] at hdist; linarith + have hsplit : ∑ x, P x * Q x x = ∑ x, (P x - w) * Q x x + w * (q + s) := by + rw [show q + s = ∑ x, Q x x from add_sum_erase _ (fun x ↦ Q x x) (mem_univ i), mul_sum, + ← sum_add_distrib] + exact sum_congr rfl fun x _ ↦ by ring + have hle : ∑ x, (P x - w) * Q x x ≤ ∑ x, (P x - w) * q := + sum_le_sum fun x _ ↦ mul_le_mul_of_nonneg_left (hi x) (sub_nonneg.2 (hPD x).le) + have hsum : ∑ x, (P x - w) * q = (1 - M * w) * q := by + rw [← sum_mul, sum_sub_distrib, hP]; simp [M] + have hMwq : (M - 1) * w * q = D * q := by rw [hMw] + rcases (Matrix.le_one_of_mem_rowStochastic hQ (i := i) (j := i)).lt_or_eq with hq | hq + · have h1 : (1 - D) * (1 - q) ≤ w * exp ε * (1 - q) := by + nlinarith [mul_le_mul_of_nonneg_left hs hw] + have h2 : 1 - D ≤ w * exp ε := le_of_mul_le_mul_right h1 (by linarith) + calc (M - 1) * (1 - D) ≤ (M - 1) * (w * exp ε) := by gcongr + _ = exp ε * D := by rw [← hMw]; ring + · -- If `Q(i | i) = 1`, every other diagonal entry vanishes and `P` cannot meet the constraint. + exfalso + replace hq : q = 1 := hq + have hs₀ : s = 0 := + le_antisymm (by simpa [q, hq] using hs) (sum_nonneg fun y _ ↦ hQ₀ y y) + obtain ⟨j, hj⟩ := exists_ne i + have hj₀ : Q j j = 0 := + (sum_eq_zero_iff_of_nonneg fun y _ ↦ hQ₀ y y).1 hs₀ j (mem_erase.2 ⟨hj, mem_univ j⟩) + have hlt : ∑ x, (P x - w) * Q x x < ∑ x, (P x - w) * q := by + refine sum_lt_sum (fun x _ ↦ mul_le_mul_of_nonneg_left (hi x) (sub_nonneg.2 (hPD x).le)) + ⟨j, mem_univ j, ?_⟩ + rw [hj₀, hq, mul_zero, mul_one] + linarith [hPD j] + simp only [hq, hs₀, mul_one, add_zero] at hsum hMwq hlt hsplit + linarith + +end Converse + +/-! ### Optimal leakage: Theorem 1 -/ + +section Optimal + +variable [Fintype α] [DecidableEq α] {S : Set (α → ℝ)} {D : ℝ} + +/-- **Perfect privacy at large distortion** (Theorem 1, second case, which the paper notes holds +for source sets of any class): for `D ≥ (M - 1) / M`, the uniform mechanism `Q(x̂ | x) = 1 / M` is +`0`-differentially private and `(S, D)`-valid for every source set `S`, so `ε*_DP(S, D) = 0`. -/ +theorem isLeast_achievableDP_zero [Nonempty α] (hS : ∀ P ∈ S, ∑ x, P x = 1) + (hD : (Fintype.card α - 1) / Fintype.card α ≤ D) : + IsLeast (achievableDP S D) 0 := by + have hM : (Fintype.card α : ℝ) ≠ 0 := by simp + have hQ : (fun _ _ ↦ (Fintype.card α : ℝ)⁻¹ : Matrix α α ℝ) ∈ Matrix.rowStochastic ℝ α := + Matrix.mem_rowStochastic_iff_sum.2 ⟨fun _ _ ↦ by positivity, fun _ ↦ by simp [hM]⟩ + refine ⟨⟨_, ⟨hQ, fun P hP ↦ ?_⟩, fun _ _ _ ↦ by simp⟩, fun ε ⟨Q, hQ, hε⟩ ↦ hε.nonneg hQ.1⟩ + rw [hammingDistortion_eq hQ, ← sum_mul, hS P hP, one_mul] + rwa [sub_div, div_self hM, one_div] at hD + +/-- **Optimal leakage when some source law is spread out** (common generalization of the first +cases of Theorem 1 and Theorem 2(b)). If `0 < D` and the convex hull of the source set `S` +contains a law `P` with `P(x) > D / (M - 1)` for every symbol `x`, then the symmetric mechanism is +optimal and `ε*_DP(S, D) = log ((M - 1)(1 - D) / D)`. -/ +theorem isLeast_achievableDP_of_lt [Nontrivial α] (hS : ∀ P ∈ S, ∑ x, P x = 1) (hD : 0 < D) + {P : α → ℝ} (hP : P ∈ convexHull ℝ S) (hPD : ∀ x, D / (Fintype.card α - 1) < P x) : + IsLeast (achievableDP S D) (log ((Fintype.card α - 1) * (1 - D) / D)) := by + have hP₁ : ∑ x, P x = 1 := by + have hlin : IsLinearMap ℝ fun P : α → ℝ ↦ ∑ x, P x := + ⟨fun _ _ ↦ sum_add_distrib, fun c P ↦ by simp [mul_sum]⟩ + exact (convex_hyperplane hlin 1).convexHull_subset_iff.2 hS hP + set M : ℝ := (Fintype.card α : ℝ) + have hM : 1 < M := by simp only [M]; exact_mod_cast Fintype.one_lt_card (α := α) + -- Summing `P(x) > D / (M - 1)` over `x` gives `D < (M - 1) / M`. + have hDM : D < (M - 1) / M := by + have h := sum_lt_sum_of_nonempty univ_nonempty fun x (_ : x ∈ univ) ↦ hPD x + rw [hP₁, sum_const, card_univ, nsmul_eq_mul, mul_div_assoc', div_lt_one (by linarith)] at h + rw [lt_div_iff₀ (by linarith)] + linarith + have hD₁ : D < 1 := hDM.trans ((div_lt_one (by linarith)).2 (by linarith)) + refine ⟨⟨symmMechanism D, ⟨symmMechanism_mem_rowStochastic hD.le hD₁.le, fun P' hP' ↦ + (hammingDistortion_symmMechanism hD.le hD₁.le (hS P' hP')).le⟩, + isLocalDP_symmMechanism hD hDM.le⟩, ?_⟩ + rintro ε ⟨Q, hQ, hε⟩ + rw [← validMechanisms_convexHull] at hQ + have h := card_sub_one_mul_le_exp_mul hQ.1 hε hP₁ hD hPD (hQ.2 P hP) + rw [log_le_iff_le_exp (div_pos (mul_pos (by linarith) (by linarith)) hD), div_le_iff₀ hD] + exact h + +/-- **Theorem 1** (Class I source sets, `0 < D < (M - 1) / M`): if the convex hull of `S` contains +the uniform distribution, the symmetric mechanism `Q_D` is optimal and +`ε*_DP(S, D) = log ((M - 1)(1 - D) / D)`. -/ +theorem isLeast_achievableDP_of_isClassI [Nontrivial α] (hS : ∀ P ∈ S, ∑ x, P x = 1) + (hI : IsClassI S) (hD : 0 < D) (hDM : D < (Fintype.card α - 1) / Fintype.card α) : + IsLeast (achievableDP S D) (log ((Fintype.card α - 1) * (1 - D) / D)) := by + have hM : (1 : ℝ) < Fintype.card α := by exact_mod_cast Fintype.one_lt_card (α := α) + refine isLeast_achievableDP_of_lt hS hD hI fun x ↦ ?_ + rw [div_lt_iff₀ (by linarith), inv_mul_eq_div] + rw [lt_div_iff₀ (by linarith)] at hDM + rw [lt_div_iff₀ (by linarith)] + linarith + +/-- **Theorem 1**, eq. (8): for a Class I source set and `0 < D`, +`ε*_DP(S, D) = log ((M - 1)(1 - D) / D)` if `D < (M - 1) / M`, and `0` otherwise. The endpoint +`D = 0` of (8), where `ε*_DP = ∞`, is excluded. -/ +theorem optimalDP_of_isClassI [Nontrivial α] (hS : ∀ P ∈ S, ∑ x, P x = 1) (hI : IsClassI S) + (hD : 0 < D) : + optimalDP S D = ((if D < (Fintype.card α - 1) / Fintype.card α then + log ((Fintype.card α - 1) * (1 - D) / D) else 0 : ℝ) : EReal) := by + split_ifs with hDM + · exact optimalDP_eq_of_isLeast (isLeast_achievableDP_of_isClassI hS hI hD hDM) + · exact optimalDP_eq_of_isLeast (isLeast_achievableDP_zero hS (not_lt.1 hDM)) + +end Optimal + +/-! ### Square mechanisms suffice: the reduction of Lemma 3 -/ + +section OutputAlphabet + +variable [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] {S : Set (α → ℝ)} {D ε : ℝ} + +/-- The reduction step of **Lemma 3** (an output alphabet of size `M` suffices). Let +`Q : α → β → ℝ` be a mechanism with an arbitrary finite output alphabet `β` containing the input +alphabet through an injection `ι`, and Hamming distortion `d(x, x̂) = 1{ι x ≠ x̂}`. Merging all +outputs outside the image of `ι` into one output gives a square mechanism that is +`ε`-differentially private whenever `Q` is, and whose expected Hamming distortion is no larger +under any source law. -/ +theorem exists_square_mechanism [Nonempty α] {ι : α → β} (hι : ι.Injective) + {Q : α → β → ℝ} (hQ₀ : ∀ x y, 0 ≤ Q x y) (hQ₁ : ∀ x, ∑ y, Q x y = 1) : + ∃ Q' ∈ Matrix.rowStochastic ℝ α, (∀ ε, IsLocalDP Q ε → IsLocalDP Q' ε) ∧ + ∀ P : α → ℝ, (∀ x, 0 ≤ P x) → + hammingDistortion P Q' ≤ ∑ x, ∑ y, P x * Q x y * if ι x = y then 0 else 1 := by + obtain ⟨x₀⟩ := ‹Nonempty α› + set R : Finset β := (univ.image ι)ᶜ + set Q' : Matrix α α ℝ := fun x x' ↦ Q x (ι x') + if x' = x₀ then ∑ y ∈ R, Q x y else 0 + have hR (x : α) : 0 ≤ ∑ y ∈ R, Q x y := sum_nonneg fun y _ ↦ hQ₀ x y + have hrow (x : α) : ∑ x', Q x (ι x') + ∑ y ∈ R, Q x y = 1 := by + rw [← sum_image (s := univ) (f := Q x) hι.injOn, sum_add_sum_compl, hQ₁] + have hQ' : Q' ∈ Matrix.rowStochastic ℝ α := by + refine Matrix.mem_rowStochastic_iff_sum.2 ⟨fun x x' ↦ ?_, fun x ↦ ?_⟩ + · exact add_nonneg (hQ₀ _ _) (by split_ifs; exacts [hR x, le_rfl]) + · simp only [Q', sum_add_distrib, sum_ite_eq', mem_univ, ↓reduceIte, hrow] + refine ⟨Q', hQ', fun ε hε x₁ x₂ x' ↦ ?_, fun P hP ↦ ?_⟩ + · simp only [Q', mul_add] + refine add_le_add (hε _ _ _) ?_ + split_ifs + · rw [mul_sum]; exact sum_le_sum fun y _ ↦ hε _ _ _ + · simp + · rw [hammingDistortion_eq hQ'] + refine sum_le_sum fun x _ ↦ ?_ + have h (y : β) : P x * Q x y * (if ι x = y then 0 else 1) = + P x * (Q x y - if ι x = y then Q x y else 0) := by + split_ifs <;> ring + simp_rw [h, ← mul_sum, sum_sub_distrib, sum_ite_eq, hQ₁] + simp only [mem_univ, ↓reduceIte] + refine mul_le_mul_of_nonneg_left ?_ (hP x) + simp only [Q'] + split_ifs <;> linarith [hR x] + +/-- The reduction step of **Lemma 3**: optimizing over mechanisms with an arbitrary finite output +alphabet gives nothing beyond square mechanisms. Any privacy level achieved by a mechanism +`Q : α → β → ℝ` meeting the distortion constraint for every (nonnegative) source law in `S` is +achieved by a `(S, D)`-valid square mechanism. The paper's Lemma 3 (existence of an optimal +mechanism with at most `M` outputs) follows by applying this to an optimal mechanism, when one +exists. -/ +theorem mem_achievableDP_of_injective [Nonempty α] (hS : ∀ P ∈ S, ∀ x, 0 ≤ P x) + {ι : α → β} (hι : ι.Injective) {Q : α → β → ℝ} (hQ₀ : ∀ x y, 0 ≤ Q x y) + (hQ₁ : ∀ x, ∑ y, Q x y = 1) + (hQD : ∀ P ∈ S, ∑ x, ∑ y, P x * Q x y * (if ι x = y then 0 else 1) ≤ D) + (hε : IsLocalDP Q ε) : ε ∈ achievableDP S D := by + obtain ⟨Q', hQ', hdp, hdist⟩ := exists_square_mechanism hι hQ₀ hQ₁ + exact ⟨Q', ⟨hQ', fun P hP ↦ (hdist P (hS P hP)).trans (hQD P hP)⟩, hdp ε hε⟩ + +end OutputAlphabet + +/-! ### Zero leakage: Lemma 7 -/ + +section ZeroLeakage + +variable [Fintype α] [DecidableEq α] {S : Set (α → ℝ)} {D : ℝ} + +/-- **Lemma 7**, general form. Suppose every source law in `S` puts its largest mass on a common +symbol `x₀` (for a Class II source set, the first symbol). Then a `(S, D)`-valid `0`-differentially +private mechanism exists iff `1 - P(x₀) ≤ D` for every `P ∈ S`. -/ +theorem zero_mem_achievableDP_iff {x₀ : α} (hS : ∀ P ∈ S, ∑ x, P x = 1) + (hx₀ : ∀ P ∈ S, ∀ x, P x ≤ P x₀) : + 0 ∈ achievableDP S D ↔ ∀ P ∈ S, 1 - P x₀ ≤ D := by + constructor + · rintro ⟨Q, ⟨hQ, hQD⟩, hε⟩ P hP + -- A `0`-DP mechanism has constant columns: `Q(y | x) = Q(y | x₀)`. + have hcol (x y : α) : Q x y = Q x₀ y := + le_antisymm (by simpa using hε x x₀ y) (by simpa using hε x₀ x y) + calc 1 - P x₀ = 1 - ∑ x, P x₀ * Q x₀ x := by + rw [← mul_sum, Matrix.sum_row_of_mem_rowStochastic hQ, mul_one] + _ ≤ 1 - ∑ x, P x * Q x₀ x := sub_le_sub_left (sum_le_sum fun x _ ↦ + mul_le_mul_of_nonneg_right (hx₀ P hP x) (Matrix.nonneg_of_mem_rowStochastic hQ)) 1 + _ = hammingDistortion P Q := by + simp [hammingDistortion_eq hQ, mul_sub, sum_sub_distrib, hS P hP, hcol] + _ ≤ D := hQD P hP + · intro h + have hQ : (fun _ y ↦ if y = x₀ then 1 else 0 : Matrix α α ℝ) ∈ Matrix.rowStochastic ℝ α := + Matrix.mem_rowStochastic_iff_sum.2 ⟨fun _ _ ↦ by split_ifs <;> norm_num, fun _ ↦ by simp⟩ + refine ⟨_, ⟨hQ, fun P hP ↦ ?_⟩, fun _ _ _ ↦ by simp⟩ + simpa [hammingDistortion_eq hQ, mul_sub, sum_sub_distrib, hS P hP] using h P hP + +/-- **Lemma 7**, general form, stated for the optimal leakage: `ε*_DP(S, D) = 0` iff +`1 - P(x₀) ≤ D` for every `P ∈ S`, when all laws in `S` have a common mode `x₀`. -/ +theorem isLeast_achievableDP_zero_iff {x₀ : α} (hS : ∀ P ∈ S, ∑ x, P x = 1) + (hx₀ : ∀ P ∈ S, ∀ x, P x ≤ P x₀) : + IsLeast (achievableDP S D) 0 ↔ ∀ P ∈ S, 1 - P x₀ ≤ D := + have : Nonempty α := ⟨x₀⟩ + ⟨fun h ↦ (zero_mem_achievableDP_iff hS hx₀).1 h.1, fun h ↦ + ⟨(zero_mem_achievableDP_iff hS hx₀).2 h, fun _ ⟨_, hQ, hε⟩ ↦ hε.nonneg hQ.1⟩⟩ + +end ZeroLeakage + +/-! ### Class II source sets: Theorem 2 -/ + +section ClassII + +variable {M : ℕ} {S : Set (Fin M → ℝ)} {D : ℝ} + +/-- The reduction step of **Lemma 4**: for a Class II source set (laws nonincreasing on `Fin M`, +Remark 1), any privacy level achieved by a `(S, D)`-valid mechanism is achieved by one whose +distortions `D_i = 1 - Q(i | i)` are nondecreasing, `D_1 ≤ ⋯ ≤ D_M`. It is obtained by relabeling +the symbols so as to sort the distortions, using the rearrangement inequality. The paper's +Lemma 4 (existence of such an optimal mechanism) follows by applying this to an optimal +mechanism, when one exists. -/ +theorem exists_monotone_distortion (hord : ∀ P ∈ S, Antitone P) {ε : ℝ} + {Q : Matrix (Fin M) (Fin M) ℝ} (hQ : Q ∈ validMechanisms S D) (hε : IsLocalDP Q ε) : + ∃ Q' ∈ validMechanisms S D, IsLocalDP Q' ε ∧ Monotone fun i ↦ 1 - Q' i i := by + set g : Fin M → ℝ := fun i ↦ 1 - Q i i + obtain ⟨σ, hσ⟩ : ∃ σ : Equiv.Perm (Fin M), Monotone (g ∘ σ) := ⟨_, Tuple.monotone_sort g⟩ + have hQ' : (fun i j ↦ Q (σ i) (σ j) : Matrix (Fin M) (Fin M) ℝ) ∈ + Matrix.rowStochastic ℝ (Fin M) := by + refine Matrix.mem_rowStochastic_iff_sum.2 + ⟨fun i j ↦ Matrix.nonneg_of_mem_rowStochastic hQ.1, fun i ↦ ?_⟩ + rw [Equiv.sum_comp σ (Q (σ i)), Matrix.sum_row_of_mem_rowStochastic hQ.1] + refine ⟨_, ⟨hQ', fun P hP ↦ ?_⟩, fun _ _ _ ↦ hε _ _ _, hσ⟩ + have h := ((hord P hP).antivary hσ).sum_mul_le_sum_mul_comp_perm + (σ := σ⁻¹) + have hPQ := hQ.2 P hP + rw [hammingDistortion_eq hQ.1] at hPQ + rw [hammingDistortion_eq hQ'] + simp only [Function.comp_apply, Equiv.Perm.coe_inv, Equiv.apply_symm_apply, g] at h + exact h.trans hPQ + +/-- The distortion thresholds `D^(k) = max_{P ∈ S} ∑_{i = M - k + 1}^{M} P_i` of (9): the largest +total mass of the `k` least likely symbols, for a Class II source set whose laws are nonincreasing +on `Fin M` (Remark 1). It is a supremum over the (nonempty, bounded) set `S`. -/ +noncomputable def distortionThreshold (S : Set (Fin M → ℝ)) (k : ℕ) : ℝ := + ⨆ P : S, ∑ i : Fin M with M ≤ i.val + k, (P : Fin M → ℝ) i + +/-- There are at most `k` symbols among the `k` last ones. -/ +lemma card_filter_le_add_le (k : ℕ) : #{i : Fin M | M ≤ (i : ℕ) + k} ≤ k := by + calc #{i : Fin M | M ≤ (i : ℕ) + k} + ≤ #(range k) := card_le_card_of_injOn (fun i : Fin M ↦ M - 1 - (i : ℕ)) + (fun i hi ↦ by simp only [coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hi + simp only [coe_range, Set.mem_Iio]; omega) + (fun i _ j _ h ↦ Fin.ext (by simp only at h; omega)) + _ = k := card_range k + +/-- For a nonincreasing nonnegative `P` on `Fin M`, the `k` last symbols carry the least mass +among all sets of at least `k` symbols. -/ +lemma sum_filter_le_sum_of_antitone {P : Fin M → ℝ} (hP₀ : ∀ i, 0 ≤ P i) (hP : Antitone P) + {Z : Finset (Fin M)} {k : ℕ} (hk : k ≤ #Z) : + ∑ i : Fin M with M ≤ i.val + k, P i ≤ ∑ i ∈ Z, P i := by + set L : Finset (Fin M) := {i | M ≤ (i : ℕ) + k} + have hLZ : #(L \ Z) ≤ #(Z \ L) := + card_sdiff_le_card_sdiff_iff.2 ((card_filter_le_add_le k).trans hk) + have hlt : ∀ z ∈ Z \ L, ∀ l ∈ L \ Z, z ≤ l := by + intro z hz l hl + simp only [L, mem_sdiff, mem_filter, mem_univ, true_and, not_le] at hz hl + exact Fin.le_def.2 (by omega) + have key : ∑ i ∈ L \ Z, P i ≤ ∑ i ∈ Z \ L, P i := by + rcases (Z \ L).eq_empty_or_nonempty with h | h + · rw [h, card_empty, Nat.le_zero, card_eq_zero] at hLZ + simp [h, hLZ] + · calc ∑ i ∈ L \ Z, P i ≤ #(L \ Z) • P ((Z \ L).max' h) := + sum_le_card_nsmul _ _ _ fun l hl ↦ hP (hlt _ (max'_mem _ h) l hl) + _ ≤ #(Z \ L) • P ((Z \ L).max' h) := nsmul_le_nsmul_left (hP₀ _) hLZ + _ ≤ ∑ i ∈ Z \ L, P i := card_nsmul_le_sum _ _ _ fun i hi ↦ hP (le_max' _ i hi) + calc ∑ i ∈ L, P i = ∑ i ∈ L ∩ Z, P i + ∑ i ∈ L \ Z, P i := (sum_inter_add_sum_sdiff L Z P).symm + _ ≤ ∑ i ∈ Z ∩ L, P i + ∑ i ∈ Z \ L, P i := by rw [inter_comm]; gcongr + _ = ∑ i ∈ Z, P i := sum_inter_add_sum_sdiff Z L P + +/-- **Theorem 2(a)** (Lemma 8): for a nonempty Class II source set (nonnegative laws, +nonincreasing on `Fin M`) and `D < D^(k)`, no mechanism with `k` or more all-zero columns is +`(S, D)`-valid. -/ +theorem notMem_validMechanisms_of_lt_distortionThreshold (hS₀ : ∀ P ∈ S, ∀ i, 0 ≤ P i) + (hord : ∀ P ∈ S, Antitone P) (hne : S.Nonempty) {k : ℕ} {Q : Matrix (Fin M) (Fin M) ℝ} + (hQ : Q ∈ Matrix.rowStochastic ℝ (Fin M)) (hk : k ≤ #{y | ∀ x, Q x y = 0}) + (hD : D < distortionThreshold S k) : Q ∉ validMechanisms S D := by + have := hne.to_subtype + obtain ⟨⟨P, hP⟩, hPD⟩ := exists_lt_of_lt_ciSup hD + rintro ⟨-, hQD⟩ + have h : ∑ i with ∀ x, Q x i = 0, P i ≤ hammingDistortion P Q := by + rw [hammingDistortion_eq hQ] + calc ∑ i with ∀ x, Q x i = 0, P i = ∑ i with ∀ x, Q x i = 0, P i * (1 - Q i i) := + sum_congr rfl fun i hi ↦ by rw [(mem_filter.1 hi).2 i]; ring + _ ≤ ∑ i, P i * (1 - Q i i) := + sum_le_sum_of_subset_of_nonneg (subset_univ _) fun i _ _ ↦ mul_nonneg (hS₀ P hP i) + (by linarith [Matrix.le_one_of_mem_rowStochastic hQ (i := i) (j := i)]) + linarith [sum_filter_le_sum_of_antitone (hS₀ P hP) (hord P hP) hk, hQD P hP] + +/-- **Lemma 7** (and the last case of Theorem 2(b)): for a nonempty Class II source set, +`ε*_DP(S, D) = 0` iff `D ≥ D^(M-1)`. -/ +theorem isLeast_achievableDP_zero_iff_distortionThreshold_le [NeZero M] + (hS : ∀ P ∈ S, (∀ i, 0 ≤ P i) ∧ ∑ i, P i = 1) (hord : ∀ P ∈ S, Antitone P) + (hne : S.Nonempty) : + IsLeast (achievableDP S D) 0 ↔ distortionThreshold S (M - 1) ≤ D := by + have := hne.to_subtype + have hsum (P : Fin M → ℝ) (hP : P ∈ S) : + ∑ i : Fin M with M ≤ i.val + (M - 1), P i = 1 - P 0 := by + have h : ({i | M ≤ (i : ℕ) + (M - 1)} : Finset (Fin M)) = univ.erase 0 := by + ext i + simp only [mem_filter, mem_univ, true_and, mem_erase, ne_eq, Fin.ext_iff, Fin.val_zero, + and_true] + have := NeZero.pos M + omega + rw [h, ← (hS P hP).2, ← add_sum_erase _ _ (mem_univ 0)] + ring + have hbdd : BddAbove + (Set.range fun P : S ↦ ∑ i : Fin M with M ≤ i.val + (M - 1), (P : Fin M → ℝ) i) := + ⟨1, by + rintro _ ⟨⟨P, hP⟩, rfl⟩ + exact (sum_le_sum_of_subset_of_nonneg (filter_subset _ _) fun i _ _ ↦ (hS P hP).1 i).trans + (hS P hP).2.le⟩ + rw [isLeast_achievableDP_zero_iff (x₀ := 0) (fun P hP ↦ (hS P hP).2) + (fun P hP i ↦ hord P hP (Fin.zero_le i)), distortionThreshold, ciSup_le_iff hbdd] + simp only [Subtype.forall] + exact forall₂_congr fun P hP ↦ by rw [hsum P hP] + +/-- **Theorem 2(b)**, first case: for a nonempty Class II source set and `0 < D < D^(1)`, the +symmetric mechanism is optimal and `ε*_DP(S, D) = log ((M - 1)(1 - D) / D)`. -/ +theorem isLeast_achievableDP_of_lt_distortionThreshold_one (hM : 2 ≤ M) + (hS : ∀ P ∈ S, (∀ i, 0 ≤ P i) ∧ ∑ i, P i = 1) (hord : ∀ P ∈ S, Antitone P) + (hne : S.Nonempty) (hD : 0 < D) (hD₁ : D < distortionThreshold S 1) : + IsLeast (achievableDP S D) (log ((M - 1) * (1 - D) / D)) := by + have : Nontrivial (Fin M) := Fin.nontrivial_iff_two_le.2 hM + have := hne.to_subtype + obtain ⟨⟨P, hP⟩, hPD⟩ := exists_lt_of_lt_ciSup hD₁ + -- Every symbol has probability larger than `D`, since the last one does. + have hPx (x : Fin M) : D < P x := by + refine hPD.trans_le ?_ + calc ∑ i : Fin M with M ≤ i.val + 1, P i ≤ #{i : Fin M | M ≤ (i : ℕ) + 1} • P x := + sum_le_card_nsmul _ _ _ fun i hi ↦ hord P hP <| by + simp only [mem_filter, mem_univ, true_and] at hi + exact Fin.le_def.2 (by omega) + _ ≤ 1 • P x := nsmul_le_nsmul_left ((hS P hP).1 x) (card_filter_le_add_le 1) + _ = P x := one_nsmul _ + have hM' : (1 : ℝ) ≤ M - 1 := by + have : (2 : ℝ) ≤ M := by exact_mod_cast hM + linarith + simpa using isLeast_achievableDP_of_lt (fun P hP ↦ (hS P hP).2) hD (subset_convexHull ℝ S hP) + fun x ↦ by simpa using (div_le_self hD.le hM').trans_lt (hPx x) + +end ClassII + +/-! ### Differential privacy bounds maximal leakage and mutual information -/ + +section Leakage + +open MeasureTheory ProbabilityTheory + +variable {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : Measure α} {κ : Kernel α β} + {ε : ℝ} [Fintype β] [MeasurableSingletonClass β] [IsMarkovKernel κ] + +/-- If the channel `κ` is `ε`-differentially private, i.e. its matrix of transition probabilities +`(κ x {y})` is, then `∑_y max_x κ x {y} ≤ e^ε`. -/ +lemma maxLeakageSum_le_of_isLocalDP [Nonempty α] + (hκ : IsLocalDP (fun x y ↦ (κ x {y}).toReal) ε) : + maxLeakageSum μ κ ≤ ENNReal.ofReal (exp ε) := by + obtain ⟨x₀⟩ := ‹Nonempty α› + calc maxLeakageSum μ κ ≤ ∑ y, ENNReal.ofReal (exp ε) * κ x₀ {y} := by + refine sum_le_sum fun y _ ↦ iSup₂_le fun x _ ↦ ?_ + rw [← ENNReal.ofReal_toReal (measure_ne_top (κ x) {y}), + ← ENNReal.ofReal_toReal (measure_ne_top (κ x₀) {y}), + ← ENNReal.ofReal_mul (exp_pos ε).le] + exact ENNReal.ofReal_le_ofReal (hκ x x₀ y) + _ = ENNReal.ofReal (exp ε) := by simp [← mul_sum, sum_measure_singleton (μ := κ x₀)] + +lemma toReal_maxLeakageSum_le_of_isLocalDP [Nonempty α] + (hκ : IsLocalDP (fun x y ↦ (κ x {y}).toReal) ε) : (maxLeakageSum μ κ).toReal ≤ exp ε := + (ENNReal.toReal_mono ENNReal.ofReal_ne_top (maxLeakageSum_le_of_isLocalDP hκ)).trans_eq + (ENNReal.toReal_ofReal (exp_pos ε).le) + +-- The instances `[Countable α] [MeasurableSingletonClass α]` are not used in the proof: they +-- restrict the statement to purely atomic inputs, where `maxLeakage` is the operational quantity. +/-- **Differential privacy bounds maximal leakage**: if the channel `κ` is `ε`-differentially +private, then `L(X → Y) ≤ ε` for every nonzero input law `μ` on a countable alphabet with +measurable singletons (so that `μ` is purely atomic and `maxLeakage μ κ` is the operational +maximal leakage). The atom `x₀` exists for every nonzero such `μ`. -/ +@[nolint unusedArguments] +theorem maxLeakage_le_of_isLocalDP [Countable α] [MeasurableSingletonClass α] {x₀ : α} + (hx₀ : μ {x₀} ≠ 0) (hκ : IsLocalDP (fun x y ↦ (κ x {y}).toReal) ε) : + maxLeakage μ κ ≤ ε := by + have : Nonempty α := ⟨x₀⟩ + rw [maxLeakage, log_le_iff_le_exp (by linarith [one_le_toReal_maxLeakageSum (κ := κ) hx₀])] + exact toReal_maxLeakageSum_le_of_isLocalDP hκ + +omit [Fintype β] in +/-- **DP leakage upper bounds MI leakage** (Section III-A): if the channel `κ` is +`ε`-differentially private, then `I(X; X̂) ≤ ε` for every input law on a countable alphabet. In +particular the worst-case MI leakage `max_{P ∈ S} I(P; Q)` of (20) is at most the DP leakage. -/ +theorem toReal_mutualInfo_compProd_le_of_isLocalDP [Finite β] [Countable α] + [IsProbabilityMeasure μ] + (hκ : IsLocalDP (fun x y ↦ (κ x {y}).toReal) ε) : (mutualInfo (μ ⊗ₘ κ)).toReal ≤ ε := by + have := Fintype.ofFinite β + obtain ⟨x, hx⟩ := MeasureTheory.Measure.exists_measure_singleton_ne_zero μ + have : Nonempty α := ⟨x⟩ + refine toReal_mutualInfo_compProd_le_maxLeakage.trans ?_ + rw [maxLeakage, log_le_iff_le_exp (by linarith [one_le_toReal_maxLeakageSum (κ := κ) hx])] + exact toReal_maxLeakageSum_le_of_isLocalDP hκ + +end Leakage + +end InformationTheory