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] 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