feat: privacy leakage measures (6/6): differential privacy under Hamming distortion

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
@@ -138,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

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

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