diff --git a/Statlib.lean b/Statlib.lean index 3ee4ad5..e79916e 100644 --- a/Statlib.lean +++ b/Statlib.lean @@ -1,5 +1,9 @@ import Statlib.Causal.PotentialResponse import Statlib.Contiguity.Def +import Statlib.Divergence.AlphaLeakage.Basic +import Statlib.Divergence.AlphaLeakage.Maximal +import Statlib.Divergence.AlphaLeakage.Operational +import Statlib.Divergence.AlphaLeakage.Properties import Statlib.Divergence.BretagnolleHuber import Statlib.Divergence.Chernoff import Statlib.Divergence.Chernoff.Prod @@ -38,6 +42,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/AlphaLeakage/Basic.lean b/Statlib/Divergence/AlphaLeakage/Basic.lean new file mode 100644 index 0000000..95f8c49 --- /dev/null +++ b/Statlib/Divergence/AlphaLeakage/Basic.lean @@ -0,0 +1,557 @@ +/- +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.Analysis.MeanInequalities +public import Mathlib.Analysis.MeanInequalitiesPow +public import Mathlib.Analysis.SpecialFunctions.Pow.Continuity +public import Mathlib.Topology.Instances.ENNReal.Lemmas +public import Mathlib.Probability.Kernel.Composition.MeasureComp +public import Mathlib.Probability.Kernel.Composition.MeasureCompProd + +/-! +# Sibson and Arimoto mutual information on finite alphabets + +Liao, Kosut, Sankar and Calmon (*Tunable measures for information leakage and applications to +privacy-utility tradeoffs*, IEEE Trans. Inf. Theory 65(12), 2019, arXiv:1809.09231) express their +tunable leakage measures through two Rényi-type generalizations of mutual information. For an +order `a ∈ (1, ∞)`, an input law `P_X` and a channel `P_{Y|X}` on finite alphabets, + +* the **Sibson mutual information** (their eq. (7)) is + `I^S_a(X; Y) = a / (a - 1) · log ∑_y (∑_x P_X(x) P_{Y|X}(y | x) ^ a) ^ (1 / a)`; +* the **Arimoto mutual information** (their eq. (9)) of a joint law `P_{X,Y}` is + `I^A_a(X; Y) = a / (a - 1) · log (∑_y ‖P_{X,Y}(·, y)‖_a / ‖P_X‖_a)`. + +We take these closed forms as definitions; the variational characterization +`I^S_a(X; Y) = min_{Q_Y} D_a(P_{X,Y} ‖ P_X × Q_Y)` of their eq. (6) and the decomposition +`I^A_a = H_a(X) - H^A_a(X | Y)` of their eq. (8) are not formalized. As in +`Statlib.Divergence.MaximalLeakage.Basic`, the definitions come in an `ℝ≥0∞`-valued +multiplicative form (`sibsonSum`, `arimotoSum`) and a real logarithmic form in nats +(`sibsonMI`, `arimotoMI`). + +## Main definitions + +* `sibsonSum a μ κ = ∑_y (∑_x μ {x} * κ x {y} ^ a) ^ a⁻¹` and `sibsonMI a μ κ`, its logarithm + scaled by `a / (a - 1)`. +* `arimotoSum a π` and `arimotoMI a π` for a joint law `π` on `α × β`. +* `escort a μ`: the escort distribution `μ {x} ^ a / ∑_x' μ {x'} ^ a`. + +## Main statements + +* `arimotoSum_compProd`: Arimoto's quantity of `(X, Y)` is Sibson's quantity of the escort + distribution of `X` (the change of variables in eqs. (100)–(103) of the paper). +* `one_le_sibsonSum`, `sibsonMI_nonneg`: Sibson mutual information is nonnegative. +* `sibsonSum_le_maxLeakageSum_rpow`, `sibsonMI_le_maxLeakage`: `I^S_a(X; Y) ≤ L(X → Y)`, which + with Theorem 2 of the paper gives eq. (44). +* `sibsonSum_comp_le`, `sibsonSum_comp_le_comp`: data processing for Sibson mutual information + under post- and pre-processing (used in Theorem 3 of the paper). +* `one_le_arimotoSum`, `arimotoMI_nonneg`: Arimoto mutual information is nonnegative (by + Minkowski's inequality). +* `arimotoMI_compProd_comp_le`: the post-processing inequality for Arimoto mutual information + (footnote 4 of the paper). +* `tendsto_sibsonSum_atTop`, `tendsto_sibsonMI_atTop`: as `a → ∞`, Sibson mutual information + tends to the maximal leakage `maxLeakage μ κ` (eq. (12) of the paper, where `I^S_∞` is defined + by continuous extension). This connects to `Statlib.Divergence.MaximalLeakage`. +* `ENNReal.Lp_finsetSum_le`: Minkowski's inequality for finite sums of vectors in `ℝ≥0∞`. + +## Mapping to Liao–Kosut–Sankar–Calmon + +* eq. (7) (Sibson MI), eq. (9) (Arimoto MI): `sibsonMI`, `arimotoMI` (definitions, `a ∈ (1, ∞)`). +* eq. (12): `tendsto_sibsonMI_atTop`. +* eqs. (100)–(103): `arimotoSum_compProd`. +* Definition 5 and Theorem 1: `Statlib.Divergence.AlphaLeakage.Operational`. +* Definition 6 and Theorem 2: `Statlib.Divergence.AlphaLeakage.Maximal`. +* Theorem 3, eq. (44), Theorem 4: `Statlib.Divergence.AlphaLeakage.Properties`. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory Filter +open scoped ENNReal Topology + +namespace InformationTheory + +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ ν : Measure α} {κ : Kernel α β} {π : Measure (α × β)} {a : ℝ} + +/-- The sum `∑_y (∑_x P_X(x) P_{Y|X}(y | x) ^ a) ^ (1 / a)` whose logarithm, scaled by +`a / (a - 1)`, is the Sibson mutual information `sibsonMI a μ κ`. -/ +noncomputable def sibsonSum [Fintype α] [Fintype β] (a : ℝ) (μ : Measure α) (κ : Kernel α β) : + ℝ≥0∞ := + ∑ y, (∑ x, μ {x} * κ x {y} ^ a) ^ a⁻¹ + +/-- The **Sibson mutual information** of order `a` between an input `X ∼ μ` and the output `Y` of +the channel `κ`, in nats, in the closed form of eq. (7) of Liao–Kosut–Sankar–Calmon: +`I^S_a(X; Y) = a / (a - 1) · log ∑_y (∑_x P_X(x) P_{Y|X}(y | x) ^ a) ^ (1 / a)`. +It is meaningful for `a ∈ (0, 1) ∪ (1, ∞)`; the results of this library are for `a > 1`. -/ +noncomputable def sibsonMI [Fintype α] [Fintype β] (a : ℝ) (μ : Measure α) (κ : Kernel α β) : + ℝ := + a / (a - 1) * Real.log (sibsonSum a μ κ).toReal + +/-- The ratio `∑_y ‖P_{X,Y}(·, y)‖_a / ‖P_X‖_a` whose logarithm, scaled by `a / (a - 1)`, is the +Arimoto mutual information `arimotoMI a π` of a joint law `π = P_{X,Y}`. -/ +noncomputable def arimotoSum [Fintype α] [Fintype β] (a : ℝ) (π : Measure (α × β)) : ℝ≥0∞ := + (∑ y, (∑ x, π {(x, y)} ^ a) ^ a⁻¹) / (∑ x, π.fst {x} ^ a) ^ a⁻¹ + +/-- The **Arimoto mutual information** of order `a` of a joint law `π = P_{X,Y}`, in nats, in the +closed form of eq. (9) of Liao–Kosut–Sankar–Calmon: +`I^A_a(X; Y) = a / (a - 1) · log (∑_y (∑_x P_{X,Y}(x, y) ^ a) ^ (1 / a) / ‖P_X‖_a)`, +where `‖P_X‖_a = (∑_x P_X(x) ^ a) ^ (1 / a)`. +It is meaningful for `a ∈ (0, 1) ∪ (1, ∞)`; the results of this library are for `a > 1`. -/ +noncomputable def arimotoMI [Fintype α] [Fintype β] (a : ℝ) (π : Measure (α × β)) : ℝ := + a / (a - 1) * Real.log (arimotoSum a π).toReal + +/-- The **escort distribution** of order `a` of `μ`, with masses `μ {x} ^ a / ∑_x' μ {x'} ^ a`. +Liao–Kosut–Sankar–Calmon use it (eqs. (100)–(103)) to turn Arimoto into Sibson mutual +information. -/ +noncomputable def escort [Fintype α] (a : ℝ) (μ : Measure α) : Measure α := + (∑ x, μ {x} ^ a)⁻¹ • ∑ x, μ {x} ^ a • Measure.dirac x + +section Singletons + +variable [Fintype α] [MeasurableSingletonClass α] + +lemma sum_smul_dirac_apply_singleton (f : α → ℝ≥0∞) (x : α) : + (∑ x', f x' • Measure.dirac x') {x} = f x := by + simp only [sum_apply, smul_apply, MeasurableSet.singleton, Measure.dirac_apply', smul_eq_mul] + rw [Finset.sum_eq_single x (fun b _ hb ↦ by + simp [Set.indicator_of_notMem (Set.mem_singleton_iff.not.2 hb)]) (by simp)] + simp + +lemma escort_singleton (a : ℝ) (μ : Measure α) (x : α) : + escort a μ {x} = (∑ x', μ {x'} ^ a)⁻¹ * μ {x} ^ a := by + rw [escort, smul_apply, sum_smul_dirac_apply_singleton, smul_eq_mul] + +lemma isProbabilityMeasure_escort (ha : 0 < a) [IsFiniteMeasure μ] (hμ : μ ≠ 0) : + IsProbabilityMeasure (escort a μ) := by + have h_ne : ∑ x, μ {x} ^ a ≠ 0 := by + obtain ⟨x, hx⟩ : ∃ x, μ {x} ≠ 0 := by + by_contra! h + exact hμ (Measure.ext_iff_singleton.2 fun x ↦ by simp [h x]) + exact ne_of_gt <| (ENNReal.rpow_pos (pos_iff_ne_zero.2 hx) (measure_ne_top μ _)).trans_le <| + Finset.single_le_sum (f := fun x ↦ μ {x} ^ a) (fun _ _ ↦ zero_le) (Finset.mem_univ x) + have h_top : ∑ x, μ {x} ^ a ≠ ∞ := ENNReal.sum_ne_top.2 fun x _ ↦ + ENNReal.rpow_ne_top_of_nonneg ha.le (measure_ne_top μ _) + constructor + rw [← Finset.coe_univ, ← sum_measure_singleton] + simp_rw [escort_singleton, ← Finset.mul_sum] + exact ENNReal.inv_mul_cancel h_ne h_top + +lemma escort_absolutelyContinuous (ha : 0 < a) : escort a μ ≪ μ := by + refine fun s hs ↦ (measure_null_iff_singleton s.to_countable).2 fun x hx ↦ ?_ + rw [escort_singleton, (measure_null_iff_singleton s.to_countable).1 hs x hx, + ENNReal.zero_rpow_of_pos ha, mul_zero] + +end Singletons + +section Formulas + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + +omit [Fintype α] [Fintype β] in +lemma compProd_singleton_eq_mul [SFinite μ] [IsSFiniteKernel κ] (x : α) (y : β) : + (μ ⊗ₘ κ) {(x, y)} = μ {x} * κ x {y} := by + rw [← Set.singleton_prod_singleton, Measure.compProd_apply_prod (measurableSet_singleton x) + (measurableSet_singleton y), lintegral_singleton, mul_comm] + +/-- **Arimoto mutual information is Sibson mutual information at the escort input**: +`I^A_a(X; Y) = I^S_a(X_a; Y)` where `X_a` follows the escort distribution `escort a μ` of `X ∼ μ`. +This is the change of variables in eqs. (100)–(103) of Liao–Kosut–Sankar–Calmon. -/ +lemma arimotoSum_compProd [SFinite μ] [IsMarkovKernel κ] (ha : 0 ≤ a) : + arimotoSum a (μ ⊗ₘ κ) = sibsonSum a (escort a μ) κ := by + have ha' : 0 ≤ a⁻¹ := inv_nonneg.2 ha + simp_rw [arimotoSum, sibsonSum, Measure.fst_compProd, compProd_singleton_eq_mul, escort_singleton, + ENNReal.mul_rpow_of_nonneg _ _ ha, mul_assoc, ← Finset.mul_sum, + ENNReal.mul_rpow_of_nonneg _ _ ha', ENNReal.inv_rpow, ← Finset.mul_sum, div_eq_mul_inv, + mul_comm] + +/-- **Arimoto mutual information is Sibson mutual information at the escort input**, eqs. +(100)–(103) of Liao–Kosut–Sankar–Calmon. -/ +lemma arimotoMI_compProd [SFinite μ] [IsMarkovKernel κ] (ha : 0 ≤ a) : + arimotoMI a (μ ⊗ₘ κ) = sibsonMI a (escort a μ) κ := by + rw [arimotoMI, sibsonMI, arimotoSum_compProd ha] + +end Formulas + +section Bounds + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + +omit [MeasurableSingletonClass β] in +lemma sibsonSum_le_card (ha : 0 < a) [IsProbabilityMeasure ν] [IsMarkovKernel κ] : + sibsonSum a ν κ ≤ Fintype.card β := by + have h_y (y : β) : (∑ x, ν {x} * κ x {y} ^ a) ^ a⁻¹ ≤ 1 := by + refine ENNReal.rpow_le_one ?_ (inv_nonneg.2 ha.le) + calc ∑ x, ν {x} * κ x {y} ^ a ≤ ∑ x, ν {x} := + Finset.sum_le_sum fun x _ ↦ + mul_le_of_le_one_right' (ENNReal.rpow_le_one prob_le_one ha.le) + _ = 1 := by simp [sum_measure_singleton] + calc sibsonSum a ν κ ≤ ∑ _y : β, (1 : ℝ≥0∞) := Finset.sum_le_sum fun y _ ↦ h_y y + _ = Fintype.card β := by simp + +omit [MeasurableSingletonClass β] in +lemma sibsonSum_ne_top (ha : 0 < a) [IsProbabilityMeasure ν] [IsMarkovKernel κ] : + sibsonSum a ν κ ≠ ∞ := + ne_top_of_le_ne_top (ENNReal.natCast_ne_top _) (sibsonSum_le_card ha) + +/-- Jensen's inequality gives `∑_y (∑_x P(x) W(y | x) ^ a) ^ (1 / a) ≥ ∑_y ∑_x P(x) W(y | x) = 1` +for `a ≥ 1`. -/ +lemma one_le_sibsonSum (ha : 1 ≤ a) [IsProbabilityMeasure ν] [IsMarkovKernel κ] : + 1 ≤ sibsonSum a ν κ := by + have ha0 : 0 < a := zero_lt_one.trans_le ha + have h_y (y : β) : ∑ x, ν {x} * κ x {y} ≤ (∑ x, ν {x} * κ x {y} ^ a) ^ a⁻¹ := by + have h := ENNReal.rpow_arith_mean_le_arith_mean_rpow Finset.univ (fun x ↦ ν {x}) + (fun x ↦ κ x {y}) (by simp [sum_measure_singleton]) ha + calc ∑ x, ν {x} * κ x {y} = ((∑ x, ν {x} * κ x {y}) ^ a) ^ a⁻¹ := + (ENNReal.rpow_rpow_inv ha0.ne' _).symm + _ ≤ _ := ENNReal.rpow_le_rpow h (inv_nonneg.2 ha0.le) + calc (1 : ℝ≥0∞) = ∑ y, ∑ x, ν {x} * κ x {y} := by + rw [Finset.sum_comm] + simp [← Finset.mul_sum, sum_measure_singleton] + _ ≤ sibsonSum a ν κ := Finset.sum_le_sum fun y _ ↦ h_y y + +lemma one_le_toReal_sibsonSum (ha : 1 ≤ a) [IsProbabilityMeasure ν] [IsMarkovKernel κ] : + 1 ≤ (sibsonSum a ν κ).toReal := by + simpa using (ENNReal.toReal_le_toReal ENNReal.one_ne_top + (sibsonSum_ne_top (zero_lt_one.trans_le ha))).2 (one_le_sibsonSum ha) + +/-- **Nonnegativity of Sibson mutual information** for `a > 1`. -/ +lemma sibsonMI_nonneg (ha : 1 < a) [IsProbabilityMeasure ν] [IsMarkovKernel κ] : + 0 ≤ sibsonMI a ν κ := + mul_nonneg (div_nonneg (by linarith) (by linarith)) + (Real.log_nonneg (one_le_toReal_sibsonSum ha.le)) + +/-- Multiplicative form of `I^S_a(X; Y) ≤ L(X → Y)`: by Hölder's inequality, +`∑_y (∑_x P(x) W(y | x) ^ a) ^ (1 / a) ≤ (∑_y max_{x ∈ supp P} W(y | x)) ^ (1 - 1 / a)`. -/ +lemma sibsonSum_le_maxLeakageSum_rpow (ha : 1 < a) [IsProbabilityMeasure ν] [IsMarkovKernel κ] : + sibsonSum a ν κ ≤ maxLeakageSum ν κ ^ (1 - a⁻¹) := by + have ha0 : 0 < a := zero_lt_one.trans ha + have hb0 : 0 ≤ 1 - a⁻¹ := sub_nonneg.2 (inv_le_one_of_one_le₀ ha.le) + set M : β → ℝ≥0∞ := fun y ↦ ⨆ (x) (_ : ν {x} ≠ 0), κ x {y} + set P : β → ℝ≥0∞ := fun y ↦ ∑ x, ν {x} * κ x {y} + -- Each column: `∑_x P(x) W(y | x) ^ a ≤ M_y ^ (a - 1) * P_Y(y)`. + have h_col (y : β) : ∑ x, ν {x} * κ x {y} ^ a ≤ M y ^ (a - 1) * P y := by + rw [Finset.mul_sum] + refine Finset.sum_le_sum fun x _ ↦ ?_ + by_cases hx : ν {x} = 0 + · simp [hx] + have hle : κ x {y} ≤ M y := le_iSup₂ (f := fun x (_ : ν {x} ≠ 0) ↦ κ x {y}) x hx + calc ν {x} * κ x {y} ^ a = ν {x} * (κ x {y} ^ (a - 1) * κ x {y}) := by + conv_lhs => rw [← sub_add_cancel a 1] + rw [ENNReal.rpow_add_of_nonneg _ _ (by linarith) zero_le_one, ENNReal.rpow_one] + _ ≤ ν {x} * (M y ^ (a - 1) * κ x {y}) := by gcongr + _ = M y ^ (a - 1) * (ν {x} * κ x {y}) := by ring + have h_term (y : β) : (∑ x, ν {x} * κ x {y} ^ a) ^ a⁻¹ ≤ P y ^ a⁻¹ * M y ^ (1 - a⁻¹) := by + calc (∑ x, ν {x} * κ x {y} ^ a) ^ a⁻¹ ≤ (M y ^ (a - 1) * P y) ^ a⁻¹ := + ENNReal.rpow_le_rpow (h_col y) (inv_nonneg.2 ha0.le) + _ = P y ^ a⁻¹ * M y ^ (1 - a⁻¹) := by + rw [ENNReal.mul_rpow_of_nonneg _ _ (inv_nonneg.2 ha0.le), ← ENNReal.rpow_mul, mul_comm] + congr 2 + field_simp + -- Hölder's inequality with the conjugate exponents `a` and `(1 - 1 / a)⁻¹`. + have hpq : a.HolderConjugate (1 - a⁻¹)⁻¹ := by + simpa using Real.HolderConjugate.inv_one_sub_inv (inv_pos.2 ha0) (inv_lt_one_of_one_lt₀ ha) + have hP : ∑ y, P y = 1 := by + simp only [P] + rw [Finset.sum_comm] + simp [← Finset.mul_sum, sum_measure_singleton] + calc sibsonSum a ν κ ≤ ∑ y, P y ^ a⁻¹ * M y ^ (1 - a⁻¹) := Finset.sum_le_sum fun y _ ↦ h_term y + _ ≤ (∑ y, (P y ^ a⁻¹) ^ a) ^ (1 / a) * + (∑ y, (M y ^ (1 - a⁻¹)) ^ (1 - a⁻¹)⁻¹) ^ (1 / (1 - a⁻¹)⁻¹) := + ENNReal.inner_le_Lp_mul_Lq _ _ _ hpq + _ = maxLeakageSum ν κ ^ (1 - a⁻¹) := by + have hb : 1 - a⁻¹ ≠ 0 := (sub_pos.2 (inv_lt_one_of_one_lt₀ ha)).ne' + simp_rw [ENNReal.rpow_inv_rpow ha0.ne', ← ENNReal.rpow_mul, mul_inv_cancel₀ hb, + ENNReal.rpow_one, hP, one_div, inv_inv, ENNReal.one_rpow, one_mul] + rfl + +/-- **Sibson mutual information is at most maximal leakage**: `I^S_a(X; Y) ≤ L(X → Y)` for +`a > 1`. Together with Theorem 2 this gives eq. (44) of Liao–Kosut–Sankar–Calmon. -/ +lemma sibsonMI_le_maxLeakage (ha : 1 < a) [IsProbabilityMeasure ν] [IsMarkovKernel κ] : + sibsonMI a ν κ ≤ maxLeakage ν κ := by + have ha0 : 0 < a := zero_lt_one.trans ha + have hb : 0 < 1 - a⁻¹ := sub_pos.2 (inv_lt_one_of_one_lt₀ ha) + obtain ⟨x, hx⟩ : ∃ x, ν {x} ≠ 0 := by + by_contra! h + have := sum_measure_singleton (μ := ν) (s := Finset.univ) + simp [h] at this + have hL := one_le_toReal_maxLeakageSum (κ := κ) hx + have h_le : (sibsonSum a ν κ).toReal ≤ (maxLeakageSum ν κ).toReal ^ (1 - a⁻¹) := by + rw [ENNReal.toReal_rpow] + exact ENNReal.toReal_mono (ENNReal.rpow_ne_top_of_nonneg hb.le maxLeakageSum_ne_top) + (sibsonSum_le_maxLeakageSum_rpow ha) + have h_log := Real.log_le_log (by linarith [one_le_toReal_sibsonSum (ν := ν) (κ := κ) ha.le]) + h_le + rw [Real.log_rpow (by linarith)] at h_log + calc sibsonMI a ν κ ≤ a / (a - 1) * ((1 - a⁻¹) * Real.log (maxLeakageSum ν κ).toReal) := + mul_le_mul_of_nonneg_left h_log (div_nonneg ha0.le (by linarith)) + _ = maxLeakage ν κ := by + rw [maxLeakage, ← mul_assoc] + convert one_mul _ using 2 + field_simp + +end Bounds + +section DataProcessing + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + [Fintype γ] [MeasurableSingletonClass γ] + +omit [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] [Fintype γ] + [MeasurableSingletonClass γ] in +/-- **Minkowski's inequality** for a finite sum of nonnegative vectors: +`‖∑_i f_i‖_p ≤ ∑_i ‖f_i‖_p` for `p ≥ 1`. -/ +lemma _root_.ENNReal.Lp_finsetSum_le {ι ι' : Type*} (s : Finset ι) (t : Finset ι') + (f : ι → ι' → ℝ≥0∞) {p : ℝ} (hp : 1 ≤ p) : + (∑ j ∈ t, (∑ i ∈ s, f i j) ^ p) ^ (1 / p) ≤ ∑ i ∈ s, (∑ j ∈ t, f i j ^ p) ^ (1 / p) := by + classical + induction s using Finset.induction_on with + | empty => + have hp0 : 0 < p := zero_lt_one.trans_le hp + simp [ENNReal.zero_rpow_of_pos hp0, hp0] + | insert i s hi ih => + simp_rw [Finset.sum_insert hi] + exact (ENNReal.Lp_add_le t (fun j ↦ f i j) (fun j ↦ ∑ i ∈ s, f i j) hp).trans + (add_le_add le_rfl ih) + +omit [Fintype α] [MeasurableSingletonClass α] [Fintype γ] in +lemma kernel_comp_singleton_eq_sum (η : Kernel β γ) (x : α) (z : γ) : + (η ∘ₖ κ) x {z} = ∑ y, η y {z} * κ x {y} := by + rw [Kernel.comp_apply' _ _ _ (measurableSet_singleton z), lintegral_fintype] + +omit [Fintype β] [Fintype γ] [MeasurableSingletonClass γ] in +lemma measure_bind_singleton_eq_sum (μ : Measure α) (κ : Kernel α β) (y : β) : + (κ ∘ₘ μ) {y} = ∑ x, κ x {y} * μ {x} := by + rw [Measure.bind_apply (measurableSet_singleton y) κ.aemeasurable, lintegral_fintype] + +omit [MeasurableSingletonClass α] in +/-- **Data processing** for Sibson mutual information, multiplicative form: post-processing the +channel output through a Markov kernel `η` cannot increase `sibsonSum`. This is Minkowski's +inequality for the `a`-norms of the vectors `(P(x) ^ (1 / a) W(y | x))_x`. -/ +lemma sibsonSum_comp_le (ha : 1 ≤ a) (η : Kernel β γ) [IsMarkovKernel η] : + sibsonSum a ν (η ∘ₖ κ) ≤ sibsonSum a ν κ := by + have ha0 : 0 < a := zero_lt_one.trans_le ha + have hinv : 0 ≤ a⁻¹ := inv_nonneg.2 ha0.le + set T : β → ℝ≥0∞ := fun y ↦ (∑ x, ν {x} * κ x {y} ^ a) ^ a⁻¹ + have h_z (z : γ) : (∑ x, ν {x} * (η ∘ₖ κ) x {z} ^ a) ^ a⁻¹ ≤ ∑ y, η y {z} * T y := by + have h_eq (x : α) : ν {x} * (η ∘ₖ κ) x {z} ^ a = + (∑ y, ν {x} ^ a⁻¹ * (η y {z} * κ x {y})) ^ a := by + rw [kernel_comp_singleton_eq_sum, ← Finset.mul_sum, ENNReal.mul_rpow_of_nonneg _ _ ha0.le, + ENNReal.rpow_inv_rpow ha0.ne'] + have h_norm (y : β) : (∑ x, (ν {x} ^ a⁻¹ * (η y {z} * κ x {y})) ^ a) ^ (1 / a) = + η y {z} * T y := by + simp_rw [ENNReal.mul_rpow_of_nonneg _ _ ha0.le, ENNReal.rpow_inv_rpow ha0.ne'] + have : ∀ x, ν {x} * (η y {z} ^ a * κ x {y} ^ a) = η y {z} ^ a * (ν {x} * κ x {y} ^ a) := + fun x ↦ by ring + simp_rw [this, ← Finset.mul_sum, one_div, ENNReal.mul_rpow_of_nonneg _ _ hinv, + ENNReal.rpow_rpow_inv ha0.ne'] + rfl + simp_rw [h_eq] + calc (∑ x, (∑ y, ν {x} ^ a⁻¹ * (η y {z} * κ x {y})) ^ a) ^ a⁻¹ + = (∑ x, (∑ y, ν {x} ^ a⁻¹ * (η y {z} * κ x {y})) ^ a) ^ (1 / a) := by rw [one_div] + _ ≤ ∑ y, (∑ x, (ν {x} ^ a⁻¹ * (η y {z} * κ x {y})) ^ a) ^ (1 / a) := + ENNReal.Lp_finsetSum_le Finset.univ Finset.univ + (fun y x ↦ ν {x} ^ a⁻¹ * (η y {z} * κ x {y})) ha + _ = ∑ y, η y {z} * T y := Finset.sum_congr rfl fun y _ ↦ h_norm y + calc sibsonSum a ν (η ∘ₖ κ) ≤ ∑ z, ∑ y, η y {z} * T y := Finset.sum_le_sum fun z _ ↦ h_z z + _ = ∑ y, (∑ z, η y {z}) * T y := by + rw [Finset.sum_comm] + simp_rw [Finset.sum_mul] + _ = sibsonSum a ν κ := by simp [sum_measure_singleton, sibsonSum, T] + +/-- **Data processing** for Sibson mutual information under pre-processing, multiplicative form: +for a Markov chain `X - Y - Z`, `I^S_a(X; Z) ≤ I^S_a(Y; Z)`, where `Y ∼ κ ∘ₘ ν`. This is Jensen's +inequality for `t ↦ t ^ a`. -/ +lemma sibsonSum_comp_le_comp (ha : 1 ≤ a) [IsMarkovKernel κ] (η : Kernel β γ) : + sibsonSum a ν (η ∘ₖ κ) ≤ sibsonSum a (κ ∘ₘ ν) η := by + have ha0 : 0 < a := zero_lt_one.trans_le ha + refine Finset.sum_le_sum fun z _ ↦ ENNReal.rpow_le_rpow ?_ (inv_nonneg.2 ha0.le) + calc ∑ x, ν {x} * (η ∘ₖ κ) x {z} ^ a ≤ ∑ x, ν {x} * ∑ y, κ x {y} * η y {z} ^ a := by + gcongr with x + rw [kernel_comp_singleton_eq_sum] + simp_rw [mul_comm (η _ {z})] + exact ENNReal.rpow_arith_mean_le_arith_mean_rpow _ _ _ (by simp [sum_measure_singleton]) + ha + _ = ∑ y, (κ ∘ₘ ν) {y} * η y {z} ^ a := by + simp_rw [measure_bind_singleton_eq_sum, Finset.mul_sum, Finset.sum_mul] + rw [Finset.sum_comm] + exact Finset.sum_congr rfl fun y _ ↦ Finset.sum_congr rfl fun x _ ↦ by ring + +end DataProcessing + +section Arimoto + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + [Fintype γ] [MeasurableSingletonClass γ] + +omit [Fintype α] [Fintype γ] [MeasurableSingletonClass γ] in +lemma fst_singleton_eq_sum (π : Measure (α × β)) (x : α) : π.fst {x} = ∑ y, π {(x, y)} := by + classical + have h : Prod.fst ⁻¹' {x} = ((Finset.univ.image fun y : β ↦ (x, y) : Finset (α × β)) : + Set (α × β)) := by + ext ⟨x', y⟩ + simp [eq_comm] + rw [Measure.fst_apply (measurableSet_singleton x), h, ← sum_measure_singleton, + Finset.sum_image fun y _ y' _ h ↦ (Prod.mk.inj h).2] + +omit [Fintype β] [MeasurableSingletonClass β] [Fintype γ] [MeasurableSingletonClass γ] in +lemma sum_rpow_fst_singleton_ne_zero (ha : 0 < a) [IsProbabilityMeasure π] : + ∑ x, π.fst {x} ^ a ≠ 0 := by + obtain ⟨x, hx⟩ : ∃ x, π.fst {x} ≠ 0 := by + by_contra! h + have := sum_measure_singleton (μ := π.fst) (s := Finset.univ) + simp [h] at this + exact ne_of_gt <| (pos_iff_ne_zero.2 ((ENNReal.rpow_eq_zero_iff_of_pos ha).not.2 hx)).trans_le + (Finset.single_le_sum (f := fun x ↦ π.fst {x} ^ a) (fun _ _ ↦ zero_le) (Finset.mem_univ x)) + +omit [MeasurableSingletonClass β] [Fintype γ] [MeasurableSingletonClass γ] in +lemma arimotoSum_ne_top (ha : 0 < a) [IsProbabilityMeasure π] : arimotoSum a π ≠ ∞ := by + refine ENNReal.div_ne_top (ENNReal.sum_ne_top.2 fun y _ ↦ + ENNReal.rpow_ne_top_of_nonneg (inv_nonneg.2 ha.le) (ENNReal.sum_ne_top.2 fun x _ ↦ + ENNReal.rpow_ne_top_of_nonneg ha.le (measure_ne_top _ _))) ?_ + exact (ENNReal.rpow_eq_zero_iff_of_pos (inv_pos.2 ha)).not.2 + (sum_rpow_fst_singleton_ne_zero ha) + +omit [Fintype γ] [MeasurableSingletonClass γ] in +/-- By Minkowski's inequality `‖P_X‖_a = ‖∑_y P_{X,Y}(·, y)‖_a ≤ ∑_y ‖P_{X,Y}(·, y)‖_a`, so +`arimotoSum a π ≥ 1`. -/ +lemma one_le_arimotoSum (ha : 1 ≤ a) [IsProbabilityMeasure π] : 1 ≤ arimotoSum a π := by + have ha0 : 0 < a := zero_lt_one.trans_le ha + have hD0 : (∑ x, π.fst {x} ^ a) ^ a⁻¹ ≠ 0 := + (ENNReal.rpow_eq_zero_iff_of_pos (inv_pos.2 ha0)).not.2 (sum_rpow_fst_singleton_ne_zero ha0) + have hDtop : (∑ x, π.fst {x} ^ a) ^ a⁻¹ ≠ ∞ := + ENNReal.rpow_ne_top_of_nonneg (inv_nonneg.2 ha0.le) (ENNReal.sum_ne_top.2 fun x _ ↦ + ENNReal.rpow_ne_top_of_nonneg ha0.le (measure_ne_top _ _)) + rw [arimotoSum, ENNReal.le_div_iff_mul_le (Or.inl hD0) (Or.inl hDtop), one_mul] + simp_rw [fst_singleton_eq_sum] + simpa only [one_div] using + ENNReal.Lp_finsetSum_le Finset.univ Finset.univ (fun y x ↦ π {(x, y)}) ha + +omit [Fintype γ] [MeasurableSingletonClass γ] in +lemma one_le_toReal_arimotoSum (ha : 1 ≤ a) [IsProbabilityMeasure π] : + 1 ≤ (arimotoSum a π).toReal := by + simpa using (ENNReal.toReal_le_toReal ENNReal.one_ne_top + (arimotoSum_ne_top (zero_lt_one.trans_le ha))).2 (one_le_arimotoSum ha) + +omit [Fintype γ] [MeasurableSingletonClass γ] in +/-- **Nonnegativity of Arimoto mutual information** for `a > 1`. -/ +lemma arimotoMI_nonneg (ha : 1 < a) [IsProbabilityMeasure π] : 0 ≤ arimotoMI a π := + mul_nonneg (div_nonneg (by linarith) (by linarith)) + (Real.log_nonneg (one_le_toReal_arimotoSum ha.le)) + +/-- **Post-processing inequality** for Arimoto mutual information, multiplicative form: for a +Markov chain `X - Y - Z`, `I^A_a(X; Z) ≤ I^A_a(X; Y)`. -/ +lemma arimotoSum_compProd_comp_le (ha : 1 ≤ a) [SFinite μ] [IsMarkovKernel κ] (η : Kernel β γ) + [IsMarkovKernel η] : arimotoSum a (μ ⊗ₘ (η ∘ₖ κ)) ≤ arimotoSum a (μ ⊗ₘ κ) := by + have ha0 : 0 ≤ a := zero_le_one.trans ha + rw [arimotoSum_compProd ha0, arimotoSum_compProd ha0] + exact sibsonSum_comp_le ha η + +/-- **Post-processing inequality** for Arimoto mutual information (footnote 4 of +Liao–Kosut–Sankar–Calmon): for a Markov chain `X - Y - Z` and `a > 1`, `I^A_a(X; Z) ≤ I^A_a(X; Y)`. +-/ +lemma arimotoMI_compProd_comp_le (ha : 1 < a) [IsProbabilityMeasure μ] [IsMarkovKernel κ] + (η : Kernel β γ) [IsMarkovKernel η] : arimotoMI a (μ ⊗ₘ (η ∘ₖ κ)) ≤ arimotoMI a (μ ⊗ₘ κ) := by + refine mul_le_mul_of_nonneg_left (Real.log_le_log ?_ ?_) (div_nonneg (by linarith) (by linarith)) + · linarith [one_le_toReal_arimotoSum (π := μ ⊗ₘ (η ∘ₖ κ)) ha.le] + · exact ENNReal.toReal_mono (arimotoSum_ne_top (zero_lt_one.trans ha)) + (arimotoSum_compProd_comp_le ha.le η) + +end Arimoto + +section Limit + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + +omit [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] [Fintype β] + [MeasurableSingletonClass β] in +/-- `c ^ (1 / a) → 1` as `a → ∞`, for `0 < c < ∞`. -/ +lemma _root_.ENNReal.tendsto_rpow_inv_atTop_nhds_one {c : ℝ≥0∞} (hc0 : c ≠ 0) (hc : c ≠ ∞) : + Tendsto (fun a : ℝ ↦ c ^ a⁻¹) atTop (𝓝 1) := by + lift c to NNReal using hc + have hc' : (0 : ℝ) < c := by simpa [pos_iff_ne_zero] using hc0 + have h := ENNReal.tendsto_ofReal + (((Real.continuousAt_const_rpow hc'.ne').tendsto).comp tendsto_inv_atTop_zero) + rw [Function.comp_def, Real.rpow_zero, ENNReal.ofReal_one] at h + refine h.congr fun a ↦ ?_ + rw [← ENNReal.ofReal_rpow_of_pos hc', ENNReal.ofReal_coe_nnreal] + +omit [Fintype β] [MeasurableSingletonClass β] in +/-- As `a → ∞`, the `a`-norm `(∑_x P(x) W(y | x) ^ a) ^ (1 / a)` of a column of the channel, +weighted by the input law, tends to the column maximum over the support of the input. -/ +lemma tendsto_rpow_inv_sum_atTop [IsProbabilityMeasure ν] (y : β) : + Tendsto (fun a : ℝ ↦ (∑ x, ν {x} * κ x {y} ^ a) ^ a⁻¹) atTop + (𝓝 (⨆ (x) (_ : ν {x} ≠ 0), κ x {y})) := by + classical + 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 + obtain ⟨x₀, hx₀S, hx₀⟩ := S.exists_max_image (fun x ↦ κ x {y}) hS + have hx₀' : ν {x₀} ≠ 0 := by simpa [S] using hx₀S + set M := ⨆ (x) (_ : ν {x} ≠ 0), κ x {y} + have hM : M = κ x₀ {y} := + le_antisymm (iSup₂_le fun x hx ↦ hx₀ x (by simpa [S] using hx)) + (le_iSup₂ (f := fun x (_ : ν {x} ≠ 0) ↦ κ x {y}) x₀ hx₀') + have h_up (a : ℝ) (ha : 0 < a) : (∑ x, ν {x} * κ x {y} ^ a) ^ a⁻¹ ≤ M := by + calc (∑ x, ν {x} * κ x {y} ^ a) ^ a⁻¹ ≤ (∑ x, ν {x} * M ^ a) ^ a⁻¹ := by + refine ENNReal.rpow_le_rpow (Finset.sum_le_sum fun x _ ↦ ?_) (inv_nonneg.2 ha.le) + by_cases hx : ν {x} = 0 + · simp [hx] + · gcongr + exact le_iSup₂ (f := fun x (_ : ν {x} ≠ 0) ↦ κ x {y}) x hx + _ = M := by + rw [← Finset.sum_mul, sum_measure_singleton, Finset.coe_univ, measure_univ, one_mul, + ENNReal.rpow_rpow_inv ha.ne'] + have h_low (a : ℝ) (ha : 0 < a) : ν {x₀} ^ a⁻¹ * M ≤ (∑ x, ν {x} * κ x {y} ^ a) ^ a⁻¹ := by + calc ν {x₀} ^ a⁻¹ * M = (ν {x₀} * κ x₀ {y} ^ a) ^ a⁻¹ := by + rw [ENNReal.mul_rpow_of_nonneg _ _ (inv_nonneg.2 ha.le), ENNReal.rpow_rpow_inv ha.ne', + hM] + _ ≤ _ := ENNReal.rpow_le_rpow (Finset.single_le_sum (f := fun x ↦ ν {x} * κ x {y} ^ a) + (fun _ _ ↦ zero_le) (Finset.mem_univ x₀)) (inv_nonneg.2 ha.le) + have h_lim : Tendsto (fun a : ℝ ↦ ν {x₀} ^ a⁻¹ * M) atTop (𝓝 M) := by + simpa using ENNReal.Tendsto.mul_const + (ENNReal.tendsto_rpow_inv_atTop_nhds_one hx₀' (measure_ne_top ν _)) (Or.inl one_ne_zero) + exact tendsto_of_tendsto_of_tendsto_of_le_of_le' h_lim tendsto_const_nhds + ((eventually_gt_atTop 0).mono h_low) ((eventually_gt_atTop 0).mono h_up) + +omit [MeasurableSingletonClass β] in +/-- As `a → ∞`, `sibsonSum a ν κ` tends to `maxLeakageSum ν κ = ∑_y max_{x ∈ supp ν} κ x {y}`. -/ +theorem tendsto_sibsonSum_atTop [IsProbabilityMeasure ν] : + Tendsto (fun a ↦ sibsonSum a ν κ) atTop (𝓝 (maxLeakageSum ν κ)) := + tendsto_finsetSum _ fun y _ ↦ tendsto_rpow_inv_sum_atTop y + +/-- **Sibson mutual information of order `∞` is maximal leakage**: as `a → ∞`, `I^S_a(X; Y)` +tends to `L(X → Y) = log ∑_y max_{x ∈ supp P_X} P_{Y|X}(y | x)`. This is eq. (12) of +Liao–Kosut–Sankar–Calmon, where `I^S_∞` is defined by continuous extension. -/ +theorem tendsto_sibsonMI_atTop [IsProbabilityMeasure ν] [IsMarkovKernel κ] : + Tendsto (fun a ↦ sibsonMI a ν κ) atTop (𝓝 (maxLeakage ν κ)) := by + obtain ⟨x, hx⟩ : ∃ x, ν {x} ≠ 0 := by + by_contra! h + have := sum_measure_singleton (μ := ν) (s := Finset.univ) + simp [h] at this + have h1 : Tendsto (fun a : ℝ ↦ a / (a - 1)) atTop (𝓝 1) := by + have h : Tendsto (fun a : ℝ ↦ 1 + (a - 1)⁻¹) atTop (𝓝 (1 + 0)) := + (tendsto_inv_atTop_zero.comp (tendsto_atTop_add_const_right _ (-1) tendsto_id)).const_add 1 + rw [add_zero] at h + refine h.congr' ?_ + filter_upwards [eventually_gt_atTop 1] with a ha + have : a - 1 ≠ 0 := by linarith + field_simp + ring + have h2 : Tendsto (fun a ↦ Real.log (sibsonSum a ν κ).toReal) atTop (𝓝 (maxLeakage ν κ)) := + ((ENNReal.tendsto_toReal maxLeakageSum_ne_top).comp tendsto_sibsonSum_atTop).log + (by linarith [one_le_toReal_maxLeakageSum (κ := κ) hx]) + simpa only [sibsonMI, one_mul] using h1.mul h2 + +end Limit + +end InformationTheory diff --git a/Statlib/Divergence/AlphaLeakage/Maximal.lean b/Statlib/Divergence/AlphaLeakage/Maximal.lean new file mode 100644 index 0000000..4de731a --- /dev/null +++ b/Statlib/Divergence/AlphaLeakage/Maximal.lean @@ -0,0 +1,641 @@ +/- +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.AlphaLeakage.Operational +public import Mathlib.Probability.Kernel.Composition.Prod +public import Mathlib.Topology.Order.IntermediateValue + +/-! +# Maximal α-leakage and the Arimoto–Sibson capacity + +Liao, Kosut, Sankar and Calmon (*Tunable measures for information leakage and applications to +privacy-utility tradeoffs*, IEEE Trans. Inf. Theory 65(12), 2019, arXiv:1809.09231; journal +version of *A tunable measure for information leakage*, ISIT 2018, arXiv:1806.03332) define the +**maximal α-leakage** (their Definition 6) as the largest α-leakage about any randomized function +of the data: `L^max_a(X → Y) = sup_{U - X - Y} L_a(U → Y)`, the supremum ranging over all random +variables `U` on finite alphabets forming a Markov chain `U - X - Y`. Their Theorem 2 evaluates it +for `a ∈ (1, ∞)` as a channel capacity: +`L^max_a(X → Y) = sup_{P_X̃ ≪ P_X} I^S_a(X̃; Y) = sup_{P_X̃ ≪ P_X} I^A_a(X̃; Y)`. + +We formalize the definition, with `U` ranging over the alphabets `Fin n` (any finite alphabet +reduces to these, `alphaLeakageRatio_le_maxAlphaLeakageRatio`), and prove Theorem 2 for +`a ∈ (1, ∞)` and finite alphabets. + +* **Converse** (`arimotoSum_joint_le`). By Theorem 1, `L_a(U → Y) = I^A_a(U; Y)`; a weighted + Hölder inequality bounds `I^A_a(U; Y)` by `I^S_a(X̃; Y)` for an explicit `P_X̃ ≪ P_X`. +* **Achievability** (`exists_arimotoSum_joint_eq`, `sibsonSum_le_maxAlphaLeakageRatio`). For + `P_X̃` charging every atom of `P_X`, the paper's construction `U = (X, J)` (eqs. (104)–(109)) + attains `I^S_a(X̃; Y)` exactly; the conditional law of the label `J` is found with the + intermediate value theorem, a step the paper leaves implicit. A general `P_X̃ ≪ P_X` is reached + by mixing it with `P_X`, which is why the supremum need not be attained. + +## Main definitions + +* `maxAlphaLeakageRatio a μ κ`, `maxAlphaLeakage a μ κ`: maximal α-leakage (Definition 6), in + multiplicative form and in nats. +* `sibsonCapacitySum a μ κ`: `sup_{ν ≪ μ} sibsonSum a ν κ`. + +## Main statements + +* `maxAlphaLeakageRatio_eq_sibsonCapacitySum`, `isLUB_sibsonMI`: **Theorem 2**, Sibson form of + eq. (31a), `L^max_a(X → Y) = sup_{P_X̃ ≪ P_X} I^S_a(X̃; Y)`. +* `maxAlphaLeakageRatio_eq_iSup_arimotoSum`: **Theorem 2**, Arimoto form of eq. (31a), + `L^max_a(X → Y) = sup_{P_X̃ ≪ P_X} I^A_a(X̃; Y)`. +* `isLUB_alphaLeakage`: Definition 6 in its original form, `maxAlphaLeakage a μ κ` is the least + upper bound of the α-leakages `L_a(U → Y)`. +* `escort_escort_inv`: the escort operations of orders `a` and `1 / a` are inverse to each other. + +The case `a = 1` of Theorem 2 (eq. (31b), mutual information) is not formalized; the case +`a = ∞` is `tendsto_maxAlphaLeakage_atTop` in `Statlib.Divergence.AlphaLeakage.Properties`. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory Filter Set +open scoped ENNReal Topology + +namespace InformationTheory + +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ ν : Measure α} {κ : Kernel α β} {ρ : Kernel α γ} {a : ℝ} + +/-- The multiplicative form of the maximal α-leakage of Definition 6 of +Liao–Kosut–Sankar–Calmon: the supremum of `alphaLeakageRatio a P_{U,Y}` over all randomized +functions `U` of `X ∼ μ` (Markov kernels `ρ : α → Fin n`, for every `n`), where `U` and the output +`Y` of the channel `κ` are conditionally independent given `X`. -/ +noncomputable def maxAlphaLeakageRatio (a : ℝ) (μ : Measure α) (κ : Kernel α β) : ℝ≥0∞ := + ⨆ (n : ℕ) (ρ : Kernel α (Fin n)) (_ : IsMarkovKernel ρ), alphaLeakageRatio a ((ρ ×ₖ κ) ∘ₘ μ) + +/-- The **maximal α-leakage** `L^max_a(X → Y)` of Definition 6 of Liao–Kosut–Sankar–Calmon, for +`a ∈ (1, ∞)`, in nats: `a / (a - 1) · log` of `maxAlphaLeakageRatio a μ κ`, that is, the +supremum of the α-leakages `L_a(U → Y)` over all Markov chains `U - X - Y` with `U` on a finite +alphabet (see `isLUB_alphaLeakage` for this form). -/ +noncomputable def maxAlphaLeakage (a : ℝ) (μ : Measure α) (κ : Kernel α β) : ℝ := + a / (a - 1) * Real.log (maxAlphaLeakageRatio a μ κ).toReal + +/-- `sup_{P_X̃ ≪ P_X} ∑_y (∑_x P_X̃(x) P_{Y|X}(y | x) ^ a) ^ (1 / a)`, the multiplicative form of +the Sibson capacity of order `a` of the channel `κ` with inputs supported in the support of `μ`. -/ +noncomputable def sibsonCapacitySum [Fintype α] [Fintype β] (a : ℝ) (μ : Measure α) + (κ : Kernel α β) : ℝ≥0∞ := + ⨆ (ν : Measure α) (_ : IsProbabilityMeasure ν) (_ : ν ≪ μ), sibsonSum a ν κ + +section Joint + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + [Fintype γ] [MeasurableSingletonClass γ] + +omit [Fintype β] [Fintype γ] in +/-- The joint law of `(U, Y)` when `X ∼ μ`, `U ∼ ρ(X)` and `Y ∼ κ(X)`. -/ +lemma kernelProd_bind_singleton [IsMarkovKernel ρ] [IsMarkovKernel κ] (u : γ) (y : β) : + ((ρ ×ₖ κ) ∘ₘ μ) {(u, y)} = ∑ x, ρ x {u} * κ x {y} * μ {x} := by + rw [Measure.bind_apply (measurableSet_singleton _) (ρ ×ₖ κ).aemeasurable, lintegral_fintype] + simp_rw [Kernel.prod_apply, ← Set.singleton_prod_singleton, Measure.prod_prod] + +omit [Fintype β] [Fintype γ] in +lemma kernelProd_bind_fst_singleton [Finite β] [IsMarkovKernel ρ] [IsMarkovKernel κ] (u : γ) : + ((ρ ×ₖ κ) ∘ₘ μ).fst {u} = ∑ x, ρ x {u} * μ {x} := by + have := Fintype.ofFinite β + rw [fst_singleton_eq_sum] + simp_rw [kernelProd_bind_singleton] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun x _ ↦ ?_ + rw [← Finset.sum_mul, ← Finset.mul_sum, sum_measure_singleton, Finset.coe_univ, measure_univ, + mul_one] + +omit [Fintype β] [MeasurableSingletonClass β] in +lemma sum_joint_fst_singleton [IsProbabilityMeasure μ] [IsMarkovKernel ρ] : + ∑ u, ∑ x, ρ x {u} * μ {x} = 1 := by + rw [Finset.sum_comm] + simp_rw [← Finset.sum_mul, sum_measure_singleton, Finset.coe_univ, measure_univ, one_mul] + simp [sum_measure_singleton] + +omit [Fintype β] [MeasurableSingletonClass β] in +lemma sum_rpow_joint_fst_ne_zero (ha : 0 < a) [IsProbabilityMeasure μ] [IsMarkovKernel ρ] : + ∑ u, (∑ x, ρ x {u} * μ {x}) ^ a ≠ 0 := by + obtain ⟨u, hu⟩ : ∃ u, ∑ x, ρ x {u} * μ {x} ≠ 0 := by + by_contra! h + have h1 := sum_joint_fst_singleton (μ := μ) (ρ := ρ) + simp [h] at h1 + exact ne_of_gt <| (pos_iff_ne_zero.2 ((ENNReal.rpow_eq_zero_iff_of_pos ha).not.2 hu)).trans_le + (Finset.single_le_sum (f := fun u ↦ (∑ x, ρ x {u} * μ {x}) ^ a) (fun _ _ ↦ zero_le) + (Finset.mem_univ u)) + +end Joint + +section UpperBound + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + [Fintype γ] [MeasurableSingletonClass γ] + +/-- **Converse half of Theorem 2** of Liao–Kosut–Sankar–Calmon: for a Markov chain `U - X - Y`, +`I^A_a(U; Y) ≤ sup_{P_X̃ ≪ P_X} I^S_a(X̃; Y)`. Writing `P_U(u) = ∑_x ρ x {u} μ {x}`, the weighted +Hölder inequality gives `P_{U,Y}(u, y) ^ a ≤ P_U(u) ^ (a - 1) ∑_x ρ x {u} μ {x} κ x {y} ^ a`, and +the right-hand side summed over `u` is `(∑_u P_U(u) ^ a) ∑_x P_X̃(x) κ x {y} ^ a` for the input law +`P_X̃(x) ∝ μ {x} ∑_u P_U(u) ^ (a - 1) ρ x {u}`, which is supported in the support of `μ`. This +replaces the escort change of variables and data-processing argument of eqs. (94)–(103). -/ +lemma arimotoSum_joint_le (ha : 1 < a) [IsProbabilityMeasure μ] [IsMarkovKernel κ] + (ρ : Kernel α γ) [IsMarkovKernel ρ] : + arimotoSum a ((ρ ×ₖ κ) ∘ₘ μ) ≤ sibsonCapacitySum a μ κ := by + have ha0 : 0 < a := zero_lt_one.trans ha + have hinv : 0 ≤ a⁻¹ := inv_nonneg.2 ha0.le + set P : γ → ℝ≥0∞ := fun u ↦ ∑ x, ρ x {u} * μ {x} + set c := ∑ u, P u ^ a + have hP_le (u : γ) : P u ≤ 1 := + (Finset.single_le_sum (f := P) (fun _ _ ↦ zero_le) (Finset.mem_univ u)).trans + (sum_joint_fst_singleton (μ := μ) (ρ := ρ)).le + have hc0 : c ≠ 0 := sum_rpow_joint_fst_ne_zero ha0 + have hctop : c ≠ ∞ := ENNReal.sum_ne_top.2 fun u _ ↦ + ENNReal.rpow_ne_top_of_nonneg ha0.le (ne_top_of_le_ne_top ENNReal.one_ne_top (hP_le u)) + -- The input law `P_X̃`. + set m : α → ℝ≥0∞ := fun x ↦ μ {x} * ∑ u, P u ^ (a - 1) * ρ x {u} + set ν : Measure α := ∑ x, (c⁻¹ * m x) • Measure.dirac x + have hν (x : α) : ν {x} = c⁻¹ * m x := sum_smul_dirac_apply_singleton _ _ + have hPa (u : γ) : P u ^ (a - 1) * P u = P u ^ a := by + conv_rhs => rw [← sub_add_cancel a 1] + rw [ENNReal.rpow_add_of_nonneg _ _ (by linarith) zero_le_one, ENNReal.rpow_one] + have hm_sum : ∑ x, m x = c := by + simp_rw [m, Finset.mul_sum] + rw [Finset.sum_comm] + refine Finset.sum_congr rfl fun u _ ↦ ?_ + rw [← hPa u, Finset.mul_sum] + exact Finset.sum_congr rfl fun x _ ↦ by ring + have hν_prob : IsProbabilityMeasure ν := ⟨by + rw [← Finset.coe_univ, ← sum_measure_singleton] + simp_rw [hν, ← Finset.mul_sum, hm_sum] + exact ENNReal.inv_mul_cancel hc0 hctop⟩ + have hν_ac : ν ≪ μ := by + refine fun s hs ↦ (measure_null_iff_singleton s.to_countable).2 fun x hx ↦ ?_ + rw [hν] + simp [m, (measure_null_iff_singleton s.to_countable).1 hs x hx] + -- The weighted Hölder inequality, column by column. + have h_y (y : β) : ∑ u, ((ρ ×ₖ κ) ∘ₘ μ) {(u, y)} ^ a ≤ c * ∑ x, ν {x} * κ x {y} ^ a := by + have h_u (u : γ) : ((ρ ×ₖ κ) ∘ₘ μ) {(u, y)} ^ a ≤ + P u ^ (a - 1) * ∑ x, ρ x {u} * μ {x} * κ x {y} ^ a := by + have h := ENNReal.inner_le_weight_mul_Lp_of_nonneg Finset.univ ha.le + (fun x ↦ ρ x {u} * μ {x}) (fun x ↦ κ x {y}) + calc ((ρ ×ₖ κ) ∘ₘ μ) {(u, y)} ^ a + = (∑ x, ρ x {u} * μ {x} * κ x {y}) ^ a := by + rw [kernelProd_bind_singleton] + congr 1 + exact Finset.sum_congr rfl fun x _ ↦ by ring + _ ≤ (P u ^ (1 - a⁻¹) * (∑ x, ρ x {u} * μ {x} * κ x {y} ^ a) ^ a⁻¹) ^ a := + ENNReal.rpow_le_rpow h ha0.le + _ = P u ^ (a - 1) * ∑ x, ρ x {u} * μ {x} * κ x {y} ^ a := by + rw [ENNReal.mul_rpow_of_nonneg _ _ ha0.le, ← ENNReal.rpow_mul, ← ENNReal.rpow_mul, + inv_mul_cancel₀ ha0.ne', ENNReal.rpow_one] + congr 2 + field_simp + calc ∑ u, ((ρ ×ₖ κ) ∘ₘ μ) {(u, y)} ^ a + ≤ ∑ u, P u ^ (a - 1) * ∑ x, ρ x {u} * μ {x} * κ x {y} ^ a := + Finset.sum_le_sum fun u _ ↦ h_u u + _ = ∑ x, m x * κ x {y} ^ a := by + simp_rw [m, Finset.mul_sum, Finset.sum_mul] + rw [Finset.sum_comm] + exact Finset.sum_congr rfl fun x _ ↦ Finset.sum_congr rfl fun u _ ↦ by ring + _ = c * ∑ x, ν {x} * κ x {y} ^ a := by + simp_rw [hν, Finset.mul_sum, ← mul_assoc, ENNReal.mul_inv_cancel hc0 hctop, one_mul] + have hc_rpow0 : c ^ a⁻¹ ≠ 0 := (ENNReal.rpow_eq_zero_iff_of_pos (inv_pos.2 ha0)).not.2 hc0 + have hc_rpow_top : c ^ a⁻¹ ≠ ∞ := ENNReal.rpow_ne_top_of_nonneg hinv hctop + calc arimotoSum a ((ρ ×ₖ κ) ∘ₘ μ) + = (∑ y, (∑ u, ((ρ ×ₖ κ) ∘ₘ μ) {(u, y)} ^ a) ^ a⁻¹) / c ^ a⁻¹ := by + simp_rw [arimotoSum, kernelProd_bind_fst_singleton] + rfl + _ ≤ (∑ y, (c * ∑ x, ν {x} * κ x {y} ^ a) ^ a⁻¹) / c ^ a⁻¹ := by + gcongr with y + exact h_y y + _ = sibsonSum a ν κ := by + simp_rw [ENNReal.mul_rpow_of_nonneg _ _ hinv, ← Finset.mul_sum, mul_comm (c ^ a⁻¹)] + exact ENNReal.mul_div_cancel_right hc_rpow0 hc_rpow_top + _ ≤ sibsonCapacitySum a μ κ := le_iSup₂_of_le ν hν_prob (le_iSup_of_le hν_ac le_rfl) + +end UpperBound + +section LowerBound + +omit [MeasurableSpace α] in +/-- For `a > 1`, every value `t ∈ [(n + 1) ^ (1 - a), 1]` is the sum `∑_j w_j ^ a` of a probability +vector `w` on `n + 1` points: by the intermediate value theorem along the segment from the uniform +vector to a point mass. -/ +lemma exists_sum_rpow_eq (ha : 1 < a) (n : ℕ) {t : ℝ} (ht₀ : ((n : ℝ) + 1) ^ (1 - a) ≤ t) + (ht₁ : t ≤ 1) : + ∃ w : Fin (n + 1) → ℝ, (∀ j, 0 ≤ w j) ∧ ∑ j, w j = 1 ∧ ∑ j, w j ^ a = t := by + have hn : (0 : ℝ) < n + 1 := by positivity + set w : ℝ → Fin (n + 1) → ℝ := fun s j ↦ (if j = 0 then s else 0) + (1 - s) / (n + 1) + set f : ℝ → ℝ := fun s ↦ ∑ j, w s j ^ a + have hw (j : Fin (n + 1)) : Continuous fun s ↦ w s j := by + by_cases hj : j = 0 <;> simp only [w, hj, ite_true, ite_false] <;> fun_prop + have hf : Continuous f := continuous_finsetSum _ fun j _ ↦ + (hw j).rpow_const fun _ ↦ Or.inr (by linarith) + have hf0 : f 0 = ((n : ℝ) + 1) ^ (1 - a) := by + simp only [f, w, ite_self, zero_add, sub_zero, Finset.sum_const, Finset.card_univ, + Fintype.card_fin, nsmul_eq_mul, Nat.cast_add, Nat.cast_one] + rw [Real.div_rpow zero_le_one hn.le, Real.one_rpow, Real.rpow_sub hn, Real.rpow_one] + field_simp + have hf1 : f 1 = 1 := by + simp only [f, w, sub_self, zero_div, add_zero] + rw [Fin.sum_univ_succ] + simp [Real.zero_rpow (by linarith : a ≠ 0)] + have ht : t ∈ Icc (f 0) (f 1) := by + rw [hf0, hf1] + exact ⟨ht₀, ht₁⟩ + obtain ⟨s, ⟨hs0, hs1⟩, hs⟩ := intermediate_value_Icc zero_le_one hf.continuousOn ht + refine ⟨w s, fun j ↦ add_nonneg (by split_ifs <;> linarith) (by + have : 0 ≤ 1 - s := by linarith + positivity), ?_, hs⟩ + simp only [w, Finset.sum_add_distrib, Finset.sum_ite_eq', Finset.mem_univ, ite_true, + Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, Nat.cast_add, + Nat.cast_one] + field_simp + ring + +omit [MeasurableSpace α] in +/-- `ℝ≥0∞` version of `exists_sum_rpow_eq`. -/ +lemma exists_sum_rpow_eq_of_le (ha : 1 < a) (n : ℕ) {t : ℝ≥0∞} + (ht₀ : ((n : ℝ≥0∞) + 1) ^ (1 - a) ≤ t) (ht₁ : t ≤ 1) : + ∃ w : Fin (n + 1) → ℝ≥0∞, ∑ j, w j = 1 ∧ ∑ j, w j ^ a = t := by + have ht : t ≠ ∞ := ne_top_of_le_ne_top ENNReal.one_ne_top ht₁ + have h₀ : ((n : ℝ) + 1) ^ (1 - a) ≤ t.toReal := by + have := ENNReal.toReal_mono ht ht₀ + rwa [← ENNReal.toReal_rpow, ENNReal.toReal_add (ENNReal.natCast_ne_top n) ENNReal.one_ne_top, + ENNReal.toReal_natCast, ENNReal.toReal_one] at this + have h₁ : t.toReal ≤ 1 := by simpa using ENNReal.toReal_mono ENNReal.one_ne_top ht₁ + obtain ⟨w, hw0, hw1, hwa⟩ := exists_sum_rpow_eq ha n h₀ h₁ + refine ⟨fun j ↦ ENNReal.ofReal (w j), ?_, ?_⟩ + · rw [← ENNReal.ofReal_sum_of_nonneg fun j _ ↦ hw0 j, hw1, ENNReal.ofReal_one] + · simp_rw [ENNReal.ofReal_rpow_of_nonneg (hw0 _) (by linarith : (0 : ℝ) ≤ a)] + rw [← ENNReal.ofReal_sum_of_nonneg fun j _ ↦ Real.rpow_nonneg (hw0 j) _, hwa, + ENNReal.ofReal_toReal ht] + +omit [MeasurableSpace α] in +lemma exists_nat_rpow_le (ha : 1 < a) {t : ℝ≥0∞} (ht : t ≠ 0) : + ∃ n : ℕ, ((n : ℝ≥0∞) + 1) ^ (1 - a) ≤ t := by + have hb : 0 < a - 1 := by linarith + obtain ⟨n, hn⟩ := ENNReal.exists_nat_gt + (ENNReal.rpow_ne_top_of_nonneg (inv_nonneg.2 hb.le) (ENNReal.inv_ne_top.2 ht) : + t⁻¹ ^ (a - 1)⁻¹ ≠ ∞) + refine ⟨n, ?_⟩ + have h : t⁻¹ ≤ ((n : ℝ≥0∞) + 1) ^ (a - 1) := + calc t⁻¹ = (t⁻¹ ^ (a - 1)⁻¹) ^ (a - 1) := (ENNReal.rpow_inv_rpow hb.ne' _).symm + _ ≤ ((n : ℝ≥0∞) + 1) ^ (a - 1) := + ENNReal.rpow_le_rpow (hn.le.trans le_self_add) hb.le + rw [show 1 - a = -(a - 1) by ring, ENNReal.rpow_neg] + simpa using ENNReal.inv_le_inv.2 h + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + +/-- **Achievability half of Theorem 2** of Liao–Kosut–Sankar–Calmon, for an input law `ν ≪ μ` that +charges every atom of `μ`: some randomized function `U = (X, J)` of `X` with `J ∈ Fin (n + 1)` +has `I^A_a(U; Y) = I^S_a(X̃; Y)` with `X̃ ∼ ν`. Given `X = x`, the label `J` is drawn from a +probability vector `w_x` with `∑_j w_x(j) ^ a ∝ ν {x} / μ {x} ^ a`, so that the escort +distribution of `U`, pushed to `X`, is `ν` (eqs. (104)–(109) of the paper; the paper leaves the +existence of `w_x` implicit, here it comes from the intermediate value theorem). -/ +lemma exists_arimotoSum_joint_eq (ha : 1 < a) [IsProbabilityMeasure μ] [IsMarkovKernel κ] + [IsProbabilityMeasure ν] (hνμ : ν ≪ μ) (hμν : ∀ x, μ {x} ≠ 0 → ν {x} ≠ 0) : + ∃ (n : ℕ) (ρ : Kernel α (α × Fin (n + 1))), IsMarkovKernel ρ ∧ + arimotoSum a ((ρ ×ₖ κ) ∘ₘ μ) = sibsonSum a ν κ := by + classical + have ha0 : 0 < a := zero_lt_one.trans ha + have hinv : 0 ≤ a⁻¹ := inv_nonneg.2 ha0.le + set S := Finset.univ.filter fun x : α ↦ μ {x} ≠ 0 + have hmem (x : α) : x ∈ S ↔ μ {x} ≠ 0 := by simp [S] + have hS : S.Nonempty := by + by_contra h + have h0 : ∀ x, μ {x} = 0 := fun x ↦ by + by_contra hx + exact h ⟨x, (hmem x).2 hx⟩ + have := sum_measure_singleton (μ := μ) (s := Finset.univ) + simp [h0] at this + have hμa0 (x : α) (hx : μ {x} ≠ 0) : μ {x} ^ a ≠ 0 := + (ENNReal.rpow_eq_zero_iff_of_pos ha0).not.2 hx + have hμatop (x : α) : μ {x} ^ a ≠ ∞ := ENNReal.rpow_ne_top_of_nonneg ha0.le (measure_ne_top _ _) + -- The normalization `λ = min_{x ∈ supp μ} μ {x} ^ a / ν {x}` and the targets `t x ≤ 1`. + set lam := S.inf' hS fun x ↦ μ {x} ^ a / ν {x} + obtain ⟨x₁, hx₁S, hx₁⟩ := Finset.exists_mem_eq_inf' hS fun x ↦ μ {x} ^ a / ν {x} + have hx₁ : lam = μ {x₁} ^ a / ν {x₁} := hx₁ + have hlam0 : lam ≠ 0 := by + rw [hx₁] + exact ENNReal.div_ne_zero.2 ⟨hμa0 x₁ ((hmem x₁).1 hx₁S), measure_ne_top ν _⟩ + set t : α → ℝ≥0∞ := fun x ↦ lam * ν {x} / μ {x} ^ a + have ht_le (x : α) (hx : μ {x} ≠ 0) : t x ≤ 1 := by + refine ENNReal.div_le_of_le_mul ?_ + rw [one_mul] + exact (ENNReal.le_div_iff_mul_le (Or.inl (hμν x hx)) (Or.inl (measure_ne_top ν _))).1 + (Finset.inf'_le _ ((hmem x).2 hx)) + set tmin := S.inf' hS t + have htmin0 : tmin ≠ 0 := by + obtain ⟨x, hxS, hx⟩ := Finset.exists_mem_eq_inf' hS t + have hx' : tmin = t x := hx + rw [hx'] + exact ENNReal.div_ne_zero.2 ⟨mul_ne_zero hlam0 (hμν x ((hmem x).1 hxS)), hμatop x⟩ + obtain ⟨n, hn⟩ := exists_nat_rpow_le ha htmin0 + -- The conditional laws `w x` of the label `J`. + have hw : ∀ x, ∃ w : Fin (n + 1) → ℝ≥0∞, ∑ j, w j = 1 ∧ (μ {x} ≠ 0 → ∑ j, w j ^ a = t x) := by + intro x + by_cases hx : μ {x} = 0 + · exact ⟨fun j ↦ if j = 0 then 1 else 0, by simp, fun h ↦ absurd hx h⟩ + · obtain ⟨w, hw1, hwa⟩ := exists_sum_rpow_eq_of_le ha n + (hn.trans (Finset.inf'_le _ ((hmem x).2 hx))) (ht_le x hx) + exact ⟨w, hw1, fun _ ↦ hwa⟩ + choose w hw1 hwa using hw + have hkey (x : α) : (∑ j, w x j ^ a) * μ {x} ^ a = lam * ν {x} := by + by_cases hx : μ {x} = 0 + · have hνx : ν {x} = 0 := hνμ hx + rw [hx, hνx, ENNReal.zero_rpow_of_pos ha0, mul_zero, mul_zero] + · rw [hwa x hx, ENNReal.div_mul_cancel (hμa0 x hx) (hμatop x)] + -- The randomized function `U = (X, J)`. + set W : α → α × Fin (n + 1) → ℝ≥0∞ := fun x p ↦ if p.1 = x then w x p.2 else 0 + set ρ : Kernel α (α × Fin (n + 1)) := + Kernel.ofFunOfCountable fun x ↦ ∑ p, W x p • Measure.dirac p + have hρ (x : α) (p : α × Fin (n + 1)) : ρ x {p} = W x p := sum_smul_dirac_apply_singleton _ _ + have hρM : IsMarkovKernel ρ := ⟨fun x ↦ ⟨by + rw [← Finset.coe_univ, ← sum_measure_singleton] + simp_rw [hρ] + rw [Fintype.sum_prod_type, Finset.sum_eq_single x (fun x' _ hx' ↦ by simp [W, hx']) + (by simp)] + simpa [W] using hw1 x⟩⟩ + have hJ (x' : α) (j : Fin (n + 1)) (y : β) : + ((ρ ×ₖ κ) ∘ₘ μ) {((x', j), y)} = w x' j * κ x' {y} * μ {x'} := by + rw [kernelProd_bind_singleton, + Finset.sum_eq_single x' (fun x _ hx ↦ by simp [hρ, W, Ne.symm hx]) (by simp)] + simp [hρ, W] + have hP (x' : α) (j : Fin (n + 1)) : ∑ x, ρ x {(x', j)} * μ {x} = w x' j * μ {x'} := by + rw [Finset.sum_eq_single x' (fun x _ hx ↦ by simp [hρ, W, Ne.symm hx]) (by simp)] + simp [hρ, W] + have hnum (y : β) : ∑ u, ((ρ ×ₖ κ) ∘ₘ μ) {(u, y)} ^ a = lam * ∑ x, ν {x} * κ x {y} ^ a := by + rw [Fintype.sum_prod_type, Finset.mul_sum] + refine Finset.sum_congr rfl fun x _ ↦ ?_ + simp_rw [hJ, ENNReal.mul_rpow_of_nonneg _ _ ha0.le] + rw [← Finset.sum_mul, ← Finset.sum_mul, mul_right_comm, hkey, mul_assoc] + have hden : ∑ u, (∑ x, ρ x {u} * μ {x}) ^ a = lam := by + rw [Fintype.sum_prod_type] + simp_rw [hP, ENNReal.mul_rpow_of_nonneg _ _ ha0.le, ← Finset.sum_mul, hkey, ← Finset.mul_sum, + sum_measure_singleton, Finset.coe_univ, measure_univ, mul_one] + have hlam_rpow0 : lam ^ a⁻¹ ≠ 0 := (ENNReal.rpow_eq_zero_iff_of_pos (inv_pos.2 ha0)).not.2 hlam0 + have hlam_rpow_top : lam ^ a⁻¹ ≠ ∞ := by + refine ENNReal.rpow_ne_top_of_nonneg hinv ?_ + rw [hx₁] + exact ENNReal.div_ne_top (hμatop x₁) (hμν x₁ ((hmem x₁).1 hx₁S)) + refine ⟨n, ρ, hρM, ?_⟩ + simp_rw [arimotoSum, kernelProd_bind_fst_singleton, hden, hnum, + ENNReal.mul_rpow_of_nonneg _ _ hinv, ← Finset.mul_sum, mul_comm (lam ^ a⁻¹)] + exact ENNReal.mul_div_cancel_right hlam_rpow0 hlam_rpow_top + +end LowerBound + +section MainTheorem + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + [Fintype γ] [MeasurableSingletonClass γ] + +omit [Fintype α] [Fintype β] [Fintype γ] in +/-- Relabelling the alphabet `γ` of `U` as `Fin (card γ)` shows that every randomized function +`U` of `X` on a finite alphabet is covered by the supremum defining `maxAlphaLeakageRatio`. -/ +lemma alphaLeakageRatio_le_maxAlphaLeakageRatio [Finite α] [Finite β] [Finite γ] (ha : 1 < a) + [IsProbabilityMeasure μ] [IsMarkovKernel κ] (ρ : Kernel α γ) [IsMarkovKernel ρ] : + alphaLeakageRatio a ((ρ ×ₖ κ) ∘ₘ μ) ≤ maxAlphaLeakageRatio a μ κ := by + have := Fintype.ofFinite α + have := Fintype.ofFinite β + have := Fintype.ofFinite γ + set e := Fintype.equivFin γ + have he : Measurable e := measurable_of_finite _ + have hmap (x : α) (u : γ) : ρ.map e x {e u} = ρ x {u} := by + rw [Kernel.map_apply' _ he _ (measurableSet_singleton _)] + congr 1 + ext v + simp + have := Kernel.IsMarkovKernel.map ρ he + have h1 (y : β) : ∑ v, ((ρ.map e ×ₖ κ) ∘ₘ μ) {(v, y)} ^ a = + ∑ u, ((ρ ×ₖ κ) ∘ₘ μ) {(u, y)} ^ a := by + rw [← e.sum_comp (fun v ↦ ((ρ.map e ×ₖ κ) ∘ₘ μ) {(v, y)} ^ a)] + simp_rw [kernelProd_bind_singleton, hmap] + have h2 : ∑ v, ((ρ.map e ×ₖ κ) ∘ₘ μ).fst {v} ^ a = ∑ u, ((ρ ×ₖ κ) ∘ₘ μ).fst {u} ^ a := by + rw [← e.sum_comp (fun v ↦ ((ρ.map e ×ₖ κ) ∘ₘ μ).fst {v} ^ a)] + simp_rw [kernelProd_bind_fst_singleton, hmap] + have h_eq : arimotoSum a ((ρ.map e ×ₖ κ) ∘ₘ μ) = arimotoSum a ((ρ ×ₖ κ) ∘ₘ μ) := by + simp_rw [arimotoSum, h1, h2] + rw [alphaLeakageRatio_eq_arimotoSum ha, ← h_eq, ← alphaLeakageRatio_eq_arimotoSum ha] + exact le_iSup_of_le (Fintype.card γ) <| le_iSup₂_of_le (ρ.map e) this le_rfl + +omit [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Fintype γ] + [MeasurableSingletonClass γ] in +/-- `ν ↦ ∑_y (∑_x ν {x} κ x {y} ^ a) ^ (1 / a)` grows at least like `s ^ (1 / a)` when `ν` is +replaced by `s • ν + (1 - s) • μ`. -/ +lemma rpow_inv_mul_sibsonSum_le (ha : 0 < a) (s : ℝ≥0∞) : + s ^ a⁻¹ * sibsonSum a ν κ ≤ sibsonSum a (s • ν + (1 - s) • μ) κ := by + rw [sibsonSum, Finset.mul_sum] + refine Finset.sum_le_sum fun y _ ↦ ?_ + rw [← ENNReal.mul_rpow_of_nonneg _ _ (inv_nonneg.2 ha.le), Finset.mul_sum] + refine ENNReal.rpow_le_rpow (Finset.sum_le_sum fun x _ ↦ ?_) (inv_nonneg.2 ha.le) + rw [add_apply, smul_apply, smul_apply, smul_eq_mul, smul_eq_mul, add_mul, mul_assoc] + exact le_self_add + +/-- **Achievability half of Theorem 2** of Liao–Kosut–Sankar–Calmon: every `I^S_a(X̃; Y)` with +`P_X̃ ≪ P_X` is approached by α-leakages `L_a(U → Y)` of randomized functions `U` of `X`. We mix +`P_X̃` with `P_X` so that it charges every atom of `P_X`, and apply +`exists_arimotoSum_joint_eq`. -/ +lemma sibsonSum_le_maxAlphaLeakageRatio (ha : 1 < a) [IsProbabilityMeasure μ] [IsMarkovKernel κ] + [IsProbabilityMeasure ν] (hνμ : ν ≪ μ) : + sibsonSum a ν κ ≤ maxAlphaLeakageRatio a μ κ := by + have ha0 : 0 < a := zero_lt_one.trans ha + refine ENNReal.le_of_forall_lt_one_mul_le fun s hs ↦ ?_ + have hs1 : 1 - s ≠ 0 := (tsub_pos_of_lt hs).ne' + set ν' := s • ν + (1 - s) • μ + have hν' (x : α) : ν' {x} = s * ν {x} + (1 - s) * μ {x} := by + simp [ν'] + have : IsProbabilityMeasure ν' := ⟨by + simp [ν', add_tsub_cancel_of_le hs.le]⟩ + have hν'μ : ν' ≪ μ := by + refine fun t ht ↦ (measure_null_iff_singleton t.to_countable).2 fun x hx ↦ ?_ + have hμx := (measure_null_iff_singleton t.to_countable).1 ht x hx + rw [hν', hμx, hνμ hμx] + simp + have hμν' (x : α) (hx : μ {x} ≠ 0) : ν' {x} ≠ 0 := by + rw [hν'] + exact fun h ↦ mul_ne_zero hs1 hx (add_eq_zero.1 h).2 + obtain ⟨n, ρ, hρ, h_eq⟩ := exists_arimotoSum_joint_eq (κ := κ) ha hν'μ hμν' + calc s * sibsonSum a ν κ ≤ s ^ a⁻¹ * sibsonSum a ν κ := by + gcongr + simpa using ENNReal.rpow_le_rpow_of_exponent_ge hs.le (inv_le_one_of_one_le₀ ha.le) + _ ≤ sibsonSum a ν' κ := rpow_inv_mul_sibsonSum_le ha0 s + _ = alphaLeakageRatio a ((ρ ×ₖ κ) ∘ₘ μ) := by rw [alphaLeakageRatio_eq_arimotoSum ha, h_eq] + _ ≤ maxAlphaLeakageRatio a μ κ := alphaLeakageRatio_le_maxAlphaLeakageRatio ha ρ + +omit [Fintype γ] [MeasurableSingletonClass γ] in +/-- **Theorem 2 of Liao–Kosut–Sankar–Calmon** (eq. (31a), Sibson form), multiplicative form: for +`a ∈ (1, ∞)` the maximal α-leakage is the Sibson capacity of order `a` of the channel over inputs +supported in the support of `P_X`: +`L^max_a(X → Y) = sup_{P_X̃ ≪ P_X} I^S_a(X̃; Y)`. -/ +theorem maxAlphaLeakageRatio_eq_sibsonCapacitySum (ha : 1 < a) [IsProbabilityMeasure μ] + [IsMarkovKernel κ] : maxAlphaLeakageRatio a μ κ = sibsonCapacitySum a μ κ := by + refine le_antisymm (iSup_le fun n ↦ iSup₂_le fun ρ _ ↦ ?_) (iSup₂_le fun ν _ ↦ iSup_le + fun hνμ ↦ sibsonSum_le_maxAlphaLeakageRatio ha hνμ) + rw [alphaLeakageRatio_eq_arimotoSum ha] + exact arimotoSum_joint_le ha ρ + +end MainTheorem + +section Arimoto + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + +omit [Fintype β] [MeasurableSingletonClass β] in +/-- The escort operation of order `a` inverts the escort operation of order `1 / a`. -/ +lemma escort_escort_inv (ha : 0 < a) [IsProbabilityMeasure ν] : escort a (escort a⁻¹ ν) = ν := by + set T := ∑ x, ν {x} ^ a⁻¹ + have hT0 : T ≠ 0 := by + obtain ⟨x, hx⟩ : ∃ x, ν {x} ≠ 0 := by + by_contra! h + have := sum_measure_singleton (μ := ν) (s := Finset.univ) + simp [h] at this + exact ne_of_gt <| (pos_iff_ne_zero.2 ((ENNReal.rpow_eq_zero_iff_of_pos (inv_pos.2 ha)).not.2 + hx)).trans_le (Finset.single_le_sum (f := fun x ↦ ν {x} ^ a⁻¹) (fun _ _ ↦ zero_le) + (Finset.mem_univ x)) + have hTtop : T ≠ ∞ := ENNReal.sum_ne_top.2 fun x _ ↦ + ENNReal.rpow_ne_top_of_nonneg (inv_nonneg.2 ha.le) (measure_ne_top ν _) + have hc0 : T⁻¹ ^ a ≠ 0 := (ENNReal.rpow_eq_zero_iff_of_pos ha).not.2 (ENNReal.inv_ne_zero.2 hTtop) + have hctop : T⁻¹ ^ a ≠ ∞ := ENNReal.rpow_ne_top_of_nonneg ha.le (ENNReal.inv_ne_top.2 hT0) + have h_pow (x : α) : escort a⁻¹ ν {x} ^ a = T⁻¹ ^ a * ν {x} := by + rw [escort_singleton, ENNReal.mul_rpow_of_nonneg _ _ ha.le, ENNReal.rpow_inv_rpow ha.ne'] + refine Measure.ext_iff_singleton.2 fun x ↦ ?_ + rw [escort_singleton] + simp_rw [h_pow, ← Finset.mul_sum, sum_measure_singleton, Finset.coe_univ, measure_univ, mul_one, + ← mul_assoc, ENNReal.inv_mul_cancel hc0 hctop, one_mul] + +/-- **Theorem 2 of Liao–Kosut–Sankar–Calmon** (eq. (31a), Arimoto form), multiplicative form: +`L^max_a(X → Y) = sup_{P_X̃ ≪ P_X} I^A_a(X̃; Y)` for `a ∈ (1, ∞)`. The Sibson and Arimoto +suprema agree because the escort operation is a bijection of the input laws supported in the +support of `P_X` (Csiszár's observation, [43, Thm. 5] in the paper). -/ +theorem maxAlphaLeakageRatio_eq_iSup_arimotoSum (ha : 1 < a) [IsProbabilityMeasure μ] + [IsMarkovKernel κ] : maxAlphaLeakageRatio a μ κ = + ⨆ (ν : Measure α) (_ : IsProbabilityMeasure ν) (_ : ν ≪ μ), arimotoSum a (ν ⊗ₘ κ) := by + have ha0 : 0 < a := zero_lt_one.trans ha + rw [maxAlphaLeakageRatio_eq_sibsonCapacitySum ha] + refine le_antisymm (iSup₂_le fun ν hν ↦ iSup_le fun hνμ ↦ ?_) + (iSup₂_le fun ν hν ↦ iSup_le fun hνμ ↦ ?_) + · have := isProbabilityMeasure_escort (μ := ν) (inv_pos.2 ha0) (IsProbabilityMeasure.ne_zero ν) + refine le_iSup₂_of_le (escort a⁻¹ ν) this <| le_iSup_of_le + ((escort_absolutelyContinuous (inv_pos.2 ha0)).trans hνμ) (le_of_eq ?_) + rw [arimotoSum_compProd ha0.le, escort_escort_inv ha0] + · have := isProbabilityMeasure_escort (μ := ν) ha0 (IsProbabilityMeasure.ne_zero ν) + rw [arimotoSum_compProd ha0.le] + exact le_iSup₂_of_le (escort a ν) this <| le_iSup_of_le + ((escort_absolutelyContinuous ha0).trans hνμ) le_rfl + +end Arimoto + +section LogForm + +omit [MeasurableSpace α] in +/-- Transfers a supremum in `ℝ≥0∞` of quantities `≥ 1` through `r ↦ a / (a - 1) · log r`. -/ +lemma isLUB_image_mul_log_toReal (ha : 1 < a) {A : Set ℝ≥0∞} (hA : ∀ r ∈ A, 1 ≤ r) + (hne : A.Nonempty) (htop : sSup A ≠ ∞) : + IsLUB ((fun r : ℝ≥0∞ ↦ a / (a - 1) * Real.log r.toReal) '' A) + (a / (a - 1) * Real.log (sSup A).toReal) := by + have hc : 0 < a / (a - 1) := div_pos (by linarith) (by linarith) + have h_one (r : ℝ≥0∞) (hr : r ∈ A) : 1 ≤ r.toReal := by + have hrtop : r ≠ ∞ := ne_top_of_le_ne_top htop (le_sSup hr) + simpa using ENNReal.toReal_mono hrtop (hA r hr) + obtain ⟨r₀, hr₀⟩ := hne + have hS1 : 1 ≤ (sSup A).toReal := + (h_one r₀ hr₀).trans (ENNReal.toReal_mono htop (le_sSup hr₀)) + refine ⟨?_, fun b hb ↦ ?_⟩ + · rintro _ ⟨r, hr, rfl⟩ + exact mul_le_mul_of_nonneg_left (Real.log_le_log (by linarith [h_one r hr]) + (ENNReal.toReal_mono htop (le_sSup hr))) hc.le + by_contra! hlt + set q := Real.exp (b / (a / (a - 1))) + have hq : q < (sSup A).toReal := by + rw [← Real.exp_log (by linarith : 0 < (sSup A).toReal)] + exact Real.exp_lt_exp.2 ((div_lt_iff₀' hc).2 hlt) + have hqS : ENNReal.ofReal q < sSup A := + (ENNReal.ofReal_lt_iff_lt_toReal (Real.exp_pos _).le htop).2 hq + obtain ⟨r, hr, hqr⟩ := lt_sSup_iff.1 hqS + have hrtop : r ≠ ∞ := ne_top_of_le_ne_top htop (le_sSup hr) + have hqr' : q < r.toReal := (ENNReal.ofReal_lt_iff_lt_toReal (Real.exp_pos _).le hrtop).1 hqr + have hbr : b < a / (a - 1) * Real.log r.toReal := by + rw [← div_lt_iff₀' hc, ← Real.exp_lt_exp, Real.exp_log (by linarith [h_one r hr])] + exact hqr' + exact absurd (hb ⟨r, hr, rfl⟩) (not_le.2 hbr) + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + +omit [MeasurableSingletonClass β] in +lemma sibsonCapacitySum_le_card (ha : 0 < a) [IsMarkovKernel κ] : + sibsonCapacitySum a μ κ ≤ Fintype.card β := + iSup₂_le fun _ _ ↦ iSup_le fun _ ↦ sibsonSum_le_card ha + +omit [Fintype α] [Fintype β] in +lemma maxAlphaLeakageRatio_ne_top [Finite α] [Finite β] (ha : 1 < a) [IsProbabilityMeasure μ] + [IsMarkovKernel κ] : maxAlphaLeakageRatio a μ κ ≠ ∞ := by + have := Fintype.ofFinite α + have := Fintype.ofFinite β + rw [maxAlphaLeakageRatio_eq_sibsonCapacitySum ha] + exact ne_top_of_le_ne_top (ENNReal.natCast_ne_top _) + (sibsonCapacitySum_le_card (zero_lt_one.trans ha)) + +/-- **Theorem 2 of Liao–Kosut–Sankar–Calmon** (eq. (31a), Sibson form): for `a ∈ (1, ∞)`, +`L^max_a(X → Y) = sup_{P_X̃ ≪ P_X} I^S_a(X̃; Y)`, as a least upper bound of real numbers. -/ +theorem isLUB_sibsonMI (ha : 1 < a) [IsProbabilityMeasure μ] [IsMarkovKernel κ] : + IsLUB {r | ∃ ν : Measure α, IsProbabilityMeasure ν ∧ ν ≪ μ ∧ r = sibsonMI a ν κ} + (maxAlphaLeakage a μ κ) := by + set A := {r : ℝ≥0∞ | ∃ ν : Measure α, IsProbabilityMeasure ν ∧ ν ≪ μ ∧ r = sibsonSum a ν κ} + have hA : sSup A = maxAlphaLeakageRatio a μ κ := by + rw [maxAlphaLeakageRatio_eq_sibsonCapacitySum ha] + refine le_antisymm (sSup_le ?_) + (iSup₂_le fun ν hν ↦ iSup_le fun hνμ ↦ le_sSup ⟨ν, hν, hνμ, rfl⟩) + rintro _ ⟨ν, hν, hνμ, rfl⟩ + exact le_iSup₂_of_le ν hν (le_iSup_of_le hνμ le_rfl) + have hset : {r | ∃ ν : Measure α, IsProbabilityMeasure ν ∧ ν ≪ μ ∧ r = sibsonMI a ν κ} = + (fun r : ℝ≥0∞ ↦ a / (a - 1) * Real.log r.toReal) '' A := by + ext r + constructor + · rintro ⟨ν, hν, hνμ, rfl⟩ + exact ⟨_, ⟨ν, hν, hνμ, rfl⟩, rfl⟩ + · rintro ⟨_, ⟨ν, hν, hνμ, rfl⟩, rfl⟩ + exact ⟨ν, hν, hνμ, rfl⟩ + rw [hset, maxAlphaLeakage, ← hA] + refine isLUB_image_mul_log_toReal ha ?_ ⟨_, μ, inferInstance, Measure.AbsolutelyContinuous.rfl, + rfl⟩ (hA ▸ maxAlphaLeakageRatio_ne_top ha) + rintro _ ⟨ν, hν, -, rfl⟩ + exact one_le_sibsonSum ha.le + +omit [Fintype α] [Fintype β] in +/-- **Definition 6 of Liao–Kosut–Sankar–Calmon**, in its original form: for `a ∈ (1, ∞)`, +`maxAlphaLeakage a μ κ` is the supremum of the α-leakages `L_a(U → Y)` over all randomized +functions `U` of `X` on finite alphabets, `U - X - Y`. -/ +theorem isLUB_alphaLeakage [Finite α] [Finite β] (ha : 1 < a) [IsProbabilityMeasure μ] + [IsMarkovKernel κ] : + IsLUB {r | ∃ (n : ℕ) (ρ : Kernel α (Fin n)), IsMarkovKernel ρ ∧ + r = alphaLeakage a ((ρ ×ₖ κ) ∘ₘ μ)} (maxAlphaLeakage a μ κ) := by + have := Fintype.ofFinite α + have := Fintype.ofFinite β + set A := {r : ℝ≥0∞ | ∃ (n : ℕ) (ρ : Kernel α (Fin n)), IsMarkovKernel ρ ∧ + r = alphaLeakageRatio a ((ρ ×ₖ κ) ∘ₘ μ)} + have hA : sSup A = maxAlphaLeakageRatio a μ κ := by + refine le_antisymm (sSup_le ?_) + (iSup_le fun n ↦ iSup₂_le fun ρ hρ ↦ le_sSup ⟨n, ρ, hρ, rfl⟩) + rintro _ ⟨n, ρ, hρ, rfl⟩ + exact le_iSup_of_le n (le_iSup₂_of_le ρ hρ le_rfl) + have hset : {r | ∃ (n : ℕ) (ρ : Kernel α (Fin n)), IsMarkovKernel ρ ∧ + r = alphaLeakage a ((ρ ×ₖ κ) ∘ₘ μ)} = + (fun r : ℝ≥0∞ ↦ a / (a - 1) * Real.log r.toReal) '' A := by + ext r + constructor + · rintro ⟨n, ρ, hρ, rfl⟩ + exact ⟨_, ⟨n, ρ, hρ, rfl⟩, rfl⟩ + · rintro ⟨_, ⟨n, ρ, hρ, rfl⟩, rfl⟩ + exact ⟨n, ρ, hρ, rfl⟩ + rw [hset, maxAlphaLeakage, ← hA] + refine isLUB_image_mul_log_toReal ha ?_ ⟨_, 1, Kernel.deterministic (fun _ ↦ 0) measurable_const, + inferInstance, rfl⟩ (hA ▸ maxAlphaLeakageRatio_ne_top ha) + rintro _ ⟨n, ρ, hρ, rfl⟩ + rw [alphaLeakageRatio_eq_arimotoSum ha] + exact one_le_arimotoSum ha.le + +end LogForm + +end InformationTheory diff --git a/Statlib/Divergence/AlphaLeakage/Operational.lean b/Statlib/Divergence/AlphaLeakage/Operational.lean new file mode 100644 index 0000000..f3dc42b --- /dev/null +++ b/Statlib/Divergence/AlphaLeakage/Operational.lean @@ -0,0 +1,223 @@ +/- +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.AlphaLeakage.Basic + +/-! +# α-leakage + +Liao, Kosut, Sankar and Calmon (*Tunable measures for information leakage and applications to +privacy-utility tradeoffs*, IEEE Trans. Inf. Theory 65(12), 2019, arXiv:1809.09231) measure how +much an adversary learns about `X` from `Y` through the **α-loss** +`ℓ_a(x, y, P_{X̂|Y}) = a / (a - 1) · (1 - P_{X̂|Y}(x | y) ^ ((a - 1) / a))` of a soft estimator +`P_{X̂|Y}` (their eq. (19)). Minimizing the expected α-loss amounts to maximizing the *gain* +`E[P_{X̂|Y}(X | Y) ^ ((a - 1) / a)]` (their eq. (29)), and the **α-leakage** (their Definition 5) +compares the best gain with and without observing `Y`: +`L_a(X → Y) = a / (a - 1) · log (max_{P_{X̂|Y}} E[P_{X̂|Y}(X | Y) ^ ((a - 1) / a)] / + max_{P_{X̂}} E[P_{X̂}(X) ^ ((a - 1) / a)])`. + +We formalize this operational definition for `a ∈ (1, ∞)` and finite alphabets, and prove their +Theorem 1: α-leakage is the Arimoto mutual information of order `a`. The key step (their +Lemma 1, eqs. (79)–(80)) is Hölder's inequality: over probability vectors `q`, +`∑_x p(x) q(x) ^ ((a - 1) / a)` is maximized by the escort vector `q ∝ p ^ a`, with maximum +`‖p‖_a = (∑_x p(x) ^ a) ^ (1 / a)`. + +## Main definitions + +* `alphaLeakageRatio a π`: the ratio of the best gains, with the suprema taken over all Markov + kernels `P_{X̂|Y}` and all probability measures `P_{X̂}`; in `ℝ≥0∞`. +* `alphaLeakage a π`: the α-leakage `a / (a - 1) · log (alphaLeakageRatio a π)`, in nats. + +## Main statements + +* `sum_mul_rpow_le_rpow_sum`, `sum_mul_rpow_div_eq`: the optimization behind Lemma 1. +* `iSup_lintegral_gain_eq`: **Lemma 1** in multiplicative form: the best gain from observing `Y` + is `∑_y ‖P_{X,Y}(·, y)‖_a`, i.e. `exp ((1 - a) / a · H^A_a(X | Y))`. +* `iSup_lintegral_blindGain_eq`: the best blind gain is `‖P_X‖_a`. +* `alphaLeakageRatio_eq_arimotoSum`, `alphaLeakage_eq_arimotoMI`: **Theorem 1**, + `L_a(X → Y) = I^A_a(X; Y)` for `a ∈ (1, ∞)`. +* `alphaLeakage_nonneg`: α-leakage is nonnegative. + +The endpoint cases `a = 1` (mutual information) and `a = ∞`, which the paper defines by continuous +extension, are not formalized here. +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory +open scoped ENNReal + +namespace InformationTheory + +variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {π : Measure (α × β)} {a : ℝ} + +/-- The multiplicative form of the α-leakage of Definition 5 of Liao–Kosut–Sankar–Calmon: the +ratio of the best expected gain `E[P_{X̂|Y}(X | Y) ^ ((a - 1) / a)]` over all estimators +`P_{X̂|Y}` (Markov kernels `β → α`) observing `Y`, to the best expected gain +`E[P_{X̂}(X) ^ ((a - 1) / a)]` over all blind estimators `P_{X̂}` (probability measures on `α`), +for `(X, Y) ∼ π`. -/ +noncomputable def alphaLeakageRatio (a : ℝ) (π : Measure (α × β)) : ℝ≥0∞ := + (⨆ (g : Kernel β α) (_ : IsMarkovKernel g), ∫⁻ p, g p.2 {p.1} ^ ((a - 1) / a) ∂π) / + ⨆ (q : Measure α) (_ : IsProbabilityMeasure q), ∫⁻ x, q {x} ^ ((a - 1) / a) ∂π.fst + +/-- The **α-leakage** `L_a(X → Y)` of Definition 5 of Liao–Kosut–Sankar–Calmon, for a joint law +`π` of `(X, Y)` and an order `a ∈ (1, ∞)`, in nats: +`a / (a - 1) · log (max_{P_{X̂|Y}} E[P_{X̂|Y}(X | Y) ^ ((a - 1) / a)] / + max_{P_{X̂}} E[P_{X̂}(X) ^ ((a - 1) / a)])`. -/ +noncomputable def alphaLeakage (a : ℝ) (π : Measure (α × β)) : ℝ := + a / (a - 1) * Real.log (alphaLeakageRatio a π).toReal + +section Holder + +variable [Fintype α] + +omit [MeasurableSpace α] in +/-- Hölder's inequality behind Lemma 1 of Liao–Kosut–Sankar–Calmon: for a probability vector +`q`, `∑_x p(x) q(x) ^ ((a - 1) / a) ≤ ‖p‖_a`. -/ +lemma sum_mul_rpow_le_rpow_sum (ha : 1 < a) (p q : α → ℝ≥0∞) (hq : ∑ x, q x = 1) : + ∑ x, p x * q x ^ ((a - 1) / a) ≤ (∑ x, p x ^ a) ^ a⁻¹ := by + have ha0 : 0 < a := zero_lt_one.trans ha + have hb : 1 - a⁻¹ ≠ 0 := (sub_pos.2 (inv_lt_one_of_one_lt₀ ha)).ne' + have hpq : a.HolderConjugate (1 - a⁻¹)⁻¹ := by + simpa using Real.HolderConjugate.inv_one_sub_inv (inv_pos.2 ha0) (inv_lt_one_of_one_lt₀ ha) + have hr : (a - 1) / a = 1 - a⁻¹ := by field_simp + calc ∑ x, p x * q x ^ ((a - 1) / a) + ≤ (∑ x, p x ^ a) ^ (1 / a) * + (∑ x, (q x ^ ((a - 1) / a)) ^ (1 - a⁻¹)⁻¹) ^ (1 / (1 - a⁻¹)⁻¹) := + ENNReal.inner_le_Lp_mul_Lq _ _ _ hpq + _ = (∑ x, p x ^ a) ^ a⁻¹ := by + simp_rw [hr, ← ENNReal.rpow_mul, mul_inv_cancel₀ hb, ENNReal.rpow_one, hq, + ENNReal.one_rpow, mul_one, one_div] + +omit [MeasurableSpace α] in +/-- The escort vector `q = p ^ a / ‖p‖_a ^ a` attains equality in `sum_mul_rpow_le_rpow_sum` +(eq. (80) of Liao–Kosut–Sankar–Calmon). -/ +lemma sum_mul_rpow_div_eq (ha : 1 < a) (p : α → ℝ≥0∞) (hp : ∀ x, p x ≠ ∞) + (h0 : ∑ x, p x ^ a ≠ 0) : + ∑ x, p x * (p x ^ a / ∑ x', p x' ^ a) ^ ((a - 1) / a) = (∑ x, p x ^ a) ^ a⁻¹ := by + set S := ∑ x', p x' ^ a + have ha0 : 0 < a := zero_lt_one.trans ha + have hr0 : 0 ≤ (a - 1) / a := div_nonneg (by linarith) ha0.le + have hS : S ≠ ∞ := ENNReal.sum_ne_top.2 fun x _ ↦ ENNReal.rpow_ne_top_of_nonneg ha0.le (hp x) + have hmul : a * ((a - 1) / a) = a - 1 := by field_simp + have h_term (x : α) : p x * (p x ^ a / S) ^ ((a - 1) / a) = p x ^ a / S ^ ((a - 1) / a) := by + rw [ENNReal.div_rpow_of_nonneg _ _ hr0, ← ENNReal.rpow_mul, hmul, ← mul_div_assoc] + congr 1 + conv_rhs => rw [← sub_add_cancel a 1] + rw [ENNReal.rpow_add_of_nonneg _ _ (by linarith) zero_le_one, ENNReal.rpow_one, mul_comm] + simp_rw [h_term, ← ENNReal.sum_div] + calc S / S ^ ((a - 1) / a) = S ^ (1 : ℝ) / S ^ ((a - 1) / a) := by rw [ENNReal.rpow_one] + _ = S ^ (1 - (a - 1) / a) := (ENNReal.rpow_sub _ _ h0 hS).symm + _ = S ^ a⁻¹ := by + congr 1 + field_simp + ring + +end Holder + +section Gain + +variable [Fintype α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] + +lemma lintegral_alphaGain_eq_sum (π : Measure (α × β)) (g : Kernel β α) : + ∫⁻ p, g p.2 {p.1} ^ ((a - 1) / a) ∂π = ∑ y, ∑ x, π {(x, y)} * g y {x} ^ ((a - 1) / a) := by + rw [lintegral_fintype, Fintype.sum_prod_type, Finset.sum_comm] + simp_rw [mul_comm] + +/-- **Lemma 1 of Liao–Kosut–Sankar–Calmon**, multiplicative form: for `a ∈ (1, ∞)`, the best +expected gain `max_{P_{X̂|Y}} E[P_{X̂|Y}(X | Y) ^ ((a - 1) / a)]` is +`∑_y ‖P_{X,Y}(·, y)‖_a`. The gain identity holds for any finite measure `π`. When `π` is a +probability measure, this equals `exp ((1 - a) / a · H^A_a(X | Y))`, and equivalently the minimal +expected α-loss is `a / (a - 1) · (1 - ∑_y ‖P_{X,Y}(·, y)‖_a)` (eq. (22)), attained by the +estimator `P_{X̂|Y}(x | y) ∝ P_{X|Y}(x | y) ^ a` of eq. (23). -/ +theorem iSup_lintegral_gain_eq (ha : 1 < a) [IsFiniteMeasure π] [Nonempty α] : + (⨆ (g : Kernel β α) (_ : IsMarkovKernel g), ∫⁻ p, g p.2 {p.1} ^ ((a - 1) / a) ∂π) = + ∑ y, (∑ x, π {(x, y)} ^ a) ^ a⁻¹ := by + classical + have ha0 : 0 < a := zero_lt_one.trans ha + refine le_antisymm (iSup₂_le fun g _ ↦ ?_) ?_ + · rw [lintegral_alphaGain_eq_sum] + exact Finset.sum_le_sum fun y _ ↦ + sum_mul_rpow_le_rpow_sum ha _ _ (by simp [sum_measure_singleton]) + -- The optimal estimator: the escort of the column `π (·, y)`, or a point mass if it vanishes. + obtain ⟨x₀⟩ := ‹Nonempty α› + set S : β → ℝ≥0∞ := fun y ↦ ∑ x, π {(x, y)} ^ a + have hS_top (y : β) : S y ≠ ∞ := ENNReal.sum_ne_top.2 fun x _ ↦ + ENNReal.rpow_ne_top_of_nonneg ha0.le (measure_ne_top π _) + set w : β → α → ℝ≥0∞ := fun y x ↦ + if S y = 0 then (if x = x₀ then 1 else 0) else π {(x, y)} ^ a / S y + set g : Kernel β α := Kernel.ofFunOfCountable fun y ↦ ∑ x, w y x • Measure.dirac x + have hg (y : β) (x : α) : g y {x} = w y x := sum_smul_dirac_apply_singleton _ _ + have hw (y : β) : ∑ x, w y x = 1 := by + by_cases hy : S y = 0 + · simp [w, hy] + · simp only [w, hy, ite_false] + rw [← ENNReal.sum_div] + exact ENNReal.div_self hy (hS_top y) + have : IsMarkovKernel g := ⟨fun y ↦ ⟨by + rw [← Finset.coe_univ, ← sum_measure_singleton] + simp_rw [hg, hw]⟩⟩ + refine le_iSup₂_of_le g this (le_of_eq ?_) + rw [lintegral_alphaGain_eq_sum] + refine Finset.sum_congr rfl fun y _ ↦ ?_ + by_cases hy : S y = 0 + · have h0 (x : α) : π {(x, y)} = 0 := + (ENNReal.rpow_eq_zero_iff_of_pos ha0).1 (Finset.sum_eq_zero_iff.1 hy x (Finset.mem_univ x)) + simp only [h0, zero_mul, Finset.sum_const_zero, ENNReal.zero_rpow_of_pos ha0, + ENNReal.zero_rpow_of_pos (inv_pos.2 ha0)] + · simp_rw [hg, w, hy, ite_false] + exact (sum_mul_rpow_div_eq ha _ (fun x ↦ measure_ne_top π _) hy).symm + +omit [Fintype β] [MeasurableSingletonClass β] in +/-- The best blind gain `max_{P_{X̂}} E[P_{X̂}(X) ^ ((a - 1) / a)]` for `X ∼ ρ` is `‖ρ‖_a` +(eq. (87) of Liao–Kosut–Sankar–Calmon). For `ρ ≠ 0` it is attained by the escort distribution +of `ρ`; for `ρ = 0` every probability estimator attains it (when `α` is nonempty). -/ +theorem iSup_lintegral_blindGain_eq (ha : 1 < a) (ρ : Measure α) [IsFiniteMeasure ρ] : + (⨆ (q : Measure α) (_ : IsProbabilityMeasure q), ∫⁻ x, q {x} ^ ((a - 1) / a) ∂ρ) = + (∑ x, ρ {x} ^ a) ^ a⁻¹ := by + have ha0 : 0 < a := zero_lt_one.trans ha + refine le_antisymm (iSup₂_le fun q _ ↦ ?_) ?_ + · rw [lintegral_fintype] + simp_rw [mul_comm] + exact sum_mul_rpow_le_rpow_sum ha _ _ (by simp [sum_measure_singleton]) + by_cases h0 : ∑ x, ρ {x} ^ a = 0 + · simp [h0, ENNReal.zero_rpow_of_pos (inv_pos.2 ha0)] + have hρ : ρ ≠ 0 := by + rintro rfl + simp [ENNReal.zero_rpow_of_pos ha0] at h0 + have := isProbabilityMeasure_escort ha0 hρ + refine le_iSup₂_of_le (escort a ρ) this (le_of_eq ?_) + rw [lintegral_fintype, ← sum_mul_rpow_div_eq ha _ (fun x ↦ measure_ne_top ρ _) h0] + refine Finset.sum_congr rfl fun x _ ↦ ?_ + rw [escort_singleton, mul_comm, ENNReal.div_eq_inv_mul] + +/-- **Theorem 1 of Liao–Kosut–Sankar–Calmon**, multiplicative form: for `a ∈ (1, ∞)`, the ratio of +best gains defining α-leakage is `∑_y ‖P_{X,Y}(·, y)‖_a / ‖P_X‖_a`. -/ +theorem alphaLeakageRatio_eq_arimotoSum (ha : 1 < a) [IsProbabilityMeasure π] : + alphaLeakageRatio a π = arimotoSum a π := by + have : Nonempty α := nonempty_of_isProbabilityMeasure π.fst + rw [alphaLeakageRatio, iSup_lintegral_gain_eq ha, iSup_lintegral_blindGain_eq ha, arimotoSum] + +/-- **Theorem 1 of Liao–Kosut–Sankar–Calmon**: for `a ∈ (1, ∞)`, the α-leakage from `X` to `Y` +is the Arimoto mutual information of order `a`, `L_a(X → Y) = I^A_a(X; Y)`. -/ +theorem alphaLeakage_eq_arimotoMI (ha : 1 < a) [IsProbabilityMeasure π] : + alphaLeakage a π = arimotoMI a π := by + rw [alphaLeakage, arimotoMI, alphaLeakageRatio_eq_arimotoSum ha] + +omit [Fintype α] [Fintype β] in +/-- α-leakage is nonnegative for `a ∈ (1, ∞)`. -/ +lemma alphaLeakage_nonneg [Finite α] [Finite β] (ha : 1 < a) [IsProbabilityMeasure π] : + 0 ≤ alphaLeakage a π := by + have := Fintype.ofFinite α + have := Fintype.ofFinite β + rw [alphaLeakage_eq_arimotoMI ha] + exact arimotoMI_nonneg ha + +end Gain + +end InformationTheory diff --git a/Statlib/Divergence/AlphaLeakage/Properties.lean b/Statlib/Divergence/AlphaLeakage/Properties.lean new file mode 100644 index 0000000..21cd3fa --- /dev/null +++ b/Statlib/Divergence/AlphaLeakage/Properties.lean @@ -0,0 +1,300 @@ +/- +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.AlphaLeakage.Maximal +public import Statlib.Divergence.MaximalLeakage.Properties + +/-! +# Properties of maximal α-leakage + +We prove the properties of maximal α-leakage listed in Theorem 3, eq. (44) and Theorem 4 of +Liao, Kosut, Sankar and Calmon (*Tunable measures for information leakage and applications to +privacy-utility tradeoffs*, IEEE Trans. Inf. Theory 65(12), 2019, arXiv:1809.09231), for +`a ∈ (1, ∞)` and finite alphabets, together with the limit `a → ∞`. All of them go through the +closed form of Theorem 2 (`maxAlphaLeakageRatio_eq_sibsonCapacitySum`). + +## Main statements + +* `maxAlphaLeakage_nonneg`: eq. (42), `L^max_a(X → Y) ≥ 0`. +* `maxAlphaLeakage_eq_zero_of_forall_eq`, `maxAlphaLeakage_eq_zero_of_compProd_eq_prod`: the + "if" direction of the equality case of eq. (42), no leakage under independence. +* `maxAlphaLeakage_le_maxLeakage`: eq. (44), `L^max_a(X → Y) ≤ L_MaxL(X → Y)`. +* `maxAlphaLeakage_le_log_card_input`, `maxAlphaLeakage_le_log_card_support`: eq. (43) for + `a > 1`, `L^max_a(X → Y) ≤ log |X|` (indeed `≤ log |supp P_X|`). +* `maxAlphaLeakage_le_log_card`: Remark 1, `L^max_a(X → Y) ≤ log |Y|`. +* `maxAlphaLeakage_comp_le`: eq. (41a), the post-processing inequality. +* `maxAlphaLeakage_comp_le_comp`: eq. (41b), the linkage inequality. +* `log_sum_rpow_div_le_maxAlphaLeakage`: Theorem 4, the lower bound by the uniform input + (without its equality condition). +* `sibsonMI_le_maxAlphaLeakage`, `alphaLeakage_le_maxAlphaLeakage`: `I^S_a(X̃; Y)` for + `P_X̃ ≪ P_X`, and `L_a(X → Y)`, are lower bounds. +* `tendsto_maxAlphaLeakage_atTop`: `L^max_a(X → Y) → L_MaxL(X → Y)` as `a → ∞`, the case + `α = ∞` of Theorem 2 (eq. (93)). + +Not formalized: quasi-convexity (Theorem 3.1), monotonicity in `a` (Theorem 3.2; eq. (44) is proved +directly instead), the "only if" directions of the equality cases in Theorem 3.4, both +directions of the equality characterization accompanying eq. (43) (only the inequality is +proved), and Theorems 5 and 6 (sub-additivity and additivity). +-/ + +@[expose] public section + +open MeasureTheory ProbabilityTheory Filter +open scoped ENNReal Topology + +namespace InformationTheory + +variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + {mγ : MeasurableSpace γ} {μ ν : Measure α} {κ : Kernel α β} {a : ℝ} + +omit [MeasurableSpace α] in +/-- `r ↦ a / (a - 1) · log r` is monotone on `[1, ∞)` for `a > 1`. -/ +lemma mul_log_toReal_le_mul_log_toReal (ha : 1 < a) {r s : ℝ≥0∞} (hr : 1 ≤ r) (hs : s ≠ ∞) + (hrs : r ≤ s) : a / (a - 1) * Real.log r.toReal ≤ a / (a - 1) * Real.log s.toReal := by + have hr' : 1 ≤ r.toReal := by + simpa using ENNReal.toReal_mono (ne_top_of_le_ne_top hs hrs) hr + exact mul_le_mul_of_nonneg_left (Real.log_le_log (by linarith) (ENNReal.toReal_mono hs hrs)) + (div_nonneg (by linarith) (by linarith)) + +section Bounds + +variable [MeasurableSingletonClass α] [MeasurableSingletonClass β] + +/-- Every `I^S_a(X̃; Y)` with `P_X̃ ≪ P_X` is a lower bound for `L^max_a(X → Y)`. -/ +lemma sibsonMI_le_maxAlphaLeakage [Fintype α] [Fintype β] (ha : 1 < a) + [IsProbabilityMeasure μ] [IsMarkovKernel κ] [IsProbabilityMeasure ν] (hνμ : ν ≪ μ) : + sibsonMI a ν κ ≤ maxAlphaLeakage a μ κ := + mul_log_toReal_le_mul_log_toReal ha (one_le_sibsonSum ha.le) (maxAlphaLeakageRatio_ne_top ha) + (sibsonSum_le_maxAlphaLeakageRatio ha hνμ) + +/-- α-leakage is at most maximal α-leakage: `L_a(X → Y) ≤ L^max_a(X → Y)`. -/ +lemma alphaLeakage_le_maxAlphaLeakage [Finite α] [Finite β] (ha : 1 < a) [IsProbabilityMeasure μ] + [IsMarkovKernel κ] : alphaLeakage a (μ ⊗ₘ κ) ≤ maxAlphaLeakage a μ κ := by + have := Fintype.ofFinite α + have := Fintype.ofFinite β + have ha0 : 0 < a := zero_lt_one.trans ha + have := isProbabilityMeasure_escort (μ := μ) ha0 (IsProbabilityMeasure.ne_zero μ) + rw [alphaLeakage_eq_arimotoMI ha, arimotoMI_compProd ha0.le] + exact sibsonMI_le_maxAlphaLeakage ha (escort_absolutelyContinuous ha0) + +lemma one_le_maxAlphaLeakageRatio [Finite α] [Finite β] (ha : 1 < a) [IsProbabilityMeasure μ] + [IsMarkovKernel κ] : 1 ≤ maxAlphaLeakageRatio a μ κ := + have := Fintype.ofFinite α + have := Fintype.ofFinite β + (one_le_sibsonSum ha.le).trans + (sibsonSum_le_maxAlphaLeakageRatio ha Measure.AbsolutelyContinuous.rfl) + +/-- **Nonnegativity of maximal α-leakage**, eq. (42) of Liao–Kosut–Sankar–Calmon. -/ +lemma maxAlphaLeakage_nonneg [Finite α] [Finite β] (ha : 1 < a) [IsProbabilityMeasure μ] + [IsMarkovKernel κ] : 0 ≤ maxAlphaLeakage a μ κ := + have := Fintype.ofFinite α + have := Fintype.ofFinite β + (sibsonMI_nonneg ha).trans (sibsonMI_le_maxAlphaLeakage ha Measure.AbsolutelyContinuous.rfl) + +omit [MeasurableSingletonClass α] [MeasurableSingletonClass β] in +lemma maxLeakageSum_mono_of_absolutelyContinuous [Fintype β] (hνμ : ν ≪ μ) : + maxLeakageSum ν κ ≤ maxLeakageSum μ κ := + Finset.sum_le_sum fun y _ ↦ iSup₂_le fun x hx ↦ + le_iSup₂ (f := fun x (_ : μ {x} ≠ 0) ↦ κ x {y}) x fun h ↦ hx (hνμ h) + +/-- Multiplicative form of `maxAlphaLeakage_le_maxLeakage`. -/ +lemma maxAlphaLeakageRatio_le_maxLeakageSum_rpow [Finite α] [Fintype β] (ha : 1 < a) + [IsProbabilityMeasure μ] [IsMarkovKernel κ] : + maxAlphaLeakageRatio a μ κ ≤ maxLeakageSum μ κ ^ (1 - a⁻¹) := by + have := Fintype.ofFinite α + have hb : 0 ≤ 1 - a⁻¹ := sub_nonneg.2 (inv_le_one_of_one_le₀ ha.le) + rw [maxAlphaLeakageRatio_eq_sibsonCapacitySum ha] + refine iSup₂_le fun ν _ ↦ iSup_le fun hνμ ↦ ?_ + exact (sibsonSum_le_maxLeakageSum_rpow ha).trans + (ENNReal.rpow_le_rpow (maxLeakageSum_mono_of_absolutelyContinuous hνμ) hb) + +/-- **Maximal α-leakage is at most maximal leakage**, eq. (44) of Liao–Kosut–Sankar–Calmon: +`L^max_a(X → Y) ≤ L_MaxL(X → Y) = I^S_∞(X; Y)` for `a ∈ (1, ∞)`. The paper derives it from the +monotonicity of `L^max_a` in `a`; here it follows from Hölder's inequality +(`sibsonSum_le_maxLeakageSum_rpow`). -/ +theorem maxAlphaLeakage_le_maxLeakage [Finite α] [Fintype β] (ha : 1 < a) + [IsProbabilityMeasure μ] [IsMarkovKernel κ] : maxAlphaLeakage a μ κ ≤ maxLeakage μ κ := by + have := Fintype.ofFinite α + have ha0 : 0 < a := zero_lt_one.trans ha + have hb : 0 < 1 - a⁻¹ := sub_pos.2 (inv_lt_one_of_one_lt₀ ha) + obtain ⟨x, hx⟩ : ∃ x, μ {x} ≠ 0 := by + by_contra! h + have := sum_measure_singleton (μ := μ) (s := Finset.univ) + simp [h] at this + have hL := one_le_toReal_maxLeakageSum (κ := κ) hx + have h_le : (maxAlphaLeakageRatio a μ κ).toReal ≤ (maxLeakageSum μ κ).toReal ^ (1 - a⁻¹) := by + rw [ENNReal.toReal_rpow] + exact ENNReal.toReal_mono (ENNReal.rpow_ne_top_of_nonneg hb.le maxLeakageSum_ne_top) + (maxAlphaLeakageRatio_le_maxLeakageSum_rpow ha) + have h1 : 1 ≤ (maxAlphaLeakageRatio a μ κ).toReal := by + simpa using ENNReal.toReal_mono (maxAlphaLeakageRatio_ne_top ha) + (one_le_maxAlphaLeakageRatio (μ := μ) (κ := κ) ha) + have h_log := Real.log_le_log (by linarith) h_le + rw [Real.log_rpow (by linarith)] at h_log + calc maxAlphaLeakage a μ κ ≤ a / (a - 1) * ((1 - a⁻¹) * Real.log (maxLeakageSum μ κ).toReal) := + mul_le_mul_of_nonneg_left h_log (div_nonneg ha0.le (by linarith)) + _ = maxLeakage μ κ := by + rw [maxLeakage, ← mul_assoc] + convert one_mul _ using 2 + field_simp + +/-- `L^max_a(X → Y) ≤ log |Y|` (Remark 1 of Liao–Kosut–Sankar–Calmon). -/ +lemma maxAlphaLeakage_le_log_card [Finite α] [Fintype β] (ha : 1 < a) [IsProbabilityMeasure μ] + [IsMarkovKernel κ] : maxAlphaLeakage a μ κ ≤ Real.log (Fintype.card β) := 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 + exact (maxAlphaLeakage_le_maxLeakage ha).trans (maxLeakage_le_log_card hx) + +/-- `L^max_a(X → Y) ≤ log |supp P_X|`, the inequality of eq. (43) of Liao–Kosut–Sankar–Calmon +for `a > 1`; its equality characterization is not formalized (the paper +states it with `|X|` for a fully supported `P_X`; see `maxAlphaLeakage_le_log_card_input`). -/ +theorem maxAlphaLeakage_le_log_card_support [Fintype α] [Finite β] (ha : 1 < a) + [IsProbabilityMeasure μ] [IsMarkovKernel κ] [DecidablePred fun x : α ↦ μ {x} ≠ 0] : + maxAlphaLeakage a μ κ ≤ Real.log (Finset.univ.filter fun x : α ↦ μ {x} ≠ 0).card := 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 (maxAlphaLeakage_le_maxLeakage ha).trans + (Real.log_le_log (by linarith [one_le_toReal_maxLeakageSum (κ := κ) hx]) ?_) + simpa using ENNReal.toReal_mono (ENNReal.natCast_ne_top _) maxLeakageSum_le_card_support + +/-- `L^max_a(X → Y) ≤ log |X|`, eq. (43) of Liao–Kosut–Sankar–Calmon for `a > 1`. -/ +theorem maxAlphaLeakage_le_log_card_input [Fintype α] [Finite β] (ha : 1 < a) + [IsProbabilityMeasure μ] [IsMarkovKernel κ] : + maxAlphaLeakage a μ κ ≤ Real.log (Fintype.card α) := by + classical + refine (maxAlphaLeakage_le_log_card_support ha).trans (Real.log_le_log ?_ ?_) + · obtain ⟨x, hx⟩ : ∃ x, μ {x} ≠ 0 := by + by_contra! h + have := sum_measure_singleton (μ := μ) (s := Finset.univ) + simp [h] at this + exact_mod_cast Finset.card_pos.2 ⟨x, by simpa using hx⟩ + · exact_mod_cast Finset.card_filter_le _ _ + +/-- **Theorem 4 of Liao–Kosut–Sankar–Calmon** (lower bound, without its equality condition): for a +fully supported `P_X` and `a ∈ (1, ∞)`, +`L^max_a(X → Y) ≥ a / (a - 1) · log (∑_y ‖P_{Y|X}(y | ·)‖_a / |X| ^ (1 / a))`, +the Sibson mutual information at the uniform input. -/ +theorem log_sum_rpow_div_le_maxAlphaLeakage [Fintype α] [Fintype β] (ha : 1 < a) + [IsProbabilityMeasure μ] [IsMarkovKernel κ] (hμ : ∀ x, μ {x} ≠ 0) : + a / (a - 1) * Real.log ((∑ y, (∑ x, κ x {y} ^ a) ^ a⁻¹) / + (Fintype.card α : ℝ≥0∞) ^ a⁻¹).toReal ≤ maxAlphaLeakage a μ κ := by + have ha0 : 0 < a := zero_lt_one.trans ha + have : Nonempty α := nonempty_of_isProbabilityMeasure μ + set N : ℝ≥0∞ := (Fintype.card α : ℝ≥0∞) + have hN0 : N ≠ 0 := by simp [N] + have hNtop : N ≠ ∞ := ENNReal.natCast_ne_top _ + set ν : Measure α := ∑ x, N⁻¹ • Measure.dirac x + have hν (x : α) : ν {x} = N⁻¹ := sum_smul_dirac_apply_singleton (fun _ ↦ N⁻¹) x + have : IsProbabilityMeasure ν := ⟨by + rw [← Finset.coe_univ, ← sum_measure_singleton] + simp_rw [hν, Finset.sum_const, Finset.card_univ, nsmul_eq_mul] + exact ENNReal.mul_inv_cancel hN0 hNtop⟩ + have hνμ : ν ≪ μ := fun s hs ↦ (measure_null_iff_singleton s.to_countable).2 fun x hx ↦ + absurd ((measure_null_iff_singleton s.to_countable).1 hs x hx) (hμ x) + have h_eq : sibsonSum a ν κ = (∑ y, (∑ x, κ x {y} ^ a) ^ a⁻¹) / N ^ a⁻¹ := by + simp_rw [sibsonSum, hν, ← Finset.mul_sum, ENNReal.mul_rpow_of_nonneg _ _ (inv_nonneg.2 ha0.le), + ENNReal.inv_rpow, ← Finset.mul_sum, ENNReal.div_eq_inv_mul] + rw [← h_eq] + exact sibsonMI_le_maxAlphaLeakage ha hνμ + +end Bounds + +section DataProcessing + +variable [Finite α] [MeasurableSingletonClass α] [Finite β] [MeasurableSingletonClass β] + [Finite γ] [MeasurableSingletonClass γ] + +/-- Multiplicative form of `maxAlphaLeakage_comp_le`. -/ +lemma maxAlphaLeakageRatio_comp_le (ha : 1 < a) [IsProbabilityMeasure μ] [IsMarkovKernel κ] + (η : Kernel β γ) [IsMarkovKernel η] : + maxAlphaLeakageRatio a μ (η ∘ₖ κ) ≤ maxAlphaLeakageRatio a μ κ := by + have := Fintype.ofFinite α + have := Fintype.ofFinite β + have := Fintype.ofFinite γ + rw [maxAlphaLeakageRatio_eq_sibsonCapacitySum ha, maxAlphaLeakageRatio_eq_sibsonCapacitySum ha] + exact iSup₂_le fun ν hν ↦ iSup_le fun hνμ ↦ + (sibsonSum_comp_le ha.le η).trans (le_iSup₂_of_le ν hν (le_iSup_of_le hνμ le_rfl)) + +/-- **Post-processing inequality**, eq. (41a) of Liao–Kosut–Sankar–Calmon (Theorem 3.3): for a +Markov chain `X - Y - Z`, `L^max_a(X → Z) ≤ L^max_a(X → Y)`. -/ +theorem maxAlphaLeakage_comp_le (ha : 1 < a) [IsProbabilityMeasure μ] [IsMarkovKernel κ] + (η : Kernel β γ) [IsMarkovKernel η] : + maxAlphaLeakage a μ (η ∘ₖ κ) ≤ maxAlphaLeakage a μ κ := by + have := Fintype.ofFinite α + have := Fintype.ofFinite β + have := Fintype.ofFinite γ + exact mul_log_toReal_le_mul_log_toReal ha (one_le_maxAlphaLeakageRatio ha) + (maxAlphaLeakageRatio_ne_top ha) (maxAlphaLeakageRatio_comp_le ha η) + +/-- Multiplicative form of `maxAlphaLeakage_comp_le_comp`. -/ +lemma maxAlphaLeakageRatio_comp_le_comp (ha : 1 < a) [IsProbabilityMeasure μ] [IsMarkovKernel κ] + (η : Kernel β γ) [IsMarkovKernel η] : + maxAlphaLeakageRatio a μ (η ∘ₖ κ) ≤ maxAlphaLeakageRatio a (κ ∘ₘ μ) η := by + have := Fintype.ofFinite α + have := Fintype.ofFinite β + have := Fintype.ofFinite γ + rw [maxAlphaLeakageRatio_eq_sibsonCapacitySum ha, maxAlphaLeakageRatio_eq_sibsonCapacitySum ha] + refine iSup₂_le fun ν hν ↦ iSup_le fun hνμ ↦ (sibsonSum_comp_le_comp ha.le η).trans ?_ + exact le_iSup₂_of_le (κ ∘ₘ ν) inferInstance (le_iSup_of_le + (hνμ.comp (ae_of_all _ fun _ ↦ Measure.AbsolutelyContinuous.rfl)) le_rfl) + +/-- **Linkage inequality**, eq. (41b) of Liao–Kosut–Sankar–Calmon (Theorem 3.3): for a Markov +chain `X - Y - Z`, `L^max_a(X → Z) ≤ L^max_a(Y → Z)`, where `Y ∼ κ ∘ₘ μ`. -/ +theorem maxAlphaLeakage_comp_le_comp (ha : 1 < a) [IsProbabilityMeasure μ] [IsMarkovKernel κ] + (η : Kernel β γ) [IsMarkovKernel η] : + maxAlphaLeakage a μ (η ∘ₖ κ) ≤ maxAlphaLeakage a (κ ∘ₘ μ) η := by + have := Fintype.ofFinite α + have := Fintype.ofFinite β + have := Fintype.ofFinite γ + exact mul_log_toReal_le_mul_log_toReal ha (one_le_maxAlphaLeakageRatio ha) + (maxAlphaLeakageRatio_ne_top ha) (maxAlphaLeakageRatio_comp_le_comp ha η) + +end DataProcessing + +section Limit + +variable [Finite α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] + +/-- **Maximal α-leakage of order `∞` is maximal leakage**: as `a → ∞`, `L^max_a(X → Y)` tends to +`L_MaxL(X → Y) = log ∑_y max_{x ∈ supp P_X} P_{Y|X}(y | x)`. This is the case `α = ∞` of Theorem 2 +of Liao–Kosut–Sankar–Calmon (eqs. (31a) and (93)), where `L^max_∞` is defined by continuous +extension. -/ +theorem tendsto_maxAlphaLeakage_atTop [Fintype β] [IsProbabilityMeasure μ] [IsMarkovKernel κ] : + Tendsto (fun a ↦ maxAlphaLeakage a μ κ) atTop (𝓝 (maxLeakage μ κ)) := by + have := Fintype.ofFinite α + exact tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_sibsonMI_atTop tendsto_const_nhds + ((eventually_gt_atTop 1).mono fun _ ha ↦ + sibsonMI_le_maxAlphaLeakage ha Measure.AbsolutelyContinuous.rfl) + ((eventually_gt_atTop 1).mono fun _ ha ↦ maxAlphaLeakage_le_maxLeakage ha) + +/-- **No leakage under independence** (the "if" direction of the equality case of eq. (42) of +Liao–Kosut–Sankar–Calmon): if the rows of the channel coincide on the support of `P_X`, i.e. `X` +and `Y` are independent, then `L^max_a(X → Y) = 0`. The converse is not formalized here. -/ +theorem maxAlphaLeakage_eq_zero_of_forall_eq [Finite β] (ha : 1 < a) [IsProbabilityMeasure μ] + [IsMarkovKernel κ] (h : ∀ x x', μ {x} ≠ 0 → μ {x'} ≠ 0 → κ x = κ x') : + maxAlphaLeakage a μ κ = 0 := by + have := Fintype.ofFinite β + exact le_antisymm ((maxAlphaLeakage_le_maxLeakage ha).trans (maxLeakage_eq_zero_iff.2 h).le) + (maxAlphaLeakage_nonneg ha) + +/-- **No leakage under independence**: if `μ ⊗ₘ κ = μ × (κ ∘ₘ μ)`, then `L^max_a(X → Y) = 0`. -/ +theorem maxAlphaLeakage_eq_zero_of_compProd_eq_prod [Finite β] (ha : 1 < a) + [IsProbabilityMeasure μ] [IsMarkovKernel κ] (h : μ ⊗ₘ κ = μ.prod (κ ∘ₘ μ)) : + maxAlphaLeakage a μ κ = 0 := by + have := Fintype.ofFinite β + exact maxAlphaLeakage_eq_zero_of_forall_eq ha + (maxLeakage_eq_zero_iff.1 (maxLeakage_eq_zero_iff_compProd_eq_prod.2 h)) + +end Limit + +end InformationTheory 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