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 6938082bf1da245d3e5a9d9ee3995126bbf03804 Mon Sep 17 00:00:00 2001 From: Kousha Kalantari <25445970+KoushaKalantari@users.noreply.github.com> Date: Fri, 13 Nov 2026 10:04:17 -0800 Subject: [PATCH 2/2] =?UTF-8?q?feat(Divergence):=20variational=20formula?= =?UTF-8?q?=20for=20the=20=E2=88=9E-R=C3=A9nyi=20divergence=20(Kurri?= =?UTF-8?q?=E2=80=93Kosut=E2=80=93Sankar)?= 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/Divergence/RenyiInfinity/Basic.lean | 659 ++++++++++++++++++++ 2 files changed, 660 insertions(+) create mode 100644 Statlib/Divergence/RenyiInfinity/Basic.lean diff --git a/Statlib.lean b/Statlib.lean index 253c245..f48c598 100644 --- a/Statlib.lean +++ b/Statlib.lean @@ -56,6 +56,7 @@ import Statlib.Divergence.Renyi.Order.Limits import Statlib.Divergence.Renyi.Prod import Statlib.Divergence.Renyi.ProdCountable import Statlib.Divergence.Renyi.Variational +import Statlib.Divergence.RenyiInfinity.Basic import Statlib.Divergence.StatInfo.Basic import Statlib.Divergence.StatInfo.CurvatureMeasure import Statlib.Divergence.StatInfo.Event diff --git a/Statlib/Divergence/RenyiInfinity/Basic.lean b/Statlib/Divergence/RenyiInfinity/Basic.lean new file mode 100644 index 0000000..ae819bd --- /dev/null +++ b/Statlib/Divergence/RenyiInfinity/Basic.lean @@ -0,0 +1,659 @@ +/- +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.Operational +public import Mathlib.Analysis.MeanInequalities +public import Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp +public import Mathlib.Analysis.SpecialFunctions.Pow.Continuity + +/-! +# A variational formula for the Rényi divergence of order `∞` + +This file formalizes, for finite alphabets, the main results of + +* G. R. Kurri, O. Kosut, L. Sankar, *A Variational Formula for Infinity-Rényi Divergence with + Applications to Information Leakage*, ISIT 2022, arXiv:2202.06040. + +The Rényi divergence of order `∞` is `D∞(P ‖ Q) = log max_x P(x) / Q(x)`. The paper shows that, +for every gain function `g : [0, 1] → [0, ∞)` with `g 0 = 0`, `g` continuous at `0` and +`0 < sup g < ∞`, +`D∞(P_X ‖ Q_X) = sup_{P_{U|X}} log (G_g(P_U) / G_g(Q_U))`, where +`G_g(ν) = sup_{P_Û} E_{U ∼ ν} g(P_Û(U))` and `P_U`, `Q_U` are the laws of `U` obtained by passing +`P_X` and `Q_X` through the channel `P_{U|X}`: the ratio of the largest expected gains in +guessing `U` does not depend on `g` once it is optimized over all channels. Specializing `g` to +the `α`-loss gain gives closed forms for two variants of maximal `α`-leakage. + +## Main definitions + +* `expRenyiDivInf P Q`: `max_x P(x) / Q(x)` in `ℝ≥0∞`, the exponential of `D∞(P ‖ Q)`. +* `renyiDivInf P Q`: `D∞(P ‖ Q) = log max_x P(x) / Q(x)`, in `EReal` (in nats). +* `maxExpGain g ν`: `sup_{P_Û} E_{U ∼ ν} g(P_Û(U))`, the largest expected gain in guessing `U ∼ ν`. +* `alphaNorm a ν`: `(∑_u ν(u) ^ a) ^ (1 / a)`. +* `condInput μ κ y`: the conditional law `P_{X|Y=y}` of the input given the output. +* `oppMaxAlphaLeakage a μ κ`: the opportunistic maximal `α`-leakage (paper, Definition 4). +* `realMaxAlphaLeakage a μ κ`: the maximal realizable `α`-leakage (paper, Definition 5). + +## Main statements + +* `iSup_maxExpGain_div_eq`, `iSup_log_maxExpGain_div_eq`: **Theorem 1**, the variational formula. +* `maxExpGain_ne_zero`: the ratio in Theorem 1 is well defined (paper, (44)–(45)). +* `iSup_lintegral_rpow_eq`: the closed form of the guessing problem for the `α`-loss gain + (Lemma 1 of Liao–Kosut–Sankar–Calmon, used for Corollary 1). +* `iSup_alphaNorm_div_eq`: **Corollary 1**. +* `iSup_lintegral_div_eq`, `iSup_log_lintegral_div_eq`: **Proposition 1**, formula (10). +* `oppMaxAlphaLeakage_eq`: **Theorem 2**, the opportunistic maximal `α`-leakage equals + `α / (α - 1) · I∞ˢ(X; Y)`, where `I∞ˢ(X; Y) = maxLeakage μ κ` is the Sibson mutual information + of order `∞` (the maximal leakage). +* `realMaxAlphaLeakage_eq`: **Theorem 3**, the maximal realizable `α`-leakage equals + `α / (α - 1) · D∞(P_XY ‖ P_X × P_Y)`. + +## Paper → Lean + +* Definition 1, (4) → `expRenyiDivInf`, `renyiDivInf`. +* Theorem 1 → `iSup_maxExpGain_div_eq` (multiplicative), `iSup_log_maxExpGain_div_eq` (with `log`); + its two halves are `maxExpGain_comp_div_le` ((19)–(24)) and `div_le_iSup_maxExpGain_div` + ((25)–(43)). +* Corollary 1 → `iSup_alphaNorm_div_eq`, `iSup_log_alphaNorm_div_eq`. +* Proposition 1, (10) → `iSup_lintegral_div_eq`, `iSup_log_lintegral_div_eq`. +* Definition 4, Theorem 2 → `oppMaxAlphaLeakageSum`, `oppMaxAlphaLeakage`, + `oppMaxAlphaLeakageSum_eq_maxLeakageSum`, `oppMaxAlphaLeakage_eq`. +* Definition 5, Theorem 3 → `realMaxAlphaLeakage`, `realMaxAlphaLeakage_eq`. + +Not formalized: Proposition 1, formula (9) (in terms of relative entropies), Remark 1 and +Appendix A (the gain `g = log`, which is not covered by Theorem 1). + +## Implementation notes + +* Distributions are `Measure`s on finite types with measurable singletons and channels are + Markov `Kernel`s, as in `Statlib.Divergence.MaximalLeakage`. Values are in `ℝ≥0∞`; + `P(x) / Q(x)` uses the conventions `p / 0 = ∞` for `p ≠ 0` and `0 / 0 = 0`, so that + `expRenyiDivInf P Q` is the maximum over the support of `P`, and is `∞` exactly when `P` is + not absolutely continuous with respect to `Q`, as in the paper. +* The supremum over channels `P_{U|X}` ranges over all alphabets `Fin n`, which covers every + finite alphabet up to relabelling. For a one-letter alphabet both expected gains equal `g 1`; + if `g 1 = 0` the ratio is `0 / 0`, which `ℝ≥0∞` evaluates to `0`, and this does not change the + supremum. On alphabets with at least two letters the denominator is nonzero + (`maxExpGain_ne_zero`). +* A gain function is a map `g : ℝ≥0∞ → ℝ≥0∞`, of which only the values on `[0, 1]` matter. The + hypotheses of Theorem 1 read `g 0 = 0`, `ContinuousWithinAt g (Set.Iic 1) 0` and + `0 < ⨆ q ≤ 1, g q < ∞`; the last one also forces `g` to be finite on `[0, 1]`. +* The proof of the achievability half differs from the paper's: we spread every letter + `x ≠ x⋆` over one common block of `m` symbols, and bound the expected gain on that block by a + counting argument (at most `1 / δ` of the `m` symbols have probability `≥ δ`) instead of the + upper concave envelope `g**`. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory Filter Topology +open scoped ENNReal NNReal + +namespace InformationTheory + +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {P Q : Measure α} {g : ℝ≥0∞ → ℝ≥0∞} {a : ℝ} + +/-- The exponential `max_x P(x) / Q(x)` of the Rényi divergence of order `∞`, in `ℝ≥0∞`. It is +`∞` when some `x` has `P(x) ≠ 0 = Q(x)`. The supremum ranges over the atoms, so this is only +meaningful for purely atomic measures, e.g. on a finite type with measurable singletons. -/ +noncomputable def expRenyiDivInf (P Q : Measure α) : ℝ≥0∞ := ⨆ x, P {x} / Q {x} + +/-- The Rényi divergence of order `∞`, `D∞(P ‖ Q) = log max_x P(x) / Q(x)` (paper, Definition 1, +equation (4)), in nats, with values in `EReal`. See `expRenyiDivInf` for the conventions. -/ +noncomputable def renyiDivInf (P Q : Measure α) : EReal := ENNReal.log (expRenyiDivInf P Q) + +/-- The largest expected gain `sup_{P_Û} E_{U ∼ ν} g(P_Û(U))` of a guess distribution `P_Û` +for `U ∼ ν`, under the gain function `g`. -/ +noncomputable def maxExpGain (g : ℝ≥0∞ → ℝ≥0∞) (ν : Measure γ) : ℝ≥0∞ := + ⨆ (π : Measure γ) (_ : IsProbabilityMeasure π), ∫⁻ u, g (π {u}) ∂ν + +lemma le_expRenyiDivInf_mul [IsFiniteMeasure Q] (x : α) (h : expRenyiDivInf P Q ≠ ∞) : + P {x} ≤ expRenyiDivInf P Q * Q {x} := by + have hx : P {x} / Q {x} ≤ expRenyiDivInf P Q := le_iSup (fun x ↦ P {x} / Q {x}) x + by_cases hQ : Q {x} = 0 + · by_contra hP + rw [hQ, ENNReal.div_zero (fun h0 ↦ hP (by simp [h0]))] at hx + exact h (top_le_iff.1 hx) + · exact (ENNReal.div_le_iff hQ (measure_ne_top Q _)).1 hx + +section Variational + +/-! ### Theorem 1: the variational formula -/ + +/-- If `P ≤ c • Q` on atoms, then `∫ f d(W ∘ P) ≤ c ∫ f d(W ∘ Q)`. -/ +lemma lintegral_comp_le_mul [Finite α] [MeasurableSingletonClass α] [Finite γ] + [MeasurableSingletonClass γ] (W : Kernel α γ) (f : γ → ℝ≥0∞) {c : ℝ≥0∞} + (hc : ∀ x, P {x} ≤ c * Q {x}) : + ∫⁻ u, f u ∂(W ∘ₘ P) ≤ c * ∫⁻ u, f u ∂(W ∘ₘ Q) := by + have := Fintype.ofFinite α + have := Fintype.ofFinite γ + simp_rw [lintegral_fintype, comp_apply_singleton, Finset.mul_sum] + refine Finset.sum_le_sum fun u _ ↦ Finset.sum_le_sum fun x _ ↦ ?_ + calc f u * (W x {u} * P {x}) ≤ f u * (W x {u} * (c * Q {x})) := by gcongr; exact hc x + _ = c * (f u * (W x {u} * Q {x})) := by ring + +/-- **Converse half of Theorem 1** (paper, (19)–(24)): for every channel `W` and every gain +function `g`, the ratio of the largest expected gains is at most `max_x P(x) / Q(x)`. -/ +lemma maxExpGain_comp_div_le [Finite α] [MeasurableSingletonClass α] [Finite γ] + [MeasurableSingletonClass γ] [IsFiniteMeasure Q] (W : Kernel α γ) (g : ℝ≥0∞ → ℝ≥0∞) : + maxExpGain g (W ∘ₘ P) / maxExpGain g (W ∘ₘ Q) ≤ expRenyiDivInf P Q := by + by_cases h : expRenyiDivInf P Q = ∞ + · simp [h] + refine ENNReal.div_le_of_le_mul' ?_ + refine iSup₂_le fun π hπ ↦ ?_ + calc ∫⁻ u, g (π {u}) ∂(W ∘ₘ P) + ≤ expRenyiDivInf P Q * ∫⁻ u, g (π {u}) ∂(W ∘ₘ Q) := + lintegral_comp_le_mul W _ fun x ↦ le_expRenyiDivInf_mul x h + _ ≤ expRenyiDivInf P Q * maxExpGain g (W ∘ₘ Q) := by + gcongr + exact le_iSup₂ (f := fun π (_ : IsProbabilityMeasure π) ↦ ∫⁻ u, g (π {u}) ∂(W ∘ₘ Q)) + π hπ + _ = maxExpGain g (W ∘ₘ Q) * expRenyiDivInf P Q := mul_comm _ _ + +/-- Guessing `u₀` with an arbitrary probability `q` (and `u₁` otherwise) shows +`ν(u₀) · sup_{q ≤ 1} g(q) ≤ maxExpGain g ν` (paper, (29)–(30) and (44)–(45)). -/ +lemma mul_iSup_le_maxExpGain [MeasurableSingletonClass γ] (ν : Measure γ) {u₀ u₁ : γ} + (h : u₁ ≠ u₀) : ν {u₀} * ⨆ (q) (_ : q ≤ 1), g q ≤ maxExpGain g ν := by + simp_rw [ENNReal.mul_iSup] + refine iSup₂_le fun q hq ↦ ?_ + set π := q • Measure.dirac u₀ + (1 - q) • Measure.dirac u₁ + have hπ : IsProbabilityMeasure π := ⟨by simp [π, add_tsub_cancel_of_le hq]⟩ + have hπ0 : π {u₀} = q := by simp [π, h] + calc ν {u₀} * g q = ∫⁻ u in {u₀}, g (π {u}) ∂ν := by rw [lintegral_singleton, hπ0, mul_comm] + _ ≤ ∫⁻ u, g (π {u}) ∂ν := setLIntegral_le_lintegral _ _ + _ ≤ maxExpGain g ν := + le_iSup₂ (f := fun π (_ : IsProbabilityMeasure π) ↦ ∫⁻ u, g (π {u}) ∂ν) π hπ + +/-- **The ratio in Theorem 1 is well defined** (paper, (44)–(45)): if `sup_{q ≤ 1} g(q) > 0`, +the largest expected gain of a probability measure on an alphabet with at least two letters is +nonzero. -/ +lemma maxExpGain_ne_zero [Finite γ] [MeasurableSingletonClass γ] [Nontrivial γ] (ν : Measure γ) + [IsProbabilityMeasure ν] (hG0 : ⨆ (q) (_ : q ≤ 1), g q ≠ 0) : maxExpGain g ν ≠ 0 := by + have := Fintype.ofFinite γ + obtain ⟨u₀, hu₀⟩ : ∃ u, ν {u} ≠ 0 := by + by_contra! h + have := sum_measure_singleton (μ := ν) (s := Finset.univ) + simp [h] at this + obtain ⟨u₁, hu₁⟩ := exists_ne u₀ + exact ((pos_iff_ne_zero.2 (mul_ne_zero hu₀ hG0)).trans_le + (mul_iSup_le_maxExpGain ν hu₁)).ne' + +/-- **Shattering bound.** If `g 0 = 0`, `g` is continuous at `0` and bounded on `[0, 1]`, then for +every `ε > 0` there is `m > 0` such that any sub-probability vector `p` on `m` symbols has total +gain `∑_j g(p_j) ≤ m ε`: at most `1 / δ` of the symbols have `p_j ≥ δ`, and the others have +`g(p_j) ≤ ε / 2`. This replaces the paper's concave-envelope bound (31)–(34). -/ +lemma exists_sum_gain_le (hg0 : g 0 = 0) (hgc : ContinuousWithinAt g (Set.Iic 1) 0) + (hG : ⨆ (q) (_ : q ≤ 1), g q ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) : + ∃ m : ℕ, 0 < m ∧ ∀ p : Fin m → ℝ≥0∞, (∀ j, p j ≤ 1) → ∑ j, p j ≤ 1 → + ∑ j, g (p j) ≤ m * ε := by + classical + set G := ⨆ (q) (_ : q ≤ 1), g q + have hε2 : ε / 2 ≠ 0 := by simp [hε] + have hev : ∀ᶠ p in 𝓝[Set.Iic 1] 0, g p < ε / 2 := by + have := hgc.tendsto + rw [hg0] at this + exact this.eventually (gt_mem_nhds (pos_iff_ne_zero.2 hε2)) + rw [eventually_nhdsWithin_iff, ENNReal.nhds_zero_basis.eventually_iff] at hev + obtain ⟨δ, hδ, hδg⟩ := hev + obtain ⟨m, hm⟩ := ENNReal.exists_nat_mul_gt hε2 (b := δ⁻¹ * G) + (ENNReal.mul_ne_top (ENNReal.inv_ne_top.2 hδ.ne') hG) + refine ⟨m, Nat.pos_of_ne_zero fun h ↦ by simp [h] at hm, fun p hp1 hpsum ↦ ?_⟩ + set S := Finset.univ.filter fun j ↦ δ ≤ p j + have hS : (S.card : ℝ≥0∞) * δ ≤ 1 := by + calc (S.card : ℝ≥0∞) * δ = ∑ _j ∈ S, δ := by simp + _ ≤ ∑ j ∈ S, p j := Finset.sum_le_sum fun j hj ↦ (Finset.mem_filter.1 hj).2 + _ ≤ ∑ j, p j := Finset.sum_le_sum_of_subset (Finset.subset_univ _) + _ ≤ 1 := hpsum + have hcard : (S.card : ℝ≥0∞) ≤ δ⁻¹ := ENNReal.le_inv_iff_mul_le.2 hS + calc ∑ j, g (p j) + = ∑ j ∈ S, g (p j) + ∑ j ∈ Finset.univ.filter (fun j ↦ ¬ δ ≤ p j), g (p j) := + (Finset.sum_filter_add_sum_filter_not _ _ _).symm + _ ≤ ∑ _j ∈ S, G + ∑ _j ∈ Finset.univ.filter (fun j ↦ ¬ δ ≤ p j), ε / 2 := by + gcongr with j hj j hj + · exact le_iSup₂ (f := fun q (_ : q ≤ 1) ↦ g q) (p j) (hp1 j) + · exact (hδg (not_le.1 (Finset.mem_filter.1 hj).2) (hp1 j)).le + _ ≤ δ⁻¹ * G + m * (ε / 2) := by + simp only [Finset.sum_const, nsmul_eq_mul] + gcongr + exact_mod_cast (Finset.card_filter_le _ _).trans_eq (Finset.card_fin m) + _ ≤ m * (ε / 2) + m * (ε / 2) := by gcongr + _ = m * ε := by rw [← mul_add, ENNReal.add_halves] + +/-- The **shattering channel** of the achievability proof: `x⋆` is sent to the symbol `0`, and +every other input is spread uniformly over the `m` symbols `1, …, m`. Then `P_U(0) = P(x⋆)` and +`Q_U(j) ≤ 1 / m` for `j ≠ 0` (a variant of the paper's channel (25)). -/ +lemma exists_shatter_kernel [Finite α] [MeasurableSingletonClass α] [IsProbabilityMeasure Q] + (x₀ : α) {m : ℕ} (hm : 0 < m) : + ∃ W : Kernel α (Fin (m + 1)), IsMarkovKernel W ∧ (∀ ν : Measure α, (W ∘ₘ ν) {0} = ν {x₀}) ∧ + ∀ j : Fin m, (W ∘ₘ Q) {j.succ} ≤ (m : ℝ≥0∞)⁻¹ := by + classical + have := Fintype.ofFinite α + set w : α → Fin (m + 1) → ℝ≥0∞ := fun x u ↦ + if x = x₀ then (if u = 0 then 1 else 0) else (if u = 0 then 0 else (m : ℝ≥0∞)⁻¹) + set W : Kernel α (Fin (m + 1)) := + Kernel.ofFunOfCountable fun x ↦ ∑ u, w x u • Measure.dirac u + have hW (x : α) (u : Fin (m + 1)) : W x {u} = w x u := by + simp [W, Kernel.ofFunOfCountable, Measure.dirac_apply' _ (measurableSet_singleton u), + Set.indicator] + have hw_sum (x : α) : ∑ u, w x u = 1 := by + rw [Fin.sum_univ_succ] + by_cases hx : x = x₀ + · simp [w, hx] + · simp only [w, hx, ite_false, ite_true, Fin.succ_ne_zero, Finset.sum_const, + Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, zero_add] + exact ENNReal.mul_inv_cancel (by exact_mod_cast hm.ne') (ENNReal.natCast_ne_top m) + have : IsMarkovKernel W := ⟨fun x ↦ ⟨by + rw [← Finset.coe_univ, ← sum_measure_singleton] + simp_rw [hW, hw_sum]⟩⟩ + refine ⟨W, this, fun ν ↦ ?_, fun j ↦ ?_⟩ + · rw [comp_apply_singleton, Finset.sum_eq_single x₀ (fun x _ hx ↦ by simp [hW, w, hx]) + (by simp)] + simp [hW, w] + · rw [comp_apply_singleton] + calc ∑ x, W x {j.succ} * Q {x} ≤ ∑ x, (m : ℝ≥0∞)⁻¹ * Q {x} := by + gcongr with x + rw [hW] + by_cases hx : x = x₀ <;> simp [w, hx] + _ = (m : ℝ≥0∞)⁻¹ := by + simp [← Finset.mul_sum, sum_measure_singleton] + +/-- **Achievability half of Theorem 1** (paper, (25)–(43)): every ratio `P(x⋆) / Q(x⋆)` is at +most the supremum of the ratios of largest expected gains over channels into `Fin n`. The proof +uses the shattering channels of `exists_shatter_kernel` with more and more symbols. -/ +lemma div_le_iSup_maxExpGain_div [Finite α] [MeasurableSingletonClass α] + [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (hg0 : g 0 = 0) + (hgc : ContinuousWithinAt g (Set.Iic 1) 0) (hG0 : ⨆ (q) (_ : q ≤ 1), g q ≠ 0) + (hG : ⨆ (q) (_ : q ≤ 1), g q ≠ ∞) (x₀ : α) : + P {x₀} / Q {x₀} ≤ ⨆ (n : ℕ) (W : Kernel α (Fin n)) (_ : IsMarkovKernel W), + maxExpGain g (W ∘ₘ P) / maxExpGain g (W ∘ₘ Q) := by + set G := ⨆ (q) (_ : q ≤ 1), g q + have key (ε : ℝ≥0∞) (hε : ε ≠ 0) : P {x₀} * G / (Q {x₀} * G + ε) ≤ + ⨆ (n : ℕ) (W : Kernel α (Fin n)) (_ : IsMarkovKernel W), + maxExpGain g (W ∘ₘ P) / maxExpGain g (W ∘ₘ Q) := by + obtain ⟨m, hm, hsum⟩ := exists_sum_gain_le hg0 hgc hG hε + obtain ⟨W, hW, hW0, hWj⟩ := exists_shatter_kernel (Q := Q) x₀ hm + have hnum : P {x₀} * G ≤ maxExpGain g (W ∘ₘ P) := by + have := mul_iSup_le_maxExpGain (g := g) (W ∘ₘ P) (u₀ := 0) + (u₁ := (⟨0, hm⟩ : Fin m).succ) (Fin.succ_ne_zero _) + rwa [hW0] at this + have hden : maxExpGain g (W ∘ₘ Q) ≤ Q {x₀} * G + ε := by + refine iSup₂_le fun π _ ↦ ?_ + have hπ : ∑ j : Fin m, π {j.succ} ≤ 1 := + calc ∑ j : Fin m, π {j.succ} ≤ π {0} + ∑ j : Fin m, π {j.succ} := le_add_self + _ = ∑ u, π {u} := (Fin.sum_univ_succ (fun u ↦ π {u})).symm + _ = 1 := by simp [sum_measure_singleton] + rw [lintegral_fintype, Fin.sum_univ_succ, hW0] + gcongr ?_ + ?_ + · rw [mul_comm] + gcongr + exact le_iSup₂ (f := fun q (_ : q ≤ 1) ↦ g q) _ prob_le_one + · calc ∑ j : Fin m, g (π {j.succ}) * (W ∘ₘ Q) {j.succ} + ≤ ∑ j : Fin m, g (π {j.succ}) * (m : ℝ≥0∞)⁻¹ := by + gcongr with j + exact hWj j + _ = (∑ j : Fin m, g (π {j.succ})) * (m : ℝ≥0∞)⁻¹ := (Finset.sum_mul ..).symm + _ ≤ (m * ε) * (m : ℝ≥0∞)⁻¹ := by + gcongr + exact hsum _ (fun _ ↦ prob_le_one) hπ + _ = ε := by + rw [mul_comm (m : ℝ≥0∞), mul_assoc, + ENNReal.mul_inv_cancel (by exact_mod_cast hm.ne') (ENNReal.natCast_ne_top m), + mul_one] + calc P {x₀} * G / (Q {x₀} * G + ε) + ≤ maxExpGain g (W ∘ₘ P) / maxExpGain g (W ∘ₘ Q) := ENNReal.div_le_div hnum hden + _ ≤ _ := le_iSup_of_le (m + 1) <| le_iSup₂_of_le (f := fun (W : Kernel α (Fin (m + 1))) + (_ : IsMarkovKernel W) ↦ maxExpGain g (W ∘ₘ P) / maxExpGain g (W ∘ₘ Q)) W hW le_rfl + have hlim : Tendsto (fun k : ℕ ↦ P {x₀} * G / (Q {x₀} * G + (k : ℝ≥0∞)⁻¹)) atTop + (𝓝 (P {x₀} * G / (Q {x₀} * G))) := by + refine ENNReal.Tendsto.const_div ?_ (Or.inr (ENNReal.mul_ne_top (measure_ne_top _ _) hG)) + simpa using tendsto_const_nhds.add ENNReal.tendsto_inv_nat_nhds_zero + rw [← ENNReal.mul_div_mul_right _ _ hG0 hG] + exact le_of_tendsto' hlim fun k ↦ key _ (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top k)) + +/-- **Theorem 1** (Kurri–Kosut–Sankar), multiplicative form. Let `P`, `Q` be probability +measures on a finite alphabet and `g` a gain function with `g 0 = 0`, `g` continuous at `0` on +`[0, 1]`, and `0 < sup_{q ≤ 1} g(q) < ∞`. Then the supremum, over all finite alphabets `Fin n` +and channels `W = P_{U|X}`, of `sup_{P_Û} E_{U ∼ P_U} g(P_Û(U)) / sup_{P_Û} E_{U ∼ Q_U} g(P_Û(U))` +equals `max_x P(x) / Q(x)`. -/ +theorem iSup_maxExpGain_div_eq [Finite α] [MeasurableSingletonClass α] + [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (hg0 : g 0 = 0) + (hgc : ContinuousWithinAt g (Set.Iic 1) 0) (hG0 : ⨆ (q) (_ : q ≤ 1), g q ≠ 0) + (hG : ⨆ (q) (_ : q ≤ 1), g q ≠ ∞) : + ⨆ (n : ℕ) (W : Kernel α (Fin n)) (_ : IsMarkovKernel W), + maxExpGain g (W ∘ₘ P) / maxExpGain g (W ∘ₘ Q) = expRenyiDivInf P Q := + le_antisymm (iSup_le fun _ ↦ iSup₂_le fun W _ ↦ maxExpGain_comp_div_le W g) + (iSup_le (div_le_iSup_maxExpGain_div hg0 hgc hG0 hG)) + +/-- **Theorem 1** (Kurri–Kosut–Sankar), equation (5): under the hypotheses of +`iSup_maxExpGain_div_eq`, +`D∞(P ‖ Q) = sup_{P_{U|X}} log (sup_{P_Û} E_{P_U} g(P_Û(U)) / sup_{P_Û} E_{Q_U} g(P_Û(U)))`. -/ +theorem iSup_log_maxExpGain_div_eq [Finite α] [MeasurableSingletonClass α] + [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (hg0 : g 0 = 0) + (hgc : ContinuousWithinAt g (Set.Iic 1) 0) (hG0 : ⨆ (q) (_ : q ≤ 1), g q ≠ 0) + (hG : ⨆ (q) (_ : q ≤ 1), g q ≠ ∞) : + ⨆ (n : ℕ) (W : Kernel α (Fin n)) (_ : IsMarkovKernel W), + ENNReal.log (maxExpGain g (W ∘ₘ P) / maxExpGain g (W ∘ₘ Q)) = renyiDivInf P Q := by + rw [renyiDivInf, ← iSup_maxExpGain_div_eq hg0 hgc hG0 hG] + simp only [← ENNReal.logOrderIso_apply, OrderIso.map_iSup] + +/-! ### Proposition 1: the variational formula over test functions -/ + +/-- **Proposition 1**, equation (10), multiplicative form: the supremum of +`E_P[f] / E_Q[f]` over functions `f : X → [0, ∞)` is `max_x P(x) / Q(x)`. -/ +theorem iSup_lintegral_div_eq [Finite α] [MeasurableSingletonClass α] [IsFiniteMeasure Q] : + ⨆ f : α → ℝ≥0, (∫⁻ x, f x ∂P) / (∫⁻ x, f x ∂Q) = expRenyiDivInf P Q := by + classical + have := Fintype.ofFinite α + refine le_antisymm (iSup_le fun f ↦ ?_) (iSup_le fun x₀ ↦ ?_) + · by_cases h : expRenyiDivInf P Q = ∞ + · simp [h] + refine ENNReal.div_le_of_le_mul' ?_ + calc ∫⁻ x, (f x : ℝ≥0∞) ∂P = ∑ x, (f x : ℝ≥0∞) * P {x} := lintegral_fintype _ + _ ≤ ∑ x, (f x : ℝ≥0∞) * (expRenyiDivInf P Q * Q {x}) := by + gcongr with x + exact le_expRenyiDivInf_mul x h + _ = (∫⁻ x, (f x : ℝ≥0∞) ∂Q) * expRenyiDivInf P Q := by + rw [lintegral_fintype, Finset.sum_mul] + exact Finset.sum_congr rfl fun x _ ↦ by ring + · refine le_iSup_of_le (fun x ↦ if x = x₀ then 1 else 0) (le_of_eq ?_) + simp [lintegral_fintype, apply_ite] + +/-- **Proposition 1**, equation (10): +`D∞(P ‖ Q) = sup_{f : X → [0, ∞)} log (E_P[f] / E_Q[f])`. -/ +theorem iSup_log_lintegral_div_eq [Finite α] [MeasurableSingletonClass α] [IsFiniteMeasure Q] : + ⨆ f : α → ℝ≥0, ENNReal.log ((∫⁻ x, f x ∂P) / (∫⁻ x, f x ∂Q)) = renyiDivInf P Q := by + rw [renyiDivInf, ← iSup_lintegral_div_eq] + simp only [← ENNReal.logOrderIso_apply, OrderIso.map_iSup] + +end Variational + +section AlphaGain + +/-! ### Corollary 1: the `α`-loss gain -/ + +/-- The `α`-norm `(∑_u ν(u) ^ a) ^ (1 / a)` of the masses of `ν`. -/ +noncomputable def alphaNorm [Fintype γ] (a : ℝ) (ν : Measure γ) : ℝ≥0∞ := + (∑ u, ν {u} ^ a) ^ (1 / a) + +/-- The guessing problem for the `α`-loss gain `t ↦ t ^ ((a - 1) / a)` has the closed form +`sup_{P_Û} E_{U ∼ ν} P_Û(U) ^ ((a - 1) / a) = (∑_u ν(u) ^ a) ^ (1 / a)` for `a > 1` +(Liao–Kosut–Sankar–Calmon, *Tunable measures for information leakage*, Lemma 1, quoted in the +paper before Corollary 1). The bound is Hölder's inequality, attained at `P_Û(u) ∝ ν(u) ^ a`. -/ +lemma iSup_lintegral_rpow_eq [Fintype γ] [MeasurableSingletonClass γ] (ν : Measure γ) + [IsFiniteMeasure ν] (ha : 1 < a) : + ⨆ (π : Measure γ) (_ : IsProbabilityMeasure π), ∫⁻ u, π {u} ^ ((a - 1) / a) ∂ν = + alphaNorm a ν := by + classical + have ha0 : 0 < a := one_pos.trans ha + set s := (a - 1) / a with hs_def + have hs0 : 0 ≤ s := div_nonneg (by linarith) ha0.le + have hconj : a.HolderConjugate (a / (a - 1)) := + (Real.holderConjugate_iff_eq_conjExponent ha).2 rfl + have hsq : s * (a / (a - 1)) = 1 := by + rw [hs_def] + field_simp [show a - 1 ≠ 0 by linarith] + refine le_antisymm (iSup₂_le fun π _ ↦ ?_) ?_ + · calc ∫⁻ u, π {u} ^ s ∂ν = ∑ u, ν {u} * π {u} ^ s := by + rw [lintegral_fintype] + simp_rw [mul_comm] + _ ≤ (∑ u, ν {u} ^ a) ^ (1 / a) * + (∑ u, (π {u} ^ s) ^ (a / (a - 1))) ^ (1 / (a / (a - 1))) := + ENNReal.inner_le_Lp_mul_Lq _ _ _ hconj + _ = alphaNorm a ν := by + simp_rw [← ENNReal.rpow_mul, hsq, ENNReal.rpow_one, sum_measure_singleton] + simp [alphaNorm] + · set S := ∑ u, ν {u} ^ a + by_cases hS : S = 0 + · rw [alphaNorm, show (∑ u, ν {u} ^ a) = 0 from hS, + ENNReal.zero_rpow_of_pos (one_div_pos.2 ha0)] + exact zero_le + have hS_top : S ≠ ∞ := ENNReal.sum_ne_top.2 fun u _ ↦ + ENNReal.rpow_ne_top_of_nonneg ha0.le (measure_ne_top ν _) + set π : Measure γ := ∑ u, (ν {u} ^ a / S) • Measure.dirac u + have hπ (u : γ) : π {u} = ν {u} ^ a / S := by + simp [π, Measure.dirac_apply' _ (measurableSet_singleton u), Set.indicator] + have hπ1 : IsProbabilityMeasure π := ⟨by + rw [← Finset.coe_univ, ← sum_measure_singleton, Finset.sum_congr rfl fun u _ ↦ hπ u, + ← ENNReal.sum_div] + exact ENNReal.div_self hS hS_top⟩ + refine le_iSup₂_of_le (f := fun (π : Measure γ) (_ : IsProbabilityMeasure π) ↦ + ∫⁻ u, π {u} ^ s ∂ν) π hπ1 (le_of_eq ?_) + have hpow (x : ℝ≥0∞) : x ^ (a * s) * x = x ^ a := by + conv_rhs => rw [show a = a * s + 1 by rw [hs_def]; field_simp; ring] + rw [ENNReal.rpow_add_of_nonneg _ _ (mul_nonneg ha0.le hs0) zero_le_one, ENNReal.rpow_one] + calc alphaNorm a ν = S ^ (1 - s) := by + rw [alphaNorm] + congr 1 + rw [hs_def] + field_simp + ring + _ = S / S ^ s := by rw [ENNReal.rpow_sub _ _ hS hS_top, ENNReal.rpow_one] + _ = ∑ u, ν {u} ^ (a * s) * ν {u} / S ^ s := by + rw [Finset.sum_congr rfl fun u _ ↦ by rw [hpow], ENNReal.sum_div] + _ = ∫⁻ u, π {u} ^ s ∂ν := by + rw [lintegral_fintype] + refine Finset.sum_congr rfl fun u _ ↦ ?_ + rw [hπ, ENNReal.div_rpow_of_nonneg _ _ hs0, ← ENNReal.rpow_mul, + ENNReal.mul_div_right_comm] + +/-- The largest expected gain for the `α`-loss gain `g_α(t) = α / (α - 1) · t ^ ((α - 1) / α)` +is `α / (α - 1) · (∑_u ν(u) ^ α) ^ (1 / α)`. -/ +lemma maxExpGain_alphaGain [Fintype γ] [MeasurableSingletonClass γ] (ν : Measure γ) + [IsFiniteMeasure ν] (ha : 1 < a) : + maxExpGain (fun t ↦ ENNReal.ofReal (a / (a - 1)) * t ^ ((a - 1) / a)) ν = + ENNReal.ofReal (a / (a - 1)) * alphaNorm a ν := by + rw [← iSup_lintegral_rpow_eq ν ha, maxExpGain, ENNReal.mul_iSup] + refine iSup_congr fun π ↦ ?_ + rw [ENNReal.mul_iSup] + exact iSup_congr fun _ ↦ lintegral_const_mul' _ _ ENNReal.ofReal_ne_top + +/-- **Corollary 1** (Kurri–Kosut–Sankar), multiplicative form: for `α > 1`, the supremum over +channels `W = P_{U|X}` of `‖P_U‖_α / ‖Q_U‖_α` is `max_x P(x) / Q(x)`. It is Theorem 1 for the +gain function `g_α(t) = α / (α - 1) · t ^ ((α - 1) / α)`. -/ +theorem iSup_alphaNorm_div_eq [Finite α] [MeasurableSingletonClass α] + [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (ha : 1 < a) : + ⨆ (n : ℕ) (W : Kernel α (Fin n)) (_ : IsMarkovKernel W), + alphaNorm a (W ∘ₘ P) / alphaNorm a (W ∘ₘ Q) = expRenyiDivInf P Q := by + set c := ENNReal.ofReal (a / (a - 1)) + have hc0 : c ≠ 0 := (ENNReal.ofReal_pos.2 (div_pos (by linarith) (by linarith))).ne' + have hct : c ≠ ∞ := ENNReal.ofReal_ne_top + have hs : 0 < (a - 1) / a := div_pos (by linarith) (by linarith) + set g : ℝ≥0∞ → ℝ≥0∞ := fun t ↦ c * t ^ ((a - 1) / a) + have hg0 : g 0 = 0 := by simp [g, ENNReal.zero_rpow_of_pos hs] + have hgc : ContinuousWithinAt g (Set.Iic 1) 0 := + ((ENNReal.continuous_const_mul hct).comp ENNReal.continuous_rpow_const).continuousWithinAt + have hG : ⨆ (q) (_ : q ≤ 1), g q = c := + le_antisymm (iSup₂_le fun q hq ↦ mul_le_of_le_one_right' (ENNReal.rpow_le_one hq hs.le)) + (le_iSup₂_of_le (f := fun q (_ : q ≤ 1) ↦ g q) 1 le_rfl (by simp [g])) + rw [← iSup_maxExpGain_div_eq (g := g) hg0 hgc (hG ▸ hc0) (hG ▸ hct)] + refine iSup_congr fun n ↦ iSup_congr fun W ↦ iSup_congr fun hW ↦ ?_ + rw [maxExpGain_alphaGain _ ha, maxExpGain_alphaGain _ ha, ENNReal.mul_div_mul_left _ _ hc0 hct] + +/-- **Corollary 1** (Kurri–Kosut–Sankar), equation (6): for `α > 1`, +`D∞(P ‖ Q) = sup_{P_{U|X}} log ((∑_u P_U(u) ^ α) ^ (1 / α) / (∑_u Q_U(u) ^ α) ^ (1 / α))`. -/ +theorem iSup_log_alphaNorm_div_eq [Finite α] [MeasurableSingletonClass α] + [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (ha : 1 < a) : + ⨆ (n : ℕ) (W : Kernel α (Fin n)) (_ : IsMarkovKernel W), + ENNReal.log (alphaNorm a (W ∘ₘ P) / alphaNorm a (W ∘ₘ Q)) = renyiDivInf P Q := by + rw [renyiDivInf, ← iSup_alphaNorm_div_eq ha] + simp only [← ENNReal.logOrderIso_apply, OrderIso.map_iSup] + +end AlphaGain + +section Leakage + +/-! ### Theorems 2 and 3: two variants of maximal `α`-leakage + +The input `X ∼ μ` is sent through the channel `κ = P_{Y|X}`; a randomized function `U` of `X` is +given by a channel `ρ = P_{U|X}`, so that `U - X - Y` is a Markov chain, `P_U = ρ ∘ μ` and +`P_{U|Y=y} = ρ ∘ P_{X|Y=y}`. -/ + +variable {μ : Measure α} {κ : Kernel α β} + +/-- The conditional law `P_{X|Y=y}(x) = P_{Y|X}(y | x) P_X(x) / P_Y(y)` of the input `X ∼ μ` +given the output `y` of the channel `κ`. It is a probability measure when `P_Y(y) ≠ 0` +(`isProbabilityMeasure_condInput`) and is only used for such `y`. -/ +noncomputable def condInput (μ : Measure α) (κ : Kernel α β) (y : β) : Measure α := + ((κ ∘ₘ μ) {y})⁻¹ • μ.withDensity fun x ↦ κ x {y} + +lemma condInput_singleton [MeasurableSingletonClass α] (y : β) (x : α) : + condInput μ κ y {x} = ((κ ∘ₘ μ) {y})⁻¹ * (κ x {y} * μ {x}) := by + rw [condInput, smul_apply, withDensity_apply _ (measurableSet_singleton x), + lintegral_singleton, smul_eq_mul] + +lemma isProbabilityMeasure_condInput [Finite α] [MeasurableSingletonClass α] + [MeasurableSingletonClass β] [IsFiniteMeasure μ] [IsMarkovKernel κ] {y : β} + (hy : (κ ∘ₘ μ) {y} ≠ 0) : IsProbabilityMeasure (condInput μ κ y) := ⟨by + have := Fintype.ofFinite α + rw [← Finset.coe_univ, ← sum_measure_singleton] + simp_rw [condInput_singleton, ← Finset.mul_sum, ← comp_apply_singleton] + exact ENNReal.inv_mul_cancel hy (measure_ne_top _ _)⟩ + +/-- `max_x P_{X|Y}(x | y) / P_X(x) = max_{x ∈ supp P_X} P_{Y|X}(y | x) / P_Y(y)` (Bayes' rule, +paper (47)–(48)). -/ +lemma expRenyiDivInf_condInput [MeasurableSingletonClass α] [IsFiniteMeasure μ] (y : β) : + expRenyiDivInf (condInput μ κ y) μ = ((κ ∘ₘ μ) {y})⁻¹ * ⨆ (x) (_ : μ {x} ≠ 0), κ x {y} := by + simp_rw [ENNReal.mul_iSup, expRenyiDivInf] + refine iSup_congr fun x ↦ ?_ + by_cases hx : μ {x} = 0 + · simp [hx, condInput_singleton] + · rw [iSup_pos hx, condInput_singleton, ← mul_assoc, + ENNReal.mul_div_cancel_right hx (measure_ne_top _ _)] + +/-- Corollary 1 applied to `P_{X|Y=y}` and `P_X`: for `α > 1` and `P_Y(y) ≠ 0`, the supremum +over `U - X - Y` of `‖P_{U|Y=y}‖_α / ‖P_U‖_α` is `max_x P_{X|Y}(x | y) / P_X(x)`. -/ +lemma iSup_alphaNorm_condInput_div_eq [Finite α] [MeasurableSingletonClass α] + [MeasurableSingletonClass β] [IsProbabilityMeasure μ] [IsMarkovKernel κ] (ha : 1 < a) + {y : β} (hy : (κ ∘ₘ μ) {y} ≠ 0) : + ⨆ (n : ℕ) (ρ : Kernel α (Fin n)) (_ : IsMarkovKernel ρ), + alphaNorm a (ρ ∘ₘ condInput μ κ y) / alphaNorm a (ρ ∘ₘ μ) = + expRenyiDivInf (condInput μ κ y) μ := by + have := isProbabilityMeasure_condInput hy + exact iSup_alphaNorm_div_eq ha + +lemma iSup_kernel_eq_zero [Finite α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] + {y : β} (hy : (κ ∘ₘ μ) {y} = 0) : ⨆ (x) (_ : μ {x} ≠ 0), κ x {y} = 0 := by + have := Fintype.ofFinite α + rw [comp_apply_singleton, Finset.sum_eq_zero_iff] at hy + refine le_antisymm (iSup₂_le fun x hx ↦ ?_) zero_le + exact ((mul_eq_zero.1 (hy x (Finset.mem_univ x))).resolve_right hx).le + +open Classical in +/-- The sum `∑_{y ∈ supp P_Y} P_Y(y) sup_{U - X - Y} ‖P_{U|Y=y}‖_α / ‖P_U‖_α` whose logarithm, +scaled by `α / (α - 1)`, is the opportunistic maximal `α`-leakage `oppMaxAlphaLeakage`. -/ +noncomputable def oppMaxAlphaLeakageSum [Fintype β] (a : ℝ) (μ : Measure α) (κ : Kernel α β) : + ℝ≥0∞ := + ∑ y with (κ ∘ₘ μ) {y} ≠ 0, (κ ∘ₘ μ) {y} * + ⨆ (n : ℕ) (ρ : Kernel α (Fin n)) (_ : IsMarkovKernel ρ), + alphaNorm a (ρ ∘ₘ condInput μ κ y) / alphaNorm a (ρ ∘ₘ μ) + +/-- The **opportunistic maximal `α`-leakage** `L̃_α^max(X → Y)` (paper, Definition 4, (15)): +`α / (α - 1) · log ∑_{y ∈ supp P_Y} P_Y(y) sup_{U - X - Y} ‖P_{U|Y=y}‖_α / ‖P_U‖_α`, +the supremum ranging over all channels `P_{U|X}` into the alphabets `Fin n`. It is meant for +`α ∈ (1, ∞)`. -/ +noncomputable def oppMaxAlphaLeakage [Fintype β] (a : ℝ) (μ : Measure α) (κ : Kernel α β) : ℝ := + a / (a - 1) * Real.log (oppMaxAlphaLeakageSum a μ κ).toReal + +/-- **Theorem 2** (Kurri–Kosut–Sankar), multiplicative form: for `α > 1`, +`∑_{y ∈ supp P_Y} P_Y(y) sup_{U - X - Y} ‖P_{U|Y=y}‖_α / ‖P_U‖_α` equals +`∑_y max_{x ∈ supp P_X} P_{Y|X}(y | x)`, i.e. `maxLeakageSum μ κ`. -/ +theorem oppMaxAlphaLeakageSum_eq_maxLeakageSum [Finite α] [MeasurableSingletonClass α] + [Fintype β] [MeasurableSingletonClass β] [IsProbabilityMeasure μ] [IsMarkovKernel κ] + (ha : 1 < a) : oppMaxAlphaLeakageSum a μ κ = maxLeakageSum μ κ := by + classical + rw [oppMaxAlphaLeakageSum, maxLeakageSum] + rw [← Finset.sum_filter_of_ne (p := fun y ↦ (κ ∘ₘ μ) {y} ≠ 0) + fun y _ h hy ↦ h (iSup_kernel_eq_zero hy)] + refine Finset.sum_congr rfl fun y hy ↦ ?_ + have hy : (κ ∘ₘ μ) {y} ≠ 0 := (Finset.mem_filter.1 hy).2 + rw [iSup_alphaNorm_condInput_div_eq ha hy, expRenyiDivInf_condInput, ← mul_assoc, + ENNReal.mul_inv_cancel hy (measure_ne_top _ _), one_mul] + +/-- **Theorem 2** (Kurri–Kosut–Sankar), equation (17): for `α > 1`, the opportunistic maximal +`α`-leakage is `α / (α - 1) · I∞ˢ(X; Y)`, where the Sibson mutual information of order `∞`, +`I∞ˢ(X; Y) = log ∑_y max_{x ∈ supp P_X} P_{Y|X}(y | x)` (paper, (12)), is the maximal leakage +`maxLeakage μ κ`. -/ +theorem oppMaxAlphaLeakage_eq [Finite α] [MeasurableSingletonClass α] + [Fintype β] [MeasurableSingletonClass β] [IsProbabilityMeasure μ] [IsMarkovKernel κ] + (ha : 1 < a) : oppMaxAlphaLeakage a μ κ = a / (a - 1) * maxLeakage μ κ := by + rw [oppMaxAlphaLeakage, oppMaxAlphaLeakageSum_eq_maxLeakageSum ha, maxLeakage] + +/-- The **maximal realizable `α`-leakage** `L_α^{r-max}(X → Y)` (paper, Definition 5, (16)): +`sup_{U - X - Y} α / (α - 1) · log max_{y ∈ supp P_Y} ‖P_{U|Y=y}‖_α / ‖P_U‖_α`, +the supremum ranging over all channels `P_{U|X}` into the alphabets `Fin n`. It is meant for +`α ∈ (1, ∞)`, and takes values in `EReal`. -/ +noncomputable def realMaxAlphaLeakage (a : ℝ) (μ : Measure α) (κ : Kernel α β) : EReal := + ⨆ (n : ℕ) (ρ : Kernel α (Fin n)) (_ : IsMarkovKernel ρ), ((a / (a - 1) : ℝ) : EReal) * + ENNReal.log (⨆ (y) (_ : (κ ∘ₘ μ) {y} ≠ 0), + alphaNorm a (ρ ∘ₘ condInput μ κ y) / alphaNorm a (ρ ∘ₘ μ)) + +lemma iSup_coe_mul_log {ι : Sort*} {c : ℝ} (hc : 0 < c) (f : ι → ℝ≥0∞) : + ⨆ i, (c : EReal) * ENNReal.log (f i) = c * ENNReal.log (⨆ i, f i) := by + simp_rw [← ENNReal.log_rpow, ENNReal.iSup_rpow_of_pos hc, ← ENNReal.logOrderIso_apply, + OrderIso.map_iSup] + +lemma compProd_singleton [MeasurableSingletonClass α] [MeasurableSingletonClass β] [SFinite μ] + [IsSFiniteKernel κ] (x : α) (y : β) : (μ ⊗ₘ κ) {(x, y)} = κ x {y} * μ {x} := by + rw [← Set.singleton_prod_singleton, Measure.compProd_apply_prod (measurableSet_singleton x) + (measurableSet_singleton y), lintegral_singleton] + +/-- `max_{y ∈ supp P_Y} max_x P_{X|Y}(x | y) / P_X(x) = max_{x, y} P_XY(x, y) / (P_X(x) P_Y(y))` +(paper, (52)–(53)). -/ +lemma iSup_expRenyiDivInf_condInput [Finite α] [MeasurableSingletonClass α] + [MeasurableSingletonClass β] [IsProbabilityMeasure μ] [IsMarkovKernel κ] : + ⨆ (y) (_ : (κ ∘ₘ μ) {y} ≠ 0), expRenyiDivInf (condInput μ κ y) μ = + expRenyiDivInf (μ ⊗ₘ κ) (μ.prod (κ ∘ₘ μ)) := by + have := Fintype.ofFinite α + rw [expRenyiDivInf, iSup_prod, iSup_comm] + refine iSup_congr fun y ↦ ?_ + by_cases hy : (κ ∘ₘ μ) {y} = 0 + · have h0 (x : α) : κ x {y} * μ {x} = 0 := by + rw [comp_apply_singleton, Finset.sum_eq_zero_iff] at hy + exact hy x (Finset.mem_univ x) + simp [hy, compProd_singleton, h0] + rw [iSup_pos hy, expRenyiDivInf] + refine iSup_congr fun x ↦ ?_ + rw [condInput_singleton, compProd_singleton, ← Set.singleton_prod_singleton, + Measure.prod_prod, ENNReal.div_eq_inv_mul, ENNReal.div_eq_inv_mul, + ENNReal.mul_inv (Or.inr (measure_ne_top _ _)) (Or.inl (measure_ne_top _ _))] + ring + +-- `[Finite β]` is not used in the proof: it keeps the statement in the finite-alphabet setting, +-- where `renyiDivInf` (a supremum over singletons) is the max-divergence. +/-- **Theorem 3** (Kurri–Kosut–Sankar), equation (18): for `α > 1`, the maximal realizable +`α`-leakage is `α / (α - 1) · D∞(P_XY ‖ P_X × P_Y)`, with `P_XY = μ ⊗ₘ κ` and +`P_X × P_Y = μ.prod (κ ∘ₘ μ)`. -/ +@[nolint unusedArguments] +theorem realMaxAlphaLeakage_eq [Finite α] [MeasurableSingletonClass α] [Finite β] + [MeasurableSingletonClass β] [IsProbabilityMeasure μ] [IsMarkovKernel κ] (ha : 1 < a) : + realMaxAlphaLeakage a μ κ = + ((a / (a - 1) : ℝ) : EReal) * renyiDivInf (μ ⊗ₘ κ) (μ.prod (κ ∘ₘ μ)) := by + have hc : 0 < a / (a - 1) := div_pos (by linarith) (by linarith) + set R : (n : ℕ) → Kernel α (Fin n) → β → ℝ≥0∞ := fun n ρ y ↦ + alphaNorm a (ρ ∘ₘ condInput μ κ y) / alphaNorm a (ρ ∘ₘ μ) + have hsup : ⨆ (n : ℕ) (ρ : Kernel α (Fin n)) (_ : IsMarkovKernel ρ), + ⨆ (y) (_ : (κ ∘ₘ μ) {y} ≠ 0), R n ρ y = expRenyiDivInf (μ ⊗ₘ κ) (μ.prod (κ ∘ₘ μ)) := by + rw [← iSup_expRenyiDivInf_condInput] + refine le_antisymm (iSup_le fun n ↦ iSup₂_le fun ρ hρ ↦ iSup₂_le fun y hy ↦ ?_) + (iSup₂_le fun y hy ↦ ?_) + · refine le_iSup₂_of_le (f := fun y (_ : (κ ∘ₘ μ) {y} ≠ 0) ↦ + expRenyiDivInf (condInput μ κ y) μ) y hy ?_ + rw [← iSup_alphaNorm_condInput_div_eq ha hy] + exact le_iSup_of_le n <| le_iSup₂_of_le (f := fun (ρ : Kernel α (Fin n)) + (_ : IsMarkovKernel ρ) ↦ R n ρ y) ρ hρ le_rfl + · rw [← iSup_alphaNorm_condInput_div_eq ha hy] + refine iSup_le fun n ↦ iSup₂_le fun ρ hρ ↦ ?_ + exact le_iSup_of_le n <| le_iSup₂_of_le (f := fun (ρ : Kernel α (Fin n)) + (_ : IsMarkovKernel ρ) ↦ ⨆ (y) (_ : (κ ∘ₘ μ) {y} ≠ 0), R n ρ y) ρ hρ <| + le_iSup₂_of_le (f := fun y (_ : (κ ∘ₘ μ) {y} ≠ 0) ↦ R n ρ y) y hy le_rfl + rw [renyiDivInf, ← hsup, realMaxAlphaLeakage] + simp_rw [iSup_coe_mul_log hc] + rfl + +end Leakage + +end InformationTheory